Re: [isabelle] Proof method to split disjunctions and conjunctions ?
On Sun, 08 Dec 2013 01:13:09 +0100, Lawrence Paulson <lp15 at cam.ac.uk>
I suggest “safe” or “clarify”.
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.
fixes P Q R :: "bool"
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 *)
This archive was generated by a fusion of
Pipermail (Mailman edition) and