theory Forcing_data imports Forcing_notions 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
locale forcing_data = forcing_notion +
fixes M 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)"
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