Redesigned the decision procedures for (Abelian) groups and commutative rings.

--- a/src/HOL/Integ/Group.ML	Sat Nov 15 13:10:52 1997 +0100
+++ b/src/HOL/Integ/Group.ML	Sat Nov 15 18:41:06 1997 +0100
@@ -1,12 +1,14 @@
 (*  Title:      HOL/Integ/Group.ML
     ID:         $Id$
     Author:     Tobias Nipkow
-    Copyright   1996 TU Muenchen
+    Copyright   1997 TU Muenchen
 *)
 
-open Group;
+(*** Groups ***)
 
-Addsimps [zeroL,zeroR,plus_assoc,plus_commute];
+(* Derives the well-known convergent set of equations for groups
+   based on the unary inverse zero-x.
+*)
 
 goal Group.thy "!!x::'a::add_group. (zero-x)+(x+y) = y";
 by (rtac trans 1);
@@ -27,7 +29,7 @@
 by (rtac (zeroR RS sym) 1);
 by (rtac trans 1);
 by (res_inst_tac [("x","zero")] left_inv2 2);
-by (Simp_tac 1);
+by (simp_tac (simpset() addsimps [zeroR]) 1);
 qed "inv_zero";
 
 goal Group.thy "!!x::'a::add_group. x+(zero-x) = zero";
@@ -44,19 +46,6 @@
 by (rtac refl 1);
 qed "right_inv2";
 
-goal Group.thy "!!x::'a::add_group. x-x = zero";
-by (stac minus_inv 1);
-by (rtac right_inv 1);
-qed "minus_self_zero";
-Addsimps [minus_self_zero];
-
-goal Group.thy "!!x::'a::add_group. x-zero = x";
-by (stac minus_inv 1);
-by (stac inv_zero 1);
-by (rtac zeroR 1);
-qed "minus_zero";
-Addsimps [minus_zero];
-
 val plus_cong = read_instantiate [("f1","op +")] (arg_cong RS cong);
 
 goal Group.thy "!!x::'a::add_group. zero-(x+y) = (zero-y)+(zero-x)";
@@ -70,22 +59,127 @@
  by (rtac plus_assoc 2);
 by (rtac trans 1);
  by (rtac plus_cong 2);
-  by (simp_tac (simpset() addsimps [left_inv,left_inv2,right_inv,right_inv2]) 2);
+  by (simp_tac (simpset() addsimps
+        [plus_assoc,left_inv,left_inv2,right_inv,right_inv2]) 2);
  by (rtac refl 2);
 by (rtac (zeroL RS sym) 1);
 qed "inv_plus";
 
+(*** convergent TRS for groups with unary inverse zero-x ***)
+val group1_simps =
+  [zeroL,zeroR,plus_assoc,left_inv,left_inv2,right_inv,right_inv2,inv_inv,
+   inv_zero,inv_plus];
+
+val group1_tac =
+  let val ss = HOL_basic_ss addsimps group1_simps
+  in simp_tac ss end;
+
+(* I believe there is no convergent TRS for groups with binary `-',
+   unless you have an extra unary `-' and simply define x-y = x+(-y).
+   This does not work with only a binary `-' because x-y = x+(zero-y) does
+   not terminate. Hence we have a special tactic for converting all
+   occurrences of x-y into x+(zero-y):
+*)
+
+local
+fun find(Const("op -",Type("fun",[T,_]))$s$t) = [(T,s,t)] @ find s @ find t
+  | find(s$t) = find s @ find t
+  | find _ = [];
+
+fun subst_tac sg (tacf,(T,s,t)) = 
+  let val typinst = [(("'a",0),ctyp_of sg T)];
+      val terminst = [(cterm_of sg (Var(("x",0),T)),cterm_of sg s),
+                      (cterm_of sg (Var(("y",0),T)),cterm_of sg t)];
+  in tacf THEN' rtac ((instantiate(typinst,terminst) minus_inv) RS ssubst) end;
+
+in
+val mk_group1_tac = SUBGOAL(fn (t,i) => fn st =>
+      let val sg = #sign(rep_thm st)
+      in foldl (subst_tac sg) (K all_tac,find t) i st
+      end)
+end;
+
+(* The following two equations are not used in any of the decision procedures,
+   but are still very useful. They also demonstrate mk_group1_tac.
+*)
+goal Group.thy "x-x = (zero::'a::add_group)";
+by(mk_group1_tac 1);
+by(group1_tac 1);
+qed "minus_self_zero";
+
+goal Group.thy "x-zero = (x::'a::add_group)";
+by(mk_group1_tac 1);
+by(group1_tac 1);
+qed "minus_zero";
+
+(*** Abelian Groups ***)
+
 goal Group.thy "x+(y+z)=y+(x+z::'a::add_agroup)";
 by (rtac trans 1);
 by (rtac plus_commute 1);
 by (rtac trans 1);
 by (rtac plus_assoc 1);
-by (Simp_tac 1);
+by (simp_tac (simpset() addsimps [plus_commute]) 1);
 qed "plus_commuteL";
-Addsimps [plus_commuteL];
+
+(* Convergent TRS for Abelian groups with unary inverse zero-x.
+   Requires ordered rewriting
+*)
+
+val agroup1_simps = plus_commute::plus_commuteL::group1_simps;
+
+val agroup1_tac =
+  let val ss = HOL_basic_ss addsimps agroup1_simps
+  in simp_tac ss end;
+
+(* Again, I do not believe there is a convergent TRS for Abelian Groups with
+   binary `-'. However, we can still decide the word problem using additional
+   rules for 
+   1. floating `-' to the top:
+      "x + (y - z) = (x + y) - (z::'a::add_group)"
+      "(x - y) + z = (x + z) - (y::'a::add_agroup)"
+      "(x - y) - z = x - (y + (z::'a::add_agroup))"
+      "x - (y - z) = (x + z) - (y::'a::add_agroup)"
+   2. and for moving `-' over to the other side:
+      (x-y = z) = (x = z+y) and (x = y-z) = (x+z = y)
+*)
+goal Group.thy "x + (y - z) = (x + y) - (z::'a::add_group)";
+by(mk_group1_tac 1);
+by(group1_tac 1);
+qed "plus_minusR";
 
