src/HOL/Algebra/Ring.thy
author hoelzl
Tue Nov 05 09:44:57 2013 +0100 (2013-11-05)
changeset 54257 5c7a3b6b05a9
parent 48891 c0eafbd55de3
child 55926 3ef14caf5637
permissions -rw-r--r--
generalize SUP and INF to the syntactic type classes Sup and Inf
     1 (*  Title:      HOL/Algebra/Ring.thy
     2     Author:     Clemens Ballarin, started 9 December 1996
     3     Copyright:  Clemens Ballarin
     4 *)
     5 
     6 theory Ring
     7 imports FiniteProduct
     8 begin
     9 
    10 section {* The Algebraic Hierarchy of Rings *}
    11 
    12 subsection {* Abelian Groups *}
    13 
    14 record 'a ring = "'a monoid" +
    15   zero :: 'a ("\<zero>\<index>")
    16   add :: "['a, 'a] => 'a" (infixl "\<oplus>\<index>" 65)
    17 
    18 text {* Derived operations. *}
    19 
    20 definition
    21   a_inv :: "[('a, 'm) ring_scheme, 'a ] => 'a" ("\<ominus>\<index> _" [81] 80)
    22   where "a_inv R = m_inv (| carrier = carrier R, mult = add R, one = zero R |)"
    23 
    24 definition
    25   a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
    26   where "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus>\<^bsub>R\<^esub> y = x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
    27 
    28 locale abelian_monoid =
    29   fixes G (structure)
    30   assumes a_comm_monoid:
    31      "comm_monoid (| carrier = carrier G, mult = add G, one = zero G |)"
    32 
    33 definition
    34   finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b" where
    35   "finsum G = finprod (| carrier = carrier G, mult = add G, one = zero G |)"
    36 
    37 syntax
    38   "_finsum" :: "index => idt => 'a set => 'b => 'b"
    39       ("(3\<Oplus>__:_. _)" [1000, 0, 51, 10] 10)
    40 syntax (xsymbols)
    41   "_finsum" :: "index => idt => 'a set => 'b => 'b"
    42       ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
    43 syntax (HTML output)
    44   "_finsum" :: "index => idt => 'a set => 'b => 'b"
    45       ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
    46 translations
    47   "\<Oplus>\<index>i:A. b" == "CONST finsum \<struct>\<index> (%i. b) A"
    48   -- {* Beware of argument permutation! *}
    49 
    50 
    51 locale abelian_group = abelian_monoid +
    52   assumes a_comm_group:
    53      "comm_group (| carrier = carrier G, mult = add G, one = zero G |)"
    54 
    55 
    56 subsection {* Basic Properties *}
    57 
    58 lemma abelian_monoidI:
    59   fixes R (structure)
    60   assumes a_closed:
    61       "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> x \<oplus> y \<in> carrier R"
    62     and zero_closed: "\<zero> \<in> carrier R"
    63     and a_assoc:
    64       "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |] ==>
    65       (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
    66     and l_zero: "!!x. x \<in> carrier R ==> \<zero> \<oplus> x = x"
    67     and a_comm:
    68       "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> x \<oplus> y = y \<oplus> x"
    69   shows "abelian_monoid R"
    70   by (auto intro!: abelian_monoid.intro comm_monoidI intro: assms)
    71 
    72 lemma abelian_groupI:
    73   fixes R (structure)
    74   assumes a_closed:
    75       "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> x \<oplus> y \<in> carrier R"
    76     and zero_closed: "zero R \<in> carrier R"
    77     and a_assoc:
    78       "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |] ==>
    79       (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
    80     and a_comm:
    81       "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> x \<oplus> y = y \<oplus> x"
    82     and l_zero: "!!x. x \<in> carrier R ==> \<zero> \<oplus> x = x"
    83     and l_inv_ex: "!!x. x \<in> carrier R ==> EX y : carrier R. y \<oplus> x = \<zero>"
    84   shows "abelian_group R"
    85   by (auto intro!: abelian_group.intro abelian_monoidI
    86       abelian_group_axioms.intro comm_monoidI comm_groupI
    87     intro: assms)
    88 
    89 lemma (in abelian_monoid) a_monoid:
    90   "monoid (| carrier = carrier G, mult = add G, one = zero G |)"
    91 by (rule comm_monoid.axioms, rule a_comm_monoid) 
    92 
    93 lemma (in abelian_group) a_group:
    94   "group (| carrier = carrier G, mult = add G, one = zero G |)"
    95   by (simp add: group_def a_monoid)
    96     (simp add: comm_group.axioms group.axioms a_comm_group)
    97 
    98 lemmas monoid_record_simps = partial_object.simps monoid.simps
    99 
   100 text {* Transfer facts from multiplicative structures via interpretation. *}
   101 
   102 sublocale abelian_monoid <
   103   add!: monoid "(| carrier = carrier G, mult = add G, one = zero G |)"
   104   where "carrier (| carrier = carrier G, mult = add G, one = zero G |) = carrier G"
   105     and "mult (| carrier = carrier G, mult = add G, one = zero G |) = add G"
   106     and "one (| carrier = carrier G, mult = add G, one = zero G |) = zero G"
   107   by (rule a_monoid) auto
   108 
   109 context abelian_monoid begin
   110 
   111 lemmas a_closed = add.m_closed 
   112 lemmas zero_closed = add.one_closed
   113 lemmas a_assoc = add.m_assoc
   114 lemmas l_zero = add.l_one
   115 lemmas r_zero = add.r_one
   116 lemmas minus_unique = add.inv_unique
   117 
   118 end
   119 
   120 sublocale abelian_monoid <
   121   add!: comm_monoid "(| carrier = carrier G, mult = add G, one = zero G |)"
   122   where "carrier (| carrier = carrier G, mult = add G, one = zero G |) = carrier G"
   123     and "mult (| carrier = carrier G, mult = add G, one = zero G |) = add G"
   124     and "one (| carrier = carrier G, mult = add G, one = zero G |) = zero G"
   125     and "finprod (| carrier = carrier G, mult = add G, one = zero G |) = finsum G"
   126   by (rule a_comm_monoid) (auto simp: finsum_def)
   127 
   128 context abelian_monoid begin
   129 
   130 lemmas a_comm = add.m_comm
   131 lemmas a_lcomm = add.m_lcomm
   132 lemmas a_ac = a_assoc a_comm a_lcomm
   133 
   134 lemmas finsum_empty = add.finprod_empty
   135 lemmas finsum_insert = add.finprod_insert
   136 lemmas finsum_zero = add.finprod_one
   137 lemmas finsum_closed = add.finprod_closed
   138 lemmas finsum_Un_Int = add.finprod_Un_Int
   139 lemmas finsum_Un_disjoint = add.finprod_Un_disjoint
   140 lemmas finsum_addf = add.finprod_multf
   141 lemmas finsum_cong' = add.finprod_cong'
   142 lemmas finsum_0 = add.finprod_0
   143 lemmas finsum_Suc = add.finprod_Suc
   144 lemmas finsum_Suc2 = add.finprod_Suc2
   145 lemmas finsum_add = add.finprod_mult
   146 
   147 lemmas finsum_cong = add.finprod_cong
   148 text {*Usually, if this rule causes a failed congruence proof error,
   149    the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
   150    Adding @{thm [source] Pi_def} to the simpset is often useful. *}
   151 
   152 lemmas finsum_reindex = add.finprod_reindex
   153 
   154 (* The following would be wrong.  Needed is the equivalent of (^) for addition,
   155   or indeed the canonical embedding from Nat into the monoid.
   156 
   157 lemma finsum_const:
   158   assumes fin [simp]: "finite A"
   159       and a [simp]: "a : carrier G"
   160     shows "finsum G (%x. a) A = a (^) card A"
   161   using fin apply induct
   162   apply force
   163   apply (subst finsum_insert)
   164   apply auto
   165   apply (force simp add: Pi_def)
   166   apply (subst m_comm)
   167   apply auto
   168 done
   169 *)
   170 
   171 lemmas finsum_singleton = add.finprod_singleton
   172 
   173 end
   174 
   175 sublocale abelian_group <
   176   add!: group "(| carrier = carrier G, mult = add G, one = zero G |)"
   177   where "carrier (| carrier = carrier G, mult = add G, one = zero G |) = carrier G"
   178     and "mult (| carrier = carrier G, mult = add G, one = zero G |) = add G"
   179     and "one (| carrier = carrier G, mult = add G, one = zero G |) = zero G"
   180     and "m_inv (| carrier = carrier G, mult = add G, one = zero G |) = a_inv G"
   181   by (rule a_group) (auto simp: m_inv_def a_inv_def)
   182 
   183 context abelian_group begin
   184 
   185 lemmas a_inv_closed = add.inv_closed
   186 
   187 lemma minus_closed [intro, simp]:
   188   "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<ominus> y \<in> carrier G"
   189   by (simp add: a_minus_def)
   190 
   191 lemmas a_l_cancel = add.l_cancel
   192 lemmas a_r_cancel = add.r_cancel
   193 lemmas l_neg = add.l_inv [simp del]
   194 lemmas r_neg = add.r_inv [simp del]
   195 lemmas minus_zero = add.inv_one
   196 lemmas minus_minus = add.inv_inv
   197 lemmas a_inv_inj = add.inv_inj
   198 lemmas minus_equality = add.inv_equality
   199 
   200 end
   201 
   202 sublocale abelian_group <
   203   add!: comm_group "(| carrier = carrier G, mult = add G, one = zero G |)"
   204   where "carrier (| carrier = carrier G, mult = add G, one = zero G |) = carrier G"
   205     and "mult (| carrier = carrier G, mult = add G, one = zero G |) = add G"
   206     and "one (| carrier = carrier G, mult = add G, one = zero G |) = zero G"
   207     and "m_inv (| carrier = carrier G, mult = add G, one = zero G |) = a_inv G"
   208     and "finprod (| carrier = carrier G, mult = add G, one = zero G |) = finsum G"
   209   by (rule a_comm_group) (auto simp: m_inv_def a_inv_def finsum_def)
   210 
   211 lemmas (in abelian_group) minus_add = add.inv_mult
   212  
   213 text {* Derive an @{text "abelian_group"} from a @{text "comm_group"} *}
   214 
   215 lemma comm_group_abelian_groupI:
   216   fixes G (structure)
   217   assumes cg: "comm_group \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   218   shows "abelian_group G"
   219 proof -
   220   interpret comm_group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   221     by (rule cg)
   222   show "abelian_group G" ..
   223 qed
   224 
   225 
   226 subsection {* Rings: Basic Definitions *}
   227 
   228 locale ring = abelian_group R + monoid R for R (structure) +
   229   assumes l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
   230       ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
   231     and r_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
   232       ==> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
   233 
   234 locale cring = ring + comm_monoid R
   235 
   236 locale "domain" = cring +
   237   assumes one_not_zero [simp]: "\<one> ~= \<zero>"
   238     and integral: "[| a \<otimes> b = \<zero>; a \<in> carrier R; b \<in> carrier R |] ==>
   239                   a = \<zero> | b = \<zero>"
   240 
   241 locale field = "domain" +
   242   assumes field_Units: "Units R = carrier R - {\<zero>}"
   243 
   244 
   245 subsection {* Rings *}
   246 
   247 lemma ringI:
   248   fixes R (structure)
   249   assumes abelian_group: "abelian_group R"
   250     and monoid: "monoid R"
   251     and l_distr: "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
   252       ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
   253     and r_distr: "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
   254       ==> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
   255   shows "ring R"
   256   by (auto intro: ring.intro
   257     abelian_group.axioms ring_axioms.intro assms)
   258 
   259 context ring begin
   260 
   261 lemma is_abelian_group: "abelian_group R" ..
   262 
   263 lemma is_monoid: "monoid R"
   264   by (auto intro!: monoidI m_assoc)
   265 
   266 lemma is_ring: "ring R"
   267   by (rule ring_axioms)
   268 
   269 end
   270 
   271 lemmas ring_record_simps = monoid_record_simps ring.simps
   272 
   273 lemma cringI:
   274   fixes R (structure)
   275   assumes abelian_group: "abelian_group R"
   276     and comm_monoid: "comm_monoid R"
   277     and l_distr: "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
   278       ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
   279   shows "cring R"
   280 proof (intro cring.intro ring.intro)
   281   show "ring_axioms R"
   282     -- {* Right-distributivity follows from left-distributivity and
   283           commutativity. *}
   284   proof (rule ring_axioms.intro)
   285     fix x y z
   286     assume R: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
   287     note [simp] = comm_monoid.axioms [OF comm_monoid]
   288       abelian_group.axioms [OF abelian_group]
   289       abelian_monoid.a_closed
   290         
   291     from R have "z \<otimes> (x \<oplus> y) = (x \<oplus> y) \<otimes> z"
   292       by (simp add: comm_monoid.m_comm [OF comm_monoid.intro])
   293     also from R have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
   294     also from R have "... = z \<otimes> x \<oplus> z \<otimes> y"
   295       by (simp add: comm_monoid.m_comm [OF comm_monoid.intro])
   296     finally show "z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y" .
   297   qed (rule l_distr)
   298 qed (auto intro: cring.intro
   299   abelian_group.axioms comm_monoid.axioms ring_axioms.intro assms)
   300 
   301 (*
   302 lemma (in cring) is_comm_monoid:
   303   "comm_monoid R"
   304   by (auto intro!: comm_monoidI m_assoc m_comm)
   305 *)
   306 
   307 lemma (in cring) is_cring:
   308   "cring R" by (rule cring_axioms)
   309 
   310 
   311 subsubsection {* Normaliser for Rings *}
   312 
   313 lemma (in abelian_group) r_neg2:
   314   "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus> (\<ominus> x \<oplus> y) = y"
   315 proof -
   316   assume G: "x \<in> carrier G" "y \<in> carrier G"
   317   then have "(x \<oplus> \<ominus> x) \<oplus> y = y"
   318     by (simp only: r_neg l_zero)
   319   with G show ?thesis
   320     by (simp add: a_ac)
   321 qed
   322 
   323 lemma (in abelian_group) r_neg1:
   324   "[| x \<in> carrier G; y \<in> carrier G |] ==> \<ominus> x \<oplus> (x \<oplus> y) = y"
   325 proof -
   326   assume G: "x \<in> carrier G" "y \<in> carrier G"
   327   then have "(\<ominus> x \<oplus> x) \<oplus> y = y" 
   328     by (simp only: l_neg l_zero)
   329   with G show ?thesis by (simp add: a_ac)
   330 qed
   331 
   332 context ring begin
   333 
   334 text {* 
   335   The following proofs are from Jacobson, Basic Algebra I, pp.~88--89.
   336 *}
   337 
   338 lemma l_null [simp]:
   339   "x \<in> carrier R ==> \<zero> \<otimes> x = \<zero>"
   340 proof -
   341   assume R: "x \<in> carrier R"
   342   then have "\<zero> \<otimes> x \<oplus> \<zero> \<otimes> x = (\<zero> \<oplus> \<zero>) \<otimes> x"
   343     by (simp add: l_distr del: l_zero r_zero)
   344   also from R have "... = \<zero> \<otimes> x \<oplus> \<zero>" by simp
   345   finally have "\<zero> \<otimes> x \<oplus> \<zero> \<otimes> x = \<zero> \<otimes> x \<oplus> \<zero>" .
   346   with R show ?thesis by (simp del: r_zero)
   347 qed
   348 
   349 lemma r_null [simp]:
   350   "x \<in> carrier R ==> x \<otimes> \<zero> = \<zero>"
   351 proof -
   352   assume R: "x \<in> carrier R"
   353   then have "x \<otimes> \<zero> \<oplus> x \<otimes> \<zero> = x \<otimes> (\<zero> \<oplus> \<zero>)"
   354     by (simp add: r_distr del: l_zero r_zero)
   355   also from R have "... = x \<otimes> \<zero> \<oplus> \<zero>" by simp
   356   finally have "x \<otimes> \<zero> \<oplus> x \<otimes> \<zero> = x \<otimes> \<zero> \<oplus> \<zero>" .
   357   with R show ?thesis by (simp del: r_zero)
   358 qed
   359 
   360 lemma l_minus:
   361   "[| x \<in> carrier R; y \<in> carrier R |] ==> \<ominus> x \<otimes> y = \<ominus> (x \<otimes> y)"
   362 proof -
   363   assume R: "x \<in> carrier R" "y \<in> carrier R"
   364   then have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y = (\<ominus> x \<oplus> x) \<otimes> y" by (simp add: l_distr)
   365   also from R have "... = \<zero>" by (simp add: l_neg)
   366   finally have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y = \<zero>" .
   367   with R have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y \<oplus> \<ominus> (x \<otimes> y) = \<zero> \<oplus> \<ominus> (x \<otimes> y)" by simp
   368   with R show ?thesis by (simp add: a_assoc r_neg)
   369 qed
   370 
   371 lemma r_minus:
   372   "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<otimes> \<ominus> y = \<ominus> (x \<otimes> y)"
   373 proof -
   374   assume R: "x \<in> carrier R" "y \<in> carrier R"
   375   then have "x \<otimes> (\<ominus> y) \<oplus> x \<otimes> y = x \<otimes> (\<ominus> y \<oplus> y)" by (simp add: r_distr)
   376   also from R have "... = \<zero>" by (simp add: l_neg)
   377   finally have "x \<otimes> (\<ominus> y) \<oplus> x \<otimes> y = \<zero>" .
   378   with R have "x \<otimes> (\<ominus> y) \<oplus> x \<otimes> y \<oplus> \<ominus> (x \<otimes> y) = \<zero> \<oplus> \<ominus> (x \<otimes> y)" by simp
   379   with R show ?thesis by (simp add: a_assoc r_neg )
   380 qed
   381 
   382 end
   383 
   384 lemma (in abelian_group) minus_eq:
   385   "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<ominus> y = x \<oplus> \<ominus> y"
   386   by (simp only: a_minus_def)
   387 
   388 text {* Setup algebra method:
   389   compute distributive normal form in locale contexts *}
   390 
   391 ML_file "ringsimp.ML"
   392 
   393 setup Algebra.attrib_setup
   394 
   395 method_setup algebra = {*
   396   Scan.succeed (SIMPLE_METHOD' o Algebra.algebra_tac)
   397 *} "normalisation of algebraic structure"
   398 
   399 lemmas (in ring) ring_simprules
   400   [algebra ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] =
   401   a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
   402   a_assoc l_zero l_neg a_comm m_assoc l_one l_distr minus_eq
   403   r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero
   404   a_lcomm r_distr l_null r_null l_minus r_minus
   405 
   406 lemmas (in cring)
   407   [algebra del: ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] =
   408   _
   409 
   410 lemmas (in cring) cring_simprules
   411   [algebra add: cring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] =
   412   a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
   413   a_assoc l_zero l_neg a_comm m_assoc l_one l_distr m_comm minus_eq
   414   r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero
   415   a_lcomm m_lcomm r_distr l_null r_null l_minus r_minus
   416 
   417 lemma (in cring) nat_pow_zero:
   418   "(n::nat) ~= 0 ==> \<zero> (^) n = \<zero>"
   419   by (induct n) simp_all
   420 
   421 context ring begin
   422 
   423 lemma one_zeroD:
   424   assumes onezero: "\<one> = \<zero>"
   425   shows "carrier R = {\<zero>}"
   426 proof (rule, rule)
   427   fix x
   428   assume xcarr: "x \<in> carrier R"
   429   from xcarr have "x = x \<otimes> \<one>" by simp
   430   with onezero have "x = x \<otimes> \<zero>" by simp
   431   with xcarr have "x = \<zero>" by simp
   432   then show "x \<in> {\<zero>}" by fast
   433 qed fast
   434 
   435 lemma one_zeroI:
   436   assumes carrzero: "carrier R = {\<zero>}"
   437   shows "\<one> = \<zero>"
   438 proof -
   439   from one_closed and carrzero
   440       show "\<one> = \<zero>" by simp
   441 qed
   442 
   443 lemma carrier_one_zero: "(carrier R = {\<zero>}) = (\<one> = \<zero>)"
   444   apply rule
   445    apply (erule one_zeroI)
   446   apply (erule one_zeroD)
   447   done
   448 
   449 lemma carrier_one_not_zero: "(carrier R \<noteq> {\<zero>}) = (\<one> \<noteq> \<zero>)"
   450   by (simp add: carrier_one_zero)
   451 
   452 end
   453 
   454 text {* Two examples for use of method algebra *}
   455 
   456 lemma
   457   fixes R (structure) and S (structure)
   458   assumes "ring R" "cring S"
   459   assumes RS: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier S" "d \<in> carrier S"
   460   shows "a \<oplus> \<ominus> (a \<oplus> \<ominus> b) = b & c \<otimes>\<^bsub>S\<^esub> d = d \<otimes>\<^bsub>S\<^esub> c"
   461 proof -
   462   interpret ring R by fact
   463   interpret cring S by fact
   464   from RS show ?thesis by algebra
   465 qed
   466 
   467 lemma
   468   fixes R (structure)
   469   assumes "ring R"
   470   assumes R: "a \<in> carrier R" "b \<in> carrier R"
   471   shows "a \<ominus> (a \<ominus> b) = b"
   472 proof -
   473   interpret ring R by fact
   474   from R show ?thesis by algebra
   475 qed
   476 
   477 
   478 subsubsection {* Sums over Finite Sets *}
   479 
   480 lemma (in ring) finsum_ldistr:
   481   "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
   482    finsum R f A \<otimes> a = finsum R (%i. f i \<otimes> a) A"
   483 proof (induct set: finite)
   484   case empty then show ?case by simp
   485 next
   486   case (insert x F) then show ?case by (simp add: Pi_def l_distr)
   487 qed
   488 
   489 lemma (in ring) finsum_rdistr:
   490   "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
   491    a \<otimes> finsum R f A = finsum R (%i. a \<otimes> f i) A"
   492 proof (induct set: finite)
   493   case empty then show ?case by simp
   494 next
   495   case (insert x F) then show ?case by (simp add: Pi_def r_distr)
   496 qed
   497 
   498 
   499 subsection {* Integral Domains *}
   500 
   501 context "domain" begin
   502 
   503 lemma zero_not_one [simp]:
   504   "\<zero> ~= \<one>"
   505   by (rule not_sym) simp
   506 
   507 lemma integral_iff: (* not by default a simp rule! *)
   508   "[| a \<in> carrier R; b \<in> carrier R |] ==> (a \<otimes> b = \<zero>) = (a = \<zero> | b = \<zero>)"
   509 proof
   510   assume "a \<in> carrier R" "b \<in> carrier R" "a \<otimes> b = \<zero>"
   511   then show "a = \<zero> | b = \<zero>" by (simp add: integral)
   512 next
   513   assume "a \<in> carrier R" "b \<in> carrier R" "a = \<zero> | b = \<zero>"
   514   then show "a \<otimes> b = \<zero>" by auto
   515 qed
   516 
   517 lemma m_lcancel:
   518   assumes prem: "a ~= \<zero>"
   519     and R: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R"
   520   shows "(a \<otimes> b = a \<otimes> c) = (b = c)"
   521 proof
   522   assume eq: "a \<otimes> b = a \<otimes> c"
   523   with R have "a \<otimes> (b \<ominus> c) = \<zero>" by algebra
   524   with R have "a = \<zero> | (b \<ominus> c) = \<zero>" by (simp add: integral_iff)
   525   with prem and R have "b \<ominus> c = \<zero>" by auto 
   526   with R have "b = b \<ominus> (b \<ominus> c)" by algebra 
   527   also from R have "b \<ominus> (b \<ominus> c) = c" by algebra
   528   finally show "b = c" .
   529 next
   530   assume "b = c" then show "a \<otimes> b = a \<otimes> c" by simp
   531 qed
   532 
   533 lemma m_rcancel:
   534   assumes prem: "a ~= \<zero>"
   535     and R: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R"
   536   shows conc: "(b \<otimes> a = c \<otimes> a) = (b = c)"
   537 proof -
   538   from prem and R have "(a \<otimes> b = a \<otimes> c) = (b = c)" by (rule m_lcancel)
   539   with R show ?thesis by algebra
   540 qed
   541 
   542 end
   543 
   544 
   545 subsection {* Fields *}
   546 
   547 text {* Field would not need to be derived from domain, the properties
   548   for domain follow from the assumptions of field *}
   549 lemma (in cring) cring_fieldI:
   550   assumes field_Units: "Units R = carrier R - {\<zero>}"
   551   shows "field R"
   552 proof
   553   from field_Units have "\<zero> \<notin> Units R" by fast
   554   moreover have "\<one> \<in> Units R" by fast
   555   ultimately show "\<one> \<noteq> \<zero>" by force
   556 next
   557   fix a b
   558   assume acarr: "a \<in> carrier R"
   559     and bcarr: "b \<in> carrier R"
   560     and ab: "a \<otimes> b = \<zero>"
   561   show "a = \<zero> \<or> b = \<zero>"
   562   proof (cases "a = \<zero>", simp)
   563     assume "a \<noteq> \<zero>"
   564     with field_Units and acarr have aUnit: "a \<in> Units R" by fast
   565     from bcarr have "b = \<one> \<otimes> b" by algebra
   566     also from aUnit acarr have "... = (inv a \<otimes> a) \<otimes> b" by simp
   567     also from acarr bcarr aUnit[THEN Units_inv_closed]
   568     have "... = (inv a) \<otimes> (a \<otimes> b)" by algebra
   569     also from ab and acarr bcarr aUnit have "... = (inv a) \<otimes> \<zero>" by simp
   570     also from aUnit[THEN Units_inv_closed] have "... = \<zero>" by algebra
   571     finally have "b = \<zero>" .
   572     then show "a = \<zero> \<or> b = \<zero>" by simp
   573   qed
   574 qed (rule field_Units)
   575 
   576 text {* Another variant to show that something is a field *}
   577 lemma (in cring) cring_fieldI2:
   578   assumes notzero: "\<zero> \<noteq> \<one>"
   579   and invex: "\<And>a. \<lbrakk>a \<in> carrier R; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>b\<in>carrier R. a \<otimes> b = \<one>"
   580   shows "field R"
   581   apply (rule cring_fieldI, simp add: Units_def)
   582   apply (rule, clarsimp)
   583   apply (simp add: notzero)
   584 proof (clarsimp)
   585   fix x
   586   assume xcarr: "x \<in> carrier R"
   587     and "x \<noteq> \<zero>"
   588   then have "\<exists>y\<in>carrier R. x \<otimes> y = \<one>" by (rule invex)
   589   then obtain y where ycarr: "y \<in> carrier R" and xy: "x \<otimes> y = \<one>" by fast
   590   from xy xcarr ycarr have "y \<otimes> x = \<one>" by (simp add: m_comm)
   591   with ycarr and xy show "\<exists>y\<in>carrier R. y \<otimes> x = \<one> \<and> x \<otimes> y = \<one>" by fast
   592 qed
   593 
   594 
   595 subsection {* Morphisms *}
   596 
   597 definition
   598   ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set"
   599   where "ring_hom R S =
   600     {h. h \<in> carrier R -> carrier S &
   601       (ALL x y. x \<in> carrier R & y \<in> carrier R -->
   602         h (x \<otimes>\<^bsub>R\<^esub> y) = h x \<otimes>\<^bsub>S\<^esub> h y & h (x \<oplus>\<^bsub>R\<^esub> y) = h x \<oplus>\<^bsub>S\<^esub> h y) &
   603       h \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>}"
   604 
   605 lemma ring_hom_memI:
   606   fixes R (structure) and S (structure)
   607   assumes hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S"
   608     and hom_mult: "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==>
   609       h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
   610     and hom_add: "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==>
   611       h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
   612     and hom_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
   613   shows "h \<in> ring_hom R S"
   614   by (auto simp add: ring_hom_def assms Pi_def)
   615 
   616 lemma ring_hom_closed:
   617   "[| h \<in> ring_hom R S; x \<in> carrier R |] ==> h x \<in> carrier S"
   618   by (auto simp add: ring_hom_def funcset_mem)
   619 
   620 lemma ring_hom_mult:
   621   fixes R (structure) and S (structure)
   622   shows
   623     "[| h \<in> ring_hom R S; x \<in> carrier R; y \<in> carrier R |] ==>
   624     h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
   625     by (simp add: ring_hom_def)
   626 
   627 lemma ring_hom_add:
   628   fixes R (structure) and S (structure)
   629   shows
   630     "[| h \<in> ring_hom R S; x \<in> carrier R; y \<in> carrier R |] ==>
   631     h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
   632     by (simp add: ring_hom_def)
   633 
   634 lemma ring_hom_one:
   635   fixes R (structure) and S (structure)
   636   shows "h \<in> ring_hom R S ==> h \<one> = \<one>\<^bsub>S\<^esub>"
   637   by (simp add: ring_hom_def)
   638 
   639 locale ring_hom_cring = R: cring R + S: cring S
   640     for R (structure) and S (structure) +
   641   fixes h
   642   assumes homh [simp, intro]: "h \<in> ring_hom R S"
   643   notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
   644     and hom_mult [simp] = ring_hom_mult [OF homh]
   645     and hom_add [simp] = ring_hom_add [OF homh]
   646     and hom_one [simp] = ring_hom_one [OF homh]
   647 
   648 lemma (in ring_hom_cring) hom_zero [simp]:
   649   "h \<zero> = \<zero>\<^bsub>S\<^esub>"
   650 proof -
   651   have "h \<zero> \<oplus>\<^bsub>S\<^esub> h \<zero> = h \<zero> \<oplus>\<^bsub>S\<^esub> \<zero>\<^bsub>S\<^esub>"
   652     by (simp add: hom_add [symmetric] del: hom_add)
   653   then show ?thesis by (simp del: S.r_zero)
   654 qed
   655 
   656 lemma (in ring_hom_cring) hom_a_inv [simp]:
   657   "x \<in> carrier R ==> h (\<ominus> x) = \<ominus>\<^bsub>S\<^esub> h x"
   658 proof -
   659   assume R: "x \<in> carrier R"
   660   then have "h x \<oplus>\<^bsub>S\<^esub> h (\<ominus> x) = h x \<oplus>\<^bsub>S\<^esub> (\<ominus>\<^bsub>S\<^esub> h x)"
   661     by (simp add: hom_add [symmetric] R.r_neg S.r_neg del: hom_add)
   662   with R show ?thesis by simp
   663 qed
   664 
   665 lemma (in ring_hom_cring) hom_finsum [simp]:
   666   "[| finite A; f \<in> A -> carrier R |] ==>
   667   h (finsum R f A) = finsum S (h o f) A"
   668 proof (induct set: finite)
   669   case empty then show ?case by simp
   670 next
   671   case insert then show ?case by (simp add: Pi_def)
   672 qed
   673 
   674 lemma (in ring_hom_cring) hom_finprod:
   675   "[| finite A; f \<in> A -> carrier R |] ==>
   676   h (finprod R f A) = finprod S (h o f) A"
   677 proof (induct set: finite)
   678   case empty then show ?case by simp
   679 next
   680   case insert then show ?case by (simp add: Pi_def)
   681 qed
   682 
   683 declare ring_hom_cring.hom_finprod [simp]
   684 
   685 lemma id_ring_hom [simp]:
   686   "id \<in> ring_hom R R"
   687   by (auto intro!: ring_hom_memI)
   688 
   689 end