Theory Forcing_Notions

section‹Forcing notions›
text‹This theory defines a locale for forcing notions, that is,
 preorders with a distinguished maximum element.›

theory Forcing_Notions
  imports
    "ZF-Constructible.Relative"
    "Delta_System_Lemma.ZF_Library"
begin

hide_const (open) Order.pred

subsection‹Basic concepts›
text‹We say that two elements $p,q$ are
  ∗‹compatible› if they have a lower bound in $P$›
definition compat_in :: "i⇒i⇒i⇒i⇒o" where
  "compat_in(A,r,p,q) ≡ ∃d∈A . ⟨d,p⟩∈r ∧ ⟨d,q⟩∈r"

lemma compat_inI :
  "⟦ d∈A ; ⟨d,p⟩∈r ; ⟨d,g⟩∈r ⟧ ⟹ compat_in(A,r,p,g)"
  by (auto simp add: compat_in_def)

lemma refl_compat:
  "⟦ refl(A,r) ; ⟨p,q⟩ ∈ r | p=q | ⟨q,p⟩ ∈ r ; p∈A ; q∈A⟧ ⟹ compat_in(A,r,p,q)"
  by (auto simp add: refl_def compat_inI)

lemma  chain_compat:
  "refl(A,r) ⟹ linear(A,r) ⟹  (∀p∈A.∀q∈A. compat_in(A,r,p,q))"
  by (simp add: refl_compat linear_def)

lemma subset_fun_image: "f:N→P ⟹ f``N⊆P"
  by (auto simp add: image_fun apply_funtype)

lemma refl_monot_domain: "refl(B,r) ⟹ A⊆B ⟹ refl(A,r)"
  unfolding refl_def by blast

locale forcing_notion =
  fixes P (‹ℙ›) and leq and one (‹𝟭›)
  assumes one_in_P:       "𝟭 ∈ ℙ"
    and leq_preord:       "preorder_on(ℙ,leq)"
    and one_max:          "∀p∈ℙ. ⟨p,𝟭⟩∈leq"
begin

abbreviation Leq :: "[i, i] ⇒ o"  (infixl ‹≼› 50)
  where "x ≼ y ≡ ⟨x,y⟩∈leq"

lemma refl_leq:
  "r∈ℙ ⟹ r≼r"
  using leq_preord unfolding preorder_on_def refl_def by simp

text‹A set $D$ is ∗‹dense› if every element $p\in \mathbb{P}$ has a lower
bound in $D$.›
definition
  dense :: "i⇒o" where
  "dense(D) ≡ ∀p∈ℙ. ∃d∈D . d≼p"

text‹There is also a weaker definition which asks for
a lower bound in $D$ only for the elements below some fixed
element $q$.›
definition
  dense_below :: "i⇒i⇒o" where
  "dense_below(D,q) ≡ ∀p∈ℙ. p≼q ⟶ (∃d∈D. d∈ℙ ∧ d≼p)"

lemma P_dense: "dense(ℙ)"
  by (insert leq_preord, auto simp add: preorder_on_def refl_def dense_def)

definition
  increasing :: "i⇒o" where
  "increasing(F) ≡ ∀x∈F. ∀ p ∈ ℙ . x≼p ⟶ p∈F"

definition
  compat :: "i⇒i⇒o" where
  "compat(p,q) ≡ compat_in(ℙ,leq,p,q)"

lemma leq_transD:  "a≼b ⟹ b≼c ⟹ a ∈ ℙ⟹ b ∈ ℙ⟹ c ∈ ℙ⟹ a≼c"
  using leq_preord trans_onD unfolding preorder_on_def by blast

lemma leq_transD':  "A⊆ℙ ⟹ a≼b ⟹ b≼c ⟹ a ∈ A ⟹ b ∈ ℙ⟹ c ∈ ℙ⟹ a≼c"
  using leq_preord trans_onD subsetD unfolding preorder_on_def by blast

lemma compatD[dest!]: "compat(p,q) ⟹ ∃d∈ℙ. d≼p ∧ d≼q"
  unfolding compat_def compat_in_def .

