[isabelle] induction on pairs of naturals



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.