# HG changeset patch # User paulson # Date 1072555334 -3600 # Node ID 8dbbb7cf36371225c63a5f4ac475640ed3c2b5c9 # Parent eb8b8241ef5b741d40e909298d086192f2b69664 re-organized numeric lemmas diff -r eb8b8241ef5b -r 8dbbb7cf3637 src/HOL/Complex/CLim.ML --- a/src/HOL/Complex/CLim.ML Thu Dec 25 23:18:04 2003 +0100 +++ b/src/HOL/Complex/CLim.ML Sat Dec 27 21:02:14 2003 +0100 @@ -1062,19 +1062,19 @@ by (asm_full_simp_tac (simpset() addsimps [hcomplex_add_commute,numeral_2_eq_2]) 2); by (auto_tac (claset(), simpset() addsimps [starfunC_inverse_inverse,hcomplex_diff_def] - delsimps [hcomplex_minus_mult_eq1 RS sym, + delsimps [minus_mult_right RS sym, minus_mult_left RS sym, + hcomplex_minus_mult_eq1 RS sym, hcomplex_minus_mult_eq2 RS sym])); by (asm_simp_tac (simpset() addsimps [inverse_add, inverse_mult_distrib RS sym, hcomplex_minus_inverse RS sym] @ hcomplex_add_ac @ hcomplex_mult_ac - delsimps [thm"Ring_and_Field.inverse_minus_eq", - inverse_mult_distrib, hcomplex_minus_mult_eq1 RS sym, + delsimps [inverse_minus_eq, + inverse_mult_distrib, minus_mult_right RS sym, minus_mult_left RS sym, + hcomplex_minus_mult_eq1 RS sym, hcomplex_minus_mult_eq2 RS sym] ) 1); -by (asm_simp_tac (simpset() addsimps [hcomplex_mult_assoc RS sym, - hcomplex_add_mult_distrib2] - delsimps [hcomplex_minus_mult_eq1 RS sym, - hcomplex_minus_mult_eq2 RS sym]) 1); +by (asm_simp_tac (HOL_ss addsimps [hcomplex_mult_assoc RS sym, + hcomplex_add_mult_distrib2]) 1); by (res_inst_tac [("y"," inverse(- hcomplex_of_complex x * hcomplex_of_complex x)")] capprox_trans 1); by (rtac inverse_add_CInfinitesimal_capprox2 1); diff -r eb8b8241ef5b -r 8dbbb7cf3637 src/HOL/Complex/NSCA.ML --- a/src/HOL/Complex/NSCA.ML Thu Dec 25 23:18:04 2003 +0100 +++ b/src/HOL/Complex/NSCA.ML Sat Dec 27 21:02:14 2003 +0100 @@ -448,9 +448,8 @@ Goalw [capprox_def,hcomplex_diff_def] "[| a @c= b; c: CFinite|] ==> a*c @c= b*c"; -by (asm_full_simp_tac (simpset() addsimps [CInfinitesimal_CFinite_mult, - hcomplex_minus_mult_eq1,hcomplex_add_mult_distrib RS sym] - delsimps [hcomplex_minus_mult_eq1 RS sym]) 1); +by (asm_full_simp_tac (HOL_ss addsimps [CInfinitesimal_CFinite_mult, + hcomplex_minus_mult_eq1,hcomplex_add_mult_distrib RS sym]) 1); qed "capprox_mult1"; Goal "[|a @c= b; c: CFinite|] ==> c*a @c= c*b"; diff -r eb8b8241ef5b -r 8dbbb7cf3637 src/HOL/Complex/NSComplex.thy --- a/src/HOL/Complex/NSComplex.thy Thu Dec 25 23:18:04 2003 +0100 +++ b/src/HOL/Complex/NSComplex.thy Sat Dec 27 21:02:14 2003 +0100 @@ -1015,7 +1015,7 @@ lemma hcmod_triangle_ineq2: "hcmod(b + a) - hcmod b <= hcmod a" apply (cut_tac x1 = "b" and y1 = "a" and c = "-hcmod b" in hcmod_triangle_ineq [THEN add_right_mono]) -apply (simp add: hypreal_add_ac) +apply (simp add: add_ac) done declare hcmod_triangle_ineq2 [simp] diff -r eb8b8241ef5b -r 8dbbb7cf3637 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Thu Dec 25 23:18:04 2003 +0100 +++ b/src/HOL/Finite_Set.thy Sat Dec 27 21:02:14 2003 +0100 @@ -483,7 +483,7 @@ "finite A ==> B <= A ==> card A - card B = card (A - B)" apply (subgoal_tac "(A - B) Un B = A") prefer 2 apply blast - apply (rule add_right_cancel [THEN iffD1]) + apply (rule nat_add_right_cancel [THEN iffD1]) apply (rule card_Un_disjoint [THEN subst]) apply (erule_tac [4] ssubst) prefer 3 apply blast diff -r eb8b8241ef5b -r 8dbbb7cf3637 src/HOL/Hyperreal/HLog.ML --- a/src/HOL/Hyperreal/HLog.ML Thu Dec 25 23:18:04 2003 +0100 +++ b/src/HOL/Hyperreal/HLog.ML Sat Dec 27 21:02:14 2003 +0100 @@ -191,7 +191,7 @@ starfun_ln_HInfinite,HInfinite_HFinite_not_Infinitesimal_mult2, starfun_exp_HInfinite],simpset() addsimps [order_less_imp_le, HInfinite_gt_zero_gt_one,powhr_as_starfun, - hypreal_0_le_mult_iff])); + zero_le_mult_iff])); qed "HInfinite_powhr"; Goal "[| x : HFinite - Infinitesimal; a : HInfinite; 0 < a |] \ @@ -224,15 +224,15 @@ Addsimps [hlog_eq_one]; Goal "[| 0 < a; a ~= 1; 0 < x |] ==> hlog a (inverse x) = - hlog a x"; -by (res_inst_tac [("x1","hlog a x")] (hypreal_add_left_cancel RS iffD1) 1); +by (res_inst_tac [("a1","hlog a x")] (add_left_cancel RS iffD1) 1); by (auto_tac (claset(),simpset() addsimps [hypreal_not_refl2 RS not_sym, hlog_mult RS sym,hypreal_inverse_gt_0])); qed "hlog_inverse"; Goal "[| 0 < a; a ~= 1; 0 < x; 0 < y|] \ \ ==> hlog a (x/y) = hlog a x - hlog a y"; -by (auto_tac (claset(),simpset() addsimps [hypreal_inverse_gt_0,hlog_mult, - hlog_inverse,hypreal_diff_def,hypreal_divide_def])); +by (auto_tac (claset(), + simpset() addsimps [hypreal_inverse_gt_0,hlog_mult, hlog_inverse,hypreal_diff_def,hypreal_divide_def])); qed "hlog_divide"; Goal "[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x < hlog a y) = (x < y)"; diff -r eb8b8241ef5b -r 8dbbb7cf3637 src/HOL/Hyperreal/HRealAbs.ML --- a/src/HOL/Hyperreal/HRealAbs.ML Thu Dec 25 23:18:04 2003 +0100 +++ b/src/HOL/Hyperreal/HRealAbs.ML Sat Dec 27 21:02:14 2003 +0100 @@ -105,7 +105,7 @@ by (asm_full_simp_tac (simpset() addsimps [hrabs_def] addsplits [split_if_asm]) 2); by (case_tac "y = 0" 1); -by (asm_full_simp_tac (simpset() addsimps [hypreal_0_less_mult_iff]) 1); +by (asm_full_simp_tac (simpset() addsimps [zero_less_mult_iff]) 1); by (rtac hypreal_mult_less_mono 1); by (auto_tac (claset(), simpset() addsimps [hrabs_def, linorder_neq_iff] diff -r eb8b8241ef5b -r 8dbbb7cf3637 src/HOL/Hyperreal/HTranscendental.ML --- a/src/HOL/Hyperreal/HTranscendental.ML Thu Dec 25 23:18:04 2003 +0100 +++ b/src/HOL/Hyperreal/HTranscendental.ML Sat Dec 27 21:02:14 2003 +0100 @@ -74,8 +74,7 @@ Addsimps [hypreal_sqrt_approx_zero]; Goal "0 <= x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)"; -by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq], - simpset())); +by (auto_tac (claset(), simpset() addsimps [order_le_less])); qed "hypreal_sqrt_approx_zero2"; Addsimps [hypreal_sqrt_approx_zero2]; @@ -637,8 +636,7 @@ MRS STAR_sin_Infinitesimal_divide) 1); by (auto_tac (claset(),simpset() addsimps [hypreal_inverse_distrib])); by (res_inst_tac [("a","inverse(hypreal_of_real pi)")] approx_SReal_mult_cancel 1); -by (auto_tac (claset() addIs [SReal_inverse],simpset() addsimps [hypreal_divide_def] @ - hypreal_mult_ac)); +by (auto_tac (claset() addIs [SReal_inverse],simpset() addsimps [hypreal_divide_def] @ mult_ac)); qed "STAR_sin_pi_divide_HNatInfinite_approx_pi"; Goal "n : HNatInfinite \ diff -r eb8b8241ef5b -r 8dbbb7cf3637 src/HOL/Hyperreal/HyperBin.ML --- a/src/HOL/Hyperreal/HyperBin.ML Thu Dec 25 23:18:04 2003 +0100 +++ b/src/HOL/Hyperreal/HyperBin.ML Sat Dec 27 21:02:14 2003 +0100 @@ -64,7 +64,7 @@ (*For specialist use: NOT as default simprules*) Goal "2 * z = (z+z::hypreal)"; by (simp_tac (simpset () - addsimps [lemma, hypreal_add_mult_distrib, + addsimps [lemma, left_distrib, hypreal_numeral_1_eq_1]) 1); qed "hypreal_mult_2"; @@ -151,7 +151,7 @@ (** For combine_numerals **) Goal "i*u + (j*u + k) = (i+j)*u + (k::hypreal)"; -by (asm_simp_tac (simpset() addsimps [hypreal_add_mult_distrib] @ add_ac) 1); +by (asm_simp_tac (simpset() addsimps [left_distrib] @ add_ac) 1); qed "left_hypreal_add_mult_distrib"; @@ -167,38 +167,38 @@ Goal "!!i::hypreal. (i*u + m = j*u + n) = ((i-j)*u + m = n)"; by (asm_simp_tac - (simpset() addsimps [hypreal_diff_def, hypreal_add_mult_distrib]@ - hypreal_add_ac@rel_iff_rel_0_rls) 1); + (simpset() addsimps [hypreal_diff_def, left_distrib]@ + add_ac@rel_iff_rel_0_rls) 1); qed "hypreal_eq_add_iff1"; Goal "!!i::hypreal. (i*u + m = j*u + n) = (m = (j-i)*u + n)"; by (asm_simp_tac - (simpset() addsimps [hypreal_diff_def, hypreal_add_mult_distrib]@ - hypreal_add_ac@rel_iff_rel_0_rls) 1); + (simpset() addsimps [hypreal_diff_def, left_distrib]@ + add_ac@rel_iff_rel_0_rls) 1); qed "hypreal_eq_add_iff2"; Goal "!!i::hypreal. (i*u + m < j*u + n) = ((i-j)*u + m < n)"; by (asm_simp_tac - (simpset() addsimps [hypreal_diff_def, hypreal_add_mult_distrib]@ - hypreal_add_ac@rel_iff_rel_0_rls) 1); + (simpset() addsimps [hypreal_diff_def, left_distrib]@ + add_ac@rel_iff_rel_0_rls) 1); qed "hypreal_less_add_iff1"; Goal "!!i::hypreal. (i*u + m < j*u + n) = (m < (j-i)*u + n)"; by (asm_simp_tac - (simpset() addsimps [hypreal_diff_def, hypreal_add_mult_distrib]@ - hypreal_add_ac@rel_iff_rel_0_rls) 1); + (simpset() addsimps [hypreal_diff_def, left_distrib]@ + add_ac@rel_iff_rel_0_rls) 1); qed "hypreal_less_add_iff2"; Goal "!!i::hypreal. (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"; by (asm_simp_tac - (simpset() addsimps [hypreal_diff_def, hypreal_add_mult_distrib]@ - hypreal_add_ac@rel_iff_rel_0_rls) 1); + (simpset() addsimps [hypreal_diff_def, left_distrib]@ + add_ac@rel_iff_rel_0_rls) 1); qed "hypreal_le_add_iff1"; Goal "!!i::hypreal. (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"; by (asm_simp_tac - (simpset() addsimps [hypreal_diff_def, hypreal_add_mult_distrib]@ - hypreal_add_ac@rel_iff_rel_0_rls) 1); + (simpset() addsimps [hypreal_diff_def, left_distrib]@ + add_ac@rel_iff_rel_0_rls) 1); qed "hypreal_le_add_iff2"; Goal "-1 * (z::hypreal) = -z"; @@ -325,29 +325,26 @@ bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min]; (*To let us treat subtraction as addition*) -val diff_simps = [hypreal_diff_def, hypreal_minus_add_distrib, - hypreal_minus_minus]; +val diff_simps = [hypreal_diff_def, minus_add_distrib, minus_minus]; (*push the unary minus down: - x * y = x * - y *) val hypreal_minus_mult_eq_1_to_2 = - [hypreal_minus_mult_eq1 RS sym, hypreal_minus_mult_eq2] MRS trans + [minus_mult_left RS sym, minus_mult_right] MRS trans |> standard; (*to extract again any uncancelled minuses*) val hypreal_minus_from_mult_simps = - [hypreal_minus_minus, hypreal_minus_mult_eq1 RS sym, - hypreal_minus_mult_eq2 RS sym]; + [minus_minus, minus_mult_left RS sym, minus_mult_right RS sym]; (*combine unary minus with numeric literals, however nested within a product*) val hypreal_mult_minus_simps = - [hypreal_mult_assoc, hypreal_minus_mult_eq1, hypreal_minus_mult_eq_1_to_2]; + [hypreal_mult_assoc, minus_mult_left, hypreal_minus_mult_eq_1_to_2]; (*Final simplification: cancel + and * *) val simplify_meta_eq = Int_Numeral_Simprocs.simplify_meta_eq [hypreal_add_zero_left, hypreal_add_zero_right, - hypreal_mult_0, hypreal_mult_0_right, hypreal_mult_1, - hypreal_mult_1_right]; + mult_left_zero, mult_right_zero, mult_1, mult_1_right]; val prep_simproc = Real_Numeral_Simprocs.prep_simproc; @@ -361,11 +358,11 @@ val trans_tac = Real_Numeral_Simprocs.trans_tac val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ - hypreal_minus_simps@hypreal_add_ac)) + hypreal_minus_simps@add_ac)) THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@hypreal_mult_minus_simps)) THEN ALLGOALS (simp_tac (HOL_ss addsimps hypreal_minus_from_mult_simps@ - hypreal_add_ac@hypreal_mult_ac)) + add_ac@mult_ac)) val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps)) val simplify_meta_eq = simplify_meta_eq end; @@ -429,10 +426,10 @@ val trans_tac = Real_Numeral_Simprocs.trans_tac val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ - hypreal_minus_simps@hypreal_add_ac)) + hypreal_minus_simps@add_ac)) THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@hypreal_mult_minus_simps)) THEN ALLGOALS (simp_tac (HOL_ss addsimps hypreal_minus_from_mult_simps@ - hypreal_add_ac@hypreal_mult_ac)) + add_ac@mult_ac)) val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps)) val simplify_meta_eq = simplify_meta_eq @@ -461,7 +458,7 @@ (*Final simplification: cancel + and * *) fun cancel_simplify_meta_eq cancel_th th = Int_Numeral_Simprocs.simplify_meta_eq - [hypreal_mult_1, hypreal_mult_1_right] + [mult_1, mult_1_right] (([th, cancel_th]) MRS trans); (*** Making constant folding work for 0 and 1 too ***) @@ -559,7 +556,7 @@ val sg_ref = Sign.self_ref (Theory.sign_of (the_context ())) val T = Hyperreal_Numeral_Simprocs.hyprealT val plus = Const ("op *", [T,T] ---> T) - val add_ac = hypreal_mult_ac + val add_ac = mult_ac end; structure Hyperreal_Times_Assoc = Assoc_Fold (Hyperreal_Times_Assoc_Data); diff -r eb8b8241ef5b -r 8dbbb7cf3637 src/HOL/Hyperreal/HyperDef.thy --- a/src/HOL/Hyperreal/HyperDef.thy Thu Dec 25 23:18:04 2003 +0100 +++ b/src/HOL/Hyperreal/HyperDef.thy Sat Dec 27 21:02:14 2003 +0100 @@ -336,18 +336,7 @@ apply (simp add: hypreal_add real_add_assoc) done -(*For AC rewriting*) -lemma hypreal_add_left_commute: "(x::hypreal)+(y+z)=y+(x+z)" - apply (rule mk_left_commute [of "op +"]) - apply (rule hypreal_add_assoc) - apply (rule hypreal_add_commute) - done - -(* hypreal addition is an AC operator *) -lemmas hypreal_add_ac = - hypreal_add_assoc hypreal_add_commute hypreal_add_left_commute - -lemma hypreal_add_zero_left [simp]: "(0::hypreal) + z = z" +lemma hypreal_add_zero_left: "(0::hypreal) + z = z" apply (unfold hypreal_zero_def) apply (rule_tac z = z in eq_Abs_hypreal) apply (simp add: hypreal_add) @@ -376,27 +365,6 @@ UN_equiv_class [OF equiv_hyprel hypreal_minus_congruent]) done -lemma hypreal_minus_minus [simp]: "- (- z) = (z::hypreal)" -apply (rule_tac z = z in eq_Abs_hypreal) -apply (simp add: hypreal_minus) -done - -lemma inj_hypreal_minus: "inj(%r::hypreal. -r)" -apply (rule inj_onI) -apply (drule_tac f = uminus in arg_cong) -apply (simp add: hypreal_minus_minus) -done - -lemma hypreal_minus_zero [simp]: "- 0 = (0::hypreal)" -apply (unfold hypreal_zero_def) -apply (simp add: hypreal_minus) -done - -lemma hypreal_minus_zero_iff [simp]: "(-x = 0) = (x = (0::hypreal))" -apply (rule_tac z = x in eq_Abs_hypreal) -apply (auto simp add: hypreal_zero_def hypreal_minus) -done - lemma hypreal_diff: "Abs_hypreal(hyprel``{%n. X n}) - Abs_hypreal(hyprel``{%n. Y n}) = Abs_hypreal(hyprel``{%n. X n - Y n})" @@ -409,24 +377,9 @@ apply (simp add: hypreal_minus hypreal_add) done -lemma hypreal_add_minus_left [simp]: "-z + z = (0::hypreal)" +lemma hypreal_add_minus_left: "-z + z = (0::hypreal)" by (simp add: hypreal_add_commute hypreal_add_minus) -lemma hypreal_add_left_cancel: "((x::hypreal) + y = x + z) = (y = z)" -apply safe -apply (drule_tac f = "%t.-x + t" in arg_cong) -apply (simp add: hypreal_add_assoc [symmetric]) -done - -lemma hypreal_add_right_cancel: "(y + (x::hypreal)= z + x) = (y = z)" -by (simp add: hypreal_add_commute hypreal_add_left_cancel) - -lemma hypreal_add_minus_cancelA [simp]: "z + ((- z) + w) = (w::hypreal)" -by (simp add: hypreal_add_assoc [symmetric]) - -lemma hypreal_minus_add_cancelA [simp]: "(-z) + (z + w) = (w::hypreal)" -by (simp add: hypreal_add_assoc [symmetric]) - subsection{*Hyperreal Multiplication*} @@ -445,71 +398,22 @@ lemma hypreal_mult_commute: "(z::hypreal) * w = w * z" apply (rule_tac z = z in eq_Abs_hypreal) apply (rule_tac z = w in eq_Abs_hypreal) -apply (simp add: hypreal_mult real_mult_ac) +apply (simp add: hypreal_mult mult_ac) done lemma hypreal_mult_assoc: "((z1::hypreal) * z2) * z3 = z1 * (z2 * z3)" apply (rule_tac z = z1 in eq_Abs_hypreal) apply (rule_tac z = z2 in eq_Abs_hypreal) apply (rule_tac z = z3 in eq_Abs_hypreal) -apply (simp add: hypreal_mult real_mult_assoc) +apply (simp add: hypreal_mult mult_assoc) done -lemma hypreal_mult_left_commute: "(z1::hypreal) * (z2 * z3) = z2 * (z1 * z3)" - apply (rule mk_left_commute [of "op *"]) - apply (rule hypreal_mult_assoc) - apply (rule hypreal_mult_commute) - done - -(* hypreal multiplication is an AC operator *) -lemmas hypreal_mult_ac = - hypreal_mult_assoc hypreal_mult_commute hypreal_mult_left_commute - -lemma hypreal_mult_1 [simp]: "(1::hypreal) * z = z" +lemma hypreal_mult_1: "(1::hypreal) * z = z" apply (unfold hypreal_one_def) apply (rule_tac z = z in eq_Abs_hypreal) apply (simp add: hypreal_mult) done -lemma hypreal_mult_1_right [simp]: "z * (1::hypreal) = z" -by (simp add: hypreal_mult_commute hypreal_mult_1) - -lemma hypreal_mult_0 [simp]: "0 * z = (0::hypreal)" -apply (unfold hypreal_zero_def) -apply (rule_tac z = z in eq_Abs_hypreal) -apply (simp add: hypreal_mult) -done - -lemma hypreal_mult_0_right [simp]: "z * 0 = (0::hypreal)" -by (simp add: hypreal_mult_commute) - -lemma hypreal_minus_mult_eq1: "-(x * y) = -x * (y::hypreal)" -apply (rule_tac z = x in eq_Abs_hypreal) -apply (rule_tac z = y in eq_Abs_hypreal) -apply (auto simp add: hypreal_minus hypreal_mult real_mult_ac real_add_ac) -done - -lemma hypreal_minus_mult_eq2: "-(x * y) = (x::hypreal) * -y" -apply (rule_tac z = x in eq_Abs_hypreal) -apply (rule_tac z = y in eq_Abs_hypreal) -apply (auto simp add: hypreal_minus hypreal_mult real_mult_ac real_add_ac) -done - -(*Pull negations out*) -declare hypreal_minus_mult_eq2 [symmetric, simp] - hypreal_minus_mult_eq1 [symmetric, simp] - -lemma hypreal_mult_minus_1 [simp]: "(- (1::hypreal)) * z = -z" -by simp - -lemma hypreal_mult_minus_1_right [simp]: "z * (- (1::hypreal)) = -z" -by (subst hypreal_mult_commute, simp) - -lemma hypreal_minus_mult_commute: "(-x) * y = (x::hypreal) * -y" -by auto - -subsection{*A few more theorems *} - lemma hypreal_add_mult_distrib: "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)" apply (rule_tac z = z1 in eq_Abs_hypreal) @@ -518,23 +422,7 @@ apply (simp add: hypreal_mult hypreal_add real_add_mult_distrib) done -lemma hypreal_add_mult_distrib2: - "(w::hypreal) * (z1 + z2) = (w * z1) + (w * z2)" -by (simp add: hypreal_mult_commute [of w] hypreal_add_mult_distrib) - - -lemma hypreal_diff_mult_distrib: - "((z1::hypreal) - z2) * w = (z1 * w) - (z2 * w)" - -apply (unfold hypreal_diff_def) -apply (simp add: hypreal_add_mult_distrib) -done - -lemma hypreal_diff_mult_distrib2: - "(w::hypreal) * (z1 - z2) = (w * z1) - (w * z2)" -by (simp add: hypreal_mult_commute [of w] hypreal_diff_mult_distrib) - -(*** one and zero are distinct ***) +text{*one and zero are distinct*} lemma hypreal_zero_not_eq_one: "0 \ (1::hypreal)" apply (unfold hypreal_zero_def hypreal_one_def) apply (auto simp add: real_zero_not_eq_one) @@ -558,23 +446,7 @@ UN_equiv_class [OF equiv_hyprel hypreal_inverse_congruent]) done -lemma HYPREAL_INVERSE_ZERO: "inverse 0 = (0::hypreal)" -by (simp add: hypreal_inverse hypreal_zero_def) - -lemma HYPREAL_DIVISION_BY_ZERO: "a / (0::hypreal) = 0" -by (simp add: hypreal_divide_def HYPREAL_INVERSE_ZERO) - -instance hypreal :: division_by_zero -proof - fix x :: hypreal - show "inverse 0 = (0::hypreal)" by (rule HYPREAL_INVERSE_ZERO) - show "x/0 = 0" by (rule HYPREAL_DIVISION_BY_ZERO) -qed - - -subsection{*Existence of Inverse*} - -lemma hypreal_mult_inverse [simp]: +lemma hypreal_mult_inverse: "x \ 0 ==> x*inverse(x) = (1::hypreal)" apply (unfold hypreal_one_def hypreal_zero_def) apply (rule_tac z = x in eq_Abs_hypreal) @@ -583,10 +455,46 @@ apply (blast intro!: real_mult_inv_right FreeUltrafilterNat_subset) done -lemma hypreal_mult_inverse_left [simp]: +lemma hypreal_mult_inverse_left: "x \ 0 ==> inverse(x)*x = (1::hypreal)" by (simp add: hypreal_mult_inverse hypreal_mult_commute) +instance hypreal :: field +proof + fix x y z :: hypreal + show "(x + y) + z = x + (y + z)" by (rule hypreal_add_assoc) + show "x + y = y + x" by (rule hypreal_add_commute) + show "0 + x = x" by simp + show "- x + x = 0" by (simp add: hypreal_add_minus_left) + show "x - y = x + (-y)" by (simp add: hypreal_diff_def) + show "(x * y) * z = x * (y * z)" by (rule hypreal_mult_assoc) + show "x * y = y * x" by (rule hypreal_mult_commute) + show "1 * x = x" by (simp add: hypreal_mult_1) + show "(x + y) * z = x * z + y * z" by (simp add: hypreal_add_mult_distrib) + show "0 \ (1::hypreal)" by (rule hypreal_zero_not_eq_one) + show "x \ 0 ==> inverse x * x = 1" by (simp add: hypreal_mult_inverse_left) + show "y \ 0 ==> x / y = x * inverse y" by (simp add: hypreal_divide_def) +qed + +(*Pull negations out*) +declare minus_mult_right [symmetric, simp] + minus_mult_left [symmetric, simp] + + +lemma HYPREAL_INVERSE_ZERO: "inverse 0 = (0::hypreal)" +by (simp add: hypreal_inverse hypreal_zero_def) + +lemma HYPREAL_DIVISION_BY_ZERO: "a / (0::hypreal) = 0" +by (simp add: hypreal_divide_def HYPREAL_INVERSE_ZERO + hypreal_mult_commute [of a]) + +instance hypreal :: division_by_zero +proof + fix x :: hypreal + show "inverse 0 = (0::hypreal)" by (rule HYPREAL_INVERSE_ZERO) + show "x/0 = 0" by (rule HYPREAL_DIVISION_BY_ZERO) +qed + subsection{*Theorems for Ordering*} @@ -603,8 +511,6 @@ apply (auto intro!: lemma_hyprel_refl, ultra) done -(* prove introduction and elimination rules for hypreal_less *) - lemma hypreal_less_not_refl: "~ (R::hypreal) < R" apply (rule_tac z = R in eq_Abs_hypreal) apply (auto simp add: hypreal_less_def, ultra) @@ -656,8 +562,6 @@ apply (insert hypreal_trichotomy [of x], blast) done -subsection{*More properties of Less Than*} - lemma hypreal_less_minus_iff: "((x::hypreal) < y) = (0 < y + -x)" apply (rule_tac z = x in eq_Abs_hypreal) apply (rule_tac z = y in eq_Abs_hypreal) @@ -670,19 +574,11 @@ apply (auto simp add: hypreal_add hypreal_zero_def hypreal_minus hypreal_less) done -lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)" -apply auto -apply (rule_tac x1 = "-y" in hypreal_add_right_cancel [THEN iffD1], auto) -done - lemma hypreal_eq_minus_iff2: "((x::hypreal) = y) = (0 = y + - x)" apply auto -apply (rule_tac x1 = "-x" in hypreal_add_right_cancel [THEN iffD1], auto) +apply (rule Ring_and_Field.add_right_cancel [of _ "-x", THEN iffD1], auto) done - -subsection{*Linearity*} - lemma hypreal_linear: "(x::hypreal) < y | x = y | y < x" apply (subst hypreal_eq_minus_iff2) apply (rule_tac x1 = x in hypreal_less_minus_iff [THEN ssubst]) @@ -710,22 +606,6 @@ apply (ultra+) done -lemma hypreal_leI: - "~(w < z) ==> z <= (w::hypreal)" -apply (unfold hypreal_le_def, assumption) -done - -lemma hypreal_leD: - "z<=w ==> ~(w<(z::hypreal))" -apply (unfold hypreal_le_def, assumption) -done - -lemma hypreal_less_le_iff: "(~(w < z)) = (z <= (w::hypreal))" -by (fast intro!: hypreal_leI hypreal_leD) - -lemma not_hypreal_leE: "~ z <= w ==> w<(z::hypreal)" -by (unfold hypreal_le_def, fast) - lemma hypreal_le_imp_less_or_eq: "!!(x::hypreal). x <= y ==> x < y | x = y" apply (unfold hypreal_le_def) apply (cut_tac hypreal_linear) @@ -780,49 +660,6 @@ instance hypreal :: linorder by (intro_classes, rule hypreal_le_linear) -lemma hypreal_minus_zero_less_iff [simp]: "(0 < -R) = (R < (0::hypreal))" -apply (rule_tac z = R in eq_Abs_hypreal) -apply (auto simp add: hypreal_zero_def hypreal_less hypreal_minus) -done - -lemma hypreal_minus_zero_less_iff2 [simp]: "(-R < 0) = ((0::hypreal) < R)" -apply (rule_tac z = R in eq_Abs_hypreal) -apply (auto simp add: hypreal_zero_def hypreal_less hypreal_minus) -done - -lemma hypreal_minus_zero_le_iff [simp]: "((0::hypreal) <= -r) = (r <= 0)" -apply (unfold hypreal_le_def) -apply (simp add: hypreal_minus_zero_less_iff2) -done - -lemma hypreal_minus_zero_le_iff2 [simp]: "(-r <= (0::hypreal)) = (0 <= r)" -apply (unfold hypreal_le_def) -apply (simp add: hypreal_minus_zero_less_iff2) -done - - -lemma hypreal_self_eq_minus_self_zero: "x = -x ==> x = (0::hypreal)" -apply (rule_tac z = x in eq_Abs_hypreal) -apply (auto simp add: hypreal_minus hypreal_zero_def, ultra) -done - -lemma hypreal_add_self_zero_cancel [simp]: "(x + x = 0) = (x = (0::hypreal))" -apply (rule_tac z = x in eq_Abs_hypreal) -apply (auto simp add: hypreal_add hypreal_zero_def) -done - -lemma hypreal_add_self_zero_cancel2 [simp]: - "(x + x + y = y) = (x = (0::hypreal))" -apply auto -apply (drule hypreal_eq_minus_iff [THEN iffD1]) -apply (auto simp add: hypreal_add_assoc hypreal_self_eq_minus_self_zero) -done - -lemma hypreal_minus_eq_swap: "(b = -a) = (-b = (a::hypreal))" -by auto - -lemma hypreal_minus_eq_cancel [simp]: "(-b = -a) = (b = (a::hypreal))" -by (simp add: hypreal_minus_eq_swap) lemma hypreal_add_less_mono1: "(A::hypreal) < B ==> A + C < B + C" apply (rule_tac z = A in eq_Abs_hypreal) @@ -849,7 +686,7 @@ apply (drule hypreal_less_minus_iff [THEN iffD1]) apply (rule hypreal_less_minus_iff [THEN iffD2]) apply (drule hypreal_mult_order, assumption) -apply (simp add: hypreal_add_mult_distrib2 hypreal_mult_commute) +apply (simp add: right_distrib hypreal_mult_commute) done lemma hypreal_mult_less_mono2: "[| (0::hypreal) z*x (1::hypreal)" by (rule hypreal_zero_not_eq_one) show "x \ y ==> z + x \ z + y" by (rule hypreal_add_left_le_mono1) show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: hypreal_mult_less_mono2) show "\x\ = (if x < 0 then -x else x)" by (auto dest: order_le_less_trans simp add: hrabs_def linorder_not_le) - show "x \ 0 ==> inverse x * x = 1" by simp - show "y \ 0 ==> x / y = x * inverse y" by (simp add: hypreal_divide_def) qed -lemma hypreal_minus_add_distrib [simp]: "-(x + (y::hypreal)) = -x + -y" - by (rule Ring_and_Field.minus_add_distrib) +lemma hypreal_mult_1_right: "z * (1::hypreal) = z" + by (rule Ring_and_Field.mult_1_right) + +lemma hypreal_mult_minus_1 [simp]: "(- (1::hypreal)) * z = -z" +by (simp) + +lemma hypreal_mult_minus_1_right [simp]: "z * (- (1::hypreal)) = -z" +by (subst hypreal_mult_commute, simp) (*Used ONCE: in NSA.ML*) lemma hypreal_minus_distrib1: "-(y + -(x::hypreal)) = x + -y" @@ -892,6 +721,12 @@ lemma hypreal_eq_minus_iff3: "(x = y + z) = (x + -z = (y::hypreal))" by (auto simp add: hypreal_add_assoc) +lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)" +apply auto +apply (rule Ring_and_Field.add_right_cancel [of _ "-y", THEN iffD1], auto) +done + +(*Used 3 TIMES: in Lim.ML*) lemma hypreal_not_eq_minus_iff: "(x \ a) = (x + -a \ (0::hypreal))" by (auto dest: hypreal_eq_minus_iff [THEN iffD2]) @@ -938,13 +773,13 @@ lemma hypreal_of_real_add [simp]: "hypreal_of_real (z1 + z2) = hypreal_of_real z1 + hypreal_of_real z2" apply (unfold hypreal_of_real_def) -apply (simp add: hypreal_add hypreal_add_mult_distrib) +apply (simp add: hypreal_add left_distrib) done lemma hypreal_of_real_mult [simp]: "hypreal_of_real (z1 * z2) = hypreal_of_real z1 * hypreal_of_real z2" apply (unfold hypreal_of_real_def) -apply (simp add: hypreal_mult hypreal_add_mult_distrib2) +apply (simp add: hypreal_mult right_distrib) done lemma hypreal_of_real_less_iff [simp]: @@ -1069,44 +904,24 @@ val eq_Abs_hypreal = thm "eq_Abs_hypreal"; val hypreal_minus_congruent = thm "hypreal_minus_congruent"; val hypreal_minus = thm "hypreal_minus"; -val hypreal_minus_minus = thm "hypreal_minus_minus"; -val inj_hypreal_minus = thm "inj_hypreal_minus"; -val hypreal_minus_zero = thm "hypreal_minus_zero"; -val hypreal_minus_zero_iff = thm "hypreal_minus_zero_iff"; val hypreal_add_congruent2 = thm "hypreal_add_congruent2"; val hypreal_add = thm "hypreal_add"; val hypreal_diff = thm "hypreal_diff"; val hypreal_add_commute = thm "hypreal_add_commute"; val hypreal_add_assoc = thm "hypreal_add_assoc"; -val hypreal_add_left_commute = thm "hypreal_add_left_commute"; val hypreal_add_zero_left = thm "hypreal_add_zero_left"; val hypreal_add_zero_right = thm "hypreal_add_zero_right"; val hypreal_add_minus = thm "hypreal_add_minus"; val hypreal_add_minus_left = thm "hypreal_add_minus_left"; -val hypreal_minus_add_distrib = thm "hypreal_minus_add_distrib"; val hypreal_minus_distrib1 = thm "hypreal_minus_distrib1"; -val hypreal_add_left_cancel = thm "hypreal_add_left_cancel"; -val hypreal_add_right_cancel = thm "hypreal_add_right_cancel"; -val hypreal_add_minus_cancelA = thm "hypreal_add_minus_cancelA"; -val hypreal_minus_add_cancelA = thm "hypreal_minus_add_cancelA"; val hypreal_mult_congruent2 = thm "hypreal_mult_congruent2"; val hypreal_mult = thm "hypreal_mult"; val hypreal_mult_commute = thm "hypreal_mult_commute"; val hypreal_mult_assoc = thm "hypreal_mult_assoc"; -val hypreal_mult_left_commute = thm "hypreal_mult_left_commute"; val hypreal_mult_1 = thm "hypreal_mult_1"; val hypreal_mult_1_right = thm "hypreal_mult_1_right"; -val hypreal_mult_0 = thm "hypreal_mult_0"; -val hypreal_mult_0_right = thm "hypreal_mult_0_right"; -val hypreal_minus_mult_eq1 = thm "hypreal_minus_mult_eq1"; -val hypreal_minus_mult_eq2 = thm "hypreal_minus_mult_eq2"; val hypreal_mult_minus_1 = thm "hypreal_mult_minus_1"; val hypreal_mult_minus_1_right = thm "hypreal_mult_minus_1_right"; -val hypreal_minus_mult_commute = thm "hypreal_minus_mult_commute"; -val hypreal_add_mult_distrib = thm "hypreal_add_mult_distrib"; -val hypreal_add_mult_distrib2 = thm "hypreal_add_mult_distrib2"; -val hypreal_diff_mult_distrib = thm "hypreal_diff_mult_distrib"; -val hypreal_diff_mult_distrib2 = thm "hypreal_diff_mult_distrib2"; val hypreal_zero_not_eq_one = thm "hypreal_zero_not_eq_one"; val hypreal_inverse_congruent = thm "hypreal_inverse_congruent"; val hypreal_inverse = thm "hypreal_inverse"; @@ -1121,6 +936,7 @@ val hypreal_minus_inverse = thm "hypreal_minus_inverse"; val hypreal_inverse_distrib = thm "hypreal_inverse_distrib"; val hypreal_less_not_refl = thm "hypreal_less_not_refl"; +val hypreal_less_irrefl = thm"hypreal_less_irrefl"; val hypreal_not_refl2 = thm "hypreal_not_refl2"; val hypreal_less_trans = thm "hypreal_less_trans"; val hypreal_less_asym = thm "hypreal_less_asym"; @@ -1136,22 +952,13 @@ val hypreal_neq_iff = thm "hypreal_neq_iff"; val hypreal_linear_less2 = thm "hypreal_linear_less2"; val hypreal_le = thm "hypreal_le"; -val hypreal_leI = thm "hypreal_leI"; -val hypreal_leD = thm "hypreal_leD"; -val hypreal_less_le_iff = thm "hypreal_less_le_iff"; -val not_hypreal_leE = thm "not_hypreal_leE"; val hypreal_le_imp_less_or_eq = thm "hypreal_le_imp_less_or_eq"; -val hypreal_less_or_eq_imp_le = thm "hypreal_less_or_eq_imp_le"; val hypreal_le_eq_less_or_eq = thm "hypreal_le_eq_less_or_eq"; val hypreal_le_refl = thm "hypreal_le_refl"; val hypreal_le_linear = thm "hypreal_le_linear"; val hypreal_le_trans = thm "hypreal_le_trans"; val hypreal_le_anti_sym = thm "hypreal_le_anti_sym"; val hypreal_less_le = thm "hypreal_less_le"; -val hypreal_minus_zero_less_iff = thm "hypreal_minus_zero_less_iff"; -val hypreal_minus_zero_less_iff2 = thm "hypreal_minus_zero_less_iff2"; -val hypreal_minus_zero_le_iff = thm "hypreal_minus_zero_le_iff"; -val hypreal_minus_zero_le_iff2 = thm "hypreal_minus_zero_le_iff2"; val hypreal_of_real_add = thm "hypreal_of_real_add"; val hypreal_of_real_mult = thm "hypreal_of_real_mult"; val hypreal_of_real_less_iff = thm "hypreal_of_real_less_iff"; @@ -1166,15 +973,9 @@ val hypreal_divide_one = thm "hypreal_divide_one"; val hypreal_add_divide_distrib = thm "hypreal_add_divide_distrib"; val hypreal_inverse_add = thm "hypreal_inverse_add"; -val hypreal_self_eq_minus_self_zero = thm "hypreal_self_eq_minus_self_zero"; -val hypreal_add_self_zero_cancel = thm "hypreal_add_self_zero_cancel"; -val hypreal_add_self_zero_cancel2 = thm "hypreal_add_self_zero_cancel2"; -val hypreal_minus_eq_swap = thm "hypreal_minus_eq_swap"; -val hypreal_minus_eq_cancel = thm "hypreal_minus_eq_cancel"; val hypreal_zero_num = thm "hypreal_zero_num"; val hypreal_one_num = thm "hypreal_one_num"; val hypreal_omega_gt_zero = thm "hypreal_omega_gt_zero"; *} - end diff -r eb8b8241ef5b -r 8dbbb7cf3637 src/HOL/Hyperreal/HyperOrd.thy --- a/src/HOL/Hyperreal/HyperOrd.thy Thu Dec 25 23:18:04 2003 +0100 +++ b/src/HOL/Hyperreal/HyperOrd.thy Sat Dec 27 21:02:14 2003 +0100 @@ -7,29 +7,15 @@ theory HyperOrd = HyperDef: +ML +{* +val left_distrib = thm"left_distrib"; +*} (*** Monotonicity results ***) -lemma hypreal_add_right_cancel_less: "(v+z < w+z) = (v < (w::hypreal))" - by (rule Ring_and_Field.add_less_cancel_right) - -lemma hypreal_add_left_cancel_less: "(z+v < z+w) = (v < (w::hypreal))" - by (rule Ring_and_Field.add_less_cancel_left) - -lemma hypreal_add_right_cancel_le: "(v+z \ w+z) = (v \ (w::hypreal))" - by (rule Ring_and_Field.add_le_cancel_right) - -lemma hypreal_add_left_cancel_le: "(z+v \ z+w) = (v \ (w::hypreal))" - by (rule Ring_and_Field.add_le_cancel_left) - -lemma hypreal_add_less_mono: "[| (z1::hypreal) < y1; z2 < y2 |] ==> z1 + z2 < y1 + y2" - by (rule Ring_and_Field.add_strict_mono) - -lemma hypreal_add_le_mono: "[|(i::hypreal)\j; k\l |] ==> i + k \ j + l" - by (rule Ring_and_Field.add_mono) - lemma hypreal_add_less_le_mono: "[|(i::hypreal)l |] ==> i + k < j + l" -by (auto dest!: order_le_imp_less_or_eq intro: hypreal_add_less_mono1 hypreal_add_less_mono) +by (auto dest!: order_le_imp_less_or_eq intro: hypreal_add_less_mono1 add_strict_mono) lemma hypreal_add_less_mono2: "!!(A::hypreal). A < B ==> C + A < C + B" by (auto intro: hypreal_add_less_mono1 simp add: hypreal_add_commute) @@ -43,18 +29,11 @@ apply (simp (no_asm_use)) done -lemma hypreal_less_add_left_cancel: "(C::hypreal) + A < C + B ==> A < B" -apply (simp (no_asm_use)) -done - lemma hypreal_add_zero_less_le_mono: "[|r < x; (0::hypreal) \ y|] ==> r < x + y" by (auto dest: hypreal_add_less_le_mono) -lemma hypreal_le_add_right_cancel: "!!(A::hypreal). A + C \ B + C ==> A \ B" - by (rule Ring_and_Field.add_le_imp_le_right) - lemma hypreal_le_add_left_cancel: "!!(A::hypreal). C + A \ C + B ==> A \ B" -apply (simp add: ); +apply simp done lemma hypreal_le_square [simp]: "(0::hypreal) \ x*x" @@ -112,9 +91,6 @@ (* existence of infinitesimal number also not *) (* corresponding to any real number *) -lemma real_of_nat_inverse_inj: "inverse (real (x::nat)) = inverse (real y) ==> x = y" -by (rule inj_real_of_nat [THEN injD], simp) - lemma lemma_epsilon_empty_singleton_disj: "{n::nat. x = inverse(real(Suc n))} = {} | (\y. {n::nat. x = inverse(real(Suc n))} = {y})" apply (auto simp add: inj_real_of_nat [THEN inj_eq]) @@ -139,72 +115,16 @@ by (simp add: hypreal_inverse omega_def epsilon_def) -subsection{*Routine Properties*} - -(* this proof is so much simpler than one for reals!! *) -lemma hypreal_inverse_less_swap: - "[| 0 < r; r < x |] ==> inverse x < inverse (r::hypreal)" - by (rule Ring_and_Field.less_imp_inverse_less) - -lemma hypreal_inverse_less_iff: - "[| 0 < r; 0 < x|] ==> (inverse x < inverse (r::hypreal)) = (r < x)" -by (rule Ring_and_Field.inverse_less_iff_less) - -lemma hypreal_inverse_le_iff: - "[| 0 < r; 0 < x|] ==> (inverse x \ inverse r) = (r \ (x::hypreal))" -by (rule Ring_and_Field.inverse_le_iff_le) - - -subsection{*Convenient Biconditionals for Products of Signs*} - -lemma hypreal_0_less_mult_iff: - "((0::hypreal) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)" - by (rule Ring_and_Field.zero_less_mult_iff) - -lemma hypreal_0_le_mult_iff: "((0::hypreal) \ x*y) = (0 \ x & 0 \ y | x \ 0 & y \ 0)" - by (rule Ring_and_Field.zero_le_mult_iff) - -lemma hypreal_mult_less_0_iff: "(x*y < (0::hypreal)) = (0 < x & y < 0 | x < 0 & 0 < y)" - by (rule Ring_and_Field.mult_less_0_iff) - -lemma hypreal_mult_le_0_iff: "(x*y \ (0::hypreal)) = (0 \ x & y \ 0 | x \ 0 & 0 \ y)" - by (rule Ring_and_Field.mult_le_0_iff) - - -lemma hypreal_mult_self_sum_ge_zero: "(0::hypreal) \ x*x + y*y" -proof - - have "0 + 0 \ x*x + y*y" by (blast intro: add_mono zero_le_square) - thus ?thesis by simp -qed - -(*TO BE DELETED*) -ML -{* -val hypreal_add_ac = thms"hypreal_add_ac"; -val hypreal_mult_ac = thms"hypreal_mult_ac"; - -val hypreal_less_irrefl = thm"hypreal_less_irrefl"; -*} - ML {* val hypreal_add_less_mono1 = thm"hypreal_add_less_mono1"; -val hypreal_add_less_mono2 = thm"hypreal_add_less_mono2"; val hypreal_mult_order = thm"hypreal_mult_order"; val hypreal_le_add_order = thm"hypreal_le_add_order"; -val hypreal_add_right_cancel_less = thm"hypreal_add_right_cancel_less"; -val hypreal_add_left_cancel_less = thm"hypreal_add_left_cancel_less"; -val hypreal_add_right_cancel_le = thm"hypreal_add_right_cancel_le"; -val hypreal_add_left_cancel_le = thm"hypreal_add_left_cancel_le"; -val hypreal_add_less_mono = thm"hypreal_add_less_mono"; val hypreal_add_left_le_mono1 = thm"hypreal_add_left_le_mono1"; -val hypreal_add_le_mono = thm"hypreal_add_le_mono"; val hypreal_add_less_le_mono = thm"hypreal_add_less_le_mono"; val hypreal_add_le_less_mono = thm"hypreal_add_le_less_mono"; val hypreal_less_add_right_cancel = thm"hypreal_less_add_right_cancel"; -val hypreal_less_add_left_cancel = thm"hypreal_less_add_left_cancel"; val hypreal_add_zero_less_le_mono = thm"hypreal_add_zero_less_le_mono"; -val hypreal_le_add_right_cancel = thm"hypreal_le_add_right_cancel"; val hypreal_le_add_left_cancel = thm"hypreal_le_add_left_cancel"; val hypreal_le_square = thm"hypreal_le_square"; val hypreal_mult_less_mono1 = thm"hypreal_mult_less_mono1"; @@ -217,21 +137,10 @@ val lemma_finite_omega_set = thm"lemma_finite_omega_set"; val not_ex_hypreal_of_real_eq_omega = thm"not_ex_hypreal_of_real_eq_omega"; val hypreal_of_real_not_eq_omega = thm"hypreal_of_real_not_eq_omega"; -val real_of_nat_inverse_inj = thm"real_of_nat_inverse_inj"; -val lemma_epsilon_empty_singleton_disj = thm"lemma_epsilon_empty_singleton_disj"; -val lemma_finite_epsilon_set = thm"lemma_finite_epsilon_set"; val not_ex_hypreal_of_real_eq_epsilon = thm"not_ex_hypreal_of_real_eq_epsilon"; val hypreal_of_real_not_eq_epsilon = thm"hypreal_of_real_not_eq_epsilon"; val hypreal_epsilon_not_zero = thm"hypreal_epsilon_not_zero"; val hypreal_epsilon_inverse_omega = thm"hypreal_epsilon_inverse_omega"; -val hypreal_inverse_less_swap = thm"hypreal_inverse_less_swap"; -val hypreal_inverse_less_iff = thm"hypreal_inverse_less_iff"; -val hypreal_inverse_le_iff = thm"hypreal_inverse_le_iff"; -val hypreal_0_less_mult_iff = thm"hypreal_0_less_mult_iff"; -val hypreal_0_le_mult_iff = thm"hypreal_0_le_mult_iff"; -val hypreal_mult_less_0_iff = thm"hypreal_mult_less_0_iff"; -val hypreal_mult_le_0_iff = thm"hypreal_mult_le_0_iff"; -val hypreal_mult_self_sum_ge_zero = thm "hypreal_mult_self_sum_ge_zero"; *} end diff -r eb8b8241ef5b -r 8dbbb7cf3637 src/HOL/Hyperreal/HyperPow.ML --- a/src/HOL/Hyperreal/HyperPow.ML Thu Dec 25 23:18:04 2003 +0100 +++ b/src/HOL/Hyperreal/HyperPow.ML Sat Dec 27 21:02:14 2003 +0100 @@ -28,7 +28,7 @@ Goal "(r::hypreal) ^ (n + m) = (r ^ n) * (r ^ m)"; by (induct_tac "n" 1); -by (auto_tac (claset(), simpset() addsimps hypreal_mult_ac)); +by (auto_tac (claset(), simpset() addsimps mult_ac)); qed "hrealpow_add"; Goal "(r::hypreal) ^ Suc 0 = r"; @@ -42,12 +42,12 @@ Goal "(0::hypreal) <= r --> 0 <= r ^ n"; by (induct_tac "n" 1); -by (auto_tac (claset(), simpset() addsimps [hypreal_0_le_mult_iff])); +by (auto_tac (claset(), simpset() addsimps [zero_le_mult_iff])); qed_spec_mp "hrealpow_ge_zero"; Goal "(0::hypreal) < r --> 0 < r ^ n"; by (induct_tac "n" 1); -by (auto_tac (claset(), simpset() addsimps [hypreal_0_less_mult_iff])); +by (auto_tac (claset(), simpset() addsimps [zero_less_mult_iff])); qed_spec_mp "hrealpow_gt_zero"; Goal "x <= y & (0::hypreal) < x --> x ^ n <= y ^ n"; @@ -81,11 +81,11 @@ Goal "((r::hypreal) * s) ^ n = (r ^ n) * (s ^ n)"; by (induct_tac "n" 1); -by (auto_tac (claset(), simpset() addsimps hypreal_mult_ac)); +by (auto_tac (claset(), simpset() addsimps mult_ac)); qed "hrealpow_mult"; Goal "(0::hypreal) <= r ^ Suc (Suc 0)"; -by (auto_tac (claset(), simpset() addsimps [hypreal_0_le_mult_iff])); +by (auto_tac (claset(), simpset() addsimps [zero_le_mult_iff])); qed "hrealpow_two_le"; Addsimps [hrealpow_two_le]; @@ -117,7 +117,7 @@ Goal "abs(x ^ Suc (Suc 0)) = (x::hypreal) ^ Suc (Suc 0)"; by (auto_tac (claset(), - simpset() addsimps [hrabs_def, hypreal_0_le_mult_iff])); + simpset() addsimps [hrabs_def, zero_le_mult_iff])); qed "hrabs_hrealpow_two"; Addsimps [hrabs_hrealpow_two]; @@ -149,7 +149,7 @@ Goal "hypreal_of_nat n < 2 ^ n"; by (induct_tac "n" 1); by (auto_tac (claset(), - simpset() addsimps [hypreal_of_nat_Suc, hypreal_add_mult_distrib])); + simpset() addsimps [hypreal_of_nat_Suc, left_distrib])); by (cut_inst_tac [("n","n")] two_hrealpow_ge_one 1); by (arith_tac 1); qed "two_hrealpow_gt"; @@ -198,7 +198,7 @@ Goal "(x + (y::hypreal)) ^ Suc (Suc 0) = \ \ x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + (hypreal_of_nat (Suc (Suc 0)))*x*y"; by (simp_tac (simpset() addsimps - [hypreal_add_mult_distrib2, hypreal_add_mult_distrib, + [right_distrib, left_distrib, hypreal_of_nat_zero, hypreal_of_nat_Suc]) 1); qed "hrealpow_sum_square_expand"; @@ -379,7 +379,7 @@ Goal "(0::hypreal) <= r pow ((1::hypnat) + (1::hypnat))"; by (auto_tac (claset(), - simpset() addsimps [hyperpow_two, hypreal_0_le_mult_iff])); + simpset() addsimps [hyperpow_two, zero_le_mult_iff])); qed "hyperpow_two_le"; Addsimps [hyperpow_two_le]; @@ -532,7 +532,7 @@ (* MOVE UP *) Goal "(0::hypreal) <= x * x"; by (auto_tac (claset(),simpset() addsimps - [hypreal_0_le_mult_iff])); + [zero_le_mult_iff])); qed "hypreal_mult_self_ge_zero"; Addsimps [hypreal_mult_self_ge_zero]; diff -r eb8b8241ef5b -r 8dbbb7cf3637 src/HOL/Hyperreal/Lim.ML --- a/src/HOL/Hyperreal/Lim.ML Thu Dec 25 23:18:04 2003 +0100 +++ b/src/HOL/Hyperreal/Lim.ML Sat Dec 27 21:02:14 2003 +0100 @@ -825,7 +825,7 @@ by Safe_tac; by (dres_inst_tac [("x","x + -a")] spec 1); by (dres_inst_tac [("x","x + a")] spec 2); -by (auto_tac (claset(), simpset() addsimps real_add_ac)); +by (auto_tac (claset(), simpset() addsimps add_ac)); qed "DERIV_LIM_iff"; Goalw [deriv_def] "(DERIV f x :> D) = \ @@ -983,7 +983,7 @@ simpset() addsimps [hypreal_add_divide_distrib])); by (dres_inst_tac [("b","hypreal_of_real Da"), ("d","hypreal_of_real Db")] approx_add 1); -by (auto_tac (claset(), simpset() addsimps hypreal_add_ac)); +by (auto_tac (claset(), simpset() addsimps add_ac)); qed "NSDERIV_add"; (* Standard theorem *) @@ -999,7 +999,7 @@ ----------------------------------------------------*) Goal "((a::hypreal)*b) + -(c*d) = (b*(a + -c)) + (c*(b + -d))"; -by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib2]) 1); +by (simp_tac (simpset() addsimps [right_distrib]) 1); val lemma_nsderiv1 = result(); Goal "[| (x + y) / z = hypreal_of_real D + yb; z \\ 0; \ @@ -1028,7 +1028,7 @@ by (dres_inst_tac [("D","Db")] lemma_nsderiv2 1); by (dtac (approx_minus_iff RS iffD2 RS (bex_Infinitesimal_iff2 RS iffD2)) 4); by (auto_tac (claset() addSIs [approx_add_mono1], - simpset() addsimps [hypreal_add_mult_distrib, hypreal_add_mult_distrib2, + simpset() addsimps [left_distrib, right_distrib, hypreal_mult_commute, hypreal_add_assoc])); by (res_inst_tac [("w1","hypreal_of_real Db * hypreal_of_real (f x)")] (hypreal_add_commute RS subst) 1); @@ -1051,9 +1051,8 @@ Goal "NSDERIV f x :> D \ \ ==> NSDERIV (%x. c * f x) x :> c*D"; by (asm_full_simp_tac - (simpset() addsimps [times_divide_eq_right RS sym, NSDERIV_NSLIM_iff, - real_minus_mult_eq2, real_add_mult_distrib2 RS sym] - delsimps [times_divide_eq_right, real_mult_minus_eq2]) 1); + (HOL_ss addsimps [times_divide_eq_right RS sym, NSDERIV_NSLIM_iff, + real_minus_mult_eq2, real_add_mult_distrib2 RS sym]) 1); by (etac (NSLIM_const RS NSLIM_mult) 1); qed "NSDERIV_cmult"; @@ -1064,9 +1063,8 @@ "DERIV f x :> D \ \ ==> DERIV (%x. c * f x) x :> c*D"; by (asm_full_simp_tac - (simpset() addsimps [times_divide_eq_right RS sym, NSDERIV_NSLIM_iff, - real_minus_mult_eq2, real_add_mult_distrib2 RS sym] - delsimps [times_divide_eq_right, real_mult_minus_eq2]) 1); + (HOL_ss addsimps [times_divide_eq_right RS sym, NSDERIV_NSLIM_iff, + real_minus_mult_eq2, real_add_mult_distrib2 RS sym]) 1); by (etac (LIM_const RS LIM_mult2) 1); qed "DERIV_cmult"; @@ -1142,7 +1140,7 @@ by (asm_full_simp_tac (simpset() addsimps [times_divide_eq_right RS sym] delsimps [times_divide_eq_right]) 1); by (auto_tac (claset(), - simpset() addsimps [hypreal_add_mult_distrib])); + simpset() addsimps [left_distrib])); qed "increment_thm"; Goal "[| NSDERIV f x :> D; h \\ 0; h \\ 0 |] \ @@ -1156,7 +1154,7 @@ \ ==> increment f x h \\ 0"; by (dtac increment_thm2 1 THEN auto_tac (claset() addSIs [Infinitesimal_HFinite_mult2,HFinite_add],simpset() addsimps - [hypreal_add_mult_distrib RS sym,mem_infmal_iff RS sym])); + [left_distrib RS sym,mem_infmal_iff RS sym])); by (etac (Infinitesimal_subset_HFinite RS subsetD) 1); qed "increment_approx_zero"; @@ -1321,19 +1319,19 @@ by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 2); by (auto_tac (claset(), simpset() addsimps [starfun_inverse_inverse, realpow_two] - delsimps [hypreal_minus_mult_eq1 RS sym, - hypreal_minus_mult_eq2 RS sym])); + delsimps [minus_mult_left RS sym, + minus_mult_right RS sym])); by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse_add, hypreal_inverse_distrib RS sym, hypreal_minus_inverse RS sym] - @ hypreal_add_ac @ hypreal_mult_ac + @ add_ac @ mult_ac delsimps [inverse_mult_distrib,inverse_minus_eq, - hypreal_minus_mult_eq1 RS sym, - hypreal_minus_mult_eq2 RS sym] ) 1); + minus_mult_left RS sym, + minus_mult_right 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); + right_distrib] + delsimps [minus_mult_left RS sym, + minus_mult_right RS sym]) 1); by (res_inst_tac [("y"," inverse(- hypreal_of_real x * hypreal_of_real x)")] approx_trans 1); by (rtac inverse_add_Infinitesimal_approx2 1); @@ -1356,8 +1354,7 @@ Goal "[| DERIV f x :> d; f(x) \\ 0 |] \ \ ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"; by (rtac (real_mult_commute RS subst) 1); -by (asm_simp_tac (simpset() addsimps [real_minus_mult_eq1, - realpow_inverse] delsimps [realpow_Suc, real_mult_minus_eq1]) 1); +by (asm_simp_tac (HOL_ss addsimps [real_minus_mult_eq1, realpow_inverse]) 1); by (fold_goals_tac [o_def]); by (blast_tac (claset() addSIs [DERIV_chain,DERIV_inverse]) 1); qed "DERIV_inverse_fun"; @@ -1379,7 +1376,8 @@ by (asm_full_simp_tac (simpset() addsimps [real_divide_def, real_add_mult_distrib2, realpow_inverse,real_minus_mult_eq1] @ real_mult_ac - delsimps [realpow_Suc, real_mult_minus_eq1, real_mult_minus_eq2]) 1); + delsimps [realpow_Suc, real_mult_minus_eq1, real_mult_minus_eq2, + minus_mult_right RS sym, minus_mult_left RS sym]) 1); qed "DERIV_quotient"; Goal "[| NSDERIV f x :> d; DERIV g x :> e; g(x) \\ 0 |] \ @@ -1556,7 +1554,7 @@ simpset() addsimps [eq_divide_2_times_iff, real_add_divide_distrib, Let_def, split_def])); by (auto_tac (claset(), - simpset() addsimps (real_add_ac@[Bolzano_bisect_le, real_diff_def]))); + simpset() addsimps (add_ac@[Bolzano_bisect_le, real_diff_def]))); qed "Bolzano_bisect_diff"; val Bolzano_nest_unique = @@ -1822,8 +1820,8 @@ by (REPEAT(dres_inst_tac [("x","a")] spec 1)); by (Asm_full_simp_tac 1); by (asm_full_simp_tac - (simpset() addsimps [inverse_eq_divide, pos_real_divide_le_eq]) 1); -by (cut_inst_tac [("x","k"),("y","M-f a")] real_0_less_mult_iff 1); + (simpset() addsimps [inverse_eq_divide, pos_divide_le_eq]) 1); +by (cut_inst_tac [("a","k"),("b","M-f a")] zero_less_mult_iff 1); by (Asm_full_simp_tac 1); (*last one*) by (REPEAT(dres_inst_tac [("x","x")] spec 1)); @@ -1881,11 +1879,11 @@ by (dtac spec 1 THEN Auto_tac); by (res_inst_tac [("x","s")] exI 1 THEN Auto_tac); by (subgoal_tac "0 < l*h" 1); -by (asm_full_simp_tac (simpset() addsimps [real_0_less_mult_iff]) 2); +by (asm_full_simp_tac (simpset() addsimps [zero_less_mult_iff]) 2); by (dres_inst_tac [("x","h")] spec 1); by (asm_full_simp_tac (simpset() addsimps [real_abs_def, inverse_eq_divide, - pos_real_le_divide_eq, pos_real_less_divide_eq] + pos_le_divide_eq, pos_less_divide_eq] addsplits [split_if_asm]) 1); qed "DERIV_left_inc"; @@ -1895,18 +1893,18 @@ by (dres_inst_tac [("x","-l")] spec 1 THEN Auto_tac); by (res_inst_tac [("x","s")] exI 1 THEN Auto_tac); by (subgoal_tac "l*h < 0" 1); -by (asm_full_simp_tac (simpset() addsimps [real_mult_less_0_iff]) 2); +by (asm_full_simp_tac (simpset() addsimps [mult_less_0_iff]) 2); by (dres_inst_tac [("x","-h")] spec 1); by (asm_full_simp_tac (simpset() addsimps [real_abs_def, inverse_eq_divide, - pos_real_less_divide_eq, + pos_less_divide_eq, symmetric real_diff_def] addsplits [split_if_asm] delsimprocs [fast_real_arith_simproc]) 1); by (subgoal_tac "0 < (f (x - h) - f x)/h" 1); by (arith_tac 2); by (asm_full_simp_tac - (simpset() addsimps [pos_real_less_divide_eq]) 1); + (simpset() addsimps [pos_less_divide_eq]) 1); qed "DERIV_left_dec"; diff -r eb8b8241ef5b -r 8dbbb7cf3637 src/HOL/Hyperreal/NSA.ML --- a/src/HOL/Hyperreal/NSA.ML Thu Dec 25 23:18:04 2003 +0100 +++ b/src/HOL/Hyperreal/NSA.ML Sat Dec 27 21:02:14 2003 +0100 @@ -270,7 +270,7 @@ by (case_tac "x <= 0" 1); by (dres_inst_tac [("y","x")] order_trans 1); by (dtac hypreal_le_anti_sym 2); -by (auto_tac (claset() addSDs [not_hypreal_leE], simpset())); +by (auto_tac (claset(), simpset() addsimps [linorder_not_le])); by (auto_tac (claset() addSIs [bexI] addIs [order_le_less_trans], simpset() addsimps [hrabs_eqI1,hrabs_eqI2,hrabs_minus_eqI1,HFinite_def])); qed "HFinite_bounded"; @@ -351,7 +351,7 @@ (hypreal_inverse_gt_0 RS order_less_trans) 1); by (assume_tac 1); by (dtac ((inverse_inverse_eq RS sym) RS subst) 1); -by (rtac (hypreal_inverse_less_iff RS iffD1) 1); +by (rtac (inverse_less_iff_less RS iffD1) 1); by (auto_tac (claset(), simpset() addsimps [SReal_inverse])); qed "HInfinite_inverse_Infinitesimal"; @@ -364,7 +364,7 @@ by (case_tac "y=0" 1); by (cut_inst_tac [("x","1"),("y","abs x"), ("u","r"),("v","abs y")] hypreal_mult_less_mono 2); -by (auto_tac (claset(), simpset() addsimps hypreal_mult_ac)); +by (auto_tac (claset(), simpset() addsimps mult_ac)); qed "HInfinite_mult"; Goalw [HInfinite_def] @@ -392,7 +392,7 @@ 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])); + simpset())); qed "HInfinite_add_le_zero"; Goal "[|x: HInfinite; y < 0; x < 0|] ==> (x + y): HInfinite"; @@ -456,7 +456,7 @@ by (asm_full_simp_tac (simpset() addsimps [linorder_not_less]) 1); by (eres_inst_tac [("x","r*ra")] ballE 1); by (fast_tac (claset() addIs [SReal_mult]) 2); -by (auto_tac (claset(), simpset() addsimps [hypreal_0_less_mult_iff])); +by (auto_tac (claset(), simpset() addsimps [zero_less_mult_iff])); by (cut_inst_tac [("x","ra"),("y","abs y"), ("u","r"),("v","abs x")] hypreal_mult_le_mono 1); by Auto_tac; @@ -598,9 +598,9 @@ val prem1::prem2::rest = goalw thy [approx_def] "[| a @= b; c @= d |] ==> a+c @= b+d"; -by (stac hypreal_minus_add_distrib 1); +by (stac minus_add_distrib 1); by (stac hypreal_add_assoc 1); -by (res_inst_tac [("y1","c")] (hypreal_add_left_commute RS subst) 1); +by (res_inst_tac [("b1","c")] (add_left_commute RS subst) 1); by (rtac (hypreal_add_assoc RS subst) 1); by (rtac ([prem1,prem2] MRS Infinitesimal_add) 1); qed "approx_add"; @@ -627,8 +627,8 @@ Goalw [approx_def] "[| a @= b; c: HFinite|] ==> a*c @= b*c"; by (asm_full_simp_tac (simpset() addsimps [Infinitesimal_HFinite_mult, - hypreal_minus_mult_eq1,hypreal_add_mult_distrib RS sym] - delsimps [hypreal_minus_mult_eq1 RS sym]) 1); + minus_mult_left,left_distrib RS sym] + delsimps [minus_mult_left RS sym]) 1); qed "approx_mult1"; Goal "[|a @= b; c: HFinite|] ==> c*a @= c*b"; @@ -668,14 +668,14 @@ Goal "[| y: Infinitesimal; x + y = z |] ==> x @= z"; by (rtac (bex_Infinitesimal_iff RS iffD1) 1); by (dtac (Infinitesimal_minus_iff RS iffD2) 1); -by (auto_tac (claset(), simpset() addsimps [hypreal_minus_add_distrib, +by (auto_tac (claset(), simpset() addsimps [minus_add_distrib, hypreal_add_assoc RS sym])); qed "Infinitesimal_add_approx"; Goal "y: Infinitesimal ==> x @= x + y"; by (rtac (bex_Infinitesimal_iff RS iffD1) 1); by (dtac (Infinitesimal_minus_iff RS iffD2) 1); -by (auto_tac (claset(), simpset() addsimps [hypreal_minus_add_distrib, +by (auto_tac (claset(), simpset() addsimps [minus_add_distrib, hypreal_add_assoc RS sym])); qed "Infinitesimal_add_approx_self"; @@ -705,8 +705,8 @@ Goal "d + b @= d + c ==> b @= c"; by (dtac (approx_minus_iff RS iffD1) 1); by (asm_full_simp_tac (simpset() addsimps - [hypreal_minus_add_distrib,approx_minus_iff RS sym] - @ hypreal_add_ac) 1); + [minus_add_distrib,approx_minus_iff RS sym] + @ add_ac) 1); qed "approx_add_left_cancel"; Goal "b + d @= c + d ==> b @= c"; @@ -718,8 +718,8 @@ Goal "b @= c ==> d + b @= d + c"; by (rtac (approx_minus_iff RS iffD2) 1); by (asm_full_simp_tac (simpset() addsimps - [hypreal_minus_add_distrib,approx_minus_iff RS sym] - @ hypreal_add_ac) 1); + [minus_add_distrib,approx_minus_iff RS sym] + @ add_ac) 1); qed "approx_add_mono1"; Goal "b @= c ==> b + a @= c + a"; @@ -1054,7 +1054,7 @@ \ r: Reals; 0 < r |] \ \ ==> t + -r <= x"; by (ftac isLubD1a 1); -by (rtac ccontr 1 THEN dtac not_hypreal_leE 1); +by (rtac ccontr 1 THEN dtac (linorder_not_le RS iffD1) 1); by (dtac SReal_minus 1 THEN dres_inst_tac [("x","t")] SReal_add 1 THEN assume_tac 1); by (dtac lemma_st_part_gt_ub 1 THEN REPEAT(assume_tac 1)); @@ -1117,7 +1117,7 @@ \ isLub Reals {s. s: Reals & s < x} t; \ \ r: Reals; 0 < r |] \ \ ==> -(x + -t) ~= r"; -by (auto_tac (claset(), simpset() addsimps [hypreal_minus_add_distrib])); +by (auto_tac (claset(), simpset() addsimps [minus_add_distrib])); by (ftac isLubD1a 1); by (dtac SReal_add_cancel 1 THEN assume_tac 1); by (dres_inst_tac [("x","-x")] SReal_minus 1); @@ -1400,8 +1400,8 @@ by (rtac ccontr 1); by (auto_tac (claset() addIs [Infinitesimal_zero RSN (2, Infinitesimal_interval)] - addSDs [hypreal_leI, order_le_imp_less_or_eq], - simpset())); + addSDs [order_le_imp_less_or_eq], + simpset() addsimps [linorder_not_less])); qed "less_Infinitesimal_less"; Goal "[| 0 < x; x ~: Infinitesimal; u: monad x |] ==> 0 < u"; @@ -1545,7 +1545,7 @@ qed "hypreal_of_real_le_add_Infininitesimal_cancel2"; Goal "[| hypreal_of_real x < e; e: Infinitesimal |] ==> hypreal_of_real x <= 0"; -by (rtac hypreal_leI 1 THEN Step_tac 1); +by (rtac (linorder_not_less RS iffD1) 1 THEN Safe_tac); by (dtac Infinitesimal_interval 1); by (dtac (SReal_hypreal_of_real RS SReal_Infinitesimal_zero) 4); by Auto_tac; @@ -1610,25 +1610,25 @@ Goal "y*y + x*x + z*z : Infinitesimal ==> x*x : Infinitesimal"; by (rtac Infinitesimal_sum_square_cancel 1); -by (asm_full_simp_tac (simpset() addsimps hypreal_add_ac) 1); +by (asm_full_simp_tac (simpset() addsimps add_ac) 1); qed "Infinitesimal_sum_square_cancel2"; Addsimps [Infinitesimal_sum_square_cancel2]; Goal "y*y + x*x + z*z : HFinite ==> x*x : HFinite"; by (rtac HFinite_sum_square_cancel 1); -by (asm_full_simp_tac (simpset() addsimps hypreal_add_ac) 1); +by (asm_full_simp_tac (simpset() addsimps add_ac) 1); qed "HFinite_sum_square_cancel2"; Addsimps [HFinite_sum_square_cancel2]; Goal "z*z + y*y + x*x : Infinitesimal ==> x*x : Infinitesimal"; by (rtac Infinitesimal_sum_square_cancel 1); -by (asm_full_simp_tac (simpset() addsimps hypreal_add_ac) 1); +by (asm_full_simp_tac (simpset() addsimps add_ac) 1); qed "Infinitesimal_sum_square_cancel3"; Addsimps [Infinitesimal_sum_square_cancel3]; Goal "z*z + y*y + x*x : HFinite ==> x*x : HFinite"; by (rtac HFinite_sum_square_cancel 1); -by (asm_full_simp_tac (simpset() addsimps hypreal_add_ac) 1); +by (asm_full_simp_tac (simpset() addsimps add_ac) 1); qed "HFinite_sum_square_cancel3"; Addsimps [HFinite_sum_square_cancel3]; @@ -1729,7 +1729,7 @@ by (subgoal_tac "st (x + y) = st ((st x + e) + (st y + ea))" 1); by (dtac sym 2 THEN dtac sym 2); by (Asm_full_simp_tac 2); -by (asm_simp_tac (simpset() addsimps hypreal_add_ac) 1); +by (asm_simp_tac (simpset() addsimps add_ac) 1); by (REPEAT(dtac st_SReal 1)); by (dtac SReal_add 1 THEN assume_tac 1); by (dtac Infinitesimal_add 1 THEN assume_tac 1); @@ -1770,7 +1770,7 @@ by (forw_inst_tac [("x","ea"),("y","x")] Infinitesimal_HFinite_mult 2); by (dtac Infinitesimal_mult 3); by (auto_tac (claset() addIs [Infinitesimal_add], - simpset() addsimps hypreal_add_ac @ hypreal_mult_ac)); + simpset() addsimps add_ac @ mult_ac)); qed "lemma_st_mult"; Goal "[| x: HFinite; y: HFinite |] \ @@ -1783,8 +1783,7 @@ by (Asm_full_simp_tac 2); by (thin_tac "x = st x + e" 1); by (thin_tac "y = st y + ea" 1); -by (asm_full_simp_tac (simpset() addsimps - [hypreal_add_mult_distrib,hypreal_add_mult_distrib2]) 1); +by (asm_full_simp_tac (simpset() addsimps [left_distrib,right_distrib]) 1); by (REPEAT(dtac st_SReal 1)); by (full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1); by (rtac st_Infinitesimal_add_SReal 1); @@ -1874,8 +1873,8 @@ Goal "x: HFinite ==> abs(st x) = st(abs x)"; by (case_tac "0 <= x" 1); -by (auto_tac (claset() addSDs [not_hypreal_leE, order_less_imp_le], - simpset() addsimps [st_zero_le,hrabs_eqI1, hrabs_minus_eqI1, +by (auto_tac (claset() addSDs [order_less_imp_le], + simpset() addsimps [linorder_not_le,st_zero_le,hrabs_eqI1, hrabs_minus_eqI1, st_zero_ge,st_minus])); qed "st_hrabs"; @@ -2214,9 +2213,9 @@ Goal "0 < u ==> \ \ (u < inverse (real(Suc n))) = (real(Suc n) < inverse u)"; by (asm_full_simp_tac (simpset() addsimps [inverse_eq_divide]) 1); -by (stac pos_real_less_divide_eq 1); +by (stac pos_less_divide_eq 1); by (assume_tac 1); -by (stac pos_real_less_divide_eq 1); +by (stac pos_less_divide_eq 1); by (simp_tac (simpset() addsimps [real_mult_commute]) 2); by (simp_tac (simpset() addsimps [real_of_nat_Suc_gt_zero]) 1); qed "real_of_nat_less_inverse_iff"; @@ -2237,7 +2236,7 @@ Goal "(inverse (real(Suc n)) <= r) = (1 <= r * real(Suc n))"; by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); by (simp_tac (simpset() addsimps [inverse_eq_divide]) 1); -by (stac pos_real_less_divide_eq 1); +by (stac pos_less_divide_eq 1); by (simp_tac (simpset() addsimps [real_of_nat_Suc_gt_zero]) 1); by (simp_tac (simpset() addsimps [real_mult_commute]) 1); qed "real_of_nat_inverse_le_iff"; diff -r eb8b8241ef5b -r 8dbbb7cf3637 src/HOL/Hyperreal/SEQ.ML --- a/src/HOL/Hyperreal/SEQ.ML Thu Dec 25 23:18:04 2003 +0100 +++ b/src/HOL/Hyperreal/SEQ.ML Sat Dec 27 21:02:14 2003 +0100 @@ -1271,7 +1271,7 @@ by (auto_tac (claset(), simpset() addsimps [real_divide_def, realpow_inverse])); by (asm_simp_tac (simpset() addsimps [inverse_eq_divide, - pos_real_divide_less_eq]) 1); + pos_divide_less_eq]) 1); qed "LIMSEQ_divide_realpow_zero"; (*---------------------------------------------------------------- diff -r eb8b8241ef5b -r 8dbbb7cf3637 src/HOL/Hyperreal/Series.ML --- a/src/HOL/Hyperreal/Series.ML Thu Dec 25 23:18:04 2003 +0100 +++ b/src/HOL/Hyperreal/Series.ML Sat Dec 27 21:02:14 2003 +0100 @@ -85,8 +85,8 @@ Addsimps [sumr_const]; Goal "sumr 0 n f + -(real n * r) = sumr 0 n (%i. f i + -r)"; -by (full_simp_tac (simpset() addsimps [sumr_add RS sym, - real_minus_mult_eq2] delsimps [real_mult_minus_eq2]) 1); +by (full_simp_tac (HOL_ss addsimps [sumr_add RS sym, real_minus_mult_eq2]) 1); +by (Simp_tac 1); qed "sumr_add_mult_const"; Goalw [real_diff_def] diff -r eb8b8241ef5b -r 8dbbb7cf3637 src/HOL/Hyperreal/Transcendental.ML --- a/src/HOL/Hyperreal/Transcendental.ML Thu Dec 25 23:18:04 2003 +0100 +++ b/src/HOL/Hyperreal/Transcendental.ML Sat Dec 27 21:02:14 2003 +0100 @@ -3062,7 +3062,7 @@ qed "STAR_exp_ln"; Goal "[|e : Infinitesimal; 0 < x |] ==> 0 < hypreal_of_real x + e"; -by (res_inst_tac [("z1","-e")] (hypreal_add_right_cancel_less RS iffD1) 1); +by (res_inst_tac [("c1","-e")] (add_less_cancel_right RS iffD1) 1); by (auto_tac (claset() addIs [Infinitesimal_less_SReal],simpset())); qed "hypreal_add_Infinitesimal_gt_zero"; diff -r eb8b8241ef5b -r 8dbbb7cf3637 src/HOL/Hyperreal/hypreal_arith.ML --- a/src/HOL/Hyperreal/hypreal_arith.ML Thu Dec 25 23:18:04 2003 +0100 +++ b/src/HOL/Hyperreal/hypreal_arith.ML Sat Dec 27 21:02:14 2003 +0100 @@ -23,7 +23,7 @@ val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps hypreal_minus_from_mult_simps @ mult_1s)) THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hypreal_mult_minus_simps)) - THEN ALLGOALS (simp_tac (HOL_ss addsimps hypreal_mult_ac)) + THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac)) val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps rel_hypreal_number_of@bin_simps)) val simplify_meta_eq = simplify_meta_eq @@ -143,7 +143,7 @@ val dest_coeff = dest_coeff val find_first = find_first [] val trans_tac = Real_Numeral_Simprocs.trans_tac - val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@hypreal_mult_ac)) + val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac)) end; structure EqCancelFactor = ExtractCommonTermFun @@ -203,7 +203,8 @@ local (* reduce contradictory <= to False *) -val simps = [True_implies_equals,inst "w" "number_of ?v" hypreal_add_mult_distrib2, +val simps = [True_implies_equals, + inst "a" "(number_of ?v)::hypreal" right_distrib, divide_1,times_divide_eq_right,times_divide_eq_left]; val simprocs = [hypreal_cancel_numeral_factors_divide]; diff -r eb8b8241ef5b -r 8dbbb7cf3637 src/HOL/Hyperreal/hypreal_arith0.ML --- a/src/HOL/Hyperreal/hypreal_arith0.ML Thu Dec 25 23:18:04 2003 +0100 +++ b/src/HOL/Hyperreal/hypreal_arith0.ML Sat Dec 27 21:02:14 2003 +0100 @@ -14,12 +14,12 @@ add_hypreal_number_of, minus_hypreal_number_of, diff_hypreal_number_of, mult_hypreal_number_of, eq_hypreal_number_of, less_hypreal_number_of, le_hypreal_number_of_eq_not_less, hypreal_diff_def, - hypreal_minus_add_distrib, hypreal_minus_minus, hypreal_mult_assoc, - hypreal_minus_zero, + minus_add_distrib, minus_minus, hypreal_mult_assoc, + minus_zero, hypreal_add_zero_left, hypreal_add_zero_right, hypreal_add_minus, hypreal_add_minus_left, - hypreal_mult_0, hypreal_mult_0_right, - hypreal_mult_1, hypreal_mult_1_right, + mult_left_zero, mult_right_zero, + mult_1, mult_1_right, hypreal_mult_minus_1, hypreal_mult_minus_1_right]; val simprocs = [Hyperreal_Times_Assoc.conv, @@ -28,7 +28,7 @@ Hyperreal_Numeral_Simprocs.eval_numerals; val mono_ss = simpset() addsimps - [hypreal_add_le_mono,hypreal_add_less_mono, + [add_mono, add_strict_mono, hypreal_add_less_le_mono,hypreal_add_le_less_mono]; val add_mono_thms_hypreal = diff -r eb8b8241ef5b -r 8dbbb7cf3637 src/HOL/Integ/int_arith1.ML --- a/src/HOL/Integ/int_arith1.ML Thu Dec 25 23:18:04 2003 +0100 +++ b/src/HOL/Integ/int_arith1.ML Sat Dec 27 21:02:14 2003 +0100 @@ -7,41 +7,6 @@ (** Misc ML bindings **) -val left_inverse = thm "left_inverse"; -val right_inverse = thm "right_inverse"; -val inverse_less_iff_less = thm"Ring_and_Field.inverse_less_iff_less"; -val inverse_eq_divide = thm"Ring_and_Field.inverse_eq_divide"; -val inverse_minus_eq = thm "inverse_minus_eq"; -val inverse_mult_distrib = thm "inverse_mult_distrib"; -val inverse_add = thm "inverse_add"; -val inverse_inverse_eq = thm "inverse_inverse_eq"; - -val add_right_mono = thm"Ring_and_Field.add_right_mono"; -val times_divide_eq_left = thm "times_divide_eq_left"; -val times_divide_eq_right = thm "times_divide_eq_right"; -val minus_minus = thm "minus_minus"; -val minus_mult_left = thm "minus_mult_left"; -val minus_mult_right = thm "minus_mult_right"; - -val pos_real_less_divide_eq = thm"pos_less_divide_eq"; -val pos_real_divide_less_eq = thm"pos_divide_less_eq"; -val pos_real_le_divide_eq = thm"pos_le_divide_eq"; -val pos_real_divide_le_eq = thm"pos_divide_le_eq"; - -val mult_less_cancel_left = thm"Ring_and_Field.mult_less_cancel_left"; -val mult_le_cancel_left = thm"Ring_and_Field.mult_le_cancel_left"; -val mult_less_cancel_right = thm"Ring_and_Field.mult_less_cancel_right"; -val mult_le_cancel_right = thm"Ring_and_Field.mult_le_cancel_right"; -val mult_cancel_left = thm"Ring_and_Field.mult_cancel_left"; -val mult_cancel_right = thm"Ring_and_Field.mult_cancel_right"; - -val field_mult_cancel_left = thm "field_mult_cancel_left"; -val field_mult_cancel_right = thm "field_mult_cancel_right"; - -val mult_divide_cancel_left = thm"Ring_and_Field.mult_divide_cancel_left"; -val mult_divide_cancel_right = thm "Ring_and_Field.mult_divide_cancel_right"; -val mult_divide_cancel_eq_if = thm"Ring_and_Field.mult_divide_cancel_eq_if"; - val NCons_Pls = thm"NCons_Pls"; val NCons_Min = thm"NCons_Min"; val NCons_BIT = thm"NCons_BIT"; diff -r eb8b8241ef5b -r 8dbbb7cf3637 src/HOL/Nat.ML --- a/src/HOL/Nat.ML Thu Dec 25 23:18:04 2003 +0100 +++ b/src/HOL/Nat.ML Sat Dec 27 21:02:14 2003 +0100 @@ -75,16 +75,16 @@ val add_leE = thm "add_leE"; val add_le_mono = thm "add_le_mono"; val add_le_mono1 = thm "add_le_mono1"; -val add_left_cancel = thm "add_left_cancel"; -val add_left_cancel_le = thm "add_left_cancel_le"; -val add_left_cancel_less = thm "add_left_cancel_less"; +val nat_add_left_cancel = thm "nat_add_left_cancel"; +val nat_add_left_cancel_le = thm "nat_add_left_cancel_le"; +val nat_add_left_cancel_less = thm "nat_add_left_cancel_less"; val add_left_commute = thm "add_left_commute"; val add_lessD1 = thm "add_lessD1"; val add_less_mono = thm "add_less_mono"; val add_less_mono1 = thm "add_less_mono1"; val add_mult_distrib = thm "add_mult_distrib"; val add_mult_distrib2 = thm "add_mult_distrib2"; -val add_right_cancel = thm "add_right_cancel"; +val nat_add_right_cancel = thm "nat_add_right_cancel"; val def_nat_rec_0 = thm "def_nat_rec_0"; val def_nat_rec_Suc = thm "def_nat_rec_Suc"; val diff_0 = thm "diff_0"; diff -r eb8b8241ef5b -r 8dbbb7cf3637 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Thu Dec 25 23:18:04 2003 +0100 +++ b/src/HOL/Nat.thy Sat Dec 27 21:02:14 2003 +0100 @@ -659,16 +659,16 @@ apply (rule nat_add_commute) done -lemma add_left_cancel [simp]: "(k + m = k + n) = (m = (n::nat))" +lemma nat_add_left_cancel [simp]: "(k + m = k + n) = (m = (n::nat))" by (induct k) simp_all -lemma add_right_cancel [simp]: "(m + k = n + k) = (m=(n::nat))" +lemma nat_add_right_cancel [simp]: "(m + k = n + k) = (m=(n::nat))" by (induct k) simp_all -lemma add_left_cancel_le [simp]: "(k + m \ k + n) = (m\(n::nat))" +lemma nat_add_left_cancel_le [simp]: "(k + m \ k + n) = (m\(n::nat))" by (induct k) simp_all -lemma add_left_cancel_less [simp]: "(k + m < k + n) = (m<(n::nat))" +lemma nat_add_left_cancel_less [simp]: "(k + m < k + n) = (m<(n::nat))" by (induct k) simp_all text {* Reasoning about @{text "m + 0 = 0"}, etc. *} diff -r eb8b8241ef5b -r 8dbbb7cf3637 src/HOL/Ring_and_Field.thy --- a/src/HOL/Ring_and_Field.thy Thu Dec 25 23:18:04 2003 +0100 +++ b/src/HOL/Ring_and_Field.thy Sat Dec 27 21:02:14 2003 +0100 @@ -1503,5 +1503,240 @@ thus ?thesis by (simp add: ac cpos mult_strict_mono) qed +ML +{* +val add_0_right = thm"add_0_right"; +val add_left_commute = thm"add_left_commute"; +val right_minus = thm"right_minus"; +val right_minus_eq = thm"right_minus_eq"; +val add_left_cancel = thm"add_left_cancel"; +val add_right_cancel = thm"add_right_cancel"; +val minus_minus = thm"minus_minus"; +val equals_zero_I = thm"equals_zero_I"; +val minus_zero = thm"minus_zero"; +val diff_self = thm"diff_self"; +val diff_0 = thm"diff_0"; +val diff_0_right = thm"diff_0_right"; +val diff_minus_eq_add = thm"diff_minus_eq_add"; +val neg_equal_iff_equal = thm"neg_equal_iff_equal"; +val neg_equal_0_iff_equal = thm"neg_equal_0_iff_equal"; +val neg_0_equal_iff_equal = thm"neg_0_equal_iff_equal"; +val equation_minus_iff = thm"equation_minus_iff"; +val minus_equation_iff = thm"minus_equation_iff"; +val mult_1_right = thm"mult_1_right"; +val mult_left_commute = thm"mult_left_commute"; +val mult_left_zero = thm"mult_left_zero"; +val mult_right_zero = thm"mult_right_zero"; +val right_distrib = thm"right_distrib"; +val combine_common_factor = thm"combine_common_factor"; +val minus_add_distrib = thm"minus_add_distrib"; +val minus_mult_left = thm"minus_mult_left"; +val minus_mult_right = thm"minus_mult_right"; +val minus_mult_minus = thm"minus_mult_minus"; +val right_diff_distrib = thm"right_diff_distrib"; +val left_diff_distrib = thm"left_diff_distrib"; +val minus_diff_eq = thm"minus_diff_eq"; +val add_right_mono = thm"add_right_mono"; +val add_mono = thm"add_mono"; +val add_strict_left_mono = thm"add_strict_left_mono"; +val add_strict_right_mono = thm"add_strict_right_mono"; +val add_strict_mono = thm"add_strict_mono"; +val add_less_imp_less_left = thm"add_less_imp_less_left"; +val add_less_imp_less_right = thm"add_less_imp_less_right"; +val add_less_cancel_left = thm"add_less_cancel_left"; +val add_less_cancel_right = thm"add_less_cancel_right"; +val add_le_cancel_left = thm"add_le_cancel_left"; +val add_le_cancel_right = thm"add_le_cancel_right"; +val add_le_imp_le_left = thm"add_le_imp_le_left"; +val add_le_imp_le_right = thm"add_le_imp_le_right"; +val le_imp_neg_le = thm"le_imp_neg_le"; +val neg_le_iff_le = thm"neg_le_iff_le"; +val neg_le_0_iff_le = thm"neg_le_0_iff_le"; +val neg_0_le_iff_le = thm"neg_0_le_iff_le"; +val neg_less_iff_less = thm"neg_less_iff_less"; +val neg_less_0_iff_less = thm"neg_less_0_iff_less"; +val neg_0_less_iff_less = thm"neg_0_less_iff_less"; +val less_minus_iff = thm"less_minus_iff"; +val minus_less_iff = thm"minus_less_iff"; +val le_minus_iff = thm"le_minus_iff"; +val minus_le_iff = thm"minus_le_iff"; +val add_diff_eq = thm"add_diff_eq"; +val diff_add_eq = thm"diff_add_eq"; +val diff_eq_eq = thm"diff_eq_eq"; +val eq_diff_eq = thm"eq_diff_eq"; +val diff_diff_eq = thm"diff_diff_eq"; +val diff_diff_eq2 = thm"diff_diff_eq2"; +val less_iff_diff_less_0 = thm"less_iff_diff_less_0"; +val diff_less_eq = thm"diff_less_eq"; +val less_diff_eq = thm"less_diff_eq"; +val diff_le_eq = thm"diff_le_eq"; +val le_diff_eq = thm"le_diff_eq"; +val eq_iff_diff_eq_0 = thm"eq_iff_diff_eq_0"; +val le_iff_diff_le_0 = thm"le_iff_diff_le_0"; +val eq_add_iff1 = thm"eq_add_iff1"; +val eq_add_iff2 = thm"eq_add_iff2"; +val less_add_iff1 = thm"less_add_iff1"; +val less_add_iff2 = thm"less_add_iff2"; +val le_add_iff1 = thm"le_add_iff1"; +val le_add_iff2 = thm"le_add_iff2"; +val mult_strict_right_mono = thm"mult_strict_right_mono"; +val mult_left_mono = thm"mult_left_mono"; +val mult_right_mono = thm"mult_right_mono"; +val mult_strict_left_mono_neg = thm"mult_strict_left_mono_neg"; +val mult_strict_right_mono_neg = thm"mult_strict_right_mono_neg"; +val mult_pos = thm"mult_pos"; +val mult_pos_neg = thm"mult_pos_neg"; +val mult_neg = thm"mult_neg"; +val zero_less_mult_pos = thm"zero_less_mult_pos"; +val zero_less_mult_iff = thm"zero_less_mult_iff"; +val mult_eq_0_iff = thm"mult_eq_0_iff"; +val zero_le_mult_iff = thm"zero_le_mult_iff"; +val mult_less_0_iff = thm"mult_less_0_iff"; +val mult_le_0_iff = thm"mult_le_0_iff"; +val zero_le_square = thm"zero_le_square"; +val zero_less_one = thm"zero_less_one"; +val zero_le_one = thm"zero_le_one"; +val mult_left_mono_neg = thm"mult_left_mono_neg"; +val mult_right_mono_neg = thm"mult_right_mono_neg"; +val mult_strict_mono = thm"mult_strict_mono"; +val mult_strict_mono' = thm"mult_strict_mono'"; +val mult_mono = thm"mult_mono"; +val mult_less_cancel_right = thm"mult_less_cancel_right"; +val mult_less_cancel_left = thm"mult_less_cancel_left"; +val mult_le_cancel_right = thm"mult_le_cancel_right"; +val mult_le_cancel_left = thm"mult_le_cancel_left"; +val mult_less_imp_less_left = thm"mult_less_imp_less_left"; +val mult_less_imp_less_right = thm"mult_less_imp_less_right"; +val mult_cancel_right = thm"mult_cancel_right"; +val mult_cancel_left = thm"mult_cancel_left"; +val left_inverse = thm "left_inverse"; +val right_inverse = thm"right_inverse"; +val right_inverse_eq = thm"right_inverse_eq"; +val nonzero_inverse_eq_divide = thm"nonzero_inverse_eq_divide"; +val divide_self = thm"divide_self"; +val divide_inverse_zero = thm"divide_inverse_zero"; +val divide_zero_left = thm"divide_zero_left"; +val inverse_eq_divide = thm"inverse_eq_divide"; +val nonzero_add_divide_distrib = thm"nonzero_add_divide_distrib"; +val add_divide_distrib = thm"add_divide_distrib"; +val field_mult_eq_0_iff = thm"field_mult_eq_0_iff"; +val field_mult_cancel_right = thm"field_mult_cancel_right"; +val field_mult_cancel_left = thm"field_mult_cancel_left"; +val nonzero_imp_inverse_nonzero = thm"nonzero_imp_inverse_nonzero"; +val inverse_zero_imp_zero = thm"inverse_zero_imp_zero"; +val inverse_nonzero_imp_nonzero = thm"inverse_nonzero_imp_nonzero"; +val inverse_nonzero_iff_nonzero = thm"inverse_nonzero_iff_nonzero"; +val nonzero_inverse_minus_eq = thm"nonzero_inverse_minus_eq"; +val inverse_minus_eq = thm"inverse_minus_eq"; +val nonzero_inverse_eq_imp_eq = thm"nonzero_inverse_eq_imp_eq"; +val inverse_eq_imp_eq = thm"inverse_eq_imp_eq"; +val inverse_eq_iff_eq = thm"inverse_eq_iff_eq"; +val nonzero_inverse_inverse_eq = thm"nonzero_inverse_inverse_eq"; +val inverse_inverse_eq = thm"inverse_inverse_eq"; +val inverse_1 = thm"inverse_1"; +val nonzero_inverse_mult_distrib = thm"nonzero_inverse_mult_distrib"; +val inverse_mult_distrib = thm"inverse_mult_distrib"; +val inverse_add = thm"inverse_add"; +val nonzero_mult_divide_cancel_left = thm"nonzero_mult_divide_cancel_left"; +val mult_divide_cancel_left = thm"mult_divide_cancel_left"; +val nonzero_mult_divide_cancel_right = thm"nonzero_mult_divide_cancel_right"; +val mult_divide_cancel_right = thm"mult_divide_cancel_right"; +val mult_divide_cancel_eq_if = thm"mult_divide_cancel_eq_if"; +val divide_1 = thm"divide_1"; +val times_divide_eq_right = thm"times_divide_eq_right"; +val times_divide_eq_left = thm"times_divide_eq_left"; +val divide_divide_eq_right = thm"divide_divide_eq_right"; +val divide_divide_eq_left = thm"divide_divide_eq_left"; +val nonzero_minus_divide_left = thm"nonzero_minus_divide_left"; +val nonzero_minus_divide_right = thm"nonzero_minus_divide_right"; +val nonzero_minus_divide_divide = thm"nonzero_minus_divide_divide"; +val minus_divide_left = thm"minus_divide_left"; +val minus_divide_right = thm"minus_divide_right"; +val minus_divide_divide = thm"minus_divide_divide"; +val positive_imp_inverse_positive = thm"positive_imp_inverse_positive"; +val negative_imp_inverse_negative = thm"negative_imp_inverse_negative"; +val inverse_le_imp_le = thm"inverse_le_imp_le"; +val inverse_positive_imp_positive = thm"inverse_positive_imp_positive"; +val inverse_positive_iff_positive = thm"inverse_positive_iff_positive"; +val inverse_negative_imp_negative = thm"inverse_negative_imp_negative"; +val inverse_negative_iff_negative = thm"inverse_negative_iff_negative"; +val inverse_nonnegative_iff_nonnegative = thm"inverse_nonnegative_iff_nonnegative"; +val inverse_nonpositive_iff_nonpositive = thm"inverse_nonpositive_iff_nonpositive"; +val less_imp_inverse_less = thm"less_imp_inverse_less"; +val inverse_less_imp_less = thm"inverse_less_imp_less"; +val inverse_less_iff_less = thm"inverse_less_iff_less"; +val le_imp_inverse_le = thm"le_imp_inverse_le"; +val inverse_le_iff_le = thm"inverse_le_iff_le"; +val inverse_le_imp_le_neg = thm"inverse_le_imp_le_neg"; +val less_imp_inverse_less_neg = thm"less_imp_inverse_less_neg"; +val inverse_less_imp_less_neg = thm"inverse_less_imp_less_neg"; +val inverse_less_iff_less_neg = thm"inverse_less_iff_less_neg"; +val le_imp_inverse_le_neg = thm"le_imp_inverse_le_neg"; +val inverse_le_iff_le_neg = thm"inverse_le_iff_le_neg"; +val zero_less_divide_iff = thm"zero_less_divide_iff"; +val divide_less_0_iff = thm"divide_less_0_iff"; +val zero_le_divide_iff = thm"zero_le_divide_iff"; +val divide_le_0_iff = thm"divide_le_0_iff"; +val divide_eq_0_iff = thm"divide_eq_0_iff"; +val pos_le_divide_eq = thm"pos_le_divide_eq"; +val neg_le_divide_eq = thm"neg_le_divide_eq"; +val le_divide_eq = thm"le_divide_eq"; +val pos_divide_le_eq = thm"pos_divide_le_eq"; +val neg_divide_le_eq = thm"neg_divide_le_eq"; +val divide_le_eq = thm"divide_le_eq"; +val pos_less_divide_eq = thm"pos_less_divide_eq"; +val neg_less_divide_eq = thm"neg_less_divide_eq"; +val less_divide_eq = thm"less_divide_eq"; +val pos_divide_less_eq = thm"pos_divide_less_eq"; +val neg_divide_less_eq = thm"neg_divide_less_eq"; +val divide_less_eq = thm"divide_less_eq"; +val nonzero_eq_divide_eq = thm"nonzero_eq_divide_eq"; +val eq_divide_eq = thm"eq_divide_eq"; +val nonzero_divide_eq_eq = thm"nonzero_divide_eq_eq"; +val divide_eq_eq = thm"divide_eq_eq"; +val divide_cancel_right = thm"divide_cancel_right"; +val divide_cancel_left = thm"divide_cancel_left"; +val divide_strict_right_mono = thm"divide_strict_right_mono"; +val divide_right_mono = thm"divide_right_mono"; +val divide_strict_left_mono = thm"divide_strict_left_mono"; +val divide_left_mono = thm"divide_left_mono"; +val divide_strict_left_mono_neg = thm"divide_strict_left_mono_neg"; +val divide_strict_right_mono_neg = thm"divide_strict_right_mono_neg"; +val zero_less_two = thm"zero_less_two"; +val less_half_sum = thm"less_half_sum"; +val gt_half_sum = thm"gt_half_sum"; +val dense = thm"dense"; +val abs_zero = thm"abs_zero"; +val abs_one = thm"abs_one"; +val abs_mult = thm"abs_mult"; +val abs_eq_0 = thm"abs_eq_0"; +val zero_less_abs_iff = thm"zero_less_abs_iff"; +val abs_not_less_zero = thm"abs_not_less_zero"; +val abs_le_zero_iff = thm"abs_le_zero_iff"; +val abs_minus_cancel = thm"abs_minus_cancel"; +val abs_ge_zero = thm"abs_ge_zero"; +val abs_idempotent = thm"abs_idempotent"; +val abs_zero_iff = thm"abs_zero_iff"; +val abs_ge_self = thm"abs_ge_self"; +val abs_ge_minus_self = thm"abs_ge_minus_self"; +val nonzero_abs_inverse = thm"nonzero_abs_inverse"; +val abs_inverse = thm"abs_inverse"; +val nonzero_abs_divide = thm"nonzero_abs_divide"; +val abs_divide = thm"abs_divide"; +val abs_leI = thm"abs_leI"; +val le_minus_self_iff = thm"le_minus_self_iff"; +val minus_le_self_iff = thm"minus_le_self_iff"; +val eq_minus_self_iff = thm"eq_minus_self_iff"; +val less_minus_self_iff = thm"less_minus_self_iff"; +val abs_le_D1 = thm"abs_le_D1"; +val abs_le_D2 = thm"abs_le_D2"; +val abs_le_iff = thm"abs_le_iff"; +val abs_less_iff = thm"abs_less_iff"; +val abs_triangle_ineq = thm"abs_triangle_ineq"; +val abs_mult_less = thm"abs_mult_less"; + +val compare_rls = thms"compare_rls"; +*} + end diff -r eb8b8241ef5b -r 8dbbb7cf3637 src/HOL/arith_data.ML --- a/src/HOL/arith_data.ML Thu Dec 25 23:18:04 2003 +0100 +++ b/src/HOL/arith_data.ML Sat Dec 27 21:02:14 2003 +0100 @@ -106,7 +106,7 @@ open Sum; val mk_bal = HOLogic.mk_eq; val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT; - val uncancel_tac = gen_uncancel_tac add_left_cancel; + val uncancel_tac = gen_uncancel_tac nat_add_left_cancel; end); @@ -117,7 +117,7 @@ open Sum; val mk_bal = HOLogic.mk_binrel "op <"; val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT; - val uncancel_tac = gen_uncancel_tac add_left_cancel_less; + val uncancel_tac = gen_uncancel_tac nat_add_left_cancel_less; end); @@ -128,7 +128,7 @@ open Sum; val mk_bal = HOLogic.mk_binrel "op <="; val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT; - val uncancel_tac = gen_uncancel_tac add_left_cancel_le; + val uncancel_tac = gen_uncancel_tac nat_add_left_cancel_le; end);