# Theory Forcing_Notions

sectionâ¹Forcing notionsâº
textâ¹This theory defines a locale for forcing notions, that is,
preorders with a distinguished maximum element.âº

theory Forcing_Notions
imports
"ZF-Constructible.Relative"
"Delta_System_Lemma.ZF_Library"
begin

subsectionâ¹Basic conceptsâº
textâ¹We say that two elements $p,q$ are
ââ¹compatibleâº if they have a lower bound in $P$âº
definition compat_in :: "iâiâiâiâo" where

lemma compat_inI :

lemma refl_compat:
"â¦ refl(A,r) ; â¨p,qâ© â r | p=q | â¨q,pâ© â r ; pâA ; qâAâ§ â¹ compat_in(A,r,p,q)"
by (auto simp add: refl_def compat_inI)

lemma  chain_compat:
"refl(A,r) â¹ linear(A,r) â¹  (âpâA.âqâA. compat_in(A,r,p,q))"

lemma subset_fun_image: "f:NâP â¹ fNâP"
by (auto simp add: image_fun apply_funtype)

lemma refl_monot_domain: "refl(B,r) â¹ AâB â¹ refl(A,r)"
unfolding refl_def by blast

locale forcing_notion =
fixes P leq one
assumes one_in_P:       "one â P"
and leq_preord:       "preorder_on(P,leq)"
begin

notation one (â¹ð­âº)

abbreviation Leq :: "[i, i] â o"  (infixl "â¼" 50)
where "x â¼ y â¡ â¨x,yâ©âleq"

lemma refl_leq:
"râP â¹ râ¼r"
using leq_preord unfolding preorder_on_def refl_def by simp

textâ¹A set $D$ is ââ¹denseâº if every element $p\in P$ has a lower
bound in $D$.âº
definition
dense :: "iâo" where
"dense(D) â¡ âpâP. âdâD . dâ¼p"

textâ¹There is also a weaker definition which asks for
a lower bound in $D$ only for the elements below some fixed
element $q$.âº
definition
dense_below :: "iâiâo" where
"dense_below(D,q) â¡ âpâP. pâ¼q â¶ (âdâD. dâP â§ dâ¼p)"

lemma P_dense: "dense(P)"
by (insert leq_preord, auto simp add: preorder_on_def refl_def dense_def)

definition
increasing :: "iâo" where
"increasing(F) â¡ âxâF. â p â P . xâ¼p â¶ pâF"

definition
compat :: "iâiâo" where
"compat(p,q) â¡ compat_in(P,leq,p,q)"

lemma leq_transD:  "aâ¼b â¹ bâ¼c â¹ a â Pâ¹ b â Pâ¹ c â Pâ¹ aâ¼c"
using leq_preord trans_onD unfolding preorder_on_def by blast

lemma leq_transD':  "AâP â¹ aâ¼b â¹ bâ¼c â¹ a â A â¹ b â Pâ¹ c â Pâ¹ aâ¼c"
using leq_preord trans_onD subsetD unfolding preorder_on_def by blast

lemma compatD[dest!]: "compat(p,q) â¹ âdâP. dâ¼p â§ dâ¼q"
unfolding compat_def compat_in_def .

abbreviation Incompatible :: "[i, i] â o"  (infixl "â¥" 50)
where "p â¥ q â¡ Â¬ compat(p,q)"

lemma compatI[intro!]: "dâP â¹ dâ¼p â¹ dâ¼q â¹ compat(p,q)"
unfolding compat_def compat_in_def by blast

lemma denseD [dest]: "dense(D) â¹ pâP â¹  âdâD. dâ¼ p"
unfolding dense_def by blast

lemma denseI [intro!]: "â¦ âp. pâP â¹ âdâD. dâ¼ p â§ â¹ dense(D)"
unfolding dense_def by blast

lemma dense_belowD [dest]:
assumes "dense_below(D,p)" "qâP" "qâ¼p"
shows "âdâD. dâP â§ dâ¼q"
using assms unfolding dense_below_def by simp

lemma dense_belowI [intro!]:
assumes "âq. qâP â¹ qâ¼p â¹ âdâD. dâP â§ dâ¼q"
shows "dense_below(D,p)"
using assms unfolding dense_below_def by simp

lemma dense_below_cong: "pâP â¹ D = D' â¹ dense_below(D,p) â· dense_below(D',p)"
by blast

