# IRC log for #isabelle, 2017-07-20

All times shown according to UTC.

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 int-e: 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 int-e I wonder whether this lemma exists anywhere else... http://downthetypehole.de/paste/lwcLxb0e
13:13 int-e (woops, not sure why the "using" before "proof -" was there)
15:10 pruvisto int-e: 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 int-e sounds about ... right I was going to say something to that effect
18:43 int-e I love metis. Metis knows about the axiom of choice (because it's the basis for skolemization...)
18:45 int-e 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 int-e seems tedious if you have several universal quantifiers to take care of
20:00 int-e (hmm, actually I would have to experiment a bit with choice_iff; it may just work)
20:03 int-e (oh and I actually had a meta-level quantifier in place of !)
20:28 pruvisto yeah well those are interchangeable
20:28 pruvisto I mean, sure, use metis if it works ^^