Quelle  DC.thy

(*  Title:      ZF/AC/DC.thy
  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} < a"
  unfolding lepoll_def
apply (rule_tac x = "λz ∈ RepFun (a,P) . μ 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 < X"
  unfolding lepoll_def
apply (rule_tac x = "λx ∈ f``X. μ 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)"
  unfolding 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)


definition
  DC  :: "i ==> o"  where
    "DC(a) ≡ ∀X R. R ⊆ Pow(X)*X ∧
                    (∀Y ∈ Pow(X). Y ≺ a ⟶ (∃x ∈ X. ⟨Y,x⟩ ∈ R))
                    ⟶ (∃f ∈ a->X. ∀b ∈ R)"

definition
  DC0 :: o  where
    "DC0 ≡ ∀A B R. R ⊆ A*B ∧ R≠0 ∧ range(R) ⊆ domain(R)
                    ⟶ (∃f ∈ nat->domain(R). ∀n ∈ nat. :R)"

definition
  ff  :: "[i, i, i, i] ==> i"  where
    "ff(b, X, Q, R) ≡
           transrec(b, λc r. THE x. first(x, {x ∈ X. ∈ R}, Q))"


locale DC0_imp =
  fixes XX and RR and X and R

  assumes all_ex: "∀Y ∈ Pow(X). Y ≺ nat ⟶ (∃x ∈ X. ⟨Y, x⟩ ∈ R)"

  defines XX_def: "XX ≡ (∪n ∈ nat. {f ∈ n->X. ∀k ∈ n. ∈ R})"
     and RR_def:  "RR ≡ {⟨z1,z2⟩:XX*XX. domain(z2)=succ(domain(z1))
                                       ∧ restrict(z2, domain(z1)) = z1}"
begin

(* ********************************************************************** *)
(* DC \<Longrightarrow> 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 \<in> nat. {f \<in> n->X. \<forall>k \<in> n. <f``k, f`k> \<in> R})           *)
(*       f RR g iff domain(g)=succ(domain(f)) \<and>                           *)
(*              restrict(g, domain(f)) = f                                *)
(*                                                                        *)
(* Then RR satisfies the hypotheses of DC.                                *)
(* So applying DC:                                                        *)
(*                                                                        *)
(*       \<exists>f \<in> nat->XX. \<forall>n \<in> nat. f`n RR f`succ(n)                        *)
(*                                                                        *)
(* Thence                                                                 *)
(*                                                                        *)
(*       ff = {<n, f`succ(n)`n>. n \<in> nat}                                 *)
(*                                                                        *)
(* is the desired function.                                               *)
(*                                                                        *)
(* ********************************************************************** *)

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

lemma lemma1_2: "RR ≠ 0"
  unfolding 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 lemma1_3: "range(RR) ⊆ domain(RR)"
  unfolding 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 lemma2:
     "[∀n ∈ nat. ∈ RR; f ∈ nat -> XX; n ∈ nat]
      ==> ∃k ∈ nat. f`succ(n) ∈ k -> X ∧ n ∈ k
                  ∧ ∈ 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 lemma3_1:
     "[∀n ∈ nat. ∈ 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 lemma3:
     "[∀n ∈ nat. ∈ 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

end

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 [OF DC0_imp.intro] DC0_imp.lemma1_2 [OF DC0_imp.intro] DC0_imp.lemma1_3 [OF DC0_imp.intro])
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 [OF DC0_imp.intro] intro: fun_weaken_type)
apply (rule oallI)
apply (frule DC0_imp.lemma2 [OF DC0_imp.intro], assumption)
  apply (blast intro: fun_weaken_type)
 apply (erule ltD) 
