# HG changeset patch
# User ballarin
# Date 1047313534 -3600
# Node ID 91c9ab25fecea8ce9151f3af415be912c19f9992
# Parent  89131afa9f011b7b4802242b7ce75abcdb2a26fb
First distributed version of Group and Ring theory.

diff -r 89131afa9f01 -r 91c9ab25fece src/HOL/Algebra/CRing.thy
--- a/src/HOL/Algebra/CRing.thy	Mon Mar 10 16:21:06 2003 +0100
+++ b/src/HOL/Algebra/CRing.thy	Mon Mar 10 17:25:34 2003 +0100
@@ -7,7 +7,8 @@
 
 header {* The algebraic hierarchy of rings as axiomatic classes *}
 
-theory Ring = Group
+theory CRing = Group
+files ("ringsimp.ML"):
 
 section {* The Algebraic Hierarchy of Rings *}
 
@@ -17,49 +18,18 @@
   zero :: 'a ("\<zero>\<index>")
   add :: "['a, 'a] => 'a" (infixl "\<oplus>\<index>" 65)
   a_inv :: "'a => 'a" ("\<ominus>\<index> _" [81] 80)
+  minus :: "['a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
 
 locale cring = abelian_monoid R +
   assumes a_abelian_group: "abelian_group (| carrier = carrier R,
       mult = add R, one = zero R, m_inv = a_inv R |)"
+    and minus_def: "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y = x \<oplus> \<ominus> y"
     and m_inv_def: "[| EX y. y \<in> carrier R & x \<otimes> y = \<one>; x \<in> carrier R |]
       ==> inv x = (THE y. y \<in> carrier R & x \<otimes> y = \<one>)"
     and l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
       ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
 
-ML {*
-  thm "cring.l_distr"
-*}
-
 (*
-locale cring = struct R +
-  assumes a_group: "abelian_group (| carrier = carrier R,
-      mult = add R, one = zero R, m_inv = a_inv R |)"
-    and m_monoid: "abelian_monoid (| carrier = carrier R - {zero R},
-      mult = mult R, one = one R |)"
-    and l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
-      ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
-
-locale field = struct R +
-  assumes a_group: "abelian_group (| carrier = carrier R,
-      mult = add R, one = zero R, m_inv = a_inv R |)"
-    and m_group: "monoid (| carrier = carrier R - {zero R},
-      mult = mult R, one = one R |)"
-    and l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
-      ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
-*)
-(*
-  a_assoc:      "(a + b) + c = a + (b + c)"
-  l_zero:       "0 + a = a"
-  l_neg:        "(-a) + a = 0"
-  a_comm:       "a + b = b + a"
-
-  m_assoc:      "(a * b) * c = a * (b * c)"
-  l_one:        "1 * a = a"
-
-  l_distr:      "(a + b) * c = a * c + b * c"
-
-  m_comm:       "a * b = b * a"
-
   -- {* Definition of derived operations *}
 
   minus_def:    "a - b = a + (-b)"
@@ -108,171 +78,154 @@
      mult = add R, one = zero R, m_inv = a_inv R |)"
   by (simp add: abelian_group_def)
 
-lemma (in cring) a_assoc:
-  "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
-  ==> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
-  using semigroup.m_assoc [OF a_semigroup]
-  by simp
+lemmas (in cring) a_closed [intro, simp] =
+  magma.m_closed [OF a_magma, simplified]
+
+lemmas (in cring) zero_closed [intro, simp] = 
+  l_one.one_closed [OF a_l_one, simplified]
+
+lemmas (in cring) a_inv_closed [intro, simp] =
+  group.inv_closed [OF a_group, simplified]
+
+lemma (in cring) minus_closed [intro, simp]:
+  "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y \<in> carrier R"
+  by (simp add: minus_def)
+
+lemmas (in cring) a_l_cancel [simp] = group.l_cancel [OF a_group, simplified]
 
