theory Forcing_notions imports Pointed_DC begin
definition compat_in :: "i⇒i⇒i⇒i⇒o" where
"compat_in(A,r,p,q) == ∃d∈A . ⟨d,p⟩∈r ∧ ⟨d,q⟩∈r"
lemma compat_inI :
"⟦ d∈A ; ⟨d,p⟩∈r ; ⟨d,g⟩∈r ⟧ ⟹ compat_in(A,r,p,g)"
by (auto simp add: compat_in_def)
lemma refl_compat:
"⟦ refl(A,r) ; ⟨p,q⟩ ∈ r | p=q | ⟨q,p⟩ ∈ r ; p∈A ; q∈A⟧ ⟹ compat_in(A,r,p,q)"
by (auto simp add: refl_def compat_inI)
lemma chain_compat:
"refl(A,r) ⟹ linear(A,r) ⟹ (∀p∈A.∀q∈A. compat_in(A,r,p,q))"
by (simp add: refl_compat linear_def)
lemma subset_fun_image: "f:N→P ⟹ f``N⊆P"
by (auto simp add: image_fun apply_funtype)
definition
antichain :: "i⇒i⇒i⇒o" where
"antichain(P,leq,A) == A⊆P ∧ (∀p∈A.∀q∈A.(¬ compat_in(P,leq,p,q)))"
definition
ccc :: "i ⇒ i ⇒ o" where
"ccc(P,leq) == ∀A. antichain(P,leq,A) ⟶ |A| ≤ nat"
locale forcing_notion =
fixes P leq one
assumes one_in_P: "one ∈ P"
and leq_preord: "preorder_on(P,leq)"
and one_max: "∀p∈P. ⟨p,one⟩∈leq"
begin
definition
dense :: "i⇒o" where
"dense(D) == ∀p∈P. ∃d∈D . ⟨d,p⟩∈leq"
definition
dense_below :: "i⇒i⇒o" where
"dense_below(D,q) == ∀p∈P. ⟨p,q⟩∈leq ⟶ (∃d∈D . ⟨d,p⟩∈leq)"
lemma P_dense: "dense(P)"
using leq_preord
unfolding preorder_on_def refl_def dense_def
by blast
definition
increasing :: "i⇒o" where
"increasing(F) == ∀x∈F. ∀ p ∈ P . ⟨x,p⟩∈leq ⟶ p∈F"
definition
compat :: "i⇒i⇒o" where
"compat(p,q) == compat_in(P,leq,p,q)"
definition
antichain :: "i⇒o" where
"antichain(A) == A⊆P ∧ (∀p∈A.∀q∈A.(¬compat(p,q)))"
definition
filter :: "i⇒o" where
"filter(G) == G⊆P ∧ increasing(G) ∧ (∀p∈G. ∀q∈G. compat_in(G,leq,p,q))"
definition
upclosure :: "i⇒i" where
"upclosure(A) == {p∈P.∃a∈A.⟨a,p⟩∈leq}"
lemma upclosureI [intro] : "p∈P ⟹ a∈A ⟹ ⟨a,p⟩∈leq ⟹ p∈upclosure(A)"
by (simp add:upclosure_def, auto)
lemma upclosureE [elim] :
"p∈upclosure(A) ⟹ (⋀x a. x∈P ⟹ a∈A ⟹ ⟨a,x⟩∈leq ⟹ R) ⟹ R"
by (auto simp add:upclosure_def)
lemma upclosureD [dest] :
"p∈upclosure(A) ⟹ ∃a∈A.(⟨a,p⟩∈leq) ∧ p∈P"
by (simp add:upclosure_def)
lemma upclosure_increasing :
"A⊆P ⟹ increasing(upclosure(A))"
apply (unfold increasing_def upclosure_def, simp)
apply clarify
apply (rule_tac x="a" in bexI)
apply (insert leq_preord, unfold preorder_on_def)
apply (drule conjunct2, unfold trans_on_def)
apply (drule_tac x="a" in bspec, fast)
apply (drule_tac x="x" in bspec, assumption)
apply (drule_tac x="p" in bspec, assumption)
apply (simp, assumption)
done
lemma upclosure_in_P: "A ⊆ P ⟹ upclosure(A) ⊆ P"
apply (rule subsetI)
apply (simp add:upclosure_def)
done
lemma A_sub_upclosure: "A ⊆ P ⟹ A⊆upclosure(A)"
apply (rule subsetI)
apply (simp add:upclosure_def, auto)
apply (insert leq_preord, unfold preorder_on_def refl_def, auto)
done
lemma elem_upclosure: "A⊆P ⟹ x∈A ⟹ x∈upclosure(A)"
by (blast dest:A_sub_upclosure)
lemma closure_compat_filter:
"A⊆P ⟹ (∀p∈A.∀q∈A. compat_in(A,leq,p,q)) ⟹ filter(upclosure(A))"
apply (unfold filter_def)
apply (intro conjI)
apply (rule upclosure_in_P, assumption)
apply (rule upclosure_increasing, assumption)
apply (unfold compat_in_def)
apply (rule ballI)+
apply (rename_tac x y)
apply (drule upclosureD)+
apply (erule bexE)+
apply (rename_tac a b)
apply (drule_tac A="A" and x="a" in bspec, assumption)
apply (drule_tac A="A" and x="b" in bspec, assumption)
apply (auto)
apply (rule_tac x="d" in bexI)
prefer 2 apply (simp add:A_sub_upclosure [THEN subsetD])
apply (insert leq_preord, unfold preorder_on_def trans_on_def, drule conjunct2)
apply (rule conjI)
apply (drule_tac x="d" in bspec, rule_tac A="A" in subsetD, assumption+)
apply (drule_tac x="a" in bspec, rule_tac A="A" in subsetD, assumption+)
apply (drule_tac x="x" in bspec, assumption, auto)
done
lemma aux_RS1: "f ∈ N → P ⟹ n∈N ⟹ f`n ∈ upclosure(f ``N)"
apply (rule_tac elem_upclosure)
apply (rule subset_fun_image, assumption)
apply (simp add: image_fun, blast)
done
end
lemma refl_monot_domain: "refl(B,r) ⟹ A⊆B ⟹ refl(A,r)"
apply (drule subset_iff [THEN iffD1])
apply (unfold refl_def)
apply (blast)
done
lemma decr_succ_decr: "f ∈ nat → P ⟹ preorder_on(P,leq) ⟹
∀n∈nat. ⟨f ` succ(n), f ` n⟩ ∈ leq ⟹
n∈nat ⟹ m∈nat ⟹ n≤m ⟶ ⟨f ` m, f ` n⟩ ∈ leq"
apply (unfold preorder_on_def, erule conjE)
apply (induct_tac m, simp add:refl_def, rename_tac x)
apply (rule impI)
apply (case_tac "n≤x", simp)
apply (drule_tac x="x" in bspec, assumption)
apply (unfold trans_on_def)
apply (drule_tac x="f`succ(x)" in bspec, simp)
apply (drule_tac x="f`x" in bspec, simp)
apply (drule_tac x="f`n" in bspec, auto)
apply (drule_tac le_succ_iff [THEN iffD1], simp add: refl_def)
done
lemma not_le_imp_lt: "⟦ ~ i ≤ j ; Ord(i); Ord(j) ⟧ ⟹ j<i"
by (simp add:not_le_iff_lt)
lemma decr_seq_linear: "refl(P,leq) ⟹ f ∈ nat → P ⟹
∀n∈nat. ⟨f ` succ(n), f ` n⟩ ∈ leq ⟹
trans[P](leq) ⟹ linear(f `` nat, leq)"
apply (unfold linear_def)
apply (rule ball_image_simp [THEN iffD2], assumption, simp, rule ballI)+
apply (rename_tac y)
apply (case_tac "x≤y")
apply (drule_tac leq="leq" and n="x" and m="y" in decr_succ_decr)
apply (simp add:preorder_on_def)
apply (simp+)
apply (drule not_le_imp_lt [THEN leI], simp_all)
apply (drule_tac leq="leq" and n="y" and m="x" in decr_succ_decr)
apply (simp add:preorder_on_def)
apply (simp+)
done
locale countable_generic = forcing_notion +
fixes 𝒟
assumes countable_subs_of_P: "𝒟 ∈ nat→Pow(P)"
and seq_of_denses: "∀n ∈ nat. dense(𝒟`n)"
begin
definition
D_generic :: "i⇒o" where
"D_generic(G) == filter(G) ∧ (∀n∈nat.(𝒟`n)∩G≠0)"
lemma RS_relation:
assumes
1: "x∈P"
and
2: "n∈nat"
shows
"∃y∈P. ⟨x,y⟩ ∈ (λm∈nat. {⟨x,y⟩∈P*P. ⟨y,x⟩∈leq ∧ y∈𝒟`(pred(m))})`n"
proof -
from seq_of_denses and 2 have "dense(𝒟 ` pred(n))" by (simp)
with 1 have
"∃d∈𝒟 ` Arith.pred(n). ⟨d, x⟩ ∈ leq"
unfolding dense_def by (simp)
then obtain d where
3: "d ∈ 𝒟 ` Arith.pred(n) ∧ ⟨d, x⟩ ∈ leq"
by (rule bexE, simp)
from countable_subs_of_P have
"𝒟 ` Arith.pred(n) ∈ Pow(P)"
using 2 by (blast dest:apply_funtype intro:pred_type)
then have
"𝒟 ` Arith.pred(n) ⊆ P"
by (rule PowD)
then have
"d ∈ P ∧ ⟨d, x⟩ ∈ leq ∧ d ∈ 𝒟 ` Arith.pred(n)"
using 3 by auto
then show ?thesis using 1 and 2 by auto
qed
theorem rasiowa_sikorski:
"p∈P ⟹ ∃G. p∈G ∧ D_generic(G)"
proof -
assume
Eq1: "p∈P"
let
?S="(λm∈nat. {⟨x,y⟩∈P*P. ⟨y,x⟩∈leq ∧ y∈𝒟`(pred(m))})"
from RS_relation have
"∀x∈P. ∀n∈nat. ∃y∈P. ⟨x,y⟩ ∈ ?S`n"
by (auto)
with sequence_DC have
"∀a∈P. (∃f ∈ nat→P. f`0 = a ∧ (∀n ∈ nat. ⟨f`n,f`succ(n)⟩∈?S`succ(n)))"
by (blast)
then obtain f where
Eq2: "f : nat→P"
and
Eq3: "f ` 0 = p ∧
(∀n∈nat.
f ` n ∈ P ∧ f ` succ(n) ∈ P ∧ ⟨f ` succ(n), f ` n⟩ ∈ leq ∧
f ` succ(n) ∈ 𝒟 ` n)"
using Eq1 by (auto)
then have
Eq4: "f``nat ⊆ P"
by (simp add:subset_fun_image)
with leq_preord have
Eq5: "refl(f``nat, leq) ∧ trans[P](leq)"
unfolding preorder_on_def by (blast intro:refl_monot_domain)
from Eq3 have
"∀n∈nat. ⟨f ` succ(n), f ` n⟩ ∈ leq"
by (simp)
with Eq2 and Eq5 and leq_preord and decr_seq_linear have
Eq6: "linear(f``nat, leq)"
unfolding preorder_on_def by (blast)
with Eq5 and chain_compat have
"(∀p∈f``nat.∀q∈f``nat. compat_in(f``nat,leq,p,q))"
by (auto)
then have
fil: "filter(upclosure(f``nat))"
(is "filter(?G)")
using closure_compat_filter and Eq4 by simp
have
gen: "∀n∈nat. 𝒟 ` n ∩ ?G ≠ 0"
proof
fix n
assume
"n∈nat"
with Eq2 and Eq3 have
"f`succ(n) ∈ ?G ∧ f`succ(n) ∈ 𝒟 ` n"
using aux_RS1 by simp
then show
"𝒟 ` n ∩ ?G ≠ 0"
by blast
qed
from Eq3 and Eq2 have
"p ∈ ?G"
using aux_RS1 by auto
with gen and fil show ?thesis
unfolding D_generic_def by auto
qed
end
end