Time 
Nick 
Message 
00:22 

keep_learning joined #isabelle 
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/ 
04:25 

aindilis` joined #isabelle 
09:13 

aindilis joined #isabelle 
09:17 
chindy 
inte: i managed to proof it now... for some reason it needed 2 aux lemmas where Isabelle tells me in both that they are useless since they can be solved directly :/ 
13:11 
inte 
I wonder whether this lemma exists anywhere else... http://downthetypehole.de/paste/lwcLxb0e 
13:13 
inte 
(woops, not sure why the "using" before "proof " was there) 
15:10 
pruvisto 
inte: you can probably use this: infinite_arbitrarily_large 
15:11 
pruvisto 
that will give you a finite subset of B with the same cardinality as A 
15:11 
pruvisto 
and then you can use e.g. finite_same_card_bij to get a bijection between A and that subset of B 
15:12 
pruvisto 
but that precise lemma apparently does not exist yet, no 
15:12 
pruvisto 
and I suppose your proof is just as simple 
15:12 
inte 
sounds about ... right I was going to say something to that effect 
18:43 
inte 
I love metis. Metis knows about the axiom of choice (because it's the basis for skolemization...) 
18:45 
inte 
Basically if you ever find yourself in need of a witness function (e.g., you have !x. ?y. P x y, and you want to obtain an f such that !x. P x (f x)), then metis is your best friend. 
19:43 

stoopkid_ joined #isabelle 
19:57 
pruvisto 
or use choice_iff 
19:57 
pruvisto 
thats what i always do 
19:58 
pruvisto 
metis is probably good at it because it does skolemisation anyway 
19:59 
inte 
seems tedious if you have several universal quantifiers to take care of 
20:00 
inte 
(hmm, actually I would have to experiment a bit with choice_iff; it may just work) 
20:03 
inte 
(oh and I actually had a metalevel quantifier in place of !) 
20:28 
pruvisto 
yeah well those are interchangeable 
20:28 
pruvisto 
I mean, sure, use metis if it works ^^ 