Theory Partial_Functions_Relative

section‹Cohen forcing notions›

theory Partial_Functions_Relative
  imports
    FiniteFun_Relative
    Cardinal_Library_Relative
begin

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,THE y . <x,y> ∈ r>"
  have 1:"⋀x. x ∈ domain(r) ⟹ ∃!y. <x,y> ∈ r"
    using assms unfolding domain_def function_def by auto
  then
  have "?f ∈ inj(domain(r), r)"
    using theI[OF 1]
    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 this
  have 1:"⋀x. x ∈ domain(r) ⟹ ∃!y. <x,y> ∈ r"
    unfolding function_def by auto
  moreover from calculation
  have "(THE u . <fst(x),u> ∈ r) = snd(x)" if "x∈r" for x
    using that subsetD[of r "d×J" x] theI[OF 1]
    by(auto,rule_tac the_equality2[OF 1],auto)
  moreover from calculation
  have "⋀x. x ∈r ⟹ <fst(x),THE y . <fst(x),y> ∈ r> = x"
    by auto
  ultimately
  have "?f∈inj(r,d)"
    by(rule_tac d= "λu . <u,THE y . <u,y> ∈ r>" in lam_injective,force,simp)
  then
  show ?thesis
    unfolding lepoll_def
    by auto
qed

(*FIXME: is this useful? *)
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 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_cardinals
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_is_function :
  "f ∈ A⇀⇗M⇖ B ⟹ function(f)"
  unfolding PFun_Space_Rel_def by simp

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

(* Fn_rel should be the relativization *)
definition
  Fn_rel :: "[i⇒o,i,i,i] ⇒ i" (‹Fn⇗_⇖'(_,_,_')›) where
  "Fn_rel(M,κ,I,J) ≡ {f ∈ I⇀⇗M⇖ J . |f|⇗M⇖ ≺⇗M⇖ κ}"

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⇖ κ" "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⇖ ≺⇗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⇖ ≺⇗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⇖  ≲⇗M⇖ κ}"   (is "?L=?R")
  using assms
proof(intro equalityI)
  show "?L ⊆ ?R"
  proof(intro subsetI)
    fix p
    assume "p∈?L"
    then
    have "|p|⇗M⇖ ≺⇗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⇖  ≲⇗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⇖ ≺⇗M⇖ ω"
    using Finite_cardinal_rel_in_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⇖ ≺⇗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
end

lemma (in M_library) Fn_rel_singletonI:
  assumes "x ∈ I" "j ∈ J" "InfCard⇗M⇖(κ)" "M(κ)" "M(I)" "M(J)"
  shows "{⟨x,j⟩} ∈ Fn⇗M⇖(κ,I,J)"
    using assms pfun_singletonI transM[of x ] transM[of j]
      cardinal_rel_singleton
      lt_Card_rel_imp_lesspoll_rel ltI[OF nat_into_InfCard_rel]
      Card_rel_cardinal_rel Card_rel_is_Ord InfCard_rel_is_Card_rel
    unfolding Fn_rel_def
    by auto

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

end

context M_library
begin

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››

end