src/HOL/Algebra/abstract/Ring.thy
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 16417 9bc16273c2d4
child 16973 b2a894562b8f
permissions -rw-r--r--
Constant "If" is now local
paulson@7998
     1
(*
ballarin@13735
     2
  Title:     The algebraic hierarchy of rings as axiomatic classes
ballarin@13735
     3
  Id:        $Id$
ballarin@13735
     4
  Author:    Clemens Ballarin, started 9 December 1996
ballarin@13735
     5
  Copyright: Clemens Ballarin
paulson@7998
     6
*)
paulson@7998
     7
ballarin@13735
     8
header {* The algebraic hierarchy of rings as axiomatic classes *}
paulson@7998
     9
haftmann@16417
    10
theory Ring imports Main
haftmann@16417
    11
uses ("order.ML") begin
paulson@7998
    12
ballarin@13735
    13
section {* Constants *}
ballarin@13735
    14
ballarin@13735
    15
text {* Most constants are already declared by HOL. *}
paulson@7998
    16
paulson@7998
    17
consts
ballarin@13735
    18
  assoc         :: "['a::times, 'a] => bool"              (infixl 50)
ballarin@13735
    19
  irred         :: "'a::{zero, one, times} => bool"
ballarin@13735
    20
  prime         :: "'a::{zero, one, times} => bool"
ballarin@13735
    21
ballarin@13735
    22
section {* Axioms *}
ballarin@13735
    23
ballarin@13735
    24
subsection {* Ring axioms *}
ballarin@13735
    25
ballarin@13735
    26
axclass ring < zero, one, plus, minus, times, inverse, power
ballarin@13735
    27
ballarin@13735
    28
  a_assoc:      "(a + b) + c = a + (b + c)"
ballarin@13735
    29
  l_zero:       "0 + a = a"
ballarin@13735
    30
  l_neg:        "(-a) + a = 0"
ballarin@13735
    31
  a_comm:       "a + b = b + a"
ballarin@13735
    32
ballarin@13735
    33
  m_assoc:      "(a * b) * c = a * (b * c)"
ballarin@13735
    34
  l_one:        "1 * a = a"
paulson@7998
    35
ballarin@13735
    36
  l_distr:      "(a + b) * c = a * c + b * c"
ballarin@13735
    37
ballarin@13735
    38
  m_comm:       "a * b = b * a"
ballarin@13735
    39
ballarin@13735
    40
  -- {* Definition of derived operations *}
paulson@7998
    41
ballarin@13735
    42
  minus_def:    "a - b = a + (-b)"
ballarin@13735
    43
  inverse_def:  "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)"
ballarin@13735
    44
  divide_def:   "a / b = a * inverse b"
ballarin@13735
    45
  power_def:    "a ^ n = nat_rec 1 (%u b. b * a) n"
paulson@7998
    46
ballarin@13735
    47
defs
ballarin@13735
    48
  assoc_def:    "a assoc b == a dvd b & b dvd a"
ballarin@13735
    49
  irred_def:    "irred a == a ~= 0 & ~ a dvd 1
ballarin@13735
    50
                          & (ALL d. d dvd a --> d dvd 1 | a dvd d)"
ballarin@13735
    51
  prime_def:    "prime p == p ~= 0 & ~ p dvd 1
ballarin@13735
    52
                          & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)"
ballarin@13735
    53
ballarin@13735
    54
subsection {* Integral domains *}
paulson@7998
    55
paulson@7998
    56
axclass
ballarin@13735
    57
  "domain" < ring
paulson@7998
    58
ballarin@13735
    59
  one_not_zero: "1 ~= 0"
ballarin@13735
    60
  integral:     "a * b = 0 ==> a = 0 | b = 0"
paulson@7998
    61
ballarin@13735
    62
subsection {* Factorial domains *}
paulson@7998
    63
paulson@7998
    64
axclass
ballarin@13735
    65
  factorial < "domain"
paulson@7998
    66
paulson@7998
    67
(*
paulson@7998
    68
  Proper definition using divisor chain condition currently not supported.
ballarin@13735
    69
  factorial_divisor:    "wf {(a, b). a dvd b & ~ (b dvd a)}"
paulson@7998
    70
*)
ballarin@13735
    71
  factorial_divisor:	"True"
ballarin@13735
    72
  factorial_prime:      "irred a ==> prime a"
paulson@7998
    73
ballarin@13735
    74
subsection {* Euclidean domains *}
paulson@7998
    75
paulson@7998
    76
