src/HOL/Algebra/Ring.thy
author paulson <lp15@cam.ac.uk>
Sat Jun 30 15:44:04 2018 +0100 (12 months ago)
changeset 68551 b680e74eb6f2
parent 68517 6b5f15387353
child 68552 391e89e03eef
permissions -rw-r--r--
More on Algebra by Paulo and Martin
wenzelm@41959
     1
(*  Title:      HOL/Algebra/Ring.thy
wenzelm@35849
     2
    Author:     Clemens Ballarin, started 9 December 1996
wenzelm@35849
     3
    Copyright:  Clemens Ballarin
ballarin@20318
     4
*)
ballarin@20318
     5
haftmann@28823
     6
theory Ring
haftmann@28823
     7
imports FiniteProduct
wenzelm@35847
     8
begin
ballarin@20318
     9
wenzelm@61382
    10
section \<open>The Algebraic Hierarchy of Rings\<close>
ballarin@27717
    11
wenzelm@61382
    12
subsection \<open>Abelian Groups\<close>
ballarin@20318
    13
ballarin@20318
    14
record 'a ring = "'a monoid" +
ballarin@20318
    15
  zero :: 'a ("\<zero>\<index>")
lp15@68443
    16
  add :: "['a, 'a] \<Rightarrow> 'a" (infixl "\<oplus>\<index>" 65)
lp15@68443
    17
lp15@68443
    18
abbreviation
lp15@68443
    19
  add_monoid :: "('a, 'm) ring_scheme \<Rightarrow> ('a, 'm) monoid_scheme"
lp15@68443
    20
  where "add_monoid R \<equiv> \<lparr> carrier = carrier R, mult = add R, one = zero R, \<dots> = (undefined :: 'm) \<rparr>"
ballarin@20318
    21
wenzelm@61382
    22
text \<open>Derived operations.\<close>
ballarin@20318
    23
wenzelm@35847
    24
definition
lp15@68443
    25
  a_inv :: "[('a, 'm) ring_scheme, 'a ] \<Rightarrow> 'a" ("\<ominus>\<index> _" [81] 80)
lp15@68443
    26
  where "a_inv R = m_inv (add_monoid R)"
lp15@68443
    27
wenzelm@35847
    28
definition
nipkow@67398
    29
  a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" ("(_ \<ominus>\<index> _)" [65,66] 65)
lp15@68445
    30
  where "x \<ominus>\<^bsub>R\<^esub> y = x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
lp15@68443
    31
lp15@68443
    32
definition
lp15@68443
    33
  add_pow :: "[_, ('b :: semiring_1), 'a] \<Rightarrow> 'a" ("[_] \<cdot>\<index> _" [81, 81] 80)
lp15@68443
    34
  where "add_pow R k a = pow (add_monoid R) a k"
ballarin@20318
    35
ballarin@20318
    36
locale abelian_monoid =
ballarin@20318
    37
  fixes G (structure)
ballarin@20318
    38
  assumes a_comm_monoid:
lp15@68443
    39
     "comm_monoid (add_monoid G)"
ballarin@20318
    40
ballarin@41433
    41
definition
lp15@68443
    42
  finsum :: "[('b, 'm) ring_scheme, 'a \<Rightarrow> 'b, 'a set] \<Rightarrow> 'b" where
lp15@68443
    43
  "finsum G = finprod (add_monoid G)"
ballarin@20318
    44
ballarin@41433
    45
syntax
lp15@68443
    46
  "_finsum" :: "index \<Rightarrow> idt \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"
ballarin@41433
    47
      ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
ballarin@41433
    48
translations
lp15@68443
    49
  "\<Oplus>\<^bsub>G\<^esub>i\<in>A. b" \<rightleftharpoons> "CONST finsum G (\<lambda>i. b) A"
wenzelm@63167
    50
  \<comment> \<open>Beware of argument permutation!\<close>
ballarin@41433
    51
ballarin@20318
    52
ballarin@20318
    53
locale abelian_group = abelian_monoid +
ballarin@20318
    54
  assumes a_comm_group:
lp15@68443
    55
     "comm_group (add_monoid G)"
ballarin@20318
    56
ballarin@20318
    57
wenzelm@61382
    58
subsection \<open>Basic Properties\<close>
ballarin@20318
    59
ballarin@20318
    60
lemma abelian_monoidI:
ballarin@20318
    61
  fixes R (structure)
lp15@68443
    62
  assumes "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> x \<oplus> y \<in> carrier R"
lp15@68443
    63
      and "\<zero> \<in> carrier R"
lp15@68443
    64
      and "\<And>x y z. \<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
lp15@68443
    65
      and "\<And>x. x \<in> carrier R \<Longrightarrow> \<zero> \<oplus> x = x"
lp15@68443
    66
      and "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> x \<oplus> y = y \<oplus> x"
ballarin@20318
    67
  shows "abelian_monoid R"
ballarin@27714
    68
  by (auto intro!: abelian_monoid.intro comm_monoidI intro: assms)
ballarin@20318
    69
lp15@68443
    70
lemma abelian_monoidE:
lp15@68443
    71
  fixes R (structure)
lp15@68443
    72
  assumes "abelian_monoid R"
lp15@68443
    73
  shows "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> x \<oplus> y \<in> carrier R"
lp15@68443
    74
    and "\<zero> \<in> carrier R"
lp15@68443
    75
    and "\<And>x y z. \<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
lp15@68443
    76
    and "\<And>x. x \<in> carrier R \<Longrightarrow> \<zero> \<oplus> x = x"
lp15@68443
    77
    and "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> x \<oplus> y = y \<oplus> x"
lp15@68443
    78
  using assms unfolding abelian_monoid_def comm_monoid_def comm_monoid_axioms_def monoid_def by auto
lp15@68443
    79
ballarin@20318
    80
lemma abelian_groupI:
ballarin@20318
    81
  fixes R (structure)
lp15@68443
    82
  assumes "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> x \<oplus> y \<in> carrier R"
lp15@68443
    83
      and "\<zero> \<in> carrier R"
lp15@68443
    84
      and "\<And>x y z. \<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
lp15@68443
    85
      and "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> x \<oplus> y = y \<oplus> x"
lp15@68443
    86
      and "\<And>x. x \<in> carrier R \<Longrightarrow> \<zero> \<oplus> x = x"
lp15@68443
    87
      and "\<And>x. x \<in> carrier R \<Longrightarrow> \<exists>y \<in> carrier R. y \<oplus> x = \<zero>"
ballarin@20318
    88
  shows "abelian_group R"
ballarin@20318
    89
  by (auto intro!: abelian_group.intro abelian_monoidI
ballarin@20318
    90
      abelian_group_axioms.intro comm_monoidI comm_groupI
ballarin@27714
    91
    intro: assms)
ballarin@20318
    92
lp15@68443
    93
lemma abelian_groupE:
lp15@68443
    94
  fixes R (structure)
lp15@68443
    95
  assumes "abelian_group R"
lp15@68443
    96
  shows "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> x \<oplus> y \<in> carrier R"
lp15@68443
    97
    and "\<zero> \<in> carrier R"
lp15@68443
    98
    and "\<And>x y z. \<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
lp15@68443
    99
    and "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> x \<oplus> y = y \<oplus> x"
lp15@68443
   100
    and "\<And>x. x \<in> carrier R \<Longrightarrow> \<zero> \<oplus> x = x"
lp15@68443
   101
    and "\<And>x. x \<in> carrier R \<Longrightarrow> \<exists>y \<in> carrier R. y \<oplus> x = \<zero>"
lp15@68443
   102
  using abelian_group.a_comm_group assms comm_groupE by fastforce+
lp15@68443
   103
ballarin@20318
   104
lemma (in abelian_monoid) a_monoid:
lp15@68443
   105
  "monoid (add_monoid G)"
lp15@68517
   106
by (rule comm_monoid.axioms, rule a_comm_monoid)
ballarin@20318
   107
ballarin@20318
   108
lemma (in abelian_group) a_group:
lp15@68443
   109
  "group (add_monoid G)"
ballarin@20318
   110
  by (simp add: group_def a_monoid)
ballarin@20318
   111
    (simp add: comm_group.axioms group.axioms a_comm_group)
