Re: [isabelle] Setting up a non-standard induction

On Wed, 27 Feb 2008, Peter Chapman wrote:

> I wish to prove a theorem that uses induction based on a pair of natural
> numbers.

> proof (induct "depth A" "n+m+1" arbitrary: Gam C rule: my_wf_induct_pair)
> but I get the error message
> *** Ill-typed instantiation:
> ***   depth A :: nat
> *** At command "proof".

This fails because the induction priciple is only about a single argument 
(a nat pair), not two individual nats.

Here is my version of the induction principle:

  less_prod_nat  (infix "<<" 50) where
  "p << q == (p, q) : less_than <*lex*> less_than"

lemma nat_prod_induct [case_names less]:
  fixes x y :: nat
  assumes induct_step: "!!x y. (!!u v. (u, v) << (x, y) ==> P u v) ==> P x y"
  shows "P x y"
proof -
  have "wf (less_than <*lex*> less_than)" by blast
  then show ?thesis
  proof (induct p == "(x, y)" arbitrary: x y)
    case (less p)
    show "P x y"
    proof (rule induct_step)
      fix u v
      assume "(u, v) << (x, y)"
      with less show "P u v" by simp

This may already serve as an example how to deal with tricky inductions in 
general (see also src/HOL/Induct/Common_Patterns.thy for further 
patterns).  The idea is to represent the pair p as a concrete expression 
"(x, y)" for arbitrary x and y, and pass this information through the 
induction.  In the body, the "less" case (which is the only case of the 
induction scheme) will hold all this information, although in a slightly 
crude form involving explicit equalities again.  The Simplifier manages to 
reduce this in the final step, towards a clean result.

Here is an example application of the above rule:

  fixes a :: 'a
    and f g :: "'a => nat"
  assumes "A (f a) (g a)"
  shows "P (f a) (g a)"
using assms
proof (induct x == "f a" y == "g a" arbitrary: a rule: nat_prod_induct)
  case (less x y)
  then have "!!b. A (f b) (g b) ==>
      (f b, g b) << (x, y) ==> P (f b) (g b)"
    by simp
  note `x = f a` and `y = g a`
  note `A (f a) (g a)`
  show "P (f a) (g a)" sorry

The best way of spelling out the body of an induction proof depends a 
little on your particular application.  Above the raw constituents are 
presented in a reasonably digestible form.  At some point the "induct" 
proof method might get smarter in taking care of equational reductions 
without requiring the above "simp" steps.


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