# 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)"

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

lemma subset_fun_image: "f:N→P ⟹ fN⊆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"

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

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

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

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 ⟹ fn ∈ 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:"fsucc(x) ≼ fx" "fn∈ℙ" "fx∈ℙ" "fsucc(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 "fm ≼ fn ∨ fn ≼ fm"
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 "fnat  ⊆ ℙ"
moreover from calculation
have "refl(fnat, 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(fnat, leq)"
using leq_preord and decr_seq_linear unfolding preorder_on_def by (blast)
moreover from calculation
have "(∀p∈fnat.∀q∈fnat. compat_in(fnat,leq,p,q))"
using chain_compat by (auto)
ultimately
have "filter(upclosure(fnat))" (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 "fsucc(n) ∈ ?G ∧ fsucc(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. ⟨enumm, RS_seq(n,P,leq,p,enum,𝒟)⟩ ∈ leq ∧ enumm ∈ 𝒟  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) ≡ enumm≼ q ∧ enumm ∈ 𝒟  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" "enumm = 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" "enumm≼ f(succ(n))" "enumm ∈ 𝒟  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) ≡ enumm≼ q ∧ enumm ∈ 𝒟  k"
assumes "n∈nat" "p∈ℙ" "ℙ ⊆ range(enum)" "enum:nat→M"
shows
"f0 = p" "fsucc(n)≼ fn ∧ fsucc(n) ∈ 𝒟  n" "fsucc(n) ∈ ℙ"
proof -
from assms
show "f0 = 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 "fsucc(n)≼ fn ∧ fsucc(n) ∈ 𝒟  n" "fsucc(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
`