(*
paulson@7998
    77
axclass
ballarin@13735
    78
  euclidean < "domain"
paulson@7998
    79
ballarin@13735
    80
  euclidean_ax:  "b ~= 0 ==> Ex (% (q, r, e_size::('a::ringS)=>nat).
paulson@7998
    81
                   a = b * q + r & e_size r < e_size b)"
paulson@7998
    82
ballarin@13735
    83
  Nothing has been proved about Euclidean domains, yet.
paulson@7998
    84
  Design question:
paulson@7998
    85
    Fix quo, rem and e_size as constants that are axiomatised with
paulson@7998
    86
    euclidean_ax?
paulson@7998
    87
    - advantage: more pragmatic and easier to use
paulson@7998
    88
    - disadvantage: for every type, one definition of quo and rem will
paulson@7998
    89
        be fixed, users may want to use differing ones;
paulson@7998
    90
        also, it seems not possible to prove that fields are euclidean
paulson@7998
    91
        domains, because that would require generic (type-independent)
paulson@7998
    92
        definitions of quo and rem.
paulson@7998
    93
*)
paulson@7998
    94
ballarin@13735
    95
subsection {* Fields *}
paulson@7998
    96
paulson@7998
    97
axclass
paulson@7998
    98
  field < ring
paulson@7998
    99
ballarin@13735
   100
  field_one_not_zero:    "1 ~= 0"
ballarin@13735
   101
                (* Avoid a common superclass as the first thing we will
ballarin@13735
   102
                   prove about fields is that they are domains. *)
ballarin@13735
   103
  field_ax:        "a ~= 0 ==> a dvd 1"
ballarin@13735
   104
ballarin@13735
   105
section {* Basic facts *}
ballarin@13735
   106
ballarin@13735
   107
subsection {* Normaliser for rings *}
ballarin@13735
   108
ballarin@13735
   109
use "order.ML"
ballarin@13735
   110
ballarin@13735
   111
method_setup ring =
ballarin@13735
   112
  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (full_simp_tac ring_ss)) *}
ballarin@13735
   113
  {* computes distributive normal form in rings *}
ballarin@13735
   114
ballarin@13735
   115
ballarin@13735
   116
subsection {* Rings and the summation operator *}
ballarin@13735
   117
ballarin@13735
   118
(* Basic facts --- move to HOL!!! *)
ballarin@13735
   119
nipkow@16052
   120
(* needed because natsum_cong (below) disables atMost_0 *)
obua@14738
   121
lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::comm_monoid_add)"
ballarin@13735
   122
by simp
nipkow@16052
   123
(*
ballarin@13735
   124
lemma natsum_Suc [simp]:
obua@14738
   125
  "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::comm_monoid_add)"
ballarin@13735
   126
by (simp add: atMost_Suc)
nipkow@16052
   127
*)
ballarin@13735
   128
lemma natsum_Suc2:
nipkow@16052
   129
  "setsum f {..Suc n} = (f 0::'a::comm_monoid_add) + (setsum (%i. f (Suc i)) {..n})"
ballarin@13735
   130
proof (induct n)
ballarin@13735
   131
  case 0 show ?case by simp
ballarin@13735
   132
next
obua@14738
   133
  case Suc thus ?case by (simp add: semigroup_add.add_assoc) 
ballarin@13735
   134
qed
ballarin@13735
   135
ballarin@13735
   136
lemma natsum_cong [cong]:
obua@14738
   137
  "!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::comm_monoid_add) |] ==>
ballarin@13735
   138
        setsum f {..j} = setsum g {..k}"
ballarin@13735
   139
by (induct j) auto
ballarin@13735
   140
obua@14738
   141
lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::comm_monoid_add)"
ballarin@13735
   142
by (induct n) simp_all
ballarin@13735
   143
ballarin@13735
   144
lemma natsum_add [simp]:
obua@14738
   145
  "!!f::nat=>'a::comm_monoid_add.
ballarin@13735
   146
   setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}"
obua@14738
   147
by (induct n) (simp_all add: add_ac)
ballarin@13735
   148
ballarin@13735
   149
(* Facts specific to rings *)
ballarin@13735
   150
obua@14738
   151
instance ring < comm_monoid_add
ballarin@13735
   152
proof
ballarin@13735
   153
  fix x y z
ballarin@13735
   154
  show "(x::'a::ring) + y = y + x" by (rule a_comm)
ballarin@13735
   155
  show "((x::'a::ring) + y) + z = x + (y + z)" by (rule a_assoc)
ballarin@13735
   156
  show "0 + (x::'a::ring) = x" by (rule l_zero)
ballarin@13735
   157
qed
ballarin@13735
   158
