Moved ring stuff from ex into Ring_and_Field.
--- 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
--- 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*}
--- 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);
-
-*)
--- 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
--- 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";
--- 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
--- 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);
-*)
--- 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
--- 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";
--- 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;
-***)
--- 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