lemma dense_below_cong': "pâP â¹ â¦âx. xâP â¹ Q(x) â· Q'(x)â§ â¹
dense_below({qâP. Q(q)},p) â· dense_below({qâP. Q'(q)},p)"
by blast

lemma dense_below_mono: "pâP â¹ D â D' â¹ dense_below(D,p) â¹ dense_below(D',p)"
by blast

lemma dense_below_under:
assumes "dense_below(D,p)" "pâP" "qâP" "qâ¼p"
shows "dense_below(D,q)"
using assms leq_transD by blast

lemma ideal_dense_below:
assumes "âq. qâP â¹ qâ¼p â¹ qâD"
shows "dense_below(D,p)"
using assms refl_leq by blast

lemma dense_below_dense_below:
assumes "dense_below({qâP. dense_below(D,q)},p)" "pâP"
shows "dense_below(D,p)"
using assms leq_transD refl_leq  by blast

textâ¹A filter is an increasing set $G$ with all its elements
being compatible in $G$.âº
definition
filter :: "iâo" where
"filter(G) â¡ GâP â§ increasing(G) â§ (âpâG. âqâG. compat_in(G,leq,p,q))"

lemma filterD : "filter(G) â¹ x â G â¹ x â P"
by (auto simp add : subsetD filter_def)

lemma filter_leqD : "filter(G) â¹ x â G â¹ y â P â¹ xâ¼y â¹ y â G"

lemma filter_imp_compat: "filter(G) â¹ pâG â¹ qâG â¹ compat(p,q)"
unfolding filter_def compat_in_def compat_def by blast

lemma low_bound_filter: â â¹says the compatibility is attained inside Gâº
assumes "filter(G)" and "pâG" and "qâG"
shows "ârâG. râ¼p â§ râ¼q"
using assms
unfolding compat_in_def filter_def by blast

textâ¹We finally introduce the upward closure of a set
and prove that the closure of $A$ is a filter if its elements are
compatible in $A$.âº
definition
upclosure :: "iâi" where
"upclosure(A) â¡ {pâP.âaâA. aâ¼p}"

lemma  upclosureI [intro] : "pâP â¹ aâA â¹ aâ¼p â¹ pâupclosure(A)"

lemma  upclosureE [elim] :
"pâupclosure(A) â¹ (âx a. xâP â¹ aâA â¹ aâ¼x â¹ R) â¹ R"

lemma  upclosureD [dest] :
"pâupclosure(A) â¹ âaâA.(aâ¼p) â§ pâP"

lemma upclosure_increasing :
assumes "AâP"
shows "increasing(upclosure(A))"
unfolding increasing_def upclosure_def
using leq_transD'[OF â¹AâPâº] by auto

lemma  upclosure_in_P: "A â P â¹ upclosure(A) â P"
using subsetI upclosure_def by simp

lemma  A_sub_upclosure: "A â P â¹ Aâupclosure(A)"
using subsetI leq_preord
unfolding upclosure_def preorder_on_def refl_def by auto

lemma  elem_upclosure: "AâP â¹ xâA  â¹ xâupclosure(A)"
by (blast dest:A_sub_upclosure)

lemma  closure_compat_filter:
assumes "AâP" "(âpâA.âqâA. compat_in(A,leq,p,q))"
shows "filter(upclosure(A))"
unfolding filter_def
proof(auto)
show "increasing(upclosure(A))"
using assms upclosure_increasing by simp
next
let ?UA="upclosure(A)"
show "compat_in(upclosure(A), leq, p, q)" if "pâ?UA" "qâ?UA" for p q
proof -
from that
obtain a b where 1:"aâA" "bâA" "aâ¼p" "bâ¼q" "pâP" "qâP"
using upclosureD[OF â¹pâ?UAâº] upclosureD[OF â¹qâ?UAâº] by auto
with assms(2)
obtain d where "dâA" "dâ¼a" "dâ¼b"
unfolding compat_in_def by auto
with 1
have "dâ¼p" "dâ¼q" "dâ?UA"
using A_sub_upclosure[THEN subsetD] â¹AâPâº
leq_transD'[of A d a] leq_transD'[of A d b] by auto
then
show ?thesis unfolding compat_in_def by auto
qed
qed

lemma  aux_RS1:  "f â N â P â¹ nâN â¹ fn â upclosure(f N)"
using elem_upclosure[OF subset_fun_image] image_fun
by (simp, blast)

lemma decr_succ_decr:
assumes "f â nat â P" "preorder_on(P,leq)"
"ânânat.  â¨f  succ(n), f  nâ© â leq"
"mânat"
shows "nânat â¹ nâ¤m â¹ â¨f  m, f  nâ© â leq"
using â¹mâ_âº
proof(induct m)
case 0
then show ?case using assms refl_leq by simp
next
case (succ x)
then
have 1:"fsucc(x) â¼ fx" "fnâP" "fxâP" "fsucc(x)âP"
using assms by simp_all
consider (lt) "n<succ(x)" | (eq) "n=succ(x)"
using succ le_succ_iff by auto
then
show ?case
proof(cases)
case lt
with 1 show ?thesis using leI succ leq_transD by auto
next
case eq
with 1 show ?thesis using refl_leq by simp
qed
qed

lemma decr_seq_linear:
assumes "refl(P,leq)" "f â nat â P"
"ânânat.  â¨f  succ(n), f  nâ© â leq"
"trans[P](leq)"
shows "linear(f  nat, leq)"
proof -
have "preorder_on(P,leq)"
unfolding preorder_on_def using assms by simp
{
fix n m
assume "nânat" "mânat"
then
have "fm â¼ fn â¨ fn â¼ fm"
proof(cases "mâ¤n")
case True
with â¹nâ_âº â¹mâ_âº
show ?thesis
using decr_succ_decr[of f n m] assms leI â¹preorder_on(P,leq)âº by simp
next
case False
with â¹nâ_âº â¹mâ_âº
show ?thesis
using decr_succ_decr[of f m n] assms leI not_le_iff_lt â¹preorder_on(P,leq)âº by simp
qed
}
then
show ?thesis
unfolding linear_def using ball_image_simp assms by auto
qed

end â â¹\<^locale>â¹forcing_notionâºâº

subsectionâ¹Towards Rasiowa-Sikorski Lemma (RSL)âº
locale countable_generic = forcing_notion +
fixes ð
assumes countable_subs_of_P:  "ð â natâPow(P)"
and     seq_of_denses:        "ân â nat. dense(ðn)"

begin

definition
D_generic :: "iâo" where
"D_generic(G) â¡ filter(G) â§ (ânânat.(ðn)â©Gâ 0)"

textâ¹The next lemma identifies a sufficient condition for obtaining
RSL.âº
lemma RS_sequence_imp_rasiowa_sikorski:
assumes
"pâP" "f : natâP" "f  0 = p"
"ân. nânat â¹ f  succ(n)â¼ f  n â§ f  succ(n) â ð  n"
shows
"âG. pâG â§ D_generic(G)"
proof -
note assms
moreover from this
have "fnat  â P"
moreover from calculation
have "refl(fnat, leq) â§ trans[P](leq)"
using leq_preord unfolding preorder_on_def by (blast intro:refl_monot_domain)
moreover from calculation
have "ânânat.  f  succ(n)â¼ f  n" by (simp)
moreover from calculation
have "linear(fnat, leq)"
using leq_preord and decr_seq_linear unfolding preorder_on_def by (blast)
moreover from calculation
have "(âpâfnat.âqâfnat. compat_in(fnat,leq,p,q))"
using chain_compat by (auto)
ultimately
have "filter(upclosure(fnat))" (is "filter(?G)")
using closure_compat_filter by simp
moreover
have "ânânat. ð  n â© ?G â  0"
proof
fix n
assume "nânat"
with assms
have "fsucc(n) â ?G â§ fsucc(n) â ð  n"
using aux_RS1 by simp
then
show "ð  n â© ?G â  0"  by blast
qed
moreover from assms
have "p â ?G"
using aux_RS1 by auto
ultimately
show ?thesis unfolding D_generic_def by auto
qed

end â â¹\<^locale>â¹countable_genericâºâº

textâ¹Now, the following recursive definition will fulfill the
requirements of lemma \<^term>â¹RS_sequence_imp_rasiowa_sikorskiâº âº

consts RS_seq :: "[i,i,i,i,i,i] â i"
primrec
"RS_seq(0,P,leq,p,enum,ð) = p"
"RS_seq(succ(n),P,leq,p,enum,ð) =
enum(Î¼ m. â¨enumm, RS_seq(n,P,leq,p,enum,ð)â© â leq â§ enumm â ð  n)"

context countable_generic
begin

lemma countable_RS_sequence_aux:
fixes p enum
defines "f(n) â¡ RS_seq(n,P,leq,p,enum,ð)"
and   "Q(q,k,m) â¡ enummâ¼ q â§ enumm â ð  k"
assumes "nânat" "pâP" "P â range(enum)" "enum:natâM"
"âx k. xâP â¹ kânat â¹  âqâP. qâ¼ x â§ q â ð  k"
shows
"f(succ(n)) â P â§ f(succ(n))â¼ f(n) â§ f(succ(n)) â ð  n"
using â¹nânatâº
proof (induct)
case 0
from assms
obtain q where "qâP" "qâ¼ p" "q â ð  0" by blast
moreover from this and â¹P â range(enum)âº
obtain m where "mânat" "enumm = q"
using Pi_rangeD[OF â¹enum:natâMâº] by blast
moreover
have "ð0 â P"
using apply_funtype[OF countable_subs_of_P] by simp
moreover note â¹pâPâº
ultimately
show ?case
using LeastI[of "Q(p,0)" m] unfolding Q_def f_def by auto
next
case (succ n)
with assms
obtain q where "qâP" "qâ¼ f(succ(n))" "q â ð  succ(n)" by blast
moreover from this and â¹P â range(enum)âº
obtain m where "mânat" "enummâ¼ f(succ(n))" "enumm â ð  succ(n)"
using Pi_rangeD[OF â¹enum:natâMâº] by blast
moreover note succ
moreover from calculation
have "ðsucc(n) â P"
using apply_funtype[OF countable_subs_of_P] by auto
ultimately
show ?case
using LeastI[of "Q(f(succ(n)),succ(n))" m] unfolding Q_def f_def by auto
qed

lemma countable_RS_sequence:
fixes p enum
defines "f â¡ Î»nânat. RS_seq(n,P,leq,p,enum,ð)"
and   "Q(q,k,m) â¡ enummâ¼ q â§ enumm â ð  k"
assumes "nânat" "pâP" "P â range(enum)" "enum:natâM"
shows
"f0 = p" "fsucc(n)â¼ fn â§ fsucc(n) â ð  n" "fsucc(n) â P"
proof -
from assms
show "f0 = p" by simp
{
fix x k
assume "xâP" "kânat"
then
have "âqâP. qâ¼ x â§ q â ð  k"
using seq_of_denses apply_funtype[OF countable_subs_of_P]
unfolding dense_def by blast
}
with assms
show "fsucc(n)â¼ fn â§ fsucc(n) â ð  n" "fsucc(n)âP"
unfolding f_def using countable_RS_sequence_aux by simp_all
qed

lemma RS_seq_type:
assumes "n â nat" "pâP" "P â range(enum)" "enum:natâM"
shows "RS_seq(n,P,leq,p,enum,ð) â P"
using assms countable_RS_sequence(1,3)
by (induct;simp)

lemma RS_seq_funtype:
assumes "pâP" "P â range(enum)" "enum:natâM"
shows "(Î»nânat. RS_seq(n,P,leq,p,enum,ð)): nat â P"
using assms lam_type RS_seq_type by auto

lemmas countable_rasiowa_sikorski =
RS_sequence_imp_rasiowa_sikorski[OF _ RS_seq_funtype countable_RS_sequence(1,2)]

end â â¹\<^locale>â¹countable_genericâºâº

end


# Theory Cohen_Posets_Relative

sectionâ¹Cohen forcing notionsâº

theory Cohen_Posets_Relative
imports
Forcing_Notions
Transitive_Models.Delta_System_Relative
Transitive_Models.Partial_Functions_Relative
begin

locale cohen_data =
fixes Îº I J::i
assumes zero_lt_kappa: "0<Îº"
begin

lemmas zero_lesspoll_kappa = zero_lesspoll[OF zero_lt_kappa]

end â â¹\<^locale>â¹cohen_dataâºâº

locale add_reals = cohen_data nat _ 2

subsectionâ¹Combinatorial results on Cohen posetsâº

sublocale cohen_data â forcing_notion "Fn(Îº,I,J)" "Fnle(Îº,I,J)" 0
proof
show "0 â Fn(Îº, I, J)"
using zero_lt_kappa zero_in_Fn by simp
then
show "âpâFn(Îº, I, J). â¨p, 0â© â Fnle(Îº, I, J)"
unfolding preorder_on_def refl_def trans_on_def
by auto
next
show "preorder_on(Fn(Îº, I, J), Fnle(Îº, I, J))"
unfolding preorder_on_def refl_def trans_on_def
by blast
qed

context cohen_data
begin

lemma compat_imp_Un_is_function:
assumes "G â Fn(Îº, I, J)" "âp q. p â G â¹ q â G â¹ compat(p,q)"
shows "function(âG)"
unfolding function_def
proof (intro allI ballI impI)
fix x y y'
then
obtain p q where "â¨x, yâ© â p" "â¨x, y'â© â q" "p â G" "q â G"
by auto
moreover from this and assms
obtain r where "r â Fn(Îº, I, J)" "r â p" "r â q"
using compatD[of p q] by force
moreover from this
have "function(r)"
using Fn_is_function by simp
ultimately
show "y = y'"
unfolding function_def by fastforce
qed

(* MOVE THIS to an appropriate place *)
lemma filter_subset_notion: "filter(G) â¹ G â Fn(Îº, I, J)"
unfolding filter_def by simp

lemma Un_filter_is_function: "filter(G) â¹ function(âG)"
using compat_imp_Un_is_function filter_imp_compat[of G]
filter_subset_notion
by simp

end â â¹\<^locale>â¹cohen_dataâºâº

locale M_cohen = M_delta +
assumes
countable_lepoll_assms2:
"M(A') â¹ M(A) â¹ M(b) â¹ M(f) â¹ separation(M, Î»y. âxâA'. y = â¨x, Î¼ i. x â if_range_F_else_F(Î»a. {p â A . domain(p) = a}, b, f, i)â©)"
and
countable_lepoll_assms3:
"M(A) â¹ M(f) â¹ M(b) â¹ M(D) â¹ M(r') â¹ M(A')â¹
separation(M, Î»y. âxâA'. y = â¨x, Î¼ i. x â if_range_F_else_F(drSR_Y(r', D, A), b, f, i)â©)"

context M_cardinal_library
begin

lemma lesspoll_nat_imp_lesspoll_rel:
assumes "A âº Ï" "M(A)"
shows "A âºâMâ Ï"
proof -
note assms
moreover from this
obtain f n where "fâbijâMâ(A,n)" "nâÏ" "A ââMâ n"
using lesspoll_nat_is_Finite Finite_rel_def[of M A]
by auto
moreover from calculation
have "A â²âMâ Ï"
using lesspoll_nat_is_Finite Infinite_imp_nats_lepoll_rel[of Ï n]
nat_not_Finite eq_lepoll_rel_trans[of A n Ï]
by auto
moreover from calculation
have "Â¬ g â bijâMâ(A,Ï)" for g
using mem_bij_rel unfolding lesspoll_def by auto
ultimately
show ?thesis
unfolding lesspoll_rel_def
by auto
qed

lemma Finite_imp_lesspoll_rel_nat:
assumes "Finite(A)" "M(A)"
shows "A âºâMâ Ï"
using Finite_imp_lesspoll_nat assms lesspoll_nat_imp_lesspoll_rel
by auto

lemma InfCard_rel_lesspoll_rel_Un:
includes Ord_dests
assumes "InfCard_rel(M,Îº)" "A âºâMâ Îº" "B âºâMâ Îº"
and types: "M(Îº)" "M(A)" "M(B)"
shows "A âª B âºâMâ Îº"
proof -
from assms
have "|A|âMâ < Îº" "|B|âMâ < Îº"
using lesspoll_rel_cardinal_rel_lt InfCard_rel_is_Card_rel
by auto
show ?thesis
proof (cases "Finite(A) â§ Finite(B)")
case True
with assms
show ?thesis
using lesspoll_rel_trans2[OF _ le_imp_lepoll_rel, of _ nat Îº]
Finite_imp_lesspoll_rel_nat[OF Finite_Un]
unfolding InfCard_rel_def
by simp
next
case False
with types
have "InfCard_rel(M,max(|A|âMâ,|B|âMâ))"
using Infinite_InfCard_rel_cardinal_rel InfCard_rel_is_Card_rel
le_trans[of nat] not_le_iff_lt[THEN iffD1, THEN leI, of "|A|âMâ" "|B|âMâ"]
unfolding max_def InfCard_rel_def
by auto
with â¹M(A)âº â¹M(B)âº
have "|A âª B|âMâ â¤ max(|A|âMâ,|B|âMâ)"
using cardinal_rel_Un_le[of "max(|A|âMâ,|B|âMâ)" A B]
not_le_iff_lt[THEN iffD1, THEN leI, of "|A|âMâ" "|B|âMâ" ]
unfolding max_def
by simp
moreover from â¹|A|âMâ < Îºâº â¹|B|âMâ < Îºâº
have "max(|A|âMâ,|B|âMâ) < Îº"
unfolding max_def
by simp
ultimately
have "|A âª B|âMâ <  Îº"
using lt_trans1
by blast
moreover
note â¹InfCard_rel(M,Îº)âº
moreover from calculation types
have "|A âª B|âMâ âºâMâ Îº"
using lt_Card_rel_imp_lesspoll_rel InfCard_rel_is_Card_rel
by simp
ultimately
show ?thesis
using cardinal_rel_eqpoll_rel eq_lesspoll_rel_trans[of "A âª B" "|A âª B|âMâ" Îº]
eqpoll_rel_sym types
by simp
qed
qed

