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