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.