--- a/src/HOL/Real/Hyperreal/HSeries.ML Wed Dec 20 12:14:50 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HSeries.ML Wed Dec 20 12:15:52 2000 +0100
@@ -187,13 +187,6 @@
real_of_nat_def,hypreal_minus,hypreal_add]));
qed "sumhr_hypreal_omega_minus_one";
-(***??SERIES.ML??replace old versions???*)
-Goal "sumr 0 (#2*n) (%i. (#-1) ^ Suc i) = #0";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed "sumr_minus_one_realpow_zero";
-Addsimps [sumr_minus_one_realpow_zero];
-
Goalw [hypnat_zero_def, hypnat_omega_def, hypreal_zero_def]
"sumhr(0, whn + whn, %i. (-#1) ^ (i+1)) = 0";
by (simp_tac (simpset() addsimps [sumhr,hypnat_add]
--- a/src/HOL/Real/Hyperreal/HyperDef.ML Wed Dec 20 12:14:50 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HyperDef.ML Wed Dec 20 12:15:52 2000 +0100
@@ -930,13 +930,9 @@
by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
qed "hypreal_eq_minus_iff3";
-Goal "(x = z + y) = (x + -z = (y::hypreal))";
-by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
-qed "hypreal_eq_minus_iff4";
-
Goal "(x ~= a) = (x + -a ~= (0::hypreal))";
-by (auto_tac (claset() addDs [sym RS
- (hypreal_eq_minus_iff RS iffD2)],simpset()));
+by (auto_tac (claset() addDs [sym RS (hypreal_eq_minus_iff RS iffD2)],
+ simpset()));
qed "hypreal_not_eq_minus_iff";
(*** linearity ***)
@@ -1074,6 +1070,7 @@
by (simp_tac (simpset() addsimps
[hypreal_minus_zero_less_iff2]) 1);
qed "hypreal_minus_zero_le_iff";
+Addsimps [hypreal_minus_zero_le_iff];
(*----------------------------------------------------------
hypreal_of_real preserves field and order properties
@@ -1305,11 +1302,6 @@
qed "hypreal_mult_self_eq_zero_iff";
Addsimps [hypreal_mult_self_eq_zero_iff];
-Goal "(0 = x * x) = (x = (0::hypreal))";
-by (auto_tac (claset() addDs [sym],simpset()));
-qed "hypreal_mult_self_eq_zero_iff2";
-Addsimps [hypreal_mult_self_eq_zero_iff2];
-
Goalw [hypreal_diff_def] "(x<y) = (x-y < (0::hypreal))";
by (rtac hypreal_less_minus_iff2 1);
qed "hypreal_less_eq_diff";
--- a/src/HOL/Real/Hyperreal/HyperOrd.ML Wed Dec 20 12:14:50 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HyperOrd.ML Wed Dec 20 12:15:52 2000 +0100
@@ -176,8 +176,8 @@
Goalw [hypreal_one_def,hypreal_zero_def,hypreal_less_def] "0 < 1hr";
by (res_inst_tac [("x","%n. #0")] exI 1);
by (res_inst_tac [("x","%n. #1")] exI 1);
-by (auto_tac (claset(),simpset() addsimps [real_zero_less_one,
- FreeUltrafilterNat_Nat_set]));
+by (auto_tac (claset(),
+ simpset() addsimps [real_zero_less_one, FreeUltrafilterNat_Nat_set]));
qed "hypreal_zero_less_one";
Goal "1hr < 1hr + 1hr";
@@ -428,52 +428,28 @@
qed "hypreal_dense";
-Goal "(x*x + y*y = 0) = (x = 0 & y = (0::hypreal))";
+(*?? more needed and earlier??*)
+Goal "(x+y = (0::hypreal)) = (x = -y)";
+by (stac hypreal_eq_minus_iff 1);
by Auto_tac;
-by (dtac (sym RS (hypreal_eq_minus_iff3 RS iffD1)) 1);
-by (dtac (sym RS (hypreal_eq_minus_iff4 RS iffD1)) 2);
-by (ALLGOALS(rtac ccontr));
-by (ALLGOALS(dtac hypreal_mult_self_not_zero));
-by (cut_inst_tac [("x1","x")] (hypreal_le_square
- RS hypreal_le_imp_less_or_eq) 1);
-by (cut_inst_tac [("x1","y")] (hypreal_le_square
- RS hypreal_le_imp_less_or_eq) 2);
-by (auto_tac (claset() addDs [sym],simpset()));
-by (dres_inst_tac [("x1","y")] (hypreal_less_minus_square
- RS hypreal_le_less_trans) 1);
-by (dres_inst_tac [("x1","x")] (hypreal_less_minus_square
- RS hypreal_le_less_trans) 2);
-by (auto_tac (claset(),simpset() addsimps
- [hypreal_less_not_refl]));
+qed "hypreal_add_eq_0_iff";
+AddIffs [hypreal_add_eq_0_iff];
+
+Goal "[| 0 <= x; 0 <= y |] ==> (x+y = 0) = (x = 0 & y = (0::hypreal))";
+by (auto_tac (claset() addIs [order_antisym], simpset()));
+qed "hypreal_add_nonneg_eq_0_iff";
+
+Goal "(x*x + y*y = 0) = (x = 0 & y = (0::hypreal))";
+by (simp_tac
+ (HOL_ss addsimps [hypreal_le_square, hypreal_add_nonneg_eq_0_iff]) 1);
+by Auto_tac;
qed "hypreal_squares_add_zero_iff";
Addsimps [hypreal_squares_add_zero_iff];
-Goal "x * x ~= 0 ==> (0::hypreal) < x* x + y*y + z*z";
-by (cut_inst_tac [("x1","x")] (hypreal_le_square
- RS hypreal_le_imp_less_or_eq) 1);
-by (auto_tac (claset() addSIs [hypreal_add_order_le],
- simpset()));
-qed "hypreal_sum_squares3_gt_zero";
-
-Goal "x * x ~= 0 ==> (0::hypreal) < y*y + x*x + z*z";
-by (dtac hypreal_sum_squares3_gt_zero 1);
-by (auto_tac (claset(), simpset() addsimps hypreal_add_ac));
-qed "hypreal_sum_squares3_gt_zero2";
-
-Goal "x * x ~= 0 ==> (0::hypreal) < y*y + z*z + x*x";
-by (dtac hypreal_sum_squares3_gt_zero 1);
-by (auto_tac (claset(), simpset() addsimps hypreal_add_ac));
-qed "hypreal_sum_squares3_gt_zero3";
-
-
Goal "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))";
+by (simp_tac (HOL_ss addsimps [hypreal_le_square, hypreal_le_add_order,
+ hypreal_add_nonneg_eq_0_iff]) 1);
by Auto_tac;
-by (ALLGOALS(rtac ccontr));
-by (ALLGOALS(dtac hypreal_mult_self_not_zero));
-by (auto_tac (claset() addDs [hypreal_not_refl2 RS not_sym,
- hypreal_sum_squares3_gt_zero3,hypreal_sum_squares3_gt_zero,
- hypreal_sum_squares3_gt_zero2],simpset() delsimps
- [hypreal_mult_self_eq_zero_iff]));
qed "hypreal_three_squares_add_zero_iff";
Addsimps [hypreal_three_squares_add_zero_iff];
@@ -758,11 +734,12 @@
----------------------------------------------------------------------------*)
Goal "((0::hypreal) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)";
- by (auto_tac (claset(), simpset() addsimps [order_le_less,
- linorder_not_less, hypreal_mult_order, hypreal_mult_less_zero1]));
+ by (auto_tac (claset(),
+ simpset() addsimps [order_le_less, linorder_not_less,
+ hypreal_mult_order, hypreal_mult_less_zero1]));
by (ALLGOALS (rtac ccontr));
-by (auto_tac (claset(), simpset() addsimps
- [order_le_less, linorder_not_less]));
+by (auto_tac (claset(),
+ simpset() addsimps [order_le_less, linorder_not_less]));
by (ALLGOALS (etac rev_mp));
by (ALLGOALS (dtac hypreal_mult_less_zero THEN' assume_tac));
by (auto_tac (claset() addDs [order_less_not_sym],
@@ -770,9 +747,9 @@
qed "hypreal_zero_less_mult_iff";
Goal "((0::hypreal) <= x*y) = (0 <= x & 0 <= y | x <= 0 & y <= 0)";
-by (auto_tac (claset() addDs [sym RS hypreal_mult_zero_disj],
- simpset() addsimps [order_le_less,
- linorder_not_less,hypreal_zero_less_mult_iff]));
+by (auto_tac (claset() addDs [hypreal_mult_zero_disj],
+ simpset() addsimps [order_le_less, linorder_not_less,
+ hypreal_zero_less_mult_iff]));
qed "hypreal_zero_le_mult_iff";
Goal "(x*y < (0::hypreal)) = (0 < x & y < 0 | x < 0 & 0 < y)";
--- a/src/HOL/Real/Hyperreal/HyperPow.ML Wed Dec 20 12:14:50 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HyperPow.ML Wed Dec 20 12:15:52 2000 +0100
@@ -114,10 +114,9 @@
qed "hrealpow_two_le_add_order2";
Addsimps [hrealpow_two_le_add_order2];
-(* See HYPER.ML *)
-Goal "(x ^ 2 + y ^ 2 + z ^ 2 = (0::hypreal)) = \
-\ (x = 0 & y = 0 & z = 0)";
-by (simp_tac (simpset() addsimps [hrealpow_two]) 1);
+Goal "(x ^ 2 + y ^ 2 + z ^ 2 = (0::hypreal)) = (x = 0 & y = 0 & z = 0)";
+by (simp_tac (HOL_ss addsimps [hypreal_three_squares_add_zero_iff,
+ hrealpow_two]) 1);
qed "hrealpow_three_squares_add_zero_iff";
Addsimps [hrealpow_three_squares_add_zero_iff];
@@ -127,8 +126,8 @@
Addsimps [hrabs_hrealpow_two];
Goal "abs(x) ^ 2 = (x::hypreal) ^ 2";
-by (simp_tac (simpset() addsimps [hrealpow_hrabs,
- hrabs_eqI1] delsimps [hpowr_Suc]) 1);
+by (simp_tac (simpset() addsimps [hrealpow_hrabs, hrabs_eqI1]
+ delsimps [hpowr_Suc]) 1);
qed "hrealpow_two_hrabs";
Addsimps [hrealpow_two_hrabs];
--- a/src/HOL/Real/Hyperreal/Lim.ML Wed Dec 20 12:14:50 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Lim.ML Wed Dec 20 12:15:52 2000 +0100
@@ -6,24 +6,11 @@
*)
-(*DELETE?????*)
fun ARITH_PROVE str = prove_goal thy str
(fn prems => [cut_facts_tac prems 1,arith_tac 1]);
-(***?REALARITH.ML?? also below??*)
-Goal "(x + - a = (#0::real)) = (x=a)";
-by (arith_tac 1);
-qed "real_add_minus_iff";
-Addsimps [real_add_minus_iff];
-
-Goal "(-b = -a) = (b = (a::real))";
-by (arith_tac 1);
-qed "real_minus_eq_cancel";
-Addsimps [real_minus_eq_cancel];
-
-
(*---------------------------------------------------------------
Theory of limits, continuity and differentiation of
real=>real functions
@@ -545,23 +532,21 @@
--------------------------------------------------------------------------*)
(* Prove equivalence between NS limits - *)
(* seems easier than using standard def *)
-Goalw [NSLIM_def]
- "(f -- a --NS> L) = ((%h. f(a + h)) -- #0 --NS> L)";
+Goalw [NSLIM_def] "(f -- a --NS> L) = ((%h. f(a + h)) -- #0 --NS> L)";
by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_zero]));
by (dres_inst_tac [("x","hypreal_of_real a + x")] spec 1);
by (dres_inst_tac [("x","-hypreal_of_real a + x")] spec 2);
by (Step_tac 1);
-by (dtac (sym RS (hypreal_eq_minus_iff4 RS iffD1)) 1);
+by (Asm_full_simp_tac 1);
by (rtac ((mem_infmal_iff RS iffD2) RS
- (Infinitesimal_add_inf_close_self RS inf_close_sym)) 2);
-by (rtac (inf_close_minus_iff2 RS iffD1) 5);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 4);
-by (dtac (sym RS (hypreal_eq_minus_iff RS iffD2)) 4);
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 3);
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 6);
-by (auto_tac (claset(),simpset() addsimps [starfun,
- hypreal_of_real_def,hypreal_minus,hypreal_add,
- real_add_assoc,inf_close_refl,hypreal_zero_def]));
+ (Infinitesimal_add_inf_close_self RS inf_close_sym)) 1);
+by (rtac (inf_close_minus_iff2 RS iffD1) 4);
+by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 3);
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 2);
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 4);
+by (auto_tac (claset(),
+ simpset() addsimps [starfun, hypreal_of_real_def, hypreal_minus,
+ hypreal_add, real_add_assoc, inf_close_refl, hypreal_zero_def]));
qed "NSLIM_h_iff";
Goal "(f -- a --NS> f a) = ((%h. f(a + h)) -- #0 --NS> f a)";
@@ -569,12 +554,10 @@
qed "NSLIM_isCont_iff";
Goal "(f -- a --> f a) = ((%h. f(a + h)) -- #0 --> f(a))";
-by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff,
- NSLIM_isCont_iff]) 1);
+by (simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_isCont_iff]) 1);
qed "LIM_isCont_iff";
-Goalw [isCont_def]
- "(isCont f x) = ((%h. f(x + h)) -- #0 --> f(x))";
+Goalw [isCont_def] "(isCont f x) = ((%h. f(x + h)) -- #0 --> f(x))";
by (simp_tac (simpset() addsimps [LIM_isCont_iff]) 1);
qed "isCont_iff";
@@ -1414,6 +1397,22 @@
---------------------------------------------------------------*)
+
+(*??REPLACE THE ONE IN HYPERDEF*??*)
+Goal "inverse(x*y) = inverse(x)*inverse(y::hypreal)";
+by (case_tac "x=0 | y=0" 1);
+by (force_tac (claset(), simpset() addsimps [HYPREAL_INVERSE_ZERO]) 1);
+by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1);
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_mult_assoc RS sym, hypreal_mult_not_0]));
+by (res_inst_tac [("c1","y")] (hypreal_mult_right_cancel RS iffD1) 1);
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_mult_not_0] @ hypreal_mult_ac));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_mult_assoc RS sym, hypreal_mult_not_0]));
+qed "inverse_mult_eq";
+
+(**?? FIXME messy proof, needs simprocs! ??*)
(*Can't get rid of x ~= #0 because it isn't continuous at zero*)
Goalw [nsderiv_def]
"x ~= #0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))";
@@ -1427,13 +1426,26 @@
delsimps [hypreal_minus_mult_eq1 RS sym,
hypreal_minus_mult_eq2 RS sym]));
by (dtac (hypreal_of_real_not_zero_iff RS iffD2) 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse_add,
- inverse_mult_eq RS sym, hypreal_minus_inverse RS sym]
- @ hypreal_add_ac @ hypreal_mult_ac delsimps [hypreal_minus_mult_eq1 RS
- sym,hypreal_minus_mult_eq2 RS sym] ) 1);
+by (asm_full_simp_tac
+ (simpset() addsimps [hypreal_inverse_add,
+ inverse_mult_eq RS sym, hypreal_minus_inverse RS sym]
+ @ hypreal_add_ac @ hypreal_mult_ac
+ delsimps [hypreal_minus_mult_eq1 RS sym,
+ hypreal_minus_mult_eq2 RS sym] ) 1);
+by (stac hypreal_inverse_add 1);
+by (asm_full_simp_tac (simpset() addsimps []) 1);
+by (stac hypreal_add_commute 1);
+by (asm_simp_tac (simpset() addsimps []) 1);
+by (asm_full_simp_tac
+ (simpset() addsimps [hypreal_inverse_add,
+ inverse_mult_eq RS sym, hypreal_minus_inverse RS sym]
+ @ hypreal_add_ac @ hypreal_mult_ac
+ delsimps [hypreal_minus_mult_eq1 RS sym,
+ hypreal_minus_mult_eq2 RS sym] ) 1);
by (asm_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym,
- hypreal_add_mult_distrib2] delsimps [hypreal_minus_mult_eq1 RS
- sym,hypreal_minus_mult_eq2 RS sym]) 1);
+ hypreal_add_mult_distrib2]
+ delsimps [hypreal_minus_mult_eq1 RS sym,
+ hypreal_minus_mult_eq2 RS sym]) 1);
by (dres_inst_tac [("x3","x") ] ((HFinite_hypreal_of_real RSN
(2,Infinitesimal_HFinite_mult2)) RS
(Infinitesimal_minus_iff RS iffD1)) 1);
@@ -1446,6 +1458,8 @@
[hypreal_minus_inverse RS sym,hypreal_of_real_mult RS sym]));
qed "NSDERIV_inverse";
+
+
Goal "x ~= #0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ 2))";
by (asm_simp_tac (simpset() addsimps [NSDERIV_inverse,
NSDERIV_DERIV_iff RS sym] delsimps [realpow_Suc]) 1);
@@ -1769,14 +1783,6 @@
(* Intermediate Value Theorem (prove contrapositive by bisection) *)
(*----------------------------------------------------------------------------*)
-
- (*ALREADY IN REALABS.ML????????????????*)
- Goalw [abs_real_def] "(abs x = #0) = (x=(#0::real))";
- by (Full_simp_tac 1);
- qed "abs_zero_iff";
- AddIffs [abs_zero_iff];
-
-
Goal "[| f(a) <= y & y <= f(b); \
\ a <= b; \
\ (ALL x. a <= x & x <= b --> isCont f x) |] \
@@ -1899,8 +1905,6 @@
by (res_inst_tac [("j","abs(f x) + abs(f(xa) - f(x))")] real_le_trans 4);
by (auto_tac (claset() addIs [abs_triangle_ineq RSN (2, real_le_trans)],
simpset() addsimps [real_diff_def,abs_ge_self]));
-(*arith_tac problem: this step should not be needed*)
-by (asm_full_simp_tac (simpset() addsimps [rename_numerals (real_eq_minus_iff2 RS sym)]) 1);
by (auto_tac (claset(),
simpset() addsimps [abs_real_def] addsplits [split_if_asm]));
qed "isCont_bounded";
--- a/src/HOL/Real/Hyperreal/NSA.ML Wed Dec 20 12:14:50 2000 +0100
+++ b/src/HOL/Real/Hyperreal/NSA.ML Wed Dec 20 12:15:52 2000 +0100
@@ -93,19 +93,19 @@
qed "SReal_omega_not_mem";
Goalw [SReal_def] "{x. hypreal_of_real x : SReal} = (UNIV::real set)";
-by (Auto_tac);
+by Auto_tac;
qed "SReal_UNIV_real";
Goalw [SReal_def] "(x: SReal) = (EX y. x = hypreal_of_real y)";
-by (Auto_tac);
+by Auto_tac;
qed "SReal_iff";
Goalw [SReal_def] "hypreal_of_real ``(UNIV::real set) = SReal";
-by (Auto_tac);
+by Auto_tac;
qed "hypreal_of_real_image";
Goalw [SReal_def] "inv hypreal_of_real ``SReal = (UNIV::real set)";
-by (Auto_tac);
+by Auto_tac;
by (rtac (inj_hypreal_of_real RS inv_f_f RS subst) 1);
by (Blast_tac 1);
qed "inv_hypreal_of_real_image";
@@ -119,7 +119,7 @@
by (auto_tac (claset(),simpset() addsimps [SReal_iff]));
by (dtac real_dense 1 THEN Step_tac 1);
by (res_inst_tac [("x","hypreal_of_real r")] bexI 1);
-by (Auto_tac);
+by Auto_tac;
qed "SReal_dense";
(*------------------------------------------------------------------
@@ -195,7 +195,7 @@
Goalw [isLub_def,leastP_def,isUb_def]
"EX Yo. isLub SReal P (hypreal_of_real Yo) \
\ ==> EX Y. isLub SReal P Y";
-by (Auto_tac);
+by Auto_tac;
qed "lemma_isLub_hypreal_of_real2";
Goal "[| P <= SReal; EX x. x: P; \
@@ -243,7 +243,7 @@
Addsimps [HFinite_hypreal_of_real];
Goalw [HFinite_def] "x : HFinite ==> EX t: SReal. abs x < t";
-by (Auto_tac);
+by Auto_tac;
qed "HFiniteD";
Goalw [HFinite_def] "x : HFinite ==> abs x : HFinite";
@@ -279,7 +279,7 @@
------------------------------------------------------------------*)
Goalw [Infinitesimal_def]
"x : Infinitesimal ==> ALL r: SReal. 0 < r --> abs x < r";
-by (Auto_tac);
+by Auto_tac;
qed "InfinitesimalD";
Goalw [Infinitesimal_def] "0 : Infinitesimal";
@@ -289,7 +289,7 @@
Goalw [Infinitesimal_def]
"[| x : Infinitesimal; y : Infinitesimal |] ==> (x + y) : Infinitesimal";
-by (Auto_tac);
+by Auto_tac;
by (rtac (hypreal_sum_of_halves RS subst) 1);
by (dtac hypreal_half_gt_zero 1);
by (dtac SReal_half 1);
@@ -314,7 +314,7 @@
Goalw [Infinitesimal_def]
"[| x : Infinitesimal; y : Infinitesimal |] \
\ ==> (x * y) : Infinitesimal";
-by (Auto_tac);
+by Auto_tac;
by (rtac (hypreal_mult_1_right RS subst) 1);
by (rtac hrabs_mult_less 1);
by (cut_facts_tac [SReal_one,hypreal_zero_less_one] 2);
@@ -346,7 +346,7 @@
(*** rather long proof ***)
Goalw [HInfinite_def,Infinitesimal_def]
"x: HInfinite ==> inverse x: Infinitesimal";
-by (Auto_tac);
+by Auto_tac;
by (eres_inst_tac [("x","inverse r")] ballE 1);
by (rtac (hrabs_inverse RS ssubst) 1);
by (forw_inst_tac [("x1","r"),("R3.0","abs x")]
@@ -363,7 +363,7 @@
Goalw [HInfinite_def]
"[|x: HInfinite;y: HInfinite|] ==> (x*y): HInfinite";
-by (Auto_tac);
+by Auto_tac;
by (cut_facts_tac [SReal_one] 1);
by (eres_inst_tac [("x","1hr")] ballE 1);
by (eres_inst_tac [("x","r")] ballE 1);
@@ -388,39 +388,34 @@
hypreal_less_imp_le]) 1);
qed "HInfinite_add_gt_zero";
-Goalw [HInfinite_def]
- "(-x: HInfinite) = (x: HInfinite)";
+Goalw [HInfinite_def] "(-x: HInfinite) = (x: HInfinite)";
by (auto_tac (claset(),simpset() addsimps
[hrabs_minus_cancel]));
qed "HInfinite_minus_iff";
-Goal "[|x: HInfinite; y <= 0; x <= 0|] \
-\ ==> (x + y): HInfinite";
+Goal "[|x: HInfinite; y <= 0; x <= 0|] ==> (x + y): HInfinite";
by (dtac (HInfinite_minus_iff RS iffD2) 1);
by (rtac (HInfinite_minus_iff RS iffD1) 1);
by (auto_tac (claset() addIs [HInfinite_add_ge_zero],
- simpset() addsimps [hypreal_minus_zero_le_iff RS sym,
- hypreal_minus_add_distrib]));
+ simpset() addsimps [hypreal_minus_zero_le_iff]));
qed "HInfinite_add_le_zero";
-Goal "[|x: HInfinite; y < 0; x < 0|] \
-\ ==> (x + y): HInfinite";
+Goal "[|x: HInfinite; y < 0; x < 0|] ==> (x + y): HInfinite";
by (blast_tac (claset() addIs [HInfinite_add_le_zero,
- hypreal_less_imp_le]) 1);
+ hypreal_less_imp_le]) 1);
qed "HInfinite_add_lt_zero";
Goal "[|a: HFinite; b: HFinite; c: HFinite|] \
\ ==> a*a + b*b + c*c : HFinite";
-by (auto_tac (claset() addIs [HFinite_mult,HFinite_add],
- simpset()));
+by (auto_tac (claset() addIs [HFinite_mult,HFinite_add], simpset()));
qed "HFinite_sum_squares";
Goal "x ~: Infinitesimal ==> x ~= 0";
-by (Auto_tac);
+by Auto_tac;
qed "not_Infinitesimal_not_zero";
Goal "x: HFinite - Infinitesimal ==> x ~= 0";
-by (Auto_tac);
+by Auto_tac;
qed "not_Infinitesimal_not_zero2";
Goal "x : Infinitesimal ==> abs x : Infinitesimal";
@@ -652,8 +647,8 @@
qed "bex_Infinitesimal_iff";
Goal "(EX y: Infinitesimal. x = z + y) = (x @= z)";
-by (asm_full_simp_tac (simpset() addsimps [hypreal_eq_minus_iff4,
- bex_Infinitesimal_iff RS sym]) 1);
+by (asm_full_simp_tac (simpset() addsimps [bex_Infinitesimal_iff RS sym]) 1);
+by (Force_tac 1);
qed "bex_Infinitesimal_iff2";
Goal "[| y: Infinitesimal; x + y = z |] ==> x @= z";
@@ -742,7 +737,7 @@
Goal "x @= hypreal_of_real D ==> x: HFinite";
by (rtac (inf_close_sym RSN (2,inf_close_HFinite)) 1);
-by (Auto_tac);
+by Auto_tac;
qed "inf_close_hypreal_of_real_HFinite";
Goal "[|a @= hypreal_of_real b; c @= hypreal_of_real d |] \
@@ -788,7 +783,7 @@
Goal "[| z <= f; f @= g; g <= z |] ==> f @= z";
by (dtac (bex_Infinitesimal_iff2 RS iffD2) 1);
-by (Auto_tac);
+by Auto_tac;
by (dres_inst_tac [("x","-g")] hypreal_add_left_le_mono1 1);
by (dres_inst_tac [("x","-g")] hypreal_add_le_mono1 1);
by (res_inst_tac [("y","-y")] Infinitesimal_add_cancel 1);
@@ -862,30 +857,30 @@
Goal "hypreal_of_real x ~= 0 ==> hypreal_of_real x : HFinite - Infinitesimal";
by (rtac SReal_HFinite_diff_Infinitesimal 1);
-by (Auto_tac);
+by Auto_tac;
qed "hypreal_of_real_HFinite_diff_Infinitesimal";
Goal "1hr+1hr ~: Infinitesimal";
-by (fast_tac (claset() addIs [SReal_two RS SReal_Infinitesimal_zero,
- hypreal_two_not_zero RS notE]) 1);
+by (fast_tac (claset() addDs [SReal_two RS SReal_Infinitesimal_zero]
+ addSEs [hypreal_two_not_zero RS notE]) 1);
qed "two_not_Infinitesimal";
Goal "1hr ~: Infinitesimal";
by (auto_tac (claset() addSDs [SReal_one RS SReal_Infinitesimal_zero],
- simpset() addsimps [hypreal_zero_not_eq_one RS not_sym]));
+ simpset() addsimps [hypreal_zero_not_eq_one RS not_sym]));
qed "hypreal_one_not_Infinitesimal";
Addsimps [hypreal_one_not_Infinitesimal];
Goal "[| y: SReal; x @= y; y~= 0 |] ==> x ~= 0";
by (cut_inst_tac [("x","y")] hypreal_trichotomy 1);
by (blast_tac (claset() addDs
- [inf_close_sym RS (mem_infmal_iff RS iffD2),
- SReal_not_Infinitesimal,SReal_minus_not_Infinitesimal]) 1);
+ [inf_close_sym RS (mem_infmal_iff RS iffD2),
+ SReal_not_Infinitesimal,SReal_minus_not_Infinitesimal]) 1);
qed "inf_close_SReal_not_zero";
Goal "[| x @= hypreal_of_real y; hypreal_of_real y ~= 0 |] ==> x ~= 0";
by (rtac inf_close_SReal_not_zero 1);
-by (Auto_tac);
+by Auto_tac;
qed "inf_close_hypreal_of_real_not_zero";
Goal "[| x @= y; y : HFinite - Infinitesimal |] \
@@ -960,7 +955,7 @@
qed "lemma_st_part_nonempty";
Goal "{s. s: SReal & s < x} <= SReal";
-by (Auto_tac);
+by Auto_tac;
qed "lemma_st_part_subset";
Goal "x: HFinite ==> EX t. isLub SReal {s. s: SReal & s < x} t";
@@ -1007,8 +1002,6 @@
Goal "t <= t + -r ==> r <= (0::hypreal)";
by (dres_inst_tac [("x","-t")] hypreal_add_left_le_mono1 1);
by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc RS sym]));
-by (dres_inst_tac [("x","r")] hypreal_add_left_le_mono1 1);
-by (Auto_tac);
qed "lemma_minus_le_zero";
Goal "[| x: HFinite; \
@@ -1075,7 +1068,7 @@
\ isLub SReal {s. s: SReal & s < x} t; \
\ r: SReal; 0 < r |] \
\ ==> x + -t ~= r";
-by (Auto_tac);
+by Auto_tac;
by (forward_tac [isLubD1a RS SReal_minus] 1);
by (dtac SReal_add_cancel 1 THEN assume_tac 1);
by (dres_inst_tac [("x","x")] lemma_SReal_lub 1);
@@ -1103,7 +1096,7 @@
\ ==> abs (x + -t) < r";
by (forward_tac [lemma_st_part1a] 1);
by (forward_tac [lemma_st_part2a] 4);
-by (Auto_tac);
+by Auto_tac;
by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
by (auto_tac (claset() addDs [lemma_st_part_not_eq1,
lemma_st_part_not_eq2],simpset() addsimps [hrabs_interval_iff2]));
@@ -1153,7 +1146,7 @@
Goal "x: HFinite ==> x ~: HInfinite";
by (EVERY1[Step_tac, dtac IntI, assume_tac]);
-by (Auto_tac);
+by Auto_tac;
qed "HFinite_not_HInfinite";
val [prem] = goalw thy [HInfinite_def] "x~: HFinite ==> x: HInfinite";
@@ -1219,7 +1212,7 @@
by (forw_inst_tac [("x","x")] not_Infinitesimal_not_zero2 1);
by (REPEAT(dtac HFinite_inverse2 1));
by (dtac inf_close_mult2 1 THEN assume_tac 1);
-by (Auto_tac);
+by Auto_tac;
by (dres_inst_tac [("c","inverse x")] inf_close_mult1 1
THEN assume_tac 1);
by (auto_tac (claset() addIs [inf_close_sym],
@@ -1296,7 +1289,7 @@
Goal "monad (abs x) <= monad(x) Un monad(-x)";
by (res_inst_tac [("x1","x")] (hrabs_disj RS disjE) 1);
-by (Auto_tac);
+by Auto_tac;
qed "monad_hrabs_Un_subset";
Goal "!! e. e : Infinitesimal ==> monad (x+e) = monad x";
@@ -1305,7 +1298,7 @@
qed "Infinitesimal_monad_eq";
Goalw [monad_def] "(u:monad x) = (-u:monad (-x))";
-by (Auto_tac);
+by Auto_tac;
qed "mem_monad_iff";
Goalw [monad_def] "(x:Infinitesimal) = (x:monad 0)";
@@ -1408,7 +1401,7 @@
by (forward_tac [lemma_inf_close_less_zero] 1);
by (REPEAT(assume_tac 1));
by (REPEAT(dtac hrabs_minus_eqI2 1));
-by (Auto_tac);
+by Auto_tac;
qed "inf_close_hrabs1";
Goal "[| x @= y; 0 < x; x ~: Infinitesimal |] \
@@ -1416,7 +1409,7 @@
by (forward_tac [lemma_inf_close_gt_zero] 1);
by (REPEAT(assume_tac 1));
by (REPEAT(dtac hrabs_eqI2 1));
-by (Auto_tac);
+by Auto_tac;
qed "inf_close_hrabs2";
Goal "x @= y ==> abs x @= abs y";
@@ -1865,16 +1858,16 @@
Goal "[| X: Rep_hypreal x; Y: Rep_hypreal x |] \
\ ==> {n. X n = Y n} : FreeUltrafilterNat";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (Auto_tac);
+by Auto_tac;
by (Ultra_tac 1);
qed "FreeUltrafilterNat_Rep_hypreal";
Goal "{n. Yb n < Y n} Int {n. -y = Yb n} <= {n. -y < Y n}";
-by (Auto_tac);
+by Auto_tac;
qed "lemma_free1";
Goal "{n. Xa n < Yc n} Int {n. y = Yc n} <= {n. Xa n < y}";
-by (Auto_tac);
+by Auto_tac;
qed "lemma_free2";
Goalw [HFinite_def]
@@ -1950,7 +1943,7 @@
by (auto_tac (claset(),simpset() delsimps [Rep_hypreal_nonempty]
addsimps [HFinite_FreeUltrafilterNat_iff,Bex_def]));
by (REPEAT(dtac spec 1));
-by (Auto_tac);
+by Auto_tac;
by (dres_inst_tac [("x","u")] spec 1 THEN
REPEAT(dtac FreeUltrafilterNat_Compl_mem 1));
by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
@@ -1965,7 +1958,7 @@
(* yet more lemmas! *)
Goal "{n. abs (Xa n) < u} Int {n. X n = Xa n} \
\ <= {n. abs (X n) < (u::real)}";
-by (Auto_tac);
+by Auto_tac;
qed "lemma_Int_HI";
Goal "{n. u < abs (X n)} Int {n. abs (X n) < (u::real)} = {}";
@@ -1977,7 +1970,7 @@
\ ==> x : HInfinite";
by (rtac (HInfinite_HFinite_iff RS iffD2) 1);
by (Step_tac 1 THEN dtac HFinite_FreeUltrafilterNat 1);
-by (Auto_tac);
+by Auto_tac;
by (dres_inst_tac [("x","u")] spec 1);
by (dtac FreeUltrafilterNat_Rep_hypreal 1 THEN assume_tac 1);
by (dres_inst_tac [("Y","{n. X n = Xa n}")] FreeUltrafilterNat_Int 1);
@@ -1998,11 +1991,11 @@
--------------------------------------------------------------------*)
Goal "{n. - u < Yd n} Int {n. xa n = Yd n} <= {n. -u < xa n}";
-by (Auto_tac);
+by Auto_tac;
qed "lemma_free4";
Goal "{n. Yb n < u} Int {n. xa n = Yb n} <= {n. xa n < u}";
-by (Auto_tac);
+by Auto_tac;
qed "lemma_free5";
Goalw [Infinitesimal_def]
--- a/src/HOL/Real/Hyperreal/SEQ.ML Wed Dec 20 12:14:50 2000 +0100
+++ b/src/HOL/Real/Hyperreal/SEQ.ML Wed Dec 20 12:15:52 2000 +0100
@@ -292,17 +292,16 @@
LIMSEQ_NSLIMSEQ_iff]) 1);
qed "LIMSEQ_inverse";
-(* trivially proved *)
-Goal "[| X ----NS> a; Y ----NS> b; b ~= #0 |] \
-\ ==> (%n. (X n) * inverse(Y n)) ----NS> a*inverse(b)";
-by (blast_tac (claset() addDs [NSLIMSEQ_inverse,NSLIMSEQ_mult]) 1);
+Goal "[| X ----NS> a; Y ----NS> b; b ~= #0 |] \
+\ ==> (%n. X n / Y n) ----NS> a/b";
+by (asm_full_simp_tac (simpset() addsimps [NSLIMSEQ_mult, NSLIMSEQ_inverse,
+ real_divide_def]) 1);
qed "NSLIMSEQ_mult_inverse";
-(* let's give a standard proof of theorem *)
-Goal "[| X ----> a; Y ----> b; b ~= #0 |] \
-\ ==> (%n. (X n) * inverse(Y n)) ----> a*inverse(b)";
-by (blast_tac (claset() addDs [LIMSEQ_inverse,LIMSEQ_mult]) 1);
-qed "LIMSEQ_mult_inverse";
+Goal "[| X ----> a; Y ----> b; b ~= #0 |] ==> (%n. X n / Y n) ----> a/b";
+by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_mult, LIMSEQ_inverse,
+ real_divide_def]) 1);
+qed "LIMSEQ_divide";
(*-----------------------------------------------
Uniqueness of limit
@@ -1296,11 +1295,11 @@
Goalw [NSLIMSEQ_def]
"[| #0 <= x; x < #1 |] ==> (%n. x ^ n) ----NS> #0";
by (auto_tac (claset() addSDs [convergent_realpow],
- simpset() addsimps [convergent_NSconvergent_iff]));
+ simpset() addsimps [convergent_NSconvergent_iff]));
by (forward_tac [NSconvergentD] 1);
-by (auto_tac (claset(),simpset() addsimps [NSLIMSEQ_def,
- NSCauchy_NSconvergent_iff RS sym,NSCauchy_def,
- starfunNat_pow]));
+by (auto_tac (claset(),
+ simpset() addsimps [NSLIMSEQ_def, NSCauchy_NSconvergent_iff RS sym,
+ NSCauchy_def, starfunNat_pow]));
by (forward_tac [HNatInfinite_add_one] 1);
by (dtac bspec 1 THEN assume_tac 1);
by (dtac bspec 1 THEN assume_tac 1);
@@ -1308,17 +1307,25 @@
by (asm_full_simp_tac (simpset() addsimps [hyperpow_add]) 1);
by (dtac inf_close_mult_subst_SReal 1 THEN assume_tac 1);
by (dtac inf_close_trans3 1 THEN assume_tac 1);
-by (auto_tac (claset() addSDs [rename_numerals
- (real_not_refl2 RS real_mult_eq_self_zero2)],
- simpset() addsimps [hypreal_of_real_mult RS sym]));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_of_real_mult RS sym]));
qed "NSLIMSEQ_realpow_zero";
(*--------------- standard version ---------------*)
Goal "[| #0 <= x; x < #1 |] ==> (%n. x ^ n) ----> #0";
-by (asm_full_simp_tac (simpset() addsimps [NSLIMSEQ_realpow_zero,
- LIMSEQ_NSLIMSEQ_iff]) 1);
+by (asm_simp_tac (simpset() addsimps [NSLIMSEQ_realpow_zero,
+ LIMSEQ_NSLIMSEQ_iff]) 1);
qed "LIMSEQ_realpow_zero";
+Goal "#1 < x ==> (%n. a / (x ^ n)) ----> #0";
+by (cut_inst_tac [("a","a"),("x1","inverse x")]
+ ([LIMSEQ_const, LIMSEQ_realpow_zero] MRS LIMSEQ_mult) 1);
+by (auto_tac (claset(),
+ simpset() addsimps [real_divide_def, realpow_inverse]));
+by (asm_simp_tac (simpset() addsimps [real_inverse_eq_divide,
+ pos_real_divide_less_eq]) 1);
+qed "LIMSEQ_divide_realpow_zero";
+
(*----------------------------------------------------------------
Limit of c^n for |c| < 1
---------------------------------------------------------------*)
@@ -1334,7 +1341,7 @@
Goal "abs(c) < #1 ==> (%n. c ^ n) ----> #0";
by (rtac (LIMSEQ_rabs_zero RS iffD1) 1);
by (auto_tac (claset() addIs [LIMSEQ_rabs_realpow_zero],
- simpset() addsimps [realpow_abs RS sym]));
+ simpset() addsimps [realpow_abs RS sym]));
qed "LIMSEQ_rabs_realpow_zero2";
Goal "abs(c) < #1 ==> (%n. c ^ n) ----NS> #0";
--- a/src/HOL/Real/Hyperreal/Series.ML Wed Dec 20 12:14:50 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Series.ML Wed Dec 20 12:15:52 2000 +0100
@@ -99,19 +99,12 @@
by (Auto_tac);
qed "sumr_shift_bounds";
-(*FIXME: replace*)
-Goal "sumr 0 (n + n) (%i. (- #1) ^ Suc i) = #0";
+Goal "sumr 0 (#2*n) (%i. (#-1) ^ Suc i) = #0";
by (induct_tac "n" 1);
by (Auto_tac);
qed "sumr_minus_one_realpow_zero";
Addsimps [sumr_minus_one_realpow_zero];
-Goal "sumr 0 (n + n) (%i. (#-1) ^ Suc i) = #0";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed "sumr_minus_one_realpow_zero2";
-Addsimps [sumr_minus_one_realpow_zero2];
-
Goal "m < Suc n ==> Suc n - m = Suc (n - m)";
by (dtac less_imp_Suc_add 1);
by (Auto_tac);
@@ -421,15 +414,13 @@
(*-------------------------------------------------------------------
sum of geometric progression
-------------------------------------------------------------------*)
-(* lemma *)
Goal "x ~= #1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - #1) * inverse(x - #1)";
by (induct_tac "n" 1);
by (Auto_tac);
by (res_inst_tac [("c1","x - #1")] (real_mult_right_cancel RS iffD1) 1);
by (auto_tac (claset(),
- simpset() addsimps [real_eq_minus_iff2 RS sym,
- real_mult_assoc, real_add_mult_distrib]));
+ simpset() addsimps [real_mult_assoc, real_add_mult_distrib]));
by (auto_tac (claset(),
simpset() addsimps [real_add_mult_distrib2,
real_diff_def, real_mult_commute]));
--- a/src/HOL/Real/RealArith.ML Wed Dec 20 12:14:50 2000 +0100
+++ b/src/HOL/Real/RealArith.ML Wed Dec 20 12:15:52 2000 +0100
@@ -212,11 +212,12 @@
val dest_coeff = dest_coeff 1
val trans_tac = trans_tac
val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_plus_1s))
- THEN ALLGOALS
- (simp_tac
- (HOL_ss addsimps [eq_real_number_of,
- real_mult_minus_right RS sym]@
- [mult_real_number_of, real_mult_number_of_left]@bin_simps@real_mult_ac))
+ THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@real_mult_minus_simps))
+ THEN ALLGOALS
+ (simp_tac
+ (HOL_ss addsimps [eq_real_number_of, mult_real_number_of,
+ real_mult_number_of_left]@
+ real_minus_from_mult_simps @ real_mult_ac))
val numeral_simp_tac =
ALLGOALS (simp_tac (HOL_ss addsimps rel_real_number_of@bin_simps))
val simplify_meta_eq = simplify_meta_eq
@@ -260,16 +261,16 @@
val real_cancel_numeral_factors =
map prep_simproc
- [("realeq_cancel_numeral_factors",
+ [("realeq_cancel_numeral_factor",
prep_pats ["(l::real) * m = n", "(l::real) = m * n"],
EqCancelNumeralFactor.proc),
- ("realless_cancel_numeral_factors",
+ ("realless_cancel_numeral_factor",
prep_pats ["(l::real) * m < n", "(l::real) < m * n"],
LessCancelNumeralFactor.proc),
- ("realle_cancel_numeral_factors",
+ ("realle_cancel_numeral_factor",
prep_pats ["(l::real) * m <= n", "(l::real) <= m * n"],
LeCancelNumeralFactor.proc),
- ("realdiv_cancel_numeral_factors",
+ ("realdiv_cancel_numeral_factor",
prep_pats ["((l::real) * m) / n", "(l::real) / (m * n)"],
DivCancelNumeralFactor.proc)];
--- a/src/HOL/Real/RealBin.ML Wed Dec 20 12:14:50 2000 +0100
+++ b/src/HOL/Real/RealBin.ML Wed Dec 20 12:15:52 2000 +0100
@@ -137,7 +137,7 @@
real_mult_minus_1_right, real_mult_minus_1, real_inverse_1,
real_minus_zero_less_iff]);
-AddIffs (map rename_numerals [real_mult_is_0, real_0_is_mult]);
+AddIffs (map rename_numerals [real_mult_is_0]);
bind_thm ("real_0_less_mult_iff",
rename_numerals real_zero_less_mult_iff);
--- a/src/HOL/Real/RealDef.ML Wed Dec 20 12:14:50 2000 +0100
+++ b/src/HOL/Real/RealDef.ML Wed Dec 20 12:15:52 2000 +0100
@@ -270,20 +270,6 @@
by (simp_tac (simpset() addsimps [real_add_commute,real_add_left_cancel]) 1);
qed "real_add_right_cancel";
-Goal "((x::real) = y) = (0 = x + (- y))";
-by (Step_tac 1);
-by (res_inst_tac [("x1","-y")]
- (real_add_right_cancel RS iffD1) 2);
-by Auto_tac;
-qed "real_eq_minus_iff";
-
-Goal "((x::real) = y) = (x + (- y) = 0)";
-by (Step_tac 1);
-by (res_inst_tac [("x1","-y")]
- (real_add_right_cancel RS iffD1) 2);
-by Auto_tac;
-qed "real_eq_minus_iff2";
-
Goal "(0::real) - x = -x";
by (simp_tac (simpset() addsimps [real_diff_def]) 1);
qed "real_diff_0";
--- a/src/HOL/Real/RealOrd.ML Wed Dec 20 12:14:50 2000 +0100
+++ b/src/HOL/Real/RealOrd.ML Wed Dec 20 12:15:52 2000 +0100
@@ -698,26 +698,7 @@
by Auto_tac;
by (blast_tac (claset() addIs [ccontr] addDs [real_mult_not_zero]) 1);
qed "real_mult_is_0";
-
-Goal "(0 = x*y) = (0 = x | (0::real) = y)";
-by (stac eq_commute 1 THEN stac real_mult_is_0 1);
-by Auto_tac;
-qed "real_0_is_mult";
-AddIffs [real_mult_is_0, real_0_is_mult];
-
-Goal "[| x ~= 1r; y * x = y |] ==> y = 0";
-by (subgoal_tac "y*(1r + -x) = 0" 1);
-by (stac real_add_mult_distrib2 2);
-by (auto_tac (claset(),
- simpset() addsimps [real_eq_minus_iff2 RS sym]));
-qed "real_mult_eq_self_zero";
-Addsimps [real_mult_eq_self_zero];
-
-Goal "[| x ~= 1r; y = y * x |] ==> y = 0";
-by (dtac sym 1);
-by (Asm_full_simp_tac 1);
-qed "real_mult_eq_self_zero2";
-Addsimps [real_mult_eq_self_zero2];
+AddIffs [real_mult_is_0];
Goal "[| 0 <= x * y; 0 < x |] ==> (0::real) <= y";
by (ftac real_inverse_gt_zero 1);
--- a/src/HOL/Real/RealPow.ML Wed Dec 20 12:14:50 2000 +0100
+++ b/src/HOL/Real/RealPow.ML Wed Dec 20 12:15:52 2000 +0100
@@ -43,7 +43,7 @@
qed "realpow_one";
Addsimps [realpow_one];
-Goal "(r::real) ^ 2 = r * r";
+Goal "(r::real)^2 = r * r";
by (Simp_tac 1);
qed "realpow_two";
@@ -111,24 +111,24 @@
by (auto_tac (claset(),simpset() addsimps real_mult_ac));
qed "realpow_mult";
-Goal "(#0::real) <= r ^ 2";
+Goal "(#0::real) <= r^2";
by (simp_tac (simpset() addsimps [rename_numerals real_le_square]) 1);
qed "realpow_two_le";
Addsimps [realpow_two_le];
-Goal "abs((x::real) ^ 2) = x ^ 2";
+Goal "abs((x::real)^2) = x^2";
by (simp_tac (simpset() addsimps [abs_eqI1,
rename_numerals real_le_square]) 1);
qed "abs_realpow_two";
Addsimps [abs_realpow_two];
-Goal "abs(x::real) ^ 2 = x ^ 2";
+Goal "abs(x::real) ^ 2 = x^2";
by (simp_tac (simpset() addsimps [realpow_abs,abs_eqI1]
delsimps [realpow_Suc]) 1);
qed "realpow_two_abs";
Addsimps [realpow_two_abs];
-Goal "(#1::real) < r ==> #1 < r ^ 2";
+Goal "(#1::real) < r ==> #1 < r^2";
by Auto_tac;
by (cut_facts_tac [rename_numerals real_zero_less_one] 1);
by (forw_inst_tac [("R1.0","#0")] real_less_trans 1);
@@ -352,37 +352,27 @@
Addsimps [realpow_two_mult_inverse];
(* 05/00 *)
-Goal "(-x) ^ 2 = (x::real) ^ 2";
+Goal "(-x)^2 = (x::real) ^ 2";
by (Simp_tac 1);
qed "realpow_two_minus";
Addsimps [realpow_two_minus];
-Goal "(x::real) ^ 2 + - (y ^ 2) = (x + -y) * (x + y)";
-by (simp_tac (simpset() addsimps [real_add_mult_distrib2,
- real_add_mult_distrib, real_minus_mult_eq2 RS sym]
- @ real_mult_ac) 1);
-qed "realpow_two_add_minus";
-
-Goalw [real_diff_def]
- "(x::real) ^ 2 - y ^ 2 = (x - y) * (x + y)";
-by (simp_tac (simpset() addsimps [realpow_two_add_minus]
- delsimps [realpow_Suc]) 1);
+Goalw [real_diff_def] "(x::real)^2 - y^2 = (x - y) * (x + y)";
+by (simp_tac (simpset() addsimps
+ [real_add_mult_distrib2, real_add_mult_distrib,
+ real_minus_mult_eq2 RS sym] @ real_mult_ac) 1);
qed "realpow_two_diff";
-Goalw [real_diff_def]
- "((x::real) ^ 2 = y ^ 2) = (x = y | x = -y)";
-by (auto_tac (claset(),simpset() delsimps [realpow_Suc]));
-by (dtac (rename_numerals (real_eq_minus_iff RS iffD1 RS sym)) 1);
-by (auto_tac (claset() addDs [rename_numerals real_add_minus_eq_minus],
- simpset() addsimps [realpow_two_add_minus] delsimps [realpow_Suc]));
+Goalw [real_diff_def] "((x::real)^2 = y^2) = (x = y | x = -y)";
+by (cut_inst_tac [("x","x"),("y","y")] realpow_two_diff 1);
+by (auto_tac (claset(), simpset() delsimps [realpow_Suc]));
qed "realpow_two_disj";
(* used in Transc *)
Goal "[|(x::real) ~= #0; m <= n |] ==> x ^ (n - m) = x ^ n * inverse (x ^ m)";
by (auto_tac (claset(),
- simpset() addsimps [le_eq_less_or_eq,
- less_iff_Suc_add,realpow_add,
- realpow_not_zero] @ real_mult_ac));
+ simpset() addsimps [le_eq_less_or_eq, less_iff_Suc_add, realpow_add,
+ realpow_not_zero] @ real_mult_ac));
qed "realpow_diff";
Goal "real_of_nat (m) ^ n = real_of_nat (m ^ n)";