[isabelle] structured induction



I love Isar structured induction.  Here are two questions.

Consider:

 lemma
   assumes h:"R M"         --"R is an inductively defined relation"
   shows "P M = {}" "Q M"  --"P and Q are any properties"
 using h proof (induct)
   case (constr1 X)        --"constr1 is a single argument constructor of R"
  show ?case

The last line will fail:

  *** Unbound schematic variable: ?case

The ProofGeneral drop down for cases shows something about 
"subcases: 1 2"  How do I get ?case to work in this setting?


Question 2: Please give pointers to some examples of well-founded
induction over a measure function in Isabelle 2008.  I know of
Makarius' note "Structured Induction Proofs ...", but I still can't
get things to work in the structured way (as opposed to using the
object language to give an explicit induction predicate ...).

Thanks
Randy

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.






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