[isabelle] Proof method to split disjunctions and conjunctions ?



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)”?


--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University





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