src/HOL/Algebra/abstract/Ring2.thy
author wenzelm
Thu, 12 May 2011 21:14:03 +0200
changeset 42768 4db4a8b164c1
parent 39159 0dec18004e75
child 42793 88bee9f6eec7
permissions -rw-r--r--
modernized simproc_setup; misc tuning and simplification;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29269
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents: 27651
diff changeset
     1
(*  Title:     HOL/Algebra/abstract/Ring2.thy
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents: 27651
diff changeset
     2
    Author:    Clemens Ballarin
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents: 27651
diff changeset
     3
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents: 27651
diff changeset
     4
The algebraic hierarchy of rings as axiomatic classes.
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     5
*)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     6
27542
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
     7
header {* The algebraic hierarchy of rings as type classes *}
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     8
27542
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
     9
theory Ring2
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
    10
imports Main
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
    11
begin
20318
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
subsection {* Ring axioms *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    14
31001
7e6ffd8f51a9 cleaned up theory power further
haftmann
parents: 30968
diff changeset
    15
class ring = zero + one + plus + minus + uminus + times + inverse + power + dvd +
27542
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
    16
  assumes a_assoc:      "(a + b) + c = a + (b + c)"
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
    17
  and l_zero:           "0 + a = a"
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
    18
  and l_neg:            "(-a) + a = 0"
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
    19
  and a_comm:           "a + b = b + a"
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    20
27542
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
    21
  assumes m_assoc:      "(a * b) * c = a * (b * c)"
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
    22
  and l_one:            "1 * a = a"
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    23
27542
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
    24
  assumes l_distr:      "(a + b) * c = a * c + b * c"
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    25
27542
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
    26
  assumes m_comm:       "a * b = b * a"
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    27
27542
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
    28
  assumes minus_def:    "a - b = a + (-b)"
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
    29
  and inverse_def:      "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)"
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
    30
  and divide_def:       "a / b = a * inverse b"
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
    31
begin
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    32
35848
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35408
diff changeset
    33
definition
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35408
diff changeset
    34
  assoc :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "assoc" 50)
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35408
diff changeset
    35
  where "a assoc b \<longleftrightarrow> a dvd b & b dvd a"
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    36
35848
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35408
diff changeset
    37
definition
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35408
diff changeset
    38
  irred :: "'a \<Rightarrow> bool" where
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35408
diff changeset
    39
  "irred a \<longleftrightarrow> a ~= 0 & ~ a dvd 1 & (ALL d. d dvd a --> d dvd 1 | a dvd d)"
27542
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
    40
35848
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35408
diff changeset
    41
definition
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35408
diff changeset
    42
  prime :: "'a \<Rightarrow> bool" where
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 35408
diff changeset
    43
  "prime p \<longleftrightarrow> p ~= 0 & ~ p dvd 1 & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)"
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    44
27542
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
    45
