section‹The general Rasiowa-Sikorski lemma›
theory Rasiowa_Sikorski imports Forcing_Notions Pointed_DC begin
context countable_generic
begin
lemma RS_relation:
assumes
1: "p∈P"
and
2: "n∈nat"
shows
"∃y∈P. ⟨p,y⟩ ∈ (λm∈nat. {⟨x,y⟩∈P*P. y≼x ∧ 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≼ p"
unfolding dense_def by (simp)
then obtain d where
3: "d ∈ 𝒟 ` Arith.pred(n) ∧ d≼ p"
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≼ p ∧ d ∈ 𝒟 ` Arith.pred(n)"
using 3 by auto
then show ?thesis using 1 and 2 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