Redesigned the decision procedures for (Abelian) groups and commutative rings.
authornipkow
Sat Nov 15 18:41:06 1997 +0100 (1997-11-15)
changeset 4230eb5586526bc9
parent 4229 551684f275b9
child 4231 a73f5a63f197
Redesigned the decision procedures for (Abelian) groups and commutative rings.
src/HOL/Integ/Group.ML
src/HOL/Integ/Group.thy
src/HOL/Integ/Lagrange.ML
src/HOL/Integ/Ring.ML
     1.1 --- a/src/HOL/Integ/Group.ML	Sat Nov 15 13:10:52 1997 +0100
     1.2 +++ b/src/HOL/Integ/Group.ML	Sat Nov 15 18:41:06 1997 +0100
     1.3 @@ -1,12 +1,14 @@
     1.4  (*  Title:      HOL/Integ/Group.ML
     1.5      ID:         $Id$
     1.6      Author:     Tobias Nipkow
     1.7 -    Copyright   1996 TU Muenchen
     1.8 +    Copyright   1997 TU Muenchen
     1.9  *)
    1.10  
    1.11 -open Group;
    1.12 +(*** Groups ***)
    1.13  
    1.14 -Addsimps [zeroL,zeroR,plus_assoc,plus_commute];
    1.15 +(* Derives the well-known convergent set of equations for groups
    1.16 +   based on the unary inverse zero-x.
    1.17 +*)
    1.18  
    1.19  goal Group.thy "!!x::'a::add_group. (zero-x)+(x+y) = y";
    1.20  by (rtac trans 1);
    1.21 @@ -27,7 +29,7 @@
    1.22  by (rtac (zeroR RS sym) 1);
    1.23  by (rtac trans 1);
    1.24  by (res_inst_tac [("x","zero")] left_inv2 2);
    1.25 -by (Simp_tac 1);
    1.26 +by (simp_tac (simpset() addsimps [zeroR]) 1);
    1.27  qed "inv_zero";
    1.28  
    1.29  goal Group.thy "!!x::'a::add_group. x+(zero-x) = zero";
    1.30 @@ -44,19 +46,6 @@
    1.31  by (rtac refl 1);
    1.32  qed "right_inv2";
    1.33  
    1.34 -goal Group.thy "!!x::'a::add_group. x-x = zero";
    1.35 -by (stac minus_inv 1);
    1.36 -by (rtac right_inv 1);
    1.37 -qed "minus_self_zero";
    1.38 -Addsimps [minus_self_zero];
    1.39 -
    1.40 -goal Group.thy "!!x::'a::add_group. x-zero = x";
    1.41 -by (stac minus_inv 1);
    1.42 -by (stac inv_zero 1);
    1.43 -by (rtac zeroR 1);
    1.44 -qed "minus_zero";
    1.45 -Addsimps [minus_zero];
    1.46 -
    1.47  val plus_cong = read_instantiate [("f1","op +")] (arg_cong RS cong);
    1.48  
    1.49  goal Group.thy "!!x::'a::add_group. zero-(x+y) = (zero-y)+(zero-x)";
    1.50 @@ -70,22 +59,127 @@
    1.51   by (rtac plus_assoc 2);
    1.52  by (rtac trans 1);
    1.53   by (rtac plus_cong 2);
    1.54 -  by (simp_tac (simpset() addsimps [left_inv,left_inv2,right_inv,right_inv2]) 2);
    1.55 +  by (simp_tac (simpset() addsimps
    1.56 +        [plus_assoc,left_inv,left_inv2,right_inv,right_inv2]) 2);
    1.57   by (rtac refl 2);
    1.58  by (rtac (zeroL RS sym) 1);
    1.59  qed "inv_plus";
    1.60  
    1.61 +(*** convergent TRS for groups with unary inverse zero-x ***)
    1.62 +val group1_simps =
    1.63 +  [zeroL,zeroR,plus_assoc,left_inv,left_inv2,right_inv,right_inv2,inv_inv,
    1.64 +   inv_zero,inv_plus];
    1.65 +
    1.66 +val group1_tac =
    1.67 +  let val ss = HOL_basic_ss addsimps group1_simps
    1.68 +  in simp_tac ss end;
    1.69 +
    1.70 +(* I believe there is no convergent TRS for groups with binary `-',
    1.71 +   unless you have an extra unary `-' and simply define x-y = x+(-y).
    1.72 +   This does not work with only a binary `-' because x-y = x+(zero-y) does
    1.73 +   not terminate. Hence we have a special tactic for converting all
    1.74 +   occurrences of x-y into x+(zero-y):
    1.75 +*)
    1.76 +
    1.77 +local
    1.78 +fun find(Const("op -",Type("fun",[T,_]))$s$t) = [(T,s,t)] @ find s @ find t
    1.79 +  | find(s$t) = find s @ find t
    1.80 +  | find _ = [];
    1.81 +
    1.82 +fun subst_tac sg (tacf,(T,s,t)) = 
    1.83 +  let val typinst = [(("'a",0),ctyp_of sg T)];
    1.84 +      val terminst = [(cterm_of sg (Var(("x",0),T)),cterm_of sg s),
    1.85 +                      (cterm_of sg (Var(("y",0),T)),cterm_of sg t)];
    1.86 +  in tacf THEN' rtac ((instantiate(typinst,terminst) minus_inv) RS ssubst) end;
    1.87 +
    1.88 +in
    1.89 +val mk_group1_tac = SUBGOAL(fn (t,i) => fn st =>
    1.90 +      let val sg = #sign(rep_thm st)
    1.91 +      in foldl (subst_tac sg) (K all_tac,find t) i st
    1.92 +      end)
    1.93 +end;
    1.94 +
    1.95 +(* The following two equations are not used in any of the decision procedures,
    1.96 +   but are still very useful. They also demonstrate mk_group1_tac.
    1.97 +*)
    1.98 +goal Group.thy "x-x = (zero::'a::add_group)";
    1.99 +by(mk_group1_tac 1);
   1.100 +by(group1_tac 1);
   1.101 +qed "minus_self_zero";
   1.102 +
   1.103 +goal Group.thy "x-zero = (x::'a::add_group)";
   1.104 +by(mk_group1_tac 1);
   1.105 +by(group1_tac 1);
   1.106 +qed "minus_zero";
   1.107 +
   1.108 +(*** Abelian Groups ***)
   1.109 +
   1.110  goal Group.thy "x+(y+z)=y+(x+z::'a::add_agroup)";
   1.111  by (rtac trans 1);
   1.112  by (rtac plus_commute 1);
   1.113  by (rtac trans 1);
   1.114  by (rtac plus_assoc 1);
   1.115 -by (Simp_tac 1);
   1.116 +by (simp_tac (simpset() addsimps [plus_commute]) 1);
   1.117  qed "plus_commuteL";
   1.118 -Addsimps [plus_commuteL];
   1.119 +
   1.120 +(* Convergent TRS for Abelian groups with unary inverse zero-x.
   1.121 +   Requires ordered rewriting
   1.122 +*)
   1.123 +
   1.124 +val agroup1_simps = plus_commute::plus_commuteL::group1_simps;
   1.125 +
   1.126 +val agroup1_tac =
   1.127 +  let val ss = HOL_basic_ss addsimps agroup1_simps
   1.128 +  in simp_tac ss end;
   1.129 +
   1.130 +(* Again, I do not believe there is a convergent TRS for Abelian Groups with
   1.131 +   binary `-'. However, we can still decide the word problem using additional
   1.132 +   rules for 
   1.133 +   1. floating `-' to the top:
   1.134 +      "x + (y - z) = (x + y) - (z::'a::add_group)"
   1.135 +      "(x - y) + z = (x + z) - (y::'a::add_agroup)"
   1.136 +      "(x - y) - z = x - (y + (z::'a::add_agroup))"
   1.137 +      "x - (y - z) = (x + z) - (y::'a::add_agroup)"
   1.138 +   2. and for moving `-' over to the other side:
   1.139 +      (x-y = z) = (x = z+y) and (x = y-z) = (x+z = y)
   1.140 +*)
   1.141 +goal Group.thy "x + (y - z) = (x + y) - (z::'a::add_group)";
   1.142 +by(mk_group1_tac 1);
   1.143 +by(group1_tac 1);
   1.144 +qed "plus_minusR";
   1.145  
   1.146 -Addsimps [inv_inv,inv_plus];
   1.147 +goal Group.thy "(x - y) + z = (x + z) - (y::'a::add_agroup)";
   1.148 +by(mk_group1_tac 1);
   1.149 +by(agroup1_tac 1);
   1.150 +qed "plus_minusL";
   1.151 +
   1.152 +goal Group.thy "(x - y) - z = x - (y + (z::'a::add_agroup))";
   1.153 +by(mk_group1_tac 1);
   1.154 +by(agroup1_tac 1);
   1.155 +qed "minus_minusL";
   1.156 +
   1.157 +goal Group.thy "x - (y - z) = (x + z) - (y::'a::add_agroup)";
   1.158 +by(mk_group1_tac 1);
   1.159 +by(agroup1_tac 1);
   1.160 +qed "minus_minusR";
   1.161  
   1.162 +goal Group.thy "!!x::'a::add_group. (x-y = z) = (x = z+y)";
   1.163 +by(stac minus_inv 1);
   1.164 +by(fast_tac (claset() addss (HOL_basic_ss addsimps group1_simps)) 1);
   1.165 +qed "minusL_iff";
   1.166 +
   1.167 +goal Group.thy "!!x::'a::add_group. (x = y-z) = (x+z = y)";
   1.168 +by(stac minus_inv 1);
   1.169 +by(fast_tac (claset() addss (HOL_basic_ss addsimps group1_simps)) 1);
   1.170 +qed "minusR_iff";
   1.171 +
   1.172 +val agroup2_simps =
   1.173 +  [zeroL,zeroR,plus_assoc,plus_commute,plus_commuteL,
   1.174 +   plus_minusR,plus_minusL,minus_minusL,minus_minusR,minusL_iff,minusR_iff];
   1.175 +
   1.176 +(* This two-phase ordered rewriting tactic works, but agroup_simps are
   1.177 +   simpler. However, agroup_simps is not confluent for arbitrary terms,
   1.178 +   it merely decides equality.
   1.179  (* Phase 1 *)
   1.180  
   1.181  goal Group.thy "!!x::'a::add_agroup. (x+(zero-y))+z = (x+z)+(zero-y)";
   1.182 @@ -125,3 +219,4 @@
   1.183  val lemma = result();
   1.184  bind_thm("minus_plusL3",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
   1.185  
   1.186 +*)
     2.1 --- a/src/HOL/Integ/Group.thy	Sat Nov 15 13:10:52 1997 +0100
     2.2 +++ b/src/HOL/Integ/Group.thy	Sat Nov 15 18:41:06 1997 +0100
     2.3 @@ -25,7 +25,13 @@
     2.4    zeroR    "x + zero = x"
     2.5  
     2.6  (* additive groups *)
     2.7 -
     2.8 +(*
     2.9 +The inverse is the binary `-'. Groups with unary and binary inverse are
    2.10 +interdefinable: x-y := x+(zero-y) and -x := zero-x. The law left_inv is
    2.11 +simply the translation of (-x)+x = zero. This characterizes groups already,
    2.12 +provided we only allow (zero-x). Law minus_inv `defines' the general x-y in
    2.13 +terms of the specific zero-y.
    2.14 +*)
    2.15  axclass  add_group < add_monoid, minus
    2.16    left_inv  "(zero-x)+x = zero"
    2.17    minus_inv "x-y = x + (zero-y)"
     3.1 --- a/src/HOL/Integ/Lagrange.ML	Sat Nov 15 13:10:52 1997 +0100
     3.2 +++ b/src/HOL/Integ/Lagrange.ML	Sat Nov 15 18:41:06 1997 +0100
     3.3 @@ -16,5 +16,22 @@
     3.4  \  sq(x1*y3 - x2*y4 + x3*y1 + x4*y2)  + \
     3.5  \  sq(x1*y4 + x2*y3 - x3*y2 + x4*y1)";
     3.6  (*Takes up to three minutes...*)
     3.7 -by (cring_simp 1);
     3.8 +by (cring_tac 1);
     3.9  qed "Lagrange_lemma";
    3.10 +
    3.11 +(* A challenge by John Harrison.
    3.12 +   Takes forever because of the naive bottom-up strategy of the rewriter.
    3.13 +
    3.14 +goalw Lagrange.thy [Lagrange.sq_def] "!!p1::'a::cring.\
    3.15 +\ (sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * \
    3.16 +\ (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2) \
    3.17 +\  = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) + \
    3.18 +\    sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) +\
    3.19 +\    sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) +\
    3.20 +\    sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) +\
    3.21 +\    sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) +\
    3.22 +\    sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +\
    3.23 +\    sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +\
    3.24 +\    sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)";
    3.25 +
    3.26 +*)
     4.1 --- a/src/HOL/Integ/Ring.ML	Sat Nov 15 13:10:52 1997 +0100
     4.2 +++ b/src/HOL/Integ/Ring.ML	Sat Nov 15 18:41:06 1997 +0100
     4.3 @@ -7,23 +7,13 @@
     4.4  and defines cring_simpl, a simplification tactic for commutative rings.
     4.5  *)
     4.6  
     4.7 -open Ring;
     4.8 -
     4.9 -(***
    4.10 -It is not clear if all thsese rules, esp. distributivity, should be part
    4.11 -of the default simpset. At the moment they are because they are used in the
    4.12 -decision procedure.
    4.13 -***)   
    4.14 -Addsimps [times_assoc,times_commute,distribL,distribR];
    4.15 -
    4.16  goal Ring.thy "!!x::'a::cring. x*(y*z)=y*(x*z)";
    4.17  by (rtac trans 1);
    4.18  by (rtac times_commute 1);
    4.19  by (rtac trans 1);
    4.20  by (rtac times_assoc 1);
    4.21 -by (Simp_tac 1);
    4.22 +by (simp_tac (HOL_basic_ss addsimps [times_commute]) 1);
    4.23  qed "times_commuteL";
    4.24 -Addsimps [times_commuteL];
    4.25  
    4.26  val times_cong = read_instantiate [("f1","op *")] (arg_cong RS cong);
    4.27  
    4.28 @@ -119,30 +109,31 @@
    4.29  by (rtac (zeroR RS sym) 1);
    4.30  qed "mult_invR";
    4.31  
    4.32 -Addsimps[mult_invL,mult_invR];
    4.33 -
    4.34 -
    4.35 -goal Ring.thy "!!x::'a::ring. x*(y-z) = x*y - x*z";
    4.36 -by (stac minus_inv 1);
    4.37 -by (rtac sym 1);
    4.38 -by (stac minus_inv 1);
    4.39 -by (Simp_tac 1);
    4.40 +goal Ring.thy "x*(y-z) = (x*y - x*z::'a::ring)";
    4.41 +by(mk_group1_tac 1);
    4.42 +by(simp_tac (HOL_basic_ss addsimps [distribL,mult_invR]) 1);
    4.43  qed "minus_distribL";
    4.44  
    4.45 -goal Ring.thy "!!x::'a::ring. (x-y)*z = x*z - y*z";
    4.46 -by (stac minus_inv 1);
    4.47 -by (rtac sym 1);
    4.48 -by (stac minus_inv 1);
    4.49 -by (Simp_tac 1);
    4.50 +goal Ring.thy "(x-y)*z = (x*z - y*z::'a::ring)";
    4.51 +by(mk_group1_tac 1);
    4.52 +by(simp_tac (HOL_basic_ss addsimps [distribR,mult_invL]) 1);
    4.53  qed "minus_distribR";
    4.54  
    4.55 -Addsimps [minus_distribL,minus_distribR];
    4.56 +val cring_simps = [times_assoc,times_commute,times_commuteL,
    4.57 +                   distribL,distribR,minus_distribL,minus_distribR]
    4.58 +                  @ agroup2_simps;
    4.59 +
    4.60 +val cring_tac =
    4.61 +  let val ss = HOL_basic_ss addsimps cring_simps
    4.62 +  in simp_tac ss end;
    4.63 +
    4.64  
    4.65  (*** The order [minus_plusL3,minus_plusL2] is important because minus_plusL3
    4.66 -     MUST be tried first ***)
    4.67 +     MUST be tried first
    4.68  val cring_simp =
    4.69    let val phase1 = simpset() addsimps
    4.70                     [plus_minusL,minus_plusR,minus_minusR,plus_minusR]
    4.71        val phase2 = HOL_ss addsimps [minus_plusL3,minus_plusL2,
    4.72                                      zeroL,zeroR,mult_zeroL,mult_zeroR]
    4.73    in simp_tac phase1 THEN' simp_tac phase2 end;
    4.74 +***)