--- a/src/HOL/Complex/ex/NSPrimes.ML Fri Jul 30 10:44:42 2004 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,491 +0,0 @@
-(* Title : NSPrimes.ML
- Author : Jacques D. Fleuriot
- Copyright : 2002 University of Edinburgh
- Description : The nonstandard primes as an extension of
- the prime numbers
-*)
-
-(*--------------------------------------------------------------*)
-(* A "choice" theorem for ultrafilters cf. almost everywhere *)
-(* quantification *)
-(*--------------------------------------------------------------*)
-
-Goal "{n. EX m. Q n m} : FreeUltrafilterNat \
-\ ==> EX f. {n. Q n (f n)} : FreeUltrafilterNat";
-by (res_inst_tac [("x","%n. (@x. Q n x)")] exI 1);
-by (Ultra_tac 1 THEN rtac someI 1 THEN Auto_tac);
-qed "UF_choice";
-
-Goal "({n. P n} : FreeUltrafilterNat --> {n. Q n} : FreeUltrafilterNat) = \
-\ ({n. P n --> Q n} : FreeUltrafilterNat)";
-by Auto_tac;
-by (ALLGOALS(Ultra_tac));
-qed "UF_if";
-
-Goal "({n. P n} : FreeUltrafilterNat & {n. Q n} : FreeUltrafilterNat) = \
-\ ({n. P n & Q n} : FreeUltrafilterNat)";
-by Auto_tac;
-by (ALLGOALS(Ultra_tac));
-qed "UF_conj";
-
-Goal "(ALL f. {n. Q n (f n)} : FreeUltrafilterNat) = \
-\ ({n. ALL m. Q n m} : FreeUltrafilterNat)";
-by Auto_tac;
-by (Ultra_tac 2);
-by (rtac ccontr 1);
-by (rtac swap 1 THEN assume_tac 2);
-by (simp_tac (simpset() addsimps [FreeUltrafilterNat_Compl_iff1,
- CLAIM "-{n. Q n} = {n. ~ Q n}"]) 1);
-by (rtac UF_choice 1);
-by (Ultra_tac 1 THEN Auto_tac);
-qed "UF_choice_ccontr";
-
-Goal "ALL M. EX N. 0 < N & (ALL m. 0 < m & (m::nat) <= M --> m dvd N)";
-by (rtac allI 1);
-by (induct_tac "M" 1);
-by Auto_tac;
-by (res_inst_tac [("x","N * (Suc n)")] exI 1);
-by (Step_tac 1 THEN Force_tac 1);
-by (dtac le_imp_less_or_eq 1 THEN etac disjE 1);
-by (force_tac (claset() addSIs [dvd_mult2],simpset()) 1);
-by (force_tac (claset() addSIs [dvd_mult],simpset()) 1);
-qed "dvd_by_all";
-
-bind_thm ("dvd_by_all2",dvd_by_all RS spec);
-
-Goal "(EX (x::hypnat). P x) = (EX f. P (Abs_hypnat(hypnatrel `` {f})))";
-by Auto_tac;
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by Auto_tac;
-qed "lemma_hypnat_P_EX";
-
-Goal "(ALL (x::hypnat). P x) = (ALL f. P (Abs_hypnat(hypnatrel `` {f})))";
-by Auto_tac;
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by Auto_tac;
-qed "lemma_hypnat_P_ALL";
-
-Goalw [hdvd_def]
- "(Abs_hypnat(hypnatrel``{%n. X n}) hdvd \
-\ Abs_hypnat(hypnatrel``{%n. Y n})) = \
-\ ({n. X n dvd Y n} : FreeUltrafilterNat)";
-by (Auto_tac THEN Ultra_tac 1);
-qed "hdvd";
-
-Goal "(hypnat_of_nat n <= 0) = (n = 0)";
-by (stac (hypnat_of_nat_zero RS sym) 1);
-by Auto_tac;
-qed "hypnat_of_nat_le_zero_iff";
-Addsimps [hypnat_of_nat_le_zero_iff];
-
-
-(* Goldblatt: Exercise 5.11(2) - p. 57 *)
-Goal "ALL M. EX N. 0 < N & (ALL m. 0 < m & (m::hypnat) <= M --> m hdvd N)";
-by (Step_tac 1);
-by (res_inst_tac [("z","M")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [lemma_hypnat_P_EX,
- lemma_hypnat_P_ALL,hypnat_zero_def,hypnat_le,hypnat_less,hdvd]));
-by (cut_facts_tac [dvd_by_all] 1);
-by (dtac (CLAIM "(ALL (M::nat). EX N. 0 < N & (ALL m. 0 < m & m <= M \
-\ --> m dvd N)) \
-\ ==> ALL (n::nat). EX N. 0 < N & (ALL m. 0 < (m::nat) & m <= (x n) \
-\ --> m dvd N)") 1);
-by (dtac choice 1);
-by (Step_tac 1);
-by (res_inst_tac [("x","f")] exI 1);
-by Auto_tac;
-by (ALLGOALS(Ultra_tac));
-by Auto_tac;
-qed "hdvd_by_all";
-
-bind_thm ("hdvd_by_all2",hdvd_by_all RS spec);
-
-(* Goldblatt: Exercise 5.11(2) - p. 57 *)
-Goal "EX (N::hypnat). 0 < N & (ALL n : - {0::nat}. hypnat_of_nat(n) hdvd N)";
-by (cut_facts_tac [hdvd_by_all] 1);
-by (dres_inst_tac [("x","whn")] spec 1);
-by Auto_tac;
-by (rtac exI 1 THEN Auto_tac);
-by (dres_inst_tac [("x","hypnat_of_nat n")] spec 1);
-by (auto_tac (claset(),
- simpset() addsimps [linorder_not_less, hypnat_of_nat_zero_iff]));
-qed "hypnat_dvd_all_hypnat_of_nat";
-
-
-(*--------------------------------------------------------------*)
-(* the nonstandard extension of the set prime numbers consists *)
-(* of precisely those hypernaturals > 1 that have no nontrivial *)
-(* factors *)
-(*--------------------------------------------------------------*)
-
-(* Goldblatt: Exercise 5.11(3a) - p 57 *)
-Goalw [starprime_def,thm "prime_def"]
- "starprime = {p. 1 < p & (ALL m. m hdvd p --> m = 1 | m = p)}";
-by (auto_tac (claset(),simpset() addsimps
- [CLAIM "{p. Q(p) & R(p)} = {p. Q(p)} Int {p. R(p)}",NatStar_Int]));
-by (ALLGOALS(res_inst_tac [("z","x")] eq_Abs_hypnat));
-by (res_inst_tac [("z","m")] eq_Abs_hypnat 2);
-by (auto_tac (claset(),simpset() addsimps [hdvd,hypnat_one_def,hypnat_less,
- lemma_hypnat_P_ALL,starsetNat_def]));
-by (dtac bspec 1 THEN dtac bspec 2 THEN Auto_tac);
-by (Ultra_tac 1 THEN Ultra_tac 1);
-by (rtac ccontr 1);
-by (dtac FreeUltrafilterNat_Compl_mem 1);
-by (auto_tac (claset(),simpset() addsimps [CLAIM "- {p. Q p} = {p. ~ Q p}"]));
-by (dtac UF_choice 1 THEN Auto_tac);
-by (dres_inst_tac [("x","f")] spec 1 THEN Auto_tac);
-by (ALLGOALS(Ultra_tac));
-qed "starprime";
-
-Goalw [thm "prime_def"] "2 : prime";
-by Auto_tac;
-by (ftac dvd_imp_le 1);
-by (auto_tac (claset() addDs [dvd_0_left],simpset() addsimps
- [ARITH_PROVE "(m <= (2::nat)) = (m = 0 | m = 1 | m = 2)"]));
-qed "prime_two";
-Addsimps [prime_two];
-
-(* proof uses course-of-value induction *)
-Goal "Suc 0 < n --> (EX k : prime. k dvd n)";
-by (res_inst_tac [("n","n")] nat_less_induct 1);
-by Auto_tac;
-by (case_tac "n : prime" 1);
-by (res_inst_tac [("x","n")] bexI 1 THEN Auto_tac);
-by (dtac (conjI RS (thm "not_prime_ex_mk")) 1 THEN Auto_tac);
-by (dres_inst_tac [("x","m")] spec 1 THEN Auto_tac);
-by (res_inst_tac [("x","ka")] bexI 1);
-by (auto_tac (claset() addIs [dvd_mult2],simpset()));
-qed_spec_mp "prime_factor_exists";
-
-(* Goldblatt Exercise 5.11(3b) - p 57 *)
-Goal "1 < n ==> (EX k : starprime. k hdvd n)";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [hypnat_one_def,
- hypnat_less,starprime_def,lemma_hypnat_P_EX,lemma_hypnat_P_ALL,
- hdvd,starsetNat_def,CLAIM "(ALL X: S. P X) = (ALL X. X : S --> P X)",
- UF_if]));
-by (res_inst_tac [("x","%n. @y. y : prime & y dvd x n")] exI 1);
-by Auto_tac;
-by (ALLGOALS (Ultra_tac));
-by (dtac sym 1 THEN Asm_simp_tac 1);
-by (ALLGOALS(rtac someI2_ex));
-by (auto_tac (claset() addSDs [prime_factor_exists],simpset()));
-qed_spec_mp "hyperprime_factor_exists";
-
-(* behaves as expected! *)
-Goal "( *sNat* insert x A) = insert (hypnat_of_nat x) ( *sNat* A)";
-by (auto_tac (claset(),simpset() addsimps [starsetNat_def,
- hypnat_of_nat_eq]));
-by (ALLGOALS(res_inst_tac [("z","xa")] eq_Abs_hypnat));
-by Auto_tac;
-by (TRYALL(dtac bspec));
-by Auto_tac;
-by (ALLGOALS(Ultra_tac));
-qed "NatStar_insert";
-
-(* Goldblatt Exercise 3.10(1) - p. 29 *)
-Goal "finite A ==> *sNat* A = hypnat_of_nat ` A";
-by (res_inst_tac [("P","%x. *sNat* x = hypnat_of_nat ` x")] finite_induct 1);
-by (auto_tac (claset(),simpset() addsimps [NatStar_insert]));
-qed "NatStar_hypnat_of_nat";
-
-(* proved elsewhere? *)
-Goal "{x} ~: FreeUltrafilterNat";
-by (auto_tac (claset() addSIs [FreeUltrafilterNat_finite],simpset()));
-qed "FreeUltrafilterNat_singleton_not_mem";
-Addsimps [FreeUltrafilterNat_singleton_not_mem];
-
-(*-------------------------------------------------------------------------------*)
-(* Another characterization of infinite set of natural numbers *)
-(*-------------------------------------------------------------------------------*)
-
-Goal "finite N ==> EX n. (ALL i:N. i<(n::nat))";
-by (eres_inst_tac [("F","N")] finite_induct 1);
-by Auto_tac;
-by (res_inst_tac [("x","Suc n + x")] exI 1);
-by Auto_tac;
-qed "finite_nat_set_bounded";
-
-Goal "finite N = (EX n. (ALL i:N. i<(n::nat)))";
-by (blast_tac (claset() addIs [finite_nat_set_bounded,
- bounded_nat_set_is_finite]) 1);
-qed "finite_nat_set_bounded_iff";
-
-Goal "(~ finite N) = (ALL n. EX i:N. n <= (i::nat))";
-by (auto_tac (claset(),simpset() addsimps [finite_nat_set_bounded_iff,
- le_def]));
-qed "not_finite_nat_set_iff";
-
-Goal "(ALL i:N. i<=(n::nat)) ==> finite N";
-by (rtac finite_subset 1);
- by (rtac finite_atMost 2);
-by Auto_tac;
-qed "bounded_nat_set_is_finite2";
-
-Goal "finite N ==> EX n. (ALL i:N. i<=(n::nat))";
-by (eres_inst_tac [("F","N")] finite_induct 1);
-by Auto_tac;
-by (res_inst_tac [("x","n + x")] exI 1);
-by Auto_tac;
-qed "finite_nat_set_bounded2";
-
-Goal "finite N = (EX n. (ALL i:N. i<=(n::nat)))";
-by (blast_tac (claset() addIs [finite_nat_set_bounded2,
- bounded_nat_set_is_finite2]) 1);
-qed "finite_nat_set_bounded_iff2";
-
-Goal "(~ finite N) = (ALL n. EX i:N. n < (i::nat))";
-by (auto_tac (claset(),simpset() addsimps [finite_nat_set_bounded_iff2,
- le_def]));
-qed "not_finite_nat_set_iff2";
-
-(*-------------------------------------------------------------------------------*)
-(* An injective function cannot define an embedded natural number *)
-(*-------------------------------------------------------------------------------*)
-
-Goal "ALL m n. m ~= n --> f n ~= f m \
-\ ==> {n. f n = N} = {} | (EX m. {n. f n = N} = {m})";
-by Auto_tac;
-by (dres_inst_tac [("x","x")] spec 1 THEN Auto_tac);
-by (subgoal_tac "ALL n. (f n = f x) = (x = n)" 1);
-by Auto_tac;
-qed "lemma_infinite_set_singleton";
-
-Goal "inj f ==> Abs_hypnat(hypnatrel `` {f}) ~: Nats";
-by (auto_tac (claset(), simpset() addsimps [SHNat_eq,hypnat_of_nat_eq]));
-by (subgoal_tac "ALL m n. m ~= n --> f n ~= f m" 1);
-by Auto_tac;
-by (dtac injD 2);
-by (assume_tac 2 THEN Force_tac 2);
-by (dres_inst_tac[("N","N")] lemma_infinite_set_singleton 1);
-by Auto_tac;
-qed "inj_fun_not_hypnat_in_SHNat";
-
-Goalw [starsetNat_def]
- "range f <= A ==> Abs_hypnat(hypnatrel `` {f}) : *sNat* A";
-by Auto_tac;
-by (Ultra_tac 1);
-by (dres_inst_tac [("c","f x")] subsetD 1);
-by (rtac rangeI 1);
-by Auto_tac;
-qed "range_subset_mem_starsetNat";
-
-(*--------------------------------------------------------------------------------*)
-(* Gleason Proposition 11-5.5. pg 149, pg 155 (ex. 3) and pg. 360 *)
-(* Let E be a nonvoid ordered set with no maximal elements (note: effectively an *)
-(* infinite set if we take E = N (Nats)). Then there exists an order-preserving *)
-(* injection from N to E. Of course, (as some doofus will undoubtedly point out! *)
-(* :-)) can use notion of least element in proof (i.e. no need for choice) if *)
-(* dealing with nats as we have well-ordering property *)
-(*--------------------------------------------------------------------------------*)
-
-Goal "E ~= {} ==> EX x. EX X : (Pow E - {{}}). x: X";
-by Auto_tac;
-val lemmaPow3 = result();
-
-Goalw [choicefun_def] "E ~= {} ==> choicefun E : E";
-by (rtac (lemmaPow3 RS someI2_ex) 1);
-by Auto_tac;
-qed "choicefun_mem_set";
-Addsimps [choicefun_mem_set];
-
-Goal "[| E ~={}; ALL x. EX y: E. x < y |] ==> injf_max n E : E";
-by (induct_tac "n" 1);
-by (Force_tac 1);
-by (simp_tac (simpset() addsimps [choicefun_def]) 1);
-by (rtac (lemmaPow3 RS someI2_ex) 1);
-by Auto_tac;
-qed "injf_max_mem_set";
-
-Goal "ALL x. EX y: E. x < y ==> injf_max n E < injf_max (Suc n) E";
-by (simp_tac (simpset() addsimps [choicefun_def]) 1);
-by (rtac (lemmaPow3 RS someI2_ex) 1);
-by Auto_tac;
-qed "injf_max_order_preserving";
-
-Goal "ALL x. EX y: E. x < y \
-\ ==> ALL n m. m < n --> injf_max m E < injf_max n E";
-by (rtac allI 1);
-by (induct_tac "n" 1);
-by Auto_tac;
-by (simp_tac (simpset() addsimps [choicefun_def]) 1);
-by (rtac (lemmaPow3 RS someI2_ex) 1);
-by Auto_tac;
-by (dtac (CLAIM "m < Suc n ==> m = n | m < n") 1);
-by Auto_tac;
-by (dres_inst_tac [("x","m")] spec 1);
-by Auto_tac;
-by (dtac subsetD 1 THEN Auto_tac);
-by (dres_inst_tac [("x","injf_max m E")] order_less_trans 1);
-by Auto_tac;
-qed "injf_max_order_preserving2";
-
-Goal "ALL x. EX y: E. x < y ==> inj (%n. injf_max n E)";
-by (rtac injI 1);
-by (rtac ccontr 1);
-by Auto_tac;
-by (dtac injf_max_order_preserving2 1);
-by (cut_inst_tac [("m","x"),("n","y")] less_linear 1);
-by Auto_tac;
-by (auto_tac (claset() addSDs [spec],simpset()));
-qed "inj_injf_max";
-
-Goal "[| (E::('a::{order} set)) ~= {}; ALL x. EX y: E. x < y |] \
-\ ==> EX f. range f <= E & inj (f::nat => 'a) & (ALL m. f m < f(Suc m))";
-by (res_inst_tac [("x","%n. injf_max n E")] exI 1);
-by (Step_tac 1);
-by (rtac injf_max_mem_set 1);
-by (rtac inj_injf_max 3);
-by (rtac injf_max_order_preserving 4);
-by Auto_tac;
-qed "infinite_set_has_order_preserving_inj";
-
-(*-------------------------------------------------------------------------------*)
-(* Only need fact that we can have an injective function from N to A for proof *)
-(*-------------------------------------------------------------------------------*)
-
-Goal "~ finite A ==> hypnat_of_nat ` A < ( *sNat* A)";
-by Auto_tac;
-by (rtac subsetD 1);
-by (rtac NatStar_hypreal_of_real_image_subset 1);
-by Auto_tac;
-by (subgoal_tac "A ~= {}" 1);
-by (Force_tac 2);
-by (dtac infinite_set_has_order_preserving_inj 1);
-by (etac (not_finite_nat_set_iff2 RS iffD1) 1);
-by Auto_tac;
-by (dtac inj_fun_not_hypnat_in_SHNat 1);
-by (dtac range_subset_mem_starsetNat 1);
-by (auto_tac (claset(),simpset() addsimps [SHNat_eq]));
-qed "hypnat_infinite_has_nonstandard";
-
-Goal "*sNat* A = hypnat_of_nat ` A ==> finite A";
-by (rtac ccontr 1);
-by (auto_tac (claset() addDs [hypnat_infinite_has_nonstandard],
- simpset()));
-qed "starsetNat_eq_hypnat_of_nat_image_finite";
-
-Goal "( *sNat* A = hypnat_of_nat ` A) = (finite A)";
-by (blast_tac (claset() addSIs [starsetNat_eq_hypnat_of_nat_image_finite,
- NatStar_hypnat_of_nat]) 1);
-qed "finite_starsetNat_iff";
-
-Goal "(~ finite A) = (hypnat_of_nat ` A < *sNat* A)";
-by (rtac iffI 1);
-by (blast_tac (claset() addSIs [hypnat_infinite_has_nonstandard]) 1);
-by (auto_tac (claset(),simpset() addsimps [finite_starsetNat_iff RS sym]));
-qed "hypnat_infinite_has_nonstandard_iff";
-
-
-(*-------------------------------------------------------------------------------*)
-(* Existence of infinitely many primes: a nonstandard proof *)
-(*-------------------------------------------------------------------------------*)
-
-Goal "~ (ALL n:- {0}. hypnat_of_nat n hdvd 1)";
-by Auto_tac;
-by (res_inst_tac [("x","2")] bexI 1);
-by (auto_tac (claset(),simpset() addsimps [hypnat_of_nat_eq,
- hypnat_one_def,hdvd,dvd_def]));
-val lemma_not_dvd_hypnat_one = result();
-Addsimps [lemma_not_dvd_hypnat_one];
-
-Goal "EX n:- {0}. ~ hypnat_of_nat n hdvd 1";
-by (cut_facts_tac [lemma_not_dvd_hypnat_one] 1);
-by (auto_tac (claset(),simpset() delsimps [lemma_not_dvd_hypnat_one]));
-val lemma_not_dvd_hypnat_one2 = result();
-Addsimps [lemma_not_dvd_hypnat_one2];
-
-(* not needed here *)
-Goalw [hypnat_zero_def,hypnat_one_def]
- "[| 0 < (N::hypnat); N ~= 1 |] ==> 1 < N";
-by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [hypnat_less]));
-by (Ultra_tac 1);
-qed "hypnat_gt_zero_gt_one";
-
-Goalw [hypnat_zero_def,hypnat_one_def]
- "0 < N ==> 1 < (N::hypnat) + 1";
-by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [hypnat_less,hypnat_add]));
-qed "hypnat_add_one_gt_one";
-
-Goal "0 ~: prime";
-by (Step_tac 1);
-by (dtac (thm "prime_g_zero") 1);
-by Auto_tac;
-qed "zero_not_prime";
-Addsimps [zero_not_prime];
-
-Goal "hypnat_of_nat 0 ~: starprime";
-by (auto_tac (claset() addSIs [bexI],
- simpset() addsimps [starprime_def,starsetNat_def,hypnat_of_nat_eq]));
-qed "hypnat_of_nat_zero_not_prime";
-Addsimps [hypnat_of_nat_zero_not_prime];
-
-Goalw [starprime_def,starsetNat_def,hypnat_zero_def]
- "0 ~: starprime";
-by (auto_tac (claset() addSIs [bexI],simpset()));
-qed "hypnat_zero_not_prime";
-Addsimps [hypnat_zero_not_prime];
-
-Goal "1 ~: prime";
-by (Step_tac 1);
-by (dtac (thm "prime_g_one") 1);
-by Auto_tac;
-qed "one_not_prime";
-Addsimps [one_not_prime];
-
-Goal "Suc 0 ~: prime";
-by (Step_tac 1);
-by (dtac (thm "prime_g_one") 1);
-by Auto_tac;
-qed "one_not_prime2";
-Addsimps [one_not_prime2];
-
-Goal "hypnat_of_nat 1 ~: starprime";
-by (auto_tac (claset() addSIs [bexI],
- simpset() addsimps [starprime_def,starsetNat_def,hypnat_of_nat_eq]));
-qed "hypnat_of_nat_one_not_prime";
-Addsimps [hypnat_of_nat_one_not_prime];
-
-Goalw [starprime_def,starsetNat_def,hypnat_one_def]
- "1 ~: starprime";
-by (auto_tac (claset() addSIs [bexI],simpset()));
-qed "hypnat_one_not_prime";
-Addsimps [hypnat_one_not_prime];
-
-Goal "[| k hdvd m; k hdvd n |] ==> k hdvd (m - n)";
-by (res_inst_tac [("z","k")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [hdvd,hypnat_minus]));
-by (Ultra_tac 1);
-by (blast_tac (claset() addIs [dvd_diff]) 1);
-qed "hdvd_diff";
-
-Goalw [dvd_def] "x dvd (1::nat) ==> x = 1";
-by Auto_tac;
-qed "dvd_one_eq_one";
-
-Goalw [hypnat_one_def] "x hdvd 1 ==> x = 1";
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [hdvd]));
-qed "hdvd_one_eq_one";
-
-Goal "~ finite prime";
-by (rtac (hypnat_infinite_has_nonstandard_iff RS iffD2) 1);
-by (cut_facts_tac [hypnat_dvd_all_hypnat_of_nat] 1);
-by (etac exE 1);
-by (etac conjE 1);
-by (subgoal_tac "1 < N + 1" 1);
-by (blast_tac (claset() addIs [hypnat_add_one_gt_one]) 2);
-by (dtac hyperprime_factor_exists 1);
-by (auto_tac (claset() addIs [NatStar_mem],simpset()));
-by (subgoal_tac "k ~: hypnat_of_nat ` prime" 1);
-by (force_tac (claset(),simpset() addsimps [starprime_def]) 1);
-by (Step_tac 1);
-by (dres_inst_tac [("x","x")] bspec 1);
-by (rtac ccontr 1 THEN Asm_full_simp_tac 1);
-by (dtac hdvd_diff 1 THEN assume_tac 1);
-by (auto_tac (claset() addDs [hdvd_one_eq_one],simpset()));
-qed "not_finite_prime";
--- a/src/HOL/Complex/ex/NSPrimes.thy Fri Jul 30 10:44:42 2004 +0200
+++ b/src/HOL/Complex/ex/NSPrimes.thy Fri Jul 30 18:37:58 2004 +0200
@@ -1,36 +1,447 @@
(* Title : NSPrimes.thy
Author : Jacques D. Fleuriot
Copyright : 2002 University of Edinburgh
- Description : The nonstandard primes as an extension of
- the prime numbers
-
-These can be used to derive an alternative proof of the infinitude of primes by
-considering a property of nonstandard sets.
+ Conversion to Isar and new proofs by Lawrence C Paulson, 2004
*)
-NSPrimes = Factorization + Complex_Main +
+header{*The Nonstandard Primes as an Extension of the Prime Numbers*}
+
+theory NSPrimes = "~~/src/HOL/NumberTheory/Factorization" + Complex_Main:
-consts
- hdvd :: [hypnat, hypnat] => bool (infixl 50)
-
-defs
- hdvd_def "(M::hypnat) hdvd N ==
- EX X Y. X: Rep_hypnat(M) & Y: Rep_hypnat(N) &
+text{*These can be used to derive an alternative proof of the infinitude of
+primes by considering a property of nonstandard sets.*}
+
+
+constdefs
+ hdvd :: "[hypnat, hypnat] => bool" (infixl "hdvd" 50)
+ "(M::hypnat) hdvd N ==
+ \<exists>X Y. X: Rep_hypnat(M) & Y: Rep_hypnat(N) &
{n::nat. X n dvd Y n} : FreeUltrafilterNat"
constdefs
- starprime :: hypnat set
+ starprime :: "hypnat set"
"starprime == ( *sNat* prime)"
constdefs
- choicefun :: 'a set => 'a
- "choicefun E == (@x. EX X: Pow(E) -{{}}. x : X)"
+ choicefun :: "'a set => 'a"
+ "choicefun E == (@x. \<exists>X \<in> Pow(E) -{{}}. x : X)"
+
+consts injf_max :: "nat => ('a::{order} set) => 'a"
+primrec
+ injf_max_zero: "injf_max 0 E = choicefun E"
+ injf_max_Suc: "injf_max (Suc n) E = choicefun({e. e:E & injf_max n E < e})"
+
+
+text{*A "choice" theorem for ultrafilters, like almost everywhere
+quantification*}
+
+lemma UF_choice: "{n. \<exists>m. Q n m} : FreeUltrafilterNat
+ ==> \<exists>f. {n. Q n (f n)} : FreeUltrafilterNat"
+apply (rule_tac x = "%n. (@x. Q n x) " in exI)
+apply (ultra, rule someI, auto)
+done
+
+lemma UF_if: "({n. P n} : FreeUltrafilterNat --> {n. Q n} : FreeUltrafilterNat) =
+ ({n. P n --> Q n} : FreeUltrafilterNat)"
+apply auto
+apply ultra+
+done
+
+lemma UF_conj: "({n. P n} : FreeUltrafilterNat & {n. Q n} : FreeUltrafilterNat) =
+ ({n. P n & Q n} : FreeUltrafilterNat)"
+apply auto
+apply ultra+
+done
+
+lemma UF_choice_ccontr: "(\<forall>f. {n. Q n (f n)} : FreeUltrafilterNat) =
+ ({n. \<forall>m. Q n m} : FreeUltrafilterNat)"
+apply auto
+ prefer 2 apply ultra
+apply (rule ccontr)
+apply (rule contrapos_np)
+ apply (erule_tac [2] asm_rl)
+apply (simp (no_asm) add: FreeUltrafilterNat_Compl_iff1 Collect_neg_eq [symmetric])
+apply (rule UF_choice, ultra)
+done
+
+lemma dvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::nat) <= M --> m dvd N)"
+apply (rule allI)
+apply (induct_tac "M", auto)
+apply (rule_tac x = "N * (Suc n) " in exI)
+apply (safe, force)
+apply (drule le_imp_less_or_eq, erule disjE)
+apply (force intro!: dvd_mult2)
+apply (force intro!: dvd_mult)
+done
+
+lemmas dvd_by_all2 = dvd_by_all [THEN spec, standard]
+
+lemma lemma_hypnat_P_EX: "(\<exists>(x::hypnat). P x) = (\<exists>f. P (Abs_hypnat(hypnatrel `` {f})))"
+apply auto
+apply (rule_tac z = x in eq_Abs_hypnat, auto)
+done
+
+lemma lemma_hypnat_P_ALL: "(\<forall>(x::hypnat). P x) = (\<forall>f. P (Abs_hypnat(hypnatrel `` {f})))"
+apply auto
+apply (rule_tac z = x in eq_Abs_hypnat, auto)
+done
+
+lemma hdvd:
+ "(Abs_hypnat(hypnatrel``{%n. X n}) hdvd
+ Abs_hypnat(hypnatrel``{%n. Y n})) =
+ ({n. X n dvd Y n} : FreeUltrafilterNat)"
+apply (unfold hdvd_def)
+apply (auto, ultra)
+done
+
+lemma hypnat_of_nat_le_zero_iff: "(hypnat_of_nat n <= 0) = (n = 0)"
+by (subst hypnat_of_nat_zero [symmetric], auto)
+declare hypnat_of_nat_le_zero_iff [simp]
+
+
+(* Goldblatt: Exercise 5.11(2) - p. 57 *)
+lemma hdvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::hypnat) <= M --> m hdvd N)"
+apply safe
+apply (rule_tac z = M in eq_Abs_hypnat)
+apply (auto simp add: lemma_hypnat_P_EX lemma_hypnat_P_ALL
+ hypnat_zero_def hypnat_le hypnat_less hdvd)
+apply (cut_tac dvd_by_all)
+apply (subgoal_tac " \<forall>(n::nat) . \<exists>N. 0 < N & (\<forall>m. 0 < (m::nat) & m <= (x n) --> m dvd N)")
+ prefer 2 apply blast
+apply (erule thin_rl)
+apply (drule choice, safe)
+apply (rule_tac x = f in exI, auto, ultra)
+apply auto
+done
+
+lemmas hdvd_by_all2 = hdvd_by_all [THEN spec, standard]
+
+(* Goldblatt: Exercise 5.11(2) - p. 57 *)
+lemma hypnat_dvd_all_hypnat_of_nat:
+ "\<exists>(N::hypnat). 0 < N & (\<forall>n \<in> -{0::nat}. hypnat_of_nat(n) hdvd N)"
+apply (cut_tac hdvd_by_all)
+apply (drule_tac x = whn in spec, auto)
+apply (rule exI, auto)
+apply (drule_tac x = "hypnat_of_nat n" in spec)
+apply (auto simp add: linorder_not_less hypnat_of_nat_zero_iff)
+done
+
+
+text{*The nonstandard extension of the set prime numbers consists of precisely
+those hypernaturals exceeding 1 that have no nontrivial factors*}
+
+(* Goldblatt: Exercise 5.11(3a) - p 57 *)
+lemma starprime:
+ "starprime = {p. 1 < p & (\<forall>m. m hdvd p --> m = 1 | m = p)}"
+apply (unfold starprime_def prime_def)
+apply (auto simp add: Collect_conj_eq NatStar_Int)
+apply (rule_tac [!] z = x in eq_Abs_hypnat)
+apply (rule_tac [2] z = m in eq_Abs_hypnat)
+apply (auto simp add: hdvd hypnat_one_def hypnat_less lemma_hypnat_P_ALL starsetNat_def)
+apply (drule bspec, drule_tac [2] bspec, auto)
+apply (ultra, ultra)
+apply (rule ccontr)
+apply (drule FreeUltrafilterNat_Compl_mem)
+apply (auto simp add: Collect_neg_eq [symmetric])
+apply (drule UF_choice, auto)
+apply (drule_tac x = f in spec, auto, ultra+)
+done
+
+lemma prime_two: "2 : prime"
+apply (unfold prime_def, auto)
+apply (frule dvd_imp_le)
+apply (auto dest: dvd_0_left)
+(*????arith raises exception Match!!??*)
+apply (case_tac m, simp, arith)
+done
+declare prime_two [simp]
+
+(* proof uses course-of-value induction *)
+lemma prime_factor_exists [rule_format]: "Suc 0 < n --> (\<exists>k \<in> prime. k dvd n)"
+apply (rule_tac n = n in nat_less_induct, auto)
+apply (case_tac "n \<in> prime")
+apply (rule_tac x = n in bexI, auto)
+apply (drule conjI [THEN not_prime_ex_mk], auto)
+apply (drule_tac x = m in spec, auto)
+apply (rule_tac x = ka in bexI)
+apply (auto intro: dvd_mult2)
+done
+
+(* Goldblatt Exercise 5.11(3b) - p 57 *)
+lemma hyperprime_factor_exists [rule_format]: "1 < n ==> (\<exists>k \<in> starprime. k hdvd n)"
+apply (rule_tac z = n in eq_Abs_hypnat)
+apply (auto simp add: hypnat_one_def hypnat_less starprime_def
+ lemma_hypnat_P_EX lemma_hypnat_P_ALL hdvd starsetNat_def Ball_def UF_if)
+apply (rule_tac x = "%n. @y. y \<in> prime & y dvd x n" in exI, auto, ultra)
+apply (drule sym, simp (no_asm_simp))
+ prefer 2 apply ultra
+apply (rule_tac [!] someI2_ex)
+apply (auto dest!: prime_factor_exists)
+done
+
+(* behaves as expected! *)
+lemma NatStar_insert: "( *sNat* insert x A) = insert (hypnat_of_nat x) ( *sNat* A)"
+apply (auto simp add: starsetNat_def hypnat_of_nat_eq)
+apply (rule_tac [!] z = xa in eq_Abs_hypnat, auto)
+apply (drule_tac [!] bspec asm_rl, auto, ultra+)
+done
+
+(* Goldblatt Exercise 3.10(1) - p. 29 *)
+lemma NatStar_hypnat_of_nat: "finite A ==> *sNat* A = hypnat_of_nat ` A"
+apply (rule_tac P = "%x. *sNat* x = hypnat_of_nat ` x" in finite_induct)
+apply (auto simp add: NatStar_insert)
+done
+
+(* proved elsewhere? *)
+lemma FreeUltrafilterNat_singleton_not_mem: "{x} \<notin> FreeUltrafilterNat"
+by (auto intro!: FreeUltrafilterNat_finite)
+declare FreeUltrafilterNat_singleton_not_mem [simp]
+
+
+subsection{*Another characterization of infinite set of natural numbers*}
+
+lemma finite_nat_set_bounded: "finite N ==> \<exists>n. (\<forall>i \<in> N. i<(n::nat))"
+apply (erule_tac F = N in finite_induct, auto)
+apply (rule_tac x = "Suc n + x" in exI, auto)
+done
+
+lemma finite_nat_set_bounded_iff: "finite N = (\<exists>n. (\<forall>i \<in> N. i<(n::nat)))"
+by (blast intro: finite_nat_set_bounded bounded_nat_set_is_finite)
+
+lemma not_finite_nat_set_iff: "(~ finite N) = (\<forall>n. \<exists>i \<in> N. n <= (i::nat))"
+by (auto simp add: finite_nat_set_bounded_iff le_def)
+
+lemma bounded_nat_set_is_finite2: "(\<forall>i \<in> N. i<=(n::nat)) ==> finite N"
+apply (rule finite_subset)
+ apply (rule_tac [2] finite_atMost, auto)
+done
+
+lemma finite_nat_set_bounded2: "finite N ==> \<exists>n. (\<forall>i \<in> N. i<=(n::nat))"
+apply (erule_tac F = N in finite_induct, auto)
+apply (rule_tac x = "n + x" in exI, auto)
+done
+
+lemma finite_nat_set_bounded_iff2: "finite N = (\<exists>n. (\<forall>i \<in> N. i<=(n::nat)))"
+by (blast intro: finite_nat_set_bounded2 bounded_nat_set_is_finite2)
+
+lemma not_finite_nat_set_iff2: "(~ finite N) = (\<forall>n. \<exists>i \<in> N. n < (i::nat))"
+by (auto simp add: finite_nat_set_bounded_iff2 le_def)
+
+
+subsection{*An injective function cannot define an embedded natural number*}
-consts injf_max :: "nat => ('a::{order} set) => 'a"
-primrec
- injf_max_zero "injf_max 0 E = choicefun E"
- injf_max_Suc "injf_max (Suc n) E = choicefun({e. e : E & injf_max n E < e})"
+lemma lemma_infinite_set_singleton: "\<forall>m n. m \<noteq> n --> f n \<noteq> f m
+ ==> {n. f n = N} = {} | (\<exists>m. {n. f n = N} = {m})"
+apply auto
+apply (drule_tac x = x in spec, auto)
+apply (subgoal_tac "\<forall>n. (f n = f x) = (x = n) ")
+apply auto
+done
+
+lemma inj_fun_not_hypnat_in_SHNat: "inj f ==> Abs_hypnat(hypnatrel `` {f}) \<notin> Nats"
+apply (auto simp add: SHNat_eq hypnat_of_nat_eq)
+apply (subgoal_tac "\<forall>m n. m \<noteq> n --> f n \<noteq> f m", auto)
+apply (drule_tac [2] injD)
+prefer 2 apply assumption
+apply (drule_tac N = N in lemma_infinite_set_singleton, auto)
+done
+
+lemma range_subset_mem_starsetNat:
+ "range f <= A ==> Abs_hypnat(hypnatrel `` {f}) \<in> *sNat* A"
+apply (unfold starsetNat_def, auto, ultra)
+apply (drule_tac c = "f x" in subsetD)
+apply (rule rangeI, auto)
+done
+
+(*--------------------------------------------------------------------------------*)
+(* Gleason Proposition 11-5.5. pg 149, pg 155 (ex. 3) and pg. 360 *)
+(* Let E be a nonvoid ordered set with no maximal elements (note: effectively an *)
+(* infinite set if we take E = N (Nats)). Then there exists an order-preserving *)
+(* injection from N to E. Of course, (as some doofus will undoubtedly point out! *)
+(* :-)) can use notion of least element in proof (i.e. no need for choice) if *)
+(* dealing with nats as we have well-ordering property *)
+(*--------------------------------------------------------------------------------*)
+
+lemma lemmaPow3: "E \<noteq> {} ==> \<exists>x. \<exists>X \<in> (Pow E - {{}}). x: X"
+by auto
+
+lemma choicefun_mem_set: "E \<noteq> {} ==> choicefun E \<in> E"
+apply (unfold choicefun_def)
+apply (rule lemmaPow3 [THEN someI2_ex], auto)
+done
+declare choicefun_mem_set [simp]
+
+lemma injf_max_mem_set: "[| E \<noteq>{}; \<forall>x. \<exists>y \<in> E. x < y |] ==> injf_max n E \<in> E"
+apply (induct_tac "n", force)
+apply (simp (no_asm) add: choicefun_def)
+apply (rule lemmaPow3 [THEN someI2_ex], auto)
+done
+
+lemma injf_max_order_preserving: "\<forall>x. \<exists>y \<in> E. x < y ==> injf_max n E < injf_max (Suc n) E"
+apply (simp (no_asm) add: choicefun_def)
+apply (rule lemmaPow3 [THEN someI2_ex], auto)
+done
+
+lemma injf_max_order_preserving2: "\<forall>x. \<exists>y \<in> E. x < y
+ ==> \<forall>n m. m < n --> injf_max m E < injf_max n E"
+apply (rule allI)
+apply (induct_tac "n", auto)
+apply (simp (no_asm) add: choicefun_def)
+apply (rule lemmaPow3 [THEN someI2_ex])
+apply (auto simp add: less_Suc_eq)
+apply (drule_tac x = m in spec)
+apply (drule subsetD, auto)
+apply (drule_tac x = "injf_max m E" in order_less_trans, auto)
+done
+
+lemma inj_injf_max: "\<forall>x. \<exists>y \<in> E. x < y ==> inj (%n. injf_max n E)"
+apply (rule inj_onI)
+apply (rule ccontr, auto)
+apply (drule injf_max_order_preserving2)
+apply (cut_tac m = x and n = y in less_linear, auto)
+apply (auto dest!: spec)
+done
+
+lemma infinite_set_has_order_preserving_inj:
+ "[| (E::('a::{order} set)) \<noteq> {}; \<forall>x. \<exists>y \<in> E. x < y |]
+ ==> \<exists>f. range f <= E & inj (f::nat => 'a) & (\<forall>m. f m < f(Suc m))"
+apply (rule_tac x = "%n. injf_max n E" in exI, safe)
+apply (rule injf_max_mem_set)
+apply (rule_tac [3] inj_injf_max)
+apply (rule_tac [4] injf_max_order_preserving, auto)
+done
+
+text{*Only need the existence of an injective function from N to A for proof*}
+
+lemma hypnat_infinite_has_nonstandard:
+ "~ finite A ==> hypnat_of_nat ` A < ( *sNat* A)"
+apply auto
+apply (rule subsetD)
+apply (rule NatStar_hypreal_of_real_image_subset, auto)
+apply (subgoal_tac "A \<noteq> {}")
+prefer 2 apply force
+apply (drule infinite_set_has_order_preserving_inj)
+apply (erule not_finite_nat_set_iff2 [THEN iffD1], auto)
+apply (drule inj_fun_not_hypnat_in_SHNat)
+apply (drule range_subset_mem_starsetNat)
+apply (auto simp add: SHNat_eq)
+done
+
+lemma starsetNat_eq_hypnat_of_nat_image_finite: "*sNat* A = hypnat_of_nat ` A ==> finite A"
+apply (rule ccontr)
+apply (auto dest: hypnat_infinite_has_nonstandard)
+done
+
+lemma finite_starsetNat_iff: "( *sNat* A = hypnat_of_nat ` A) = (finite A)"
+by (blast intro!: starsetNat_eq_hypnat_of_nat_image_finite NatStar_hypnat_of_nat)
+
+lemma hypnat_infinite_has_nonstandard_iff: "(~ finite A) = (hypnat_of_nat ` A < *sNat* A)"
+apply (rule iffI)
+apply (blast intro!: hypnat_infinite_has_nonstandard)
+apply (auto simp add: finite_starsetNat_iff [symmetric])
+done
+
+subsection{*Existence of Infinitely Many Primes: a Nonstandard Proof*}
+
+lemma lemma_not_dvd_hypnat_one: "~ (\<forall>n \<in> - {0}. hypnat_of_nat n hdvd 1)"
+apply auto
+apply (rule_tac x = 2 in bexI)
+apply (auto simp add: hypnat_of_nat_eq hypnat_one_def hdvd dvd_def)
+done
+declare lemma_not_dvd_hypnat_one [simp]
+
+lemma lemma_not_dvd_hypnat_one2: "\<exists>n \<in> - {0}. ~ hypnat_of_nat n hdvd 1"
+apply (cut_tac lemma_not_dvd_hypnat_one)
+apply (auto simp del: lemma_not_dvd_hypnat_one)
+done
+declare lemma_not_dvd_hypnat_one2 [simp]
+
+(* not needed here *)
+lemma hypnat_gt_zero_gt_one:
+ "[| 0 < (N::hypnat); N \<noteq> 1 |] ==> 1 < N"
+apply (unfold hypnat_zero_def hypnat_one_def)
+apply (rule_tac z = N in eq_Abs_hypnat)
+apply (auto simp add: hypnat_less, ultra)
+done
+
+lemma hypnat_add_one_gt_one:
+ "0 < N ==> 1 < (N::hypnat) + 1"
+apply (unfold hypnat_zero_def hypnat_one_def)
+apply (rule_tac z = N in eq_Abs_hypnat)
+apply (auto simp add: hypnat_less hypnat_add)
+done
+
+lemma zero_not_prime: "0 \<notin> prime"
+apply safe
+apply (drule prime_g_zero, auto)
+done
+declare zero_not_prime [simp]
+
+lemma hypnat_of_nat_zero_not_prime: "hypnat_of_nat 0 \<notin> starprime"
+by (auto intro!: bexI simp add: starprime_def starsetNat_def hypnat_of_nat_eq)
+declare hypnat_of_nat_zero_not_prime [simp]
+
+lemma hypnat_zero_not_prime:
+ "0 \<notin> starprime"
+apply (unfold starprime_def starsetNat_def hypnat_zero_def)
+apply (auto intro!: bexI)
+done
+declare hypnat_zero_not_prime [simp]
+
+lemma one_not_prime: "1 \<notin> prime"
+apply safe
+apply (drule prime_g_one, auto)
+done
+declare one_not_prime [simp]
+
+lemma one_not_prime2: "Suc 0 \<notin> prime"
+apply safe
+apply (drule prime_g_one, auto)
+done
+declare one_not_prime2 [simp]
+
+lemma hypnat_of_nat_one_not_prime: "hypnat_of_nat 1 \<notin> starprime"
+by (auto intro!: bexI simp add: starprime_def starsetNat_def hypnat_of_nat_eq)
+declare hypnat_of_nat_one_not_prime [simp]
+
+lemma hypnat_one_not_prime: "1 \<notin> starprime"
+apply (unfold starprime_def starsetNat_def hypnat_one_def)
+apply (auto intro!: bexI)
+done
+declare hypnat_one_not_prime [simp]
+
+lemma hdvd_diff: "[| k hdvd m; k hdvd n |] ==> k hdvd (m - n)"
+apply (rule_tac z = k in eq_Abs_hypnat)
+apply (rule_tac z = m in eq_Abs_hypnat)
+apply (rule_tac z = n in eq_Abs_hypnat)
+apply (auto simp add: hdvd hypnat_minus, ultra)
+apply (blast intro: dvd_diff)
+done
+
+lemma dvd_one_eq_one: "x dvd (1::nat) ==> x = 1"
+by (unfold dvd_def, auto)
+
+lemma hdvd_one_eq_one: "x hdvd 1 ==> x = 1"
+apply (unfold hypnat_one_def)
+apply (rule_tac z = x in eq_Abs_hypnat)
+apply (auto simp add: hdvd)
+done
+
+theorem not_finite_prime: "~ finite prime"
+apply (rule hypnat_infinite_has_nonstandard_iff [THEN iffD2])
+apply (cut_tac hypnat_dvd_all_hypnat_of_nat)
+apply (erule exE)
+apply (erule conjE)
+apply (subgoal_tac "1 < N + 1")
+prefer 2 apply (blast intro: hypnat_add_one_gt_one)
+apply (drule hyperprime_factor_exists)
+apply (auto intro: NatStar_mem)
+apply (subgoal_tac "k \<notin> hypnat_of_nat ` prime")
+apply (force simp add: starprime_def, safe)
+apply (drule_tac x = x in bspec)
+apply (rule ccontr, simp)
+apply (drule hdvd_diff, assumption)
+apply (auto dest: hdvd_one_eq_one)
+done
end
-
-
--- a/src/HOL/Hyperreal/Integration.ML Fri Jul 30 10:44:42 2004 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1087 +0,0 @@
-(* Title : Integration.ML
- Author : Jacques D. Fleuriot
- Copyright : 2000 University of Edinburgh
- Description : Theory of integration (c.f. Harison's HOL development)
-*)
-
-val mult_2 = thm"mult_2";
-val mult_2_right = thm"mult_2_right";
-
-fun ARITH_PROVE str = prove_goal thy str
- (fn prems => [cut_facts_tac prems 1,arith_tac 1]);
-
-fun CLAIM_SIMP str thms =
- prove_goal (the_context()) str
- (fn prems => [cut_facts_tac prems 1,
- auto_tac (claset(),simpset() addsimps thms)]);
-
-fun CLAIM str = CLAIM_SIMP str [];
-
-Goalw [psize_def] "a = b ==> psize (%n. if n = 0 then a else b) = 0";
-by Auto_tac;
-qed "partition_zero";
-Addsimps [partition_zero];
-
-Goalw [psize_def] "a < b ==> psize (%n. if n = 0 then a else b) = 1";
-by Auto_tac;
-by (rtac some_equality 1);
-by Auto_tac;
-by (dres_inst_tac [("x","1")] spec 1);
-by Auto_tac;
-qed "partition_one";
-Addsimps [partition_one];
-
-Goalw [partition_def]
- "a <= b ==> partition(a,b)(%n. if n = 0 then a else b)";
-by (auto_tac (claset(),simpset() addsimps [order_le_less]));
-qed "partition_single";
-Addsimps [partition_single];
-
-Goalw [partition_def] "partition(a,b) D ==> (D(0) = a)";
-by Auto_tac;
-qed "partition_lhs";
-
-Goalw [partition_def]
- "(partition(a,b) D) = \
-\ ((D 0 = a) & \
-\ (ALL n. n < (psize D) --> D n < D(Suc n)) & \
-\ (ALL n. (psize D) <= n --> (D n = b)))";
-by Auto_tac;
-by (ALLGOALS(subgoal_tac "psize D = N"));
-by Auto_tac;
-by (ALLGOALS(simp_tac (simpset() addsimps [psize_def])));
-by (ALLGOALS(rtac some_equality));
-by (Blast_tac 1 THEN Blast_tac 2);
-by (ALLGOALS(rtac ccontr));
-by (ALLGOALS(dtac (ARITH_PROVE "n ~= (N::nat) ==> n < N | N < n")));
-by (Step_tac 1);
-by (dres_inst_tac [("x","Na")] spec 1);
-by (rotate_tac 3 1);
-by (dres_inst_tac [("x","Suc Na")] spec 1);
-by (Asm_full_simp_tac 1);
-by (rotate_tac 2 1);
-by (dres_inst_tac [("x","N")] spec 1);
-by (Asm_full_simp_tac 1);
-by (dres_inst_tac [("x","Na")] spec 1);
-by (rotate_tac 3 1);
-by (dres_inst_tac [("x","Suc Na")] spec 1);
-by (Asm_full_simp_tac 1);
-by (rotate_tac 2 1);
-by (dres_inst_tac [("x","N")] spec 1);
-by (Asm_full_simp_tac 1);
-qed "partition";
-
-Goal "partition(a,b) D ==> (D(psize D) = b)";
-by (dtac (partition RS subst) 1);
-by (Step_tac 1);
-by (REPEAT(dres_inst_tac [("x","psize D")] spec 1));
-by Auto_tac;
-qed "partition_rhs";
-
-Goal "[|partition(a,b) D; psize D <= n |] ==> (D n = b)";
-by (dtac (partition RS subst) 1);
-by (Blast_tac 1);
-qed "partition_rhs2";
-
-Goal
- "partition(a,b) D & m + Suc d <= n & n <= (psize D) --> D(m) < D(m + Suc d)";
-by (induct_tac "d" 1);
-by Auto_tac;
-by (ALLGOALS(dtac (partition RS subst)));
-by (Step_tac 1);
-by (ALLGOALS(dtac (ARITH_PROVE "Suc m <= n ==> m < n")));
-by (ALLGOALS(dtac less_le_trans));
-by (assume_tac 1 THEN assume_tac 2);
-by (ALLGOALS(blast_tac (claset() addIs [order_less_trans])));
-qed_spec_mp "lemma_partition_lt_gen";
-
-Goal "m < n ==> EX d. n = m + Suc d";
-by (auto_tac (claset(),simpset() addsimps [less_iff_Suc_add]));
-qed "less_eq_add_Suc";
-
-Goal "[|partition(a,b) D; m < n; n <= (psize D)|] ==> D(m) < D(n)";
-by (auto_tac (claset() addDs [less_eq_add_Suc] addIs [lemma_partition_lt_gen],
- simpset()));
-qed "partition_lt_gen";
-
-Goal "partition(a,b) D ==> (n < (psize D) --> D(0) < D(Suc n))";
-by (dtac (partition RS subst) 1);
-by (induct_tac "n" 1);
-by (Blast_tac 1);
-by (blast_tac (claset() addSDs [leI] addDs
- [(ARITH_PROVE "m <= n ==> m <= Suc n"),
- le_less_trans,order_less_trans]) 1);
-qed_spec_mp "partition_lt";
-
-Goal "partition(a,b) D ==> a <= b";
-by (ftac (partition RS subst) 1);
-by (Step_tac 1);
-by (rotate_tac 2 1);
-by (dres_inst_tac [("x","psize D")] spec 1);
-by (Step_tac 1);
-by (rtac ccontr 1);
-by (case_tac "psize D = 0" 1);
-by (Step_tac 1);
-by (dres_inst_tac [("n","psize D - 1")] partition_lt 2);
-by Auto_tac;
-qed "partition_le";
-
-Goal "[|partition(a,b) D; n < (psize D)|] ==> D(n) < D(psize D)";
-by (auto_tac (claset() addIs [partition_lt_gen],simpset()));
-qed "partition_gt";
-
-Goal "partition(a,b) D ==> ((a = b) = (psize D = 0))";
-by (ftac (partition RS subst) 1);
-by (Step_tac 1);
-by (rotate_tac 2 1);
-by (dres_inst_tac [("x","psize D")] spec 1);
-by (rtac ccontr 1);
-by (dres_inst_tac [("n","psize D - 1")] partition_lt 1);
-by (Blast_tac 3 THEN Auto_tac);
-qed "partition_eq";
-
-Goal "partition(a,b) D ==> a <= D(r)";
-by (ftac (partition RS subst) 1);
-by (Step_tac 1);
-by (induct_tac "r" 1);
-by (cut_inst_tac [("m","Suc n"),("n","psize D")]
- (ARITH_PROVE "m < n | n <= (m::nat)") 2);
-by (Step_tac 1);
-by (eres_inst_tac [("j","D n")] real_le_trans 1);
-by (dres_inst_tac [("x","n")] spec 1);
-by (blast_tac (claset() addIs [less_trans,order_less_imp_le]) 1);
-by (res_inst_tac [("j","b")] real_le_trans 1);
-by (etac partition_le 1);
-by (Blast_tac 1);
-qed "partition_lb";
-
-Goal "[| partition(a,b) D; psize D ~= 0 |] ==> a < D(Suc n)";
-by (res_inst_tac [("t","a")] (partition_lhs RS subst) 1);
-by (assume_tac 1);
-by (cut_inst_tac [("m","psize D"),("n","Suc n")]
- (ARITH_PROVE "m < n | n <= (m::nat)") 1);
-by (ftac (partition RS subst) 1);
-by (Step_tac 1);
-by (rotate_tac 3 1);
-by (dres_inst_tac [("x","Suc n")] spec 1);
-by (etac impE 1);
-by (etac less_imp_le 1);
-by (ftac partition_rhs 1);
-by (dtac partition_gt 1 THEN assume_tac 1);
-by (Asm_simp_tac 1);
-by (blast_tac (claset() addIs [partition_lt,less_le_trans]) 1);
-qed "partition_lb_lt";
-
-Goal "partition(a,b) D ==> D(r) <= b";
-by (ftac (partition RS subst) 1);
-by (cut_inst_tac [("m","r"),("n","psize D")]
- (ARITH_PROVE "m < n | n <= (m::nat)") 1);
-by (Step_tac 1);
-by (Blast_tac 2);
-by (subgoal_tac "ALL x. D((psize D) - x) <= b" 1);
-by (rotate_tac 4 1);
-by (dres_inst_tac [("x","psize D - r")] spec 1);
-by (dtac (ARITH_PROVE "p < m ==> m - (m - p) = (p::nat)") 1);
-by (thin_tac "ALL n. psize D <= n --> D n = b" 1);
-by (Asm_full_simp_tac 1);
-by (Step_tac 1);
-by (induct_tac "x" 1);
-by (Simp_tac 1 THEN Blast_tac 1);
-by (case_tac "psize D - Suc n = 0" 1);
-by (thin_tac "ALL n. psize D <= n --> D n = b" 1);
-by (asm_simp_tac (simpset() addsimps [partition_le]) 1);
-by (rtac real_le_trans 1 THEN assume_tac 2);
-by (rtac (ARITH_PROVE "0 < m - Suc n ==> (m - n) = Suc(m - Suc n)"
- RS ssubst) 1);
-by (dres_inst_tac [("x","psize D - Suc n")] spec 2);
-by (thin_tac "ALL n. psize D <= n --> D n = b" 2);
-by (Asm_full_simp_tac 2);
-by (arith_tac 1);
-qed "partition_ub";
-
-Goal "[| partition(a,b) D; n < psize D |] ==> D(n) < b";
-by (blast_tac (claset() addIs [partition_rhs RS subst] addIs
- [partition_gt]) 1);
-qed "partition_ub_lt";
-
-Goal "[| partition (a, b) D1; partition (b, c) D2 |] \
-\ ==> (ALL n. \
-\ n < psize D1 + psize D2 --> \
-\ (if n < psize D1 then D1 n else D2 (n - psize D1)) \
-\ < (if Suc n < psize D1 then D1 (Suc n) \
-\ else D2 (Suc n - psize D1))) & \
-\ (ALL n. \
-\ psize D1 + psize D2 <= n --> \
-\ (if n < psize D1 then D1 n else D2 (n - psize D1)) = \
-\ (if psize D1 + psize D2 < psize D1 then D1 (psize D1 + psize D2) \
-\ else D2 (psize D1 + psize D2 - psize D1)))";
-by (Step_tac 1);
-by (auto_tac (claset() addIs [partition_lt_gen],simpset()));
-by (dres_inst_tac [("m","psize D1")]
- (leI RSN(2,ARITH_PROVE "[| n < m; m <= Suc n |] ==> m = Suc n")) 1);
-by (assume_tac 1);
-by (auto_tac (claset() addSIs [partition_lt_gen],
- simpset() addsimps [partition_lhs,partition_ub_lt]));
-by (blast_tac (claset() addIs [ARITH_PROVE "~n < m ==> n - m < Suc n - m"]) 1);
-by (auto_tac (claset(),simpset() addsimps [
- ARITH_PROVE "~ n < m ==> (Suc n - m <= p) = (Suc n <= m + p)"]));
-by (dtac (ARITH_PROVE "p + q <= (n::nat) ==> q <= n - p") 1);
-by (auto_tac (claset() addSIs [partition_rhs2], simpset() addsimps
- [partition_rhs]));
-qed "lemma_partition_append1";
-
-Goal "[| partition (a, b) D1; partition (b, c) D2; N < psize D1 |] \
-\ ==> D1(N) < D2 (psize D2)";
-by (res_inst_tac [("y","D1(psize D1)")] order_less_le_trans 1);
-by (etac partition_gt 1 THEN assume_tac 1);
-by (auto_tac (claset(),simpset() addsimps [partition_rhs,partition_le]));
-qed "lemma_psize1";
-
-Goal "[| partition (a, b) D1; partition (b, c) D2 |] \
-\ ==> psize (%n. if n < psize D1 then D1 n else D2 (n - psize D1)) = \
-\ psize D1 + psize D2";
-by (res_inst_tac
- [("D2","%n. if n < psize D1 then D1 n else D2 (n - psize D1)")]
- ((psize_def RS meta_eq_to_obj_eq) RS ssubst) 1);
-by (rtac some1_equality 1);
-by (blast_tac (claset() addSIs [lemma_partition_append1]) 2);
-by (rtac ex1I 1 THEN rtac lemma_partition_append1 1);
-by Auto_tac;
-by (rtac ccontr 1);
-by (dtac (ARITH_PROVE "m ~= n ==> m < n | n < (m::nat)") 1);
-by (Step_tac 1);
-by (rotate_tac 3 1);
-by (dres_inst_tac [("x","psize D1 + psize D2")] spec 1);
-by Auto_tac;
-by (case_tac "N < psize D1" 1);
-by (auto_tac (claset() addDs [lemma_psize1],simpset()));
-by (dtac leI 1);
-by (dtac (ARITH_PROVE "[|p <= n; n < p + m|] ==> n - p < (m::nat)") 1);
-by (assume_tac 1);
-by (dres_inst_tac [("a","b"),("b","c")] partition_gt 1);
-by Auto_tac;
-by (dres_inst_tac [("x","psize D1 + psize D2")] spec 1);
-by (auto_tac (claset(),simpset() addsimps [partition_rhs2]));
-qed "lemma_partition_append2";
-
-Goalw [tpart_def]
-"[|psize D = 0; tpart(a,b) (D,p)|] ==> a = b";
-by (auto_tac (claset(),simpset() addsimps [partition_eq]));
-qed "tpart_eq_lhs_rhs";
-
-Goalw [tpart_def] "tpart(a,b) (D,p) ==> partition(a,b) D";
-by Auto_tac;
-qed "tpart_partition";
-
-Goal "[| tpart(a,b) (D1,p1); fine(g) (D1,p1); \
-\ tpart(b,c) (D2,p2); fine(g) (D2,p2) |] \
-\ ==> EX D p. tpart(a,c) (D,p) & fine(g) (D,p)";
-by (res_inst_tac
- [("x","%n. if n < psize D1 then D1 n else D2 (n - psize D1)")] exI 1);
-by (res_inst_tac
- [("x","%n. if n < psize D1 then p1 n else p2 (n - psize D1)")] exI 1);
-by (cut_inst_tac [("m","psize D1")] (ARITH_PROVE "0 < (m::nat) | m = 0") 1);
-by (auto_tac (claset() addDs [tpart_eq_lhs_rhs],simpset()));
-by (asm_full_simp_tac (simpset() addsimps [fine_def,
- [tpart_partition,tpart_partition] MRS lemma_partition_append2]) 2);
-by Auto_tac;
-by (dres_inst_tac [("m","psize D1"),("n","n")]
- (leI RSN(2,ARITH_PROVE "[| n < m; m <= Suc n |] ==> m = Suc n")) 2);
-by Auto_tac;
-by (dtac (tpart_partition RS partition_rhs) 2);
-by (dtac (tpart_partition RS partition_lhs) 2);
-by Auto_tac;
-by (rotate_tac 3 2);
-by (dres_inst_tac [("x","n - psize D1")] spec 2);
-by (auto_tac (claset(),simpset() addsimps
- [ARITH_PROVE "[| (0::nat) < p; p <= n |] ==> (n - p < m) = (n < p + m)",
- ARITH_PROVE "~n < p ==> Suc n - p = Suc(n - p)"]));
-by (auto_tac (claset(),simpset() addsimps [tpart_def,
- ARITH_PROVE "~n < p ==> Suc n - p = Suc(n - p)"]));
-by (dres_inst_tac [("m","psize D1"),("n","n")]
- (leI RSN(2,ARITH_PROVE "[| n < m; m <= Suc n |] ==> m = Suc n")) 2);
-by Auto_tac;
-by (dtac partition_rhs 2);
-by (dtac partition_lhs 2);
-by Auto_tac;
-by (rtac (partition RS ssubst) 1);
-by (rtac (lemma_partition_append2 RS ssubst) 1);
-by (rtac conjI 3);
-by (dtac lemma_partition_append1 4);
-by (auto_tac (claset(),simpset() addsimps [partition_lhs,partition_rhs]));
-qed "partition_append";
-
-(* ------------------------------------------------------------------------ *)
-(* We can always find a division which is fine wrt any gauge *)
-(* ------------------------------------------------------------------------ *)
-
-Goal "[| a <= b; gauge(%x. a <= x & x <= b) g |] \
-\ ==> EX D p. tpart(a,b) (D,p) & fine g (D,p)";
-by (cut_inst_tac
- [("P","%(u,v). a <= u & v <= b --> (EX D p. tpart(u,v) (D,p) & fine(g) (D,p))")]
- lemma_BOLZANO2 1);
-by (Step_tac 1);
-by (REPEAT(blast_tac (claset() addIs [real_le_trans]) 1));
-by (auto_tac (claset() addIs [partition_append],simpset()));
-by (case_tac "a <= x & x <= b" 1);
-by (res_inst_tac [("x","1")] exI 2);
-by Auto_tac;
-by (res_inst_tac [("x","g x")] exI 1);
-by (auto_tac (claset(),simpset() addsimps [gauge_def]));
-by (res_inst_tac [("x","%n. if n = 0 then aa else ba")] exI 1);
-by (res_inst_tac [("x","%n. if n = 0 then x else ba")] exI 1);
-by (auto_tac (claset(),simpset() addsimps [tpart_def,fine_def]));
-qed "partition_exists";
-
-(* ------------------------------------------------------------------------ *)
-(* Lemmas about combining gauges *)
-(* ------------------------------------------------------------------------ *)
-
-Goalw [gauge_def]
- "[| gauge(E) g1; gauge(E) g2 |] \
-\ ==> gauge(E) (%x. if g1(x) < g2(x) then g1(x) else g2(x))";
-by Auto_tac;
-qed "gauge_min";
-
-Goalw [fine_def]
- "fine (%x. if g1(x) < g2(x) then g1(x) else g2(x)) (D,p) \
-\ ==> fine(g1) (D,p) & fine(g2) (D,p)";
-by (auto_tac (claset(),simpset() addsimps [split_if]));
-qed "fine_min";
-
-
-(* ------------------------------------------------------------------------ *)
-(* The integral is unique if it exists *)
-(* ------------------------------------------------------------------------ *)
-
-Goalw [Integral_def]
- "[| a <= b; Integral(a,b) f k1; Integral(a,b) f k2 |] ==> k1 = k2";
-by Auto_tac;
-by (REPEAT(dres_inst_tac [("x","abs(k1 - k2)/2")] spec 1));
-by (Auto_tac THEN TRYALL(arith_tac));
-by (dtac gauge_min 1 THEN assume_tac 1);
-by (dres_inst_tac [("g","%x. if g x < ga x then g x else ga x")]
- partition_exists 1 THEN assume_tac 1);
-by Auto_tac;
-by (dtac fine_min 1);
-by (REPEAT(dtac spec 1) THEN Auto_tac);
-by (subgoal_tac
- "abs((rsum(D,p) f - k2) - (rsum(D,p) f - k1)) < abs(k1 - k2)" 1);
-by (arith_tac 1);
-by (dtac add_strict_mono 1 THEN assume_tac 1);
-by (auto_tac (claset(),
- HOL_ss addsimps [left_distrib RS sym,
- mult_2_right RS sym, mult_less_cancel_right]));
-by (ALLGOALS(arith_tac));
-qed "Integral_unique";
-
-Goalw [Integral_def] "Integral(a,a) f 0";
-by Auto_tac;
-by (res_inst_tac [("x","%x. 1")] exI 1);
-by (auto_tac (claset() addDs [partition_eq],simpset() addsimps [gauge_def,
- tpart_def,rsum_def]));
-qed "Integral_zero";
-Addsimps [Integral_zero];
-
-Goal "sumr 0 m (%n. D (Suc n) - D n) = D(m) - D 0";
-by (induct_tac "m" 1);
-by Auto_tac;
-qed "sumr_partition_eq_diff_bounds";
-Addsimps [sumr_partition_eq_diff_bounds];
-
-Goal "a <= b ==> Integral(a,b) (%x. 1) (b - a)";
-by (dtac real_le_imp_less_or_eq 1 THEN Auto_tac);
-by (auto_tac (claset(),simpset() addsimps [rsum_def,Integral_def]));
-by (res_inst_tac [("x","%x. b - a")] exI 1);
-by (auto_tac (claset(),simpset() addsimps [gauge_def,
- abs_interval_iff,tpart_def,partition]));
-qed "Integral_eq_diff_bounds";
-
-Goal "a <= b ==> Integral(a,b) (%x. c) (c*(b - a))";
-by (dtac real_le_imp_less_or_eq 1 THEN Auto_tac);
-by (auto_tac (claset(),simpset() addsimps [rsum_def,Integral_def]));
-by (res_inst_tac [("x","%x. b - a")] exI 1);
-by (auto_tac (claset(),simpset() addsimps
- [sumr_mult RS sym,gauge_def,abs_interval_iff,
- right_diff_distrib RS sym,partition,tpart_def]));
-qed "Integral_mult_const";
-
-Goal "[| a <= b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)";
-by (dtac real_le_imp_less_or_eq 1);
-by (auto_tac (claset() addDs [[real_le_refl,Integral_zero] MRS Integral_unique],
- simpset()));
-by (auto_tac (claset(),simpset() addsimps [rsum_def,Integral_def,
- sumr_mult RS sym,real_mult_assoc]));
-by (res_inst_tac [("a2","c")] ((abs_ge_zero RS real_le_imp_less_or_eq)
- RS disjE) 1);
-by (dtac sym 2);
-by (Asm_full_simp_tac 2 THEN Blast_tac 2);
-by (dres_inst_tac [("x","e/abs c")] spec 1 THEN Auto_tac);
-by (asm_full_simp_tac (simpset() addsimps [zero_less_mult_iff,
- real_divide_def]) 1);
-by (rtac exI 1 THEN Auto_tac);
-by (REPEAT(dtac spec 1) THEN Auto_tac);
-by (res_inst_tac [("z1","inverse(abs c)")] (real_mult_less_iff1 RS iffD1) 1);
-by (fold_tac [real_divide_def]);
-by (auto_tac (claset(),
- simpset() addsimps [right_diff_distrib RS sym,
- abs_mult, real_mult_assoc RS sym,
- ARITH_PROVE "c ~= 0 ==> abs (c::real) ~= 0",
- positive_imp_inverse_positive]));
-qed "Integral_mult";
-
-(* ------------------------------------------------------------------------ *)
-(* Fundamental theorem of calculus (Part I) *)
-(* ------------------------------------------------------------------------ *)
-
-(* "Straddle Lemma" : Swartz & Thompson: AMM 95(7) 1988 *)
-
-Goal "ALL x. P(x) --> (EX y. Q x y) ==> EX f. (ALL x. P(x) --> Q x (f x))";
-by (cut_inst_tac [("S","Collect (%x. P x)"),("Q","Q")] (CLAIM_SIMP
- "(ALL x:S. (EX y. Q x y)) --> (EX f. (ALL x:S. Q x (f x)))" [bchoice]) 1);
-by Auto_tac;
-qed "choiceP";
-
-Goal "ALL x. P(x) --> (EX y. R(y) & (EX z. Q x y z)) ==> \
-\ EX f fa. (ALL x. P(x) --> R(f x) & Q x (f x) (fa x))";
-by (dtac (CLAIM "(ALL x. P(x) --> (EX y. R(y) & (EX z. Q x y z))) = \
-\ (ALL x. P(x) --> (EX y z. R(y) & Q x y z))" RS iffD1) 1);;
-by (dtac choiceP 1 THEN Step_tac 1);
-by (dtac choiceP 1 THEN Auto_tac);
-qed "choiceP2";
-
-Goal "ALL x. (EX y. R(y) & (EX z. Q x y z)) ==> \
-\ EX f fa. (ALL x. R(f x) & Q x (f x) (fa x))";
-by (dtac (CLAIM "(ALL x. (EX y. R(y) & (EX z. Q x y z))) = \
-\ (ALL x. (EX y z. R(y) & Q x y z))" RS iffD1) 1);;
-by (dtac choice 1 THEN Step_tac 1);
-by (dtac choice 1 THEN Auto_tac);
-qed "choice2";
-
-(* new simplifications e.g. (y < x/n) = (y * n < x) are a real nuisance
- they break the original proofs and make new proofs longer! *)
-Goalw [gauge_def]
- "[| ALL x. a <= x & x <= b --> DERIV f x :> f'(x); 0 < e |]\
-\ ==> EX g. gauge(%x. a <= x & x <= b) g & \
-\ (ALL x u v. a <= u & u <= x & x <= v & v <= b & (v - u) < g(x) \
-\ --> abs((f(v) - f(u)) - (f'(x) * (v - u))) <= e * (v - u))";
-by (subgoal_tac "ALL x. a <= x & x <= b --> \
-\ (EX d. 0 < d & \
-\ (ALL u v. u <= x & x <= v & (v - u) < d --> \
-\ abs((f(v) - f(u)) - (f'(x) * (v - u))) <= e * (v - u)))" 1);
-by (dtac choiceP 1);
-by Auto_tac;
-by (dtac spec 1 THEN Auto_tac);
-by (auto_tac (claset(),simpset() addsimps [DERIV_iff2,LIM_def]));
-by (dres_inst_tac [("x","e/2")] spec 1);
-by Auto_tac;
-by (subgoal_tac "ALL z. abs(z - x) < s --> \
-\ abs((f(z) - f(x)) - (f'(x) * (z - x))) <= (e / 2) * abs(z - x)" 1);
-by Auto_tac;
-by (case_tac "0 < abs(z - x)" 2);
-by (dtac (ARITH_PROVE "~ 0 < abs z ==> z = (0::real)") 3);
-by (asm_full_simp_tac (simpset() addsimps
- [ARITH_PROVE "(z - x = 0) = (z = (x::real))"]) 3);
-by (dres_inst_tac [("x","z")] spec 2);
-by (res_inst_tac [("z1","abs(inverse(z - x))")]
- (real_mult_le_cancel_iff2 RS iffD1) 2);
-by (Asm_full_simp_tac 2);
-by (asm_full_simp_tac (simpset()
- delsimps [abs_inverse, abs_mult]
- addsimps [abs_mult RS sym, real_mult_assoc RS sym]) 2);
-by (subgoal_tac "inverse (z - x) * (f z - f x - f' x * (z - x)) = \
-\ (f z - f x)/(z - x) - f' x" 2);
-by (asm_full_simp_tac (simpset() addsimps [abs_mult RS sym] @ mult_ac) 2);
-by (asm_full_simp_tac (simpset() addsimps [real_diff_def]) 2);
-by (rtac (real_mult_commute RS subst) 2);
-by (asm_full_simp_tac (simpset() addsimps [left_distrib,
- real_diff_def]) 2);
-by (dtac (CLAIM "z ~= x ==> z + -x ~= (0::real)") 2);
-by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc,
- real_divide_def]) 2);
-by (simp_tac (simpset() addsimps [left_distrib]) 2);
-by (res_inst_tac [("x","s")] exI 1 THEN Auto_tac);
-by (res_inst_tac [("u1","u"),("v1","v")] (ARITH_PROVE "u < v | v <= (u::real)"
- RS disjE) 1);
-by (dres_inst_tac [("x","v")] real_le_imp_less_or_eq 2);
-by Auto_tac;
-(*29*)
-by (res_inst_tac [("j","abs((f(v) - f(x)) - (f'(x) * (v - x))) + \
-\ abs((f(x) - f(u)) - (f'(x) * (x - u)))")] real_le_trans 1);
-by (rtac (abs_triangle_ineq RSN (2,real_le_trans)) 1);
-by (asm_full_simp_tac (simpset() addsimps [right_diff_distrib]) 1);
-by (arith_tac 1);
-by (res_inst_tac [("t","e*(v - u)")] (real_sum_of_halves RS subst) 1);
-by (rtac add_mono 1);
-by (res_inst_tac [("j","(e / 2) * abs(v - x)")] real_le_trans 1);
-
-by (Asm_full_simp_tac 2 THEN arith_tac 2);
-by (ALLGOALS (thin_tac "ALL xa. \
-\ xa ~= x & abs (xa + - x) < s --> \
-\ abs ((f xa - f x) / (xa - x) + - f' x) * 2 < e"));
-by (dres_inst_tac [("x","v")] spec 1 THEN Auto_tac);
-by (arith_tac 1);
-by (dres_inst_tac [("x","u")] spec 1 THEN Auto_tac);
-by (arith_tac 1);
-by (subgoal_tac "abs (f u - f x - f' x * (u - x)) = \
-\ abs (f x - f u - f' x * (x - u))" 1);
-by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [right_distrib,
- real_diff_def]) 2);
-by (arith_tac 2);
-by(rtac real_le_trans 1);
-by Auto_tac;
-by (arith_tac 1);
-qed "lemma_straddle";
-
-Goal "((number_of c - 1) * x <= 0) =((number_of c ::real) * x <= x)";
-by (rtac ((ARITH_PROVE "(x <= y) = (x - y <= (0::real))") RS ssubst) 1);
-by (simp_tac (simpset() addsimps [left_diff_distrib,
- CLAIM_SIMP "c * x - x = (c - 1) * (x::real)" [left_diff_distrib]]) 1);
-qed "lemma_number_of_mult_le";
-
-
-Goal "[|a <= b; ALL x. a <= x & x <= b --> DERIV f x :> f'(x) |] \
-\ ==> Integral(a,b) f' (f(b) - f(a))";
-by (dtac real_le_imp_less_or_eq 1 THEN Auto_tac);
-by (auto_tac (claset(),simpset() addsimps [Integral_def]));
-by (rtac ccontr 1);
-by (subgoal_tac "ALL e. 0 < e --> \
-\ (EX g. gauge (%x. a <= x & x <= b) g & \
-\ (ALL D p. \
-\ tpart (a, b) (D, p) & fine g (D, p) --> \
-\ abs (rsum (D, p) f' - (f b - f a)) <= e))" 1);
-by (rotate_tac 3 1);
-by (dres_inst_tac [("x","e/2")] spec 1 THEN Auto_tac);
-by (dtac spec 1 THEN Auto_tac);
-by (REPEAT(dtac spec 1) THEN Auto_tac);
-by (dres_inst_tac [("e","ea/(b - a)")] lemma_straddle 1);
-by (auto_tac (claset(),simpset() addsimps [thm"Ring_and_Field.zero_less_divide_iff"]));
-by (rtac exI 1);
-by (auto_tac (claset(),simpset() addsimps [tpart_def,rsum_def]));
-by (subgoal_tac "sumr 0 (psize D) (%n. f(D(Suc n)) - f(D n)) = \
-\ f b - f a" 1);
-by (cut_inst_tac [("D","%n. f(D n)"),("m","psize D")]
- sumr_partition_eq_diff_bounds 2);
-by (asm_full_simp_tac (simpset() addsimps [partition_lhs,partition_rhs]) 2);
-by (dtac sym 1 THEN Asm_full_simp_tac 1);
-by (simp_tac (simpset() addsimps [sumr_diff]) 1);
-by (rtac (sumr_rabs RS real_le_trans) 1);
-by (subgoal_tac
- "ea = sumr 0 (psize D) (%n. (ea / (b - a)) * (D(Suc n) - (D n)))" 1);
-by (asm_full_simp_tac (simpset() addsimps
- [ARITH_PROVE "abs(y - (x::real)) = abs(x - y)"]) 1);
-by (res_inst_tac [("t","ea")] ssubst 1 THEN assume_tac 1);
-by (rtac sumr_le2 1);
-by (rtac (sumr_mult RS subst) 2);
-by (auto_tac (claset(),simpset() addsimps [partition_rhs,
- partition_lhs,partition_lb,partition_ub,fine_def]));
-qed "FTC1";
-
-
-Goal "[| Integral(a,b) f k1; k2 = k1 |] ==> Integral(a,b) f k2";
-by (Asm_simp_tac 1);
-qed "Integral_subst";
-
-Goal "[| a <= b; b <= c; Integral(a,b) f' k1; Integral(b,c) f' k2; \
-\ ALL x. a <= x & x <= c --> DERIV f x :> f' x |] \
-\ ==> Integral(a,c) f' (k1 + k2)";
-by (rtac (FTC1 RS Integral_subst) 1);
-by Auto_tac;
-by (ftac FTC1 1 THEN Auto_tac);
-by (forw_inst_tac [("a","b")] FTC1 1 THEN Auto_tac);
-by (dres_inst_tac [("x","x")] spec 1 THEN Auto_tac);
-by (dres_inst_tac [("k2.0","f b - f a")] Integral_unique 1);
-by (dres_inst_tac [("k2.0","f c - f b")] Integral_unique 3);
-by Auto_tac;
-qed "Integral_add";
-
-Goal "partition(a,b) D ==> psize D = (LEAST n. D(n) = b)";
-by (auto_tac (claset() addSIs [Least_equality RS sym,partition_rhs],simpset()));
-by (rtac ccontr 1);
-by (dtac partition_ub_lt 1);
-by (auto_tac (claset(), simpset() addsimps [linorder_not_less RS sym]));
-qed "partition_psize_Least";
-
-Goal "partition (a, c) D ==> ~ (EX n. c < D(n))";
-by (Step_tac 1);
-by (dres_inst_tac [("r","n")] partition_ub 1);
-by Auto_tac;
-qed "lemma_partition_bounded";
-
-Goal "partition (a, c) D ==> D = (%n. if D n < c then D n else c)";
-by (rtac ext 1 THEN Auto_tac);
-by (auto_tac (claset() addSDs [lemma_partition_bounded],simpset()));
-by (dres_inst_tac [("x","n")] spec 1);
-by Auto_tac;
-qed "lemma_partition_eq";
-
-Goal "partition (a, c) D ==> D = (%n. if D n <= c then D n else c)";
-by (rtac ext 1 THEN Auto_tac);
-by (auto_tac (claset() addSDs [lemma_partition_bounded],simpset()));
-by (dres_inst_tac [("x","n")] spec 1);
-by Auto_tac;
-qed "lemma_partition_eq2";
-
-Goal "[| partition(a,b) D; n < psize D |] ==> D n < D (Suc n)";
-by (auto_tac (claset(),simpset() addsimps [partition]));
-qed "partition_lt_Suc";
-
-Goal "tpart(a,c) (D,p) ==> p = (%n. if D n < c then p n else c)";
-by (rtac ext 1);
-by (auto_tac (claset(),simpset() addsimps [tpart_def]));
-by (dtac (linorder_not_less RS iffD1) 1);
-by (dres_inst_tac [("r","Suc n")] partition_ub 1);
-by (dres_inst_tac [("x","n")] spec 1);
-by Auto_tac;
-qed "tpart_tag_eq";
-
-(*----------------------------------------------------------------------------*)
-(* Lemmas for Additivity Theorem of gauge integral *)
-(*----------------------------------------------------------------------------*)
-
-Goal "[| a <= D n; D n < b; partition(a,b) D |] ==> n < psize D";
-by (dtac (partition RS iffD1) 1 THEN Step_tac 1);
-by (rtac ccontr 1 THEN dtac leI 1);
-by Auto_tac;
-qed "lemma_additivity1";
-
-Goal "[| a <= D n; partition(a,D n) D |] ==> psize D <= n";
-by (rtac ccontr 1 THEN dtac not_leE 1);
-by (ftac (partition RS iffD1) 1 THEN Step_tac 1);
-by (forw_inst_tac [("r","Suc n")] partition_ub 1);
-by (auto_tac (claset() addSDs [spec],simpset()));
-qed "lemma_additivity2";
-
-Goal "[| partition(a,b) D; psize D < m |] ==> D(m) = D(psize D)";
-by (auto_tac (claset(),simpset() addsimps [partition]));
-qed "partition_eq_bound";
-
-Goal "[| partition(a,b) D; psize D < m |] ==> D(r) <= D(m)";
-by (ftac (partition RS iffD1) 1 THEN Auto_tac);
-by (etac partition_ub 1);
-qed "partition_ub2";
-
-Goalw [tpart_def]
- "[| tpart(a,b) (D,p); psize D <= m |] ==> p(m) = D(m)";
-by Auto_tac;
-by (dres_inst_tac [("x","m")] spec 1);
-by (auto_tac (claset(),simpset() addsimps [partition_rhs2]));
-qed "tag_point_eq_partition_point";
-
-Goal "[| partition(a,b) D; D m < D n |] ==> m < n";
-by (cut_inst_tac [("m","n"),("n","psize D")] less_linear 1);
-by Auto_tac;
-by (rtac ccontr 1 THEN dtac leI 1 THEN dtac le_imp_less_or_eq 1);
-by (cut_inst_tac [("m","m"),("n","psize D")] less_linear 1);
-by (auto_tac (claset() addDs [partition_gt],simpset()));
-by (dres_inst_tac [("n","m")] partition_lt_gen 1 THEN Auto_tac);
-by (ftac partition_eq_bound 1);
-by (dtac partition_gt 2);
-by Auto_tac;
-by (rtac ccontr 1 THEN dtac leI 1 THEN dtac le_imp_less_or_eq 1);
-by (auto_tac (claset() addDs [partition_eq_bound],simpset()));
-by (rtac ccontr 1 THEN dtac leI 1 THEN dtac le_imp_less_or_eq 1);
-by (ftac partition_eq_bound 1 THEN assume_tac 1);
-by (dres_inst_tac [("m","m")] partition_eq_bound 1);
-by Auto_tac;
-qed "partition_lt_cancel";
-
-Goalw [psize_def]
- "[| a <= D n; D n < b; partition (a, b) D |] \
-\ ==> psize (%x. if D x < D n then D(x) else D n) = n";
-by (ftac lemma_additivity1 1);
-by (assume_tac 1 THEN assume_tac 1);
-by (rtac some_equality 1);
-by (auto_tac (claset() addIs [partition_lt_Suc],simpset()));
-by (dres_inst_tac [("n","n")] partition_lt_gen 1);
-by (assume_tac 1 THEN arith_tac 1 THEN arith_tac 1);
-by (cut_inst_tac [("m","na"),("n","psize D")] less_linear 1);
-by (auto_tac (claset() addDs [partition_lt_cancel],simpset()));
-by (rtac ccontr 1);
-by (dtac (ARITH_PROVE "m ~= (n::nat) ==> m < n | n < m") 1);
-by (etac disjE 1);
-by (rotate_tac 5 1);
-by (dres_inst_tac [("x","n")] spec 1);
-by Auto_tac;
-by (dres_inst_tac [("n","n")] partition_lt_gen 1);
-by Auto_tac;
-by (arith_tac 1);
-by (dres_inst_tac [("x","n")] spec 1);
-by (asm_full_simp_tac (simpset() addsimps [split_if]) 1);
-qed "lemma_additivity4_psize_eq";
-
-Goal "partition (a, b) D \
-\ ==> psize (%x. if D x < D n then D(x) else D n) <= psize D";
-by (forw_inst_tac [("r","n")] partition_ub 1);
-by (dres_inst_tac [("x","D n")] real_le_imp_less_or_eq 1);
-by (auto_tac (claset(),simpset() addsimps
- [lemma_partition_eq RS sym]));
-by (forw_inst_tac [("r","n")] partition_lb 1);
-by (dtac lemma_additivity4_psize_eq 1);
-by (rtac ccontr 3 THEN Auto_tac);
-by (ftac (not_leE RSN (2,partition_eq_bound)) 1);
-by (auto_tac (claset(),simpset() addsimps [partition_rhs]));
-qed "lemma_psize_left_less_psize";
-
-Goal "[| partition(a,b) D; na < psize (%x. if D x < D n then D(x) else D n) |] \
-\ ==> na < psize D";
-by (etac (lemma_psize_left_less_psize RSN (2,less_le_trans)) 1);
-by (assume_tac 1);
-qed "lemma_psize_left_less_psize2";
-
-
-Goal "[| partition(a,b) D; D na < D n; D n < D (Suc na); \
-\ n < psize D |] \
-\ ==> False";
-by (cut_inst_tac [("m","n"),("n","Suc na")] less_linear 1);
-by Auto_tac;
-by (dres_inst_tac [("n","n")] partition_lt_gen 2);
-by Auto_tac;
-by (cut_inst_tac [("m","psize D"),("n","na")] less_linear 1);
-by (auto_tac (claset(),simpset() addsimps [partition_rhs2]));
-by (dtac (ARITH_PROVE "n < Suc na ==> n < na | n = na") 1);
-by Auto_tac;
-by (dres_inst_tac [("n","na")] partition_lt_gen 1);
-by Auto_tac;
-qed "lemma_additivity3";
-
-Goalw [psize_def] "psize (%x. k) = 0";
-by Auto_tac;
-qed "psize_const";
-Addsimps [psize_const];
-
-Goal "[| partition(a,b) D; D na < D n; D n < D (Suc na); \
-\ na < psize D |] \
-\ ==> False";
-by (forw_inst_tac [("m","n")] partition_lt_cancel 1);
-by (auto_tac (claset() addIs [lemma_additivity3],simpset()));
-qed "lemma_additivity3a";
-
-Goal "[| partition(a,b) D; D n < b |] ==> psize (%x. D (x + n)) <= psize D - n";
-by (res_inst_tac [("D2","(%x. D (x + n))")] (psize_def RS
- meta_eq_to_obj_eq RS ssubst) 1);
-by (res_inst_tac [("a","psize D - n")] someI2 1);
-by Auto_tac;
-by (dtac (ARITH_PROVE "(m::nat) < n - p ==> m + p < n") 1);
-by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
-by (dtac (ARITH_PROVE "(m::nat) - n <= p ==> m <= p + n") 1);
-by (case_tac "psize D <= n" 1);
-by (dtac not_leE 2);
-by (asm_simp_tac (simpset() addsimps
- [ARITH_PROVE "p <= n ==> p - n = (0::nat)"]) 1);
-by (blast_tac (claset() addDs [partition_rhs2]) 1);
-by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
-by (rtac ccontr 1 THEN dtac not_leE 1);
-by (dres_inst_tac [("x","psize D - n")] spec 1);
-by Auto_tac;
-by (ftac partition_rhs 1 THEN Step_tac 1);
-by (ftac partition_lt_cancel 1 THEN assume_tac 1);
-by (dtac (partition RS iffD1) 1 THEN Step_tac 1);
-by (subgoal_tac "~ D (psize D - n + n) < D (Suc (psize D - n + n))" 1);
-by (Blast_tac 1);
-by (rotate_tac 6 1 THEN dres_inst_tac [("x","Suc (psize D)")] spec 1);
-by (Asm_simp_tac 1);
-qed "better_lemma_psize_right_eq1";
-
-Goal "partition (a, D n) D ==> psize D <= n";
-by (rtac ccontr 1 THEN dtac not_leE 1);
-by (ftac partition_lt_Suc 1 THEN assume_tac 1);
-by (forw_inst_tac [("r","Suc n")] partition_ub 1);
-by Auto_tac;
-qed "psize_le_n";
-
-Goal "partition(a,D n) D ==> psize (%x. D (x + n)) <= psize D - n";
-by (res_inst_tac [("D2","(%x. D (x + n))")] (psize_def RS
- meta_eq_to_obj_eq RS ssubst) 1);
-by (res_inst_tac [("a","psize D - n")] someI2 1);
-by Auto_tac;
-by (dtac (ARITH_PROVE "(m::nat) < n - p ==> m + p < n") 1);
-by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
-by (dtac (ARITH_PROVE "(m::nat) - n <= p ==> m <= p + n") 1);
-by (case_tac "psize D <= n" 1);
-by (dtac not_leE 2);
-by (asm_simp_tac (simpset() addsimps
- [ARITH_PROVE "p <= n ==> p - n = (0::nat)"]) 1);
-by (blast_tac (claset() addDs [partition_rhs2]) 1);
-by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
-by (rtac ccontr 1 THEN dtac not_leE 1);
-by (ftac psize_le_n 1);
-by (dres_inst_tac [("x","psize D - n")] spec 1);
-by (asm_full_simp_tac (simpset() addsimps
- [ARITH_PROVE "p <= n ==> p - n = (0::nat)"]) 1);
-by (dtac (partition RS iffD1) 1 THEN Step_tac 1);
-by (rotate_tac 5 1 THEN dres_inst_tac [("x","Suc n")] spec 1);
-by Auto_tac;
-qed "better_lemma_psize_right_eq1a";
-
-Goal "partition(a,b) D ==> psize (%x. D (x + n)) <= psize D - n";
-by (forw_inst_tac [("r1","n")] (partition_ub RS real_le_imp_less_or_eq) 1);
-by (blast_tac (claset() addIs [better_lemma_psize_right_eq1a,
- better_lemma_psize_right_eq1]) 1);
-qed "better_lemma_psize_right_eq";
-
-Goal "[| partition(a,b) D; D n < b |] ==> psize (%x. D (x + n)) <= psize D";
-by (res_inst_tac [("D2","(%x. D (x + n))")] (psize_def RS
- meta_eq_to_obj_eq RS ssubst) 1);
-by (res_inst_tac [("a","psize D - n")] someI2 1);
-by Auto_tac;
-by (dtac (ARITH_PROVE "(m::nat) < n - p ==> m + p < n") 1);
-by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
-by (subgoal_tac "n <= psize D" 1);
-by (dtac (ARITH_PROVE "(m::nat) - n <= p ==> m <= p + n") 1);
-by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
-by (rtac ccontr 1 THEN dtac not_leE 1);
-by (dtac (less_imp_le RSN (2,partition_rhs2)) 1);
-by Auto_tac;
-by (rtac ccontr 1 THEN dtac not_leE 1);
-by (dres_inst_tac [("x","psize D")] spec 1);
-by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
-qed "lemma_psize_right_eq1";
-
-(* should be combined with previous theorem; also proof has redundancy *)
-Goal "partition(a,D n) D ==> psize (%x. D (x + n)) <= psize D";
-by (res_inst_tac [("D2","(%x. D (x + n))")] (psize_def RS
- meta_eq_to_obj_eq RS ssubst) 1);
-by (res_inst_tac [("a","psize D - n")] someI2 1);
-by Auto_tac;
-by (dtac (ARITH_PROVE "(m::nat) < n - p ==> m + p < n") 1);
-by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
-by (dtac (ARITH_PROVE "(m::nat) - n <= p ==> m <= p + n") 1);
-by (case_tac "psize D <= n" 1);
-by (dtac not_leE 2);
-by (asm_simp_tac (simpset() addsimps
- [ARITH_PROVE "p <= n ==> p - n = (0::nat)"]) 1);
-by (blast_tac (claset() addDs [partition_rhs2]) 1);
-by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
-by (rtac ccontr 1 THEN dtac not_leE 1);
-by (dres_inst_tac [("x","psize D")] spec 1);
-by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
-qed "lemma_psize_right_eq1a";
-
-Goal "[| partition(a,b) D |] ==> psize (%x. D (x + n)) <= psize D";
-by (forw_inst_tac [("r1","n")] (partition_ub RS real_le_imp_less_or_eq) 1);
-by (blast_tac (claset() addIs [lemma_psize_right_eq1a,lemma_psize_right_eq1]) 1);
-qed "lemma_psize_right_eq";
-
-Goal "[| a <= D n; tpart (a, b) (D, p) |] \
-\ ==> tpart(a, D n) (%x. if D x < D n then D(x) else D n, \
-\ %x. if D x < D n then p(x) else D n)";
-by (forw_inst_tac [("r","n")] (tpart_partition RS partition_ub) 1);
-by (dres_inst_tac [("x","D n")] real_le_imp_less_or_eq 1);
-by (auto_tac (claset(),simpset() addsimps
- [tpart_partition RS lemma_partition_eq RS sym,
- tpart_tag_eq RS sym]));
-by (ftac (tpart_partition RSN (3,lemma_additivity1)) 1);
-by (auto_tac (claset(),simpset() addsimps [tpart_def]));
-by (dtac ((linorder_not_less RS iffD1) RS real_le_imp_less_or_eq) 2);
-by (Auto_tac);
-by (blast_tac (claset() addDs [lemma_additivity3]) 2);
-by (dtac (linorder_not_less RS iffD1) 2 THEN dres_inst_tac [("x","na")] spec 2);
-by (arith_tac 2);
-by (ftac lemma_additivity4_psize_eq 1);
-by (REPEAT(assume_tac 1));
-by (rtac (partition RS iffD2) 1);
-by (ftac (partition RS iffD1) 1);
-by (auto_tac (claset() addIs [partition_lt_gen],simpset() addsimps []));
-by (dres_inst_tac [("n","n")] partition_lt_gen 1);
-by (assume_tac 1 THEN arith_tac 1);
-by (Blast_tac 1);
-by (dtac partition_lt_cancel 1 THEN Auto_tac);
-qed "tpart_left1";
-
-Goal "[| a <= D n; tpart (a, b) (D, p); gauge (%x. a <= x & x <= D n) g;\
-\ fine (%x. if x < D n then min (g x) ((D n - x)/ 2) \
-\ else if x = D n then min (g (D n)) (ga (D n)) \
-\ else min (ga x) ((x - D n)/ 2)) (D, p) |] \
-\ ==> fine g \
-\ (%x. if D x < D n then D(x) else D n, \
-\ %x. if D x < D n then p(x) else D n)";
-by (auto_tac (claset(),simpset() addsimps [fine_def,tpart_def,gauge_def]));
-by (ALLGOALS (ftac lemma_psize_left_less_psize2));
-by (TRYALL(assume_tac));
-by (ALLGOALS (dres_inst_tac [("x","na")] spec) THEN Auto_tac);
-by (ALLGOALS(dres_inst_tac [("x","na")] spec));
-by Auto_tac;
-by (asm_full_simp_tac (simpset() addsimps [split_if]) 1);
-by (dtac ((linorder_not_less RS iffD1) RS real_le_imp_less_or_eq) 1);
-by (Step_tac 1);
-by (blast_tac (claset() addDs [lemma_additivity3a]) 1);
-by (dtac sym 1 THEN Auto_tac);
-qed "fine_left1";
-
-Goal "[| a <= D n; tpart (a, b) (D, p) |] \
-\ ==> tpart(D n, b) (%x. D(x + n),%x. p(x + n))";
-by (asm_full_simp_tac (simpset() addsimps [tpart_def,partition_def]) 1);
-by (Step_tac 1);
-by (res_inst_tac [("x","N - n")] exI 1 THEN Auto_tac);
-by (rotate_tac 2 1);
-by (dres_inst_tac [("x","na + n")] spec 1);
-by (rotate_tac 3 2);
-by (dres_inst_tac [("x","na + n")] spec 2);
-by (ALLGOALS(arith_tac));
-qed "tpart_right1";
-
-Goal "[| a <= D n; tpart (a, b) (D, p); gauge (%x. D n <= x & x <= b) ga;\
-\ fine (%x. if x < D n then min (g x) ((D n - x)/ 2) \
-\ else if x = D n then min (g (D n)) (ga (D n)) \
-\ else min (ga x) ((x - D n)/ 2)) (D, p) |] \
-\ ==> fine ga (%x. D(x + n),%x. p(x + n))";
-by (auto_tac (claset(),simpset() addsimps [fine_def,gauge_def]));
-by (dres_inst_tac [("x","na + n")] spec 1);
-by (forw_inst_tac [("n","n")] (tpart_partition RS better_lemma_psize_right_eq) 1);
-by Auto_tac;
-by (arith_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [tpart_def]) 1 THEN Step_tac 1);
-by (subgoal_tac "D n <= p (na + n)" 1);
-by (dres_inst_tac [("y","p (na + n)")] real_le_imp_less_or_eq 1);
-by (Step_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [split_if]) 1);
-by (Asm_full_simp_tac 1);
-by (dtac less_le_trans 1 THEN assume_tac 1);
-by (rotate_tac 5 1);
-by (dres_inst_tac [("x","na + n")] spec 1 THEN Step_tac 1);
-by (rtac real_le_trans 1 THEN assume_tac 2);
-by (case_tac "na = 0" 1 THEN Auto_tac);
-by (rtac (partition_lt_gen RS order_less_imp_le) 1);
-by Auto_tac;
-by (arith_tac 1);
-qed "fine_right1";
-
-Goalw [rsum_def]
- "rsum (D, p) (%x. f x + g x) = rsum (D, p) f + rsum(D, p) g";
-by (auto_tac (claset(),simpset() addsimps [sumr_add,left_distrib]));
-qed "rsum_add";
-
-(* Bartle/Sherbert: Theorem 10.1.5 p. 278 *)
-Goalw [Integral_def]
- "[| a <= b; Integral(a,b) f k1; Integral(a,b) g k2 |] \
-\ ==> Integral(a,b) (%x. f x + g x) (k1 + k2)";
-by Auto_tac;
-by (REPEAT(dres_inst_tac [("x","e/2")] spec 1));
-by Auto_tac;
-by (dtac gauge_min 1 THEN assume_tac 1);
-by (res_inst_tac [("x","(%x. if ga x < gaa x then ga x else gaa x)")] exI 1);
-by Auto_tac;
-by (dtac fine_min 1);
-by (REPEAT(dtac spec 1) THEN Auto_tac);
-by (dres_inst_tac [("a","abs (rsum (D, p) f - k1)* 2"),
- ("c","abs (rsum (D, p) g - k2) * 2")]
- add_strict_mono 1 THEN assume_tac 1);
-by (auto_tac (claset(),HOL_ss addsimps [rsum_add,left_distrib RS sym,
- mult_2_right RS sym,real_mult_less_iff1,CLAIM "(0::real) < 2"]));
-by (arith_tac 1);
-qed "Integral_add_fun";
-
-Goal "[| partition(a,b) D; r < psize D |] ==> 0 < D (Suc r) - D r";
-by (auto_tac (claset(),simpset() addsimps [partition]));
-qed "partition_lt_gen2";
-
-Goalw [tpart_def]
- "[| ALL x. a <= x & x <= b --> f x <= g x; \
-\ tpart(a,b) (D,p) \
-\ |] ==> ALL n. n <= psize D --> f (p n) <= g (p n)";
-by (Auto_tac THEN ftac (partition RS iffD1) 1);
-by Auto_tac;
-by (dres_inst_tac [("x","p n")] spec 1);
-by Auto_tac;
-by (case_tac "n = 0" 1);
-by (rtac (partition_lt_gen RS order_less_le_trans RS order_less_imp_le) 2);
-by Auto_tac;
-by (dtac le_imp_less_or_eq 1 THEN Auto_tac);
-by (dres_inst_tac [("x","psize D")] spec 2 THEN Auto_tac);
-by (dres_inst_tac [("r","Suc n")] partition_ub 1);
-by (dres_inst_tac [("x","n")] spec 1);
-by Auto_tac;
-qed "lemma_Integral_le";
-
-Goalw [rsum_def]
- "[| ALL x. a <= x & x <= b --> f x <= g x; \
-\ tpart(a,b) (D,p) \
-\ |] ==> rsum(D,p) f <= rsum(D,p) g";
-by (auto_tac (claset() addSIs [sumr_le2] addDs
- [tpart_partition RS partition_lt_gen2] addSDs
- [lemma_Integral_le],simpset()));
-qed "lemma_Integral_rsum_le";
-
-Goalw [Integral_def]
- "[| a <= b; \
-\ ALL x. a <= x & x <= b --> f(x) <= g(x); \
-\ Integral(a,b) f k1; Integral(a,b) g k2 \
-\ |] ==> k1 <= k2";
-by Auto_tac;
-by (rotate_tac 2 1);
-by (dres_inst_tac [("x","abs(k1 - k2)/2")] spec 1);
-by (dres_inst_tac [("x","abs(k1 - k2)/2")] spec 1);
-by Auto_tac;
-by (dtac gauge_min 1 THEN assume_tac 1);
-by (dres_inst_tac [("g","%x. if ga x < gaa x then ga x else gaa x")]
- partition_exists 1 THEN assume_tac 1);
-by Auto_tac;
-by (dtac fine_min 1);
-by (dres_inst_tac [("x","D")] spec 1 THEN dres_inst_tac [("x","D")] spec 1);
-by (dres_inst_tac [("x","p")] spec 1 THEN dres_inst_tac [("x","p")] spec 1);
-by Auto_tac;
-by (ftac lemma_Integral_rsum_le 1 THEN assume_tac 1);
-by (subgoal_tac
- "abs((rsum(D,p) f - k1) - (rsum(D,p) g - k2)) < abs(k1 - k2)" 1);
-by (arith_tac 1);
-by (dtac add_strict_mono 1 THEN assume_tac 1);
-by (auto_tac (claset(),HOL_ss addsimps [left_distrib RS sym,
- mult_2_right RS sym,real_mult_less_iff1,CLAIM "(0::real) < 2"]));
-by (arith_tac 1);
-qed "Integral_le";
-
-Goalw [Integral_def]
- "(EX k. Integral(a,b) f k) ==> \
-\ (ALL e. 0 < e --> \
-\ (EX g. gauge (%x. a <= x & x <= b) g & \
-\ (ALL D1 D2 p1 p2. \
-\ tpart(a,b) (D1, p1) & fine g (D1,p1) & \
-\ tpart(a,b) (D2, p2) & fine g (D2,p2) --> \
-\ abs(rsum(D1,p1) f - rsum(D2,p2) f) < e)))";
-by Auto_tac;
-by (dres_inst_tac [("x","e/2")] spec 1);
-by Auto_tac;
-by (rtac exI 1 THEN Auto_tac);
-by (forw_inst_tac [("x","D1")] spec 1);
-by (forw_inst_tac [("x","D2")] spec 1);
-by (REPEAT(dtac spec 1) THEN Auto_tac);
-by (thin_tac "0 < e" 1);
-by (dtac add_strict_mono 1 THEN assume_tac 1);
-by (auto_tac (claset(),HOL_ss addsimps [left_distrib RS sym,
- mult_2_right RS sym,real_mult_less_iff1,CLAIM "(0::real) < 2"]));
-by (arith_tac 1);
-qed "Integral_imp_Cauchy";
-
-Goalw [Cauchy_def]
- "Cauchy X = \
-\ (ALL j. (EX M. ALL m n. M <= m & M <= n --> \
-\ abs (X m + - X n) < inverse(real (Suc j))))";
-by Auto_tac;
-by (dtac reals_Archimedean 1);
-by (Step_tac 1);
-by (dres_inst_tac [("x","n")] spec 1);
-by Auto_tac;
-by (res_inst_tac [("x","M")] exI 1);
-by Auto_tac;
-by (dres_inst_tac [("x","m")] spec 1);
-by (dres_inst_tac [("x","na")] spec 1);
-by Auto_tac;
-qed "Cauchy_iff2";
-
-Goal "[| a <= b; ALL n. gauge (%x. a <= x & x <= b) (fa n) |] \
-\ ==> ALL n. EX D p. tpart (a, b) (D, p) & fine (fa n) (D, p)";
-by (Step_tac 1);
-by (rtac partition_exists 1 THEN Auto_tac);
-qed "partition_exists2";
-
-Goal "[| a <= b; ALL c. a <= c & c <= b --> f' c <= g' c; \
-\ ALL x. DERIV f x :> f' x; ALL x. DERIV g x :> g' x \
-\ |] ==> f b - f a <= g b - g a";
-by (rtac Integral_le 1);
-by (assume_tac 1);
-by (rtac FTC1 2);
-by (rtac FTC1 4);
-by Auto_tac;
-qed "monotonic_anti_derivative";
--- a/src/HOL/Hyperreal/Integration.thy Fri Jul 30 10:44:42 2004 +0200
+++ b/src/HOL/Hyperreal/Integration.thy Fri Jul 30 18:37:58 2004 +0200
@@ -1,58 +1,910 @@
(* Title : Integration.thy
Author : Jacques D. Fleuriot
Copyright : 2000 University of Edinburgh
- Description : Theory of integration (cf. Harrison's HOL development)
+ Conversion to Isar and new proofs by Lawrence C Paulson, 2004
*)
-Integration = MacLaurin +
+header{*Theory of Integration*}
+theory Integration = MacLaurin:
+
+text{*We follow John Harrison in formalizing the Gauge integral.*}
constdefs
-
-(* ------------------------------------------------------------------------ *)
-(* Partitions and tagged partitions etc. *)
-(* ------------------------------------------------------------------------ *)
+ --{*Partitions and tagged partitions etc.*}
partition :: "[(real*real),nat => real] => bool"
- "partition == %(a,b) D. ((D 0 = a) &
- (EX N. ((ALL n. n < N --> D(n) < D(Suc n)) &
- (ALL n. N <= n --> (D(n) = b)))))"
-
- psize :: (nat => real) => nat
- "psize D == @N. (ALL n. n < N --> D(n) < D(Suc n)) &
- (ALL n. N <= n --> (D(n) = D(N)))"
-
+ "partition == %(a,b) D. ((D 0 = a) &
+ (\<exists>N. ((\<forall>n. n < N --> D(n) < D(Suc n)) &
+ (\<forall>n. N \<le> n --> (D(n) = b)))))"
+
+ psize :: "(nat => real) => nat"
+ "psize D == @N. (\<forall>n. n < N --> D(n) < D(Suc n)) &
+ (\<forall>n. N \<le> n --> (D(n) = D(N)))"
+
tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool"
"tpart == %(a,b) (D,p). partition(a,b) D &
- (ALL n. D(n) <= p(n) & p(n) <= D(Suc n))"
+ (\<forall>n. D(n) \<le> p(n) & p(n) \<le> D(Suc n))"
-(* ------------------------------------------------------------------------ *)
-(* Gauges and gauge-fine divisions *)
-(* ------------------------------------------------------------------------ *)
-
- gauge :: [real => bool, real => real] => bool
- "gauge E g == ALL x. E x --> 0 < g(x)"
+ --{*Gauges and gauge-fine divisions*}
+
+ gauge :: "[real => bool, real => real] => bool"
+ "gauge E g == \<forall>x. E x --> 0 < g(x)"
fine :: "[real => real, ((nat => real)*(nat => real))] => bool"
- "fine == % g (D,p). ALL n. n < (psize D) --> D(Suc n) - D(n) < g(p n)"
+ "fine == % g (D,p). \<forall>n. n < (psize D) --> D(Suc n) - D(n) < g(p n)"
-(* ------------------------------------------------------------------------ *)
-(* Riemann sum *)
-(* ------------------------------------------------------------------------ *)
+ --{*Riemann sum*}
rsum :: "[((nat=>real)*(nat=>real)),real=>real] => real"
"rsum == %(D,p) f. sumr 0 (psize(D)) (%n. f(p n) * (D(Suc n) - D(n)))"
-(* ------------------------------------------------------------------------ *)
-(* Gauge integrability (definite) *)
-(* ------------------------------------------------------------------------ *)
+ --{*Gauge integrability (definite)*}
Integral :: "[(real*real),real=>real,real] => bool"
- "Integral == %(a,b) f k. ALL e. 0 < e -->
- (EX g. gauge(%x. a <= x & x <= b) g &
- (ALL D p. tpart(a,b) (D,p) & fine(g)(D,p) -->
- abs(rsum(D,p) f - k) < e))"
-end
+ "Integral == %(a,b) f k. \<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 - k\<bar> < e))"
+
+
+lemma partition_zero [simp]: "a = b ==> psize (%n. if n = 0 then a else b) = 0"
+by (auto simp add: psize_def)
+
+lemma partition_one [simp]: "a < b ==> psize (%n. if n = 0 then a else b) = 1"
+apply (simp add: psize_def)
+apply (rule some_equality, auto)
+apply (drule_tac x = 1 in spec, auto)
+done
+
+lemma partition_single [simp]:
+ "a \<le> b ==> partition(a,b)(%n. if n = 0 then a else b)"
+by (auto simp add: partition_def order_le_less)
+
+lemma partition_lhs: "partition(a,b) D ==> (D(0) = a)"
+by (simp add: partition_def)
+
+lemma partition:
+ "(partition(a,b) D) =
+ ((D 0 = a) &
+ (\<forall>n. n < (psize D) --> D n < D(Suc n)) &
+ (\<forall>n. (psize D) \<le> n --> (D n = b)))"
+apply (simp add: partition_def, auto)
+apply (subgoal_tac [!] "psize D = N", auto)
+apply (simp_all (no_asm) add: psize_def)
+apply (rule_tac [!] some_equality, blast)
+ prefer 2 apply blast
+apply (rule_tac [!] ccontr)
+apply (simp_all add: linorder_neq_iff, safe)
+apply (drule_tac x = Na in spec)
+apply (rotate_tac 3)
+apply (drule_tac x = "Suc Na" in spec, simp)
+apply (rotate_tac 2)
+apply (drule_tac x = N in spec, simp)
+apply (drule_tac x = Na in spec)
+apply (drule_tac x = "Suc Na" and P = "%n. Na \<le> n \<longrightarrow> D n = D Na" in spec, auto)
+done
+
+lemma partition_rhs: "partition(a,b) D ==> (D(psize D) = b)"
+by (simp add: partition)
+
+lemma partition_rhs2: "[|partition(a,b) D; psize D \<le> n |] ==> (D n = b)"
+by (simp add: partition)
+
+lemma lemma_partition_lt_gen [rule_format]:
+ "partition(a,b) D & m + Suc d \<le> n & n \<le> (psize D) --> D(m) < D(m + Suc d)"
+apply (induct_tac "d", auto simp add: partition)
+apply (blast dest: Suc_le_lessD intro: less_le_trans order_less_trans)
+done
+
+lemma less_eq_add_Suc: "m < n ==> \<exists>d. n = m + Suc d"
+by (auto simp add: less_iff_Suc_add)
+
+lemma partition_lt_gen:
+ "[|partition(a,b) D; m < n; n \<le> (psize D)|] ==> D(m) < D(n)"
+by (auto dest: less_eq_add_Suc intro: lemma_partition_lt_gen)
+
+lemma partition_lt: "partition(a,b) D ==> n < (psize D) ==> D(0) < D(Suc n)"
+apply (induct "n")
+apply (auto simp add: partition)
+done
+
+lemma partition_le: "partition(a,b) D ==> a \<le> b"
+apply (frule partition [THEN iffD1], safe)
+apply (rotate_tac 2)
+apply (drule_tac x = "psize D" in spec, safe)
+apply (rule ccontr)
+apply (case_tac "psize D = 0", safe)
+apply (drule_tac [2] n = "psize D - 1" in partition_lt, auto)
+done
+
+lemma partition_gt: "[|partition(a,b) D; n < (psize D)|] ==> D(n) < D(psize D)"
+by (auto intro: partition_lt_gen)
+
+lemma partition_eq: "partition(a,b) D ==> ((a = b) = (psize D = 0))"
+apply (frule partition [THEN iffD1], safe)
+apply (rotate_tac 2)
+apply (drule_tac x = "psize D" in spec)
+apply (rule ccontr)
+apply (drule_tac n = "psize D - 1" in partition_lt)
+prefer 3 apply (blast, auto)
+done
+
+lemma partition_lb: "partition(a,b) D ==> a \<le> D(r)"
+apply (frule partition [THEN iffD1], safe)
+apply (induct_tac "r")
+apply (cut_tac [2] y = "Suc n" and x = "psize D" in linorder_le_less_linear, safe)
+ apply (blast intro: order_trans partition_le)
+apply (drule_tac x = n in spec)
+apply (best intro: order_less_trans order_trans order_less_imp_le)
+done
+
+lemma partition_lb_lt: "[| partition(a,b) D; psize D ~= 0 |] ==> a < D(Suc n)"
+apply (rule_tac t = a in partition_lhs [THEN subst], assumption)
+apply (cut_tac x = "Suc n" and y = "psize D" in linorder_le_less_linear)
+apply (frule partition [THEN iffD1], safe)
+ apply (blast intro: partition_lt less_le_trans)
+apply (rotate_tac 3)
+apply (drule_tac x = "Suc n" in spec)
+apply (erule impE)
+apply (erule less_imp_le)
+apply (frule partition_rhs)
+apply (drule partition_gt, assumption)
+apply (simp (no_asm_simp))
+done
+
+lemma partition_ub: "partition(a,b) D ==> D(r) \<le> b"
+apply (frule partition [THEN iffD1])
+apply (cut_tac x = "psize D" and y = r in linorder_le_less_linear, safe, blast)
+apply (subgoal_tac "\<forall>x. D ((psize D) - x) \<le> b")
+apply (rotate_tac 4)
+apply (drule_tac x = "psize D - r" in spec)
+apply (subgoal_tac "psize D - (psize D - r) = r")
+apply simp
+apply arith
+apply safe
+apply (induct_tac "x")
+apply (simp (no_asm), blast)
+apply (case_tac "psize D - Suc n = 0")
+apply (erule_tac V = "\<forall>n. psize D \<le> n --> D n = b" in thin_rl)
+apply (simp (no_asm_simp) add: partition_le)
+apply (rule order_trans)
+ prefer 2 apply assumption
+apply (subgoal_tac "psize D - n = Suc (psize D - Suc n)")
+ prefer 2 apply arith
+apply (drule_tac x = "psize D - Suc n" in spec)
+apply (erule_tac V = "\<forall>n. psize D \<le> n --> D n = b" in thin_rl, simp)
+done
+
+lemma partition_ub_lt: "[| partition(a,b) D; n < psize D |] ==> D(n) < b"
+by (blast intro: partition_rhs [THEN subst] partition_gt)
+
+lemma lemma_partition_append1:
+ "[| partition (a, b) D1; partition (b, c) D2 |]
+ ==> (\<forall>n.
+ n < psize D1 + psize D2 -->
+ (if n < psize D1 then D1 n else D2 (n - psize D1))
+ < (if Suc n < psize D1 then D1 (Suc n)
+ else D2 (Suc n - psize D1))) &
+ (\<forall>n.
+ psize D1 + psize D2 \<le> n -->
+ (if n < psize D1 then D1 n else D2 (n - psize D1)) =
+ (if psize D1 + psize D2 < psize D1 then D1 (psize D1 + psize D2)
+ else D2 (psize D1 + psize D2 - psize D1)))"
+apply safe
+apply (auto intro: partition_lt_gen)
+apply (subgoal_tac "psize D1 = Suc n")
+apply (auto intro!: partition_lt_gen simp add: partition_lhs partition_ub_lt)
+apply (auto intro!: partition_rhs2 simp add: partition_rhs
+ split: nat_diff_split)
+done
+
+lemma lemma_psize1:
+ "[| partition (a, b) D1; partition (b, c) D2; N < psize D1 |]
+ ==> D1(N) < D2 (psize D2)"
+apply (rule_tac y = "D1 (psize D1) " in order_less_le_trans)
+apply (erule partition_gt, assumption)
+apply (auto simp add: partition_rhs partition_le)
+done
+
+lemma lemma_partition_append2:
+ "[| partition (a, b) D1; partition (b, c) D2 |]
+ ==> psize (%n. if n < psize D1 then D1 n else D2 (n - psize D1)) =
+ psize D1 + psize D2"
+apply (rule_tac D2 = "%n. if n < psize D1 then D1 n else D2 (n - psize D1) "
+ in psize_def [THEN meta_eq_to_obj_eq, THEN ssubst])
+apply (rule some1_equality)
+prefer 2 apply (blast intro!: lemma_partition_append1)
+apply (rule ex1I, rule lemma_partition_append1, auto)
+apply (rule ccontr)
+apply (simp add: linorder_neq_iff, safe)
+apply (rotate_tac 3)
+apply (drule_tac x = "psize D1 + psize D2" in spec, auto)
+apply (case_tac "N < psize D1")
+apply (auto dest: lemma_psize1)
+apply (subgoal_tac "N - psize D1 < psize D2")
+ prefer 2 apply arith
+apply (drule_tac a = b and b = c in partition_gt, auto)
+apply (drule_tac x = "psize D1 + psize D2" in spec)
+apply (auto simp add: partition_rhs2)
+done
+
+lemma tpart_eq_lhs_rhs:
+"[|psize D = 0; tpart(a,b) (D,p)|] ==> a = b"
+apply (simp add: tpart_def)
+apply (auto simp add: partition_eq)
+done
+
+lemma tpart_partition: "tpart(a,b) (D,p) ==> partition(a,b) D"
+by (simp add: tpart_def)
+
+lemma partition_append:
+ "[| tpart(a,b) (D1,p1); fine(g) (D1,p1);
+ tpart(b,c) (D2,p2); fine(g) (D2,p2) |]
+ ==> \<exists>D p. tpart(a,c) (D,p) & fine(g) (D,p)"
+apply (rule_tac x = "%n. if n < psize D1 then D1 n else D2 (n - psize D1)"
+ in exI)
+apply (rule_tac x = "%n. if n < psize D1 then p1 n else p2 (n - psize D1)"
+ in exI)
+apply (case_tac "psize D1 = 0")
+apply (auto dest: tpart_eq_lhs_rhs)
+ prefer 2
+apply (simp add: fine_def
+ lemma_partition_append2 [OF tpart_partition tpart_partition])
+ --{*But must not expand @{term fine} in other subgoals*}
+apply auto
+apply (subgoal_tac "psize D1 = Suc n")
+ prefer 2 apply arith
+apply (drule tpart_partition [THEN partition_rhs])
+apply (drule tpart_partition [THEN partition_lhs])
+apply (auto split: nat_diff_split)
+apply (auto simp add: tpart_def)
+defer 1
+ apply (subgoal_tac "psize D1 = Suc n")
+ prefer 2 apply arith
+ apply (drule partition_rhs)
+ apply (drule partition_lhs, auto)
+apply (simp split: nat_diff_split)
+apply (subst partition)
+apply (subst lemma_partition_append2)
+apply (rule_tac [3] conjI)
+apply (drule_tac [4] lemma_partition_append1)
+apply (auto simp add: partition_lhs partition_rhs)
+done
+
+text{*We can always find a division which is fine wrt any gauge*}
+
+lemma partition_exists:
+ "[| a \<le> b; gauge(%x. a \<le> x & x \<le> b) g |]
+ ==> \<exists>D p. tpart(a,b) (D,p) & fine g (D,p)"
+apply (cut_tac P = "%(u,v). a \<le> u & v \<le> b -->
+ (\<exists>D p. tpart (u,v) (D,p) & fine (g) (D,p))"
+ in lemma_BOLZANO2)
+apply safe
+apply (blast intro: real_le_trans)+
+apply (auto intro: partition_append)
+apply (case_tac "a \<le> x & x \<le> b")
+apply (rule_tac [2] x = 1 in exI, auto)
+apply (rule_tac x = "g x" in exI)
+apply (auto simp add: gauge_def)
+apply (rule_tac x = "%n. if n = 0 then aa else ba" in exI)
+apply (rule_tac x = "%n. if n = 0 then x else ba" in exI)
+apply (auto simp add: tpart_def fine_def)
+done
+
+text{*Lemmas about combining gauges*}
+
+lemma gauge_min:
+ "[| gauge(E) g1; gauge(E) g2 |]
+ ==> gauge(E) (%x. if g1(x) < g2(x) then g1(x) else g2(x))"
+by (simp add: gauge_def)
+
+lemma fine_min:
+ "fine (%x. if g1(x) < g2(x) then g1(x) else g2(x)) (D,p)
+ ==> fine(g1) (D,p) & fine(g2) (D,p)"
+by (auto simp add: fine_def split: split_if_asm)
+
+
+text{*The integral is unique if it exists*}
+
+lemma Integral_unique:
+ "[| a \<le> b; Integral(a,b) f k1; Integral(a,b) f k2 |] ==> k1 = k2"
+apply (simp add: Integral_def)
+apply (drule_tac x = "\<bar>k1 - k2\<bar> /2" in spec)+
+apply auto
+apply (drule gauge_min, assumption)
+apply (drule_tac g = "%x. if g x < ga x then g x else ga x"
+ in partition_exists, assumption, auto)
+apply (drule fine_min)
+apply (drule spec)+
+apply auto
+apply (subgoal_tac "abs ((rsum (D,p) f - k2) - (rsum (D,p) f - k1)) < \<bar>k1 - k2\<bar> ")
+apply arith
+apply (drule add_strict_mono, assumption)
+apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
+ mult_less_cancel_right, arith)
+done
+
+lemma Integral_zero [simp]: "Integral(a,a) f 0"
+apply (auto simp add: Integral_def)
+apply (rule_tac x = "%x. 1" in exI)
+apply (auto dest: partition_eq simp add: gauge_def tpart_def rsum_def)
+done
+
+lemma sumr_partition_eq_diff_bounds [simp]:
+ "sumr 0 m (%n. D (Suc n) - D n) = D(m) - D 0"
+by (induct_tac "m", auto)
+
+lemma Integral_eq_diff_bounds: "a \<le> b ==> Integral(a,b) (%x. 1) (b - a)"
+apply (drule real_le_imp_less_or_eq, auto)
+apply (auto simp add: rsum_def Integral_def)
+apply (rule_tac x = "%x. b - a" in exI)
+apply (auto simp add: gauge_def abs_interval_iff tpart_def partition)
+done
+
+lemma Integral_mult_const: "a \<le> b ==> Integral(a,b) (%x. c) (c*(b - a))"
+apply (drule real_le_imp_less_or_eq, auto)
+apply (auto simp add: rsum_def Integral_def)
+apply (rule_tac x = "%x. b - a" in exI)
+apply (auto simp add: sumr_mult [symmetric] gauge_def abs_interval_iff
+ right_diff_distrib [symmetric] partition tpart_def)
+done
+
+lemma Integral_mult:
+ "[| a \<le> b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)"
+apply (drule real_le_imp_less_or_eq)
+apply (auto dest: Integral_unique [OF real_le_refl Integral_zero])
+apply (auto simp add: rsum_def Integral_def sumr_mult [symmetric] real_mult_assoc)
+apply (rule_tac a2 = c in abs_ge_zero [THEN real_le_imp_less_or_eq, THEN disjE])
+ prefer 2 apply force
+apply (drule_tac x = "e/abs c" in spec, auto)
+apply (simp add: zero_less_mult_iff divide_inverse)
+apply (rule exI, auto)
+apply (drule spec)+
+apply auto
+apply (rule_tac z1 = "inverse (abs c) " in real_mult_less_iff1 [THEN iffD1])
+apply (auto simp add: divide_inverse [symmetric] right_diff_distrib [symmetric])
+done
+
+text{*Fundamental theorem of calculus (Part I)*}
+
+text{*"Straddle Lemma" : Swartz & Thompson: AMM 95(7) 1988 *}
+
+lemma choiceP: "\<forall>x. P(x) --> (\<exists>y. Q x y) ==> \<exists>f. (\<forall>x. P(x) --> Q x (f x))"
+by meson
+
+lemma choiceP2: "\<forall>x. P(x) --> (\<exists>y. R(y) & (\<exists>z. Q x y z)) ==>
+ \<exists>f fa. (\<forall>x. P(x) --> R(f x) & Q x (f x) (fa x))"
+by meson
+
+(*UNUSED
+lemma choice2: "\<forall>x. (\<exists>y. R(y) & (\<exists>z. Q x y z)) ==>
+ \<exists>f fa. (\<forall>x. R(f x) & Q x (f x) (fa x))"
+*)
+
+
+(* new simplifications e.g. (y < x/n) = (y * n < x) are a real nuisance
+ they break the original proofs and make new proofs longer! *)
+lemma strad1:
+ "\<lbrakk>\<forall>xa::real. xa \<noteq> x \<and> \<bar>xa + - x\<bar> < s \<longrightarrow>
+ \<bar>(f xa - f x) / (xa - x) + - f' x\<bar> * 2 < e;
+ 0 < e; a \<le> x; x \<le> b; 0 < s\<rbrakk>
+ \<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>"
+apply auto
+apply (case_tac "0 < \<bar>z - x\<bar> ")
+ prefer 2 apply (simp add: zero_less_abs_iff)
+apply (drule_tac x = z in spec)
+apply (rule_tac z1 = "\<bar>inverse (z - x)\<bar>"
+ in real_mult_le_cancel_iff2 [THEN iffD1])
+ apply simp
+apply (simp del: abs_inverse abs_mult add: abs_mult [symmetric]
+ mult_assoc [symmetric])
+apply (subgoal_tac "inverse (z - x) * (f z - f x - f' x * (z - x))
+ = (f z - f x) / (z - x) - f' x")
+ apply (simp add: abs_mult [symmetric] mult_ac diff_minus)
+apply (subst mult_commute)
+apply (simp add: left_distrib diff_minus)
+apply (simp add: mult_assoc divide_inverse)
+apply (simp add: left_distrib)
+done
+
+lemma lemma_straddle:
+ "[| \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x); 0 < e |]
+ ==> \<exists>g. gauge(%x. a \<le> x & x \<le> b) g &
+ (\<forall>x u v. a \<le> u & u \<le> x & x \<le> v & v \<le> b & (v - u) < g(x)
+ --> abs((f(v) - f(u)) - (f'(x) * (v - u))) \<le> e * (v - u))"
+apply (simp add: gauge_def)
+apply (subgoal_tac "\<forall>x. a \<le> x & x \<le> b -->
+ (\<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)))")
+apply (drule choiceP, auto)
+apply (drule spec, auto)
+apply (auto simp add: DERIV_iff2 LIM_def)
+apply (drule_tac x = "e/2" in spec, auto)
+apply (frule strad1, assumption+)
+apply (rule_tac x = s in exI, auto)
+apply (rule_tac x = u and y = v in linorder_cases, auto)
+apply (rule_tac j = "abs ((f (v) - f (x)) - (f' (x) * (v - x))) + abs ((f (x) - f (u)) - (f' (x) * (x - u)))"
+ in real_le_trans)
+apply (rule abs_triangle_ineq [THEN [2] real_le_trans])
+apply (simp add: right_diff_distrib, arith)
+apply (rule_tac t = "e* (v - u) " in real_sum_of_halves [THEN subst])
+apply (rule add_mono)
+apply (rule_tac j = " (e / 2) * \<bar>v - x\<bar> " in real_le_trans)
+ prefer 2 apply simp apply arith
+apply (erule_tac [!]
+ V= "\<forall>xa. xa ~= x & \<bar>xa + - x\<bar> < s --> \<bar>(f xa - f x) / (xa - x) + - f' x\<bar> * 2 < e"
+ in thin_rl)
+apply (drule_tac x = v in spec, auto, arith)
+apply (drule_tac x = u in spec, auto, arith)
+apply (subgoal_tac "\<bar>f u - f x - f' x * (u - x)\<bar> = \<bar>f x - f u - f' x * (x - u)\<bar>")
+apply (rule order_trans)
+apply (auto simp add: abs_le_interval_iff)
+apply (simp add: right_diff_distrib, arith)
+done
+
+lemma FTC1: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |]
+ ==> Integral(a,b) f' (f(b) - f(a))"
+apply (drule real_le_imp_less_or_eq, auto)
+apply (auto simp add: Integral_def)
+apply (rule ccontr)
+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))")
+apply (rotate_tac 3)
+apply (drule_tac x = "e/2" in spec, auto)
+apply (drule spec, auto)
+apply ((drule spec)+, auto)
+apply (drule_tac e = "ea/ (b - a) " in lemma_straddle)
+apply (auto simp add: zero_less_divide_iff)
+apply (rule exI)
+apply (auto simp add: tpart_def rsum_def)
+apply (subgoal_tac "sumr 0 (psize D) (%n. f (D (Suc n)) - f (D n)) = f b - f a")
+ prefer 2
+ apply (cut_tac D = "%n. f (D n) " and m = "psize D"
+ in sumr_partition_eq_diff_bounds)
+ apply (simp add: partition_lhs partition_rhs)
+apply (drule sym, simp)
+apply (simp (no_asm) add: sumr_diff)
+apply (rule sumr_rabs [THEN real_le_trans])
+apply (subgoal_tac "ea = sumr 0 (psize D) (%n. (ea / (b - a)) * (D (Suc n) - (D n))) ")
+apply (simp add: abs_minus_commute)
+apply (rule_tac t = ea in ssubst, assumption)
+apply (rule sumr_le2)
+apply (rule_tac [2] sumr_mult [THEN subst])
+apply (auto simp add: partition_rhs partition_lhs partition_lb partition_ub
+ fine_def)
+done
+lemma Integral_subst: "[| Integral(a,b) f k1; k2=k1 |] ==> Integral(a,b) f k2"
+by simp
+
+lemma Integral_add:
+ "[| a \<le> b; b \<le> c; Integral(a,b) f' k1; Integral(b,c) f' k2;
+ \<forall>x. a \<le> x & x \<le> c --> DERIV f x :> f' x |]
+ ==> Integral(a,c) f' (k1 + k2)"
+apply (rule FTC1 [THEN Integral_subst], auto)
+apply (frule FTC1, auto)
+apply (frule_tac a = b in FTC1, auto)
+apply (drule_tac x = x in spec, auto)
+apply (drule_tac ?k2.0 = "f b - f a" in Integral_unique)
+apply (drule_tac [3] ?k2.0 = "f c - f b" in Integral_unique, auto)
+done
+
+lemma partition_psize_Least:
+ "partition(a,b) D ==> psize D = (LEAST n. D(n) = b)"
+apply (auto intro!: Least_equality [symmetric] partition_rhs)
+apply (rule ccontr)
+apply (drule partition_ub_lt)
+apply (auto simp add: linorder_not_less [symmetric])
+done
+
+lemma lemma_partition_bounded: "partition (a, c) D ==> ~ (\<exists>n. c < D(n))"
+apply safe
+apply (drule_tac r = n in partition_ub, auto)
+done
+
+lemma lemma_partition_eq:
+ "partition (a, c) D ==> D = (%n. if D n < c then D n else c)"
+apply (rule ext, auto)
+apply (auto dest!: lemma_partition_bounded)
+apply (drule_tac x = n in spec, auto)
+done
+
+lemma lemma_partition_eq2:
+ "partition (a, c) D ==> D = (%n. if D n \<le> c then D n else c)"
+apply (rule ext, auto)
+apply (auto dest!: lemma_partition_bounded)
+apply (drule_tac x = n in spec, auto)
+done
+
+lemma partition_lt_Suc:
+ "[| partition(a,b) D; n < psize D |] ==> D n < D (Suc n)"
+by (auto simp add: partition)
+
+lemma tpart_tag_eq: "tpart(a,c) (D,p) ==> p = (%n. if D n < c then p n else c)"
+apply (rule ext)
+apply (auto simp add: tpart_def)
+apply (drule linorder_not_less [THEN iffD1])
+apply (drule_tac r = "Suc n" in partition_ub)
+apply (drule_tac x = n in spec, auto)
+done
+
+subsection{*Lemmas for Additivity Theorem of Gauge Integral*}
+
+lemma lemma_additivity1:
+ "[| a \<le> D n; D n < b; partition(a,b) D |] ==> n < psize D"
+by (auto simp add: partition linorder_not_less [symmetric])
+
+lemma lemma_additivity2: "[| a \<le> D n; partition(a,D n) D |] ==> psize D \<le> n"
+apply (rule ccontr, drule not_leE)
+apply (frule partition [THEN iffD1], safe)
+apply (frule_tac r = "Suc n" in partition_ub)
+apply (auto dest!: spec)
+done
+
+lemma partition_eq_bound:
+ "[| partition(a,b) D; psize D < m |] ==> D(m) = D(psize D)"
+by (auto simp add: partition)
+
+lemma partition_ub2: "[| partition(a,b) D; psize D < m |] ==> D(r) \<le> D(m)"
+by (simp add: partition partition_ub)
+
+lemma tag_point_eq_partition_point:
+ "[| tpart(a,b) (D,p); psize D \<le> m |] ==> p(m) = D(m)"
+apply (simp add: tpart_def, auto)
+apply (drule_tac x = m in spec)
+apply (auto simp add: partition_rhs2)
+done
+
+lemma partition_lt_cancel: "[| partition(a,b) D; D m < D n |] ==> m < n"
+apply (cut_tac m = n and n = "psize D" in less_linear, auto)
+apply (rule ccontr, drule leI, drule le_imp_less_or_eq)
+apply (cut_tac m = m and n = "psize D" in less_linear)
+apply (auto dest: partition_gt)
+apply (drule_tac n = m in partition_lt_gen, auto)
+apply (frule partition_eq_bound)
+apply (drule_tac [2] partition_gt, auto)
+apply (rule ccontr, drule leI, drule le_imp_less_or_eq)
+apply (auto dest: partition_eq_bound)
+apply (rule ccontr, drule leI, drule le_imp_less_or_eq)
+apply (frule partition_eq_bound, assumption)
+apply (drule_tac m = m in partition_eq_bound, auto)
+done
+
+lemma lemma_additivity4_psize_eq:
+ "[| a \<le> D n; D n < b; partition (a, b) D |]
+ ==> psize (%x. if D x < D n then D(x) else D n) = n"
+apply (unfold psize_def)
+apply (frule lemma_additivity1)
+apply (assumption, assumption)
+apply (rule some_equality)
+apply (auto intro: partition_lt_Suc)
+apply (drule_tac n = n in partition_lt_gen)
+apply (assumption, arith, arith)
+apply (cut_tac m = na and n = "psize D" in less_linear)
+apply (auto dest: partition_lt_cancel)
+apply (rule_tac x=N and y=n in linorder_cases)
+apply (drule_tac x = n and P="%m. N \<le> m --> ?f m = ?g m" in spec, auto)
+apply (drule_tac n = n in partition_lt_gen, auto, arith)
+apply (drule_tac x = n in spec)
+apply (simp split: split_if_asm)
+done
+
+lemma lemma_psize_left_less_psize:
+ "partition (a, b) D
+ ==> psize (%x. if D x < D n then D(x) else D n) \<le> psize D"
+apply (frule_tac r = n in partition_ub)
+apply (drule_tac x = "D n" in real_le_imp_less_or_eq)
+apply (auto simp add: lemma_partition_eq [symmetric])
+apply (frule_tac r = n in partition_lb)
+apply (drule lemma_additivity4_psize_eq)
+apply (rule_tac [3] ccontr, auto)
+apply (frule_tac not_leE [THEN [2] partition_eq_bound])
+apply (auto simp add: partition_rhs)
+done
+
+lemma lemma_psize_left_less_psize2:
+ "[| partition(a,b) D; na < psize (%x. if D x < D n then D(x) else D n) |]
+ ==> na < psize D"
+apply (erule_tac lemma_psize_left_less_psize [THEN [2] less_le_trans], assumption)
+done
+
+
+lemma lemma_additivity3:
+ "[| partition(a,b) D; D na < D n; D n < D (Suc na);
+ n < psize D |]
+ ==> False"
+apply (cut_tac m = n and n = "Suc na" in less_linear, auto)
+apply (drule_tac [2] n = n in partition_lt_gen, auto)
+apply (cut_tac m = "psize D" and n = na in less_linear)
+apply (auto simp add: partition_rhs2 less_Suc_eq)
+apply (drule_tac n = na in partition_lt_gen, auto)
+done
+
+lemma psize_const [simp]: "psize (%x. k) = 0"
+by (simp add: psize_def, auto)
+
+lemma lemma_additivity3a:
+ "[| partition(a,b) D; D na < D n; D n < D (Suc na);
+ na < psize D |]
+ ==> False"
+apply (frule_tac m = n in partition_lt_cancel)
+apply (auto intro: lemma_additivity3)
+done
+
+lemma better_lemma_psize_right_eq1:
+ "[| partition(a,b) D; D n < b |] ==> psize (%x. D (x + n)) \<le> psize D - n"
+apply (simp add: psize_def [of "(%x. D (x + n))"]);
+apply (rule_tac a = "psize D - n" in someI2, auto)
+ apply (simp add: partition less_diff_conv)
+ apply (simp add: le_diff_conv)
+ apply (case_tac "psize D \<le> n")
+ apply (simp add: partition_rhs2)
+ apply (simp add: partition linorder_not_le)
+apply (rule ccontr, drule not_leE)
+apply (drule_tac x = "psize D - n" in spec, auto)
+apply (frule partition_rhs, safe)
+apply (frule partition_lt_cancel, assumption)
+apply (drule partition [THEN iffD1], safe)
+apply (subgoal_tac "~ D (psize D - n + n) < D (Suc (psize D - n + n))")
+ apply blast
+apply (drule_tac x = "Suc (psize D)" and P="%n. ?P n \<longrightarrow> D n = D (psize D)"
+ in spec)
+apply (simp (no_asm_simp))
+done
+
+lemma psize_le_n: "partition (a, D n) D ==> psize D \<le> n"
+apply (rule ccontr, drule not_leE)
+apply (frule partition_lt_Suc, assumption)
+apply (frule_tac r = "Suc n" in partition_ub, auto)
+done
+
+lemma better_lemma_psize_right_eq1a:
+ "partition(a,D n) D ==> psize (%x. D (x + n)) \<le> psize D - n"
+apply (simp add: psize_def [of "(%x. D (x + n))"]);
+apply (rule_tac a = "psize D - n" in someI2, auto)
+ apply (simp add: partition less_diff_conv)
+ apply (simp add: le_diff_conv)
+apply (case_tac "psize D \<le> n")
+ apply (force intro: partition_rhs2)
+ apply (simp add: partition linorder_not_le)
+apply (rule ccontr, drule not_leE)
+apply (frule psize_le_n)
+apply (drule_tac x = "psize D - n" in spec, simp)
+apply (drule partition [THEN iffD1], safe)
+apply (drule_tac x = "Suc n" and P="%na. psize D \<le> na \<longrightarrow> D na = D n" in spec, auto)
+done
+
+lemma better_lemma_psize_right_eq:
+ "partition(a,b) D ==> psize (%x. D (x + n)) \<le> psize D - n"
+apply (frule_tac r1 = n in partition_ub [THEN real_le_imp_less_or_eq])
+apply (blast intro: better_lemma_psize_right_eq1a better_lemma_psize_right_eq1)
+done
+
+lemma lemma_psize_right_eq1:
+ "[| partition(a,b) D; D n < b |] ==> psize (%x. D (x + n)) \<le> psize D"
+apply (simp add: psize_def [of "(%x. D (x + n))"]);
+apply (rule_tac a = "psize D - n" in someI2, auto)
+ apply (simp add: partition less_diff_conv)
+ apply (subgoal_tac "n \<le> psize D")
+ apply (simp add: partition le_diff_conv)
+ apply (rule ccontr, drule not_leE)
+ apply (drule_tac less_imp_le [THEN [2] partition_rhs2], auto)
+apply (rule ccontr, drule not_leE)
+apply (drule_tac x = "psize D" in spec)
+apply (simp add: partition)
+done
+
+(* should be combined with previous theorem; also proof has redundancy *)
+lemma lemma_psize_right_eq1a:
+ "partition(a,D n) D ==> psize (%x. D (x + n)) \<le> psize D"
+apply (simp add: psize_def [of "(%x. D (x + n))"]);
+apply (rule_tac a = "psize D - n" in someI2, auto)
+ apply (simp add: partition less_diff_conv)
+ apply (case_tac "psize D \<le> n")
+ apply (force intro: partition_rhs2 simp add: le_diff_conv)
+ apply (simp add: partition le_diff_conv)
+apply (rule ccontr, drule not_leE)
+apply (drule_tac x = "psize D" in spec)
+apply (simp add: partition)
+done
+
+lemma lemma_psize_right_eq:
+ "[| partition(a,b) D |] ==> psize (%x. D (x + n)) \<le> psize D"
+apply (frule_tac r1 = n in partition_ub [THEN real_le_imp_less_or_eq])
+apply (blast intro: lemma_psize_right_eq1a lemma_psize_right_eq1)
+done
+
+lemma tpart_left1:
+ "[| a \<le> D n; tpart (a, b) (D, p) |]
+ ==> tpart(a, D n) (%x. if D x < D n then D(x) else D n,
+ %x. if D x < D n then p(x) else D n)"
+apply (frule_tac r = n in tpart_partition [THEN partition_ub])
+apply (drule_tac x = "D n" in real_le_imp_less_or_eq)
+apply (auto simp add: tpart_partition [THEN lemma_partition_eq, symmetric] tpart_tag_eq [symmetric])
+apply (frule_tac tpart_partition [THEN [3] lemma_additivity1])
+apply (auto simp add: tpart_def)
+apply (drule_tac [2] linorder_not_less [THEN iffD1, THEN real_le_imp_less_or_eq], auto)
+ prefer 3
+ apply (drule linorder_not_less [THEN iffD1])
+ apply (drule_tac x=na in spec, arith)
+ prefer 2 apply (blast dest: lemma_additivity3)
+apply (frule lemma_additivity4_psize_eq)
+apply (assumption+)
+apply (rule partition [THEN iffD2])
+apply (frule partition [THEN iffD1])
+apply (auto intro: partition_lt_gen)
+apply (drule_tac n = n in partition_lt_gen)
+apply (assumption, arith, blast)
+apply (drule partition_lt_cancel, auto)
+done
+
+lemma fine_left1:
+ "[| a \<le> D n; tpart (a, b) (D, p); gauge (%x. a \<le> x & x \<le> D n) g;
+ fine (%x. if x < D n then min (g x) ((D n - x)/ 2)
+ else if x = D n then min (g (D n)) (ga (D n))
+ else min (ga x) ((x - D n)/ 2)) (D, p) |]
+ ==> fine g
+ (%x. if D x < D n then D(x) else D n,
+ %x. if D x < D n then p(x) else D n)"
+apply (auto simp add: fine_def tpart_def gauge_def)
+apply (frule_tac [!] na=na in lemma_psize_left_less_psize2)
+apply (drule_tac [!] x = na in spec, auto)
+apply (drule_tac [!] x = na in spec, auto)
+apply (auto dest: lemma_additivity3a simp add: split_if_asm)
+done
+
+lemma tpart_right1:
+ "[| a \<le> D n; tpart (a, b) (D, p) |]
+ ==> tpart(D n, b) (%x. D(x + n),%x. p(x + n))"
+apply (simp add: tpart_def partition_def, safe)
+apply (rule_tac x = "N - n" in exI, auto)
+apply (rotate_tac 2)
+apply (drule_tac x = "na + n" in spec)
+apply (rotate_tac [2] 3)
+apply (drule_tac [2] x = "na + n" in spec, arith+)
+done
+
+lemma fine_right1:
+ "[| a \<le> D n; tpart (a, b) (D, p); gauge (%x. D n \<le> x & x \<le> b) ga;
+ fine (%x. if x < D n then min (g x) ((D n - x)/ 2)
+ else if x = D n then min (g (D n)) (ga (D n))
+ else min (ga x) ((x - D n)/ 2)) (D, p) |]
+ ==> fine ga (%x. D(x + n),%x. p(x + n))"
+apply (auto simp add: fine_def gauge_def)
+apply (drule_tac x = "na + n" in spec)
+apply (frule_tac n = n in tpart_partition [THEN better_lemma_psize_right_eq], auto, arith)
+apply (simp add: tpart_def, safe)
+apply (subgoal_tac "D n \<le> p (na + n) ")
+apply (drule_tac y = "p (na + n) " in real_le_imp_less_or_eq)
+apply safe
+apply (simp split: split_if_asm, simp)
+apply (drule less_le_trans, assumption)
+apply (rotate_tac 5)
+apply (drule_tac x = "na + n" in spec, safe)
+apply (rule_tac y="D (na + n)" in order_trans)
+apply (case_tac "na = 0", auto)
+apply (erule partition_lt_gen [THEN order_less_imp_le], arith+)
+done
+
+lemma rsum_add: "rsum (D, p) (%x. f x + g x) = rsum (D, p) f + rsum(D, p) g"
+by (simp add: rsum_def sumr_add left_distrib)
+
+(* Bartle/Sherbert: Theorem 10.1.5 p. 278 *)
+lemma Integral_add_fun:
+ "[| a \<le> b; Integral(a,b) f k1; Integral(a,b) g k2 |]
+ ==> Integral(a,b) (%x. f x + g x) (k1 + k2)"
+apply (simp add: Integral_def, auto)
+apply ((drule_tac x = "e/2" in spec)+)
+apply auto
+apply (drule gauge_min, assumption)
+apply (rule_tac x = " (%x. if ga x < gaa x then ga x else gaa x) " in exI)
+apply auto
+apply (drule fine_min)
+apply ((drule spec)+, auto)
+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)
+apply (auto simp only: rsum_add left_distrib [symmetric]
+ mult_2_right [symmetric] real_mult_less_iff1, arith)
+done
+
+lemma partition_lt_gen2:
+ "[| partition(a,b) D; r < psize D |] ==> 0 < D (Suc r) - D r"
+by (auto simp add: partition)
+
+lemma lemma_Integral_le:
+ "[| \<forall>x. a \<le> x & x \<le> b --> f x \<le> g x;
+ tpart(a,b) (D,p)
+ |] ==> \<forall>n. n \<le> psize D --> f (p n) \<le> g (p n)"
+apply (simp add: tpart_def)
+apply (auto, frule partition [THEN iffD1], auto)
+apply (drule_tac x = "p n" in spec, auto)
+apply (case_tac "n = 0", simp)
+apply (rule partition_lt_gen [THEN order_less_le_trans, THEN order_less_imp_le], auto)
+apply (drule le_imp_less_or_eq, auto)
+apply (drule_tac [2] x = "psize D" in spec, auto)
+apply (drule_tac r = "Suc n" in partition_ub)
+apply (drule_tac x = n in spec, auto)
+done
+
+lemma lemma_Integral_rsum_le:
+ "[| \<forall>x. a \<le> x & x \<le> b --> f x \<le> g x;
+ tpart(a,b) (D,p)
+ |] ==> rsum(D,p) f \<le> rsum(D,p) g"
+apply (simp add: rsum_def)
+apply (auto intro!: sumr_le2 dest: tpart_partition [THEN partition_lt_gen2]
+ dest!: lemma_Integral_le)
+done
+
+lemma Integral_le:
+ "[| a \<le> b;
+ \<forall>x. a \<le> x & x \<le> b --> f(x) \<le> g(x);
+ Integral(a,b) f k1; Integral(a,b) g k2
+ |] ==> k1 \<le> k2"
+apply (simp add: Integral_def)
+apply (rotate_tac 2)
+apply (drule_tac x = "\<bar>k1 - k2\<bar> /2" in spec)
+apply (drule_tac x = "\<bar>k1 - k2\<bar> /2" in spec)
+apply auto
+apply (drule gauge_min, assumption)
+apply (drule_tac g = "%x. if ga x < gaa x then ga x else gaa x"
+ in partition_exists, assumption, auto)
+apply (drule fine_min)
+apply (drule_tac x = D in spec, drule_tac x = D in spec)
+apply (drule_tac x = p in spec, drule_tac x = p in spec, auto)
+apply (frule lemma_Integral_rsum_le, assumption)
+apply (subgoal_tac "\<bar>(rsum (D,p) f - k1) - (rsum (D,p) g - k2)\<bar> < \<bar>k1 - k2\<bar> ")
+apply arith
+apply (drule add_strict_mono, assumption)
+apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
+ real_mult_less_iff1, arith)
+done
+
+lemma Integral_imp_Cauchy:
+ "(\<exists>k. Integral(a,b) f k) ==>
+ (\<forall>e. 0 < e -->
+ (\<exists>g. gauge (%x. a \<le> x & x \<le> b) g &
+ (\<forall>D1 D2 p1 p2.
+ tpart(a,b) (D1, p1) & fine g (D1,p1) &
+ tpart(a,b) (D2, p2) & fine g (D2,p2) -->
+ \<bar>rsum(D1,p1) f - rsum(D2,p2) f\<bar> < e)))"
+apply (simp add: Integral_def, auto)
+apply (drule_tac x = "e/2" in spec, auto)
+apply (rule exI, auto)
+apply (frule_tac x = D1 in spec)
+apply (frule_tac x = D2 in spec)
+apply ((drule spec)+, auto)
+apply (erule_tac V = "0 < e" in thin_rl)
+apply (drule add_strict_mono, assumption)
+apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
+ real_mult_less_iff1, arith)
+done
+
+lemma Cauchy_iff2:
+ "Cauchy X =
+ (\<forall>j. (\<exists>M. \<forall>m n. M \<le> m & M \<le> n -->
+ \<bar>X m + - X n\<bar> < inverse(real (Suc j))))"
+apply (simp add: Cauchy_def, auto)
+apply (drule reals_Archimedean, safe)
+apply (drule_tac x = n in spec, auto)
+apply (rule_tac x = M in exI, auto)
+apply (drule_tac x = m in spec)
+apply (drule_tac x = na in spec, auto)
+done
+
+lemma partition_exists2:
+ "[| a \<le> b; \<forall>n. gauge (%x. a \<le> x & x \<le> b) (fa n) |]
+ ==> \<forall>n. \<exists>D p. tpart (a, b) (D, p) & fine (fa n) (D, p)"
+apply safe
+apply (rule partition_exists, auto)
+done
+
+lemma monotonic_anti_derivative:
+ "[| a \<le> b; \<forall>c. a \<le> c & c \<le> b --> f' c \<le> g' c;
+ \<forall>x. DERIV f x :> f' x; \<forall>x. DERIV g x :> g' x |]
+ ==> f b - f a \<le> g b - g a"
+apply (rule Integral_le, assumption)
+apply (rule_tac [2] FTC1)
+apply (rule_tac [4] FTC1, auto)
+done
+
+end
--- a/src/HOL/IsaMakefile Fri Jul 30 10:44:42 2004 +0200
+++ b/src/HOL/IsaMakefile Fri Jul 30 18:37:58 2004 +0200
@@ -151,7 +151,7 @@
Hyperreal/HTranscendental.thy Hyperreal/HyperArith.thy\
Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy\
Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\
- Hyperreal/Lim.thy Hyperreal/Log.thy\
+ Hyperreal/Integration.thy Hyperreal/Lim.thy Hyperreal/Log.thy\
Hyperreal/MacLaurin.thy Hyperreal/NatStar.thy\
Hyperreal/NSA.thy Hyperreal/NthRoot.thy Hyperreal/Poly.thy\
Hyperreal/SEQ.thy Hyperreal/Series.thy Hyperreal/Star.thy \
@@ -168,8 +168,7 @@
$(LOG)/HOL-Complex-ex.gz: $(OUT)/HOL-Complex Library/Primes.thy \
Complex/ex/ROOT.ML Complex/ex/document/root.tex \
- Complex/ex/BinEx.thy \
- Complex/ex/NSPrimes.ML Complex/ex/NSPrimes.thy\
+ Complex/ex/BinEx.thy Complex/ex/NSPrimes.thy\
Complex/ex/Sqrt.thy Complex/ex/Sqrt_Script.thy
@cd Complex; $(ISATOOL) usedir $(OUT)/HOL-Complex ex
--- a/src/HOL/OrderedGroup.thy Fri Jul 30 10:44:42 2004 +0200
+++ b/src/HOL/OrderedGroup.thy Fri Jul 30 18:37:58 2004 +0200
@@ -728,6 +728,15 @@
apply (rule order_trans[of _ 0])
by auto
+lemma abs_minus_commute:
+ fixes a :: "'a::lordered_ab_group_abs"
+ shows "abs (a-b) = abs(b-a)"
+proof -
+ have "abs (a-b) = abs (- (a-b))" by (simp only: abs_minus_cancel)
+ also have "... = abs(b-a)" by simp
+ finally show ?thesis .
+qed
+
lemma zero_le_iff_zero_nprt: "(0 \<le> a) = (nprt a = 0)"
by (simp add: le_def_meet nprt_def meet_comm)