-lemma (in cring) l_zero:
-  "x \<in> carrier R ==> \<zero> \<oplus> x = x"
-  using l_one.l_one [OF a_l_one]
+lemmas (in cring) a_r_cancel [simp] = group.r_cancel [OF a_group, simplified]
+
+lemmas (in cring) a_assoc = semigroup.m_assoc [OF a_semigroup, simplified]
+
+lemmas (in cring) l_zero [simp] = l_one.l_one [OF a_l_one, simplified]
+
+lemmas (in cring) l_neg = group.l_inv [OF a_group, simplified]
+
+lemmas (in cring) a_comm = abelian_semigroup.m_comm [OF a_abelian_semigroup,
+  simplified]
+
+lemmas (in cring) a_lcomm =
+  abelian_semigroup.m_lcomm [OF a_abelian_semigroup, simplified]
+
+lemma (in cring) r_zero [simp]:
+  "x \<in> carrier R ==> x \<oplus> \<zero> = x"
+  using group.r_one [OF a_group]
   by simp
 
-lemma (in cring) l_neg:
-  "x \<in> carrier R ==> (\<ominus> x) \<oplus> x = \<zero>"
-  using group.l_inv [OF a_group]
+lemma (in cring) r_neg:
+  "x \<in> carrier R ==> x \<oplus> (\<ominus> x) = \<zero>"
+  using group.r_inv [OF a_group]
+  by simp
+
+lemmas (in cring) minus_zero [simp] = group.inv_one [OF a_group, simplified]
+
+lemma (in cring) minus_minus [simp]:
+  "x \<in> carrier R ==> \<ominus> (\<ominus> x) = x"
+  using group.inv_inv [OF a_group, simplified]
   by simp
 
-lemma (in cring) a_comm:
-  "[| x \<in> carrier R; y \<in> carrier R |]
-  ==> x \<oplus> y = y \<oplus> x"
-  using abelian_semigroup.m_comm [OF a_abelian_semigroup]
+lemma (in cring) minus_add:
+  "[| x \<in> carrier R; y \<in> carrier R |] ==> \<ominus> (x \<oplus> y) = \<ominus> x \<oplus> \<ominus> y"
+  using abelian_group.inv_mult [OF a_abelian_group]
   by simp
 
+lemmas (in cring) a_ac = a_assoc a_comm a_lcomm
 
+subsection {* Normaliser for Commutative Rings *}
 
-
+lemma (in cring) r_neg2:
+  "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<oplus> (\<ominus> x \<oplus> y) = y"
+proof -
+  assume G: "x \<in> carrier R" "y \<in> carrier R"
+  then have "(x \<oplus> \<ominus> x) \<oplus> y = y" by (simp only: r_neg l_zero)
+  with G show ?thesis by (simp add: a_ac)
 qed
 
-  l_zero:       "0 + a = a"
-  l_neg:        "(-a) + a = 0"
-  a_comm:       "a + b = b + a"
-
-  m_assoc:      "(a * b) * c = a * (b * c)"
-  l_one:        "1 * a = a"
-
-  l_distr:      "(a + b) * c = a * c + b * c"
-
-  m_comm:       "a * b = b * a"
-text {* Normaliser for Commutative Rings *}
-
-use "order.ML"
-
-method_setup ring =
-  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (full_simp_tac ring_ss)) *}
-  {* computes distributive normal form in rings *}
-
-subsection {* Rings and the summation operator *}
-
-(* Basic facts --- move to HOL!!! *)
-
-lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::plus_ac0)"
-by simp
-
-lemma natsum_Suc [simp]:
-  "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::plus_ac0)"
-by (simp add: atMost_Suc)
-
-lemma natsum_Suc2:
-  "setsum f {..Suc n} = (setsum (%i. f (Suc i)) {..n} + f 0::'a::plus_ac0)"
-proof (induct n)
-  case 0 show ?case by simp
-next
-  case Suc thus ?case by (simp add: assoc) 
+lemma (in cring) r_neg1:
+  "[| x \<in> carrier R; y \<in> carrier R |] ==> \<ominus> x \<oplus> (x \<oplus> y) = y"
+proof -
+  assume G: "x \<in> carrier R" "y \<in> carrier R"
+  then have "(\<ominus> x \<oplus> x) \<oplus> y = y" by (simp only: l_neg l_zero)
+  with G show ?thesis by (simp add: a_ac)
 qed
 
