*To*: John Wickerson <jpw48 at cam.ac.uk>*Subject*: [isabelle] induction on pairs of naturals*From*: Christian Urban <urbanc at in.tum.de>*Date*: Mon, 31 Oct 2011 15:08:56 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <F8D6DA04-50D2-4D60-A91E-845F42946A3D@cam.ac.uk>*References*: <F8D6DA04-50D2-4D60-A91E-845F42946A3D@cam.ac.uk>*Reply-to*: christian.urban at kcl.ac.uk

Hi John, There is a really cool feature of the function package that is not widely known and that helps tremendously with such proofs. It cannot deal with pairs, I think, but if you formulate the induction predicate as a function taking two arguments then you can solve your problem like this. lemma assumes "!!n. P 0 n" and "!!m. P m 0" and "!!n m. [|P n (Suc m); P (Suc n) m|] ==> P (Suc n) (Suc m)" shows "P m n" using assms apply(induction_schema) apply(pat_completeness) apply(lexicographic_order) done >From this you original lemma should follow. Have a look at src/HOL/ex/Induction_Schema.thy for further examples. I think it will also help in your case with lists. Best wishes, Christian John Wickerson writes: > Hello, > > I'm trying to justify the following induction principle over pairs of naturals. The principle is that if you can show Phi(0,n) for all n, and Phi(m,0) for all m, and if you also show that Phi(m,n+1) and Phi(m+1,n) imply Phi(m+1,n+1) for all m and n, then you can deduce Phi(m,n) for all m and n. > > My proof plan is to show that this is an instance of wf induction, but I'm really struggling! (I previously tried to justify it using ordinary mathematical induction, but got stuck on that too.) I would very much appreciate any suggestions people may have for how I can complete this proof. > > > lemma pair_induction: > fixes \<Phi> :: "nat \<times> nat \<Rightarrow> bool" > assumes "\<And>n2. \<Phi>(0, n2)" > assumes "\<And>n1. \<Phi>(n1, 0)" > assumes "\<And>n1 n2. \<lbrakk>\<Phi>(Suc n1, n2); \<Phi>(n1, Suc n2)\<rbrakk> \<Longrightarrow> \<Phi>(Suc n1, Suc n2)" > shows "\<And>n1 n2. \<Phi>(n1,n2)" > proof - > fix n1 n2 > let ?r = "{((m1,m2),(n1,n2)) | m1 m2 n1 n2. > (Suc m1 = n1 \<and> Suc m2 = n2) \<or> (m1 = n1 \<and> Suc m2 = n2) > \<or> (Suc m1 = n1 \<and> m2 = n2)}" > have "wf ?r" > and "\<And>p. (\<And>q. (q, p) \<in> ?r \<Longrightarrow> \<Phi> q) \<Longrightarrow> \<Phi> p" sorry > from wf_induct_rule[OF this] > show "\<Phi>(n1,n2)" sorry > qed > > Many thanks! > > john --

**Follow-Ups**:**Re: [isabelle] induction on pairs of naturals***From:*John Wickerson

**References**:**[isabelle] induction on pairs of naturals***From:*John Wickerson

- Previous by Date: Re: [isabelle] induction on pairs of naturals
- Next by Date: Re: [isabelle] induction on pairs of naturals
- Previous by Thread: Re: [isabelle] induction on pairs of naturals
- Next by Thread: Re: [isabelle] induction on pairs of naturals
- Cl-isabelle-users October 2011 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