# IRC log for #isabelle, 2011-12-23

All times shown according to UTC.

Time Nick Message
05:13 eyebloom joined #isabelle
14:24 eyebloom joined #isabelle
14:33 eyebloom Just a toy problem I'm having trouble prooving:
14:34 eyebloom primrec contain :: "'a => 'a list => bool" where
14:34 eyebloom "contain b [] = False" |
14:34 eyebloom "contain b (a # l) = ((a = b) \or (contain b l))"
14:34 eyebloom primrec containsAll :: "'a list => 'a list => bool" where
14:34 eyebloom "containsAll []      l = True" |
14:34 eyebloom "containsAll (a # b) l = (contain a l \and containsAll b l)"
14:34 eyebloom lemma [simp]: "\<forall> l. contain [] l"
14:34 eyebloom lemma "containsAll c [] ==> c = []"
15:17 larsrh eyebloom: your first lemma doesn't need the `\<forall>`
15:17 larsrh free variables are universally quantified (roughly)
15:18 larsrh and I'd say the second one should go through via case distinction
15:39 int-e the first lemma is wrong?
15:39 int-e (contain should be containsAll there)
16:35 eyebloom joined #isabelle
16:46 eyebloom The second lemma basically says that if an empty list contains all the elements in another list the other list must also be empty.
16:54 eyebloom int-e: Ah yes, I see, not sure how that got through the typechecker....
16:56 int-e l  would have type  ('a list) list  then
16:56 eyebloom Ok, thanks, that lemma turns into the stated rule then basically.
16:57 eyebloom I still think the second one is true but haven't prooved it yet.
17:00 eyebloom I think I have to generalize the []