# [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
`
lemma cutAdmissibility:
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.*