theory Forcing_Data
imports
Forcing_Notions
Relative
"~~/src/ZF/Constructible/Formula"
begin
lemma lam_codomain: "∀n∈N. (λx∈N. b(x))`n ∈ B ⟹ (λx∈N. b(x)) : N→B"
apply (rule fun_weaken_type)
apply (subgoal_tac " (λx∈N. b(x)) : N → {b(x).x∈N}", assumption)
apply (auto simp add:lam_funtype)
done
lemma Transset_M :
"Transset(M) ⟹ y∈x ⟹ x ∈ M ⟹ y ∈ M"
by (simp add: Transset_def,auto)
definition
infinity_ax :: "(i ⇒ o) ⇒ o" where
"infinity_ax(M) ==
(∃I[M]. (∃z[M]. empty(M,z) ∧ z∈I) ∧ (∀y[M]. y∈I ⟶ (∃sy[M]. successor(M,y,sy) ∧ sy∈I)))"
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 ; arity(φ)=1 ∨ arity(φ)=2 ⟧ ⟹
(∀a∈M. separation(##M,λx. sats(M,φ,[x,a])))"
and replacement_ax: "⟦ φ ∈ formula ; arity(φ)=2 ∨ arity(φ)=succ(2) ⟧ ⟹
(∀a∈M. strong_replacement(##M,λx y. sats(M,φ,[x,y,a])))"
locale forcing_data = forcing_notion + M_ZF +
fixes enum
assumes M_countable: "enum∈bij(nat,M)"
and P_in_M: "P ∈ M"
and leq_in_M: "leq ∈ M"
and trans_M: "Transset(M)"
begin
definition
M_generic :: "i⇒o" where
"M_generic(G) == filter(G) ∧ (∀D∈M. D⊆P ∧ dense(D)⟶D∩G≠0)"
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
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)"
by (rule lam_codomain)
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 cg.rasiowa_sikorski and Eq1 obtain G where
Eq6: "p∈G ∧ filter(G) ∧ (∀n∈nat.(?D`n)∩G≠0)"
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
end
end