--- a/src/HOL/Hyperreal/HRealAbs.ML Fri Jan 05 10:17:19 2001 +0100
+++ b/src/HOL/Hyperreal/HRealAbs.ML Fri Jan 05 10:17:48 2001 +0100
@@ -210,10 +210,15 @@
Embedding of the naturals in the hyperreals
----------------------------------------------------------------------------*)
-Goalw [hypreal_of_nat_def]
- "hypreal_of_nat n1 + hypreal_of_nat n2 = hypreal_of_nat (n1 + n2)";
-by (simp_tac (simpset() addsimps [hypreal_of_real_add, real_of_nat_add]) 1);
+Goal "hypreal_of_nat (m + n) = hypreal_of_nat m + hypreal_of_nat n";
+by (simp_tac (simpset() addsimps [hypreal_of_nat_def]) 1);
qed "hypreal_of_nat_add";
+Addsimps [hypreal_of_nat_add];
+
+Goal "hypreal_of_nat (m * n) = hypreal_of_nat m * hypreal_of_nat n";
+by (simp_tac (simpset() addsimps [hypreal_of_nat_def]) 1);
+qed "hypreal_of_nat_mult";
+Addsimps [hypreal_of_nat_mult];
Goalw [hypreal_of_nat_def]
"(n < m) = (hypreal_of_nat n < hypreal_of_nat m)";
--- a/src/HOL/Hyperreal/HyperArith0.ML Fri Jan 05 10:17:19 2001 +0100
+++ b/src/HOL/Hyperreal/HyperArith0.ML Fri Jan 05 10:17:48 2001 +0100
@@ -130,33 +130,16 @@
hypreal_mult_less_mono2]));
qed "hypreal_mult_less_mono2_neg";
-Goal "[| i <= j; (0::hypreal) <= k |] ==> i*k <= j*k";
-by (auto_tac (claset(),
- simpset() addsimps [order_le_less, hypreal_mult_less_mono1]));
-qed "hypreal_mult_le_mono1";
-
Goal "[| i <= j; k <= (0::hypreal) |] ==> j*k <= i*k";
by (auto_tac (claset(),
simpset() addsimps [order_le_less, hypreal_mult_less_mono1_neg]));
qed "hypreal_mult_le_mono1_neg";
-Goal "[| i <= j; (0::hypreal) <= k |] ==> k*i <= k*j";
-by (dtac hypreal_mult_le_mono1 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute])));
-qed "hypreal_mult_le_mono2";
-
Goal "[| i <= j; k <= (0::hypreal) |] ==> k*j <= k*i";
by (dtac hypreal_mult_le_mono1_neg 1);
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute])));
qed "hypreal_mult_le_mono2_neg";
-Goal "[| u <= v; x <= y; 0 <= v; (0::hypreal) <= x |] ==> u * x <= v * y";
-by (etac (hypreal_mult_le_mono1 RS order_trans) 1);
-by (assume_tac 1);
-by (etac hypreal_mult_le_mono2 1);
-by (assume_tac 1);
-qed "hypreal_mult_le_mono";
-
Goal "(m*k < n*k) = (((#0::hypreal) < k & m<n) | (k < #0 & n<m))";
by (case_tac "k = (0::hypreal)" 1);
by (auto_tac (claset(),
--- a/src/HOL/Hyperreal/HyperBin.ML Fri Jan 05 10:17:19 2001 +0100
+++ b/src/HOL/Hyperreal/HyperBin.ML Fri Jan 05 10:17:48 2001 +0100
@@ -615,3 +615,22 @@
qed "hypreal_of_real_le_number_of_iff";
Addsimps [hypreal_of_real_le_number_of_iff];
+(** <= monotonicity results: needed for arithmetic **)
+
+Goal "[| i <= j; (0::hypreal) <= k |] ==> i*k <= j*k";
+by (auto_tac (claset(),
+ simpset() addsimps [order_le_less, hypreal_mult_less_mono1]));
+qed "hypreal_mult_le_mono1";
+
+Goal "[| i <= j; (0::hypreal) <= k |] ==> k*i <= k*j";
+by (dtac hypreal_mult_le_mono1 1);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute])));
+qed "hypreal_mult_le_mono2";
+
+Goal "[| u <= v; x <= y; 0 <= v; (0::hypreal) <= x |] ==> u * x <= v * y";
+by (etac (hypreal_mult_le_mono1 RS order_trans) 1);
+by (assume_tac 1);
+by (etac hypreal_mult_le_mono2 1);
+by (assume_tac 1);
+qed "hypreal_mult_le_mono";
+
--- a/src/HOL/Hyperreal/HyperNat.ML Fri Jan 05 10:17:19 2001 +0100
+++ b/src/HOL/Hyperreal/HyperNat.ML Fri Jan 05 10:17:48 2001 +0100
@@ -1196,8 +1196,8 @@
by (auto_tac (claset() addSDs [bspec] addIs [lemma_hyprel_refl],
simpset() addsimps [hypreal_add]));
by (Ultra_tac 1);
-by (dres_inst_tac [("t","Y xb")] sym 1);
-by (auto_tac (claset(),simpset() addsimps [real_of_nat_add RS sym]));
+by (res_inst_tac [("x","no+noa")] exI 1);
+by Auto_tac;
qed "HNat_add";
Goalw [HNat_def,starset_def]
@@ -1205,10 +1205,10 @@
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
by (auto_tac (claset() addSDs [bspec] addIs [lemma_hyprel_refl],
- simpset() addsimps [hypreal_mult]));
+ simpset() addsimps [hypreal_mult]));
by (Ultra_tac 1);
-by (dres_inst_tac [("t","Y xb")] sym 1);
-by (auto_tac (claset(),simpset() addsimps [real_of_nat_mult RS sym]));
+by (res_inst_tac [("x","no*noa")] exI 1);
+by Auto_tac;
qed "HNat_mult";
(*---------------------------------------------------------------
@@ -1224,9 +1224,9 @@
"hypreal_of_hypnat (Abs_hypnat(hypnatrel^^{%n. X n})) = \
\ Abs_hypreal(hyprel ^^ {%n. real_of_nat (X n)})";
by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
-by (auto_tac (claset() addEs [FreeUltrafilterNat_Int RS
- FreeUltrafilterNat_subset],simpset() addsimps
- [lemma_hyprel_FUFN]));
+by (auto_tac (claset()
+ addEs [FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset],
+ simpset() addsimps [lemma_hyprel_FUFN]));
qed "hypreal_of_hypnat";
Goal "inj(hypreal_of_hypnat)";
@@ -1261,19 +1261,21 @@
by (simp_tac (simpset() addsimps [hypreal_of_hypnat, real_of_nat_one]) 1);
qed "hypreal_of_hypnat_one";
-Goal "hypreal_of_hypnat n1 + hypreal_of_hypnat n2 = hypreal_of_hypnat (n1 + n2)";
-by (res_inst_tac [("z","n1")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","n2")] eq_Abs_hypnat 1);
-by (asm_simp_tac (simpset() addsimps [hypreal_of_hypnat,
- hypreal_add,hypnat_add,real_of_nat_add]) 1);
+Goal "hypreal_of_hypnat (m + n) = hypreal_of_hypnat m + hypreal_of_hypnat n";
+by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
+by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
+by (asm_simp_tac (simpset() addsimps
+ [hypreal_of_hypnat, hypreal_add,hypnat_add,real_of_nat_add]) 1);
qed "hypreal_of_hypnat_add";
+Addsimps [hypreal_of_hypnat_add];
-Goal "hypreal_of_hypnat n1 * hypreal_of_hypnat n2 = hypreal_of_hypnat (n1 * n2)";
-by (res_inst_tac [("z","n1")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","n2")] eq_Abs_hypnat 1);
-by (asm_simp_tac (simpset() addsimps [hypreal_of_hypnat,
- hypreal_mult,hypnat_mult,real_of_nat_mult]) 1);
+Goal "hypreal_of_hypnat (m * n) = hypreal_of_hypnat m * hypreal_of_hypnat n";
+by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
+by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
+by (asm_simp_tac (simpset() addsimps
+ [hypreal_of_hypnat, hypreal_mult,hypnat_mult,real_of_nat_mult]) 1);
qed "hypreal_of_hypnat_mult";
+Addsimps [hypreal_of_hypnat_mult];
Goal "(hypreal_of_hypnat n < hypreal_of_hypnat m) = (n < m)";
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
--- a/src/HOL/Hyperreal/HyperOrd.ML Fri Jan 05 10:17:19 2001 +0100
+++ b/src/HOL/Hyperreal/HyperOrd.ML Fri Jan 05 10:17:48 2001 +0100
@@ -289,11 +289,6 @@
hypreal_mult_le_less_mono1]) 1);
qed "hypreal_mult_le_less_mono2";
-Goal "[| (0::hypreal)<=z; x<=y |] ==> z*x<=z*y";
-by (dres_inst_tac [("x","x")] order_le_imp_less_or_eq 1);
-by (auto_tac (claset() addIs [hypreal_mult_le_less_mono2], simpset()));
-qed "hypreal_mult_le_le_mono1";
-
val prem1::prem2::prem3::rest = goal thy
"[| (0::hypreal)<y; x<r; y*r<t*s |] ==> y*x<t*s";
by (rtac ([[prem1,prem2] MRS hypreal_mult_less_mono2, prem3]
--- a/src/HOL/Hyperreal/HyperPow.ML Fri Jan 05 10:17:19 2001 +0100
+++ b/src/HOL/Hyperreal/HyperPow.ML Fri Jan 05 10:17:48 2001 +0100
@@ -200,8 +200,7 @@
using induction: proof is much simpler this way!
---------------------------------------------------------------*)
Goal "[|(#0::hypreal) <= x; #0 <= y;x ^ Suc n <= y ^ Suc n |] ==> x <= y";
-by (full_simp_tac
- (HOL_ss addsimps [zero_eq_numeral_0 RS sym, hypreal_zero_def]) 1);
+by (full_simp_tac (simpset() addsimps [rename_numerals hypreal_zero_def]) 1);
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
by (auto_tac (claset(),
@@ -238,14 +237,14 @@
qed "hyperpow";
Goalw [hypnat_one_def] "(#0::hypreal) pow (n + 1hn) = #0";
-by (simp_tac (HOL_ss addsimps [zero_eq_numeral_0 RS sym, hypreal_zero_def]) 1);
+by (simp_tac (simpset() addsimps [rename_numerals hypreal_zero_def]) 1);
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
by (auto_tac (claset(), simpset() addsimps [hyperpow,hypnat_add]));
qed "hyperpow_zero";
Addsimps [hyperpow_zero];
Goal "r ~= (#0::hypreal) --> r pow n ~= #0";
-by (simp_tac (HOL_ss addsimps [zero_eq_numeral_0 RS sym, hypreal_zero_def]) 1);
+by (simp_tac (simpset() addsimps [rename_numerals hypreal_zero_def]) 1);
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
by (auto_tac (claset(), simpset() addsimps [hyperpow]));
@@ -255,7 +254,7 @@
qed_spec_mp "hyperpow_not_zero";
Goal "r ~= (#0::hypreal) --> inverse(r pow n) = (inverse r) pow n";
-by (simp_tac (HOL_ss addsimps [zero_eq_numeral_0 RS sym, hypreal_zero_def]) 1);
+by (simp_tac (simpset() addsimps [rename_numerals hypreal_zero_def]) 1);
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
by (auto_tac (claset() addSDs [FreeUltrafilterNat_Compl_mem],
@@ -288,41 +287,38 @@
Addsimps [hyperpow_one];
Goalw [hypnat_one_def]
- "r pow (1hn + 1hn) = r * r";
+ "r pow (1hn + 1hn) = r * r";
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
by (auto_tac (claset(),
- simpset() addsimps [hyperpow,hypnat_add, hypreal_mult,realpow_two]));
+ simpset() addsimps [hyperpow,hypnat_add, hypreal_mult]));
qed "hyperpow_two";
Goal "(#0::hypreal) < r --> #0 < r pow n";
-by (simp_tac (HOL_ss addsimps [zero_eq_numeral_0 RS sym, hypreal_zero_def]) 1);
+by (simp_tac (simpset() addsimps [rename_numerals hypreal_zero_def]) 1);
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset, realpow_gt_zero],
simpset() addsimps [hyperpow,hypreal_less, hypreal_le]));
qed_spec_mp "hyperpow_gt_zero";
-Goal "(#0::hypreal) < r --> #0 <= r pow n";
-by (blast_tac (claset() addSIs [hyperpow_gt_zero, order_less_imp_le]) 1);
-qed_spec_mp "hyperpow_ge_zero";
-
Goal "(#0::hypreal) <= r --> #0 <= r pow n";
-by (simp_tac (HOL_ss addsimps [zero_eq_numeral_0 RS sym, hypreal_zero_def]) 1);
+by (simp_tac (simpset() addsimps [rename_numerals hypreal_zero_def]) 1);
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset, realpow_ge_zero2],
+by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset, realpow_ge_zero],
simpset() addsimps [hyperpow,hypreal_le]));
-qed "hyperpow_ge_zero2";
+qed "hyperpow_ge_zero";
Goal "(#0::hypreal) < x & x <= y --> x pow n <= y pow n";
-by (full_simp_tac
- (HOL_ss addsimps [zero_eq_numeral_0 RS sym, hypreal_zero_def]) 1);
+by (full_simp_tac (simpset() addsimps [rename_numerals hypreal_zero_def]) 1);
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (auto_tac (claset() addIs [realpow_le,
- (FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset)],
- simpset() addsimps [hyperpow,hypreal_le,hypreal_less]));
+by (auto_tac (claset(),
+ simpset() addsimps [hyperpow,hypreal_le,hypreal_less]));
+by (etac (FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset) 1
+ THEN assume_tac 1);
+by (auto_tac (claset() addIs [realpow_le], simpset()));
qed_spec_mp "hyperpow_le";
Goal "#1 pow n = (#1::hypreal)";
--- a/src/HOL/Hyperreal/SEQ.ML Fri Jan 05 10:17:19 2001 +0100
+++ b/src/HOL/Hyperreal/SEQ.ML Fri Jan 05 10:17:48 2001 +0100
@@ -416,15 +416,13 @@
qed "BseqD";
Goalw [Bseq_def]
- "[| #0 < K; ALL n. abs(X n) <= K |] \
-\ ==> Bseq X";
+ "[| #0 < K; ALL n. abs(X n) <= K |] ==> Bseq X";
by (Blast_tac 1);
qed "BseqI";
Goal "(EX K. #0 < K & (ALL n. abs(X n) <= K)) = \
\ (EX N. ALL n. abs(X n) <= real_of_nat(Suc N))";
by Auto_tac;
-by (Force_tac 2);
by (cut_inst_tac [("x","K")] reals_Archimedean2 1);
by (Clarify_tac 1);
by (res_inst_tac [("x","n")] exI 1);
@@ -1255,12 +1253,11 @@
Proof will use (NS) Cauchy equivalence for convergence and
also fact that bounded and monotonic sequence converges.
---------------------------------------------------------------*)
-Goalw [Bseq_def]
- "[| #0 <= x; x < #1 |] ==> Bseq (%n. x ^ n)";
+Goalw [Bseq_def] "[| #0 <= x; x < #1 |] ==> Bseq (%n. x ^ n)";
by (res_inst_tac [("x","#1")] exI 1);
-by (auto_tac (claset() addDs [conjI RS realpow_le2]
+by (auto_tac (claset() addDs [conjI RS realpow_le]
addIs [order_less_imp_le],
- simpset() addsimps [real_zero_less_one,abs_eqI1,realpow_abs RS sym] ));
+ simpset() addsimps [abs_eqI1, realpow_abs RS sym] ));
qed "Bseq_realpow";
Goal "[| #0 <= x; x < #1 |] ==> monoseq (%n. x ^ n)";
--- a/src/HOL/Hyperreal/Series.ML Fri Jan 05 10:17:19 2001 +0100
+++ b/src/HOL/Hyperreal/Series.ML Fri Jan 05 10:17:48 2001 +0100
@@ -568,7 +568,6 @@
by (dtac Suc_le_imp_diff_ge2 1 THEN Auto_tac);
qed "ratio_test_lemma2";
-
Goal "[| c < #1; ALL n. N <= n --> abs(f(Suc n)) <= c*abs(f n) |] \
\ ==> summable f";
by (forward_tac [ratio_test_lemma2] 1);
@@ -581,8 +580,8 @@
rename_numerals realpow_not_zero]));
by (induct_tac "na" 1 THEN Auto_tac);
by (res_inst_tac [("y","c*abs(f(N + n))")] order_trans 1);
-by (auto_tac (claset() addIs [real_mult_le_le_mono1],
- simpset() addsimps [summable_def]));
+by (auto_tac (claset() addIs [real_mult_le_mono1],
+ simpset() addsimps [summable_def]));
by (asm_full_simp_tac (simpset() addsimps real_mult_ac) 1);
by (res_inst_tac [("x","abs(f N) * (#1/(#1 - c)) / (c ^ N)")] exI 1);
by (rtac sums_divide 1);
--- a/src/HOL/Hyperreal/hypreal_arith0.ML Fri Jan 05 10:17:19 2001 +0100
+++ b/src/HOL/Hyperreal/hypreal_arith0.ML Fri Jan 05 10:17:48 2001 +0100
@@ -6,8 +6,6 @@
Instantiation of the generic linear arithmetic package for type hypreal.
*)
-val hypreal_mult_le_mono2 = rotate_prems 1 hypreal_mult_le_le_mono1;
-
local
(* reduce contradictory <= to False *)
--- a/src/HOL/Real/RComplete.ML Fri Jan 05 10:17:19 2001 +0100
+++ b/src/HOL/Real/RComplete.ML Fri Jan 05 10:17:48 2001 +0100
@@ -207,8 +207,7 @@
(simpset() addsimps [linorder_not_less, real_inverse_eq_divide]) 2);
by (Clarify_tac 2);
by (dres_inst_tac [("x","n")] spec 2);
-by (dres_inst_tac [("z","real_of_nat (Suc n)")]
- (rotate_prems 1 real_mult_le_le_mono1) 2);
+by (dres_inst_tac [("k","real_of_nat (Suc n)")] (real_mult_le_mono1) 2);
by (rtac real_of_nat_ge_zero 2);
by (asm_full_simp_tac (simpset()
addsimps [real_of_nat_Suc_gt_zero RS real_not_refl2 RS not_sym,
--- a/src/HOL/Real/RealArith0.ML Fri Jan 05 10:17:19 2001 +0100
+++ b/src/HOL/Real/RealArith0.ML Fri Jan 05 10:17:48 2001 +0100
@@ -118,21 +118,11 @@
addsimps [real_minus_mult_eq1]));;
qed "real_mult_less_mono2_neg";
-Goal "[| i <= j; (0::real) <= k |] ==> i*k <= j*k";
-by (auto_tac (claset(),
- simpset() addsimps [order_le_less, real_mult_less_mono1]));
-qed "real_mult_le_mono1";
-
Goal "[| i <= j; k <= (0::real) |] ==> j*k <= i*k";
by (auto_tac (claset(),
simpset() addsimps [order_le_less, real_mult_less_mono1_neg]));
qed "real_mult_le_mono1_neg";
-Goal "[| i <= j; (0::real) <= k |] ==> k*i <= k*j";
-by (dtac real_mult_le_mono1 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [real_mult_commute])));
-qed "real_mult_le_mono2";
-
Goal "[| i <= j; k <= (0::real) |] ==> k*j <= k*i";
by (dtac real_mult_le_mono1_neg 1);
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [real_mult_commute])));
--- a/src/HOL/Real/RealBin.ML Fri Jan 05 10:17:19 2001 +0100
+++ b/src/HOL/Real/RealBin.ML Fri Jan 05 10:17:48 2001 +0100
@@ -137,7 +137,9 @@
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]);
+AddIffs
+ (map rename_numerals
+ [real_mult_is_0, real_of_nat_zero_iff, real_le_square]);
bind_thm ("real_0_less_mult_iff",
rename_numerals real_zero_less_mult_iff);
@@ -151,14 +153,22 @@
bind_thm ("real_inverse_less_0", rename_numerals real_inverse_less_zero);
bind_thm ("real_inverse_gt_0", rename_numerals real_inverse_gt_zero);
-Addsimps [rename_numerals real_le_square];
+Addsimps [zero_eq_numeral_0,one_eq_numeral_1];
-(*Perhaps add some theorems that aren't in the default simpset, as
- done in Integ/NatBin.ML*)
+(** real_of_nat **)
+Goal "(#0 < real_of_nat n) = (0<n)";
+by (simp_tac (HOL_ss addsimps [real_of_nat_less_iff,
+ rename_numerals real_of_nat_zero RS sym]) 1);
+qed "zero_less_real_of_nat_iff";
+AddIffs [zero_less_real_of_nat_iff];
-Addsimps [zero_eq_numeral_0,one_eq_numeral_1];
+Goal "(#0 <= real_of_nat n) = (0<=n)";
+by (simp_tac (HOL_ss addsimps [real_of_nat_le_iff,
+ rename_numerals real_of_nat_zero RS sym]) 1);
+qed "zero_le_real_of_nat_iff";
+AddIffs [zero_le_real_of_nat_iff];
(** Simplification of arithmetic when nested to the right **)
@@ -594,3 +604,22 @@
AddIffs [real_less_iff_diff_less_0 RS sym];
AddIffs [real_eq_iff_diff_eq_0 RS sym];
AddIffs [real_le_iff_diff_le_0 RS sym];
+
+(** <= monotonicity results: needed for arithmetic **)
+
+Goal "[| i <= j; (0::real) <= k |] ==> i*k <= j*k";
+by (auto_tac (claset(),
+ simpset() addsimps [order_le_less, real_mult_less_mono1]));
+qed "real_mult_le_mono1";
+
+Goal "[| i <= j; (0::real) <= k |] ==> k*i <= k*j";
+by (dtac real_mult_le_mono1 1);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [real_mult_commute])));
+qed "real_mult_le_mono2";
+
+Goal "[| (i::real) <= j; k <= l; 0 <= j; 0 <= k |] ==> i*k <= j*l";
+by (etac (real_mult_le_mono1 RS order_trans) 1);
+by (assume_tac 1);
+by (etac real_mult_le_mono2 1);
+by (assume_tac 1);
+qed "real_mult_le_mono";
--- a/src/HOL/Real/RealInt.ML Fri Jan 05 10:17:19 2001 +0100
+++ b/src/HOL/Real/RealInt.ML Fri Jan 05 10:17:48 2001 +0100
@@ -53,30 +53,35 @@
preal_of_prat_add RS sym,prat_of_pnat_add RS sym,
zadd,real_add,pnat_of_nat_add] @ pnat_add_ac));
qed "real_of_int_add";
+Addsimps [real_of_int_add RS sym];
Goal "-real_of_int x = real_of_int (-x)";
by (res_inst_tac [("z","x")] eq_Abs_Integ 1);
by (auto_tac (claset(), simpset() addsimps [real_of_int, real_minus,zminus]));
qed "real_of_int_minus";
+Addsimps [real_of_int_minus RS sym];
Goalw [zdiff_def,real_diff_def]
"real_of_int x - real_of_int y = real_of_int (x - y)";
-by (simp_tac (simpset() addsimps [real_of_int_add, real_of_int_minus]) 1);
+by (simp_tac (HOL_ss addsimps [real_of_int_add, real_of_int_minus]) 1);
qed "real_of_int_diff";
+Addsimps [real_of_int_diff RS sym];
Goal "real_of_int x * real_of_int y = real_of_int (x * y)";
by (res_inst_tac [("z","x")] eq_Abs_Integ 1);
by (res_inst_tac [("z","y")] eq_Abs_Integ 1);
-by (auto_tac (claset(),simpset() addsimps [real_of_int,
- real_mult,zmult,preal_of_prat_mult RS sym,pnat_of_nat_mult,
- prat_of_pnat_mult RS sym,preal_of_prat_add RS sym,
- prat_of_pnat_add RS sym,pnat_of_nat_add] @ mult_ac @add_ac
- @ pnat_add_ac));
+by (auto_tac (claset(),
+ simpset() addsimps [real_of_int, real_mult,zmult,
+ preal_of_prat_mult RS sym,pnat_of_nat_mult,
+ prat_of_pnat_mult RS sym,preal_of_prat_add RS sym,
+ prat_of_pnat_add RS sym,pnat_of_nat_add] @ mult_ac @add_ac
+ @ pnat_add_ac));
qed "real_of_int_mult";
+Addsimps [real_of_int_mult RS sym];
Goal "real_of_int (int (Suc n)) = real_of_int (int n) + 1r";
by (simp_tac (simpset() addsimps [real_of_int_one RS sym,
- real_of_int_add,zadd_int] @ zadd_ac) 1);
+ zadd_int] @ zadd_ac) 1);
qed "real_of_int_Suc";
(* relating two of the embeddings *)
--- a/src/HOL/Real/RealOrd.ML Fri Jan 05 10:17:19 2001 +0100
+++ b/src/HOL/Real/RealOrd.ML Fri Jan 05 10:17:48 2001 +0100
@@ -130,18 +130,6 @@
by (Asm_full_simp_tac 1);
qed "real_mult_less_zero1";
-Goal "[| 0 <= x; 0 <= y |] ==> (0::real) <= x * y";
-by (REPEAT(dtac order_le_imp_less_or_eq 1));
-by (auto_tac (claset() addIs [real_mult_order, order_less_imp_le],
- simpset()));
-qed "real_le_mult_order";
-
-Goal "[| 0 < x; 0 <= y |] ==> (0::real) <= x * y";
-by (dtac order_le_imp_less_or_eq 1);
-by (auto_tac (claset() addIs [real_mult_order, order_less_imp_le],
- simpset()));
-qed "real_less_le_mult_order";
-
Goal "[| 0 < x; y < 0 |] ==> x*y < (0::real)";
by (dtac (real_minus_zero_less_iff RS iffD2) 1);
by (dtac real_mult_order 1 THEN assume_tac 1);
@@ -328,6 +316,7 @@
by (simp_tac (simpset() addsimps
[real_of_posnat_add,real_add_assoc RS sym]) 1);
qed "real_of_nat_add";
+Addsimps [real_of_nat_add];
(*Not for addsimps: often the LHS is used to represent a positive natural*)
Goalw [real_of_nat_def] "real_of_nat (Suc n) = real_of_nat n + 1r";
@@ -364,9 +353,10 @@
Goal "real_of_nat (m * n) = real_of_nat m * real_of_nat n";
by (induct_tac "m" 1);
by (auto_tac (claset(),
- simpset() addsimps [real_of_nat_add, real_of_nat_Suc,
+ simpset() addsimps [real_of_nat_Suc,
real_add_mult_distrib, real_add_commute]));
qed "real_of_nat_mult";
+Addsimps [real_of_nat_mult];
Goal "(real_of_nat n = real_of_nat m) = (n = m)";
by (auto_tac (claset() addDs [inj_real_of_nat RS injD], simpset()));
@@ -393,7 +383,6 @@
Goal "(real_of_nat n = 0) = (n = 0)";
by (auto_tac (claset() addIs [inj_real_of_nat RS injD], simpset()));
qed "real_of_nat_zero_iff";
-Addsimps [real_of_nat_zero_iff];
Goal "neg z ==> real_of_nat (nat z) = 0";
by (asm_simp_tac (simpset() addsimps [neg_nat, real_of_nat_zero]) 1);
@@ -479,15 +468,6 @@
by (auto_tac (claset() addIs [real_mult_less_mono1],simpset()));
qed "real_mult_le_less_mono1";
-Goal "[| (0::real) <= z; x < y |] ==> z*x <= z*y";
-by (asm_simp_tac (simpset() addsimps [real_mult_commute,real_mult_le_less_mono1]) 1);
-qed "real_mult_le_less_mono2";
-
-Goal "[| (0::real) <= z; x <= y |] ==> z*x <= z*y";
-by (dres_inst_tac [("x","x")] order_le_imp_less_or_eq 1);
-by (auto_tac (claset() addIs [real_mult_le_less_mono2], simpset()));
-qed "real_mult_le_le_mono1";
-
Goal "[| u<v; x<y; (0::real) < v; 0 < x |] ==> u*x < v* y";
by (etac (real_mult_less_mono1 RS order_less_trans) 1);
by (assume_tac 1);
@@ -495,6 +475,7 @@
by (assume_tac 1);
qed "real_mult_less_mono";
+(*Variant of the theorem above; sometimes it's stronger*)
Goal "[| x < y; r1 < r2; (0::real) <= r1; 0 <= x|] ==> r1 * x < r2 * y";
by (subgoal_tac "0<r2" 1);
by (blast_tac (claset() addIs [order_le_less_trans]) 2);
@@ -504,32 +485,6 @@
simpset()));
qed "real_mult_less_mono'";
-Goal "[| r1 <= r2; x <= y; (0::real) < r1; 0 <= x |] ==> r1 * x <= r2 * y";
-by (subgoal_tac "0<r2" 1);
-by (blast_tac (claset() addIs [order_less_le_trans]) 2);
-by (rtac real_less_or_eq_imp_le 1);
-by (REPEAT(dtac order_le_imp_less_or_eq 1));
-by (auto_tac (claset() addIs [real_mult_less_mono, real_mult_order],
- simpset()));
-qed "real_mult_le_mono";
-
-Goal "[| (0::real) < r1; r1 < r2; 0 <= x; x <= y |] ==> r1 * x <= r2 * y";
-by (blast_tac (claset() addIs [real_mult_le_mono, order_less_imp_le]) 1);
-qed "real_mult_le_mono2";
-
-Goal "[| (0::real) <= r1; r1 < r2; 0 <= x; x <= y |] ==> r1 * x <= r2 * y";
-by (dtac order_le_imp_less_or_eq 1);
-by (auto_tac (claset() addIs [real_mult_le_mono2],simpset()));
-by (dtac order_trans 1 THEN assume_tac 1);
-by (auto_tac (claset() addIs [real_less_le_mult_order], simpset()));
-qed "real_mult_le_mono3";
-
-Goal "[| (0::real) <= r1; r1 <= r2; 0 <= x; x <= y |] ==> r1 * x <= r2 * y";
-by (dres_inst_tac [("x","r1")] order_le_imp_less_or_eq 1);
-by (auto_tac (claset() addIs [real_mult_le_mono3, real_mult_le_le_mono1],
- simpset()));
-qed "real_mult_le_mono4";
-
Goal "1r <= x ==> 0 < x";
by (rtac ccontr 1 THEN dtac real_leI 1);
by (dtac order_trans 1 THEN assume_tac 1);
--- a/src/HOL/Real/RealPow.ML Fri Jan 05 10:17:19 2001 +0100
+++ b/src/HOL/Real/RealPow.ML Fri Jan 05 10:17:48 2001 +0100
@@ -46,13 +46,6 @@
by (Simp_tac 1);
qed "realpow_two";
-Goal "(#0::real) < r --> #0 <= r ^ n";
-by (induct_tac "n" 1);
-by (auto_tac (claset() addDs [order_less_imp_le]
- addIs [rename_numerals real_le_mult_order],
- simpset()));
-qed_spec_mp "realpow_ge_zero";
-
Goal "(#0::real) < r --> #0 < r ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset() addIs [rename_numerals real_mult_order],
@@ -61,23 +54,14 @@
Goal "(#0::real) <= r --> #0 <= r ^ n";
by (induct_tac "n" 1);
-by (auto_tac (claset() addIs [rename_numerals real_le_mult_order],
- simpset()));
-qed_spec_mp "realpow_ge_zero2";
-
-Goal "(#0::real) < x & x <= y --> x ^ n <= y ^ n";
-by (induct_tac "n" 1);
-by (auto_tac (claset() addSIs [real_mult_le_mono],
- simpset()));
-by (asm_simp_tac (simpset() addsimps [realpow_ge_zero]) 1);
-qed_spec_mp "realpow_le";
+by (auto_tac (claset(), simpset() addsimps [real_0_le_mult_iff]));
+qed_spec_mp "realpow_ge_zero";
Goal "(#0::real) <= x & x <= y --> x ^ n <= y ^ n";
by (induct_tac "n" 1);
-by (auto_tac (claset() addSIs [real_mult_le_mono4],
- simpset()));
-by (asm_simp_tac (simpset() addsimps [realpow_ge_zero2]) 1);
-qed_spec_mp "realpow_le2";
+by (auto_tac (claset() addSIs [real_mult_le_mono], simpset()));
+by (asm_simp_tac (simpset() addsimps [realpow_ge_zero]) 1);
+qed_spec_mp "realpow_le";
Goal "(#0::real) < x & x < y & 0 < n --> x ^ n < y ^ n";
by (induct_tac "n" 1);
@@ -205,13 +189,12 @@
Goal "#0 <= r & r < (#1::real) & n < N --> r ^ N <= r ^ n";
by (induct_tac "N" 1);
-by Auto_tac;
-by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_zero2));
-by (ALLGOALS(dtac (rename_numerals real_mult_le_mono3)));
-by (REPEAT(assume_tac 1));
-by (REPEAT(assume_tac 3));
-by (auto_tac (claset(),simpset() addsimps
- [less_Suc_eq]));
+by (ALLGOALS Asm_simp_tac);
+by (Clarify_tac 1);
+by (subgoal_tac "r * r ^ na <= #1 * r ^ n" 1);
+by (Asm_full_simp_tac 1);
+by (rtac real_mult_le_mono 1);
+by (auto_tac (claset(), simpset() addsimps [realpow_ge_zero, less_Suc_eq]));
qed_spec_mp "realpow_less_le";
Goal "[| #0 <= r; r < (#1::real); n <= N |] ==> r ^ N <= r ^ n";