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> _" [81] 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