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