-lemma natsum_cong [cong]:
-  "!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::plus_ac0) |] ==>
-        setsum f {..j} = setsum g {..k}"
-by (induct j) auto
-
-lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::plus_ac0)"
-by (induct n) simp_all
-
-lemma natsum_add [simp]:
-  "!!f::nat=>'a::plus_ac0.
-   setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}"
-by (induct n) (simp_all add: plus_ac0)
-
-(* Facts specific to rings *)
-
-instance ring < plus_ac0
-proof
-  fix x y z
-  show "(x::'a::ring) + y = y + x" by (rule a_comm)
-  show "((x::'a::ring) + y) + z = x + (y + z)" by (rule a_assoc)
-  show "0 + (x::'a::ring) = x" by (rule l_zero)
+lemma (in cring) r_distr:
+  "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
+  ==> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
+proof -
+  assume G: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
+  then have "z \<otimes> (x \<oplus> y) = (x \<oplus> y) \<otimes> z" by (simp add: m_comm)
+  also from G have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
+  also from G have "... = z \<otimes> x \<oplus> z \<otimes> y" by (simp add: m_comm)
+  finally show ?thesis .
 qed
 
-ML {*
-  local
-    val lhss = 
-        [read_cterm (sign_of (the_context ()))
-                    ("?t + ?u::'a::ring", TVar (("'z", 0), [])),
-	 read_cterm (sign_of (the_context ()))
-                    ("?t - ?u::'a::ring", TVar (("'z", 0), [])),
-	 read_cterm (sign_of (the_context ()))
-                    ("?t * ?u::'a::ring", TVar (("'z", 0), [])),
-	 read_cterm (sign_of (the_context ()))
-                    ("- ?t::'a::ring", TVar (("'z", 0), []))
-	];
-    fun proc sg _ t = 
-      let val rew = Tactic.prove sg [] []
-            (HOLogic.mk_Trueprop
-              (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t))))
-                (fn _ => simp_tac ring_ss 1)
-            |> mk_meta_eq;
-          val (t', u) = Logic.dest_equals (Thm.prop_of rew);
-      in if t' aconv u 
-        then None
-        else Some rew 
-    end;
-  in
-    val ring_simproc = mk_simproc "ring" lhss proc;
-  end;
+text {* 
+  The following proofs are from Jacobson, Basic Algebra I, pp.~88--89
 *}
 
-ML_setup {* Addsimprocs [ring_simproc] *}
-
-lemma natsum_ldistr:
-  "!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}"
-by (induct n) simp_all
-
-lemma natsum_rdistr:
-  "!!a::'a::ring. a * setsum f {..n::nat} = setsum (%i. a * f i) {..n}"
-by (induct n) simp_all
-
-subsection {* Integral Domains *}
+lemma (in cring) l_null [simp]:
+  "x \<in> carrier R ==> \<zero> \<otimes> x = \<zero>"
+proof -
+  assume R: "x \<in> carrier R"
+  then have "\<zero> \<otimes> x \<oplus> \<zero> \<otimes> x = (\<zero> \<oplus> \<zero>) \<otimes> x"
+    by (simp add: l_distr del: l_zero r_zero)
+  also from R have "... = \<zero> \<otimes> x \<oplus> \<zero>" by simp
+  finally have "\<zero> \<otimes> x \<oplus> \<zero> \<otimes> x = \<zero> \<otimes> x \<oplus> \<zero>" .
+  with R show ?thesis by (simp del: r_zero)
+qed
 
-declare one_not_zero [simp]
-
-lemma zero_not_one [simp]:
-  "0 ~= (1::'a::domain)" 
-by (rule not_sym) simp
+lemma (in cring) r_null [simp]:
+  "x \<in> carrier R ==> x \<otimes> \<zero> = \<zero>"
+proof -
+  assume R: "x \<in> carrier R"
+  then have "x \<otimes> \<zero> = \<zero> \<otimes> x" by (simp add: ac)
+  also from R have "... = \<zero>" by simp
+  finally show ?thesis .
+qed
 
-lemma integral_iff: (* not by default a simp rule! *)
-  "(a * b = (0::'a::domain)) = (a = 0 | b = 0)"
-proof
-  assume "a * b = 0" then show "a = 0 | b = 0" by (simp add: integral)
-next
-  assume "a = 0 | b = 0" then show "a * b = 0" by auto
+lemma (in cring) l_minus:
+  "[| x \<in> carrier R; y \<in> carrier R |] ==> \<ominus> x \<otimes> y = \<ominus> (x \<otimes> y)"
+proof -
+  assume R: "x \<in> carrier R" "y \<in> carrier R"
+  then have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y = (\<ominus> x \<oplus> x) \<otimes> y" by (simp add: l_distr)
+  also from R have "... = \<zero>" by (simp add: l_neg l_null)
+  finally have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y = \<zero>" .
+  with R have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y \<oplus> \<ominus> (x \<otimes> y) = \<zero> \<oplus> \<ominus> (x \<otimes> y)" by simp
+  with R show ?thesis by (simp add: a_assoc r_neg )
 qed
 
-(*
-lemma "(a::'a::ring) - (a - b) = b" apply simp
- simproc seems to fail on this example (fixed with new term order)
-*)
-(*
-lemma bug: "(b::'a::ring) - (b - a) = a" by simp
-   simproc for rings cannot prove "(a::'a::ring) - (a - b) = b" 
-*)
-lemma m_lcancel:
-  assumes prem: "(a::'a::domain) ~= 0" shows conc: "(a * b = a * c) = (b = c)"
-proof
-  assume eq: "a * b = a * c"
-  then have "a * (b - c) = 0" by simp
-  then have "a = 0 | (b - c) = 0" by (simp only: integral_iff)
-  with prem have "b - c = 0" by auto 
-  then have "b = b - (b - c)" by simp 
-  also have "b - (b - c) = c" by simp
-  finally show "b = c" .
-next
-  assume "b = c" then show "a * b = a * c" by simp
+lemma (in cring) r_minus:
+  "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<otimes> \<ominus> y = \<ominus> (x \<otimes> y)"
+proof -
+  assume R: "x \<in> carrier R" "y \<in> carrier R"
+  then have "x \<otimes> \<ominus> y = \<ominus> y \<otimes> x" by (simp add: ac)
+  also from R have "... = \<ominus> (y \<otimes> x)" by (simp add: l_minus)
+  also from R have "... = \<ominus> (x \<otimes> y)" by (simp add: ac)
+  finally show ?thesis .
 qed
 
-lemma m_rcancel:
-  "(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)"
-by (simp add: m_lcancel)
+lemmas (in cring) cring_simprules =
+  a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
+  a_assoc l_zero l_neg a_comm m_assoc l_one l_distr m_comm minus_def
+  r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero
+  a_lcomm m_lcomm r_distr l_null r_null l_minus r_minus
+
+use "ringsimp.ML"
+
+method_setup algebra =
+  {* Method.ctxt_args cring_normalise *}
+  {* computes distributive normal form in commutative rings (locales version) *}
+
+lemma
+  includes cring R + cring S
+  shows "[| a \<in> carrier R; b \<in> carrier R; c \<in> carrier S; d \<in> carrier S |] ==> 
+  a \<oplus> \<ominus> (a \<oplus> \<ominus> b) = b & c \<otimes>\<^sub>2 d = d \<otimes>\<^sub>2 c"
+  by algebra
+
+lemma
+  includes cring
+  shows "[| a \<in> carrier R; b \<in> carrier R |] ==> a \<ominus> (a \<ominus> b) = b"
+  by algebra
 
 end
diff -r 89131afa9f01 -r 91c9ab25fece src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Mon Mar 10 16:21:06 2003 +0100
+++ b/src/HOL/Algebra/Group.thy	Mon Mar 10 17:25:34 2003 +0100
@@ -20,14 +20,6 @@
 
 subsection {* Definitions *}
 
-(* The following may be unnecessary. *)
-text {*
-  We write groups additively.  This simplifies notation for rings.
-  All rings have an additive inverse, only fields have a
-  multiplicative one.  This definitions reduces the need for
-  qualifiers.
-*}
-
 record 'a semigroup =
   carrier :: "'a set"
   mult :: "['a, 'a] => 'a" (infixl "\<otimes>\<index>" 70)
@@ -104,6 +96,14 @@
   then show "y \<otimes> x = z \<otimes> x" by simp
 qed
 
+lemma (in group) inv_one [simp]:
+  "inv \<one> = \<one>"
+proof -
+  have "inv \<one> = \<one> \<otimes> (inv \<one>)" by simp
+  moreover have "... = \<one>" by (simp add: r_inv)
+  finally show ?thesis .
+qed
+
 lemma (in group) inv_inv [simp]:
   "x \<in> carrier G ==> inv (inv x) = x"
 proof -
@@ -112,7 +112,7 @@
   with x show ?thesis by simp
 qed
 
-lemma (in group) inv_mult:
+lemma (in group) inv_mult_group:
   "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv y \<otimes> inv x"
 proof -
   assume G: "x \<in> carrier G" "y \<in> carrier G"
@@ -245,21 +245,21 @@
 
 constdefs
   DirProdSemigroup ::
-    "[('a, 'c) semigroup_scheme, ('b, 'd) semigroup_scheme]
+    "[('a, 'm) semigroup_scheme, ('b, 'n) semigroup_scheme]
     => ('a \<times> 'b) semigroup"
     (infixr "\<times>\<^sub>s" 80)
   "G \<times>\<^sub>s H == (| carrier = carrier G \<times> carrier H,
     mult = (%(xg, xh) (yg, yh). (mult G xg yg, mult H xh yh)) |)"
 
   DirProdMonoid ::
