# Theory DC

Up to index of Isabelle/ZF/AC

theory DC
imports AC_Equiv Hartog Cardinal_aux
begin

    (*  Title:      ZF/AC/DC.thy
        ID:         $Id: DC.thy,v 1.16 2005/06/17 14:15:10 haftmann Exp $
        Author:     Krzysztof Grabczewski

    The proofs concerning the Axiom of Dependent Choice
    *)

    theory DC imports AC_Equiv Hartog Cardinal_aux begin

    lemma RepFun_lepoll: "Ord(a) ==> {P(b). b ∈ a} \<lesssim> a"
    apply (unfold lepoll_def)
    apply (rule_tac x = "λz ∈ RepFun (a,P) . LEAST i. z=P (i) " in exI)
    apply (rule_tac d="%z. P (z)" in lam_injective)
     apply (fast intro!: Least_in_Ord)
    apply (rule sym)
    apply (fast intro: LeastI Ord_in_Ord)
    done

    text{*Trivial in the presence of AC, but here we need a wellordering of X*}
    lemma image_Ord_lepoll: "[| f ∈ X->Y; Ord(X) |] ==> f``X \<lesssim> X"
    apply (unfold lepoll_def)
    apply (rule_tac x = "λx ∈ f``X. LEAST y. f`y = x" in exI)
    apply (rule_tac d = "%z. f`z" in lam_injective)
    apply (fast intro!: Least_in_Ord apply_equality, clarify)
    apply (rule LeastI)
     apply (erule apply_equality, assumption+)
    apply (blast intro: Ord_in_Ord)
    done

    lemma range_subset_domain:
          "[| R ⊆ X*X;   !!g. g ∈ X ==> ∃u. <g,u> ∈ R |]
           ==> range(R) ⊆ domain(R)"
    by blast

    lemma cons_fun_type: "g ∈ n->X ==> cons(<n,x>, g) ∈ succ(n) -> cons(x, X)"
    apply (unfold succ_def)
    apply (fast intro!: fun_extend elim!: mem_irrefl)
    done

    lemma cons_fun_type2:
         "[| g ∈ n->X; x ∈ X |] ==> cons(<n,x>, g) ∈ succ(n) -> X"
    by (erule cons_absorb [THEN subst], erule cons_fun_type)

    lemma cons_image_n: "n ∈ nat ==> cons(<n,x>, g)``n = g``n"
    by (fast elim!: mem_irrefl)

    lemma cons_val_n: "g ∈ n->X ==> cons(<n,x>, g)`n = x"
    by (fast intro!: apply_equality elim!: cons_fun_type)

    lemma cons_image_k: "k ∈ n ==> cons(<n,x>, g)``k = g``k"
    by (fast elim: mem_asym)

    lemma cons_val_k: "[| k ∈ n; g ∈ n->X |] ==> cons(<n,x>, g)`k = g`k"
    by (fast intro!: apply_equality consI2 elim!: cons_fun_type apply_Pair)

    lemma domain_cons_eq_succ: "domain(f)=x ==> domain(cons(<x,y>, f)) = succ(x)"
    by (simp add: domain_cons succ_def)

    lemma restrict_cons_eq: "g ∈ n->X ==> restrict(cons(<n,x>, g), n) = g"
    apply (simp add: restrict_def Pi_iff)
    apply (blast intro: elim: mem_irrefl)
    done

    lemma succ_in_succ: "[| Ord(k); i ∈ k |] ==> succ(i) ∈ succ(k)"
    apply (rule Ord_linear [of "succ(i)" "succ(k)", THEN disjE])
    apply (fast elim: Ord_in_Ord mem_irrefl mem_asym)+
    done

    lemma restrict_eq_imp_val_eq:
          "[|restrict(f, domain(g)) = g; x ∈ domain(g)|]
           ==> f`x = g`x"
    by (erule subst, simp add: restrict)

    lemma domain_eq_imp_fun_type: "[| domain(f)=A; f ∈ B->C |] ==> f ∈ A->C"
    by (frule domain_of_fun, fast)

    lemma ex_in_domain: "[| R ⊆ A * B; R ≠ 0 |] ==> ∃x. x ∈ domain(R)"
    by (fast elim!: not_emptyE)

    constdefs

      DC  :: "i => o"
        "DC(a) == ∀X R. R ⊆ Pow(X)*X  &
                        (∀Y ∈ Pow(X). Y \<prec> a --> (∃x ∈ X. <Y,x> ∈ R))
                        --> (∃f ∈ a->X. ∀b<a. <f``b,f`b> ∈ R)"

      DC0 :: o
        "DC0 == ∀A B R. R ⊆ A*B & R≠0 & range(R) ⊆ domain(R)
                        --> (∃f ∈ nat->domain(R). ∀n ∈ nat. <f`n,f`succ(n)>:R)"

      ff  :: "[i, i, i, i] => i"
        "ff(b, X, Q, R) ==
               transrec(b, %c r. THE x. first(x, {x ∈ X. <r``c, x> ∈ R}, Q))"

    locale (open) DC0_imp =
      fixes XX and RR and X and R

      assumes all_ex: "∀Y ∈ Pow(X). Y \<prec> nat --> (∃x ∈ X. <Y, x> ∈ R)"

      defines XX_def: "XX == (\<Union>n ∈ nat. {f ∈ n->X. ∀k ∈ n. <f``k, f`k> ∈ R})"
         and RR_def:  "RR == {<z1,z2>:XX*XX. domain(z2)=succ(domain(z1))
                                           & restrict(z2, domain(z1)) = z1}"

    (* ********************************************************************** *)
    (* DC ==> DC(omega)                                                       *)
    (*                                                                        *)
    (* The scheme of the proof:                                               *)
    (*                                                                        *)
    (* Assume DC. Let R and X satisfy the premise of DC(omega).               *)
    (*                                                                        *)
    (* Define XX and RR as follows:                                           *)
    (*                                                                        *)
    (*       XX = (\<Union>n ∈ nat. {f ∈ n->X. ∀k ∈ n. <f``k, f`k> ∈ R})           *)
    (*       f RR g iff domain(g)=succ(domain(f)) &                           *)
    (*              restrict(g, domain(f)) = f                                *)
    (*                                                                        *)
    (* Then RR satisfies the hypotheses of DC.                                *)
    (* So applying DC:                                                        *)
    (*                                                                        *)
    (*       ∃f ∈ nat->XX. ∀n ∈ nat. f`n RR f`succ(n)                        *)
    (*                                                                        *)
    (* Thence                                                                 *)
    (*                                                                        *)
    (*       ff = {<n, f`succ(n)`n>. n ∈ nat}                                 *)
    (*                                                                        *)
    (* is the desired function.                                               *)
    (*                                                                        *)
    (* ********************************************************************** *)

    lemma (in DC0_imp) lemma1_1: "RR ⊆ XX*XX"
    by (unfold RR_def, fast)

    lemma (in DC0_imp) lemma1_2: "RR ≠ 0"
    apply (unfold RR_def XX_def)
    apply (rule all_ex [THEN ballE])
    apply (erule_tac [2] notE [OF _ empty_subsetI [THEN PowI]])
    apply (erule_tac impE [OF _ nat_0I [THEN n_lesspoll_nat]])
    apply (erule bexE)
    apply (rule_tac a = "<0, {<0, x>}>" in not_emptyI)
    apply (rule CollectI)
    apply (rule SigmaI)
    apply (rule nat_0I [THEN UN_I])
    apply (simp (no_asm_simp) add: nat_0I [THEN UN_I])
    apply (rule nat_1I [THEN UN_I])
    apply (force intro!: singleton_fun [THEN Pi_type]
                 simp add: singleton_0 [symmetric])
    apply (simp add: singleton_0)
    done

    lemma (in DC0_imp) lemma1_3: "range(RR) ⊆ domain(RR)"
    apply (unfold RR_def XX_def)
    apply (rule range_subset_domain, blast, clarify)
    apply (frule fun_is_rel [THEN image_subset, THEN PowI,
                             THEN all_ex [THEN bspec]])
    apply (erule impE[OF _ lesspoll_trans1[OF image_Ord_lepoll
                                              [OF _ nat_into_Ord] n_lesspoll_nat]],
           assumption+)
    apply (erule bexE)
    apply (rule_tac x = "cons (<n,x>, g) " in exI)
    apply (rule CollectI)
    apply (force elim!: cons_fun_type2
                 simp add: cons_image_n cons_val_n cons_image_k cons_val_k)
    apply (simp add: domain_of_fun succ_def restrict_cons_eq)
    done

    lemma (in DC0_imp) lemma2:
         "[| ∀n ∈ nat. <f`n, f`succ(n)> ∈ RR;  f ∈ nat -> XX;  n ∈ nat |]
          ==> ∃k ∈ nat. f`succ(n) ∈ k -> X & n ∈ k
                      & <f`succ(n)``n, f`succ(n)`n> ∈ R"
    apply (induct_tac "n")
    apply (drule apply_type [OF _ nat_1I])
    apply (drule bspec [OF _ nat_0I])
    apply (simp add: XX_def, safe)
    apply (rule rev_bexI, assumption)
    apply (subgoal_tac "0 ∈ y", force)
    apply (force simp add: RR_def
                 intro: ltD elim!: nat_0_le [THEN leE])
    (** LEVEL 7, other subgoal **)
    apply (drule bspec [OF _ nat_succI], assumption)
    apply (subgoal_tac "f ` succ (succ (x)) ∈ succ (k) ->X")
    apply (drule apply_type [OF _ nat_succI [THEN nat_succI]], assumption)
    apply (simp (no_asm_use) add: XX_def RR_def)
    apply safe
    apply (frule_tac a="succ(k)" in domain_of_fun [symmetric, THEN trans],
           assumption)
    apply (frule_tac a=y in domain_of_fun [symmetric, THEN trans],
           assumption)
    apply (fast elim!: nat_into_Ord [THEN succ_in_succ]
                dest!: bspec [OF _ nat_into_Ord [THEN succ_in_succ]])
    apply (drule domain_of_fun)
    apply (simp add: XX_def RR_def, clarify)
    apply (blast dest: domain_of_fun [symmetric, THEN trans] )
    done

    lemma (in DC0_imp) lemma3_1:
         "[| ∀n ∈ nat. <f`n, f`succ(n)> ∈ RR;  f ∈ nat -> XX;  m ∈ nat |]
          ==>  {f`succ(x)`x. x ∈ m} = {f`succ(m)`x. x ∈ m}"
    apply (subgoal_tac "∀x ∈ m. f`succ (m) `x = f`succ (x) `x")
    apply simp
    apply (induct_tac "m", blast)
    apply (rule ballI)
    apply (erule succE)
     apply (rule restrict_eq_imp_val_eq)
      apply (drule bspec [OF _ nat_succI], assumption)
      apply (simp add: RR_def)
     apply (drule lemma2, assumption+)
     apply (fast dest!: domain_of_fun)
    apply (drule_tac x = xa in bspec, assumption)
    apply (erule sym [THEN trans, symmetric])
    apply (rule restrict_eq_imp_val_eq [symmetric])
     apply (drule bspec [OF _ nat_succI], assumption)
     apply (simp add: RR_def)
    apply (drule lemma2, assumption+)
    apply (blast dest!: domain_of_fun
                 intro: nat_into_Ord OrdmemD [THEN subsetD])
    done

    lemma (in DC0_imp) lemma3:
         "[| ∀n ∈ nat. <f`n, f`succ(n)> ∈ RR;  f ∈ nat -> XX;  m ∈ nat |]
          ==> (λx ∈ nat. f`succ(x)`x) `` m = f`succ(m)``m"
    apply (erule natE, simp)
    apply (subst image_lam)
     apply (fast elim!: OrdmemD [OF nat_succI Ord_nat])
    apply (subst lemma3_1, assumption+)
     apply fast
    apply (fast dest!: lemma2
                elim!: image_fun [symmetric, OF _ OrdmemD [OF _ nat_into_Ord]])
    done

    theorem DC0_imp_DC_nat: "DC0 ==> DC(nat)"
    apply (unfold DC_def DC0_def, clarify)
    apply (elim allE)
    apply (erule impE)
       (*these three results comprise Lemma 1*)
    apply (blast intro!: DC0_imp.lemma1_1 DC0_imp.lemma1_2 DC0_imp.lemma1_3)
    apply (erule bexE)
    apply (rule_tac x = "λn ∈ nat. f`succ (n) `n" in rev_bexI)
     apply (rule lam_type, blast dest!: DC0_imp.lemma2 intro: fun_weaken_type)
    apply (rule oallI)
    apply (frule DC0_imp.lemma2, assumption)
      apply (blast intro: fun_weaken_type)
     apply (erule ltD)
    (** LEVEL 11: last subgoal **)
    apply (subst DC0_imp.lemma3, assumption+)
      apply (fast elim!: fun_weaken_type)
     apply (erule ltD)
    apply (force simp add: lt_def)
    done

    (* ************************************************************************
       DC(omega) ==> DC

       The scheme of the proof:

       Assume DC(omega). Let R and x satisfy the premise of DC.

       Define XX and RR as follows:

        XX = (\<Union>n ∈ nat. {f ∈ succ(n)->domain(R). ∀k ∈ n. <f`k, f`succ(k)> ∈ R})

        RR = {<z1,z2>:Fin(XX)*XX.
               (domain(z2)=succ(\<Union>f ∈ z1. domain(f)) &
                (∀f ∈ z1. restrict(z2, domain(f)) = f)) |
               (~ (∃g ∈ XX. domain(g)=succ(\<Union>f ∈ z1. domain(f)) &
                            (∀f ∈ z1. restrict(g, domain(f)) = f)) &
                z2={<0,x>})}

       Then XX and RR satisfy the hypotheses of DC(omega).
       So applying DC:

             ∃f ∈ nat->XX. ∀n ∈ nat. f``n RR f`n

       Thence

             ff = {<n, f`n`n>. n ∈ nat}

       is the desired function.

    ************************************************************************* *)

    lemma singleton_in_funs:
     "x ∈ X ==> {<0,x>} ∈
                (\<Union>n ∈ nat. {f ∈ succ(n)->X. ∀k ∈ n. <f`k, f`succ(k)> ∈ R})"
    apply (rule nat_0I [THEN UN_I])
    apply (force simp add: singleton_0 [symmetric]
                 intro!: singleton_fun [THEN Pi_type])
    done

    locale (open) imp_DC0 =
      fixes XX and RR and x and R and f and allRR
      defines XX_def: "XX == (\<Union>n ∈ nat.
                          {f ∈ succ(n)->domain(R). ∀k ∈ n. <f`k, f`succ(k)> ∈ R})"
          and RR_def:
             "RR == {<z1,z2>:Fin(XX)*XX.
                      (domain(z2)=succ(\<Union>f ∈ z1. domain(f))
                        & (∀f ∈ z1. restrict(z2, domain(f)) = f))
                      | (~ (∃g ∈ XX. domain(g)=succ(\<Union>f ∈ z1. domain(f))
                         & (∀f ∈ z1. restrict(g, domain(f)) = f)) & z2={<0,x>})}"
          and allRR_def:
            "allRR == ∀b<nat.
                       <f``b, f`b> ∈
                        {<z1,z2>∈Fin(XX)*XX. (domain(z2)=succ(\<Union>f ∈ z1. domain(f))
                                        & (\<Union>f ∈ z1. domain(f)) = b
                                        & (∀f ∈ z1. restrict(z2,domain(f)) = f))}"

    lemma (in imp_DC0) lemma4:
         "[| range(R) ⊆ domain(R);  x ∈ domain(R) |]
          ==> RR ⊆ Pow(XX)*XX &
                 (∀Y ∈ Pow(XX). Y \<prec> nat --> (∃x ∈ XX. <Y,x>:RR))"
    apply (rule conjI)
    apply (force dest!: FinD [THEN PowI] simp add: RR_def)
    apply (rule impI [THEN ballI])
    apply (drule Finite_Fin [OF lesspoll_nat_is_Finite PowD], assumption)
    apply (case_tac
           "∃g ∈ XX. domain (g) =
                 succ(\<Union>f ∈ Y. domain(f)) & (∀f∈Y. restrict(g, domain(f)) = f)")
    apply (simp add: RR_def, blast)
    apply (safe del: domainE)
    apply (unfold XX_def RR_def)
    apply (rule rev_bexI, erule singleton_in_funs)
    apply (simp add: nat_0I [THEN rev_bexI] cons_fun_type2)
    done

    lemma (in imp_DC0) UN_image_succ_eq:
         "[| f ∈ nat->X; n ∈ nat |]
          ==> (\<Union>x ∈ f``succ(n). P(x)) =  P(f`n) Un (\<Union>x ∈ f``n. P(x))"
    by (simp add: image_fun OrdmemD)

    lemma (in imp_DC0) UN_image_succ_eq_succ:
         "[| (\<Union>x ∈ f``n. P(x)) = y; P(f`n) = succ(y);
             f ∈ nat -> X; n ∈ nat |] ==> (\<Union>x ∈ f``succ(n). P(x)) = succ(y)"
    by (simp add: UN_image_succ_eq, blast)

    lemma (in imp_DC0) apply_domain_type:
         "[| h ∈ succ(n) -> D;  n ∈ nat; domain(h)=succ(y) |] ==> h`y ∈ D"
    by (fast elim: apply_type dest!: trans [OF sym domain_of_fun])

    lemma (in imp_DC0) image_fun_succ:
         "[| h ∈ nat -> X; n ∈ nat |] ==> h``succ(n) = cons(h`n, h``n)"
    by (simp add: image_fun OrdmemD)

    lemma (in imp_DC0) f_n_type:
         "[| domain(f`n) = succ(k); f ∈ nat -> XX;  n ∈ nat |]
          ==> f`n ∈ succ(k) -> domain(R)"
    apply (unfold XX_def)
    apply (drule apply_type, assumption)
    apply (fast elim: domain_eq_imp_fun_type)
    done

    lemma (in imp_DC0) f_n_pairs_in_R [rule_format]:
         "[| h ∈ nat -> XX;  domain(h`n) = succ(k);  n ∈ nat |]
          ==> ∀i ∈ k. <h`n`i, h`n`succ(i)> ∈ R"
    apply (unfold XX_def)
    apply (drule apply_type, assumption)
    apply (elim UN_E CollectE)
    apply (drule domain_of_fun [symmetric, THEN trans], assumption, simp)
    done

    lemma (in imp_DC0) restrict_cons_eq_restrict:
         "[| restrict(h, domain(u))=u;  h ∈ n->X;  domain(u) ⊆ n |]
          ==> restrict(cons(<n, y>, h), domain(u)) = u"
    apply (unfold restrict_def)
    apply (simp add: restrict_def Pi_iff)
    apply (erule sym [THEN trans, symmetric])
    apply (blast elim: mem_irrefl)
    done

    lemma (in imp_DC0) all_in_image_restrict_eq:
         "[| ∀x ∈ f``n. restrict(f`n, domain(x))=x;
             f ∈ nat -> XX;
             n ∈ nat;  domain(f`n) = succ(n);
             (\<Union>x ∈ f``n. domain(x)) ⊆ n |]
          ==> ∀x ∈ f``succ(n). restrict(cons(<succ(n),y>, f`n), domain(x)) = x"
    apply (rule ballI)
    apply (simp add: image_fun_succ)
    apply (drule f_n_type, assumption+)
    apply (erule disjE)
     apply (simp add: domain_of_fun restrict_cons_eq)
    apply (blast intro!: restrict_cons_eq_restrict)
    done

    lemma (in imp_DC0) simplify_recursion:
         "[| ∀b<nat. <f``b, f`b> ∈ RR;
             f ∈ nat -> XX; range(R) ⊆ domain(R); x ∈ domain(R)|]
          ==> allRR"
    apply (unfold RR_def allRR_def)
    apply (rule oallI, drule ltD)
    apply (erule nat_induct)
    apply (drule_tac x=0 in ospec, blast intro: Limit_has_0)
    apply (force simp add: singleton_fun [THEN domain_of_fun] singleton_in_funs)
    (*induction step*) (** LEVEL 5 **)
    (*prevent simplification of ~∃ to ∀~ *)
    apply (simp only: separation split)
    apply (drule_tac x="succ(xa)" in ospec, blast intro: ltI)
    apply (elim conjE disjE)
    apply (force elim!: trans subst_context
                 intro!: UN_image_succ_eq_succ)
    apply (erule notE)
    apply (simp add: XX_def UN_image_succ_eq_succ)
    apply (elim conjE bexE)
    apply (drule apply_domain_type, assumption+)
    apply (erule domainE)+
    apply (frule f_n_type)
    apply (simp add: XX_def, assumption+)
    apply (rule rev_bexI, erule nat_succI)
    apply (rename_tac m i j y z)
    apply (rule_tac x = "cons(<succ(m), z>, f`m)" in bexI)
    prefer 2 apply (blast intro: cons_fun_type2)
    apply (rule conjI)
    prefer 2 apply (fast del: ballI subsetI
                     elim: trans [OF _ subst_context, THEN domain_cons_eq_succ]
                           subst_context
                           all_in_image_restrict_eq [simplified XX_def]
                           trans equalityD1)
    (*one remaining subgoal*)
    apply (rule ballI)
    apply (erule succE)
    (** LEVEL 25 **)
     apply (simp add: cons_val_n cons_val_k)
    (*assumption+ will not perform the required backtracking!*)
    apply (drule f_n_pairs_in_R [simplified XX_def, OF _ domain_of_fun],
           assumption, assumption, assumption)
    apply (simp add: nat_into_Ord [THEN succ_in_succ] succI2 cons_val_k)
    done

    lemma (in imp_DC0) lemma2:
         "[| allRR; f ∈ nat->XX; range(R) ⊆ domain(R); x ∈ domain(R); n ∈ nat |]
          ==> f`n ∈ succ(n) -> domain(R) & (∀i ∈ n. <f`n`i, f`n`succ(i)>:R)"
    apply (unfold allRR_def)
    apply (drule ospec)
    apply (erule ltI [OF _ Ord_nat])
    apply (erule CollectE, simp)
    apply (rule conjI)
    prefer 2 apply (fast elim!: f_n_pairs_in_R trans subst_context)
    apply (unfold XX_def)
    apply (fast elim!: trans [THEN domain_eq_imp_fun_type] subst_context)
    done

    lemma (in imp_DC0) lemma3:
         "[| allRR; f ∈ nat->XX; n∈nat; range(R) ⊆ domain(R);  x ∈ domain(R) |]
          ==> f`n`n = f`succ(n)`n"
    apply (frule lemma2 [THEN conjunct1, THEN domain_of_fun], assumption+)
    apply (unfold allRR_def)
    apply (drule ospec)
    apply (drule ltI [OF nat_succI Ord_nat], assumption, simp)
    apply (elim conjE ballE)
    apply (erule restrict_eq_imp_val_eq [symmetric], force)
    apply (simp add: image_fun OrdmemD)
    done

    theorem DC_nat_imp_DC0: "DC(nat) ==> DC0"
    apply (unfold DC_def DC0_def)
    apply (intro allI impI)
    apply (erule asm_rl conjE ex_in_domain [THEN exE] allE)+
    apply (erule impE [OF _ imp_DC0.lemma4], assumption+)
    apply (erule bexE)
    apply (drule imp_DC0.simplify_recursion, assumption+)
    apply (rule_tac x = "λn ∈ nat. f`n`n" in bexI)
    apply (rule_tac [2] lam_type)
    apply (erule_tac [2] apply_type [OF imp_DC0.lemma2 [THEN conjunct1] succI1])
    apply (rule ballI)
    apply (frule_tac n="succ(n)" in imp_DC0.lemma2,
           (assumption|erule nat_succI)+)
    apply (drule imp_DC0.lemma3, auto)
    done

    (* ********************************************************************** *)
    (* ∀K. Card(K) --> DC(K) ==> WO3                                       *)
    (* ********************************************************************** *)

    lemma fun_Ord_inj:
          "[| f ∈ a->X;  Ord(a);
              !!b c. [| b<c; c ∈ a |] ==> f`b≠f`c |]
           ==> f ∈ inj(a, X)"
    apply (unfold inj_def, simp)
    apply (intro ballI impI)
    apply (rule_tac j=x in Ord_in_Ord [THEN Ord_linear_lt], assumption+)
    apply (blast intro: Ord_in_Ord, auto)
    apply (atomize, blast dest: not_sym)
    done

    lemma value_in_image: "[| f ∈ X->Y; A ⊆ X; a ∈ A |] ==> f`a ∈ f``A"
    by (fast elim!: image_fun [THEN ssubst])

    theorem DC_WO3: "(∀K. Card(K) --> DC(K)) ==> WO3"
    apply (unfold DC_def WO3_def)
    apply (rule allI)
    apply (case_tac "A \<prec> Hartog (A)")
    apply (fast dest!: lesspoll_imp_ex_lt_eqpoll
                intro!: Ord_Hartog leI [THEN le_imp_subset])
    apply (erule allE impE)+
    apply (rule Card_Hartog)
    apply (erule_tac x = A in allE)
    apply (erule_tac x = "{<z1,z2> ∈ Pow (A) *A . z1 \<prec> Hartog (A) & z2 ∉ z1}"
                     in allE)
    apply simp
    apply (erule impE, fast elim: lesspoll_lemma [THEN not_emptyE])
    apply (erule bexE)
    apply (rule Hartog_lepoll_selfE)
    apply (rule lepoll_def [THEN def_imp_iff, THEN iffD2])
    apply (rule exI, rule fun_Ord_inj, assumption, rule Ord_Hartog)
    apply (drule value_in_image)
    apply (drule OrdmemD, rule Ord_Hartog, assumption+, erule ltD)
    apply (drule ospec)
    apply (blast intro: ltI Ord_Hartog, force)
    done

    (* ********************************************************************** *)
    (* WO1 ==> ∀K. Card(K) --> DC(K)                                       *)
    (* ********************************************************************** *)

    lemma images_eq:
         "[| ∀x ∈ A. f`x=g`x; f ∈ Df->Cf; g ∈ Dg->Cg; A ⊆ Df; A ⊆ Dg |]
          ==> f``A = g``A"
    apply (simp (no_asm_simp) add: image_fun)
    done

    lemma lam_images_eq:
         "[| Ord(a); b ∈ a |] ==> (λx ∈ a. h(x))``b = (λx ∈ b. h(x))``b"
    apply (rule images_eq)
        apply (rule ballI)
        apply (drule OrdmemD [THEN subsetD], assumption+)
        apply simp
       apply (fast elim!: RepFunI OrdmemD intro!: lam_type)+
    done

    lemma lam_type_RepFun: "(λb ∈ a. h(b)) ∈ a -> {h(b). b ∈ a}"
    by (fast intro!: lam_type RepFunI)

    lemma lemmaX:
         "[| ∀Y ∈ Pow(X). Y \<prec> K --> (∃x ∈ X. <Y, x> ∈ R);
             b ∈ K; Z ∈ Pow(X); Z \<prec> K |]
          ==> {x ∈ X. <Z,x> ∈ R} ≠ 0"
    by blast

    lemma WO1_DC_lemma:
         "[| Card(K); well_ord(X,Q);
             ∀Y ∈ Pow(X). Y \<prec> K --> (∃x ∈ X. <Y, x> ∈ R); b ∈ K |]
          ==> ff(b, X, Q, R) ∈ {x ∈ X. <(λc ∈ b. ff(c, X, Q, R))``b, x> ∈ R}"
    apply (rule_tac P = "b ∈ K" in impE, (erule_tac [2] asm_rl)+)
    apply (rule_tac i=b in Card_is_Ord [THEN Ord_in_Ord, THEN trans_induct],
           assumption+)
    apply (rule impI)
    apply (rule ff_def [THEN def_transrec, THEN ssubst])
    apply (erule the_first_in, fast)
    apply (simp add: image_fun [OF lam_type_RepFun subset_refl])
    apply (erule lemmaX, assumption)
     apply (blast intro: Card_is_Ord OrdmemD [THEN subsetD])
    apply (blast intro: lesspoll_trans1 in_Card_imp_lesspoll RepFun_lepoll)
    done

    theorem WO1_DC_Card: "WO1 ==> ∀K. Card(K) --> DC(K)"
    apply (unfold DC_def WO1_def)
    apply (rule allI impI)+
    apply (erule allE exE conjE)+
    apply (rule_tac x = "λb ∈ K. ff (b, X, Ra, R) " in bexI)
     apply (simp add: lam_images_eq [OF Card_is_Ord ltD])
     apply (fast elim!: ltE WO1_DC_lemma [THEN CollectD2])
    apply (rule_tac lam_type)
    apply (rule WO1_DC_lemma [THEN CollectD1], assumption+)
    done

    end

