Theory Cohen_Posets

section‹Cohen forcing notions›

theory Cohen_Posets
  imports
    Forcing_Notions
    Names ― ‹only for \<^term>‹SepReplace››
    Recursion_Thms ― ‹only for the definition of \<^term>‹Rrel››
    "Delta_System_Lemma.ZF_Library"
begin

lemmas app_fun= apply_iff[THEN iffD1]

definition
  Fn :: "[i,i,i] ⇒ i" where
  "Fn(κ,I,J) ≡ ⋃{(d→J) .. d ∈ Pow(I),  d≺κ}"

lemma FnI [intro]:
  assumes "p : d → J" "d ⊆ I" "d ≺ κ"
  shows "p ∈ Fn(κ,I,J)"
  using assms Sep_and_Replace
  unfolding Fn_def by auto

lemma FnD [dest]:
  assumes "p ∈ Fn(κ,I,J)"
  shows "∃d. p : d → J ∧ d ⊆ I ∧ d ≺ κ"
  using assms Sep_and_Replace
  unfolding Fn_def by auto

lemma Fn_is_function : "p ∈ Fn(κ,I,J) ⟹ function(p)"
  unfolding Fn_def using Sep_and_Replace fun_is_function by auto

lemma Fn_csucc :
  assumes "Ord(κ)"
  shows "Fn(csucc(κ),I,J) = ⋃{(d→J) .. d ∈ Pow(I), d≲κ}"
  using assms
  unfolding Fn_def using lesspoll_csucc by (simp)

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 Fn_nat_eq_FiniteFun : "Fn(nat,I,J) = I -||> J"
  unfolding Fn_def
proof (intro equalityI subsetI)
  fix x
  assume "x ∈ I -||> J"
  then
  show "x ∈ ⋃{(d→J) .. d ∈ Pow(I), d≺nat}"
  proof (induct)
    case emptyI
    have "0: 0→J" by simp
    moreover
    have "|0|<nat" using ltI by simp
    ultimately
    show ?case using lt_Card_imp_lesspoll Card_nat
      by (simp,rule_tac x="0→J" in bexI)
        (auto | rule_tac x="0" in bexI)+
  next
    case (consI a b h)
    then
    obtain d where "h:d→J" "d≺nat" "d⊆I" 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 by (simp,rule_tac x="?d→J" in bexI)
        (force dest:app_fun)+
  qed
next
  fix x
  assume "x ∈ ⋃{(d→J) .. d ∈ Pow(I),  d≺nat}"
  then
  obtain d where "x:d→J" "d ∈ Pow(I)" "d≺nat" 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

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

locale cohen_data=
  fixes κ I J::i
  assumes zero_lt_kappa: "0<κ"
begin

lemmas zero_lesspoll_kappa= zero_lesspoll[OF zero_lt_kappa]

end (* cohen_data *)

sublocale cohen_data ⊆ forcing_notion "Fn(κ,I,J)" "Fnle(κ,I,J)" 0
proof
  show "0 ∈ Fn(κ, I, J)"
    unfolding Fn_def
    by (simp,rule_tac x="0 → J" in bexI, auto)
      (rule_tac x=0 in bexI, auto intro:zero_lesspoll_kappa)
  then
  show "∀p∈Fn(κ, 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

