Re: [isabelle] Proof method to split disjunctions and conjunctions ?



I suggest “safe” or “clarify”.

Larry Paulson


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.” [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.