Theory Incompleteness.Goedel_I

chapter ‹Section 6 Material and Gödel's First Incompleteness Theorem›

theory Goedel_I
imports Pf_Predicates Functions
begin

section‹The Function W and Lemma 6.1›

subsection‹Predicate form, defined on sequences›

definition SeqWR :: "hf  hf  hf  bool"
  where "SeqWR s k y  LstSeq s k y  app s 0 = 0 
                        (l  k. app s (succ l) = q_Eats (app s l) (app s l))"

nominal_function SeqWRP :: "tm  tm  tm  fm"
  where "atom l  (s,k,sl); atom sl  (s) 
    SeqWRP s k y = LstSeqP s k y AND
          HPair Zero Zero IN s AND
          All2 l k (Ex sl (HPair (Var l) (Var sl) IN s AND
                           HPair (SUCC (Var l)) (Q_Succ (Var sl)) IN s))"
  by (auto simp: eqvt_def SeqWRP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
  by lexicographic_order

lemma
  shows SeqWRP_fresh_iff [simp]: "a  SeqWRP s k y  a  s  a  k  a  y" (is ?thesis1)
    and eval_fm_SeqWRP [simp]:   "eval_fm e (SeqWRP s k y)  SeqWR se ke ye"  (is ?thesis2)
    and SeqWRP_sf [iff]:         "Sigma_fm (SeqWRP s k y)"  (is ?thsf)
proof -
  obtain l::name and sl::name where "atom l  (s,k,sl)" "atom sl  (s)"
    by (metis obtain_fresh)
  thus ?thesis1 ?thesis2 ?thsf
      by (auto simp: SeqWR_def q_defs LstSeq_imp_Ord
             Seq_iff_app [of "se", OF LstSeq_imp_Seq_succ]
             Ord_trans [of _ _ "succ ke"])
qed

lemma SeqWRP_subst [simp]:
      "(SeqWRP s k y)(i::=t) = SeqWRP (subst i t s) (subst i t k) (subst i t y)"
proof -
  obtain l::name and sl::name
    where "atom l  (s,k,sl,t,i)" "atom sl  (s,k,t,i)"
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: SeqWRP.simps [where l=l and sl=sl])
qed

lemma SeqWRP_cong:
  assumes "H  s EQ s'" and  "H  k EQ k'" and  "H  y EQ y'"
  shows "H  SeqWRP s k y IFF SeqWRP s' k' y'"
  by (rule P3_cong [OF _ assms], auto)

declare SeqWRP.simps [simp del]

subsection‹Predicate form of W›

definition WR :: "hf  hf  bool"
  where "WR x y  (s. SeqWR s x y)"

nominal_function WRP :: "tm  tm  fm"
  where "atom s  (x,y) 
    WRP x y = Ex s (SeqWRP (Var s) x y)"
  by (auto simp: eqvt_def WRP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
  by lexicographic_order

lemma
  shows WRP_fresh_iff [simp]: "a  WRP x y  a  x  a  y" (is ?thesis1)
    and eval_fm_WRP [simp]:   "eval_fm e (WRP x y)  WR xe ye"  (is ?thesis2)
    and sigma_fm_WRP [simp]:  "Sigma_fm (WRP x y)"  (is ?thsf)
proof -
  obtain s::name where "atom s  (x,y)"
    by (metis obtain_fresh)
  thus ?thesis1 ?thesis2 ?thsf
    by (auto simp: WR_def)
qed

lemma WRP_subst [simp]: "(WRP x y)(i::=t) = WRP (subst i t x) (subst i t y)"
proof -
  obtain s::name where "atom s  (x,y,t,i)"
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: WRP.simps [of s])
qed

lemma WRP_cong: "H  t EQ t'  H  u EQ u'  H  WRP t u IFF WRP t' u'"
  by (rule P2_cong) auto

declare WRP.simps [simp del]

lemma WR0_iff: "WR 0 y  y=0"
  by (simp add: WR_def SeqWR_def) (metis LstSeq_1 LstSeq_app)

lemma WR0: "WR 0 0"
  by (simp add: WR0_iff)

lemma WR_succ_iff: assumes i: "Ord i" shows "WR (succ i) z = (y. z = q_Eats y y  WR i y)"
proof
  assume "WR (succ i) z"
  then obtain s where s: "SeqWR s (succ i) z"
    by (auto simp: WR_def i)
  moreover then have "app s (succ i) = z"
    by (auto simp: SeqWR_def)
  ultimately show "y. z = q_Eats y y  WR i y" using i 
    by (auto simp: WR_def SeqWR_def) (metis LstSeq_trunc hmem_succ_self)
