prefer "locale begin ... end";
authorwenzelm
Wed Aug 29 20:01:39 2018 +0200 (13 months ago)
changeset 68847511d163ab623
parent 68846 da0cb00a4d6a
child 68848 8825efd1c2cf
child 68849 0f9b2fa0556f
child 68890 725d5ed56563
prefer "locale begin ... end";
src/ZF/AC/AC16_WO4.thy
src/ZF/AC/DC.thy
     1.1 --- a/src/ZF/AC/AC16_WO4.thy	Wed Aug 29 19:35:41 2018 +0200
     1.2 +++ b/src/ZF/AC/AC16_WO4.thy	Wed Aug 29 20:01:39 2018 +0200
     1.3 @@ -220,8 +220,9 @@
     1.4      and mpos[iff]:      "0<m"
     1.5      and Infinite[iff]:  "~ Finite(y)"
     1.6      and noLepoll:  "~ y \<lesssim> {v \<in> Pow(x). v \<approx> m}"
     1.7 +begin
     1.8  
     1.9 -lemma (in AC16) knat [iff]: "k \<in> nat"
    1.10 +lemma knat [iff]: "k \<in> nat"
    1.11  by (simp add: k_def)
    1.12  
    1.13  
    1.14 @@ -230,7 +231,7 @@
    1.15  (*      where a is certain k-2 element subset of y                        *)
    1.16  (* ********************************************************************** *)
    1.17  
    1.18 -lemma (in AC16) Diff_Finite_eqpoll: "[| l \<approx> a; a \<subseteq> y |] ==> y - a \<approx> y"
    1.19 +lemma Diff_Finite_eqpoll: "[| l \<approx> a; a \<subseteq> y |] ==> y - a \<approx> y"
    1.20  apply (insert WO_R Infinite lnat)
    1.21  apply (rule eqpoll_trans) 
    1.22  apply (rule Diff_lesspoll_eqpoll_Card) 
    1.23 @@ -247,10 +248,10 @@
    1.24  done
    1.25  
    1.26  
    1.27 -lemma (in AC16) s_subset: "s(u) \<subseteq> t_n"
    1.28 +lemma s_subset: "s(u) \<subseteq> t_n"
    1.29  by (unfold s_def, blast)
    1.30  
    1.31 -lemma (in AC16) sI: 
    1.32 +lemma sI: 
    1.33        "[| w \<in> t_n; cons(b,cons(u,a)) \<subseteq> w; a \<subseteq> y; b \<in> y-a; l \<approx> a |] 
    1.34         ==> w \<in> s(u)"
    1.35  apply (unfold s_def succ_def k_def)
    1.36 @@ -258,11 +259,11 @@
    1.37               intro: subset_imp_lepoll lepoll_trans)
    1.38  done
    1.39  
    1.40 -lemma (in AC16) in_s_imp_u_in: "v \<in> s(u) ==> u \<in> v"
    1.41 +lemma in_s_imp_u_in: "v \<in> s(u) ==> u \<in> v"
    1.42  by (unfold s_def, blast)
    1.43  
    1.44  
    1.45 -lemma (in AC16) ex1_superset_a:
    1.46 +lemma ex1_superset_a:
    1.47       "[| l \<approx> a;  a \<subseteq> y;  b \<in> y - a;  u \<in> x |]   
    1.48        ==> \<exists>! c. c \<in> s(u) & a \<subseteq> c & b \<in> c"
    1.49  apply (rule all_ex [simplified k_def, THEN ballE])
    1.50 @@ -273,7 +274,7 @@
    1.51               intro!: cons_cons_subset eqpoll_sym [THEN cons_cons_eqpoll])
    1.52  done
    1.53  
    1.54 -lemma (in AC16) the_eq_cons:
    1.55 +lemma the_eq_cons:
    1.56       "[| \<forall>v \<in> s(u). succ(l) \<approx> v \<inter> y;   
    1.57           l \<approx> a;  a \<subseteq> y;  b \<in> y - a;  u \<in> x |]    
    1.58        ==> (THE c. c \<in> s(u) & a \<subseteq> c & b \<in> c) \<inter> y = cons(b, a)"
    1.59 @@ -282,7 +283,7 @@
    1.60  apply (fast+)
    1.61  done
    1.62  
    1.63 -lemma (in AC16) y_lepoll_subset_s:
    1.64 +lemma y_lepoll_subset_s:
    1.65       "[| \<forall>v \<in> s(u). succ(l) \<approx> v \<inter> y;   
    1.66           l \<approx> a;  a \<subseteq> y;  u \<in> x |]   
    1.67        ==> y \<lesssim> {v \<in> s(u). a \<subseteq> v}"
    1.68 @@ -306,14 +307,14 @@
    1.69  
    1.70  
    1.71  (*relies on the disjointness of x, y*)
    1.72 -lemma (in AC16) x_imp_not_y [dest]: "a \<in> x ==> a \<notin> y"
    1.73 +lemma x_imp_not_y [dest]: "a \<in> x ==> a \<notin> y"
    1.74  by (blast dest:  disjoint [THEN equalityD1, THEN subsetD, OF IntI])
    1.75  
    1.76 -lemma (in AC16) w_Int_eq_w_Diff:
    1.77 +lemma w_Int_eq_w_Diff:
    1.78       "w \<subseteq> x \<union> y ==> w \<inter> (x - {u}) = w - cons(u, w \<inter> y)" 
    1.79  by blast
    1.80  
    1.81 -lemma (in AC16) w_Int_eqpoll_m:
    1.82 +lemma w_Int_eqpoll_m:
    1.83       "[| w \<in> {v \<in> s(u). a \<subseteq> v};   
    1.84           l \<approx> a;  u \<in> x;   
    1.85           \<forall>v \<in> s(u). succ(l) \<approx> v \<inter> y |] 
    1.86 @@ -335,12 +336,12 @@
    1.87  (*      to {v \<in> Pow(x). v \<approx> n-k}                                       *)
    1.88  (* ********************************************************************** *)
    1.89  
    1.90 -lemma (in AC16) eqpoll_m_not_empty: "a \<approx> m ==> a \<noteq> 0"
    1.91 +lemma eqpoll_m_not_empty: "a \<approx> m ==> a \<noteq> 0"
    1.92  apply (insert mpos)
    1.93  apply (fast elim!: zero_lt_natE dest!: eqpoll_succ_imp_not_empty)
    1.94  done
    1.95  
    1.96 -lemma (in AC16) cons_cons_in:
    1.97 +lemma cons_cons_in:
    1.98       "[| z \<in> xa \<inter> (x - {u}); l \<approx> a; a \<subseteq> y; u \<in> x |]   
    1.99        ==> \<exists>! w. w \<in> t_n & cons(z, cons(u, a)) \<subseteq> w"
   1.100  apply (rule all_ex [THEN bspec])
   1.101 @@ -348,7 +349,7 @@
   1.102  apply (fast intro!: cons_eqpoll_succ elim: eqpoll_sym)
   1.103  done
   1.104  
   1.105 -lemma (in AC16) subset_s_lepoll_w:
   1.106 +lemma subset_s_lepoll_w:
   1.107       "[| \<forall>v \<in> s(u). succ(l) \<approx> v \<inter> y; a \<subseteq> y; l \<approx> a; u \<in> x |]   
   1.108        ==> {v \<in> s(u). a \<subseteq> v} \<lesssim> {v \<in> Pow(x). v \<approx> m}"
   1.109  apply (rule_tac f3 = "\<lambda>w \<in> {v \<in> s (u) . a \<subseteq> v}. w \<inter> (x - {u})" 
   1.110 @@ -371,14 +372,14 @@
   1.111  (* well_ord_subsets_lepoll_n                                              *)
   1.112  (* ********************************************************************** *)
   1.113  
   1.114 -lemma (in AC16) well_ord_subsets_eqpoll_n:
   1.115 +lemma well_ord_subsets_eqpoll_n:
   1.116       "n \<in> nat ==> \<exists>S. well_ord({z \<in> Pow(y) . z \<approx> succ(n)}, S)"
   1.117  apply (rule WO_R [THEN well_ord_infinite_subsets_eqpoll_X,
   1.118                    THEN eqpoll_def [THEN def_imp_iff, THEN iffD1], THEN exE])
   1.119  apply (fast intro: bij_is_inj [THEN well_ord_rvimage])+
   1.120  done
   1.121  
   1.122 -lemma (in AC16) well_ord_subsets_lepoll_n:
   1.123 +lemma well_ord_subsets_lepoll_n:
   1.124       "n \<in> nat ==> \<exists>R. well_ord({z \<in> Pow(y). z \<lesssim> n}, R)"
   1.125  apply (induct_tac "n")
   1.126  apply (force intro!: well_ord_unit simp add: subsets_lepoll_0_eq_unit)
   1.127 @@ -392,13 +393,13 @@
   1.128  done
   1.129  
   1.130  
   1.131 -lemma (in AC16) LL_subset: "LL \<subseteq> {z \<in> Pow(y). z \<lesssim> succ(k #+ m)}"
   1.132 +lemma LL_subset: "LL \<subseteq> {z \<in> Pow(y). z \<lesssim> succ(k #+ m)}"
   1.133  apply (unfold LL_def MM_def)
   1.134  apply (insert "includes")
   1.135  apply (blast intro: subset_imp_lepoll eqpoll_imp_lepoll lepoll_trans)
   1.136  done
   1.137  
   1.138 -lemma (in AC16) well_ord_LL: "\<exists>S. well_ord(LL,S)"
   1.139 +lemma well_ord_LL: "\<exists>S. well_ord(LL,S)"
   1.140  apply (rule well_ord_subsets_lepoll_n [THEN exE, of "succ(k#+m)"])
   1.141  apply simp 
   1.142  apply (blast intro: well_ord_subset [OF _ LL_subset])
   1.143 @@ -408,7 +409,7 @@
   1.144  (* every element of LL is a contained in exactly one element of MM        *)
   1.145  (* ********************************************************************** *)
   1.146  
   1.147 -lemma (in AC16) unique_superset_in_MM:
   1.148 +lemma unique_superset_in_MM:
   1.149       "v \<in> LL ==> \<exists>! w. w \<in> MM & v \<subseteq> w"
   1.150  apply (unfold MM_def LL_def, safe, fast)
   1.151  apply (rule lepoll_imp_eqpoll_subset [THEN exE], assumption)
   1.152 @@ -425,34 +426,34 @@
   1.153  (* The union of appropriate values is the whole x                         *)
   1.154  (* ********************************************************************** *)
   1.155  
   1.156 -lemma (in AC16) Int_in_LL: "w \<in> MM ==> w \<inter> y \<in> LL"
   1.157 +lemma Int_in_LL: "w \<in> MM ==> w \<inter> y \<in> LL"
   1.158  by (unfold LL_def, fast)
   1.159  
   1.160 -lemma (in AC16) in_LL_eq_Int: 
   1.161 +lemma in_LL_eq_Int: 
   1.162       "v \<in> LL ==> v = (THE x. x \<in> MM & v \<subseteq> x) \<inter> y"
   1.163  apply (unfold LL_def, clarify)
   1.164  apply (subst unique_superset_in_MM [THEN the_equality2])
   1.165  apply (auto simp add: Int_in_LL)
   1.166  done
   1.167  
   1.168 -lemma (in AC16) unique_superset1: "a \<in> LL \<Longrightarrow> (THE x. x \<in> MM \<and> a \<subseteq> x) \<in> MM"
   1.169 +lemma unique_superset1: "a \<in> LL \<Longrightarrow> (THE x. x \<in> MM \<and> a \<subseteq> x) \<in> MM"
   1.170  by (erule unique_superset_in_MM [THEN theI, THEN conjunct1]) 
   1.171  
   1.172 -lemma (in AC16) the_in_MM_subset:
   1.173 +lemma the_in_MM_subset:
   1.174       "v \<in> LL ==> (THE x. x \<in> MM & v \<subseteq> x) \<subseteq> x \<union> y"
   1.175  apply (drule unique_superset1)
   1.176  apply (unfold MM_def)
   1.177  apply (fast dest!: unique_superset1 "includes" [THEN subsetD])
   1.178  done
   1.179  
   1.180 -lemma (in AC16) GG_subset: "v \<in> LL ==> GG ` v \<subseteq> x"
   1.181 +lemma GG_subset: "v \<in> LL ==> GG ` v \<subseteq> x"
   1.182  apply (unfold GG_def)
   1.183  apply (frule the_in_MM_subset)
   1.184  apply (frule in_LL_eq_Int)
   1.185  apply (force elim: equalityE)
   1.186  done
   1.187  
   1.188 -lemma (in AC16) nat_lepoll_ordertype: "nat \<lesssim> ordertype(y, R)"
   1.189 +lemma nat_lepoll_ordertype: "nat \<lesssim> ordertype(y, R)"
   1.190  apply (rule nat_le_infinite_Ord [THEN le_imp_lepoll]) 
   1.191   apply (rule Ord_ordertype [OF WO_R]) 
   1.192  apply (rule ordertype_eqpoll [THEN eqpoll_imp_lepoll, THEN lepoll_infinite]) 
   1.193 @@ -460,7 +461,7 @@
   1.194  apply (rule Infinite) 
   1.195  done
   1.196  
   1.197 -lemma (in AC16) ex_subset_eqpoll_n: "n \<in> nat ==> \<exists>z. z \<subseteq> y & n \<approx> z"
   1.198 +lemma ex_subset_eqpoll_n: "n \<in> nat ==> \<exists>z. z \<subseteq> y & n \<approx> z"
   1.199  apply (erule nat_lepoll_imp_ex_eqpoll_n)
   1.200  apply (rule lepoll_trans [OF nat_lepoll_ordertype]) 
   1.201  apply (rule ordertype_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll]) 
   1.202 @@ -468,7 +469,7 @@
   1.203  done
   1.204  
   1.205  
   1.206 -lemma (in AC16) exists_proper_in_s: "u \<in> x ==> \<exists>v \<in> s(u). succ(k) \<lesssim> v \<inter> y"
   1.207 +lemma exists_proper_in_s: "u \<in> x ==> \<exists>v \<in> s(u). succ(k) \<lesssim> v \<inter> y"
   1.208  apply (rule ccontr)
   1.209  apply (subgoal_tac "\<forall>v \<in> s (u) . k \<approx> v \<inter> y")
   1.210  prefer 2 apply (simp add: s_def, blast intro: succ_not_lepoll_imp_eqpoll)
   1.211 @@ -479,12 +480,12 @@
   1.212  apply (blast intro: lepoll_trans [OF y_lepoll_subset_s subset_s_lepoll_w])
   1.213  done
   1.214  
   1.215 -lemma (in AC16) exists_in_MM: "u \<in> x ==> \<exists>w \<in> MM. u \<in> w"
   1.216 +lemma exists_in_MM: "u \<in> x ==> \<exists>w \<in> MM. u \<in> w"
   1.217  apply (erule exists_proper_in_s [THEN bexE])
   1.218  apply (unfold MM_def s_def, fast)
   1.219  done
   1.220  
   1.221 -lemma (in AC16) exists_in_LL: "u \<in> x ==> \<exists>w \<in> LL. u \<in> GG`w"
   1.222 +lemma exists_in_LL: "u \<in> x ==> \<exists>w \<in> LL. u \<in> GG`w"
   1.223  apply (rule exists_in_MM [THEN bexE], assumption)
   1.224  apply (rule bexI)
   1.225  apply (erule_tac [2] Int_in_LL)
   1.226 @@ -494,7 +495,7 @@
   1.227  apply (fast elim!: Int_in_LL)+
   1.228  done
   1.229  
   1.230 -lemma (in AC16) OUN_eq_x: "well_ord(LL,S) ==>       
   1.231 +lemma OUN_eq_x: "well_ord(LL,S) ==>       
   1.232        (\<Union>b<ordertype(LL,S). GG ` (converse(ordermap(LL,S)) ` b)) = x"
   1.233  apply (rule equalityI)
   1.234  apply (rule subsetI)
   1.235 @@ -514,18 +515,18 @@
   1.236  (* Every element of the family is less than or equipollent to n-k (m)     *)
   1.237  (* ********************************************************************** *)
   1.238  
   1.239 -lemma (in AC16) in_MM_eqpoll_n: "w \<in> MM ==> w \<approx> succ(k #+ m)"
   1.240 +lemma in_MM_eqpoll_n: "w \<in> MM ==> w \<approx> succ(k #+ m)"
   1.241  apply (unfold MM_def)
   1.242  apply (fast dest: "includes" [THEN subsetD])
   1.243  done
   1.244  
   1.245 -lemma (in AC16) in_LL_eqpoll_n: "w \<in> LL ==> succ(k) \<lesssim> w"
   1.246 +lemma in_LL_eqpoll_n: "w \<in> LL ==> succ(k) \<lesssim> w"
   1.247  by (unfold LL_def MM_def, fast)
   1.248  
   1.249 -lemma (in AC16) in_LL: "w \<in> LL ==> w \<subseteq> (THE x. x \<in> MM \<and> w \<subseteq> x)"
   1.250 +lemma in_LL: "w \<in> LL ==> w \<subseteq> (THE x. x \<in> MM \<and> w \<subseteq> x)"
   1.251  by (erule subset_trans [OF in_LL_eq_Int [THEN equalityD1] Int_lower1])
   1.252  
   1.253 -lemma (in AC16) all_in_lepoll_m: 
   1.254 +lemma all_in_lepoll_m: 
   1.255        "well_ord(LL,S) ==>       
   1.256         \<forall>b<ordertype(LL,S). GG ` (converse(ordermap(LL,S)) ` b) \<lesssim> m"
   1.257  apply (unfold GG_def)
   1.258 @@ -541,7 +542,7 @@
   1.259                                    THEN apply_type])+
   1.260  done
   1.261  
   1.262 -lemma (in AC16) "conclusion":
   1.263 +lemma "conclusion":
   1.264       "\<exists>a f. Ord(a) & domain(f) = a & (\<Union>b<a. f ` b) = x & (\<forall>b<a. f ` b \<lesssim> m)"
   1.265  apply (rule well_ord_LL [THEN exE])
   1.266  apply (rename_tac S)
   1.267 @@ -553,13 +554,13 @@
   1.268                      Ord_ordertype  OUN_eq_x  all_in_lepoll_m [THEN ospec])
   1.269  done
   1.270  
   1.271 +end
   1.272 +
   1.273  
   1.274  (* ********************************************************************** *)
   1.275  (* The main theorem AC16(n, k) ==> WO4(n-k)                               *)
   1.276  (* ********************************************************************** *)
   1.277  
   1.278 -term AC16
   1.279 -
   1.280  theorem AC16_WO4: 
   1.281       "[| AC_Equiv.AC16(k #+ m, k); 0 < k; 0 < m; k \<in> nat; m \<in> nat |] ==> WO4(m)"
   1.282  apply (unfold AC_Equiv.AC16_def WO4_def)
     2.1 --- a/src/ZF/AC/DC.thy	Wed Aug 29 19:35:41 2018 +0200
     2.2 +++ b/src/ZF/AC/DC.thy	Wed Aug 29 20:01:39 2018 +0200
     2.3 @@ -104,7 +104,7 @@
     2.4    defines XX_def: "XX == (\<Union>n \<in> nat. {f \<in> n->X. \<forall>k \<in> n. <f``k, f`k> \<in> R})"
     2.5       and RR_def:  "RR == {<z1,z2>:XX*XX. domain(z2)=succ(domain(z1))  
     2.6                                         & restrict(z2, domain(z1)) = z1}"
     2.7 -
     2.8 +begin
     2.9  
    2.10  (* ********************************************************************** *)
    2.11  (* DC ==> DC(omega)                                                       *)
    2.12 @@ -132,10 +132,10 @@
    2.13  (*                                                                        *)
    2.14  (* ********************************************************************** *)
    2.15  
    2.16 -lemma (in DC0_imp) lemma1_1: "RR \<subseteq> XX*XX"
    2.17 +lemma lemma1_1: "RR \<subseteq> XX*XX"
    2.18  by (unfold RR_def, fast)
    2.19  
    2.20 -lemma (in DC0_imp) lemma1_2: "RR \<noteq> 0"
    2.21 +lemma lemma1_2: "RR \<noteq> 0"
    2.22  apply (unfold RR_def XX_def)
    2.23  apply (rule all_ex [THEN ballE])
    2.24  apply (erule_tac [2] notE [OF _ empty_subsetI [THEN PowI]])
    2.25 @@ -152,7 +152,7 @@
    2.26  apply (simp add: singleton_0)
    2.27  done
    2.28  
    2.29 -lemma (in DC0_imp) lemma1_3: "range(RR) \<subseteq> domain(RR)"
    2.30 +lemma lemma1_3: "range(RR) \<subseteq> domain(RR)"
    2.31  apply (unfold RR_def XX_def)
    2.32  apply (rule range_subset_domain, blast, clarify)
    2.33  apply (frule fun_is_rel [THEN image_subset, THEN PowI, 
    2.34 @@ -168,7 +168,7 @@
    2.35  apply (simp add: domain_of_fun succ_def restrict_cons_eq)
    2.36  done
    2.37  
    2.38 -lemma (in DC0_imp) lemma2:
    2.39 +lemma lemma2:
    2.40       "[| \<forall>n \<in> nat. <f`n, f`succ(n)> \<in> RR;  f \<in> nat -> XX;  n \<in> nat |]   
    2.41        ==> \<exists>k \<in> nat. f`succ(n) \<in> k -> X & n \<in> k   
    2.42                    & <f`succ(n)``n, f`succ(n)`n> \<in> R"
    2.43 @@ -197,7 +197,7 @@
    2.44  apply (blast dest: domain_of_fun [symmetric, THEN trans] )
    2.45  done
    2.46  
    2.47 -lemma (in DC0_imp) lemma3_1:
    2.48 +lemma lemma3_1:
    2.49       "[| \<forall>n \<in> nat. <f`n, f`succ(n)> \<in> RR;  f \<in> nat -> XX;  m \<in> nat |]   
    2.50        ==>  {f`succ(x)`x. x \<in> m} = {f`succ(m)`x. x \<in> m}"
    2.51  apply (subgoal_tac "\<forall>x \<in> m. f`succ (m) `x = f`succ (x) `x")
    2.52 @@ -220,7 +220,7 @@
    2.53               intro: nat_into_Ord OrdmemD [THEN subsetD])
    2.54  done
    2.55  
    2.56 -lemma (in DC0_imp) lemma3:
    2.57 +lemma lemma3:
    2.58       "[| \<forall>n \<in> nat. <f`n, f`succ(n)> \<in> RR;  f \<in> nat -> XX;  m \<in> nat |]  
    2.59        ==> (\<lambda>x \<in> nat. f`succ(x)`x) `` m = f`succ(m)``m"
    2.60  apply (erule natE, simp)
    2.61 @@ -232,6 +232,7 @@
    2.62              elim!: image_fun [symmetric, OF _ OrdmemD [OF _ nat_into_Ord]])
    2.63  done
    2.64  
    2.65 +end
    2.66  
    2.67  theorem DC0_imp_DC_nat: "DC0 ==> DC(nat)"
    2.68  apply (unfold DC_def DC0_def, clarify)
    2.69 @@ -310,8 +311,9 @@
    2.70                      {<z1,z2>\<in>Fin(XX)*XX. (domain(z2)=succ(\<Union>f \<in> z1. domain(f))
    2.71                                      & (\<Union>f \<in> z1. domain(f)) = b  
    2.72                                      & (\<forall>f \<in> z1. restrict(z2,domain(f)) = f))}"
    2.73 +begin
    2.74  
    2.75 -lemma (in imp_DC0) lemma4:
    2.76 +lemma lemma4:
    2.77       "[| range(R) \<subseteq> domain(R);  x \<in> domain(R) |]   
    2.78        ==> RR \<subseteq> Pow(XX)*XX &   
    2.79               (\<forall>Y \<in> Pow(XX). Y \<prec> nat \<longrightarrow> (\<exists>x \<in> XX. <Y,x>:RR))"
    2.80 @@ -329,25 +331,25 @@
    2.81  apply (simp add: nat_0I [THEN rev_bexI] cons_fun_type2)
    2.82  done
    2.83  
    2.84 -lemma (in imp_DC0) UN_image_succ_eq:
    2.85 +lemma UN_image_succ_eq:
    2.86       "[| f \<in> nat->X; n \<in> nat |] 
    2.87        ==> (\<Union>x \<in> f``succ(n). P(x)) =  P(f`n) \<union> (\<Union>x \<in> f``n. P(x))"
    2.88  by (simp add: image_fun OrdmemD) 
    2.89  
    2.90 -lemma (in imp_DC0) UN_image_succ_eq_succ:
    2.91 +lemma UN_image_succ_eq_succ:
    2.92       "[| (\<Union>x \<in> f``n. P(x)) = y; P(f`n) = succ(y);   
    2.93           f \<in> nat -> X; n \<in> nat |] ==> (\<Union>x \<in> f``succ(n). P(x)) = succ(y)"
    2.94  by (simp add: UN_image_succ_eq, blast)
    2.95  
    2.96 -lemma (in imp_DC0) apply_domain_type:
    2.97 +lemma apply_domain_type:
    2.98       "[| h \<in> succ(n) -> D;  n \<in> nat; domain(h)=succ(y) |] ==> h`y \<in> D"
    2.99  by (fast elim: apply_type dest!: trans [OF sym domain_of_fun])
   2.100  
   2.101 -lemma (in imp_DC0) image_fun_succ:
   2.102 +lemma image_fun_succ:
   2.103       "[| h \<in> nat -> X; n \<in> nat |] ==> h``succ(n) = cons(h`n, h``n)"
   2.104  by (simp add: image_fun OrdmemD) 
   2.105  
   2.106 -lemma (in imp_DC0) f_n_type:
   2.107 +lemma f_n_type:
   2.108       "[| domain(f`n) = succ(k); f \<in> nat -> XX;  n \<in> nat |]    
   2.109        ==> f`n \<in> succ(k) -> domain(R)"
   2.110  apply (unfold XX_def)
   2.111 @@ -355,7 +357,7 @@
   2.112  apply (fast elim: domain_eq_imp_fun_type)
   2.113  done
   2.114  
   2.115 -lemma (in imp_DC0) f_n_pairs_in_R [rule_format]: 
   2.116 +lemma f_n_pairs_in_R [rule_format]: 
   2.117       "[| h \<in> nat -> XX;  domain(h`n) = succ(k);  n \<in> nat |]   
   2.118        ==> \<forall>i \<in> k. <h`n`i, h`n`succ(i)> \<in> R"
   2.119  apply (unfold XX_def)
   2.120 @@ -364,7 +366,7 @@
   2.121  apply (drule domain_of_fun [symmetric, THEN trans], assumption, simp)
   2.122  done
   2.123  
   2.124 -lemma (in imp_DC0) restrict_cons_eq_restrict: 
   2.125 +lemma restrict_cons_eq_restrict: 
   2.126       "[| restrict(h, domain(u))=u;  h \<in> n->X;  domain(u) \<subseteq> n |]   
   2.127        ==> restrict(cons(<n, y>, h), domain(u)) = u"
   2.128  apply (unfold restrict_def)
   2.129 @@ -373,7 +375,7 @@
   2.130  apply (blast elim: mem_irrefl)  
   2.131  done
   2.132  
   2.133 -lemma (in imp_DC0) all_in_image_restrict_eq:
   2.134 +lemma all_in_image_restrict_eq:
   2.135       "[| \<forall>x \<in> f``n. restrict(f`n, domain(x))=x;   
   2.136           f \<in> nat -> XX;   
   2.137           n \<in> nat;  domain(f`n) = succ(n);   
   2.138 @@ -387,7 +389,7 @@
   2.139  apply (blast intro!: restrict_cons_eq_restrict)
   2.140  done
   2.141  
   2.142 -lemma (in imp_DC0) simplify_recursion: 
   2.143 +lemma simplify_recursion: 
   2.144       "[| \<forall>b<nat. <f``b, f`b> \<in> RR;   
   2.145           f \<in> nat -> XX; range(R) \<subseteq> domain(R); x \<in> domain(R)|]    
   2.146        ==> allRR"
   2.147 @@ -432,7 +434,7 @@
   2.148  done
   2.149  
   2.150  
   2.151 -lemma (in imp_DC0) lemma2: 
   2.152 +lemma lemma2: 
   2.153       "[| allRR; f \<in> nat->XX; range(R) \<subseteq> domain(R); x \<in> domain(R); n \<in> nat |]
   2.154        ==> f`n \<in> succ(n) -> domain(R) & (\<forall>i \<in> n. <f`n`i, f`n`succ(i)>:R)"
   2.155  apply (unfold allRR_def)
   2.156 @@ -445,7 +447,7 @@
   2.157  apply (fast elim!: trans [THEN domain_eq_imp_fun_type] subst_context)
   2.158  done
   2.159  
   2.160 -lemma (in imp_DC0) lemma3:
   2.161 +lemma lemma3:
   2.162       "[| allRR; f \<in> nat->XX; n\<in>nat; range(R) \<subseteq> domain(R);  x \<in> domain(R) |]
   2.163        ==> f`n`n = f`succ(n)`n"
   2.164  apply (frule lemma2 [THEN conjunct1, THEN domain_of_fun], assumption+)
   2.165 @@ -457,6 +459,8 @@
   2.166  apply (simp add: image_fun OrdmemD) 
   2.167  done
   2.168  
   2.169 +end
   2.170 +
   2.171  
   2.172  theorem DC_nat_imp_DC0: "DC(nat) ==> DC0"
   2.173  apply (unfold DC_def DC0_def)