Re: [isabelle] Isabelle help
On Saturday 20 October 2007, RF Todd wrote:
> I am stuck with the following:
> theorem 211: "(l \<noteq> m) \<Longrightarrow> ((\<exists>P. (incident
> l P \<and> incident m P)) \<or> \<not>(\<exists>P. (incident l P
> \<and> incident m P)))"
> apply simp
> I am stuck with how to prove this. If you do 'simp' it simplifies it
> but then i cannot get rid of the /<or> on the RHS of the arrow without
> applying the rules 'disjI1' or 'disjI2' which just removes half of the
You could also try using the rule 'disjCI', which doesn't remove anything - it
just moves the negation of one disjunct into the premises:
assumes "~Q ==> P" shows "P|Q"
This archive was generated by a fusion of
Pipermail (Mailman edition) and