src/HOL/Algebra/abstract/Ring2.thy
author wenzelm
Thu Apr 26 14:24:08 2007 +0200 (2007-04-26)
changeset 22808 a7daa74e2980
parent 22384 33a46e6c7f04
child 22997 d4f3b015b50b
permissions -rw-r--r--
eliminated unnamed infixes, tuned syntax;
ballarin@20318
     1
(*
ballarin@20318
     2
  Title:     The algebraic hierarchy of rings as axiomatic classes
ballarin@20318
     3
  Id:        $Id$
ballarin@20318
     4
  Author:    Clemens Ballarin, started 9 December 1996
ballarin@20318
     5
  Copyright: Clemens Ballarin
ballarin@20318
     6
*)
ballarin@20318
     7
ballarin@20318
     8
header {* The algebraic hierarchy of rings as axiomatic classes *}
ballarin@20318
     9
ballarin@20318
    10
theory Ring2 imports Main
wenzelm@21423
    11
begin
ballarin@20318
    12
ballarin@20318
    13
section {* Constants *}
ballarin@20318
    14
ballarin@20318
    15
text {* Most constants are already declared by HOL. *}
ballarin@20318
    16
ballarin@20318
    17
consts
wenzelm@22808
    18
  assoc         :: "['a::times, 'a] => bool"              (infixl "assoc" 50)
ballarin@20318
    19
  irred         :: "'a::{zero, one, times} => bool"
ballarin@20318
    20
  prime         :: "'a::{zero, one, times} => bool"
ballarin@20318
    21
ballarin@20318
    22
section {* Axioms *}
ballarin@20318
    23
ballarin@20318
    24
subsection {* Ring axioms *}
ballarin@20318
    25
ballarin@20318
    26
axclass ring < zero, one, plus, minus, times, inverse, power
ballarin@20318
    27
ballarin@20318
    28
  a_assoc:      "(a + b) + c = a + (b + c)"
ballarin@20318
    29
  l_zero:       "0 + a = a"
ballarin@20318
    30
  l_neg:        "(-a) + a = 0"
ballarin@20318
    31
  a_comm:       "a + b = b + a"
ballarin@20318
    32
ballarin@20318
    33
  m_assoc:      "(a * b) * c = a * (b * c)"
ballarin@20318
    34
  l_one:        "1 * a = a"
ballarin@20318
    35
ballarin@20318
    36
  l_distr:      "(a + b) * c = a * c + b * c"
ballarin@20318
    37
ballarin@20318
    38
  m_comm:       "a * b = b * a"
ballarin@20318
    39
ballarin@20318
    40
  -- {* Definition of derived operations *}
ballarin@20318
    41
ballarin@20318
    42
  minus_def:    "a - b = a + (-b)"
ballarin@20318
    43
  inverse_def:  "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)"
ballarin@20318
    44
  divide_def:   "a / b = a * inverse b"
ballarin@20318
    45
  power_def:    "a ^ n = nat_rec 1 (%u b. b * a) n"
ballarin@20318
    46
ballarin@20318
    47
defs
ballarin@20318
    48
  assoc_def:    "a assoc b == a dvd b & b dvd a"
ballarin@20318
    49
  irred_def:    "irred a == a ~= 0 & ~ a dvd 1
ballarin@20318
    50
                          & (ALL d. d dvd a --> d dvd 1 | a dvd d)"
ballarin@20318
    51
  prime_def:    "prime p == p ~= 0 & ~ p dvd 1
ballarin@20318
    52
                          & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)"
ballarin@20318
    53
ballarin@20318
    54
subsection {* Integral domains *}
ballarin@20318
    55
ballarin@20318
    56
axclass
ballarin@20318
    57
  "domain" < ring
ballarin@20318
    58
ballarin@20318
    59
  one_not_zero: "1 ~= 0"
ballarin@20318
    60
  integral:     "a * b = 0 ==> a = 0 | b = 0"
ballarin@20318
    61
ballarin@20318
    62
subsection {* Factorial domains *}
ballarin@20318
    63