end â â¹\<^locale>â¹M_cardinal_libraryâºâº

lemma (in M_cohen) Fn_rel_unionI:
assumes "p â FnâMâ(Îº,I,J)" "qâFnâMâ(Îº,I,J)" "InfCardâMâ(Îº)"
"M(Îº)" "M(I)" "M(J)" "domain(p) â© domain(q) = 0"
shows "pâªq â FnâMâ(Îº,I,J)"
proof -
note assms
moreover from calculation
have "p âºâMâ Îº" "q âºâMâ Îº" "M(p)" "M(q)"
using Fn_rel_is_function by simp_all
moreover from calculation
have "pâªq âºâMâ Îº"
using eqpoll_rel_sym cardinal_rel_eqpoll_rel InfCard_rel_lesspoll_rel_Un
by simp_all
ultimately
show ?thesis
unfolding Fn_rel_def
using pfun_unionI cardinal_rel_eqpoll_rel eq_lesspoll_rel_trans[OF _ â¹pâªq âºâMâ _âº]
by auto
qed

lemma (in M_cohen) restrict_eq_imp_compat_rel:
assumes "p â FnâMâ(Îº, I, J)" "q â FnâMâ(Îº, I, J)" "InfCardâMâ(Îº)" "M(J)" "M(Îº)"
shows "p âª q â FnâMâ(Îº, I, J)"
proof -
note assms
moreover from calculation
have "p âºâMâ Îº" "q âºâMâ Îº" "M(p)" "M(q)"
using Fn_rel_is_function by simp_all
moreover from calculation
have "pâªq âºâMâ Îº"
using InfCard_rel_lesspoll_rel_Un cardinal_rel_eqpoll_rel[THEN eqpoll_rel_sym]
by auto
ultimately
show ?thesis
unfolding Fn_rel_def
using pfun_restrict_eq_imp_compat cardinal_rel_eqpoll_rel
eq_lesspoll_rel_trans[OF _ â¹pâªq âºâMâ _âº]
by auto
qed

lemma (in M_cohen) InfCard_rel_imp_n_lesspoll_rel :
assumes "InfCardâMâ(Îº)" "M(Îº)" "nâÏ"
shows "n âºâMâ Îº"
proof -
note assms
moreover from this
have "n âºâMâ Ï"
using n_lesspoll_rel_nat by simp
ultimately
show ?thesis
using lesspoll_rel_trans2 Infinite_iff_lepoll_rel_nat InfCard_rel_imp_Infinite nat_into_M
by simp
qed

lemma (in M_cohen) cons_in_Fn_rel:
assumes "x â domain(p)" "p â FnâMâ(Îº,I,J)" "x â I" "j â J" "InfCardâMâ(Îº)"
"M(Îº)" "M(I)" "M(J)"
using assms cons_eq Fn_rel_unionI[OF Fn_rel_singletonI[of x I j J] â¹pâ_âº]
InfCard_rel_imp_n_lesspoll_rel
by auto

lemma (in M_library) Fnle_rel_Aleph_rel1_closed[intro,simp]:
"M(FnleâMâ(âµâ1ââMâ, âµâ1ââMâ, Ï ââMâ 2))"
by simp

begin

lemmas zero_lesspoll_rel_kappa = zero_lesspoll_rel[OF zero_lt_kappa]

(* MOVE THIS to some appropriate place. Notice that in Forcing_Notions
we don't import anything relative. *)
relativize relational "compat_in" "is_compat_in" external
synthesize "compat_in" from_definition "is_compat_in" assuming "nonempty"
context
notes Un_assoc[simp] Un_trasposition_aux2[simp]
begin
arity_theorem for "compat_in_fm"
end

lemma (in M_trivial) compat_in_abs[absolut]:
assumes
"M(A)" "M(r)" "M(p)" "M(q)"
shows
"is_compat_in(M,A,r,p,q) â· compat_in(A,r,p,q)"
using assms unfolding is_compat_in_def compat_in_def by simp

definition
antichain :: "iâiâiâo" where
"antichain(P,leq,A) â¡ AâP â§ (âpâA. âqâA. pâ q â¶ Â¬compat_in(P,leq,p,q))"

relativize relational  "antichain" "antichain_rel"
definition
ccc :: "i â i â o" where
"ccc(P,leq) â¡ âA. antichain(P,leq,A) â¶ |A| â¤ nat"

abbreviation
antichain_rel_abbr :: "[iâo,i,i,i] â o" (â¹antichainâ_â'(_,_,_')âº) where
"antichainâMâ(P,leq,A) â¡ antichain_rel(M,P,leq,A)"

abbreviation
antichain_r_set :: "[i,i,i,i] â o" (â¹antichainâ_â'(_,_,_')âº) where
"antichainâMâ(P,leq,A) â¡ antichain_rel(##M,P,leq,A)"

context M_trivial
begin

lemma antichain_abs [absolut]:
"â¦ M(A); M(P); M(leq) â§ â¹ antichainâMâ(P,leq,A) â· antichain(P,leq,A)"
unfolding antichain_rel_def antichain_def by (simp add:absolut)

end â â¹\<^locale>â¹M_trivialâºâº

relativize relational "ccc" "ccc_rel"

abbreviation
ccc_rel_abbr :: "[iâo,i,i]âo" (â¹cccâ_â'(_,_')âº) where
"ccc_rel_abbr(M) â¡ ccc_rel(M)"

abbreviation
ccc_r_set :: "[i,i,i]âo" (â¹cccâ_â'(_,_')âº) where
"ccc_r_set(M) â¡ ccc_rel(##M)"

context M_cardinals
begin

lemma def_ccc_rel:
shows
"cccâMâ(P,leq) â· (âA[M]. antichainâMâ(P,leq,A) â¶ |A|âMâ â¤ Ï)"
using is_cardinal_iff

end â â¹\<^locale>â¹M_cardinalsâºâº

context M_FiniteFun
begin

lemma Fnle_nat_closed[intro,simp]:
assumes "M(I)" "M(J)"
shows "M(Fnle(Ï,I,J))"
unfolding Fnle_def Fnlerel_def Rrel_def
using supset_separation FiniteFun_closed Fn_nat_eq_FiniteFun assms by simp

lemma Fn_nat_closed:
assumes "M(A)" "M(B)" shows "M(Fn(Ï,A,B))"
using assms Fn_nat_eq_FiniteFun
by simp

end â â¹\<^locale>â¹M_FiniteFunâºâº

begin

lemma lam_replacement_drSR_Y: "M(A) â¹ M(D) â¹ M(r') â¹ lam_replacement(M, drSR_Y(r',D,A))"
using lam_replacement_drSR_Y
by simp

lemma (in M_trans) mem_F_bound3:
fixes F A
defines "F â¡ dC_F"
shows "xâF(A,c) â¹ c â (range(f) âª {domain(x). xâA})"
using apply_0 unfolding F_def
by (cases "M(c)", auto simp:F_def drSR_Y_def dC_F_def)

