[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.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and