# Re: [isabelle] structured induction

```On Tue, 5 Aug 2008, Randy Pollack wrote:

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

You first need to enter the particular sub cases before the ?case binding
show up.  See the end of src/HOL/Induct/Common_Patterns.thy for examples
for induction with multiple goals.

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

Maybe you did not use the proper rule, which is wf_induct_rule as opposed
to the old wf_induct (the correct rule is already declared as canonical
induction scheme for `wf r` facts).  Here is an example pattern involving
both an extra parameter x and premise "A x a", apart from the induction
argument a:

lemma
fixes a :: 'a
and r :: "('a * 'a) set"
and x :: 'b
assumes "wf r"
and "A x a"
shows "B x a"
using assms
proof (induct a arbitrary: x)
case (less a)
note prem = `A x a`
-- {* cf. @{thm less.prems} *}
note hyp = `!!x y. (y, a) : r ==> A x y ==> B x y`
-- {* cf. @{thm less.hyps} *}
show ?case sorry
qed

The example from the "Structured Induction Proofs ..." paper is in
src/HOL/Isar_examples/Puzzle.thy (it uses the less_induct rule).

Makarius

```

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