lemma ccc_rel_Fn_nat:
assumes "M(I)"
shows "cccâMâ(Fn(nat,I,2), Fnle(nat,I,2))"
proof -
have repFun_dom_closed:"M({domain(p) . p â A})" if "M(A)" for A
using RepFun_closed domain_replacement_simp transM[OF _ â¹M(A)âº] that
by auto
from assms
have "M(Fn(nat,I,2))" using Fn_nat_eq_FiniteFun by simp
{
fix A
assume "Â¬ |A|âMâ â¤ nat" "M(A)" "A â Fn(nat, I, 2)"
moreover from this
have "countable_rel(M,{pâA. domain(p) = d})" if "M(d)" for d
proof (cases "dâºâMânat â§ d â I")
case True
with â¹A â Fn(nat, I, 2)âº â¹M(A)âº
have "{p â A . domain(p) = d} â d ââMâ 2"
using domain_of_fun function_space_rel_char[of _ 2]
by (auto,subgoal_tac "M(domain(x))",simp_all add:transM[of _ A],force)
moreover from True â¹M(d)âº
have "Finite(d ââMâ 2)"
using Finite_Pi[THEN  subset_Finite, of _ d "Î»_. 2"]
lesspoll_rel_nat_is_Finite_rel function_space_rel_char[of _ 2]
by auto
moreover from â¹M(d)âº
have "M(d ââMâ 2)"
by simp
moreover from â¹M(A)âº
have "M({p â A . domain(p) = d})"
using separation_closed domain_eq_separation[OF â¹M(d)âº] by simp
ultimately
show ?thesis using subset_Finite[of _ "dââMâ2" ]
by (auto intro!:Finite_imp_countable_rel)
next
case False
with â¹A â Fn(nat, I, 2)âº â¹M(A)âº
have "domain(p) â  d" if "pâA" for p
proof -
note False that â¹M(A)âº
moreover from this
obtain d' where "d' â I" "pâd' â 2" "d' âº Ï"
using FnD[OF subsetD[OF â¹Aâ_âº â¹pâAâº]]
by auto
moreover from this
have "p â d'" "domain(p) = d'"
using function_eqpoll Pi_iff
by auto
ultimately
show ?thesis
using lesspoll_nat_imp_lesspoll_rel transM[of p]
by auto
qed
then
show ?thesis
using empty_lepoll_relI by auto
qed
have 2:"M(x) â¹ x â dC_F(X, i) â¹ M(i)" for x X i
unfolding dC_F_def
by auto
moreover
have "uncountable_rel(M,{domain(p) . p â A})"
proof
interpret M_replacement_lepoll M dC_F
using lam_replacement_dC_F domain_eq_separation lam_replacement_inj_rel
unfolding dC_F_def
proof(unfold_locales,simp_all)
fix X b f
assume "M(X)" "M(b)" "M(f)"
with 2[of X]
show "lam_replacement(M, Î»x. Î¼ i. x â if_range_F_else_F(Î»d. {p â X . domain(p) = d}, b, f, i))"
using lam_replacement_dC_F domain_eq_separation
mem_F_bound3 countable_lepoll_assms2 repFun_dom_closed
by (rule_tac lam_Least_assumption_general[where U="Î»_. {domain(x). xâX}"],auto)
qed (auto)
have "âaâA. x = domain(a) â¹ M(dC_F(A,x))" for x
using â¹M(A)âº transM[OF _ â¹M(A)âº] by (auto)
moreover
have "w â A â§ domain(w) = x â¹ M(x)" for w x
using transM[OF _ â¹M(A)âº] by auto
ultimately
interpret M_cardinal_UN_lepoll _ "dC_F(A)" "{domain(p). pâA}"
using lam_replacement_dC_F lam_replacement_inj_rel â¹M(A)âº
lepoll_assumptions domain_eq_separation
countable_lepoll_assms2 repFun_dom_closed
lepoll_assumptions1[OF â¹M(A)âº repFun_dom_closed[OF â¹M(A)âº]]
apply(unfold_locales)
by(simp_all del:if_range_F_else_F_def,
rule_tac lam_Least_assumption_general[where U="Î»_. {domain(x). xâA}"])
from â¹A â Fn(nat, I, 2)âº
have x:"(âdâ{domain(p) . p â A}. {pâA. domain(p) = d}) = A"
by auto
moreover
assume "countable_rel(M,{domain(p) . p â A})"
moreover
note â¹âd. M(d) â¹ countable_rel(M,{pâA. domain(p) = d})âº
moreover from â¹M(A)âº
have "pâA â¹ M(domain(p))" for p
by (auto dest: transM)
ultimately
have "countable_rel(M,A)"
using countable_rel_imp_countable_rel_UN
unfolding dC_F_def
by auto
with â¹Â¬ |A|âMâ â¤ natâº â¹M(A)âº
show False
using countable_rel_iff_cardinal_rel_le_nat by simp
qed
moreover from â¹A â Fn(nat, I, 2)âº â¹M(A)âº
have "p â A â¹ Finite(domain(p))" for p
using lesspoll_rel_nat_is_Finite_rel[of "domain(p)"]
lesspoll_nat_imp_lesspoll_rel[of "domain(p)"]
domain_of_fun[of p _ "Î»_. 2"] by (auto dest:transM)
moreover
note repFun_dom_closed[OF â¹M(A)âº]
ultimately
obtain D where "delta_system(D)" "D â {domain(p) . p â A}" "D ââMâ âµâ1ââMâ" "M(D)"
using delta_system_uncountable_rel[of "{domain(p) . p â A}"] by auto
then
have delta:"âd1âD. âd2âD. d1 â  d2 â¶ d1 â© d2 = âD"
using delta_system_root_eq_Inter
by simp
moreover from â¹D ââMâ âµâ1ââMââº â¹M(D)âº
have "uncountable_rel(M,D)"
using uncountable_rel_iff_subset_eqpoll_rel_Aleph_rel1 by auto
moreover from this and â¹D â {domain(p) . p â A}âº
obtain p1 where "p1 â A" "domain(p1) â D"
using uncountable_rel_not_empty[of D] by blast
moreover from this and â¹p1 â A â¹ Finite(domain(p1))âº
have "Finite(domain(p1))"
using Finite_domain by simp
moreover
define r where "r â¡ âD"
moreover from â¹M(D)âº
have "M(r)" "M(rÃ2)"
unfolding r_def by simp_all
ultimately
have "Finite(r)" using subset_Finite[of "r" "domain(p1)"]
by auto
have "countable_rel(M,{restrict(p,r) . pâA})"
proof -
note â¹M(Fn(nat, I, 2))âº â¹M(r)âº
moreover from this
have "fâFn(nat, I, 2) â¹ M(restrict(f,r))" for f
by (blast dest: transM)
ultimately
have "fâFn(nat, I, 2) â¹ restrict(f,r) â Pow_rel(M,r Ã 2)" for f
using restrict_subset_Sigma[of f _ "Î»_. 2" r] Pow_rel_char
by (auto del:FnD dest!:FnD simp: Pi_def) (auto dest:transM)
with â¹A â Fn(nat, I, 2)âº
have "{restrict(f,r) . f â A } â Pow_rel(M,r Ã 2)"
by fast
moreover from â¹M(A)âº â¹M(r)âº
have "M({restrict(f,r) . f â A })"
using RepFun_closed restrict_strong_replacement transM[OF _ â¹M(A)âº] by auto
moreover
note â¹Finite(r)âº â¹M(r)âº
ultimately
show ?thesis
using Finite_Sigma[THEN Finite_Pow_rel, of r "Î»_. 2"]
by (intro Finite_imp_countable_rel) (auto intro:subset_Finite)
qed
moreover from â¹M(A)âº â¹M(D)âº
have "M({pâA. domain(p) â D})"
using domain_mem_separation by simp
have "uncountable_rel(M,{pâA. domain(p) â D})" (is "uncountable_rel(M,?X)")
proof
from â¹D â {domain(p) . p â A}âº
have "(Î»pâ?X. domain(p)) â surj(?X, D)"
using lam_type unfolding surj_def by auto
moreover from â¹M(A)âº â¹M(?X)âº
have "M(Î»pâ?X. domain(p))"
using lam_closed[OF domain_replacement â¹M(?X)âº] transM[OF _ â¹M(?X)âº] by simp
moreover
note â¹M(?X)âº â¹M(D)âº
moreover from calculation
have surjection:"(Î»pâ?X. domain(p)) â surjâMâ(?X, D)"
using surj_rel_char by simp
moreover
assume "countable_rel(M,?X)"
moreover
note â¹uncountable_rel(M,D)âº
ultimately
show False
using surj_rel_countable_rel[OF _ surjection] by auto
qed
moreover
have "D = (âfâPow_rel(M,rÃ2) . {y . pâA, restrict(p,r) = f â§ y=domain(p) â§ domain(p) â D})"
proof -
{
fix z
assume "z â D"
with â¹M(D)âº
have â¹M(z)âº by (auto dest:transM)
from â¹zâDâº â¹D â _âº â¹M(A)âº
obtain p  where "domain(p) = z" "p â A" "M(p)"
by (auto dest:transM)
moreover from â¹A â Fn(nat, I, 2)âº â¹M(z)âº and this
have "p â z ââMâ 2"
using domain_of_fun function_space_rel_char by (auto del:FnD dest!:FnD)
moreover from this â¹M(z)âº
have "p â z â 2"
using domain_of_fun function_space_rel_char by (auto)
moreover from this â¹M(r)âº
have "restrict(p,r) â r Ã 2"
using function_restrictI[of p r] fun_is_function[of p z "Î»_. 2"]
restrict_subset_Sigma[of p z "Î»_. 2" r] function_space_rel_char
by (auto simp:Pi_def)
moreover from â¹M(p)âº â¹M(r)âº
have "M(restrict(p,r))" by simp
moreover
note â¹M(r)âº
ultimately
have "âpâA.  restrict(p,r) â Pow_rel(M,rÃ2) â§ domain(p) = z"
using Pow_rel_char by auto
}
then
show ?thesis
by (intro equalityI) (force)+
qed
from â¹M(D)âºâ¹M(r)âº
have "M({y . pâA, restrict(p,r) = f â§ y=domain(p) â§ domain(p) â D})" (is "M(?Y(A,f))")
if "M(f)" "M(A)" for f A
using drSR_Y_closed[unfolded drSR_Y_def] that
by simp
then
obtain f where "uncountable_rel(M,?Y(A,f))" "M(f)"
proof -
have 1:"M(i)"
if "M(B)" "M(x)"
"x â {y . x â B, restrict(x, r) = i â§ y = domain(x) â§ domain(x) â D}"
for B x i
using that â¹M(r)âº
by (auto dest:transM)
note â¹M(r)âº
moreover from this
have "M(PowâMâ(r Ã 2))" by simp
moreover
note â¹M(A)âº â¹âf A. M(f) â¹ M(A) â¹ M(?Y(A,f))âº â¹M(D)âº
moreover from calculation
interpret M_replacement_lepoll M "drSR_Y(r,D)"
using countable_lepoll_assms3 lam_replacement_inj_rel lam_replacement_drSR_Y
drSR_Y_closed lam_Least_assumption_drSR_Y
from calculation
have "x â PowâMâ(r Ã 2) â¹ M(drSR_Y(r, D, A, x))" for x
unfolding drSR_Y_def by (auto dest:transM)
ultimately
interpret M_cardinal_UN_lepoll _ "?Y(A)" "Pow_rel(M,rÃ2)"
using countable_lepoll_assms3 lam_replacement_drSR_Y
lepoll_assumptions[where S="Pow_rel(M,rÃ2)", unfolded lepoll_assumptions_defs]
lam_Least_assumption_drSR_Y[unfolded drSR_Y_def]
unfolding drSR_Y_def
apply unfold_locales
apply (simp_all add:lam_replacement_inj_rel del: if_range_F_else_F_def,rule_tac 1,simp_all)
by ((fastforce dest:transM[OF _ â¹M(A)âº])+)
{
from â¹Finite(r)âº â¹M(r)âº
have "countable_rel(M,Pow_rel(M,rÃ2))"
using Finite_Sigma[THEN Finite_Pow_rel] Finite_imp_countable_rel
by simp
moreover
assume "M(f) â¹ countable_rel(M,?Y(A,f))" for f
moreover
note â¹D = (âfâPow_rel(M,rÃ2) .?Y(A,f))âº â¹M(r)âº
moreover
note â¹uncountable_rel(M,D)âº
ultimately
have "False"
using countable_rel_imp_countable_rel_UN by (auto dest: transM)
}
with that
show ?thesis
by auto
qed
moreover from this â¹M(A)âº and â¹M(f) â¹ M(A) â¹ M(?Y(A,f))âº
have "M(?Y(A,f))"
by blast
ultimately
obtain j where "j â inj_rel(M,nat, ?Y(A,f))" "M(j)"
using uncountable_rel_iff_nat_lt_cardinal_rel[THEN iffD1, THEN leI,
THEN cardinal_rel_le_imp_lepoll_rel, THEN lepoll_relD]
by auto
with â¹M(?Y(A,f))âº
have "j0 â  j1" "j0 â ?Y(A,f)" "j1 â ?Y(A,f)"
using inj_is_fun[THEN apply_type, of j nat "?Y(A,f)"]
inj_rel_char
unfolding inj_def by auto
then
obtain p q where "domain(p) â  domain(q)" "p â A" "q â A"
"domain(p) â D" "domain(q) â D"
"restrict(p,r) = restrict(q,r)" by auto
moreover from this and delta
have "domain(p) â© domain(q) = r"
unfolding r_def by simp
moreover
note â¹A â Fn(nat, I, 2)âº Fn_nat_abs[OF â¹M(I)âº nat_into_M[of 2],simplified]
moreover from calculation
have "p â FnâMâ(nat, I, 2)" "q â FnâMâ(nat, I, 2)"
by auto
moreover from calculation
have "p âª q â Fn(nat, I, 2)"
using restrict_eq_imp_compat_rel InfCard_rel_nat
by simp
ultimately
have "âpâA. âqâA. p â  q â§ compat_in(Fn(nat, I, 2), Fnle(nat, I, 2), p, q)"
unfolding compat_in_def
by (rule_tac bexI[of _ p], rule_tac bexI[of _ q]) blast
}
moreover from assms
have "M(Fnle(Ï,I,2))"
by simp
moreover note â¹M(Fn(Ï,I,2))âº
ultimately
show ?thesis using def_ccc_rel by (auto simp:absolut antichain_def) fastforce
qed