ballarin@20318
   112
ballarin@20318
   113
lemmas monoid_record_simps = partial_object.simps monoid.simps
ballarin@20318
   114
wenzelm@61382
   115
text \<open>Transfer facts from multiplicative structures via interpretation.\<close>
ballarin@20318
   116
ballarin@41433
   117
sublocale abelian_monoid <
lp15@68443
   118
       add: monoid "(add_monoid G)"
lp15@68443
   119
  rewrites "carrier (add_monoid G) = carrier G"
lp15@68443
   120
       and "mult    (add_monoid G) = add G"
lp15@68443
   121
       and "one     (add_monoid G) = zero G"
lp15@68443
   122
       and "(\<lambda>a k. pow (add_monoid G) a k) = (\<lambda>a k. add_pow G k a)"
lp15@68443
   123
  by (rule a_monoid) (auto simp add: add_pow_def)
ballarin@20318
   124
lp15@68443
   125
context abelian_monoid
lp15@68443
   126
begin
ballarin@27933
   127
lp15@68517
   128
lemmas a_closed = add.m_closed
ballarin@41433
   129
lemmas zero_closed = add.one_closed
ballarin@41433
   130
lemmas a_assoc = add.m_assoc
ballarin@41433
   131
lemmas l_zero = add.l_one
ballarin@41433
   132
lemmas r_zero = add.r_one
ballarin@41433
   133
lemmas minus_unique = add.inv_unique
ballarin@20318
   134
ballarin@41433
   135
end
ballarin@20318
   136
ballarin@41433
   137
sublocale abelian_monoid <
lp15@68443
   138
  add: comm_monoid "(add_monoid G)"
lp15@68443
   139
  rewrites "carrier (add_monoid G) = carrier G"
lp15@68443
   140
       and "mult    (add_monoid G) = add G"
lp15@68443
   141
       and "one     (add_monoid G) = zero G"
lp15@68443
   142
       and "finprod (add_monoid G) = finsum G"
lp15@68443
   143
       and "pow     (add_monoid G) = (\<lambda>a k. add_pow G k a)"
lp15@68443
   144
  by (rule a_comm_monoid) (auto simp: finsum_def add_pow_def)
ballarin@20318
   145
ballarin@41433
   146
context abelian_monoid begin
ballarin@20318
   147
ballarin@41433
   148
lemmas a_comm = add.m_comm
ballarin@41433
   149
lemmas a_lcomm = add.m_lcomm
ballarin@41433
   150
lemmas a_ac = a_assoc a_comm a_lcomm
ballarin@20318
   151
ballarin@41433
   152
lemmas finsum_empty = add.finprod_empty
ballarin@41433
   153
lemmas finsum_insert = add.finprod_insert
ballarin@41433
   154
lemmas finsum_zero = add.finprod_one
ballarin@41433
   155
lemmas finsum_closed = add.finprod_closed
ballarin@41433
   156
lemmas finsum_Un_Int = add.finprod_Un_Int
ballarin@41433
   157
lemmas finsum_Un_disjoint = add.finprod_Un_disjoint
ballarin@41433
   158
lemmas finsum_addf = add.finprod_multf
ballarin@41433
   159
lemmas finsum_cong' = add.finprod_cong'
ballarin@41433
   160
lemmas finsum_0 = add.finprod_0
ballarin@41433
   161
lemmas finsum_Suc = add.finprod_Suc
ballarin@41433
   162
lemmas finsum_Suc2 = add.finprod_Suc2
rene@60112
   163
lemmas finsum_infinite = add.finprod_infinite
ballarin@20318
   164
ballarin@41433
   165
lemmas finsum_cong = add.finprod_cong
wenzelm@61382
   166
text \<open>Usually, if this rule causes a failed congruence proof error,
wenzelm@63167
   167
   the reason is that the premise \<open>g \<in> B \<rightarrow> carrier G\<close> cannot be shown.
wenzelm@61382
   168
   Adding @{thm [source] Pi_def} to the simpset is often useful.\<close>
ballarin@20318
   169
ballarin@41433
   170
lemmas finsum_reindex = add.finprod_reindex
ballarin@27699
   171
nipkow@67341
   172
(* The following would be wrong.  Needed is the equivalent of [^] for addition,
ballarin@27699
   173
  or indeed the canonical embedding from Nat into the monoid.
ballarin@27699
   174
ballarin@27933
   175
lemma finsum_const:
ballarin@27699
   176
  assumes fin [simp]: "finite A"
ballarin@27699
   177
      and a [simp]: "a : carrier G"
nipkow@67341
   178
    shows "finsum G (%x. a) A = a [^] card A"
ballarin@27699
   179
  using fin apply induct
ballarin@27699
   180
  apply force
ballarin@27699
   181
  apply (subst finsum_insert)
ballarin@27699
   182
  apply auto
ballarin@27699
   183
  apply (force simp add: Pi_def)
ballarin@27699
   184
  apply (subst m_comm)
ballarin@27699
   185
  apply auto
ballarin@27699
   186
done
ballarin@27699
   187
*)
ballarin@27699
   188
ballarin@41433
   189
lemmas finsum_singleton = add.finprod_singleton
ballarin@27933
   190
ballarin@27933
   191
end
ballarin@27933
   192
ballarin@41433
   193
sublocale abelian_group <
lp15@68443
   194
        add: group "(add_monoid G)"
lp15@68443
   195
  rewrites "carrier (add_monoid G) = carrier G"
lp15@68443
   196
       and "mult    (add_monoid G) = add G"
lp15@68443
   197
       and "one     (add_monoid G) = zero G"
lp15@68443
   198
       and "m_inv   (add_monoid G) = a_inv G"
lp15@68443
   199
       and "pow     (add_monoid G) = (\<lambda>a k. add_pow G k a)"
lp15@68443
   200
  by (rule a_group) (auto simp: m_inv_def a_inv_def add_pow_def)
ballarin@41433
   201
wenzelm@55926
   202
context abelian_group
wenzelm@55926
   203
begin
ballarin@41433
   204
ballarin@41433
   205
lemmas a_inv_closed = add.inv_closed
ballarin@41433
   206
ballarin@41433
   207
lemma minus_closed [intro, simp]:
ballarin@41433
   208
  "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<ominus> y \<in> carrier G"
ballarin@41433
   209
  by (simp add: a_minus_def)
ballarin@41433
   210
ballarin@41433
   211
lemmas l_neg = add.l_inv [simp del]
ballarin@41433
   212
lemmas r_neg = add.r_inv [simp del]
ballarin@41433
   213
lemmas minus_minus = add.inv_inv
ballarin@41433
   214
lemmas a_inv_inj = add.inv_inj
ballarin@41433
   215
lemmas minus_equality = add.inv_equality
ballarin@41433
   216
ballarin@41433
   217
end
ballarin@41433
   218
ballarin@41433
   219
sublocale abelian_group <
lp15@68443
   220
   add: comm_group "(add_monoid G)"
lp15@68443
   221
  rewrites "carrier (add_monoid G) = carrier G"
lp15@68443
   222
       and "mult    (add_monoid G) = add G"
lp15@68443
   223
       and "one     (add_monoid G) = zero G"
lp15@68443
   224
       and "m_inv   (add_monoid G) = a_inv G"
lp15@68443
   225
       and "finprod (add_monoid G) = finsum G"
lp15@68443
   226
       and "pow     (add_monoid G) = (\<lambda>a k. add_pow G k a)"
lp15@68443
   227
  by (rule a_comm_group) (auto simp: m_inv_def a_inv_def finsum_def add_pow_def)
ballarin@41433
   228
ballarin@41433
   229
lemmas (in abelian_group) minus_add = add.inv_mult
lp15@68517
   230
wenzelm@63167
   231
text \<open>Derive an \<open>abelian_group\<close> from a \<open>comm_group\<close>\<close>
ballarin@41433
   232
ballarin@41433
   233
lemma comm_group_abelian_groupI:
ballarin@41433
   234
  fixes G (structure)
lp15@68443
   235
  assumes cg: "comm_group (add_monoid G)"
ballarin@41433
   236
  shows "abelian_group G"
ballarin@41433
   237
proof -
lp15@68443
   238
  interpret comm_group "(add_monoid G)"
