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
> 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:
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"
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
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:
fixes a :: 'a
and f g :: "'a => nat"
assumes "A (f a) (g a)"
shows "P (f a) (g a)"
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)"
note `x = f a` and `y = g a`
note `A (f a) (g a)`
show "P (f a) (g a)" sorry
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and