# HG changeset patch
# User nipkow
# Date 1082140396 -7200
# Node ID 985eb6708207b1fb7eea41fc7a8788bd97a3bea1
# Parent  e06ded775eca7e838ed742e08a293a294f4c9f40
Moved ring stuff from ex into Ring_and_Field.

diff -r e06ded775eca -r 985eb6708207 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Apr 16 19:04:17 2004 +0200
+++ b/src/HOL/IsaMakefile	Fri Apr 16 20:33:16 2004 +0200
@@ -584,16 +584,16 @@
 
 $(LOG)/HOL-ex.gz: $(OUT)/HOL ex/Antiquote.thy \
   ex/BT.thy ex/BinEx.thy ex/Exceptions.thy \
-  ex/Group.ML ex/Group.thy ex/Higher_Order_Logic.thy \
-  ex/Hilbert_Classical.thy ex/InSort.thy ex/IntRing.ML \
+  ex/Higher_Order_Logic.thy \
+  ex/Hilbert_Classical.thy ex/InSort.thy \
   ex/InductiveInvariant.thy  ex/InductiveInvariant_examples.thy\
-  ex/IntRing.thy ex/Intuitionistic.thy \
-  ex/Lagrange.ML ex/Lagrange.thy ex/Locales.thy ex/MergeSort.thy \
+  ex/Intuitionistic.thy \
+  ex/Lagrange.thy ex/Locales.thy ex/MergeSort.thy \
   ex/MT.ML ex/MT.thy ex/MonoidGroup.thy ex/Multiquote.thy \
   ex/NatSum.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy ex/Puzzle.thy \
   ex/Qsort.thy ex/Quickcheck_Examples.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
   ex/Refute_Examples.thy \
-  ex/Ring.ML ex/Ring.thy ex/StringEx.thy ex/SVC_Oracle.ML ex/SVC_Oracle.thy \
+  ex/StringEx.thy ex/SVC_Oracle.ML ex/SVC_Oracle.thy \
   ex/Tarski.thy ex/Tuple.thy ex/Classical.thy \
   ex/mesontest2.ML ex/mesontest2.thy ex/set.thy ex/svc_funcs.ML \
   ex/svc_test.ML ex/svc_test.thy ex/document/root.bib ex/document/root.tex
diff -r e06ded775eca -r 985eb6708207 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Fri Apr 16 19:04:17 2004 +0200
+++ b/src/HOL/Ring_and_Field.thy	Fri Apr 16 20:33:16 2004 +0200
@@ -19,10 +19,7 @@
   zero [simp]: "0 + x = x"
 
 lemma plus_ac0_left_commute: "x + (y+z) = y + ((x+z)::'a::plus_ac0)"
-apply (rule plus_ac0.commute [THEN trans])
-apply (rule plus_ac0.assoc [THEN trans])
-apply (rule plus_ac0.commute [THEN arg_cong])
-done
+by(rule mk_left_commute[of "op +",OF plus_ac0.assoc plus_ac0.commute])
 
 lemma plus_ac0_zero_right [simp]: "x + 0 = (x ::'a::plus_ac0)"
 apply (rule plus_ac0.commute [THEN trans])
@@ -39,15 +36,7 @@
 
 theorem times_ac1_left_commute: "(x::'a::times_ac1) * ((y::'a) * z) =
   y * (x * z)"
-proof -
-  have "(x::'a::times_ac1) * (y * z) = (x * y) * z"
-    by (rule times_ac1.assoc [THEN sym])
-  also have "x * y = y * x"
-    by (rule times_ac1.commute)
-  also have "(y * x) * z = y * (x * z)"
-    by (rule times_ac1.assoc)
-  finally show ?thesis .
-qed
+by(rule mk_left_commute[of "op *",OF times_ac1.assoc times_ac1.commute])
 
 theorem times_ac1_one_right [simp]: "(x::'a::times_ac1) * 1 = x"
 proof -