(*
(* The following requires Cardinal_Library, dependent on AC *)
lemma InfCard_lesspoll_Un:
  includes Ord_dests
  assumes "InfCard(κ)" "A ≺ κ" "B ≺ κ"
  shows "A ∪ B ≺ κ"
proof -
  from assms
  have "|A| < κ" "|B| < κ"
    using lesspoll_cardinal_lt InfCard_is_Card by auto
  show ?thesis
  proof (cases "Finite(A) ∧ Finite(B)")
    case True
    with assms
    show ?thesis
      using lesspoll_trans2[OF _ le_imp_lepoll, of _ nat κ]
        Finite_imp_lesspoll_nat[OF Finite_Un]
      unfolding InfCard_def by simp
  next
    case False
    then
    have "InfCard(max(|A|,|B|))"
      using Infinite_InfCard_cardinal InfCard_is_Card
        le_trans[of nat] not_le_iff_lt[THEN iffD1, THEN leI, of "|A|" "|B|"]
      unfolding max_def InfCard_def
      by (auto)
    then
    have "|A ∪ B| ≤ max(|A|,|B|)"
      using cardinal_Un_le[of "max(|A|,|B|)"]
        not_le_iff_lt[THEN iffD1, THEN leI, of "|A|" "|B|" ]
      unfolding max_def
      by auto
    moreover from ‹|A| < κ› ‹|B| < κ›
    have "max(|A|,|B|) < κ"
      unfolding max_def by simp
    ultimately
    have "|A ∪ B| <  κ"
      using lt_trans1 by blast
    moreover
    note ‹InfCard(κ)›
    moreover from calculation
    have "|A ∪ B| ≺ κ"
      using lt_Card_imp_lesspoll InfCard_is_Card by simp
    ultimately
    show ?thesis
      using  cardinal_eqpoll eq_lesspoll_trans eqpoll_sym by blast
  qed
qed
*)

subsection‹MOVE THIS to an appropriate place›

definition
  antichain :: "i⇒i⇒i⇒o" where
  "antichain(P,leq,A) ≡ A⊆P ∧ (∀p∈A. ∀q∈A.
                p≠q ⟶ ¬compat_in(P,leq,p,q))"
definition
  ccc :: "i ⇒ i ⇒ o" where
  "ccc(P,leq) ≡ ∀A. antichain(P,leq,A) ⟶ |A| ≤ nat"

subsection‹Combinatorial results on Cohen posets›

context cohen_data
begin

(*
(* The following requires Cardinal_Library, dependent on AC *)
lemma restrict_eq_imp_compat:
  assumes "f ∈ Fn(κ, I, J)" "g ∈ Fn(κ, I, J)" "InfCard(κ)"
    "restrict(f, domain(f) ∩ domain(g)) = restrict(g, domain(f) ∩ domain(g))"
  shows "f ∪ g ∈ Fn(κ, I, J)"
proof -
  from assms
  obtain d1 d2 where "f : d1 → J" "d1 ∈ Pow(I)" "d1 ≺ κ"
    "g : d2 → J" "d2 ∈ Pow(I)" "d2 ≺ κ"
    by blast
  with assms
  show ?thesis
    using domain_of_fun InfCard_lesspoll_Un[of κ d1 d2]
      restrict_eq_imp_Un_into_Pi[of f d1 "λ_. J" g d2 "λ_. J"]
    by auto
qed
*)

lemma restrict_eq_imp_compat :
  assumes "f ∈ Fn(nat, I, J)" "g ∈ Fn(nat, I, J)" "InfCard(nat)"
    "restrict(f, domain(f) ∩ domain(g)) = restrict(g, domain(f) ∩ domain(g))"
  shows "f ∪ g ∈ Fn(nat, I, J)"
proof -
  from assms
  obtain d1 d2 where "f : d1 → J" "d1 ∈ Pow(I)" "d1 ≺ nat"
    "g : d2 → J" "d2 ∈ Pow(I)" "d2 ≺ nat"
    by blast
  with assms
  show ?thesis
    using domain_of_fun
      restrict_eq_imp_Un_into_Pi[of f d1 "λ_. J" g d2 "λ_. J"]
    by (auto dest!:lesspoll_nat_is_Finite intro!:Finite_imp_lesspoll_nat)
qed

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

(* MOVE THIS to an appropriate place *)
lemma filter_subset_notion : "filter(G) ⟹ G ⊆ Fn(κ, I, J)"
  unfolding filter_def by simp

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 (* cohen_data *)

locale add_reals= cohen_data nat _ 2

end