(* 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";
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";