ballarin@41433
   239
    by (rule cg)
ballarin@41433
   240
  show "abelian_group G" ..
ballarin@41433
   241
qed
ballarin@41433
   242
ballarin@20318
   243
wenzelm@61382
   244
subsection \<open>Rings: Basic Definitions\<close>
ballarin@20318
   245
lp15@68443
   246
locale semiring = abelian_monoid (* for add *) R + monoid (* for mult *) R for R (structure) +
lp15@68443
   247
  assumes l_distr: "\<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
lp15@68443
   248
      and r_distr: "\<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
lp15@68443
   249
      and l_null[simp]: "x \<in> carrier R \<Longrightarrow> \<zero> \<otimes> x = \<zero>"
lp15@68443
   250
      and r_null[simp]: "x \<in> carrier R \<Longrightarrow> x \<otimes> \<zero> = \<zero>"
rene@59851
   251
lp15@68443
   252
locale ring = abelian_group (* for add *) R + monoid (* for mult *) R for R (structure) +
lp15@68443
   253
  assumes "\<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
lp15@68443
   254
      and "\<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
ballarin@20318
   255
lp15@68443
   256
locale cring = ring + comm_monoid (* for mult *) R
ballarin@20318
   257
ballarin@20318
   258
locale "domain" = cring +
wenzelm@67091
   259
  assumes one_not_zero [simp]: "\<one> \<noteq> \<zero>"
lp15@68443
   260
      and integral: "\<lbrakk> a \<otimes> b = \<zero>; a \<in> carrier R; b \<in> carrier R \<rbrakk> \<Longrightarrow> a = \<zero> \<or> b = \<zero>"
ballarin@20318
   261
ballarin@20318
   262
locale field = "domain" +
ballarin@20318
   263
  assumes field_Units: "Units R = carrier R - {\<zero>}"
ballarin@20318
   264
ballarin@20318
   265
wenzelm@61382
   266
subsection \<open>Rings\<close>
ballarin@20318
   267
ballarin@20318
   268
lemma ringI:
ballarin@20318
   269
  fixes R (structure)
lp15@68443
   270
  assumes "abelian_group R"
lp15@68443
   271
      and "monoid R"
lp15@68443
   272
      and "\<And>x y z. \<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
lp15@68443
   273
      and "\<And>x y z. \<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
ballarin@20318
   274
  shows "ring R"
ballarin@20318
   275
  by (auto intro: ring.intro
ballarin@27714
   276
    abelian_group.axioms ring_axioms.intro assms)
ballarin@20318
   277
lp15@68443
   278
lemma ringE:
lp15@68443
   279
  fixes R (structure)
lp15@68443
   280
  assumes "ring R"
lp15@68443
   281
  shows "abelian_group R"
lp15@68443
   282
    and "monoid R"
lp15@68443
   283
    and "\<And>x y z. \<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
lp15@68443
   284
    and "\<And>x y z. \<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
lp15@68443
   285
  using assms unfolding ring_def ring_axioms_def by auto
lp15@68443
   286
ballarin@41433
   287
context ring begin
ballarin@41433
   288
wenzelm@46721
   289
lemma is_abelian_group: "abelian_group R" ..
ballarin@20318
   290
wenzelm@46721
   291
lemma is_monoid: "monoid R"
ballarin@20318
   292
  by (auto intro!: monoidI m_assoc)
ballarin@20318
   293
wenzelm@46721
   294
lemma is_ring: "ring R"
wenzelm@26202
   295
  by (rule ring_axioms)
ballarin@20318
   296
ballarin@41433
   297
end
lp15@68443
   298
thm monoid_record_simps
ballarin@20318
   299
lemmas ring_record_simps = monoid_record_simps ring.simps
ballarin@20318
   300
ballarin@20318
   301
lemma cringI:
ballarin@20318
   302
  fixes R (structure)
ballarin@20318
   303
  assumes abelian_group: "abelian_group R"
ballarin@20318
   304
    and comm_monoid: "comm_monoid R"
lp15@68443
   305
    and l_distr: "\<And>x y z. \<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow>
