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 
this:

  from `x:A` have "P x"
  proof induct
    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 
anyway.


	Makarius





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