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> _"  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
```