Re: [isabelle] Isabelle help

On Saturday 20 October 2007, RF Todd wrote:
> Hi,
> 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
> equation.

You could also try using the rule 'disjCI', which doesn't remove anything - it 
just moves the negation of one disjunct into the premises:

lemma disjCI:
  assumes "~Q ==> P" shows "P|Q"

- Brian

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