ballarin@20318
    64
axclass
ballarin@20318
    65
  factorial < "domain"
ballarin@20318
    66
ballarin@20318
    67
(*
ballarin@20318
    68
  Proper definition using divisor chain condition currently not supported.
ballarin@20318
    69
  factorial_divisor:    "wf {(a, b). a dvd b & ~ (b dvd a)}"
ballarin@20318
    70
*)
ballarin@20318
    71
  factorial_divisor:	"True"
ballarin@20318
    72
  factorial_prime:      "irred a ==> prime a"
ballarin@20318
    73
ballarin@20318
    74
subsection {* Euclidean domains *}
ballarin@20318
    75
ballarin@20318
    76
(*
ballarin@20318
    77
axclass
ballarin@20318
    78
  euclidean < "domain"
ballarin@20318
    79
ballarin@20318
    80
  euclidean_ax:  "b ~= 0 ==> Ex (% (q, r, e_size::('a::ringS)=>nat).
ballarin@20318
    81
                   a = b * q + r & e_size r < e_size b)"
ballarin@20318
    82
ballarin@20318
    83
  Nothing has been proved about Euclidean domains, yet.
ballarin@20318
    84
  Design question:
ballarin@20318
    85
    Fix quo, rem and e_size as constants that are axiomatised with
ballarin@20318
    86
    euclidean_ax?
ballarin@20318
    87
    - advantage: more pragmatic and easier to use
ballarin@20318
    88
    - disadvantage: for every type, one definition of quo and rem will
ballarin@20318
    89
        be fixed, users may want to use differing ones;
ballarin@20318
    90
        also, it seems not possible to prove that fields are euclidean
ballarin@20318
    91
        domains, because that would require generic (type-independent)
ballarin@20318
    92
        definitions of quo and rem.
ballarin@20318
    93
*)
ballarin@20318
    94
ballarin@20318
    95
subsection {* Fields *}
ballarin@20318
    96
ballarin@20318
    97
axclass
ballarin@20318
    98
  field < ring
ballarin@20318
    99
ballarin@20318
   100
  field_one_not_zero:    "1 ~= 0"
ballarin@20318
   101
                (* Avoid a common superclass as the first thing we will
ballarin@20318
   102
                   prove about fields is that they are domains. *)
ballarin@20318
   103
  field_ax:        "a ~= 0 ==> a dvd 1"
ballarin@20318
   104
wenzelm@21423
   105
ballarin@20318
   106
section {* Basic facts *}
ballarin@20318
   107
ballarin@20318
   108
subsection {* Normaliser for rings *}
ballarin@20318
   109
wenzelm@21423
   110
(* derived rewrite rules *)
wenzelm@21423
   111
wenzelm@21423
   112
lemma a_lcomm: "(a::'a::ring)+(b+c) = b+(a+c)"
wenzelm@21423
   113
  apply (rule a_comm [THEN trans])
wenzelm@21423
   114
  apply (rule a_assoc [THEN trans])
wenzelm@21423
   115
  apply (rule a_comm [THEN arg_cong])
wenzelm@21423
   116
  done
wenzelm@21423
   117
wenzelm@21423
   118
lemma r_zero: "(a::'a::ring) + 0 = a"
wenzelm@21423
   119
  apply (rule a_comm [THEN trans])
wenzelm@21423
   120
  apply (rule l_zero)
wenzelm@21423
   121
  done
wenzelm@21423
   122
wenzelm@21423
   123
lemma r_neg: "(a::'a::ring) + (-a) = 0"
wenzelm@21423
   124
  apply (rule a_comm [THEN trans])
wenzelm@21423
   125
  apply (rule l_neg)
wenzelm@21423
   126
  done
wenzelm@21423
   127
wenzelm@21423
   128
lemma r_neg2: "(a::'a::ring) + (-a + b) = b"
wenzelm@21423
   129
  apply (rule a_assoc [symmetric, THEN trans])
wenzelm@21423
   130
  apply (simp add: r_neg l_zero)
wenzelm@21423
   131
  done
