Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] disjCI2

Email Gateway (Aug 22 2022 at 20:30):

From: "Fernandez, Matthew" <matthew.fernandez@intel.com>

-----Original Message-----
From: cl-isabelle-users-bounces@lists.cam.ac.uk [mailto:cl-isabelle-users-
bounces@lists.cam.ac.uk] On Behalf Of Alexander Krauss
Sent: Monday, September 30, 2019 00:44
To: cl-isabelle-users@lists.cam.ac.uk
Subject: [isabelle] disjCI2

Hi all,

HOL has the following classical introduction rule for disjunction:

disjCI: (¬ ?Q ⟹ ?P) ⟹ ?P ∨ ?Q

I sometimes miss the following symmetric rule:

disjCI2: (¬ ?P ⟹ ?Q) ⟹ ?P ∨ ?Q

Any thoughts on adding this rule? Are there good alternatives in situations
like this:

have "P ∨ Q"
proof (rule disjCI2)
assume "¬ P"
show "Q"
sorry

qed

I wouldn't say it's a good alternative, but here is another spelling of disjCI2:

have "P ∨ Q"
proof (rule Meson.disj_comm[OF disjCI])
assume "¬P"
show "Q"
sorry

Alex

Email Gateway (Aug 22 2022 at 20:40):

From: Alexander Krauss <krauss@in.tum.de>
Hi all,

HOL has the following classical introduction rule for disjunction:

disjCI: (¬ ?Q ⟹ ?P) ⟹ ?P ∨ ?Q

I sometimes miss the following symmetric rule:

disjCI2: (¬ ?P ⟹ ?Q) ⟹ ?P ∨ ?Q

Any thoughts on adding this rule? Are there good alternatives in
situations like this:

have "P ∨ Q"
proof (rule disjCI2)
assume "¬ P"
show "Q"
sorry

qed

Alex

Last updated: Feb 01 2025 at 20:19 UTC