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> wrote:

I suggest “safe” or “clarify”.

Larry Paulson

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


--
Yannick Duchêne




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.