@@ -525,6 +514,13 @@
        diff_less_eq less_diff_eq diff_le_eq le_diff_eq
        diff_eq_eq eq_diff_eq
 
+text{*This list of rewrites decides ring equalities by ordered rewriting.*}
+lemmas ring_eq_simps =
+  times_ac1.assoc times_ac1.commute times_ac1_left_commute
+  left_distrib right_distrib left_diff_distrib right_diff_distrib
+  plus_ac0.assoc plus_ac0.commute plus_ac0_left_commute
+  add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
+  diff_eq_eq eq_diff_eq
 
 subsection{*Lemmas for the @{text cancel_numerals} simproc*}
 
diff -r e06ded775eca -r 985eb6708207 src/HOL/ex/Group.ML
--- a/src/HOL/ex/Group.ML	Fri Apr 16 19:04:17 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,222 +0,0 @@
-(*  Title:      HOL/Integ/Group.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1997 TU Muenchen
-*)
-
-(*** Groups ***)
-
-(* Derives the well-known convergent set of equations for groups
-   based on the unary inverse 0-x.
-*)
-
-Goal "!!x::'a::add_group. (0 - x) + (x + y) = y";
-by (rtac trans 1);
-by (rtac (plus_assoc RS sym) 1);
-by (stac left_inv 1);
-by (rtac zeroL 1);
-qed "left_inv2";
-
-Goal "!!x::'a::add_group. (0 - (0 - x)) = x";
-by (rtac trans 1);
-by (res_inst_tac [("x","0 - x")] left_inv2 2);
-by (stac left_inv 1);
-by (rtac (zeroR RS sym) 1);
-qed "inv_inv";
-
-Goal "0 - 0 = (0::'a::add_group)";
-by (rtac trans 1);
-by (rtac (zeroR RS sym) 1);
-by (rtac trans 1);
-by (res_inst_tac [("x","0")] left_inv2 2);
-by (simp_tac (simpset() addsimps [zeroR]) 1);
-qed "inv_zero";
-
-Goal "!!x::'a::add_group. x + (0 - x) = 0";
-by (rtac trans 1);
-by (res_inst_tac [("x","0-x")] left_inv 2);
-by (stac inv_inv 1);
-by (rtac refl 1);
-qed "right_inv";
-
-Goal "!!x::'a::add_group. x + ((0 - x) + y) = y";
-by (rtac trans 1);
-by (res_inst_tac [("x","0 - x")] left_inv2 2);
-by (stac inv_inv 1);
-by (rtac refl 1);
-qed "right_inv2";
-
-val plus_cong = read_instantiate [("f1","op +")] (arg_cong RS cong);
-
-Goal "!!x::'a::add_group. 0 - (x + y) = (0 - y) + (0 - x)";
-by (rtac trans 1);
- by (rtac zeroR 2);
-by (rtac trans 1);
- by (rtac plus_cong 2);
-  by (rtac refl 2);
- by (res_inst_tac [("x","x+y")] right_inv 2);
-by (rtac trans 1);
- by (rtac plus_assoc 2);
-by (rtac trans 1);
- by (rtac plus_cong 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 0 - 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 + (0 - y) does
-   not terminate. Hence we have a special tactic for converting all
-   occurrences of x - y into x + (0 - 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 "x - x = (0::'a::add_group)";
-by (mk_group1_tac 1);
-by (group1_tac 1);
-qed "minus_self_zero";
-
-Goal "x - 0 = (x::'a::add_group)";
-by (mk_group1_tac 1);
-by (group1_tac 1);
-qed "minus_zero";
-
-(*** Abelian Groups ***)
-
-Goal "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 (simpset() addsimps [plus_commute]) 1);
-qed "plus_commuteL";
-
-(* Convergent TRS for Abelian groups with unary inverse 0 - 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 "x + (y - z) = (x + y) - (z::'a::add_group)";
-by (mk_group1_tac 1);
-by (group1_tac 1);
-qed "plus_minusR";
-
-Goal "(x - y) + z = (x + z) - (y::'a::add_agroup)";
-by (mk_group1_tac 1);
-by (agroup1_tac 1);
-qed "plus_minusL";
-
-Goal "(x - y) - z = x - (y + (z::'a::add_agroup))";
-by (mk_group1_tac 1);
-by (agroup1_tac 1);
-qed "minus_minusL";
-
-Goal "x - (y - z) = (x + z) - (y::'a::add_agroup)";
-by (mk_group1_tac 1);
-by (agroup1_tac 1);
-qed "minus_minusR";
-
-Goal "!!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 "!!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 "!!x::'a::add_agroup. (x+(0-y))+z = (x+z)+(0-y)";
-by (Simp_tac 1);
-val lemma = result();
-bind_thm("plus_minusL",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
-
-Goal "!!x::'a::add_agroup. x+(0-(y+z)) = (x+(0-y))+(0-z)";
-by (Simp_tac 1);
-val lemma = result();
-bind_thm("minus_plusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
-
-Goal "!!x::'a::add_agroup. x+(0-(y+(0-z))) = (x+z)+(0-y)";
-by (Simp_tac 1);
-val lemma = result();
-bind_thm("minus_minusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
-
-Goal "!!x::'a::add_agroup. x+(y+(0-z)) = (x+y)+(0-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 "!!x::'a::add_agroup. (x+y)+(0-z) = x+(y+(0-z))";
-by (Simp_tac 1);
-val lemma = result();
-bind_thm("minus_plusL2",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
-
-Goal "!!x::'a::add_agroup. (x+y)+(0-x) = y";
-by (rtac (plus_assoc RS trans) 1);
-by (rtac trans 1);
- by (rtac plus_cong 1);
-  by (rtac refl 1);
- by (rtac right_inv2 2);
-by (rtac plus_commute 1);
-val lemma = result();
-bind_thm("minus_plusL3",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
-
-*)
diff -r e06ded775eca -r 985eb6708207 src/HOL/ex/Group.thy
--- a/src/HOL/ex/Group.thy	Fri Apr 16 19:04:17 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-(*  Title:      HOL/Integ/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 = Main +
-
-(* additive semigroups *)
-
-axclass  add_semigroup < plus
-  plus_assoc   "(x + y) + z = x + (y + z)"
-
-
-(* additive monoids *)
-
-axclass  add_monoid < add_semigroup, zero
-  zeroL    "0 + x = x"
-  zeroR    "x + 0 = x"
-
-(* additive groups *)
-(*
-The inverse is the binary `-'. Groups with unary and binary inverse are
-interdefinable: x-y := x+(0-y) and -x := 0-x. The law left_inv is
-simply the translation of (-x)+x = 0. This characterizes groups already,
-provided we only allow (0-x). Law minus_inv `defines' the general x-y in
-terms of the specific 0-y.
-*)
-axclass  add_group < add_monoid, minus
-  left_inv  "(0-x)+x = 0"
-  minus_inv "x-y = x + (0-y)"
-
-(* additive abelian groups *)
-
-axclass  add_agroup < add_group
-  plus_commute  "x + y = y + x"
-
-end
diff -r e06ded775eca -r 985eb6708207 src/HOL/ex/IntRing.ML
--- a/src/HOL/ex/IntRing.ML	Fri Apr 16 19:04:17 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(*  Title:      HOL/Integ/IntRing.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow and Markus Wenzel
-    Copyright   1996 TU Muenchen
-
-The instantiation of Lagrange's lemma for int.
-*)
-
-Goal "!!i1::int. \
-\  (sq i1 + sq i2 + sq i3 + sq i4) * (sq j1 + sq j2 + sq j3 + sq j4) = \
-\  sq(i1*j1 - i2*j2 - i3*j3 - i4*j4)  + \
-\  sq(i1*j2 + i2*j1 + i3*j4 - i4*j3)  + \
-\  sq(i1*j3 - i2*j4 + i3*j1 + i4*j2)  + \
-\  sq(i1*j4 + i2*j3 - i3*j2 + i4*j1)";
-by (rtac Lagrange_lemma 1);
-qed "Lagrange_lemma_int";
diff -r e06ded775eca -r 985eb6708207 src/HOL/ex/IntRing.thy
--- a/src/HOL/ex/IntRing.thy	Fri Apr 16 19:04:17 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(*  Title:      HOL/Integ/IntRing.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow and Markus Wenzel
-    Copyright   1996 TU Muenchen
-
-The integers form a commutative ring.
-With an application of Lagrange's lemma.
-*)
-
-IntRing = Ring + Lagrange +
-
-instance int :: add_semigroup (zadd_assoc)
-instance int :: add_monoid (zadd_0,zadd_0_right)
-instance int :: add_group {|Auto_tac|}
-instance int :: add_agroup (zadd_commute)
-instance int :: ring (zmult_assoc,zadd_zmult_distrib2,zadd_zmult_distrib)
-instance int :: cring (zmult_commute)
-
-end
diff -r e06ded775eca -r 985eb6708207 src/HOL/ex/Lagrange.ML
--- a/src/HOL/ex/Lagrange.ML	Fri Apr 16 19:04:17 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-(*  Title:      HOL/Integ/Lagrange.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1996 TU Muenchen
-
-
-The following lemma essentially shows that every natural number is the sum of
-four squares, provided all prime numbers are.  However, this is an abstract
-theorem about commutative rings.  It has, a priori, nothing to do with nat.*)
-
-Goalw [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_tac 1);  (*once a slow step, but now (2001) just three seconds!*)
-qed "Lagrange_lemma";
-
-
-(* A challenge by John Harrison.
-   Takes forever because of the naive bottom-up strategy of the rewriter.
-
-Goalw [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)";
-by (cring_tac 1);
-*)
diff -r e06ded775eca -r 985eb6708207 src/HOL/ex/Lagrange.thy
--- a/src/HOL/ex/Lagrange.thy	Fri Apr 16 19:04:17 2004 +0200
+++ b/src/HOL/ex/Lagrange.thy	Fri Apr 16 20:33:16 2004 +0200
@@ -10,9 +10,42 @@
 
 The enterprising reader might consider proving all of Lagrange's theorem.
 *)
-Lagrange = Ring +
 
-constdefs sq :: 'a::times => 'a
+theory Lagrange = Main:
+
+constdefs sq :: "'a::times => 'a"
          "sq x == x*x"
 
+(* The following lemma essentially shows that every natural number is the sum
+of four squares, provided all prime numbers are.  However, this is an
+abstract theorem about commutative rings.  It has, a priori, nothing to do
+with nat.*)
+
+(*once a slow step, but now (2001) just three seconds!*)
+lemma Lagrange_lemma:
+ "!!x1::'a::ring.
+  (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(simp add: sq_def ring_eq_simps)
+
+
+(* A challenge by John Harrison. Takes about 4 mins on a 3GHz machine.
+
+lemma "!!p1::'a::ring.
+ (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)"
+by(simp add: sq_def ring_eq_simps)
+*)
+
 end
diff -r e06ded775eca -r 985eb6708207 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Fri Apr 16 19:04:17 2004 +0200
+++ b/src/HOL/ex/ROOT.ML	Fri Apr 16 20:33:16 2004 +0200
@@ -33,7 +33,7 @@
 no_document use_thy "List_Prefix";
 time_use_thy "Exceptions";
 
-time_use_thy "IntRing";
+time_use_thy "Lagrange";
 
 time_use_thy "set";
 time_use_thy "MT";
diff -r e06ded775eca -r 985eb6708207 src/HOL/ex/Ring.ML
--- a/src/HOL/ex/Ring.ML	Fri Apr 16 19:04:17 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,139 +0,0 @@
-(*  Title:      HOL/Integ/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.
-*)
-
-Goal "!!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 (HOL_basic_ss addsimps [times_commute]) 1);
-qed "times_commuteL";
-
-val times_cong = read_instantiate [("f1","op *")] (arg_cong RS cong);
-
-Goal "!!x::'a::ring. 0*x = 0";
-by (rtac trans 1);
- by (rtac right_inv 2);
-by (rtac trans 1);
- by (rtac plus_cong 2);
-  by (rtac refl 3);
- by (rtac trans 2);
-  by (rtac times_cong 3);
-   by (rtac zeroL 3);
-  by (rtac refl 3);
- by (rtac (distribR RS sym) 2);
-by (rtac trans 1);
- by (rtac (plus_assoc RS sym) 2);
-by (rtac trans 1);
- by (rtac plus_cong 2);
-  by (rtac refl 2);
- by (rtac (right_inv RS sym) 2);
-by (rtac (zeroR RS sym) 1);
-qed "mult_zeroL";
-
-Goal "!!x::'a::ring. x*0 = 0";
-by (rtac trans 1);
- by (rtac right_inv 2);
-by (rtac trans 1);
- by (rtac plus_cong 2);
-  by (rtac refl 3);
- by (rtac trans 2);
-  by (rtac times_cong 3);
-   by (rtac zeroL 4);
-  by (rtac refl 3);
- by (rtac (distribL RS sym) 2);
-by (rtac trans 1);
- by (rtac (plus_assoc RS sym) 2);
-by (rtac trans 1);
- by (rtac plus_cong 2);
-  by (rtac refl 2);
- by (rtac (right_inv RS sym) 2);
-by (rtac (zeroR RS sym) 1);
-qed "mult_zeroR";
-
-Goal "!!x::'a::ring. (0-x)*y = 0-(x*y)";
-by (rtac trans 1);
- by (rtac zeroL 2);
-by (rtac trans 1);
- by (rtac plus_cong 2);
-  by (rtac refl 3);
- by (rtac mult_zeroL 2);
-by (rtac trans 1);
- by (rtac plus_cong 2);
-  by (rtac refl 3);
- by (rtac times_cong 2);
-  by (rtac left_inv 2);
- by (rtac refl 2);
-by (rtac trans 1);
- by (rtac plus_cong 2);
-  by (rtac refl 3);
- by (rtac (distribR RS sym) 2);
-by (rtac trans 1);
- by (rtac (plus_assoc RS sym) 2);
-by (rtac trans 1);
- by (rtac plus_cong 2);
-  by (rtac refl 2);
- by (rtac (right_inv RS sym) 2);
-by (rtac (zeroR RS sym) 1);
-qed "mult_invL";
-
-Goal "!!x::'a::ring. x*(0-y) = 0-(x*y)";
-by (rtac trans 1);
- by (rtac zeroL 2);
-by (rtac trans 1);
- by (rtac plus_cong 2);
-  by (rtac refl 3);
- by (rtac mult_zeroR 2);
-by (rtac trans 1);
- by (rtac plus_cong 2);
-  by (rtac refl 3);
- by (rtac times_cong 2);
-  by (rtac refl 2);
- by (rtac left_inv 2);
-by (rtac trans 1);
- by (rtac plus_cong 2);
-  by (rtac refl 3);
- by (rtac (distribL RS sym) 2);
-by (rtac trans 1);
- by (rtac (plus_assoc RS sym) 2);
-by (rtac trans 1);
- by (rtac plus_cong 2);
-  by (rtac refl 2);
- by (rtac (right_inv RS sym) 2);
-by (rtac (zeroR RS sym) 1);
-qed "mult_invR";
-
-Goal "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 "(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";
-
-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
-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 e06ded775eca -r 985eb6708207 src/HOL/ex/Ring.thy
--- a/src/HOL/ex/Ring.thy	Fri Apr 16 19:04:17 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-(*  Title:      HOL/Integ/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