end

# Theory Edrel

theory Edrel
imports
Transitive_Models.ZF_Miscellanea
Transitive_Models.Recursion_Thms

begin

subsectionâ¹The well-founded relation \<^term>â¹edâºâº

lemma eclose_sing : "x â eclose(a) â¹ x â eclose({a})"
using subsetD[OF mem_eclose_subset]
by simp

lemma ecloseE :
assumes  "x â eclose(A)"
shows  "x â A â¨ (â B â A . x â eclose(B))"
using assms
proof (induct rule:eclose_induct_down)
case (1 y)
then
show ?case
using arg_into_eclose by auto
next
case (2 y z)
from â¹y â A â¨ (âBâA. y â eclose(B))âº
consider (inA) "y â A" | (exB) "(âBâA. y â eclose(B))"
by auto
then show ?case
proof (cases)
case inA
then
show ?thesis using 2 arg_into_eclose by auto
next
case exB
then obtain B where "y â eclose(B)" "BâA"
by auto
then
show ?thesis using 2 ecloseD[of y B z] by auto
qed
qed

lemma eclose_singE : "x â eclose({a}) â¹ x = a â¨ x â eclose(a)"
by(blast dest: ecloseE)

lemma in_eclose_sing :
assumes "x â eclose({a})" "a â eclose(z)"
shows "x â eclose({z})"
proof -
from â¹xâeclose({a})âº
consider "x=a" | "xâeclose(a)"
using eclose_singE by auto
then
show ?thesis
using eclose_sing mem_eclose_trans assms
by (cases, auto)
qed

lemma in_dom_in_eclose :
assumes "x â domain(z)"
shows "x â eclose(z)"
proof -
from assms
obtain y where "â¨x,yâ© â z"
unfolding domain_def by auto
then
show ?thesis
unfolding Pair_def
using ecloseD[of "{x,x}"] ecloseD[of "{{x,x},{x,y}}"] arg_into_eclose
by auto
qed

textâ¹termâ¹edâº is the well-founded relation on which \<^term>â¹valâº is defined.âº
definition
ed :: "[i,i] â o" where
"ed(x,y) â¡ x â domain(y)"

definition
edrel :: "i â i" where
"edrel(A) â¡ Rrel(ed,A)"

lemma edI[intro!]: "tâdomain(x) â¹ ed(t,x)"
unfolding ed_def .

lemma edD[dest!]: "ed(t,x) â¹ tâdomain(x)"
unfolding ed_def .

lemma rank_ed:
assumes "ed(y,x)"
shows "succ(rank(y)) â¤ rank(x)"
proof
from assms
obtain p where "â¨y,pâ©âx" by auto
moreover
obtain s where "yâs" "sââ¨y,pâ©" unfolding Pair_def by auto
ultimately
using rank_lt by blast+
then
show "rank(y) < rank(x)"
using lt_trans by blast
qed

lemma edrel_dest [dest]: "x â edrel(A) â¹ â aâ A. â b â A. x =â¨a,bâ©"

lemma edrelD : "x â edrel(A) â¹ â aâ A. â b â A. x =â¨a,bâ© â§ a â domain(b)"

lemma edrelI [intro!]: "xâA â¹ yâA â¹ x â domain(y) â¹ â¨x,yâ©âedrel(A)"

lemma edrel_trans: "Transset(A) â¹ yâA â¹ x â domain(y) â¹ â¨x,yâ©âedrel(A)"
by (rule edrelI, auto simp add:Transset_def domain_def Pair_def)

lemma domain_trans: "Transset(A) â¹ yâA â¹ x â domain(y) â¹ xâA"
by (auto simp add: Transset_def domain_def Pair_def)

lemma relation_edrel : "relation(edrel(A))"

lemma field_edrel : "field(edrel(A))âA"
by blast

lemma edrel_sub_memrel: "edrel(A) â trancl(Memrel(eclose(A)))"
proof
let
?r="trancl(Memrel(eclose(A)))"
fix z
assume "zâedrel(A)"
then
obtain x y where "xâA" "yâA" "z=â¨x,yâ©" "xâdomain(y)"
using edrelD
by blast
moreover from this
obtain u v where "xâu" "uâv" "vây"
unfolding domain_def Pair_def by auto
moreover from calculation
have "xâeclose(A)" "yâeclose(A)" "yâeclose(A)"
using arg_into_eclose Transset_eclose[unfolded Transset_def]
by simp_all
moreover from calculation
have "vâeclose(A)"
by auto
moreover from calculation
have "uâeclose(A)"
using Transset_eclose[unfolded Transset_def]
by auto
moreover from calculation
moreover from this
using trancl_trans[OF _ trancl_trans[of _ v _ y]]
by simp
ultimately
show "zâ?r"
by simp
qed

lemma wf_edrel : "wf(edrel(A))"
using wf_subset [of "trancl(Memrel(eclose(A)))"] edrel_sub_memrel
wf_trancl wf_Memrel
by auto

lemma ed_induction:
assumes "âx. â¦ây.  ed(y,x) â¹ Q(y) â§ â¹ Q(x)"
shows "Q(a)"
proof(induct rule: wf_induct2[OF wf_edrel[of "eclose({a})"] ,of a "eclose({a})"])
case 1
then show ?case using arg_into_eclose by simp
next
case 2
then show ?case using field_edrel .
next
case (3 x)
then
show ?case
using assms[of x] edrelI domain_trans[OF Transset_eclose 3(1)] by blast
qed

lemma dom_under_edrel_eclose: "edrel(eclose({x})) - {x} = domain(x)"
proof(intro equalityI)
show "edrel(eclose({x})) - {x} â domain(x)"
unfolding edrel_def Rrel_def ed_def
by auto
next
show "domain(x) â edrel(eclose({x})) - {x}"
unfolding edrel_def Rrel_def
using in_dom_in_eclose eclose_sing arg_into_eclose
by blast
qed

lemma ed_eclose : "â¨y,zâ© â edrel(A) â¹ y â eclose(z)"

lemma tr_edrel_eclose : "â¨y,zâ© â edrel(eclose({x}))^+ â¹ y â eclose(z)"

lemma restrict_edrel_eq :
assumes "z â domain(x)"
shows "edrel(eclose({x})) â© eclose({z})Ãeclose({z}) = edrel(eclose({z}))"
proof(intro equalityI subsetI)
let ?ec="Î» y . edrel(eclose({y}))"
let ?ez="eclose({z})"
let ?rr="?ec(x) â© ?ez Ã ?ez"
fix y
assume "y â ?rr"
then
obtain a b where "â¨a,bâ© â ?rr" "a â ?ez" "b â ?ez" "â¨a,bâ© â ?ec(x)" "y=â¨a,bâ©"
by blast
moreover from this
have "a â domain(b)"
using edrelD by blast
ultimately
show "y â edrel(eclose({z}))"
by blast
next
let ?ec="Î» y . edrel(eclose({y}))"
let ?ez="eclose({z})"
let ?rr="?ec(x) â© ?ez Ã ?ez"
fix y
assume "y â edrel(?ez)"
then
obtain a b where "a â ?ez" "b â ?ez" "y=â¨a,bâ©" "a â domain(b)"
using edrelD by blast
moreover
from this assms
have "z â eclose(x)"
using in_dom_in_eclose by simp
moreover
from assms calculation
have "a â eclose({x})" "b â eclose({x})"
using in_eclose_sing by simp_all
moreover from calculation
by blast
ultimately
show "y â ?rr"
by simp
qed

lemma tr_edrel_subset :
assumes "z â domain(x)"
shows   "tr_down(edrel(eclose({x})),z) â eclose({z})"
proof(intro subsetI)
let ?r="Î» x . edrel(eclose({x}))"
fix y
assume "y â tr_down(?r(x),z)"
then
using tr_downD by simp
with assms
show "y â eclose({z})"
using tr_edrel_eclose eclose_sing by simp
qed

end

# Theory FrecR

sectionâ¹Well-founded relation on namesâº
theory FrecR
imports
Transitive_Models.Discipline_Function
Edrel
begin

textâ¹\<^term>â¹frecRâº is the well-founded relation on names that allows
us to define forcing for atomic formulas.âº

definition
ftype :: "iâi" where
"ftype â¡ fst"

definition
name1 :: "iâi" where
"name1(x) â¡ fst(snd(x))"

definition
name2 :: "iâi" where
"name2(x) â¡ fst(snd(snd(x)))"

definition
cond_of :: "iâi" where
"cond_of(x) â¡ snd(snd(snd((x))))"

lemma components_simp:
unfolding ftype_def name1_def name2_def cond_of_def
by simp_all

definition eclose_n :: "[iâi,i] â i" where
"eclose_n(name,x) = eclose({name(x)})"

definition
ecloseN :: "i â i" where
"ecloseN(x) = eclose_n(name1,x) âª eclose_n(name2,x)"

lemma components_in_eclose :
unfolding ecloseN_def eclose_n_def
using components_simp arg_into_eclose by auto

lemmas names_simp = components_simp(2) components_simp(3)

lemma ecloseNI1 :
assumes "x â eclose(n1) â¨ xâeclose(n2)"
unfolding ecloseN_def eclose_n_def
using assms eclose_sing names_simp
by auto

lemmas ecloseNI = ecloseNI1

lemma ecloseN_mono :
assumes "u â ecloseN(x)" "name1(x) â ecloseN(y)" "name2(x) â ecloseN(y)"
shows "u â ecloseN(y)"
proof -
from â¹uâ_âº
consider (a) "uâeclose({name1(x)})" | (b) "u â eclose({name2(x)})"
unfolding ecloseN_def  eclose_n_def by auto
then
show ?thesis
proof cases
case a
with â¹name1(x) â _âº
show ?thesis
unfolding ecloseN_def  eclose_n_def
using eclose_singE[OF a] mem_eclose_trans[of u "name1(x)" ] by auto
next
case b
with â¹name2(x) â _âº
show ?thesis
unfolding ecloseN_def eclose_n_def
using eclose_singE[OF b] mem_eclose_trans[of u "name2(x)"] by auto
qed
qed

definition
is_ftype :: "(iâo)âiâiâo" where
"is_ftype â¡ is_fst"

definition
ftype_fm :: "[i,i] â i" where
"ftype_fm â¡ fst_fm"

lemma is_ftype_iff_sats [iff_sats]:
assumes
"nth(a,env) = x" "nth(b,env) = y" "aânat" "bânat" "env â list(A)"
shows
"is_ftype(##A,x,y)  â· sats(A,ftype_fm(a,b), env)"
unfolding ftype_fm_def is_ftype_def
using assms sats_fst_fm
by simp