ballarin@13735
   159
ML {*
ballarin@13735
   160
  local
ballarin@13735
   161
    val lhss = 
wenzelm@15020
   162
        ["t + u::'a::ring",
wenzelm@15020
   163
	 "t - u::'a::ring",
wenzelm@15020
   164
	 "t * u::'a::ring",
wenzelm@15020
   165
	 "- t::'a::ring"];
ballarin@13735
   166
    fun proc sg _ t = 
ballarin@13735
   167
      let val rew = Tactic.prove sg [] []
ballarin@13735
   168
            (HOLogic.mk_Trueprop
ballarin@13735
   169
              (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t))))
ballarin@13735
   170
                (fn _ => simp_tac ring_ss 1)
ballarin@13735
   171
            |> mk_meta_eq;
ballarin@13735
   172
          val (t', u) = Logic.dest_equals (Thm.prop_of rew);
ballarin@13735
   173
      in if t' aconv u 
skalberg@15531
   174
        then NONE
skalberg@15531
   175
        else SOME rew 
ballarin@13735
   176
    end;
ballarin@13735
   177
  in
wenzelm@15020
   178
    val ring_simproc = Simplifier.simproc (sign_of (the_context ())) "ring" lhss proc;
ballarin@13735
   179
  end;
ballarin@13735
   180
*}
ballarin@13735
   181
ballarin@13735
   182
ML_setup {* Addsimprocs [ring_simproc] *}
ballarin@13735
   183
ballarin@13735
   184
lemma natsum_ldistr:
ballarin@13735
   185
  "!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}"
ballarin@13735
   186
by (induct n) simp_all
ballarin@13735
   187
ballarin@13735
   188
lemma natsum_rdistr:
ballarin@13735
   189
  "!!a::'a::ring. a * setsum f {..n::nat} = setsum (%i. a * f i) {..n}"
ballarin@13735
   190
by (induct n) simp_all
ballarin@13735
   191
ballarin@13735
   192
subsection {* Integral Domains *}
ballarin@13735
   193
ballarin@13735
   194
declare one_not_zero [simp]
ballarin@13735
   195
ballarin@13735
   196
lemma zero_not_one [simp]:
ballarin@13735
   197
  "0 ~= (1::'a::domain)" 
ballarin@13735
   198
by (rule not_sym) simp
ballarin@13735
   199
ballarin@13735
   200
lemma integral_iff: (* not by default a simp rule! *)
ballarin@13735
   201
  "(a * b = (0::'a::domain)) = (a = 0 | b = 0)"
ballarin@13735
   202
proof
ballarin@13735
   203
  assume "a * b = 0" then show "a = 0 | b = 0" by (simp add: integral)
ballarin@13735
   204
next
ballarin@13735
   205
  assume "a = 0 | b = 0" then show "a * b = 0" by auto
ballarin@13735
   206
qed
ballarin@13735
   207
ballarin@13735
   208
(*
ballarin@13735
   209
lemma "(a::'a::ring) - (a - b) = b" apply simp
ballarin@13783
   210
 simproc seems to fail on this example (fixed with new term order)
ballarin@13735
   211
*)
ballarin@13783
   212
(*
ballarin@13735
   213
lemma bug: "(b::'a::ring) - (b - a) = a" by simp
ballarin@13783
   214
   simproc for rings cannot prove "(a::'a::ring) - (a - b) = b" 
ballarin@13783
   215
*)
ballarin@13735
   216
lemma m_lcancel:
ballarin@13735
   217
  assumes prem: "(a::'a::domain) ~= 0" shows conc: "(a * b = a * c) = (b = c)"
ballarin@13735
   218
proof
ballarin@13735
   219
  assume eq: "a * b = a * c"
ballarin@13735
   220
  then have "a * (b - c) = 0" by simp
ballarin@13735
   221
  then have "a = 0 | (b - c) = 0" by (simp only: integral_iff)
ballarin@13735
   222
  with prem have "b - c = 0" by auto 
ballarin@13735
   223
  then have "b = b - (b - c)" by simp 
ballarin@13783
   224
  also have "b - (b - c) = c" by simp
ballarin@13735
   225
  finally show "b = c" .
ballarin@13735
   226
next
ballarin@13735
   227
  assume "b = c" then show "a * b = a * c" by simp
ballarin@13735
   228
qed
ballarin@13735
   229
ballarin@13735
   230
lemma m_rcancel:
ballarin@13735
   231
  "(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)"
ballarin@13735
   232
by (simp add: m_lcancel)
paulson@7998
   233
paulson@7998
   234
end