src/HOL/Integ/Ring.ML

--- a/src/HOL/Integ/Ring.ML	Sat Nov 15 13:10:52 1997 +0100
+++ b/src/HOL/Integ/Ring.ML	Sat Nov 15 18:41:06 1997 +0100
@@ -7,23 +7,13 @@
 and defines cring_simpl, a simplification tactic for commutative rings.
 *)
 
-open Ring;
-
-(***
-It is not clear if all thsese rules, esp. distributivity, should be part
-of the default simpset. At the moment they are because they are used in the
-decision procedure.
-***)   
-Addsimps [times_assoc,times_commute,distribL,distribR];
-
 goal Ring.thy "!!x::'a::cring. x*(y*z)=y*(x*z)";
 by (rtac trans 1);
 by (rtac times_commute 1);
 by (rtac trans 1);
 by (rtac times_assoc 1);
-by (Simp_tac 1);
+by (simp_tac (HOL_basic_ss addsimps [times_commute]) 1);
 qed "times_commuteL";
-Addsimps [times_commuteL];
 
 val times_cong = read_instantiate [("f1","op *")] (arg_cong RS cong);
 
@@ -119,30 +109,31 @@
 by (rtac (zeroR RS sym) 1);
 qed "mult_invR";
 
-Addsimps[mult_invL,mult_invR];
-
-
-goal Ring.thy "!!x::'a::ring. x*(y-z) = x*y - x*z";
-by (stac minus_inv 1);
-by (rtac sym 1);
-by (stac minus_inv 1);
-by (Simp_tac 1);
+goal Ring.thy "x*(y-z) = (x*y - x*z::'a::ring)";
+by(mk_group1_tac 1);
+by(simp_tac (HOL_basic_ss addsimps [distribL,mult_invR]) 1);
 qed "minus_distribL";
 
-goal Ring.thy "!!x::'a::ring. (x-y)*z = x*z - y*z";
-by (stac minus_inv 1);
-by (rtac sym 1);
-by (stac minus_inv 1);
-by (Simp_tac 1);
+goal Ring.thy "(x-y)*z = (x*z - y*z::'a::ring)";
+by(mk_group1_tac 1);
+by(simp_tac (HOL_basic_ss addsimps [distribR,mult_invL]) 1);
 qed "minus_distribR";
 
-Addsimps [minus_distribL,minus_distribR];
+val cring_simps = [times_assoc,times_commute,times_commuteL,
+                   distribL,distribR,minus_distribL,minus_distribR]
+                  @ agroup2_simps;
+
+val cring_tac =
+  let val ss = HOL_basic_ss addsimps cring_simps
+  in simp_tac ss end;
+
 
 (*** The order [minus_plusL3,minus_plusL2] is important because minus_plusL3
-     MUST be tried first ***)
+     MUST be tried first
 val cring_simp =
   let val phase1 = simpset() addsimps
                    [plus_minusL,minus_plusR,minus_minusR,plus_minusR]
       val phase2 = HOL_ss addsimps [minus_plusL3,minus_plusL2,
                                     zeroL,zeroR,mult_zeroL,mult_zeroR]
   in simp_tac phase1 THEN' simp_tac phase2 end;
+***)