# IRC log for #isabelle, 2017-09-15

All times shown according to UTC.

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 int-e . o O ( lemma "¬(∀x. P x) ⟷ (∃x. ¬P x)" by (rule not_all) )
11:22 int-e (it seems strange to state a lemma that is an instance of another one)
11:24 int-e 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