--- 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);
--- 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";
--- 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]
--- 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
--- 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)";
--- 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]
--- 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 \
--- 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);
--- 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 \<noteq> (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 \<noteq> 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 \<noteq> 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 \<noteq> (1::hypreal)" by (rule hypreal_zero_not_eq_one)
+ show "x \<noteq> 0 ==> inverse x * x = 1" by (simp add: hypreal_mult_inverse_left)
+ show "y \<noteq> 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<y |] ==> z*x<z*y"
@@ -858,31 +695,23 @@
subsection{*The Hyperreals Form an Ordered Field*}
-instance hypreal :: inverse ..
-
instance hypreal :: ordered_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
- 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
- show "(x + y) * z = x * z + y * z" by (simp add: hypreal_add_mult_distrib)
- show "0 \<noteq> (1::hypreal)" by (rule hypreal_zero_not_eq_one)
show "x \<le> y ==> z + x \<le> 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 "\<bar>x\<bar> = (if x < 0 then -x else x)"
by (auto dest: order_le_less_trans simp add: hrabs_def linorder_not_le)
- show "x \<noteq> 0 ==> inverse x * x = 1" by simp
- show "y \<noteq> 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 \<noteq> a) = (x + -a \<noteq> (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
--- 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 \<le> w+z) = (v \<le> (w::hypreal))"
- by (rule Ring_and_Field.add_le_cancel_right)
-
-lemma hypreal_add_left_cancel_le: "(z+v \<le> z+w) = (v \<le> (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)\<le>j; k\<le>l |] ==> i + k \<le> j + l"
- by (rule Ring_and_Field.add_mono)
-
lemma hypreal_add_less_le_mono: "[|(i::hypreal)<j; k\<le>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) \<le> y|] ==> r < x + y"
by (auto dest: hypreal_add_less_le_mono)
-lemma hypreal_le_add_right_cancel: "!!(A::hypreal). A + C \<le> B + C ==> A \<le> B"
- by (rule Ring_and_Field.add_le_imp_le_right)
-
lemma hypreal_le_add_left_cancel: "!!(A::hypreal). C + A \<le> C + B ==> A \<le> B"
-apply (simp add: );
+apply simp
done
lemma hypreal_le_square [simp]: "(0::hypreal) \<le> 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))} = {} |
(\<exists>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 \<le> inverse r) = (r \<le> (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) \<le> x*y) = (0 \<le> x & 0 \<le> y | x \<le> 0 & y \<le> 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 \<le> (0::hypreal)) = (0 \<le> x & y \<le> 0 | x \<le> 0 & 0 \<le> y)"
- by (rule Ring_and_Field.mult_le_0_iff)
-
-
-lemma hypreal_mult_self_sum_ge_zero: "(0::hypreal) \<le> x*x + y*y"
-proof -
- have "0 + 0 \<le> 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
--- 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];
--- 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 \\<noteq> 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 \\<approx> 0; h \\<noteq> 0 |] \
@@ -1156,7 +1154,7 @@
\ ==> increment f x h \\<approx> 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) \\<noteq> 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) \\<noteq> 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";
--- 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";
--- 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";
(*----------------------------------------------------------------
--- 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]
--- 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";
--- 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];
--- 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 =
--- 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";
--- 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";
--- 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 \<le> k + n) = (m\<le>(n::nat))"
+lemma nat_add_left_cancel_le [simp]: "(k + m \<le> k + n) = (m\<le>(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. *}
--- 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
--- 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);