definition
is_name1 :: "(iâo)âiâiâo" where
"is_name1(M,x,t2) â¡ is_hcomp(M,is_fst(M),is_snd(M),x,t2)"

definition
name1_fm :: "[i,i] â i" where
"name1_fm(x,t) â¡ hcomp_fm(fst_fm,snd_fm,x,t)"

lemma sats_name1_fm [simp]:
"â¦ x â nat; y â nat;env â list(A) â§ â¹
(A, env â¨ name1_fm(x,y)) â· is_name1(##A, nth(x,env), nth(y,env))"
unfolding name1_fm_def is_name1_def
using sats_fst_fm sats_snd_fm sats_hcomp_fm[of A "is_fst(##A)" _ fst_fm "is_snd(##A)"]
by simp

lemma is_name1_iff_sats [iff_sats]:
assumes
"nth(a,env) = x" "nth(b,env) = y" "aânat" "bânat" "env â list(A)"
shows
"is_name1(##A,x,y)  â· A , env â¨ name1_fm(a,b)"
using assms sats_name1_fm
by simp

definition
is_snd_snd :: "(iâo)âiâiâo" where
"is_snd_snd(M,x,t) â¡ is_hcomp(M,is_snd(M),is_snd(M),x,t)"

definition
snd_snd_fm :: "[i,i]âi" where
"snd_snd_fm(x,t) â¡ hcomp_fm(snd_fm,snd_fm,x,t)"

lemma sats_snd2_fm [simp]:
"â¦ x â nat; y â nat;env â list(A) â§ â¹
(A, env  â¨ snd_snd_fm(x,y)) â· is_snd_snd(##A, nth(x,env), nth(y,env))"
unfolding snd_snd_fm_def is_snd_snd_def
using sats_snd_fm sats_hcomp_fm[of A "is_snd(##A)" _ snd_fm "is_snd(##A)"]
by simp

definition
is_name2 :: "(iâo)âiâiâo" where
"is_name2(M,x,t3) â¡ is_hcomp(M,is_fst(M),is_snd_snd(M),x,t3)"

definition
name2_fm :: "[i,i] â i" where
"name2_fm(x,t3) â¡ hcomp_fm(fst_fm,snd_snd_fm,x,t3)"

lemma sats_name2_fm :
"â¦ x â nat; y â nat;env â list(A) â§
â¹ (A , env â¨ name2_fm(x,y)) â· is_name2(##A, nth(x,env), nth(y,env))"
unfolding name2_fm_def is_name2_def
using sats_fst_fm sats_snd2_fm sats_hcomp_fm[of A "is_fst(##A)" _ fst_fm "is_snd_snd(##A)"]
by simp

lemma is_name2_iff_sats [iff_sats]:
assumes
"nth(a,env) = x" "nth(b,env) = y" "aânat" "bânat" "env â list(A)"
shows
"is_name2(##A,x,y)  â· A, env â¨ name2_fm(a,b)"
using assms sats_name2_fm
by simp

definition
is_cond_of :: "(iâo)âiâiâo" where
"is_cond_of(M,x,t4) â¡ is_hcomp(M,is_snd(M),is_snd_snd(M),x,t4)"

definition
cond_of_fm :: "[i,i] â i" where
"cond_of_fm(x,t4) â¡ hcomp_fm(snd_fm,snd_snd_fm,x,t4)"

lemma sats_cond_of_fm :
"â¦ x â nat; y â nat;env â list(A) â§ â¹
(A, env â¨ cond_of_fm(x,y)) â· is_cond_of(##A, nth(x,env), nth(y,env))"
unfolding cond_of_fm_def is_cond_of_def
using sats_snd_fm sats_snd2_fm sats_hcomp_fm[of A "is_snd(##A)" _ snd_fm "is_snd_snd(##A)"]
by simp

lemma is_cond_of_iff_sats [iff_sats]:
assumes
"nth(a,env) = x" "nth(b,env) = y" "aânat" "bânat" "env â list(A)"
shows
"is_cond_of(##A,x,y) â· A, env â¨ cond_of_fm(a,b)"
using assms sats_cond_of_fm
by simp

lemma components_type[TC] :
assumes "aânat" "bânat"
shows
"ftype_fm(a,b)âformula"
"name1_fm(a,b)âformula"
"name2_fm(a,b)âformula"
"cond_of_fm(a,b)âformula"
using assms
unfolding ftype_fm_def fst_fm_def snd_fm_def snd_snd_fm_def name1_fm_def name2_fm_def
cond_of_fm_def hcomp_fm_def
by simp_all

lemmas components_iff_sats = is_ftype_iff_sats is_name1_iff_sats is_name2_iff_sats
is_cond_of_iff_sats

lemmas components_defs = ftype_fm_def snd_snd_fm_def hcomp_fm_def
name1_fm_def name2_fm_def cond_of_fm_def

definition
is_eclose_n :: "[iâo,[iâo,i,i]âo,i,i] â o" where
"is_eclose_n(N,is_name,en,t) â¡
ân1[N].âs1[N]. is_name(N,t,n1) â§ is_singleton(N,n1,s1) â§ is_eclose(N,s1,en)"

definition
eclose_n1_fm :: "[i,i] â i" where

definition
eclose_n2_fm :: "[i,i] â i" where

definition
is_ecloseN :: "[iâo,i,i] â o" where
"is_ecloseN(N,t,en) â¡ âen1[N].âen2[N].
is_eclose_n(N,is_name1,en1,t) â§ is_eclose_n(N,is_name2,en2,t)â§
union(N,en1,en2,en)"

definition
ecloseN_fm :: "[i,i] â i" where

lemma ecloseN_fm_type [TC] :
"â¦ en â nat ; t â nat â§ â¹ ecloseN_fm(en,t) â formula"
unfolding ecloseN_fm_def eclose_n1_fm_def eclose_n2_fm_def by simp

lemma sats_ecloseN_fm [simp]:
"â¦ en â nat; t â nat ; env â list(A) â§
â¹ (A, env â¨ ecloseN_fm(en,t)) â· is_ecloseN(##A,nth(t,env),nth(en,env))"
unfolding ecloseN_fm_def is_ecloseN_def eclose_n1_fm_def eclose_n2_fm_def is_eclose_n_def
using nth_0 nth_ConsI sats_name1_fm sats_name2_fm singleton_iff_sats[symmetric]
by auto

lemma is_ecloseN_iff_sats [iff_sats]:
"â¦ nth(en, env) = ena; nth(t, env) = ta; en â nat; t â nat ; env â list(A) â§
â¹ is_ecloseN(##A,ta,ena) â· A, env â¨ ecloseN_fm(en,t)"
by simp

(* Relation of forces *)
definition
frecR :: "i â i â o" where
"frecR(x,y) â¡
(ftype(x) = 1 â§ ftype(y) = 0
â§ (name1(x) â domain(name1(y)) âª domain(name2(y)) â§ (name2(x) = name1(y) â¨ name2(x) = name2(y))))
â¨ (ftype(x) = 0 â§ ftype(y) =  1 â§ name1(x) = name1(y) â§ name2(x) â domain(name2(y)))"

lemma frecR_ftypeD :
assumes "frecR(x,y)"
shows "(ftype(x) = 0 â§ ftype(y) = 1) â¨ (ftype(x) = 1 â§ ftype(y) = 0)"
using assms unfolding frecR_def by auto

lemma frecRI1: "s â domain(n1) â¨ s â domain(n2) â¹ frecR(â¨1, s, n1, qâ©, â¨0, n1, n2, q'â©)"

lemma frecRI1': "s â domain(n1) âª domain(n2) â¹ frecR(â¨1, s, n1, qâ©, â¨0, n1, n2, q'â©)"

lemma frecRI2: "s â domain(n1) â¨ s â domain(n2) â¹ frecR(â¨1, s, n2, qâ©, â¨0, n1, n2, q'â©)"

lemma frecRI2': "s â domain(n1) âª domain(n2) â¹ frecR(â¨1, s, n2, qâ©, â¨0, n1, n2, q'â©)"

unfolding frecR_def by (auto simp add:components_simp)

lemma frecRI3': "s â domain(n2) â¹ frecR(â¨0, n1, s, qâ©, â¨1, n1, n2, q'â©)"
unfolding frecR_def by (auto simp add:components_simp)

lemma frecR_D1 :
"frecR(x,y) â¹ ftype(y) = 0 â¹ ftype(x) = 1 â§
(name1(x) â domain(name1(y)) âª domain(name2(y)) â§ (name2(x) = name1(y) â¨ name2(x) = name2(y)))"
unfolding frecR_def
by auto

lemma frecR_D2 :
"frecR(x,y) â¹ ftype(y) = 1 â¹ ftype(x) = 0 â§
ftype(x) = 0 â§ ftype(y) =  1 â§ name1(x) = name1(y) â§ name2(x) â domain(name2(y))"
unfolding frecR_def
by auto

lemma frecR_DI :
using assms
unfolding frecR_def

relativize "frecR" "is_frecR"

schematic_goal sats_frecR_fm_auto:
assumes
"iânat" "jânat" "envâlist(A)"
shows
"is_frecR(##A,nth(i,env),nth(j,env)) â· A, env â¨ ?fr_fm(i,j)"
unfolding is_frecR_def
by (insert assms ; (rule sep_rules' cartprod_iff_sats components_iff_sats
| simp del:sats_cartprod_fm)+)

synthesize "frecR" from_schematic sats_frecR_fm_auto

textâ¹Third item of Kunen's observations (p. 257) about the trcl relation.âº
lemma eq_ftypep_not_frecrR:
assumes "ftype(x) = ftype(y)"
shows "Â¬ frecR(x,y)"
using assms frecR_ftypeD by force

definition
rank_names :: "i â i" where
"rank_names(x) â¡ max(rank(name1(x)),rank(name2(x)))"

lemma rank_names_types [TC]:
shows "Ord(rank_names(x))"
unfolding rank_names_def max_def using Ord_rank Ord_Un by auto

definition
mtype_form :: "i â i" where
"mtype_form(x) â¡ if rank(name1(x)) < rank(name2(x)) then 0 else 2"

definition
type_form :: "i â i" where
"type_form(x) â¡ if ftype(x) = 0 then 1 else mtype_form(x)"

lemma type_form_tc [TC]:
shows "type_form(x) â 3"
unfolding type_form_def mtype_form_def by auto

lemma frecR_le_rnk_names :
assumes  "frecR(x,y)"
shows "rank_names(x)â¤rank_names(y)"
proof -
obtain a b c d where
H: "a = name1(x)" "b = name2(x)"
"c = name1(y)" "d = name2(y)"
"(a â domain(c)âªdomain(d) â§ (b=c â¨ b = d)) â¨ (a = c â§ b â domain(d))"
using assms
unfolding frecR_def
by force
then
consider
(m) "a â domain(c) â§ (b = c â¨ b = d) "
| (n) "a â domain(d) â§ (b = c â¨ b = d)"
| (o) "b â domain(d) â§ a = c"
by auto
then
show ?thesis
proof(cases)
case m
then
have "rank(a) < rank(c)"
using eclose_rank_lt  in_dom_in_eclose
by simp
with â¹rank(a) < rank(c)âº H m
show ?thesis
unfolding rank_names_def
using Ord_rank max_cong max_cong2 leI
by auto
next
case n
then
have "rank(a) < rank(d)"
using eclose_rank_lt in_dom_in_eclose
by simp
with â¹rank(a) < rank(d)âº H n
show ?thesis
unfolding rank_names_def
using Ord_rank max_cong2 max_cong max_commutes[of "rank(c)" "rank(d)"] leI
by auto
next
case o
then
have "rank(b) < rank(d)" (is "?b < ?d") "rank(a) = rank(c)" (is "?a = _")
using eclose_rank_lt in_dom_in_eclose
by simp_all
with H
show ?thesis
unfolding rank_names_def
using Ord_rank max_commutes max_cong2[OF leI[OF â¹?b < ?dâº], of ?a]
by simp
qed
qed

definition
Î :: "i â i" where
"Î(x) = 3 ** rank_names(x) ++ type_form(x)"

lemma Î_type [TC]:
shows "Ord(Î(x))"
unfolding Î_def by simp

lemma Î_mono :
assumes "frecR(x,y)"
shows "Î(x) < Î(y)"
proof -
have F: "type_form(x) < 3" "type_form(y) < 3"
using ltI
by simp_all
from assms
have A: "rank_names(x) â¤ rank_names(y)" (is "?x â¤ ?y")
using frecR_le_rnk_names
by simp
then
have "Ord(?y)"
unfolding rank_names_def
using Ord_rank max_def
by simp
note leE[OF â¹?xâ¤?yâº]
then
show ?thesis
proof(cases)
case 1
then
show ?thesis
unfolding Î_def
using oadd_lt_mono2 â¹?x < ?yâº F
by auto
next
case 2
consider (a) "ftype(x) = 0 â§ ftype(y) = 1" | (b) "ftype(x) = 1 â§ ftype(y) = 0"
using frecR_ftypeD[OF â¹frecR(x,y)âº]
by auto
then show ?thesis
proof(cases)
case b
moreover from this
have "type_form(y) = 1"
using type_form_def by simp
moreover from calculation
have "name2(x) = name1(y) â¨ name2(x) = name2(y) "  (is "?Ï = ?Ï' â¨ ?Ï = ?Ï'")
"name1(x) â domain(name1(y)) âª domain(name2(y))" (is "?Ï â domain(?Ï') âª domain(?Ï')")
using assms unfolding type_form_def frecR_def by auto
moreover from calculation
have E: "rank(?Ï) = rank(?Ï') â¨ rank(?Ï) = rank(?Ï')" by auto
from calculation
consider (c) "rank(?Ï) < rank(?Ï')" |  (d) "rank(?Ï) < rank(?Ï')"
using eclose_rank_lt in_dom_in_eclose by force
then
have "rank(?Ï) < rank(?Ï)"
proof (cases)
case c
with â¹rank_names(x) = rank_names(y) âº
show ?thesis
unfolding rank_names_def mtype_form_def type_form_def
using max_D2[OF E c] E assms Ord_rank
by simp
next
case d
with â¹rank_names(x) = rank_names(y) âº
show ?thesis
unfolding rank_names_def mtype_form_def type_form_def
using max_D2[OF _ d] max_commutes E assms Ord_rank disj_commute
by simp
qed
with b
have "type_form(x) = 0" unfolding type_form_def mtype_form_def by simp
with â¹rank_names(x) = rank_names(y) âº â¹type_form(y) = 1âº â¹type_form(x) = 0âº
show ?thesis
unfolding Î_def by auto
next
case a
then
have "name1(x) = name1(y)" (is "?Ï = ?Ï'")
"name2(x) â domain(name2(y))" (is "?Ï â domain(?Ï')")
"type_form(x) = 1"
using assms
unfolding type_form_def frecR_def
by auto
then
have "rank(?Ï) = rank(?Ï')" "rank(?Ï) < rank(?Ï')"
using  eclose_rank_lt in_dom_in_eclose
by simp_all
with â¹rank_names(x) = rank_names(y) âº
have "rank(?Ï') â¤ rank(?Ï')"
using Ord_rank max_D1
unfolding rank_names_def
by simp
with a
have "type_form(y) = 2"
unfolding type_form_def mtype_form_def
using not_lt_iff_le assms
by simp
with â¹rank_names(x) = rank_names(y) âº â¹type_form(y) = 2âº â¹type_form(x) = 1âº
show ?thesis
unfolding Î_def by auto
qed
qed
qed

definition
frecrel :: "i â i" where
"frecrel(A) â¡ Rrel(frecR,A)"

lemma frecrelI :
assumes "x â A" "yâA" "frecR(x,y)"
using assms unfolding frecrel_def Rrel_def by auto

lemma frecrelD :
shows
"ftype(x) â A1" "ftype(x) â A1"
"name1(x) â A2" "name1(y) â A2"
"name2(x) â A3" "name2(x) â A3"
"cond_of(x) â A4" "cond_of(y) â A4"
"frecR(x,y)"
using assms
unfolding frecrel_def Rrel_def ftype_def by (auto simp add:components_simp)

lemma wf_frecrel :
shows "wf(frecrel(A))"
proof -
have "frecrel(A) â measure(A,Î)"
unfolding frecrel_def Rrel_def measure_def
using Î_mono
by force
then
show ?thesis
using wf_subset wf_measure by auto
qed

lemma core_induction_aux:
fixes A1 A2 :: "i"
assumes
"Transset(A1)"
"âÏ Î¸ p.  p â A2 â¹ â¦âq Ï. â¦ qâA2 ; Ïâdomain(Î¸)â§ â¹ Q(0,Ï,Ï,q)â§ â¹ Q(1,Ï,Î¸,p)"
"âÏ Î¸ p.  p â A2 â¹ â¦âq Ï. â¦ qâA2 ; Ïâdomain(Ï) âª domain(Î¸)â§ â¹ Q(1,Ï,Ï,q) â§ Q(1,Ï,Î¸,q)â§ â¹ Q(0,Ï,Î¸,p)"
shows "aâ2ÃA1ÃA1ÃA2 â¹ Q(ftype(a),name1(a),name2(a),cond_of(a))"
proof (induct a rule:wf_induct[OF wf_frecrel[of "2ÃA1ÃA1ÃA2"]])
case (1 x)
let ?Ï = "name1(x)"
let ?Î¸ = "name2(x)"
let ?D = "2ÃA1ÃA1ÃA2"
assume "x â ?D"
then
have "cond_of(x)âA2"
from â¹xâ?Dâº
consider (eq) "ftype(x)=0" | (mem) "ftype(x)=1"
then
show ?case
proof cases
case eq
then
have "Q(1, Ï, ?Ï, q) â§ Q(1, Ï, ?Î¸, q)" if "Ï â domain(?Ï) âª domain(?Î¸)" and "qâA2" for q Ï
proof -
from 1
have "?ÏâA1" "?Î¸âA1" "?Ïâeclose(A1)" "?Î¸âeclose(A1)"
using  arg_into_eclose
moreover from â¹Transset(A1)âº that(1)
have "Ïâeclose(?Ï) âª eclose(?Î¸)"
using in_dom_in_eclose
by auto
then
have "ÏâA1"
using mem_eclose_subset[OF â¹?ÏâA1âº] mem_eclose_subset[OF â¹?Î¸âA1âº]
Transset_eclose_eq_arg[OF â¹Transset(A1)âº]
by auto
with â¹qâA2âº â¹?Î¸ â A1âº â¹cond_of(x)âA2âº â¹?ÏâA1âº
have "frecR(â¨1, Ï, ?Ï, qâ©, x)" (is "frecR(?T,_)")
"frecR(â¨1, Ï, ?Î¸, qâ©, x)" (is "frecR(?U,_)")
using frecRI1'[OF that(1)] frecR_DI  â¹ftype(x) = 0âº
frecRI2'[OF that(1)]
with â¹xâ?Dâº â¹ÏâA1âº â¹qâA2âº
using frecrelI[of ?T ?D x]  frecrelI[of ?U ?D x]
with â¹qâA2âº â¹ÏâA1âº â¹?ÏâA1âº â¹?Î¸âA1âº
have "Q(1, Ï, ?Ï, q)"
using 1
moreover from â¹qâA2âº â¹ÏâA1âº â¹?ÏâA1âº â¹?Î¸âA1âº â¹â¨?U,xâ©â frecrel(?D)âº
have "Q(1, Ï, ?Î¸, q)"
using 1 by (force simp add:components_simp)
ultimately
show ?thesis
by simp
qed
with assms(3) â¹ftype(x) = 0âº â¹cond_of(x)âA2âº
show ?thesis
by auto
next
case mem
have "Q(0, ?Ï,  Ï, q)" if "Ï â domain(?Î¸)" and "qâA2" for q Ï
proof -
from 1 assms
have "?ÏâA1" "?Î¸âA1" "cond_of(x)âA2" "?Ïâeclose(A1)" "?Î¸âeclose(A1)"
using arg_into_eclose
with  â¹Transset(A1)âº that(1)
have "Ïâ eclose(?Î¸)"
using in_dom_in_eclose
by auto
then
have "ÏâA1"
using mem_eclose_subset[OF â¹?Î¸âA1âº] Transset_eclose_eq_arg[OF â¹Transset(A1)âº]
by auto
with â¹qâA2âº â¹?Î¸ â A1âº â¹cond_of(x)âA2âº â¹?ÏâA1âº â¹ftype(x) = 1âº
have "frecR(â¨0, ?Ï, Ï, qâ©, x)" (is "frecR(?T,_)")
using frecRI3'[OF that(1)] frecR_DI
with â¹xâ?Dâº â¹ÏâA1âº â¹qâA2âº â¹?ÏâA1âº
using frecrelI[of ?T ?D x]
with â¹qâA2âº â¹ÏâA1âº â¹?ÏâA1âº â¹?Î¸âA1âº 1
show ?thesis
qed
with assms(2) â¹ftype(x) = 1âº â¹cond_of(x)âA2âº
show ?thesis
by auto
qed
qed

lemma def_frecrel : "frecrel(A) = {zâAÃA. âx y. z = â¨x, yâ© â§ frecR(x,y)}"
unfolding frecrel_def Rrel_def ..

lemma frecrel_fst_snd:
"frecrel(A) = {z â AÃA .
ftype(fst(z)) = 1 â§
ftype(snd(z)) = 0 â§ name1(fst(z)) â domain(name1(snd(z))) âª domain(name2(snd(z))) â§
(name2(fst(z)) = name1(snd(z)) â¨ name2(fst(z)) = name2(snd(z)))
â¨ (ftype(fst(z)) = 0 â§
ftype(snd(z)) = 1 â§  name1(fst(z)) = name1(snd(z)) â§ name2(fst(z)) â domain(name2(snd(z))))}"
unfolding def_frecrel frecR_def
by (intro equalityI subsetI CollectI; elim CollectE; auto)

end
ody>

# Theory FrecR_Arities

theory FrecR_Arities
imports
FrecR
begin

context
notes FOL_arities[simp]
begin

arity_theorem intermediate for "fst_fm"
lemma arity_fst_fm [arity] :
"â¦xânat ; tânatâ§ â¹ arity(fst_fm(x,t)) = succ(x) âª succ(t)"
using arity_fst_fm'
by auto

arity_theorem intermediate for "snd_fm"
lemma arity_snd_fm [arity] :
"â¦xânat ; tânatâ§ â¹ arity(snd_fm(x,t)) = succ(x) âª succ(t)"
using arity_snd_fm'
by auto

lemma arity_snd_snd_fm [arity] :
"â¦xânat ; tânatâ§ â¹ arity(snd_snd_fm(x,t)) = succ(x) âª succ(t)"
unfolding snd_snd_fm_def hcomp_fm_def
using arity_snd_fm arity_empty_fm union_abs2 pred_Un_distrib
by auto

lemma arity_ftype_fm [arity] :
"â¦xânat ; tânatâ§ â¹ arity(ftype_fm(x,t)) = succ(x) âª succ(t)"
unfolding ftype_fm_def
using arity_fst_fm
by auto

lemma arity_name1_fm [arity] :
"â¦xânat ; tânatâ§ â¹ arity(name1_fm(x,t)) = succ(x) âª succ(t)"
unfolding name1_fm_def hcomp_fm_def
using arity_fst_fm arity_snd_fm union_abs2 pred_Un_distrib
by auto

lemma arity_name2_fm [arity] :
"â¦xânat ; tânatâ§ â¹ arity(name2_fm(x,t)) = succ(x) âª succ(t)"
unfolding name2_fm_def hcomp_fm_def
using arity_fst_fm arity_snd_snd_fm union_abs2 pred_Un_distrib
by auto

lemma arity_cond_of_fm [arity] :
"â¦xânat ; tânatâ§ â¹ arity(cond_of_fm(x,t)) = succ(x) âª succ(t)"
unfolding cond_of_fm_def hcomp_fm_def
using arity_snd_fm arity_snd_snd_fm union_abs2 pred_Un_distrib
by auto

lemma arity_eclose_n1_fm [arity] :
"â¦xânat ; tânatâ§ â¹ arity(eclose_n1_fm(x,t)) = succ(x) âª succ(t)"
unfolding eclose_n1_fm_def
using arity_is_eclose_fm arity_singleton_fm arity_name1_fm union_abs2 pred_Un_distrib
by auto

lemma arity_eclose_n2_fm [arity] :
"â¦xânat ; tânatâ§ â¹ arity(eclose_n2_fm(x,t)) = succ(x) âª succ(t)"
unfolding eclose_n2_fm_def
using arity_is_eclose_fm arity_singleton_fm arity_name2_fm union_abs2 pred_Un_distrib
by auto

lemma arity_ecloseN_fm [arity] :
"â¦xânat ; tânatâ§ â¹ arity(ecloseN_fm(x,t)) = succ(x) âª succ(t)"
unfolding ecloseN_fm_def
using arity_eclose_n1_fm arity_eclose_n2_fm arity_union_fm union_abs2 pred_Un_distrib
by auto

lemma arity_frecR_fm [arity]:
"â¦aânat;bânatâ§ â¹ arity(frecR_fm(a,b)) = succ(a) âª succ(b)"
unfolding frecR_fm_def
using arity_ftype_fm arity_name1_fm arity_name2_fm arity_domain_fm
arity_empty_fm arity_union_fm pred_Un_distrib arity_succ_fm
by auto

end â â¹@{thm [source] FOL_arities}âº

end
body>

# Theory Fm_Definitions

sectionâ¹Concepts involved in instances of Replacementâº
theory Fm_Definitions
imports
Transitive_Models.Renaming_Auto
Transitive_Models.Aleph_Relative
FrecR_Arities
begin

txtâ¹In this theory we put every concept that should be synthesized in a formula
to have an instance of replacement.

The automatic synthesis of a concept /foo/ requires that every concept used to
define /foo/ is already synthesized. We try to use our meta-programs to synthesize
concepts: given the absolute concept /foo/ we relativize in relational form
obtaining /is\_foo/ and the we synthesize the formula /is\_foo\_fm/.
The meta-program that synthesizes formulas also produce satisfactions lemmas.

Having one file to collect every formula needed for replacements breaks
the reading flow: we need to introduce the concept in this theory in order
to use the meta-programs; moreover there are some concepts for which we prove
here the satisfaction lemmas manually, while for others we prove them
on its theory.
âº

declare arity_subset_fm [simp del] arity_ordinal_fm[simp del, arity] arity_transset_fm[simp del]
FOL_arities[simp del]

txtâ¹Formulas for particular replacement instancesâº

textâ¹Now we introduce some definitions used in the definition of check; which
is defined by well-founded recursion using replacement in the recursive call.âº

â â¹The well-founded relation for defining check.âº
definition
rcheck :: "i â i" where
"rcheck(x) â¡ Memrel(eclose({x}))^+"

relativize "rcheck" "is_rcheck"
synthesize "is_rcheck" from_definition
arity_theorem for "is_rcheck_fm"

â â¹The function used for the replacement.âº
definition
PHcheck :: "[iâo,i,i,i,i] â o" where
"PHcheck(M,o,f,y,p) â¡ M(p) â§ (âfy[M]. fun_apply(M,f,y,fy) â§ pair(M,fy,o,p))"

synthesize "PHcheck" from_definition assuming "nonempty"
arity_theorem for "PHcheck_fm"

â â¹The recursive call for check. We could use the meta-program relationalize for
this; but it makes some proofs more involved.âº
definition
is_Hcheck :: "[iâo,i,i,i,i] â o" where
"is_Hcheck(M,o,z,f,hc)  â¡ is_Replace(M,z,PHcheck(M,o,f),hc)"

synthesize "is_Hcheck" from_definition assuming "nonempty"

lemma arity_is_Hcheck_fm:
assumes "mânat" "nânat" "pânat" "oânat"
shows "arity(is_Hcheck_fm(m,n,p,o)) = succ(o) âª succ(n) âª succ(p) âª succ(m) "
unfolding is_Hcheck_fm_def
using assms arity_Replace_fm[rule_format,OF PHcheck_fm_type _ _ _ arity_PHcheck_fm]
pred_Un_distrib Un_assoc Un_nat_type
by simp

â â¹The relational version of check is hand-made because our automatic tool
does not handle \<^term>â¹wfrecâº.âº
definition
is_check :: "[iâo,i,i,i] â o" where
"is_check(M,o,x,z) â¡ ârch[M]. is_rcheck(M,x,rch) â§
is_wfrec(M,is_Hcheck(M,o),rch,x,z)"

â â¹Finally, we internalize the formula.âº
definition
check_fm :: "[i,i,i] â i" where

lemma check_fm_type[TC]: "xânat â¹ oânat â¹ zânat â¹ check_fm(x,o,z) â formula"

lemma sats_check_fm :
assumes
"oânat" "xânat" "zânat" "envâlist(M)" "0âM"
shows
"(M , env â¨ check_fm(x,o,z)) â· is_check(##M,nth(o,env),nth(x,env),nth(z,env))"
proof -
have sats_is_Hcheck_fm:
"âa0 a1 a2 a3 a4 a6. â¦ a0âM; a1âM; a2âM; a3âM; a4âM;a6 âMâ§ â¹
is_Hcheck(##M,a6,a2, a1, a0) â·
(M , [a0,a1,a2,a3,a4,r,a6]@env â¨ is_Hcheck_fm(6,2,1,0))" if "râM" for r
using that assms
by simp
then
â· is_wfrec(##M,is_Hcheck(##M,nth(o,env)),r,nth(x,env),nth(z,env))"
if "râM" for r
using that assms is_wfrec_iff_sats'[symmetric]
by simp
then
show ?thesis
unfolding is_check_def check_fm_def
using assms is_rcheck_iff_sats[symmetric]
by simp
qed

lemma iff_sats_check_fm[iff_sats] :
assumes
"nth(o, env) = oa" "nth(x, env) = xa" "nth(z, env) = za" "o â nat" "x â nat" "z â nat" "env â list(A)" "0 â A"
shows "is_check(##A, oa,xa, za) â· A, env â¨ check_fm(x,o, z)"
using assms sats_check_fm[symmetric]
by auto

lemma arity_check_fm[arity]:
assumes "mânat" "nânat" "oânat"
shows "arity(check_fm(m,n,o)) = succ(o) âª succ(n) âª succ(m) "
unfolding check_fm_def
using assms arity_is_wfrec_fm[rule_format,OF _ _ _ _ _ arity_is_Hcheck_fm]
pred_Un_distrib Un_assoc arity_tran_closure_fm

notation check_fm (â¹â_â§v_ is _ââº)

subsectionâ¹Names for forcing the Axiom of Choice.âº
definition
upair_name :: "i â i â i â i" where

relativize "upair_name" "is_upair_name"
synthesize "upair_name" from_definition "is_upair_name"
arity_theorem for "upair_name_fm"

definition
opair_name :: "i â i â i â i" where
"opair_name(Ï,Ï,on) â¡ upair_name(upair_name(Ï,Ï,on),upair_name(Ï,Ï,on),on)"

relativize "opair_name" "is_opair_name"
synthesize "opair_name" from_definition "is_opair_name"
arity_theorem for "opair_name_fm"

definition
is_opname_check :: "[iâo,i,i,i,i] â o" where
"is_opname_check(M,on,s,x,y) â¡ âchx[M]. âsx[M]. is_check(M,on,x,chx) â§
fun_apply(M,s,x,sx) â§ is_opair_name(M,chx,sx,on,y)"

synthesize "is_opname_check" from_definition assuming "nonempty"
arity_theorem for "is_opname_check_fm"

â â¹The pair of elements belongs to some set. The intended set is the preorder.âº
definition
is_leq :: "[iâo,i,i,i] â o" where
"is_leq(A,l,q,p) â¡ âqp[A]. (pair(A,q,p,qp) â§ qpâl)"

synthesize "is_leq" from_definition assuming "nonempty"
arity_theorem for "is_leq_fm"

abbreviation
fm_leq :: "[i,i,i] â i" (â¹â_â¼â_â_ââº) where
"fm_leq(A,l,B) â¡ is_leq_fm(l,A,B)"

subsectionâ¹Formulas used to prove some generic instances.âº

definition Ï_repl :: "iâi" where
shows "`