Theory Forcing_Data
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
locale M_ctm= M_ZF_trans +
fixes enum
assumes M_countable: "enum∈bij(nat,M)"
begin
end
locale M_ctm_AC= M_ctm + M_ZFC_trans
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 P_sub_M : "P⊆M"
using transitivity[OF _ P_in_M] by auto
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
lemma one_in_M : "one ∈ M"
by (insert one_in_P P_in_M, simp add: transitivity)
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