src/HOL/Algebra/CRing.thy
author ballarin
Mon Aug 02 09:44:46 2004 +0200 (2004-08-02)
changeset 15095 63f5f4c265dd
parent 14963 d584e32f7d46
child 15328 35951e6a7855
permissions -rw-r--r--
Theories now take advantage of recent syntax improvements with (structure).
     1 (*
     2   Title:     The algebraic hierarchy of rings
     3   Id:        $Id$
     4   Author:    Clemens Ballarin, started 9 December 1996
     5   Copyright: Clemens Ballarin
     6 *)
     7 
     8 header {* Abelian Groups *}
     9 
    10 theory CRing = FiniteProduct
    11 files ("ringsimp.ML"):
    12 
    13 record 'a ring = "'a monoid" +
    14   zero :: 'a ("\<zero>\<index>")
    15   add :: "['a, 'a] => 'a" (infixl "\<oplus>\<index>" 65)
    16 
    17 text {* Derived operations. *}
    18 
    19 constdefs (structure R)
    20   a_inv :: "[('a, 'm) ring_scheme, 'a ] => 'a" ("\<ominus>\<index> _" [81] 80)
    21   "a_inv R == m_inv (| carrier = carrier R, mult = add R, one = zero R |)"
    22 
    23   minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
    24   "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y == x \<oplus> (\<ominus> y)"
    25 
    26 locale abelian_monoid = struct G +
    27   assumes a_comm_monoid:
    28      "comm_monoid (| carrier = carrier G, mult = add G, one = zero G |)"
    29 
    30 
    31 text {*
    32   The following definition is redundant but simple to use.
    33 *}
    34 
    35 locale abelian_group = abelian_monoid +
    36   assumes a_comm_group:
    37      "comm_group (| carrier = carrier G, mult = add G, one = zero G |)"
    38 
    39 
    40 subsection {* Basic Properties *}
    41 
    42 lemma abelian_monoidI:
    43   includes struct R
    44   assumes a_closed:
    45       "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> x \<oplus> y \<in> carrier R"
    46     and zero_closed: "\<zero> \<in> carrier R"
    47     and a_assoc:
    48       "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |] ==>
    49       (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
    50     and l_zero: "!!x. x \<in> carrier R ==> \<zero> \<oplus> x = x"
    51     and a_comm:
    52       "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> x \<oplus> y = y \<oplus> x"
    53   shows "abelian_monoid R"
    54   by (auto intro!: abelian_monoid.intro comm_monoidI intro: prems)
    55 
    56 lemma abelian_groupI:
    57   includes struct R
    58   assumes a_closed:
    59       "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> x \<oplus> y \<in> carrier R"
    60     and zero_closed: "zero R \<in> carrier R"
    61     and a_assoc:
    62       "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |] ==>
    63       (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
    64     and a_comm:
    65       "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> x \<oplus> y = y \<oplus> x"
    66     and l_zero: "!!x. x \<in> carrier R ==> \<zero> \<oplus> x = x"
    67     and l_inv_ex: "!!x. x \<in> carrier R ==> EX y : carrier R. y \<oplus> x = \<zero>"
    68   shows "abelian_group R"
    69   by (auto intro!: abelian_group.intro abelian_monoidI
    70       abelian_group_axioms.intro comm_monoidI comm_groupI
    71     intro: prems)
    72 
    73 lemma (in abelian_monoid) a_monoid:
    74   "monoid (| carrier = carrier G, mult = add G, one = zero G |)"
    75 by (rule comm_monoid.axioms, rule a_comm_monoid) 
    76 
    77 lemma (in abelian_group) a_group:
    78   "group (| carrier = carrier G, mult = add G, one = zero G |)"
    79 by (simp add: group_def a_monoid comm_group.axioms a_comm_group) 
    80 
    81 lemmas monoid_record_simps = partial_object.simps monoid.simps
    82 
    83 lemma (in abelian_monoid) a_closed [intro, simp]:
    84   "\<lbrakk> x \<in> carrier G; y \<in> carrier G \<rbrakk> \<Longrightarrow> x \<oplus> y \<in> carrier G"
    85   by (rule monoid.m_closed [OF a_monoid, simplified monoid_record_simps]) 
    86 
    87 lemma (in abelian_monoid) zero_closed [intro, simp]:
    88   "\<zero> \<in> carrier G"
    89   by (rule monoid.one_closed [OF a_monoid, simplified monoid_record_simps])
    90 
    91 lemma (in abelian_group) a_inv_closed [intro, simp]:
    92   "x \<in> carrier G ==> \<ominus> x \<in> carrier G"
    93   by (simp add: a_inv_def
    94     group.inv_closed [OF a_group, simplified monoid_record_simps])
    95 
    96 lemma (in abelian_group) minus_closed [intro, simp]:
    97   "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<ominus> y \<in> carrier G"
    98   by (simp add: minus_def)
    99 
   100 lemma (in abelian_group) a_l_cancel [simp]:
   101   "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   102    (x \<oplus> y = x \<oplus> z) = (y = z)"
   103   by (rule group.l_cancel [OF a_group, simplified monoid_record_simps])
   104 
   105 lemma (in abelian_group) a_r_cancel [simp]:
   106   "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   107    (y \<oplus> x = z \<oplus> x) = (y = z)"
   108   by (rule group.r_cancel [OF a_group, simplified monoid_record_simps])
   109 
   110 lemma (in abelian_monoid) a_assoc:
   111   "\<lbrakk>x \<in> carrier G; y \<in> carrier G; z \<in> carrier G\<rbrakk> \<Longrightarrow>
   112   (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
   113   by (rule monoid.m_assoc [OF a_monoid, simplified monoid_record_simps])
   114 
   115 lemma (in abelian_monoid) l_zero [simp]:
   116   "x \<in> carrier G ==> \<zero> \<oplus> x = x"
   117   by (rule monoid.l_one [OF a_monoid, simplified monoid_record_simps])
   118 
   119 lemma (in abelian_group) l_neg:
   120   "x \<in> carrier G ==> \<ominus> x \<oplus> x = \<zero>"
   121   by (simp add: a_inv_def
   122     group.l_inv [OF a_group, simplified monoid_record_simps])
   123 
   124 lemma (in abelian_monoid) a_comm:
   125   "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> x \<oplus> y = y \<oplus> x"
   126   by (rule comm_monoid.m_comm [OF a_comm_monoid,
   127     simplified monoid_record_simps])
   128 
   129 lemma (in abelian_monoid) a_lcomm:
   130   "\<lbrakk>x \<in> carrier G; y \<in> carrier G; z \<in> carrier G\<rbrakk> \<Longrightarrow>
   131    x \<oplus> (y \<oplus> z) = y \<oplus> (x \<oplus> z)"
   132   by (rule comm_monoid.m_lcomm [OF a_comm_monoid,
   133                                 simplified monoid_record_simps])
   134 
   135 lemma (in abelian_monoid) r_zero [simp]:
   136   "x \<in> carrier G ==> x \<oplus> \<zero> = x"
   137   using monoid.r_one [OF a_monoid]
   138   by simp
   139 
   140 lemma (in abelian_group) r_neg:
   141   "x \<in> carrier G ==> x \<oplus> (\<ominus> x) = \<zero>"
   142   using group.r_inv [OF a_group]
   143   by (simp add: a_inv_def)
   144 
   145 lemma (in abelian_group) minus_zero [simp]:
   146   "\<ominus> \<zero> = \<zero>"
   147   by (simp add: a_inv_def
   148     group.inv_one [OF a_group, simplified monoid_record_simps])
   149 
   150 lemma (in abelian_group) minus_minus [simp]:
   151   "x \<in> carrier G ==> \<ominus> (\<ominus> x) = x"
   152   using group.inv_inv [OF a_group, simplified monoid_record_simps]
   153   by (simp add: a_inv_def)
   154 
   155 lemma (in abelian_group) a_inv_inj:
   156   "inj_on (a_inv G) (carrier G)"
   157   using group.inv_inj [OF a_group, simplified monoid_record_simps]
   158   by (simp add: a_inv_def)
   159 
   160 lemma (in abelian_group) minus_add:
   161   "[| x \<in> carrier G; y \<in> carrier G |] ==> \<ominus> (x \<oplus> y) = \<ominus> x \<oplus> \<ominus> y"
   162   using comm_group.inv_mult [OF a_comm_group]
   163   by (simp add: a_inv_def)
   164 
   165 lemmas (in abelian_monoid) a_ac = a_assoc a_comm a_lcomm
   166 
   167 subsection {* Sums over Finite Sets *}
   168 
   169 text {*
   170   This definition makes it easy to lift lemmas from @{term finprod}.
   171 *}
   172 
   173 constdefs
   174   finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b"
   175   "finsum G f A == finprod (| carrier = carrier G,
   176      mult = add G, one = zero G |) f A"
   177 
   178 syntax
   179   "_finsum" :: "index => idt => 'a set => 'b => 'b"
   180       ("(3\<Oplus>__:_. _)" [1000, 0, 51, 10] 10)
   181 syntax (xsymbols)
   182   "_finsum" :: "index => idt => 'a set => 'b => 'b"
   183       ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
   184 syntax (HTML output)
   185   "_finsum" :: "index => idt => 'a set => 'b => 'b"
   186       ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
   187 translations
   188   "\<Oplus>\<index>i:A. b" == "finsum \<struct>\<index> (%i. b) A"
   189   -- {* Beware of argument permutation! *}
   190 
   191 (*
   192   lemmas (in abelian_monoid) finsum_empty [simp] =
   193     comm_monoid.finprod_empty [OF a_comm_monoid, simplified]
   194   is dangeous, because attributes (like simplified) are applied upon opening
   195   the locale, simplified refers to the simpset at that time!!!
   196 
   197   lemmas (in abelian_monoid) finsum_empty [simp] =
   198     abelian_monoid.finprod_empty [OF a_abelian_monoid, folded finsum_def,
   199       simplified monoid_record_simps]
   200   makes the locale slow, because proofs are repeated for every
   201   "lemma (in abelian_monoid)" command.
   202   When lemma is used time in UnivPoly.thy from beginning to UP_cring goes down
   203   from 110 secs to 60 secs.
   204 *)
   205 
   206 lemma (in abelian_monoid) finsum_empty [simp]:
   207   "finsum G f {} = \<zero>"
   208   by (rule comm_monoid.finprod_empty [OF a_comm_monoid,
   209     folded finsum_def, simplified monoid_record_simps])
   210 
   211 lemma (in abelian_monoid) finsum_insert [simp]:
   212   "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |]
   213   ==> finsum G f (insert a F) = f a \<oplus> finsum G f F"
   214   by (rule comm_monoid.finprod_insert [OF a_comm_monoid,
   215     folded finsum_def, simplified monoid_record_simps])
   216 
   217 lemma (in abelian_monoid) finsum_zero [simp]:
   218   "finite A ==> (\<Oplus>i\<in>A. \<zero>) = \<zero>"
   219   by (rule comm_monoid.finprod_one [OF a_comm_monoid, folded finsum_def,
   220     simplified monoid_record_simps])
   221 
   222 lemma (in abelian_monoid) finsum_closed [simp]:
   223   fixes A
   224   assumes fin: "finite A" and f: "f \<in> A -> carrier G" 
   225   shows "finsum G f A \<in> carrier G"
   226   by (rule comm_monoid.finprod_closed [OF a_comm_monoid,
   227     folded finsum_def, simplified monoid_record_simps])
   228 
   229 lemma (in abelian_monoid) finsum_Un_Int:
   230   "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
   231      finsum G g (A Un B) \<oplus> finsum G g (A Int B) =
   232      finsum G g A \<oplus> finsum G g B"
   233   by (rule comm_monoid.finprod_Un_Int [OF a_comm_monoid,
   234     folded finsum_def, simplified monoid_record_simps])
   235 
   236 lemma (in abelian_monoid) finsum_Un_disjoint:
   237   "[| finite A; finite B; A Int B = {};
   238       g \<in> A -> carrier G; g \<in> B -> carrier G |]
   239    ==> finsum G g (A Un B) = finsum G g A \<oplus> finsum G g B"
   240   by (rule comm_monoid.finprod_Un_disjoint [OF a_comm_monoid,
   241     folded finsum_def, simplified monoid_record_simps])
   242 
   243 lemma (in abelian_monoid) finsum_addf:
   244   "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
   245    finsum G (%x. f x \<oplus> g x) A = (finsum G f A \<oplus> finsum G g A)"
   246   by (rule comm_monoid.finprod_multf [OF a_comm_monoid,
   247     folded finsum_def, simplified monoid_record_simps])
   248 
   249 lemma (in abelian_monoid) finsum_cong':
   250   "[| A = B; g : B -> carrier G;
   251       !!i. i : B ==> f i = g i |] ==> finsum G f A = finsum G g B"
   252   by (rule comm_monoid.finprod_cong' [OF a_comm_monoid,
   253     folded finsum_def, simplified monoid_record_simps]) auto
   254 
   255 lemma (in abelian_monoid) finsum_0 [simp]:
   256   "f : {0::nat} -> carrier G ==> finsum G f {..0} = f 0"
   257   by (rule comm_monoid.finprod_0 [OF a_comm_monoid, folded finsum_def,
   258     simplified monoid_record_simps])
   259 
   260 lemma (in abelian_monoid) finsum_Suc [simp]:
   261   "f : {..Suc n} -> carrier G ==>
   262    finsum G f {..Suc n} = (f (Suc n) \<oplus> finsum G f {..n})"
   263   by (rule comm_monoid.finprod_Suc [OF a_comm_monoid, folded finsum_def,
   264     simplified monoid_record_simps])
   265 
   266 lemma (in abelian_monoid) finsum_Suc2:
   267   "f : {..Suc n} -> carrier G ==>
   268    finsum G f {..Suc n} = (finsum G (%i. f (Suc i)) {..n} \<oplus> f 0)"
   269   by (rule comm_monoid.finprod_Suc2 [OF a_comm_monoid, folded finsum_def,
   270     simplified monoid_record_simps])
   271 
   272 lemma (in abelian_monoid) finsum_add [simp]:
   273   "[| f : {..n} -> carrier G; g : {..n} -> carrier G |] ==>
   274      finsum G (%i. f i \<oplus> g i) {..n::nat} =
   275      finsum G f {..n} \<oplus> finsum G g {..n}"
   276   by (rule comm_monoid.finprod_mult [OF a_comm_monoid, folded finsum_def,
   277     simplified monoid_record_simps])
   278 
   279 lemma (in abelian_monoid) finsum_cong:
   280   "[| A = B; f : B -> carrier G = True;
   281       !!i. i : B ==> f i = g i |] ==> finsum G f A = finsum G g B"
   282   by (rule comm_monoid.finprod_cong [OF a_comm_monoid, folded finsum_def,
   283     simplified monoid_record_simps]) auto
   284 
   285 text {*Usually, if this rule causes a failed congruence proof error,
   286    the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
   287    Adding @{thm [source] Pi_def} to the simpset is often useful. *}
   288 
   289 section {* The Algebraic Hierarchy of Rings *}
   290 
   291 subsection {* Basic Definitions *}
   292 
   293 locale ring = abelian_group R + monoid R +
   294   assumes l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
   295       ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
   296     and r_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
   297       ==> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
   298 
   299 locale cring = ring + comm_monoid R
   300 
   301 locale "domain" = cring +
   302   assumes one_not_zero [simp]: "\<one> ~= \<zero>"
   303     and integral: "[| a \<otimes> b = \<zero>; a \<in> carrier R; b \<in> carrier R |] ==>
   304                   a = \<zero> | b = \<zero>"
   305 
   306 locale field = "domain" +
   307   assumes field_Units: "Units R = carrier R - {\<zero>}"
   308 
   309 subsection {* Basic Facts of Rings *}
   310 
   311 lemma ringI:
   312   includes struct R
   313   assumes abelian_group: "abelian_group R"
   314     and monoid: "monoid R"
   315     and l_distr: "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
   316       ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
   317     and r_distr: "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
   318       ==> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
   319   shows "ring R"
   320   by (auto intro: ring.intro
   321     abelian_group.axioms ring_axioms.intro prems)
   322 
   323 lemma (in ring) is_abelian_group:
   324   "abelian_group R"
   325   by (auto intro!: abelian_groupI a_assoc a_comm l_neg)
   326 
   327 lemma (in ring) is_monoid:
   328   "monoid R"
   329   by (auto intro!: monoidI m_assoc)
   330 
   331 lemma cringI:
   332   includes struct R
   333   assumes abelian_group: "abelian_group R"
   334     and comm_monoid: "comm_monoid R"
   335     and l_distr: "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
   336       ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
   337   shows "cring R"
   338   proof (rule cring.intro)
   339     show "ring_axioms R"
   340     -- {* Right-distributivity follows from left-distributivity and
   341           commutativity. *}
   342     proof (rule ring_axioms.intro)
   343       fix x y z
   344       assume R: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
   345       note [simp]= comm_monoid.axioms [OF comm_monoid]
   346         abelian_group.axioms [OF abelian_group]
   347         abelian_monoid.a_closed
   348         
   349       from R have "z \<otimes> (x \<oplus> y) = (x \<oplus> y) \<otimes> z"
   350         by (simp add: comm_monoid.m_comm [OF comm_monoid.intro])
   351       also from R have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
   352       also from R have "... = z \<otimes> x \<oplus> z \<otimes> y"
   353         by (simp add: comm_monoid.m_comm [OF comm_monoid.intro])
   354       finally show "z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y" .
   355     qed
   356   qed (auto intro: cring.intro
   357       abelian_group.axioms comm_monoid.axioms ring_axioms.intro prems)
   358 
   359 lemma (in cring) is_comm_monoid:
   360   "comm_monoid R"
   361   by (auto intro!: comm_monoidI m_assoc m_comm)
   362 
   363 subsection {* Normaliser for Rings *}
   364 
   365 lemma (in abelian_group) r_neg2:
   366   "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus> (\<ominus> x \<oplus> y) = y"
   367 proof -
   368   assume G: "x \<in> carrier G" "y \<in> carrier G"
   369   then have "(x \<oplus> \<ominus> x) \<oplus> y = y"
   370     by (simp only: r_neg l_zero)
   371   with G show ?thesis 
   372     by (simp add: a_ac)
   373 qed
   374 
   375 lemma (in abelian_group) r_neg1:
   376   "[| x \<in> carrier G; y \<in> carrier G |] ==> \<ominus> x \<oplus> (x \<oplus> y) = y"
   377 proof -
   378   assume G: "x \<in> carrier G" "y \<in> carrier G"
   379   then have "(\<ominus> x \<oplus> x) \<oplus> y = y" 
   380     by (simp only: l_neg l_zero)
   381   with G show ?thesis by (simp add: a_ac)
   382 qed
   383 
   384 text {* 
   385   The following proofs are from Jacobson, Basic Algebra I, pp.~88--89
   386 *}
   387 
   388 lemma (in ring) l_null [simp]:
   389   "x \<in> carrier R ==> \<zero> \<otimes> x = \<zero>"
   390 proof -
   391   assume R: "x \<in> carrier R"
   392   then have "\<zero> \<otimes> x \<oplus> \<zero> \<otimes> x = (\<zero> \<oplus> \<zero>) \<otimes> x"
   393     by (simp add: l_distr del: l_zero r_zero)
   394   also from R have "... = \<zero> \<otimes> x \<oplus> \<zero>" by simp
   395   finally have "\<zero> \<otimes> x \<oplus> \<zero> \<otimes> x = \<zero> \<otimes> x \<oplus> \<zero>" .
   396   with R show ?thesis by (simp del: r_zero)
   397 qed
   398 
   399 lemma (in ring) r_null [simp]:
   400   "x \<in> carrier R ==> x \<otimes> \<zero> = \<zero>"
   401 proof -
   402   assume R: "x \<in> carrier R"
   403   then have "x \<otimes> \<zero> \<oplus> x \<otimes> \<zero> = x \<otimes> (\<zero> \<oplus> \<zero>)"
   404     by (simp add: r_distr del: l_zero r_zero)
   405   also from R have "... = x \<otimes> \<zero> \<oplus> \<zero>" by simp
   406   finally have "x \<otimes> \<zero> \<oplus> x \<otimes> \<zero> = x \<otimes> \<zero> \<oplus> \<zero>" .
   407   with R show ?thesis by (simp del: r_zero)
   408 qed
   409 
   410 lemma (in ring) l_minus:
   411   "[| x \<in> carrier R; y \<in> carrier R |] ==> \<ominus> x \<otimes> y = \<ominus> (x \<otimes> y)"
   412 proof -
   413   assume R: "x \<in> carrier R" "y \<in> carrier R"
   414   then have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y = (\<ominus> x \<oplus> x) \<otimes> y" by (simp add: l_distr)
   415   also from R have "... = \<zero>" by (simp add: l_neg l_null)
   416   finally have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y = \<zero>" .
   417   with R have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y \<oplus> \<ominus> (x \<otimes> y) = \<zero> \<oplus> \<ominus> (x \<otimes> y)" by simp
   418   with R show ?thesis by (simp add: a_assoc r_neg )
   419 qed
   420 
   421 lemma (in ring) r_minus:
   422   "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<otimes> \<ominus> y = \<ominus> (x \<otimes> y)"
   423 proof -
   424   assume R: "x \<in> carrier R" "y \<in> carrier R"
   425   then have "x \<otimes> (\<ominus> y) \<oplus> x \<otimes> y = x \<otimes> (\<ominus> y \<oplus> y)" by (simp add: r_distr)
   426   also from R have "... = \<zero>" by (simp add: l_neg r_null)
   427   finally have "x \<otimes> (\<ominus> y) \<oplus> x \<otimes> y = \<zero>" .
   428   with R have "x \<otimes> (\<ominus> y) \<oplus> x \<otimes> y \<oplus> \<ominus> (x \<otimes> y) = \<zero> \<oplus> \<ominus> (x \<otimes> y)" by simp
   429   with R show ?thesis by (simp add: a_assoc r_neg )
   430 qed
   431 
   432 lemma (in ring) minus_eq:
   433   "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y = x \<oplus> \<ominus> y"
   434   by (simp only: minus_def)
   435 
   436 lemmas (in ring) ring_simprules =
   437   a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
   438   a_assoc l_zero l_neg a_comm m_assoc l_one l_distr minus_eq
   439   r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero
   440   a_lcomm r_distr l_null r_null l_minus r_minus
   441 
   442 lemmas (in cring) cring_simprules =
   443   a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
   444   a_assoc l_zero l_neg a_comm m_assoc l_one l_distr m_comm minus_eq
   445   r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero
   446   a_lcomm m_lcomm r_distr l_null r_null l_minus r_minus
   447 
   448 use "ringsimp.ML"
   449 
   450 method_setup algebra =
   451   {* Method.ctxt_args cring_normalise *}
   452   {* computes distributive normal form in locale context cring *}
   453 
   454 lemma (in cring) nat_pow_zero:
   455   "(n::nat) ~= 0 ==> \<zero> (^) n = \<zero>"
   456   by (induct n) simp_all
   457 
   458 text {* Two examples for use of method algebra *}
   459 
   460 lemma
   461   includes ring R + cring S
   462   shows "[| a \<in> carrier R; b \<in> carrier R; c \<in> carrier S; d \<in> carrier S |] ==> 
   463   a \<oplus> \<ominus> (a \<oplus> \<ominus> b) = b & c \<otimes>\<^bsub>S\<^esub> d = d \<otimes>\<^bsub>S\<^esub> c"
   464   by algebra
   465 
   466 lemma
   467   includes cring
   468   shows "[| a \<in> carrier R; b \<in> carrier R |] ==> a \<ominus> (a \<ominus> b) = b"
   469   by algebra
   470 
   471 subsection {* Sums over Finite Sets *}
   472 
   473 lemma (in cring) finsum_ldistr:
   474   "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
   475    finsum R f A \<otimes> a = finsum R (%i. f i \<otimes> a) A"
   476 proof (induct set: Finites)
   477   case empty then show ?case by simp
   478 next
   479   case (insert F x) then show ?case by (simp add: Pi_def l_distr)
   480 qed
   481 
   482 lemma (in cring) finsum_rdistr:
   483   "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
   484    a \<otimes> finsum R f A = finsum R (%i. a \<otimes> f i) A"
   485 proof (induct set: Finites)
   486   case empty then show ?case by simp
   487 next
   488   case (insert F x) then show ?case by (simp add: Pi_def r_distr)
   489 qed
   490 
   491 subsection {* Facts of Integral Domains *}
   492 
   493 lemma (in "domain") zero_not_one [simp]:
   494   "\<zero> ~= \<one>"
   495   by (rule not_sym) simp
   496 
   497 lemma (in "domain") integral_iff: (* not by default a simp rule! *)
   498   "[| a \<in> carrier R; b \<in> carrier R |] ==> (a \<otimes> b = \<zero>) = (a = \<zero> | b = \<zero>)"
   499 proof
   500   assume "a \<in> carrier R" "b \<in> carrier R" "a \<otimes> b = \<zero>"
   501   then show "a = \<zero> | b = \<zero>" by (simp add: integral)
   502 next
   503   assume "a \<in> carrier R" "b \<in> carrier R" "a = \<zero> | b = \<zero>"
   504   then show "a \<otimes> b = \<zero>" by auto
   505 qed
   506 
   507 lemma (in "domain") m_lcancel:
   508   assumes prem: "a ~= \<zero>"
   509     and R: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R"
   510   shows "(a \<otimes> b = a \<otimes> c) = (b = c)"
   511 proof
   512   assume eq: "a \<otimes> b = a \<otimes> c"
   513   with R have "a \<otimes> (b \<ominus> c) = \<zero>" by algebra
   514   with R have "a = \<zero> | (b \<ominus> c) = \<zero>" by (simp add: integral_iff)
   515   with prem and R have "b \<ominus> c = \<zero>" by auto 
   516   with R have "b = b \<ominus> (b \<ominus> c)" by algebra 
   517   also from R have "b \<ominus> (b \<ominus> c) = c" by algebra
   518   finally show "b = c" .
   519 next
   520   assume "b = c" then show "a \<otimes> b = a \<otimes> c" by simp
   521 qed
   522 
   523 lemma (in "domain") m_rcancel:
   524   assumes prem: "a ~= \<zero>"
   525     and R: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R"
   526   shows conc: "(b \<otimes> a = c \<otimes> a) = (b = c)"
   527 proof -
   528   from prem and R have "(a \<otimes> b = a \<otimes> c) = (b = c)" by (rule m_lcancel)
   529   with R show ?thesis by algebra
   530 qed
   531 
   532 subsection {* Morphisms *}
   533 
   534 constdefs (structure R S)
   535   ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set"
   536   "ring_hom R S == {h. h \<in> carrier R -> carrier S &
   537       (ALL x y. x \<in> carrier R & y \<in> carrier R -->
   538         h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y & h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y) &
   539       h \<one> = \<one>\<^bsub>S\<^esub>}"
   540 
   541 lemma ring_hom_memI:
   542   includes struct R + struct S
   543   assumes hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S"
   544     and hom_mult: "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==>
   545       h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
   546     and hom_add: "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==>
   547       h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
   548     and hom_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
   549   shows "h \<in> ring_hom R S"
   550   by (auto simp add: ring_hom_def prems Pi_def)
   551 
   552 lemma ring_hom_closed:
   553   "[| h \<in> ring_hom R S; x \<in> carrier R |] ==> h x \<in> carrier S"
   554   by (auto simp add: ring_hom_def funcset_mem)
   555 
   556 lemma ring_hom_mult:
   557   includes struct R + struct S
   558   shows
   559     "[| h \<in> ring_hom R S; x \<in> carrier R; y \<in> carrier R |] ==>
   560     h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
   561     by (simp add: ring_hom_def)
   562 
   563 lemma ring_hom_add:
   564   includes struct R + struct S
   565   shows
   566     "[| h \<in> ring_hom R S; x \<in> carrier R; y \<in> carrier R |] ==>
   567     h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
   568     by (simp add: ring_hom_def)
   569 
   570 lemma ring_hom_one:
   571   includes struct R + struct S
   572   shows "h \<in> ring_hom R S ==> h \<one> = \<one>\<^bsub>S\<^esub>"
   573   by (simp add: ring_hom_def)
   574 
   575 locale ring_hom_cring = cring R + cring S + var h +
   576   assumes homh [simp, intro]: "h \<in> ring_hom R S"
   577   notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
   578     and hom_mult [simp] = ring_hom_mult [OF homh]
   579     and hom_add [simp] = ring_hom_add [OF homh]
   580     and hom_one [simp] = ring_hom_one [OF homh]
   581 
   582 lemma (in ring_hom_cring) hom_zero [simp]:
   583   "h \<zero> = \<zero>\<^bsub>S\<^esub>"
   584 proof -
   585   have "h \<zero> \<oplus>\<^bsub>S\<^esub> h \<zero> = h \<zero> \<oplus>\<^bsub>S\<^esub> \<zero>\<^bsub>S\<^esub>"
   586     by (simp add: hom_add [symmetric] del: hom_add)
   587   then show ?thesis by (simp del: S.r_zero)
   588 qed
   589 
   590 lemma (in ring_hom_cring) hom_a_inv [simp]:
   591   "x \<in> carrier R ==> h (\<ominus> x) = \<ominus>\<^bsub>S\<^esub> h x"
   592 proof -
   593   assume R: "x \<in> carrier R"
   594   then have "h x \<oplus>\<^bsub>S\<^esub> h (\<ominus> x) = h x \<oplus>\<^bsub>S\<^esub> (\<ominus>\<^bsub>S\<^esub> h x)"
   595     by (simp add: hom_add [symmetric] R.r_neg S.r_neg del: hom_add)
   596   with R show ?thesis by simp
   597 qed
   598 
   599 lemma (in ring_hom_cring) hom_finsum [simp]:
   600   "[| finite A; f \<in> A -> carrier R |] ==>
   601   h (finsum R f A) = finsum S (h o f) A"
   602 proof (induct set: Finites)
   603   case empty then show ?case by simp
   604 next
   605   case insert then show ?case by (simp add: Pi_def)
   606 qed
   607 
   608 lemma (in ring_hom_cring) hom_finprod:
   609   "[| finite A; f \<in> A -> carrier R |] ==>
   610   h (finprod R f A) = finprod S (h o f) A"
   611 proof (induct set: Finites)
   612   case empty then show ?case by simp
   613 next
   614   case insert then show ?case by (simp add: Pi_def)
   615 qed
   616 
   617 declare ring_hom_cring.hom_finprod [simp]
   618 
   619 lemma id_ring_hom [simp]:
   620   "id \<in> ring_hom R R"
   621   by (auto intro!: ring_hom_memI)
   622 
   623 end