wenzelm@21423
   132
wenzelm@21423
   133
lemma r_neg1: "-(a::'a::ring) + (a + b) = b"
wenzelm@21423
   134
  apply (rule a_assoc [symmetric, THEN trans])
wenzelm@21423
   135
  apply (simp add: l_neg l_zero)
wenzelm@21423
   136
  done
wenzelm@21423
   137
wenzelm@21423
   138
wenzelm@21423
   139
(* auxiliary *)
wenzelm@21423
   140
wenzelm@21423
   141
lemma a_lcancel: "!! a::'a::ring. a + b = a + c ==> b = c"
wenzelm@21423
   142
  apply (rule box_equals)
wenzelm@21423
   143
  prefer 2
wenzelm@21423
   144
  apply (rule l_zero)
wenzelm@21423
   145
  prefer 2
wenzelm@21423
   146
  apply (rule l_zero)
wenzelm@21423
   147
  apply (rule_tac a1 = a in l_neg [THEN subst])
wenzelm@21423
   148
  apply (simp add: a_assoc)
wenzelm@21423
   149
  done
wenzelm@21423
   150
wenzelm@21423
   151
lemma minus_add: "-((a::'a::ring) + b) = (-a) + (-b)"
wenzelm@21423
   152
  apply (rule_tac a = "a + b" in a_lcancel)
wenzelm@21423
   153
  apply (simp add: r_neg l_neg l_zero a_assoc a_comm a_lcomm)
wenzelm@21423
   154
  done
wenzelm@21423
   155
wenzelm@21423
   156
lemma minus_minus: "-(-(a::'a::ring)) = a"
wenzelm@21423
   157
  apply (rule a_lcancel)
wenzelm@21423
   158
  apply (rule r_neg [THEN trans])
wenzelm@21423
   159
  apply (rule l_neg [symmetric])
wenzelm@21423
   160
  done
wenzelm@21423
   161
wenzelm@21423
   162
lemma minus0: "- 0 = (0::'a::ring)"
wenzelm@21423
   163
  apply (rule a_lcancel)
wenzelm@21423
   164
  apply (rule r_neg [THEN trans])
wenzelm@21423
   165
  apply (rule l_zero [symmetric])
wenzelm@21423
   166
  done
wenzelm@21423
   167
wenzelm@21423
   168
wenzelm@21423
   169
(* derived rules for multiplication *)
wenzelm@21423
   170
wenzelm@21423
   171
lemma m_lcomm: "(a::'a::ring)*(b*c) = b*(a*c)"
wenzelm@21423
   172
  apply (rule m_comm [THEN trans])
wenzelm@21423
   173
  apply (rule m_assoc [THEN trans])
wenzelm@21423
   174
  apply (rule m_comm [THEN arg_cong])
wenzelm@21423
   175
  done
wenzelm@21423
   176
wenzelm@21423
   177
lemma r_one: "(a::'a::ring) * 1 = a"
wenzelm@21423
   178
  apply (rule m_comm [THEN trans])
wenzelm@21423
   179
  apply (rule l_one)
wenzelm@21423
   180
  done
wenzelm@21423
   181
wenzelm@21423
   182
lemma r_distr: "(a::'a::ring) * (b + c) = a * b + a * c"
wenzelm@21423
   183
  apply (rule m_comm [THEN trans])
wenzelm@21423
   184
  apply (rule l_distr [THEN trans])
wenzelm@21423
   185
  apply (simp add: m_comm)
wenzelm@21423
   186
  done
wenzelm@21423
   187
wenzelm@21423
   188
wenzelm@21423
   189
(* the following proof is from Jacobson, Basic Algebra I, pp. 88-89 *)
wenzelm@21423
   190
lemma l_null: "0 * (a::'a::ring) = 0"
wenzelm@21423
   191
  apply (rule a_lcancel)
wenzelm@21423
   192
  apply (rule l_distr [symmetric, THEN trans])
wenzelm@21423
   193
  apply (simp add: r_zero)
wenzelm@21423
   194
  done
