section‹Transitive set models of ZF›
text‹This theory defines the locale \<^term>‹M_ZF_trans› for
transitive models of ZF, and the associated \<^term>‹forcing_data›
that adds a forcing notion›
theory Forcing_Data
imports
Forcing_Notions
Interface
begin
lemma Transset_M :
"Transset(M) ⟹ y∈x ⟹ x ∈ M ⟹ y ∈ M"
by (simp add: Transset_def,auto)
locale M_ctm = M_ZF_trans +
fixes enum
assumes M_countable: "enum∈bij(nat,M)"
begin
lemma tuples_in_M: "A∈M ⟹ B∈M ⟹ ⟨A,B⟩∈M"
by (simp flip:setclass_iff)
subsection‹\<^term>‹Collects› in $M$›
lemma Collect_in_M_0p :
assumes
Qfm : "Q_fm ∈ formula" and
Qarty : "arity(Q_fm) = 1" and
Qsats : "⋀x. x∈M ⟹ sats(M,Q_fm,[x]) ⟷ is_Q(##M,x)" and
Qabs : "⋀x. x∈M ⟹ is_Q(##M,x) ⟷ Q(x)" and
"A∈M"
shows
"Collect(A,Q)∈M"
proof -
have "z∈A ⟹ z∈M" for z
using ‹A∈M› transitivity by simp
then
have 1:"Collect(A,is_Q(##M)) = Collect(A,Q)"
using Qabs Collect_cong[of "A" "A" "is_Q(##M)" "Q"] by simp
have "separation(##M,is_Q(##M))"
using separation_ax Qsats Qarty Qfm
separation_cong[of "##M" "λy. sats(M,Q_fm,[y])" "is_Q(##M)"]
by simp
then
have "Collect(A,is_Q(##M))∈M"
using separation_closed ‹A∈M› by simp
then
show ?thesis using 1 by simp
qed
lemma Collect_in_M_2p :
assumes
Qfm : "Q_fm ∈ formula" and
Qarty : "arity(Q_fm) = 3" and
params_M : "y∈M" "z∈M" and
Qsats : "⋀x. x∈M ⟹ sats(M,Q_fm,[x,y,z]) ⟷ is_Q(##M,x,y,z)" and
Qabs : "⋀x. x∈M ⟹ is_Q(##M,x,y,z) ⟷ Q(x,y,z)" and
"A∈M"
shows
"Collect(A,λx. Q(x,y,z))∈M"
proof -
have "z∈A ⟹ z∈M" for z
using ‹A∈M› transitivity by simp
then
have 1:"Collect(A,λx. is_Q(##M,x,y,z)) = Collect(A,λx. Q(x,y,z))"
using Qabs Collect_cong[of "A" "A" "λx. is_Q(##M,x,y,z)" "λx. Q(x,y,z)"] by simp
have "separation(##M,λx. is_Q(##M,x,y,z))"
using separation_ax Qsats Qarty Qfm params_M
separation_cong[of "##M" "λx. sats(M,Q_fm,[x,y,z])" "λx. is_Q(##M,x,y,z)"]
by simp
then
have "Collect(A,λx. is_Q(##M,x,y,z))∈M"
using separation_closed ‹A∈M› by simp
then
show ?thesis using 1 by simp
qed
lemma Collect_in_M_4p :
assumes
Qfm : "Q_fm ∈ formula" and
Qarty : "arity(Q_fm) = 5" and
params_M : "a1∈M" "a2∈M" "a3∈M" "a4∈M" and
Qsats : "⋀x. x∈M ⟹ sats(M,Q_fm,[x,a1,a2,a3,a4]) ⟷ is_Q(##M,x,a1,a2,a3,a4)" and
Qabs : "⋀x. x∈M ⟹ is_Q(##M,x,a1,a2,a3,a4) ⟷ Q(x,a1,a2,a3,a4)" and
"A∈M"
shows
"Collect(A,λx. Q(x,a1,a2,a3,a4))∈M"
proof -
have "z∈A ⟹ z∈M" for z
using ‹A∈M› transitivity by simp
then
have 1:"Collect(A,λx. is_Q(##M,x,a1,a2,a3,a4)) = Collect(A,λx. Q(x,a1,a2,a3,a4))"
using Qabs Collect_cong[of "A" "A" "λx. is_Q(##M,x,a1,a2,a3,a4)" "λx. Q(x,a1,a2,a3,a4)"]
by simp
have "separation(##M,λx. is_Q(##M,x,a1,a2,a3,a4))"
using separation_ax Qsats Qarty Qfm params_M
separation_cong[of "##M" "λx. sats(M,Q_fm,[x,a1,a2,a3,a4])"
"λx. is_Q(##M,x,a1,a2,a3,a4)"]
by simp
then
have "Collect(A,λx. is_Q(##M,x,a1,a2,a3,a4))∈M"
using separation_closed ‹A∈M› by simp
then
show ?thesis using 1 by simp
qed
lemma Repl_in_M :
assumes
f_fm: "f_fm ∈ formula" and
f_ar: "arity(f_fm)≤ 2 #+ length(env)" and
fsats: "⋀x y. x∈M ⟹ y∈M ⟹ sats(M,f_fm,[x,y]@env) ⟷ is_f(x,y)" and
fabs: "⋀x y. x∈M ⟹ y∈M ⟹ is_f(x,y) ⟷ y = f(x)" and
fclosed: "⋀x. x∈A ⟹ f(x) ∈ M" and
"A∈M" "env∈list(M)"
shows "{f(x). x∈A}∈M"
proof -
have "strong_replacement(##M, λx y. sats(M,f_fm,[x,y]@env))"
using replacement_ax f_fm f_ar ‹env∈list(M)› by simp
then
have "strong_replacement(##M, λx y. y = f(x))"
using fsats fabs
strong_replacement_cong[of "##M" "λx y. sats(M,f_fm,[x,y]@env)" "λx y. y = f(x)"]
by simp
then
have "{ y . x∈A , y = f(x) } ∈ M"
using ‹A∈M› fclosed strong_replacement_closed by simp
moreover
have "{f(x). x∈A} = { y . x∈A , y = f(x) }"
by auto
ultimately show ?thesis by simp
qed
end
subsection‹A forcing locale and generic filters›
locale forcing_data = forcing_notion + M_ctm +
assumes P_in_M: "P ∈ M"
and leq_in_M: "leq ∈ M"
begin
lemma transD : "Transset(M) ⟹ y ∈ M ⟹ y ⊆ M"
by (unfold Transset_def, blast)
lemmas P_sub_M = transD[OF trans_M P_in_M]
definition
M_generic :: "i⇒o" where
"M_generic(G) ≡ filter(G) ∧ (∀D∈M. D⊆P ∧ dense(D)⟶D∩G≠0)"
lemma M_genericD [dest]: "M_generic(G) ⟹ x∈G ⟹ x∈P"
unfolding M_generic_def by (blast dest:filterD)
lemma M_generic_leqD [dest]: "M_generic(G) ⟹ p∈G ⟹ q∈P ⟹ p≼q ⟹ q∈G"
unfolding M_generic_def by (blast dest:filter_leqD)
lemma M_generic_compatD [dest]: "M_generic(G) ⟹ p∈G ⟹ r∈G ⟹ ∃q∈G. q≼p ∧ q≼r"
unfolding M_generic_def by (blast dest:low_bound_filter)
lemma M_generic_denseD [dest]: "M_generic(G) ⟹ dense(D) ⟹ D⊆P ⟹ D∈M ⟹ ∃q∈G. q∈D"
unfolding M_generic_def by blast
lemma G_nonempty: "M_generic(G) ⟹ G≠0"
proof -
have "P⊆P" ..
assume
"M_generic(G)"
with P_in_M P_dense ‹P⊆P› show
"G ≠ 0"
unfolding M_generic_def by auto
qed
lemma one_in_G :
assumes "M_generic(G)"
shows "one ∈ G"
proof -
from assms have "G⊆P"
unfolding M_generic_def and filter_def by simp
from ‹M_generic(G)› have "increasing(G)"
unfolding M_generic_def and filter_def by simp
with ‹G⊆P› and ‹M_generic(G)›
show ?thesis
using G_nonempty and one_in_P and one_max
unfolding increasing_def by blast
qed
lemma G_subset_M: "M_generic(G) ⟹ G ⊆ M"
using transitivity[OF _ P_in_M] by auto
declare iff_trans [trans]
lemma generic_filter_existence:
"p∈P ⟹ ∃G. p∈G ∧ M_generic(G)"
proof -
assume "p∈P"
let ?D="λn∈nat. (if (enum`n⊆P ∧ dense(enum`n)) then enum`n else P)"
have "∀n∈nat. ?D`n ∈ Pow(P)"
by auto
then
have "?D:nat→Pow(P)"
using lam_type by auto
have Eq4: "∀n∈nat. dense(?D`n)"
proof(intro ballI)
fix n
assume "n∈nat"
then
have "dense(?D`n) ⟷ dense(if enum`n ⊆ P ∧ dense(enum`n) then enum`n else P)"
by simp
also
have "... ⟷ (¬(enum`n ⊆ P ∧ dense(enum`n)) ⟶ dense(P)) "
using split_if by simp
finally
show "dense(?D`n)"
using P_dense ‹n∈nat› by auto
qed
from ‹?D∈_› and Eq4
interpret cg: countable_generic P leq one ?D
by (unfold_locales, auto)
from ‹p∈P›
obtain G where Eq6: "p∈G ∧ filter(G) ∧ (∀n∈nat.(?D`n)∩G≠0)"
using cg.countable_rasiowa_sikorski[where M="λ_. M"] P_sub_M
M_countable[THEN bij_is_fun] M_countable[THEN bij_is_surj, THEN surj_range]
unfolding cg.D_generic_def by blast
then
have Eq7: "(∀D∈M. D⊆P ∧ dense(D)⟶D∩G≠0)"
proof (intro ballI impI)
fix D
assume "D∈M" and Eq9: "D ⊆ P ∧ dense(D) "
have "∀y∈M. ∃x∈nat. enum`x= y"
using M_countable and bij_is_surj unfolding surj_def by (simp)
with ‹D∈M› obtain n where Eq10: "n∈nat ∧ enum`n = D"
by auto
with Eq9 and if_P
have "?D`n = D" by (simp)
with Eq6 and Eq10
show "D∩G≠0" by auto
qed
with Eq6
show ?thesis unfolding M_generic_def by auto
qed
end
lemma (in M_trivial) compat_in_abs :
assumes
"M(A)" "M(r)" "M(p)" "M(q)"
shows
"is_compat_in(M,A,r,p,q) ⟷ compat_in(A,r,p,q)"
using assms unfolding is_compat_in_def compat_in_def by simp
context forcing_data begin
definition
compat_in_fm :: "[i,i,i,i] ⇒ i" where
"compat_in_fm(A,r,p,q) ≡
Exists(And(Member(0,succ(A)),Exists(And(pair_fm(1,p#+2,0),
And(Member(0,r#+2),
Exists(And(pair_fm(2,q#+3,0),Member(0,r#+3))))))))"
lemma compat_in_fm_type[TC] :
"⟦ A∈nat;r∈nat;p∈nat;q∈nat⟧ ⟹ compat_in_fm(A,r,p,q)∈formula"
unfolding compat_in_fm_def by simp
lemma sats_compat_in_fm:
assumes
"A∈nat" "r∈nat" "p∈nat" "q∈nat" "env∈list(M)"
shows
"sats(M,compat_in_fm(A,r,p,q),env) ⟷
is_compat_in(##M,nth(A, env),nth(r, env),nth(p, env),nth(q, env))"
unfolding compat_in_fm_def is_compat_in_def using assms by simp
end
end