src/ZF/ex/Ring.thy
author ballarin
Thu Dec 11 18:30:26 2008 +0100 (2008-12-11)
changeset 29223 e09c53289830
parent 28952 15a4b2cf8c34
child 41524 4d2f9a1c24c7
permissions -rw-r--r--
Conversion of HOL-Main and ZF to new locales.
paulson@14883
     1
(* Title:  ZF/ex/Ring.thy
paulson@14883
     2
paulson@14883
     3
*)
paulson@14883
     4
paulson@14883
     5
header {* Rings *}
paulson@14883
     6
haftmann@16417
     7
theory Ring imports Group begin
paulson@14883
     8
paulson@14883
     9
(*First, we must simulate a record declaration:
paulson@14883
    10
record ring = monoid +
paulson@14883
    11
  add :: "[i, i] => i" (infixl "\<oplus>\<index>" 65)
paulson@14883
    12
  zero :: i ("\<zero>\<index>")
paulson@14883
    13
*)
paulson@14883
    14
wenzelm@21233
    15
definition
wenzelm@21404
    16
  add_field :: "i => i" where
wenzelm@21233
    17
  "add_field(M) = fst(snd(snd(snd(M))))"
paulson@14883
    18
wenzelm@21404
    19
definition
wenzelm@21404
    20
  ring_add :: "[i, i, i] => i" (infixl "\<oplus>\<index>" 65) where
wenzelm@21233
    21
  "ring_add(M,x,y) = add_field(M) ` <x,y>"
paulson@14883
    22
wenzelm@21404
    23
definition
wenzelm@21404
    24
  zero :: "i => i" ("\<zero>\<index>") where
wenzelm@21233
    25
  "zero(M) = fst(snd(snd(snd(snd(M)))))"
paulson@14883
    26
paulson@14883
    27
paulson@14883
    28
lemma add_field_eq [simp]: "add_field(<C,M,I,A,z>) = A"
paulson@14883
    29
  by (simp add: add_field_def)
paulson@14883
    30
paulson@14883
    31
lemma add_eq [simp]: "ring_add(<C,M,I,A,z>, x, y) = A ` <x,y>"
paulson@14883
    32
  by (simp add: ring_add_def)
paulson@14883
    33
paulson@14883
    34
lemma zero_eq [simp]: "zero(<C,M,I,A,Z,z>) = Z"
paulson@14883
    35
  by (simp add: zero_def)
paulson@14883
    36
paulson@14883
    37
paulson@14883
    38
text {* Derived operations. *}
paulson@14883
    39
wenzelm@21233
    40
definition
wenzelm@21404
    41
  a_inv :: "[i,i] => i" ("\<ominus>\<index> _" [81] 80) where
paulson@14883
    42
  "a_inv(R) == m_inv (<carrier(R), add_field(R), zero(R), 0>)"
paulson@14883
    43
wenzelm@21404
    44
definition
wenzelm@21404
    45
  minus :: "[i,i,i] => i" (infixl "\<ominus>\<index>" 65) where
wenzelm@21233
    46
  "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus>\<^bsub>R\<^esub> y = x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
paulson@14883
    47
ballarin@29223
    48
locale abelian_monoid = fixes G (structure)
paulson@14883
    49
  assumes a_comm_monoid: 
paulson@14883
    50
    "comm_monoid (<carrier(G), add_field(G), zero(G), 0>)"
paulson@14883
    51
paulson@14883
    52
text {*
paulson@14883
    53
  The following definition is redundant but simple to use.
paulson@14883
    54
*}
paulson@14883
    55
paulson@14883
    56
locale abelian_group = abelian_monoid +
paulson@14883
    57
  assumes a_comm_group: 
paulson@14883
    58
    "comm_group (<carrier(G), add_field(G), zero(G), 0>)"
paulson@14883
    59
ballarin@29223
    60
locale ring = abelian_group R + monoid R for R (structure) +
paulson@14883
    61
  assumes l_distr: "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R); z \<in> carrier(R)\<rbrakk>
paulson@14883
    62
      \<Longrightarrow> (x \<oplus> y) \<cdot> z = x \<cdot> z \<oplus> y \<cdot> z"
paulson@14883
    63
    and r_distr: "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R); z \<in> carrier(R)\<rbrakk>
paulson@14883
    64
      \<Longrightarrow> z \<cdot> (x \<oplus> y) = z \<cdot> x \<oplus> z \<cdot> y"
paulson@14883
    65
paulson@14883
    66
locale cring = ring + comm_monoid R
paulson@14883
    67
paulson@14883
    68
