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:


abbreviation
  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
    qed
  qed
qed


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:


lemma
  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
qed


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.


	Makarius





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