Email Gateway (Aug 18 2022 at 11:28): Email Gateway (Aug 18 2022 at 11:28):From: Peter Chapman <pc@cs.st-and.ac.uk>
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
Email Gateway (Aug 18 2022 at 11:29):From: Makarius <makarius@sketis.net>
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
Last updated: May 03 2024 at 04:19 UTC