conversion of Hyperreal/{Fact,Filter} to Isar scripts
authorpaulson
Sat Jul 31 20:54:23 2004 +0200 (2004-07-31)
changeset 15094a7d1a3fdc30d
parent 15093 49ede01e9ee6
child 15095 63f5f4c265dd
conversion of Hyperreal/{Fact,Filter} to Isar scripts
src/HOL/Hyperreal/Fact.thy
src/HOL/Hyperreal/Filter.thy
src/HOL/Hyperreal/Integration.thy
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/Hyperreal/Fact.thy	Fri Jul 30 18:37:58 2004 +0200
     1.2 +++ b/src/HOL/Hyperreal/Fact.thy	Sat Jul 31 20:54:23 2004 +0200
     1.3 @@ -1,14 +1,74 @@
     1.4 -(*  Title       : Fact.thy 
     1.5 +(*  Title       : Fact.thy
     1.6      Author      : Jacques D. Fleuriot
     1.7      Copyright   : 1998  University of Cambridge
     1.8 -    Description : Factorial function
     1.9 +    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
    1.10  *)
    1.11  
    1.12 -Fact = NatStar + 
    1.13 +header{*Factorial Function*}
    1.14 +
    1.15 +theory Fact = Real:
    1.16 +
    1.17 +consts fact :: "nat => nat"
    1.18 +primrec
    1.19 +   fact_0:     "fact 0 = 1"
    1.20 +   fact_Suc:   "fact (Suc n) = (Suc n) * fact n"
    1.21 +
    1.22 +
    1.23 +lemma fact_gt_zero [simp]: "0 < fact n"
    1.24 +by (induct "n", auto)
    1.25 +
    1.26 +lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0"
    1.27 +by simp
    1.28 +
    1.29 +lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0"
    1.30 +by auto
    1.31 +
    1.32 +lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact n)"
    1.33 +by auto
    1.34 +
    1.35 +lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact n)"
    1.36 +by simp
    1.37 +
    1.38 +lemma fact_ge_one [simp]: "1 \<le> fact n"
    1.39 +by (induct "n", auto)
    1.40  
    1.41 -consts fact :: nat => nat 
    1.42 -primrec 
    1.43 -   fact_0     "fact 0 = 1"
    1.44 -   fact_Suc   "fact (Suc n) = (Suc n) * fact n" 
    1.45 +lemma fact_mono: "m \<le> n ==> fact m \<le> fact n"
    1.46 +apply (drule le_imp_less_or_eq)
    1.47 +apply (auto dest!: less_imp_Suc_add)
    1.48 +apply (induct_tac "k", auto)
    1.49 +done
    1.50 +
    1.51 +text{*Note that @{term "fact 0 = fact 1"}*}
    1.52 +lemma fact_less_mono: "[| 0 < m; m < n |] ==> fact m < fact n"
    1.53 +apply (drule_tac m = m in less_imp_Suc_add, auto)
    1.54 +apply (induct_tac "k", auto)
    1.55 +done
    1.56 +
    1.57 +lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact n))"
    1.58 +by (auto simp add: positive_imp_inverse_positive)
    1.59 +
    1.60 +lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact n))"
    1.61 +by (auto intro: order_less_imp_le)
    1.62 +
    1.63 +lemma fact_diff_Suc [rule_format]:
    1.64 +     "\<forall>m. n < Suc m --> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
    1.65 +apply (induct n, auto)
    1.66 +apply (drule_tac x = "m - 1" in spec, auto)
    1.67 +done
    1.68 +
    1.69 +lemma fact_num0 [simp]: "fact 0 = 1"
    1.70 +by auto
    1.71 +
    1.72 +lemma fact_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m - 1))"
    1.73 +by (case_tac "m", auto)
    1.74 +
    1.75 +lemma fact_add_num_eq_if:
    1.76 +     "fact (m+n) = (if (m+n = 0) then 1 else (m+n) * (fact (m + n - 1)))"
    1.77 +by (case_tac "m+n", auto)
    1.78 +
    1.79 +lemma fact_add_num_eq_if2:
    1.80 +     "fact (m+n) = (if m=0 then fact n else (m+n) * (fact ((m - 1) + n)))"
    1.81 +by (case_tac "m", auto)
    1.82 +
    1.83  
    1.84  end
    1.85 \ No newline at end of file
     2.1 --- a/src/HOL/Hyperreal/Filter.thy	Fri Jul 30 18:37:58 2004 +0200
     2.2 +++ b/src/HOL/Hyperreal/Filter.thy	Sat Jul 31 20:54:23 2004 +0200
     2.3 @@ -2,44 +2,517 @@
     2.4      ID          : $Id$
     2.5      Author      : Jacques D. Fleuriot
     2.6      Copyright   : 1998  University of Cambridge
     2.7 -    Description : Filters and Ultrafilters
     2.8 +    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     2.9  *) 
    2.10  
    2.11 -Filter = Zorn + 
    2.12 +header{*Filters and Ultrafilters*}
    2.13 +
    2.14 +theory Filter = Zorn:
    2.15  
    2.16  constdefs
    2.17  
    2.18 -  is_Filter       :: ['a set set,'a set] => bool
    2.19 -  "is_Filter F S == (F <= Pow(S) & S : F & {} ~: F &
    2.20 -                   (ALL u: F. ALL v: F. u Int v : F) &
    2.21 -                   (ALL u v. u: F & u <= v & v <= S --> v: F))" 
    2.22 +  is_Filter       :: "['a set set,'a set] => bool"
    2.23 +  "is_Filter F S == (F <= Pow(S) & S \<in> F & {} ~: F &
    2.24 +                   (\<forall>u \<in> F. \<forall>v \<in> F. u Int v \<in> F) &
    2.25 +                   (\<forall>u v. u \<in> F & u <= v & v <= S --> v \<in> F))" 
    2.26  
    2.27 -  Filter          :: 'a set => 'a set set set
    2.28 +  Filter          :: "'a set => 'a set set set"
    2.29    "Filter S == {X. is_Filter X S}"
    2.30   
    2.31    (* free filter does not contain any finite set *)
    2.32  
    2.33 -  Freefilter      :: 'a set => 'a set set set
    2.34 -  "Freefilter S == {X. X: Filter S & (ALL x: X. ~ finite x)}"
    2.35 +  Freefilter      :: "'a set => 'a set set set"
    2.36 +  "Freefilter S == {X. X \<in> Filter S & (\<forall>x \<in> X. ~ finite x)}"
    2.37  
    2.38 -  Ultrafilter     :: 'a set => 'a set set set
    2.39 -  "Ultrafilter S == {X. X: Filter S & (ALL A: Pow(S). A: X | S - A : X)}"
    2.40 +  Ultrafilter     :: "'a set => 'a set set set"
    2.41 +  "Ultrafilter S == {X. X \<in> Filter S & (\<forall>A \<in> Pow(S). A \<in> X | S - A \<in> X)}"
    2.42  
    2.43 -  FreeUltrafilter :: 'a set => 'a set set set
    2.44 -  "FreeUltrafilter S == {X. X: Ultrafilter S & (ALL x: X. ~ finite x)}" 
    2.45 +  FreeUltrafilter :: "'a set => 'a set set set"
    2.46 +  "FreeUltrafilter S == {X. X \<in> Ultrafilter S & (\<forall>x \<in> X. ~ finite x)}" 
    2.47  
    2.48    (* A locale makes proof of Ultrafilter Theorem more modular *)
    2.49 -locale UFT = 
    2.50 -       fixes     frechet :: "'a set => 'a set set"
    2.51 -                 superfrechet :: "'a set => 'a set set set"
    2.52 +locale (open) UFT = 
    2.53 +  fixes frechet      :: "'a set => 'a set set"
    2.54 +    and superfrechet :: "'a set => 'a set set set"
    2.55 +  assumes not_finite_UNIV:  "~finite (UNIV :: 'a set)"
    2.56 +  defines frechet_def:  
    2.57 +		"frechet S == {A. finite (S - A)}"
    2.58 +      and superfrechet_def:
    2.59 +		"superfrechet S == {G.  G \<in> Filter S & frechet S <= G}"
    2.60 +
    2.61 +
    2.62 +(*------------------------------------------------------------------
    2.63 +      Properties of Filters and Freefilters - 
    2.64 +      rules for intro, destruction etc.
    2.65 + ------------------------------------------------------------------*)
    2.66 +
    2.67 +lemma is_FilterD1: "is_Filter X S ==> X <= Pow(S)"
    2.68 +apply (simp add: is_Filter_def)
    2.69 +done
    2.70 +
    2.71 +lemma is_FilterD2: "is_Filter X S ==> X ~= {}"
    2.72 +apply (auto simp add: is_Filter_def)
    2.73 +done
    2.74 +
    2.75 +lemma is_FilterD3: "is_Filter X S ==> {} ~: X"
    2.76 +apply (simp add: is_Filter_def)
    2.77 +done
    2.78 +
    2.79 +lemma mem_FiltersetI: "is_Filter X S ==> X \<in> Filter S"
    2.80 +apply (simp add: Filter_def)
    2.81 +done
    2.82 +
    2.83 +lemma mem_FiltersetD: "X \<in> Filter S ==> is_Filter X S"
    2.84 +apply (simp add: Filter_def)
    2.85 +done
    2.86 +
    2.87 +lemma Filter_empty_not_mem: "X \<in> Filter S ==> {} ~: X"
    2.88 +apply (erule mem_FiltersetD [THEN is_FilterD3])
    2.89 +done
    2.90 +
    2.91 +lemmas Filter_empty_not_memE = Filter_empty_not_mem [THEN notE, standard]
    2.92 +
    2.93 +lemma mem_FiltersetD1: "[| X \<in> Filter S; A \<in> X; B \<in> X |] ==> A Int B \<in> X"
    2.94 +apply (unfold Filter_def is_Filter_def)
    2.95 +apply blast
    2.96 +done
    2.97 +
    2.98 +lemma mem_FiltersetD2: "[| X \<in> Filter S; A \<in> X; A <= B; B <= S|] ==> B \<in> X"
    2.99 +apply (unfold Filter_def is_Filter_def)
   2.100 +apply blast
   2.101 +done
   2.102 +
   2.103 +lemma mem_FiltersetD3: "[| X \<in> Filter S; A \<in> X |] ==> A \<in> Pow S"
   2.104 +apply (unfold Filter_def is_Filter_def)
   2.105 +apply blast
   2.106 +done
   2.107 +
   2.108 +lemma mem_FiltersetD4: "X \<in> Filter S  ==> S \<in> X"
   2.109 +apply (unfold Filter_def is_Filter_def)
   2.110 +apply blast
   2.111 +done
   2.112 +
   2.113 +lemma is_FilterI: 
   2.114 +      "[| X <= Pow(S); 
   2.115 +               S \<in> X;  
   2.116 +               X ~= {};  
   2.117 +               {} ~: X;  
   2.118 +               \<forall>u \<in> X. \<forall>v \<in> X. u Int v \<in> X;  
   2.119 +               \<forall>u v. u \<in> X & u<=v & v<=S --> v \<in> X  
   2.120 +            |] ==> is_Filter X S"
   2.121 +apply (unfold is_Filter_def)
   2.122 +apply blast
   2.123 +done
   2.124 +
   2.125 +lemma mem_FiltersetI2: "[| X <= Pow(S); 
   2.126 +               S \<in> X;  
   2.127 +               X ~= {};  
   2.128 +               {} ~: X;  
   2.129 +               \<forall>u \<in> X. \<forall>v \<in> X. u Int v \<in> X;  
   2.130 +               \<forall>u v. u \<in> X & u<=v & v<=S --> v \<in> X  
   2.131 +            |] ==> X \<in> Filter S"
   2.132 +by (blast intro: mem_FiltersetI is_FilterI)
   2.133 +
   2.134 +lemma is_FilterE_lemma: 
   2.135 +      "is_Filter X S ==> X <= Pow(S) &  
   2.136 +                           S \<in> X &  
   2.137 +                           X ~= {} &  
   2.138 +                           {} ~: X  &  
   2.139 +                           (\<forall>u \<in> X. \<forall>v \<in> X. u Int v \<in> X) &  
   2.140 +                           (\<forall>u v. u \<in> X & u <= v & v<=S --> v \<in> X)"
   2.141 +apply (unfold is_Filter_def)
   2.142 +apply fast
   2.143 +done
   2.144 +
   2.145 +lemma memFiltersetE_lemma: 
   2.146 +      "X \<in> Filter S ==> X <= Pow(S) & 
   2.147 +                           S \<in> X &  
   2.148 +                           X ~= {} &  
   2.149 +                           {} ~: X  &  
   2.150 +                           (\<forall>u \<in> X. \<forall>v \<in> X. u Int v \<in> X) &  
   2.151 +                           (\<forall>u v. u \<in> X & u <= v & v<=S --> v \<in> X)"
   2.152 +by (erule mem_FiltersetD [THEN is_FilterE_lemma])
   2.153 +
   2.154 +lemma Freefilter_Filter: "X \<in> Freefilter S ==> X \<in> Filter S"
   2.155 +apply (simp add: Filter_def Freefilter_def)
   2.156 +done
   2.157 +
   2.158 +lemma mem_Freefilter_not_finite: "X \<in> Freefilter S ==> \<forall>y \<in> X. ~finite(y)"
   2.159 +apply (simp add: Freefilter_def)
   2.160 +done
   2.161 +
   2.162 +lemma mem_FreefiltersetD1: "[| X \<in> Freefilter S; x \<in> X |] ==> ~ finite x"
   2.163 +apply (blast dest!: mem_Freefilter_not_finite)
   2.164 +done
   2.165  
   2.166 -       assumes   not_finite_UNIV "~finite (UNIV :: 'a set)"
   2.167 +lemmas mem_FreefiltersetE1 = mem_FreefiltersetD1 [THEN notE, standard]
   2.168 +
   2.169 +lemma mem_FreefiltersetD2: "[| X \<in> Freefilter S; finite x|] ==> x ~: X"
   2.170 +apply (blast dest!: mem_Freefilter_not_finite)
   2.171 +done
   2.172 +
   2.173 +lemma mem_FreefiltersetI1: 
   2.174 +      "[| X \<in> Filter S; \<forall>x. ~(x \<in> X & finite x) |] ==> X \<in> Freefilter S"
   2.175 +by (simp add: Freefilter_def)
   2.176 +
   2.177 +lemma mem_FreefiltersetI2: 
   2.178 +      "[| X \<in> Filter S; \<forall>x. (x ~: X | ~ finite x) |] ==> X \<in> Freefilter S"
   2.179 +by (simp add: Freefilter_def)
   2.180 +
   2.181 +lemma Filter_Int_not_empty: "[| X \<in> Filter S; A \<in> X; B \<in> X |] ==> A Int B ~= {}"
   2.182 +apply (frule_tac A = "A" and B = "B" in mem_FiltersetD1)
   2.183 +apply (auto dest!: Filter_empty_not_mem)
   2.184 +done
   2.185 +
   2.186 +lemmas Filter_Int_not_emptyE = Filter_Int_not_empty [THEN notE, standard]
   2.187 +
   2.188 +subsection{*Ultrafilters and Free Ultrafilters*}
   2.189 +
   2.190 +lemma Ultrafilter_Filter: "X \<in> Ultrafilter S ==> X \<in> Filter S"
   2.191 +apply (simp add: Ultrafilter_def)
   2.192 +done
   2.193 +
   2.194 +lemma mem_UltrafiltersetD2: 
   2.195 +      "X \<in> Ultrafilter S ==> \<forall>A \<in> Pow(S). A \<in> X | S - A \<in> X"
   2.196 +by (auto simp add: Ultrafilter_def)
   2.197 +
   2.198 +lemma mem_UltrafiltersetD3: 
   2.199 +      "[|X \<in> Ultrafilter S; A <= S; A ~: X |] ==> S - A \<in> X"
   2.200 +by (auto simp add: Ultrafilter_def)
   2.201 +
   2.202 +lemma mem_UltrafiltersetD4: 
   2.203 +      "[|X \<in> Ultrafilter S; A <= S; S - A ~: X |] ==> A \<in> X"
   2.204 +by (auto simp add: Ultrafilter_def)
   2.205 +
   2.206 +lemma mem_UltrafiltersetI: 
   2.207 +     "[| X \<in> Filter S;  
   2.208 +         \<forall>A \<in> Pow(S). A \<in> X | S - A \<in> X |] ==> X \<in> Ultrafilter S"
   2.209 +by (simp add: Ultrafilter_def)
   2.210 +
   2.211 +lemma FreeUltrafilter_Ultrafilter: 
   2.212 +     "X \<in> FreeUltrafilter S ==> X \<in> Ultrafilter S"
   2.213 +by (auto simp add: Ultrafilter_def FreeUltrafilter_def)
   2.214 +
   2.215 +lemma mem_FreeUltrafilter_not_finite: 
   2.216 +     "X \<in> FreeUltrafilter S ==> \<forall>y \<in> X. ~finite(y)"
   2.217 +by (simp add: FreeUltrafilter_def)
   2.218 +
   2.219 +lemma mem_FreeUltrafiltersetD1: "[| X \<in> FreeUltrafilter S; x \<in> X |] ==> ~ finite x"
   2.220 +apply (blast dest!: mem_FreeUltrafilter_not_finite)
   2.221 +done
   2.222  
   2.223 -       defines   frechet_def "frechet S == {A. finite (S - A)}"
   2.224 -                 superfrechet_def "superfrechet S == 
   2.225 -                                   {G.  G: Filter S & frechet S <= G}"
   2.226 -end
   2.227 +lemmas mem_FreeUltrafiltersetE1 = mem_FreeUltrafiltersetD1 [THEN notE, standard]
   2.228 +
   2.229 +lemma mem_FreeUltrafiltersetD2: "[| X \<in> FreeUltrafilter S; finite x|] ==> x ~: X"
   2.230 +apply (blast dest!: mem_FreeUltrafilter_not_finite)
   2.231 +done
   2.232 +
   2.233 +lemma mem_FreeUltrafiltersetI1: 
   2.234 +      "[| X \<in> Ultrafilter S;  
   2.235 +          \<forall>x. ~(x \<in> X & finite x) |] ==> X \<in> FreeUltrafilter S"
   2.236 +by (simp add: FreeUltrafilter_def)
   2.237 +
   2.238 +lemma mem_FreeUltrafiltersetI2: 
   2.239 +      "[| X \<in> Ultrafilter S;  
   2.240 +          \<forall>x. (x ~: X | ~ finite x) |] ==> X \<in> FreeUltrafilter S"
   2.241 +by (simp add: FreeUltrafilter_def)
   2.242 +
   2.243 +lemma FreeUltrafilter_iff: 
   2.244 +     "(X \<in> FreeUltrafilter S) = (X \<in> Freefilter S & (\<forall>x \<in> Pow(S). x \<in> X | S - x \<in> X))"
   2.245 +by (auto simp add: FreeUltrafilter_def Freefilter_def Ultrafilter_def)
   2.246 +
   2.247 +
   2.248 +(*-------------------------------------------------------------------
   2.249 +   A Filter F on S is an ultrafilter iff it is a maximal filter 
   2.250 +   i.e. whenever G is a filter on I and F <= F then F = G
   2.251 + --------------------------------------------------------------------*)
   2.252 +(*---------------------------------------------------------------------
   2.253 +  lemmas that shows existence of an extension to what was assumed to
   2.254 +  be a maximal filter. Will be used to derive contradiction in proof of
   2.255 +  property of ultrafilter 
   2.256 + ---------------------------------------------------------------------*)
   2.257 +lemma lemma_set_extend: "[| F ~= {}; A <= S |] ==> \<exists>x. x \<in> {X. X <= S & (\<exists>f \<in> F. A Int f <= X)}"
   2.258 +apply blast
   2.259 +done
   2.260 +
   2.261 +lemma lemma_set_not_empty: "a \<in> X ==> X ~= {}"
   2.262 +apply (safe)
   2.263 +done
   2.264 +
   2.265 +lemma lemma_empty_Int_subset_Compl: "x Int F <= {} ==> F <= - x"
   2.266 +apply blast
   2.267 +done
   2.268 +
   2.269 +lemma mem_Filterset_disjI: 
   2.270 +      "[| F \<in> Filter S; A ~: F; A <= S|]  
   2.271 +           ==> \<forall>B. B ~: F | ~ B <= A"
   2.272 +apply (unfold Filter_def is_Filter_def)
   2.273 +apply blast
   2.274 +done
   2.275 +
   2.276 +lemma Ultrafilter_max_Filter: "F \<in> Ultrafilter S ==>  
   2.277 +          (F \<in> Filter S & (\<forall>G \<in> Filter S. F <= G --> F = G))"
   2.278 +apply (auto simp add: Ultrafilter_def)
   2.279 +apply (drule_tac x = "x" in bspec)
   2.280 +apply (erule mem_FiltersetD3 , assumption)
   2.281 +apply (safe)
   2.282 +apply (drule subsetD , assumption)
   2.283 +apply (blast dest!: Filter_Int_not_empty)
   2.284 +done
   2.285  
   2.286  
   2.287 +(*--------------------------------------------------------------------------------
   2.288 +     This is a very long and tedious proof; need to break it into parts.
   2.289 +     Have proof that {X. X <= S & (\<exists>f \<in> F. A Int f <= X)} is a filter as 
   2.290 +     a lemma
   2.291 +--------------------------------------------------------------------------------*)
   2.292 +lemma max_Filter_Ultrafilter: 
   2.293 +      "[| F \<in> Filter S;  
   2.294 +          \<forall>G \<in> Filter S. F <= G --> F = G |] ==> F \<in> Ultrafilter S"
   2.295 +apply (simp add: Ultrafilter_def)
   2.296 +apply (safe)
   2.297 +apply (rule ccontr)
   2.298 +apply (frule mem_FiltersetD [THEN is_FilterD2])
   2.299 +apply (frule_tac x = "{X. X <= S & (\<exists>f \<in> F. A Int f <= X) }" in bspec)
   2.300 +apply (rule mem_FiltersetI2) 
   2.301 +apply (blast intro: elim:); 
   2.302 +apply (simp add: ); 
   2.303 +apply (blast dest: mem_FiltersetD3)
   2.304 +apply (erule lemma_set_extend [THEN exE])
   2.305 +apply (assumption , erule lemma_set_not_empty)
   2.306 +txt{*First we prove @{term "{} \<notin> {X. X \<subseteq> S \<and> (\<exists>f\<in>F. A \<inter> f \<subseteq> X)}"}*}
   2.307 +   apply (clarify ); 
   2.308 +   apply (drule lemma_empty_Int_subset_Compl)
   2.309 +   apply (frule mem_Filterset_disjI) 
   2.310 +   apply assumption; 
   2.311 +   apply (blast intro: elim:); 
   2.312 +   apply (fast dest: mem_FiltersetD3 elim:) 
   2.313 +txt{*Next case: @{term "u \<inter> v"} is an element*}
   2.314 +  apply (intro ballI) 
   2.315 +apply (simp add: ); 
   2.316 +  apply (rule conjI, blast) 
   2.317 +apply (clarify ); 
   2.318 +  apply (rule_tac x = "f Int fa" in bexI)
   2.319 +   apply (fast intro: elim:); 
   2.320 +  apply (blast dest: mem_FiltersetD1 elim:)
   2.321 + apply force;
   2.322 +apply (blast dest: mem_FiltersetD3 elim:) 
   2.323 +done
   2.324 +
   2.325 +lemma Ultrafilter_iff: "(F \<in> Ultrafilter S) = (F \<in> Filter S & (\<forall>G \<in> Filter S. F <= G --> F = G))"
   2.326 +apply (blast intro!: Ultrafilter_max_Filter max_Filter_Ultrafilter)
   2.327 +done
   2.328  
   2.329  
   2.330 +subsection{* A Few Properties of Freefilters*}
   2.331 +
   2.332 +lemma lemma_Compl_cancel_eq: "F1 Int F2 = ((F1 Int Y) Int F2) Un ((F2 Int (- Y)) Int F1)"
   2.333 +apply auto
   2.334 +done
   2.335 +
   2.336 +lemma finite_IntI1: "finite X ==> finite (X Int Y)"
   2.337 +apply (erule Int_lower1 [THEN finite_subset])
   2.338 +done
   2.339 +
   2.340 +lemma finite_IntI2: "finite Y ==> finite (X Int Y)"
   2.341 +apply (erule Int_lower2 [THEN finite_subset])
   2.342 +done
   2.343 +
   2.344 +lemma finite_Int_Compl_cancel: "[| finite (F1 Int Y);  
   2.345 +                  finite (F2 Int (- Y))  
   2.346 +               |] ==> finite (F1 Int F2)"
   2.347 +apply (rule_tac Y1 = "Y" in lemma_Compl_cancel_eq [THEN ssubst])
   2.348 +apply (rule finite_UnI)
   2.349 +apply (auto intro!: finite_IntI1 finite_IntI2)
   2.350 +done
   2.351 +
   2.352 +lemma Freefilter_lemma_not_finite: "U \<in> Freefilter S  ==>  
   2.353 +          ~ (\<exists>f1 \<in> U. \<exists>f2 \<in> U. finite (f1 Int x)  
   2.354 +                             & finite (f2 Int (- x)))"
   2.355 +apply (safe)
   2.356 +apply (frule_tac A = "f1" and B = "f2" in Freefilter_Filter [THEN mem_FiltersetD1])
   2.357 +apply (drule_tac [3] x = "f1 Int f2" in mem_FreefiltersetD1)
   2.358 +apply (drule_tac [4] finite_Int_Compl_cancel)
   2.359 +apply auto
   2.360 +done
   2.361 +
   2.362 +(* the lemmas below follow *)
   2.363 +lemma Freefilter_Compl_not_finite_disjI: "U \<in> Freefilter S ==>  
   2.364 +           \<forall>f \<in> U. ~ finite (f Int x) | ~finite (f Int (- x))"
   2.365 +by (blast dest!: Freefilter_lemma_not_finite bspec)
   2.366 +
   2.367 +lemma Freefilter_Compl_not_finite_disjI2: "U \<in> Freefilter S ==> (\<forall>f \<in> U. ~ finite (f Int x)) | (\<forall>f \<in> U. ~finite (f Int (- x)))"
   2.368 +apply (blast dest!: Freefilter_lemma_not_finite bspec)
   2.369 +done
   2.370 +
   2.371 +lemma cofinite_Filter: "~ finite (UNIV:: 'a set) ==> {A:: 'a set. finite (- A)} \<in> Filter UNIV"
   2.372 +apply (rule mem_FiltersetI2)
   2.373 +apply (auto simp del: Collect_empty_eq)
   2.374 +apply (erule_tac c = "UNIV" in equalityCE)
   2.375 +apply auto
   2.376 +apply (erule Compl_anti_mono [THEN finite_subset])
   2.377 +apply assumption
   2.378 +done
   2.379 +
   2.380 +lemma not_finite_UNIV_disjI: "~finite(UNIV :: 'a set) ==> ~finite (X :: 'a set) | ~finite (- X)" 
   2.381 +apply (drule_tac A1 = "X" in Compl_partition [THEN ssubst])
   2.382 +apply simp
   2.383 +done
   2.384 +
   2.385 +lemma not_finite_UNIV_Compl: "[| ~finite(UNIV :: 'a set); finite (X :: 'a set) |] ==>  ~finite (- X)"
   2.386 +apply (drule_tac X = "X" in not_finite_UNIV_disjI)
   2.387 +apply blast
   2.388 +done
   2.389 +
   2.390 +lemma mem_cofinite_Filter_not_finite:
   2.391 +     "~ finite (UNIV:: 'a set) 
   2.392 +      ==> \<forall>X \<in> {A:: 'a set. finite (- A)}. ~ finite X"
   2.393 +by (auto dest: not_finite_UNIV_disjI)
   2.394 +
   2.395 +lemma cofinite_Freefilter:
   2.396 +    "~ finite (UNIV:: 'a set) ==> {A:: 'a set. finite (- A)} \<in> Freefilter UNIV"
   2.397 +apply (rule mem_FreefiltersetI2)
   2.398 +apply (rule cofinite_Filter , assumption)
   2.399 +apply (blast dest!: mem_cofinite_Filter_not_finite)
   2.400 +done
   2.401 +
   2.402 +(*????Set.thy*)
   2.403 +lemma UNIV_diff_Compl [simp]: "UNIV - x = - x"
   2.404 +apply auto
   2.405 +done
   2.406 +
   2.407 +lemma FreeUltrafilter_contains_cofinite_set: 
   2.408 +     "[| ~finite(UNIV :: 'a set); (U :: 'a set set): FreeUltrafilter UNIV 
   2.409 +          |] ==> {X. finite(- X)} <= U"
   2.410 +by (auto simp add: Ultrafilter_def FreeUltrafilter_def)
   2.411 +
   2.412 +(*--------------------------------------------------------------------
   2.413 +   We prove: 1. Existence of maximal filter i.e. ultrafilter
   2.414 +             2. Freeness property i.e ultrafilter is free
   2.415 +             Use a locale to prove various lemmas and then 
   2.416 +             export main result: The Ultrafilter Theorem
   2.417 + -------------------------------------------------------------------*)
   2.418 +
   2.419 +lemma (in UFT) chain_Un_subset_Pow: 
   2.420 +   "!!(c :: 'a set set set). c \<in> chain (superfrechet S) ==>  Union c <= Pow S"
   2.421 +apply (simp add: chain_def superfrechet_def frechet_def)
   2.422 +apply (blast dest: mem_FiltersetD3 elim:) 
   2.423 +done
   2.424 +
   2.425 +lemma (in UFT) mem_chain_psubset_empty: 
   2.426 +          "!!(c :: 'a set set set). c: chain (superfrechet S)  
   2.427 +          ==> !x: c. {} < x"
   2.428 +by (auto simp add: chain_def Filter_def is_Filter_def superfrechet_def frechet_def)
   2.429 +
   2.430 +lemma (in UFT) chain_Un_not_empty: "!!(c :: 'a set set set).  
   2.431 +             [| c: chain (superfrechet S); 
   2.432 +                c ~= {} |] 
   2.433 +             ==> Union(c) ~= {}"
   2.434 +apply (drule mem_chain_psubset_empty)
   2.435 +apply (safe)
   2.436 +apply (drule bspec , assumption)
   2.437 +apply (auto dest: Union_upper bspec simp add: psubset_def)
   2.438 +done
   2.439 +
   2.440 +lemma (in UFT) Filter_empty_not_mem_Un: 
   2.441 +       "!!(c :: 'a set set set). c \<in> chain (superfrechet S) ==> {} ~: Union(c)"
   2.442 +by (auto simp add: is_Filter_def Filter_def chain_def superfrechet_def)
   2.443 +
   2.444 +lemma (in UFT) Filter_Un_Int: "c \<in> chain (superfrechet S)  
   2.445 +          ==> \<forall>u \<in> Union(c). \<forall>v \<in> Union(c). u Int v \<in> Union(c)"
   2.446 +apply (safe)
   2.447 +apply (frule_tac x = "X" and y = "Xa" in chainD)
   2.448 +apply (assumption)+
   2.449 +apply (drule chainD2)
   2.450 +apply (erule disjE)
   2.451 + apply (rule_tac [2] X = "X" in UnionI)
   2.452 +  apply (rule_tac X = "Xa" in UnionI)
   2.453 +apply (auto intro: mem_FiltersetD1 simp add: superfrechet_def)
   2.454 +done
   2.455 +
   2.456 +lemma (in UFT) Filter_Un_subset: "c \<in> chain (superfrechet S)  
   2.457 +          ==> \<forall>u v. u \<in> Union(c) &  
   2.458 +                  (u :: 'a set) <= v & v <= S --> v \<in> Union(c)"
   2.459 +apply (safe)
   2.460 +apply (drule chainD2)
   2.461 +apply (drule subsetD , assumption)
   2.462 +apply (rule UnionI , assumption)
   2.463 +apply (auto intro: mem_FiltersetD2 simp add: superfrechet_def)
   2.464 +done
   2.465 +
   2.466 +lemma (in UFT) lemma_mem_chain_Filter:
   2.467 +      "!!(c :: 'a set set set).  
   2.468 +             [| c \<in> chain (superfrechet S); 
   2.469 +                x \<in> c  
   2.470 +             |] ==> x \<in> Filter S"
   2.471 +by (auto simp add: chain_def superfrechet_def)
   2.472 +
   2.473 +lemma (in UFT) lemma_mem_chain_frechet_subset: 
   2.474 +     "!!(c :: 'a set set set).  
   2.475 +             [| c \<in> chain (superfrechet S); 
   2.476 +                x \<in> c  
   2.477 +             |] ==> frechet S <= x"
   2.478 +by (auto simp add: chain_def superfrechet_def)
   2.479 +
   2.480 +lemma (in UFT) Un_chain_mem_cofinite_Filter_set: "!!(c :: 'a set set set).  
   2.481 +          [| c ~= {};  
   2.482 +             c \<in> chain (superfrechet (UNIV :: 'a set)) 
   2.483 +          |] ==> Union c \<in> superfrechet (UNIV)"
   2.484 +apply (simp (no_asm) add: superfrechet_def frechet_def)
   2.485 +apply (safe)
   2.486 +apply (rule mem_FiltersetI2)
   2.487 +apply (erule chain_Un_subset_Pow)
   2.488 +apply (rule UnionI , assumption)
   2.489 +apply (erule lemma_mem_chain_Filter [THEN mem_FiltersetD4] , assumption)
   2.490 +apply (erule chain_Un_not_empty)
   2.491 +apply (erule_tac [2] Filter_empty_not_mem_Un)
   2.492 +apply (erule_tac [2] Filter_Un_Int)
   2.493 +apply (erule_tac [2] Filter_Un_subset)
   2.494 +apply (subgoal_tac [2] "xa \<in> frechet (UNIV) ")
   2.495 +apply (blast intro: elim:); 
   2.496 +apply (rule UnionI)
   2.497 +apply assumption; 
   2.498 +apply (rule lemma_mem_chain_frechet_subset [THEN subsetD])
   2.499 +apply (auto simp add: frechet_def)
   2.500 +done
   2.501 +
   2.502 +lemma (in UFT) max_cofinite_Filter_Ex: "\<exists>U \<in> superfrechet (UNIV).  
   2.503 +                \<forall>G \<in> superfrechet (UNIV). U <= G --> U = G"
   2.504 +apply (rule Zorn_Lemma2)
   2.505 +apply (insert not_finite_UNIV [THEN cofinite_Filter])
   2.506 +apply (safe)
   2.507 +apply (rule_tac Q = "c={}" in excluded_middle [THEN disjE])
   2.508 +apply (rule_tac x = "Union c" in bexI , blast)
   2.509 +apply (rule Un_chain_mem_cofinite_Filter_set);
   2.510 +apply (auto simp add: superfrechet_def frechet_def)
   2.511 +done
   2.512 +
   2.513 +lemma (in UFT) max_cofinite_Freefilter_Ex: "\<exists>U \<in> superfrechet UNIV. ( 
   2.514 +                \<forall>G \<in> superfrechet UNIV. U <= G --> U = G)   
   2.515 +                              & (\<forall>x \<in> U. ~finite x)"
   2.516 +apply (insert not_finite_UNIV [THEN UFT.max_cofinite_Filter_Ex]);
   2.517 +apply (safe)
   2.518 +apply (rule_tac x = "U" in bexI)
   2.519 +apply (auto simp add: superfrechet_def frechet_def)
   2.520 +apply (drule_tac c = "- x" in subsetD)
   2.521 +apply (simp (no_asm_simp))
   2.522 +apply (frule_tac A = "x" and B = "- x" in mem_FiltersetD1)
   2.523 +apply (drule_tac [3] Filter_empty_not_mem)
   2.524 +apply (auto ); 
   2.525 +done
   2.526 +
   2.527 +text{*There exists a free ultrafilter on any infinite set*}
   2.528 +
   2.529 +theorem (in UFT) FreeUltrafilter_ex: "\<exists>U. U \<in> FreeUltrafilter (UNIV :: 'a set)"
   2.530 +apply (simp add: FreeUltrafilter_def)
   2.531 +apply (insert not_finite_UNIV [THEN UFT.max_cofinite_Freefilter_Ex])
   2.532 +apply (simp add: superfrechet_def Ultrafilter_iff frechet_def)
   2.533 +apply (safe)
   2.534 +apply (rule_tac x = "U" in exI)
   2.535 +apply (safe)
   2.536 +apply blast
   2.537 +done
   2.538 +
   2.539 +theorems FreeUltrafilter_Ex = UFT.FreeUltrafilter_ex
   2.540 +
   2.541 +end
     3.1 --- a/src/HOL/Hyperreal/Integration.thy	Fri Jul 30 18:37:58 2004 +0200
     3.2 +++ b/src/HOL/Hyperreal/Integration.thy	Sat Jul 31 20:54:23 2004 +0200
     3.3 @@ -83,7 +83,7 @@
     3.4  apply (rotate_tac 2)
     3.5  apply (drule_tac x = N in spec, simp)
     3.6  apply (drule_tac x = Na in spec)
     3.7 -apply (drule_tac x = "Suc Na" and P = "%n. Na \<le> n \<longrightarrow> D n = D Na" in spec, auto)
     3.8 +apply (drule_tac x = "Suc Na" and P = "%n. Na\<le>n \<longrightarrow> D n = D Na" in spec, auto)
     3.9  done
    3.10  
    3.11  lemma partition_rhs: "partition(a,b) D ==> (D(psize D) = b)"
    3.12 @@ -203,7 +203,7 @@
    3.13  lemma lemma_psize1:
    3.14       "[| partition (a, b) D1; partition (b, c) D2; N < psize D1 |]
    3.15        ==> D1(N) < D2 (psize D2)"
    3.16 -apply (rule_tac y = "D1 (psize D1) " in order_less_le_trans)
    3.17 +apply (rule_tac y = "D1 (psize D1)" in order_less_le_trans)
    3.18  apply (erule partition_gt, assumption)
    3.19  apply (auto simp add: partition_rhs partition_le)
    3.20  done
    3.21 @@ -319,7 +319,7 @@
    3.22  apply (drule fine_min)
    3.23  apply (drule spec)+
    3.24  apply auto
    3.25 -apply (subgoal_tac "abs ((rsum (D,p) f - k2) - (rsum (D,p) f - k1)) < \<bar>k1 - k2\<bar> ")
    3.26 +apply (subgoal_tac "\<bar>(rsum (D,p) f - k2) - (rsum (D,p) f - k1)\<bar> < \<bar>k1 - k2\<bar>")
    3.27  apply arith
    3.28  apply (drule add_strict_mono, assumption)
    3.29  apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric] 
    3.30 @@ -363,7 +363,7 @@
    3.31  apply (rule exI, auto)
    3.32  apply (drule spec)+
    3.33  apply auto
    3.34 -apply (rule_tac z1 = "inverse (abs c) " in real_mult_less_iff1 [THEN iffD1])
    3.35 +apply (rule_tac z1 = "inverse (abs c)" in real_mult_less_iff1 [THEN iffD1])
    3.36  apply (auto simp add: divide_inverse [symmetric] right_diff_distrib [symmetric])
    3.37  done
    3.38  
    3.39 @@ -385,14 +385,14 @@
    3.40  
    3.41  
    3.42  (* new simplifications e.g. (y < x/n) = (y * n < x) are a real nuisance
    3.43 -   they break the original proofs and make new proofs longer!                 *)
    3.44 +   they break the original proofs and make new proofs longer!*)
    3.45  lemma strad1:
    3.46         "\<lbrakk>\<forall>xa::real. xa \<noteq> x \<and> \<bar>xa + - x\<bar> < s \<longrightarrow>
    3.47               \<bar>(f xa - f x) / (xa - x) + - f' x\<bar> * 2 < e;
    3.48          0 < e; a \<le> x; x \<le> b; 0 < s\<rbrakk>
    3.49         \<Longrightarrow> \<forall>z. \<bar>z - x\<bar> < s -->\<bar>f z - f x - f' x * (z - x)\<bar> * 2 \<le> e * \<bar>z - x\<bar>"
    3.50  apply auto
    3.51 -apply (case_tac "0 < \<bar>z - x\<bar> ")
    3.52 +apply (case_tac "0 < \<bar>z - x\<bar>")
    3.53   prefer 2 apply (simp add: zero_less_abs_iff)
    3.54  apply (drule_tac x = z in spec)
    3.55  apply (rule_tac z1 = "\<bar>inverse (z - x)\<bar>" 
    3.56 @@ -413,10 +413,12 @@
    3.57       "[| \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x); 0 < e |]
    3.58        ==> \<exists>g. gauge(%x. a \<le> x & x \<le> b) g &
    3.59                  (\<forall>x u v. a \<le> u & u \<le> x & x \<le> v & v \<le> b & (v - u) < g(x)
    3.60 -                  --> abs((f(v) - f(u)) - (f'(x) * (v - u))) \<le> e * (v - u))"
    3.61 +                  --> \<bar>(f(v) - f(u)) - (f'(x) * (v - u))\<bar> \<le> e * (v - u))"
    3.62  apply (simp add: gauge_def)
    3.63  apply (subgoal_tac "\<forall>x. a \<le> x & x \<le> b --> 
    3.64 -        (\<exists>d. 0 < d & (\<forall>u v. u \<le> x & x \<le> v & (v - u) < d --> abs ((f (v) - f (u)) - (f' (x) * (v - u))) \<le> e * (v - u)))")
    3.65 +        (\<exists>d. 0 < d & 
    3.66 +             (\<forall>u v. u \<le> x & x \<le> v & (v - u) < d --> 
    3.67 +                \<bar>(f (v) - f (u)) - (f' (x) * (v - u))\<bar> \<le> e * (v - u)))")
    3.68  apply (drule choiceP, auto)
    3.69  apply (drule spec, auto)
    3.70  apply (auto simp add: DERIV_iff2 LIM_def)
    3.71 @@ -424,13 +426,14 @@
    3.72  apply (frule strad1, assumption+)
    3.73  apply (rule_tac x = s in exI, auto)
    3.74  apply (rule_tac x = u and y = v in linorder_cases, auto)
    3.75 -apply (rule_tac j = "abs ((f (v) - f (x)) - (f' (x) * (v - x))) + abs ((f (x) - f (u)) - (f' (x) * (x - u)))"
    3.76 +apply (rule_tac j = "\<bar>(f (v) - f (x)) - (f' (x) * (v - x))\<bar> + 
    3.77 +                     \<bar>(f (x) - f (u)) - (f' (x) * (x - u))\<bar>"
    3.78         in real_le_trans)
    3.79  apply (rule abs_triangle_ineq [THEN [2] real_le_trans])
    3.80  apply (simp add: right_diff_distrib, arith)
    3.81 -apply (rule_tac t = "e* (v - u) " in real_sum_of_halves [THEN subst])
    3.82 +apply (rule_tac t = "e* (v - u)" in real_sum_of_halves [THEN subst])
    3.83  apply (rule add_mono)
    3.84 -apply (rule_tac j = " (e / 2) * \<bar>v - x\<bar> " in real_le_trans)
    3.85 +apply (rule_tac j = " (e / 2) * \<bar>v - x\<bar>" in real_le_trans)
    3.86   prefer 2 apply simp apply arith
    3.87  apply (erule_tac [!]
    3.88         V= "\<forall>xa. xa ~= x & \<bar>xa + - x\<bar> < s --> \<bar>(f xa - f x) / (xa - x) + - f' x\<bar> * 2 < e"
    3.89 @@ -453,19 +456,19 @@
    3.90  apply (drule_tac x = "e/2" in spec, auto)
    3.91  apply (drule spec, auto)
    3.92  apply ((drule spec)+, auto)
    3.93 -apply (drule_tac e = "ea/ (b - a) " in lemma_straddle)
    3.94 +apply (drule_tac e = "ea/ (b - a)" in lemma_straddle)
    3.95  apply (auto simp add: zero_less_divide_iff)
    3.96  apply (rule exI)
    3.97  apply (auto simp add: tpart_def rsum_def)
    3.98 -apply (subgoal_tac "sumr 0 (psize D) (%n. f (D (Suc n)) - f (D n)) = f b - f a")
    3.99 +apply (subgoal_tac "sumr 0 (psize D) (%n. f(D(Suc n)) - f(D n)) = f b - f a")
   3.100   prefer 2
   3.101 - apply (cut_tac D = "%n. f (D n) " and m = "psize D"
   3.102 + apply (cut_tac D = "%n. f (D n)" and m = "psize D"
   3.103          in sumr_partition_eq_diff_bounds)
   3.104   apply (simp add: partition_lhs partition_rhs)
   3.105  apply (drule sym, simp)
   3.106  apply (simp (no_asm) add: sumr_diff)
   3.107  apply (rule sumr_rabs [THEN real_le_trans])
   3.108 -apply (subgoal_tac "ea = sumr 0 (psize D) (%n. (ea / (b - a)) * (D (Suc n) - (D n))) ")
   3.109 +apply (subgoal_tac "ea = sumr 0 (psize D) (%n. (ea / (b - a)) * (D (Suc n) - (D n)))")
   3.110  apply (simp add: abs_minus_commute)
   3.111  apply (rule_tac t = ea in ssubst, assumption)
   3.112  apply (rule sumr_le2)
   3.113 @@ -775,8 +778,8 @@
   3.114  apply (drule_tac x = "na + n" in spec)
   3.115  apply (frule_tac n = n in tpart_partition [THEN better_lemma_psize_right_eq], auto, arith)
   3.116  apply (simp add: tpart_def, safe)
   3.117 -apply (subgoal_tac "D n \<le> p (na + n) ")
   3.118 -apply (drule_tac y = "p (na + n) " in real_le_imp_less_or_eq)
   3.119 +apply (subgoal_tac "D n \<le> p (na + n)")
   3.120 +apply (drule_tac y = "p (na + n)" in real_le_imp_less_or_eq)
   3.121  apply safe
   3.122  apply (simp split: split_if_asm, simp)
   3.123  apply (drule less_le_trans, assumption)
   3.124 @@ -790,7 +793,7 @@
   3.125  lemma rsum_add: "rsum (D, p) (%x. f x + g x) =  rsum (D, p) f + rsum(D, p) g"
   3.126  by (simp add: rsum_def sumr_add left_distrib)
   3.127  
   3.128 -(* Bartle/Sherbert: Theorem 10.1.5 p. 278 *)
   3.129 +text{* Bartle/Sherbert: Theorem 10.1.5 p. 278 *}
   3.130  lemma Integral_add_fun:
   3.131      "[| a \<le> b; Integral(a,b) f k1; Integral(a,b) g k2 |]
   3.132       ==> Integral(a,b) (%x. f x + g x) (k1 + k2)"
   3.133 @@ -798,7 +801,7 @@
   3.134  apply ((drule_tac x = "e/2" in spec)+)
   3.135  apply auto
   3.136  apply (drule gauge_min, assumption)
   3.137 -apply (rule_tac x = " (%x. if ga x < gaa x then ga x else gaa x) " in exI)
   3.138 +apply (rule_tac x = " (%x. if ga x < gaa x then ga x else gaa x)" in exI)
   3.139  apply auto
   3.140  apply (drule fine_min)
   3.141  apply ((drule spec)+, auto)
   3.142 @@ -852,7 +855,7 @@
   3.143  apply (drule_tac x = D in spec, drule_tac x = D in spec)
   3.144  apply (drule_tac x = p in spec, drule_tac x = p in spec, auto)
   3.145  apply (frule lemma_Integral_rsum_le, assumption)
   3.146 -apply (subgoal_tac "\<bar>(rsum (D,p) f - k1) - (rsum (D,p) g - k2)\<bar> < \<bar>k1 - k2\<bar> ")
   3.147 +apply (subgoal_tac "\<bar>(rsum (D,p) f - k1) - (rsum (D,p) g - k2)\<bar> < \<bar>k1 - k2\<bar>")
   3.148  apply arith
   3.149  apply (drule add_strict_mono, assumption)
   3.150  apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
     4.1 --- a/src/HOL/IsaMakefile	Fri Jul 30 18:37:58 2004 +0200
     4.2 +++ b/src/HOL/IsaMakefile	Sat Jul 31 20:54:23 2004 +0200
     4.3 @@ -144,10 +144,9 @@
     4.4    Real/Lubs.thy Real/rat_arith.ML\
     4.5    Real/Rational.thy Real/PReal.thy Real/RComplete.thy \
     4.6    Real/ROOT.ML Real/Real.thy Real/real_arith.ML Real/RealDef.thy \
     4.7 -  Real/RealPow.thy Real/document/root.tex Real/real_arith.ML\
     4.8 -  Hyperreal/EvenOdd.thy\
     4.9 -  Hyperreal/Fact.ML Hyperreal/Fact.thy Hyperreal/HLog.thy\
    4.10 -  Hyperreal/Filter.ML Hyperreal/Filter.thy Hyperreal/HSeries.thy\
    4.11 +  Real/RealPow.thy Real/document/root.tex\
    4.12 +  Hyperreal/EvenOdd.thy Hyperreal/Fact.thy Hyperreal/HLog.thy\
    4.13 +  Hyperreal/Filter.thy Hyperreal/HSeries.thy\
    4.14    Hyperreal/HTranscendental.thy Hyperreal/HyperArith.thy\
    4.15    Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy\
    4.16    Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\