locale "domain" = cring +
paulson@14883
    69
  assumes one_not_zero [simp]: "\<one> \<noteq> \<zero>"
paulson@14883
    70
    and integral: "\<lbrakk>a \<cdot> b = \<zero>; a \<in> carrier(R); b \<in> carrier(R)\<rbrakk> \<Longrightarrow>
paulson@14883
    71
                  a = \<zero> | b = \<zero>"
paulson@14883
    72
paulson@14883
    73
paulson@14883
    74
subsection {* Basic Properties *}
paulson@14883
    75
paulson@14883
    76
lemma (in abelian_monoid) a_monoid:
paulson@14883
    77
     "monoid (<carrier(G), add_field(G), zero(G), 0>)"
paulson@14883
    78
apply (insert a_comm_monoid) 
paulson@14883
    79
apply (simp add: comm_monoid_def) 
paulson@14883
    80
done
paulson@14883
    81
paulson@14883
    82
lemma (in abelian_group) a_group:
paulson@14883
    83
     "group (<carrier(G), add_field(G), zero(G), 0>)"
paulson@14883
    84
apply (insert a_comm_group) 
paulson@14883
    85
apply (simp add: comm_group_def group_def) 
paulson@14883
    86
done
paulson@14883
    87
paulson@14883
    88
paulson@14883
    89
lemma (in abelian_monoid) l_zero [simp]:
paulson@14883
    90
     "x \<in> carrier(G) \<Longrightarrow> \<zero> \<oplus> x = x"
paulson@14883
    91
apply (insert monoid.l_one [OF a_monoid])
paulson@14883
    92
apply (simp add: ring_add_def) 
paulson@14883
    93
done
paulson@14883
    94
paulson@14883
    95
lemma (in abelian_monoid) zero_closed [intro, simp]:
paulson@14883
    96
     "\<zero> \<in> carrier(G)"
paulson@14883
    97
by (rule monoid.one_closed [OF a_monoid, simplified])
paulson@14883
    98
paulson@14883
    99
lemma (in abelian_group) a_inv_closed [intro, simp]:
paulson@14883
   100
     "x \<in> carrier(G) \<Longrightarrow> \<ominus> x \<in> carrier(G)"
paulson@14883
   101
by (simp add: a_inv_def  group.inv_closed [OF a_group, simplified])
paulson@14883
   102
paulson@14883
   103
lemma (in abelian_monoid) a_closed [intro, simp]:
paulson@14883
   104
     "[| x \<in> carrier(G); y \<in> carrier(G) |] ==> x \<oplus> y \<in> carrier(G)"
paulson@14883
   105
by (rule monoid.m_closed [OF a_monoid, 
paulson@14883
   106
                  simplified, simplified ring_add_def [symmetric]])
paulson@14883
   107
paulson@14883
   108
lemma (in abelian_group) minus_closed [intro, simp]:
paulson@14883
   109
     "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<ominus> y \<in> carrier(G)"
paulson@14883
   110
by (simp add: minus_def)
paulson@14883
   111
paulson@14883
   112
lemma (in abelian_group) a_l_cancel [simp]:
paulson@14883
   113
     "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> 
paulson@14883
   114
      \<Longrightarrow> (x \<oplus> y = x \<oplus> z) <-> (y = z)"
paulson@14883
   115
by (rule group.l_cancel [OF a_group, 
paulson@14883
   116
             simplified, simplified ring_add_def [symmetric]])
paulson@14883
   117
paulson@14883
   118
lemma (in abelian_group) a_r_cancel [simp]:
paulson@14883
   119
     "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> 
paulson@14883
   120
      \<Longrightarrow> (y \<oplus> x = z \<oplus> x) <-> (y = z)"
paulson@14883
   121
by (rule group.r_cancel [OF a_group, simplified, simplified ring_add_def [symmetric]])
paulson@14883
   122
paulson@14883
   123
lemma (in abelian_monoid) a_assoc:
paulson@14883
   124
  "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> 
paulson@14883
   125
   \<Longrightarrow> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
paulson@14883
   126
by (rule monoid.m_assoc [OF a_monoid, simplified, simplified ring_add_def [symmetric]])
paulson@14883
   127
paulson@14883
   128
lemma (in abelian_group) l_neg:
paulson@14883
   129
     "x \<in> carrier(G) \<Longrightarrow> \<ominus> x \<oplus> x = \<zero>"
paulson@14883
   130
by (simp add: a_inv_def
paulson@14883
   131
     group.l_inv [OF a_group, simplified, simplified ring_add_def [symmetric]])
