section‹Cohen forcing notions› theory Partial_Functions_Relative imports Cardinal_Library_Relative begin text‹In this theory we introduce bounded partial functions and its relative version; for historical reasons the relative version is based on a proper definition of partial functions. We note that finite partial functions are easier and are used to prove some lemmas about finite sets in the theory \<^theory>‹Transitive_Models.ZF_Library_Relative›.› definition Fn :: "[i,i,i] ⇒ i" where "Fn(κ,I,J) ≡ ⋃{y . d ∈ Pow(I), y=(d→J) ∧ d≺κ}" lemma domain_function_lepoll : assumes "function(r)" shows "domain(r) ≲ r" proof - let ?f="λx∈domain(r) . ⟨x,r`x⟩" have "⟨x, r ` x⟩ ∈ r" if "⟨x, y⟩ ∈ r" for x y proof - have "x∈domain(r)" using that by auto with assms show ?thesis using function_apply_Pair by auto qed then have "?f ∈ inj(domain(r), r)" by(rule_tac lam_injective,auto) then show ?thesis unfolding lepoll_def by force qed lemma function_lepoll: assumes "r:d→J" shows "r ≲ d" proof - let ?f="λx∈r . fst(x)" note assms Pi_iff[THEN iffD1,OF assms] moreover from calculation have "r`fst(x) = snd(x)" if "x∈r" for x using that apply_equality by auto ultimately have "?f∈inj(r,d)" by(rule_tac d= "λu . ⟨u, r`u⟩" in lam_injective,auto) then show ?thesis unfolding lepoll_def by auto qed lemma function_eqpoll : assumes "r:d→J" shows "r ≈ d" using assms domain_of_fun domain_function_lepoll Pi_iff[THEN iffD1,OF assms] eqpollI[OF function_lepoll[OF assms]] subset_imp_lepoll by force lemma Fn_char : "Fn(κ,I,J) = {f ∈ Pow(I×J) . function(f) ∧ f ≺ κ}" (is "?L=?R") proof (intro equalityI subsetI) fix x assume "x ∈ ?R" moreover from this have "domain(x) ∈ Pow(I)" "domain(x) ≲ x" "x≺ κ" using domain_function_lepoll by auto ultimately show "x ∈ ?L" unfolding Fn_def using lesspoll_trans1 Pi_iff by (auto,rule_tac rev_bexI[of "domain(x) → J"],auto) next fix x assume "x ∈ ?L" then obtain d where "x:d→J" "d ∈ Pow(I)" "d≺κ" unfolding Fn_def by auto moreover from this have "x≺κ" using function_lepoll[THEN lesspoll_trans1] by auto moreover from calculation have "x ∈ Pow(I×J)" "function(x)" using Pi_iff by auto ultimately show "x ∈ ?R" by simp qed lemma zero_in_Fn: assumes "0 < κ" shows "0 ∈ Fn(κ, I, J)" using lt_Card_imp_lesspoll assms zero_lesspoll unfolding Fn_def by (simp,rule_tac x="0→J" in bexI,simp) (rule ReplaceI[of _ 0],simp_all) lemma Fn_nat_eq_FiniteFun: "Fn(nat,I,J) = I -||> J" proof (intro equalityI subsetI) fix x assume "x ∈ I -||> J" then show "x ∈ Fn(nat,I,J)" proof (induct) case emptyI then show ?case using zero_in_Fn ltI by simp next case (consI a b h) then obtain d where "h:d→J" "d≺nat" "d⊆I" unfolding Fn_def by auto moreover from this have "Finite(d)" using lesspoll_nat_is_Finite by simp ultimately have "h : d -||> J" using fun_FiniteFunI Finite_into_Fin by blast note ‹h:d→J› moreover from this have "domain(cons(⟨a, b⟩, h)) = cons(a,d)" (is "domain(?h) = ?d") and "domain(h) = d" using domain_of_fun by simp_all moreover note consI moreover from calculation have "cons(⟨a, b⟩, h) ∈ cons(a,d) → J" using fun_extend3 by simp moreover from ‹Finite(d)› have "Finite(cons(a,d))" by simp moreover from this have "cons(a,d) ≺ nat" using Finite_imp_lesspoll_nat by simp ultimately show ?case unfolding Fn_def by (simp,rule_tac x="?d→J" in bexI) (force dest:app_fun)+ qed next fix x assume "x ∈ Fn(nat,I,J)" then obtain d where "x:d→J" "d ∈ Pow(I)" "d≺nat" unfolding Fn_def by auto moreover from this have "Finite(d)" using lesspoll_nat_is_Finite by simp moreover from calculation have "d ∈ Fin(I)" using Finite_into_Fin[of d] Fin_mono by auto ultimately show "x ∈ I -||> J" using fun_FiniteFunI FiniteFun_mono by blast qed lemma Fn_nat_subset_Pow: "Fn(κ,I,J) ⊆ Pow(I×J)" using Fn_char by auto lemma FnI: assumes "p : d → J" "d ⊆ I" "d ≺ κ" shows "p ∈ Fn(κ,I,J)" using assms unfolding Fn_def by auto lemma FnD[dest]: assumes "p ∈ Fn(κ,I,J)" shows "∃d. p : d → J ∧ d ⊆ I ∧ d ≺ κ" using assms unfolding Fn_def by auto lemma Fn_is_function: "p ∈ Fn(κ,I,J) ⟹ function(p)" unfolding Fn_def using fun_is_function by auto lemma Fn_csucc: assumes "Ord(κ)" shows "Fn(csucc(κ),I,J) = ⋃{y . d ∈ Pow(I), y=(d→J) ∧ d≲κ}" using assms unfolding Fn_def using lesspoll_csucc by (simp) definition FnleR :: "i ⇒ i ⇒ o" (infixl ‹⊇› 50) where "f ⊇ g ≡ g ⊆ f" lemma FnleR_iff_subset [iff]: "f ⊇ g ⟷ g ⊆ f" unfolding FnleR_def .. definition Fnlerel :: "i ⇒ i" where "Fnlerel(A) ≡ Rrel(λx y. x ⊇ y,A)" definition Fnle :: "[i,i,i] ⇒ i" where "Fnle(κ,I,J) ≡ Fnlerel(Fn(κ,I,J))" lemma FnleI[intro]: assumes "p ∈ Fn(κ,I,J)" "q ∈ Fn(κ,I,J)" "p ⊇ q" shows "⟨p,q⟩ ∈ Fnle(κ,I,J)" using assms unfolding Fnlerel_def Fnle_def FnleR_def Rrel_def by auto lemma FnleD[dest]: assumes "⟨p,q⟩ ∈ Fnle(κ,I,J)" shows "p ∈ Fn(κ,I,J)" "q ∈ Fn(κ,I,J)" "p ⊇ q" using assms unfolding Fnlerel_def Fnle_def FnleR_def Rrel_def by auto definition PFun_Space_Rel :: "[i,i⇒o, i] ⇒ i" ("_⇀⇗_⇖_") where "A ⇀⇗M⇖ B ≡ {f ∈ Pow(A×B) . M(f) ∧ function(f)}" lemma (in M_library) PFun_Space_subset_Powrel : assumes "M(A)" "M(B)" shows "A ⇀⇗M⇖ B = {f ∈ Pow⇗M⇖(A×B) . function(f)}" using Pow_rel_char assms unfolding PFun_Space_Rel_def by auto lemma (in M_library) PFun_Space_closed : assumes "M(A)" "M(B)" shows "M(A ⇀⇗M⇖ B)" using assms PFun_Space_subset_Powrel separation_is_function by auto lemma pfun_is_function : "f ∈ A⇀⇗M⇖ B ⟹ function(f)" unfolding PFun_Space_Rel_def by simp lemma pfun_range : "f ∈ A ⇀⇗M⇖ B ⟹ range(f) ⊆ B" unfolding PFun_Space_Rel_def by auto lemma pfun_domain : "f ∈ A ⇀⇗M⇖ B ⟹ domain(f) ⊆ A" unfolding PFun_Space_Rel_def by auto lemma Un_filter_fun_space_closed: assumes "G ⊆ I → J" "⋀ f g . f∈G ⟹ g∈G ⟹ ∃d∈I→ J . d ⊇ f ∧ d ⊇ g" shows "⋃G ∈ Pow(I×J)" "function(⋃G)" proof - from assms show "⋃G ∈ Pow(I×J)" using Union_Pow_iff unfolding Pi_def by auto next show "function(⋃G)" unfolding function_def proof(auto) fix B B' x y y' assume "B ∈ G" "⟨x, y⟩ ∈ B" "B' ∈ G" "⟨x, y'⟩ ∈ B'" moreover from assms this have "B ∈ I → J" "B' ∈ I → J" by auto moreover from calculation assms(2)[of B B'] obtain d where "d ⊇ B" "d ⊇ B'" "d∈I → J" "⟨x, y⟩ ∈ d" "⟨x, y'⟩ ∈ d" using subsetD[OF ‹G⊆_›] by auto then show "y=y'" using fun_is_function[OF ‹d∈_›] unfolding function_def by force qed qed lemma Un_filter_is_fun : assumes "G ⊆ I → J" "⋀ f g . f∈G ⟹ g∈G ⟹ ∃d∈I→ J . d⊇f ∧ d⊇g" "G≠0" shows "⋃G ∈ I → J" using assms Un_filter_fun_space_closed Pi_iff proof(simp_all) show "I⊆domain(⋃G)" proof - from ‹G≠0› obtain f where "f⊆⋃G" "f∈G" by auto with ‹G⊆_› have "f∈I→J" by auto then show ?thesis using subset_trans[OF _ domain_mono[OF ‹f⊆⋃G›],of I] unfolding Pi_def by auto qed qed context M_Pi begin lemma mem_function_space_relD: assumes "f ∈ function_space_rel(M,A,y)" "M(A)" "M(y)" shows "f ∈ A → y" and "M(f)" using assms function_space_rel_char by simp_all lemma pfunI : assumes "C⊆A" "f ∈ C →⇗M⇖ B" "M(C)" "M(B)" shows "f∈ A ⇀⇗M⇖ B" proof - from assms have "f ∈ C→B" "M(f)" using mem_function_space_relD by simp_all with assms show ?thesis using Pi_iff unfolding PFun_Space_Rel_def by auto qed lemma zero_in_PFun_rel: assumes "M(I)" "M(J)" shows "0 ∈ I ⇀⇗M⇖ J" using pfunI[of 0] nonempty mem_function_space_rel_abs assms by simp lemma pfun_subsetI : assumes "f ∈ A ⇀⇗M⇖ B" "g⊆f" "M(g)" shows "g∈ A ⇀⇗M⇖ B" using assms function_subset unfolding PFun_Space_Rel_def by auto lemma pfun_Un_filter_closed: assumes "G ⊆I⇀⇗M⇖ J" "⋀ f g . f∈G ⟹ g∈G ⟹ ∃d∈I⇀⇗M⇖ J . d⊇f ∧ d⊇g" shows "⋃G ∈ Pow(I×J)" "function(⋃G)" proof - from assms show "⋃G ∈ Pow(I×J)" using Union_Pow_iff unfolding PFun_Space_Rel_def by auto next show "function(⋃G)" unfolding function_def proof(auto) fix B B' x y y' assume "B ∈ G" "⟨x, y⟩ ∈ B" "B' ∈ G" "⟨x, y'⟩ ∈ B'" moreover from calculation assms obtain d where "d ∈ I ⇀⇗M⇖ J" "function(d)" "⟨x, y⟩ ∈ d" "⟨x, y'⟩ ∈ d" using pfun_is_function by force ultimately show "y=y'" unfolding function_def by auto qed qed lemma pfun_Un_filter_closed'': assumes "G ⊆I⇀⇗M⇖ J" "⋀ f g . f∈G ⟹ g∈G ⟹ ∃d∈G . d⊇f ∧ d⊇g" shows "⋃G ∈ Pow(I×J)" "function(⋃G)" proof - from assms have "⋀ f g . f∈G ⟹ g∈G ⟹ ∃d∈I⇀⇗M⇖ J . d⊇f ∧ d⊇g" using subsetD[OF assms(1),THEN [2] bexI] by force then show "⋃G ∈ Pow(I×J)" "function(⋃G)" using assms pfun_Un_filter_closed unfolding PFun_Space_Rel_def by auto qed lemma pfun_Un_filter_closed': assumes "G ⊆I⇀⇗M⇖ J" "⋀ f g . f∈G ⟹ g∈G ⟹ ∃d∈G . d⊇f ∧ d⊇g" "M(G)" shows "⋃G ∈ I⇀⇗M⇖ J" using assms pfun_Un_filter_closed'' unfolding PFun_Space_Rel_def by auto lemma pfunD : assumes "f ∈ A⇀⇗M⇖ B" shows "∃C[M]. C⊆A ∧ f ∈ C→B" proof - note assms moreover from this have "f∈Pow(A×B)" "function(f)" "M(f)" unfolding PFun_Space_Rel_def by simp_all moreover from this have "domain(f) ⊆ A" "f ∈ domain(f) → B" "M(domain(f))" using assms Pow_iff[of f "A×B"] domain_subset Pi_iff by auto ultimately show ?thesis by auto qed lemma pfunD_closed : assumes "f ∈ A⇀⇗M⇖ B" shows "M(f)" using assms unfolding PFun_Space_Rel_def by simp lemma pfun_singletonI : assumes "x ∈ A" "b ∈ B" "M(A)" "M(B)" shows "{⟨x,b⟩} ∈ A⇀⇗M⇖ B" using assms transM[of x A] transM[of b B] unfolding PFun_Space_Rel_def function_def by auto lemma pfun_unionI : assumes "f ∈ A⇀⇗M⇖ B" "g ∈ A⇀⇗M⇖ B" "domain(f)∩domain(g)=0" shows "f∪g ∈ A⇀⇗M⇖ B" using assms unfolding PFun_Space_Rel_def function_def by blast lemma (in M_library) pfun_restrict_eq_imp_compat: assumes "f ∈ I⇀⇗M⇖ J" "g ∈ I⇀⇗M⇖ J" "M(J)" "restrict(f, domain(f) ∩ domain(g)) = restrict(g, domain(f) ∩ domain(g))" shows "f ∪ g ∈ I⇀⇗M⇖ J" proof - note assms moreover from this obtain C D where "f : C → J" "C ⊆ I" "D ⊆ I" "M(C)" "M(D)" "g : D → J" using pfunD[of f] pfunD[of g] by force moreover from calculation have "f∪g ∈ C∪D → J" using restrict_eq_imp_Un_into_Pi'[OF ‹f∈C→_› ‹g∈D→_›] by auto ultimately show ?thesis using pfunI[of "C∪D" _ "f∪g"] Un_subset_iff pfunD_closed function_space_rel_char by auto qed lemma FiniteFun_pfunI : assumes "f ∈ A-||> B" "M(A)" "M(B)" shows "f ∈ A ⇀⇗M⇖ B" using assms(1) proof(induct) case emptyI then show ?case using assms nonempty mem_function_space_rel_abs pfunI[OF empty_subsetI, of 0] by simp next case (consI a b h) note consI moreover from this have "M(a)" "M(b)" "M(h)" "domain(h) ⊆ A" using transM[OF _ ‹M(A)›] transM[OF _ ‹M(B)›] FinD FiniteFun_domain_Fin pfunD_closed by simp_all moreover from calculation have "{a}∪domain(h)⊆A" "M({a}∪domain(h))" "M(cons(<a,b>,h))" "domain(cons(<a,b>,h)) = {a}∪domain(h)" by auto moreover from calculation have "cons(<a,b>,h) ∈ {a}∪domain(h) → B" using FiniteFun_is_fun[OF FiniteFun.consI, of a A b B h] by auto ultimately show "cons(<a,b>,h) ∈ A ⇀⇗M⇖ B" using assms mem_function_space_rel_abs pfunI by simp_all qed lemma PFun_FiniteFunI : assumes "f ∈ A ⇀⇗M⇖ B" "Finite(f)" shows "f ∈ A-||> B" proof - from assms have "f∈Fin(A×B)" "function(f)" using Finite_Fin Pow_iff unfolding PFun_Space_Rel_def by auto then show ?thesis using FiniteFunI by simp qed end ― ‹\<^locale>‹M_Pi›› definition Fn_rel :: "[i⇒o,i,i,i] ⇒ i" (‹Fn⇗_⇖'(_,_,_')›) where "Fn_rel(M,κ,I,J) ≡ {f ∈ I⇀⇗M⇖ J . f ≺⇗M⇖ κ}" ― ‹Eventually we can define \<^term>‹Fn_rel› as the relativization of \<^term>‹Fn›› context M_library begin lemma Fn_rel_subset_PFun_rel : "Fn⇗M⇖(κ,I,J) ⊆ I⇀⇗M⇖ J" unfolding Fn_rel_def by auto lemma Fn_relI[intro]: assumes "f : d → J" "d ⊆ I" "f ≺⇗M⇖ κ" "M(d)" "M(J)" "M(f)" shows "f ∈ Fn_rel(M,κ,I,J)" using assms pfunI mem_function_space_rel_abs unfolding Fn_rel_def by auto lemma Fn_relD[dest]: assumes "p ∈ Fn_rel(M,κ,I,J)" shows "∃C[M]. C⊆I ∧ p : C → J ∧ p ≺⇗M⇖ κ" using assms pfunD unfolding Fn_rel_def by simp lemma Fn_rel_is_function: assumes "p ∈ Fn_rel(M,κ,I,J)" shows "function(p)" "M(p)" "p ≺⇗M⇖ κ" "p∈ I⇀⇗M⇖ J" using assms unfolding Fn_rel_def PFun_Space_Rel_def by simp_all lemma Fn_rel_mono: assumes "p ∈ Fn_rel(M,κ,I,J)" "κ ≺⇗M⇖ κ'" "M(κ)" "M(κ')" shows "p ∈ Fn_rel(M,κ',I,J)" using assms lesspoll_rel_trans[OF _ assms(2)] cardinal_rel_closed Fn_rel_is_function(2)[OF assms(1)] unfolding Fn_rel_def by simp lemma Fn_rel_mono': assumes "p ∈ Fn_rel(M,κ,I,J)" "κ ≲⇗M⇖ κ'" "M(κ)" "M(κ')" shows "p ∈ Fn_rel(M,κ',I,J)" proof - note assms then consider "κ ≺⇗M⇖ κ'" | "κ ≈⇗M⇖ κ'" using lepoll_rel_iff_leqpoll_rel by auto then show ?thesis proof(cases) case 1 with assms show ?thesis using Fn_rel_mono by simp next case 2 then show ?thesis using assms cardinal_rel_closed Fn_rel_is_function[OF assms(1)] lesspoll_rel_eq_trans unfolding Fn_rel_def by simp qed qed lemma Fn_csucc: assumes "Ord(κ)" "M(κ)" shows "Fn_rel(M,(κ⇧^{+})⇗M⇖,I,J) = {p∈ I⇀⇗M⇖ J . p ≲⇗M⇖ κ}" (is "?L=?R") using assms proof(intro equalityI) show "?L ⊆ ?R" proof(intro subsetI) fix p assume "p∈?L" then have "p ≺⇗M⇖ csucc_rel(M,κ)" "M(p)" "p∈ I⇀⇗M⇖ J" using Fn_rel_is_function by simp_all then show "p∈?R" using assms lesspoll_rel_csucc_rel by simp qed next show "?R⊆?L" proof(intro subsetI) fix p assume "p∈?R" then have "p∈ I⇀⇗M⇖ J" "p ≲⇗M⇖ κ" using assms lesspoll_rel_csucc_rel by simp_all then show "p∈?L" using assms lesspoll_rel_csucc_rel pfunD_closed unfolding Fn_rel_def by simp qed qed lemma Finite_imp_lesspoll_nat: assumes "Finite(A)" shows "A ≺ nat" using assms subset_imp_lepoll[OF naturals_subset_nat] eq_lepoll_trans n_lesspoll_nat eq_lesspoll_trans unfolding Finite_def lesspoll_def by auto lemma FinD_Finite : assumes "a∈Fin(A)" shows "Finite(a)" using assms by(induct,simp_all) lemma Fn_rel_nat_eq_FiniteFun: assumes "M(I)" "M(J)" shows "I -||> J = Fn_rel(M,ω,I,J)" proof(intro equalityI subsetI) fix p assume "p∈I -||> J" with assms have "p∈ I ⇀⇗M⇖ J" "Finite(p)" using FiniteFun_pfunI FinD_Finite[OF subsetD[OF FiniteFun.dom_subset,OF ‹p∈_›]] by auto moreover from this have "p ≺⇗M⇖ ω" using Finite_lesspoll_rel_nat pfunD_closed[of p] n_lesspoll_rel_nat by simp ultimately show "p∈ Fn_rel(M,ω,I,J)" unfolding Fn_rel_def by simp next fix p assume "p∈ Fn_rel(M,ω,I,J)" then have "p∈ I ⇀⇗M⇖ J" "p ≺⇗M⇖ ω" unfolding Fn_rel_def by simp_all moreover from this have "Finite(p)" using Finite_cardinal_rel_Finite lesspoll_rel_nat_is_Finite_rel pfunD_closed cardinal_rel_closed[of p] Finite_cardinal_rel_iff'[THEN iffD1] by simp ultimately show "p∈I -||> J" using PFun_FiniteFunI by simp qed lemma Fn_nat_abs: assumes "M(I)" "M(J)" shows "Fn(nat,I,J) = Fn_rel(M,ω,I,J)" using assms Fn_rel_nat_eq_FiniteFun Fn_nat_eq_FiniteFun by simp lemma Fn_rel_singletonI: assumes "x ∈ I" "j ∈ J" "1 ≺⇗M⇖ κ" "M(κ)" "M(I)" "M(J)" shows "{⟨x,j⟩} ∈ Fn⇗M⇖(κ,I,J)" using pfun_singletonI transM[of x] transM[of j] assms eq_lesspoll_rel_trans[OF singleton_eqpoll_rel_1] unfolding Fn_rel_def by auto end ― ‹\<^locale>‹M_library›› definition Fnle_rel :: "[i⇒o,i,i,i] ⇒ i" (‹Fnle⇗_⇖'(_,_,_')›) where "Fnle_rel(M,κ,I,J) ≡ Fnlerel(Fn⇗M⇖(κ,I,J))" abbreviation Fn_r_set :: "[i,i,i,i] ⇒ i" (‹Fn⇗_⇖'(_,_,_')›) where "Fn_r_set(M) ≡ Fn_rel(##M)" abbreviation Fnle_r_set :: "[i,i,i,i] ⇒ i" (‹Fnle⇗_⇖'(_,_,_')›) where "Fnle_r_set(M) ≡ Fnle_rel(##M)" context M_library begin lemma Fnle_relI[intro]: assumes "p ∈ Fn_rel(M,κ,I,J)" "q ∈ Fn_rel(M,κ,I,J)" "p ⊇ q" shows "⟨p, q⟩ ∈ Fnle_rel(M,κ,I,J)" using assms unfolding Fnlerel_def Fnle_rel_def FnleR_def Rrel_def by auto lemma Fnle_relD[dest]: assumes "⟨p, q⟩ ∈ Fnle_rel(M,κ,I,J)" shows "p ∈ Fn_rel(M,κ,I,J)" "q ∈ Fn_rel(M,κ,I,J)" "p ⊇ q" using assms unfolding Fnlerel_def Fnle_rel_def FnleR_def Rrel_def by auto lemma Fn_rel_closed[intro,simp]: assumes "M(κ)" "M(I)" "M(J)" shows "M(Fn⇗M⇖(κ,I,J))" using assms separation_cardinal_rel_lesspoll_rel PFun_Space_closed unfolding Fn_rel_def by auto lemma Fn_rel_subset_Pow: assumes "M(κ)" "M(I)" "M(J)" shows "Fn⇗M⇖(κ,I,J) ⊆ Pow(I×J)" unfolding Fn_rel_def PFun_Space_Rel_def by auto lemma Fnle_rel_closed[intro,simp]: assumes "M(κ)" "M(I)" "M(J)" shows "M(Fnle⇗M⇖(κ,I,J))" unfolding Fnle_rel_def Fnlerel_def Rrel_def FnleR_def using assms supset_separation Fn_rel_closed by auto lemma zero_in_Fn_rel: assumes "0<κ" "M(κ)" "M(I)" "M(J)" shows "0 ∈ Fn⇗M⇖(κ, I, J)" unfolding Fn_rel_def using zero_in_PFun_rel zero_lesspoll_rel assms by simp lemma zero_top_Fn_rel: assumes "p∈Fn⇗M⇖(κ, I, J)" "0<κ" "M(κ)" "M(I)" "M(J)" shows "⟨p, 0⟩ ∈ Fnle⇗M⇖(κ, I, J)" using assms zero_in_Fn_rel unfolding preorder_on_def refl_def trans_on_def by auto lemma preorder_on_Fnle_rel: assumes "M(κ)" "M(I)" "M(J)" shows "preorder_on(Fn⇗M⇖(κ, I, J), Fnle⇗M⇖(κ, I, J))" unfolding preorder_on_def refl_def trans_on_def by blast end ― ‹\<^locale>‹M_library›› 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 end ― ‹\<^locale>‹M_cardinal_library›› context M_cardinal_library_extra begin 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 lemma 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 restrict_eq_imp_compat_rel: assumes "p ∈ Fn⇗M⇖(κ, I, J)" "q ∈ Fn⇗M⇖(κ, I, J)" "InfCard⇗M⇖(κ)" "M(J)" "M(κ)" "restrict(p, domain(p) ∩ domain(q)) = restrict(q, domain(p) ∩ domain(q))" 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 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 cons_in_Fn_rel: assumes "x ∉ domain(p)" "p ∈ Fn⇗M⇖(κ,I,J)" "x ∈ I" "j ∈ J" "InfCard⇗M⇖(κ)" "M(κ)" "M(I)" "M(J)" shows "cons(⟨x,j⟩, p) ∈ Fn⇗M⇖(κ,I,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 dense_dom_dense: assumes "x ∈ I" "InfCard⇗M⇖(κ)" "M(I)" "M(J)" "z∈J" "M(κ)" "p∈Fn⇗M⇖(κ, I, J)" shows "∃d∈{ p ∈ Fn⇗M⇖(κ, I, J) . x ∈ domain(p) }. ⟨d,p⟩ ∈ Fnle⇗M⇖(κ, I, J)" proof (cases "x ∈ domain(p)") case True with ‹x ∈ I› ‹p ∈ Fn⇗M⇖(κ, I, J)› show ?thesis by auto next case False note ‹p ∈ Fn⇗M⇖(κ, I, J)› moreover from this and False and assms have "cons(⟨x,z⟩, p) ∈ Fn⇗M⇖(κ, I, J)" "M(x)" using cons_in_Fn_rel by (auto dest:transM) ultimately show ?thesis using Fn_relD by blast qed lemma (in M_cardinal_library) domain_lepoll_rel : assumes "function(r)" "M(r)" shows "domain(r) ≲⇗M⇖ r" proof - let ?f="λx∈domain(r) . ⟨x,r`x⟩" have "⟨x, r ` x⟩ ∈ r" if "⟨x, y⟩ ∈ r" for x y proof - have "x∈domain(r)" using that by auto with assms show ?thesis using function_apply_Pair by auto qed then have "?f ∈ inj(domain(r), r)" by(rule_tac lam_injective,auto) moreover note assms moreover from calculation have "M(?f)" using lam_replacement_constant[of r] lam_replacement_identity assms lam_replacement_apply lam_replacement_Pair[THEN [5] lam_replacement_hcomp2] by(rule_tac lam_replacement_imp_lam_closed,auto dest:transM[of _ r]) ultimately have "?f ∈ inj⇗M⇖(domain(r),r)" using inj_rel_char by auto with ‹M(?f)› show ?thesis using lepoll_relI by simp qed lemma dense_surj_dense: assumes "x ∈ J" "InfCard⇗M⇖(κ)" "M(I)" "M(J)" "M(κ)" "p∈Fn⇗M⇖(κ, I, J)" "κ ≲⇗M⇖ I" shows "∃d∈{ p ∈ Fn⇗M⇖(κ, I, J) . x ∈ range(p) }. ⟨d,p⟩ ∈ Fnle⇗M⇖(κ, I, J)" proof - from ‹p ∈ _› ‹M(J)› ‹x∈_› lesspoll_rel_def have "domain(p) ⊆ I" "M(p)" "p ≺⇗M⇖ κ" "M(x)" "function(p)" using pfun_domain[OF Fn_rel_is_function(4)] Fn_rel_is_function transM[of x J] by simp_all moreover from calculation assms have 1:"domain(p) ≺⇗M⇖ κ" "M(domain(p))" "domain(p) ≺⇗M⇖ I" using domain_lepoll_rel lesspoll_rel_trans1[of "domain(p)" p κ] lesspoll_rel_trans2 by auto with calculation ‹κ ≲⇗M⇖ I› ‹M(I)› ‹M(κ)› have "domain(p) ≠ I" proof - {assume "domain(p) = I" with 1 have "domain(p) ≺⇗M⇖ domain(p)" by auto with ‹M(domain(p))› have False using lesspoll_rel_irrefl[of "domain(p)"] by simp } then show ?thesis by auto qed ultimately obtain α where "α ∉ domain(p)" "α∈I" by force moreover note assms moreover from calculation have "cons(⟨α,x⟩, p) ∈ Fn⇗M⇖(κ, I, J)" using InfCard_rel_Aleph_rel cons_in_Fn_rel[of α p κ I J x] by auto ultimately show ?thesis using Fnle_relI by blast qed end ― ‹\<^locale>‹M_cardinal_library_extra›› end