next
  assume "y. z = q_Eats y y  WR i y"
  then obtain y where z: "z = q_Eats y y" and y: "WR i y"
    by blast
  thus "WR (succ i) z" using i
    apply (auto simp: WR_def SeqWR_def)
    apply (rule_tac x="insf s (succ i) (q_Eats y y)" in exI)
    apply (auto simp: LstSeq_imp_Seq_succ app_insf_Seq_if LstSeq_insf succ_notin_self)
    done
qed

lemma WR_succ: "Ord i  WR (succ i) (q_Eats y y) = WR i y"
  by (metis WR_succ_iff q_Eats_iff)

lemma WR_ord_of: "WR (ord_of i) «ORD_OF i»e"
  by (induct i) (auto simp: WR0_iff WR_succ_iff quot_Succ q_defs)

text‹Lemma 6.1›
lemma WR_quot_Var: "WR «Var x»e ««Var x»»e"
  by (auto simp: quot_Var quot_Succ)
     (metis One_nat_def Ord_ord_of WR_ord_of WR_succ htuple.simps q_Eats_def)

lemma ground_WRP [simp]: "ground_fm (WRP x y)  ground x  ground y"
  by (auto simp: ground_aux_def ground_fm_aux_def supp_conv_fresh)

lemma prove_WRP:  "{}  WRP «Var x» ««Var x»»"
  by (auto simp: WR_quot_Var ground_aux_def supp_conv_fresh intro: Sigma_fm_imp_thm)

subsection‹Proving that these relations are functions›

lemma SeqWRP_Zero_E:
  assumes "insert (y EQ Zero) H  A"  "H  k EQ Zero"
  shows "insert (SeqWRP s k y) H  A"
proof -
  obtain l::name and sl::name
    where "atom l  (s,k,sl)" "atom sl  (s)"
    by (metis obtain_fresh)
  thus ?thesis
    apply (auto simp: SeqWRP.simps [where s=s and l=l and sl=sl])
    apply (rule cut_same [where A = "LstSeqP s Zero y"])
    apply (blast intro: thin1 assms  LstSeqP_cong [OF Refl _ Refl, THEN Iff_MP_same])
    apply (rule cut_same [where A = "y EQ Zero"])
    apply (blast intro: LstSeqP_EQ)
    apply (metis rotate2 assms(1) thin1)
    done
qed

lemma SeqWRP_SUCC_lemma:
  assumes y': "atom y'  (s,k,y)"
  shows "{SeqWRP s (SUCC k) y}  Ex y' (SeqWRP s k (Var y') AND y EQ Q_Succ (Var y'))"
