Theory Partial_Functions_Relative

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