src/HOL/Algebra/abstract/Ring2.thy
author haftmann
Sat, 18 Nov 2006 00:20:24 +0100
changeset 21416 f23e4e75dfd3
parent 20318 0e0ea63fe768
child 21423 6cdd0589aa73
permissions -rw-r--r--
dvd_def now with object equality
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     1
(*
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     2
  Title:     The algebraic hierarchy of rings as axiomatic classes
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     3
  Id:        $Id$
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     4
  Author:    Clemens Ballarin, started 9 December 1996
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     5
  Copyright: Clemens Ballarin
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     6
*)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     7
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     8
header {* The algebraic hierarchy of rings as axiomatic classes *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     9
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    10
theory Ring2 imports Main
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    11
uses ("order.ML") begin
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    12
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    13
section {* Constants *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    14
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    15
text {* Most constants are already declared by HOL. *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    16
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    17
consts
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    18
  assoc         :: "['a::times, 'a] => bool"              (infixl 50)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    19
  irred         :: "'a::{zero, one, times} => bool"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    20
  prime         :: "'a::{zero, one, times} => bool"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    21
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    22
section {* Axioms *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    23
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    24
subsection {* Ring axioms *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    25
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    26
axclass ring < zero, one, plus, minus, times, inverse, power
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    27
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    28
  a_assoc:      "(a + b) + c = a + (b + c)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    29
  l_zero:       "0 + a = a"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    30
  l_neg:        "(-a) + a = 0"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    31
  a_comm:       "a + b = b + a"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    32
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    33
  m_assoc:      "(a * b) * c = a * (b * c)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    34
  l_one:        "1 * a = a"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    35
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    36
  l_distr:      "(a + b) * c = a * c + b * c"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    37
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    38
  m_comm:       "a * b = b * a"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    39
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    40
  -- {* Definition of derived operations *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    41
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    42
  minus_def:    "a - b = a + (-b)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    43
  inverse_def:  "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    44
  divide_def:   "a / b = a * inverse b"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    45
  power_def:    "a ^ n = nat_rec 1 (%u b. b * a) n"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    46
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    47
defs
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    48
  assoc_def:    "a assoc b == a dvd b & b dvd a"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    49
  irred_def:    "irred a == a ~= 0 & ~ a dvd 1
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    50
                          & (ALL d. d dvd a --> d dvd 1 | a dvd d)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    51
  prime_def:    "prime p == p ~= 0 & ~ p dvd 1
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    52
                          & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    53
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    54
subsection {* Integral domains *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    55
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    56
axclass
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    57
  "domain" < ring
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    58
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    59
  one_not_zero: "1 ~= 0"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    60
  integral:     "a * b = 0 ==> a = 0 | b = 0"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    61
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    62
subsection {* Factorial domains *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    63
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    64
axclass
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    65
  factorial < "domain"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    66
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    67
(*
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    68
  Proper definition using divisor chain condition currently not supported.
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    69
  factorial_divisor:    "wf {(a, b). a dvd b & ~ (b dvd a)}"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    70
*)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    71
  factorial_divisor:	"True"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    72
  factorial_prime:      "irred a ==> prime a"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    73
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    74
subsection {* Euclidean domains *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    75
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    76
(*
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    77
axclass
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    78
  euclidean < "domain"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    79
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    80
  euclidean_ax:  "b ~= 0 ==> Ex (% (q, r, e_size::('a::ringS)=>nat).
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    81
                   a = b * q + r & e_size r < e_size b)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    82
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    83
  Nothing has been proved about Euclidean domains, yet.
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    84
  Design question:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    85
    Fix quo, rem and e_size as constants that are axiomatised with
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    86
    euclidean_ax?
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    87
    - advantage: more pragmatic and easier to use
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    88
    - disadvantage: for every type, one definition of quo and rem will
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    89
        be fixed, users may want to use differing ones;
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    90
        also, it seems not possible to prove that fields are euclidean
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    91
        domains, because that would require generic (type-independent)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    92
        definitions of quo and rem.
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    93
*)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    94
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    95
subsection {* Fields *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    96
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    97
axclass
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    98
  field < ring
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    99
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   100
  field_one_not_zero:    "1 ~= 0"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   101
                (* Avoid a common superclass as the first thing we will
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   102
                   prove about fields is that they are domains. *)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   103
  field_ax:        "a ~= 0 ==> a dvd 1"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   104
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   105
section {* Basic facts *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   106
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   107
subsection {* Normaliser for rings *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   108
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   109
use "order.ML"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   110
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   111
method_setup ring =
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   112
  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (full_simp_tac ring_ss)) *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   113
  {* computes distributive normal form in rings *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   114
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   115
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   116
subsection {* Rings and the summation operator *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   117
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   118
(* Basic facts --- move to HOL!!! *)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   119
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   120
(* needed because natsum_cong (below) disables atMost_0 *)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   121
lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::comm_monoid_add)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   122
by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   123
(*
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   124
lemma natsum_Suc [simp]:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   125
  "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::comm_monoid_add)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   126
by (simp add: atMost_Suc)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   127
*)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   128
lemma natsum_Suc2:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   129
  "setsum f {..Suc n} = (f 0::'a::comm_monoid_add) + (setsum (%i. f (Suc i)) {..n})"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   130
proof (induct n)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   131
  case 0 show ?case by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   132
next
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   133
  case Suc thus ?case by (simp add: semigroup_add_class.add_assoc) 
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   134
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   135
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   136
lemma natsum_cong [cong]:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   137
  "!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::comm_monoid_add) |] ==>
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   138
        setsum f {..j} = setsum g {..k}"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   139
by (induct j) auto
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   140
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   141
lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::comm_monoid_add)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   142
by (induct n) simp_all
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   143
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   144
lemma natsum_add [simp]:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   145
  "!!f::nat=>'a::comm_monoid_add.
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   146
   setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   147
by (induct n) (simp_all add: add_ac)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   148
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   149
(* Facts specific to rings *)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   150
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   151
instance ring < comm_monoid_add
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   152
proof
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   153
  fix x y z
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   154
  show "(x::'a::ring) + y = y + x" by (rule a_comm)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   155
  show "((x::'a::ring) + y) + z = x + (y + z)" by (rule a_assoc)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   156
  show "0 + (x::'a::ring) = x" by (rule l_zero)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   157
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   158
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   159
ML {*
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   160
  local
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   161
    val lhss = 
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   162
        ["t + u::'a::ring",
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   163
	 "t - u::'a::ring",
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   164
	 "t * u::'a::ring",
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   165
	 "- t::'a::ring"];
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   166
    fun proc ss t = 
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   167
      let val rew = Goal.prove (Simplifier.the_context ss) [] []
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   168
            (HOLogic.mk_Trueprop
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   169
              (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t))))
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   170
                (fn _ => simp_tac (Simplifier.inherit_context ss ring_ss) 1)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   171
            |> mk_meta_eq;
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   172
          val (t', u) = Logic.dest_equals (Thm.prop_of rew);
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   173
      in if t' aconv u 
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   174
        then NONE
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   175
        else SOME rew 
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   176
    end;
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   177
  in
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   178
    val ring_simproc = Simplifier.simproc (the_context ()) "ring" lhss (K proc);
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   179
  end;
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   180
*}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   181
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   182
ML_setup {* Addsimprocs [ring_simproc] *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   183
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   184
lemma natsum_ldistr:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   185
  "!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   186
by (induct n) simp_all
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   187
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   188
lemma natsum_rdistr:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   189
  "!!a::'a::ring. a * setsum f {..n::nat} = setsum (%i. a * f i) {..n}"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   190
by (induct n) simp_all
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   191
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   192
subsection {* Integral Domains *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   193
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   194
declare one_not_zero [simp]
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   195
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   196
lemma zero_not_one [simp]:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   197
  "0 ~= (1::'a::domain)" 
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   198
by (rule not_sym) simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   199
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   200
lemma integral_iff: (* not by default a simp rule! *)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   201
  "(a * b = (0::'a::domain)) = (a = 0 | b = 0)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   202
proof
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   203
  assume "a * b = 0" then show "a = 0 | b = 0" by (simp add: integral)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   204
next
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   205
  assume "a = 0 | b = 0" then show "a * b = 0" by auto
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   206
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   207
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   208
(*
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   209
lemma "(a::'a::ring) - (a - b) = b" apply simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   210
 simproc seems to fail on this example (fixed with new term order)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   211
*)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   212
(*
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   213
lemma bug: "(b::'a::ring) - (b - a) = a" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   214
   simproc for rings cannot prove "(a::'a::ring) - (a - b) = b" 
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   215
*)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   216
lemma m_lcancel:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   217
  assumes prem: "(a::'a::domain) ~= 0" shows conc: "(a * b = a * c) = (b = c)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   218
proof
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   219
  assume eq: "a * b = a * c"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   220
  then have "a * (b - c) = 0" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   221
  then have "a = 0 | (b - c) = 0" by (simp only: integral_iff)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   222
  with prem have "b - c = 0" by auto 
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   223
  then have "b = b - (b - c)" by simp 
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   224
  also have "b - (b - c) = c" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   225
  finally show "b = c" .
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   226
next
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   227
  assume "b = c" then show "a * b = a * c" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   228
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   229
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   230
lemma m_rcancel:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   231
  "(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   232
by (simp add: m_lcancel)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   233
21416
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   234
lemma power_0 [simp]:
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   235
  "(a::'a::ring) ^ 0 = 1" unfolding power_def by simp
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   236
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   237
lemma power_Suc [simp]:
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   238
  "(a::'a::ring) ^ Suc n = a ^ n * a" unfolding power_def by simp
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   239
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   240
lemma power_one [simp]:
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   241
  "1 ^ n = (1::'a::ring)" by (induct n) simp_all
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   242
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   243
lemma power_zero [simp]:
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   244
  "n \<noteq> 0 \<Longrightarrow> 0 ^ n = (0::'a::ring)" by (induct n) simp_all
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   245
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   246
lemma power_mult [simp]:
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   247
  "(a::'a::ring) ^ m * a ^ n = a ^ (m + n)"
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   248
  by (induct m) simp_all
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   249
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   250
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   251
section "Divisibility"
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   252
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   253
lemma dvd_zero_right [simp]:
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   254
  "(a::'a::ring) dvd 0"
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   255
proof
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   256
  show "0 = a * 0" by simp
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   257
qed
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   258
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   259
lemma dvd_zero_left:
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   260
  "0 dvd (a::'a::ring) \<Longrightarrow> a = 0" unfolding dvd_def by simp
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   261
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   262
lemma dvd_refl_ring [simp]:
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   263
  "(a::'a::ring) dvd a"
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   264
proof
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   265
  show "a = a * 1" by simp
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   266
qed
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   267
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   268
lemma dvd_trans_ring:
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   269
  fixes a b c :: "'a::ring"
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   270
  assumes a_dvd_b: "a dvd b"
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   271
  and b_dvd_c: "b dvd c"
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   272
  shows "a dvd c"
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   273
proof -
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   274
  from a_dvd_b obtain l where "b = a * l" using dvd_def by blast
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   275
  moreover from b_dvd_c obtain j where "c = b * j" using dvd_def by blast
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   276
  ultimately have "c = a * (l * j)" by simp
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   277
  then have "\<exists>k. c = a * k" ..
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   278
  then show ?thesis using dvd_def by blast
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   279
qed
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   280
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   281
lemma dvd_def':
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   282
  "m dvd n \<equiv> \<exists>k. n = m * k" unfolding dvd_def by simp
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   283
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   284
end