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