wenzelm@21423
   195
wenzelm@21423
   196
lemma r_null: "(a::'a::ring) * 0 = 0"
wenzelm@21423
   197
  apply (rule m_comm [THEN trans])
wenzelm@21423
   198
  apply (rule l_null)
wenzelm@21423
   199
  done
wenzelm@21423
   200
wenzelm@21423
   201
lemma l_minus: "(-(a::'a::ring)) * b = - (a * b)"
wenzelm@21423
   202
  apply (rule a_lcancel)
wenzelm@21423
   203
  apply (rule r_neg [symmetric, THEN [2] trans])
wenzelm@21423
   204
  apply (rule l_distr [symmetric, THEN trans])
wenzelm@21423
   205
  apply (simp add: l_null r_neg)
wenzelm@21423
   206
  done
wenzelm@21423
   207
wenzelm@21423
   208
lemma r_minus: "(a::'a::ring) * (-b) = - (a * b)"
wenzelm@21423
   209
  apply (rule a_lcancel)
wenzelm@21423
   210
  apply (rule r_neg [symmetric, THEN [2] trans])
wenzelm@21423
   211
  apply (rule r_distr [symmetric, THEN trans])
wenzelm@21423
   212
  apply (simp add: r_null r_neg)
wenzelm@21423
   213
  done
wenzelm@21423
   214
wenzelm@21423
   215
(*** Term order for commutative rings ***)
wenzelm@21423
   216
wenzelm@21423
   217
ML {*
wenzelm@21423
   218
fun ring_ord (Const (a, _)) =
wenzelm@21423
   219
    find_index (fn a' => a = a')
wenzelm@21423
   220
      ["HOL.zero", "HOL.plus", "HOL.uminus", "HOL.minus", "HOL.one", "HOL.times"]
wenzelm@21423
   221
  | ring_ord _ = ~1;
wenzelm@21423
   222
wenzelm@21423
   223
fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS);
wenzelm@21423
   224
wenzelm@21423
   225
val ring_ss = HOL_basic_ss settermless termless_ring addsimps
wenzelm@21423
   226
  [thm "a_assoc", thm "l_zero", thm "l_neg", thm "a_comm", thm "m_assoc",
wenzelm@21423
   227
   thm "l_one", thm "l_distr", thm "m_comm", thm "minus_def",
wenzelm@21423
   228
   thm "r_zero", thm "r_neg", thm "r_neg2", thm "r_neg1", thm "minus_add",
wenzelm@21423
   229
   thm "minus_minus", thm "minus0", thm "a_lcomm", thm "m_lcomm", (*thm "r_one",*)
wenzelm@21423
   230
   thm "r_distr", thm "l_null", thm "r_null", thm "l_minus", thm "r_minus"];
wenzelm@21423
   231
*}   (* Note: r_one is not necessary in ring_ss *)
ballarin@20318
   232
ballarin@20318
   233
method_setup ring =
wenzelm@21588
   234
  {* Method.no_args (Method.SIMPLE_METHOD' (full_simp_tac ring_ss)) *}
ballarin@20318
   235
  {* computes distributive normal form in rings *}
ballarin@20318
   236
wenzelm@21423
   237
lemmas ring_simps =
wenzelm@21423
   238
  l_zero r_zero l_neg r_neg minus_minus minus0
wenzelm@21423
   239
  l_one r_one l_null r_null l_minus r_minus
wenzelm@21423
   240
ballarin@20318
   241
ballarin@20318
   242
subsection {* Rings and the summation operator *}
ballarin@20318
   243
ballarin@20318
   244
(* Basic facts --- move to HOL!!! *)
ballarin@20318
   245
ballarin@20318
   246
(* needed because natsum_cong (below) disables atMost_0 *)
ballarin@20318
   247
lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::comm_monoid_add)"
ballarin@20318
   248
by simp
ballarin@20318
   249
(*
ballarin@20318
   250
lemma natsum_Suc [simp]:
ballarin@20318
   251
  "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::comm_monoid_add)"
ballarin@20318
   252
by (simp add: atMost_Suc)
ballarin@20318
   253
*)
ballarin@20318
   254
lemma natsum_Suc2:
ballarin@20318
   255
  "setsum f {..Suc n} = (f 0::'a::comm_monoid_add) + (setsum (%i. f (Suc i)) {..n})"
ballarin@20318
   256
proof (induct n)
ballarin@20318
   257
  case 0 show ?case by simp
ballarin@20318
   258
next
haftmann@22384
   259
  case Suc thus ?case by (simp add: add_assoc) 
ballarin@20318
   260
qed
ballarin@20318
   261
ballarin@20318
   262
lemma natsum_cong [cong]:
ballarin@20318
   263
  "!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::comm_monoid_add) |] ==>
ballarin@20318
   264
        setsum f {..j} = setsum g {..k}"
ballarin@20318
   265
by (induct j) auto
ballarin@20318
   266
ballarin@20318
   267
lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::comm_monoid_add)"
ballarin@20318
   268