lemma RepFun_lepoll:

      Ord(a) ==> {P(b) . b ∈ a} lepoll a

lemma image_Ord_lepoll:

      [| f ∈ X -> Y; Ord(X) |] ==> f `` X lepoll X

lemma range_subset_domain:

      [| R ⊆ X × X; !!g. g ∈ X ==> ∃u. ⟨g, u⟩ ∈ R |] ==> range(R) ⊆ domain(R)

lemma cons_fun_type:

      g ∈ n -> X ==> cons(⟨n, x⟩, g) ∈ succ(n) -> cons(x, X)

lemma cons_fun_type2:

      [| g ∈ n -> X; x ∈ X |] ==> cons(⟨n, x⟩, g) ∈ succ(n) -> X

lemma cons_image_n:

      n ∈ nat ==> cons(⟨n, x⟩, g) `` n = g `` n

lemma cons_val_n:

      g ∈ n -> X ==> cons(⟨n, x⟩, g) ` n = x

lemma cons_image_k:

      k ∈ n ==> cons(⟨n, x⟩, g) `` k = g `` k

lemma cons_val_k:

      [| k ∈ n; g ∈ n -> X |] ==> cons(⟨n, x⟩, g) ` k = g ` k

lemma domain_cons_eq_succ:

      domain(f) = x ==> domain(cons(⟨x, y⟩, f)) = succ(x)

lemma restrict_cons_eq:

      g ∈ n -> X ==> restrict(cons(⟨n, x⟩, g), n) = g

lemma succ_in_succ:

      [| Ord(k); i ∈ k |] ==> succ(i) ∈ succ(k)

lemma restrict_eq_imp_val_eq:

      [| restrict(f, domain(g)) = g; x ∈ domain(g) |] ==> f ` x = g ` x

lemma domain_eq_imp_fun_type:

      [| domain(f) = A; f ∈ B -> C |] ==> f ∈ A -> C

lemma ex_in_domain:

      [| R ⊆ A × B; R ≠ 0 |] ==> ∃x. x ∈ domain(R)

lemma lemma1_1:

      ∀Y∈Pow(X). Y lesspoll nat --> (∃x∈X. ⟨Y, x⟩ ∈ R)
      ==> {⟨z1,z2⟩ ∈ (\<Union>n∈nat. {f ∈ n -> X . ∀k∈n. ⟨f `` k, f ` k⟩ ∈ R}) ×
                     (\<Union>n∈nat. {f ∈ n -> X . ∀k∈n. ⟨f `` k, f ` k⟩ ∈ R}) .
           domain(z2) = succ(domain(z1)) ∧ restrict(z2, domain(z1)) = z1} ⊆
          (\<Union>n∈nat. {f ∈ n -> X . ∀k∈n. ⟨f `` k, f ` k⟩ ∈ R}) ×
          (\<Union>n∈nat. {f ∈ n -> X . ∀k∈n. ⟨f `` k, f ` k⟩ ∈ R})

lemma lemma1_2:

      ∀Y∈Pow(X). Y lesspoll nat --> (∃x∈X. ⟨Y, x⟩ ∈ R)
      ==> {⟨z1,z2⟩ ∈ (\<Union>n∈nat. {f ∈ n -> X . ∀k∈n. ⟨f `` k, f ` k⟩ ∈ R}) ×
                     (\<Union>n∈nat. {f ∈ n -> X . ∀k∈n. ⟨f `` k, f ` k⟩ ∈ R}) .
           domain(z2) = succ(domain(z1)) ∧ restrict(z2, domain(z1)) = z1} ≠
          0

lemma lemma1_3:

      ∀Y∈Pow(X). Y lesspoll nat --> (∃x∈X. ⟨Y, x⟩ ∈ R)
      ==> range({⟨z1,z2⟩ ∈ (\<Union>n∈nat. {f ∈ n -> X . ∀k∈n. ⟨f `` k, f ` k⟩ ∈ R}) ×
                           (\<Union>n∈nat. {f ∈ n -> X . ∀k∈n. ⟨f `` k, f ` k⟩ ∈ R}) .
                 domain(z2) = succ(domain(z1)) ∧ restrict(z2, domain(z1)) = z1}) ⊆
          domain
           ({⟨z1,z2⟩ ∈ (\<Union>n∈nat. {f ∈ n -> X . ∀k∈n. ⟨f `` k, f ` k⟩ ∈ R}) ×
                       (\<Union>n∈nat. {f ∈ n -> X . ∀k∈n. ⟨f `` k, f ` k⟩ ∈ R}) .
             domain(z2) = succ(domain(z1)) ∧ restrict(z2, domain(z1)) = z1})

lemma lemma2:

      [| ∀Y∈Pow(X). Y lesspoll nat --> (∃x∈X. ⟨Y, x⟩ ∈ R);
         ∀n∈nat.
            ⟨f ` n, f ` succ(n)⟩ ∈
            {⟨z1,z2⟩ ∈ (\<Union>n∈nat. {f ∈ n -> X . ∀k∈n. ⟨f `` k, f ` k⟩ ∈ R}) ×
                       (\<Union>n∈nat. {f ∈ n -> X . ∀k∈n. ⟨f `` k, f ` k⟩ ∈ R}) .
             domain(z2) = succ(domain(z1)) ∧ restrict(z2, domain(z1)) = z1};
         f ∈ nat -> (\<Union>n∈nat. {f ∈ n -> X . ∀k∈n. ⟨f `` k, f ` k⟩ ∈ R});
         n ∈ nat |]
      ==> ∃k∈nat.
             f ` succ(n) ∈ k -> X ∧ n ∈ k ∧ ⟨f ` succ(n) `` n, f ` succ(n) ` n⟩ ∈ R

