*To*: Peter Chapman <pc at cs.st-and.ac.uk>*Subject*: Re: [isabelle] Setting up a non-standard induction*From*: Makarius <makarius at sketis.net>*Date*: Thu, 28 Feb 2008 13:29:23 +0100 (CET)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <5A095B39-EA35-4398-A4EE-313C47E52993@cs.st-and.ac.uk>*References*: <5A095B39-EA35-4398-A4EE-313C47E52993@cs.st-and.ac.uk>

On Wed, 27 Feb 2008, Peter Chapman wrote: > I wish to prove a theorem that uses induction based on a pair of natural > numbers. > 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: 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

**References**:**[isabelle] Setting up a non-standard induction***From:*Peter Chapman

- Previous by Date: [isabelle] Cl&C 2008 - Second Call for Papers
- Next by Date: Re: [isabelle] Running cygwin isabelle from windows Gnu Emacs
- Previous by Thread: [isabelle] Setting up a non-standard induction
- Next by Thread: [isabelle] CMCS 08: final call for short contributions
- Cl-isabelle-users February 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list