by (induct n) simp_all
ballarin@20318
   269
ballarin@20318
   270
lemma natsum_add [simp]:
ballarin@20318
   271
  "!!f::nat=>'a::comm_monoid_add.
ballarin@20318
   272
   setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}"
ballarin@20318
   273
by (induct n) (simp_all add: add_ac)
ballarin@20318
   274
ballarin@20318
   275
(* Facts specific to rings *)
ballarin@20318
   276
ballarin@20318
   277
instance ring < comm_monoid_add
ballarin@20318
   278
proof
ballarin@20318
   279
  fix x y z
ballarin@20318
   280
  show "(x::'a::ring) + y = y + x" by (rule a_comm)
ballarin@20318
   281
  show "((x::'a::ring) + y) + z = x + (y + z)" by (rule a_assoc)
ballarin@20318
   282
  show "0 + (x::'a::ring) = x" by (rule l_zero)
ballarin@20318
   283
qed
ballarin@20318
   284
ballarin@20318
   285
ML {*
ballarin@20318
   286
  local
ballarin@20318
   287
    val lhss = 
ballarin@20318
   288
        ["t + u::'a::ring",
ballarin@20318
   289
	 "t - u::'a::ring",
ballarin@20318
   290
	 "t * u::'a::ring",
ballarin@20318
   291
	 "- t::'a::ring"];
ballarin@20318
   292
    fun proc ss t = 
ballarin@20318
   293
      let val rew = Goal.prove (Simplifier.the_context ss) [] []
ballarin@20318
   294
            (HOLogic.mk_Trueprop
ballarin@20318
   295
              (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t))))
ballarin@20318
   296
                (fn _ => simp_tac (Simplifier.inherit_context ss ring_ss) 1)
ballarin@20318
   297
            |> mk_meta_eq;
ballarin@20318
   298
          val (t', u) = Logic.dest_equals (Thm.prop_of rew);
ballarin@20318
   299
      in if t' aconv u 
ballarin@20318
   300
        then NONE
ballarin@20318
   301
        else SOME rew 
ballarin@20318
   302
    end;
ballarin@20318
   303
  in
ballarin@20318
   304
    val ring_simproc = Simplifier.simproc (the_context ()) "ring" lhss (K proc);
ballarin@20318
   305
  end;
ballarin@20318
   306
*}
ballarin@20318
   307
ballarin@20318
   308
ML_setup {* Addsimprocs [ring_simproc] *}
ballarin@20318
   309
ballarin@20318
   310
lemma natsum_ldistr:
ballarin@20318
   311
  "!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}"
ballarin@20318
   312
by (induct n) simp_all
ballarin@20318
   313
ballarin@20318
   314
lemma natsum_rdistr:
ballarin@20318
   315
  "!!a::'a::ring. a * setsum f {..n::nat} = setsum (%i. a * f i) {..n}"
ballarin@20318
   316
by (induct n) simp_all
ballarin@20318
   317
ballarin@20318
   318
subsection {* Integral Domains *}
ballarin@20318
   319
ballarin@20318
   320
