src/HOL/Algebra/CRing.thy
 author ballarin Mon Mar 10 17:25:34 2003 +0100 (2003-03-10) changeset 13854 91c9ab25fece parent 13835 12b2ffbe543a child 13864 f44f121dd275 permissions -rw-r--r--
First distributed version of Group and Ring theory.
```     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 {* The algebraic hierarchy of rings as axiomatic classes *}
```
```     9
```
```    10 theory CRing = Group
```
```    11 files ("ringsimp.ML"):
```
```    12
```
```    13 section {* The Algebraic Hierarchy of Rings *}
```
```    14
```
```    15 subsection {* Basic Definitions *}
```
```    16
```
```    17 record 'a ring = "'a group" +
```
```    18   zero :: 'a ("\<zero>\<index>")
```
```    19   add :: "['a, 'a] => 'a" (infixl "\<oplus>\<index>" 65)
```
```    20   a_inv :: "'a => 'a" ("\<ominus>\<index> _"  80)
```
```    21   minus :: "['a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
```
```    22
```
```    23 locale cring = abelian_monoid R +
```
```    24   assumes a_abelian_group: "abelian_group (| carrier = carrier R,
```
```    25       mult = add R, one = zero R, m_inv = a_inv R |)"
```
```    26     and minus_def: "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y = x \<oplus> \<ominus> y"
```
```    27     and m_inv_def: "[| EX y. y \<in> carrier R & x \<otimes> y = \<one>; x \<in> carrier R |]
```
```    28       ==> inv x = (THE y. y \<in> carrier R & x \<otimes> y = \<one>)"
```
```    29     and l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
```
```    30       ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
```
```    31
```
```    32 (*
```
```    33   -- {* Definition of derived operations *}
```
```    34
```
```    35   minus_def:    "a - b = a + (-b)"
```
```    36   inverse_def:  "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)"
```
```    37   divide_def:   "a / b = a * inverse b"
```
```    38   power_def:    "a ^ n = nat_rec 1 (%u b. b * a) n"
```
```    39 *)
```
```    40 subsection {* Basic Facts *}
```
```    41
```
```    42 lemma (in cring) a_magma [simp, intro]:
```
```    43   "magma (| carrier = carrier R,
```
```    44      mult = add R, one = zero R, m_inv = a_inv R |)"
```
```    45   using a_abelian_group by (simp only: abelian_group_def)
```
```    46
```
```    47 lemma (in cring) a_l_one [simp, intro]:
```
```    48   "l_one (| carrier = carrier R,
```
```    49      mult = add R, one = zero R, m_inv = a_inv R |)"
```
```    50   using a_abelian_group by (simp only: abelian_group_def)
```
```    51
```
```    52 lemma (in cring) a_abelian_group_parts [simp, intro]:
```
```    53   "semigroup_axioms (| carrier = carrier R,
```
```    54      mult = add R, one = zero R, m_inv = a_inv R |)"
```
```    55   "group_axioms (| carrier = carrier R,
```
```    56      mult = add R, one = zero R, m_inv = a_inv R |)"
```
```    57   "abelian_semigroup_axioms (| carrier = carrier R,
```
```    58      mult = add R, one = zero R, m_inv = a_inv R |)"
```
```    59   using a_abelian_group by (simp_all only: abelian_group_def)
```
```    60
```
```    61 lemma (in cring) a_semigroup:
```
```    62   "semigroup (| carrier = carrier R,
```
```    63      mult = add R, one = zero R, m_inv = a_inv R |)"
```
```    64   by (simp add: semigroup_def)
```
```    65
```
```    66 lemma (in cring) a_group:
```
```    67   "group (| carrier = carrier R,
```
```    68      mult = add R, one = zero R, m_inv = a_inv R |)"
```
```    69   by (simp add: group_def)
```
```    70
```
```    71 lemma (in cring) a_abelian_semigroup:
```
```    72   "abelian_semigroup (| carrier = carrier R,
```
```    73      mult = add R, one = zero R, m_inv = a_inv R |)"
```
```    74   by (simp add: abelian_semigroup_def)
```
```    75
```
```    76 lemma (in cring) a_abelian_group:
```
```    77   "abelian_group (| carrier = carrier R,
```
```    78      mult = add R, one = zero R, m_inv = a_inv R |)"
```
```    79   by (simp add: abelian_group_def)
```
```    80
```
```    81 lemmas (in cring) a_closed [intro, simp] =
```
```    82   magma.m_closed [OF a_magma, simplified]
```
```    83
```
```    84 lemmas (in cring) zero_closed [intro, simp] =
```
```    85   l_one.one_closed [OF a_l_one, simplified]
```
```    86
```
```    87 lemmas (in cring) a_inv_closed [intro, simp] =
```
```    88   group.inv_closed [OF a_group, simplified]
```
```    89
```
```    90 lemma (in cring) minus_closed [intro, simp]:
```
```    91   "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y \<in> carrier R"
```
```    92   by (simp add: minus_def)
```
```    93
```
```    94 lemmas (in cring) a_l_cancel [simp] = group.l_cancel [OF a_group, simplified]
```
```    95
```
```    96 lemmas (in cring) a_r_cancel [simp] = group.r_cancel [OF a_group, simplified]
```
```    97
```
```    98 lemmas (in cring) a_assoc = semigroup.m_assoc [OF a_semigroup, simplified]
```
```    99
```
```   100 lemmas (in cring) l_zero [simp] = l_one.l_one [OF a_l_one, simplified]
```
```   101
```
```   102 lemmas (in cring) l_neg = group.l_inv [OF a_group, simplified]
```
```   103
```
```   104 lemmas (in cring) a_comm = abelian_semigroup.m_comm [OF a_abelian_semigroup,
```
```   105   simplified]
```
```   106
```
```   107 lemmas (in cring) a_lcomm =
```
```   108   abelian_semigroup.m_lcomm [OF a_abelian_semigroup, simplified]
```
```   109
```
```   110 lemma (in cring) r_zero [simp]:
```
```   111   "x \<in> carrier R ==> x \<oplus> \<zero> = x"
```
```   112   using group.r_one [OF a_group]
```
```   113   by simp
```
```   114
```
```   115 lemma (in cring) r_neg:
```
```   116   "x \<in> carrier R ==> x \<oplus> (\<ominus> x) = \<zero>"
```
```   117   using group.r_inv [OF a_group]
```
```   118   by simp
```
```   119
```
```   120 lemmas (in cring) minus_zero [simp] = group.inv_one [OF a_group, simplified]
```
```   121
```
```   122 lemma (in cring) minus_minus [simp]:
```
```   123   "x \<in> carrier R ==> \<ominus> (\<ominus> x) = x"
```
```   124   using group.inv_inv [OF a_group, simplified]
```
```   125   by simp
```
```   126
```
```   127 lemma (in cring) minus_add:
```
```   128   "[| x \<in> carrier R; y \<in> carrier R |] ==> \<ominus> (x \<oplus> y) = \<ominus> x \<oplus> \<ominus> y"
```
```   129   using abelian_group.inv_mult [OF a_abelian_group]
```
```   130   by simp
```
```   131
```
```   132 lemmas (in cring) a_ac = a_assoc a_comm a_lcomm
```
```   133
```
```   134 subsection {* Normaliser for Commutative Rings *}
```
```   135
```
```   136 lemma (in cring) r_neg2:
```
```   137   "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<oplus> (\<ominus> x \<oplus> y) = y"
```
```   138 proof -
```
```   139   assume G: "x \<in> carrier R" "y \<in> carrier R"
```
```   140   then have "(x \<oplus> \<ominus> x) \<oplus> y = y" by (simp only: r_neg l_zero)
```
```   141   with G show ?thesis by (simp add: a_ac)
```
```   142 qed
```
```   143
```
```   144 lemma (in cring) r_neg1:
```
```   145   "[| x \<in> carrier R; y \<in> carrier R |] ==> \<ominus> x \<oplus> (x \<oplus> y) = y"
```
```   146 proof -
```
```   147   assume G: "x \<in> carrier R" "y \<in> carrier R"
```
```   148   then have "(\<ominus> x \<oplus> x) \<oplus> y = y" by (simp only: l_neg l_zero)
```
```   149   with G show ?thesis by (simp add: a_ac)
```
```   150 qed
```
```   151
```
```   152 lemma (in cring) r_distr:
```
```   153   "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
```
```   154   ==> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
```
```   155 proof -
```
```   156   assume G: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
```
```   157   then have "z \<otimes> (x \<oplus> y) = (x \<oplus> y) \<otimes> z" by (simp add: m_comm)
```
```   158   also from G have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
```
```   159   also from G have "... = z \<otimes> x \<oplus> z \<otimes> y" by (simp add: m_comm)
```
```   160   finally show ?thesis .
```
```   161 qed
```
```   162
```
```   163 text {*
```
```   164   The following proofs are from Jacobson, Basic Algebra I, pp.~88--89
```
```   165 *}
```
```   166
```
```   167 lemma (in cring) l_null [simp]:
```
```   168   "x \<in> carrier R ==> \<zero> \<otimes> x = \<zero>"
```
```   169 proof -
```
```   170   assume R: "x \<in> carrier R"
```
```   171   then have "\<zero> \<otimes> x \<oplus> \<zero> \<otimes> x = (\<zero> \<oplus> \<zero>) \<otimes> x"
```
```   172     by (simp add: l_distr del: l_zero r_zero)
```
```   173   also from R have "... = \<zero> \<otimes> x \<oplus> \<zero>" by simp
```
```   174   finally have "\<zero> \<otimes> x \<oplus> \<zero> \<otimes> x = \<zero> \<otimes> x \<oplus> \<zero>" .
```
```   175   with R show ?thesis by (simp del: r_zero)
```
```   176 qed
```
```   177
```
```   178 lemma (in cring) r_null [simp]:
```
```   179   "x \<in> carrier R ==> x \<otimes> \<zero> = \<zero>"
```
```   180 proof -
```
```   181   assume R: "x \<in> carrier R"
```
```   182   then have "x \<otimes> \<zero> = \<zero> \<otimes> x" by (simp add: ac)
```
```   183   also from R have "... = \<zero>" by simp
```
```   184   finally show ?thesis .
```
```   185 qed
```
```   186
```
```   187 lemma (in cring) l_minus:
```
```   188   "[| x \<in> carrier R; y \<in> carrier R |] ==> \<ominus> x \<otimes> y = \<ominus> (x \<otimes> y)"
```
```   189 proof -
```
```   190   assume R: "x \<in> carrier R" "y \<in> carrier R"
```
```   191   then have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y = (\<ominus> x \<oplus> x) \<otimes> y" by (simp add: l_distr)
```
```   192   also from R have "... = \<zero>" by (simp add: l_neg l_null)
```
```   193   finally have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y = \<zero>" .
```
```   194   with R have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y \<oplus> \<ominus> (x \<otimes> y) = \<zero> \<oplus> \<ominus> (x \<otimes> y)" by simp
```
```   195   with R show ?thesis by (simp add: a_assoc r_neg )
```
```   196 qed
```
```   197
```
```   198 lemma (in cring) r_minus:
```
```   199   "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<otimes> \<ominus> y = \<ominus> (x \<otimes> y)"
```
```   200 proof -
```
```   201   assume R: "x \<in> carrier R" "y \<in> carrier R"
```
```   202   then have "x \<otimes> \<ominus> y = \<ominus> y \<otimes> x" by (simp add: ac)
```
```   203   also from R have "... = \<ominus> (y \<otimes> x)" by (simp add: l_minus)
```
```   204   also from R have "... = \<ominus> (x \<otimes> y)" by (simp add: ac)
```
```   205   finally show ?thesis .
```
```   206 qed
```
```   207
```
```   208 lemmas (in cring) cring_simprules =
```
```   209   a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
```
```   210   a_assoc l_zero l_neg a_comm m_assoc l_one l_distr m_comm minus_def
```
```   211   r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero
```
```   212   a_lcomm m_lcomm r_distr l_null r_null l_minus r_minus
```
```   213
```
```   214 use "ringsimp.ML"
```
```   215
```
```   216 method_setup algebra =
```
```   217   {* Method.ctxt_args cring_normalise *}
```
```   218   {* computes distributive normal form in commutative rings (locales version) *}
```
```   219
```
```   220 lemma
```
```   221   includes cring R + cring S
```
```   222   shows "[| a \<in> carrier R; b \<in> carrier R; c \<in> carrier S; d \<in> carrier S |] ==>
```
```   223   a \<oplus> \<ominus> (a \<oplus> \<ominus> b) = b & c \<otimes>\<^sub>2 d = d \<otimes>\<^sub>2 c"
```
```   224   by algebra
```
```   225
```
```   226 lemma
```
```   227   includes cring
```
```   228   shows "[| a \<in> carrier R; b \<in> carrier R |] ==> a \<ominus> (a \<ominus> b) = b"
```
```   229   by algebra
```
```   230
```
```   231 end
```