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
"ZF-Constructible-Trans.Relative"
"ZF-Constructible-Trans.Formula"
Interface
begin
lemma Transset_M :
"Transset(M) ⟹ y∈x ⟹ x ∈ M ⟹ y ∈ M"
by (simp add: Transset_def,auto)
locale M_ZF =
fixes M
assumes
upair_ax: "upair_ax(##M)"
and Union_ax: "Union_ax(##M)"
and power_ax: "power_ax(##M)"
and extensionality: "extensionality(##M)"
and foundation_ax: "foundation_ax(##M)"
and infinity_ax: "infinity_ax(##M)"
and separation_ax: "φ∈formula ⟹ env∈list(M) ⟹ arity(φ) ≤ 1 #+ length(env) ⟹
separation(##M,λx. sats(M,φ,[x] @ env))"
and replacement_ax: "φ∈formula ⟹ env∈list(M) ⟹ arity(φ) ≤ 2 #+ length(env) ⟹
strong_replacement(##M,λx y. sats(M,φ,[x,y] @ env))"
locale M_ctm = M_ZF +
fixes enum
assumes M_countable: "enum∈bij(nat,M)"
and trans_M: "Transset(M)"
begin
interpretation intf: M_ZF_trans "M"
apply (rule M_ZF_trans.intro)
apply (simp_all add: trans_M upair_ax Union_ax power_ax extensionality
foundation_ax infinity_ax separation_ax[simplified]
replacement_ax[simplified])
done
lemmas transitivity = Transset_intf[OF trans_M]
lemma zero_in_M: "0 ∈ M"
by (rule intf.zero_in_M)
lemma tuples_in_M: "A∈M ⟹ B∈M ⟹ <A,B>∈M"
by (simp flip:setclass_iff)
lemma nat_in_M : "nat ∈ M"
by (rule intf.nat_in_M)
lemma n_in_M : "n∈nat ⟹ n∈M"
using nat_in_M transitivity by simp
lemma mtriv: "M_trivial(##M)"
by (rule intf.mtriv)
lemma mtrans: "M_trans(##M)"
by (rule intf.mtrans)
lemma mbasic: "M_basic(##M)"
by (rule intf.mbasic)
lemma mtrancl: "M_trancl(##M)"
by (rule intf.mtrancl)
lemma mdatatypes: "M_datatypes(##M)"
by (rule intf.mdatatypes)
lemma meclose: "M_eclose(##M)"
by (rule intf.meclose)
lemma meclose_pow: "M_eclose_pow(##M)"
by (rule intf.meclose_pow)
end
sublocale M_ctm ⊆ M_trivial "##M"
by (rule mtriv)
sublocale M_ctm ⊆ M_trans "##M"
by (rule mtrans)
sublocale M_ctm ⊆ M_basic "##M"
by (rule mbasic)
sublocale M_ctm ⊆ M_trancl "##M"
by (rule mtrancl)
sublocale M_ctm ⊆ M_datatypes "##M"
by (rule mdatatypes)
sublocale M_ctm ⊆ M_eclose "##M"
by (rule meclose)
sublocale M_ctm ⊆ M_eclose_pow "##M"
by (rule meclose_pow)
context M_ctm
begin
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[of z A] 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[of z A] 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[of z A] 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
Eq1: "p∈P"
let
?D="λn∈nat. (if (enum`n⊆P ∧ dense(enum`n)) then enum`n else P)"
have
Eq2: "∀n∈nat. ?D`n ∈ Pow(P)"
by auto
then have
Eq3: "?D:nat→Pow(P)"
using lam_type by auto
have
Eq4: "∀n∈nat. dense(?D`n)"
proof
show
"dense(?D`n)"
if Eq5: "n∈nat" for n
proof -
have
"dense(?D`n)
⟷ dense(if enum ` n ⊆ P ∧ dense(enum ` n) then enum ` n else P)"
using Eq5 by simp
also have
" ... ⟷ (¬(enum ` n ⊆ P ∧ dense(enum ` n)) ⟶ dense(P)) "
using split_if by simp
finally show ?thesis
using P_dense and Eq5 by auto
qed
qed
from Eq3 and Eq4 interpret
cg: countable_generic P leq one ?D
by (unfold_locales, auto)
from Eq1
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)
show
"D ∩ G ≠ 0"
if Eq8: "D∈M" and
Eq9: "D ⊆ P ∧ dense(D) " for D
proof -
from M_countable and bij_is_surj have
"∀y∈M. ∃x∈nat. enum`x= y"
unfolding surj_def by (simp)
with Eq8 obtain n where
Eq10: "n∈nat ∧ enum`n = D"
by auto
with Eq9 and if_P have
Eq11: "?D`n = D"
by (simp)
with Eq6 and Eq10 show
"D∩G≠0"
by auto
qed
with Eq6 have
Eq12: "∃G. filter(G) ∧ (∀D∈M. D⊆P ∧ dense(D)⟶D∩G≠0)"
by auto
qed
with Eq6 show ?thesis
unfolding M_generic_def by auto
qed
lemma compat_in_abs :
assumes
"A∈M" "r∈M" "p∈M" "q∈M"
shows
"is_compat_in(##M,A,r,p,q) ⟷ compat_in(A,r,p,q)"
proof -
have 1:"d∈A ⟹ d∈M" for d
using transitivity ‹A∈M› by simp
moreover
have "d∈A ⟹ ⟨d, t⟩ ∈ M" if "t∈M" for t d
using that 1 pair_in_M_iff by simp
ultimately show ?thesis
unfolding is_compat_in_def compat_in_def
using assms pair_in_M_iff transitivity by auto
qed
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