paulson@14883
   132
paulson@14883
   133
lemma (in abelian_monoid) a_comm:
paulson@14883
   134
     "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<oplus> y = y \<oplus> x"
paulson@14883
   135
by (rule comm_monoid.m_comm [OF a_comm_monoid,
paulson@14883
   136
    simplified, simplified ring_add_def [symmetric]])
paulson@14883
   137
paulson@14883
   138
lemma (in abelian_monoid) a_lcomm:
paulson@14883
   139
     "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> 
paulson@14883
   140
      \<Longrightarrow> x \<oplus> (y \<oplus> z) = y \<oplus> (x \<oplus> z)"
paulson@14883
   141
by (rule comm_monoid.m_lcomm [OF a_comm_monoid,
paulson@14883
   142
    simplified, simplified ring_add_def [symmetric]])
paulson@14883
   143
paulson@14883
   144
lemma (in abelian_monoid) r_zero [simp]:
paulson@14883
   145
     "x \<in> carrier(G) \<Longrightarrow> x \<oplus> \<zero> = x"
paulson@14883
   146
  using monoid.r_one [OF a_monoid]
paulson@14883
   147
  by (simp add: ring_add_def [symmetric])
paulson@14883
   148
paulson@14883
   149
lemma (in abelian_group) r_neg:
paulson@14883
   150
     "x \<in> carrier(G) \<Longrightarrow> x \<oplus> (\<ominus> x) = \<zero>"
paulson@14883
   151
  using group.r_inv [OF a_group]
paulson@14883
   152
  by (simp add: a_inv_def ring_add_def [symmetric])
paulson@14883
   153
paulson@14883
   154
lemma (in abelian_group) minus_zero [simp]:
paulson@14883
   155
     "\<ominus> \<zero> = \<zero>"
paulson@14883
   156
  by (simp add: a_inv_def
paulson@14883
   157
    group.inv_one [OF a_group, simplified ])
paulson@14883
   158
paulson@14883
   159
lemma (in abelian_group) minus_minus [simp]:
paulson@14883
   160
     "x \<in> carrier(G) \<Longrightarrow> \<ominus> (\<ominus> x) = x"
paulson@14883
   161
  using group.inv_inv [OF a_group, simplified]
paulson@14883
   162
  by (simp add: a_inv_def)
paulson@14883
   163
paulson@14883
   164
lemma (in abelian_group) minus_add:
paulson@14883
   165
     "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> \<ominus> (x \<oplus> y) = \<ominus> x \<oplus> \<ominus> y"
paulson@14883
   166
  using comm_group.inv_mult [OF a_comm_group]
paulson@14883
   167
  by (simp add: a_inv_def ring_add_def [symmetric])
paulson@14883
   168
paulson@14883
   169
lemmas (in abelian_monoid) a_ac = a_assoc a_comm a_lcomm
paulson@14883
   170
paulson@14883
   171
text {* 
paulson@14883
   172
  The following proofs are from Jacobson, Basic Algebra I, pp.~88--89
paulson@14883
   173
*}
paulson@14883
   174
wenzelm@21233
   175
context ring
wenzelm@21233
   176
begin
wenzelm@21233
   177
wenzelm@21233
   178
lemma l_null [simp]: "x \<in> carrier(R) \<Longrightarrow> \<zero> \<cdot> x = \<zero>"
paulson@14883
   179
proof -
paulson@14883
   180
  assume R: "x \<in> carrier(R)"
paulson@14883
   181
  then have "\<zero> \<cdot> x \<oplus> \<zero> \<cdot> x = (\<zero> \<oplus> \<zero>) \<cdot> x"
paulson@14883
   182
    by (blast intro: l_distr [THEN sym]) 
paulson@14883
   183
  also from R have "... = \<zero> \<cdot> x \<oplus> \<zero>" by simp
paulson@14883
   184
  finally have "\<zero> \<cdot> x \<oplus> \<zero> \<cdot> x = \<zero> \<cdot> x \<oplus> \<zero>" .
paulson@14883
   185
  with R show ?thesis by (simp del: r_zero)
paulson@14883
   186
qed
paulson@14883
   187
wenzelm@21233
   188
lemma r_null [simp]: "x \<in> carrier(R) \<Longrightarrow> x \<cdot> \<zero> = \<zero>"
paulson@14883
   189
proof -
paulson@14883
   190
  assume R: "x \<in> carrier(R)"
paulson@14883
   191
  then have "x \<cdot> \<zero> \<oplus> x \<cdot> \<zero> = x \<cdot> (\<zero> \<oplus> \<zero>)"
