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"
  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 


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