Theory Rasiowa_Sikorski

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 (* countable_generic *)

end