declare one_not_zero [simp]
ballarin@20318
   321
ballarin@20318
   322
lemma zero_not_one [simp]:
ballarin@20318
   323
  "0 ~= (1::'a::domain)" 
ballarin@20318
   324
by (rule not_sym) simp
ballarin@20318
   325
ballarin@20318
   326
lemma integral_iff: (* not by default a simp rule! *)
ballarin@20318
   327
  "(a * b = (0::'a::domain)) = (a = 0 | b = 0)"
ballarin@20318
   328
proof
ballarin@20318
   329
  assume "a * b = 0" then show "a = 0 | b = 0" by (simp add: integral)
ballarin@20318
   330
next
ballarin@20318
   331
  assume "a = 0 | b = 0" then show "a * b = 0" by auto
ballarin@20318
   332
qed
ballarin@20318
   333
ballarin@20318
   334
(*
ballarin@20318
   335
lemma "(a::'a::ring) - (a - b) = b" apply simp
ballarin@20318
   336
 simproc seems to fail on this example (fixed with new term order)
ballarin@20318
   337
*)
ballarin@20318
   338
(*
ballarin@20318
   339
lemma bug: "(b::'a::ring) - (b - a) = a" by simp
ballarin@20318
   340
   simproc for rings cannot prove "(a::'a::ring) - (a - b) = b" 
ballarin@20318
   341
*)
ballarin@20318
   342
lemma m_lcancel:
ballarin@20318
   343
  assumes prem: "(a::'a::domain) ~= 0" shows conc: "(a * b = a * c) = (b = c)"
ballarin@20318
   344
proof
ballarin@20318
   345
  assume eq: "a * b = a * c"
ballarin@20318
   346
  then have "a * (b - c) = 0" by simp
ballarin@20318
   347
  then have "a = 0 | (b - c) = 0" by (simp only: integral_iff)
ballarin@20318
   348
  with prem have "b - c = 0" by auto 
ballarin@20318
   349
  then have "b = b - (b - c)" by simp 
ballarin@20318
   350
  also have "b - (b - c) = c" by simp
ballarin@20318
   351
  finally show "b = c" .
ballarin@20318
   352
next
ballarin@20318
   353
  assume "b = c" then show "a * b = a * c" by simp
ballarin@20318
   354
qed
ballarin@20318
   355
ballarin@20318
   356
lemma m_rcancel:
ballarin@20318
   357
  "(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)"
ballarin@20318
   358
by (simp add: m_lcancel)
ballarin@20318
   359
haftmann@21416
   360
lemma power_0 [simp]:
haftmann@21416
   361
  "(a::'a::ring) ^ 0 = 1" unfolding power_def by simp
haftmann@21416
   362
haftmann@21416
   363
lemma power_Suc [simp]:
haftmann@21416
   364
  "(a::'a::ring) ^ Suc n = a ^ n * a" unfolding power_def by simp
haftmann@21416
   365
haftmann@21416
   366
lemma power_one [simp]:
haftmann@21416
   367
  "1 ^ n = (1::'a::ring)" by (induct n) simp_all
haftmann@21416
   368
haftmann@21416
   369
lemma power_zero [simp]:
haftmann@21416
   370
  "n \<noteq> 0 \<Longrightarrow> 0 ^ n = (0::'a::ring)" by (induct n) simp_all
haftmann@21416
   371
haftmann@21416
   372
lemma power_mult [simp]:
haftmann@21416
   373
  "(a::'a::ring) ^ m * a ^ n = a ^ (m + n)"
haftmann@21416
   374
  by (induct m) simp_all
haftmann@21416
   375
haftmann@21416
   376
haftmann@21416
   377
section "Divisibility"
haftmann@21416
   378
haftmann@21416
   379
lemma dvd_zero_right [simp]:
haftmann@21416
   380
  "(a::'a::ring) dvd 0"
haftmann@21416
   381
proof
haftmann@21416
   382
  show "0 = a * 0" by simp
haftmann@21416
   383
qed
haftmann@21416
   384
