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 
inte 
the first lemma is wrong? 
15:39 
inte 
(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 
inte: Ah yes, I see, not sure how that got through the typechecker.... 
16:56 
inte 
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 [] 