# Theory Goedel_I

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

theory Goedel_I
imports Pf_Predicates Functions II_Prelims
begin

section‹The Function W and Lemma 6.1›

subsection‹Predicate form, defined on sequences›

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 SeqWRP_sf [iff]:         "Sigma_fm (SeqWRP s k y)"  (is ?thsf)
and SeqWRP_imp_OrdP:         "{SeqWRP s k t} ⊢ OrdP k" (is ?thOrd)
and SeqWRP_LstSeqP:          "{SeqWRP s k t} ⊢ LstSeqP s k t" (is ?thlstseq)
proof -
obtain l::name and sl::name where "atom l ♯ (s,k,sl)" "atom sl ♯ (s)"
by (metis obtain_fresh)
thus ?thesis1 ?thsf ?thOrd ?thlstseq
by (auto intro: LstSeqP_OrdP[THEN cut1])
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›

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 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 ?thsf
by auto
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 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 SeqWRP_Zero: "{} ⊢ SyntaxN.Ex s (SeqWRP (Var s) Zero Zero)"
proof -
obtain l sl :: name where "atom l ♯ (s, sl)" "atom sl ♯ s" by (metis obtain_fresh)
then show ?thesis
apply (subst SeqWRP.simps[of l _ _ sl]; simp)
apply (rule Ex_I[where x="(Eats Zero (HPair Zero Zero))"], simp)
apply (auto intro!: Mem_Eats_I2)
done
qed

lemma WRP_Zero: "{} ⊢ WRP Zero Zero"
by (subst WRP.simps[of undefined]) (auto simp: SeqWRP_Zero)

lemma SeqWRP_HPair_Zero_Zero: "{SeqWRP s k y} ⊢ HPair Zero Zero IN s"
proof -
let ?vs = "(s,k,y)"
obtain l::name and sl::name
where "atom l ♯ (?vs,sl)" "atom sl ♯ (?vs)" by (metis obtain_fresh)
then show ?thesis
by (subst SeqWRP.simps[of l _ _ sl]) auto
qed

lemma SeqWRP_Succ:
assumes "atom s ♯ (s1,k1,y)"
shows "{SeqWRP s1 k1 y} ⊢ SyntaxN.Ex s (SeqWRP (Var s) (SUCC k1) (Q_Succ y))"
proof -
let ?vs = "(s,s1,k1,y)"
obtain l::name and sl::name and l1::name and sl1::name
where atoms:
"atom l ♯ (?vs,sl1,l1,sl)"
"atom sl ♯ (?vs,sl1,l1)"
"atom l1 ♯ (?vs,sl1)"
"atom sl1 ♯ (?vs)"
by (metis obtain_fresh)
let ?hyp = "{RestrictedP s1 (SUCC k1) (Var s), OrdP k1, SeqWRP s1 k1 y}"
show ?thesis
using assms atoms
apply (auto simp: SeqWRP.simps [of l "Var s" _ sl])
apply (rule cut_same [where A="OrdP k1"])
apply (rule SeqWRP_imp_OrdP)
apply (rule cut_same [OF exists_RestrictedP [of s s1 "SUCC k1"]])
apply (rule AssumeH Ex_EH Conj_EH | simp)+
apply (rule Ex_I [where x="Eats (Var s) (HPair (SUCC k1)  (Q_Succ y))"])
apply (simp_all (no_asm_simp))
apply (rule Conj_I)
apply (blast intro: RestrictedP_LstSeqP_Eats[THEN cut2] SeqWRP_LstSeqP[THEN cut1])
apply (rule Conj_I)
apply (rule Mem_Eats_I1)
apply (blast intro: RestrictedP_Mem[THEN cut3] SeqWRP_HPair_Zero_Zero[THEN cut1] Zero_In_SUCC[THEN cut1])
proof (rule All2_SUCC_I, simp_all)
show "?hyp ⊢  SyntaxN.Ex sl
(HPair k1 (Var sl) IN Eats (Var s) (HPair (SUCC k1) (Q_Succ y)) AND
HPair (SUCC k1) (Q_Succ (Var sl)) IN
Eats (Var s) (HPair (SUCC k1) (Q_Succ y)))"
― ‹verifying the final values›
apply (rule Ex_I [where x="y"])
using assms atoms apply simp
apply (rule Conj_I[rotated])
apply (rule Mem_Eats_I2, rule Refl)
apply (rule Mem_Eats_I1)
apply (rule RestrictedP_Mem[THEN cut3])
apply (rule AssumeH)
apply (simp add: LstSeqP_imp_Mem SeqWRP_LstSeqP thin1)
apply (rule Mem_SUCC_Refl)
done
next
show "?hyp ⊢ All2 l k1
(SyntaxN.Ex sl
(HPair (Var l) (Var sl) IN
Eats (Var s) (HPair (SUCC k1) (Q_Succ y)) AND
HPair (SUCC (Var l)) (Q_Succ (Var sl)) IN
Eats (Var s) (HPair (SUCC k1) (Q_Succ y))))"
― ‹verifying the sequence buildup›
apply (rule All_I Imp_I)+
using assms atoms apply simp_all
― ‹... the sequence buildup via s1›
apply (simp add: SeqWRP.simps [of l s1 _ sl])
apply (rule AssumeH Ex_EH Conj_EH)+
apply (rule All2_E [THEN rotate2], auto del: Disj_EH)
apply (rule Ex_I [where x="Var sl"], simp)
apply (rule Conj_I)
apply (blast intro: Mem_Eats_I1 [OF RestrictedP_Mem [THEN cut3]] Mem_SUCC_I1)
apply (blast intro: Mem_Eats_I1 [OF RestrictedP_Mem [THEN cut3]] OrdP_IN_SUCC)
done
qed
qed (*>*)

