conversion of Integration and NSPrimes to Isar scripts
authorpaulson
Fri Jul 30 18:37:58 2004 +0200 (2004-07-30)
changeset 1509349ede01e9ee6
parent 15092 7fe7f022476c
child 15094 a7d1a3fdc30d
conversion of Integration and NSPrimes to Isar scripts
src/HOL/Complex/ex/NSPrimes.ML
src/HOL/Complex/ex/NSPrimes.thy
src/HOL/Hyperreal/Integration.ML
src/HOL/Hyperreal/Integration.thy
src/HOL/IsaMakefile
src/HOL/OrderedGroup.thy
     1.1 --- a/src/HOL/Complex/ex/NSPrimes.ML	Fri Jul 30 10:44:42 2004 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,491 +0,0 @@
     1.4 -(*  Title       : NSPrimes.ML
     1.5 -    Author      : Jacques D. Fleuriot
     1.6 -    Copyright   : 2002 University of Edinburgh
     1.7 -    Description : The nonstandard primes as an extension of 
     1.8 -                  the prime numbers
     1.9 -*)
    1.10 -
    1.11 -(*--------------------------------------------------------------*) 
    1.12 -(* A "choice" theorem for ultrafilters cf. almost everywhere    *)
    1.13 -(* quantification                                               *)
    1.14 -(*--------------------------------------------------------------*) 
    1.15 -    
    1.16 -Goal "{n. EX m. Q n m} : FreeUltrafilterNat \
    1.17 -\     ==> EX f. {n. Q n (f n)} : FreeUltrafilterNat";
    1.18 -by (res_inst_tac [("x","%n. (@x. Q n x)")] exI 1);
    1.19 -by (Ultra_tac 1 THEN rtac someI 1 THEN Auto_tac);
    1.20 -qed "UF_choice";
    1.21 -
    1.22 -Goal "({n. P n} : FreeUltrafilterNat --> {n. Q n} : FreeUltrafilterNat) = \
    1.23 -\     ({n. P n --> Q n} : FreeUltrafilterNat)";
    1.24 -by Auto_tac;
    1.25 -by (ALLGOALS(Ultra_tac));
    1.26 -qed "UF_if";
    1.27 -
    1.28 -Goal "({n. P n} : FreeUltrafilterNat & {n. Q n} : FreeUltrafilterNat) = \
    1.29 -\     ({n. P n & Q n} : FreeUltrafilterNat)";
    1.30 -by Auto_tac;
    1.31 -by (ALLGOALS(Ultra_tac));
    1.32 -qed "UF_conj";
    1.33 -
    1.34 -Goal "(ALL f. {n. Q n (f n)} : FreeUltrafilterNat) = \
    1.35 -\     ({n. ALL m. Q n m} : FreeUltrafilterNat)";
    1.36 -by Auto_tac;
    1.37 -by (Ultra_tac 2);
    1.38 -by (rtac ccontr 1);
    1.39 -by (rtac swap 1 THEN assume_tac 2);
    1.40 -by (simp_tac (simpset() addsimps [FreeUltrafilterNat_Compl_iff1,
    1.41 -    CLAIM "-{n. Q n} = {n. ~ Q n}"]) 1);
    1.42 -by (rtac UF_choice 1);
    1.43 -by (Ultra_tac 1 THEN Auto_tac);
    1.44 -qed "UF_choice_ccontr";
    1.45 -
    1.46 -Goal "ALL M. EX N. 0 < N & (ALL m. 0 < m & (m::nat) <= M --> m dvd N)";
    1.47 -by (rtac allI 1);
    1.48 -by (induct_tac "M" 1);
    1.49 -by Auto_tac;
    1.50 -by (res_inst_tac [("x","N * (Suc n)")] exI 1);
    1.51 -by (Step_tac 1 THEN Force_tac 1);
    1.52 -by (dtac le_imp_less_or_eq 1 THEN etac disjE 1);
    1.53 -by (force_tac (claset() addSIs [dvd_mult2],simpset()) 1);
    1.54 -by (force_tac (claset() addSIs [dvd_mult],simpset()) 1);
    1.55 -qed "dvd_by_all";
    1.56 -
    1.57 -bind_thm ("dvd_by_all2",dvd_by_all RS spec);
    1.58 -
    1.59 -Goal "(EX (x::hypnat). P x) = (EX f. P (Abs_hypnat(hypnatrel `` {f})))";
    1.60 -by Auto_tac;
    1.61 -by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
    1.62 -by Auto_tac;
    1.63 -qed "lemma_hypnat_P_EX";
    1.64 -
    1.65 -Goal "(ALL (x::hypnat). P x) = (ALL f. P (Abs_hypnat(hypnatrel `` {f})))";
    1.66 -by Auto_tac;
    1.67 -by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
    1.68 -by Auto_tac;
    1.69 -qed "lemma_hypnat_P_ALL";
    1.70 -
    1.71 -Goalw [hdvd_def]
    1.72 -      "(Abs_hypnat(hypnatrel``{%n. X n}) hdvd \
    1.73 -\           Abs_hypnat(hypnatrel``{%n. Y n})) = \
    1.74 -\      ({n. X n dvd Y n} : FreeUltrafilterNat)";
    1.75 -by (Auto_tac THEN Ultra_tac 1);
    1.76 -qed "hdvd";
    1.77 -
    1.78 -Goal "(hypnat_of_nat n <= 0) = (n = 0)";
    1.79 -by (stac (hypnat_of_nat_zero RS sym) 1);
    1.80 -by Auto_tac;
    1.81 -qed "hypnat_of_nat_le_zero_iff";
    1.82 -Addsimps [hypnat_of_nat_le_zero_iff];
    1.83 -
    1.84 -
    1.85 -(* Goldblatt: Exercise 5.11(2) - p. 57 *)
    1.86 -Goal "ALL M. EX N. 0 < N & (ALL m. 0 < m & (m::hypnat) <= M --> m hdvd N)";
    1.87 -by (Step_tac 1);
    1.88 -by (res_inst_tac [("z","M")] eq_Abs_hypnat 1);
    1.89 -by (auto_tac (claset(),simpset() addsimps [lemma_hypnat_P_EX,
    1.90 -    lemma_hypnat_P_ALL,hypnat_zero_def,hypnat_le,hypnat_less,hdvd]));
    1.91 -by (cut_facts_tac [dvd_by_all] 1);
    1.92 -by (dtac (CLAIM "(ALL (M::nat). EX N. 0 < N & (ALL m. 0 < m & m <= M \
    1.93 -\                               --> m dvd N)) \
    1.94 -\                ==> ALL (n::nat). EX N. 0 < N & (ALL m. 0 < (m::nat) & m <= (x n) \
    1.95 -\                                  --> m dvd N)") 1);
    1.96 -by (dtac choice 1);
    1.97 -by (Step_tac 1);
    1.98 -by (res_inst_tac [("x","f")] exI 1);
    1.99 -by Auto_tac;
   1.100 -by (ALLGOALS(Ultra_tac));
   1.101 -by Auto_tac;
   1.102 -qed "hdvd_by_all";
   1.103 -
   1.104 -bind_thm ("hdvd_by_all2",hdvd_by_all RS spec);
   1.105 -
   1.106 -(* Goldblatt: Exercise 5.11(2) - p. 57 *)
   1.107 -Goal "EX (N::hypnat). 0 < N & (ALL n : - {0::nat}. hypnat_of_nat(n) hdvd N)"; 
   1.108 -by (cut_facts_tac [hdvd_by_all] 1);
   1.109 -by (dres_inst_tac [("x","whn")] spec 1);
   1.110 -by Auto_tac;
   1.111 -by (rtac exI 1 THEN Auto_tac);
   1.112 -by (dres_inst_tac [("x","hypnat_of_nat n")] spec 1);
   1.113 -by (auto_tac (claset(),
   1.114 -     simpset() addsimps [linorder_not_less, hypnat_of_nat_zero_iff]));
   1.115 -qed "hypnat_dvd_all_hypnat_of_nat";
   1.116 -
   1.117 -
   1.118 -(*--------------------------------------------------------------*)
   1.119 -(* the nonstandard extension of the set prime numbers consists  *)
   1.120 -(* of precisely those hypernaturals > 1 that have no nontrivial *)
   1.121 -(* factors                                                      *)
   1.122 -(*--------------------------------------------------------------*) 
   1.123 -
   1.124 -(* Goldblatt: Exercise 5.11(3a) - p 57  *)
   1.125 -Goalw [starprime_def,thm "prime_def"]
   1.126 -  "starprime = {p. 1 < p & (ALL m. m hdvd p --> m = 1 | m = p)}";
   1.127 -by (auto_tac (claset(),simpset() addsimps 
   1.128 -    [CLAIM "{p. Q(p) & R(p)} = {p. Q(p)} Int {p. R(p)}",NatStar_Int]));
   1.129 -by (ALLGOALS(res_inst_tac [("z","x")] eq_Abs_hypnat));
   1.130 -by (res_inst_tac [("z","m")] eq_Abs_hypnat 2);
   1.131 -by (auto_tac (claset(),simpset() addsimps [hdvd,hypnat_one_def,hypnat_less,
   1.132 -    lemma_hypnat_P_ALL,starsetNat_def]));
   1.133 -by (dtac bspec 1 THEN dtac bspec 2 THEN Auto_tac);
   1.134 -by (Ultra_tac 1 THEN Ultra_tac 1); 
   1.135 -by (rtac ccontr 1);
   1.136 -by (dtac FreeUltrafilterNat_Compl_mem 1);
   1.137 -by (auto_tac (claset(),simpset() addsimps [CLAIM "- {p. Q p} = {p. ~ Q p}"]));
   1.138 -by (dtac UF_choice 1 THEN Auto_tac);
   1.139 -by (dres_inst_tac [("x","f")] spec 1 THEN Auto_tac);
   1.140 -by (ALLGOALS(Ultra_tac));
   1.141 -qed "starprime";
   1.142 -
   1.143 -Goalw [thm "prime_def"] "2 : prime";
   1.144 -by Auto_tac;
   1.145 -by (ftac dvd_imp_le 1);
   1.146 -by (auto_tac (claset() addDs [dvd_0_left],simpset() addsimps 
   1.147 -    [ARITH_PROVE "(m <= (2::nat)) = (m = 0 | m = 1 | m = 2)"]));
   1.148 -qed "prime_two";
   1.149 -Addsimps [prime_two];
   1.150 -
   1.151 -(* proof uses course-of-value induction *)
   1.152 -Goal "Suc 0 < n --> (EX k : prime. k dvd n)";
   1.153 -by (res_inst_tac [("n","n")] nat_less_induct 1);
   1.154 -by Auto_tac;
   1.155 -by (case_tac "n : prime" 1);
   1.156 -by (res_inst_tac [("x","n")] bexI 1 THEN Auto_tac);
   1.157 -by (dtac (conjI RS (thm "not_prime_ex_mk")) 1 THEN Auto_tac);
   1.158 -by (dres_inst_tac [("x","m")] spec 1 THEN Auto_tac);
   1.159 -by (res_inst_tac [("x","ka")] bexI 1);
   1.160 -by (auto_tac (claset() addIs [dvd_mult2],simpset()));
   1.161 -qed_spec_mp "prime_factor_exists";
   1.162 -
   1.163 -(* Goldblatt Exercise 5.11(3b) - p 57  *)
   1.164 -Goal "1 < n ==> (EX k : starprime. k hdvd n)";
   1.165 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.166 -by (auto_tac (claset(),simpset() addsimps [hypnat_one_def,
   1.167 -    hypnat_less,starprime_def,lemma_hypnat_P_EX,lemma_hypnat_P_ALL,
   1.168 -    hdvd,starsetNat_def,CLAIM "(ALL X: S. P X) = (ALL X. X : S --> P X)",
   1.169 -    UF_if]));
   1.170 -by (res_inst_tac [("x","%n. @y. y : prime & y dvd x n")] exI 1);
   1.171 -by Auto_tac;
   1.172 -by (ALLGOALS (Ultra_tac));
   1.173 -by (dtac sym 1 THEN Asm_simp_tac 1);
   1.174 -by (ALLGOALS(rtac someI2_ex));
   1.175 -by (auto_tac (claset() addSDs [prime_factor_exists],simpset()));
   1.176 -qed_spec_mp "hyperprime_factor_exists";
   1.177 -
   1.178 -(* behaves as expected! *)
   1.179 -Goal "( *sNat* insert x A) = insert (hypnat_of_nat x) ( *sNat* A)";
   1.180 -by (auto_tac (claset(),simpset() addsimps [starsetNat_def,
   1.181 -    hypnat_of_nat_eq]));
   1.182 -by (ALLGOALS(res_inst_tac [("z","xa")] eq_Abs_hypnat));
   1.183 -by Auto_tac;
   1.184 -by (TRYALL(dtac bspec));
   1.185 -by Auto_tac;
   1.186 -by (ALLGOALS(Ultra_tac));
   1.187 -qed "NatStar_insert";
   1.188 -
   1.189 -(* Goldblatt Exercise 3.10(1) - p. 29 *)
   1.190 -Goal "finite A ==> *sNat* A = hypnat_of_nat ` A";
   1.191 -by (res_inst_tac [("P","%x. *sNat* x = hypnat_of_nat ` x")] finite_induct 1);
   1.192 -by (auto_tac (claset(),simpset() addsimps [NatStar_insert]));
   1.193 -qed "NatStar_hypnat_of_nat";
   1.194 -
   1.195 -(* proved elsewhere? *)
   1.196 -Goal "{x} ~: FreeUltrafilterNat";
   1.197 -by (auto_tac (claset() addSIs [FreeUltrafilterNat_finite],simpset()));
   1.198 -qed "FreeUltrafilterNat_singleton_not_mem";
   1.199 -Addsimps [FreeUltrafilterNat_singleton_not_mem];
   1.200 -
   1.201 -(*-------------------------------------------------------------------------------*)
   1.202 -(* Another characterization of infinite set of natural numbers                   *)
   1.203 -(*-------------------------------------------------------------------------------*)
   1.204 -
   1.205 -Goal "finite N ==> EX n. (ALL i:N. i<(n::nat))";
   1.206 -by (eres_inst_tac [("F","N")] finite_induct 1);
   1.207 -by Auto_tac;
   1.208 -by (res_inst_tac [("x","Suc n + x")] exI 1);
   1.209 -by Auto_tac;
   1.210 -qed "finite_nat_set_bounded";
   1.211 -
   1.212 -Goal "finite N = (EX n. (ALL i:N. i<(n::nat)))";
   1.213 -by (blast_tac (claset() addIs [finite_nat_set_bounded,
   1.214 -    bounded_nat_set_is_finite]) 1);
   1.215 -qed "finite_nat_set_bounded_iff";
   1.216 -
   1.217 -Goal "(~ finite N) = (ALL n. EX i:N. n <= (i::nat))";
   1.218 -by (auto_tac (claset(),simpset() addsimps [finite_nat_set_bounded_iff,
   1.219 -    le_def]));
   1.220 -qed "not_finite_nat_set_iff";
   1.221 -
   1.222 -Goal "(ALL i:N. i<=(n::nat)) ==> finite N";
   1.223 -by (rtac finite_subset 1);
   1.224 - by (rtac finite_atMost 2);
   1.225 -by Auto_tac;
   1.226 -qed "bounded_nat_set_is_finite2";
   1.227 -
   1.228 -Goal "finite N ==> EX n. (ALL i:N. i<=(n::nat))";
   1.229 -by (eres_inst_tac [("F","N")] finite_induct 1);
   1.230 -by Auto_tac;
   1.231 -by (res_inst_tac [("x","n + x")] exI 1);
   1.232 -by Auto_tac;
   1.233 -qed "finite_nat_set_bounded2";
   1.234 -
   1.235 -Goal "finite N = (EX n. (ALL i:N. i<=(n::nat)))";
   1.236 -by (blast_tac (claset() addIs [finite_nat_set_bounded2,
   1.237 -    bounded_nat_set_is_finite2]) 1);
   1.238 -qed "finite_nat_set_bounded_iff2";
   1.239 -
   1.240 -Goal "(~ finite N) = (ALL n. EX i:N. n < (i::nat))";
   1.241 -by (auto_tac (claset(),simpset() addsimps [finite_nat_set_bounded_iff2,
   1.242 -    le_def]));
   1.243 -qed "not_finite_nat_set_iff2";
   1.244 -
   1.245 -(*-------------------------------------------------------------------------------*)
   1.246 -(* An injective function cannot define an embedded natural number                *)
   1.247 -(*-------------------------------------------------------------------------------*)
   1.248 -
   1.249 -Goal "ALL m n. m ~= n --> f n ~= f m \
   1.250 -\     ==>  {n. f n = N} = {} |  (EX m. {n. f n = N} = {m})";
   1.251 -by Auto_tac;
   1.252 -by (dres_inst_tac [("x","x")] spec 1 THEN Auto_tac); 
   1.253 -by (subgoal_tac "ALL n. (f n = f x) = (x = n)" 1);
   1.254 -by Auto_tac;
   1.255 -qed "lemma_infinite_set_singleton";
   1.256 -
   1.257 -Goal "inj f ==> Abs_hypnat(hypnatrel `` {f}) ~: Nats";
   1.258 -by (auto_tac (claset(), simpset() addsimps [SHNat_eq,hypnat_of_nat_eq])); 
   1.259 -by (subgoal_tac "ALL m n. m ~= n --> f n ~= f m" 1);
   1.260 -by Auto_tac;
   1.261 -by (dtac injD 2);
   1.262 -by (assume_tac 2 THEN Force_tac 2);
   1.263 -by (dres_inst_tac[("N","N")] lemma_infinite_set_singleton 1);
   1.264 -by Auto_tac;
   1.265 -qed "inj_fun_not_hypnat_in_SHNat";
   1.266 -
   1.267 -Goalw [starsetNat_def] 
   1.268 -   "range f <= A ==> Abs_hypnat(hypnatrel `` {f}) : *sNat* A";
   1.269 -by Auto_tac;
   1.270 -by (Ultra_tac 1);
   1.271 -by (dres_inst_tac [("c","f x")] subsetD 1);
   1.272 -by (rtac rangeI 1);
   1.273 -by Auto_tac;
   1.274 -qed "range_subset_mem_starsetNat";
   1.275 -
   1.276 -(*--------------------------------------------------------------------------------*)
   1.277 -(* Gleason Proposition 11-5.5. pg 149, pg 155 (ex. 3) and pg. 360                 *)
   1.278 -(* Let E be a nonvoid ordered set with no maximal elements (note: effectively an  *) 
   1.279 -(* infinite set if we take E = N (Nats)). Then there exists an order-preserving   *) 
   1.280 -(* injection from N to E. Of course, (as some doofus will undoubtedly point out!  *)
   1.281 -(* :-)) can use notion of least element in proof (i.e. no need for choice) if     *)
   1.282 -(* dealing with nats as we have well-ordering property                            *) 
   1.283 -(*--------------------------------------------------------------------------------*)
   1.284 -
   1.285 -Goal "E ~= {} ==> EX x. EX X : (Pow E - {{}}). x: X";
   1.286 -by Auto_tac;
   1.287 -val lemmaPow3 = result();
   1.288 -
   1.289 -Goalw [choicefun_def] "E ~= {} ==> choicefun E : E";
   1.290 -by (rtac (lemmaPow3 RS someI2_ex) 1);
   1.291 -by Auto_tac;
   1.292 -qed "choicefun_mem_set";
   1.293 -Addsimps [choicefun_mem_set];
   1.294 -
   1.295 -Goal "[| E ~={}; ALL x. EX y: E. x < y |] ==> injf_max n E : E";
   1.296 -by (induct_tac "n" 1);
   1.297 -by (Force_tac 1);
   1.298 -by (simp_tac (simpset() addsimps [choicefun_def]) 1);
   1.299 -by (rtac (lemmaPow3 RS someI2_ex) 1);
   1.300 -by Auto_tac;
   1.301 -qed "injf_max_mem_set";
   1.302 -
   1.303 -Goal "ALL x. EX y: E. x < y ==> injf_max n E < injf_max (Suc n) E";
   1.304 -by (simp_tac (simpset() addsimps [choicefun_def]) 1);
   1.305 -by (rtac (lemmaPow3 RS someI2_ex) 1);
   1.306 -by Auto_tac;
   1.307 -qed "injf_max_order_preserving";
   1.308 -
   1.309 -Goal "ALL x. EX y: E. x < y \
   1.310 -\     ==> ALL n m. m < n --> injf_max m E < injf_max n E";
   1.311 -by (rtac allI 1);
   1.312 -by (induct_tac "n" 1);
   1.313 -by Auto_tac;
   1.314 -by (simp_tac (simpset() addsimps [choicefun_def]) 1);
   1.315 -by (rtac (lemmaPow3 RS someI2_ex) 1);
   1.316 -by Auto_tac;
   1.317 -by (dtac (CLAIM "m < Suc n ==> m = n | m < n") 1);
   1.318 -by Auto_tac;
   1.319 -by (dres_inst_tac [("x","m")] spec 1);
   1.320 -by Auto_tac;
   1.321 -by (dtac subsetD 1 THEN Auto_tac);
   1.322 -by (dres_inst_tac [("x","injf_max m E")] order_less_trans 1);
   1.323 -by Auto_tac;
   1.324 -qed "injf_max_order_preserving2";
   1.325 -
   1.326 -Goal "ALL x. EX y: E. x < y ==> inj (%n. injf_max n E)";
   1.327 -by (rtac injI 1);
   1.328 -by (rtac ccontr 1);
   1.329 -by Auto_tac;
   1.330 -by (dtac injf_max_order_preserving2 1);
   1.331 -by (cut_inst_tac [("m","x"),("n","y")] less_linear 1);
   1.332 -by Auto_tac;
   1.333 -by (auto_tac (claset() addSDs [spec],simpset()));
   1.334 -qed "inj_injf_max";
   1.335 -
   1.336 -Goal "[| (E::('a::{order} set)) ~= {}; ALL x. EX y: E. x < y |] \
   1.337 -\     ==> EX f. range f <= E & inj (f::nat => 'a) & (ALL m. f m < f(Suc m))";
   1.338 -by (res_inst_tac [("x","%n. injf_max n E")] exI 1);
   1.339 -by (Step_tac 1);
   1.340 -by (rtac injf_max_mem_set 1);
   1.341 -by (rtac inj_injf_max 3);
   1.342 -by (rtac injf_max_order_preserving 4);
   1.343 -by Auto_tac;
   1.344 -qed "infinite_set_has_order_preserving_inj";
   1.345 -
   1.346 -(*-------------------------------------------------------------------------------*)
   1.347 -(* Only need fact that we can have an injective function from N to A for proof   *)
   1.348 -(*-------------------------------------------------------------------------------*)
   1.349 -
   1.350 -Goal "~ finite A ==> hypnat_of_nat ` A < ( *sNat* A)";
   1.351 -by Auto_tac;
   1.352 -by (rtac subsetD 1);
   1.353 -by (rtac NatStar_hypreal_of_real_image_subset 1);
   1.354 -by Auto_tac;
   1.355 -by (subgoal_tac "A ~= {}" 1);
   1.356 -by (Force_tac 2);
   1.357 -by (dtac infinite_set_has_order_preserving_inj 1);
   1.358 -by (etac (not_finite_nat_set_iff2 RS iffD1) 1);
   1.359 -by Auto_tac;
   1.360 -by (dtac inj_fun_not_hypnat_in_SHNat 1);
   1.361 -by (dtac range_subset_mem_starsetNat 1);
   1.362 -by (auto_tac (claset(),simpset() addsimps [SHNat_eq]));
   1.363 -qed "hypnat_infinite_has_nonstandard";
   1.364 -
   1.365 -Goal "*sNat* A =  hypnat_of_nat ` A ==> finite A";
   1.366 -by (rtac ccontr 1);
   1.367 -by (auto_tac (claset() addDs [hypnat_infinite_has_nonstandard],
   1.368 -    simpset()));
   1.369 -qed "starsetNat_eq_hypnat_of_nat_image_finite";
   1.370 -
   1.371 -Goal "( *sNat* A = hypnat_of_nat ` A) = (finite A)";
   1.372 -by (blast_tac (claset() addSIs [starsetNat_eq_hypnat_of_nat_image_finite,
   1.373 -    NatStar_hypnat_of_nat]) 1);
   1.374 -qed "finite_starsetNat_iff";
   1.375 -
   1.376 -Goal "(~ finite A) = (hypnat_of_nat ` A < *sNat* A)";
   1.377 -by (rtac iffI 1);
   1.378 -by (blast_tac (claset() addSIs [hypnat_infinite_has_nonstandard]) 1);
   1.379 -by (auto_tac (claset(),simpset() addsimps [finite_starsetNat_iff RS sym]));
   1.380 -qed "hypnat_infinite_has_nonstandard_iff";
   1.381 -
   1.382 -
   1.383 -(*-------------------------------------------------------------------------------*)
   1.384 -(* Existence of infinitely many primes: a nonstandard proof                      *)
   1.385 -(*-------------------------------------------------------------------------------*)
   1.386 -
   1.387 -Goal "~ (ALL n:- {0}. hypnat_of_nat n hdvd 1)";
   1.388 -by Auto_tac;
   1.389 -by (res_inst_tac [("x","2")] bexI 1);
   1.390 -by (auto_tac (claset(),simpset() addsimps [hypnat_of_nat_eq,
   1.391 -    hypnat_one_def,hdvd,dvd_def]));
   1.392 -val lemma_not_dvd_hypnat_one = result();
   1.393 -Addsimps [lemma_not_dvd_hypnat_one];
   1.394 -
   1.395 -Goal "EX n:- {0}. ~ hypnat_of_nat n hdvd 1";
   1.396 -by (cut_facts_tac [lemma_not_dvd_hypnat_one] 1);
   1.397 -by (auto_tac (claset(),simpset() delsimps [lemma_not_dvd_hypnat_one]));
   1.398 -val lemma_not_dvd_hypnat_one2 = result();
   1.399 -Addsimps [lemma_not_dvd_hypnat_one2];
   1.400 -
   1.401 -(* not needed here *)
   1.402 -Goalw [hypnat_zero_def,hypnat_one_def] 
   1.403 -  "[| 0 < (N::hypnat); N ~= 1 |] ==> 1 < N";
   1.404 -by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
   1.405 -by (auto_tac (claset(),simpset() addsimps [hypnat_less]));
   1.406 -by (Ultra_tac 1);
   1.407 -qed "hypnat_gt_zero_gt_one";
   1.408 -
   1.409 -Goalw [hypnat_zero_def,hypnat_one_def]
   1.410 -    "0 < N ==> 1 < (N::hypnat) + 1";
   1.411 -by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
   1.412 -by (auto_tac (claset(),simpset() addsimps [hypnat_less,hypnat_add]));
   1.413 -qed "hypnat_add_one_gt_one";
   1.414 -
   1.415 -Goal "0 ~: prime";
   1.416 -by (Step_tac 1);
   1.417 -by (dtac (thm "prime_g_zero") 1);
   1.418 -by Auto_tac;
   1.419 -qed "zero_not_prime";
   1.420 -Addsimps [zero_not_prime];
   1.421 -
   1.422 -Goal "hypnat_of_nat 0 ~: starprime";
   1.423 -by (auto_tac (claset() addSIs [bexI],
   1.424 -      simpset() addsimps [starprime_def,starsetNat_def,hypnat_of_nat_eq]));
   1.425 -qed "hypnat_of_nat_zero_not_prime";
   1.426 -Addsimps [hypnat_of_nat_zero_not_prime];
   1.427 -
   1.428 -Goalw [starprime_def,starsetNat_def,hypnat_zero_def]
   1.429 -   "0 ~: starprime";
   1.430 -by (auto_tac (claset() addSIs [bexI],simpset()));
   1.431 -qed "hypnat_zero_not_prime";
   1.432 -Addsimps [hypnat_zero_not_prime];
   1.433 -
   1.434 -Goal "1 ~: prime";
   1.435 -by (Step_tac 1);
   1.436 -by (dtac (thm "prime_g_one") 1);
   1.437 -by Auto_tac;
   1.438 -qed "one_not_prime";
   1.439 -Addsimps [one_not_prime];
   1.440 -
   1.441 -Goal "Suc 0 ~: prime";
   1.442 -by (Step_tac 1);
   1.443 -by (dtac (thm "prime_g_one") 1);
   1.444 -by Auto_tac;
   1.445 -qed "one_not_prime2";
   1.446 -Addsimps [one_not_prime2];
   1.447 -
   1.448 -Goal "hypnat_of_nat 1 ~: starprime";
   1.449 -by (auto_tac (claset() addSIs [bexI],
   1.450 -     simpset() addsimps [starprime_def,starsetNat_def,hypnat_of_nat_eq]));
   1.451 -qed "hypnat_of_nat_one_not_prime";
   1.452 -Addsimps [hypnat_of_nat_one_not_prime];
   1.453 -
   1.454 -Goalw [starprime_def,starsetNat_def,hypnat_one_def]
   1.455 -   "1 ~: starprime";
   1.456 -by (auto_tac (claset() addSIs [bexI],simpset()));
   1.457 -qed "hypnat_one_not_prime";
   1.458 -Addsimps [hypnat_one_not_prime];
   1.459 -
   1.460 -Goal "[| k hdvd m; k hdvd n |] ==> k hdvd (m - n)";
   1.461 -by (res_inst_tac [("z","k")] eq_Abs_hypnat 1);
   1.462 -by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
   1.463 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.464 -by (auto_tac (claset(),simpset() addsimps [hdvd,hypnat_minus]));
   1.465 -by (Ultra_tac 1);
   1.466 -by (blast_tac (claset() addIs [dvd_diff]) 1);
   1.467 -qed "hdvd_diff";
   1.468 -
   1.469 -Goalw [dvd_def] "x dvd (1::nat) ==> x = 1";
   1.470 -by Auto_tac;
   1.471 -qed "dvd_one_eq_one";
   1.472 -
   1.473 -Goalw [hypnat_one_def] "x hdvd 1 ==> x = 1";
   1.474 -by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   1.475 -by (auto_tac (claset(),simpset() addsimps [hdvd]));
   1.476 -qed "hdvd_one_eq_one";
   1.477 -
   1.478 -Goal "~ finite prime";
   1.479 -by (rtac (hypnat_infinite_has_nonstandard_iff RS iffD2) 1);
   1.480 -by (cut_facts_tac [hypnat_dvd_all_hypnat_of_nat] 1);
   1.481 -by (etac exE 1);
   1.482 -by (etac conjE 1);
   1.483 -by (subgoal_tac "1 < N + 1" 1);
   1.484 -by (blast_tac (claset() addIs [hypnat_add_one_gt_one]) 2);
   1.485 -by (dtac hyperprime_factor_exists 1);
   1.486 -by (auto_tac (claset() addIs [NatStar_mem],simpset()));
   1.487 -by (subgoal_tac "k ~: hypnat_of_nat ` prime" 1);
   1.488 -by (force_tac (claset(),simpset() addsimps [starprime_def]) 1);
   1.489 -by (Step_tac 1);
   1.490 -by (dres_inst_tac [("x","x")] bspec 1);
   1.491 -by (rtac ccontr 1 THEN Asm_full_simp_tac 1);
   1.492 -by (dtac hdvd_diff 1 THEN assume_tac 1);
   1.493 -by (auto_tac (claset() addDs [hdvd_one_eq_one],simpset()));
   1.494 -qed "not_finite_prime";
     2.1 --- a/src/HOL/Complex/ex/NSPrimes.thy	Fri Jul 30 10:44:42 2004 +0200
     2.2 +++ b/src/HOL/Complex/ex/NSPrimes.thy	Fri Jul 30 18:37:58 2004 +0200
     2.3 @@ -1,36 +1,447 @@
     2.4  (*  Title       : NSPrimes.thy
     2.5      Author      : Jacques D. Fleuriot
     2.6      Copyright   : 2002 University of Edinburgh
     2.7 -    Description : The nonstandard primes as an extension of 
     2.8 -                  the prime numbers
     2.9 -
    2.10 -These can be used to derive an alternative proof of the infinitude of primes by
    2.11 -considering a property of nonstandard sets.
    2.12 +    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
    2.13  *)
    2.14  
    2.15 -NSPrimes = Factorization + Complex_Main +
    2.16 +header{*The Nonstandard Primes as an Extension of the Prime Numbers*}
    2.17 +
    2.18 +theory NSPrimes = "~~/src/HOL/NumberTheory/Factorization" + Complex_Main:
    2.19  
    2.20 -consts
    2.21 -  hdvd  :: [hypnat, hypnat] => bool       (infixl 50) 
    2.22 -  
    2.23 -defs
    2.24 -  hdvd_def "(M::hypnat) hdvd N ==
    2.25 -	           EX X Y. X: Rep_hypnat(M) & Y: Rep_hypnat(N) & 
    2.26 +text{*These can be used to derive an alternative proof of the infinitude of
    2.27 +primes by considering a property of nonstandard sets.*}
    2.28 +
    2.29 +
    2.30 +constdefs
    2.31 +  hdvd  :: "[hypnat, hypnat] => bool"       (infixl "hdvd" 50)
    2.32 +   "(M::hypnat) hdvd N ==
    2.33 +	           \<exists>X Y. X: Rep_hypnat(M) & Y: Rep_hypnat(N) &
    2.34                                 {n::nat. X n dvd Y n} : FreeUltrafilterNat"
    2.35  
    2.36  constdefs
    2.37 -  starprime :: hypnat set
    2.38 +  starprime :: "hypnat set"
    2.39    "starprime == ( *sNat* prime)"
    2.40  
    2.41  constdefs
    2.42 -  choicefun :: 'a set => 'a
    2.43 -  "choicefun E == (@x. EX X: Pow(E) -{{}}. x : X)" 
    2.44 +  choicefun :: "'a set => 'a"
    2.45 +  "choicefun E == (@x. \<exists>X \<in> Pow(E) -{{}}. x : X)"
    2.46 +
    2.47 +consts injf_max :: "nat => ('a::{order} set) => 'a"
    2.48 +primrec
    2.49 +  injf_max_zero: "injf_max 0 E = choicefun E"
    2.50 +  injf_max_Suc:  "injf_max (Suc n) E = choicefun({e. e:E & injf_max n E < e})"
    2.51 +
    2.52 +
    2.53 +text{*A "choice" theorem for ultrafilters, like almost everywhere
    2.54 +quantification*}
    2.55 +
    2.56 +lemma UF_choice: "{n. \<exists>m. Q n m} : FreeUltrafilterNat
    2.57 +      ==> \<exists>f. {n. Q n (f n)} : FreeUltrafilterNat"
    2.58 +apply (rule_tac x = "%n. (@x. Q n x) " in exI)
    2.59 +apply (ultra, rule someI, auto)
    2.60 +done
    2.61 +
    2.62 +lemma UF_if: "({n. P n} : FreeUltrafilterNat --> {n. Q n} : FreeUltrafilterNat) =
    2.63 +      ({n. P n --> Q n} : FreeUltrafilterNat)"
    2.64 +apply auto
    2.65 +apply ultra+
    2.66 +done
    2.67 +
    2.68 +lemma UF_conj: "({n. P n} : FreeUltrafilterNat & {n. Q n} : FreeUltrafilterNat) =
    2.69 +      ({n. P n & Q n} : FreeUltrafilterNat)"
    2.70 +apply auto
    2.71 +apply ultra+
    2.72 +done
    2.73 +
    2.74 +lemma UF_choice_ccontr: "(\<forall>f. {n. Q n (f n)} : FreeUltrafilterNat) =
    2.75 +      ({n. \<forall>m. Q n m} : FreeUltrafilterNat)"
    2.76 +apply auto
    2.77 + prefer 2 apply ultra
    2.78 +apply (rule ccontr)
    2.79 +apply (rule contrapos_np)
    2.80 + apply (erule_tac [2] asm_rl)
    2.81 +apply (simp (no_asm) add: FreeUltrafilterNat_Compl_iff1 Collect_neg_eq [symmetric])
    2.82 +apply (rule UF_choice, ultra)
    2.83 +done
    2.84 +
    2.85 +lemma dvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::nat) <= M --> m dvd N)"
    2.86 +apply (rule allI)
    2.87 +apply (induct_tac "M", auto)
    2.88 +apply (rule_tac x = "N * (Suc n) " in exI)
    2.89 +apply (safe, force)
    2.90 +apply (drule le_imp_less_or_eq, erule disjE)
    2.91 +apply (force intro!: dvd_mult2)
    2.92 +apply (force intro!: dvd_mult)
    2.93 +done
    2.94 +
    2.95 +lemmas dvd_by_all2 = dvd_by_all [THEN spec, standard]
    2.96 +
    2.97 +lemma lemma_hypnat_P_EX: "(\<exists>(x::hypnat). P x) = (\<exists>f. P (Abs_hypnat(hypnatrel `` {f})))"
    2.98 +apply auto
    2.99 +apply (rule_tac z = x in eq_Abs_hypnat, auto)
   2.100 +done
   2.101 +
   2.102 +lemma lemma_hypnat_P_ALL: "(\<forall>(x::hypnat). P x) = (\<forall>f. P (Abs_hypnat(hypnatrel `` {f})))"
   2.103 +apply auto
   2.104 +apply (rule_tac z = x in eq_Abs_hypnat, auto)
   2.105 +done
   2.106 +
   2.107 +lemma hdvd:
   2.108 +      "(Abs_hypnat(hypnatrel``{%n. X n}) hdvd
   2.109 +            Abs_hypnat(hypnatrel``{%n. Y n})) =
   2.110 +       ({n. X n dvd Y n} : FreeUltrafilterNat)"
   2.111 +apply (unfold hdvd_def)
   2.112 +apply (auto, ultra)
   2.113 +done
   2.114 +
   2.115 +lemma hypnat_of_nat_le_zero_iff: "(hypnat_of_nat n <= 0) = (n = 0)"
   2.116 +by (subst hypnat_of_nat_zero [symmetric], auto)
   2.117 +declare hypnat_of_nat_le_zero_iff [simp]
   2.118 +
   2.119 +
   2.120 +(* Goldblatt: Exercise 5.11(2) - p. 57 *)
   2.121 +lemma hdvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::hypnat) <= M --> m hdvd N)"
   2.122 +apply safe
   2.123 +apply (rule_tac z = M in eq_Abs_hypnat)
   2.124 +apply (auto simp add: lemma_hypnat_P_EX lemma_hypnat_P_ALL
   2.125 +              hypnat_zero_def hypnat_le hypnat_less hdvd)
   2.126 +apply (cut_tac dvd_by_all)
   2.127 +apply (subgoal_tac " \<forall>(n::nat) . \<exists>N. 0 < N & (\<forall>m. 0 < (m::nat) & m <= (x n) --> m dvd N)")
   2.128 + prefer 2 apply blast
   2.129 +apply (erule thin_rl)
   2.130 +apply (drule choice, safe)
   2.131 +apply (rule_tac x = f in exI, auto, ultra)
   2.132 +apply auto
   2.133 +done
   2.134 +
   2.135 +lemmas hdvd_by_all2 = hdvd_by_all [THEN spec, standard]
   2.136 +
   2.137 +(* Goldblatt: Exercise 5.11(2) - p. 57 *)
   2.138 +lemma hypnat_dvd_all_hypnat_of_nat:
   2.139 +     "\<exists>(N::hypnat). 0 < N & (\<forall>n \<in> -{0::nat}. hypnat_of_nat(n) hdvd N)"
   2.140 +apply (cut_tac hdvd_by_all)
   2.141 +apply (drule_tac x = whn in spec, auto)
   2.142 +apply (rule exI, auto)
   2.143 +apply (drule_tac x = "hypnat_of_nat n" in spec)
   2.144 +apply (auto simp add: linorder_not_less hypnat_of_nat_zero_iff)
   2.145 +done
   2.146 +
   2.147 +
   2.148 +text{*The nonstandard extension of the set prime numbers consists of precisely
   2.149 +those hypernaturals exceeding 1 that have no nontrivial factors*}
   2.150 +
   2.151 +(* Goldblatt: Exercise 5.11(3a) - p 57  *)
   2.152 +lemma starprime:
   2.153 +  "starprime = {p. 1 < p & (\<forall>m. m hdvd p --> m = 1 | m = p)}"
   2.154 +apply (unfold starprime_def prime_def)
   2.155 +apply (auto simp add: Collect_conj_eq NatStar_Int)
   2.156 +apply (rule_tac [!] z = x in eq_Abs_hypnat)
   2.157 +apply (rule_tac [2] z = m in eq_Abs_hypnat)
   2.158 +apply (auto simp add: hdvd hypnat_one_def hypnat_less lemma_hypnat_P_ALL starsetNat_def)
   2.159 +apply (drule bspec, drule_tac [2] bspec, auto)
   2.160 +apply (ultra, ultra)
   2.161 +apply (rule ccontr)
   2.162 +apply (drule FreeUltrafilterNat_Compl_mem)
   2.163 +apply (auto simp add: Collect_neg_eq [symmetric])
   2.164 +apply (drule UF_choice, auto)
   2.165 +apply (drule_tac x = f in spec, auto, ultra+)
   2.166 +done
   2.167 +
   2.168 +lemma prime_two:  "2 : prime"
   2.169 +apply (unfold prime_def, auto)
   2.170 +apply (frule dvd_imp_le)
   2.171 +apply (auto dest: dvd_0_left)
   2.172 +(*????arith raises exception Match!!??*)
   2.173 +apply (case_tac m, simp, arith)
   2.174 +done
   2.175 +declare prime_two [simp]
   2.176 +
   2.177 +(* proof uses course-of-value induction *)
   2.178 +lemma prime_factor_exists [rule_format]: "Suc 0 < n --> (\<exists>k \<in> prime. k dvd n)"
   2.179 +apply (rule_tac n = n in nat_less_induct, auto)
   2.180 +apply (case_tac "n \<in> prime")
   2.181 +apply (rule_tac x = n in bexI, auto)
   2.182 +apply (drule conjI [THEN not_prime_ex_mk], auto)
   2.183 +apply (drule_tac x = m in spec, auto)
   2.184 +apply (rule_tac x = ka in bexI)
   2.185 +apply (auto intro: dvd_mult2)
   2.186 +done
   2.187 +
   2.188 +(* Goldblatt Exercise 5.11(3b) - p 57  *)
   2.189 +lemma hyperprime_factor_exists [rule_format]: "1 < n ==> (\<exists>k \<in> starprime. k hdvd n)"
   2.190 +apply (rule_tac z = n in eq_Abs_hypnat)
   2.191 +apply (auto simp add: hypnat_one_def hypnat_less starprime_def
   2.192 +    lemma_hypnat_P_EX lemma_hypnat_P_ALL hdvd starsetNat_def Ball_def UF_if)
   2.193 +apply (rule_tac x = "%n. @y. y \<in> prime & y dvd x n" in exI, auto, ultra)
   2.194 +apply (drule sym, simp (no_asm_simp))
   2.195 + prefer 2 apply ultra
   2.196 +apply (rule_tac [!] someI2_ex)
   2.197 +apply (auto dest!: prime_factor_exists)
   2.198 +done
   2.199 +
   2.200 +(* behaves as expected! *)
   2.201 +lemma NatStar_insert: "( *sNat* insert x A) = insert (hypnat_of_nat x) ( *sNat* A)"
   2.202 +apply (auto simp add: starsetNat_def hypnat_of_nat_eq)
   2.203 +apply (rule_tac [!] z = xa in eq_Abs_hypnat, auto)
   2.204 +apply (drule_tac [!] bspec asm_rl, auto, ultra+)
   2.205 +done
   2.206 +
   2.207 +(* Goldblatt Exercise 3.10(1) - p. 29 *)
   2.208 +lemma NatStar_hypnat_of_nat: "finite A ==> *sNat* A = hypnat_of_nat ` A"
   2.209 +apply (rule_tac P = "%x. *sNat* x = hypnat_of_nat ` x" in finite_induct)
   2.210 +apply (auto simp add: NatStar_insert)
   2.211 +done
   2.212 +
   2.213 +(* proved elsewhere? *)
   2.214 +lemma FreeUltrafilterNat_singleton_not_mem: "{x} \<notin> FreeUltrafilterNat"
   2.215 +by (auto intro!: FreeUltrafilterNat_finite)
   2.216 +declare FreeUltrafilterNat_singleton_not_mem [simp]
   2.217 +
   2.218 +
   2.219 +subsection{*Another characterization of infinite set of natural numbers*}
   2.220 +
   2.221 +lemma finite_nat_set_bounded: "finite N ==> \<exists>n. (\<forall>i \<in> N. i<(n::nat))"
   2.222 +apply (erule_tac F = N in finite_induct, auto)
   2.223 +apply (rule_tac x = "Suc n + x" in exI, auto)
   2.224 +done
   2.225 +
   2.226 +lemma finite_nat_set_bounded_iff: "finite N = (\<exists>n. (\<forall>i \<in> N. i<(n::nat)))"
   2.227 +by (blast intro: finite_nat_set_bounded bounded_nat_set_is_finite)
   2.228 +
   2.229 +lemma not_finite_nat_set_iff: "(~ finite N) = (\<forall>n. \<exists>i \<in> N. n <= (i::nat))"
   2.230 +by (auto simp add: finite_nat_set_bounded_iff le_def)
   2.231 +
   2.232 +lemma bounded_nat_set_is_finite2: "(\<forall>i \<in> N. i<=(n::nat)) ==> finite N"
   2.233 +apply (rule finite_subset)
   2.234 + apply (rule_tac [2] finite_atMost, auto)
   2.235 +done
   2.236 +
   2.237 +lemma finite_nat_set_bounded2: "finite N ==> \<exists>n. (\<forall>i \<in> N. i<=(n::nat))"
   2.238 +apply (erule_tac F = N in finite_induct, auto)
   2.239 +apply (rule_tac x = "n + x" in exI, auto)
   2.240 +done
   2.241 +
   2.242 +lemma finite_nat_set_bounded_iff2: "finite N = (\<exists>n. (\<forall>i \<in> N. i<=(n::nat)))"
   2.243 +by (blast intro: finite_nat_set_bounded2 bounded_nat_set_is_finite2)
   2.244 +
   2.245 +lemma not_finite_nat_set_iff2: "(~ finite N) = (\<forall>n. \<exists>i \<in> N. n < (i::nat))"
   2.246 +by (auto simp add: finite_nat_set_bounded_iff2 le_def)
   2.247 +
   2.248 +
   2.249 +subsection{*An injective function cannot define an embedded natural number*}
   2.250  
   2.251 -consts injf_max :: "nat => ('a::{order} set) => 'a"  
   2.252 -primrec
   2.253 -  injf_max_zero "injf_max 0 E = choicefun E"
   2.254 -  injf_max_Suc  "injf_max (Suc n) E = choicefun({e. e : E & injf_max n E < e})"
   2.255 +lemma lemma_infinite_set_singleton: "\<forall>m n. m \<noteq> n --> f n \<noteq> f m
   2.256 +      ==>  {n. f n = N} = {} |  (\<exists>m. {n. f n = N} = {m})"
   2.257 +apply auto
   2.258 +apply (drule_tac x = x in spec, auto)
   2.259 +apply (subgoal_tac "\<forall>n. (f n = f x) = (x = n) ")
   2.260 +apply auto
   2.261 +done
   2.262 +
   2.263 +lemma inj_fun_not_hypnat_in_SHNat: "inj f ==> Abs_hypnat(hypnatrel `` {f}) \<notin> Nats"
   2.264 +apply (auto simp add: SHNat_eq hypnat_of_nat_eq)
   2.265 +apply (subgoal_tac "\<forall>m n. m \<noteq> n --> f n \<noteq> f m", auto)
   2.266 +apply (drule_tac [2] injD)
   2.267 +prefer 2 apply assumption
   2.268 +apply (drule_tac N = N in lemma_infinite_set_singleton, auto)
   2.269 +done
   2.270 +
   2.271 +lemma range_subset_mem_starsetNat:
   2.272 +   "range f <= A ==> Abs_hypnat(hypnatrel `` {f}) \<in> *sNat* A"
   2.273 +apply (unfold starsetNat_def, auto, ultra)
   2.274 +apply (drule_tac c = "f x" in subsetD)
   2.275 +apply (rule rangeI, auto)
   2.276 +done
   2.277 +
   2.278 +(*--------------------------------------------------------------------------------*)
   2.279 +(* Gleason Proposition 11-5.5. pg 149, pg 155 (ex. 3) and pg. 360                 *)
   2.280 +(* Let E be a nonvoid ordered set with no maximal elements (note: effectively an  *)
   2.281 +(* infinite set if we take E = N (Nats)). Then there exists an order-preserving   *)
   2.282 +(* injection from N to E. Of course, (as some doofus will undoubtedly point out!  *)
   2.283 +(* :-)) can use notion of least element in proof (i.e. no need for choice) if     *)
   2.284 +(* dealing with nats as we have well-ordering property                            *)
   2.285 +(*--------------------------------------------------------------------------------*)
   2.286 +
   2.287 +lemma lemmaPow3: "E \<noteq> {} ==> \<exists>x. \<exists>X \<in> (Pow E - {{}}). x: X"
   2.288 +by auto
   2.289 +
   2.290 +lemma choicefun_mem_set: "E \<noteq> {} ==> choicefun E \<in> E"
   2.291 +apply (unfold choicefun_def)
   2.292 +apply (rule lemmaPow3 [THEN someI2_ex], auto)
   2.293 +done
   2.294 +declare choicefun_mem_set [simp]
   2.295 +
   2.296 +lemma injf_max_mem_set: "[| E \<noteq>{}; \<forall>x. \<exists>y \<in> E. x < y |] ==> injf_max n E \<in> E"
   2.297 +apply (induct_tac "n", force)
   2.298 +apply (simp (no_asm) add: choicefun_def)
   2.299 +apply (rule lemmaPow3 [THEN someI2_ex], auto)
   2.300 +done
   2.301 +
   2.302 +lemma injf_max_order_preserving: "\<forall>x. \<exists>y \<in> E. x < y ==> injf_max n E < injf_max (Suc n) E"
   2.303 +apply (simp (no_asm) add: choicefun_def)
   2.304 +apply (rule lemmaPow3 [THEN someI2_ex], auto)
   2.305 +done
   2.306 +
   2.307 +lemma injf_max_order_preserving2: "\<forall>x. \<exists>y \<in> E. x < y
   2.308 +      ==> \<forall>n m. m < n --> injf_max m E < injf_max n E"
   2.309 +apply (rule allI)
   2.310 +apply (induct_tac "n", auto)
   2.311 +apply (simp (no_asm) add: choicefun_def)
   2.312 +apply (rule lemmaPow3 [THEN someI2_ex])
   2.313 +apply (auto simp add: less_Suc_eq)
   2.314 +apply (drule_tac x = m in spec)
   2.315 +apply (drule subsetD, auto)
   2.316 +apply (drule_tac x = "injf_max m E" in order_less_trans, auto)
   2.317 +done
   2.318 +
   2.319 +lemma inj_injf_max: "\<forall>x. \<exists>y \<in> E. x < y ==> inj (%n. injf_max n E)"
   2.320 +apply (rule inj_onI)
   2.321 +apply (rule ccontr, auto)
   2.322 +apply (drule injf_max_order_preserving2)
   2.323 +apply (cut_tac m = x and n = y in less_linear, auto)
   2.324 +apply (auto dest!: spec)
   2.325 +done
   2.326 +
   2.327 +lemma infinite_set_has_order_preserving_inj:
   2.328 +     "[| (E::('a::{order} set)) \<noteq> {}; \<forall>x. \<exists>y \<in> E. x < y |]
   2.329 +      ==> \<exists>f. range f <= E & inj (f::nat => 'a) & (\<forall>m. f m < f(Suc m))"
   2.330 +apply (rule_tac x = "%n. injf_max n E" in exI, safe)
   2.331 +apply (rule injf_max_mem_set)
   2.332 +apply (rule_tac [3] inj_injf_max)
   2.333 +apply (rule_tac [4] injf_max_order_preserving, auto)
   2.334 +done
   2.335 +
   2.336 +text{*Only need the existence of an injective function from N to A for proof*}
   2.337 +
   2.338 +lemma hypnat_infinite_has_nonstandard:
   2.339 +     "~ finite A ==> hypnat_of_nat ` A < ( *sNat* A)"
   2.340 +apply auto
   2.341 +apply (rule subsetD)
   2.342 +apply (rule NatStar_hypreal_of_real_image_subset, auto)
   2.343 +apply (subgoal_tac "A \<noteq> {}")
   2.344 +prefer 2 apply force
   2.345 +apply (drule infinite_set_has_order_preserving_inj)
   2.346 +apply (erule not_finite_nat_set_iff2 [THEN iffD1], auto)
   2.347 +apply (drule inj_fun_not_hypnat_in_SHNat)
   2.348 +apply (drule range_subset_mem_starsetNat)
   2.349 +apply (auto simp add: SHNat_eq)
   2.350 +done
   2.351 +
   2.352 +lemma starsetNat_eq_hypnat_of_nat_image_finite: "*sNat* A =  hypnat_of_nat ` A ==> finite A"
   2.353 +apply (rule ccontr)
   2.354 +apply (auto dest: hypnat_infinite_has_nonstandard)
   2.355 +done
   2.356 +
   2.357 +lemma finite_starsetNat_iff: "( *sNat* A = hypnat_of_nat ` A) = (finite A)"
   2.358 +by (blast intro!: starsetNat_eq_hypnat_of_nat_image_finite NatStar_hypnat_of_nat)
   2.359 +
   2.360 +lemma hypnat_infinite_has_nonstandard_iff: "(~ finite A) = (hypnat_of_nat ` A < *sNat* A)"
   2.361 +apply (rule iffI)
   2.362 +apply (blast intro!: hypnat_infinite_has_nonstandard)
   2.363 +apply (auto simp add: finite_starsetNat_iff [symmetric])
   2.364 +done
   2.365 +
   2.366 +subsection{*Existence of Infinitely Many Primes: a Nonstandard Proof*}
   2.367 +
   2.368 +lemma lemma_not_dvd_hypnat_one: "~ (\<forall>n \<in> - {0}. hypnat_of_nat n hdvd 1)"
   2.369 +apply auto
   2.370 +apply (rule_tac x = 2 in bexI)
   2.371 +apply (auto simp add: hypnat_of_nat_eq hypnat_one_def hdvd dvd_def)
   2.372 +done
   2.373 +declare lemma_not_dvd_hypnat_one [simp]
   2.374 +
   2.375 +lemma lemma_not_dvd_hypnat_one2: "\<exists>n \<in> - {0}. ~ hypnat_of_nat n hdvd 1"
   2.376 +apply (cut_tac lemma_not_dvd_hypnat_one)
   2.377 +apply (auto simp del: lemma_not_dvd_hypnat_one)
   2.378 +done
   2.379 +declare lemma_not_dvd_hypnat_one2 [simp]
   2.380 +
   2.381 +(* not needed here *)
   2.382 +lemma hypnat_gt_zero_gt_one:
   2.383 +  "[| 0 < (N::hypnat); N \<noteq> 1 |] ==> 1 < N"
   2.384 +apply (unfold hypnat_zero_def hypnat_one_def)
   2.385 +apply (rule_tac z = N in eq_Abs_hypnat)
   2.386 +apply (auto simp add: hypnat_less, ultra)
   2.387 +done
   2.388 +
   2.389 +lemma hypnat_add_one_gt_one:
   2.390 +    "0 < N ==> 1 < (N::hypnat) + 1"
   2.391 +apply (unfold hypnat_zero_def hypnat_one_def)
   2.392 +apply (rule_tac z = N in eq_Abs_hypnat)
   2.393 +apply (auto simp add: hypnat_less hypnat_add)
   2.394 +done
   2.395 +
   2.396 +lemma zero_not_prime: "0 \<notin> prime"
   2.397 +apply safe
   2.398 +apply (drule prime_g_zero, auto)
   2.399 +done
   2.400 +declare zero_not_prime [simp]
   2.401 +
   2.402 +lemma hypnat_of_nat_zero_not_prime: "hypnat_of_nat 0 \<notin> starprime"
   2.403 +by (auto intro!: bexI simp add: starprime_def starsetNat_def hypnat_of_nat_eq)
   2.404 +declare hypnat_of_nat_zero_not_prime [simp]
   2.405 +
   2.406 +lemma hypnat_zero_not_prime:
   2.407 +   "0 \<notin> starprime"
   2.408 +apply (unfold starprime_def starsetNat_def hypnat_zero_def)
   2.409 +apply (auto intro!: bexI)
   2.410 +done
   2.411 +declare hypnat_zero_not_prime [simp]
   2.412 +
   2.413 +lemma one_not_prime: "1 \<notin> prime"
   2.414 +apply safe
   2.415 +apply (drule prime_g_one, auto)
   2.416 +done
   2.417 +declare one_not_prime [simp]
   2.418 +
   2.419 +lemma one_not_prime2: "Suc 0 \<notin> prime"
   2.420 +apply safe
   2.421 +apply (drule prime_g_one, auto)
   2.422 +done
   2.423 +declare one_not_prime2 [simp]
   2.424 +
   2.425 +lemma hypnat_of_nat_one_not_prime: "hypnat_of_nat 1 \<notin> starprime"
   2.426 +by (auto intro!: bexI simp add: starprime_def starsetNat_def hypnat_of_nat_eq)
   2.427 +declare hypnat_of_nat_one_not_prime [simp]
   2.428 +
   2.429 +lemma hypnat_one_not_prime: "1 \<notin> starprime"
   2.430 +apply (unfold starprime_def starsetNat_def hypnat_one_def)
   2.431 +apply (auto intro!: bexI)
   2.432 +done
   2.433 +declare hypnat_one_not_prime [simp]
   2.434 +
   2.435 +lemma hdvd_diff: "[| k hdvd m; k hdvd n |] ==> k hdvd (m - n)"
   2.436 +apply (rule_tac z = k in eq_Abs_hypnat)
   2.437 +apply (rule_tac z = m in eq_Abs_hypnat)
   2.438 +apply (rule_tac z = n in eq_Abs_hypnat)
   2.439 +apply (auto simp add: hdvd hypnat_minus, ultra)
   2.440 +apply (blast intro: dvd_diff)
   2.441 +done
   2.442 +
   2.443 +lemma dvd_one_eq_one: "x dvd (1::nat) ==> x = 1"
   2.444 +by (unfold dvd_def, auto)
   2.445 +
   2.446 +lemma hdvd_one_eq_one: "x hdvd 1 ==> x = 1"
   2.447 +apply (unfold hypnat_one_def)
   2.448 +apply (rule_tac z = x in eq_Abs_hypnat)
   2.449 +apply (auto simp add: hdvd)
   2.450 +done
   2.451 +
   2.452 +theorem not_finite_prime: "~ finite prime"
   2.453 +apply (rule hypnat_infinite_has_nonstandard_iff [THEN iffD2])
   2.454 +apply (cut_tac hypnat_dvd_all_hypnat_of_nat)
   2.455 +apply (erule exE)
   2.456 +apply (erule conjE)
   2.457 +apply (subgoal_tac "1 < N + 1")
   2.458 +prefer 2 apply (blast intro: hypnat_add_one_gt_one)
   2.459 +apply (drule hyperprime_factor_exists)
   2.460 +apply (auto intro: NatStar_mem)
   2.461 +apply (subgoal_tac "k \<notin> hypnat_of_nat ` prime")
   2.462 +apply (force simp add: starprime_def, safe)
   2.463 +apply (drule_tac x = x in bspec)
   2.464 +apply (rule ccontr, simp)
   2.465 +apply (drule hdvd_diff, assumption)
   2.466 +apply (auto dest: hdvd_one_eq_one)
   2.467 +done
   2.468  
   2.469  end
   2.470 -
   2.471 -
     3.1 --- a/src/HOL/Hyperreal/Integration.ML	Fri Jul 30 10:44:42 2004 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,1087 +0,0 @@
     3.4 -(*  Title       : Integration.ML
     3.5 -    Author      : Jacques D. Fleuriot
     3.6 -    Copyright   : 2000  University of Edinburgh
     3.7 -    Description : Theory of integration (c.f. Harison's HOL development)
     3.8 -*)
     3.9 -
    3.10 -val mult_2 = thm"mult_2";
    3.11 -val mult_2_right = thm"mult_2_right";
    3.12 -
    3.13 -fun ARITH_PROVE str = prove_goal thy str
    3.14 -                      (fn prems => [cut_facts_tac prems 1,arith_tac 1]);
    3.15 -
    3.16 -fun CLAIM_SIMP str thms =
    3.17 -               prove_goal (the_context()) str
    3.18 -               (fn prems => [cut_facts_tac prems 1,
    3.19 -                   auto_tac (claset(),simpset() addsimps thms)]);
    3.20 -
    3.21 -fun CLAIM str = CLAIM_SIMP str [];
    3.22 -
    3.23 -Goalw [psize_def] "a = b ==> psize (%n. if n = 0 then a else b) = 0";
    3.24 -by Auto_tac;
    3.25 -qed "partition_zero";
    3.26 -Addsimps [partition_zero];
    3.27 -
    3.28 -Goalw [psize_def] "a < b ==> psize (%n. if n = 0 then a else b) = 1";
    3.29 -by Auto_tac;
    3.30 -by (rtac some_equality 1);
    3.31 -by Auto_tac;
    3.32 -by (dres_inst_tac [("x","1")] spec 1);
    3.33 -by Auto_tac;
    3.34 -qed "partition_one";
    3.35 -Addsimps [partition_one];
    3.36 -
    3.37 -Goalw [partition_def] 
    3.38 -   "a <= b ==> partition(a,b)(%n. if n = 0 then a else b)";
    3.39 -by (auto_tac (claset(),simpset() addsimps [order_le_less]));
    3.40 -qed "partition_single";
    3.41 -Addsimps [partition_single];
    3.42 -
    3.43 -Goalw [partition_def] "partition(a,b) D ==> (D(0) = a)";
    3.44 -by Auto_tac;
    3.45 -qed "partition_lhs";
    3.46 -
    3.47 -Goalw [partition_def]
    3.48 -       "(partition(a,b) D) = \
    3.49 -\       ((D 0 = a) & \
    3.50 -\        (ALL n. n < (psize D) --> D n < D(Suc n)) & \
    3.51 -\        (ALL n. (psize D) <= n --> (D n = b)))";
    3.52 -by Auto_tac;
    3.53 -by (ALLGOALS(subgoal_tac "psize D = N"));
    3.54 -by Auto_tac;
    3.55 -by (ALLGOALS(simp_tac (simpset() addsimps [psize_def])));
    3.56 -by (ALLGOALS(rtac some_equality));
    3.57 -by (Blast_tac 1 THEN Blast_tac 2);
    3.58 -by (ALLGOALS(rtac ccontr));
    3.59 -by (ALLGOALS(dtac (ARITH_PROVE "n ~= (N::nat) ==> n < N | N < n")));
    3.60 -by (Step_tac 1);
    3.61 -by (dres_inst_tac [("x","Na")] spec 1);
    3.62 -by (rotate_tac 3 1);
    3.63 -by (dres_inst_tac [("x","Suc Na")] spec 1);
    3.64 -by (Asm_full_simp_tac 1);
    3.65 -by (rotate_tac 2 1);
    3.66 -by (dres_inst_tac [("x","N")] spec 1);
    3.67 -by (Asm_full_simp_tac 1);
    3.68 -by (dres_inst_tac [("x","Na")] spec 1);
    3.69 -by (rotate_tac 3 1);
    3.70 -by (dres_inst_tac [("x","Suc Na")] spec 1);
    3.71 -by (Asm_full_simp_tac 1);
    3.72 -by (rotate_tac 2 1);
    3.73 -by (dres_inst_tac [("x","N")] spec 1);
    3.74 -by (Asm_full_simp_tac 1);
    3.75 -qed "partition";
    3.76 -
    3.77 -Goal "partition(a,b) D ==> (D(psize D) = b)";
    3.78 -by (dtac (partition RS subst) 1);
    3.79 -by (Step_tac 1);
    3.80 -by (REPEAT(dres_inst_tac [("x","psize D")] spec 1));
    3.81 -by Auto_tac;
    3.82 -qed "partition_rhs";
    3.83 -
    3.84 -Goal "[|partition(a,b) D; psize D <= n |] ==> (D n = b)";
    3.85 -by (dtac (partition RS subst) 1);
    3.86 -by (Blast_tac 1);
    3.87 -qed "partition_rhs2";
    3.88 -
    3.89 -Goal 
    3.90 - "partition(a,b) D & m + Suc d <= n & n <= (psize D) --> D(m) < D(m + Suc d)";
    3.91 -by (induct_tac "d" 1);
    3.92 -by Auto_tac;
    3.93 -by (ALLGOALS(dtac (partition RS subst)));
    3.94 -by (Step_tac 1);
    3.95 -by (ALLGOALS(dtac (ARITH_PROVE "Suc m <= n ==> m < n")));
    3.96 -by (ALLGOALS(dtac less_le_trans));
    3.97 -by (assume_tac 1 THEN assume_tac 2);
    3.98 -by (ALLGOALS(blast_tac (claset() addIs [order_less_trans])));
    3.99 -qed_spec_mp "lemma_partition_lt_gen";
   3.100 -
   3.101 -Goal "m < n ==> EX d. n = m + Suc d";
   3.102 -by (auto_tac (claset(),simpset() addsimps [less_iff_Suc_add]));
   3.103 -qed "less_eq_add_Suc";
   3.104 -
   3.105 -Goal "[|partition(a,b) D; m < n; n <= (psize D)|] ==> D(m) < D(n)";
   3.106 -by (auto_tac (claset() addDs [less_eq_add_Suc] addIs [lemma_partition_lt_gen],
   3.107 -    simpset()));
   3.108 -qed "partition_lt_gen";
   3.109 -
   3.110 -Goal "partition(a,b) D ==> (n < (psize D) --> D(0) < D(Suc n))";
   3.111 -by (dtac (partition RS subst) 1);
   3.112 -by (induct_tac "n" 1);
   3.113 -by (Blast_tac 1);
   3.114 -by (blast_tac (claset() addSDs [leI] addDs 
   3.115 -    [(ARITH_PROVE "m <= n ==> m <= Suc n"),
   3.116 -    le_less_trans,order_less_trans]) 1);
   3.117 -qed_spec_mp "partition_lt";
   3.118 -
   3.119 -Goal "partition(a,b) D ==> a <= b";
   3.120 -by (ftac (partition RS subst) 1);
   3.121 -by (Step_tac 1);
   3.122 -by (rotate_tac 2 1);
   3.123 -by (dres_inst_tac [("x","psize D")] spec 1);
   3.124 -by (Step_tac 1);
   3.125 -by (rtac ccontr 1);
   3.126 -by (case_tac "psize D = 0" 1);
   3.127 -by (Step_tac 1);
   3.128 -by (dres_inst_tac [("n","psize D - 1")] partition_lt 2);
   3.129 -by Auto_tac;
   3.130 -qed "partition_le";
   3.131 -
   3.132 -Goal "[|partition(a,b) D; n < (psize D)|] ==> D(n) < D(psize D)";
   3.133 -by (auto_tac (claset() addIs [partition_lt_gen],simpset()));
   3.134 -qed "partition_gt";
   3.135 -
   3.136 -Goal "partition(a,b) D ==> ((a = b) = (psize D = 0))";
   3.137 -by (ftac (partition RS subst) 1);
   3.138 -by (Step_tac 1);
   3.139 -by (rotate_tac 2 1);
   3.140 -by (dres_inst_tac [("x","psize D")] spec 1);
   3.141 -by (rtac ccontr 1);
   3.142 -by (dres_inst_tac [("n","psize D - 1")] partition_lt 1);
   3.143 -by (Blast_tac 3 THEN Auto_tac);
   3.144 -qed "partition_eq";
   3.145 -
   3.146 -Goal "partition(a,b) D ==> a <= D(r)";
   3.147 -by (ftac (partition RS subst) 1);
   3.148 -by (Step_tac 1);
   3.149 -by (induct_tac "r" 1);
   3.150 -by (cut_inst_tac [("m","Suc n"),("n","psize D")] 
   3.151 -    (ARITH_PROVE "m < n | n <= (m::nat)") 2);
   3.152 -by (Step_tac 1);
   3.153 -by (eres_inst_tac [("j","D n")] real_le_trans 1);
   3.154 -by (dres_inst_tac [("x","n")] spec 1);
   3.155 -by (blast_tac (claset() addIs [less_trans,order_less_imp_le]) 1);
   3.156 -by (res_inst_tac [("j","b")] real_le_trans 1);
   3.157 -by (etac partition_le 1);
   3.158 -by (Blast_tac 1);
   3.159 -qed "partition_lb";
   3.160 -
   3.161 -Goal "[| partition(a,b) D; psize D ~= 0 |] ==> a < D(Suc n)";
   3.162 -by (res_inst_tac [("t","a")] (partition_lhs RS subst) 1);
   3.163 -by (assume_tac 1);
   3.164 -by (cut_inst_tac [("m","psize D"),("n","Suc n")] 
   3.165 -    (ARITH_PROVE "m < n | n <= (m::nat)") 1);
   3.166 -by (ftac (partition RS subst) 1);
   3.167 -by (Step_tac 1);
   3.168 -by (rotate_tac 3 1);
   3.169 -by (dres_inst_tac [("x","Suc n")] spec 1);
   3.170 -by (etac impE 1);
   3.171 -by (etac less_imp_le 1);
   3.172 -by (ftac partition_rhs 1);
   3.173 -by (dtac partition_gt 1 THEN assume_tac 1);
   3.174 -by (Asm_simp_tac 1);
   3.175 -by (blast_tac (claset() addIs [partition_lt,less_le_trans]) 1);
   3.176 -qed "partition_lb_lt";
   3.177 -
   3.178 -Goal "partition(a,b) D ==> D(r) <= b";
   3.179 -by (ftac (partition RS subst) 1);
   3.180 -by (cut_inst_tac [("m","r"),("n","psize D")] 
   3.181 -    (ARITH_PROVE "m < n | n <= (m::nat)") 1);
   3.182 -by (Step_tac 1);
   3.183 -by (Blast_tac 2);
   3.184 -by (subgoal_tac "ALL x. D((psize D) - x) <= b" 1);
   3.185 -by (rotate_tac 4 1);
   3.186 -by (dres_inst_tac [("x","psize D - r")] spec 1);
   3.187 -by (dtac (ARITH_PROVE "p < m ==> m - (m - p) = (p::nat)") 1);
   3.188 -by (thin_tac "ALL n. psize D <= n --> D n = b" 1);
   3.189 -by (Asm_full_simp_tac 1);
   3.190 -by (Step_tac 1);
   3.191 -by (induct_tac "x" 1);
   3.192 -by (Simp_tac 1 THEN Blast_tac 1);
   3.193 -by (case_tac "psize D - Suc n = 0" 1);
   3.194 -by (thin_tac "ALL n. psize D <= n --> D n = b" 1);
   3.195 -by (asm_simp_tac (simpset() addsimps [partition_le]) 1);
   3.196 -by (rtac real_le_trans 1 THEN assume_tac 2);
   3.197 -by (rtac (ARITH_PROVE "0 < m - Suc n ==> (m - n) = Suc(m - Suc n)" 
   3.198 -          RS ssubst) 1);
   3.199 -by (dres_inst_tac [("x","psize D - Suc n")] spec 2);
   3.200 -by (thin_tac "ALL n. psize D <= n --> D n = b" 2);
   3.201 -by (Asm_full_simp_tac 2);
   3.202 -by (arith_tac 1);
   3.203 -qed "partition_ub";
   3.204 -
   3.205 -Goal "[| partition(a,b) D; n < psize D |] ==> D(n) < b"; 
   3.206 -by (blast_tac (claset() addIs [partition_rhs RS subst] addIs
   3.207 -    [partition_gt]) 1);
   3.208 -qed "partition_ub_lt";
   3.209 -
   3.210 -Goal "[| partition (a, b) D1; partition (b, c) D2 |] \
   3.211 -\      ==> (ALL n. \
   3.212 -\            n < psize D1 + psize D2 --> \
   3.213 -\            (if n < psize D1 then D1 n else D2 (n - psize D1)) \
   3.214 -\            < (if Suc n < psize D1 then D1 (Suc n) \
   3.215 -\               else D2 (Suc n - psize D1))) & \
   3.216 -\        (ALL n. \
   3.217 -\            psize D1 + psize D2 <= n --> \
   3.218 -\            (if n < psize D1 then D1 n else D2 (n - psize D1)) = \
   3.219 -\            (if psize D1 + psize D2 < psize D1 then D1 (psize D1 + psize D2) \
   3.220 -\             else D2 (psize D1 + psize D2 - psize D1)))";
   3.221 -by (Step_tac 1);
   3.222 -by (auto_tac (claset() addIs [partition_lt_gen],simpset()));
   3.223 -by (dres_inst_tac [("m","psize D1")] 
   3.224 -    (leI RSN(2,ARITH_PROVE "[| n < m; m <= Suc n |] ==> m = Suc n")) 1);
   3.225 -by (assume_tac 1);
   3.226 -by (auto_tac (claset() addSIs [partition_lt_gen],
   3.227 -    simpset() addsimps [partition_lhs,partition_ub_lt]));
   3.228 -by (blast_tac (claset() addIs [ARITH_PROVE "~n < m ==> n - m < Suc n - m"]) 1);
   3.229 -by (auto_tac (claset(),simpset() addsimps [
   3.230 -    ARITH_PROVE "~ n < m ==> (Suc n - m <= p) = (Suc n <= m + p)"]));
   3.231 -by (dtac (ARITH_PROVE "p + q <= (n::nat) ==> q <= n - p") 1);
   3.232 -by (auto_tac (claset() addSIs [partition_rhs2], simpset() addsimps 
   3.233 -    [partition_rhs]));
   3.234 -qed "lemma_partition_append1";
   3.235 -
   3.236 -Goal "[| partition (a, b) D1; partition (b, c) D2; N < psize D1 |] \
   3.237 -\     ==> D1(N) < D2 (psize D2)";
   3.238 -by (res_inst_tac [("y","D1(psize D1)")] order_less_le_trans 1);
   3.239 -by (etac partition_gt 1 THEN assume_tac 1);
   3.240 -by (auto_tac (claset(),simpset() addsimps [partition_rhs,partition_le]));
   3.241 -qed "lemma_psize1";
   3.242 -
   3.243 -Goal "[| partition (a, b) D1; partition (b, c) D2 |] \
   3.244 -\     ==> psize (%n. if n < psize D1 then D1 n else D2 (n - psize D1)) = \
   3.245 -\         psize D1 + psize D2";
   3.246 -by (res_inst_tac 
   3.247 -    [("D2","%n. if n < psize D1 then D1 n else D2 (n - psize D1)")] 
   3.248 -    ((psize_def RS meta_eq_to_obj_eq) RS ssubst) 1);
   3.249 -by (rtac some1_equality 1);
   3.250 -by (blast_tac (claset() addSIs [lemma_partition_append1]) 2);
   3.251 -by (rtac ex1I 1 THEN rtac lemma_partition_append1 1);
   3.252 -by Auto_tac;
   3.253 -by (rtac ccontr 1);
   3.254 -by (dtac (ARITH_PROVE "m ~= n ==> m < n | n < (m::nat)") 1);
   3.255 -by (Step_tac 1);
   3.256 -by (rotate_tac 3 1);
   3.257 -by (dres_inst_tac [("x","psize D1 + psize D2")] spec 1);
   3.258 -by Auto_tac;
   3.259 -by (case_tac "N < psize D1" 1);
   3.260 -by (auto_tac (claset() addDs [lemma_psize1],simpset()));
   3.261 -by (dtac leI 1);
   3.262 -by (dtac (ARITH_PROVE "[|p <= n; n < p + m|] ==> n - p < (m::nat)") 1);
   3.263 -by (assume_tac 1);
   3.264 -by (dres_inst_tac [("a","b"),("b","c")] partition_gt 1);
   3.265 -by Auto_tac;
   3.266 -by (dres_inst_tac [("x","psize D1 + psize D2")] spec 1);
   3.267 -by (auto_tac (claset(),simpset() addsimps [partition_rhs2]));
   3.268 -qed "lemma_partition_append2";
   3.269 -
   3.270 -Goalw [tpart_def]
   3.271 -"[|psize D = 0; tpart(a,b) (D,p)|] ==> a = b";
   3.272 -by (auto_tac (claset(),simpset() addsimps [partition_eq]));
   3.273 -qed "tpart_eq_lhs_rhs";
   3.274 -
   3.275 -Goalw [tpart_def] "tpart(a,b) (D,p) ==> partition(a,b) D";
   3.276 -by Auto_tac;
   3.277 -qed "tpart_partition";
   3.278 -
   3.279 -Goal "[| tpart(a,b) (D1,p1); fine(g) (D1,p1); \
   3.280 -\        tpart(b,c) (D2,p2); fine(g) (D2,p2) |] \ 
   3.281 -\      ==> EX D p. tpart(a,c) (D,p) & fine(g) (D,p)";
   3.282 -by (res_inst_tac 
   3.283 -    [("x","%n. if n < psize D1 then D1 n else D2 (n - psize D1)")] exI 1);
   3.284 -by (res_inst_tac 
   3.285 -    [("x","%n. if n < psize D1 then p1 n else p2 (n - psize D1)")] exI 1);
   3.286 -by (cut_inst_tac [("m","psize D1")] (ARITH_PROVE "0 < (m::nat) | m = 0") 1);
   3.287 -by (auto_tac (claset() addDs [tpart_eq_lhs_rhs],simpset()));
   3.288 -by (asm_full_simp_tac (simpset() addsimps [fine_def,
   3.289 -    [tpart_partition,tpart_partition] MRS lemma_partition_append2]) 2);
   3.290 -by Auto_tac;
   3.291 -by (dres_inst_tac [("m","psize D1"),("n","n")] 
   3.292 -    (leI RSN(2,ARITH_PROVE "[| n < m; m <= Suc n |] ==> m = Suc n")) 2);
   3.293 -by Auto_tac;
   3.294 -by (dtac (tpart_partition RS partition_rhs) 2);
   3.295 -by (dtac (tpart_partition RS partition_lhs) 2);
   3.296 -by Auto_tac;
   3.297 -by (rotate_tac 3 2);
   3.298 -by (dres_inst_tac [("x","n - psize D1")] spec 2);
   3.299 -by (auto_tac (claset(),simpset() addsimps 
   3.300 -    [ARITH_PROVE "[| (0::nat) < p; p <= n |] ==> (n - p < m) = (n < p + m)",
   3.301 -     ARITH_PROVE "~n < p ==> Suc n - p = Suc(n - p)"]));
   3.302 -by (auto_tac (claset(),simpset() addsimps [tpart_def,
   3.303 -    ARITH_PROVE "~n < p ==> Suc n - p = Suc(n - p)"]));
   3.304 -by (dres_inst_tac [("m","psize D1"),("n","n")] 
   3.305 -    (leI RSN(2,ARITH_PROVE "[| n < m; m <= Suc n |] ==> m = Suc n")) 2);
   3.306 -by Auto_tac;
   3.307 -by (dtac partition_rhs 2);
   3.308 -by (dtac partition_lhs 2);
   3.309 -by Auto_tac;
   3.310 -by (rtac (partition RS ssubst) 1);
   3.311 -by (rtac (lemma_partition_append2 RS ssubst) 1);
   3.312 -by (rtac conjI 3);
   3.313 -by (dtac lemma_partition_append1 4);
   3.314 -by (auto_tac (claset(),simpset() addsimps [partition_lhs,partition_rhs]));
   3.315 -qed "partition_append";
   3.316 -
   3.317 -(* ------------------------------------------------------------------------ *)
   3.318 -(* We can always find a division which is fine wrt any gauge                *)
   3.319 -(* ------------------------------------------------------------------------ *)
   3.320 -
   3.321 -Goal "[| a <= b; gauge(%x. a <= x & x <= b) g |] \
   3.322 -\     ==> EX D p. tpart(a,b) (D,p) & fine g (D,p)";
   3.323 -by (cut_inst_tac 
   3.324 - [("P","%(u,v). a <= u & v <= b --> (EX D p. tpart(u,v) (D,p) & fine(g) (D,p))")]
   3.325 - lemma_BOLZANO2 1);
   3.326 -by (Step_tac 1);
   3.327 -by (REPEAT(blast_tac (claset() addIs [real_le_trans]) 1));
   3.328 -by (auto_tac (claset() addIs [partition_append],simpset()));
   3.329 -by (case_tac "a <= x & x <= b" 1);
   3.330 -by (res_inst_tac [("x","1")] exI 2);
   3.331 -by Auto_tac;
   3.332 -by (res_inst_tac [("x","g x")] exI 1);
   3.333 -by (auto_tac (claset(),simpset() addsimps [gauge_def]));
   3.334 -by (res_inst_tac [("x","%n. if n = 0 then aa else ba")] exI 1);
   3.335 -by (res_inst_tac [("x","%n. if n = 0 then x else ba")] exI 1);
   3.336 -by (auto_tac (claset(),simpset() addsimps [tpart_def,fine_def]));
   3.337 -qed "partition_exists";
   3.338 -
   3.339 -(* ------------------------------------------------------------------------ *)
   3.340 -(* Lemmas about combining gauges                                            *)
   3.341 -(* ------------------------------------------------------------------------ *)
   3.342 -
   3.343 -Goalw [gauge_def] 
   3.344 -     "[| gauge(E) g1; gauge(E) g2 |] \
   3.345 -\     ==> gauge(E) (%x. if g1(x) < g2(x) then g1(x) else g2(x))";
   3.346 -by Auto_tac;
   3.347 -qed "gauge_min";
   3.348 -
   3.349 -Goalw [fine_def]
   3.350 -      "fine (%x. if g1(x) < g2(x) then g1(x) else g2(x)) (D,p) \
   3.351 -\      ==> fine(g1) (D,p) & fine(g2) (D,p)";
   3.352 -by (auto_tac (claset(),simpset() addsimps [split_if]));
   3.353 -qed "fine_min";
   3.354 -
   3.355 -
   3.356 -(* ------------------------------------------------------------------------ *)
   3.357 -(* The integral is unique if it exists                                      *)
   3.358 -(* ------------------------------------------------------------------------ *)
   3.359 -
   3.360 -Goalw [Integral_def] 
   3.361 -    "[| a <= b; Integral(a,b) f k1; Integral(a,b) f k2 |] ==> k1 = k2";
   3.362 -by Auto_tac;
   3.363 -by (REPEAT(dres_inst_tac [("x","abs(k1 - k2)/2")] spec 1));
   3.364 -by (Auto_tac THEN TRYALL(arith_tac));
   3.365 -by (dtac gauge_min 1 THEN assume_tac 1);
   3.366 -by (dres_inst_tac [("g","%x. if g x < ga x then g x else ga x")] 
   3.367 -    partition_exists 1 THEN assume_tac 1);
   3.368 -by Auto_tac;
   3.369 -by (dtac fine_min 1);
   3.370 -by (REPEAT(dtac spec 1) THEN Auto_tac);
   3.371 -by (subgoal_tac 
   3.372 -    "abs((rsum(D,p) f - k2) - (rsum(D,p) f - k1)) < abs(k1 - k2)" 1);
   3.373 -by (arith_tac 1);
   3.374 -by (dtac add_strict_mono 1 THEN assume_tac 1);
   3.375 -by (auto_tac (claset(),
   3.376 -    HOL_ss addsimps [left_distrib RS sym,
   3.377 -                     mult_2_right RS sym, mult_less_cancel_right]));
   3.378 -by (ALLGOALS(arith_tac));
   3.379 -qed "Integral_unique";
   3.380 -
   3.381 -Goalw [Integral_def] "Integral(a,a) f 0";
   3.382 -by Auto_tac;
   3.383 -by (res_inst_tac [("x","%x. 1")] exI 1);
   3.384 -by (auto_tac (claset() addDs [partition_eq],simpset() addsimps [gauge_def,
   3.385 -     tpart_def,rsum_def]));
   3.386 -qed "Integral_zero"; 
   3.387 -Addsimps [Integral_zero];
   3.388 -
   3.389 -Goal "sumr 0 m (%n. D (Suc n) - D n) = D(m) - D 0";
   3.390 -by (induct_tac "m" 1);
   3.391 -by Auto_tac;
   3.392 -qed "sumr_partition_eq_diff_bounds";
   3.393 -Addsimps [sumr_partition_eq_diff_bounds];
   3.394 -
   3.395 -Goal "a <= b ==> Integral(a,b) (%x. 1) (b - a)";
   3.396 -by (dtac real_le_imp_less_or_eq 1 THEN Auto_tac);
   3.397 -by (auto_tac (claset(),simpset() addsimps [rsum_def,Integral_def]));
   3.398 -by (res_inst_tac [("x","%x. b - a")] exI 1);
   3.399 -by (auto_tac (claset(),simpset() addsimps [gauge_def,
   3.400 -    abs_interval_iff,tpart_def,partition]));
   3.401 -qed "Integral_eq_diff_bounds";
   3.402 -
   3.403 -Goal "a <= b ==> Integral(a,b) (%x. c)  (c*(b - a))";
   3.404 -by (dtac real_le_imp_less_or_eq 1 THEN Auto_tac);
   3.405 -by (auto_tac (claset(),simpset() addsimps [rsum_def,Integral_def]));
   3.406 -by (res_inst_tac [("x","%x. b - a")] exI 1);
   3.407 -by (auto_tac (claset(),simpset() addsimps 
   3.408 -    [sumr_mult RS sym,gauge_def,abs_interval_iff,
   3.409 -     right_diff_distrib RS sym,partition,tpart_def]));
   3.410 -qed "Integral_mult_const";
   3.411 -
   3.412 -Goal "[| a <= b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)";
   3.413 -by (dtac real_le_imp_less_or_eq 1);
   3.414 -by (auto_tac (claset() addDs [[real_le_refl,Integral_zero] MRS Integral_unique],
   3.415 -    simpset()));
   3.416 -by (auto_tac (claset(),simpset() addsimps [rsum_def,Integral_def,
   3.417 -    sumr_mult RS sym,real_mult_assoc]));
   3.418 -by (res_inst_tac [("a2","c")] ((abs_ge_zero RS real_le_imp_less_or_eq)
   3.419 -    RS disjE) 1);
   3.420 -by (dtac sym 2);
   3.421 -by (Asm_full_simp_tac 2 THEN Blast_tac 2);
   3.422 -by (dres_inst_tac [("x","e/abs c")] spec 1 THEN Auto_tac);
   3.423 -by (asm_full_simp_tac (simpset() addsimps [zero_less_mult_iff,
   3.424 -    real_divide_def]) 1);
   3.425 -by (rtac exI 1 THEN Auto_tac);
   3.426 -by (REPEAT(dtac spec 1) THEN Auto_tac);
   3.427 -by (res_inst_tac [("z1","inverse(abs c)")] (real_mult_less_iff1 RS iffD1) 1);
   3.428 -by (fold_tac [real_divide_def]);
   3.429 -by (auto_tac (claset(),
   3.430 -      simpset() addsimps [right_diff_distrib RS sym,
   3.431 -                     abs_mult, real_mult_assoc RS sym,
   3.432 -    ARITH_PROVE "c ~= 0 ==> abs (c::real) ~= 0",
   3.433 -    positive_imp_inverse_positive]));
   3.434 -qed "Integral_mult";
   3.435 -
   3.436 -(* ------------------------------------------------------------------------ *)
   3.437 -(* Fundamental theorem of calculus (Part I)                                 *)
   3.438 -(* ------------------------------------------------------------------------ *)
   3.439 -
   3.440 -(* "Straddle Lemma" : Swartz & Thompson: AMM 95(7) 1988 *)
   3.441 -
   3.442 -Goal "ALL x. P(x) --> (EX y. Q x y) ==> EX f. (ALL x. P(x) --> Q x (f x))";
   3.443 -by (cut_inst_tac [("S","Collect (%x. P x)"),("Q","Q")] (CLAIM_SIMP 
   3.444 -    "(ALL x:S. (EX y. Q x y)) --> (EX f. (ALL x:S. Q x (f x)))" [bchoice]) 1);
   3.445 -by Auto_tac;
   3.446 -qed "choiceP";
   3.447 -
   3.448 -Goal "ALL x. P(x) --> (EX y. R(y) & (EX z. Q x y z)) ==> \
   3.449 -\     EX f fa. (ALL x. P(x) --> R(f x) & Q x (f x) (fa x))";
   3.450 -by (dtac (CLAIM "(ALL x. P(x) --> (EX y. R(y) & (EX z. Q x y z))) = \
   3.451 -\                (ALL x. P(x) --> (EX y z. R(y) & Q x y z))" RS iffD1) 1);;
   3.452 -by (dtac choiceP 1 THEN Step_tac 1);
   3.453 -by (dtac choiceP 1 THEN Auto_tac);
   3.454 -qed "choiceP2";
   3.455 -
   3.456 -Goal "ALL x. (EX y. R(y) & (EX z. Q x y z)) ==> \
   3.457 -\     EX f fa. (ALL x. R(f x) & Q x (f x) (fa x))";
   3.458 -by (dtac (CLAIM "(ALL x. (EX y. R(y) & (EX z. Q x y z))) = \
   3.459 -\                (ALL x. (EX y z. R(y) & Q x y z))" RS iffD1) 1);;
   3.460 -by (dtac choice 1 THEN Step_tac 1);
   3.461 -by (dtac choice 1 THEN Auto_tac);
   3.462 -qed "choice2";
   3.463 -
   3.464 -(* new simplifications e.g. (y < x/n) = (y * n < x) are a real nuisance 
   3.465 -   they break the original proofs and make new proofs longer!                 *)
   3.466 -Goalw [gauge_def]
   3.467 -     "[| ALL x. a <= x & x <= b --> DERIV f x :> f'(x); 0 < e |]\
   3.468 -\     ==> EX g. gauge(%x. a <= x & x <= b) g & \
   3.469 -\               (ALL x u v. a <= u & u <= x & x <= v & v <= b & (v - u) < g(x) \
   3.470 -\                 --> abs((f(v) - f(u)) - (f'(x) * (v - u))) <= e * (v - u))";
   3.471 -by (subgoal_tac "ALL x. a <= x & x <= b --> \
   3.472 -\                  (EX d. 0 < d & \
   3.473 -\                     (ALL u v. u <= x & x <= v & (v - u) < d --> \
   3.474 -\                     abs((f(v) - f(u)) - (f'(x) * (v - u))) <= e * (v - u)))" 1);
   3.475 -by (dtac choiceP 1);
   3.476 -by Auto_tac;
   3.477 -by (dtac spec 1 THEN Auto_tac);
   3.478 -by (auto_tac (claset(),simpset() addsimps [DERIV_iff2,LIM_def]));
   3.479 -by (dres_inst_tac [("x","e/2")] spec 1);
   3.480 -by Auto_tac;
   3.481 -by (subgoal_tac "ALL z. abs(z - x) < s --> \
   3.482 -\        abs((f(z) - f(x)) - (f'(x) * (z - x))) <= (e / 2) * abs(z - x)" 1);
   3.483 -by Auto_tac;
   3.484 -by (case_tac "0 < abs(z - x)" 2);
   3.485 -by (dtac (ARITH_PROVE "~ 0 < abs z ==> z = (0::real)") 3);
   3.486 -by (asm_full_simp_tac (simpset() addsimps 
   3.487 -    [ARITH_PROVE "(z - x = 0) = (z = (x::real))"]) 3);
   3.488 -by (dres_inst_tac [("x","z")] spec 2);
   3.489 -by (res_inst_tac [("z1","abs(inverse(z - x))")] 
   3.490 -         (real_mult_le_cancel_iff2 RS iffD1) 2);
   3.491 -by (Asm_full_simp_tac 2);
   3.492 -by (asm_full_simp_tac (simpset() 
   3.493 -     delsimps [abs_inverse, abs_mult]
   3.494 -     addsimps [abs_mult RS sym, real_mult_assoc RS sym]) 2);
   3.495 -by (subgoal_tac "inverse (z - x) * (f z - f x - f' x * (z - x)) = \
   3.496 -\                (f z - f x)/(z - x) - f' x" 2);
   3.497 -by (asm_full_simp_tac (simpset() addsimps [abs_mult RS sym] @ mult_ac) 2);
   3.498 -by (asm_full_simp_tac (simpset() addsimps [real_diff_def]) 2);
   3.499 -by (rtac (real_mult_commute RS subst) 2);
   3.500 -by (asm_full_simp_tac (simpset() addsimps [left_distrib,
   3.501 -    real_diff_def]) 2);
   3.502 -by (dtac (CLAIM "z ~= x ==> z + -x ~= (0::real)") 2);
   3.503 -by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc,
   3.504 -    real_divide_def]) 2);
   3.505 -by (simp_tac (simpset() addsimps [left_distrib]) 2);
   3.506 -by (res_inst_tac [("x","s")] exI 1 THEN Auto_tac);
   3.507 -by (res_inst_tac [("u1","u"),("v1","v")] (ARITH_PROVE "u < v | v <= (u::real)"
   3.508 -    RS disjE) 1);
   3.509 -by (dres_inst_tac [("x","v")] real_le_imp_less_or_eq 2);
   3.510 -by Auto_tac;
   3.511 -(*29*)
   3.512 -by (res_inst_tac [("j","abs((f(v) - f(x)) - (f'(x) * (v - x))) + \
   3.513 -\                  abs((f(x) - f(u)) - (f'(x) * (x - u)))")] real_le_trans 1);
   3.514 -by (rtac (abs_triangle_ineq RSN (2,real_le_trans)) 1);
   3.515 -by (asm_full_simp_tac (simpset() addsimps [right_diff_distrib]) 1);
   3.516 -by (arith_tac 1);
   3.517 -by (res_inst_tac [("t","e*(v - u)")] (real_sum_of_halves RS subst) 1);
   3.518 -by (rtac add_mono 1);
   3.519 -by (res_inst_tac [("j","(e / 2) * abs(v - x)")] real_le_trans 1);
   3.520 -
   3.521 -by (Asm_full_simp_tac 2 THEN arith_tac 2);
   3.522 -by (ALLGOALS (thin_tac "ALL xa. \
   3.523 -\             xa ~= x & abs (xa + - x) < s --> \
   3.524 -\             abs ((f xa - f x) / (xa - x) + - f' x) * 2 < e"));
   3.525 -by (dres_inst_tac [("x","v")] spec 1 THEN Auto_tac);
   3.526 -by (arith_tac 1);
   3.527 -by (dres_inst_tac [("x","u")] spec 1 THEN Auto_tac);
   3.528 -by (arith_tac 1);
   3.529 -by (subgoal_tac "abs (f u - f x - f' x * (u - x)) = \
   3.530 -\                abs (f x - f u - f' x * (x - u))" 1);
   3.531 -by (Asm_full_simp_tac 1);
   3.532 -by (asm_full_simp_tac (simpset() addsimps [right_distrib,
   3.533 -    real_diff_def]) 2);
   3.534 -by (arith_tac 2);
   3.535 -by(rtac real_le_trans 1);
   3.536 -by Auto_tac;
   3.537 -by (arith_tac 1);
   3.538 -qed "lemma_straddle";
   3.539 -
   3.540 -Goal "((number_of c - 1) * x <= 0) =((number_of c ::real) * x <= x)";
   3.541 -by (rtac ((ARITH_PROVE "(x <= y) = (x - y <= (0::real))") RS ssubst) 1);
   3.542 -by (simp_tac (simpset() addsimps [left_diff_distrib,
   3.543 -    CLAIM_SIMP "c * x - x = (c - 1) * (x::real)" [left_diff_distrib]]) 1);
   3.544 -qed "lemma_number_of_mult_le";
   3.545 - 
   3.546 -
   3.547 -Goal "[|a <= b; ALL x. a <= x & x <= b --> DERIV f x :> f'(x) |] \
   3.548 -\     ==> Integral(a,b) f' (f(b) - f(a))";
   3.549 -by (dtac real_le_imp_less_or_eq 1 THEN Auto_tac);
   3.550 -by (auto_tac (claset(),simpset() addsimps [Integral_def]));
   3.551 -by (rtac ccontr 1);
   3.552 -by (subgoal_tac "ALL e. 0 < e --> \ 
   3.553 -\                   (EX g. gauge (%x. a <= x & x <= b) g & \
   3.554 -\                   (ALL D p. \
   3.555 -\                       tpart (a, b) (D, p) & fine g (D, p) --> \
   3.556 -\                       abs (rsum (D, p) f' - (f b - f a)) <= e))" 1);
   3.557 -by (rotate_tac 3 1);
   3.558 -by (dres_inst_tac [("x","e/2")] spec 1 THEN Auto_tac);
   3.559 -by (dtac spec 1 THEN Auto_tac);
   3.560 -by (REPEAT(dtac spec 1) THEN Auto_tac);
   3.561 -by (dres_inst_tac [("e","ea/(b - a)")] lemma_straddle 1);
   3.562 -by (auto_tac (claset(),simpset() addsimps [thm"Ring_and_Field.zero_less_divide_iff"]));
   3.563 -by (rtac exI 1);
   3.564 -by (auto_tac (claset(),simpset() addsimps [tpart_def,rsum_def]));
   3.565 -by (subgoal_tac "sumr 0 (psize D) (%n. f(D(Suc n)) - f(D n)) = \
   3.566 -\   f b - f a" 1);
   3.567 -by (cut_inst_tac [("D","%n. f(D n)"),("m","psize D")] 
   3.568 -    sumr_partition_eq_diff_bounds 2);
   3.569 -by (asm_full_simp_tac (simpset() addsimps [partition_lhs,partition_rhs]) 2);
   3.570 -by (dtac sym 1 THEN Asm_full_simp_tac 1);
   3.571 -by (simp_tac (simpset() addsimps [sumr_diff]) 1);
   3.572 -by (rtac (sumr_rabs RS real_le_trans) 1);
   3.573 -by (subgoal_tac 
   3.574 -    "ea = sumr 0 (psize D) (%n. (ea / (b - a)) * (D(Suc n) - (D n)))" 1);
   3.575 -by (asm_full_simp_tac (simpset() addsimps 
   3.576 -    [ARITH_PROVE "abs(y - (x::real)) = abs(x - y)"]) 1);
   3.577 -by (res_inst_tac [("t","ea")] ssubst 1 THEN assume_tac 1);
   3.578 -by (rtac sumr_le2 1);
   3.579 -by (rtac (sumr_mult RS subst) 2);
   3.580 -by (auto_tac (claset(),simpset() addsimps [partition_rhs,
   3.581 -    partition_lhs,partition_lb,partition_ub,fine_def]));
   3.582 -qed "FTC1";
   3.583 -
   3.584 -
   3.585 -Goal "[| Integral(a,b) f k1; k2 = k1 |] ==> Integral(a,b) f k2";
   3.586 -by (Asm_simp_tac 1);
   3.587 -qed "Integral_subst";
   3.588 -
   3.589 -Goal "[| a <= b; b <= c; Integral(a,b) f' k1; Integral(b,c) f' k2; \
   3.590 -\        ALL x. a <= x & x <= c --> DERIV f x :> f' x |] \
   3.591 -\    ==> Integral(a,c) f' (k1 + k2)";
   3.592 -by (rtac (FTC1 RS Integral_subst) 1);
   3.593 -by Auto_tac;
   3.594 -by (ftac FTC1 1 THEN Auto_tac);
   3.595 -by (forw_inst_tac [("a","b")] FTC1 1 THEN Auto_tac);
   3.596 -by (dres_inst_tac [("x","x")] spec 1 THEN Auto_tac);
   3.597 -by (dres_inst_tac [("k2.0","f b - f a")] Integral_unique 1);
   3.598 -by (dres_inst_tac [("k2.0","f c - f b")] Integral_unique 3);
   3.599 -by Auto_tac;
   3.600 -qed "Integral_add";
   3.601 -
   3.602 -Goal "partition(a,b) D ==> psize D = (LEAST n. D(n) = b)";
   3.603 -by (auto_tac (claset() addSIs [Least_equality RS sym,partition_rhs],simpset()));
   3.604 -by (rtac ccontr 1);
   3.605 -by (dtac partition_ub_lt 1);
   3.606 -by (auto_tac (claset(), simpset() addsimps [linorder_not_less RS sym]));
   3.607 -qed "partition_psize_Least";
   3.608 -
   3.609 -Goal "partition (a, c) D ==> ~ (EX n. c < D(n))";
   3.610 -by (Step_tac 1);
   3.611 -by (dres_inst_tac [("r","n")] partition_ub 1);
   3.612 -by Auto_tac;
   3.613 -qed "lemma_partition_bounded";
   3.614 -
   3.615 -Goal "partition (a, c) D ==> D = (%n. if D n < c then D n else c)";
   3.616 -by (rtac ext 1 THEN Auto_tac);
   3.617 -by (auto_tac (claset() addSDs [lemma_partition_bounded],simpset()));
   3.618 -by (dres_inst_tac [("x","n")] spec 1);
   3.619 -by Auto_tac;
   3.620 -qed "lemma_partition_eq";
   3.621 -
   3.622 -Goal "partition (a, c) D ==> D = (%n. if D n <= c then D n else c)";
   3.623 -by (rtac ext 1 THEN Auto_tac);
   3.624 -by (auto_tac (claset() addSDs [lemma_partition_bounded],simpset()));
   3.625 -by (dres_inst_tac [("x","n")] spec 1);
   3.626 -by Auto_tac;
   3.627 -qed "lemma_partition_eq2";
   3.628 -
   3.629 -Goal "[| partition(a,b) D; n < psize D |] ==> D n < D (Suc n)";
   3.630 -by (auto_tac (claset(),simpset() addsimps [partition]));
   3.631 -qed "partition_lt_Suc";
   3.632 -
   3.633 -Goal "tpart(a,c) (D,p) ==> p = (%n. if D n < c then p n else c)";
   3.634 -by (rtac ext 1);
   3.635 -by (auto_tac (claset(),simpset() addsimps [tpart_def]));
   3.636 -by (dtac (linorder_not_less RS iffD1) 1);
   3.637 -by (dres_inst_tac [("r","Suc n")] partition_ub 1);
   3.638 -by (dres_inst_tac [("x","n")] spec 1);
   3.639 -by Auto_tac;
   3.640 -qed "tpart_tag_eq";
   3.641 -
   3.642 -(*----------------------------------------------------------------------------*)
   3.643 -(* Lemmas for Additivity Theorem of gauge integral                            *)
   3.644 -(*----------------------------------------------------------------------------*)
   3.645 -
   3.646 -Goal "[| a <= D n; D n < b; partition(a,b) D |] ==> n < psize D";
   3.647 -by (dtac (partition RS iffD1) 1 THEN Step_tac 1);
   3.648 -by (rtac ccontr 1 THEN dtac leI 1);
   3.649 -by Auto_tac;
   3.650 -qed "lemma_additivity1";
   3.651 -
   3.652 -Goal "[| a <= D n; partition(a,D n) D |] ==> psize D <= n";
   3.653 -by (rtac ccontr 1 THEN dtac not_leE 1);
   3.654 -by (ftac (partition RS iffD1) 1 THEN Step_tac 1);
   3.655 -by (forw_inst_tac [("r","Suc n")] partition_ub 1);
   3.656 -by (auto_tac (claset() addSDs [spec],simpset()));
   3.657 -qed "lemma_additivity2";
   3.658 -
   3.659 -Goal "[| partition(a,b) D; psize D < m |] ==> D(m) = D(psize D)";
   3.660 -by (auto_tac (claset(),simpset() addsimps [partition]));
   3.661 -qed "partition_eq_bound";
   3.662 -
   3.663 -Goal "[| partition(a,b) D; psize D < m |] ==> D(r) <= D(m)";
   3.664 -by (ftac (partition RS iffD1) 1 THEN Auto_tac);
   3.665 -by (etac partition_ub 1);
   3.666 -qed "partition_ub2";
   3.667 -
   3.668 -Goalw [tpart_def]
   3.669 -    "[| tpart(a,b) (D,p); psize D <= m |] ==> p(m) = D(m)";
   3.670 -by Auto_tac;
   3.671 -by (dres_inst_tac [("x","m")] spec 1);
   3.672 -by (auto_tac (claset(),simpset() addsimps [partition_rhs2]));
   3.673 -qed "tag_point_eq_partition_point";
   3.674 -
   3.675 -Goal "[| partition(a,b) D; D m < D n |] ==> m < n";
   3.676 -by (cut_inst_tac [("m","n"),("n","psize D")] less_linear 1);
   3.677 -by Auto_tac;
   3.678 -by (rtac ccontr 1 THEN dtac leI 1 THEN dtac le_imp_less_or_eq 1);
   3.679 -by (cut_inst_tac [("m","m"),("n","psize D")] less_linear 1);
   3.680 -by (auto_tac (claset() addDs [partition_gt],simpset()));
   3.681 -by (dres_inst_tac [("n","m")] partition_lt_gen 1 THEN Auto_tac);
   3.682 -by (ftac partition_eq_bound 1);
   3.683 -by (dtac partition_gt 2);
   3.684 -by Auto_tac;
   3.685 -by (rtac ccontr 1 THEN dtac leI 1 THEN dtac le_imp_less_or_eq 1);
   3.686 -by (auto_tac (claset() addDs [partition_eq_bound],simpset()));
   3.687 -by (rtac ccontr 1 THEN dtac leI 1 THEN dtac le_imp_less_or_eq 1);
   3.688 -by (ftac partition_eq_bound 1 THEN assume_tac 1);
   3.689 -by (dres_inst_tac [("m","m")] partition_eq_bound 1);
   3.690 -by Auto_tac;
   3.691 -qed "partition_lt_cancel";
   3.692 -
   3.693 -Goalw [psize_def] 
   3.694 -     "[| a <= D n; D n < b; partition (a, b) D |] \
   3.695 -\     ==> psize (%x. if D x < D n then D(x) else D n) = n";
   3.696 -by (ftac lemma_additivity1 1);
   3.697 -by (assume_tac 1 THEN assume_tac 1);
   3.698 -by (rtac some_equality 1);
   3.699 -by (auto_tac (claset() addIs [partition_lt_Suc],simpset()));
   3.700 -by (dres_inst_tac [("n","n")] partition_lt_gen 1);
   3.701 -by (assume_tac 1 THEN arith_tac 1 THEN arith_tac 1);
   3.702 -by (cut_inst_tac [("m","na"),("n","psize D")] less_linear 1);
   3.703 -by (auto_tac (claset() addDs [partition_lt_cancel],simpset()));
   3.704 -by (rtac ccontr 1);
   3.705 -by (dtac (ARITH_PROVE "m ~= (n::nat) ==> m < n | n < m") 1);
   3.706 -by (etac disjE 1);
   3.707 -by (rotate_tac 5 1);
   3.708 -by (dres_inst_tac [("x","n")] spec 1);
   3.709 -by Auto_tac;
   3.710 -by (dres_inst_tac [("n","n")] partition_lt_gen 1);
   3.711 -by Auto_tac;
   3.712 -by (arith_tac 1);
   3.713 -by (dres_inst_tac [("x","n")] spec 1);
   3.714 -by (asm_full_simp_tac (simpset() addsimps [split_if]) 1);
   3.715 -qed "lemma_additivity4_psize_eq";
   3.716 -
   3.717 -Goal "partition (a, b) D  \
   3.718 -\     ==> psize (%x. if D x < D n then D(x) else D n) <= psize D";
   3.719 -by (forw_inst_tac [("r","n")] partition_ub 1);
   3.720 -by (dres_inst_tac [("x","D n")] real_le_imp_less_or_eq 1);
   3.721 -by (auto_tac (claset(),simpset() addsimps 
   3.722 -    [lemma_partition_eq RS sym]));
   3.723 -by (forw_inst_tac [("r","n")] partition_lb 1);
   3.724 -by (dtac lemma_additivity4_psize_eq 1);
   3.725 -by (rtac ccontr 3 THEN Auto_tac);
   3.726 -by (ftac (not_leE RSN (2,partition_eq_bound)) 1);
   3.727 -by (auto_tac (claset(),simpset() addsimps [partition_rhs]));
   3.728 -qed "lemma_psize_left_less_psize";
   3.729 -
   3.730 -Goal "[| partition(a,b) D; na < psize (%x. if D x < D n then D(x) else D n) |] \
   3.731 -\     ==> na < psize D";
   3.732 -by (etac (lemma_psize_left_less_psize RSN (2,less_le_trans)) 1);
   3.733 -by (assume_tac 1);
   3.734 -qed "lemma_psize_left_less_psize2";
   3.735 -
   3.736 -
   3.737 -Goal "[| partition(a,b) D; D na < D n; D n < D (Suc na); \
   3.738 -\        n < psize D |] \
   3.739 -\     ==> False";
   3.740 -by (cut_inst_tac [("m","n"),("n","Suc na")] less_linear 1);
   3.741 -by Auto_tac;
   3.742 -by (dres_inst_tac [("n","n")] partition_lt_gen 2);
   3.743 -by Auto_tac;
   3.744 -by (cut_inst_tac [("m","psize D"),("n","na")] less_linear 1);
   3.745 -by (auto_tac (claset(),simpset() addsimps [partition_rhs2]));
   3.746 -by (dtac (ARITH_PROVE "n < Suc na ==> n < na | n = na") 1);
   3.747 -by Auto_tac;
   3.748 -by (dres_inst_tac [("n","na")] partition_lt_gen 1);
   3.749 -by Auto_tac;
   3.750 -qed "lemma_additivity3";
   3.751 -
   3.752 -Goalw [psize_def] "psize (%x. k) = 0";
   3.753 -by Auto_tac;
   3.754 -qed "psize_const";
   3.755 -Addsimps [psize_const];
   3.756 -
   3.757 -Goal "[| partition(a,b) D; D na < D n; D n < D (Suc na); \
   3.758 -\        na < psize D |] \
   3.759 -\     ==> False";
   3.760 -by (forw_inst_tac [("m","n")] partition_lt_cancel 1);
   3.761 -by (auto_tac (claset() addIs [lemma_additivity3],simpset()));
   3.762 -qed "lemma_additivity3a";
   3.763 -
   3.764 -Goal "[| partition(a,b) D; D n < b |] ==> psize (%x. D (x + n)) <= psize D - n";
   3.765 -by (res_inst_tac [("D2","(%x. D (x + n))")] (psize_def RS 
   3.766 -    meta_eq_to_obj_eq RS ssubst) 1);
   3.767 -by (res_inst_tac [("a","psize D - n")] someI2 1);
   3.768 -by Auto_tac;
   3.769 -by (dtac (ARITH_PROVE "(m::nat) < n - p  ==> m + p < n") 1);
   3.770 -by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
   3.771 -by (dtac (ARITH_PROVE "(m::nat) - n <= p  ==> m <= p + n") 1);
   3.772 -by (case_tac "psize D <= n" 1);
   3.773 -by (dtac not_leE 2);
   3.774 -by (asm_simp_tac (simpset() addsimps 
   3.775 -    [ARITH_PROVE "p <= n ==> p - n = (0::nat)"]) 1);
   3.776 -by (blast_tac (claset() addDs [partition_rhs2]) 1);
   3.777 -by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
   3.778 -by (rtac ccontr 1 THEN dtac not_leE 1);
   3.779 -by (dres_inst_tac [("x","psize D - n")] spec 1);
   3.780 -by Auto_tac;
   3.781 -by (ftac partition_rhs 1 THEN Step_tac 1); 
   3.782 -by (ftac partition_lt_cancel 1 THEN assume_tac 1);
   3.783 -by (dtac (partition  RS iffD1) 1 THEN Step_tac 1);
   3.784 -by (subgoal_tac "~  D (psize D - n + n) < D (Suc (psize D - n + n))" 1);
   3.785 -by (Blast_tac 1);
   3.786 -by (rotate_tac 6 1 THEN dres_inst_tac [("x","Suc (psize D)")] spec 1);
   3.787 -by (Asm_simp_tac 1);
   3.788 -qed "better_lemma_psize_right_eq1";
   3.789 -
   3.790 -Goal "partition (a, D n) D ==> psize D <= n";
   3.791 -by (rtac ccontr 1 THEN dtac not_leE 1);
   3.792 -by (ftac partition_lt_Suc 1 THEN assume_tac 1);
   3.793 -by (forw_inst_tac [("r","Suc n")] partition_ub 1);
   3.794 -by Auto_tac;
   3.795 -qed "psize_le_n";
   3.796 -
   3.797 -Goal "partition(a,D n) D ==> psize (%x. D (x + n)) <= psize D - n";
   3.798 -by (res_inst_tac [("D2","(%x. D (x + n))")] (psize_def RS 
   3.799 -    meta_eq_to_obj_eq RS ssubst) 1);
   3.800 -by (res_inst_tac [("a","psize D - n")] someI2 1);
   3.801 -by Auto_tac;
   3.802 -by (dtac (ARITH_PROVE "(m::nat) < n - p  ==> m + p < n") 1);
   3.803 -by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
   3.804 -by (dtac (ARITH_PROVE "(m::nat) - n <= p  ==> m <= p + n") 1);
   3.805 -by (case_tac "psize D <= n" 1);
   3.806 -by (dtac not_leE 2);
   3.807 -by (asm_simp_tac (simpset() addsimps 
   3.808 -    [ARITH_PROVE "p <= n ==> p - n = (0::nat)"]) 1);
   3.809 -by (blast_tac (claset() addDs [partition_rhs2]) 1);
   3.810 -by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
   3.811 -by (rtac ccontr 1 THEN dtac not_leE 1);
   3.812 -by (ftac psize_le_n 1);
   3.813 -by (dres_inst_tac [("x","psize D - n")] spec 1);
   3.814 -by (asm_full_simp_tac (simpset() addsimps 
   3.815 -    [ARITH_PROVE "p <= n ==> p - n = (0::nat)"]) 1);
   3.816 -by (dtac (partition  RS iffD1) 1 THEN Step_tac 1);
   3.817 -by (rotate_tac 5 1 THEN dres_inst_tac [("x","Suc n")] spec 1);
   3.818 -by Auto_tac;
   3.819 -qed "better_lemma_psize_right_eq1a";
   3.820 -
   3.821 -Goal "partition(a,b) D ==> psize (%x. D (x + n)) <= psize D - n";
   3.822 -by (forw_inst_tac [("r1","n")] (partition_ub RS real_le_imp_less_or_eq) 1);
   3.823 -by (blast_tac (claset() addIs [better_lemma_psize_right_eq1a,
   3.824 -    better_lemma_psize_right_eq1]) 1);
   3.825 -qed "better_lemma_psize_right_eq";
   3.826 -
   3.827 -Goal "[| partition(a,b) D; D n < b |] ==> psize (%x. D (x + n)) <= psize D";
   3.828 -by (res_inst_tac [("D2","(%x. D (x + n))")] (psize_def RS 
   3.829 -    meta_eq_to_obj_eq RS ssubst) 1);
   3.830 -by (res_inst_tac [("a","psize D - n")] someI2 1);
   3.831 -by Auto_tac;
   3.832 -by (dtac (ARITH_PROVE "(m::nat) < n - p  ==> m + p < n") 1);
   3.833 -by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
   3.834 -by (subgoal_tac "n <= psize D" 1);
   3.835 -by (dtac (ARITH_PROVE "(m::nat) - n <= p  ==> m <= p + n") 1);
   3.836 -by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
   3.837 -by (rtac ccontr 1 THEN dtac not_leE 1);
   3.838 -by (dtac (less_imp_le RSN (2,partition_rhs2)) 1);
   3.839 -by Auto_tac;
   3.840 -by (rtac ccontr 1 THEN dtac not_leE 1);
   3.841 -by (dres_inst_tac [("x","psize D")] spec 1);
   3.842 -by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
   3.843 -qed "lemma_psize_right_eq1";
   3.844 -
   3.845 -(* should be combined with previous theorem; also proof has redundancy *)
   3.846 -Goal "partition(a,D n) D ==> psize (%x. D (x + n)) <= psize D";
   3.847 -by (res_inst_tac [("D2","(%x. D (x + n))")] (psize_def RS 
   3.848 -    meta_eq_to_obj_eq RS ssubst) 1);
   3.849 -by (res_inst_tac [("a","psize D - n")] someI2 1);
   3.850 -by Auto_tac;
   3.851 -by (dtac (ARITH_PROVE "(m::nat) < n - p  ==> m + p < n") 1);
   3.852 -by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
   3.853 -by (dtac (ARITH_PROVE "(m::nat) - n <= p  ==> m <= p + n") 1);
   3.854 -by (case_tac "psize D <= n" 1);
   3.855 -by (dtac not_leE 2);
   3.856 -by (asm_simp_tac (simpset() addsimps 
   3.857 -    [ARITH_PROVE "p <= n ==> p - n = (0::nat)"]) 1);
   3.858 -by (blast_tac (claset() addDs [partition_rhs2]) 1);
   3.859 -by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
   3.860 -by (rtac ccontr 1 THEN dtac not_leE 1);
   3.861 -by (dres_inst_tac [("x","psize D")] spec 1);
   3.862 -by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
   3.863 -qed "lemma_psize_right_eq1a";
   3.864 -
   3.865 -Goal "[| partition(a,b) D |] ==> psize (%x. D (x + n)) <= psize D";
   3.866 -by (forw_inst_tac [("r1","n")] (partition_ub RS real_le_imp_less_or_eq) 1);
   3.867 -by (blast_tac (claset() addIs [lemma_psize_right_eq1a,lemma_psize_right_eq1]) 1);
   3.868 -qed "lemma_psize_right_eq";
   3.869 -
   3.870 -Goal "[| a <= D n; tpart (a, b) (D, p) |] \
   3.871 -\     ==> tpart(a, D n) (%x. if D x < D n then D(x) else D n, \
   3.872 -\         %x. if D x < D n then p(x) else D n)";
   3.873 -by (forw_inst_tac [("r","n")] (tpart_partition RS partition_ub) 1);
   3.874 -by (dres_inst_tac [("x","D n")] real_le_imp_less_or_eq 1);
   3.875 -by (auto_tac (claset(),simpset() addsimps 
   3.876 -    [tpart_partition RS lemma_partition_eq RS sym,
   3.877 -     tpart_tag_eq RS sym]));
   3.878 -by (ftac (tpart_partition RSN (3,lemma_additivity1)) 1); 
   3.879 -by (auto_tac (claset(),simpset() addsimps [tpart_def]));
   3.880 -by (dtac ((linorder_not_less RS iffD1) RS real_le_imp_less_or_eq) 2);
   3.881 -by (Auto_tac);
   3.882 -by (blast_tac (claset() addDs [lemma_additivity3]) 2);
   3.883 -by (dtac (linorder_not_less RS iffD1) 2 THEN dres_inst_tac [("x","na")] spec 2);
   3.884 -by (arith_tac 2);
   3.885 -by (ftac lemma_additivity4_psize_eq 1);
   3.886 -by (REPEAT(assume_tac 1));
   3.887 -by (rtac (partition RS iffD2) 1);
   3.888 -by (ftac (partition RS iffD1) 1);
   3.889 -by (auto_tac (claset() addIs [partition_lt_gen],simpset() addsimps []));
   3.890 -by (dres_inst_tac [("n","n")] partition_lt_gen 1);
   3.891 -by (assume_tac 1 THEN arith_tac 1);
   3.892 -by (Blast_tac 1);
   3.893 -by (dtac partition_lt_cancel 1 THEN Auto_tac);
   3.894 -qed "tpart_left1";
   3.895 -
   3.896 -Goal "[| a <= D n; tpart (a, b) (D, p); gauge (%x. a <= x & x <= D n) g;\
   3.897 -\        fine (%x. if x < D n then min (g x) ((D n - x)/ 2) \
   3.898 -\                else if x = D n then min (g (D n)) (ga (D n)) \
   3.899 -\                     else min (ga x) ((x - D n)/ 2)) (D, p) |] \
   3.900 -\     ==> fine g \
   3.901 -\          (%x. if D x < D n then D(x) else D n, \
   3.902 -\           %x. if D x < D n then p(x) else D n)";
   3.903 -by (auto_tac (claset(),simpset() addsimps [fine_def,tpart_def,gauge_def]));
   3.904 -by (ALLGOALS (ftac lemma_psize_left_less_psize2));
   3.905 -by (TRYALL(assume_tac));
   3.906 -by (ALLGOALS (dres_inst_tac [("x","na")] spec) THEN Auto_tac);
   3.907 -by (ALLGOALS(dres_inst_tac [("x","na")] spec));
   3.908 -by Auto_tac;
   3.909 -by (asm_full_simp_tac (simpset() addsimps [split_if]) 1);
   3.910 -by (dtac ((linorder_not_less RS iffD1) RS real_le_imp_less_or_eq) 1);
   3.911 -by (Step_tac 1);
   3.912 -by (blast_tac (claset() addDs [lemma_additivity3a]) 1);
   3.913 -by (dtac sym 1 THEN Auto_tac);
   3.914 -qed "fine_left1";
   3.915 -
   3.916 -Goal "[| a <= D n; tpart (a, b) (D, p) |] \
   3.917 -\     ==> tpart(D n, b) (%x. D(x + n),%x. p(x + n))";
   3.918 -by (asm_full_simp_tac (simpset() addsimps [tpart_def,partition_def]) 1);
   3.919 -by (Step_tac 1);
   3.920 -by (res_inst_tac [("x","N - n")] exI 1 THEN Auto_tac);
   3.921 -by (rotate_tac 2 1);
   3.922 -by (dres_inst_tac [("x","na + n")] spec 1);
   3.923 -by (rotate_tac 3 2);
   3.924 -by (dres_inst_tac [("x","na + n")] spec 2);
   3.925 -by (ALLGOALS(arith_tac));
   3.926 -qed "tpart_right1";
   3.927 -
   3.928 -Goal "[| a <= D n; tpart (a, b) (D, p); gauge (%x. D n <= x & x <= b) ga;\
   3.929 -\        fine (%x. if x < D n then min (g x) ((D n - x)/ 2) \
   3.930 -\                else if x = D n then min (g (D n)) (ga (D n)) \
   3.931 -\                     else min (ga x) ((x - D n)/ 2)) (D, p) |] \
   3.932 -\     ==> fine ga (%x. D(x + n),%x. p(x + n))";
   3.933 -by (auto_tac (claset(),simpset() addsimps [fine_def,gauge_def]));
   3.934 -by (dres_inst_tac [("x","na + n")] spec 1);
   3.935 -by (forw_inst_tac [("n","n")] (tpart_partition RS better_lemma_psize_right_eq) 1);
   3.936 -by Auto_tac;
   3.937 -by (arith_tac 1);
   3.938 -by (asm_full_simp_tac (simpset() addsimps [tpart_def]) 1 THEN Step_tac 1);
   3.939 -by (subgoal_tac "D n <= p (na + n)" 1);
   3.940 -by (dres_inst_tac [("y","p (na + n)")] real_le_imp_less_or_eq 1);
   3.941 -by (Step_tac 1);
   3.942 -by (asm_full_simp_tac (simpset() addsimps [split_if]) 1);
   3.943 -by (Asm_full_simp_tac 1);
   3.944 -by (dtac less_le_trans 1 THEN assume_tac 1);
   3.945 -by (rotate_tac 5 1);
   3.946 -by (dres_inst_tac [("x","na + n")] spec 1 THEN Step_tac 1);
   3.947 -by (rtac real_le_trans 1 THEN assume_tac 2);
   3.948 -by (case_tac "na = 0" 1 THEN Auto_tac);
   3.949 -by (rtac (partition_lt_gen RS order_less_imp_le) 1);
   3.950 -by Auto_tac;
   3.951 -by (arith_tac 1);
   3.952 -qed "fine_right1";
   3.953 -
   3.954 -Goalw [rsum_def] 
   3.955 -   "rsum (D, p) (%x. f x + g x) =  rsum (D, p) f + rsum(D, p) g";
   3.956 -by (auto_tac (claset(),simpset() addsimps [sumr_add,left_distrib]));
   3.957 -qed "rsum_add";
   3.958 -
   3.959 -(* Bartle/Sherbert: Theorem 10.1.5 p. 278 *)
   3.960 -Goalw [Integral_def] 
   3.961 -    "[| a <= b; Integral(a,b) f k1; Integral(a,b) g k2 |] \
   3.962 -\    ==> Integral(a,b) (%x. f x + g x) (k1 + k2)";
   3.963 -by Auto_tac;
   3.964 -by (REPEAT(dres_inst_tac [("x","e/2")] spec 1));
   3.965 -by Auto_tac;
   3.966 -by (dtac gauge_min 1 THEN assume_tac 1);
   3.967 -by (res_inst_tac [("x","(%x. if ga x < gaa x then ga x else gaa x)")] exI 1);
   3.968 -by Auto_tac;
   3.969 -by (dtac fine_min 1);
   3.970 -by (REPEAT(dtac spec 1) THEN Auto_tac);
   3.971 -by (dres_inst_tac  [("a","abs (rsum (D, p) f - k1)* 2"),
   3.972 -    ("c","abs (rsum (D, p) g - k2) * 2")] 
   3.973 -    add_strict_mono 1 THEN assume_tac 1);
   3.974 -by (auto_tac (claset(),HOL_ss addsimps [rsum_add,left_distrib RS sym,
   3.975 -    mult_2_right RS sym,real_mult_less_iff1,CLAIM "(0::real) < 2"]));
   3.976 -by (arith_tac 1);
   3.977 -qed "Integral_add_fun";
   3.978 -
   3.979 -Goal "[| partition(a,b) D; r < psize D |] ==> 0 < D (Suc r) - D r";
   3.980 -by (auto_tac (claset(),simpset() addsimps [partition]));
   3.981 -qed "partition_lt_gen2";
   3.982 -
   3.983 -Goalw [tpart_def] 
   3.984 -     "[| ALL x. a <= x & x <= b --> f x <= g x; \
   3.985 -\        tpart(a,b) (D,p) \
   3.986 -\     |] ==> ALL n. n <= psize D --> f (p n) <= g (p n)";
   3.987 -by (Auto_tac THEN ftac (partition RS iffD1) 1);
   3.988 -by Auto_tac;
   3.989 -by (dres_inst_tac [("x","p n")] spec 1);
   3.990 -by Auto_tac;
   3.991 -by (case_tac "n = 0" 1);
   3.992 -by (rtac (partition_lt_gen RS order_less_le_trans RS order_less_imp_le) 2);
   3.993 -by Auto_tac;
   3.994 -by (dtac le_imp_less_or_eq 1 THEN Auto_tac);
   3.995 -by (dres_inst_tac [("x","psize D")] spec 2 THEN Auto_tac);
   3.996 -by (dres_inst_tac [("r","Suc n")] partition_ub 1);
   3.997 -by (dres_inst_tac [("x","n")] spec 1);
   3.998 -by Auto_tac;
   3.999 -qed "lemma_Integral_le";
  3.1000 -
  3.1001 -Goalw [rsum_def] 
  3.1002 -     "[| ALL x. a <= x & x <= b --> f x <= g x; \
  3.1003 -\        tpart(a,b) (D,p) \
  3.1004 -\     |] ==> rsum(D,p) f <= rsum(D,p) g";
  3.1005 -by (auto_tac (claset() addSIs [sumr_le2] addDs 
  3.1006 -    [tpart_partition RS partition_lt_gen2] addSDs 
  3.1007 -    [lemma_Integral_le],simpset()));
  3.1008 -qed "lemma_Integral_rsum_le";
  3.1009 -
  3.1010 -Goalw [Integral_def] 
  3.1011 -    "[| a <= b; \
  3.1012 -\       ALL x. a <= x & x <= b --> f(x) <= g(x); \
  3.1013 -\       Integral(a,b) f k1; Integral(a,b) g k2 \
  3.1014 -\    |] ==> k1 <= k2";
  3.1015 -by Auto_tac;
  3.1016 -by (rotate_tac 2 1);
  3.1017 -by (dres_inst_tac [("x","abs(k1 - k2)/2")] spec 1);
  3.1018 -by (dres_inst_tac [("x","abs(k1 - k2)/2")] spec 1);
  3.1019 -by Auto_tac;
  3.1020 -by (dtac gauge_min 1 THEN assume_tac 1);
  3.1021 -by (dres_inst_tac [("g","%x. if ga x < gaa x then ga x else gaa x")] 
  3.1022 -    partition_exists 1 THEN assume_tac 1);
  3.1023 -by Auto_tac;
  3.1024 -by (dtac fine_min 1);
  3.1025 -by (dres_inst_tac [("x","D")] spec 1 THEN dres_inst_tac [("x","D")] spec 1);
  3.1026 -by (dres_inst_tac [("x","p")] spec 1 THEN dres_inst_tac [("x","p")] spec 1);
  3.1027 -by Auto_tac;
  3.1028 -by (ftac lemma_Integral_rsum_le 1 THEN assume_tac 1);
  3.1029 -by (subgoal_tac 
  3.1030 -    "abs((rsum(D,p) f - k1) - (rsum(D,p) g - k2)) < abs(k1 - k2)" 1);
  3.1031 -by (arith_tac 1);
  3.1032 -by (dtac add_strict_mono 1 THEN assume_tac 1);
  3.1033 -by (auto_tac (claset(),HOL_ss addsimps [left_distrib RS sym,
  3.1034 -    mult_2_right RS sym,real_mult_less_iff1,CLAIM "(0::real) < 2"]));
  3.1035 -by (arith_tac 1);
  3.1036 -qed "Integral_le";
  3.1037 -
  3.1038 -Goalw [Integral_def] 
  3.1039 -     "(EX k. Integral(a,b) f k) ==> \
  3.1040 -\     (ALL e. 0 < e --> \
  3.1041 -\              (EX g. gauge (%x. a <= x & x <= b) g & \
  3.1042 -\                      (ALL D1 D2 p1 p2. \
  3.1043 -\                           tpart(a,b) (D1, p1) & fine g (D1,p1) & \
  3.1044 -\                           tpart(a,b) (D2, p2) & fine g (D2,p2) --> \ 
  3.1045 -\                           abs(rsum(D1,p1) f - rsum(D2,p2) f) < e)))";
  3.1046 -by Auto_tac;
  3.1047 -by (dres_inst_tac [("x","e/2")] spec 1);
  3.1048 -by Auto_tac;
  3.1049 -by (rtac exI 1 THEN Auto_tac);
  3.1050 -by (forw_inst_tac [("x","D1")] spec 1);
  3.1051 -by (forw_inst_tac [("x","D2")] spec 1);
  3.1052 -by (REPEAT(dtac spec 1) THEN Auto_tac);
  3.1053 -by (thin_tac "0 < e" 1);
  3.1054 -by (dtac add_strict_mono 1 THEN assume_tac 1);
  3.1055 -by (auto_tac (claset(),HOL_ss addsimps [left_distrib RS sym,
  3.1056 -    mult_2_right RS sym,real_mult_less_iff1,CLAIM "(0::real) < 2"]));
  3.1057 -by (arith_tac 1);
  3.1058 -qed "Integral_imp_Cauchy";
  3.1059 -
  3.1060 -Goalw [Cauchy_def] 
  3.1061 -     "Cauchy X = \
  3.1062 -\     (ALL j. (EX M. ALL m n. M <= m & M <= n --> \
  3.1063 -\              abs (X m + - X n) < inverse(real (Suc j))))";
  3.1064 -by Auto_tac;
  3.1065 -by (dtac reals_Archimedean 1);
  3.1066 -by (Step_tac 1);
  3.1067 -by (dres_inst_tac [("x","n")] spec 1);
  3.1068 -by Auto_tac;
  3.1069 -by (res_inst_tac [("x","M")] exI 1);
  3.1070 -by Auto_tac;
  3.1071 -by (dres_inst_tac [("x","m")] spec 1);
  3.1072 -by (dres_inst_tac [("x","na")] spec 1);
  3.1073 -by Auto_tac;
  3.1074 -qed "Cauchy_iff2";
  3.1075 -
  3.1076 -Goal "[| a <= b; ALL n. gauge (%x. a <= x & x <= b) (fa n) |] \
  3.1077 -\     ==> ALL n. EX D p. tpart (a, b) (D, p) & fine (fa n) (D, p)";
  3.1078 -by (Step_tac 1);
  3.1079 -by (rtac partition_exists 1 THEN Auto_tac);
  3.1080 -qed "partition_exists2";
  3.1081 -
  3.1082 -Goal "[| a <= b; ALL c. a <= c & c <= b --> f' c <= g' c; \
  3.1083 -\        ALL x. DERIV f x :> f' x; ALL x. DERIV g x :> g' x \
  3.1084 -\     |] ==> f b - f a <= g b - g a";
  3.1085 -by (rtac Integral_le 1);
  3.1086 -by (assume_tac 1);
  3.1087 -by (rtac FTC1 2);
  3.1088 -by (rtac FTC1 4);
  3.1089 -by Auto_tac;
  3.1090 -qed "monotonic_anti_derivative";
     4.1 --- a/src/HOL/Hyperreal/Integration.thy	Fri Jul 30 10:44:42 2004 +0200
     4.2 +++ b/src/HOL/Hyperreal/Integration.thy	Fri Jul 30 18:37:58 2004 +0200
     4.3 @@ -1,58 +1,910 @@
     4.4  (*  Title       : Integration.thy
     4.5      Author      : Jacques D. Fleuriot
     4.6      Copyright   : 2000  University of Edinburgh
     4.7 -    Description : Theory of integration (cf. Harrison's HOL development)
     4.8 +    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     4.9  *)
    4.10  
    4.11 -Integration = MacLaurin + 
    4.12 +header{*Theory of Integration*}
    4.13  
    4.14 +theory Integration = MacLaurin:
    4.15 +
    4.16 +text{*We follow John Harrison in formalizing the Gauge integral.*}
    4.17  
    4.18  constdefs
    4.19  
    4.20 -  
    4.21 -(* ------------------------------------------------------------------------ *)
    4.22 -(* Partitions and tagged partitions etc.                                    *)
    4.23 -(* ------------------------------------------------------------------------ *)
    4.24 +  --{*Partitions and tagged partitions etc.*}
    4.25  
    4.26    partition :: "[(real*real),nat => real] => bool"
    4.27 -  "partition == %(a,b) D. ((D 0 = a) & 
    4.28 -                         (EX N. ((ALL n. n < N --> D(n) < D(Suc n)) &
    4.29 -                            (ALL n. N <= n --> (D(n) = b)))))"
    4.30 -  
    4.31 -  psize :: (nat => real) => nat
    4.32 -  "psize D == @N. (ALL n. n < N --> D(n) < D(Suc n)) &
    4.33 -                  (ALL n. N <= n --> (D(n) = D(N)))"
    4.34 -  
    4.35 +  "partition == %(a,b) D. ((D 0 = a) &
    4.36 +                         (\<exists>N. ((\<forall>n. n < N --> D(n) < D(Suc n)) &
    4.37 +                            (\<forall>n. N \<le> n --> (D(n) = b)))))"
    4.38 +
    4.39 +  psize :: "(nat => real) => nat"
    4.40 +  "psize D == @N. (\<forall>n. n < N --> D(n) < D(Suc n)) &
    4.41 +                  (\<forall>n. N \<le> n --> (D(n) = D(N)))"
    4.42 +
    4.43    tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool"
    4.44    "tpart == %(a,b) (D,p). partition(a,b) D &
    4.45 -                          (ALL n. D(n) <= p(n) & p(n) <= D(Suc n))"
    4.46 +                          (\<forall>n. D(n) \<le> p(n) & p(n) \<le> D(Suc n))"
    4.47  
    4.48 -(* ------------------------------------------------------------------------ *)
    4.49 -(* Gauges and gauge-fine divisions                                          *)
    4.50 -(* ------------------------------------------------------------------------ *)
    4.51 -  
    4.52 -  gauge :: [real => bool, real => real] => bool
    4.53 -  "gauge E g == ALL x. E x --> 0 < g(x)"
    4.54 +  --{*Gauges and gauge-fine divisions*}
    4.55 +
    4.56 +  gauge :: "[real => bool, real => real] => bool"
    4.57 +  "gauge E g == \<forall>x. E x --> 0 < g(x)"
    4.58  
    4.59    fine :: "[real => real, ((nat => real)*(nat => real))] => bool"
    4.60 -  "fine == % g (D,p). ALL n. n < (psize D) --> D(Suc n) - D(n) < g(p n)"
    4.61 +  "fine == % g (D,p). \<forall>n. n < (psize D) --> D(Suc n) - D(n) < g(p n)"
    4.62  
    4.63 -(* ------------------------------------------------------------------------ *)
    4.64 -(* Riemann sum                                                              *)
    4.65 -(* ------------------------------------------------------------------------ *)
    4.66 +  --{*Riemann sum*}
    4.67  
    4.68    rsum :: "[((nat=>real)*(nat=>real)),real=>real] => real"
    4.69    "rsum == %(D,p) f. sumr 0 (psize(D)) (%n. f(p n) * (D(Suc n) - D(n)))"
    4.70  
    4.71 -(* ------------------------------------------------------------------------ *)
    4.72 -(* Gauge integrability (definite)                                           *)
    4.73 -(* ------------------------------------------------------------------------ *)
    4.74 +  --{*Gauge integrability (definite)*}
    4.75  
    4.76     Integral :: "[(real*real),real=>real,real] => bool"
    4.77 -   "Integral == %(a,b) f k. ALL e. 0 < e -->
    4.78 -                               (EX g. gauge(%x. a <= x & x <= b) g &
    4.79 -                               (ALL D p. tpart(a,b) (D,p) & fine(g)(D,p) -->
    4.80 -                                         abs(rsum(D,p) f - k) < e))"    
    4.81 -end
    4.82 +   "Integral == %(a,b) f k. \<forall>e. 0 < e -->
    4.83 +                               (\<exists>g. gauge(%x. a \<le> x & x \<le> b) g &
    4.84 +                               (\<forall>D p. tpart(a,b) (D,p) & fine(g)(D,p) -->
    4.85 +                                         \<bar>rsum(D,p) f - k\<bar> < e))"
    4.86 +
    4.87 +
    4.88 +lemma partition_zero [simp]: "a = b ==> psize (%n. if n = 0 then a else b) = 0"
    4.89 +by (auto simp add: psize_def)
    4.90 +
    4.91 +lemma partition_one [simp]: "a < b ==> psize (%n. if n = 0 then a else b) = 1"
    4.92 +apply (simp add: psize_def)
    4.93 +apply (rule some_equality, auto)
    4.94 +apply (drule_tac x = 1 in spec, auto)
    4.95 +done
    4.96 +
    4.97 +lemma partition_single [simp]:
    4.98 +     "a \<le> b ==> partition(a,b)(%n. if n = 0 then a else b)"
    4.99 +by (auto simp add: partition_def order_le_less)
   4.100 +
   4.101 +lemma partition_lhs: "partition(a,b) D ==> (D(0) = a)"
   4.102 +by (simp add: partition_def)
   4.103 +
   4.104 +lemma partition:
   4.105 +       "(partition(a,b) D) =
   4.106 +        ((D 0 = a) &
   4.107 +         (\<forall>n. n < (psize D) --> D n < D(Suc n)) &
   4.108 +         (\<forall>n. (psize D) \<le> n --> (D n = b)))"
   4.109 +apply (simp add: partition_def, auto)
   4.110 +apply (subgoal_tac [!] "psize D = N", auto)
   4.111 +apply (simp_all (no_asm) add: psize_def)
   4.112 +apply (rule_tac [!] some_equality, blast)
   4.113 +  prefer 2 apply blast
   4.114 +apply (rule_tac [!] ccontr)
   4.115 +apply (simp_all add: linorder_neq_iff, safe)
   4.116 +apply (drule_tac x = Na in spec)
   4.117 +apply (rotate_tac 3)
   4.118 +apply (drule_tac x = "Suc Na" in spec, simp)
   4.119 +apply (rotate_tac 2)
   4.120 +apply (drule_tac x = N in spec, simp)
   4.121 +apply (drule_tac x = Na in spec)
   4.122 +apply (drule_tac x = "Suc Na" and P = "%n. Na \<le> n \<longrightarrow> D n = D Na" in spec, auto)
   4.123 +done
   4.124 +
   4.125 +lemma partition_rhs: "partition(a,b) D ==> (D(psize D) = b)"
   4.126 +by (simp add: partition)
   4.127 +
   4.128 +lemma partition_rhs2: "[|partition(a,b) D; psize D \<le> n |] ==> (D n = b)"
   4.129 +by (simp add: partition)
   4.130 +
   4.131 +lemma lemma_partition_lt_gen [rule_format]:
   4.132 + "partition(a,b) D & m + Suc d \<le> n & n \<le> (psize D) --> D(m) < D(m + Suc d)"
   4.133 +apply (induct_tac "d", auto simp add: partition)
   4.134 +apply (blast dest: Suc_le_lessD  intro: less_le_trans order_less_trans)
   4.135 +done
   4.136 +
   4.137 +lemma less_eq_add_Suc: "m < n ==> \<exists>d. n = m + Suc d"
   4.138 +by (auto simp add: less_iff_Suc_add)
   4.139 +
   4.140 +lemma partition_lt_gen:
   4.141 +     "[|partition(a,b) D; m < n; n \<le> (psize D)|] ==> D(m) < D(n)"
   4.142 +by (auto dest: less_eq_add_Suc intro: lemma_partition_lt_gen)
   4.143 +
   4.144 +lemma partition_lt: "partition(a,b) D ==> n < (psize D) ==> D(0) < D(Suc n)"
   4.145 +apply (induct "n")
   4.146 +apply (auto simp add: partition)
   4.147 +done
   4.148 +
   4.149 +lemma partition_le: "partition(a,b) D ==> a \<le> b"
   4.150 +apply (frule partition [THEN iffD1], safe)
   4.151 +apply (rotate_tac 2)
   4.152 +apply (drule_tac x = "psize D" in spec, safe)
   4.153 +apply (rule ccontr)
   4.154 +apply (case_tac "psize D = 0", safe)
   4.155 +apply (drule_tac [2] n = "psize D - 1" in partition_lt, auto)
   4.156 +done
   4.157 +
   4.158 +lemma partition_gt: "[|partition(a,b) D; n < (psize D)|] ==> D(n) < D(psize D)"
   4.159 +by (auto intro: partition_lt_gen)
   4.160 +
   4.161 +lemma partition_eq: "partition(a,b) D ==> ((a = b) = (psize D = 0))"
   4.162 +apply (frule partition [THEN iffD1], safe)
   4.163 +apply (rotate_tac 2)
   4.164 +apply (drule_tac x = "psize D" in spec)
   4.165 +apply (rule ccontr)
   4.166 +apply (drule_tac n = "psize D - 1" in partition_lt)
   4.167 +prefer 3 apply (blast, auto)
   4.168 +done
   4.169 +
   4.170 +lemma partition_lb: "partition(a,b) D ==> a \<le> D(r)"
   4.171 +apply (frule partition [THEN iffD1], safe)
   4.172 +apply (induct_tac "r")
   4.173 +apply (cut_tac [2] y = "Suc n" and x = "psize D" in linorder_le_less_linear, safe)
   4.174 + apply (blast intro: order_trans partition_le)
   4.175 +apply (drule_tac x = n in spec)
   4.176 +apply (best intro: order_less_trans order_trans order_less_imp_le)
   4.177 +done
   4.178 +
   4.179 +lemma partition_lb_lt: "[| partition(a,b) D; psize D ~= 0 |] ==> a < D(Suc n)"
   4.180 +apply (rule_tac t = a in partition_lhs [THEN subst], assumption)
   4.181 +apply (cut_tac x = "Suc n" and y = "psize D" in linorder_le_less_linear)
   4.182 +apply (frule partition [THEN iffD1], safe)
   4.183 + apply (blast intro: partition_lt less_le_trans)
   4.184 +apply (rotate_tac 3)
   4.185 +apply (drule_tac x = "Suc n" in spec)
   4.186 +apply (erule impE)
   4.187 +apply (erule less_imp_le)
   4.188 +apply (frule partition_rhs)
   4.189 +apply (drule partition_gt, assumption)
   4.190 +apply (simp (no_asm_simp))
   4.191 +done
   4.192 +
   4.193 +lemma partition_ub: "partition(a,b) D ==> D(r) \<le> b"
   4.194 +apply (frule partition [THEN iffD1])
   4.195 +apply (cut_tac x = "psize D" and y = r in linorder_le_less_linear, safe, blast)
   4.196 +apply (subgoal_tac "\<forall>x. D ((psize D) - x) \<le> b")
   4.197 +apply (rotate_tac 4)
   4.198 +apply (drule_tac x = "psize D - r" in spec)
   4.199 +apply (subgoal_tac "psize D - (psize D - r) = r")
   4.200 +apply simp
   4.201 +apply arith
   4.202 +apply safe
   4.203 +apply (induct_tac "x")
   4.204 +apply (simp (no_asm), blast)
   4.205 +apply (case_tac "psize D - Suc n = 0")
   4.206 +apply (erule_tac V = "\<forall>n. psize D \<le> n --> D n = b" in thin_rl)
   4.207 +apply (simp (no_asm_simp) add: partition_le)
   4.208 +apply (rule order_trans)
   4.209 + prefer 2 apply assumption
   4.210 +apply (subgoal_tac "psize D - n = Suc (psize D - Suc n)")
   4.211 + prefer 2 apply arith
   4.212 +apply (drule_tac x = "psize D - Suc n" in spec)
   4.213 +apply (erule_tac V = "\<forall>n. psize D \<le> n --> D n = b" in thin_rl, simp)
   4.214 +done
   4.215 +
   4.216 +lemma partition_ub_lt: "[| partition(a,b) D; n < psize D |] ==> D(n) < b"
   4.217 +by (blast intro: partition_rhs [THEN subst] partition_gt)
   4.218 +
   4.219 +lemma lemma_partition_append1:
   4.220 +     "[| partition (a, b) D1; partition (b, c) D2 |]
   4.221 +       ==> (\<forall>n.
   4.222 +             n < psize D1 + psize D2 -->
   4.223 +             (if n < psize D1 then D1 n else D2 (n - psize D1))
   4.224 +             < (if Suc n < psize D1 then D1 (Suc n)
   4.225 +                else D2 (Suc n - psize D1))) &
   4.226 +         (\<forall>n.
   4.227 +             psize D1 + psize D2 \<le> n -->
   4.228 +             (if n < psize D1 then D1 n else D2 (n - psize D1)) =
   4.229 +             (if psize D1 + psize D2 < psize D1 then D1 (psize D1 + psize D2)
   4.230 +              else D2 (psize D1 + psize D2 - psize D1)))"
   4.231 +apply safe
   4.232 +apply (auto intro: partition_lt_gen)
   4.233 +apply (subgoal_tac "psize D1 = Suc n")
   4.234 +apply (auto intro!: partition_lt_gen simp add: partition_lhs partition_ub_lt)
   4.235 +apply (auto intro!: partition_rhs2 simp add: partition_rhs
   4.236 +            split: nat_diff_split)
   4.237 +done
   4.238 +
   4.239 +lemma lemma_psize1:
   4.240 +     "[| partition (a, b) D1; partition (b, c) D2; N < psize D1 |]
   4.241 +      ==> D1(N) < D2 (psize D2)"
   4.242 +apply (rule_tac y = "D1 (psize D1) " in order_less_le_trans)
   4.243 +apply (erule partition_gt, assumption)
   4.244 +apply (auto simp add: partition_rhs partition_le)
   4.245 +done
   4.246 +
   4.247 +lemma lemma_partition_append2:
   4.248 +     "[| partition (a, b) D1; partition (b, c) D2 |]
   4.249 +      ==> psize (%n. if n < psize D1 then D1 n else D2 (n - psize D1)) =
   4.250 +          psize D1 + psize D2"
   4.251 +apply (rule_tac D2 = "%n. if n < psize D1 then D1 n else D2 (n - psize D1) "
   4.252 +       in psize_def [THEN meta_eq_to_obj_eq, THEN ssubst])
   4.253 +apply (rule some1_equality)
   4.254 +prefer 2 apply (blast intro!: lemma_partition_append1)
   4.255 +apply (rule ex1I, rule lemma_partition_append1, auto)
   4.256 +apply (rule ccontr)
   4.257 +apply (simp add: linorder_neq_iff, safe)
   4.258 +apply (rotate_tac 3)
   4.259 +apply (drule_tac x = "psize D1 + psize D2" in spec, auto)
   4.260 +apply (case_tac "N < psize D1")
   4.261 +apply (auto dest: lemma_psize1)
   4.262 +apply (subgoal_tac "N - psize D1 < psize D2")
   4.263 + prefer 2 apply arith
   4.264 +apply (drule_tac a = b and b = c in partition_gt, auto)
   4.265 +apply (drule_tac x = "psize D1 + psize D2" in spec)
   4.266 +apply (auto simp add: partition_rhs2)
   4.267 +done
   4.268 +
   4.269 +lemma tpart_eq_lhs_rhs:
   4.270 +"[|psize D = 0; tpart(a,b) (D,p)|] ==> a = b"
   4.271 +apply (simp add: tpart_def)
   4.272 +apply (auto simp add: partition_eq)
   4.273 +done
   4.274 +
   4.275 +lemma tpart_partition: "tpart(a,b) (D,p) ==> partition(a,b) D"
   4.276 +by (simp add: tpart_def)
   4.277 +
   4.278 +lemma partition_append:
   4.279 +     "[| tpart(a,b) (D1,p1); fine(g) (D1,p1);
   4.280 +         tpart(b,c) (D2,p2); fine(g) (D2,p2) |]
   4.281 +       ==> \<exists>D p. tpart(a,c) (D,p) & fine(g) (D,p)"
   4.282 +apply (rule_tac x = "%n. if n < psize D1 then D1 n else D2 (n - psize D1)"
   4.283 +       in exI)
   4.284 +apply (rule_tac x = "%n. if n < psize D1 then p1 n else p2 (n - psize D1)"
   4.285 +       in exI)
   4.286 +apply (case_tac "psize D1 = 0")
   4.287 +apply (auto dest: tpart_eq_lhs_rhs)
   4.288 + prefer 2
   4.289 +apply (simp add: fine_def
   4.290 +                 lemma_partition_append2 [OF tpart_partition tpart_partition])
   4.291 +  --{*But must not expand @{term fine} in other subgoals*}
   4.292 +apply auto
   4.293 +apply (subgoal_tac "psize D1 = Suc n")
   4.294 + prefer 2 apply arith
   4.295 +apply (drule tpart_partition [THEN partition_rhs])
   4.296 +apply (drule tpart_partition [THEN partition_lhs])
   4.297 +apply (auto split: nat_diff_split)
   4.298 +apply (auto simp add: tpart_def)
   4.299 +defer 1
   4.300 + apply (subgoal_tac "psize D1 = Suc n")
   4.301 +  prefer 2 apply arith
   4.302 + apply (drule partition_rhs)
   4.303 + apply (drule partition_lhs, auto)
   4.304 +apply (simp split: nat_diff_split)
   4.305 +apply (subst partition)
   4.306 +apply (subst lemma_partition_append2)
   4.307 +apply (rule_tac [3] conjI)
   4.308 +apply (drule_tac [4] lemma_partition_append1)
   4.309 +apply (auto simp add: partition_lhs partition_rhs)
   4.310 +done
   4.311 +
   4.312 +text{*We can always find a division which is fine wrt any gauge*}
   4.313 +
   4.314 +lemma partition_exists:
   4.315 +     "[| a \<le> b; gauge(%x. a \<le> x & x \<le> b) g |]
   4.316 +      ==> \<exists>D p. tpart(a,b) (D,p) & fine g (D,p)"
   4.317 +apply (cut_tac P = "%(u,v). a \<le> u & v \<le> b --> 
   4.318 +                   (\<exists>D p. tpart (u,v) (D,p) & fine (g) (D,p))" 
   4.319 +       in lemma_BOLZANO2)
   4.320 +apply safe
   4.321 +apply (blast intro: real_le_trans)+
   4.322 +apply (auto intro: partition_append)
   4.323 +apply (case_tac "a \<le> x & x \<le> b")
   4.324 +apply (rule_tac [2] x = 1 in exI, auto)
   4.325 +apply (rule_tac x = "g x" in exI)
   4.326 +apply (auto simp add: gauge_def)
   4.327 +apply (rule_tac x = "%n. if n = 0 then aa else ba" in exI)
   4.328 +apply (rule_tac x = "%n. if n = 0 then x else ba" in exI)
   4.329 +apply (auto simp add: tpart_def fine_def)
   4.330 +done
   4.331 +
   4.332 +text{*Lemmas about combining gauges*}
   4.333 +
   4.334 +lemma gauge_min:
   4.335 +     "[| gauge(E) g1; gauge(E) g2 |]
   4.336 +      ==> gauge(E) (%x. if g1(x) < g2(x) then g1(x) else g2(x))"
   4.337 +by (simp add: gauge_def)
   4.338 +
   4.339 +lemma fine_min:
   4.340 +      "fine (%x. if g1(x) < g2(x) then g1(x) else g2(x)) (D,p)
   4.341 +       ==> fine(g1) (D,p) & fine(g2) (D,p)"
   4.342 +by (auto simp add: fine_def split: split_if_asm)
   4.343 +
   4.344 +
   4.345 +text{*The integral is unique if it exists*}
   4.346 +
   4.347 +lemma Integral_unique:
   4.348 +    "[| a \<le> b; Integral(a,b) f k1; Integral(a,b) f k2 |] ==> k1 = k2"
   4.349 +apply (simp add: Integral_def)
   4.350 +apply (drule_tac x = "\<bar>k1 - k2\<bar> /2" in spec)+
   4.351 +apply auto
   4.352 +apply (drule gauge_min, assumption)
   4.353 +apply (drule_tac g = "%x. if g x < ga x then g x else ga x" 
   4.354 +       in partition_exists, assumption, auto)
   4.355 +apply (drule fine_min)
   4.356 +apply (drule spec)+
   4.357 +apply auto
   4.358 +apply (subgoal_tac "abs ((rsum (D,p) f - k2) - (rsum (D,p) f - k1)) < \<bar>k1 - k2\<bar> ")
   4.359 +apply arith
   4.360 +apply (drule add_strict_mono, assumption)
   4.361 +apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric] 
   4.362 +                mult_less_cancel_right, arith)
   4.363 +done
   4.364 +
   4.365 +lemma Integral_zero [simp]: "Integral(a,a) f 0"
   4.366 +apply (auto simp add: Integral_def)
   4.367 +apply (rule_tac x = "%x. 1" in exI)
   4.368 +apply (auto dest: partition_eq simp add: gauge_def tpart_def rsum_def)
   4.369 +done
   4.370 +
   4.371 +lemma sumr_partition_eq_diff_bounds [simp]:
   4.372 +     "sumr 0 m (%n. D (Suc n) - D n) = D(m) - D 0"
   4.373 +by (induct_tac "m", auto)
   4.374 +
   4.375 +lemma Integral_eq_diff_bounds: "a \<le> b ==> Integral(a,b) (%x. 1) (b - a)"
   4.376 +apply (drule real_le_imp_less_or_eq, auto)
   4.377 +apply (auto simp add: rsum_def Integral_def)
   4.378 +apply (rule_tac x = "%x. b - a" in exI)
   4.379 +apply (auto simp add: gauge_def abs_interval_iff tpart_def partition)
   4.380 +done
   4.381 +
   4.382 +lemma Integral_mult_const: "a \<le> b ==> Integral(a,b) (%x. c)  (c*(b - a))"
   4.383 +apply (drule real_le_imp_less_or_eq, auto)
   4.384 +apply (auto simp add: rsum_def Integral_def)
   4.385 +apply (rule_tac x = "%x. b - a" in exI)
   4.386 +apply (auto simp add: sumr_mult [symmetric] gauge_def abs_interval_iff 
   4.387 +               right_diff_distrib [symmetric] partition tpart_def)
   4.388 +done
   4.389 +
   4.390 +lemma Integral_mult:
   4.391 +     "[| a \<le> b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)"
   4.392 +apply (drule real_le_imp_less_or_eq)
   4.393 +apply (auto dest: Integral_unique [OF real_le_refl Integral_zero])
   4.394 +apply (auto simp add: rsum_def Integral_def sumr_mult [symmetric] real_mult_assoc)
   4.395 +apply (rule_tac a2 = c in abs_ge_zero [THEN real_le_imp_less_or_eq, THEN disjE])
   4.396 + prefer 2 apply force
   4.397 +apply (drule_tac x = "e/abs c" in spec, auto)
   4.398 +apply (simp add: zero_less_mult_iff divide_inverse)
   4.399 +apply (rule exI, auto)
   4.400 +apply (drule spec)+
   4.401 +apply auto
   4.402 +apply (rule_tac z1 = "inverse (abs c) " in real_mult_less_iff1 [THEN iffD1])
   4.403 +apply (auto simp add: divide_inverse [symmetric] right_diff_distrib [symmetric])
   4.404 +done
   4.405 +
   4.406 +text{*Fundamental theorem of calculus (Part I)*}
   4.407 +
   4.408 +text{*"Straddle Lemma" : Swartz & Thompson: AMM 95(7) 1988 *}
   4.409 +
   4.410 +lemma choiceP: "\<forall>x. P(x) --> (\<exists>y. Q x y) ==> \<exists>f. (\<forall>x. P(x) --> Q x (f x))"
   4.411 +by meson
   4.412 +
   4.413 +lemma choiceP2: "\<forall>x. P(x) --> (\<exists>y. R(y) & (\<exists>z. Q x y z)) ==>
   4.414 +      \<exists>f fa. (\<forall>x. P(x) --> R(f x) & Q x (f x) (fa x))"
   4.415 +by meson
   4.416 +
   4.417 +(*UNUSED
   4.418 +lemma choice2: "\<forall>x. (\<exists>y. R(y) & (\<exists>z. Q x y z)) ==>
   4.419 +      \<exists>f fa. (\<forall>x. R(f x) & Q x (f x) (fa x))"
   4.420 +*)
   4.421 +
   4.422 +
   4.423 +(* new simplifications e.g. (y < x/n) = (y * n < x) are a real nuisance
   4.424 +   they break the original proofs and make new proofs longer!                 *)
   4.425 +lemma strad1:
   4.426 +       "\<lbrakk>\<forall>xa::real. xa \<noteq> x \<and> \<bar>xa + - x\<bar> < s \<longrightarrow>
   4.427 +             \<bar>(f xa - f x) / (xa - x) + - f' x\<bar> * 2 < e;
   4.428 +        0 < e; a \<le> x; x \<le> b; 0 < s\<rbrakk>
   4.429 +       \<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>"
   4.430 +apply auto
   4.431 +apply (case_tac "0 < \<bar>z - x\<bar> ")
   4.432 + prefer 2 apply (simp add: zero_less_abs_iff)
   4.433 +apply (drule_tac x = z in spec)
   4.434 +apply (rule_tac z1 = "\<bar>inverse (z - x)\<bar>" 
   4.435 +       in real_mult_le_cancel_iff2 [THEN iffD1])
   4.436 + apply simp
   4.437 +apply (simp del: abs_inverse abs_mult add: abs_mult [symmetric]
   4.438 +          mult_assoc [symmetric])
   4.439 +apply (subgoal_tac "inverse (z - x) * (f z - f x - f' x * (z - x)) 
   4.440 +                    = (f z - f x) / (z - x) - f' x")
   4.441 + apply (simp add: abs_mult [symmetric] mult_ac diff_minus)
   4.442 +apply (subst mult_commute)
   4.443 +apply (simp add: left_distrib diff_minus)
   4.444 +apply (simp add: mult_assoc divide_inverse)
   4.445 +apply (simp add: left_distrib)
   4.446 +done
   4.447 +
   4.448 +lemma lemma_straddle:
   4.449 +     "[| \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x); 0 < e |]
   4.450 +      ==> \<exists>g. gauge(%x. a \<le> x & x \<le> b) g &
   4.451 +                (\<forall>x u v. a \<le> u & u \<le> x & x \<le> v & v \<le> b & (v - u) < g(x)
   4.452 +                  --> abs((f(v) - f(u)) - (f'(x) * (v - u))) \<le> e * (v - u))"
   4.453 +apply (simp add: gauge_def)
   4.454 +apply (subgoal_tac "\<forall>x. a \<le> x & x \<le> b --> 
   4.455 +        (\<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)))")
   4.456 +apply (drule choiceP, auto)
   4.457 +apply (drule spec, auto)
   4.458 +apply (auto simp add: DERIV_iff2 LIM_def)
   4.459 +apply (drule_tac x = "e/2" in spec, auto)
   4.460 +apply (frule strad1, assumption+)
   4.461 +apply (rule_tac x = s in exI, auto)
   4.462 +apply (rule_tac x = u and y = v in linorder_cases, auto)
   4.463 +apply (rule_tac j = "abs ((f (v) - f (x)) - (f' (x) * (v - x))) + abs ((f (x) - f (u)) - (f' (x) * (x - u)))"
   4.464 +       in real_le_trans)
   4.465 +apply (rule abs_triangle_ineq [THEN [2] real_le_trans])
   4.466 +apply (simp add: right_diff_distrib, arith)
   4.467 +apply (rule_tac t = "e* (v - u) " in real_sum_of_halves [THEN subst])
   4.468 +apply (rule add_mono)
   4.469 +apply (rule_tac j = " (e / 2) * \<bar>v - x\<bar> " in real_le_trans)
   4.470 + prefer 2 apply simp apply arith
   4.471 +apply (erule_tac [!]
   4.472 +       V= "\<forall>xa. xa ~= x & \<bar>xa + - x\<bar> < s --> \<bar>(f xa - f x) / (xa - x) + - f' x\<bar> * 2 < e"
   4.473 +        in thin_rl)
   4.474 +apply (drule_tac x = v in spec, auto, arith)
   4.475 +apply (drule_tac x = u in spec, auto, arith)
   4.476 +apply (subgoal_tac "\<bar>f u - f x - f' x * (u - x)\<bar> = \<bar>f x - f u - f' x * (x - u)\<bar>")
   4.477 +apply (rule order_trans)
   4.478 +apply (auto simp add: abs_le_interval_iff)
   4.479 +apply (simp add: right_diff_distrib, arith)
   4.480 +done
   4.481 +
   4.482 +lemma FTC1: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |]
   4.483 +      ==> Integral(a,b) f' (f(b) - f(a))"
   4.484 +apply (drule real_le_imp_less_or_eq, auto)
   4.485 +apply (auto simp add: Integral_def)
   4.486 +apply (rule ccontr)
   4.487 +apply (subgoal_tac "\<forall>e. 0 < e --> (\<exists>g. gauge (%x. a \<le> x & x \<le> b) g & (\<forall>D p. tpart (a, b) (D, p) & fine g (D, p) --> \<bar>rsum (D, p) f' - (f b - f a)\<bar> \<le> e))")
   4.488 +apply (rotate_tac 3)
   4.489 +apply (drule_tac x = "e/2" in spec, auto)
   4.490 +apply (drule spec, auto)
   4.491 +apply ((drule spec)+, auto)
   4.492 +apply (drule_tac e = "ea/ (b - a) " in lemma_straddle)
   4.493 +apply (auto simp add: zero_less_divide_iff)
   4.494 +apply (rule exI)
   4.495 +apply (auto simp add: tpart_def rsum_def)
   4.496 +apply (subgoal_tac "sumr 0 (psize D) (%n. f (D (Suc n)) - f (D n)) = f b - f a")
   4.497 + prefer 2
   4.498 + apply (cut_tac D = "%n. f (D n) " and m = "psize D"
   4.499 +        in sumr_partition_eq_diff_bounds)
   4.500 + apply (simp add: partition_lhs partition_rhs)
   4.501 +apply (drule sym, simp)
   4.502 +apply (simp (no_asm) add: sumr_diff)
   4.503 +apply (rule sumr_rabs [THEN real_le_trans])
   4.504 +apply (subgoal_tac "ea = sumr 0 (psize D) (%n. (ea / (b - a)) * (D (Suc n) - (D n))) ")
   4.505 +apply (simp add: abs_minus_commute)
   4.506 +apply (rule_tac t = ea in ssubst, assumption)
   4.507 +apply (rule sumr_le2)
   4.508 +apply (rule_tac [2] sumr_mult [THEN subst])
   4.509 +apply (auto simp add: partition_rhs partition_lhs partition_lb partition_ub
   4.510 +          fine_def)
   4.511 +done
   4.512  
   4.513  
   4.514 +lemma Integral_subst: "[| Integral(a,b) f k1; k2=k1 |] ==> Integral(a,b) f k2"
   4.515 +by simp
   4.516 +
   4.517 +lemma Integral_add:
   4.518 +     "[| a \<le> b; b \<le> c; Integral(a,b) f' k1; Integral(b,c) f' k2;
   4.519 +         \<forall>x. a \<le> x & x \<le> c --> DERIV f x :> f' x |]
   4.520 +     ==> Integral(a,c) f' (k1 + k2)"
   4.521 +apply (rule FTC1 [THEN Integral_subst], auto)
   4.522 +apply (frule FTC1, auto)
   4.523 +apply (frule_tac a = b in FTC1, auto)
   4.524 +apply (drule_tac x = x in spec, auto)
   4.525 +apply (drule_tac ?k2.0 = "f b - f a" in Integral_unique)
   4.526 +apply (drule_tac [3] ?k2.0 = "f c - f b" in Integral_unique, auto)
   4.527 +done
   4.528 +
   4.529 +lemma partition_psize_Least:
   4.530 +     "partition(a,b) D ==> psize D = (LEAST n. D(n) = b)"
   4.531 +apply (auto intro!: Least_equality [symmetric] partition_rhs)
   4.532 +apply (rule ccontr)
   4.533 +apply (drule partition_ub_lt)
   4.534 +apply (auto simp add: linorder_not_less [symmetric])
   4.535 +done
   4.536 +
   4.537 +lemma lemma_partition_bounded: "partition (a, c) D ==> ~ (\<exists>n. c < D(n))"
   4.538 +apply safe
   4.539 +apply (drule_tac r = n in partition_ub, auto)
   4.540 +done
   4.541 +
   4.542 +lemma lemma_partition_eq:
   4.543 +     "partition (a, c) D ==> D = (%n. if D n < c then D n else c)"
   4.544 +apply (rule ext, auto)
   4.545 +apply (auto dest!: lemma_partition_bounded)
   4.546 +apply (drule_tac x = n in spec, auto)
   4.547 +done
   4.548 +
   4.549 +lemma lemma_partition_eq2:
   4.550 +     "partition (a, c) D ==> D = (%n. if D n \<le> c then D n else c)"
   4.551 +apply (rule ext, auto)
   4.552 +apply (auto dest!: lemma_partition_bounded)
   4.553 +apply (drule_tac x = n in spec, auto)
   4.554 +done
   4.555 +
   4.556 +lemma partition_lt_Suc:
   4.557 +     "[| partition(a,b) D; n < psize D |] ==> D n < D (Suc n)"
   4.558 +by (auto simp add: partition)
   4.559 +
   4.560 +lemma tpart_tag_eq: "tpart(a,c) (D,p) ==> p = (%n. if D n < c then p n else c)"
   4.561 +apply (rule ext)
   4.562 +apply (auto simp add: tpart_def)
   4.563 +apply (drule linorder_not_less [THEN iffD1])
   4.564 +apply (drule_tac r = "Suc n" in partition_ub)
   4.565 +apply (drule_tac x = n in spec, auto)
   4.566 +done
   4.567 +
   4.568 +subsection{*Lemmas for Additivity Theorem of Gauge Integral*}
   4.569 +
   4.570 +lemma lemma_additivity1:
   4.571 +     "[| a \<le> D n; D n < b; partition(a,b) D |] ==> n < psize D"
   4.572 +by (auto simp add: partition linorder_not_less [symmetric])
   4.573 +
   4.574 +lemma lemma_additivity2: "[| a \<le> D n; partition(a,D n) D |] ==> psize D \<le> n"
   4.575 +apply (rule ccontr, drule not_leE)
   4.576 +apply (frule partition [THEN iffD1], safe)
   4.577 +apply (frule_tac r = "Suc n" in partition_ub)
   4.578 +apply (auto dest!: spec)
   4.579 +done
   4.580 +
   4.581 +lemma partition_eq_bound:
   4.582 +     "[| partition(a,b) D; psize D < m |] ==> D(m) = D(psize D)"
   4.583 +by (auto simp add: partition)
   4.584 +
   4.585 +lemma partition_ub2: "[| partition(a,b) D; psize D < m |] ==> D(r) \<le> D(m)"
   4.586 +by (simp add: partition partition_ub)
   4.587 +
   4.588 +lemma tag_point_eq_partition_point:
   4.589 +    "[| tpart(a,b) (D,p); psize D \<le> m |] ==> p(m) = D(m)"
   4.590 +apply (simp add: tpart_def, auto)
   4.591 +apply (drule_tac x = m in spec)
   4.592 +apply (auto simp add: partition_rhs2)
   4.593 +done
   4.594 +
   4.595 +lemma partition_lt_cancel: "[| partition(a,b) D; D m < D n |] ==> m < n"
   4.596 +apply (cut_tac m = n and n = "psize D" in less_linear, auto)
   4.597 +apply (rule ccontr, drule leI, drule le_imp_less_or_eq)
   4.598 +apply (cut_tac m = m and n = "psize D" in less_linear)
   4.599 +apply (auto dest: partition_gt)
   4.600 +apply (drule_tac n = m in partition_lt_gen, auto)
   4.601 +apply (frule partition_eq_bound)
   4.602 +apply (drule_tac [2] partition_gt, auto)
   4.603 +apply (rule ccontr, drule leI, drule le_imp_less_or_eq)
   4.604 +apply (auto dest: partition_eq_bound)
   4.605 +apply (rule ccontr, drule leI, drule le_imp_less_or_eq)
   4.606 +apply (frule partition_eq_bound, assumption)
   4.607 +apply (drule_tac m = m in partition_eq_bound, auto)
   4.608 +done
   4.609 +
   4.610 +lemma lemma_additivity4_psize_eq:
   4.611 +     "[| a \<le> D n; D n < b; partition (a, b) D |]
   4.612 +      ==> psize (%x. if D x < D n then D(x) else D n) = n"
   4.613 +apply (unfold psize_def)
   4.614 +apply (frule lemma_additivity1)
   4.615 +apply (assumption, assumption)
   4.616 +apply (rule some_equality)
   4.617 +apply (auto intro: partition_lt_Suc)
   4.618 +apply (drule_tac n = n in partition_lt_gen)
   4.619 +apply (assumption, arith, arith)
   4.620 +apply (cut_tac m = na and n = "psize D" in less_linear)
   4.621 +apply (auto dest: partition_lt_cancel)
   4.622 +apply (rule_tac x=N and y=n in linorder_cases)
   4.623 +apply (drule_tac x = n and P="%m. N \<le> m --> ?f m = ?g m" in spec, auto)
   4.624 +apply (drule_tac n = n in partition_lt_gen, auto, arith)
   4.625 +apply (drule_tac x = n in spec)
   4.626 +apply (simp split: split_if_asm)
   4.627 +done
   4.628 +
   4.629 +lemma lemma_psize_left_less_psize:
   4.630 +     "partition (a, b) D
   4.631 +      ==> psize (%x. if D x < D n then D(x) else D n) \<le> psize D"
   4.632 +apply (frule_tac r = n in partition_ub)
   4.633 +apply (drule_tac x = "D n" in real_le_imp_less_or_eq)
   4.634 +apply (auto simp add: lemma_partition_eq [symmetric])
   4.635 +apply (frule_tac r = n in partition_lb)
   4.636 +apply (drule lemma_additivity4_psize_eq)
   4.637 +apply (rule_tac [3] ccontr, auto)
   4.638 +apply (frule_tac not_leE [THEN [2] partition_eq_bound])
   4.639 +apply (auto simp add: partition_rhs)
   4.640 +done
   4.641 +
   4.642 +lemma lemma_psize_left_less_psize2:
   4.643 +     "[| partition(a,b) D; na < psize (%x. if D x < D n then D(x) else D n) |]
   4.644 +      ==> na < psize D"
   4.645 +apply (erule_tac lemma_psize_left_less_psize [THEN [2] less_le_trans], assumption)
   4.646 +done
   4.647 +
   4.648 +
   4.649 +lemma lemma_additivity3:
   4.650 +     "[| partition(a,b) D; D na < D n; D n < D (Suc na);
   4.651 +         n < psize D |]
   4.652 +      ==> False"
   4.653 +apply (cut_tac m = n and n = "Suc na" in less_linear, auto)
   4.654 +apply (drule_tac [2] n = n in partition_lt_gen, auto)
   4.655 +apply (cut_tac m = "psize D" and n = na in less_linear)
   4.656 +apply (auto simp add: partition_rhs2 less_Suc_eq)
   4.657 +apply (drule_tac n = na in partition_lt_gen, auto)
   4.658 +done
   4.659 +
   4.660 +lemma psize_const [simp]: "psize (%x. k) = 0"
   4.661 +by (simp add: psize_def, auto)
   4.662 +
   4.663 +lemma lemma_additivity3a:
   4.664 +     "[| partition(a,b) D; D na < D n; D n < D (Suc na);
   4.665 +         na < psize D |]
   4.666 +      ==> False"
   4.667 +apply (frule_tac m = n in partition_lt_cancel)
   4.668 +apply (auto intro: lemma_additivity3)
   4.669 +done
   4.670 +
   4.671 +lemma better_lemma_psize_right_eq1:
   4.672 +     "[| partition(a,b) D; D n < b |] ==> psize (%x. D (x + n)) \<le> psize D - n"
   4.673 +apply (simp add: psize_def [of "(%x. D (x + n))"]);
   4.674 +apply (rule_tac a = "psize D - n" in someI2, auto)
   4.675 +  apply (simp add: partition less_diff_conv)
   4.676 + apply (simp add: le_diff_conv)
   4.677 + apply (case_tac "psize D \<le> n")
   4.678 +  apply (simp add: partition_rhs2)
   4.679 + apply (simp add: partition linorder_not_le)
   4.680 +apply (rule ccontr, drule not_leE)
   4.681 +apply (drule_tac x = "psize D - n" in spec, auto)
   4.682 +apply (frule partition_rhs, safe)
   4.683 +apply (frule partition_lt_cancel, assumption)
   4.684 +apply (drule partition [THEN iffD1], safe)
   4.685 +apply (subgoal_tac "~ D (psize D - n + n) < D (Suc (psize D - n + n))")
   4.686 + apply blast
   4.687 +apply (drule_tac x = "Suc (psize D)" and P="%n. ?P n \<longrightarrow> D n = D (psize D)"
   4.688 +       in spec)
   4.689 +apply (simp (no_asm_simp))
   4.690 +done
   4.691 +
   4.692 +lemma psize_le_n: "partition (a, D n) D ==> psize D \<le> n"
   4.693 +apply (rule ccontr, drule not_leE)
   4.694 +apply (frule partition_lt_Suc, assumption)
   4.695 +apply (frule_tac r = "Suc n" in partition_ub, auto)
   4.696 +done
   4.697 +
   4.698 +lemma better_lemma_psize_right_eq1a:
   4.699 +     "partition(a,D n) D ==> psize (%x. D (x + n)) \<le> psize D - n"
   4.700 +apply (simp add: psize_def [of "(%x. D (x + n))"]);
   4.701 +apply (rule_tac a = "psize D - n" in someI2, auto)
   4.702 +  apply (simp add: partition less_diff_conv)
   4.703 + apply (simp add: le_diff_conv)
   4.704 +apply (case_tac "psize D \<le> n")
   4.705 +  apply (force intro: partition_rhs2)
   4.706 + apply (simp add: partition linorder_not_le)
   4.707 +apply (rule ccontr, drule not_leE)
   4.708 +apply (frule psize_le_n)
   4.709 +apply (drule_tac x = "psize D - n" in spec, simp)
   4.710 +apply (drule partition [THEN iffD1], safe)
   4.711 +apply (drule_tac x = "Suc n" and P="%na. psize D \<le> na \<longrightarrow> D na = D n" in spec, auto)
   4.712 +done
   4.713 +
   4.714 +lemma better_lemma_psize_right_eq:
   4.715 +     "partition(a,b) D ==> psize (%x. D (x + n)) \<le> psize D - n"
   4.716 +apply (frule_tac r1 = n in partition_ub [THEN real_le_imp_less_or_eq])
   4.717 +apply (blast intro: better_lemma_psize_right_eq1a better_lemma_psize_right_eq1)
   4.718 +done
   4.719 +
   4.720 +lemma lemma_psize_right_eq1:
   4.721 +     "[| partition(a,b) D; D n < b |] ==> psize (%x. D (x + n)) \<le> psize D"
   4.722 +apply (simp add: psize_def [of "(%x. D (x + n))"]);
   4.723 +apply (rule_tac a = "psize D - n" in someI2, auto)
   4.724 +  apply (simp add: partition less_diff_conv)
   4.725 + apply (subgoal_tac "n \<le> psize D")
   4.726 +  apply (simp add: partition le_diff_conv)
   4.727 + apply (rule ccontr, drule not_leE)
   4.728 + apply (drule_tac less_imp_le [THEN [2] partition_rhs2], auto)
   4.729 +apply (rule ccontr, drule not_leE)
   4.730 +apply (drule_tac x = "psize D" in spec)
   4.731 +apply (simp add: partition)
   4.732 +done
   4.733 +
   4.734 +(* should be combined with previous theorem; also proof has redundancy *)
   4.735 +lemma lemma_psize_right_eq1a:
   4.736 +     "partition(a,D n) D ==> psize (%x. D (x + n)) \<le> psize D"
   4.737 +apply (simp add: psize_def [of "(%x. D (x + n))"]);
   4.738 +apply (rule_tac a = "psize D - n" in someI2, auto)
   4.739 +  apply (simp add: partition less_diff_conv)
   4.740 + apply (case_tac "psize D \<le> n")
   4.741 +  apply (force intro: partition_rhs2 simp add: le_diff_conv)
   4.742 + apply (simp add: partition le_diff_conv)
   4.743 +apply (rule ccontr, drule not_leE)
   4.744 +apply (drule_tac x = "psize D" in spec)
   4.745 +apply (simp add: partition)
   4.746 +done
   4.747 +
   4.748 +lemma lemma_psize_right_eq:
   4.749 +     "[| partition(a,b) D |] ==> psize (%x. D (x + n)) \<le> psize D"
   4.750 +apply (frule_tac r1 = n in partition_ub [THEN real_le_imp_less_or_eq])
   4.751 +apply (blast intro: lemma_psize_right_eq1a lemma_psize_right_eq1)
   4.752 +done
   4.753 +
   4.754 +lemma tpart_left1:
   4.755 +     "[| a \<le> D n; tpart (a, b) (D, p) |]
   4.756 +      ==> tpart(a, D n) (%x. if D x < D n then D(x) else D n,
   4.757 +          %x. if D x < D n then p(x) else D n)"
   4.758 +apply (frule_tac r = n in tpart_partition [THEN partition_ub])
   4.759 +apply (drule_tac x = "D n" in real_le_imp_less_or_eq)
   4.760 +apply (auto simp add: tpart_partition [THEN lemma_partition_eq, symmetric] tpart_tag_eq [symmetric])
   4.761 +apply (frule_tac tpart_partition [THEN [3] lemma_additivity1])
   4.762 +apply (auto simp add: tpart_def)
   4.763 +apply (drule_tac [2] linorder_not_less [THEN iffD1, THEN real_le_imp_less_or_eq], auto)
   4.764 +  prefer 3
   4.765 +  apply (drule linorder_not_less [THEN iffD1])
   4.766 +  apply (drule_tac x=na in spec, arith)
   4.767 + prefer 2 apply (blast dest: lemma_additivity3)
   4.768 +apply (frule lemma_additivity4_psize_eq)
   4.769 +apply (assumption+)
   4.770 +apply (rule partition [THEN iffD2])
   4.771 +apply (frule partition [THEN iffD1])
   4.772 +apply (auto intro: partition_lt_gen)
   4.773 +apply (drule_tac n = n in partition_lt_gen)
   4.774 +apply (assumption, arith, blast)
   4.775 +apply (drule partition_lt_cancel, auto)
   4.776 +done
   4.777 +
   4.778 +lemma fine_left1:
   4.779 +     "[| a \<le> D n; tpart (a, b) (D, p); gauge (%x. a \<le> x & x \<le> D n) g;
   4.780 +         fine (%x. if x < D n then min (g x) ((D n - x)/ 2)
   4.781 +                 else if x = D n then min (g (D n)) (ga (D n))
   4.782 +                      else min (ga x) ((x - D n)/ 2)) (D, p) |]
   4.783 +      ==> fine g
   4.784 +           (%x. if D x < D n then D(x) else D n,
   4.785 +            %x. if D x < D n then p(x) else D n)"
   4.786 +apply (auto simp add: fine_def tpart_def gauge_def)
   4.787 +apply (frule_tac [!] na=na in lemma_psize_left_less_psize2)
   4.788 +apply (drule_tac [!] x = na in spec, auto)
   4.789 +apply (drule_tac [!] x = na in spec, auto)
   4.790 +apply (auto dest: lemma_additivity3a simp add: split_if_asm)
   4.791 +done
   4.792 +
   4.793 +lemma tpart_right1:
   4.794 +     "[| a \<le> D n; tpart (a, b) (D, p) |]
   4.795 +      ==> tpart(D n, b) (%x. D(x + n),%x. p(x + n))"
   4.796 +apply (simp add: tpart_def partition_def, safe)
   4.797 +apply (rule_tac x = "N - n" in exI, auto)
   4.798 +apply (rotate_tac 2)
   4.799 +apply (drule_tac x = "na + n" in spec)
   4.800 +apply (rotate_tac [2] 3)
   4.801 +apply (drule_tac [2] x = "na + n" in spec, arith+)
   4.802 +done
   4.803 +
   4.804 +lemma fine_right1:
   4.805 +     "[| a \<le> D n; tpart (a, b) (D, p); gauge (%x. D n \<le> x & x \<le> b) ga;
   4.806 +         fine (%x. if x < D n then min (g x) ((D n - x)/ 2)
   4.807 +                 else if x = D n then min (g (D n)) (ga (D n))
   4.808 +                      else min (ga x) ((x - D n)/ 2)) (D, p) |]
   4.809 +      ==> fine ga (%x. D(x + n),%x. p(x + n))"
   4.810 +apply (auto simp add: fine_def gauge_def)
   4.811 +apply (drule_tac x = "na + n" in spec)
   4.812 +apply (frule_tac n = n in tpart_partition [THEN better_lemma_psize_right_eq], auto, arith)
   4.813 +apply (simp add: tpart_def, safe)
   4.814 +apply (subgoal_tac "D n \<le> p (na + n) ")
   4.815 +apply (drule_tac y = "p (na + n) " in real_le_imp_less_or_eq)
   4.816 +apply safe
   4.817 +apply (simp split: split_if_asm, simp)
   4.818 +apply (drule less_le_trans, assumption)
   4.819 +apply (rotate_tac 5)
   4.820 +apply (drule_tac x = "na + n" in spec, safe)
   4.821 +apply (rule_tac y="D (na + n)" in order_trans)
   4.822 +apply (case_tac "na = 0", auto)
   4.823 +apply (erule partition_lt_gen [THEN order_less_imp_le], arith+)
   4.824 +done
   4.825 +
   4.826 +lemma rsum_add: "rsum (D, p) (%x. f x + g x) =  rsum (D, p) f + rsum(D, p) g"
   4.827 +by (simp add: rsum_def sumr_add left_distrib)
   4.828 +
   4.829 +(* Bartle/Sherbert: Theorem 10.1.5 p. 278 *)
   4.830 +lemma Integral_add_fun:
   4.831 +    "[| a \<le> b; Integral(a,b) f k1; Integral(a,b) g k2 |]
   4.832 +     ==> Integral(a,b) (%x. f x + g x) (k1 + k2)"
   4.833 +apply (simp add: Integral_def, auto)
   4.834 +apply ((drule_tac x = "e/2" in spec)+)
   4.835 +apply auto
   4.836 +apply (drule gauge_min, assumption)
   4.837 +apply (rule_tac x = " (%x. if ga x < gaa x then ga x else gaa x) " in exI)
   4.838 +apply auto
   4.839 +apply (drule fine_min)
   4.840 +apply ((drule spec)+, auto)
   4.841 +apply (drule_tac a = "\<bar>rsum (D, p) f - k1\<bar> * 2" and c = "\<bar>rsum (D, p) g - k2\<bar> * 2" in add_strict_mono, assumption)
   4.842 +apply (auto simp only: rsum_add left_distrib [symmetric]
   4.843 +                mult_2_right [symmetric] real_mult_less_iff1, arith)
   4.844 +done
   4.845 +
   4.846 +lemma partition_lt_gen2:
   4.847 +     "[| partition(a,b) D; r < psize D |] ==> 0 < D (Suc r) - D r"
   4.848 +by (auto simp add: partition)
   4.849 +
   4.850 +lemma lemma_Integral_le:
   4.851 +     "[| \<forall>x. a \<le> x & x \<le> b --> f x \<le> g x;
   4.852 +         tpart(a,b) (D,p)
   4.853 +      |] ==> \<forall>n. n \<le> psize D --> f (p n) \<le> g (p n)"
   4.854 +apply (simp add: tpart_def)
   4.855 +apply (auto, frule partition [THEN iffD1], auto)
   4.856 +apply (drule_tac x = "p n" in spec, auto)
   4.857 +apply (case_tac "n = 0", simp)
   4.858 +apply (rule partition_lt_gen [THEN order_less_le_trans, THEN order_less_imp_le], auto)
   4.859 +apply (drule le_imp_less_or_eq, auto)
   4.860 +apply (drule_tac [2] x = "psize D" in spec, auto)
   4.861 +apply (drule_tac r = "Suc n" in partition_ub)
   4.862 +apply (drule_tac x = n in spec, auto)
   4.863 +done
   4.864 +
   4.865 +lemma lemma_Integral_rsum_le:
   4.866 +     "[| \<forall>x. a \<le> x & x \<le> b --> f x \<le> g x;
   4.867 +         tpart(a,b) (D,p)
   4.868 +      |] ==> rsum(D,p) f \<le> rsum(D,p) g"
   4.869 +apply (simp add: rsum_def)
   4.870 +apply (auto intro!: sumr_le2 dest: tpart_partition [THEN partition_lt_gen2]
   4.871 +               dest!: lemma_Integral_le)
   4.872 +done
   4.873 +
   4.874 +lemma Integral_le:
   4.875 +    "[| a \<le> b;
   4.876 +        \<forall>x. a \<le> x & x \<le> b --> f(x) \<le> g(x);
   4.877 +        Integral(a,b) f k1; Integral(a,b) g k2
   4.878 +     |] ==> k1 \<le> k2"
   4.879 +apply (simp add: Integral_def)
   4.880 +apply (rotate_tac 2)
   4.881 +apply (drule_tac x = "\<bar>k1 - k2\<bar> /2" in spec)
   4.882 +apply (drule_tac x = "\<bar>k1 - k2\<bar> /2" in spec)
   4.883 +apply auto
   4.884 +apply (drule gauge_min, assumption)
   4.885 +apply (drule_tac g = "%x. if ga x < gaa x then ga x else gaa x" 
   4.886 +       in partition_exists, assumption, auto)
   4.887 +apply (drule fine_min)
   4.888 +apply (drule_tac x = D in spec, drule_tac x = D in spec)
   4.889 +apply (drule_tac x = p in spec, drule_tac x = p in spec, auto)
   4.890 +apply (frule lemma_Integral_rsum_le, assumption)
   4.891 +apply (subgoal_tac "\<bar>(rsum (D,p) f - k1) - (rsum (D,p) g - k2)\<bar> < \<bar>k1 - k2\<bar> ")
   4.892 +apply arith
   4.893 +apply (drule add_strict_mono, assumption)
   4.894 +apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
   4.895 +                       real_mult_less_iff1, arith)
   4.896 +done
   4.897 +
   4.898 +lemma Integral_imp_Cauchy:
   4.899 +     "(\<exists>k. Integral(a,b) f k) ==>
   4.900 +      (\<forall>e. 0 < e -->
   4.901 +               (\<exists>g. gauge (%x. a \<le> x & x \<le> b) g &
   4.902 +                       (\<forall>D1 D2 p1 p2.
   4.903 +                            tpart(a,b) (D1, p1) & fine g (D1,p1) &
   4.904 +                            tpart(a,b) (D2, p2) & fine g (D2,p2) -->
   4.905 +                            \<bar>rsum(D1,p1) f - rsum(D2,p2) f\<bar> < e)))"
   4.906 +apply (simp add: Integral_def, auto)
   4.907 +apply (drule_tac x = "e/2" in spec, auto)
   4.908 +apply (rule exI, auto)
   4.909 +apply (frule_tac x = D1 in spec)
   4.910 +apply (frule_tac x = D2 in spec)
   4.911 +apply ((drule spec)+, auto)
   4.912 +apply (erule_tac V = "0 < e" in thin_rl)
   4.913 +apply (drule add_strict_mono, assumption)
   4.914 +apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
   4.915 +                       real_mult_less_iff1, arith)
   4.916 +done
   4.917 +
   4.918 +lemma Cauchy_iff2:
   4.919 +     "Cauchy X =
   4.920 +      (\<forall>j. (\<exists>M. \<forall>m n. M \<le> m & M \<le> n -->
   4.921 +               \<bar>X m + - X n\<bar> < inverse(real (Suc j))))"
   4.922 +apply (simp add: Cauchy_def, auto)
   4.923 +apply (drule reals_Archimedean, safe)
   4.924 +apply (drule_tac x = n in spec, auto)
   4.925 +apply (rule_tac x = M in exI, auto)
   4.926 +apply (drule_tac x = m in spec)
   4.927 +apply (drule_tac x = na in spec, auto)
   4.928 +done
   4.929 +
   4.930 +lemma partition_exists2:
   4.931 +     "[| a \<le> b; \<forall>n. gauge (%x. a \<le> x & x \<le> b) (fa n) |]
   4.932 +      ==> \<forall>n. \<exists>D p. tpart (a, b) (D, p) & fine (fa n) (D, p)"
   4.933 +apply safe
   4.934 +apply (rule partition_exists, auto)
   4.935 +done
   4.936 +
   4.937 +lemma monotonic_anti_derivative:
   4.938 +     "[| a \<le> b; \<forall>c. a \<le> c & c \<le> b --> f' c \<le> g' c;
   4.939 +         \<forall>x. DERIV f x :> f' x; \<forall>x. DERIV g x :> g' x |]
   4.940 +      ==> f b - f a \<le> g b - g a"
   4.941 +apply (rule Integral_le, assumption)
   4.942 +apply (rule_tac [2] FTC1)
   4.943 +apply (rule_tac [4] FTC1, auto)
   4.944 +done
   4.945 +
   4.946 +end
     5.1 --- a/src/HOL/IsaMakefile	Fri Jul 30 10:44:42 2004 +0200
     5.2 +++ b/src/HOL/IsaMakefile	Fri Jul 30 18:37:58 2004 +0200
     5.3 @@ -151,7 +151,7 @@
     5.4    Hyperreal/HTranscendental.thy Hyperreal/HyperArith.thy\
     5.5    Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy\
     5.6    Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\
     5.7 -  Hyperreal/Lim.thy Hyperreal/Log.thy\
     5.8 +  Hyperreal/Integration.thy Hyperreal/Lim.thy Hyperreal/Log.thy\
     5.9    Hyperreal/MacLaurin.thy Hyperreal/NatStar.thy\
    5.10    Hyperreal/NSA.thy Hyperreal/NthRoot.thy Hyperreal/Poly.thy\
    5.11    Hyperreal/SEQ.thy Hyperreal/Series.thy Hyperreal/Star.thy \
    5.12 @@ -168,8 +168,7 @@
    5.13  
    5.14  $(LOG)/HOL-Complex-ex.gz: $(OUT)/HOL-Complex Library/Primes.thy \
    5.15    Complex/ex/ROOT.ML Complex/ex/document/root.tex \
    5.16 -  Complex/ex/BinEx.thy \
    5.17 -  Complex/ex/NSPrimes.ML Complex/ex/NSPrimes.thy\
    5.18 +  Complex/ex/BinEx.thy Complex/ex/NSPrimes.thy\
    5.19    Complex/ex/Sqrt.thy Complex/ex/Sqrt_Script.thy
    5.20  	@cd Complex; $(ISATOOL) usedir $(OUT)/HOL-Complex ex
    5.21  
     6.1 --- a/src/HOL/OrderedGroup.thy	Fri Jul 30 10:44:42 2004 +0200
     6.2 +++ b/src/HOL/OrderedGroup.thy	Fri Jul 30 18:37:58 2004 +0200
     6.3 @@ -728,6 +728,15 @@
     6.4  apply (rule order_trans[of _ 0])
     6.5  by auto
     6.6  
     6.7 +lemma abs_minus_commute: 
     6.8 +  fixes a :: "'a::lordered_ab_group_abs"
     6.9 +  shows "abs (a-b) = abs(b-a)"
    6.10 +proof -
    6.11 +  have "abs (a-b) = abs (- (a-b))" by (simp only: abs_minus_cancel)
    6.12 +  also have "... = abs(b-a)" by simp
    6.13 +  finally show ?thesis .
    6.14 +qed
    6.15 +
    6.16  lemma zero_le_iff_zero_nprt: "(0 \<le> a) = (nprt a = 0)"
    6.17  by (simp add: le_def_meet nprt_def meet_comm)
    6.18