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