lemma WRP_Succ: "{OrdP i, WRP i y} ⊢ WRP (SUCC i) (Q_Succ y)"
proof -
obtain s t :: name where "atom s ♯ (i, y)" "atom t ♯ (s,i, y)" by (metis obtain_fresh)
then show ?thesis
by (subst WRP.simps[of s], simp, subst WRP.simps[of t], simp) (force intro: SeqWRP_Succ[THEN cut1])
qed

lemma WRP: "{} ⊢ WRP (ORD_OF i) «ORD_OF i»"
by (induct i)
(auto simp: WRP_Zero quot_Succ intro!: WRP_Succ[THEN cut2])

lemma prove_WRP:  "{} ⊢ WRP «Var x» ««Var x»»"
unfolding quot_Var quot_Succ
by (rule WRP_Succ[THEN cut2]) (auto simp: WRP)

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

section‹The Function HF and Lemma 6.2›

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 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)
and SeqHRP_imp_LstSeqP: "{ SeqHRP x y s k } ⊢ LstSeqP s k (HPair x y)"  (is ?thlstseq)
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 ?thlstseq
by (auto intro: LstSeqP_OrdP)
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›

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 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 ?thsf
by auto
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

lemma HRP_ORD_OF: "{} ⊢ HRP (ORD_OF i) «ORD_OF i»"
proof -
let ?vs = "(i)"
obtain s k 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 s ♯ (?vs,sl,sl',m,n,sm,sm',sn,sn',l,k)"
"atom k ♯ (?vs,sl,sl',m,n,sm,sm',sn,sn',l)"
"atom l ♯ (?vs,sl,sl',m,n,sm,sm',sn,sn')"
"atom sl ♯ (?vs,sl',m,n,sm,sm',sn,sn')" "atom sl' ♯ (?vs,m,n,sm,sm',sn,sn')"
"atom m ♯ (?vs,n,sm,sm',sn,sn')" "atom n ♯ (?vs,sm,sm',sn,sn')"
"atom sm ♯ (?vs,sm',sn,sn')" "atom sm' ♯ (?vs,sn,sn')"
"atom sn ♯ (?vs,sn')" "atom sn' ♯ ?vs"
by (metis obtain_fresh)
then show ?thesis
apply (subst HRP.simps[of s _ _ k]; simp)
apply (subst SeqHRP.simps[of l _ _ sl sl' m n sm sm' sn sn']; simp?)
apply (rule Ex_I[where x="Eats Zero (HPair Zero (HPair (ORD_OF i) «ORD_OF i»))"]; simp)
apply (rule Ex_I[where x="Zero"]; simp)
apply (rule Conj_I[OF LstSeqP_single])
apply (rule All2_SUCC_I, simp)
apply auto [2]
apply (rule Ex_I[where x="ORD_OF i"], simp)
apply (rule Ex_I[where x="«ORD_OF i»"], simp)
apply (auto intro!: Disj_I1 WRP Mem_Eats_I2)
done
qed

lemma SeqHRP_HPair:
assumes "atom s ♯ (k,s1,s2,k1,k2,x,y,x',y')" "atom k ♯ (s1,s2,k1,k2,x,y,x',y')"
shows "{SeqHRP x x' s1 k1,
SeqHRP y y' s2 k2}
⊢ Ex s (Ex k (SeqHRP (HPair x y) (Q_HPair x' y') (Var s) (Var k)))" (*<*)
proof -
let ?vs = "(s1,s2,s,k1,k2,k,x,y,x',y')"
obtain km::name and kn::name and j::name and k'::name
and 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 atoms2: "atom km ♯ (kn,j,k',l,s1,s2,s,k1,k2,k,x,y,x',y',sl,sl',m,n,sm,sm',sn,sn')"
"atom kn ♯ (j,k',l,s1,s2,s,k1,k2,k,x,y,x',y',sl,sl',m,n,sm,sm',sn,sn')"
"atom j ♯ (k',l,s1,s2,s,k1,k2,k,x,y,x',y',sl,sl',m,n,sm,sm',sn,sn')"
and atoms: "atom k' ♯ (l,s1,s2,s,k1,k2,k,x,y,x',y',sl,sl',m,n,sm,sm',sn,sn')"
"atom l ♯ (s1,s2,s,k1,k2,k,x,y,x',y',sl,sl',m,n,sm,sm',sn,sn')"
"atom sl ♯ (s1,s2,s,k1,k2,k,x,y,x',y',sl',m,n,sm,sm',sn,sn')"
"atom sl' ♯ (s1,s2,s,k1,k2,k,x,y,x',y',m,n,sm,sm',sn,sn')"
"atom m ♯ (s1,s2,s,k1,k2,k,x,y,x',y',n,sm,sm',sn,sn')"
"atom n ♯ (s1,s2,s,k1,k2,k,x,y,x',y',sm,sm',sn,sn')"
"atom sm ♯ (s1,s2,s,k1,k2,k,x,y,x',y',sm',sn,sn')"
"atom sm' ♯ (s1,s2,s,k1,k2,k,x,y,x',y',sn,sn')"
"atom sn ♯ (s1,s2,s,k1,k2,k,x,y,x',y',sn')"
"atom sn' ♯ (s1,s2,s,k1,k2,k,x,y,x',y')"
by (metis obtain_fresh)
let ?hyp = "{HaddP k1 k2 (Var k'), OrdP k1, OrdP k2, SeqAppendP s1 (SUCC k1) s2 (SUCC k2) (Var s),
SeqHRP x x' s1 k1, SeqHRP y y' s2 k2}"
show ?thesis
using assms atoms
apply (auto simp: SeqHRP.simps [of l "Var s" _ sl sl' m n sm sm' sn sn'])
apply (rule cut_same [where A="OrdP k1 AND OrdP k2"])
apply (metis Conj_I SeqHRP_imp_OrdP thin1 thin2)
apply (rule cut_same [OF exists_SeqAppendP [of s s1 "SUCC k1" s2 "SUCC k2"]])
apply (rule AssumeH Ex_EH Conj_EH | simp)+
apply (rule cut_same [OF exists_HaddP [where j=k' and x=k1 and y=k2]])
apply (rule AssumeH Ex_EH Conj_EH | simp)+
apply (rule Ex_I [where x="Eats (Var s) (HPair (SUCC(SUCC(Var k'))) (HPair(HPair x y)(Q_HPair x' y')))"])
apply (simp_all (no_asm_simp))
apply (rule Ex_I [where x="SUCC (SUCC (Var k'))"], simp)
apply (rule Conj_I)
apply (blast intro: LstSeqP_SeqAppendP_Eats SeqHRP_imp_LstSeqP [THEN cut1])
proof (rule All2_SUCC_I, simp_all)
show "?hyp ⊢     SyntaxN.Ex sl
(SyntaxN.Ex sl'
(HPair (SUCC (SUCC (Var k'))) (HPair (Var sl) (Var sl')) IN
Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (HPair x y) (Q_HPair x' y'))) AND
(OrdP (Var sl) AND WRP (Var sl) (Var sl') OR
SyntaxN.Ex m
(SyntaxN.Ex n
(SyntaxN.Ex sm
(SyntaxN.Ex sm'
(SyntaxN.Ex sn
(SyntaxN.Ex sn'
(Var m IN SUCC (SUCC (Var k')) AND
Var n IN SUCC (SUCC (Var k')) AND
HPair (Var m) (HPair (Var sm) (Var sm')) IN
Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (HPair x y) (Q_HPair x' y'))) AND
HPair (Var n) (HPair (Var sn) (Var sn')) IN
Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (HPair x y) (Q_HPair x' y'))) AND
Var sl EQ HPair (Var sm) (Var sn) AND Var sl' EQ Q_HPair (Var sm') (Var sn'))))))))))"
― ‹verifying the final values›
apply (rule Ex_I [where x="HPair x y"])
using assms atoms apply simp
apply (rule Ex_I [where x="Q_HPair x' y'"], simp)
apply (rule Conj_I, metis Mem_Eats_I2 Refl)
apply (rule Disj_I2)
apply (rule Ex_I [where x=k1], simp)
apply (rule Ex_I [where x="SUCC (Var k')"], simp)
apply (rule Ex_I [where x=x], simp)
apply (rule_tac x=x' in Ex_I, simp)
apply (rule Ex_I [where x=y], simp)
apply (rule_tac x=y' in Ex_I, simp)
apply (rule Conj_I)
apply (blast intro: HaddP_Mem_I LstSeqP_OrdP Mem_SUCC_I1)
apply (rule Conj_I [OF Mem_SUCC_Refl])
apply (blast intro: Disj_I1 Mem_Eats_I1 Mem_SUCC_Refl SeqHRP_imp_LstSeqP [THEN cut1]
LstSeqP_imp_Mem SeqAppendP_Mem1 [THEN cut3] SeqAppendP_Mem2 [THEN cut4] HaddP_SUCC1 [THEN cut1])
done
next
show "?hyp ⊢  All2 l (SUCC (SUCC (Var k')))
(SyntaxN.Ex sl
(SyntaxN.Ex sl'
(HPair (Var l) (HPair (Var sl) (Var sl')) IN
Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (HPair x y) (Q_HPair x' y'))) AND
(OrdP (Var sl) AND WRP (Var sl) (Var sl') OR
SyntaxN.Ex m
(SyntaxN.Ex n
(SyntaxN.Ex sm
(SyntaxN.Ex sm'
(SyntaxN.Ex sn
(SyntaxN.Ex sn'
(Var m IN Var l AND
Var n IN Var l AND
HPair (Var m) (HPair (Var sm) (Var sm')) IN
Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (HPair x y) (Q_HPair x' y'))) AND
HPair (Var n) (HPair (Var sn) (Var sn')) IN
Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (HPair x y) (Q_HPair x' y'))) AND
Var sl EQ HPair (Var sm) (Var sn) AND Var sl' EQ Q_HPair (Var sm') (Var sn')))))))))))"
― ‹verifying the sequence buildup›
apply (rule cut_same [where A="HaddP (SUCC k1) (SUCC k2) (SUCC (SUCC (Var k')))"])
apply (rule All_I Imp_I)+
using assms atoms atoms2 apply simp_all
apply (rule AssumeH)
apply (blast intro: OrdP_SUCC_I LstSeqP_OrdP)
― ‹... the sequence buildup via s1›
apply (simp add: SeqHRP.simps [of l s1 _ sl sl' m n sm sm' sn sn'])
apply (rule AssumeH Ex_EH Conj_EH)+
apply (rule All2_E [THEN rotate2])
apply (simp | rule AssumeH Ex_EH Conj_EH)+
apply (rule Ex_I [where x="Var sl"], simp)
apply (rule Ex_I [where x="Var sl'"], simp)
apply (rule Conj_I [OF Mem_Eats_I1])
apply (metis SeqAppendP_Mem1 rotate3 thin2 thin4)
apply (rule AssumeH Disj_IE1H Ex_EH Conj_EH)+
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_all (no_asm_simp))
apply (rule Conj_I, rule AssumeH)+
apply (rule Conj_I)
apply (blast intro: OrdP_Trans [OF OrdP_SUCC_I] Mem_Eats_I1 [OF SeqAppendP_Mem1 [THEN cut3]] Hyp)
apply (blast intro: Disj_I1 Disj_I2 OrdP_Trans [OF OrdP_SUCC_I] Mem_Eats_I1 [OF SeqAppendP_Mem1 [THEN cut3]] Hyp)
― ‹... the sequence buildup via s2›
apply (simp add: SeqHRP.simps [of l s2 _ sl sl' m n sm sm' sn sn'])
apply (rule AssumeH Ex_EH Conj_EH)+
apply (rule All2_E [THEN rotate2])
apply (simp | rule AssumeH Ex_EH Conj_EH)+
apply (rule Ex_I [where x="Var sl"], simp)
apply (rule Ex_I [where x="Var sl'"], simp)
apply (rule cut_same [where A="OrdP (Var j)"])
apply (rule Conj_I)
apply (blast intro: Mem_Eats_I1 SeqAppendP_Mem2 [THEN cut4] del: Disj_EH)
apply (rule AssumeH Disj_IE1H Ex_EH Conj_EH)+
apply (rule cut_same [OF exists_HaddP [where j=km and x="SUCC k1" and y="Var m"]])
apply (blast intro: Ord_IN_Ord, simp)
apply (rule cut_same [OF exists_HaddP [where j=kn and x="SUCC k1" and y="Var n"]])
apply (metis AssumeH(6) Ord_IN_Ord0 rotate8, simp)
apply (rule AssumeH Ex_EH Conj_EH | simp)+
apply (rule Ex_I [where x="Var km"], simp)
apply (rule Ex_I [where x="Var kn"], 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_all (no_asm_simp))
apply (rule Conj_I [OF _ Conj_I])
apply (blast intro!: HaddP_Mem_cancel_left [THEN Iff_MP2_same] OrdP_SUCC_I intro: LstSeqP_OrdP Hyp)+
apply (blast del: Disj_EH  intro: OrdP_Trans Hyp
intro!: Mem_Eats_I1 SeqAppendP_Mem2 [THEN cut4] HaddP_imp_OrdP [THEN cut1])
done
qed
qed (*>*)

lemma HRP_HPair: "{HRP x x', HRP y y'} ⊢ HRP (HPair x y) (Q_HPair x' y')"
proof -
obtain k1::name and s1::name and k2::name and s2::name and k::name and s::name
where "atom s1 ♯ (x,y,x',y')"        "atom k1 ♯ (x,y,x',y',s1)"
"atom s2 ♯ (x,y,x',y',k1,s1)"  "atom k2 ♯ (x,y,x',y',s2,k1,s1)"
"atom s  ♯ (x,y,x',y',k2,s2,k1,s1)" "atom k  ♯ (x,y,x',y',s,k2,s2,k1,s1)"
by (metis obtain_fresh)
thus ?thesis
by (force simp: HRP.simps [of s "HPair x y" _ k]
HRP.simps [of s1 x _ k1]
HRP.simps [of s2 y _ k2]
intro: SeqHRP_HPair [THEN cut2])
qed

lemma HRP_HPair_quot: "{HRP x «x», HRP y «y»} ⊢ HRP (HPair x y) «HPair x y»"
using HRP_HPair[of x "«x»" y "«y»"]
unfolding HPair_def quot_simps by auto

lemma prove_HRP_coding_tm: fixes t::tm shows "coding_tm t ⟹ {} ⊢ HRP t «t»"
by (induct t rule: coding_tm.induct)
(auto simp: quot_simps HRP_ORD_OF HRP_HPair_quot[THEN cut2])

lemmas prove_HRP = prove_HRP_coding_tm[OF quot_fm_coding]

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»)»"
using SubstFormP by blast

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)

end

```