Theory Succession_Poset
section‹A poset of successions›
theory Succession_Poset
imports
ZF_Trans_Interpretations
Proper_Extension
begin
text‹In this theory we define a separative poset. Its underlying set is the
set of finite binary sequences (that is, with codomain $2={0,1}$);
of course, one can see that set as
the set \<^term>‹ω-||>2› or equivalently as the set of partial functions
\<^term>‹Fn(ω,ω,2)›, i.e. the set of partial functions bounded by \<^term>‹ω›.
The order relation of the poset is that of being less defined as functions
(cf. \<^term>‹Fnlerel(A⇗<ω⇖)›), so it could be surprising that we have not used
\<^term>‹Fn(ω,ω,2)› for the set. The only reason why we keep this alternative
definition is because we can prove \<^term>‹A⇗<ω⇖ ∈ M› (and therefore
\<^term>‹Fnlerel(A⇗<ω⇖) ∈ M›) using only one instance of separation.›
definition seq_upd :: "i ⇒ i ⇒ i" where
"seq_upd(f,a) ≡ λ j ∈ succ(domain(f)) . if j < domain(f) then f`j else a"
lemma seq_upd_succ_type :
assumes "n∈nat" "f∈n→A" "a∈A"
shows "seq_upd(f,a)∈ succ(n) → A"
proof -
from assms
have equ: "domain(f) = n"
using domain_of_fun by simp
{
fix j
assume "j∈succ(domain(f))"
with equ ‹n∈_›
have "j≤n"
using ltI by auto
with ‹n∈_›
consider (lt) "j<n" | (eq) "j=n"
using leD by auto
then
have "(if j < n then f`j else a) ∈ A"
proof cases
case lt
with ‹f∈_›
show ?thesis
using apply_type ltD[OF lt] by simp
next
case eq
with ‹a∈_›
show ?thesis
by auto
qed
}
with equ
show ?thesis
unfolding seq_upd_def
using lam_type[of "succ(domain(f))"]
by auto
qed
lemma seq_upd_type :
assumes "f∈A⇗<ω⇖" "a∈A"
shows "seq_upd(f,a) ∈ A⇗<ω⇖"
proof -
from ‹f∈_›
obtain y where "y∈nat" "f∈y→A"
unfolding seqspace_def by blast
with ‹a∈A›
have "seq_upd(f,a)∈succ(y)→A"
using seq_upd_succ_type by simp
with ‹y∈_›
show ?thesis
unfolding seqspace_def by auto
qed
lemma seq_upd_apply_domain [simp]:
assumes "f:n→A" "n∈nat"
shows "seq_upd(f,a)`n = a"
unfolding seq_upd_def using assms domain_of_fun by auto
lemma zero_in_seqspace :
shows "0 ∈ A⇗<ω⇖"
unfolding seqspace_def
by force
definition
seqlerel :: "i ⇒ i" where
"seqlerel(A) ≡ Fnlerel(A⇗<ω⇖)"
definition
seqle :: "i" where
"seqle ≡ seqlerel(2)"
lemma seqleI[intro!]:
"⟨f,g⟩ ∈ 2⇗<ω⇖×2⇗<ω⇖ ⟹ g ⊆ f ⟹ ⟨f,g⟩ ∈ seqle"
unfolding seqle_def seqlerel_def seqspace_def Rrel_def Fnlerel_def
by blast
lemma seqleD[dest!]:
"z ∈ seqle ⟹ ∃x y. ⟨x,y⟩ ∈ 2⇗<ω⇖×2⇗<ω⇖ ∧ y ⊆ x ∧ z = ⟨x,y⟩"
unfolding Rrel_def seqle_def seqlerel_def Fnlerel_def
by blast
lemma upd_leI :
assumes "f∈2⇗<ω⇖" "a∈2"
shows "⟨seq_upd(f,a),f⟩∈seqle" (is "⟨?f,_⟩∈_")
proof
show " ⟨?f, f⟩ ∈ 2⇗<ω⇖ × 2⇗<ω⇖"
using assms seq_upd_type by auto
next
show "f ⊆ seq_upd(f,a)"
proof
fix x
assume "x ∈ f"
moreover from ‹f ∈ 2⇗<ω⇖›
obtain n where "n∈nat" "f : n → 2"
by blast
moreover from calculation
obtain y where "y∈n" "x=⟨y,f`y⟩"
using Pi_memberD[of f n "λ_ . 2"]
by blast
moreover from ‹f:n→2›
have "domain(f) = n"
using domain_of_fun by simp
ultimately
show "x ∈ seq_upd(f,a)"
unfolding seq_upd_def lam_def
by (auto intro:ltI)
qed
qed
lemma preorder_on_seqle: "preorder_on(2⇗<ω⇖,seqle)"
unfolding preorder_on_def refl_def trans_on_def by blast
lemma zero_seqle_max: "x∈2⇗<ω⇖ ⟹ ⟨x,0⟩ ∈ seqle"
using zero_in_seqspace
by auto
interpretation sp:forcing_notion "2⇗<ω⇖" "seqle" "0"
using preorder_on_seqle zero_seqle_max zero_in_seqspace
by unfold_locales simp_all
notation sp.Leq (infixl "≼s" 50)
notation sp.Incompatible (infixl "⊥s" 50)
lemma seqspace_separative:
assumes "f∈2⇗<ω⇖"
shows "seq_upd(f,0) ⊥s seq_upd(f,1)" (is "?f ⊥s ?g")
proof
assume "sp.compat(?f, ?g)"
then
obtain h where "h ∈ 2⇗<ω⇖" "?f ⊆ h" "?g ⊆ h"
by blast
moreover from ‹f∈_›
obtain y where "y∈nat" "f:y→2"
by blast
moreover from this
have "?f: succ(y) → 2" "?g: succ(y) → 2"
using seq_upd_succ_type by blast+
moreover from this
have "⟨y,?f`y⟩ ∈ ?f" "⟨y,?g`y⟩ ∈ ?g"
using apply_Pair by auto
ultimately
have "⟨y,0⟩ ∈ h" "⟨y,1⟩ ∈ h"
by auto
moreover from ‹h ∈ 2⇗<ω⇖›
obtain n where "n∈nat" "h:n→2"
by blast
ultimately
show "False"
using fun_is_function[of h n "λ_. 2"]
unfolding seqspace_def function_def by auto
qed
definition seqleR_fm :: "i ⇒ i" where
"seqleR_fm(fg) ≡ Exists(Exists(And(pair_fm(0,1,fg+⇩ω2),subset_fm(1,0))))"
lemma type_seqleR_fm : "fg ∈ nat ⟹ seqleR_fm(fg) ∈ formula"
unfolding seqleR_fm_def
by simp
arity_theorem for "seqleR_fm"
lemma (in M_ctm1) seqleR_fm_sats :
assumes "fg∈nat" "env∈list(M)"
shows "(M, env ⊨ seqleR_fm(fg)) ⟷ (∃f[##M]. ∃g[##M]. pair(##M,f,g,nth(fg,env)) ∧ f ⊇ g)"
unfolding seqleR_fm_def
using assms trans_M sats_subset_fm pair_iff_sats
by auto
context M_ctm1
begin
lemma seqle_in_M: "seqle ∈ M"
using arity_seqleR_fm seqleR_fm_sats type_seqleR_fm
cartprod_closed seqspace_closed nat_into_M nat_in_M pair_in_M_iff
unfolding seqle_def seqlerel_def Rrel_def Fnlerel_def
by (rule_tac Collect_in_M[of "seqleR_fm(0)" "[]"],auto)
subsection‹Cohen extension is proper›
interpretation ctm_separative "2⇗<ω⇖" seqle 0
proof (unfold_locales)
fix f
let ?q="seq_upd(f,0)" and ?r="seq_upd(f,1)"
assume "f ∈ 2⇗<ω⇖"
then
have "?q ≼s f ∧ ?r ≼s f ∧ ?q ⊥s ?r"
using upd_leI seqspace_separative by auto
moreover from calculation
have "?q ∈ 2⇗<ω⇖" "?r ∈ 2⇗<ω⇖"
using seq_upd_type[of f 2] by auto
ultimately
show "∃q∈2⇗<ω⇖. ∃r∈2⇗<ω⇖. q ≼s f ∧ r ≼s f ∧ q ⊥s r"
by (rule_tac bexI)+
next
show "2⇗<ω⇖ ∈ M"
using nat_into_M seqspace_closed by simp
next
show "seqle ∈ M"
using seqle_in_M .
qed
lemma cohen_extension_is_proper: "∃G. M_generic(G) ∧ M ≠ M[G]"
using proper_extension generic_filter_existence zero_in_seqspace
by force
end
end