abbreviation Incompatible :: "[i, i] ⇒ o"  (infixl ‹⊥› 50)
  where "p ⊥ q ≡ ¬ compat(p,q)"

lemma compatI[intro!]: "d∈ℙ ⟹ d≼p ⟹ d≼q ⟹ compat(p,q)"
  unfolding compat_def compat_in_def by blast

lemma Incompatible_imp_not_eq: "⟦ p ⊥ q; p∈ℙ; q∈ℙ ⟧⟹ p ≠ q"
  using refl_leq by blast

lemma denseD [dest]: "dense(D) ⟹ p∈ℙ ⟹  ∃d∈D. d≼ p"
  unfolding dense_def by blast

lemma denseI [intro!]: "⟦ ⋀p. p∈ℙ ⟹ ∃d∈D. d≼ p ⟧ ⟹ dense(D)"
  unfolding dense_def by blast

lemma dense_belowD [dest]:
  assumes "dense_below(D,p)" "q∈ℙ" "q≼p"
  shows "∃d∈D. d∈ℙ ∧ d≼q"
  using assms unfolding dense_below_def by simp

lemma dense_belowI [intro!]:
  assumes "⋀q. q∈ℙ ⟹ q≼p ⟹ ∃d∈D. d∈ℙ ∧ d≼q"
  shows "dense_below(D,p)"
  using assms unfolding dense_below_def by simp

lemma dense_below_cong: "p∈ℙ ⟹ D = D' ⟹ dense_below(D,p) ⟷ dense_below(D',p)"
  by blast