-Addsimps [inv_inv,inv_plus];
+goal Group.thy "(x - y) + z = (x + z) - (y::'a::add_agroup)";
+by(mk_group1_tac 1);
+by(agroup1_tac 1);
+qed "plus_minusL";
+
+goal Group.thy "(x - y) - z = x - (y + (z::'a::add_agroup))";
+by(mk_group1_tac 1);
+by(agroup1_tac 1);
+qed "minus_minusL";
+
+goal Group.thy "x - (y - z) = (x + z) - (y::'a::add_agroup)";
+by(mk_group1_tac 1);
+by(agroup1_tac 1);
+qed "minus_minusR";
 
+goal Group.thy "!!x::'a::add_group. (x-y = z) = (x = z+y)";
+by(stac minus_inv 1);
+by(fast_tac (claset() addss (HOL_basic_ss addsimps group1_simps)) 1);
+qed "minusL_iff";
+
+goal Group.thy "!!x::'a::add_group. (x = y-z) = (x+z = y)";
+by(stac minus_inv 1);
+by(fast_tac (claset() addss (HOL_basic_ss addsimps group1_simps)) 1);
+qed "minusR_iff";
+
+val agroup2_simps =
+  [zeroL,zeroR,plus_assoc,plus_commute,plus_commuteL,
+   plus_minusR,plus_minusL,minus_minusL,minus_minusR,minusL_iff,minusR_iff];
+
+(* This two-phase ordered rewriting tactic works, but agroup_simps are
+   simpler. However, agroup_simps is not confluent for arbitrary terms,
+   it merely decides equality.
 (* Phase 1 *)
 
 goal Group.thy "!!x::'a::add_agroup. (x+(zero-y))+z = (x+z)+(zero-y)";
@@ -125,3 +219,4 @@
 val lemma = result();
 bind_thm("minus_plusL3",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
 
+*)

--- a/src/HOL/Integ/Group.thy	Sat Nov 15 13:10:52 1997 +0100
+++ b/src/HOL/Integ/Group.thy	Sat Nov 15 18:41:06 1997 +0100
@@ -25,7 +25,13 @@
   zeroR    "x + zero = x"
 
 (* additive groups *)
-
+(*
+The inverse is the binary `-'. Groups with unary and binary inverse are
+interdefinable: x-y := x+(zero-y) and -x := zero-x. The law left_inv is
+simply the translation of (-x)+x = zero. This characterizes groups already,
+provided we only allow (zero-x). Law minus_inv `defines' the general x-y in
+terms of the specific zero-y.
+*)
 axclass  add_group < add_monoid, minus
   left_inv  "(zero-x)+x = zero"
   minus_inv "x-y = x + (zero-y)"

--- a/src/HOL/Integ/Lagrange.ML	Sat Nov 15 13:10:52 1997 +0100
+++ b/src/HOL/Integ/Lagrange.ML	Sat Nov 15 18:41:06 1997 +0100
@@ -16,5 +16,22 @@
 \  sq(x1*y3 - x2*y4 + x3*y1 + x4*y2)  + \
 \  sq(x1*y4 + x2*y3 - x3*y2 + x4*y1)";
 (*Takes up to three minutes...*)
-by (cring_simp 1);
+by (cring_tac 1);
 qed "Lagrange_lemma";
+
+(* A challenge by John Harrison.
+   Takes forever because of the naive bottom-up strategy of the rewriter.
+
+goalw Lagrange.thy [Lagrange.sq_def] "!!p1::'a::cring.\
+\ (sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * \
+\ (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2) \
+\  = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) + \
+\    sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) +\
+\    sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) +\
+\    sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) +\
+\    sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) +\
+\    sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +\
+\    sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +\
+\    sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)";
+
+*)

--- 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;
+***)