Re: [isabelle] induction on pairs of naturals



Well-founded induction is rather brain-bending, and no amount of experience eliminates that problem. But it isn't difficult to prove using other means:

lemma pair_induction_lemma:
 fixes \<Phi> :: "nat \<times> nat \<Rightarrow> bool"
 assumes z1: "\<And>n2. \<Phi>(0, n2)"
 assumes z2:"\<And>n1. \<Phi>(n1, 0)"
 assumes sc: "\<And>n1 n2. \<lbrakk>\<Phi>(Suc n1, n2); \<Phi>(n1, Suc n2)\<rbrakk> \<Longrightarrow> \<Phi>(Suc n1, Suc n2)"
 shows "\<And>n1 n2. n1+n2 < k \<Longrightarrow> \<Phi>(n1,n2)"
proof (induct k)
  case 0 thus ?case by auto 
next
  case (Suc k')
  note case1 = this
  show ?case
    proof (cases n1)
      case 0 thus ?thesis using z1 by auto 
    next
      case (Suc m1)
      note case2 = this
      show ?thesis
      proof (cases n2)
        case 0 thus ?thesis using z2 by auto 
      next
        case (Suc m2)
        thus ?thesis using case1 case2 
          by (auto simp add: sc) 
      qed  
    qed
qed

This is only a lemma, now just put k = Suc(n1+n2). For your generalised version, it may suffice for you to introduce an appropriate length function.

Larry Paulson


On 31 Oct 2011, at 14:47, John Wickerson wrote:

> 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.