--- a/src/HOL/Hyperreal/HyperBin.ML Mon Dec 22 15:42:21 2003 +0100
+++ b/src/HOL/Hyperreal/HyperBin.ML Mon Dec 22 16:22:14 2003 +0100
@@ -124,7 +124,7 @@
(** Simplification of arithmetic when nested to the right **)
Goal "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::hypreal)";
-by Auto_tac;
+by (asm_full_simp_tac (simpset() addsimps [add_assoc RS sym]) 1);
qed "hypreal_add_number_of_left";
Goal "number_of v *(number_of w * z) = (number_of(bin_mult v w) * z::hypreal)";
@@ -139,7 +139,7 @@
Goal "number_of v + (c - number_of w) = \
\ number_of (bin_add v (bin_minus w)) + (c::hypreal)";
by (stac (diff_hypreal_number_of RS sym) 1);
-by Auto_tac;
+by (asm_full_simp_tac (HOL_ss addsimps [hypreal_diff_def]@add_ac) 1);
qed "hypreal_add_number_of_diff2";
Addsimps [hypreal_add_number_of_left, hypreal_mult_number_of_left,
@@ -166,7 +166,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]) 1);
+by (asm_simp_tac (simpset() addsimps [hypreal_add_mult_distrib] @ add_ac) 1);
qed "left_hypreal_add_mult_distrib";
@@ -524,9 +524,6 @@
Addsimprocs Hyperreal_Numeral_Simprocs.cancel_numerals;
Addsimprocs [Hyperreal_Numeral_Simprocs.combine_numerals];
-(*The Abel_Cancel simprocs are now obsolete*)
-Delsimprocs [Hyperreal_Cancel.sum_conv, Hyperreal_Cancel.rel_conv];
-
(*examples:
print_depth 22;
set timing;
--- a/src/HOL/Hyperreal/HyperOrd.thy Mon Dec 22 15:42:21 2003 +0100
+++ b/src/HOL/Hyperreal/HyperOrd.thy Mon Dec 22 16:22:14 2003 +0100
@@ -326,63 +326,4 @@
val hypreal_mult_self_sum_ge_zero = thm "hypreal_mult_self_sum_ge_zero";
*}
-(**** The simproc abel_cancel ****)
-
-(*** Two lemmas needed for the simprocs ***)
-
-(*Deletion of other terms in the formula, seeking the -x at the front of z*)
-lemma hypreal_add_cancel_21: "((x::hypreal) + (y + z) = y + u) = ((x + z) = u)"
-apply (subst hypreal_add_left_commute)
-apply (rule hypreal_add_left_cancel)
-done
-
-(*A further rule to deal with the case that
- everything gets cancelled on the right.*)
-lemma hypreal_add_cancel_end: "((x::hypreal) + (y + z) = y) = (x = -z)"
-apply (subst hypreal_add_left_commute)
-apply (rule_tac t = y in hypreal_add_zero_right [THEN subst], subst hypreal_add_left_cancel)
-apply (simp (no_asm) add: hypreal_eq_diff_eq [symmetric])
-done
-
-ML{*
-val hypreal_add_cancel_21 = thm "hypreal_add_cancel_21";
-val hypreal_add_cancel_end = thm "hypreal_add_cancel_end";
-
-structure Hyperreal_Cancel_Data =
-struct
- val ss = HOL_ss
- val eq_reflection = eq_reflection
-
- val sg_ref = Sign.self_ref (Theory.sign_of (the_context ()))
- val T = Type("HyperDef.hypreal",[])
- val zero = Const ("0", T)
- val restrict_to_left = restrict_to_left
- val add_cancel_21 = hypreal_add_cancel_21
- val add_cancel_end = hypreal_add_cancel_end
- val add_left_cancel = hypreal_add_left_cancel
- val add_assoc = hypreal_add_assoc
- val add_commute = hypreal_add_commute
- val add_left_commute = hypreal_add_left_commute
- val add_0 = hypreal_add_zero_left
- val add_0_right = hypreal_add_zero_right
-
- val eq_diff_eq = hypreal_eq_diff_eq
- val eqI_rules = [hypreal_less_eqI, hypreal_eq_eqI, hypreal_le_eqI]
- fun dest_eqI th =
- #1 (HOLogic.dest_bin "op =" HOLogic.boolT
- (HOLogic.dest_Trueprop (concl_of th)))
-
- val diff_def = hypreal_diff_def
- val minus_add_distrib = hypreal_minus_add_distrib
- val minus_minus = hypreal_minus_minus
- val minus_0 = hypreal_minus_zero
- val add_inverses = [hypreal_add_minus, hypreal_add_minus_left]
- val cancel_simps = [hypreal_add_minus_cancelA, hypreal_minus_add_cancelA]
-end;
-
-structure Hyperreal_Cancel = Abel_Cancel (Hyperreal_Cancel_Data);
-
-Addsimprocs [Hyperreal_Cancel.sum_conv, Hyperreal_Cancel.rel_conv];
-*}
-
end