lp15@68443
   306
                            (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
ballarin@20318
   307
  shows "cring R"
wenzelm@23350
   308
proof (intro cring.intro ring.intro)
wenzelm@23350
   309
  show "ring_axioms R"
wenzelm@63167
   310
    \<comment> \<open>Right-distributivity follows from left-distributivity and
wenzelm@61382
   311
          commutativity.\<close>
wenzelm@23350
   312
  proof (rule ring_axioms.intro)
wenzelm@23350
   313
    fix x y z
wenzelm@23350
   314
    assume R: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
wenzelm@23350
   315
    note [simp] = comm_monoid.axioms [OF comm_monoid]
wenzelm@23350
   316
      abelian_group.axioms [OF abelian_group]
wenzelm@23350
   317
      abelian_monoid.a_closed
lp15@68517
   318
wenzelm@23350
   319
    from R have "z \<otimes> (x \<oplus> y) = (x \<oplus> y) \<otimes> z"
wenzelm@23350
   320
      by (simp add: comm_monoid.m_comm [OF comm_monoid.intro])
wenzelm@23350
   321
    also from R have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
wenzelm@23350
   322
    also from R have "... = z \<otimes> x \<oplus> z \<otimes> y"
wenzelm@23350
   323
      by (simp add: comm_monoid.m_comm [OF comm_monoid.intro])
wenzelm@23350
   324
    finally show "z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y" .
wenzelm@23350
   325
  qed (rule l_distr)
wenzelm@23350
   326
qed (auto intro: cring.intro
ballarin@27714
   327
  abelian_group.axioms comm_monoid.axioms ring_axioms.intro assms)
ballarin@20318
   328
lp15@68443
   329
lemma cringE:
lp15@68443
   330
  fixes R (structure)
lp15@68443
   331
  assumes "cring R"
lp15@68443
   332
  shows "comm_monoid R"
lp15@68443
   333
    and "\<And>x y z. \<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
lp15@68443
   334
  using assms cring_def apply auto by (simp add: assms cring.axioms(1) ringE(3))
lp15@68443
   335
ballarin@20318
   336
lemma (in cring) is_cring:
wenzelm@26202
   337
  "cring R" by (rule cring_axioms)
wenzelm@23350
   338
lp15@68445
   339
lemma (in ring) minus_zero [simp]: "\<ominus> \<zero> = \<zero>"
lp15@68445
   340
  by (simp add: a_inv_def)
ballarin@20318
   341
wenzelm@61382
   342
subsubsection \<open>Normaliser for Rings\<close>
ballarin@20318
   343
lp15@68443
   344
lemma (in abelian_group) r_neg1:
lp15@68443
   345
  "\<lbrakk> x \<in> carrier G; y \<in> carrier G \<rbrakk> \<Longrightarrow> (\<ominus> x) \<oplus> (x \<oplus> y) = y"
lp15@68443
   346
proof -
lp15@68443
   347
  assume G: "x \<in> carrier G" "y \<in> carrier G"
lp15@68517
   348
  then have "(\<ominus> x \<oplus> x) \<oplus> y = y"
lp15@68443
   349
    by (simp only: l_neg l_zero)
lp15@68443
   350
  with G show ?thesis by (simp add: a_ac)
lp15@68443
   351
qed
lp15@68443
   352
ballarin@20318
   353
lemma (in abelian_group) r_neg2:
lp15@68443
   354
  "\<lbrakk> x \<in> carrier G; y \<in> carrier G \<rbrakk> \<Longrightarrow> x \<oplus> ((\<ominus> x) \<oplus> y) = y"
ballarin@20318
   355
proof -
ballarin@20318
   356
  assume G: "x \<in> carrier G" "y \<in> carrier G"
ballarin@20318
   357
  then have "(x \<oplus> \<ominus> x) \<oplus> y = y"
ballarin@20318
   358
    by (simp only: r_neg l_zero)
ballarin@41433
   359
  with G show ?thesis
ballarin@20318
   360
    by (simp add: a_ac)
ballarin@20318
   361
qed
ballarin@20318
   362
ballarin@41433
   363
context ring begin
ballarin@41433
   364
wenzelm@61382
   365
text \<open>
ballarin@41433
   366
  The following proofs are from Jacobson, Basic Algebra I, pp.~88--89.
wenzelm@61382
   367
\<close>
ballarin@20318
   368
rene@59851
   369
sublocale semiring
ballarin@20318
   370
proof -
rene@59851
   371
  note [simp] = ring_axioms[unfolded ring_def ring_axioms_def]
rene@59851
   372
  show "semiring R"
rene@59851
   373
  proof (unfold_locales)
rene@59851
   374
    fix x
rene@59851
   375
    assume R: "x \<in> carrier R"
rene@59851
   376
    then have "\<zero> \<otimes> x \<oplus> \<zero> \<otimes> x = (\<zero> \<oplus> \<zero>) \<otimes> x"
rene@59851
   377
      by (simp del: l_zero r_zero)
rene@59851
   378
    also from R have "... = \<zero> \<otimes> x \<oplus> \<zero>" by simp
rene@59851
   379
    finally have "\<zero> \<otimes> x \<oplus> \<zero> \<otimes> x = \<zero> \<otimes> x \<oplus> \<zero>" .
rene@59851
   380
    with R show "\<zero> \<otimes> x = \<zero>" by (simp del: r_zero)
rene@59851
   381
    from R have "x \<otimes> \<zero> \<oplus> x \<otimes> \<zero> = x \<otimes> (\<zero> \<oplus> \<zero>)"
rene@59851
   382
      by (simp del: l_zero r_zero)
rene@59851
   383
    also from R have "... = x \<otimes> \<zero> \<oplus> \<zero>" by simp
rene@59851
   384
    finally have "x \<otimes> \<zero> \<oplus> x \<otimes> \<zero> = x \<otimes> \<zero> \<oplus> \<zero>" .
rene@59851
   385
    with R show "x \<otimes> \<zero> = \<zero>" by (simp del: r_zero)
rene@59851
   386
  qed auto
ballarin@20318
   387
qed
ballarin@20318
   388
ballarin@41433
   389
lemma l_minus:
lp15@68443
   390
  "\<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> (\<ominus> x) \<otimes> y = \<ominus> (x \<otimes> y)"
ballarin@20318
   391
proof -
ballarin@20318
   392
  assume R: "x \<in> carrier R" "y \<in> carrier R"
ballarin@20318
   393
  then have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y = (\<ominus> x \<oplus> x) \<otimes> y" by (simp add: l_distr)
wenzelm@44677
   394
  also from R have "... = \<zero>" by (simp add: l_neg)
ballarin@20318
   395
  finally have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y = \<zero>" .
ballarin@20318
   396
  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@21896
   397
  with R show ?thesis by (simp add: a_assoc r_neg)
ballarin@20318
   398
qed
ballarin@20318
   399
ballarin@41433
   400
lemma r_minus:
lp15@68443
   401
  "\<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> x \<otimes> (\<ominus> y) = \<ominus> (x \<otimes> y)"
ballarin@20318
   402
proof -
ballarin@20318
   403
  assume R: "x \<in> carrier R" "y \<in> carrier R"
ballarin@20318
   404
  then have "x \<otimes> (\<ominus> y) \<oplus> x \<otimes> y = x \<otimes> (\<ominus> y \<oplus> y)" by (simp add: r_distr)
wenzelm@44677
   405
  also from R have "... = \<zero>" by (simp add: l_neg)
ballarin@20318
   406
  finally have "x \<otimes> (\<ominus> y) \<oplus> x \<otimes> y = \<zero>" .
ballarin@20318
   407
  with R have "x \<otimes> (\<ominus> y) \<oplus> x \<otimes> y \<oplus> \<ominus> (x \<otimes> y) = \<zero> \<oplus> \<ominus> (x \<otimes> y)" by simp
ballarin@20318
   408
  with R show ?thesis by (simp add: a_assoc r_neg )
ballarin@20318
   409
qed
ballarin@20318
   410
ballarin@41433
   411
end
ballarin@41433
   412
lp15@68445
   413
lemma (in abelian_group) minus_eq: "x \<ominus> y = x \<oplus> (\<ominus> y)"
lp15@68445
   414
  by (rule a_minus_def)
ballarin@20318
   415
wenzelm@61382
   416
text \<open>Setup algebra method:
wenzelm@61382
   417
  compute distributive normal form in locale contexts\<close>
ballarin@20318
   418
lp15@68443
   419
wenzelm@48891
   420
ML_file "ringsimp.ML"
ballarin@20318
   421
wenzelm@61382
   422
attribute_setup algebra = \<open>
wenzelm@58811
   423
  Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon || Scan.succeed true)
wenzelm@58811
   424
    -- Scan.lift Args.name -- Scan.repeat Args.term
wenzelm@58811
   425
    >> (fn ((b, n), ts) => if b then Ringsimp.add_struct (n, ts) else Ringsimp.del_struct (n, ts))
wenzelm@61382
   426
\<close> "theorems controlling algebra method"
wenzelm@47701
   427
wenzelm@61382
   428
