Theory Cohen_Posets_Relative

sectionCohen 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 ― ‹localecohen_data

abbreviation
  inj_dense :: "[i,i,i,i]i" where
  "inj_dense(I,J,w,x) 
    { pFn(ω,I×ω,J) . (nω. w,n,1  p  x,n,0  p) }"

lemma dense_inj_dense:
  assumes "w  I" "x  I" "w  x" "pFn(ω,I×ω,J)" "0J" "1J"
  shows "dinj_dense(I,J,w,x). d ,p  Fnle(ω,I×ω,J)"
proof -
  obtain n where "w,n  domain(p)" "x,n  domain(p)" "n  ω"
  proof -
    {
      assume "w,n  domain(p)  x,n  domain(p)" if "n  ω" for n
      then
      have "ω  range(domain(p))" by blast
      then
      have "¬ Finite(p)"
        using Finite_range Finite_domain subset_Finite nat_not_Finite
        by auto
      with p  _
      have False
        using Fn_nat_eq_FiniteFun FiniteFun.dom_subset[of "I×ω" J]
          Fin_into_Finite by auto
    }
    with that― ‹the shape of the goal puts assumptions in this variable
    show ?thesis by auto
  qed
  moreover
  note p  _ assms
  moreover from calculation
  have "cons(x,n,0, p)  Fn(ω,I×ω,J)"
    using FiniteFun.consI[of "x,n" "I×ω" 0 J p]
      Fn_nat_eq_FiniteFun by auto
  ultimately
  have "cons(w,n,1, cons(x,n,0, p) )  Fn(ω,I×ω,J)"
    using FiniteFun.consI[of "w,n" "I × ω" 1 J "cons(x,n,0, p)"]
      Fn_nat_eq_FiniteFun by auto
  with n  ω
  show ?thesis
    using p  _ by (intro bexI) auto
qed

locale add_reals = cohen_data nat _ 2

subsectionCombinatorial 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 "pFn(κ, 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'
  assume "x, y  G" "x, y'  G"
  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

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 ― ‹localecohen_data

locale M_cohen = M_delta +
  assumes
    countable_lepoll_assms2:
    "M(A')  M(A)  M(b)  M(f)  separation(M, λy. xA'. 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. xA'. y = x, μ i. x  if_range_F_else_F(drSR_Y(r', D, A), b, f, i))"

lemma (in M_library) Fnle_rel_Aleph_rel1_closed[intro,simp]:
  "M(Fnle⇗M⇖(ℵ⇘1⇙⇗M, ℵ⇘1⇙⇗M, ω →⇗M2))"
  by simp

locale M_add_reals = M_cohen + add_reals
begin

lemmas zero_lesspoll_rel_kappa = zero_lesspoll_rel[OF zero_lt_kappa]

end ― ‹localeM_add_reals

(* 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 :: "iiio" where
  "antichain(P,leq,A)  AP  (pA. qA. pq  ¬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 :: "[io,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 ― ‹localeM_trivial

relativize relational "ccc" "ccc_rel"

abbreviation
  ccc_rel_abbr :: "[io,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
  unfolding ccc_rel_def by (simp add:absolut)

end ― ‹localeM_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 ― ‹localeM_FiniteFun

context M_add_reals
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 "xF(A,c)  c  (range(f)  {domain(x). xA})"
  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,{pA. domain(p) = d})" if "M(d)" for d
    proof (cases "d≺⇗Mnat  d  I")
      case True
      with A  Fn(nat, I, 2) M(A)
      have "{p  A . domain(p) = d}  d →⇗M2"
        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 →⇗M2)"
        using Finite_Pi[THEN [2] 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 →⇗M2)"
        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→⇗M2" ]
        by (auto intro!:Finite_imp_countable_rel)
    next
      case False
      with A  Fn(nat, I, 2) M(A)
      have "domain(p)  d" if "pA" for p
      proof -
        note False that M(A)
        moreover from this
        obtain d' where "d'  I" "pd'  2" "d'  ω"
          using FnD[OF subsetD[OF A_ pA]]
          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 lam_replacement_minimum
        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). xX}"],auto)
      qed (auto)
      have "aA. 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). pA}"
        using lam_replacement_dC_F lam_replacement_inj_rel M(A)
          lepoll_assumptions domain_eq_separation lam_replacement_minimum
          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). xA}"])
          (auto simp del:if_range_F_else_F_def simp add:dC_F_def)
      from A  Fn(nat, I, 2)
      have x:"(d{domain(p) . p  A}. {pA. domain(p) = d}) = A"
        by auto
      moreover
      assume "countable_rel(M,{domain(p) . p  A})"
      moreover
      note d. M(d)  countable_rel(M,{pA. domain(p) = d})
      moreover from M(A)
      have "pA  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:"d1D. d2D. 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) . pA})"
    proof -
      note M(Fn(nat, I, 2)) M(r)
      moreover from this
      have "fFn(nat, I, 2)  M(restrict(f,r))" for f
        by (blast dest: transM)
      ultimately
      have "fFn(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({pA. domain(p)  D})"
      using domain_mem_separation by simp
    have "uncountable_rel(M,{pA. 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 = (fPow_rel(M,r×2) . {y . pA, 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 zD 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 →⇗M2"
          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 "pA.  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 . pA, 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 lam_replacement_minimum
        by (unfold_locales,simp_all add:drSR_Y_def,rule_tac 1,simp_all)
      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] lam_replacement_minimum
        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 = (fPow_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 "j`0  j`1" "j`0  ?Y(A,f)" "j`1  ?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 "pA. qA. 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 ― ‹localeM_add_reals

end