lemma lemma3_1:

      [| ∀Y∈Pow(X). Y lesspoll nat --> (∃x∈X. ⟨Y, x⟩ ∈ R);
         ∀n∈nat.
            ⟨f ` n, f ` succ(n)⟩ ∈
            {⟨z1,z2⟩ ∈ (\<Union>n∈nat. {f ∈ n -> X . ∀k∈n. ⟨f `` k, f ` k⟩ ∈ R}) ×
                       (\<Union>n∈nat. {f ∈ n -> X . ∀k∈n. ⟨f `` k, f ` k⟩ ∈ R}) .
             domain(z2) = succ(domain(z1)) ∧ restrict(z2, domain(z1)) = z1};
         f ∈ nat -> (\<Union>n∈nat. {f ∈ n -> X . ∀k∈n. ⟨f `` k, f ` k⟩ ∈ R});
         m ∈ nat |]
      ==> {f ` succ(x) ` x . x ∈ m} = {f ` succ(m) ` x . x ∈ m}

lemma lemma3:

      [| ∀Y∈Pow(X). Y lesspoll nat --> (∃x∈X. ⟨Y, x⟩ ∈ R);
         ∀n∈nat.
            ⟨f ` n, f ` succ(n)⟩ ∈
            {⟨z1,z2⟩ ∈ (\<Union>n∈nat. {f ∈ n -> X . ∀k∈n. ⟨f `` k, f ` k⟩ ∈ R}) ×
                       (\<Union>n∈nat. {f ∈ n -> X . ∀k∈n. ⟨f `` k, f ` k⟩ ∈ R}) .
             domain(z2) = succ(domain(z1)) ∧ restrict(z2, domain(z1)) = z1};
         f ∈ nat -> (\<Union>n∈nat. {f ∈ n -> X . ∀k∈n. ⟨f `` k, f ` k⟩ ∈ R});
         m ∈ nat |]
      ==> (λx∈nat. f ` succ(x) ` x) `` m = f ` succ(m) `` m

theorem DC0_imp_DC_nat:

      DC0 ==> DC(nat)

lemma singleton_in_funs:

      x ∈ X
      ==> {⟨0, x⟩} ∈
          (\<Union>n∈nat. {f ∈ succ(n) -> X . ∀k∈n. ⟨f ` k, f ` succ(k)⟩ ∈ R})

lemma lemma4:

      [| range(R) ⊆ domain(R); x ∈ domain(R) |]
      ==> {⟨z1,z2⟩ ∈ Fin(\<Union>n∈nat.
                            {f ∈ succ(n) -> domain(R) .
                             ∀k∈n. ⟨f ` k, f ` succ(k)⟩ ∈ R}) ×
                     (\<Union>n∈nat.
                         {f ∈ succ(n) -> domain(R) .
                          ∀k∈n. ⟨f ` k, f ` succ(k)⟩ ∈ R}) .
           domain(z2) = succ(\<Union>f∈z1. domain(f)) ∧
           (∀f∈z1. restrict(z2, domain(f)) = f) ∨
           ¬ (∃g∈\<Union>n∈nat.
                    {f ∈ succ(n) -> domain(R) . ∀k∈n. ⟨f ` k, f ` succ(k)⟩ ∈ R}.
                 domain(g) = succ(\<Union>f∈z1. domain(f)) ∧
                 (∀f∈z1. restrict(g, domain(f)) = f)) ∧
           z2 = {⟨0, x⟩}} ⊆
          Pow(\<Union>n∈nat.
                 {f ∈ succ(n) -> domain(R) . ∀k∈n. ⟨f ` k, f ` succ(k)⟩ ∈ R}) ×
          (\<Union>n∈nat.
              {f ∈ succ(n) -> domain(R) . ∀k∈n. ⟨f ` k, f ` succ(k)⟩ ∈ R}) ∧
          (∀Y∈Pow(\<Union>n∈nat.
                     {f ∈ succ(n) -> domain(R) . ∀k∈n. ⟨f ` k, f ` succ(k)⟩ ∈ R}).
              Y lesspoll nat -->
              (∃x∈\<Union>n∈nat.
                     {f ∈ succ(n) -> domain(R) . ∀k∈n. ⟨f ` k, f ` succ(k)⟩ ∈ R}.
                  ⟨Y, x⟩ ∈
                  {⟨z1,z2⟩ ∈ Fin(\<Union>n∈nat.
                                    {f ∈ succ(n) -> domain(R) .
                                     ∀k∈n. ⟨f ` k, f ` succ(k)⟩ ∈ R}) ×
                             (\<Union>n∈nat.
                                 {f ∈ succ(n) -> domain(R) .
                                  ∀k∈n. ⟨f ` k, f ` succ(k)⟩ ∈ R}) .
                   domain(z2) = succ(\<Union>f∈z1. domain(f)) ∧
                   (∀f∈z1. restrict(z2, domain(f)) = f) ∨
                   ¬ (∃g∈\<Union>n∈nat.
                            {f ∈ succ(n) -> domain(R) .
                             ∀k∈n. ⟨f ` k, f ` succ(k)⟩ ∈ R}.
                         domain(g) = succ(\<Union>f∈z1. domain(f)) ∧
                         (∀f∈z1. restrict(g, domain(f)) = f)) ∧
                   z2 = {⟨0, x⟩}}))

lemma UN_image_succ_eq:

      [| f ∈ nat -> X; n ∈ nat |]
      ==> (\<Union>x∈f `` succ(n). P(x)) = P(f ` n) ∪ (\<Union>x∈f `` n. P(x))

