# HG changeset patch
# User nipkow
# Date 849014897 -3600
# Node ID 4b43a8d046e5fd0f96465b064e7ab09f957193b0
# Parent  a3fb552f10e38cb0deaccff632446660146d2779
A bit of commutative ing theory, with a simplification tacxtic and an example.

diff -r a3fb552f10e3 -r 4b43a8d046e5 src/HOL/ex/Group.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Group.ML	Tue Nov 26 14:28:17 1996 +0100
@@ -0,0 +1,127 @@
+(*  Title:      HOL/ex/Group.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1996 TU Muenchen
+*)
+
+open Group;
+
+Addsimps [zeroL,zeroR,plus_assoc,plus_commute];
+
+goal Group.thy "!!x::'a::add_group. (zero-x)+(x+y) = y";
+br trans 1;
+br (plus_assoc RS sym) 1;
+by(stac left_inv 1);
+br zeroL 1;
+qed "left_inv2";
+
+goal Group.thy "!!x::'a::add_group. (zero-(zero-x)) = x";
+br trans 1;
+by(res_inst_tac [("x","zero-x")] left_inv2 2);
+by(stac left_inv 1);
+br (zeroR RS sym) 1;
+qed "inv_inv";
+
+goal Group.thy "zero-zero = (zero::'a::add_group)";
+br trans 1;
+br (zeroR RS sym) 1;
+br trans 1;
+by(res_inst_tac [("x","zero")] left_inv2 2);
+by(Simp_tac 1);
+qed "inv_zero";
+
+goal Group.thy "!!x::'a::add_group. x+(zero-x) = zero";
+br trans 1;
+by(res_inst_tac [("x","zero-x")] left_inv 2);
+by(stac inv_inv 1);
+br refl 1;
+qed "right_inv";
+
+goal Group.thy "!!x::'a::add_group. x+((zero-x)+y) = y";
+br trans 1;
+by(res_inst_tac [("x","zero-x")] left_inv2 2);
+by(stac inv_inv 1);
+br refl 1;
+qed "right_inv2";
+
+goal Group.thy "!!x::'a::add_group. x-x = zero";
+by(stac minus_inv 1);
+br 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);
+br 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)";
+br trans 1;
+ br zeroR 2;
+br trans 1;
+ br plus_cong 2;
+  br refl 2;
+ by(res_inst_tac [("x","x+y")] right_inv 2);
+br trans 1;
+ br plus_assoc 2;
+br trans 1;
+ br plus_cong 2;
+  by(simp_tac (!simpset addsimps [left_inv,left_inv2,right_inv,right_inv2]) 2);
+ br refl 2;
+br (zeroL RS sym) 1;
+qed "inv_plus";
+
+goal Group.thy "x+(y+z)=y+(x+z::'a::add_agroup)";
+br trans 1;
+br plus_commute 1;
+br trans 1;
+br plus_assoc 1;
+by(Simp_tac 1);
+qed "plus_commuteL";
+Addsimps [plus_commuteL];
+
+Addsimps [inv_inv,inv_plus];
+
+(* Phase 1 *)
+
+goal Group.thy "!!x::'a::add_agroup. (x+(zero-y))+z = (x+z)+(zero-y)";
+by(Simp_tac 1);
+val lemma = result();
+bind_thm("plus_minusL",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
+
+goal Group.thy "!!x::'a::add_agroup. x+(zero-(y+z)) = (x+(zero-y))+(zero-z)";
+by(Simp_tac 1);
+val lemma = result();
+bind_thm("minus_plusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
+
+goal Group.thy "!!x::'a::add_agroup. x+(zero-(y+(zero-z))) = (x+z)+(zero-y)";
+by(Simp_tac 1);
+val lemma = result();
+bind_thm("minus_minusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
+
+goal Group.thy "!!x::'a::add_agroup. x+(y+(zero-z)) = (x+y)+(zero-z)";
+by(Simp_tac 1);
+val lemma = result();
+bind_thm("plus_minusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
+
+(* Phase 2 *)
+
+goal Group.thy "!!x::'a::add_agroup. (x+y)+(zero-z) = x+(y+(zero-z))";
+by(Simp_tac 1);
+val lemma = result();
+bind_thm("minus_plusL2",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
+
+goal Group.thy "!!x::'a::add_agroup. (x+y)+(zero-x) = y";
+br (plus_assoc RS trans) 1;
+br trans 1;
+ br plus_cong 1;
+  br refl 1;
+ br right_inv2 2;
+br plus_commute 1;
+val lemma = result();
+bind_thm("minus_plusL3",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
+
diff -r a3fb552f10e3 -r 4b43a8d046e5 src/HOL/ex/Group.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Group.thy	Tue Nov 26 14:28:17 1996 +0100
@@ -0,0 +1,38 @@
+(*  Title:      HOL/ex/Group.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1996 TU Muenchen
+
+A little bit of group theory leading up to rings. Hence groups are additive.
+*)
+
+Group = Set +
+
+(* 0 already used in Nat *)
+axclass  zero < term
+consts   zero :: "'a::zero"
+
+(* additive semigroups *)
+
+axclass  add_semigroup < plus
+  plus_assoc   "(x + y) + z = x + (y + z)"
+
+
+(* additive monoids *)
+
+axclass  add_monoid < add_semigroup, zero
+  zeroL    "zero + x = x"
+  zeroR    "x + zero = x"
+
+(* additive groups *)
+
+axclass  add_group < add_monoid, minus
+  left_inv  "(zero-x)+x = zero"
+  minus_inv "x-y = x + (zero-y)"
+
+(* additive abelian groups *)
+
+axclass  add_agroup < add_group
+  plus_commute  "x + y = y + x"
+
+end
diff -r a3fb552f10e3 -r 4b43a8d046e5 src/HOL/ex/Lagrange.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Lagrange.ML	Tue Nov 26 14:28:17 1996 +0100
@@ -0,0 +1,18 @@
+(*  Title:      HOL/ex/Lagrange.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1996 TU Muenchen
+
+
+The following lemma schows that all composite natural numbers are sums of
+fours squares, provided all prime numbers are.
+*)
+
+goalw Lagrange.thy [Lagrange.sq_def] "!!x1::'a::cring. \
+\  (sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) = \
+\  sq(x1*y1 - x2*y2 - x3*y3 - x4*y4)  + \
+\  sq(x1*y2 + x2*y1 + x3*y4 - x4*y3)  + \
+\  sq(x1*y3 - x2*y4 + x3*y1 + x4*y2)  + \
+\  sq(x1*y4 + x2*y3 - x3*y2 + x4*y1)";
+by(cring_simp 1);
+qed "Lagrange_lemma";
diff -r a3fb552f10e3 -r 4b43a8d046e5 src/HOL/ex/Lagrange.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Lagrange.thy	Tue Nov 26 14:28:17 1996 +0100
@@ -0,0 +1,18 @@
+(*  Title:      HOL/ex/Lagrange.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1996 TU Muenchen
+
+
+This theory only contains a single thm, which is a lemma in Lagrange's proof
+that every natural number is the sum of 4 squares.  It's sole purpose is to
+demonstrate ordered rewriting for commutative rings.
+
+The enterprising reader might consider proving all of Lagrange's thm.
+*)
+Lagrange = Ring +
+
+constdefs sq :: 'a::times => 'a
+         "sq x == x*x"
+
+end
diff -r a3fb552f10e3 -r 4b43a8d046e5 src/HOL/ex/Ring.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Ring.ML	Tue Nov 26 14:28:17 1996 +0100
@@ -0,0 +1,148 @@
+(*  Title:      HOL/ex/Ring.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1996 TU Muenchen
+
+Derives a few equational consequences about rings
+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)";
+br trans 1;
+br times_commute 1;
+br trans 1;
+br times_assoc 1;
+by(Simp_tac 1);
+qed "times_commuteL";
+Addsimps [times_commuteL];
+
+val times_cong = read_instantiate [("f1","op *")] (arg_cong RS cong);
+
+goal Ring.thy "!!x::'a::ring. zero*x = zero";
+br trans 1;
+ br right_inv 2;
+br trans 1;
+ br plus_cong 2;
+  br refl 3;
+ br trans 2;
+  br times_cong 3;
+   br zeroL 3;
+  br refl 3;
+ br (distribR RS sym) 2;
+br trans 1;
+ br(plus_assoc RS sym) 2;
+br trans 1;
+ br plus_cong 2;
+  br refl 2;
+ br (right_inv RS sym) 2;
+br (zeroR RS sym) 1;
+qed "mult_zeroL";
+
+goal Ring.thy "!!x::'a::ring. x*zero = zero";
+br trans 1;
+ br right_inv 2;
+br trans 1;
+ br plus_cong 2;
+  br refl 3;
+ br trans 2;
+  br times_cong 3;
+   br zeroL 4;
+  br refl 3;
+ br (distribL RS sym) 2;
+br trans 1;
+ br(plus_assoc RS sym) 2;
+br trans 1;
+ br plus_cong 2;
+  br refl 2;
+ br (right_inv RS sym) 2;
+br (zeroR RS sym) 1;
+qed "mult_zeroR";
+
+goal Ring.thy "!!x::'a::ring. (zero-x)*y = zero-(x*y)";
+br trans 1;
+ br zeroL 2;
+br trans 1;
+ br plus_cong 2;
+  br refl 3;
+ br mult_zeroL 2;
+br trans 1;
+ br plus_cong 2;
+  br refl 3;
+ br times_cong 2;
+  br left_inv 2;
+ br refl 2;
+br trans 1;
+ br plus_cong 2;
+  br refl 3;
+ br (distribR RS sym) 2;
+br trans 1;
+ br(plus_assoc RS sym) 2;
+br trans 1;
+ br plus_cong 2;
+  br refl 2;
+ br (right_inv RS sym) 2;
+br (zeroR RS sym) 1;
+qed "mult_invL";
+
+goal Ring.thy "!!x::'a::ring. x*(zero-y) = zero-(x*y)";
+br trans 1;
+ br zeroL 2;
+br trans 1;
+ br plus_cong 2;
+  br refl 3;
+ br mult_zeroR 2;
+br trans 1;
+ br plus_cong 2;
+  br refl 3;
+ br times_cong 2;
+  br refl 2;
+ br left_inv 2;
+br trans 1;
+ br plus_cong 2;
+  br refl 3;
+ br (distribL RS sym) 2;
+br trans 1;
+ br(plus_assoc RS sym) 2;
+br trans 1;
+ br plus_cong 2;
+  br refl 2;
+ br (right_inv RS sym) 2;
+br (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);
+br sym 1;
+by(stac minus_inv 1);
+by(Simp_tac 1);
+qed "minus_distribL";
+
+goal Ring.thy "!!x::'a::ring. (x-y)*z = x*z - y*z";
+by(stac minus_inv 1);
+br sym 1;
+by(stac minus_inv 1);
+by(Simp_tac 1);
+qed "minus_distribR";
+
+Addsimps [minus_distribL,minus_distribR];
+
+(*** The order [minus_plusL3,minus_plusL2] is important because minus_plusL3
+     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;
diff -r a3fb552f10e3 -r 4b43a8d046e5 src/HOL/ex/Ring.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Ring.thy	Tue Nov 26 14:28:17 1996 +0100
@@ -0,0 +1,24 @@
+(*  Title:      HOL/ex/Ring.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1996 TU Muenchen
+
+Bits of rings.
+Main output: a simplification tactic for commutative rings.
+*)
+
+Ring = Group +
+
+(* Ring *)
+
+axclass  ring < add_agroup, times
+  times_assoc "(x*y)*z = x*(y*z)"
+  distribL    "x*(y+z) = x*y + x*z"
+  distribR    "(x+y)*z = x*z + y*z"
+
+(* Commutative ring *)
+
+axclass cring < ring
+  times_commute "x*y = y*x"
+
+end