end
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
    46
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
    47
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    48
subsection {* Integral domains *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    49
27542
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
    50
class "domain" = ring +
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
    51
  assumes one_not_zero: "1 ~= 0"
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
    52
  and integral: "a * b = 0 ==> a = 0 | b = 0"
20318
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 {* Factorial domains *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    55
27542
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
    56
class factorial = "domain" +
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    57
(*
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    58
  Proper definition using divisor chain condition currently not supported.
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    59
  factorial_divisor:    "wf {(a, b). a dvd b & ~ (b dvd a)}"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    60
*)
29665
2b956243d123 explicit check for exactly one type variable in class specification elements
haftmann
parents: 29269
diff changeset
    61
  (*assumes factorial_divisor: "True"*)
2b956243d123 explicit check for exactly one type variable in class specification elements
haftmann
parents: 29269
diff changeset
    62
  assumes factorial_prime: "irred a ==> prime a"
2b956243d123 explicit check for exactly one type variable in class specification elements
haftmann
parents: 29269
diff changeset
    63
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    64
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    65
subsection {* Euclidean domains *}
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
(*
35330
e7eb254db165 tuned comment
haftmann
parents: 35267
diff changeset
    68
class euclidean = "domain" +
e7eb254db165 tuned comment
haftmann
parents: 35267
diff changeset
    69
  assumes euclidean_ax: "b ~= 0 ==> Ex (% (q, r, e_size::('a::ringS)=>nat).
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    70
                   a = b * q + r & e_size r < e_size b)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    71
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    72
  Nothing has been proved about Euclidean domains, yet.
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    73
  Design question:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    74
    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
    75
    euclidean_ax?
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    76
    - advantage: more pragmatic and easier to use
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    77
    - disadvantage: for every type, one definition of quo and rem will
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    78
        be fixed, users may want to use differing ones;
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    79
        also, it seems not possible to prove that fields are euclidean
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    80
        domains, because that would require generic (type-independent)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    81
        definitions of quo and rem.
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
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    84
subsection {* Fields *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    85
27542
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
    86
class field = ring +
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
    87
  assumes field_one_not_zero: "1 ~= 0"
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    88
                (* Avoid a common superclass as the first thing we will
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    89
                   prove about fields is that they are domains. *)
27542
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
    90
  and field_ax: "a ~= 0 ==> a dvd 1"
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    91
21423
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
    92
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    93
section {* Basic facts *}
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 {* Normaliser for rings *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    96
21423
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
    97
(* derived rewrite rules *)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
    98
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
    99
lemma a_lcomm: "(a::'a::ring)+(b+c) = b+(a+c)"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   100
  apply (rule a_comm [THEN trans])
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   101
  apply (rule a_assoc [THEN trans])
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   102
  apply (rule a_comm [THEN arg_cong])
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   103
  done
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   104
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   105
lemma r_zero: "(a::'a::ring) + 0 = a"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   106
  apply (rule a_comm [THEN trans])
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   107
  apply (rule l_zero)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   108
  done
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   109
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   110
lemma r_neg: "(a::'a::ring) + (-a) = 0"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   111
  apply (rule a_comm [THEN trans])
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   112
  apply (rule l_neg)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   113
  done
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   114
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   115
lemma r_neg2: "(a::'a::ring) + (-a + b) = b"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   116
  apply (rule a_assoc [symmetric, THEN trans])
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   117
  apply (simp add: r_neg l_zero)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   118
  done
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   119
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   120
lemma r_neg1: "-(a::'a::ring) + (a + b) = b"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   121
  apply (rule a_assoc [symmetric, THEN trans])
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   122
  apply (simp add: l_neg l_zero)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   123
  done
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   124
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   125
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   126
(* auxiliary *)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   127
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   128
lemma a_lcancel: "!! a::'a::ring. a + b = a + c ==> b = c"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   129
  apply (rule box_equals)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   130
  prefer 2
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   131
  apply (rule l_zero)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   132
  prefer 2
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   133
  apply (rule l_zero)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   134
  apply (rule_tac a1 = a in l_neg [THEN subst])
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   135
  apply (simp add: a_assoc)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   136
  done
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   137
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   138
lemma minus_add: "-((a::'a::ring) + b) = (-a) + (-b)"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   139
  apply (rule_tac a = "a + b" in a_lcancel)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   140
  apply (simp add: r_neg l_neg l_zero a_assoc a_comm a_lcomm)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   141
  done
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   142
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   143
lemma minus_minus: "-(-(a::'a::ring)) = a"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   144
  apply (rule a_lcancel)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   145
  apply (rule r_neg [THEN trans])
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   146
  apply (rule l_neg [symmetric])
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   147
  done
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   148
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   149
lemma minus0: "- 0 = (0::'a::ring)"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   150
  apply (rule a_lcancel)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   151
  apply (rule r_neg [THEN trans])
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   152
  apply (rule l_zero [symmetric])
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   153
  done
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   154
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   155
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   156
(* derived rules for multiplication *)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   157
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   158
lemma m_lcomm: "(a::'a::ring)*(b*c) = b*(a*c)"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   159
  apply (rule m_comm [THEN trans])
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   160
  apply (rule m_assoc [THEN trans])
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   161
  apply (rule m_comm [THEN arg_cong])
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   162
  done
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   163
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   164
lemma r_one: "(a::'a::ring) * 1 = a"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   165
  apply (rule m_comm [THEN trans])
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   166
  apply (rule l_one)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   167
  done
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   168
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   169
lemma r_distr: "(a::'a::ring) * (b + c) = a * b + a * c"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   170
  apply (rule m_comm [THEN trans])
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   171
  apply (rule l_distr [THEN trans])
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   172
  apply (simp add: m_comm)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   173
  done
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   174
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   175
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   176
(* the following proof is from Jacobson, Basic Algebra I, pp. 88-89 *)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   177
lemma l_null: "0 * (a::'a::ring) = 0"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   178
  apply (rule a_lcancel)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   179
  apply (rule l_distr [symmetric, THEN trans])
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   180
  apply (simp add: r_zero)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   181
  done
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   182
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   183
lemma r_null: "(a::'a::ring) * 0 = 0"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   184
  apply (rule m_comm [THEN trans])
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   185
  apply (rule l_null)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   186
  done
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   187
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   188
lemma l_minus: "(-(a::'a::ring)) * b = - (a * b)"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   189
  apply (rule a_lcancel)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   190
  apply (rule r_neg [symmetric, THEN [2] trans])
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   191
  apply (rule l_distr [symmetric, THEN trans])
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   192
  apply (simp add: l_null r_neg)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   193
  done
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   194
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   195
lemma r_minus: "(a::'a::ring) * (-b) = - (a * b)"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   196
  apply (rule a_lcancel)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   197
  apply (rule r_neg [symmetric, THEN [2] trans])
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   198
  apply (rule r_distr [symmetric, THEN trans])
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   199
  apply (simp add: r_null r_neg)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   200
  done
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   201
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   202
(*** Term order for commutative rings ***)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   203
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   204
ML {*
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   205
fun ring_ord (Const (a, _)) =
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   206
    find_index (fn a' => a = a')
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 34974
diff changeset
   207
      [@{const_name Groups.zero}, @{const_name Groups.plus}, @{const_name Groups.uminus},
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 34974
diff changeset
   208
        @{const_name Groups.minus}, @{const_name Groups.one}, @{const_name Groups.times}]
21423
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   209
  | ring_ord _ = ~1;
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   210
35408
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 35330
diff changeset
   211
fun termless_ring (a, b) = (Term_Ord.term_lpo ring_ord (a, b) = LESS);
21423
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   212
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   213
val ring_ss = HOL_basic_ss settermless termless_ring addsimps
39159
0dec18004e75 more antiquotations;
wenzelm
parents: 38715
diff changeset
   214
  [@{thm a_assoc}, @{thm l_zero}, @{thm l_neg}, @{thm a_comm}, @{thm m_assoc},
0dec18004e75 more antiquotations;
wenzelm
parents: 38715
diff changeset
   215
   @{thm l_one}, @{thm l_distr}, @{thm m_comm}, @{thm minus_def},
0dec18004e75 more antiquotations;
wenzelm
parents: 38715
diff changeset
   216
   @{thm r_zero}, @{thm r_neg}, @{thm r_neg2}, @{thm r_neg1}, @{thm minus_add},
0dec18004e75 more antiquotations;
wenzelm
parents: 38715
diff changeset
   217
   @{thm minus_minus}, @{thm minus0}, @{thm a_lcomm}, @{thm m_lcomm}, (*@{thm r_one},*)
0dec18004e75 more antiquotations;
wenzelm
parents: 38715
diff changeset
   218
   @{thm r_distr}, @{thm l_null}, @{thm r_null}, @{thm l_minus}, @{thm r_minus}];
21423
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   219
*}   (* Note: r_one is not necessary in ring_ss *)
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   220
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   221
method_setup ring =
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
   222
  {* Scan.succeed (K (SIMPLE_METHOD' (full_simp_tac ring_ss))) *}
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   223
  {* computes distributive normal form in rings *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   224
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   225
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   226
subsection {* Rings and the summation operator *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   227
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   228
(* Basic facts --- move to HOL!!! *)
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
(* needed because natsum_cong (below) disables atMost_0 *)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   231
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
   232
by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   233
(*
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   234
lemma natsum_Suc [simp]:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   235
  "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
   236
by (simp add: atMost_Suc)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   237
*)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   238
lemma natsum_Suc2:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   239
  "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
   240
proof (induct n)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   241
  case 0 show ?case by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   242
next
32449
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32010
diff changeset
   243
  case Suc thus ?case by (simp add: add_assoc)
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   244
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   245
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   246
lemma natsum_cong [cong]:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   247
  "!!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
   248
        setsum f {..j} = setsum g {..k}"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   249
by (induct j) auto
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   250
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   251
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
   252
by (induct n) simp_all
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   253
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   254
lemma natsum_add [simp]:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   255
  "!!f::nat=>'a::comm_monoid_add.
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   256
   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
   257
by (induct n) (simp_all add: add_ac)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   258
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   259
(* Facts specific to rings *)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   260
27542
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
   261
subclass (in ring) comm_monoid_add
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   262
proof
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   263
  fix x y z
27542
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
   264
  show "x + y = y + x" by (rule a_comm)
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
   265
  show "(x + y) + z = x + (y + z)" by (rule a_assoc)
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
   266
  show "0 + x = x" by (rule l_zero)
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   267
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   268
42768
4db4a8b164c1 modernized simproc_setup;
wenzelm
parents: 39159
diff changeset
   269
simproc_setup
4db4a8b164c1 modernized simproc_setup;
wenzelm
parents: 39159
diff changeset
   270
  ring ("t + u::'a::ring" | "t - u::'a::ring" | "t * u::'a::ring" | "- t::'a::ring") =
4db4a8b164c1 modernized simproc_setup;
wenzelm
parents: 39159
diff changeset
   271
{*
4db4a8b164c1 modernized simproc_setup;
wenzelm
parents: 39159
diff changeset
   272
  fn _ => fn ss => fn ct =>
4db4a8b164c1 modernized simproc_setup;
wenzelm
parents: 39159
diff changeset
   273
    let
4db4a8b164c1 modernized simproc_setup;
wenzelm
parents: 39159
diff changeset
   274
      val ctxt = Simplifier.the_context ss;
4db4a8b164c1 modernized simproc_setup;
wenzelm
parents: 39159
diff changeset
   275
      val {t, T, maxidx, ...} = Thm.rep_cterm ct;
4db4a8b164c1 modernized simproc_setup;
wenzelm
parents: 39159
diff changeset
   276
      val rew =
4db4a8b164c1 modernized simproc_setup;
wenzelm
parents: 39159
diff changeset
   277
        Goal.prove ctxt [] []
4db4a8b164c1 modernized simproc_setup;
wenzelm
parents: 39159
diff changeset
   278
          (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, Var (("x", maxidx + 1), T))))
4db4a8b164c1 modernized simproc_setup;
wenzelm
parents: 39159
diff changeset
   279
          (fn _ => simp_tac (Simplifier.inherit_context ss ring_ss) 1)
4db4a8b164c1 modernized simproc_setup;
wenzelm
parents: 39159
diff changeset
   280
        |> mk_meta_eq;
4db4a8b164c1 modernized simproc_setup;
wenzelm
parents: 39159
diff changeset
   281
      val (t', u) = Logic.dest_equals (Thm.prop_of rew);
4db4a8b164c1 modernized simproc_setup;
wenzelm
parents: 39159
diff changeset
   282
    in if t' aconv u then NONE else SOME rew end
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   283
*}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   284
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   285
lemma natsum_ldistr:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   286
  "!!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
   287
by (induct n) simp_all
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   288
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   289
lemma natsum_rdistr:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   290
  "!!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
   291
by (induct n) simp_all
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   292
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   293
subsection {* Integral Domains *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   294
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   295
declare one_not_zero [simp]
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   296
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   297
lemma zero_not_one [simp]:
32449
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32010
diff changeset
   298
  "0 ~= (1::'a::domain)"
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   299
by (rule not_sym) simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   300
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   301
lemma integral_iff: (* not by default a simp rule! *)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   302
  "(a * b = (0::'a::domain)) = (a = 0 | b = 0)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   303
proof
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   304
  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
   305
next
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   306
  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
   307
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   308
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   309
(*
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   310
lemma "(a::'a::ring) - (a - b) = b" apply simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   311
 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
   312
*)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   313
(*
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   314
lemma bug: "(b::'a::ring) - (b - a) = a" by simp
32449
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32010
diff changeset
   315
   simproc for rings cannot prove "(a::'a::ring) - (a - b) = b"
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   316
*)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   317
lemma m_lcancel:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   318
  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
   319
proof
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   320
  assume eq: "a * b = a * c"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   321
  then have "a * (b - c) = 0" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   322
  then have "a = 0 | (b - c) = 0" by (simp only: integral_iff)
32449
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32010
diff changeset
   323
  with prem have "b - c = 0" by auto
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32010
diff changeset
   324
  then have "b = b - (b - c)" by simp
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   325
  also have "b - (b - c) = c" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   326
  finally show "b = c" .
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   327
next
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   328
  assume "b = c" then show "a * b = a * c" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   329
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   330
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   331
lemma m_rcancel:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   332
  "(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   333
by (simp add: m_lcancel)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   334
27542
9bf0a22f8bcd class instead of axclass
haftmann
parents: 26480
diff changeset
   335
declare power_Suc [simp]
21416
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   336
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   337
lemma power_one [simp]:
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   338
  "1 ^ n = (1::'a::ring)" by (induct n) simp_all
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   339
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   340
lemma power_zero [simp]:
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   341
  "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
   342
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   343
lemma power_mult [simp]:
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   344
  "(a::'a::ring) ^ m * a ^ n = a ^ (m + n)"
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   345
  by (induct m) simp_all
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   346
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   347
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   348
section "Divisibility"
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   349
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   350
lemma dvd_zero_right [simp]:
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   351
  "(a::'a::ring) dvd 0"
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   352
proof
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   353
  show "0 = a * 0" by simp
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   354
qed
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   355
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   356
lemma dvd_zero_left:
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   357
  "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
   358
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   359
lemma dvd_refl_ring [simp]:
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   360
  "(a::'a::ring) dvd a"
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   361
proof
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   362
  show "a = a * 1" by simp
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   363
qed
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   364
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   365
lemma dvd_trans_ring:
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   366
  fixes a b c :: "'a::ring"
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   367
  assumes a_dvd_b: "a dvd b"
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   368
  and b_dvd_c: "b dvd c"
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   369
  shows "a dvd c"
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   370
proof -
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   371
  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
   372
  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
   373
  ultimately have "c = a * (l * j)" by simp
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   374
  then have "\<exists>k. c = a * k" ..
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   375
  then show ?thesis using dvd_def by blast
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   376
qed
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   377
21423
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   378
32449
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32010
diff changeset
   379
lemma unit_mult:
21423
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   380
  "!!a::'a::ring. [| a dvd 1; b dvd 1 |] ==> a * b dvd 1"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   381
  apply (unfold dvd_def)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   382
  apply clarify
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   383
  apply (rule_tac x = "k * ka" in exI)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   384
  apply simp
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   385
  done
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   386
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   387
lemma unit_power: "!!a::'a::ring. a dvd 1 ==> a^n dvd 1"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   388
  apply (induct_tac n)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   389
   apply simp
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   390
  apply (simp add: unit_mult)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   391
  done
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   392
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   393
lemma dvd_add_right [simp]:
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   394
  "!! a::'a::ring. [| a dvd b; a dvd c |] ==> a dvd b + c"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   395
  apply (unfold dvd_def)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   396
  apply clarify
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   397
  apply (rule_tac x = "k + ka" in exI)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   398
  apply (simp add: r_distr)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   399
  done
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   400
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   401
lemma dvd_uminus_right [simp]:
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   402
  "!! a::'a::ring. a dvd b ==> a dvd -b"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   403
  apply (unfold dvd_def)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   404
  apply clarify
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   405
  apply (rule_tac x = "-k" in exI)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   406
  apply (simp add: r_minus)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   407
  done
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   408
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   409
lemma dvd_l_mult_right [simp]:
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   410
  "!! a::'a::ring. a dvd b ==> a dvd c*b"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   411
  apply (unfold dvd_def)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   412
  apply clarify
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   413
  apply (rule_tac x = "c * k" in exI)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   414
  apply simp
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   415
  done
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   416
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   417
lemma dvd_r_mult_right [simp]:
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   418
  "!! a::'a::ring. a dvd b ==> a dvd b*c"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   419
  apply (unfold dvd_def)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   420
  apply clarify
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   421
  apply (rule_tac x = "k * c" in exI)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   422
  apply simp
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   423
  done
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   424
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   425
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   426
(* Inverse of multiplication *)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   427
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   428
section "inverse"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   429
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   430
lemma inverse_unique: "!! a::'a::ring. [| a * x = 1; a * y = 1 |] ==> x = y"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   431
  apply (rule_tac a = "(a*y) * x" and b = "y * (a*x)" in box_equals)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   432
    apply (simp (no_asm))
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   433
  apply auto
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   434
  done
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   435
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   436
lemma r_inverse_ring: "!! a::'a::ring. a dvd 1 ==> a * inverse a = 1"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   437
  apply (unfold inverse_def dvd_def)
42768
4db4a8b164c1 modernized simproc_setup;
wenzelm
parents: 39159
diff changeset
   438
  using [[simproc del: ring]]
4db4a8b164c1 modernized simproc_setup;
wenzelm
parents: 39159
diff changeset
   439
  apply simp
21423
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   440
  apply clarify
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   441
  apply (rule theI)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   442
   apply assumption
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   443
  apply (rule inverse_unique)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   444
   apply assumption
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   445
  apply assumption
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   446
  done
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   447
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   448
lemma l_inverse_ring: "!! a::'a::ring. a dvd 1 ==> inverse a * a = 1"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   449
  by (simp add: r_inverse_ring)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   450
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   451
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   452
(* Fields *)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   453
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   454
section "Fields"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   455
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   456
lemma field_unit [simp]: "!! a::'a::field. (a dvd 1) = (a ~= 0)"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   457
  by (auto dest: field_ax dvd_zero_left simp add: field_one_not_zero)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   458
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   459
lemma r_inverse [simp]: "!! a::'a::field. a ~= 0 ==> a * inverse a = 1"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   460
  by (simp add: r_inverse_ring)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   461
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   462
lemma l_inverse [simp]: "!! a::'a::field. a ~= 0 ==> inverse a * a= 1"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   463
  by (simp add: l_inverse_ring)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   464
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   465
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   466
(* fields are integral domains *)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   467
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   468
lemma field_integral: "!! a::'a::field. a * b = 0 ==> a = 0 | b = 0"
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 22997
diff changeset
   469
  apply (tactic "step_tac @{claset} 1")
21423
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   470
  apply (rule_tac a = " (a*b) * inverse b" in box_equals)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   471
    apply (rule_tac [3] refl)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   472
   prefer 2
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   473
   apply (simp (no_asm))
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   474
   apply auto
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   475
  done
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   476
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   477
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   478
(* fields are factorial domains *)
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   479
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   480
lemma field_fact_prime: "!! a::'a::field. irred a ==> prime a"
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21416
diff changeset
   481
  unfolding prime_def irred_def by (blast intro: field_ax)
21416
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 20318
diff changeset
   482
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   483
end