theory Utils
  imports "ZF-Constructible.Formula"
begin

ML_file ‹utils.ML›

end

signature UTILS =
 sig
    val binop : term -> term -> term -> term
    val add_: term -> term -> term
    val app_: term -> term -> term
    val concat_: term -> term -> term
    val dest_apply: term -> term * term
    val dest_iff_lhs: term -> term
    val dest_iff_rhs: term -> term
    val dest_iff_tms: term -> term * term
    val dest_lhs_def: term -> term
    val dest_rhs_def: term -> term
    val dest_satisfies_tms: term -> term * term
    val dest_satisfies_frm: term -> term
    val dest_eq_tms: term -> term * term
    val dest_sats_frm: term -> (term * term) * term
    val dest_trueprop: term -> term
    val eq_: term -> term -> term
    val fix_vars: thm -> string list -> Proof.context -> thm
    val formula_: term
    val freeName: term -> string
    val inList: ''a -> ''a list -> bool
    val isFree: term -> bool
    val length_: term -> term
    val list_: term -> term
    val lt_: term -> term -> term
    val mem_: term -> term -> term
    val mk_FinSet: term list -> term
    val mk_Pair: term -> term -> term
    val mk_ZFlist: ('a -> term) -> 'a list -> term
    val mk_ZFnat: int -> term
    val nat_: term
    val nth_: term -> term -> term
    val subset_: term -> term -> term
    val thm_concl_tm :  Proof.context -> xstring -> 
        ((indexname * typ) * cterm) list * term * Proof.context
    val to_ML_list: term -> term list
    val tp: term -> term
  end

structure Utils : UTILS =
struct 
(* Smart constructors for ZF-terms *)

fun inList a = exists (fn b => a = b)

fun binop h t u = h $ t $ u
val mk_Pair  = binop @{const Pair}

fun mk_FinSet nil = @{const zero}
  | mk_FinSet (e :: es) = @{const cons} $ e $ mk_FinSet es

fun mk_ZFnat 0 = @{const zero}
  | mk_ZFnat n = @{const succ} $ mk_ZFnat (n-1)

fun mk_ZFlist _ nil = @{const "Nil"}
  | mk_ZFlist f (t :: ts) = @{const "Cons"} $ f t $ mk_ZFlist f ts

fun to_ML_list (@{const Nil}) = nil
  | to_ML_list (@{const Cons} $ t $ ts) = t :: to_ML_list ts
|   to_ML_list _ = nil

fun isFree (Free (_,_)) = true
  | isFree _ = false

fun freeName (Free (n,_)) = n
  | freeName _ = error "Not a free variable"

val app_ = binop @{const apply}

fun tp x = @{const Trueprop} $ x
fun length_ env = @{const length} $ env
val nth_ = binop @{const nth}
val add_ = binop @{const add}
val mem_ = binop @{const mem}
val subset_ = binop @{const Subset}
val lt_ = binop @{const lt}
val concat_ = binop @{const app}
val eq_ = binop @{const IFOL.eq(i)}

(* Abbreviation for sets *)
fun list_ set = @{const list} $ set
val nat_ = @{const nat}
val formula_ = @{const formula}

(** Destructors of terms **)
fun dest_eq_tms (Const (@{const_name IFOL.eq},_) $ t $ u) = (t, u)
  | dest_eq_tms t = raise TERM ("dest_eq_tms", [t])

fun dest_lhs_def (Const (@{const_name Pure.eq},_) $ x $ _) = x
  | dest_lhs_def t = raise TERM ("dest_lhs_def", [t])

fun dest_rhs_def (Const (@{const_name Pure.eq},_) $ _ $ y) = y
  | dest_rhs_def t = raise TERM ("dest_rhs_def", [t])


fun dest_apply (@{const apply} $ t $ u) = (t,u)
  | dest_apply t = raise TERM ("dest_applies_op", [t])

fun dest_satisfies_tms (@{const Formula.satisfies} $ A $ f) = (A,f)
  | dest_satisfies_tms t = raise TERM ("dest_satisfies_tms", [t]);

val dest_satisfies_frm = #2 o dest_satisfies_tms

fun dest_sats_frm t = t |> dest_eq_tms |> #1 |> dest_apply |>> dest_satisfies_tms ;

fun dest_trueprop (@{const IFOL.Trueprop} $ t) = t
  | dest_trueprop t = t

fun dest_iff_tms (@{const IFOL.iff} $ t $ u) = (t, u)
  | dest_iff_tms t = raise TERM ("dest_iff_tms", [t])

val dest_iff_lhs = #1 o dest_iff_tms
val dest_iff_rhs = #2 o dest_iff_tms

fun thm_concl_tm ctxt thm_ref =
  let val (((_,vars),thm_tms),ctxt1) = Variable.import true [Proof_Context.get_thm ctxt thm_ref] ctxt
  in (vars, thm_tms |> hd |> Thm.concl_of, ctxt1)
end

fun fix_vars thm vars ctxt = let
  val (_, ctxt1) = Variable.add_fixes vars ctxt
  in singleton (Proof_Context.export ctxt1 ctxt) thm
end

end ;

section‹Forcing notions›
text‹This theory defines a locale for forcing notions, that is,
 preorders with a distinguished maximum element.›

theory Forcing_Notions
  imports "ZF-Constructible.Relative"
begin

subsection‹Basic concepts›
text‹We say that two elements $p,q$ are
  ∗‹compatible› if they have a lower bound in $P$›
definition compat_in :: "i⇒i⇒i⇒i⇒o" where
  "compat_in(A,r,p,q) ≡ ∃d∈A . ⟨d,p⟩∈r ∧ ⟨d,q⟩∈r"

definition
  is_compat_in :: "[i⇒o,i,i,i,i] ⇒ o" where
  "is_compat_in(M,A,r,p,q) ≡ ∃d[M]. d∈A ∧ (∃dp[M]. pair(M,d,p,dp) ∧ dp∈r ∧ 
                                   (∃dq[M]. pair(M,d,q,dq) ∧ dq∈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)

lemma refl_monot_domain: "refl(B,r) ⟹ A⊆B ⟹ refl(A,r)"  
  unfolding refl_def by blast

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

abbreviation Leq :: "[i, i] ⇒ o"  (infixl "≼" 50)
  where "x ≼ y ≡ ⟨x,y⟩∈leq"

lemma refl_leq:
  "r∈P ⟹ r≼r"
  using leq_preord unfolding preorder_on_def refl_def by simp

text‹A set $D$ is ∗‹dense› if every element $p\in P$ has a lower 
bound in $D$.›
definition 
  dense :: "i⇒o" where
  "dense(D) ≡ ∀p∈P. ∃d∈D . d≼p"

text‹There is also a weaker definition which asks for 
a lower bound in $D$ only for the elements below some fixed 
element $q$.›
definition 
  dense_below :: "i⇒i⇒o" where
  "dense_below(D,q) ≡ ∀p∈P. p≼q ⟶ (∃d∈D. d∈P ∧ d≼p)"

lemma P_dense: "dense(P)"
  by (insert leq_preord, auto simp add: preorder_on_def refl_def dense_def)

definition 
  increasing :: "i⇒o" where
  "increasing(F) ≡ ∀x∈F. ∀ p ∈ P . x≼p ⟶ p∈F"

definition 
  compat :: "i⇒i⇒o" where
  "compat(p,q) ≡ compat_in(P,leq,p,q)"

lemma leq_transD:  "a≼b ⟹ b≼c ⟹ a ∈ P⟹ b ∈ P⟹ c ∈ P⟹ a≼c"
  using leq_preord trans_onD unfolding preorder_on_def by blast

lemma leq_transD':  "A⊆P ⟹ a≼b ⟹ b≼c ⟹ a ∈ A ⟹ b ∈ P⟹ c ∈ P⟹ a≼c"
  using leq_preord trans_onD subsetD unfolding preorder_on_def by blast


lemma leq_reflI: "p∈P ⟹ p≼p"
  using leq_preord unfolding preorder_on_def refl_def by blast

lemma compatD[dest!]: "compat(p,q) ⟹ ∃d∈P. d≼p ∧ d≼q"
  unfolding compat_def compat_in_def .

abbreviation Incompatible :: "[i, i] ⇒ o"  (infixl "⊥" 50)
  where "p ⊥ q ≡ ¬ compat(p,q)"

lemma compatI[intro!]: "d∈P ⟹ d≼p ⟹ d≼q ⟹ compat(p,q)"
  unfolding compat_def compat_in_def by blast

lemma denseD [dest]: "dense(D) ⟹ p∈P ⟹  ∃d∈D. d≼ p"
  unfolding dense_def by blast

lemma denseI [intro!]: "⟦ ⋀p. p∈P ⟹ ∃d∈D. d≼ p ⟧ ⟹ dense(D)"
  unfolding dense_def by blast

lemma dense_belowD [dest]:
  assumes "dense_below(D,p)" "q∈P" "q≼p"
  shows "∃d∈D. d∈P ∧ d≼q"
  using assms unfolding dense_below_def by simp
    (*obtains d where "d∈D" "d∈P" "d≼q"
  using assms unfolding dense_below_def by blast *)

lemma dense_belowI [intro!]: 
  assumes "⋀q. q∈P ⟹ q≼p ⟹ ∃d∈D. d∈P ∧ d≼q" 
  shows "dense_below(D,p)"
  using assms unfolding dense_below_def by simp

lemma dense_below_cong: "p∈P ⟹ D = D' ⟹ dense_below(D,p) ⟷ dense_below(D',p)"
  by blast

lemma dense_below_cong': "p∈P ⟹ ⟦⋀x. x∈P ⟹ Q(x) ⟷ Q'(x)⟧ ⟹ 
           dense_below({q∈P. Q(q)},p) ⟷ dense_below({q∈P. Q'(q)},p)"
  by blast

lemma dense_below_mono: "p∈P ⟹ D ⊆ D' ⟹ dense_below(D,p) ⟹ dense_below(D',p)"
  by blast

lemma dense_below_under:
  assumes "dense_below(D,p)" "p∈P" "q∈P" "q≼p"
  shows "dense_below(D,q)"
  using assms leq_transD by blast

lemma ideal_dense_below:
  assumes "⋀q. q∈P ⟹ q≼p ⟹ q∈D"
  shows "dense_below(D,p)"
  using assms leq_reflI by blast

lemma dense_below_dense_below: 
  assumes "dense_below({q∈P. dense_below(D,q)},p)" "p∈P" 
  shows "dense_below(D,p)"  
  using assms leq_transD leq_reflI  by blast
    (* Long proof *)
    (*  unfolding dense_below_def
proof (intro ballI impI)
  fix r
  assume "r∈P" ‹r≼p›
  with assms
  obtain q where "q∈P" "q≼r" "dense_below(D,q)"
    using assms by auto
  moreover from this
  obtain d where "d∈P" "d≼q" "d∈D"
    using assms leq_preord unfolding preorder_on_def refl_def by blast
  moreover
  note ‹r∈P›
  ultimately
  show "∃d∈D. d ∈ P ∧ d≼ r"
    using leq_preord trans_onD unfolding preorder_on_def by blast
qed *)

definition
  antichain :: "i⇒o" where
  "antichain(A) ≡ A⊆P ∧ (∀p∈A.∀q∈A.(¬compat(p,q)))"

text‹A filter is an increasing set $G$ with all its elements 
being compatible in $G$.›
definition 
  filter :: "i⇒o" where
  "filter(G) ≡ G⊆P ∧ increasing(G) ∧ (∀p∈G. ∀q∈G. compat_in(G,leq,p,q))"

lemma filterD : "filter(G) ⟹ x ∈ G ⟹ x ∈ P"
  by (auto simp add : subsetD filter_def)

lemma filter_leqD : "filter(G) ⟹ x ∈ G ⟹ y ∈ P ⟹ x≼y ⟹ y ∈ G"
  by (simp add: filter_def increasing_def)

lemma filter_imp_compat: "filter(G) ⟹ p∈G ⟹ q∈G ⟹ compat(p,q)"
  unfolding filter_def compat_in_def compat_def by blast

lemma low_bound_filter: ― ‹says the compatibility is attained inside G›
  assumes "filter(G)" and "p∈G" and "q∈G"
  shows "∃r∈G. r≼p ∧ r≼q" 
  using assms 
  unfolding compat_in_def filter_def by blast

text‹We finally introduce the upward closure of a set
and prove that the closure of $A$ is a filter if its elements are
compatible in $A$.›
definition  
  upclosure :: "i⇒i" where
  "upclosure(A) ≡ {p∈P.∃a∈A. a≼p}"

lemma  upclosureI [intro] : "p∈P ⟹ a∈A ⟹ a≼p ⟹ p∈upclosure(A)"
  by (simp add:upclosure_def, auto)

lemma  upclosureE [elim] :
  "p∈upclosure(A) ⟹ (⋀x a. x∈P ⟹ a∈A ⟹ a≼x ⟹ R) ⟹ R"
  by (auto simp add:upclosure_def)

lemma  upclosureD [dest] :
  "p∈upclosure(A) ⟹ ∃a∈A.(a≼p) ∧ p∈P"
  by (simp add:upclosure_def)

lemma upclosure_increasing :
  assumes "A⊆P"
  shows "increasing(upclosure(A))"
  unfolding increasing_def upclosure_def
  using leq_transD'[OF ‹A⊆P›] by auto

lemma  upclosure_in_P: "A ⊆ P ⟹ upclosure(A) ⊆ P"
  using subsetI upclosure_def by simp

lemma  A_sub_upclosure: "A ⊆ P ⟹ A⊆upclosure(A)"
  using subsetI leq_preord 
  unfolding upclosure_def preorder_on_def refl_def by auto

lemma  elem_upclosure: "A⊆P ⟹ x∈A  ⟹ x∈upclosure(A)"
  by (blast dest:A_sub_upclosure)

lemma  closure_compat_filter:
  assumes "A⊆P" "(∀p∈A.∀q∈A. compat_in(A,leq,p,q))"
  shows "filter(upclosure(A))"
  unfolding filter_def
proof(auto)
  show "increasing(upclosure(A))"
    using assms upclosure_increasing by simp
next
  let ?UA="upclosure(A)"
  show "compat_in(upclosure(A), leq, p, q)" if "p∈?UA" "q∈?UA" for p q
  proof -
    from that
    obtain a b where 1:"a∈A" "b∈A" "a≼p" "b≼q" "p∈P" "q∈P"
      using upclosureD[OF ‹p∈?UA›] upclosureD[OF ‹q∈?UA›] by auto
    with assms(2)
    obtain d where "d∈A" "d≼a" "d≼b"
      unfolding compat_in_def by auto
    with 1
    have 2:"d≼p" "d≼q" "d∈?UA"
      using A_sub_upclosure[THEN subsetD] ‹A⊆P›
        leq_transD'[of A d a] leq_transD'[of A d b] by auto
    then
    show ?thesis unfolding compat_in_def by auto
  qed
qed

lemma  aux_RS1:  "f ∈ N → P ⟹ n∈N ⟹ f`n ∈ upclosure(f ``N)"
  using elem_upclosure[OF subset_fun_image] image_fun
  by (simp, blast)

lemma decr_succ_decr: 
  assumes "f ∈ nat → P" "preorder_on(P,leq)"
    "∀n∈nat.  ⟨f ` succ(n), f ` n⟩ ∈ leq"
    "m∈nat"
  shows "n∈nat ⟹ n≤m ⟹ ⟨f ` m, f ` n⟩ ∈ leq"
  using ‹m∈_›
proof(induct m)
  case 0
  then show ?case using assms leq_reflI by simp
next
  case (succ x)
  then
  have 1:"f`succ(x) ≼ f`x" "f`n∈P" "f`x∈P" "f`succ(x)∈P"
    using assms by simp_all
  consider (lt) "n<succ(x)" | (eq) "n=succ(x)"
    using succ le_succ_iff by auto
  then 
  show ?case 
  proof(cases)
    case lt
    with 1 show ?thesis using leI succ leq_transD by auto
  next
    case eq
    with 1 show ?thesis using leq_reflI by simp
  qed
qed

lemma decr_seq_linear: 
  assumes "refl(P,leq)" "f ∈ nat → P"
    "∀n∈nat.  ⟨f ` succ(n), f ` n⟩ ∈ leq"
    "trans[P](leq)"
  shows "linear(f `` nat, leq)"
proof -
  have "preorder_on(P,leq)" 
    unfolding preorder_on_def using assms by simp
  {
    fix n m
    assume "n∈nat" "m∈nat"
    then
    have "f`m ≼ f`n ∨ f`n ≼ f`m"
    proof(cases "m≤n")
      case True
      with ‹n∈_› ‹m∈_›
      show ?thesis 
        using decr_succ_decr[of f n m] assms leI ‹preorder_on(P,leq)› by simp
    next
      case False
      with ‹n∈_› ‹m∈_›
      show ?thesis 
        using decr_succ_decr[of f m n] assms leI not_le_iff_lt ‹preorder_on(P,leq)› by simp
    qed
  }
  then
  show ?thesis
    unfolding linear_def using ball_image_simp assms by auto
qed

end (* forcing_notion *)

subsection‹Towards Rasiowa-Sikorski Lemma (RSL)›
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)"

text‹The next lemma identifies a sufficient condition for obtaining
RSL.›
lemma RS_sequence_imp_rasiowa_sikorski:
  assumes 
    "p∈P" "f : nat→P" "f ` 0 = p"
    "⋀n. n∈nat ⟹ f ` succ(n)≼ f ` n ∧ f ` succ(n) ∈ 𝒟 ` n" 
  shows
    "∃G. p∈G ∧ D_generic(G)"
proof -
  note assms
  moreover from this 
  have "f``nat  ⊆ P"
    by (simp add:subset_fun_image)
  moreover from calculation
  have "refl(f``nat, leq) ∧ trans[P](leq)"
    using leq_preord unfolding preorder_on_def by (blast intro:refl_monot_domain)
  moreover from calculation 
  have "∀n∈nat.  f ` succ(n)≼ f ` n" by (simp)
  moreover from calculation
  have "linear(f``nat, leq)"
    using leq_preord and decr_seq_linear unfolding preorder_on_def by (blast)
  moreover from calculation
  have "(∀p∈f``nat.∀q∈f``nat. compat_in(f``nat,leq,p,q))"             
    using chain_compat by (auto)
  ultimately  
  have "filter(upclosure(f``nat))" (is "filter(?G)")
    using closure_compat_filter by simp
  moreover
  have "∀n∈nat. 𝒟 ` n ∩ ?G ≠ 0"
  proof
    fix n
    assume "n∈nat"
    with assms 
    have "f`succ(n) ∈ ?G ∧ f`succ(n) ∈ 𝒟 ` n"
      using aux_RS1 by simp
    then 
    show "𝒟 ` n ∩ ?G ≠ 0"  by blast
  qed
  moreover from assms 
  have "p ∈ ?G"
    using aux_RS1 by auto
  ultimately 
  show ?thesis unfolding D_generic_def by auto
qed

end (* countable_generic *)

text‹Now, the following recursive definition will fulfill the 
requirements of lemma \<^term>‹RS_sequence_imp_rasiowa_sikorski› ›

consts RS_seq :: "[i,i,i,i,i,i] ⇒ i"
primrec
  "RS_seq(0,P,leq,p,enum,𝒟) = p"
  "RS_seq(succ(n),P,leq,p,enum,𝒟) = 
    enum`(μ m. ⟨enum`m, RS_seq(n,P,leq,p,enum,𝒟)⟩ ∈ leq ∧ enum`m ∈ 𝒟 ` n)"

context countable_generic
begin

lemma preimage_rangeD:
  assumes "f∈Pi(A,B)" "b ∈ range(f)" 
  shows "∃a∈A. f`a = b"
  using assms apply_equality[OF _ assms(1), of _ b] domain_type[OF _ assms(1)] by auto

lemma countable_RS_sequence_aux:
  fixes p enum
  defines "f(n) ≡ RS_seq(n,P,leq,p,enum,𝒟)"
    and   "Q(q,k,m) ≡ enum`m≼ q ∧ enum`m ∈ 𝒟 ` k"
  assumes "n∈nat" "p∈P" "P ⊆ range(enum)" "enum:nat→M"
    "⋀x k. x∈P ⟹ k∈nat ⟹  ∃q∈P. q≼ x ∧ q ∈ 𝒟 ` k" 
  shows 
    "f(succ(n)) ∈ P ∧ f(succ(n))≼ f(n) ∧ f(succ(n)) ∈ 𝒟 ` n"
  using ‹n∈nat›
proof (induct)
  case 0
  from assms 
  obtain q where "q∈P" "q≼ p" "q ∈ 𝒟 ` 0" by blast
  moreover from this and ‹P ⊆ range(enum)›
  obtain m where "m∈nat" "enum`m = q" 
    using preimage_rangeD[OF ‹enum:nat→M›] by blast
  moreover 
  have "𝒟`0 ⊆ P"
    using apply_funtype[OF countable_subs_of_P] by simp
  moreover note ‹p∈P›
  ultimately
  show ?case 
    using LeastI[of "Q(p,0)" m] unfolding Q_def f_def by auto
next
  case (succ n)
  with assms 
  obtain q where "q∈P" "q≼ f(succ(n))" "q ∈ 𝒟 ` succ(n)" by blast
  moreover from this and ‹P ⊆ range(enum)›
  obtain m where "m∈nat" "enum`m≼ f(succ(n))" "enum`m ∈ 𝒟 ` succ(n)"
    using preimage_rangeD[OF ‹enum:nat→M›] by blast
  moreover note succ
  moreover from calculation
  have "𝒟`succ(n) ⊆ P" 
    using apply_funtype[OF countable_subs_of_P] by auto
  ultimately
  show ?case
    using LeastI[of "Q(f(succ(n)),succ(n))" m] unfolding Q_def f_def by auto
qed

lemma countable_RS_sequence:
  fixes p enum
  defines "f ≡ λn∈nat. RS_seq(n,P,leq,p,enum,𝒟)"
    and   "Q(q,k,m) ≡ enum`m≼ q ∧ enum`m ∈ 𝒟 ` k"
  assumes "n∈nat" "p∈P" "P ⊆ range(enum)" "enum:nat→M"
  shows 
    "f`0 = p" "f`succ(n)≼ f`n ∧ f`succ(n) ∈ 𝒟 ` n" "f`succ(n) ∈ P"
proof -
  from assms
  show "f`0 = p" by simp
  {
    fix x k
    assume "x∈P" "k∈nat"
    then
    have "∃q∈P. q≼ x ∧ q ∈ 𝒟 ` k"
      using seq_of_denses apply_funtype[OF countable_subs_of_P] 
      unfolding dense_def by blast
  }
  with assms
  show "f`succ(n)≼ f`n ∧ f`succ(n) ∈ 𝒟 ` n" "f`succ(n)∈P"
    unfolding f_def using countable_RS_sequence_aux by simp_all
qed

lemma RS_seq_type: 
  assumes "n ∈ nat" "p∈P" "P ⊆ range(enum)" "enum:nat→M"
  shows "RS_seq(n,P,leq,p,enum,𝒟) ∈ P"
  using assms countable_RS_sequence(1,3)  
  by (induct;simp) 

lemma RS_seq_funtype:
  assumes "p∈P" "P ⊆ range(enum)" "enum:nat→M"
  shows "(λn∈nat. RS_seq(n,P,leq,p,enum,𝒟)): nat → P"
  using assms lam_type RS_seq_type by auto

lemmas countable_rasiowa_sikorski = 
  RS_sequence_imp_rasiowa_sikorski[OF _ RS_seq_funtype countable_RS_sequence(1,2)]
end (* countable_generic *)

end

section‹A pointed version of DC›
theory Pointed_DC imports ZF.AC

begin
txt‹This proof of DC is from Moschovakis "Notes on Set Theory"›

consts dc_witness :: "i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i"
primrec
  wit0   : "dc_witness(0,A,a,s,R) = a"
  witrec :"dc_witness(succ(n),A,a,s,R) = s`{x∈A. ⟨dc_witness(n,A,a,s,R),x⟩∈R }"

lemma witness_into_A [TC]:
  assumes "a∈A"
    "(∀X . X≠0 ∧ X⊆A ⟶ s`X∈X)"
    "∀y∈A. {x∈A. ⟨y,x⟩∈R } ≠ 0" "n∈nat"
  shows "dc_witness(n, A, a, s, R)∈A"
  using ‹n∈nat›
proof(induct n)
  case 0
  then show ?case using ‹a∈A› by simp
next
  case (succ x)
  then
  show ?case using assms by auto
qed

lemma witness_related :
  assumes "a∈A"
    "(∀X . X≠0 ∧ X⊆A ⟶ s`X∈X)"
    "∀y∈A. {x∈A. ⟨y,x⟩∈R } ≠ 0" "n∈nat"
  shows "⟨dc_witness(n, A, a, s, R),dc_witness(succ(n), A, a, s, R)⟩∈R"
proof -
  from assms
  have "dc_witness(n, A, a, s, R)∈A" (is "?x ∈ A")
    using witness_into_A[of _ _ s R n] by simp
  with assms
  show ?thesis by auto
qed

lemma witness_funtype:
  assumes "a∈A"
    "(∀X . X≠0 ∧ X⊆A ⟶ s`X∈X)"
    "∀y∈A. {x∈A. ⟨y,x⟩∈R } ≠ 0"
  shows "(λn∈nat. dc_witness(n, A, a, s, R)) ∈ nat → A" (is "?f ∈ _ → _")
proof -
  have "?f ∈ nat → {dc_witness(n, A, a, s, R). n∈nat}" (is "_ ∈ _ → ?B")
    using lam_funtype assms by simp
  then
  have "?B ⊆ A"
    using witness_into_A assms by auto
  with ‹?f ∈ _›
  show ?thesis
    using fun_weaken_type
    by simp
qed

lemma witness_to_fun:   assumes "a∈A"
  "(∀X . X≠0 ∧ X⊆A ⟶ s`X∈X)"
  "∀y∈A. {x∈A. ⟨y,x⟩∈R } ≠ 0"
shows "∃f ∈ nat→A. ∀n∈nat. f`n =dc_witness(n,A,a,s,R)"
  using assms bexI[of _ "λn∈nat. dc_witness(n,A,a,s,R)"] witness_funtype
  by simp

theorem pointed_DC  :
  assumes "(∀x∈A. ∃y∈A. ⟨x,y⟩∈ R)"
  shows "∀a∈A. (∃f ∈ nat→A. f`0 = a ∧ (∀n ∈ nat. ⟨f`n,f`succ(n)⟩∈R))"
proof -
  have 0:"∀y∈A. {x ∈ A . ⟨y, x⟩ ∈ R} ≠ 0"
    using assms by auto
  from AC_func_Pow[of A]
  obtain g
    where 1: "g ∈ Pow(A) - {0} → A"
      "∀X. X ≠ 0 ∧ X ⊆ A ⟶ g ` X ∈ X"
    by auto
  let ?f ="λa.λn∈nat. dc_witness(n,A,a,g,R)"
  {
    fix a
    assume "a∈A"
    from ‹a∈A›
    have f0: "?f(a)`0 = a" by simp
    with ‹a∈A›
    have "⟨?f(a) ` n, ?f(a) ` succ(n)⟩ ∈ R" if "n∈nat" for n
      using witness_related[OF ‹a∈A› 1(2) 0] beta that by simp
    then
    have "∃f∈nat → A. f ` 0 = a ∧ (∀n∈nat. ⟨f ` n, f ` succ(n)⟩ ∈ R)" (is "∃x∈_ .?P(x)")
      using f0 witness_funtype 0 1 ‹a∈_› by blast
  }
  then show ?thesis by auto
qed

lemma aux_DC_on_AxNat2 : "∀x∈A×nat. ∃y∈A. ⟨x,⟨y,succ(snd(x))⟩⟩ ∈ R ⟹
                  ∀x∈A×nat. ∃y∈A×nat. ⟨x,y⟩ ∈ {⟨a,b⟩∈R. snd(b) = succ(snd(a))}"
  by (rule ballI, erule_tac x="x" in ballE, simp_all)

lemma infer_snd : "c∈ A×B ⟹ snd(c) = k ⟹ c=⟨fst(c),k⟩"
  by auto

corollary DC_on_A_x_nat :
  assumes "(∀x∈A×nat. ∃y∈A. ⟨x,⟨y,succ(snd(x))⟩⟩ ∈ R)" "a∈A"
  shows "∃f ∈ nat→A. f`0 = a ∧ (∀n ∈ nat. ⟨⟨f`n,n⟩,⟨f`succ(n),succ(n)⟩⟩∈R)" (is "∃x∈_.?P(x)")
proof -
  let ?R'="{⟨a,b⟩∈R. snd(b) = succ(snd(a))}"
  from assms(1)
  have "∀x∈A×nat. ∃y∈A×nat. ⟨x,y⟩ ∈ ?R'"
    using aux_DC_on_AxNat2 by simp
  with ‹a∈_›
  obtain f where
    F:"f∈nat→A×nat" "f ` 0 = ⟨a,0⟩"  "∀n∈nat. ⟨f ` n, f ` succ(n)⟩ ∈ ?R'"
    using pointed_DC[of "A×nat" ?R'] by blast
  let ?f="λx∈nat. fst(f`x)"
  from F
  have "?f∈nat→A" "?f ` 0 = a" by auto
  have 1:"n∈ nat ⟹ f`n= ⟨?f`n, n⟩" for n
  proof(induct n set:nat)
    case 0
    then show ?case using F by simp
  next
    case (succ x)
    then
    have "⟨f`x, f`succ(x)⟩ ∈ ?R'" "f`x ∈ A×nat" "f`succ(x)∈A×nat"
      using F by simp_all
    then
    have "snd(f`succ(x)) = succ(snd(f`x))" by simp
    with succ ‹f`x∈_›
    show ?case using infer_snd[OF ‹f`succ(_)∈_›] by auto
  qed
  have "⟨⟨?f`n,n⟩,⟨?f`succ(n),succ(n)⟩⟩ ∈ R" if "n∈nat" for n
    using that 1[of "succ(n)"] 1[OF ‹n∈_›] F(3) by simp
  with ‹f`0=⟨a,0⟩›
  show ?thesis using rev_bexI[OF ‹?f∈_›] by simp
qed

lemma aux_sequence_DC :
  assumes "∀x∈A. ∀n∈nat. ∃y∈A. ⟨x,y⟩ ∈ S`n"
    "R={⟨⟨x,n⟩,⟨y,m⟩⟩ ∈ (A×nat)×(A×nat). ⟨x,y⟩∈S`m }"
  shows "∀ x∈A×nat . ∃y∈A. ⟨x,⟨y,succ(snd(x))⟩⟩ ∈ R"
  using assms Pair_fst_snd_eq by auto

lemma aux_sequence_DC2 : "∀x∈A. ∀n∈nat. ∃y∈A. ⟨x,y⟩ ∈ S`n ⟹
        ∀x∈A×nat. ∃y∈A. ⟨x,⟨y,succ(snd(x))⟩⟩ ∈ {⟨⟨x,n⟩,⟨y,m⟩⟩∈(A×nat)×(A×nat). ⟨x,y⟩∈S`m }"
  by auto

lemma sequence_DC:
  assumes "∀x∈A. ∀n∈nat. ∃y∈A. ⟨x,y⟩ ∈ S`n"
  shows "∀a∈A. (∃f ∈ nat→A. f`0 = a ∧ (∀n ∈ nat. ⟨f`n,f`succ(n)⟩∈S`succ(n)))"
  by (rule ballI,insert assms,drule aux_sequence_DC2, drule DC_on_A_x_nat, auto)

end

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

section‹Auxiliary results on arithmetic›
theory Nat_Miscellanea imports ZF begin

text‹Most of these results will get used at some point for the
calculation of arities.›
lemmas nat_succI =  Ord_succ_mem_iff [THEN iffD2,OF nat_into_Ord]

lemma nat_succD : "m ∈ nat ⟹  succ(n) ∈ succ(m) ⟹ n ∈ m"
  by (drule_tac j="succ(m)" in ltI,auto elim:ltD)

lemmas zero_in =  ltD [OF nat_0_le]

lemma in_n_in_nat :  "m ∈ nat ⟹ n ∈ m ⟹ n ∈ nat"
  by(drule ltI[of "n"],auto simp add: lt_nat_in_nat)

lemma in_succ_in_nat : "m ∈ nat ⟹ n ∈ succ(m) ⟹ n ∈ nat"
  by(auto simp add:in_n_in_nat)

lemma ltI_neg : "x ∈ nat ⟹ j ≤ x ⟹ j ≠ x ⟹ j < x"
  by (simp add: le_iff)

lemma succ_pred_eq  :  "m ∈ nat ⟹ m ≠ 0  ⟹ succ(pred(m)) = m"
  by (auto elim: natE)

lemma succ_ltI : "succ(j) < n ⟹ j < n"
  by (simp add: succ_leE[OF leI])

lemma succ_In : "n ∈ nat ⟹ succ(j) ∈ n ⟹ j ∈ n"
  by (rule succ_ltI[THEN ltD], auto intro: ltI)

lemmas succ_leD = succ_leE[OF leI]

lemma succpred_leI : "n ∈ nat ⟹  n ≤ succ(pred(n))"
  by (auto elim: natE)

lemma succpred_n0 : "succ(n) ∈ p ⟹ p≠0"
  by (auto)


lemma funcI : "f ∈ A → B ⟹ a ∈ A ⟹ b= f ` a ⟹ ⟨a, b⟩ ∈ f"
  by(simp_all add: apply_Pair)

lemmas natEin = natE [OF lt_nat_in_nat]

lemma succ_in : "succ(x) ≤ y  ⟹ x ∈ y"
  by (auto dest:ltD)

lemmas Un_least_lt_iffn =  Un_least_lt_iff [OF nat_into_Ord nat_into_Ord]

lemma pred_le2 : "n∈ nat ⟹ m ∈ nat ⟹ pred(n) ≤ m ⟹ n ≤ succ(m)"
  by(subgoal_tac "n∈nat",rule_tac n="n" in natE,auto)

lemma pred_le : "n∈ nat ⟹ m ∈ nat ⟹ n ≤ succ(m) ⟹ pred(n) ≤ m"
  by(subgoal_tac "pred(n)∈nat",rule_tac n="n" in natE,auto)

lemma Un_leD1 : "Ord(i)⟹ Ord(j)⟹ Ord(k)⟹  i ∪ j ≤ k ⟹ i ≤ k"   
  by (rule Un_least_lt_iff[THEN iffD1[THEN conjunct1]],simp_all)

lemma Un_leD2 : "Ord(i)⟹ Ord(j)⟹ Ord(k)⟹  i ∪ j ≤k ⟹ j ≤ k"   
  by (rule Un_least_lt_iff[THEN iffD1[THEN conjunct2]],simp_all)

lemma gt1 : "n ∈ nat ⟹ i ∈ n ⟹ i ≠ 0 ⟹ i ≠ 1 ⟹ 1<i"
  by(rule_tac n="i" in natE,erule in_n_in_nat,auto intro: Ord_0_lt)

lemma pred_mono : "m ∈ nat ⟹ n ≤ m ⟹ pred(n) ≤ pred(m)"
  by(rule_tac n="n" in natE,auto simp add:le_in_nat,erule_tac n="m" in natE,auto)

lemma succ_mono : "m ∈ nat ⟹ n ≤ m ⟹ succ(n) ≤ succ(m)"
  by auto

lemma pred2_Un: 
  assumes "j ∈ nat" "m ≤ j" "n ≤ j" 
  shows "pred(pred(m ∪ n)) ≤ pred(pred(j))" 
  using assms pred_mono[of "j"] le_in_nat Un_least_lt pred_mono by simp

lemma nat_union_abs1 : 
  "⟦ Ord(i) ; Ord(j) ; i ≤ j ⟧ ⟹ i ∪ j = j"
  by (rule Un_absorb1,erule le_imp_subset)

lemma nat_union_abs2 : 
  "⟦ Ord(i) ; Ord(j) ; i ≤ j ⟧ ⟹ j ∪ i = j"
  by (rule Un_absorb2,erule le_imp_subset)

lemma nat_un_max : "Ord(i) ⟹ Ord(j) ⟹ i ∪ j = max(i,j)"
  using max_def nat_union_abs1 not_lt_iff_le leI nat_union_abs2
  by auto

lemma nat_max_ty : "Ord(i) ⟹Ord(j) ⟹ Ord(max(i,j))"
  unfolding max_def by simp

lemma le_not_lt_nat : "Ord(p) ⟹ Ord(q) ⟹ ¬ p≤ q ⟹ q ≤ p" 
  by (rule ltE,rule not_le_iff_lt[THEN iffD1],auto,drule ltI[of q p],auto,erule leI)

lemmas nat_simp_union = nat_un_max nat_max_ty max_def 

lemma le_succ : "x∈nat ⟹ x≤succ(x)" by simp
lemma le_pred : "x∈nat ⟹ pred(x)≤x" 
  using pred_le[OF _ _ le_succ] pred_succ_eq 
  by simp

lemma Un_le_compat : "o ≤ p ⟹ q ≤ r ⟹ Ord(o) ⟹ Ord(p) ⟹ Ord(q) ⟹ Ord(r) ⟹ o ∪ q ≤ p ∪ r"
  using le_trans[of q r "p∪r",OF _ Un_upper2_le] le_trans[of o p "p∪r",OF _ Un_upper1_le]
    nat_simp_union 
  by auto

lemma Un_le : "p ≤ r ⟹ q ≤ r ⟹
               Ord(p) ⟹ Ord(q) ⟹ Ord(r) ⟹ 
                p ∪ q ≤ r"
  using nat_simp_union by auto

lemma Un_leI3 : "o ≤ r ⟹ p ≤ r ⟹ q ≤ r ⟹ 
                Ord(o) ⟹ Ord(p) ⟹ Ord(q) ⟹ Ord(r) ⟹ 
                o ∪ p ∪ q ≤ r"
  using nat_simp_union by auto

lemma diff_mono :
  assumes "m ∈ nat" "n∈nat" "p ∈ nat" "m < n" "p≤m"
  shows "m#-p < n#-p"
proof -
  from assms
  have "m#-p ∈ nat" "m#-p #+p = m"
    using add_diff_inverse2 by simp_all
  with assms
  show ?thesis
    using less_diff_conv[of n p "m #- p",THEN iffD2] by simp
qed

lemma pred_Un:
  "x ∈ nat ⟹ y ∈ nat ⟹ Arith.pred(succ(x) ∪ y) = x ∪ Arith.pred(y)"
  "x ∈ nat ⟹ y ∈ nat ⟹ Arith.pred(x ∪ succ(y)) = Arith.pred(x) ∪ y"
  using pred_Un_distrib pred_succ_eq by simp_all

lemma le_natI : "j ≤ n ⟹ n ∈ nat ⟹ j∈nat"
  by(drule ltD,rule in_n_in_nat,rule nat_succ_iff[THEN iffD2,of n],simp_all)

lemma le_natE : "n∈nat ⟹ j < n ⟹  j∈n"
  by(rule ltE[of j n],simp+)

lemma diff_cancel :
  assumes "m ∈ nat" "n∈nat" "m < n"
  shows "m#-n = 0"
  using assms diff_is_0_lemma leI by simp

lemma leD : assumes "n∈nat" "j ≤ n"
  shows "j < n | j = n"
  using leE[OF ‹j≤n›,of "j<n | j = n"] by auto

subsection‹Some results in ordinal arithmetic›
text‹The following results are auxiliary to the proof of 
wellfoundedness of the relation \<^term>‹frecR››

lemma max_cong :
  assumes "x ≤ y" "Ord(y)" "Ord(z)" shows "max(x,y) ≤ max(y,z)"
  using assms 
proof (cases "y ≤ z")
  case True
  then show ?thesis 
    unfolding max_def using assms by simp
next
  case False
  then have "z ≤ y"  using assms not_le_iff_lt leI by simp
  then show ?thesis 
    unfolding max_def using assms by simp 
qed

lemma max_commutes : 
  assumes "Ord(x)" "Ord(y)"
  shows "max(x,y) = max(y,x)"
  using assms Un_commute nat_simp_union(1) nat_simp_union(1)[symmetric] by auto

lemma max_cong2 :
  assumes "x ≤ y" "Ord(y)" "Ord(z)" "Ord(x)" 
  shows "max(x,z) ≤ max(y,z)"
proof -
  from assms 
  have " x ∪ z ≤ y ∪ z"
    using lt_Ord Ord_Un Un_mono[OF  le_imp_subset[OF ‹x≤y›]]  subset_imp_le by auto
  then show ?thesis 
    using  nat_simp_union ‹Ord(x)› ‹Ord(z)› ‹Ord(y)› by simp
qed

lemma max_D1 :
  assumes "x = y" "w < z"  "Ord(x)"  "Ord(w)" "Ord(z)" "max(x,w) = max(y,z)"
  shows "z≤y"
proof -
  from assms
  have "w <  x ∪ w" using Un_upper2_lt[OF ‹w<z›] assms nat_simp_union by simp
  then
  have "w < x" using assms lt_Un_iff[of x w w] lt_not_refl by auto
  then 
  have "y = y ∪ z" using assms max_commutes nat_simp_union assms leI by simp 
  then 
  show ?thesis using Un_leD2 assms by simp
qed

lemma max_D2 :
  assumes "w = y ∨ w = z" "x < y"  "Ord(x)"  "Ord(w)" "Ord(y)" "Ord(z)" "max(x,w) = max(y,z)"
  shows "x<w"
proof -
  from assms
  have "x < z ∪ y" using Un_upper2_lt[OF ‹x<y›] by simp
  then
  consider (a) "x < y" | (b) "x < w"
    using assms nat_simp_union by simp
  then show ?thesis proof (cases)
    case a
    consider (c) "w = y" | (d) "w = z" 
      using assms by auto
    then show ?thesis proof (cases)
      case c
      with a show ?thesis by simp
    next
      case d
      with a
      show ?thesis 
      proof (cases "y <w")
        case True       
        then show ?thesis using lt_trans[OF ‹x<y›] by simp
      next
        case False
        then
        have "w ≤ y" 
          using not_lt_iff_le[OF assms(5) assms(4)] by simp
        with ‹w=z›
        have "max(z,y) = y"  unfolding max_def using assms by simp
        with assms
        have "... = x ∪ w" using nat_simp_union max_commutes  by simp
        then show ?thesis using le_Un_iff assms by blast
      qed
    qed
  next
    case b
    then show ?thesis .
  qed
qed

lemma oadd_lt_mono2 :
  assumes  "Ord(n)" "Ord(α)" "Ord(β)" "α < β" "x < n" "y < n" "0 <n"
  shows "n ** α ++ x < n **β ++ y"
proof -
  consider (0) "β=0" | (s) γ where  "Ord(γ)" "β = succ(γ)" | (l) "Limit(β)"
    using Ord_cases[OF ‹Ord(β)›,of ?thesis] by force
  then show ?thesis 
  proof cases
    case 0
    then show ?thesis using ‹α<β› by auto
  next
    case s
    then
    have "α≤γ" using ‹α<β› using leI by auto
    then
    have "n ** α ≤ n ** γ" using omult_le_mono[OF _ ‹α≤γ›] ‹Ord(n)› by simp
    then
    have "n ** α ++ x < n ** γ ++ n" using oadd_lt_mono[OF _ ‹x<n›] by simp
    also
    have "... = n ** β" using ‹β=succ(_)› omult_succ ‹Ord(β)› ‹Ord(n)› by simp
    finally
    have "n ** α ++ x < n ** β" by auto
    then
    show ?thesis using oadd_le_self ‹Ord(β)› lt_trans2 ‹Ord(n)› by auto
  next
    case l
    have "Ord(x)" using ‹x<n› lt_Ord by simp
    with l
    have "succ(α) < β" using Limit_has_succ ‹α<β› by simp
    have "n ** α ++ x < n ** α ++ n" 
      using oadd_lt_mono[OF le_refl[OF Ord_omult[OF _ ‹Ord(α)›]] ‹x<n›] ‹Ord(n)› by simp
    also
    have "... = n ** succ(α)" using omult_succ ‹Ord(α)› ‹Ord(n)› by simp
    finally
    have "n ** α ++ x < n ** succ(α)" by simp 
    with ‹succ(α) < β›
    have "n ** α ++ x < n ** β" using lt_trans omult_lt_mono ‹Ord(n)› ‹0<n›  by auto      
    then show ?thesis using oadd_le_self ‹Ord(β)› lt_trans2 ‹Ord(n)› by auto
  qed
qed
end