Time 
Nick 
Message 
00:38 
chindy 
is there a standard way of limiting the set real to all reals >0 ? 
02:47 

ilbot3 joined #isabelle 
02:47 

Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html  Now with logging: http://irclog.perlgeek.de/isabelle/ 
07:13 
pruvisto 
chindy: {x. x > 0} 
11:36 

silver joined #isabelle 
12:01 

cic joined #isabelle 
15:36 

ammbauer joined #isabelle 
17:26 
chindy 
how do i specify a set of all elements of type: For example for showing total_on as an example: "total_on_nat Rel ⟷ (total_on (Nats::nat) (Rel:: nat * nat))". where i intend to show that Rel is total on Natural numbers 
17:47 
ammbauer 
chindy: use UNIV. 
17:47 
ammbauer 
"total_on_nat Rel <> total_on UNIV (Rel::nat rel)" 
17:47 
ammbauer 
or with fancy abbreviation "total_on_nat Rel <> total (Rel::nat rel)" 
18:06 
chindy 
so "let s = UNIV (X::real set) in" .... lets s be a set of all elements e taht are element of real ? 
18:07 

silver_ joined #isabelle 
18:08 
inte 
UNIV :: real set is the set of all real numbers. 
18:11 

ertesx joined #isabelle 
18:12 
inte 
note: lemma "{x. True} = UNIV" by simp 
18:19 
chindy 
ah thx 
20:47 
JCaesar 
btw, the statement 'element of real' doesn't really make sense in Isabelle/HOL… 
20:48 
pruvisto 
Well, there is the constant "ℝ", which is the set of all real numbers 
20:49 
pruvisto 
but it only makes sense as a subset of a real algebra 
20:49 
pruvisto 
e.g. you can have "ℝ :: complex" 
20:49 
pruvisto 
the set of all real numbers, viewed as a subset of the complex numbers 
21:22 
chindy 
pruvisto: thanks, but I think in my case it made sense as i had a (real, real) set and needed it to be total, which needs a set so "total_on (UNIV :: real set) relation" is probably the way to go 
21:52 

wagle joined #isabelle 
23:35 

stoopkid joined #isabelle 