Theory Partial_Functions_Relative

sectionCohen 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=(dJ)  dκ}"

lemma domain_function_lepoll :
  assumes "function(r)"
  shows "domain(r)  r"
proof -
  let ?f="λxdomain(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:dJ"
  shows "r  d"
proof -
  let ?f="λxr . 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 "xr" 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 "?finj(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:dJ"
  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:dJ" "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="0J" 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:dJ" "dnat" "dI" 
      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:dJ
    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="?dJ" in bexI)
        (force dest:app_fun)+
  qed
next
  fix x
  assume "x  Fn(nat,I,J)"
  then
  obtain d where "x:dJ" "d  Pow(I)" "dnat"
    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=(dJ)  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,io, i]  i"  ("_⇀⇗__")
  where "A ⇀⇗MB  {f  Pow(A×B) . M(f)  function(f)}"

lemma (in M_library) PFun_Space_subset_Powrel :
  assumes "M(A)" "M(B)"
  shows "A ⇀⇗MB = {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 ⇀⇗MB)"
  using assms PFun_Space_subset_Powrel separation_is_function
  by auto

lemma Un_filter_fun_space_closed:
  assumes "G  I  J" " f g . fG  gG  dI 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'" "dI  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 . fG  gG  dI J . df  dg" "G0"
  shows "G  I  J"
  using assms Un_filter_fun_space_closed Pi_iff
proof(simp_all)
  show "Idomain(G)"
  proof -
    from G0
    obtain f where "fG" "fG"
      by auto
    with G_
    have "fIJ" by auto
    then
    show ?thesis
      using subset_trans[OF _ domain_mono[OF fG],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 "CA" "f  C →⇗MB" "M(C)" "M(B)"
  shows "f A ⇀⇗MB"
proof -
  from assms
  have "f  CB" "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 ⇀⇗MJ"
  using pfunI[of 0] nonempty mem_function_space_rel_abs assms
  by simp

lemma pfun_subsetI :
  assumes "f  A ⇀⇗MB" "gf" "M(g)"
  shows "g A ⇀⇗MB"
using assms function_subset
  unfolding PFun_Space_Rel_def
  by auto

lemma pfun_is_function :
  "f  A⇀⇗MB  function(f)"
  unfolding PFun_Space_Rel_def by simp

lemma pfun_Un_filter_closed:
  assumes "G I⇀⇗MJ" " f g . fG  gG  dI⇀⇗MJ . df  dg"
  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 ⇀⇗MJ" "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⇀⇗MJ" " f g . fG  gG  dG . df  dg"
  shows "G  Pow(I×J)" "function(G)"
proof -
  from assms
  have " f g . fG  gG  dI⇀⇗MJ . df  dg"
    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⇀⇗MJ" " f g . fG  gG  dG . df  dg" "M(G)"
  shows "G  I⇀⇗MJ"
  using assms pfun_Un_filter_closed''
  unfolding PFun_Space_Rel_def
  by auto

lemma pfunD :
  assumes "f  A⇀⇗MB"
  shows "C[M]. CA  f  CB"
proof -
  note assms
  moreover from this
  have "fPow(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⇀⇗MB"
  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⇀⇗MB"
  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⇀⇗MB" "g  A⇀⇗MB" "domain(f)domain(g)=0"
  shows "fg  A⇀⇗MB"
  using assms
  unfolding PFun_Space_Rel_def function_def
  by blast

lemma (in M_library) pfun_restrict_eq_imp_compat:
  assumes "f  I⇀⇗MJ" "g  I⇀⇗MJ" "M(J)"
    "restrict(f, domain(f)  domain(g)) = restrict(g, domain(f)  domain(g))"
  shows "f  g  I⇀⇗MJ"
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 "fg  CD  J"
    using restrict_eq_imp_Un_into_Pi'[OF fC_ gD_]
    by auto
  ultimately
  show ?thesis
    using pfunI[of "CD" _ "fg"] 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 ⇀⇗MB"
  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 ⇀⇗MB"
    using assms  mem_function_space_rel_abs pfunI
    by simp_all
qed

lemma PFun_FiniteFunI :
  assumes "f  A ⇀⇗MB" "Finite(f)"
  shows  "f  A-||> B"
proof -
  from assms
  have "fFin(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 :: "[io,i,i,i]  i" (Fn⇗_⇖'(_,_,_')) where
  "Fn_rel(M,κ,I,J)  {f  I⇀⇗MJ . |f|⇗M⇖ ≺⇗Mκ}"

context  M_library
begin

lemma Fn_rel_subset_PFun_rel : "Fn⇗M⇖(κ,I,J)  I⇀⇗MJ"
  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]. CI  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⇀⇗MJ"
  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⇀⇗MJ . |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⇖ ≺⇗Mcsucc_rel(M,κ)" "M(p)" "p I⇀⇗MJ"
      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⇀⇗MJ" " |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 "aFin(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 "pI -||> J"
  with assms
  have "p I ⇀⇗MJ" "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 ⇀⇗MJ"  "|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 "pI -||> 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 :: "[io,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 "pFn⇗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 ― ‹localeM_library

end