Email Gateway (Aug 19 2022 at 13:15): Email Gateway (Aug 19 2022 at 13:15):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Hello boys'n girls,
I may have missed it in the big Isar‑Ref or else it's just indeed missing:
is there a proof method to show a disjunction is True choosing to prove
one of its element is True and to show a conjunction is False choosing to
prove one of its element is False?
I obviously mean more or less long sequences of disjunctions and
conjunctions, not minimal “(?P ∨ ?Q)” or “(?P ∧ ?Q)”.
I do it like I did before (some one year ago) using schematic variables,
to help readability a bit, but I'm still not happy with it and am seeking
for a proof method to more specifically (and cleanly) deal with it.
Schematic variables helps readability, while not enough as it still
quickly looks encumbered.
May be something close or related to “proof (cases t)”?
Email Gateway (Aug 19 2022 at 13:16):From: Lawrence Paulson <lp15@cam.ac.uk>
I suggest “safe” or “clarify”.
Larry Paulson
Email Gateway (Aug 19 2022 at 13:16):From: Yannick <yannick_duchene@yahoo.fr>
I will try those two right after. I was back to ask the same with things
like “show "⟦?H0; ?H1; ?H2⟧ ⟹ ?thesis"”, I mean if there is a method to
choose to prove it by proving "¬ ?H0".
I'm looking at “safe” or “clarify” in Isar‑Ref right in a minute (I need
to understand what it precisely do, … don't want to just play with it).
Lot of thanks for the pointers Larry!
Email Gateway (Aug 19 2022 at 13:16):From: Yannick <yannick_duchene@yahoo.fr>
It's not very well documented in Isar‑Ref.
Another option is to not bother adding as many intro/elimination rules for
the often required sequence length.
Ex:
lemma disjI2of3:
fixes P Q R :: "bool"
assumes "Q"
shows "P ∨ Q ∨ R"
proof - show "P ∨ Q ∨ R" using Q by simp qed
Then use it as in:
lemma "P ∨ Q ∨ R"
proof (intro disjI2of3)
(* prove Q here, and it's OK *)
oops
Email Gateway (Aug 19 2022 at 13:16):From: Joachim Breitner <mail@joachim-breitner.de>
Hi,
signature.asc
Email Gateway (Aug 19 2022 at 13:16):From: Lawrence Paulson <lp15@cam.ac.uk>
Try the Tutorial, section 5.13, Other Classical Reasoning Methods.
Larry
Last updated: Apr 26 2024 at 08:19 UTC