Time 
Nick 
Message 
01:48 

ilbot3 joined #isabelle 
01:48 

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/ 
01:55 

dmiles joined #isabelle 
02:34 

keep_learning joined #isabelle 
13:45 

w_ joined #isabelle 
13:45 
w_ 
hey 
13:45 
w_ 
anyone here? 
13:45 
w_ 
I'm having trouble proving a really simple lemma 
13:45 
w_ 
" ∀j<i. P j ⟹ P i ⟹ ∀j≤i. P j " 
13:45 
w_ 
can't figure out how to prove it 
13:46 
w_ 
try0 says no proof found... 
13:47 
w_ 
oh nvm 
13:47 
w_ 
try worked 
13:50 

silver joined #isabelle 
14:00 
JCaesar 
:) 
17:35 
chindy 
Anyone know if there are any theories specifically for correspondences/set valued functions ? 
17:37 
inte 
I don't know. I'd consider treating such a thing as a relation. 
17:46 
inte 
since they're isomorphic: http://downthetypehole.de/paste/BFOV9mIA 
18:51 
w_ 
does anyone know how to get min to return a nat? 
18:51 
w_ 
I've got r = (int min {(j::nat) . A!j = m}) 
18:51 
w_ 
but it fails 
18:51 
w_ 
Type unification failed: Clash of types "_ ⇒ _" and "nat" 
18:51 
w_ 
Type error in application: incompatible operand type 
18:51 
w_ 
Operator: int :: nat ⇒ int 
18:51 
w_ 
Operand: min :: ??'a ⇒ ??'a ⇒ ??'a 
18:52 
w_ 
in this case isabelle should know that min should return a nat, right? 
18:52 
w_ 
since I specified (j::nat) 
18:57 
ammbauer 
w_: min is for taking the minimum of two values. you want to use "Min" 
18:58 
w_ 
aha got it 
18:58 
w_ 
thank you very much 
19:28 

Merv_ joined #isabelle 
19:33 
chindy 
w_: also as a side node i blieve the argument of Min must be countable or foldable 
20:14 
larsrh 
we need an isabellebot 
20:15 
larsrh 
! type "Min" or something 
21:10 
chindy 
+1 
21:28 

Merv joined #isabelle 
22:04 

inte joined #isabelle 
22:36 
pruvisto 
larsrh: cool, maybe you should bring up that idea with the developer of libisabelle 
22:37 
pruvisto 
also, chindy, no it doesn't 
22:37 
pruvisto 
it just needs a linorder 
22:37 
pruvisto 
but for infinite sets, "Min" is essentially undefined 
22:38 
pruvisto 
for infinite sets, one can use "Inf", which requires some more structure on the type (semilattice probably) 
22:45 
chindy 
pruvisto: thats what i mean... i just remember wondering why max wouldnt work on an inifite set... 
22:53 
pruvisto 
Because there may not exist a maximum in an infinite set 
22:54 
pruvisto 
well, a minimum 
22:55 
pruvisto 
I guess one could have defined "Min" such that it always returns a minimum whenever there exists one 
22:55 
pruvisto 
but I think in those cases you would normally rather use "Inf" anyway 