# HG changeset patch # User paulson # Date 978686268 -3600 # Node ID 27e4d90b35b50446b127a033614d9e7af4c33c71 # Parent 2781ac7a46196326bd922f81b53cc061b9a674ae more removal of obsolete rules diff -r 2781ac7a4619 -r 27e4d90b35b5 src/HOL/Hyperreal/HRealAbs.ML --- 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)"; diff -r 2781ac7a4619 -r 27e4d90b35b5 src/HOL/Hyperreal/HyperArith0.ML --- 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 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"; + diff -r 2781ac7a4619 -r 27e4d90b35b5 src/HOL/Hyperreal/HyperNat.ML --- 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); diff -r 2781ac7a4619 -r 27e4d90b35b5 src/HOL/Hyperreal/HyperOrd.ML --- 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 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)"; diff -r 2781ac7a4619 -r 27e4d90b35b5 src/HOL/Hyperreal/SEQ.ML --- 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)"; diff -r 2781ac7a4619 -r 27e4d90b35b5 src/HOL/Hyperreal/Series.ML --- 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); diff -r 2781ac7a4619 -r 27e4d90b35b5 src/HOL/Hyperreal/hypreal_arith0.ML --- 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 *) diff -r 2781ac7a4619 -r 27e4d90b35b5 src/HOL/Real/RComplete.ML --- 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, diff -r 2781ac7a4619 -r 27e4d90b35b5 src/HOL/Real/RealArith0.ML --- 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]))); diff -r 2781ac7a4619 -r 27e4d90b35b5 src/HOL/Real/RealBin.ML --- 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 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"; diff -r 2781ac7a4619 -r 27e4d90b35b5 src/HOL/Real/RealInt.ML --- 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 *) diff -r 2781ac7a4619 -r 27e4d90b35b5 src/HOL/Real/RealOrd.ML --- 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 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 r1 * x <= r2 * y"; -by (subgoal_tac "0 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); diff -r 2781ac7a4619 -r 27e4d90b35b5 src/HOL/Real/RealPow.ML --- 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";