[isabelle] Setting up a non-standard induction

```Hi

```
I wish to prove a theorem that uses induction based on a pair of natural numbers. To make this concrete, I have that
```
wf (less_than <*lex*> less_than)

and then I have proved the induction scheme

lemma my_wf_induct_pair:
assumes    b: "/\x. [| /\y. ((fst y,snd y),(fst x,snd x))
```
\<in> (less_than <*lex*> less_than) -> P y |] => P x"
``` shows "P x"
(proof omitted)
done

```
Now, in the lemma I wish to prove, I have two natural numbers, one of which is computed using a function form => nat called "depth", and the other which is the sum of two other natural numbers, n and m. So, I wrote
```
fixes A :: "form"
and n m :: "nat"
assumes a: "Gam =>* A at n" "Gam + {#A#} =>* C at m"
shows "\<exists> k. Gam =>* C at k"
using a
```
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".

```
How do I get Isabelle to do the induction based on the lexicographic path ordering of (depth A, n+m+1)? I've tried putting
```
```
proof (induct ("depth A",n+m+1) arbitrary : Gam C rule:,my_wf_induct_pair)
```
but then I get a "bad argument" error.

Many thanks

Peter

```

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