lemma dense_below_cong': "p∈ℙ ⟹ ⟦⋀x. x∈ℙ ⟹ Q(x) ⟷ Q'(x)⟧ ⟹
           dense_below({q∈ℙ. Q(q)},p) ⟷ dense_below({q∈ℙ. Q'(q)},p)"
  by blast

lemma dense_below_mono: "p∈ℙ ⟹ D ⊆ D' ⟹ dense_below(D,p) ⟹ dense_below(D',p)"
  by blast

lemma dense_below_under:
  assumes "dense_below(D,p)" "p∈ℙ" "q∈ℙ" "q≼p"
  shows "dense_below(D,q)"
  using assms leq_transD by blast

lemma ideal_dense_below:
  assumes "⋀q. q∈ℙ ⟹ q≼p ⟹ q∈D"
  shows "dense_below(D,p)"
  using assms refl_leq by blast

lemma dense_below_dense_below:
  assumes "dense_below({q∈ℙ. dense_below(D,q)},p)" "p∈ℙ"
  shows "dense_below(D,p)"
  using assms leq_transD refl_leq  by blast

text‹A filter is an increasing set $G$ with all its elements
being compatible in $G$.›
definition
  filter :: "i⇒o" where
  "filter(G) ≡ G⊆ℙ ∧ increasing(G) ∧ (∀p∈G. ∀q∈G. compat_in(G,leq,p,q))"

lemma filterD : "filter(G) ⟹ x ∈ G ⟹ x ∈ ℙ"
  by (auto simp add : subsetD filter_def)

lemma filter_subset_notion[dest]: "filter(G) ⟹ G ⊆ ℙ"
  by (auto dest:filterD)

lemma filter_leqD : "filter(G) ⟹ x ∈ G ⟹ y ∈ ℙ ⟹ x≼y ⟹ y ∈ G"
  by (simp add: filter_def increasing_def)

lemma filter_imp_compat: "filter(G) ⟹ p∈G ⟹ q∈G ⟹ compat(p,q)"
  unfolding filter_def compat_in_def compat_def by blast

lemma low_bound_filter: ― ‹says the compatibility is attained inside G›
  assumes "filter(G)" and "p∈G" and "q∈G"
  shows "∃r∈G. r≼p ∧ r≼q"
  using assms
  unfolding compat_in_def filter_def by blast

text‹We finally introduce the upward closure of a set
and prove that the closure of $A$ is a filter if its elements are
compatible in $A$.›
definition
  upclosure :: "i⇒i" where
  "upclosure(A) ≡ {p∈ℙ.∃a∈A. a≼p}"

lemma  upclosureI [intro] : "p∈ℙ ⟹ a∈A ⟹ a≼p ⟹ p∈upclosure(A)"
  by (simp add:upclosure_def, auto)

lemma  upclosureE [elim] :
  "p∈upclosure(A) ⟹ (⋀x a. x∈ℙ ⟹ a∈A ⟹ a≼x ⟹ R) ⟹ R"
  by (auto simp add:upclosure_def)

lemma  upclosureD [dest] :
  "p∈upclosure(A) ⟹ ∃a∈A.(a≼p) ∧ p∈ℙ"
  by (simp add:upclosure_def)

lemma upclosure_increasing :
  assumes "A⊆ℙ"
  shows "increasing(upclosure(A))"
  unfolding increasing_def upclosure_def
  using leq_transD'[OF ‹A⊆ℙ›] by auto

lemma  upclosure_in_P: "A ⊆ ℙ ⟹ upclosure(A) ⊆ ℙ"
  using subsetI upclosure_def by simp

lemma  A_sub_upclosure: "A ⊆ ℙ ⟹ A⊆upclosure(A)"
  using subsetI leq_preord
  unfolding upclosure_def preorder_on_def refl_def by auto

lemma  elem_upclosure: "A⊆ℙ ⟹ x∈A  ⟹ x∈upclosure(A)"
  by (blast dest:A_sub_upclosure)

lemma  closure_compat_filter:
  assumes "A⊆ℙ" "(∀p∈A.∀q∈A. compat_in(A,leq,p,q))"
  shows "filter(upclosure(A))"
  unfolding filter_def
proof(auto)
  show "increasing(upclosure(A))"
    using assms upclosure_increasing by simp
next
  let ?UA="upclosure(A)"
  show "compat_in(upclosure(A), leq, p, q)" if "p∈?UA" "q∈?UA" for p q
  proof -
    from that
    obtain a b where 1:"a∈A" "b∈A" "a≼p" "b≼q" "p∈ℙ" "q∈ℙ"
      using upclosureD[OF ‹p∈?UA›] upclosureD[OF ‹q∈?UA›] by auto
    with assms(2)
    obtain d where "d∈A" "d≼a" "d≼b"
      unfolding compat_in_def by auto
    with 1
    have "d≼p" "d≼q" "d∈?UA"
      using A_sub_upclosure[THEN subsetD] ‹A⊆ℙ›
        leq_transD'[of A d a] leq_transD'[of A d b] by auto
    then
    show ?thesis unfolding compat_in_def by auto
  qed
qed

lemma  aux_RS1:  "f ∈ N → ℙ ⟹ n∈N ⟹ f`n ∈ upclosure(f ``N)"
  using elem_upclosure[OF subset_fun_image] image_fun
  by (simp, blast)

lemma decr_succ_decr:
  assumes "f ∈ nat → ℙ" "preorder_on(ℙ,leq)"
    "∀n∈nat.  ⟨f ` succ(n), f ` n⟩ ∈ leq"
    "m∈nat"
  shows "n∈nat ⟹ n≤m ⟹ ⟨f ` m, f ` n⟩ ∈ leq"
  using ‹m∈_›
proof(induct m)
  case 0
  then show ?case using assms refl_leq by simp
next
  case (succ x)
  then
  have 1:"f`succ(x) ≼ f`x" "f`n∈ℙ" "f`x∈ℙ" "f`succ(x)∈ℙ"
    using assms by simp_all
  consider (lt) "n<succ(x)" | (eq) "n=succ(x)"
    using succ le_succ_iff by auto
  then
  show ?case
  proof(cases)
    case lt
    with 1 show ?thesis using leI succ leq_transD by auto
  next
    case eq
    with 1 show ?thesis using refl_leq by simp
  qed
qed

lemma decr_seq_linear:
  assumes "refl(ℙ,leq)" "f ∈ nat → ℙ"
    "∀n∈nat.  ⟨f ` succ(n), f ` n⟩ ∈ leq"
    "trans[ℙ](leq)"
  shows "linear(f `` nat, leq)"
proof -
  have "preorder_on(ℙ,leq)"
    unfolding preorder_on_def using assms by simp
  {
    fix n m
    assume "n∈nat" "m∈nat"
    then
    have "f`m ≼ f`n ∨ f`n ≼ f`m"
    proof(cases "m≤n")
      case True
      with ‹n∈_› ‹m∈_›
      show ?thesis
        using decr_succ_decr[of f n m] assms leI ‹preorder_on(ℙ,leq)› by simp
    next
      case False
      with ‹n∈_› ‹m∈_›
      show ?thesis
        using decr_succ_decr[of f m n] assms leI not_le_iff_lt ‹preorder_on(ℙ,leq)› by simp
    qed
  }
  then
  show ?thesis
    unfolding linear_def using ball_image_simp assms by auto
qed

end ― ‹\<^locale>‹forcing_notion››

subsection‹Towards Rasiowa-Sikorski Lemma (RSL)›
locale countable_generic = forcing_notion +
  fixes 𝒟
  assumes countable_subs_of_P:  "𝒟 ∈ nat→Pow(ℙ)"
    and     seq_of_denses:        "∀n ∈ nat. dense(𝒟`n)"

begin

definition
  D_generic :: "i⇒o" where
  "D_generic(G) ≡ filter(G) ∧ (∀n∈nat.(𝒟`n)∩G≠0)"

text‹The next lemma identifies a sufficient condition for obtaining
RSL.›
lemma RS_sequence_imp_rasiowa_sikorski:
  assumes
    "p∈ℙ" "f : nat→ℙ" "f ` 0 = p"
    "⋀n. n∈nat ⟹ f ` succ(n)≼ f ` n ∧ f ` succ(n) ∈ 𝒟 ` n"
  shows
    "∃G. p∈G ∧ D_generic(G)"
proof -
  note assms
  moreover from this
  have "f``nat  ⊆ ℙ"
    by (simp add:subset_fun_image)
  moreover from calculation
  have "refl(f``nat, leq) ∧ trans[ℙ](leq)"
    using leq_preord unfolding preorder_on_def by (blast intro:refl_monot_domain)
  moreover from calculation
  have "∀n∈nat.  f ` succ(n)≼ f ` n" by (simp)
  moreover from calculation
  have "linear(f``nat, leq)"
    using leq_preord and decr_seq_linear unfolding preorder_on_def by (blast)
  moreover from calculation
  have "(∀p∈f``nat.∀q∈f``nat. compat_in(f``nat,leq,p,q))"
    using chain_compat by (auto)
  ultimately
  have "filter(upclosure(f``nat))" (is "filter(?G)")
    using closure_compat_filter by simp
  moreover
  have "∀n∈nat. 𝒟 ` n ∩ ?G ≠ 0"
  proof
    fix n
    assume "n∈nat"
    with assms
    have "f`succ(n) ∈ ?G ∧ f`succ(n) ∈ 𝒟 ` n"
      using aux_RS1 by simp
    then
    show "𝒟 ` n ∩ ?G ≠ 0"  by blast
  qed
  moreover from assms
  have "p ∈ ?G"
    using aux_RS1 by auto
  ultimately
  show ?thesis unfolding D_generic_def by auto
qed

end ― ‹\<^locale>‹countable_generic››

text‹Now, the following recursive definition will fulfill the
requirements of lemma \<^term>‹RS_sequence_imp_rasiowa_sikorski› ›

consts RS_seq :: "[i,i,i,i,i,i] ⇒ i"
primrec
  "RS_seq(0,P,leq,p,enum,𝒟) = p"
  "RS_seq(succ(n),P,leq,p,enum,𝒟) =
    enum`(μ m. ⟨enum`m, RS_seq(n,P,leq,p,enum,𝒟)⟩ ∈ leq ∧ enum`m ∈ 𝒟 ` n)"

context countable_generic
begin

lemma countable_RS_sequence_aux:
  fixes p enum
  defines "f(n) ≡ RS_seq(n,ℙ,leq,p,enum,𝒟)"
    and   "Q(q,k,m) ≡ enum`m≼ q ∧ enum`m ∈ 𝒟 ` k"
  assumes "n∈nat" "p∈ℙ" "ℙ ⊆ range(enum)" "enum:nat→M"
    "⋀x k. x∈ℙ ⟹ k∈nat ⟹  ∃q∈ℙ. q≼ x ∧ q ∈ 𝒟 ` k"
  shows
    "f(succ(n)) ∈ ℙ ∧ f(succ(n))≼ f(n) ∧ f(succ(n)) ∈ 𝒟 ` n"
  using ‹n∈nat›
proof (induct)
  case 0
  from assms
  obtain q where "q∈ℙ" "q≼ p" "q ∈ 𝒟 ` 0" by blast
  moreover from this and ‹ℙ ⊆ range(enum)›
  obtain m where "m∈nat" "enum`m = q"
    using Pi_rangeD[OF ‹enum:nat→M›] by blast
  moreover
  have "𝒟`0 ⊆ ℙ"
    using apply_funtype[OF countable_subs_of_P] by simp
  moreover note ‹p∈ℙ›
  ultimately
  show ?case
    using LeastI[of "Q(p,0)" m] unfolding Q_def f_def by auto
next
  case (succ n)
  with assms
  obtain q where "q∈ℙ" "q≼ f(succ(n))" "q ∈ 𝒟 ` succ(n)" by blast
  moreover from this and ‹ℙ ⊆ range(enum)›
  obtain m where "m∈nat" "enum`m≼ f(succ(n))" "enum`m ∈ 𝒟 ` succ(n)"
    using Pi_rangeD[OF ‹enum:nat→M›] by blast
  moreover note succ
  moreover from calculation
  have "𝒟`succ(n) ⊆ ℙ"
    using apply_funtype[OF countable_subs_of_P] by auto
  ultimately
  show ?case
    using LeastI[of "Q(f(succ(n)),succ(n))" m] unfolding Q_def f_def by auto
qed

lemma countable_RS_sequence:
  fixes p enum
  defines "f ≡ λn∈nat. RS_seq(n,ℙ,leq,p,enum,𝒟)"
    and   "Q(q,k,m) ≡ enum`m≼ q ∧ enum`m ∈ 𝒟 ` k"
  assumes "n∈nat" "p∈ℙ" "ℙ ⊆ range(enum)" "enum:nat→M"
  shows
    "f`0 = p" "f`succ(n)≼ f`n ∧ f`succ(n) ∈ 𝒟 ` n" "f`succ(n) ∈ ℙ"
proof -
  from assms
  show "f`0 = p" by simp
  {
    fix x k
    assume "x∈ℙ" "k∈nat"
    then
    have "∃q∈ℙ. q≼ x ∧ q ∈ 𝒟 ` k"
      using seq_of_denses apply_funtype[OF countable_subs_of_P]
      unfolding dense_def by blast
  }
  with assms
  show "f`succ(n)≼ f`n ∧ f`succ(n) ∈ 𝒟 ` n" "f`succ(n)∈ℙ"
    unfolding f_def using countable_RS_sequence_aux by simp_all
qed

lemma RS_seq_type:
  assumes "n ∈ nat" "p∈ℙ" "ℙ ⊆ range(enum)" "enum:nat→M"
  shows "RS_seq(n,ℙ,leq,p,enum,𝒟) ∈ ℙ"
  using assms countable_RS_sequence(1,3)
  by (induct;simp)

lemma RS_seq_funtype:
  assumes "p∈ℙ" "ℙ ⊆ range(enum)" "enum:nat→M"
  shows "(λn∈nat. RS_seq(n,ℙ,leq,p,enum,𝒟)): nat → ℙ"
  using assms lam_type RS_seq_type by auto

lemmas countable_rasiowa_sikorski =
  RS_sequence_imp_rasiowa_sikorski[OF _ RS_seq_funtype countable_RS_sequence(1,2)]

end ― ‹\<^locale>‹countable_generic››

end