method_setup algebra = \<open>
wenzelm@58811
   429
  Scan.succeed (SIMPLE_METHOD' o Ringsimp.algebra_tac)
wenzelm@61382
   430
\<close> "normalisation of algebraic structure"
ballarin@20318
   431
rene@59851
   432
lemmas (in semiring) semiring_simprules
rene@59851
   433
  [algebra ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] =
rene@59851
   434
  a_closed zero_closed  m_closed one_closed
rene@59851
   435
  a_assoc l_zero  a_comm m_assoc l_one l_distr r_zero
lp15@68517
   436
  a_lcomm r_distr l_null r_null
rene@59851
   437
ballarin@20318
   438
lemmas (in ring) ring_simprules
ballarin@20318
   439
  [algebra ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] =
ballarin@20318
   440
  a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
ballarin@20318
   441
  a_assoc l_zero l_neg a_comm m_assoc l_one l_distr minus_eq
ballarin@20318
   442
  r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero
ballarin@20318
   443
  a_lcomm r_distr l_null r_null l_minus r_minus
ballarin@20318
   444
ballarin@20318
   445
lemmas (in cring)
ballarin@20318
   446
  [algebra del: ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] =
ballarin@20318
   447
  _
ballarin@20318
   448
ballarin@20318
   449
lemmas (in cring) cring_simprules
ballarin@20318
   450
  [algebra add: cring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] =
ballarin@20318
   451
  a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
ballarin@20318
   452
  a_assoc l_zero l_neg a_comm m_assoc l_one l_distr m_comm minus_eq
ballarin@20318
   453
  r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero
ballarin@20318
   454
  a_lcomm m_lcomm r_distr l_null r_null l_minus r_minus
ballarin@20318
   455
rene@59851
   456
lemma (in semiring) nat_pow_zero:
nipkow@67341
   457
  "(n::nat) \<noteq> 0 \<Longrightarrow> \<zero> [^] n = \<zero>"
ballarin@20318
   458
  by (induct n) simp_all
ballarin@20318
   459
rene@59851
   460
context semiring begin
ballarin@41433
   461
ballarin@41433
   462
lemma one_zeroD:
ballarin@20318
   463
  assumes onezero: "\<one> = \<zero>"
ballarin@20318
   464
  shows "carrier R = {\<zero>}"
ballarin@20318
   465
proof (rule, rule)
ballarin@20318
   466
  fix x
ballarin@20318
   467
  assume xcarr: "x \<in> carrier R"
wenzelm@47409
   468
  from xcarr have "x = x \<otimes> \<one>" by simp
wenzelm@47409
   469
  with onezero have "x = x \<otimes> \<zero>" by simp
wenzelm@47409
   470
  with xcarr have "x = \<zero>" by simp
wenzelm@47409
   471
  then show "x \<in> {\<zero>}" by fast
ballarin@20318
   472
qed fast
ballarin@20318
   473
ballarin@41433
   474
lemma one_zeroI:
ballarin@20318
   475
  assumes carrzero: "carrier R = {\<zero>}"
ballarin@20318
   476
  shows "\<one> = \<zero>"
ballarin@20318
   477
proof -
ballarin@20318
   478
  from one_closed and carrzero
ballarin@20318
   479
      show "\<one> = \<zero>" by simp
ballarin@20318
   480
qed
ballarin@20318
   481
wenzelm@46721
   482
lemma carrier_one_zero: "(carrier R = {\<zero>}) = (\<one> = \<zero>)"
wenzelm@46721
   483
  apply rule
wenzelm@46721
   484
   apply (erule one_zeroI)
wenzelm@46721
   485
  apply (erule one_zeroD)
wenzelm@46721
   486
  done
ballarin@20318
   487
wenzelm@46721
   488
lemma carrier_one_not_zero: "(carrier R \<noteq> {\<zero>}) = (\<one> \<noteq> \<zero>)"
ballarin@27717
   489
  by (simp add: carrier_one_zero)
ballarin@20318
   490
ballarin@41433
   491
end
ballarin@41433
   492
wenzelm@61382
   493
text \<open>Two examples for use of method algebra\<close>
ballarin@20318
   494
ballarin@20318
   495
lemma
ballarin@27611
   496
  fixes R (structure) and S (structure)
ballarin@27611
   497
  assumes "ring R" "cring S"
ballarin@27611
   498
  assumes RS: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier S" "d \<in> carrier S"
lp15@68443
   499
  shows "a \<oplus> (\<ominus> (a \<oplus> (\<ominus> b))) = b \<and> c \<otimes>\<^bsub>S\<^esub> d = d \<otimes>\<^bsub>S\<^esub> c"
ballarin@27611
   500
proof -
ballarin@29237
   501
  interpret ring R by fact
ballarin@29237
   502
  interpret cring S by fact
ballarin@27611
   503
  from RS show ?thesis by algebra
ballarin@27611
   504
qed
ballarin@20318
   505
ballarin@20318
   506
lemma
ballarin@27611
   507
  fixes R (structure)
ballarin@27611
   508
  assumes "ring R"
ballarin@27611
   509
  assumes R: "a \<in> carrier R" "b \<in> carrier R"
ballarin@27611
   510
  shows "a \<ominus> (a \<ominus> b) = b"
ballarin@27611
   511
proof -
ballarin@29237
   512
  interpret ring R by fact
ballarin@27611
   513
  from R show ?thesis by algebra
ballarin@27611
   514
qed
ballarin@20318
   515
wenzelm@35849
   516
wenzelm@61382
   517
subsubsection \<open>Sums over Finite Sets\<close>
ballarin@20318
   518
rene@59851
   519
lemma (in semiring) finsum_ldistr:
lp15@68443
   520
  "\<lbrakk> finite A; a \<in> carrier R; f: A \<rightarrow> carrier R \<rbrakk> \<Longrightarrow>
lp15@68443
   521
    (\<Oplus> i \<in> A. (f i)) \<otimes> a = (\<Oplus> i \<in> A. ((f i) \<otimes> a))"
berghofe@22265
   522
proof (induct set: finite)
ballarin@20318
   523
  case empty then show ?case by simp
ballarin@20318
   524
next
ballarin@20318
   525
  case (insert x F) then show ?case by (simp add: Pi_def l_distr)
ballarin@20318
   526
qed
ballarin@20318
   527
rene@59851
   528
lemma (in semiring) finsum_rdistr:
lp15@68443
   529
  "\<lbrakk> finite A; a \<in> carrier R; f: A \<rightarrow> carrier R \<rbrakk> \<Longrightarrow>
lp15@68443
   530
   a \<otimes> (\<Oplus> i \<in> A. (f i)) = (\<Oplus> i \<in> A. (a \<otimes> (f i)))"
berghofe@22265
   531
proof (induct set: finite)
ballarin@20318
   532
  case empty then show ?case by simp
ballarin@20318
   533
next
ballarin@20318
   534
  case (insert x F) then show ?case by (simp add: Pi_def r_distr)
ballarin@20318
   535
qed
ballarin@20318
   536
lp15@68443
   537
(* ************************************************************************** *)
lp15@68443
   538
(* Contributed by Paulo E. de Vilhena.                                        *)
lp15@68443
   539
lp15@68443
   540
text \<open>A quick detour\<close>
lp15@68443
   541
lp15@68443
   542
lemma add_pow_int_ge: "(k :: int) \<ge> 0 \<Longrightarrow> [ k ] \<cdot>\<^bsub>R\<^esub> a = [ nat k ] \<cdot>\<^bsub>R\<^esub> a"
lp15@68443
   543
  by (simp add: add_pow_def int_pow_def nat_pow_def)
lp15@68443
   544
lp15@68443
   545
lemma add_pow_int_lt: "(k :: int) < 0 \<Longrightarrow> [ k ] \<cdot>\<^bsub>R\<^esub> a = \<ominus>\<^bsub>R\<^esub> ([ nat (- k) ] \<cdot>\<^bsub>R\<^esub> a)"
lp15@68517
   546
  by (simp add: int_pow_def nat_pow_def a_inv_def add_pow_def)
lp15@68443
   547
lp15@68443
   548
corollary (in semiring) add_pow_ldistr:
lp15@68443
   549
  assumes "a \<in> carrier R" "b \<in> carrier R"
lp15@68443
   550
  shows "([(k :: nat)] \<cdot> a) \<otimes> b = [k] \<cdot> (a \<otimes> b)"
lp15@68443
   551
proof -
lp15@68443
   552
  have "([k] \<cdot> a) \<otimes> b = (\<Oplus> i \<in> {..< k}. a) \<otimes> b"
lp15@68443
   553
    using add.finprod_const[OF assms(1), of "{..<k}"] by simp
lp15@68443
   554
  also have " ... = (\<Oplus> i \<in> {..< k}. (a \<otimes> b))"
lp15@68443
   555
    using finsum_ldistr[of "{..<k}" b "\<lambda>x. a"] assms by simp
lp15@68443
   556
  also have " ... = [k] \<cdot> (a \<otimes> b)"
lp15@68443
   557
    using add.finprod_const[of "a \<otimes> b" "{..<k}"] assms by simp
lp15@68443
   558
  finally show ?thesis .
lp15@68443
   559
qed
lp15@68443
   560
lp15@68443
   561
corollary (in semiring) add_pow_rdistr:
lp15@68443
   562
  assumes "a \<in> carrier R" "b \<in> carrier R"
lp15@68443
   563
  shows "a \<otimes> ([(k :: nat)] \<cdot> b) = [k] \<cdot> (a \<otimes> b)"
lp15@68443
   564
proof -
lp15@68443
   565
  have "a \<otimes> ([k] \<cdot> b) = a \<otimes> (\<Oplus> i \<in> {..< k}. b)"
lp15@68443
   566
    using add.finprod_const[OF assms(2), of "{..<k}"] by simp
lp15@68443
   567
  also have " ... = (\<Oplus> i \<in> {..< k}. (a \<otimes> b))"
lp15@68443
   568
    using finsum_rdistr[of "{..<k}" a "\<lambda>x. b"] assms by simp
lp15@68443
   569
  also have " ... = [k] \<cdot> (a \<otimes> b)"
lp15@68443
   570
    using add.finprod_const[of "a \<otimes> b" "{..<k}"] assms by simp
lp15@68443
   571
  finally show ?thesis .
lp15@68517
   572
qed
lp15@68443
   573
lp15@68443
   574
(* For integers, we need the uniqueness of the additive inverse *)
lp15@68443
   575
lemma (in ring) add_pow_ldistr_int:
lp15@68443
   576
  assumes "a \<in> carrier R" "b \<in> carrier R"
lp15@68443
   577
  shows "([(k :: int)] \<cdot> a) \<otimes> b = [k] \<cdot> (a \<otimes> b)"
lp15@68443
   578
proof (cases "k \<ge> 0")
lp15@68443
   579
  case True thus ?thesis
lp15@68443
   580
    using add_pow_int_ge[of k R] add_pow_ldistr[OF assms] by auto
lp15@68443
   581
next
lp15@68443
   582
  case False thus ?thesis
lp15@68443
   583
    using add_pow_int_lt[of k R a] add_pow_int_lt[of k R "a \<otimes> b"]
lp15@68517
   584
          add_pow_ldistr[OF assms, of "nat (- k)"] assms l_minus by auto
lp15@68443
   585
qed
lp15@68443
   586
lp15@68443
   587
lemma (in ring) add_pow_rdistr_int:
lp15@68443
   588
  assumes "a \<in> carrier R" "b \<in> carrier R"
lp15@68443
   589
  shows "a \<otimes> ([(k :: int)] \<cdot> b) = [k] \<cdot> (a \<otimes> b)"
lp15@68443
   590
proof (cases "k \<ge> 0")
lp15@68443
   591
  case True thus ?thesis
lp15@68443
   592
    using add_pow_int_ge[of k R] add_pow_rdistr[OF assms] by auto
lp15@68443
   593
next
lp15@68443
   594
  case False thus ?thesis
lp15@68443
   595
    using add_pow_int_lt[of k R b] add_pow_int_lt[of k R "a \<otimes> b"]
lp15@68517
   596
          add_pow_rdistr[OF assms, of "nat (- k)"] assms r_minus by auto
lp15@68443
   597
qed
lp15@68443
   598
ballarin@20318
   599
wenzelm@61382
   600
subsection \<open>Integral Domains\<close>
ballarin@20318
   601
ballarin@41433
   602
context "domain" begin
ballarin@41433
   603
lp15@68443
   604
lemma zero_not_one [simp]: "\<zero> \<noteq> \<one>"
ballarin@20318
   605
  by (rule not_sym) simp
ballarin@20318
   606
ballarin@41433
   607
lemma integral_iff: (* not by default a simp rule! *)
lp15@68443
   608
  "\<lbrakk> a \<in> carrier R; b \<in> carrier R \<rbrakk> \<Longrightarrow> (a \<otimes> b = \<zero>) = (a = \<zero> \<or> b = \<zero>)"
ballarin@20318
   609
proof
ballarin@20318
   610
  assume "a \<in> carrier R" "b \<in> carrier R" "a \<otimes> b = \<zero>"
wenzelm@67091
   611
  then show "a = \<zero> \<or> b = \<zero>" by (simp add: integral)
ballarin@20318
   612
next
wenzelm@67091
   613
  assume "a \<in> carrier R" "b \<in> carrier R" "a = \<zero> \<or> b = \<zero>"
ballarin@20318
   614
  then show "a \<otimes> b = \<zero>" by auto
ballarin@20318
   615
qed
ballarin@20318
   616
ballarin@41433
   617
lemma m_lcancel:
wenzelm@67091
   618
  assumes prem: "a \<noteq> \<zero>"
ballarin@20318
   619
    and R: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R"
ballarin@20318
   620
  shows "(a \<otimes> b = a \<otimes> c) = (b = c)"
ballarin@20318
   621
proof
ballarin@20318
   622
  assume eq: "a \<otimes> b = a \<otimes> c"
ballarin@20318
   623
  with R have "a \<otimes> (b \<ominus> c) = \<zero>" by algebra
wenzelm@67091
   624
  with R have "a = \<zero> \<or> (b \<ominus> c) = \<zero>" by (simp add: integral_iff)
lp15@68517
   625
  with prem and R have "b \<ominus> c = \<zero>" by auto
lp15@68445
   626
  with R have "b = b \<ominus> (b \<ominus> c)" by algebra
ballarin@20318
   627
  also from R have "b \<ominus> (b \<ominus> c) = c" by algebra
ballarin@20318
   628
  finally show "b = c" .
ballarin@20318
   629
next
ballarin@20318
   630
  assume "b = c" then show "a \<otimes> b = a \<otimes> c" by simp
ballarin@20318
   631
qed
ballarin@20318
   632
ballarin@41433
   633
lemma m_rcancel:
wenzelm@67091
   634
  assumes prem: "a \<noteq> \<zero>"
ballarin@20318
   635
    and R: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R"
ballarin@20318
   636
  shows conc: "(b \<otimes> a = c \<otimes> a) = (b = c)"
ballarin@20318
   637
proof -
ballarin@20318
   638
  from prem and R have "(a \<otimes> b = a \<otimes> c) = (b = c)" by (rule m_lcancel)
ballarin@20318
   639
  with R show ?thesis by algebra
ballarin@20318
   640
qed
ballarin@20318
   641
ballarin@41433
   642
end
ballarin@41433
   643
ballarin@20318
   644
wenzelm@61382
   645
subsection \<open>Fields\<close>
ballarin@20318
   646
wenzelm@61382
   647
text \<open>Field would not need to be derived from domain, the properties
wenzelm@61382
   648
  for domain follow from the assumptions of field\<close>
lp15@68443
   649
lp15@68551
   650
lemma fieldE :
lp15@68551
   651
  fixes R (structure)
lp15@68551
   652
  assumes "field R"
lp15@68551
   653
  shows "cring R"
lp15@68551
   654
    and one_not_zero : "\<one> \<noteq> \<zero>"
lp15@68551
   655
    and integral: "\<And>a b. \<lbrakk> a \<otimes> b = \<zero>; a \<in> carrier R; b \<in> carrier R \<rbrakk> \<Longrightarrow> a = \<zero> \<or> b = \<zero>"
lp15@68551
   656
  and field_Units: "Units R = carrier R - {\<zero>}"
lp15@68551
   657
  using assms unfolding field_def field_axioms_def domain_def domain_axioms_def by simp_all
lp15@68551
   658
ballarin@20318
   659
lemma (in cring) cring_fieldI:
ballarin@20318
   660
  assumes field_Units: "Units R = carrier R - {\<zero>}"
ballarin@20318
   661
  shows "field R"
haftmann@28823
   662
proof
wenzelm@47409
   663
  from field_Units have "\<zero> \<notin> Units R" by fast
wenzelm@47409
   664
  moreover have "\<one> \<in> Units R" by fast
wenzelm@47409
   665
  ultimately show "\<one> \<noteq> \<zero>" by force
ballarin@20318
   666
next
ballarin@20318
   667
  fix a b
ballarin@20318
   668
  assume acarr: "a \<in> carrier R"
ballarin@20318
   669
    and bcarr: "b \<in> carrier R"
ballarin@20318
   670
    and ab: "a \<otimes> b = \<zero>"
ballarin@20318
   671
  show "a = \<zero> \<or> b = \<zero>"
ballarin@20318
   672
  proof (cases "a = \<zero>", simp)
ballarin@20318
   673
    assume "a \<noteq> \<zero>"
wenzelm@47409
   674
    with field_Units and acarr have aUnit: "a \<in> Units R" by fast
wenzelm@47409
   675
    from bcarr have "b = \<one> \<otimes> b" by algebra
wenzelm@47409
   676
    also from aUnit acarr have "... = (inv a \<otimes> a) \<otimes> b" by simp
ballarin@20318
   677
    also from acarr bcarr aUnit[THEN Units_inv_closed]
ballarin@20318
   678
    have "... = (inv a) \<otimes> (a \<otimes> b)" by algebra
wenzelm@47409
   679
    also from ab and acarr bcarr aUnit have "... = (inv a) \<otimes> \<zero>" by simp
wenzelm@47409
   680
    also from aUnit[THEN Units_inv_closed] have "... = \<zero>" by algebra
wenzelm@47409
   681
    finally have "b = \<zero>" .
wenzelm@47409
   682
    then show "a = \<zero> \<or> b = \<zero>" by simp
ballarin@20318
   683
  qed
wenzelm@23350
   684
qed (rule field_Units)
ballarin@20318
   685
wenzelm@61382
   686
text \<open>Another variant to show that something is a field\<close>
ballarin@20318
   687
lemma (in cring) cring_fieldI2:
ballarin@20318
   688
  assumes notzero: "\<zero> \<noteq> \<one>"
ballarin@20318
   689
  and invex: "\<And>a. \<lbrakk>a \<in> carrier R; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>b\<in>carrier R. a \<otimes> b = \<one>"
ballarin@20318
   690
  shows "field R"
ballarin@20318
   691
  apply (rule cring_fieldI, simp add: Units_def)
ballarin@20318
   692
  apply (rule, clarsimp)
ballarin@20318
   693
  apply (simp add: notzero)
ballarin@20318
   694
proof (clarsimp)
ballarin@20318
   695
  fix x
ballarin@20318
   696
  assume xcarr: "x \<in> carrier R"
ballarin@20318
   697
    and "x \<noteq> \<zero>"
wenzelm@47409
   698
  then have "\<exists>y\<in>carrier R. x \<otimes> y = \<one>" by (rule invex)
wenzelm@47409
   699
  then obtain y where ycarr: "y \<in> carrier R" and xy: "x \<otimes> y = \<one>" by fast
ballarin@20318
   700
  from xy xcarr ycarr have "y \<otimes> x = \<one>" by (simp add: m_comm)
wenzelm@47409
   701
  with ycarr and xy show "\<exists>y\<in>carrier R. y \<otimes> x = \<one> \<and> x \<otimes> y = \<one>" by fast
ballarin@20318
   702
qed
ballarin@20318
   703
ballarin@20318
   704
wenzelm@61382
   705
subsection \<open>Morphisms\<close>
ballarin@20318
   706
wenzelm@35847
   707
definition
ballarin@20318
   708
  ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set"
wenzelm@35848
   709
  where "ring_hom R S =
wenzelm@67091
   710
    {h. h \<in> carrier R \<rightarrow> carrier S \<and>
wenzelm@67091
   711
      (\<forall>x y. x \<in> carrier R \<and> y \<in> carrier R \<longrightarrow>
wenzelm@67091
   712
        h (x \<otimes>\<^bsub>R\<^esub> y) = h x \<otimes>\<^bsub>S\<^esub> h y \<and> h (x \<oplus>\<^bsub>R\<^esub> y) = h x \<oplus>\<^bsub>S\<^esub> h y) \<and>
wenzelm@35847
   713
      h \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>}"
ballarin@20318
   714
ballarin@20318
   715
lemma ring_hom_memI:
ballarin@20318
   716
  fixes R (structure) and S (structure)
lp15@68443
   717
  assumes "\<And>x. x \<in> carrier R \<Longrightarrow> h x \<in> carrier S"
lp15@68443
   718
      and "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
lp15@68443
   719
      and "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
lp15@68443
   720
      and "h \<one> = \<one>\<^bsub>S\<^esub>"
ballarin@20318
   721
  shows "h \<in> ring_hom R S"
ballarin@27714
   722
  by (auto simp add: ring_hom_def assms Pi_def)
ballarin@20318
   723
lp15@68443
   724
lemma ring_hom_memE:
lp15@68443
   725
  fixes R (structure) and S (structure)
lp15@68443
   726
  assumes "h \<in> ring_hom R S"
lp15@68443
   727
  shows "\<And>x. x \<in> carrier R \<Longrightarrow> h x \<in> carrier S"
lp15@68443
   728
    and "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
lp15@68443
   729
    and "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
lp15@68443
   730
    and "h \<one> = \<one>\<^bsub>S\<^esub>"
lp15@68443
   731
  using assms unfolding ring_hom_def by auto
lp15@68443
   732
ballarin@20318
   733
lemma ring_hom_closed:
lp15@68443
   734
  "\<lbrakk> h \<in> ring_hom R S; x \<in> carrier R \<rbrakk> \<Longrightarrow> h x \<in> carrier S"
ballarin@20318
   735
  by (auto simp add: ring_hom_def funcset_mem)
ballarin@20318
   736
ballarin@20318
   737
lemma ring_hom_mult:
ballarin@20318
   738
  fixes R (structure) and S (structure)
lp15@68443
   739
  shows "\<lbrakk> h \<in> ring_hom R S; x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
ballarin@20318
   740
    by (simp add: ring_hom_def)
ballarin@20318
   741
ballarin@20318
   742
lemma ring_hom_add:
ballarin@20318
   743
  fixes R (structure) and S (structure)
lp15@68443
   744
  shows "\<lbrakk> h \<in> ring_hom R S; x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
ballarin@20318
   745
    by (simp add: ring_hom_def)
ballarin@20318
   746
ballarin@20318
   747
lemma ring_hom_one:
ballarin@20318
   748
  fixes R (structure) and S (structure)
lp15@68443
   749
  shows "h \<in> ring_hom R S \<Longrightarrow> h \<one> = \<one>\<^bsub>S\<^esub>"
ballarin@20318
   750
  by (simp add: ring_hom_def)
ballarin@20318
   751
lp15@68443
   752
lemma ring_hom_zero:
lp15@68443
   753
  fixes R (structure) and S (structure)
lp15@68443
   754
  assumes "h \<in> ring_hom R S" "ring R" "ring S"
lp15@68443
   755
  shows "h \<zero> = \<zero>\<^bsub>S\<^esub>"
lp15@68443
   756
proof -
lp15@68443
   757
  have "h \<zero> = h \<zero> \<oplus>\<^bsub>S\<^esub> h \<zero>"
lp15@68443
   758
    using ring_hom_add[OF assms(1), of \<zero> \<zero>] assms(2)
lp15@68443
   759
    by (simp add: ring.ring_simprules(2) ring.ring_simprules(15))
lp15@68443
   760
  thus ?thesis
lp15@68443
   761
    by (metis abelian_group.l_neg assms ring.is_abelian_group ring.ring_simprules(18) ring.ring_simprules(2) ring_hom_closed)
lp15@68443
   762
qed
lp15@68443
   763
lp15@68443
   764
locale ring_hom_cring =
lp15@68443
   765
  R?: cring R + S?: cring S for R (structure) and S (structure) + fixes h
ballarin@20318
   766
  assumes homh [simp, intro]: "h \<in> ring_hom R S"
ballarin@20318
   767
  notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
ballarin@20318
   768
    and hom_mult [simp] = ring_hom_mult [OF homh]
ballarin@20318
   769
    and hom_add [simp] = ring_hom_add [OF homh]
ballarin@20318
   770
    and hom_one [simp] = ring_hom_one [OF homh]
ballarin@20318
   771
lp15@68443
   772
lemma (in ring_hom_cring) hom_zero [simp]: "h \<zero> = \<zero>\<^bsub>S\<^esub>"
ballarin@20318
   773
proof -
ballarin@20318
   774
  have "h \<zero> \<oplus>\<^bsub>S\<^esub> h \<zero> = h \<zero> \<oplus>\<^bsub>S\<^esub> \<zero>\<^bsub>S\<^esub>"
ballarin@20318
   775
    by (simp add: hom_add [symmetric] del: hom_add)
ballarin@20318
   776
  then show ?thesis by (simp del: S.r_zero)
ballarin@20318
   777
qed
ballarin@20318
   778
ballarin@20318
   779
lemma (in ring_hom_cring) hom_a_inv [simp]:
lp15@68443
   780
  "x \<in> carrier R \<Longrightarrow> h (\<ominus> x) = \<ominus>\<^bsub>S\<^esub> h x"
ballarin@20318
   781
proof -
ballarin@20318
   782
  assume R: "x \<in> carrier R"
ballarin@20318
   783
  then have "h x \<oplus>\<^bsub>S\<^esub> h (\<ominus> x) = h x \<oplus>\<^bsub>S\<^esub> (\<ominus>\<^bsub>S\<^esub> h x)"
ballarin@20318
   784
    by (simp add: hom_add [symmetric] R.r_neg S.r_neg del: hom_add)
ballarin@20318
   785
  with R show ?thesis by simp
ballarin@20318
   786
qed
ballarin@20318
   787
ballarin@20318
   788
lemma (in ring_hom_cring) hom_finsum [simp]:
lp15@68443
   789
  assumes "f: A \<rightarrow> carrier R"
lp15@68443
   790
  shows "h (\<Oplus> i \<in> A. f i) = (\<Oplus>\<^bsub>S\<^esub> i \<in> A. (h o f) i)"
lp15@68443
   791
  using assms by (induct A rule: infinite_finite_induct, auto simp: Pi_def)
ballarin@20318
   792
ballarin@20318
   793
lemma (in ring_hom_cring) hom_finprod:
lp15@68443
   794
  assumes "f: A \<rightarrow> carrier R"
lp15@68443
   795
  shows "h (\<Otimes> i \<in> A. f i) = (\<Otimes>\<^bsub>S\<^esub> i \<in> A. (h o f) i)"
lp15@68443
   796
  using assms by (induct A rule: infinite_finite_induct, auto simp: Pi_def)
ballarin@20318
   797
ballarin@20318
   798
declare ring_hom_cring.hom_finprod [simp]
ballarin@20318
   799
lp15@68443
   800
lemma id_ring_hom [simp]: "id \<in> ring_hom R R"
ballarin@20318
   801
  by (auto intro!: ring_hom_memI)
ballarin@20318
   802
lp15@68443
   803
(* Next lemma contributed by Paulo Emílio de Vilhena. *)
lp15@68443
   804
lp15@68443
   805
lemma ring_hom_trans:
lp15@68443
   806
  "\<lbrakk> f \<in> ring_hom R S; g \<in> ring_hom S T \<rbrakk> \<Longrightarrow> g \<circ> f \<in> ring_hom R T"
lp15@68443
   807
  by (rule ring_hom_memI) (auto simp add: ring_hom_closed ring_hom_mult ring_hom_add ring_hom_one)
lp15@68443
   808
lp15@68445
   809
subsection\<open>Jeremy Avigad's @{text"More_Finite_Product"} material\<close>
lp15@68445
   810
lp15@68445
   811
(* need better simplification rules for rings *)
lp15@68445
   812
(* the next one holds more generally for abelian groups *)
lp15@68445
   813
lp15@68445
   814
lemma (in cring) sum_zero_eq_neg: "x \<in> carrier R \<Longrightarrow> y \<in> carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y"
lp15@68445
   815
  by (metis minus_equality)
lp15@68445
   816
lp15@68445
   817
lemma (in domain) square_eq_one:
lp15@68445
   818
  fixes x
lp15@68445
   819
  assumes [simp]: "x \<in> carrier R"
lp15@68445
   820
    and "x \<otimes> x = \<one>"
lp15@68445
   821
  shows "x = \<one> \<or> x = \<ominus>\<one>"
lp15@68445
   822
proof -
lp15@68445
   823
  have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>"
lp15@68445
   824
    by (simp add: ring_simprules)
lp15@68445
   825
  also from \<open>x \<otimes> x = \<one>\<close> have "\<dots> = \<zero>"
lp15@68445
   826
    by (simp add: ring_simprules)
lp15@68445
   827
  finally have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = \<zero>" .
lp15@68445
   828
  then have "(x \<oplus> \<one>) = \<zero> \<or> (x \<oplus> \<ominus> \<one>) = \<zero>"
lp15@68445
   829
    by (intro integral) auto
lp15@68445
   830
  then show ?thesis
lp15@68445
   831
    by (metis add.inv_closed add.inv_solve_right assms(1) l_zero one_closed zero_closed)
lp15@68445
   832
qed
lp15@68445
   833
lp15@68445
   834
lemma (in domain) inv_eq_self: "x \<in> Units R \<Longrightarrow> x = inv x \<Longrightarrow> x = \<one> \<or> x = \<ominus>\<one>"
lp15@68445
   835
  by (metis Units_closed Units_l_inv square_eq_one)
lp15@68445
   836
lp15@68445
   837
lp15@68445
   838
text \<open>
lp15@68445
   839
  The following translates theorems about groups to the facts about
lp15@68445
   840
  the units of a ring. (The list should be expanded as more things are
lp15@68445
   841
  needed.)
lp15@68445
   842
\<close>
lp15@68445
   843
lp15@68445
   844
lemma (in ring) finite_ring_finite_units [intro]: "finite (carrier R) \<Longrightarrow> finite (Units R)"
lp15@68445
   845
  by (rule finite_subset) auto
lp15@68445
   846
lp15@68445
   847
lemma (in monoid) units_of_pow:
lp15@68445
   848
  fixes n :: nat
lp15@68445
   849
  shows "x \<in> Units G \<Longrightarrow> x [^]\<^bsub>units_of G\<^esub> n = x [^]\<^bsub>G\<^esub> n"
lp15@68445
   850
  apply (induct n)
lp15@68445
   851
  apply (auto simp add: units_group group.is_monoid
lp15@68445
   852
    monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult)
lp15@68445
   853
  done
lp15@68445
   854
lp15@68445
   855
lemma (in cring) units_power_order_eq_one:
lp15@68445
   856
  "finite (Units R) \<Longrightarrow> a \<in> Units R \<Longrightarrow> a [^] card(Units R) = \<one>"
lp15@68445
   857
  by (metis comm_group.power_order_eq_one units_comm_group units_of_carrier units_of_one units_of_pow)
lp15@68445
   858
lp15@68445
   859
subsection\<open>Jeremy Avigad's @{text"More_Ring"} material\<close>
lp15@68445
   860
lp15@68445
   861
lemma (in cring) field_intro2: "\<zero>\<^bsub>R\<^esub> \<noteq> \<one>\<^bsub>R\<^esub> \<Longrightarrow> \<forall>x \<in> carrier R - {\<zero>\<^bsub>R\<^esub>}. x \<in> Units R \<Longrightarrow> field R"
lp15@68445
   862
  apply (unfold_locales)
lp15@68445
   863
    apply (use cring_axioms in auto)
lp15@68445
   864
   apply (rule trans)
lp15@68445
   865
    apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b")
lp15@68445
   866
     apply assumption
lp15@68445
   867
    apply (subst m_assoc)
lp15@68445
   868
       apply auto
lp15@68445
   869
  apply (unfold Units_def)
lp15@68445
   870
  apply auto
lp15@68445
   871
  done
lp15@68445
   872
lp15@68445
   873
lemma (in monoid) inv_char:
lp15@68445
   874
  "x \<in> carrier G \<Longrightarrow> y \<in> carrier G \<Longrightarrow> x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y"
lp15@68445
   875
  apply (subgoal_tac "x \<in> Units G")
lp15@68445
   876
   apply (subgoal_tac "y = inv x \<otimes> \<one>")
lp15@68445
   877
    apply simp
lp15@68445
   878
   apply (erule subst)
lp15@68445
   879
   apply (subst m_assoc [symmetric])
lp15@68445
   880
      apply auto
lp15@68445
   881
  apply (unfold Units_def)
lp15@68445
   882
  apply auto
lp15@68445
   883
  done
lp15@68445
   884
lp15@68445
   885
lemma (in comm_monoid) comm_inv_char: "x \<in> carrier G \<Longrightarrow> y \<in> carrier G \<Longrightarrow> x \<otimes> y = \<one> \<Longrightarrow> inv x = y"
lp15@68445
   886
  by (simp add: inv_char m_comm)
lp15@68445
   887
lp15@68445
   888
lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>"
lp15@68445
   889
  apply (rule inv_char)
lp15@68445
   890
     apply (auto simp add: l_minus r_minus)
lp15@68445
   891
  done
lp15@68445
   892
lp15@68445
   893
lemma (in monoid) inv_eq_imp_eq: "x \<in> Units G \<Longrightarrow> y \<in> Units G \<Longrightarrow> inv x = inv y \<Longrightarrow> x = y"
lp15@68445
   894
  apply (subgoal_tac "inv (inv x) = inv (inv y)")
lp15@68445
   895
   apply (subst (asm) Units_inv_inv)+
lp15@68445
   896
    apply auto
lp15@68445
   897
  done
lp15@68445
   898
lp15@68445
   899
lemma (in ring) Units_minus_one_closed [intro]: "\<ominus> \<one> \<in> Units R"
lp15@68445
   900
  apply (unfold Units_def)
lp15@68445
   901
  apply auto
lp15@68445
   902
  apply (rule_tac x = "\<ominus> \<one>" in bexI)
lp15@68445
   903
   apply auto
lp15@68445
   904
  apply (simp add: l_minus r_minus)
lp15@68445
   905
  done
lp15@68445
   906
lp15@68445
   907
lemma (in ring) inv_eq_neg_one_eq: "x \<in> Units R \<Longrightarrow> inv x = \<ominus> \<one> \<longleftrightarrow> x = \<ominus> \<one>"
lp15@68445
   908
  apply auto
lp15@68445
   909
  apply (subst Units_inv_inv [symmetric])
lp15@68445
   910
   apply auto
lp15@68445
   911
  done
lp15@68445
   912
lp15@68445
   913
lemma (in monoid) inv_eq_one_eq: "x \<in> Units G \<Longrightarrow> inv x = \<one> \<longleftrightarrow> x = \<one>"
lp15@68445
   914
  by (metis Units_inv_inv inv_one)
lp15@68445
   915
ballarin@20318
   916
end