[isabelle] structured induction

I love Isar structured induction.  Here are two questions.


   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 ...).


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.