First distributed version of Group and Ring theory.
authorballarin
Mon Mar 10 17:25:34 2003 +0100 (2003-03-10)
changeset 1385491c9ab25fece
parent 13853 89131afa9f01
child 13855 644692eca537
First distributed version of Group and Ring theory.
src/HOL/Algebra/CRing.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/ringsimp.ML
     1.1 --- a/src/HOL/Algebra/CRing.thy	Mon Mar 10 16:21:06 2003 +0100
     1.2 +++ b/src/HOL/Algebra/CRing.thy	Mon Mar 10 17:25:34 2003 +0100
     1.3 @@ -7,7 +7,8 @@
     1.4  
     1.5  header {* The algebraic hierarchy of rings as axiomatic classes *}
     1.6  
     1.7 -theory Ring = Group
     1.8 +theory CRing = Group
     1.9 +files ("ringsimp.ML"):
    1.10  
    1.11  section {* The Algebraic Hierarchy of Rings *}
    1.12  
    1.13 @@ -17,49 +18,18 @@
    1.14    zero :: 'a ("\<zero>\<index>")
    1.15    add :: "['a, 'a] => 'a" (infixl "\<oplus>\<index>" 65)
    1.16    a_inv :: "'a => 'a" ("\<ominus>\<index> _" [81] 80)
    1.17 +  minus :: "['a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
    1.18  
    1.19  locale cring = abelian_monoid R +
    1.20    assumes a_abelian_group: "abelian_group (| carrier = carrier R,
    1.21        mult = add R, one = zero R, m_inv = a_inv R |)"
    1.22 +    and minus_def: "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y = x \<oplus> \<ominus> y"
    1.23      and m_inv_def: "[| EX y. y \<in> carrier R & x \<otimes> y = \<one>; x \<in> carrier R |]
    1.24        ==> inv x = (THE y. y \<in> carrier R & x \<otimes> y = \<one>)"
    1.25      and l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
    1.26        ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
    1.27  
    1.28 -ML {*
    1.29 -  thm "cring.l_distr"
    1.30 -*}
    1.31 -
    1.32  (*
    1.33 -locale cring = struct R +
    1.34 -  assumes a_group: "abelian_group (| carrier = carrier R,
    1.35 -      mult = add R, one = zero R, m_inv = a_inv R |)"
    1.36 -    and m_monoid: "abelian_monoid (| carrier = carrier R - {zero R},
    1.37 -      mult = mult R, one = one R |)"
    1.38 -    and l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
    1.39 -      ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
    1.40 -
    1.41 -locale field = struct R +
    1.42 -  assumes a_group: "abelian_group (| carrier = carrier R,
    1.43 -      mult = add R, one = zero R, m_inv = a_inv R |)"
    1.44 -    and m_group: "monoid (| carrier = carrier R - {zero R},
    1.45 -      mult = mult R, one = one R |)"
    1.46 -    and l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
    1.47 -      ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
    1.48 -*)
    1.49 -(*
    1.50 -  a_assoc:      "(a + b) + c = a + (b + c)"
    1.51 -  l_zero:       "0 + a = a"
    1.52 -  l_neg:        "(-a) + a = 0"
    1.53 -  a_comm:       "a + b = b + a"
    1.54 -
    1.55 -  m_assoc:      "(a * b) * c = a * (b * c)"
    1.56 -  l_one:        "1 * a = a"
    1.57 -
    1.58 -  l_distr:      "(a + b) * c = a * c + b * c"
    1.59 -
    1.60 -  m_comm:       "a * b = b * a"
    1.61 -
    1.62    -- {* Definition of derived operations *}
    1.63  
    1.64    minus_def:    "a - b = a + (-b)"
    1.65 @@ -108,171 +78,154 @@
    1.66       mult = add R, one = zero R, m_inv = a_inv R |)"
    1.67    by (simp add: abelian_group_def)
    1.68  
    1.69 -lemma (in cring) a_assoc:
    1.70 -  "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
    1.71 -  ==> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
    1.72 -  using semigroup.m_assoc [OF a_semigroup]
    1.73 -  by simp
    1.74 +lemmas (in cring) a_closed [intro, simp] =
    1.75 +  magma.m_closed [OF a_magma, simplified]
    1.76 +
    1.77 +lemmas (in cring) zero_closed [intro, simp] = 
    1.78 +  l_one.one_closed [OF a_l_one, simplified]
    1.79 +
    1.80 +lemmas (in cring) a_inv_closed [intro, simp] =
    1.81 +  group.inv_closed [OF a_group, simplified]
    1.82 +
    1.83 +lemma (in cring) minus_closed [intro, simp]:
    1.84 +  "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y \<in> carrier R"
    1.85 +  by (simp add: minus_def)
    1.86 +
    1.87 +lemmas (in cring) a_l_cancel [simp] = group.l_cancel [OF a_group, simplified]
    1.88  
    1.89 -lemma (in cring) l_zero:
    1.90 -  "x \<in> carrier R ==> \<zero> \<oplus> x = x"
    1.91 -  using l_one.l_one [OF a_l_one]
    1.92 +lemmas (in cring) a_r_cancel [simp] = group.r_cancel [OF a_group, simplified]
    1.93 +
    1.94 +lemmas (in cring) a_assoc = semigroup.m_assoc [OF a_semigroup, simplified]
    1.95 +
    1.96 +lemmas (in cring) l_zero [simp] = l_one.l_one [OF a_l_one, simplified]
    1.97 +
    1.98 +lemmas (in cring) l_neg = group.l_inv [OF a_group, simplified]
    1.99 +
   1.100 +lemmas (in cring) a_comm = abelian_semigroup.m_comm [OF a_abelian_semigroup,
   1.101 +  simplified]
   1.102 +
   1.103 +lemmas (in cring) a_lcomm =
   1.104 +  abelian_semigroup.m_lcomm [OF a_abelian_semigroup, simplified]
   1.105 +
   1.106 +lemma (in cring) r_zero [simp]:
   1.107 +  "x \<in> carrier R ==> x \<oplus> \<zero> = x"
   1.108 +  using group.r_one [OF a_group]
   1.109    by simp
   1.110  
   1.111 -lemma (in cring) l_neg:
   1.112 -  "x \<in> carrier R ==> (\<ominus> x) \<oplus> x = \<zero>"
   1.113 -  using group.l_inv [OF a_group]
   1.114 +lemma (in cring) r_neg:
   1.115 +  "x \<in> carrier R ==> x \<oplus> (\<ominus> x) = \<zero>"
   1.116 +  using group.r_inv [OF a_group]
   1.117 +  by simp
   1.118 +
   1.119 +lemmas (in cring) minus_zero [simp] = group.inv_one [OF a_group, simplified]
   1.120 +
   1.121 +lemma (in cring) minus_minus [simp]:
   1.122 +  "x \<in> carrier R ==> \<ominus> (\<ominus> x) = x"
   1.123 +  using group.inv_inv [OF a_group, simplified]
   1.124    by simp
   1.125  
   1.126 -lemma (in cring) a_comm:
   1.127 -  "[| x \<in> carrier R; y \<in> carrier R |]
   1.128 -  ==> x \<oplus> y = y \<oplus> x"
   1.129 -  using abelian_semigroup.m_comm [OF a_abelian_semigroup]
   1.130 +lemma (in cring) minus_add:
   1.131 +  "[| x \<in> carrier R; y \<in> carrier R |] ==> \<ominus> (x \<oplus> y) = \<ominus> x \<oplus> \<ominus> y"
   1.132 +  using abelian_group.inv_mult [OF a_abelian_group]
   1.133    by simp
   1.134  
   1.135 +lemmas (in cring) a_ac = a_assoc a_comm a_lcomm
   1.136  
   1.137 +subsection {* Normaliser for Commutative Rings *}
   1.138  
   1.139 -
   1.140 +lemma (in cring) r_neg2:
   1.141 +  "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<oplus> (\<ominus> x \<oplus> y) = y"
   1.142 +proof -
   1.143 +  assume G: "x \<in> carrier R" "y \<in> carrier R"
   1.144 +  then have "(x \<oplus> \<ominus> x) \<oplus> y = y" by (simp only: r_neg l_zero)
   1.145 +  with G show ?thesis by (simp add: a_ac)
   1.146  qed
   1.147  
   1.148 -  l_zero:       "0 + a = a"
   1.149 -  l_neg:        "(-a) + a = 0"
   1.150 -  a_comm:       "a + b = b + a"
   1.151 -
   1.152 -  m_assoc:      "(a * b) * c = a * (b * c)"
   1.153 -  l_one:        "1 * a = a"
   1.154 -
   1.155 -  l_distr:      "(a + b) * c = a * c + b * c"
   1.156 -
   1.157 -  m_comm:       "a * b = b * a"
   1.158 -text {* Normaliser for Commutative Rings *}
   1.159 -
   1.160 -use "order.ML"
   1.161 -
   1.162 -method_setup ring =
   1.163 -  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (full_simp_tac ring_ss)) *}
   1.164 -  {* computes distributive normal form in rings *}
   1.165 -
   1.166 -subsection {* Rings and the summation operator *}
   1.167 -
   1.168 -(* Basic facts --- move to HOL!!! *)
   1.169 -
   1.170 -lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::plus_ac0)"
   1.171 -by simp
   1.172 -
   1.173 -lemma natsum_Suc [simp]:
   1.174 -  "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::plus_ac0)"
   1.175 -by (simp add: atMost_Suc)
   1.176 -
   1.177 -lemma natsum_Suc2:
   1.178 -  "setsum f {..Suc n} = (setsum (%i. f (Suc i)) {..n} + f 0::'a::plus_ac0)"
   1.179 -proof (induct n)
   1.180 -  case 0 show ?case by simp
   1.181 -next
   1.182 -  case Suc thus ?case by (simp add: assoc) 
   1.183 +lemma (in cring) r_neg1:
   1.184 +  "[| x \<in> carrier R; y \<in> carrier R |] ==> \<ominus> x \<oplus> (x \<oplus> y) = y"
   1.185 +proof -
   1.186 +  assume G: "x \<in> carrier R" "y \<in> carrier R"
   1.187 +  then have "(\<ominus> x \<oplus> x) \<oplus> y = y" by (simp only: l_neg l_zero)
   1.188 +  with G show ?thesis by (simp add: a_ac)
   1.189  qed
   1.190  
   1.191 -lemma natsum_cong [cong]:
   1.192 -  "!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::plus_ac0) |] ==>
   1.193 -        setsum f {..j} = setsum g {..k}"
   1.194 -by (induct j) auto
   1.195 -
   1.196 -lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::plus_ac0)"
   1.197 -by (induct n) simp_all
   1.198 -
   1.199 -lemma natsum_add [simp]:
   1.200 -  "!!f::nat=>'a::plus_ac0.
   1.201 -   setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}"
   1.202 -by (induct n) (simp_all add: plus_ac0)
   1.203 -
   1.204 -(* Facts specific to rings *)
   1.205 -
   1.206 -instance ring < plus_ac0
   1.207 -proof
   1.208 -  fix x y z
   1.209 -  show "(x::'a::ring) + y = y + x" by (rule a_comm)
   1.210 -  show "((x::'a::ring) + y) + z = x + (y + z)" by (rule a_assoc)
   1.211 -  show "0 + (x::'a::ring) = x" by (rule l_zero)
   1.212 +lemma (in cring) r_distr:
   1.213 +  "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
   1.214 +  ==> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
   1.215 +proof -
   1.216 +  assume G: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
   1.217 +  then have "z \<otimes> (x \<oplus> y) = (x \<oplus> y) \<otimes> z" by (simp add: m_comm)
   1.218 +  also from G have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
   1.219 +  also from G have "... = z \<otimes> x \<oplus> z \<otimes> y" by (simp add: m_comm)
   1.220 +  finally show ?thesis .
   1.221  qed
   1.222  
   1.223 -ML {*
   1.224 -  local
   1.225 -    val lhss = 
   1.226 -        [read_cterm (sign_of (the_context ()))
   1.227 -                    ("?t + ?u::'a::ring", TVar (("'z", 0), [])),
   1.228 -	 read_cterm (sign_of (the_context ()))
   1.229 -                    ("?t - ?u::'a::ring", TVar (("'z", 0), [])),
   1.230 -	 read_cterm (sign_of (the_context ()))
   1.231 -                    ("?t * ?u::'a::ring", TVar (("'z", 0), [])),
   1.232 -	 read_cterm (sign_of (the_context ()))
   1.233 -                    ("- ?t::'a::ring", TVar (("'z", 0), []))
   1.234 -	];
   1.235 -    fun proc sg _ t = 
   1.236 -      let val rew = Tactic.prove sg [] []
   1.237 -            (HOLogic.mk_Trueprop
   1.238 -              (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t))))
   1.239 -                (fn _ => simp_tac ring_ss 1)
   1.240 -            |> mk_meta_eq;
   1.241 -          val (t', u) = Logic.dest_equals (Thm.prop_of rew);
   1.242 -      in if t' aconv u 
   1.243 -        then None
   1.244 -        else Some rew 
   1.245 -    end;
   1.246 -  in
   1.247 -    val ring_simproc = mk_simproc "ring" lhss proc;
   1.248 -  end;
   1.249 +text {* 
   1.250 +  The following proofs are from Jacobson, Basic Algebra I, pp.~88--89
   1.251  *}
   1.252  
   1.253 -ML_setup {* Addsimprocs [ring_simproc] *}
   1.254 -
   1.255 -lemma natsum_ldistr:
   1.256 -  "!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}"
   1.257 -by (induct n) simp_all
   1.258 -
   1.259 -lemma natsum_rdistr:
   1.260 -  "!!a::'a::ring. a * setsum f {..n::nat} = setsum (%i. a * f i) {..n}"
   1.261 -by (induct n) simp_all
   1.262 -
   1.263 -subsection {* Integral Domains *}
   1.264 +lemma (in cring) l_null [simp]:
   1.265 +  "x \<in> carrier R ==> \<zero> \<otimes> x = \<zero>"
   1.266 +proof -
   1.267 +  assume R: "x \<in> carrier R"
   1.268 +  then have "\<zero> \<otimes> x \<oplus> \<zero> \<otimes> x = (\<zero> \<oplus> \<zero>) \<otimes> x"
   1.269 +    by (simp add: l_distr del: l_zero r_zero)
   1.270 +  also from R have "... = \<zero> \<otimes> x \<oplus> \<zero>" by simp
   1.271 +  finally have "\<zero> \<otimes> x \<oplus> \<zero> \<otimes> x = \<zero> \<otimes> x \<oplus> \<zero>" .
   1.272 +  with R show ?thesis by (simp del: r_zero)
   1.273 +qed
   1.274  
   1.275 -declare one_not_zero [simp]
   1.276 -
   1.277 -lemma zero_not_one [simp]:
   1.278 -  "0 ~= (1::'a::domain)" 
   1.279 -by (rule not_sym) simp
   1.280 +lemma (in cring) r_null [simp]:
   1.281 +  "x \<in> carrier R ==> x \<otimes> \<zero> = \<zero>"
   1.282 +proof -
   1.283 +  assume R: "x \<in> carrier R"
   1.284 +  then have "x \<otimes> \<zero> = \<zero> \<otimes> x" by (simp add: ac)
   1.285 +  also from R have "... = \<zero>" by simp
   1.286 +  finally show ?thesis .
   1.287 +qed
   1.288  
   1.289 -lemma integral_iff: (* not by default a simp rule! *)
   1.290 -  "(a * b = (0::'a::domain)) = (a = 0 | b = 0)"
   1.291 -proof
   1.292 -  assume "a * b = 0" then show "a = 0 | b = 0" by (simp add: integral)
   1.293 -next
   1.294 -  assume "a = 0 | b = 0" then show "a * b = 0" by auto
   1.295 +lemma (in cring) l_minus:
   1.296 +  "[| x \<in> carrier R; y \<in> carrier R |] ==> \<ominus> x \<otimes> y = \<ominus> (x \<otimes> y)"
   1.297 +proof -
   1.298 +  assume R: "x \<in> carrier R" "y \<in> carrier R"
   1.299 +  then have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y = (\<ominus> x \<oplus> x) \<otimes> y" by (simp add: l_distr)
   1.300 +  also from R have "... = \<zero>" by (simp add: l_neg l_null)
   1.301 +  finally have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y = \<zero>" .
   1.302 +  with R have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y \<oplus> \<ominus> (x \<otimes> y) = \<zero> \<oplus> \<ominus> (x \<otimes> y)" by simp
   1.303 +  with R show ?thesis by (simp add: a_assoc r_neg )
   1.304  qed
   1.305  
   1.306 -(*
   1.307 -lemma "(a::'a::ring) - (a - b) = b" apply simp
   1.308 - simproc seems to fail on this example (fixed with new term order)
   1.309 -*)
   1.310 -(*
   1.311 -lemma bug: "(b::'a::ring) - (b - a) = a" by simp
   1.312 -   simproc for rings cannot prove "(a::'a::ring) - (a - b) = b" 
   1.313 -*)
   1.314 -lemma m_lcancel:
   1.315 -  assumes prem: "(a::'a::domain) ~= 0" shows conc: "(a * b = a * c) = (b = c)"
   1.316 -proof
   1.317 -  assume eq: "a * b = a * c"
   1.318 -  then have "a * (b - c) = 0" by simp
   1.319 -  then have "a = 0 | (b - c) = 0" by (simp only: integral_iff)
   1.320 -  with prem have "b - c = 0" by auto 
   1.321 -  then have "b = b - (b - c)" by simp 
   1.322 -  also have "b - (b - c) = c" by simp
   1.323 -  finally show "b = c" .
   1.324 -next
   1.325 -  assume "b = c" then show "a * b = a * c" by simp
   1.326 +lemma (in cring) r_minus:
   1.327 +  "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<otimes> \<ominus> y = \<ominus> (x \<otimes> y)"
   1.328 +proof -
   1.329 +  assume R: "x \<in> carrier R" "y \<in> carrier R"
   1.330 +  then have "x \<otimes> \<ominus> y = \<ominus> y \<otimes> x" by (simp add: ac)
   1.331 +  also from R have "... = \<ominus> (y \<otimes> x)" by (simp add: l_minus)
   1.332 +  also from R have "... = \<ominus> (x \<otimes> y)" by (simp add: ac)
   1.333 +  finally show ?thesis .
   1.334  qed
   1.335  
   1.336 -lemma m_rcancel:
   1.337 -  "(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)"
   1.338 -by (simp add: m_lcancel)
   1.339 +lemmas (in cring) cring_simprules =
   1.340 +  a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
   1.341 +  a_assoc l_zero l_neg a_comm m_assoc l_one l_distr m_comm minus_def
   1.342 +  r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero
   1.343 +  a_lcomm m_lcomm r_distr l_null r_null l_minus r_minus
   1.344 +
   1.345 +use "ringsimp.ML"
   1.346 +
   1.347 +method_setup algebra =
   1.348 +  {* Method.ctxt_args cring_normalise *}
   1.349 +  {* computes distributive normal form in commutative rings (locales version) *}
   1.350 +
   1.351 +lemma
   1.352 +  includes cring R + cring S
   1.353 +  shows "[| a \<in> carrier R; b \<in> carrier R; c \<in> carrier S; d \<in> carrier S |] ==> 
   1.354 +  a \<oplus> \<ominus> (a \<oplus> \<ominus> b) = b & c \<otimes>\<^sub>2 d = d \<otimes>\<^sub>2 c"
   1.355 +  by algebra
   1.356 +
   1.357 +lemma
   1.358 +  includes cring
   1.359 +  shows "[| a \<in> carrier R; b \<in> carrier R |] ==> a \<ominus> (a \<ominus> b) = b"
   1.360 +  by algebra
   1.361  
   1.362  end
     2.1 --- a/src/HOL/Algebra/Group.thy	Mon Mar 10 16:21:06 2003 +0100
     2.2 +++ b/src/HOL/Algebra/Group.thy	Mon Mar 10 17:25:34 2003 +0100
     2.3 @@ -20,14 +20,6 @@
     2.4  
     2.5  subsection {* Definitions *}
     2.6  
     2.7 -(* The following may be unnecessary. *)
     2.8 -text {*
     2.9 -  We write groups additively.  This simplifies notation for rings.
    2.10 -  All rings have an additive inverse, only fields have a
    2.11 -  multiplicative one.  This definitions reduces the need for
    2.12 -  qualifiers.
    2.13 -*}
    2.14 -
    2.15  record 'a semigroup =
    2.16    carrier :: "'a set"
    2.17    mult :: "['a, 'a] => 'a" (infixl "\<otimes>\<index>" 70)
    2.18 @@ -104,6 +96,14 @@
    2.19    then show "y \<otimes> x = z \<otimes> x" by simp
    2.20  qed
    2.21  
    2.22 +lemma (in group) inv_one [simp]:
    2.23 +  "inv \<one> = \<one>"
    2.24 +proof -
    2.25 +  have "inv \<one> = \<one> \<otimes> (inv \<one>)" by simp
    2.26 +  moreover have "... = \<one>" by (simp add: r_inv)
    2.27 +  finally show ?thesis .
    2.28 +qed
    2.29 +
    2.30  lemma (in group) inv_inv [simp]:
    2.31    "x \<in> carrier G ==> inv (inv x) = x"
    2.32  proof -
    2.33 @@ -112,7 +112,7 @@
    2.34    with x show ?thesis by simp
    2.35  qed
    2.36  
    2.37 -lemma (in group) inv_mult:
    2.38 +lemma (in group) inv_mult_group:
    2.39    "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv y \<otimes> inv x"
    2.40  proof -
    2.41    assume G: "x \<in> carrier G" "y \<in> carrier G"
    2.42 @@ -245,21 +245,21 @@
    2.43  
    2.44  constdefs
    2.45    DirProdSemigroup ::
    2.46 -    "[('a, 'c) semigroup_scheme, ('b, 'd) semigroup_scheme]
    2.47 +    "[('a, 'm) semigroup_scheme, ('b, 'n) semigroup_scheme]
    2.48      => ('a \<times> 'b) semigroup"
    2.49      (infixr "\<times>\<^sub>s" 80)
    2.50    "G \<times>\<^sub>s H == (| carrier = carrier G \<times> carrier H,
    2.51      mult = (%(xg, xh) (yg, yh). (mult G xg yg, mult H xh yh)) |)"
    2.52  
    2.53    DirProdMonoid ::
    2.54 -    "[('a, 'c) monoid_scheme, ('b, 'd) monoid_scheme] => ('a \<times> 'b) monoid"
    2.55 +    "[('a, 'm) monoid_scheme, ('b, 'n) monoid_scheme] => ('a \<times> 'b) monoid"
    2.56      (infixr "\<times>\<^sub>m" 80)
    2.57    "G \<times>\<^sub>m H == (| carrier = carrier (G \<times>\<^sub>s H),
    2.58      mult = mult (G \<times>\<^sub>s H),
    2.59      one = (one G, one H) |)"
    2.60  
    2.61    DirProdGroup ::
    2.62 -    "[('a, 'c) group_scheme, ('b, 'd) group_scheme] => ('a \<times> 'b) group"
    2.63 +    "[('a, 'm) group_scheme, ('b, 'n) group_scheme] => ('a \<times> 'b) group"
    2.64      (infixr "\<times>\<^sub>g" 80)
    2.65    "G \<times>\<^sub>g H == (| carrier = carrier (G \<times>\<^sub>m H),
    2.66      mult = mult (G \<times>\<^sub>m H),
    2.67 @@ -409,4 +409,8 @@
    2.68  
    2.69  locale abelian_group = abelian_monoid + group
    2.70  
    2.71 +lemma (in abelian_group) inv_mult:
    2.72 +  "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y"
    2.73 +  by (simp add: ac inv_mult_group)
    2.74 +
    2.75  end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Algebra/ringsimp.ML	Mon Mar 10 17:25:34 2003 +0100
     3.3 @@ -0,0 +1,87 @@
     3.4 +(*
     3.5 +  Title:     Normalisation method for locale cring
     3.6 +  Id:        $Id$
     3.7 +  Author:    Clemens Ballarin
     3.8 +  Copyright: TU Muenchen
     3.9 +*)
    3.10 +
    3.11 +local
    3.12 +
    3.13 +(*** Lexicographic path order on terms.
    3.14 +
    3.15 +  See Baader & Nipkow, Term rewriting, CUP 1998.
    3.16 +  Without variables.  Const, Var, Bound, Free and Abs are treated all as
    3.17 +  constants.
    3.18 +
    3.19 +  f_ord maps strings to integers and serves two purposes:
    3.20 +  - Predicate on constant symbols.  Those that are not recognised by f_ord
    3.21 +    must be mapped to ~1.
    3.22 +  - Order on the recognised symbols.  These must be mapped to distinct
    3.23 +    integers >= 0.
    3.24 +
    3.25 +***)
    3.26 +
    3.27 +fun dest_hd f_ord (Const (a, T)) = 
    3.28 +      let val ord = f_ord a in
    3.29 +        if ord = ~1 then ((1, ((a, 0), T)), 0) else ((0, (("", ord), T)), 0)
    3.30 +      end
    3.31 +  | dest_hd _ (Free (a, T)) = ((1, ((a, 0), T)), 0)
    3.32 +  | dest_hd _ (Var v) = ((1, v), 1)
    3.33 +  | dest_hd _ (Bound i) = ((1, (("", i), Term.dummyT)), 2)
    3.34 +  | dest_hd _ (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
    3.35 +
    3.36 +fun term_lpo f_ord (s, t) =
    3.37 +  let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in
    3.38 +    if forall (fn si => term_lpo f_ord (si, t) = LESS) ss
    3.39 +    then case hd_ord f_ord (f, g) of
    3.40 +	GREATER =>
    3.41 +	  if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
    3.42 +	  then GREATER else LESS
    3.43 +      | EQUAL =>
    3.44 +	  if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
    3.45 +	  then list_ord (term_lpo f_ord) (ss, ts)
    3.46 +	  else LESS
    3.47 +      | LESS => LESS
    3.48 +    else GREATER
    3.49 +  end
    3.50 +and hd_ord f_ord (f, g) = case (f, g) of
    3.51 +    (Abs (_, T, t), Abs (_, U, u)) =>
    3.52 +      (case term_lpo f_ord (t, u) of EQUAL => Term.typ_ord (T, U) | ord => ord)
    3.53 +  | (_, _) => prod_ord (prod_ord int_ord
    3.54 +                  (prod_ord Term.indexname_ord Term.typ_ord)) int_ord
    3.55 +                (dest_hd f_ord f, dest_hd f_ord g)
    3.56 +
    3.57 +in
    3.58 +
    3.59 +(*** Term order for commutative rings ***)
    3.60 +
    3.61 +fun ring_ord a =
    3.62 +  find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "Cring.ring.a_inv",
    3.63 +  "CRing.ring.minus", "Group.monoid.one", "Group.semigroup.mult"];
    3.64 +
    3.65 +fun termless_ring (a, b) = (term_lpo ring_ord (a, b) = LESS);
    3.66 +
    3.67 +val cring_ss = HOL_ss settermless termless_ring;
    3.68 +
    3.69 +fun cring_normalise ctxt = let
    3.70 +    fun filter t = case HOLogic.dest_Trueprop t of
    3.71 +        Const ("CRing.cring_axioms", _) $ Free (s, _) => [s]
    3.72 +      | _ => [] 
    3.73 +      handle TERM _ => [];
    3.74 +    val insts = flat (map (filter o #prop o rep_thm)
    3.75 +      (ProofContext.prems_of ctxt));
    3.76 +val _ = warning ("Rings in proof context: " ^ implode insts);
    3.77 +    val simps =
    3.78 +      flat (map (fn s => ProofContext.get_thms ctxt (s ^ ".cring_simprules"))
    3.79 +        insts);
    3.80 +  in Method.SIMPLE_METHOD' HEADGOAL (asm_full_simp_tac (cring_ss addsimps simps))
    3.81 +  end;
    3.82 +
    3.83 +(*
    3.84 +val ring_ss = HOL_basic_ss settermless termless_ring addsimps
    3.85 +  [a_assoc, l_zero, l_neg, a_comm, m_assoc, l_one, l_distr, m_comm, minus_def,
    3.86 +   r_zero, r_neg, r_neg2, r_neg1, minus_add, minus_minus, minus0,
    3.87 +   a_lcomm, m_lcomm, (*r_one,*) r_distr, l_null, r_null, l_minus, r_minus];
    3.88 +*)
    3.89 +
    3.90 +end;
    3.91 \ No newline at end of file