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