(** LEVEL 11: last subgoal **)
apply (subst DC0_imp.lemma3 [OF DC0_imp.intro], 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 = (∪n ∈ nat. {f ∈ succ(n)->domain(R). ∀k ∈ n. 🚫k, f`succ(k)> ∈ R})
 
  RR = {⟨z1,z2⟩:Fin(XX)*XX.
  (domain(z2)=succ(∪f ∈ z1. domain(f)) ∧
  (∀f ∈ z1. restrict(z2, domain(f)) = f)) |
  (¬ (∃g ∈ XX. domain(g)=succ(∪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 = {🚫 f`n`n>. n ∈ nat}
 
  is the desired function.
 
************************************************************************* *)

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


locale imp_DC0 =
  fixes XX and RR and x and R and f and allRR
  defines XX_def: "XX ≡ (∪n ∈ nat.
                      {f ∈ succ(n)->domain(R). ∀k ∈ n. ∈ R})"
      and RR_def:
         "RR ≡ {⟨z1,z2⟩:Fin(XX)*XX.
                  (domain(z2)=succ(∪f ∈ z1. domain(f))
                    ∧ (∀f ∈ z1. restrict(z2, domain(f)) = f))
                  | (¬ (∃g ∈ XX. domain(g)=succ(∪f ∈ z1. domain(f))
                     ∧ (∀f ∈ z1. restrict(g, domain(f)) = f)) ∧ z2={⟨0,x⟩})}"
      and allRR_def:
        "allRR ≡ ∀b
                    ∈
                    {⟨z1,z2⟩∈Fin(XX)*XX. (domain(z2)=succ(∪f ∈ z1. domain(f))
                                    ∧ (∪f ∈ z1. domain(f)) = b
                                    ∧ (∀f ∈ z1. restrict(z2,domain(f)) = f))}"
begin

lemma lemma4:
     "[range(R) ⊆ domain(R); x ∈ domain(R)]
      ==> RR ⊆ Pow(XX)*XX ∧
             (∀Y ∈ Pow(XX). Y ≺ 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(∪f ∈ Y. domain(f)) ∧ (∀f∈Y. restrict(g, domain(f)) = f)")
apply (simp add: RR_def, blast)
apply (safe del: domainE)
  unfolding 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 UN_image_succ_eq:
     "[f ∈ nat->X; n ∈ nat]
      ==> (∪x ∈ f``succ(n). P(x)) = P(f`n) ∪ (∪x ∈ f``n. P(x))"
by (simp add: image_fun OrdmemD) 

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

lemma 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 image_fun_succ:
     "[h ∈ nat -> X; n ∈ nat] ==> h``succ(n) = cons(h`n, h``n)"
by (simp add: image_fun OrdmemD) 

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

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

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

lemma all_in_image_restrict_eq:
     "[∀x ∈ f``n. restrict(f`n, domain(x))=x;
         f ∈ nat -> XX;
         n ∈ nat; domain(f`n) = succ(n);
         (∪x ∈ f``n. domain(x)) ⊆ n]
      ==> ∀x ∈ f``succ(n). restrict(cons(, 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 simplify_recursion: 
     "[∀b ∈ RR;
         f ∈ nat -> XX; range(R) ⊆ domain(R); x ∈ domain(R)]
      ==> allRR"
  unfolding 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 \<not>\<exists> to \<forall>\<not> *)
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(, 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 lemma2: 
     "[allRR; f ∈ nat->XX; range(R) ⊆ domain(R); x ∈ domain(R); n ∈ nat]
      ==> f`n ∈ succ(n) -> domain(R) ∧ (∀i ∈ n. :R)"
  unfolding 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)
  unfolding XX_def
apply (fast elim!: trans [THEN domain_eq_imp_fun_type] subst_context)
done

lemma 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+)
  unfolding 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

end


theorem DC_nat_imp_DC0: "DC(nat) ==> DC0"
  unfolding 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

(* ********************************************************************** *)
(* \<forall>K. Card(K) \<longrightarrow> DC(K) \<Longrightarrow> WO3                                       *)
(* ********************************************************************** *)

lemma fun_Ord_inj:
      "[f ∈ a->X; Ord(a);
          ∧b c. [b∈ 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])

lemma lesspoll_lemma: "[¬ A ≺ B; C ≺ B] ==> A - C ≠ 0"
  unfolding lesspoll_def
apply (fast dest!: Diff_eq_0_iff [THEN iffD1, THEN subset_imp_lepoll]
            intro!: eqpollI elim: notE
            elim!: eqpollE lepoll_trans)
done

theorem DC_WO3: "(∀K. Card(K) ⟶ DC(K)) ==> WO3"
  unfolding DC_def WO3_def
apply (rule allI)
apply (case_tac "A ≺ 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 ≺ 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 \<Longrightarrow> \<forall>K. Card(K) \<longrightarrow> 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 ≺ K ⟶ (∃x ∈ X. ⟨Y, x⟩ ∈ R);
         b ∈ K; Z ∈ Pow(X); Z ≺ K]
      ==> {x ∈ X. ⟨Z,x⟩ ∈ R} ≠ 0"
by blast


lemma WO1_DC_lemma:
     "[Card(K); well_ord(X,Q);
         ∀Y ∈ Pow(X). Y ≺ 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)"
  unfolding 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