# HG changeset patch # User paulson # Date 1091205478 -7200 # Node ID 49ede01e9ee65bb688277efcd13ffe2b4b871878 # Parent 7fe7f022476cdb78eb34fa78b85c6240f252969e conversion of Integration and NSPrimes to Isar scripts diff -r 7fe7f022476c -r 49ede01e9ee6 src/HOL/Complex/ex/NSPrimes.ML --- 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"; diff -r 7fe7f022476c -r 49ede01e9ee6 src/HOL/Complex/ex/NSPrimes.thy --- 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 == + \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. \X \ 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. \m. Q n m} : FreeUltrafilterNat + ==> \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: "(\f. {n. Q n (f n)} : FreeUltrafilterNat) = + ({n. \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: "\M. \N. 0 < N & (\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: "(\(x::hypnat). P x) = (\f. P (Abs_hypnat(hypnatrel `` {f})))" +apply auto +apply (rule_tac z = x in eq_Abs_hypnat, auto) +done + +lemma lemma_hypnat_P_ALL: "(\(x::hypnat). P x) = (\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: "\M. \N. 0 < N & (\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 " \(n::nat) . \N. 0 < N & (\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: + "\(N::hypnat). 0 < N & (\n \ -{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 & (\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 --> (\k \ prime. k dvd n)" +apply (rule_tac n = n in nat_less_induct, auto) +apply (case_tac "n \ 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 ==> (\k \ 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 \ 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} \ 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 ==> \n. (\i \ 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 = (\n. (\i \ N. i<(n::nat)))" +by (blast intro: finite_nat_set_bounded bounded_nat_set_is_finite) + +lemma not_finite_nat_set_iff: "(~ finite N) = (\n. \i \ N. n <= (i::nat))" +by (auto simp add: finite_nat_set_bounded_iff le_def) + +lemma bounded_nat_set_is_finite2: "(\i \ 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 ==> \n. (\i \ 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 = (\n. (\i \ N. i<=(n::nat)))" +by (blast intro: finite_nat_set_bounded2 bounded_nat_set_is_finite2) + +lemma not_finite_nat_set_iff2: "(~ finite N) = (\n. \i \ 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: "\m n. m \ n --> f n \ f m + ==> {n. f n = N} = {} | (\m. {n. f n = N} = {m})" +apply auto +apply (drule_tac x = x in spec, auto) +apply (subgoal_tac "\n. (f n = f x) = (x = n) ") +apply auto +done + +lemma inj_fun_not_hypnat_in_SHNat: "inj f ==> Abs_hypnat(hypnatrel `` {f}) \ Nats" +apply (auto simp add: SHNat_eq hypnat_of_nat_eq) +apply (subgoal_tac "\m n. m \ n --> f n \ 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}) \ *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 \ {} ==> \x. \X \ (Pow E - {{}}). x: X" +by auto + +lemma choicefun_mem_set: "E \ {} ==> choicefun E \ E" +apply (unfold choicefun_def) +apply (rule lemmaPow3 [THEN someI2_ex], auto) +done +declare choicefun_mem_set [simp] + +lemma injf_max_mem_set: "[| E \{}; \x. \y \ E. x < y |] ==> injf_max n E \ 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: "\x. \y \ 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: "\x. \y \ E. x < y + ==> \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: "\x. \y \ 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)) \ {}; \x. \y \ E. x < y |] + ==> \f. range f <= E & inj (f::nat => 'a) & (\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 \ {}") +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: "~ (\n \ - {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: "\n \ - {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 \ 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 \ 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 \ 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 \ 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 \ prime" +apply safe +apply (drule prime_g_one, auto) +done +declare one_not_prime [simp] + +lemma one_not_prime2: "Suc 0 \ 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 \ 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 \ 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 \ 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 - - diff -r 7fe7f022476c -r 49ede01e9ee6 src/HOL/Hyperreal/Integration.ML --- 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"; diff -r 7fe7f022476c -r 49ede01e9ee6 src/HOL/Hyperreal/Integration.thy --- 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) & + (\N. ((\n. n < N --> D(n) < D(Suc n)) & + (\n. N \ n --> (D(n) = b)))))" + + psize :: "(nat => real) => nat" + "psize D == @N. (\n. n < N --> D(n) < D(Suc n)) & + (\n. N \ 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))" + (\n. D(n) \ p(n) & p(n) \ 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 == \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). \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. \e. 0 < e --> + (\g. gauge(%x. a \ x & x \ b) g & + (\D p. tpart(a,b) (D,p) & fine(g)(D,p) --> + \rsum(D,p) f - k\ < 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 \ 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) & + (\n. n < (psize D) --> D n < D(Suc n)) & + (\n. (psize D) \ 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 \ n \ 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 \ n |] ==> (D n = b)" +by (simp add: partition) + +lemma lemma_partition_lt_gen [rule_format]: + "partition(a,b) D & m + Suc d \ n & n \ (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 ==> \d. n = m + Suc d" +by (auto simp add: less_iff_Suc_add) + +lemma partition_lt_gen: + "[|partition(a,b) D; m < n; n \ (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 \ 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 \ 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) \ 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 "\x. D ((psize D) - x) \ 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 = "\n. psize D \ 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 = "\n. psize D \ 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 |] + ==> (\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))) & + (\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)))" +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) |] + ==> \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 \ b; gauge(%x. a \ x & x \ b) g |] + ==> \D p. tpart(a,b) (D,p) & fine g (D,p)" +apply (cut_tac P = "%(u,v). a \ u & v \ b --> + (\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 \ x & x \ 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 \ b; Integral(a,b) f k1; Integral(a,b) f k2 |] ==> k1 = k2" +apply (simp add: Integral_def) +apply (drule_tac x = "\k1 - k2\ /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)) < \k1 - k2\ ") +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 \ 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 \ 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 \ 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: "\x. P(x) --> (\y. Q x y) ==> \f. (\x. P(x) --> Q x (f x))" +by meson + +lemma choiceP2: "\x. P(x) --> (\y. R(y) & (\z. Q x y z)) ==> + \f fa. (\x. P(x) --> R(f x) & Q x (f x) (fa x))" +by meson + +(*UNUSED +lemma choice2: "\x. (\y. R(y) & (\z. Q x y z)) ==> + \f fa. (\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: + "\\xa::real. xa \ x \ \xa + - x\ < s \ + \(f xa - f x) / (xa - x) + - f' x\ * 2 < e; + 0 < e; a \ x; x \ b; 0 < s\ + \ \z. \z - x\ < s -->\f z - f x - f' x * (z - x)\ * 2 \ e * \z - x\" +apply auto +apply (case_tac "0 < \z - x\ ") + prefer 2 apply (simp add: zero_less_abs_iff) +apply (drule_tac x = z in spec) +apply (rule_tac z1 = "\inverse (z - x)\" + 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: + "[| \x. a \ x & x \ b --> DERIV f x :> f'(x); 0 < e |] + ==> \g. gauge(%x. a \ x & x \ b) g & + (\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))" +apply (simp add: gauge_def) +apply (subgoal_tac "\x. a \ x & x \ b --> + (\d. 0 < d & (\u v. u \ x & x \ v & (v - u) < d --> abs ((f (v) - f (u)) - (f' (x) * (v - u))) \ 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) * \v - x\ " in real_le_trans) + prefer 2 apply simp apply arith +apply (erule_tac [!] + V= "\xa. xa ~= x & \xa + - x\ < s --> \(f xa - f x) / (xa - x) + - f' x\ * 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 "\f u - f x - f' x * (u - x)\ = \f x - f u - f' x * (x - u)\") +apply (rule order_trans) +apply (auto simp add: abs_le_interval_iff) +apply (simp add: right_diff_distrib, arith) +done + +lemma FTC1: "[|a \ b; \x. a \ x & x \ 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 "\e. 0 < e --> (\g. gauge (%x. a \ x & x \ b) g & (\D p. tpart (a, b) (D, p) & fine g (D, p) --> \rsum (D, p) f' - (f b - f a)\ \ 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 \ b; b \ c; Integral(a,b) f' k1; Integral(b,c) f' k2; + \x. a \ x & x \ 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 ==> ~ (\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 \ 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 \ 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 \ D n; partition(a,D n) D |] ==> psize D \ 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) \ D(m)" +by (simp add: partition partition_ub) + +lemma tag_point_eq_partition_point: + "[| tpart(a,b) (D,p); psize D \ 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 \ 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 \ 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) \ 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)) \ 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 \ 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 \ D n = D (psize D)" + in spec) +apply (simp (no_asm_simp)) +done + +lemma psize_le_n: "partition (a, D n) D ==> psize D \ 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)) \ 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 \ 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 \ na \ D na = D n" in spec, auto) +done + +lemma better_lemma_psize_right_eq: + "partition(a,b) D ==> psize (%x. D (x + n)) \ 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)) \ 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 \ 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)) \ 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 \ 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)) \ 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 \ 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 \ 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)" +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 \ 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 \ 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))" +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 \ 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 \ 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 = "\rsum (D, p) f - k1\ * 2" and c = "\rsum (D, p) g - k2\ * 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: + "[| \x. a \ x & x \ b --> f x \ g x; + tpart(a,b) (D,p) + |] ==> \n. n \ psize D --> f (p n) \ 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: + "[| \x. a \ x & x \ b --> f x \ g x; + tpart(a,b) (D,p) + |] ==> rsum(D,p) f \ 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 \ b; + \x. a \ x & x \ b --> f(x) \ g(x); + Integral(a,b) f k1; Integral(a,b) g k2 + |] ==> k1 \ k2" +apply (simp add: Integral_def) +apply (rotate_tac 2) +apply (drule_tac x = "\k1 - k2\ /2" in spec) +apply (drule_tac x = "\k1 - k2\ /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 "\(rsum (D,p) f - k1) - (rsum (D,p) g - k2)\ < \k1 - k2\ ") +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: + "(\k. Integral(a,b) f k) ==> + (\e. 0 < e --> + (\g. gauge (%x. a \ x & x \ b) g & + (\D1 D2 p1 p2. + tpart(a,b) (D1, p1) & fine g (D1,p1) & + tpart(a,b) (D2, p2) & fine g (D2,p2) --> + \rsum(D1,p1) f - rsum(D2,p2) f\ < 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 = + (\j. (\M. \m n. M \ m & M \ n --> + \X m + - X n\ < 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 \ b; \n. gauge (%x. a \ x & x \ b) (fa n) |] + ==> \n. \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 \ b; \c. a \ c & c \ b --> f' c \ g' c; + \x. DERIV f x :> f' x; \x. DERIV g x :> g' x |] + ==> f b - f a \ g b - g a" +apply (rule Integral_le, assumption) +apply (rule_tac [2] FTC1) +apply (rule_tac [4] FTC1, auto) +done + +end diff -r 7fe7f022476c -r 49ede01e9ee6 src/HOL/IsaMakefile --- 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 diff -r 7fe7f022476c -r 49ede01e9ee6 src/HOL/OrderedGroup.thy --- 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 \ a) = (nprt a = 0)" by (simp add: le_def_meet nprt_def meet_comm)