Re: [isabelle] Case split for inductive definitions in Isar
On Fri, 23 May 2008, Peter Chapman wrote:
> I have a proof in which I wish to perform a case split as the proof method.
For Isabelle2007 see the isar-ref manual section 4.3.5 "Proof by cases and
induction", especially page 100, which gives an overview how the
cases/induct methods select the rules being used in a proof.
For eliminating inductive set membership "x:A", the basic idiom is like
from `x:A` have "P x"
case (blah a b c)
Assuming the usual declarations produced by the Isabelle/HOL packages,
this will use the A.cases rule as expected (A.exhaust is an obsolete name
for that). These rules rarely need to be referenced explicitly by name
This archive was generated by a fusion of
Pipermail (Mailman edition) and