lemma UN_image_succ_eq_succ:

      [| (\<Union>x∈f `` n. P(x)) = y; P(f ` n) = succ(y); f ∈ nat -> X; n ∈ nat |]
      ==> (\<Union>x∈f `` succ(n). P(x)) = succ(y)

lemma apply_domain_type:

      [| h ∈ succ(n) -> D; n ∈ nat; domain(h) = succ(y) |] ==> h ` y ∈ D

lemma image_fun_succ:

      [| h ∈ nat -> X; n ∈ nat |] ==> h `` succ(n) = cons(h ` n, h `` n)

lemma f_n_type:

      [| domain(f ` n) = succ(k);
         f ∈ nat ->
             (\<Union>n∈nat.
                 {f ∈ succ(n) -> domain(R) . ∀k∈n. ⟨f ` k, f ` succ(k)⟩ ∈ R});
         n ∈ nat |]
      ==> f ` n ∈ succ(k) -> domain(R)

lemma f_n_pairs_in_R:

      [| h ∈ nat ->
             (\<Union>n∈nat.
                 {f ∈ succ(n) -> domain(R) . ∀k∈n. ⟨f ` k, f ` succ(k)⟩ ∈ R});
         domain(h ` n) = succ(k); n ∈ nat |]
      ==> ∀i∈k. ⟨h ` n ` i, h ` n ` succ(i)⟩ ∈ R