paulson@14883
   192
    by (simp add: r_distr del: l_zero r_zero)
paulson@14883
   193
  also from R have "... = x \<cdot> \<zero> \<oplus> \<zero>" by simp
paulson@14883
   194
  finally have "x \<cdot> \<zero> \<oplus> x \<cdot> \<zero> = x \<cdot> \<zero> \<oplus> \<zero>" .
paulson@14883
   195
  with R show ?thesis by (simp del: r_zero)
paulson@14883
   196
qed
paulson@14883
   197
wenzelm@21233
   198
lemma l_minus:
paulson@14883
   199
  "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> \<ominus> x \<cdot> y = \<ominus> (x \<cdot> y)"
paulson@14883
   200
proof -
paulson@14883
   201
  assume R: "x \<in> carrier(R)" "y \<in> carrier(R)"
paulson@14883
   202
  then have "(\<ominus> x) \<cdot> y \<oplus> x \<cdot> y = (\<ominus> x \<oplus> x) \<cdot> y" by (simp add: l_distr)
paulson@14883
   203
  also from R have "... = \<zero>" by (simp add: l_neg l_null)
paulson@14883
   204
  finally have "(\<ominus> x) \<cdot> y \<oplus> x \<cdot> y = \<zero>" .
paulson@14883
   205
  with R have "(\<ominus> x) \<cdot> y \<oplus> x \<cdot> y \<oplus> \<ominus> (x \<cdot> y) = \<zero> \<oplus> \<ominus> (x \<cdot> y)" by simp
paulson@14883
   206
  with R show ?thesis by (simp add: a_assoc r_neg)
paulson@14883
   207
qed
paulson@14883
   208
wenzelm@21233
   209
lemma r_minus:
paulson@14883
   210
  "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<cdot> \<ominus> y = \<ominus> (x \<cdot> y)"
paulson@14883
   211
proof -
paulson@14883
   212
  assume R: "x \<in> carrier(R)" "y \<in> carrier(R)"
paulson@14883
   213
  then have "x \<cdot> (\<ominus> y) \<oplus> x \<cdot> y = x \<cdot> (\<ominus> y \<oplus> y)" by (simp add: r_distr)
paulson@14883
   214
  also from R have "... = \<zero>" by (simp add: l_neg r_null)
paulson@14883
   215
  finally have "x \<cdot> (\<ominus> y) \<oplus> x \<cdot> y = \<zero>" .
paulson@14883
   216
  with R have "x \<cdot> (\<ominus> y) \<oplus> x \<cdot> y \<oplus> \<ominus> (x \<cdot> y) = \<zero> \<oplus> \<ominus> (x \<cdot> y)" by simp
paulson@14883
   217
  with R show ?thesis by (simp add: a_assoc r_neg)
paulson@14883
   218
qed
paulson@14883
   219
wenzelm@21233
   220
lemma minus_eq:
paulson@14883
   221
  "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus> y = x \<oplus> \<ominus> y"
paulson@14883
   222
  by (simp only: minus_def)
paulson@14883
   223
wenzelm@21233
   224
end
wenzelm@21233
   225
paulson@14883
   226
paulson@14883
   227
subsection {* Morphisms *}
paulson@14883
   228
wenzelm@21233
   229
definition
wenzelm@21404
   230
  ring_hom :: "[i,i] => i" where
wenzelm@21233
   231
  "ring_hom(R,S) ==