haftmann@21416
   385
lemma dvd_zero_left:
haftmann@21416
   386
  "0 dvd (a::'a::ring) \<Longrightarrow> a = 0" unfolding dvd_def by simp
haftmann@21416
   387
haftmann@21416
   388
lemma dvd_refl_ring [simp]:
haftmann@21416
   389
  "(a::'a::ring) dvd a"
haftmann@21416
   390
proof
haftmann@21416
   391
  show "a = a * 1" by simp
haftmann@21416
   392
qed
haftmann@21416
   393
haftmann@21416
   394
lemma dvd_trans_ring:
haftmann@21416
   395
  fixes a b c :: "'a::ring"
haftmann@21416
   396
  assumes a_dvd_b: "a dvd b"
haftmann@21416
   397
  and b_dvd_c: "b dvd c"
haftmann@21416
   398
  shows "a dvd c"
haftmann@21416
   399
proof -
haftmann@21416
   400
  from a_dvd_b obtain l where "b = a * l" using dvd_def by blast
haftmann@21416
   401
  moreover from b_dvd_c obtain j where "c = b * j" using dvd_def by blast
haftmann@21416
   402
  ultimately have "c = a * (l * j)" by simp
haftmann@21416
   403
  then have "\<exists>k. c = a * k" ..
haftmann@21416
   404
  then show ?thesis using dvd_def by blast
haftmann@21416
   405
qed
haftmann@21416
   406
wenzelm@21423
   407
wenzelm@21423
   408
lemma unit_mult: 
wenzelm@21423
   409
  "!!a::'a::ring. [| a dvd 1; b dvd 1 |] ==> a * b dvd 1"
wenzelm@21423
   410
  apply (unfold dvd_def)
wenzelm@21423
   411
  apply clarify
wenzelm@21423
   412
  apply (rule_tac x = "k * ka" in exI)
wenzelm@21423
   413
  apply simp
wenzelm@21423
   414
  done
wenzelm@21423
   415
wenzelm@21423
   416
lemma unit_power: "!!a::'a::ring. a dvd 1 ==> a^n dvd 1"
wenzelm@21423
   417
  apply (induct_tac n)
wenzelm@21423
   418
   apply simp
wenzelm@21423
   419
  apply (simp add: unit_mult)
wenzelm@21423
   420
  done
wenzelm@21423
   421
wenzelm@21423
   422
lemma dvd_add_right [simp]:
wenzelm@21423
   423
  "!! a::'a::ring. [| a dvd b; a dvd c |] ==> a dvd b + c"
wenzelm@21423
   424
  apply (unfold dvd_def)
wenzelm@21423
   425
  apply clarify
wenzelm@21423
   426
  apply (rule_tac x = "k + ka" in exI)
wenzelm@21423
   427
  apply (simp add: r_distr)
wenzelm@21423
   428
  done
wenzelm@21423
   429
wenzelm@21423
   430
lemma dvd_uminus_right [simp]:
wenzelm@21423
   431
  "!! a::'a::ring. a dvd b ==> a dvd -b"
wenzelm@21423
   432
  apply (unfold dvd_def)
wenzelm@21423
   433
  apply clarify
wenzelm@21423
   434
  apply (rule_tac x = "-k" in exI)
wenzelm@21423
   435
  apply (simp add: r_minus)
wenzelm@21423
   436
  done
wenzelm@21423
   437
wenzelm@21423
   438
lemma dvd_l_mult_right [simp]:
wenzelm@21423
   439
  "!! a::'a::ring. a dvd b ==> a dvd c*b"
wenzelm@21423
   440
  apply (unfold dvd_def)
wenzelm@21423
   441
  apply clarify
wenzelm@21423
   442
  apply (rule_tac x = "c * k" in exI)
wenzelm@21423
   443
  apply simp
wenzelm@21423
   444
  done
wenzelm@21423
   445
wenzelm@21423
   446
lemma dvd_r_mult_right [simp]:
wenzelm@21423
   447
  "!! a::'a::ring. a dvd b ==> a dvd b*c"