lemma restrict_cons_eq_restrict:

      [| restrict(h, domain(u)) = u; h ∈ n -> X; domain(u) ⊆ n |]
      ==> restrict(cons(⟨n, y⟩, h), domain(u)) = u

lemma all_in_image_restrict_eq:

      [| ∀x∈f `` n. restrict(f ` n, domain(x)) = x;
         f ∈ nat ->
             (\<Union>n∈nat.
                 {f ∈ succ(n) -> domain(R) . ∀k∈n. ⟨f ` k, f ` succ(k)⟩ ∈ R});
         n ∈ nat; domain(f ` n) = succ(n); (\<Union>x∈f `` n. domain(x)) ⊆ n |]
      ==> ∀x∈f `` succ(n). restrict(cons(⟨succ(n), y⟩, f ` n), domain(x)) = x

lemma simplify_recursion:

      [| ∀b<nat.
            ⟨f `` b, f ` b⟩ ∈
            {⟨z1,z2⟩ ∈ Fin(\<Union>n∈nat.
                              {f ∈ succ(n) -> domain(R) .
                               ∀k∈n. ⟨f ` k, f ` succ(k)⟩ ∈ R}) ×
                       (\<Union>n∈nat.
                           {f ∈ succ(n) -> domain(R) .
                            ∀k∈n. ⟨f ` k, f ` succ(k)⟩ ∈ R}) .
             domain(z2) = succ(\<Union>f∈z1. domain(f)) ∧
             (∀f∈z1. restrict(z2, domain(f)) = f) ∨
             ¬ (∃g∈\<Union>n∈nat.
                      {f ∈ succ(n) -> domain(R) . ∀k∈n. ⟨f ` k, f ` succ(k)⟩ ∈ R}.
                   domain(g) = succ(\<Union>f∈z1. domain(f)) ∧
                   (∀f∈z1. restrict(g, domain(f)) = f)) ∧
             z2 = {⟨0, x⟩}};
         f ∈ nat ->
             (\<Union>n∈nat.
                 {f ∈ succ(n) -> domain(R) . ∀k∈n. ⟨f ` k, f ` succ(k)⟩ ∈ R});
         range(R) ⊆ domain(R); x ∈ domain(R) |]
      ==> ∀b<nat.
             ⟨f `` b, f ` b⟩ ∈
             {⟨z1,z2⟩ ∈ Fin(\<Union>n∈nat.
                               {f ∈ succ(n) -> domain(R) .
                                ∀k∈n. ⟨f ` k, f ` succ(k)⟩ ∈ R}) ×
                        (\<Union>n∈nat.
                            {f ∈ succ(n) -> domain(R) .
                             ∀k∈n. ⟨f ` k, f ` succ(k)⟩ ∈ R}) .
              domain(z2) = succ(\<Union>f∈z1. domain(f)) ∧
              (\<Union>f∈z1. domain(f)) = b ∧ (∀f∈z1. restrict(z2, domain(f)) = f)}

lemma lemma2:

      [| ∀b<nat.
            ⟨f `` b, f ` b⟩ ∈
            {⟨z1,z2⟩ ∈ Fin(\<Union>n∈nat.
                              {f ∈ succ(n) -> domain(R) .
                               ∀k∈n. ⟨f ` k, f ` succ(k)⟩ ∈ R}) ×
                       (\<Union>n∈nat.
                           {f ∈ succ(n) -> domain(R) .
                            ∀k∈n. ⟨f ` k, f ` succ(k)⟩ ∈ R}) .
             domain(z2) = succ(\<Union>f∈z1. domain(f)) ∧
             (\<Union>f∈z1. domain(f)) = b ∧ (∀f∈z1. restrict(z2, domain(f)) = f)};
         f ∈ nat ->
             (\<Union>n∈nat.
                 {f ∈ succ(n) -> domain(R) . ∀k∈n. ⟨f ` k, f ` succ(k)⟩ ∈ R});
         range(R) ⊆ domain(R); x ∈ domain(R); n ∈ nat |]
      ==> f ` n ∈ succ(n) -> domain(R) ∧ (∀i∈n. ⟨f ` n ` i, f ` n ` succ(i)⟩ ∈ R)

lemma lemma3:

      [| ∀b<nat.
            ⟨f `` b, f ` b⟩ ∈
            {⟨z1,z2⟩ ∈ Fin(\<Union>n∈nat.
                              {f ∈ succ(n) -> domain(R) .
                               ∀k∈n. ⟨f ` k, f ` succ(k)⟩ ∈ R}) ×
                       (\<Union>n∈nat.
                           {f ∈ succ(n) -> domain(R) .
                            ∀k∈n. ⟨f ` k, f ` succ(k)⟩ ∈ R}) .
             domain(z2) = succ(\<Union>f∈z1. domain(f)) ∧
             (\<Union>f∈z1. domain(f)) = b ∧ (∀f∈z1. restrict(z2, domain(f)) = f)};
         f ∈ nat ->
             (\<Union>n∈nat.
                 {f ∈ succ(n) -> domain(R) . ∀k∈n. ⟨f ` k, f ` succ(k)⟩ ∈ R});
         n ∈ nat; range(R) ⊆ domain(R); x ∈ domain(R) |]
      ==> f ` n ` n = f ` succ(n) ` n

