Re: [isabelle] Isabelle help



Hi Rachel,

Thanks for that. I have created a rule which i am trying to use in the proof of theorem 211. The rule is

axiom1b: "(P /<noteq> Q) /<Longrightarrow> ((/<exists> l. (incident P l /<and> incident Q l)) /<or> /<not>(/<exists> l. (incident P l /<and> incident Q l)))"

Hmm, I don't see what you'd need this axiom for, because it is also an instance of the tautology "A \<or> \<not> A". Furthermore, this theorem does not unify with the formula of theorem 211 as here P and Q are different, while in 211, l and m are different.

However, in general you could use such a theorem with tactics like rule, drule, erule, and frule. I guess you are already working (have worked) through the examples in the Isabelle/HOL tutorial. If not, see:

http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf

best regards,
Simon





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.