src/HOL/Hyperreal/Integration.ML

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

     "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,
-                     real_mult_2_right RS sym, mult_less_cancel_right]));
+                     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 (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,
-    real_mult_2_right RS sym,real_mult_less_iff1,CLAIM "(0::real) < 2"]));
+    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]));

 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,
-    real_mult_2_right RS sym,real_mult_less_iff1,CLAIM "(0::real) < 2"]));
+    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) ==> \

 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,
-    real_mult_2_right RS sym,real_mult_less_iff1,CLAIM "(0::real) < 2"]));
+    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 = \