# HG changeset patch # User nipkow # Date 879615666 -3600 # Node ID eb5586526bc9a5f02575f5129e1895929cf943c8 # Parent 551684f275b974925b150e4e3d980fb0c4058381 Redesigned the decision procedures for (Abelian) groups and commutative rings. diff -r 551684f275b9 -r eb5586526bc9 src/HOL/Integ/Group.ML --- 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); +*) diff -r 551684f275b9 -r eb5586526bc9 src/HOL/Integ/Group.thy --- 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)" diff -r 551684f275b9 -r eb5586526bc9 src/HOL/Integ/Lagrange.ML --- 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)"; + +*) diff -r 551684f275b9 -r eb5586526bc9 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; +***)