proof -
  obtain l::name and sl::name
    where atoms: "atom l  (s,k,y,y',sl)" "atom sl  (s,k,y,y')"
    by (metis obtain_fresh)
  thus ?thesis using y'
    apply (auto simp: SeqWRP.simps [where s=s and l=l and sl=sl])
    apply (rule All2_SUCC_E' [where t=k, THEN rotate2], auto)
    apply (rule Ex_I [where x = "Var sl"], auto)
    apply (blast intro: LstSeqP_SUCC) ― ‹showing @{term"SeqWRP s k (Var sl)"}
    apply (blast intro: ContraProve LstSeqP_EQ)
    done
qed

lemma SeqWRP_SUCC_E:
  assumes y': "atom y'  (s,k,y)" and k': "H  k' EQ (SUCC k)"
  shows "insert (SeqWRP s k' y) H   Ex y' (SeqWRP s k (Var y') AND y EQ Q_Succ (Var y'))"
  using SeqWRP_cong [OF Refl k' Refl] cut1 [OF SeqWRP_SUCC_lemma [of y' s k y]]
  by (metis Assume Iff_MP_left Iff_sym y')

lemma SeqWRP_unique: "{OrdP x, SeqWRP s x y, SeqWRP s' x y'}  y' EQ y"
proof -
  obtain i::name and j::name and j'::name and k::name and sl::name and sl'::name and l::name and pi::name
    where  i: "atom i  (s,s',y,y')" and j: "atom j  (s,s',i,x,y,y')" and j': "atom j'  (s,s',i,j,x,y,y')"
      and atoms: "atom k  (s,s',i,j,j')" "atom sl  (s,s',i,j,j',k)" "atom sl'  (s,s',i,j,j',k,sl)"
                 "atom pi  (s,s',i,j,j',k,sl,sl')"
    by (metis obtain_fresh)
  have "{OrdP (Var i)}  All j (All j' (SeqWRP s (Var i) (Var j) IMP (SeqWRP s' (Var i) (Var j') IMP Var j' EQ Var j)))"
    apply (rule OrdIndH [where j=k])
    using i j j' atoms apply auto
    apply (rule rotate4)
    apply (rule OrdP_cases_E [where k=pi], simp_all)
    ― ‹Zero case›
    apply (rule SeqWRP_Zero_E [THEN rotate3])
    prefer 2 apply blast
    apply (rule SeqWRP_Zero_E [THEN rotate4])
    prefer 2 apply blast
    apply (blast intro: ContraProve [THEN rotate4] Sym Trans)
    ― ‹SUCC case›
    apply (rule Ex_I [where x = "Var pi"], auto)
    apply (metis ContraProve EQ_imp_SUBS2 Mem_SUCC_I2 Refl Subset_D)
    apply (rule cut_same)
    apply (rule SeqWRP_SUCC_E [of sl' s' "Var pi", THEN rotate4], auto)
    apply (rule cut_same)
    apply (rule SeqWRP_SUCC_E [of sl s "Var pi", THEN rotate7], auto)
    apply (rule All_E [where x = "Var sl", THEN rotate5], simp)
    apply (rule All_E [where x = "Var sl'"], simp)
    apply (rule Imp_E, blast)+
    apply (rule cut_same [OF Q_Succ_cong [OF Assume]])
    apply (blast intro: Trans [OF Hyp Sym] HPair_cong)
    done
  hence "{OrdP (Var i)}  (All j' (SeqWRP s (Var i) (Var j) IMP (SeqWRP s' (Var i) (Var j') IMP Var j' EQ Var j)))(j::=y)"
    by (metis All_D)
  hence "{OrdP (Var i)}  (SeqWRP s (Var i) y IMP (SeqWRP s' (Var i) (Var j') IMP Var j' EQ y))(j'::=y')"
    using j j'
    by simp (drule All_D [where x=y'], simp)
  hence "{}  OrdP (Var i) IMP (SeqWRP s (Var i) y IMP (SeqWRP s' (Var i) y' IMP y' EQ y))"
    using j j'
    by simp (metis Imp_I)
  hence "{}  (OrdP (Var i) IMP (SeqWRP s (Var i) y IMP (SeqWRP s' (Var i) y' IMP y' EQ y)))(i::=x)"
    by (metis Subst emptyE)
  thus ?thesis using i
    by simp (metis anti_deduction insert_commute)
qed

theorem WRP_unique: "{OrdP x, WRP x y, WRP x y'}  y' EQ y"
proof -
  obtain s::name and s'::name
    where "atom s  (x,y,y')"  "atom s'  (x,y,y',s)"
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: SeqWRP_unique [THEN rotate3] WRP.simps [of s _ y]  WRP.simps [of s' _ y'])
qed

subsection‹The equivalent function›

definition W :: "hf  tm"
  where "W  hmemrec (λf z. if z=0 then Zero else Q_Eats (f (pred z)) (f (pred z)))"

lemma W0 [simp]: "W 0 = Zero"
  by (rule trans [OF def_hmemrec [OF W_def]]) auto

lemma W_succ [simp]: "Ord i  W (succ i) = Q_Eats (W i) (W i)"
  by (rule trans [OF def_hmemrec [OF W_def]]) (auto simp: ecut_apply SUCC_def W_def)

lemma W_ord_of [simp]: "W (ord_of i) = «ORD_OF i»"
  by (induct i, auto simp: SUCC_def quot_simps)

lemma WR_iff_eq_W: "Ord x  WR x y  y = W xe"
proof (induct x arbitrary: y rule: Ord_induct2)
  case 0 thus ?case
    by (metis W0 WR0_iff eval_tm.simps(1))
next
  case (succ k) thus ?case
    by (auto simp: WR_succ_iff q_Eats_def)
qed


section‹The Function HF and Lemma 6.2›

definition SeqHR :: "hf  hf  hf  hf  bool"
where "SeqHR x x' s k 
       BuildSeq2 (λy y'. Ord y  WR y y')
                 (λu u' v v' w w'. u = v,w  u' = q_HPair v' w') s k x x'"

subsection ‹Defining the syntax: quantified body›

nominal_function SeqHRP :: "tm  tm  tm  tm  fm"
  where "atom l  (s,k,sl,sl',m,n,sm,sm',sn,sn');
          atom sl  (s,sl',m,n,sm,sm',sn,sn');
          atom sl'  (s,m,n,sm,sm',sn,sn');
          atom m  (s,n,sm,sm',sn,sn');
          atom n  (s,sm,sm',sn,sn');
          atom sm  (s,sm',sn,sn');
          atom sm'  (s,sn,sn');
          atom sn  (s,sn');
          atom sn'  (s) 
    SeqHRP x x' s k =
      LstSeqP s k (HPair x x') AND
      All2 l (SUCC k) (Ex sl (Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND
                ((OrdP (Var sl) AND WRP (Var sl) (Var sl')) OR
                 Ex m (Ex n (Ex sm (Ex sm' (Ex sn (Ex sn' (Var m IN Var l AND Var n IN Var l AND
                       HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND
                       HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND
                       Var sl EQ HPair (Var sm) (Var sn) AND
                       Var sl' EQ Q_HPair (Var sm') (Var sn')))))))))))"
by (auto simp: eqvt_def SeqHRP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
  by lexicographic_order

lemma
 shows SeqHRP_fresh_iff [simp]:
      "a  SeqHRP x x' s k  a  x  a  x'  a  s  a  k"  (is ?thesis1)
   and eval_fm_SeqHRP [simp]:
      "eval_fm e (SeqHRP x x' s k)  SeqHR xe x'e se ke"  (is ?thesis2)
  and SeqHRP_sf [iff]:  "Sigma_fm (SeqHRP x x' s k)"  (is ?thsf)
  and SeqHRP_imp_OrdP: "{ SeqHRP x y s k }  OrdP k"  (is ?thord)
proof -
  obtain l::name and sl::name and sl'::name and m::name and n::name and
         sm::name and sm'::name and sn::name and sn'::name
    where atoms:
         "atom l  (s,k,sl,sl',m,n,sm,sm',sn,sn')"
         "atom sl  (s,sl',m,n,sm,sm',sn,sn')" "atom sl'  (s,m,n,sm,sm',sn,sn')"
         "atom m  (s,n,sm,sm',sn,sn')" "atom n  (s,sm,sm',sn,sn')"
         "atom sm  (s,sm',sn,sn')" "atom sm'  (s,sn,sn')"
         "atom sn  (s,sn')" "atom sn'  (s)"
    by (metis obtain_fresh)
  thus ?thesis1 ?thsf ?thord
    by (auto intro: LstSeqP_OrdP)
  show ?thesis2 using atoms
    by (fastforce simp: LstSeq_imp_Ord SeqHR_def 
             BuildSeq2_def BuildSeq_def Builds_def
             HBall_def q_HPair_def q_Eats_def
             Seq_iff_app [of "se", OF LstSeq_imp_Seq_succ]
             Ord_trans [of _ _ "succ ke"]
             cong: conj_cong)
qed

lemma SeqHRP_subst [simp]:
      "(SeqHRP x x' s k)(i::=t) = SeqHRP (subst i t x) (subst i t x') (subst i t s) (subst i t k)"
proof -
  obtain l::name and sl::name and sl'::name and m::name and n::name and
         sm::name and sm'::name and sn::name and sn'::name
    where "atom l  (s,k,t,i,sl,sl',m,n,sm,sm',sn,sn')"
          "atom sl  (s,t,i,sl',m,n,sm,sm',sn,sn')"
          "atom sl'  (s,t,i,m,n,sm,sm',sn,sn')"
          "atom m  (s,t,i,n,sm,sm',sn,sn')" "atom n  (s,t,i,sm,sm',sn,sn')"
          "atom sm  (s,t,i,sm',sn,sn')" "atom sm'  (s,t,i,sn,sn')"
          "atom sn  (s,t,i,sn')" "atom sn'  (s,t,i)"
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: SeqHRP.simps [of l _ _ sl sl' m n sm sm' sn sn'])
qed

lemma SeqHRP_cong:
  assumes "H  x EQ x'" and "H  y EQ y'" "H  s EQ s'" and  "H  k EQ k'"
  shows "H  SeqHRP x y s k IFF SeqHRP x' y' s' k'"
  by (rule P4_cong [OF _ assms], auto)

subsection ‹Defining the syntax: main predicate›

definition HR :: "hf  hf  bool"
  where "HR x x'  s k. SeqHR x x' s k"

nominal_function HRP :: "tm  tm  fm"
  where "atom s  (x,x',k); atom k  (x,x') 
         HRP x x' = Ex s (Ex k (SeqHRP x x' (Var s) (Var k)))"
  by (auto simp: eqvt_def HRP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
  by lexicographic_order

lemma
 shows HRP_fresh_iff [simp]: "a  HRP x x'  a  x  a  x'"  (is ?thesis1)
   and eval_fm_HRP [simp]:   "eval_fm e (HRP x x')  HR xe x'e"  (is ?thesis2)
   and HRP_sf [iff]:         "Sigma_fm (HRP x x')"  (is ?thsf)
proof -
  obtain s::name and k::name  where "atom s  (x,x',k)"  "atom k  (x,x')"
    by (metis obtain_fresh)
  thus ?thesis1 ?thesis2 ?thsf
    by (auto simp: HR_def q_defs)
qed

lemma HRP_subst [simp]: "(HRP x x')(i::=t) = HRP (subst i t x) (subst i t x')"
proof -
  obtain s::name and k::name where "atom s  (x,x',t,i,k)"  "atom k  (x,x',t,i)"
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: HRP.simps [of s _ _ k])
qed

subsection‹Proving that these relations are functions›

lemma SeqHRP_lemma:
  assumes "atom m  (x,x',s,k,n,sm,sm',sn,sn')" "atom n  (x,x',s,k,sm,sm',sn,sn')"
          "atom sm  (x,x',s,k,sm',sn,sn')" "atom sm'  (x,x',s,k,sn,sn')"
          "atom sn  (x,x',s,k,sn')" "atom sn'  (x,x',s,k)"
    shows "{ SeqHRP x x' s k }
          (OrdP x AND WRP x x') OR
             Ex m (Ex n (Ex sm (Ex sm' (Ex sn (Ex sn' (Var m IN k AND Var n IN k AND
                       SeqHRP (Var sm) (Var sm') s (Var m) AND
                       SeqHRP (Var sn) (Var sn') s (Var n) AND
                       x EQ HPair (Var sm) (Var sn) AND
                       x' EQ Q_HPair (Var sm') (Var sn')))))))"
proof -
  obtain l::name and sl::name and sl'::name
    where atoms:
          "atom l  (x,x',s,k,sl,sl',m,n,sm,sm',sn,sn')"
          "atom sl  (x,x',s,k,sl',m,n,sm,sm',sn,sn')"
          "atom sl'  (x,x',s,k,m,n,sm,sm',sn,sn')"
    by (metis obtain_fresh)
  thus ?thesis using atoms assms
    apply (simp add: SeqHRP.simps [of l s k sl sl' m n sm sm' sn sn'])
    apply (rule Conj_E)
    apply (rule All2_SUCC_E' [where t=k, THEN rotate2], simp_all)
    apply (rule rotate2)
    apply (rule Ex_E Conj_E)+
    apply (rule cut_same [where A = "HPair x x' EQ HPair (Var sl) (Var sl')"])
    apply (metis Assume LstSeqP_EQ rotate4, simp_all, clarify)
    apply (rule Disj_E [THEN rotate4])
    apply (rule Disj_I1) 
    apply (metis Assume AssumeH(3) Sym thin1  Iff_MP_same [OF Conj_cong [OF OrdP_cong WRP_cong] Assume])
    ― ‹auto could be used but is VERY SLOW›
    apply (rule Disj_I2) 
    apply (rule Ex_E Conj_EH)+
    apply simp_all
    apply (rule Ex_I [where x = "Var m"], simp)
    apply (rule Ex_I [where x = "Var n"], simp)
    apply (rule Ex_I [where x = "Var sm"], simp)
    apply (rule Ex_I [where x = "Var sm'"], simp)
    apply (rule Ex_I [where x = "Var sn"], simp)
    apply (rule Ex_I [where x = "Var sn'"], simp)
    apply (simp add: SeqHRP.simps [of l _ _ sl sl' m n sm sm' sn sn'])
    apply (rule Conj_I, blast)+
    ― ‹first SeqHRP subgoal›
    apply (rule Conj_I)+
    apply (blast intro: LstSeqP_Mem)
    apply (rule All2_Subset [OF Hyp], blast)
    apply (blast intro!: SUCC_Subset_Ord LstSeqP_OrdP, blast, simp)
    ― ‹next SeqHRP subgoal›
    apply (rule Conj_I)+
    apply (blast intro: LstSeqP_Mem)
    apply (rule All2_Subset [OF Hyp], blast)
    apply (auto intro!: SUCC_Subset_Ord LstSeqP_OrdP)
    ― ‹finally, the equality pair›
    apply (blast intro: Trans)+
    done
qed
 
lemma SeqHRP_unique: "{SeqHRP x y s u, SeqHRP x y' s' u'}  y' EQ y"
proof -
  obtain i::name and j::name and j'::name and k::name and k'::name and l::name
     and m::name and n::name and sm::name and sn::name and sm'::name and sn'::name
     and m2::name and n2::name and sm2::name and sn2::name and sm2'::name and sn2'::name
    where atoms:  "atom i  (s,s',y,y')"   "atom j  (s,s',i,x,y,y')"  "atom j'  (s,s',i,j,x,y,y')"
                  "atom k  (s,s',x,y,y',u',i,j,j')" "atom k'  (s,s',x,y,y',k,i,j,j')" "atom l  (s,s',i,j,j',k,k')"
                  "atom m  (s,s',i,j,j',k,k',l)"   "atom n  (s,s',i,j,j',k,k',l,m)"
                  "atom sm  (s,s',i,j,j',k,k',l,m,n)"  "atom sn  (s,s',i,j,j',k,k',l,m,n,sm)"
                  "atom sm'  (s,s',i,j,j',k,k',l,m,n,sm,sn)"   "atom sn'  (s,s',i,j,j',k,k',l,m,n,sm,sn,sm')"
                  "atom m2  (s,s',i,j,j',k,k',l,m,n,sm,sn,sm',sn')"   "atom n2  (s,s',i,j,j',k,k',l,m,n,sm,sn,sm',sn',m2)"
                  "atom sm2  (s,s',i,j,j',k,k',l,m,n,sm,sn,sm',sn',m2,n2)"  "atom sn2  (s,s',i,j,j',k,k',l,m,n,sm,sn,sm',sn',m2,n2,sm2)"
                  "atom sm2'  (s,s',i,j,j',k,k',l,m,n,sm,sn,sm',sn',m2,n2,sm2,sn2)"   "atom sn2'  (s,s',i,j,j',k,k',l,m,n,sm,sn,sm',sn',m2,n2,sm2,sn2,sm2')"
    by (metis obtain_fresh)
  have "{OrdP (Var k)}
        All i (All j (All j' (All k' (SeqHRP (Var i) (Var j) s (Var k) IMP (SeqHRP (Var i) (Var j') s' (Var k') IMP Var j' EQ Var j)))))"
    apply (rule OrdIndH [where j=l])
    using atoms apply auto
    apply (rule Swap)
    apply (rule cut_same)
    apply (rule cut1 [OF SeqHRP_lemma [of m "Var i" "Var j" s "Var k" n sm sm' sn sn']], simp_all, blast)
    apply (rule cut_same)
    apply (rule cut1 [OF SeqHRP_lemma [of m2 "Var i" "Var j'" s' "Var k'" n2 sm2 sm2' sn2 sn2']], simp_all, blast)
    apply (rule Disj_EH Conj_EH)+
    ― ‹case 1, both are ordinals›
    apply (blast intro: cut3 [OF WRP_unique])
    ― ‹case 2, @{term "OrdP (Var i)"} but also a pair›
    apply (rule Conj_EH Ex_EH)+
    apply simp_all
    apply (rule cut_same [where A = "OrdP (HPair (Var sm) (Var sn))"])
    apply (blast intro: OrdP_cong [OF Hyp, THEN Iff_MP_same], blast)
    ― ‹towards second two cases›
    apply (rule Ex_E Disj_EH Conj_EH)+
    ― ‹case 3, @{term "OrdP (Var i)"} but also a pair›
    apply (rule cut_same [where A = "OrdP (HPair (Var sm2) (Var sn2))"])
    apply (blast intro: OrdP_cong [OF Hyp, THEN Iff_MP_same], blast)
    ― ‹case 4, two pairs›
    apply (rule Ex_E Disj_EH Conj_EH)+
    apply (rule All_E' [OF Hyp, where x="Var m"], blast)
    apply (rule All_E' [OF Hyp, where x="Var n"], blast, simp_all)
    apply (rule Disj_EH, blast intro: thin1 ContraProve)+
    apply (rule All_E [where x="Var sm"], simp)
    apply (rule All_E [where x="Var sm'"], simp)
    apply (rule All_E [where x="Var sm2'"], simp)
    apply (rule All_E [where x="Var m2"], simp)
    apply (rule All_E [where x="Var sn", THEN rotate2], simp)
    apply (rule All_E [where x="Var sn'"], simp)
    apply (rule All_E [where x="Var sn2'"], simp)
    apply (rule All_E [where x="Var n2"], simp)
    apply (rule cut_same [where A = "HPair (Var sm) (Var sn) EQ HPair (Var sm2) (Var sn2)"])
    apply (blast intro: Sym Trans)
    apply (rule cut_same [where A = "SeqHRP (Var sn) (Var sn2') s' (Var n2)"])
    apply (blast intro: SeqHRP_cong [OF Hyp Refl Refl, THEN Iff_MP2_same])
    apply (rule cut_same [where A = "SeqHRP (Var sm) (Var sm2') s' (Var m2)"])
    apply (blast intro: SeqHRP_cong [OF Hyp Refl Refl, THEN Iff_MP2_same])
    apply (rule Disj_EH, blast intro: thin1 ContraProve)+
    apply (blast intro: Trans [OF Hyp Sym] intro!: HPair_cong)
    done
  hence "{OrdP (Var k)}
          All j (All j' (All k' (SeqHRP x (Var j) s (Var k)
               IMP (SeqHRP x (Var j') s' (Var k') IMP Var j' EQ Var j))))"
    apply (rule All_D [where x = x, THEN cut_same])
    using atoms by auto
  hence "{OrdP (Var k)}
          All j' (All k' (SeqHRP x y s (Var k) IMP (SeqHRP x (Var j') s' (Var k') IMP Var j' EQ y)))"
    apply (rule All_D [where x = y, THEN cut_same])
    using atoms by auto
  hence "{OrdP (Var k)}
           All k' (SeqHRP x y s (Var k) IMP (SeqHRP x y' s' (Var k') IMP y' EQ y))"
    apply (rule All_D [where x = y', THEN cut_same])
    using atoms by auto
  hence "{OrdP (Var k)}  SeqHRP x y s (Var k) IMP (SeqHRP x y' s' u' IMP y' EQ y)"
    apply (rule All_D [where x = u', THEN cut_same])
    using atoms by auto
  hence "{SeqHRP x y s (Var k)}  SeqHRP x y s (Var k) IMP (SeqHRP x y' s' u' IMP y' EQ y)"
    by (metis SeqHRP_imp_OrdP cut1)
  hence "{}  ((SeqHRP x y s (Var k) IMP (SeqHRP x y' s' u' IMP y' EQ y)))(k::=u)"
    by (metis Subst emptyE Assume MP_same Imp_I)
  hence "{}  SeqHRP x y s u IMP (SeqHRP x y' s' u' IMP y' EQ y)"
    using atoms by simp
  thus ?thesis
    by (metis anti_deduction insert_commute)
qed

theorem HRP_unique: "{HRP x y, HRP x y'}  y' EQ y"
proof -
  obtain s::name and s'::name and k::name and k'::name
    where "atom s  (x,y,y')" "atom s'  (x,y,y',s)" 
          "atom k  (x,y,y',s,s')" "atom k'  (x,y,y',s,s',k)"
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: SeqHRP_unique HRP.simps [of s x y k]  HRP.simps [of s' x y' k'])
qed

subsection ‹Finally The Function HF Itself›

definition HF :: "hf  tm"
  where "HF  hmemrec (λf z. if Ord z then W z else Q_HPair (f (hfst z)) (f (hsnd z)))"

lemma HF_Ord [simp]: "Ord i  HF i = W i"
  by (rule trans [OF def_hmemrec [OF HF_def]]) auto

lemma HF_pair [simp]: "HF (hpair x y) = Q_HPair (HF x) (HF y)"
  by (rule trans [OF def_hmemrec [OF HF_def]]) (auto simp: ecut_apply HF_def)

lemma SeqHR_hpair: "SeqHR x1 x3 s1 k1  SeqHR x2 x4 s2 k2  s k. SeqHR x1,x2 (q_HPair x3 x4) s k"
  by (auto simp: SeqHR_def intro: BuildSeq2_combine)

lemma HR_H:  "coding_hf x  HR x HF xe"
proof (induct x rule: hmem_rel_induct)
  case (step x) show ?case
  proof (cases "Ord x")
    case True thus ?thesis
      by (auto simp: HR_def SeqHR_def Ord_not_hpair WR_iff_eq_W [where e=e] intro!: BuildSeq2_exI)
  next
    case False 
    then obtain x1 x2 where x: "x = x1,x2" 
      by (metis Ord_ord_of coding_hf.simps step.prems)
    then have x12: "(x1, x)  hmem_rel" "(x2, x)  hmem_rel"
      by (auto simp: hmem_rel_iff_hmem_eclose)
    have co12: "coding_hf x1"  "coding_hf x2" using False step x
      by (metis Ord_ord_of coding_hf_hpair)+
    hence "HR x1 HF x1e"  "HR x2 HF x2e" 
      by (auto simp: x12 step)
    thus ?thesis using x SeqHR_hpair
      by (auto simp: HR_def q_defs)
  qed
qed

text‹Lemma 6.2›
lemma HF_quot_coding_tm: "coding_tm t  HF te = «t»"
  by (induct t rule: coding_tm.induct) (auto, simp add: HPair_def quot_Eats)

lemma HR_quot_fm: fixes A::fm shows "HR «A»e ««A»»e"
  by (metis HR_H HF_quot_coding_tm coding_tm_hf quot_fm_coding)

lemma prove_HRP: fixes A::fm shows "{}  HRP «A» ««A»»"
  by (auto simp: supp_conv_fresh Sigma_fm_imp_thm ground_aux_def ground_fm_aux_def HR_quot_fm)


section‹The Function K and Lemma 6.3›

nominal_function KRP :: "tm  tm  tm  fm"
  where "atom y  (v,x,x') 
         KRP v x x' = Ex y (HRP x (Var y) AND SubstFormP v (Var y) x x')"
  by (auto simp: eqvt_def KRP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
  by lexicographic_order

lemma KRP_fresh_iff [simp]: "a  KRP v x x'  a  v  a  x  a  x'"
proof -
  obtain y::name where "atom y  (v,x,x')"
    by (metis obtain_fresh)
  thus ?thesis
    by auto
qed

lemma KRP_subst [simp]: "(KRP v x x')(i::=t) = KRP (subst i t v) (subst i t x) (subst i t x')"
proof -
  obtain y::name where "atom y  (v,x,x',t,i)"
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: KRP.simps [of y])
qed

declare KRP.simps [simp del]

lemma prove_SubstFormP: "{}  SubstFormP «Var i» ««A»» «A» «A(i::=«A»)»"
  by (auto simp: supp_conv_fresh Sigma_fm_imp_thm ground_aux_def SubstForm_quot)

lemma prove_KRP: "{}  KRP «Var i» «A» «A(i::=«A»)»"
  by (auto simp: KRP.simps [of y] 
           intro!: Ex_I [where x="««A»»"] prove_HRP prove_SubstFormP)

lemma KRP_unique: "{KRP v x y, KRP v x y'}  y' EQ y"
proof -
  obtain u::name and u'::name where "atom u  (v,x,y,y')" "atom u'  (v,x,y,y',u)"
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: KRP.simps [of u v x y] KRP.simps [of u' v x y'] 
             intro: SubstFormP_cong [THEN Iff_MP2_same]
                    SubstFormP_unique [THEN cut2] HRP_unique [THEN cut2])
qed

lemma KRP_subst_fm: "{KRP «Var i» «β» (Var j)}  Var j EQ «β(i::=«β»)»"
  by (metis KRP_unique cut0 prove_KRP)


section‹The Diagonal Lemma and Gödel's Theorem›

lemma diagonal: 
  obtains δ where "{}  δ IFF α(i::=«δ»)"  "supp δ = supp α - {atom i}"
proof -
  obtain k::name and j::name
    where atoms: "atom k  (i,j,α)" "atom j  (i,α)"
    by (metis obtain_fresh)
  define β where "β = Ex j (KRP «Var i» (Var i) (Var j) AND α(i ::= Var j))"
  hence 1: "{}  β(i ::= «β») IFF (Ex j (KRP «Var i» (Var i) (Var j) AND α(i ::= Var j)))(i ::= «β»)"
    by (metis Iff_refl)
  have 2: "{}  (Ex j (KRP «Var i» (Var i) (Var j) AND α(i ::= Var j)))(i ::= «β») IFF
                Ex j (Var j EQ «β(i::=«β»)» AND α(i::=Var j))"
    using atoms
    apply (auto intro!: Ex_cong Conj_cong KRP_subst_fm)
    apply (rule Iff_MP_same [OF Var_Eq_subst_Iff])
    apply (auto intro: prove_KRP thin0)
    done
  have 3: "{}  Ex j (Var j EQ «β(i::=«β»)» AND α(i::=Var j)) IFF α(i::=«β(i::=«β»)»)"
    using atoms
    apply auto
    apply (rule cut_same [OF Iff_MP2_same [OF Var_Eq_subst_Iff AssumeH(2)]])
    apply (auto intro: Ex_I [where x="«β(i::=«β»)»"])
    done
  have "supp (β(i ::= «β»)) = supp α - {atom i}" using atoms
    by (auto simp: fresh_at_base ground_fm_aux_def β_def supp_conv_fresh)
  thus ?thesis using atoms
    by (metis that 1 2 3 Iff_trans)
qed

text‹Gödel's first incompleteness theorem: Our theory is incomplete. NB it is provably consistent›
theorem Goedel_I:
  obtains δ where "{}  δ IFF Neg (PfP «δ»)"  "¬ {}  δ"  "¬ {}  Neg δ"  
                  "eval_fm e δ"  "ground_fm δ"
proof -
  fix i::name
  obtain δ where        "{}  δ IFF Neg ((PfP (Var i))(i::=«δ»))"
             and suppd: "supp δ = supp (Neg (PfP (Var i))) - {atom i}"
    by (metis SyntaxN.Neg diagonal)
  then have diag: "{}  δ IFF Neg (PfP «δ»)"
    by simp
  then have np: "¬ {}  δ  ¬ {}  Neg δ"
    by (metis Iff_MP_same NegNeg_D Neg_D Neg_cong consistent proved_iff_proved_PfP)
  then have "eval_fm e δ" using hfthm_sound [where e=e, OF diag]
    by simp (metis Pf_quot_imp_is_proved)
  moreover have "ground_fm δ" using suppd  
    by (simp add: supp_conv_fresh ground_fm_aux_def subset_eq) (metis fresh_ineq_at_base)
  ultimately show ?thesis
    by (metis diag np that)
qed

end