theorem DC_nat_imp_DC0:

      DC(nat) ==> DC0

lemma fun_Ord_inj:

      [| f ∈ a -> X; Ord(a); !!b c. [| b < c; c ∈ a |] ==> f ` b ≠ f ` c |]
      ==> f ∈ inj(a, X)

lemma value_in_image:

      [| f ∈ X -> Y; A ⊆ X; a ∈ A |] ==> f ` a ∈ f `` A

theorem DC_WO3:

      ∀K. Card(K) --> DC(K) ==> WO3

lemma images_eq:

      [| ∀x∈A. f ` x = g ` x; f ∈ Df -> Cf; g ∈ Dg -> Cg; A ⊆ Df; A ⊆ Dg |]
      ==> f `` A = g `` A

lemma lam_images_eq:

      [| Ord(a); b ∈ a |] ==> (λx∈a. h(x)) `` b = (λx∈b. h(x)) `` b

lemma lam_type_RepFun:

      (λb∈a. h(b)) ∈ a -> {h(b) . b ∈ a}

lemma lemmaX:

      [| ∀Y∈Pow(X). Y lesspoll K --> (∃x∈X. ⟨Y, x⟩ ∈ R); b ∈ K; Z ∈ Pow(X);
         Z lesspoll K |]
      ==> {x ∈ X . ⟨Z, x⟩ ∈ R} ≠ 0

lemma WO1_DC_lemma:

      [| Card(K); well_ord(X, Q); ∀Y∈Pow(X). Y lesspoll K --> (∃x∈X. ⟨Y, x⟩ ∈ R);
         b ∈ K |]
      ==> ff(b, X, Q, R) ∈ {x ∈ X . ⟨(λc∈b. ff(c, X, Q, R)) `` b, x⟩ ∈ R}

theorem WO1_DC_Card:

      WO1 ==> ∀K. Card(K) --> DC(K)