Re: [isabelle] Proof method to split disjunctions and conjunctions ?
I suggest “safe” or “clarify”.
On 8 Dec 2013, at 00:01, Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr> wrote:
> 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