paulson@14883
   232
    {h \<in> carrier(R) -> carrier(S).
paulson@14883
   233
      (\<forall>x y. x \<in> carrier(R) & y \<in> carrier(R) -->
paulson@14883
   234
        h ` (x \<cdot>\<^bsub>R\<^esub> y) = (h ` x) \<cdot>\<^bsub>S\<^esub> (h ` y) &
paulson@14883
   235
        h ` (x \<oplus>\<^bsub>R\<^esub> y) = (h ` x) \<oplus>\<^bsub>S\<^esub> (h ` y)) &
paulson@14883
   236
      h ` \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>}"
paulson@14883
   237
paulson@14883
   238
lemma ring_hom_memI:
paulson@14883
   239
  assumes hom_type: "h \<in> carrier(R) \<rightarrow> carrier(S)"
paulson@14883
   240
    and hom_mult: "\<And>x y. \<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow>
paulson@14883
   241
      h ` (x \<cdot>\<^bsub>R\<^esub> y) = (h ` x) \<cdot>\<^bsub>S\<^esub> (h ` y)"
paulson@14883
   242
    and hom_add: "\<And>x y. \<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow>
paulson@14883
   243
      h ` (x \<oplus>\<^bsub>R\<^esub> y) = (h ` x) \<oplus>\<^bsub>S\<^esub> (h ` y)"
paulson@14883
   244
    and hom_one: "h ` \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>"
paulson@14883
   245
  shows "h \<in> ring_hom(R,S)"
paulson@14883
   246
by (auto simp add: ring_hom_def prems)
paulson@14883
   247
paulson@14883
   248
lemma ring_hom_closed:
paulson@14883
   249
     "\<lbrakk>h \<in> ring_hom(R,S); x \<in> carrier(R)\<rbrakk> \<Longrightarrow> h ` x \<in> carrier(S)"
paulson@14883
   250
by (auto simp add: ring_hom_def)
paulson@14883
   251
paulson@14883
   252
lemma ring_hom_mult:
paulson@14883
   253
     "\<lbrakk>h \<in> ring_hom(R,S); x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> 
paulson@14883
   254
      \<Longrightarrow> h ` (x \<cdot>\<^bsub>R\<^esub> y) = (h ` x) \<cdot>\<^bsub>S\<^esub> (h ` y)"
paulson@14883
   255
by (simp add: ring_hom_def)
paulson@14883
   256
paulson@14883
   257
lemma ring_hom_add:
paulson@14883
   258
     "\<lbrakk>h \<in> ring_hom(R,S); x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> 
paulson@14883
   259
      \<Longrightarrow> h ` (x \<oplus>\<^bsub>R\<^esub> y) = (h ` x) \<oplus>\<^bsub>S\<^esub> (h ` y)"
paulson@14883
   260
by (simp add: ring_hom_def)
paulson@14883
   261
paulson@14883
   262
lemma ring_hom_one: "h \<in> ring_hom(R,S) \<Longrightarrow> h ` \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>"
paulson@14883
   263
by (simp add: ring_hom_def)
paulson@14883
   264
ballarin@29223
   265
locale ring_hom_cring = R: cring R + S: cring S
ballarin@29223
   266
  for R (structure) and S (structure) and h +
paulson@14883
   267
  assumes homh [simp, intro]: "h \<in> ring_hom(R,S)"
paulson@14883
   268
  notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
paulson@14883
   269
    and hom_mult [simp] = ring_hom_mult [OF homh]
paulson@14883
   270
    and hom_add [simp] = ring_hom_add [OF homh]
paulson@14883
   271
    and hom_one [simp] = ring_hom_one [OF homh]
paulson@14883
   272
paulson@14883
   273
lemma (in ring_hom_cring) hom_zero [simp]:
paulson@14883
   274
     "h ` \<zero>\<^bsub>R\<^esub> = \<zero>\<^bsub>S\<^esub>"
paulson@14883
   275
proof -
paulson@14883
   276
  have "h ` \<zero>\<^bsub>R\<^esub> \<oplus>\<^bsub>S\<^esub> h ` \<zero> = h ` \<zero>\<^bsub>R\<^esub> \<oplus>\<^bsub>S\<^esub> \<zero>\<^bsub>S\<^esub>"
paulson@14883
   277
    by (simp add: hom_add [symmetric] del: hom_add)
paulson@14883
   278
  then show ?thesis by (simp del: S.r_zero)
paulson@14883
   279
qed
paulson@14883
   280
paulson@14883
   281
lemma (in ring_hom_cring) hom_a_inv [simp]:
paulson@14883
   282
     "x \<in> carrier(R) \<Longrightarrow> h ` (\<ominus>\<^bsub>R\<^esub> x) = \<ominus>\<^bsub>S\<^esub> h ` x"
paulson@14883
   283
proof -
paulson@14883
   284
  assume R: "x \<in> carrier(R)"
paulson@14883
   285
  then have "h ` x \<oplus>\<^bsub>S\<^esub> h ` (\<ominus> x) = h ` x \<oplus>\<^bsub>S\<^esub> (\<ominus>\<^bsub>S\<^esub> (h ` x))"
paulson@14883
   286
    by (simp add: hom_add [symmetric] R.r_neg S.r_neg del: hom_add)
paulson@14883
   287
  with R show ?thesis by simp
paulson@14883
   288
qed
paulson@14883
   289
paulson@14883
   290
lemma (in ring) id_ring_hom [simp]: "id(carrier(R)) \<in> ring_hom(R,R)"
paulson@14883
   291
apply (rule ring_hom_memI)  
paulson@14883
   292
apply (auto simp add: id_type) 
paulson@14883
   293
done
paulson@14883
   294
paulson@14883
   295
end