Email Gateway (Aug 18 2022 at 10:54): Email Gateway (Aug 18 2022 at 10:54):From: RF Todd <R.F.Todd@sms.ed.ac.uk>
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.
I wonder if you can give me any advice?
Rachel
----- End forwarded message -----
Email Gateway (Aug 18 2022 at 10:54):From: Amine Chaieb <chaieb@in.tum.de>
Hi,
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)))"
by blast
Amine.
Email Gateway (Aug 18 2022 at 10:54):From: Brian Huffman <brianh@cs.pdx.edu>
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"
Email Gateway (Aug 18 2022 at 10:55):From: Simon Meier <simon.meier@inf.ethz.ch>
Hi Rachel,
your theorem is actually nothing else than an instance of the tautology
"A \<or> \<not> A".
A step by step proof would look as follows:
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(case_tac "(\<exists>P. incident l P \<and> incident m P)")
apply(rule disjI1)
apply(assumption)
apply(rule disjI2)
apply(assumption)
done
The assumption that "l \<noteq> m" is actually not needed. Furthermore,
classical reasoning is done for example by the tactics blast and auto.
They solve your problem at once:
theorem modified_211: "((\<exists>P. (incident
l P \<and> incident m P)) \<or> \<not>(\<exists>P. (incident l P
\<and> incident m P)))"
apply(auto)
done
Have fun,
Simon
Email Gateway (Aug 18 2022 at 10:55):From: Simon Meier <simon.meier@inf.ethz.ch>
Hi Rachel,
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
Last updated: May 03 2024 at 08:18 UTC