section‹The general Rasiowa-Sikorski lemma›
theory Rasiowa_Sikorski imports Forcing_Notions Pointed_DC begin
context countable_generic
begin
lemma RS_relation:
assumes "p∈P" "n∈nat"
shows "∃y∈P. ⟨p,y⟩ ∈ (λm∈nat. {⟨x,y⟩∈P×P. y≼x ∧ y∈𝒟`(pred(m))})`n"
proof -
from seq_of_denses ‹n∈nat›
have "dense(𝒟 ` pred(n))" by simp
with ‹p∈P›
have "∃d∈𝒟 ` Arith.pred(n). d≼ p"
unfolding dense_def by simp
then obtain d where 3: "d ∈ 𝒟 ` Arith.pred(n) ∧ d≼ p"
by blast
from countable_subs_of_P ‹n∈nat›
have "𝒟 ` Arith.pred(n) ∈ Pow(P)"
by (blast dest:apply_funtype intro:pred_type)
then
have "𝒟 ` Arith.pred(n) ⊆ P"
by (rule PowD)
with 3
have "d ∈ P ∧ d≼ p ∧ d ∈ 𝒟 ` Arith.pred(n)"
by auto
with ‹p∈P› ‹n∈nat›
show ?thesis by auto
qed
lemma DC_imp_RS_sequence:
assumes "p∈P"
shows "∃f. f: nat→P ∧ f ` 0 = p ∧
(∀n∈nat. f ` succ(n)≼ f ` n ∧ f ` succ(n) ∈ 𝒟 ` n)"
proof -
let ?S="(λm∈nat. {⟨x,y⟩∈P×P. y≼x ∧ y∈𝒟`(pred(m))})"
have "∀x∈P. ∀n∈nat. ∃y∈P. ⟨x,y⟩ ∈ ?S`n"
using RS_relation by (auto)
then
have "∀a∈P. (∃f ∈ nat→P. f`0 = a ∧ (∀n ∈ nat. ⟨f`n,f`succ(n)⟩∈?S`succ(n)))"
using sequence_DC by (blast)
with ‹p∈P›
show ?thesis by auto
qed
theorem rasiowa_sikorski:
"p∈P ⟹ ∃G. p∈G ∧ D_generic(G)"
using RS_sequence_imp_rasiowa_sikorski by (auto dest:DC_imp_RS_sequence)
end
end