wenzelm@21423
   448
  apply (unfold dvd_def)
wenzelm@21423
   449
  apply clarify
wenzelm@21423
   450
  apply (rule_tac x = "k * c" in exI)
wenzelm@21423
   451
  apply simp
wenzelm@21423
   452
  done
wenzelm@21423
   453
wenzelm@21423
   454
wenzelm@21423
   455
(* Inverse of multiplication *)
wenzelm@21423
   456
wenzelm@21423
   457
section "inverse"
wenzelm@21423
   458
wenzelm@21423
   459
lemma inverse_unique: "!! a::'a::ring. [| a * x = 1; a * y = 1 |] ==> x = y"
wenzelm@21423
   460
  apply (rule_tac a = "(a*y) * x" and b = "y * (a*x)" in box_equals)
wenzelm@21423
   461
    apply (simp (no_asm))
wenzelm@21423
   462
  apply auto
wenzelm@21423
   463
  done
wenzelm@21423
   464
wenzelm@21423
   465
lemma r_inverse_ring: "!! a::'a::ring. a dvd 1 ==> a * inverse a = 1"
wenzelm@21423
   466
  apply (unfold inverse_def dvd_def)
wenzelm@21423
   467
  apply (tactic {* asm_full_simp_tac (simpset () delsimprocs [ring_simproc]) 1 *})
wenzelm@21423
   468
  apply clarify
wenzelm@21423
   469
  apply (rule theI)
wenzelm@21423
   470
   apply assumption
wenzelm@21423
   471
  apply (rule inverse_unique)
wenzelm@21423
   472
   apply assumption
wenzelm@21423
   473
  apply assumption
wenzelm@21423
   474
  done
wenzelm@21423
   475
wenzelm@21423
   476
lemma l_inverse_ring: "!! a::'a::ring. a dvd 1 ==> inverse a * a = 1"
wenzelm@21423
   477
  by (simp add: r_inverse_ring)
wenzelm@21423
   478
wenzelm@21423
   479
wenzelm@21423
   480
(* Fields *)
wenzelm@21423
   481
wenzelm@21423
   482
section "Fields"
wenzelm@21423
   483
wenzelm@21423
   484
lemma field_unit [simp]: "!! a::'a::field. (a dvd 1) = (a ~= 0)"
wenzelm@21423
   485
  by (auto dest: field_ax dvd_zero_left simp add: field_one_not_zero)
wenzelm@21423
   486
wenzelm@21423
   487
lemma r_inverse [simp]: "!! a::'a::field. a ~= 0 ==> a * inverse a = 1"
wenzelm@21423
   488
  by (simp add: r_inverse_ring)
wenzelm@21423
   489
wenzelm@21423
   490
lemma l_inverse [simp]: "!! a::'a::field. a ~= 0 ==> inverse a * a= 1"
wenzelm@21423
   491
  by (simp add: l_inverse_ring)
wenzelm@21423
   492
wenzelm@21423
   493
wenzelm@21423
   494
(* fields are integral domains *)
wenzelm@21423
   495
wenzelm@21423
   496
lemma field_integral: "!! a::'a::field. a * b = 0 ==> a = 0 | b = 0"
wenzelm@21423
   497
  apply (tactic "Step_tac 1")
wenzelm@21423
   498
  apply (rule_tac a = " (a*b) * inverse b" in box_equals)
wenzelm@21423
   499
    apply (rule_tac [3] refl)
wenzelm@21423
   500
   prefer 2
wenzelm@21423
   501
   apply (simp (no_asm))
wenzelm@21423
   502
   apply auto
wenzelm@21423
   503
  done
wenzelm@21423
   504
wenzelm@21423
   505
wenzelm@21423
   506
(* fields are factorial domains *)
wenzelm@21423
   507
wenzelm@21423
   508
lemma field_fact_prime: "!! a::'a::field. irred a ==> prime a"
wenzelm@21423
   509
  unfolding prime_def irred_def by (blast intro: field_ax)
haftmann@21416
   510
ballarin@20318
   511
end