Time 
Nick 
Message 
01:54 

ilbot3 joined #isabelle 
01:54 

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/ 
09:56 
qertyyyy 
hi, I want to proof this: 
09:56 
qertyyyy 
lemma "(¬(∀ xs. (optPenu xs = None) ∨ (the (optPenu xs)) ∈ set xs)) = (∃ xs. ¬((optPenu xs = None) ∨ (the (optPenu xs)) ∈ set xs))" 
09:56 
qertyyyy 
where optPenu is defined like this 
09:56 
qertyyyy 
fun optPenu :: "'a list ⇒ 'a option" where 
09:56 
qertyyyy 
"optPenu [] = None" 
09:56 
qertyyyy 
"optPenu [x] = None" 
09:56 
qertyyyy 
"optPenu [x,y] = Some x" 
09:56 
qertyyyy 
"optPenu (x#xs) = optPenu xs" 
09:57 
qertyyyy 
usually this should wirk with simp or subst not_all , rule refl 
09:57 
qertyyyy 
by I seems to miss something , since this does not work .... 
10:45 
ammbauer 
you have to "help" isabelle with some type annotations: 
10:45 
ammbauer 
(¬(∀ (xs::'a list). (optPenu xs = None) ∨ (the (optPenu xs)) ∈ set xs)) = (∃(xs::'a list). ¬((optPenu xs = None) ∨ (the (optPenu xs)) ∈ set xs)) 
11:21 
inte 
. o O ( lemma "¬(∀x. P x) ⟷ (∃x. ¬P x)" by (rule not_all) ) 
11:22 
inte 
(it seems strange to state a lemma that is an instance of another one) 
11:24 
inte 
Note that in this case, the type problem doesn't occur because the type of "P" connects the types of the two "x"; it's monomorphic. 
15:55 

stoopkid__ joined #isabelle 