Theory Pointed_DC

theory Pointed_DC
imports AC
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]:  "a∈A ⟹ n∈nat ⟹
                             (∀X . X≠0 ∧ X⊆A ⟶ s`X∈X) ⟹
                             ∀y∈A. {x∈A. ⟨y,x⟩∈R } ≠ 0 ⟹
                             dc_witness(n, A, a, s, R)∈A"
  apply (induct_tac n ,simp+)
  apply (drule_tac x="dc_witness(x, A, a, s, R)" in bspec, assumption)
  apply (drule_tac x="{xa ∈ A . ⟨dc_witness(x, A, a, s, R), xa⟩ ∈ R}" in  spec)
  apply auto 
  done
lemma witness_related :  "a∈A ⟹ n∈nat ⟹
                             (∀X . X≠0 ∧ X⊆A ⟶ s`X∈X) ⟹
                             ∀y∈A. {x∈A. ⟨y,x⟩∈R } ≠ 0 ⟹
                             ⟨dc_witness(n, A, a, s, R),dc_witness(succ(n), A, a, s, R)⟩∈R"
  apply (frule_tac n="n" and s="s"  and R="R" in witness_into_A, assumption+)
   apply (drule_tac x="dc_witness(n, A, a, s, R)" in bspec, assumption)
  apply (drule_tac x= "{x ∈ A . ⟨dc_witness(n, A, a, s, R), x⟩ ∈ R}" in spec)
  apply (simp, blast) 
  done
    
lemma witness_funtype: "a∈A ⟹ 
                        (∀X . X≠0 ∧ X⊆A ⟶ s`X∈X) ⟹
                        ∀y∈A. {x∈A. ⟨y,x⟩∈R } ≠ 0 ⟹
                        (λn∈nat. dc_witness(n, A, a, s, R)) ∈ nat → A"
  apply (rule_tac B="{dc_witness(n, A, a, s, R). n∈nat}" in fun_weaken_type)
  apply (rule lam_funtype)
  apply ( blast intro:witness_into_A)
  done
    
lemma witness_to_fun: "a∈A ⟹ (∀X . X≠0 ∧ X⊆A ⟶ s`X∈X) ⟹
                             ∀y∈A. {x∈A. ⟨y,x⟩∈R } ≠ 0 ⟹
                             ∃f ∈ nat→A. ∀n∈nat. f`n =dc_witness(n,A,a,s,R)"
  apply (rule_tac x="λn∈nat. dc_witness(n,A,a,s,R)" in  bexI, simp)
  apply (rule witness_funtype, simp+)
  done

theorem pointed_DC  : "(∀x∈A. ∃y∈A. ⟨x,y⟩∈ R) ⟹
                       ∀a∈A. (∃f ∈ nat→A. f`0 = a ∧ (∀n ∈ nat. ⟨f`n,f`succ(n)⟩∈R))"
  apply (rule)
  apply (insert AC_func_Pow)
  apply (drule allI)
  apply (drule_tac x="A" in spec)
  apply (drule_tac P="λf .∀x∈Pow(A) - {0}. f ` x ∈ x"
               and A="Pow(A)-{0}→ A" 
               and Q=" ∃f∈nat→ A. f ` 0 = a ∧ (∀n∈nat. ⟨f ` n, f ` succ(n)⟩ ∈ R)" in bexE)
  prefer 2 apply (assumption)           
  apply (rename_tac s)
  apply (rule_tac x="λn∈nat. dc_witness(n,A,a,s,R)" in bexI)
   prefer 2  apply (blast intro:witness_funtype)
  apply (rule  conjI, simp)
  apply (rule ballI, rename_tac m)
  apply (subst beta, simp)+
  apply (rule witness_related, auto)
  done

    
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))}"
  apply (rule ballI, erule_tac x="x" in ballE, simp_all)
  done

lemma infer_snd : "c∈ A×B ⟹ snd(c) = k ⟹ c=⟨fst(c),k⟩"
  by auto
    
corollary DC_on_A_x_nat : 
  "(∀x∈A×nat. ∃y∈A. ⟨x,⟨y,succ(snd(x))⟩⟩ ∈ R) ⟹
    ∀a∈A. (∃f ∈ nat→A. f`0 = a ∧ (∀n ∈ nat. ⟨⟨f`n,n⟩,⟨f`succ(n),succ(n)⟩⟩∈R))"
  apply (frule aux_DC_on_AxNat2)
  apply (drule_tac R="{⟨a,b⟩∈R. snd(b) = succ(snd(a))}" in  pointed_DC)
  apply (rule ballI)
  apply (rotate_tac)
  apply (drule_tac x="⟨a,0⟩" in  bspec, simp)
  apply (erule bexE, rename_tac g)  
  apply (rule_tac x="λx∈nat. fst(g`x)" and A="nat→A" in bexI, auto)
  apply (subgoal_tac "∀n∈nat. g`n= ⟨fst(g ` n), n⟩")
   prefer 2 apply (rule ballI, rename_tac m)
   apply (induct_tac m, simp)
   apply (rename_tac d, auto)
  apply (frule_tac A="nat" and x="d" in bspec, simp)
  apply (rule_tac A="A" and B="nat" in infer_snd, auto)
  apply (rule_tac a="⟨fst(g ` d), d⟩" and b="g ` d" in ssubst, assumption)
    (* Notorio: simp, auto ni blast lo hacen aquí! 
       El problema es que está usando "mal" las assumptions: esta sí sirve
       apply (simp (no_asm)) *)
  apply (subst snd_conv, simp)
  done

lemma aux_sequence_DC : "⋀R. ∀x∈A. ∀n∈nat. ∃y∈A. ⟨x,y⟩ ∈ S`n ⟹
                        R={⟨⟨x,n⟩,⟨y,m⟩⟩∈(A×nat)×(A×nat). ⟨x,y⟩∈S`m } ⟹
                        ∀x∈A×nat. ∃y∈A. ⟨x,⟨y,succ(snd(x))⟩⟩ ∈ R"
  apply (rule ballI, rename_tac v)
  apply (frule Pair_fst_snd_eq)  
  apply (erule_tac x="fst(v)" in ballE)
   apply (drule_tac x="succ(snd(v))" in bspec, auto)
  done

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: "∀x∈A. ∀n∈nat. ∃y∈A. ⟨x,y⟩ ∈ S`n ⟹
    ∀a∈A. (∃f ∈ nat→A. f`0 = a ∧ (∀n ∈ nat. ⟨f`n,f`succ(n)⟩∈S`succ(n)))"
  apply (drule aux_sequence_DC2)
  apply (drule DC_on_A_x_nat, auto)
  done
end