Email Gateway (Aug 19 2022 at 17:08): Email Gateway (Aug 19 2022 at 17:08):From: mahmoud abdelazim <m.abdelazim@icloud.com>
Does exists a modus tollens rule in isabelle?
Email Gateway (Aug 19 2022 at 17:08):From: Peter Lammich <lammich@in.tum.de>
You may try
HOL.contrapos_nn: ⟦¬ ?Q; ?P ⟹ ?Q⟧ ⟹ ¬ ?P
or just prove the rule you need "by blast"
Email Gateway (Aug 19 2022 at 17:08):From: Alfio Martini <alfio.martini@acm.org>
Hi Mahmoud,
Like Peter mentioned, you can prove it if you want. There are many ways.
Two of them are shown below:
theorem mt:
assumes mj: "A⟶B" and mi: "¬B"
shows "¬A" using mj and mi by simp
theorem mt2:
assumes mj: "A⟶B" and mi: "¬B"
shows "¬A"
proof (rule notI)
assume A
from mj and this have B by (rule mp)
from mi and this show False by (rule notE)
qed
Best!
Last updated: Apr 26 2024 at 01:06 UTC