Theory Pointed_DC

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