--- a/src/HOL/Complex/ex/Sqrt.thy Fri Dec 19 10:38:48 2003 +0100
+++ b/src/HOL/Complex/ex/Sqrt.thy Fri Dec 19 17:13:28 2003 +0100
@@ -43,7 +43,7 @@
proof -
from gcd have "real ?k / real ?l =
real (?gcd * ?k) / real (?gcd * ?l)"
- by (simp add: real_mult_div_cancel1)
+ by (simp add: mult_divide_cancel_left)
also from gcd_k and gcd_l have "\<dots> = real m / real n" by simp
also from x_rat have "\<dots> = \<bar>x\<bar>" ..
finally show ?thesis ..
--- a/src/HOL/Hyperreal/HyperArith0.ML Fri Dec 19 10:38:48 2003 +0100
+++ b/src/HOL/Hyperreal/HyperArith0.ML Fri Dec 19 17:13:28 2003 +0100
@@ -8,196 +8,6 @@
Also, common factor cancellation
*)
-Goal "x - - y = x + (y::hypreal)";
-by (Simp_tac 1);
-qed "hypreal_diff_minus_eq";
-Addsimps [hypreal_diff_minus_eq];
-
-Goal "((x * y = 0) = (x = 0 | y = (0::hypreal)))";
-by Auto_tac;
-qed "hypreal_mult_is_0";
-AddIffs [hypreal_mult_is_0];
-
-(** Division and inverse **)
-
-Goal "0/x = (0::hypreal)";
-by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1);
-qed "hypreal_0_divide";
-Addsimps [hypreal_0_divide];
-
-Goal "((0::hypreal) < inverse x) = (0 < x)";
-by (case_tac "x=0" 1);
-by (asm_simp_tac (HOL_ss addsimps [HYPREAL_INVERSE_ZERO]) 1);
-by (auto_tac (claset() addDs [hypreal_inverse_less_0],
- simpset() addsimps [linorder_neq_iff,
- hypreal_inverse_gt_0]));
-qed "hypreal_0_less_inverse_iff";
-Addsimps [hypreal_0_less_inverse_iff];
-
-Goal "(inverse x < (0::hypreal)) = (x < 0)";
-by (case_tac "x=0" 1);
-by (asm_simp_tac (HOL_ss addsimps [HYPREAL_INVERSE_ZERO]) 1);
-by (auto_tac (claset() addDs [hypreal_inverse_less_0],
- simpset() addsimps [linorder_neq_iff,
- hypreal_inverse_gt_0]));
-qed "hypreal_inverse_less_0_iff";
-Addsimps [hypreal_inverse_less_0_iff];
-
-Goal "((0::hypreal) <= inverse x) = (0 <= x)";
-by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
-qed "hypreal_0_le_inverse_iff";
-Addsimps [hypreal_0_le_inverse_iff];
-
-Goal "(inverse x <= (0::hypreal)) = (x <= 0)";
-by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
-qed "hypreal_inverse_le_0_iff";
-Addsimps [hypreal_inverse_le_0_iff];
-
-Goalw [hypreal_divide_def] "x/(0::hypreal) = 0";
-by (stac (HYPREAL_INVERSE_ZERO) 1);
-by (Simp_tac 1);
-qed "HYPREAL_DIVIDE_ZERO";
-
-Goal "inverse (x::hypreal) = 1/x";
-by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1);
-qed "hypreal_inverse_eq_divide";
-
-Goal "((0::hypreal) < x/y) = (0 < x & 0 < y | x < 0 & y < 0)";
-by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_0_less_mult_iff]) 1);
-qed "hypreal_0_less_divide_iff";
-Addsimps [inst "x" "number_of ?w" hypreal_0_less_divide_iff];
-
-Goal "(x/y < (0::hypreal)) = (0 < x & y < 0 | x < 0 & 0 < y)";
-by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_less_0_iff]) 1);
-qed "hypreal_divide_less_0_iff";
-Addsimps [inst "x" "number_of ?w" hypreal_divide_less_0_iff];
-
-Goal "((0::hypreal) <= x/y) = ((x <= 0 | 0 <= y) & (0 <= x | y <= 0))";
-by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_0_le_mult_iff]) 1);
-by Auto_tac;
-qed "hypreal_0_le_divide_iff";
-Addsimps [inst "x" "number_of ?w" hypreal_0_le_divide_iff];
-
-Goal "(x/y <= (0::hypreal)) = ((x <= 0 | y <= 0) & (0 <= x | 0 <= y))";
-by (simp_tac (simpset() addsimps [hypreal_divide_def,
- hypreal_mult_le_0_iff]) 1);
-by Auto_tac;
-qed "hypreal_divide_le_0_iff";
-Addsimps [inst "x" "number_of ?w" hypreal_divide_le_0_iff];
-
-Goal "(inverse(x::hypreal) = 0) = (x = 0)";
-by (auto_tac (claset(),
- simpset() addsimps [HYPREAL_INVERSE_ZERO]));
-by (rtac ccontr 1);
-by (blast_tac (claset() addDs [hypreal_inverse_not_zero]) 1);
-qed "hypreal_inverse_zero_iff";
-Addsimps [hypreal_inverse_zero_iff];
-
-Goal "(x/y = 0) = (x=0 | y=(0::hypreal))";
-by (auto_tac (claset(), simpset() addsimps [hypreal_divide_def]));
-qed "hypreal_divide_eq_0_iff";
-Addsimps [hypreal_divide_eq_0_iff];
-
-Goal "h ~= (0::hypreal) ==> h/h = 1";
-by (asm_simp_tac
- (simpset() addsimps [hypreal_divide_def, hypreal_mult_inverse_left]) 1);
-qed "hypreal_divide_self_eq";
-Addsimps [hypreal_divide_self_eq];
-
-
-(**** Factor cancellation theorems for "hypreal" ****)
-
-(** Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =,
- but not (yet?) for k*m < n*k. **)
-
-bind_thm ("hypreal_mult_minus_right", hypreal_minus_mult_eq2 RS sym);
-
-Goal "(-y < -x) = ((x::hypreal) < y)";
-by (arith_tac 1);
-qed "hypreal_minus_less_minus";
-Addsimps [hypreal_minus_less_minus];
-
-Goal "[| i<j; k < (0::hypreal) |] ==> j*k < i*k";
-by (rtac (hypreal_minus_less_minus RS iffD1) 1);
-by (auto_tac (claset(),
- simpset() delsimps [hypreal_minus_mult_eq2 RS sym]
- addsimps [hypreal_minus_mult_eq2,
- hypreal_mult_less_mono1]));
-qed "hypreal_mult_less_mono1_neg";
-
-Goal "[| i<j; k < (0::hypreal) |] ==> k*j < k*i";
-by (rtac (hypreal_minus_less_minus RS iffD1) 1);
-by (auto_tac (claset(),
- simpset() delsimps [hypreal_minus_mult_eq1 RS sym]
- addsimps [hypreal_minus_mult_eq1,
- hypreal_mult_less_mono2]));
-qed "hypreal_mult_less_mono2_neg";
-
-Goal "[| i <= j; k <= (0::hypreal) |] ==> j*k <= i*k";
-by (auto_tac (claset(),
- simpset() addsimps [order_le_less, hypreal_mult_less_mono1_neg]));
-qed "hypreal_mult_le_mono1_neg";
-
-Goal "[| i <= j; k <= (0::hypreal) |] ==> k*j <= k*i";
-by (dtac hypreal_mult_le_mono1_neg 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute])));
-qed "hypreal_mult_le_mono2_neg";
-
-Goal "(m*k < n*k) = (((0::hypreal) < k & m<n) | (k < 0 & n<m))";
-by (case_tac "k = (0::hypreal)" 1);
-by (auto_tac (claset(),
- simpset() addsimps [linorder_neq_iff,
- hypreal_mult_less_mono1, hypreal_mult_less_mono1_neg]));
-by (auto_tac (claset(),
- simpset() addsimps [linorder_not_less,
- inst "y1" "m*k" (linorder_not_le RS sym),
- inst "y1" "m" (linorder_not_le RS sym)]));
-by (TRYALL (etac notE));
-by (auto_tac (claset(),
- simpset() addsimps [order_less_imp_le, hypreal_mult_le_mono1,
- hypreal_mult_le_mono1_neg]));
-qed "hypreal_mult_less_cancel2";
-
-Goal "(m*k <= n*k) = (((0::hypreal) < k --> m<=n) & (k < 0 --> n<=m))";
-by (simp_tac (simpset() addsimps [linorder_not_less RS sym,
- hypreal_mult_less_cancel2]) 1);
-qed "hypreal_mult_le_cancel2";
-
-Goal "(k*m < k*n) = (((0::hypreal) < k & m<n) | (k < 0 & n<m))";
-by (simp_tac (simpset() addsimps [inst "z" "k" hypreal_mult_commute,
- hypreal_mult_less_cancel2]) 1);
-qed "hypreal_mult_less_cancel1";
-
-Goal "!!k::hypreal. (k*m <= k*n) = ((0 < k --> m<=n) & (k < 0 --> n<=m))";
-by (simp_tac (simpset() addsimps [linorder_not_less RS sym,
- hypreal_mult_less_cancel1]) 1);
-qed "hypreal_mult_le_cancel1";
-
-Goal "!!k::hypreal. (k*m = k*n) = (k = 0 | m=n)";
-by (case_tac "k=0" 1);
-by (auto_tac (claset(), simpset() addsimps [hypreal_mult_left_cancel]));
-qed "hypreal_mult_eq_cancel1";
-
-Goal "!!k::hypreal. (m*k = n*k) = (k = 0 | m=n)";
-by (case_tac "k=0" 1);
-by (auto_tac (claset(), simpset() addsimps [hypreal_mult_right_cancel]));
-qed "hypreal_mult_eq_cancel2";
-
-Goal "!!k::hypreal. k~=0 ==> (k*m) / (k*n) = (m/n)";
-by (asm_simp_tac
- (simpset() addsimps [hypreal_divide_def, hypreal_inverse_distrib]) 1);
-by (subgoal_tac "k * m * (inverse k * inverse n) = \
-\ (k * inverse k) * (m * inverse n)" 1);
-by (asm_full_simp_tac (simpset() addsimps []) 1);
-by (asm_full_simp_tac (HOL_ss addsimps hypreal_mult_ac) 1);
-qed "hypreal_mult_div_cancel1";
-
-(*For ExtractCommonTerm*)
-Goal "(k*m) / (k*n) = (if k = (0::hypreal) then 0 else m/n)";
-by (simp_tac (simpset() addsimps [hypreal_mult_div_cancel1]) 1);
-qed "hypreal_mult_div_cancel_disj";
-
-
local
open Hyperreal_Numeral_Simprocs
in
@@ -224,7 +34,7 @@
val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binop "HOL.divide"
val dest_bal = HOLogic.dest_bin "HOL.divide" hyprealT
- val cancel = hypreal_mult_div_cancel1 RS trans
+ val cancel = mult_divide_cancel_left RS trans
val neg_exchanges = false
)
@@ -233,7 +43,7 @@
val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" hyprealT
- val cancel = hypreal_mult_eq_cancel1 RS trans
+ val cancel = mult_cancel_left RS trans
val neg_exchanges = false
)
@@ -242,7 +52,7 @@
val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "op <"
val dest_bal = HOLogic.dest_bin "op <" hyprealT
- val cancel = hypreal_mult_less_cancel1 RS trans
+ val cancel = mult_less_cancel_left RS trans
val neg_exchanges = true
)
@@ -251,7 +61,7 @@
val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "op <="
val dest_bal = HOLogic.dest_bin "op <=" hyprealT
- val cancel = hypreal_mult_le_cancel1 RS trans
+ val cancel = mult_le_cancel_left RS trans
val neg_exchanges = true
)
@@ -341,7 +151,7 @@
val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" hyprealT
- val simplify_meta_eq = cancel_simplify_meta_eq hypreal_mult_eq_cancel1
+ val simplify_meta_eq = cancel_simplify_meta_eq mult_cancel_left
);
@@ -350,7 +160,7 @@
val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binop "HOL.divide"
val dest_bal = HOLogic.dest_bin "HOL.divide" hyprealT
- val simplify_meta_eq = cancel_simplify_meta_eq hypreal_mult_div_cancel_disj
+ val simplify_meta_eq = cancel_simplify_meta_eq mult_divide_cancel_eq_if
);
val hypreal_cancel_factor =
@@ -387,119 +197,9 @@
*)
-(*** Simplification of inequalities involving literal divisors ***)
-
-Goal "0<z ==> ((x::hypreal) <= y/z) = (x*z <= y)";
-by (subgoal_tac "(x*z <= y) = (x*z <= (y/z)*z)" 1);
-by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac hypreal_mult_le_cancel2 1);
-by (Asm_simp_tac 1);
-qed "pos_hypreal_le_divide_eq";
-Addsimps [inst "z" "number_of ?w" pos_hypreal_le_divide_eq];
-
-Goal "z<0 ==> ((x::hypreal) <= y/z) = (y <= x*z)";
-by (subgoal_tac "(y <= x*z) = ((y/z)*z <= x*z)" 1);
-by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac hypreal_mult_le_cancel2 1);
-by (Asm_simp_tac 1);
-qed "neg_hypreal_le_divide_eq";
-Addsimps [inst "z" "number_of ?w" neg_hypreal_le_divide_eq];
-
-Goal "0<z ==> (y/z <= (x::hypreal)) = (y <= x*z)";
-by (subgoal_tac "(y <= x*z) = ((y/z)*z <= x*z)" 1);
-by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac hypreal_mult_le_cancel2 1);
-by (Asm_simp_tac 1);
-qed "pos_hypreal_divide_le_eq";
-Addsimps [inst "z" "number_of ?w" pos_hypreal_divide_le_eq];
-
-Goal "z<0 ==> (y/z <= (x::hypreal)) = (x*z <= y)";
-by (subgoal_tac "(x*z <= y) = (x*z <= (y/z)*z)" 1);
-by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac hypreal_mult_le_cancel2 1);
-by (Asm_simp_tac 1);
-qed "neg_hypreal_divide_le_eq";
-Addsimps [inst "z" "number_of ?w" neg_hypreal_divide_le_eq];
-
-Goal "0<z ==> ((x::hypreal) < y/z) = (x*z < y)";
-by (subgoal_tac "(x*z < y) = (x*z < (y/z)*z)" 1);
-by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac hypreal_mult_less_cancel2 1);
-by (Asm_simp_tac 1);
-qed "pos_hypreal_less_divide_eq";
-Addsimps [inst "z" "number_of ?w" pos_hypreal_less_divide_eq];
-
-Goal "z<0 ==> ((x::hypreal) < y/z) = (y < x*z)";
-by (subgoal_tac "(y < x*z) = ((y/z)*z < x*z)" 1);
-by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac hypreal_mult_less_cancel2 1);
-by (Asm_simp_tac 1);
-qed "neg_hypreal_less_divide_eq";
-Addsimps [inst "z" "number_of ?w" neg_hypreal_less_divide_eq];
-
-Goal "0<z ==> (y/z < (x::hypreal)) = (y < x*z)";
-by (subgoal_tac "(y < x*z) = ((y/z)*z < x*z)" 1);
-by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac hypreal_mult_less_cancel2 1);
-by (Asm_simp_tac 1);
-qed "pos_hypreal_divide_less_eq";
-Addsimps [inst "z" "number_of ?w" pos_hypreal_divide_less_eq];
-
-Goal "z<0 ==> (y/z < (x::hypreal)) = (x*z < y)";
-by (subgoal_tac "(x*z < y) = (x*z < (y/z)*z)" 1);
-by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac hypreal_mult_less_cancel2 1);
-by (Asm_simp_tac 1);
-qed "neg_hypreal_divide_less_eq";
-Addsimps [inst "z" "number_of ?w" neg_hypreal_divide_less_eq];
-
-Goal "z~=0 ==> ((x::hypreal) = y/z) = (x*z = y)";
-by (subgoal_tac "(x*z = y) = (x*z = (y/z)*z)" 1);
-by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac hypreal_mult_eq_cancel2 1);
-by (Asm_simp_tac 1);
-qed "hypreal_eq_divide_eq";
-Addsimps [inst "z" "number_of ?w" hypreal_eq_divide_eq];
-
-Goal "z~=0 ==> (y/z = (x::hypreal)) = (y = x*z)";
-by (subgoal_tac "(y = x*z) = ((y/z)*z = x*z)" 1);
-by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac hypreal_mult_eq_cancel2 1);
-by (Asm_simp_tac 1);
-qed "hypreal_divide_eq_eq";
-Addsimps [inst "z" "number_of ?w" hypreal_divide_eq_eq];
-
-Goal "(m/k = n/k) = (k = 0 | m = (n::hypreal))";
-by (case_tac "k=0" 1);
-by (asm_simp_tac (simpset() addsimps [HYPREAL_DIVIDE_ZERO]) 1);
-by (asm_simp_tac (simpset() addsimps [hypreal_divide_eq_eq, hypreal_eq_divide_eq,
- hypreal_mult_eq_cancel2]) 1);
-qed "hypreal_divide_eq_cancel2";
-
-Goal "(k/m = k/n) = (k = 0 | m = (n::hypreal))";
-by (case_tac "m=0 | n = 0" 1);
-by (auto_tac (claset(),
- simpset() addsimps [HYPREAL_DIVIDE_ZERO, hypreal_divide_eq_eq,
- hypreal_eq_divide_eq, hypreal_mult_eq_cancel1]));
-qed "hypreal_divide_eq_cancel1";
(** Division by 1, -1 **)
-Goal "(x::hypreal)/1 = x";
-by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1);
-qed "hypreal_divide_1";
-Addsimps [hypreal_divide_1];
-
Goal "x/-1 = -(x::hypreal)";
by (Simp_tac 1);
qed "hypreal_divide_minus1";
@@ -510,11 +210,6 @@
qed "hypreal_minus1_divide";
Addsimps [hypreal_minus1_divide];
-Goal "[| (0::hypreal) < d1; 0 < d2 |] ==> EX e. 0 < e & e < d1 & e < d2";
-by (res_inst_tac [("x","(min d1 d2)/2")] exI 1);
-by (asm_simp_tac (simpset() addsimps [min_def]) 1);
-qed "hypreal_lbound_gt_zero";
-
(*** General rewrites to improve automation, like those for type "int" ***)
@@ -561,21 +256,6 @@
Addsimps [hypreal_le_minus_iff];
-(*Distributive laws for literals*)
-Addsimps (map (inst "w" "number_of ?v")
- [hypreal_add_mult_distrib, hypreal_add_mult_distrib2,
- hypreal_diff_mult_distrib, hypreal_diff_mult_distrib2]);
-
-Addsimps (map (inst "x" "number_of ?v")
- [hypreal_less_minus, hypreal_le_minus, hypreal_equation_minus]);
-Addsimps (map (inst "y" "number_of ?v")
- [hypreal_minus_less, hypreal_minus_le, hypreal_minus_equation]);
-
-Addsimps (map (simplify (simpset()) o inst "x" "1")
- [hypreal_less_minus, hypreal_le_minus, hypreal_equation_minus]);
-Addsimps (map (simplify (simpset()) o inst "y" "1")
- [hypreal_minus_less, hypreal_minus_le, hypreal_minus_equation]);
-
(*** Simprules combining x+y and 0 ***)
Goal "(x+y = (0::hypreal)) = (y = -x)";
@@ -629,21 +309,3 @@
qed "hypreal_minus_diff_eq";
Addsimps [hypreal_minus_diff_eq];
-
-(*** Density of the Hyperreals ***)
-
-Goal "x < y ==> x < (x+y) / (2::hypreal)";
-by Auto_tac;
-qed "hypreal_less_half_sum";
-
-Goal "x < y ==> (x+y)/(2::hypreal) < y";
-by Auto_tac;
-qed "hypreal_gt_half_sum";
-
-Goal "x < y ==> EX r::hypreal. x < r & r < y";
-by (blast_tac (claset() addSIs [hypreal_less_half_sum, hypreal_gt_half_sum]) 1);
-qed "hypreal_dense";
-
-
-(*Replaces "inverse #nn" by 1/#nn *)
-Addsimps [inst "x" "number_of ?w" hypreal_inverse_eq_divide];
--- a/src/HOL/Hyperreal/HyperDef.thy Fri Dec 19 10:38:48 2003 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy Fri Dec 19 17:13:28 2003 +0100
@@ -990,13 +990,6 @@
by (simp add: hypreal_divide_def)
declare hypreal_zero_divide [simp] hypreal_divide_one [simp]
-lemma hypreal_times_divide1_eq [simp]: "(x::hypreal) * (y/z) = (x*y)/z"
-by (simp add: hypreal_divide_def hypreal_mult_assoc)
-
-lemma hypreal_times_divide2_eq [simp]: "(y/z) * (x::hypreal) = (y*x)/z"
-by (simp add: hypreal_divide_def hypreal_mult_ac)
-
-
lemma hypreal_divide_divide1_eq [simp]: "(x::hypreal) / (y/z) = (x*z)/y"
by (simp add: hypreal_divide_def hypreal_inverse_distrib hypreal_mult_ac)
@@ -1296,8 +1289,6 @@
val hypreal_of_real_divide = thm "hypreal_of_real_divide";
val hypreal_zero_divide = thm "hypreal_zero_divide";
val hypreal_divide_one = thm "hypreal_divide_one";
-val hypreal_times_divide1_eq = thm "hypreal_times_divide1_eq";
-val hypreal_times_divide2_eq = thm "hypreal_times_divide2_eq";
val hypreal_divide_divide1_eq = thm "hypreal_divide_divide1_eq";
val hypreal_divide_divide2_eq = thm "hypreal_divide_divide2_eq";
val hypreal_minus_divide_eq = thm "hypreal_minus_divide_eq";
--- a/src/HOL/Hyperreal/HyperOrd.thy Fri Dec 19 10:38:48 2003 +0100
+++ b/src/HOL/Hyperreal/HyperOrd.thy Fri Dec 19 17:13:28 2003 +0100
@@ -7,6 +7,14 @@
theory HyperOrd = HyperDef:
+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
+
+
defs (overloaded)
hrabs_def: "abs (r::hypreal) == (if 0 \<le> r then r else -r)"
@@ -247,17 +255,6 @@
done
declare hypreal_le_square [simp]
-lemma hypreal_less_minus_square: "- (x*x) \<le> (0::hypreal)"
-apply (unfold hypreal_le_def)
-apply (auto dest!: hypreal_le_square [THEN order_le_less_trans]
- simp add: hypreal_minus_zero_less_iff)
-done
-declare hypreal_less_minus_square [simp]
-
-lemma hypreal_mult_0_less: "(0*x<r)=((0::hypreal)<r)"
-apply (simp (no_asm))
-done
-
lemma hypreal_mult_less_mono1: "[| (0::hypreal) < z; x < y |] ==> x*z < y*z"
apply (rotate_tac 1)
apply (drule hypreal_less_minus_iff [THEN iffD1])
@@ -449,8 +446,6 @@
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_less_minus_square = thm"hypreal_less_minus_square";
-val hypreal_mult_0_less = thm"hypreal_mult_0_less";
val hypreal_mult_less_mono1 = thm"hypreal_mult_less_mono1";
val hypreal_mult_less_mono2 = thm"hypreal_mult_less_mono2";
val hypreal_mult_less_mono = thm"hypreal_mult_less_mono";
--- a/src/HOL/Hyperreal/HyperPow.ML Fri Dec 19 10:38:48 2003 +0100
+++ b/src/HOL/Hyperreal/HyperPow.ML Fri Dec 19 17:13:28 2003 +0100
@@ -19,8 +19,6 @@
Goal "r ~= (0::hypreal) --> inverse(r ^ n) = (inverse r) ^ n";
by (induct_tac "n" 1);
by Auto_tac;
-by (forw_inst_tac [("n","n")] hrealpow_not_zero 1);
-by (auto_tac (claset(), simpset() addsimps [hypreal_inverse_distrib]));
qed_spec_mp "hrealpow_inverse";
Goal "abs (r::hypreal) ^ n = abs (r ^ n)";
@@ -105,13 +103,10 @@
by (auto_tac (claset() addIs [order_antisym], simpset()));
qed "hypreal_add_nonneg_eq_0_iff";
-Goal "(x*y = 0) = (x = 0 | y = (0::hypreal))";
-by Auto_tac;
-qed "hypreal_mult_is_0";
-
Goal "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))";
by (simp_tac (HOL_ss addsimps [hypreal_le_square, hypreal_le_add_order,
- hypreal_add_nonneg_eq_0_iff, hypreal_mult_is_0]) 1);
+ hypreal_add_nonneg_eq_0_iff]) 1);
+by Auto_tac;
qed "hypreal_three_squares_add_zero_iff";
Goal "(x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + z ^ Suc (Suc 0) = (0::hypreal)) = (x = 0 & y = 0 & z = 0)";
--- a/src/HOL/Hyperreal/Integration.ML Fri Dec 19 10:38:48 2003 +0100
+++ b/src/HOL/Hyperreal/Integration.ML Fri Dec 19 17:13:28 2003 +0100
@@ -356,8 +356,9 @@
"abs((rsum(D,p) f - k2) - (rsum(D,p) f - k1)) < abs(k1 - k2)" 1);
by (arith_tac 1);
by (dtac real_add_less_mono 1 THEN assume_tac 1);
-by (auto_tac (claset(),HOL_ss addsimps [real_add_mult_distrib RS sym,
- real_mult_2_right RS sym,real_mult_less_cancel2]));
+by (auto_tac (claset(),
+ HOL_ss addsimps [real_add_mult_distrib RS sym,
+ real_mult_2_right RS sym, mult_less_cancel_right]));
by (ALLGOALS(arith_tac));
qed "Integral_unique";
--- a/src/HOL/Hyperreal/Lim.ML Fri Dec 19 10:38:48 2003 +0100
+++ b/src/HOL/Hyperreal/Lim.ML Fri Dec 19 17:13:28 2003 +0100
@@ -7,6 +7,9 @@
val times_divide_eq_right = thm"times_divide_eq_right";
+val inverse_mult_distrib = thm"inverse_mult_distrib";
+val inverse_minus_eq = thm "inverse_minus_eq";
+
fun ARITH_PROVE str = prove_goal thy str
(fn prems => [cut_facts_tac prems 1,arith_tac 1]);
@@ -1020,8 +1023,8 @@
by (simp_tac (simpset() addsimps [hypreal_add_divide_distrib]) 1);
by (REPEAT(dtac (bex_Infinitesimal_iff2 RS iffD2) 1));
by (auto_tac (claset(),
- simpset() delsimps [hypreal_times_divide1_eq]
- addsimps [hypreal_times_divide1_eq RS sym]));
+ simpset() delsimps [times_divide_eq_right]
+ addsimps [times_divide_eq_right RS sym]));
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],
@@ -1136,8 +1139,8 @@
by (thin_tac "(( *f* f) (hypreal_of_real(x) + h) + \
\ - hypreal_of_real (f x)) / h = hypreal_of_real(D) + y" 2);
by (assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_times_divide1_eq RS sym]
- delsimps [hypreal_times_divide1_eq]) 1);
+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]));
qed "increment_thm";
@@ -1324,7 +1327,8 @@
(simpset() addsimps [hypreal_inverse_add,
hypreal_inverse_distrib RS sym, hypreal_minus_inverse RS sym]
@ hypreal_add_ac @ hypreal_mult_ac
- delsimps [hypreal_minus_mult_eq1 RS sym,
+ delsimps [inverse_mult_distrib,inverse_minus_eq,
+ hypreal_minus_mult_eq1 RS sym,
hypreal_minus_mult_eq2 RS sym] ) 1);
by (asm_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym,
hypreal_add_mult_distrib2]
@@ -1818,7 +1822,7 @@
by (REPEAT(dres_inst_tac [("x","a")] spec 1));
by (Asm_full_simp_tac 1);
by (asm_full_simp_tac
- (simpset() addsimps [real_inverse_eq_divide, pos_real_divide_le_eq]) 1);
+ (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);
by (Asm_full_simp_tac 1);
(*last one*)
@@ -1880,7 +1884,7 @@
by (asm_full_simp_tac (simpset() addsimps [real_0_less_mult_iff]) 2);
by (dres_inst_tac [("x","h")] spec 1);
by (asm_full_simp_tac
- (simpset() addsimps [real_abs_def, real_inverse_eq_divide,
+ (simpset() addsimps [real_abs_def, inverse_eq_divide,
pos_real_le_divide_eq, pos_real_less_divide_eq]
addsplits [split_if_asm]) 1);
qed "DERIV_left_inc";
@@ -1894,7 +1898,7 @@
by (asm_full_simp_tac (simpset() addsimps [real_mult_less_0_iff]) 2);
by (dres_inst_tac [("x","-h")] spec 1);
by (asm_full_simp_tac
- (simpset() addsimps [real_abs_def, real_inverse_eq_divide,
+ (simpset() addsimps [real_abs_def, inverse_eq_divide,
pos_real_less_divide_eq,
symmetric real_diff_def]
addsplits [split_if_asm]
@@ -2165,7 +2169,7 @@
by (dtac ((real_not_refl2 RS not_sym) RS DERIV_const_ratio_const2) 2
THEN assume_tac 2);
by (ALLGOALS (dres_inst_tac [("f","%u. (b-a)*u")] arg_cong));
-by (auto_tac (claset(), simpset() addsimps [real_inverse_eq_divide]));
+by (auto_tac (claset(), simpset() addsimps [inverse_eq_divide]));
by (asm_full_simp_tac (simpset() addsimps [real_add_commute, eq_commute]) 1);
qed "DERIV_const_average";
--- a/src/HOL/Hyperreal/Log.ML Fri Dec 19 10:38:48 2003 +0100
+++ b/src/HOL/Hyperreal/Log.ML Fri Dec 19 17:13:28 2003 +0100
@@ -74,7 +74,7 @@
Goalw [powr_def]
"[| x powr a < x powr b; 1 < x |] ==> a < b";
by (auto_tac (claset() addDs [ln_gt_zero],
- simpset() addsimps [rename_numerals real_mult_less_cancel2]));
+ simpset() addsimps [mult_less_cancel_right]));
qed "powr_less_cancel";
Goal "1 < x ==> (x powr a < x powr b) = (a < b)";
--- a/src/HOL/Hyperreal/NSA.ML Fri Dec 19 10:38:48 2003 +0100
+++ b/src/HOL/Hyperreal/NSA.ML Fri Dec 19 17:13:28 2003 +0100
@@ -330,11 +330,11 @@
by (ftac hrabs_less_gt_zero 1);
by (dres_inst_tac [("x","r/t")] bspec 1);
by (blast_tac (claset() addIs [SReal_divide]) 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_0_less_divide_iff]) 1);
+by (asm_full_simp_tac (simpset() addsimps [thm"Ring_and_Field.zero_less_divide_iff"]) 1);
by (case_tac "x=0 | y=0" 1);
by (cut_inst_tac [("u","abs x"),("v","r/t"),("x","abs y")]
hypreal_mult_less_mono 2);
-by (auto_tac (claset(), simpset() addsimps [hypreal_0_less_divide_iff]));
+by (auto_tac (claset(), simpset() addsimps [thm"Ring_and_Field.zero_less_divide_iff"]));
qed "Infinitesimal_HFinite_mult";
Goal "[| x : Infinitesimal; y : HFinite |] ==> (y * x) : Infinitesimal";
@@ -347,7 +347,6 @@
"x: HInfinite ==> inverse x: Infinitesimal";
by Auto_tac;
by (eres_inst_tac [("x","inverse r")] ballE 1);
-by (stac hrabs_inverse 1);
by (forw_inst_tac [("x1","r"),("z","abs x")]
(hypreal_inverse_gt_0 RS order_less_trans) 1);
by (assume_tac 1);
@@ -2212,7 +2211,7 @@
Goal "0 < u ==> \
\ (u < inverse (real(Suc n))) = (real(Suc n) < inverse u)";
-by (asm_full_simp_tac (simpset() addsimps [real_inverse_eq_divide]) 1);
+by (asm_full_simp_tac (simpset() addsimps [inverse_eq_divide]) 1);
by (stac pos_real_less_divide_eq 1);
by (assume_tac 1);
by (stac pos_real_less_divide_eq 1);
@@ -2235,7 +2234,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 [real_inverse_eq_divide]) 1);
+by (simp_tac (simpset() addsimps [inverse_eq_divide]) 1);
by (stac pos_real_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);
--- a/src/HOL/Hyperreal/SEQ.ML Fri Dec 19 10:38:48 2003 +0100
+++ b/src/HOL/Hyperreal/SEQ.ML Fri Dec 19 17:13:28 2003 +0100
@@ -1270,7 +1270,7 @@
([LIMSEQ_const, LIMSEQ_realpow_zero] MRS LIMSEQ_mult) 1);
by (auto_tac (claset(),
simpset() addsimps [real_divide_def, realpow_inverse]));
-by (asm_simp_tac (simpset() addsimps [real_inverse_eq_divide,
+by (asm_simp_tac (simpset() addsimps [inverse_eq_divide,
pos_real_divide_less_eq]) 1);
qed "LIMSEQ_divide_realpow_zero";
--- a/src/HOL/Hyperreal/Transcendental.ML Fri Dec 19 10:38:48 2003 +0100
+++ b/src/HOL/Hyperreal/Transcendental.ML Fri Dec 19 17:13:28 2003 +0100
@@ -456,7 +456,7 @@
by (res_inst_tac [("x","0")] exI 1 THEN Step_tac 1);
by (subgoal_tac "0 < abs (x ^ n)" 1);
by (res_inst_tac [("z","abs (x ^ n)")] (CLAIM_SIMP
- "[| (0::real) <z; x*z<=y*z |] ==> x<=y" [real_mult_le_cancel1]) 1);
+ "[| (0::real) <z; x*z<=y*z |] ==> x<=y" [mult_le_cancel_left]) 1);
by (auto_tac (claset(),
simpset() addsimps [real_mult_assoc,realpow_abs]));
by (dres_inst_tac [("x","0")] spec 2 THEN Force_tac 2);
@@ -481,7 +481,7 @@
simpset() addsimps
[realpow_abs,real_divide_eq_inverse RS sym]));
by (res_inst_tac [("z","abs(x)")] (CLAIM_SIMP
- "[|(0::real)<z; x*z<y*z |] ==> x<y" [real_mult_less_cancel1]) 1);
+ "[|(0::real)<z; x*z<y*z |] ==> x<y" [mult_less_cancel_left]) 1);
by (auto_tac (claset(),simpset() addsimps [abs_mult RS sym,real_mult_assoc]));
qed "powser_insidea";
@@ -624,7 +624,7 @@
by (dtac real_gt_half_sum 2);
by (auto_tac (claset(),simpset() addsimps [abs_eqI2]));
by (res_inst_tac [("z","k/2")] (CLAIM_SIMP
- "[| (0::real) <z; x*z<=y*z |] ==> x<=y" [real_mult_le_cancel1]) 2);
+ "[| (0::real) <z; x*z<=y*z |] ==> x<=y" [mult_le_cancel_left]) 2);
by (auto_tac (claset() addIs [abs_ge_zero RS real_le_trans],simpset()));
by (dtac real_le_imp_less_or_eq 1);
by Auto_tac;
@@ -639,7 +639,7 @@
by (res_inst_tac [("y","K * abs x")] order_le_less_trans 1);
by (res_inst_tac [("R2.0","K * e")] real_less_trans 2);
by (res_inst_tac [("z","inverse K")] (CLAIM_SIMP
- "[|(0::real) <z; z*x<z*y |] ==> x<y" [real_mult_less_cancel1]) 3);
+ "[|(0::real) <z; z*x<z*y |] ==> x<y" [mult_less_cancel_left]) 3);
by (asm_full_simp_tac (simpset() addsimps [mult_assoc RS sym]) 4);
by (Force_tac 1);
by (asm_full_simp_tac (simpset() addsimps [mult_less_cancel_left]) 1);
--- a/src/HOL/Hyperreal/hypreal_arith.ML Fri Dec 19 10:38:48 2003 +0100
+++ b/src/HOL/Hyperreal/hypreal_arith.ML Fri Dec 19 17:13:28 2003 +0100
@@ -10,7 +10,7 @@
(* reduce contradictory <= to False *)
val simps = [True_implies_equals,inst "w" "number_of ?v" hypreal_add_mult_distrib2,
- hypreal_divide_1,hypreal_times_divide1_eq,hypreal_times_divide2_eq];
+ divide_1,times_divide_eq_right,times_divide_eq_left];
val simprocs = [hypreal_cancel_numeral_factors_divide];
--- a/src/HOL/Real/RComplete.ML Fri Dec 19 10:38:48 2003 +0100
+++ b/src/HOL/Real/RComplete.ML Fri Dec 19 17:13:28 2003 +0100
@@ -199,7 +199,7 @@
by (rtac ccontr 1);
by (subgoal_tac "ALL n. x * real (Suc n) <= 1" 1);
by (asm_full_simp_tac
- (simpset() addsimps [linorder_not_less, real_inverse_eq_divide]) 2);
+ (simpset() addsimps [linorder_not_less, inverse_eq_divide]) 2);
by (Clarify_tac 2);
by (dres_inst_tac [("x","n")] spec 2);
by (dres_inst_tac [("k","real (Suc n)")] (real_mult_le_mono1) 2);
--- a/src/HOL/Real/RealOrd.thy Fri Dec 19 10:38:48 2003 +0100
+++ b/src/HOL/Real/RealOrd.thy Fri Dec 19 17:13:28 2003 +0100
@@ -272,9 +272,6 @@
lemma real_mult_not_zero: "[| x ~= 0; y ~= 0 |] ==> x * y ~= (0::real)"
by simp
-lemma real_inverse_eq_divide: "inverse (x::real) = 1/x"
- by (rule Ring_and_Field.inverse_eq_divide)
-
lemma real_inverse_inverse: "inverse(inverse (x::real)) = x"
by (rule Ring_and_Field.inverse_inverse_eq)
@@ -337,38 +334,6 @@
by (rule Ring_and_Field.add_le_cancel_left)
-subsection{*Factor Cancellation Theorems for Type @{text real}*}
-
-lemma real_mult_less_cancel2:
- "(m*k < n*k) = (((0::real) < k & m<n) | (k < 0 & n<m))"
- by (rule Ring_and_Field.mult_less_cancel_right)
-
-lemma real_mult_le_cancel2:
- "(m*k <= n*k) = (((0::real) < k --> m<=n) & (k < 0 --> n<=m))"
- by (rule Ring_and_Field.mult_le_cancel_right)
-
-lemma real_mult_less_cancel1:
- "(k*m < k*n) = (((0::real) < k & m<n) | (k < 0 & n<m))"
- by (rule Ring_and_Field.mult_less_cancel_left)
-
-lemma real_mult_le_cancel1:
- "!!k::real. (k*m <= k*n) = ((0 < k --> m<=n) & (k < 0 --> n<=m))"
- by (rule Ring_and_Field.mult_le_cancel_left)
-
-lemma real_mult_eq_cancel1: "!!k::real. (k*m = k*n) = (k = 0 | m=n)"
- by (rule Ring_and_Field.mult_cancel_left)
-
-lemma real_mult_eq_cancel2: "!!k::real. (m*k = n*k) = (k = 0 | m=n)"
- by (rule Ring_and_Field.mult_cancel_right)
-
-lemma real_mult_div_cancel1: "!!k::real. k~=0 ==> (k*m) / (k*n) = (m/n)"
- by (rule Ring_and_Field.mult_divide_cancel_left)
-
-lemma real_mult_div_cancel_disj:
- "(k*m) / (k*n) = (if k = (0::real) then 0 else m/n)"
- by (rule Ring_and_Field.mult_divide_cancel_eq_if)
-
-
subsection{*Inverse and Division*}
lemma real_inverse_gt_0: "0 < x ==> 0 < inverse (x::real)"
--- a/src/HOL/Real/real_arith.ML Fri Dec 19 10:38:48 2003 +0100
+++ b/src/HOL/Real/real_arith.ML Fri Dec 19 17:13:28 2003 +0100
@@ -30,15 +30,17 @@
and d = gcd(m,m') and n=m/d and n'=m'/d.
*)
-val real_inverse_eq_divide = thm"real_inverse_eq_divide";
-val real_mult_less_cancel2 = thm"real_mult_less_cancel2";
-val real_mult_le_cancel2 = thm"real_mult_le_cancel2";
-val real_mult_less_cancel1 = thm"real_mult_less_cancel1";
-val real_mult_le_cancel1 = thm"real_mult_le_cancel1";
-val real_mult_eq_cancel1 = thm"real_mult_eq_cancel1";
-val real_mult_eq_cancel2 = thm"real_mult_eq_cancel2";
-val real_mult_div_cancel1 = thm"real_mult_div_cancel1";
-val real_mult_div_cancel_disj = thm"real_mult_div_cancel_disj";
+val inverse_eq_divide = thm"Ring_and_Field.inverse_eq_divide";
+
+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 mult_divide_cancel_left = thm"Ring_and_Field.mult_divide_cancel_left";
+val mult_divide_cancel_eq_if = thm"Ring_and_Field.mult_divide_cancel_eq_if";
local
@@ -67,7 +69,7 @@
val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binop "HOL.divide"
val dest_bal = HOLogic.dest_bin "HOL.divide" HOLogic.realT
- val cancel = real_mult_div_cancel1 RS trans
+ val cancel = mult_divide_cancel_left RS trans
val neg_exchanges = false
)
@@ -76,7 +78,7 @@
val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" HOLogic.realT
- val cancel = real_mult_eq_cancel1 RS trans
+ val cancel = mult_cancel_left RS trans
val neg_exchanges = false
)
@@ -85,7 +87,7 @@
val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "op <"
val dest_bal = HOLogic.dest_bin "op <" HOLogic.realT
- val cancel = real_mult_less_cancel1 RS trans
+ val cancel = mult_less_cancel_left RS trans
val neg_exchanges = true
)
@@ -94,7 +96,7 @@
val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "op <="
val dest_bal = HOLogic.dest_bin "op <=" HOLogic.realT
- val cancel = real_mult_le_cancel1 RS trans
+ val cancel = mult_le_cancel_left RS trans
val neg_exchanges = true
)
@@ -185,7 +187,7 @@
val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" HOLogic.realT
- val simplify_meta_eq = cancel_simplify_meta_eq real_mult_eq_cancel1
+ val simplify_meta_eq = cancel_simplify_meta_eq mult_cancel_left
);
@@ -194,7 +196,7 @@
val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binop "HOL.divide"
val dest_bal = HOLogic.dest_bin "HOL.divide" HOLogic.realT
- val simplify_meta_eq = cancel_simplify_meta_eq real_mult_div_cancel_disj
+ val simplify_meta_eq = cancel_simplify_meta_eq mult_divide_cancel_eq_if
);
val real_cancel_factor =
--- a/src/HOL/Ring_and_Field.thy Fri Dec 19 10:38:48 2003 +0100
+++ b/src/HOL/Ring_and_Field.thy Fri Dec 19 17:13:28 2003 +0100
@@ -1398,7 +1398,7 @@
lemma abs_idempotent [simp]: "abs (abs a) = abs (a::'a::ordered_ring)"
by (force elim: order_less_asym simp add: abs_if)
-lemma abs_zero_iff [iff]: "(abs a = 0) = (a = (0::'a::ordered_ring))"
+lemma abs_zero_iff [simp]: "(abs a = 0) = (a = (0::'a::ordered_ring))"
by (simp add: abs_if)
lemma abs_ge_self: "a \<le> abs (a::'a::ordered_ring)"