Theory Forcing_Notions

sectionForcing notions
textThis 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

subsectionBasic concepts
textWe say that two elements $p,q$ are
  compatible if they have a lower bound in $P$
definition compat_in :: "iiiio" where
  "compat_in(A,r,p,q)  dA . d,pr  d,qr"

lemma compat_inI :
  " dA ; d,pr ; d,gr   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 ; pA ; qA  compat_in(A,r,p,q)"
  by (auto simp add: refl_def compat_inI)

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

lemma subset_fun_image: "f:NP  f``NP"
  by (auto simp add: image_fun apply_funtype)

lemma refl_monot_domain: "refl(B,r)  AB  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,yleq"

lemma refl_leq:
  "r  rr"
  using leq_preord unfolding preorder_on_def refl_def by simp

textA set $D$ is dense if every element $p\in \mathbb{P}$ has a lower
bound in $D$.
definition
  dense :: "io" where
  "dense(D)  p. dD . dp"

textThere 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 :: "iio" where
  "dense_below(D,q)  p. pq  (dD. d  dp)"

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

definition
  increasing :: "io" where
  "increasing(F)  xF.  p   . xp  pF"

definition
  compat :: "iio" where
  "compat(p,q)  compat_in(,leq,p,q)"

lemma leq_transD:  "ab  bc  a   b   c   ac"
  using leq_preord trans_onD unfolding preorder_on_def by blast

lemma leq_transD':  "A  ab  bc  a  A  b   c   ac"
  using leq_preord trans_onD subsetD unfolding preorder_on_def by blast

lemma compatD[dest!]: "compat(p,q)  d. dp  dq"
  unfolding compat_def compat_in_def .

abbreviation Incompatible :: "[i, i]  o"  (infixl "" 50)
  where "p  q  ¬ compat(p,q)"

lemma compatI[intro!]: "d  dp  dq  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   dD. d p"
  unfolding dense_def by blast

lemma denseI [intro!]: " p. p  dD. d p   dense(D)"
  unfolding dense_def by blast

lemma dense_belowD [dest]:
  assumes "dense_below(D,p)" "q" "qp"
  shows "dD. d  dq"
  using assms unfolding dense_below_def by simp

lemma dense_belowI [intro!]:
  assumes "q. q  qp  dD. d  dq"
  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" "qp"
  shows "dense_below(D,q)"
  using assms leq_transD by blast

lemma ideal_dense_below:
  assumes "q. q  qp  qD"
  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

textA filter is an increasing set $G$ with all its elements
being compatible in $G$.
definition
  filter :: "io" where
  "filter(G)  G  increasing(G)  (pG. qG. 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    xy  y  G"
  by (simp add: filter_def increasing_def)

lemma filter_imp_compat: "filter(G)  pG  qG  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 "pG" and "qG"
  shows "rG. rp  rq"
  using assms
  unfolding compat_in_def filter_def by blast

textWe 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 :: "ii" where
  "upclosure(A)  {p.aA. ap}"

lemma  upclosureI [intro] : "p  aA  ap  pupclosure(A)"
  by (simp add:upclosure_def, auto)

lemma  upclosureE [elim] :
  "pupclosure(A)  (x a. x  aA  ax  R)  R"
  by (auto simp add:upclosure_def)

lemma  upclosureD [dest] :
  "pupclosure(A)  aA.(ap)  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    Aupclosure(A)"
  using subsetI leq_preord
  unfolding upclosure_def preorder_on_def refl_def by auto

lemma  elem_upclosure: "A  xA   xupclosure(A)"
  by (blast dest:A_sub_upclosure)

lemma  closure_compat_filter:
  assumes "A" "(pA.qA. 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:"aA" "bA" "ap" "bq" "p" "q"
      using upclosureD[OF p?UA] upclosureD[OF q?UA] by auto
    with assms(2)
    obtain d where "dA" "da" "db"
      unfolding compat_in_def by auto
    with 1
    have "dp" "dq" "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    nN  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)"
    "nnat.  f ` succ(n), f ` n  leq"
    "mnat"
  shows "nnat  nm  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  "
    "nnat.  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 "nnat" "mnat"
    then
    have "f`m  f`n  f`n  f`m"
    proof(cases "mn")
      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 ― ‹localeforcing_notion

subsectionTowards Rasiowa-Sikorski Lemma (RSL)
locale countable_generic = forcing_notion +
  fixes 𝒟
  assumes countable_subs_of_P:  "𝒟  natPow()"
    and     seq_of_denses:        "n  nat. dense(𝒟`n)"

begin

definition
  D_generic :: "io" where
  "D_generic(G)  filter(G)  (nnat.(𝒟`n)G0)"

textThe next lemma identifies a sufficient condition for obtaining
RSL.
lemma RS_sequence_imp_rasiowa_sikorski:
  assumes
    "p" "f : nat" "f ` 0 = p"
    "n. nnat  f ` succ(n) f ` n  f ` succ(n)  𝒟 ` n"
  shows
    "G. pG  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 "nnat.  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 "(pf``nat.qf``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 "nnat. 𝒟 ` n  ?G  0"
  proof
    fix n
    assume "nnat"
    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 ― ‹localecountable_generic

textNow, the following recursive definition will fulfill the
requirements of lemma termRS_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 "nnat" "p" "  range(enum)" "enum:natM"
    "x k. x  knat   q. q x  q  𝒟 ` k"
  shows
    "f(succ(n))    f(succ(n)) f(n)  f(succ(n))  𝒟 ` n"
  using nnat
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 "mnat" "enum`m = q"
    using Pi_rangeD[OF enum:natM] 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 "mnat" "enum`m f(succ(n))" "enum`m  𝒟 ` succ(n)"
    using Pi_rangeD[OF enum:natM] 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  λnnat. RS_seq(n,,leq,p,enum,𝒟)"
    and   "Q(q,k,m)  enum`m q  enum`m  𝒟 ` k"
  assumes "nnat" "p" "  range(enum)" "enum:natM"
  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" "knat"
    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:natM"
  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:natM"
  shows "(λnnat. 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 ― ‹localecountable_generic

end