# HG changeset patch
# User paulson
# Date 1072106534 -3600
# Node ID f79633c262a343a39306d9985f9701b221629c89
# Parent  2f048db93d086e9138bcdb2d8cb5dd346aa56e79
removal of the abel_cancel simproc for hypreal

diff -r 2f048db93d08 -r f79633c262a3 src/HOL/Hyperreal/HyperBin.ML
--- 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;
diff -r 2f048db93d08 -r f79633c262a3 src/HOL/Hyperreal/HyperOrd.thy
--- 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