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"
begin

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"

definition
  is_compat_in :: "[i⇒o,i,i,i,i] ⇒ o" where
  "is_compat_in(M,A,r,p,q) ≡ ∃d[M]. d∈A ∧ (∃dp[M]. pair(M,d,p,dp) ∧ dp∈r ∧ 
                                   (∃dq[M]. pair(M,d,q,dq) ∧ dq∈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

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

definition 
  ccc :: "i ⇒ i ⇒ o" where
  "ccc(P,leq) ≡ ∀A. antichain(P,leq,A) ⟶ |A| ≤ nat"

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

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

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

text‹A set $D$ is ∗‹dense› if every element $p\in P$ has a lower 
bound in $D$.›
definition 
  dense :: "i⇒o" where
  "dense(D) ≡ ∀p∈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. p≼q ⟶ (∃d∈D. d∈P ∧ d≼p)"

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

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

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

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

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


lemma leq_reflI: "p∈P ⟹ p≼p"
  using leq_preord unfolding preorder_on_def refl_def by blast

lemma compatD[dest!]: "compat(p,q) ⟹ ∃d∈P. 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∈P ⟹ d≼p ⟹ d≼q ⟹ compat(p,q)"
  unfolding compat_def compat_in_def by blast

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

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

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

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

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

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

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

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

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

lemma dense_below_dense_below: 
  assumes "dense_below({q∈P. dense_below(D,q)},p)" "p∈P" 
  shows "dense_below(D,p)"  
  using assms leq_transD leq_reflI  by blast
    (* Long proof *)
    (*  unfolding dense_below_def
proof (intro ballI impI)
  fix r
  assume "r∈P" ‹r≼p›
  with assms
  obtain q where "q∈P" "q≼r" "dense_below(D,q)"
    using assms by auto
  moreover from this
  obtain d where "d∈P" "d≼q" "d∈D"
    using assms leq_preord unfolding preorder_on_def refl_def by blast
  moreover
  note ‹r∈P›
  ultimately
  show "∃d∈D. d ∈ P ∧ d≼ r"
    using leq_preord trans_onD unfolding preorder_on_def by blast
qed *)

definition
  antichain :: "i⇒o" where
  "antichain(A) ≡ A⊆P ∧ (∀p∈A.∀q∈A.(¬compat(p,q)))"

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

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

lemma filter_leqD : "filter(G) ⟹ x ∈ G ⟹ y ∈ P ⟹ 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∈P.∃a∈A. a≼p}"

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

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

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

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

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

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

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

lemma  closure_compat_filter:
  assumes "A⊆P" "(∀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∈P" "q∈P"
      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 2:"d≼p" "d≼q" "d∈?UA"
      using A_sub_upclosure[THEN subsetD] ‹A⊆P›
        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 → P ⟹ 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 → P" "preorder_on(P,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 leq_reflI by simp
next
  case (succ x)
  then
  have 1:"f`succ(x) ≼ f`x" "f`n∈P" "f`x∈P" "f`succ(x)∈P"
    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 leq_reflI by simp
  qed
qed

lemma decr_seq_linear: 
  assumes "refl(P,leq)" "f ∈ nat → P"
    "∀n∈nat.  ⟨f ` succ(n), f ` n⟩ ∈ leq"
    "trans[P](leq)"
  shows "linear(f `` nat, leq)"
proof -
  have "preorder_on(P,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(P,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(P,leq)› by simp
    qed
  }
  then
  show ?thesis
    unfolding linear_def using ball_image_simp assms by auto
qed

end (* forcing_notion *)

subsection‹Towards Rasiowa-Sikorski Lemma (RSL)›
locale countable_generic = forcing_notion +
  fixes 𝒟
  assumes countable_subs_of_P:  "𝒟 ∈ nat→Pow(P)"
    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∈P" "f : nat→P" "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  ⊆ P"
    by (simp add:subset_fun_image)
  moreover from calculation
  have "refl(f``nat, leq) ∧ trans[P](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 (* 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 preimage_rangeD:
  assumes "f∈Pi(A,B)" "b ∈ range(f)" 
  shows "∃a∈A. f`a = b"
  using assms apply_equality[OF _ assms(1), of _ b] domain_type[OF _ assms(1)] by auto

lemma countable_RS_sequence_aux:
  fixes p enum
  defines "f(n) ≡ RS_seq(n,P,leq,p,enum,𝒟)"
    and   "Q(q,k,m) ≡ enum`m≼ q ∧ enum`m ∈ 𝒟 ` k"
  assumes "n∈nat" "p∈P" "P ⊆ range(enum)" "enum:nat→M"
    "⋀x k. x∈P ⟹ k∈nat ⟹  ∃q∈P. q≼ x ∧ q ∈ 𝒟 ` k" 
  shows 
    "f(succ(n)) ∈ P ∧ f(succ(n))≼ f(n) ∧ f(succ(n)) ∈ 𝒟 ` n"
  using ‹n∈nat›
proof (induct)
  case 0
  from assms 
  obtain q where "q∈P" "q≼ p" "q ∈ 𝒟 ` 0" by blast
  moreover from this and ‹P ⊆ range(enum)›
  obtain m where "m∈nat" "enum`m = q" 
    using preimage_rangeD[OF ‹enum:nat→M›] by blast
  moreover 
  have "𝒟`0 ⊆ P"
    using apply_funtype[OF countable_subs_of_P] by simp
  moreover note ‹p∈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∈P" "q≼ f(succ(n))" "q ∈ 𝒟 ` succ(n)" by blast
  moreover from this and ‹P ⊆ range(enum)›
  obtain m where "m∈nat" "enum`m≼ f(succ(n))" "enum`m ∈ 𝒟 ` succ(n)"
    using preimage_rangeD[OF ‹enum:nat→M›] by blast
  moreover note succ
  moreover from calculation
  have "𝒟`succ(n) ⊆ P" 
    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,P,leq,p,enum,𝒟)"
    and   "Q(q,k,m) ≡ enum`m≼ q ∧ enum`m ∈ 𝒟 ` k"
  assumes "n∈nat" "p∈P" "P ⊆ range(enum)" "enum:nat→M"
  shows 
    "f`0 = p" "f`succ(n)≼ f`n ∧ f`succ(n) ∈ 𝒟 ` n" "f`succ(n) ∈ P"
proof -
  from assms
  show "f`0 = p" by simp
  {
    fix x k
    assume "x∈P" "k∈nat"
    then
    have "∃q∈P. 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)∈P"
    unfolding f_def using countable_RS_sequence_aux by simp_all
qed

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

lemma RS_seq_funtype:
  assumes "p∈P" "P ⊆ range(enum)" "enum:nat→M"
  shows "(λn∈nat. RS_seq(n,P,leq,p,enum,𝒟)): nat → P"
  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 (* countable_generic *)

end