-    "[('a, 'c) monoid_scheme, ('b, 'd) monoid_scheme] => ('a \<times> 'b) monoid"
+    "[('a, 'm) monoid_scheme, ('b, 'n) monoid_scheme] => ('a \<times> 'b) monoid"
     (infixr "\<times>\<^sub>m" 80)
   "G \<times>\<^sub>m H == (| carrier = carrier (G \<times>\<^sub>s H),
     mult = mult (G \<times>\<^sub>s H),
     one = (one G, one H) |)"
 
   DirProdGroup ::
-    "[('a, 'c) group_scheme, ('b, 'd) group_scheme] => ('a \<times> 'b) group"
+    "[('a, 'm) group_scheme, ('b, 'n) group_scheme] => ('a \<times> 'b) group"
     (infixr "\<times>\<^sub>g" 80)
   "G \<times>\<^sub>g H == (| carrier = carrier (G \<times>\<^sub>m H),
     mult = mult (G \<times>\<^sub>m H),
@@ -409,4 +409,8 @@
 
 locale abelian_group = abelian_monoid + group
 
+lemma (in abelian_group) inv_mult:
+  "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y"
+  by (simp add: ac inv_mult_group)
+
 end
diff -r 89131afa9f01 -r 91c9ab25fece src/HOL/Algebra/ringsimp.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/ringsimp.ML	Mon Mar 10 17:25:34 2003 +0100
@@ -0,0 +1,87 @@
+(*
+  Title:     Normalisation method for locale cring
+  Id:        $Id$
+  Author:    Clemens Ballarin
+  Copyright: TU Muenchen
+*)
+
+local
+
+(*** Lexicographic path order on terms.
+
+  See Baader & Nipkow, Term rewriting, CUP 1998.
+  Without variables.  Const, Var, Bound, Free and Abs are treated all as
+  constants.
+
+  f_ord maps strings to integers and serves two purposes:
+  - Predicate on constant symbols.  Those that are not recognised by f_ord
+    must be mapped to ~1.
+  - Order on the recognised symbols.  These must be mapped to distinct
+    integers >= 0.
+
+***)
+
+fun dest_hd f_ord (Const (a, T)) = 
+      let val ord = f_ord a in
+        if ord = ~1 then ((1, ((a, 0), T)), 0) else ((0, (("", ord), T)), 0)
+      end
+  | dest_hd _ (Free (a, T)) = ((1, ((a, 0), T)), 0)
+  | dest_hd _ (Var v) = ((1, v), 1)
+  | dest_hd _ (Bound i) = ((1, (("", i), Term.dummyT)), 2)
+  | dest_hd _ (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
+
+fun term_lpo f_ord (s, t) =
+  let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in
+    if forall (fn si => term_lpo f_ord (si, t) = LESS) ss
+    then case hd_ord f_ord (f, g) of
+	GREATER =>
+	  if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
+	  then GREATER else LESS
+      | EQUAL =>
+	  if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
+	  then list_ord (term_lpo f_ord) (ss, ts)
+	  else LESS
+      | LESS => LESS
+    else GREATER
+  end
+and hd_ord f_ord (f, g) = case (f, g) of
+    (Abs (_, T, t), Abs (_, U, u)) =>
+      (case term_lpo f_ord (t, u) of EQUAL => Term.typ_ord (T, U) | ord => ord)
+  | (_, _) => prod_ord (prod_ord int_ord
+                  (prod_ord Term.indexname_ord Term.typ_ord)) int_ord
+                (dest_hd f_ord f, dest_hd f_ord g)
+
+in
+
+(*** Term order for commutative rings ***)
+
+fun ring_ord a =
+  find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "Cring.ring.a_inv",
+  "CRing.ring.minus", "Group.monoid.one", "Group.semigroup.mult"];
+
+fun termless_ring (a, b) = (term_lpo ring_ord (a, b) = LESS);
+
+val cring_ss = HOL_ss settermless termless_ring;
+
+fun cring_normalise ctxt = let
+    fun filter t = case HOLogic.dest_Trueprop t of
+        Const ("CRing.cring_axioms", _) $ Free (s, _) => [s]
+      | _ => [] 
+      handle TERM _ => [];
+    val insts = flat (map (filter o #prop o rep_thm)
+      (ProofContext.prems_of ctxt));
+val _ = warning ("Rings in proof context: " ^ implode insts);
+    val simps =
+      flat (map (fn s => ProofContext.get_thms ctxt (s ^ ".cring_simprules"))
+        insts);
+  in Method.SIMPLE_METHOD' HEADGOAL (asm_full_simp_tac (cring_ss addsimps simps))
+  end;
+
+(*
+val ring_ss = HOL_basic_ss settermless termless_ring addsimps
+  [a_assoc, l_zero, l_neg, a_comm, m_assoc, l_one, l_distr, m_comm, minus_def,
+   r_zero, r_neg, r_neg2, r_neg1, minus_add, minus_minus, minus0,
+   a_lcomm, m_lcomm, (*r_one,*) r_distr, l_null, r_null, l_minus, r_minus];
+*)
+
+end;
\ No newline at end of file