src/HOL/Rings.thy
author haftmann
Fri, 19 Jun 2015 07:53:35 +0200
changeset 60517 f16e4fb20652
parent 60516 0826b7025d07
child 60529 24c2ef12318b
permissions -rw-r--r--
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35050
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 35043
diff changeset
     1
(*  Title:      HOL/Rings.thy
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30961
diff changeset
     2
    Author:     Gertrud Bauer
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30961
diff changeset
     3
    Author:     Steven Obua
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30961
diff changeset
     4
    Author:     Tobias Nipkow
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30961
diff changeset
     5
    Author:     Lawrence C Paulson
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30961
diff changeset
     6
    Author:     Markus Wenzel
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30961
diff changeset
     7
    Author:     Jeremy Avigad
14265
95b42e69436c HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff changeset
     8
*)
95b42e69436c HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff changeset
     9
58889
5b7a9633cfa8 modernized header uniformly as section;
wenzelm
parents: 58776
diff changeset
    10
section {* Rings *}
14265
95b42e69436c HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff changeset
    11
35050
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 35043
diff changeset
    12
theory Rings
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 35043
diff changeset
    13
imports Groups
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15077
diff changeset
    14
begin
14504
7a3d80e276d4 new type class abelian_group
paulson
parents: 14475
diff changeset
    15
22390
378f34b1e380 now using "class"
haftmann
parents: 21328
diff changeset
    16
class semiring = ab_semigroup_add + semigroup_mult +
58776
95e58e04e534 use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
hoelzl
parents: 58649
diff changeset
    17
  assumes distrib_right[algebra_simps]: "(a + b) * c = a * c + b * c"
95e58e04e534 use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
hoelzl
parents: 58649
diff changeset
    18
  assumes distrib_left[algebra_simps]: "a * (b + c) = a * b + a * c"
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
    19
begin
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
    20
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
    21
text{*For the @{text combine_numerals} simproc*}
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
    22
lemma combine_common_factor:
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
    23
  "a * e + (b * e + c) = (a + b) * e + c"
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 57512
diff changeset
    24
by (simp add: distrib_right ac_simps)
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
    25
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
    26
end
14504
7a3d80e276d4 new type class abelian_group
paulson
parents: 14475
diff changeset
    27
22390
378f34b1e380 now using "class"
haftmann
parents: 21328
diff changeset
    28
class mult_zero = times + zero +
25062
af5ef0d4d655 global class syntax
haftmann
parents: 24748
diff changeset
    29
  assumes mult_zero_left [simp]: "0 * a = 0"
af5ef0d4d655 global class syntax
haftmann
parents: 24748
diff changeset
    30
  assumes mult_zero_right [simp]: "a * 0 = 0"
58195
1fee63e0377d added various facts
haftmann
parents: 57514
diff changeset
    31
begin
1fee63e0377d added various facts
haftmann
parents: 57514
diff changeset
    32
1fee63e0377d added various facts
haftmann
parents: 57514
diff changeset
    33
lemma mult_not_zero:
1fee63e0377d added various facts
haftmann
parents: 57514
diff changeset
    34
  "a * b \<noteq> 0 \<Longrightarrow> a \<noteq> 0 \<and> b \<noteq> 0"
1fee63e0377d added various facts
haftmann
parents: 57514
diff changeset
    35
  by auto
1fee63e0377d added various facts
haftmann
parents: 57514
diff changeset
    36
1fee63e0377d added various facts
haftmann
parents: 57514
diff changeset
    37
end
21199
2d83f93c3580 * Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents: 20633
diff changeset
    38
58198
099ca49b5231 generalized
haftmann
parents: 58195
diff changeset
    39
class semiring_0 = semiring + comm_monoid_add + mult_zero
099ca49b5231 generalized
haftmann
parents: 58195
diff changeset
    40
29904
856f16a3b436 add class cancel_comm_monoid_add
huffman
parents: 29833
diff changeset
    41
class semiring_0_cancel = semiring + cancel_comm_monoid_add
25186
f4d1ebffd025 localized further
haftmann
parents: 25152
diff changeset
    42
begin
14504
7a3d80e276d4 new type class abelian_group
paulson
parents: 14475
diff changeset
    43
25186
f4d1ebffd025 localized further
haftmann
parents: 25152
diff changeset
    44
subclass semiring_0
28823
dcbef866c9e2 tuned unfold_locales invocation
haftmann
parents: 28559
diff changeset
    45
proof
21199
2d83f93c3580 * Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents: 20633
diff changeset
    46
  fix a :: 'a
49962
a8cc904a6820 Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents: 44921
diff changeset
    47
  have "0 * a + 0 * a = 0 * a + 0" by (simp add: distrib_right [symmetric])
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
    48
  thus "0 * a = 0" by (simp only: add_left_cancel)
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
    49
next
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
    50
  fix a :: 'a
49962
a8cc904a6820 Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents: 44921
diff changeset
    51
  have "a * 0 + a * 0 = a * 0 + 0" by (simp add: distrib_left [symmetric])
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
    52
  thus "a * 0 = 0" by (simp only: add_left_cancel)
21199
2d83f93c3580 * Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents: 20633
diff changeset
    53
qed
14940
b9ab8babd8b3 Further development of matrix theory
obua
parents: 14770
diff changeset
    54
25186
f4d1ebffd025 localized further
haftmann
parents: 25152
diff changeset
    55
end
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
    56
22390
378f34b1e380 now using "class"
haftmann
parents: 21328
diff changeset
    57
class comm_semiring = ab_semigroup_add + ab_semigroup_mult +
25062
af5ef0d4d655 global class syntax
haftmann
parents: 24748
diff changeset
    58
  assumes distrib: "(a + b) * c = a * c + b * c"
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
    59
begin
14504
7a3d80e276d4 new type class abelian_group
paulson
parents: 14475
diff changeset
    60
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
    61
subclass semiring
28823
dcbef866c9e2 tuned unfold_locales invocation
haftmann
parents: 28559
diff changeset
    62
proof
14738
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents: 14603
diff changeset
    63
  fix a b c :: 'a
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents: 14603
diff changeset
    64
  show "(a + b) * c = a * c + b * c" by (simp add: distrib)
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 57512
diff changeset
    65
  have "a * (b + c) = (b + c) * a" by (simp add: ac_simps)
14738
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents: 14603
diff changeset
    66
  also have "... = b * a + c * a" by (simp only: distrib)
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 57512
diff changeset
    67
  also have "... = a * b + a * c" by (simp add: ac_simps)
14738
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents: 14603
diff changeset
    68
  finally show "a * (b + c) = a * b + a * c" by blast
14504
7a3d80e276d4 new type class abelian_group
paulson
parents: 14475
diff changeset
    69
qed
7a3d80e276d4 new type class abelian_group
paulson
parents: 14475
diff changeset
    70
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
    71
end
14504
7a3d80e276d4 new type class abelian_group
paulson
parents: 14475
diff changeset
    72
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
    73
class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
    74
begin
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
    75
27516
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
    76
subclass semiring_0 ..
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
    77
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
    78
end
14504
7a3d80e276d4 new type class abelian_group
paulson
parents: 14475
diff changeset
    79
29904
856f16a3b436 add class cancel_comm_monoid_add
huffman
parents: 29833
diff changeset
    80
class comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_add
25186
f4d1ebffd025 localized further
haftmann
parents: 25152
diff changeset
    81
begin
14940
b9ab8babd8b3 Further development of matrix theory
obua
parents: 14770
diff changeset
    82
27516
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
    83
subclass semiring_0_cancel ..
14940
b9ab8babd8b3 Further development of matrix theory
obua
parents: 14770
diff changeset
    84
28141
193c3ea0f63b instances comm_semiring_0_cancel < comm_semiring_0, comm_ring < comm_semiring_0_cancel
huffman
parents: 27651
diff changeset
    85
subclass comm_semiring_0 ..
193c3ea0f63b instances comm_semiring_0_cancel < comm_semiring_0, comm_ring < comm_semiring_0_cancel
huffman
parents: 27651
diff changeset
    86
25186
f4d1ebffd025 localized further
haftmann
parents: 25152
diff changeset
    87
end
21199
2d83f93c3580 * Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents: 20633
diff changeset
    88
22390
378f34b1e380 now using "class"
haftmann
parents: 21328
diff changeset
    89
class zero_neq_one = zero + one +
25062
af5ef0d4d655 global class syntax
haftmann
parents: 24748
diff changeset
    90
  assumes zero_neq_one [simp]: "0 \<noteq> 1"
26193
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
    91
begin
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
    92
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
    93
lemma one_neq_zero [simp]: "1 \<noteq> 0"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
    94
by (rule not_sym) (rule zero_neq_one)
26193
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
    95
54225
8a49a5a30284 generalized of_bool conversion
haftmann
parents: 54147
diff changeset
    96
definition of_bool :: "bool \<Rightarrow> 'a"
8a49a5a30284 generalized of_bool conversion
haftmann
parents: 54147
diff changeset
    97
where
8a49a5a30284 generalized of_bool conversion
haftmann
parents: 54147
diff changeset
    98
  "of_bool p = (if p then 1 else 0)" 
8a49a5a30284 generalized of_bool conversion
haftmann
parents: 54147
diff changeset
    99
8a49a5a30284 generalized of_bool conversion
haftmann
parents: 54147
diff changeset
   100
lemma of_bool_eq [simp, code]:
8a49a5a30284 generalized of_bool conversion
haftmann
parents: 54147
diff changeset
   101
  "of_bool False = 0"
8a49a5a30284 generalized of_bool conversion
haftmann
parents: 54147
diff changeset
   102
  "of_bool True = 1"
8a49a5a30284 generalized of_bool conversion
haftmann
parents: 54147
diff changeset
   103
  by (simp_all add: of_bool_def)
8a49a5a30284 generalized of_bool conversion
haftmann
parents: 54147
diff changeset
   104
8a49a5a30284 generalized of_bool conversion
haftmann
parents: 54147
diff changeset
   105
lemma of_bool_eq_iff:
8a49a5a30284 generalized of_bool conversion
haftmann
parents: 54147
diff changeset
   106
  "of_bool p = of_bool q \<longleftrightarrow> p = q"
8a49a5a30284 generalized of_bool conversion
haftmann
parents: 54147
diff changeset
   107
  by (simp add: of_bool_def)
8a49a5a30284 generalized of_bool conversion
haftmann
parents: 54147
diff changeset
   108
55187
6d0d93316daf split rules for of_bool, similar to if
haftmann
parents: 54703
diff changeset
   109
lemma split_of_bool [split]:
6d0d93316daf split rules for of_bool, similar to if
haftmann
parents: 54703
diff changeset
   110
  "P (of_bool p) \<longleftrightarrow> (p \<longrightarrow> P 1) \<and> (\<not> p \<longrightarrow> P 0)"
6d0d93316daf split rules for of_bool, similar to if
haftmann
parents: 54703
diff changeset
   111
  by (cases p) simp_all
6d0d93316daf split rules for of_bool, similar to if
haftmann
parents: 54703
diff changeset
   112
6d0d93316daf split rules for of_bool, similar to if
haftmann
parents: 54703
diff changeset
   113
lemma split_of_bool_asm:
6d0d93316daf split rules for of_bool, similar to if
haftmann
parents: 54703
diff changeset
   114
  "P (of_bool p) \<longleftrightarrow> \<not> (p \<and> \<not> P 1 \<or> \<not> p \<and> \<not> P 0)"
6d0d93316daf split rules for of_bool, similar to if
haftmann
parents: 54703
diff changeset
   115
  by (cases p) simp_all
6d0d93316daf split rules for of_bool, similar to if
haftmann
parents: 54703
diff changeset
   116
  
54225
8a49a5a30284 generalized of_bool conversion
haftmann
parents: 54147
diff changeset
   117
end  
14265
95b42e69436c HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff changeset
   118
22390
378f34b1e380 now using "class"
haftmann
parents: 21328
diff changeset
   119
class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
14504
7a3d80e276d4 new type class abelian_group
paulson
parents: 14475
diff changeset
   120
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   121
text {* Abstract divisibility *}
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   122
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   123
class dvd = times
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   124
begin
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   125
50420
f1a27e82af16 corrected nonsensical associativity of `` and dvd
nipkow
parents: 49962
diff changeset
   126
definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "dvd" 50) where
37767
a2b7a20d6ea3 dropped superfluous [code del]s
haftmann
parents: 36977
diff changeset
   127
  "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   128
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   129
lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a"
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   130
  unfolding dvd_def ..
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   131
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   132
lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P"
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   133
  unfolding dvd_def by blast 
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   134
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   135
end
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   136
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   137
context comm_monoid_mult
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   138
begin
14738
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents: 14603
diff changeset
   139
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   140
subclass dvd .
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   141
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   142
lemma dvd_refl [simp]:
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   143
  "a dvd a"
28559
55c003a5600a tuned default rules of (dvd)
haftmann
parents: 28141
diff changeset
   144
proof
55c003a5600a tuned default rules of (dvd)
haftmann
parents: 28141
diff changeset
   145
  show "a = a * 1" by simp
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   146
qed
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   147
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   148
lemma dvd_trans:
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   149
  assumes "a dvd b" and "b dvd c"
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   150
  shows "a dvd c"
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   151
proof -
28559
55c003a5600a tuned default rules of (dvd)
haftmann
parents: 28141
diff changeset
   152
  from assms obtain v where "b = a * v" by (auto elim!: dvdE)
55c003a5600a tuned default rules of (dvd)
haftmann
parents: 28141
diff changeset
   153
  moreover from assms obtain w where "c = b * w" by (auto elim!: dvdE)
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 56544
diff changeset
   154
  ultimately have "c = a * (v * w)" by (simp add: mult.assoc)
28559
55c003a5600a tuned default rules of (dvd)
haftmann
parents: 28141
diff changeset
   155
  then show ?thesis ..
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   156
qed
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   157
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   158
lemma one_dvd [simp]:
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   159
  "1 dvd a"
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   160
  by (auto intro!: dvdI)
28559
55c003a5600a tuned default rules of (dvd)
haftmann
parents: 28141
diff changeset
   161
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   162
lemma dvd_mult [simp]:
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   163
  "a dvd c \<Longrightarrow> a dvd (b * c)"
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   164
  by (auto intro!: mult.left_commute dvdI elim!: dvdE)
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   165
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   166
lemma dvd_mult2 [simp]:
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   167
  "a dvd b \<Longrightarrow> a dvd (b * c)"
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   168
  using dvd_mult [of a b c] by (simp add: ac_simps) 
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   169
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   170
lemma dvd_triv_right [simp]:
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   171
  "a dvd b * a"
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   172
  by (rule dvd_mult) (rule dvd_refl)
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   173
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   174
lemma dvd_triv_left [simp]:
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   175
  "a dvd a * b"
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   176
  by (rule dvd_mult2) (rule dvd_refl)
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   177
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   178
lemma mult_dvd_mono:
30042
31039ee583fa Removed subsumed lemmas
nipkow
parents: 29981
diff changeset
   179
  assumes "a dvd b"
31039ee583fa Removed subsumed lemmas
nipkow
parents: 29981
diff changeset
   180
    and "c dvd d"
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   181
  shows "a * c dvd b * d"
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   182
proof -
30042
31039ee583fa Removed subsumed lemmas
nipkow
parents: 29981
diff changeset
   183
  from `a dvd b` obtain b' where "b = a * b'" ..
31039ee583fa Removed subsumed lemmas
nipkow
parents: 29981
diff changeset
   184
  moreover from `c dvd d` obtain d' where "d = c * d'" ..
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 57512
diff changeset
   185
  ultimately have "b * d = (a * c) * (b' * d')" by (simp add: ac_simps)
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   186
  then show ?thesis ..
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   187
qed
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   188
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   189
lemma dvd_mult_left:
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   190
  "a * b dvd c \<Longrightarrow> a dvd c"
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   191
  by (simp add: dvd_def mult.assoc) blast
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   192
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   193
lemma dvd_mult_right:
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   194
  "a * b dvd c \<Longrightarrow> b dvd c"
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   195
  using dvd_mult_left [of b a c] by (simp add: ac_simps)
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   196
  
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   197
end
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   198
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   199
class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   200
begin
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   201
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   202
subclass semiring_1 ..
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   203
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   204
lemma dvd_0_left_iff [simp]:
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   205
  "0 dvd a \<longleftrightarrow> a = 0"
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   206
  by (auto intro: dvd_refl elim!: dvdE)
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   207
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   208
lemma dvd_0_right [iff]:
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   209
  "a dvd 0"
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   210
proof
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   211
  show "0 = a * 0" by simp
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   212
qed
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   213
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   214
lemma dvd_0_left:
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   215
  "0 dvd a \<Longrightarrow> a = 0"
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   216
  by simp
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   217
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   218
lemma dvd_add [simp]:
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   219
  assumes "a dvd b" and "a dvd c"
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   220
  shows "a dvd (b + c)"
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   221
proof -
29925
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29915
diff changeset
   222
  from `a dvd b` obtain b' where "b = a * b'" ..
17d1e32ef867 dvd and setprod lemmas
nipkow
parents: 29915
diff changeset
   223
  moreover from `a dvd c` obtain c' where "c = a * c'" ..
49962
a8cc904a6820 Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents: 44921
diff changeset
   224
  ultimately have "b + c = a * (b' + c')" by (simp add: distrib_left)
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   225
  then show ?thesis ..
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   226
qed
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   227
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   228
end
14421
ee97b6463cb4 new Ring_and_Field hierarchy, eliminating redundant axioms
paulson
parents: 14398
diff changeset
   229
29904
856f16a3b436 add class cancel_comm_monoid_add
huffman
parents: 29833
diff changeset
   230
class semiring_1_cancel = semiring + cancel_comm_monoid_add
856f16a3b436 add class cancel_comm_monoid_add
huffman
parents: 29833
diff changeset
   231
  + zero_neq_one + monoid_mult
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   232
begin
14940
b9ab8babd8b3 Further development of matrix theory
obua
parents: 14770
diff changeset
   233
27516
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
   234
subclass semiring_0_cancel ..
25512
4134f7c782e2 using intro_locales instead of unfold_locales if appropriate
haftmann
parents: 25450
diff changeset
   235
27516
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
   236
subclass semiring_1 ..
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   237
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   238
end
21199
2d83f93c3580 * Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents: 20633
diff changeset
   239
29904
856f16a3b436 add class cancel_comm_monoid_add
huffman
parents: 29833
diff changeset
   240
class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add
856f16a3b436 add class cancel_comm_monoid_add
huffman
parents: 29833
diff changeset
   241
  + zero_neq_one + comm_monoid_mult
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   242
begin
14738
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents: 14603
diff changeset
   243
27516
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
   244
subclass semiring_1_cancel ..
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
   245
subclass comm_semiring_0_cancel ..
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
   246
subclass comm_semiring_1 ..
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   247
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   248
end
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   249
59816
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   250
class comm_semiring_1_diff_distrib = comm_semiring_1_cancel +
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   251
  assumes right_diff_distrib' [algebra_simps]: "a * (b - c) = a * b - a * c"
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   252
begin
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   253
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   254
lemma left_diff_distrib' [algebra_simps]:
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   255
  "(b - c) * a = b * a - c * a"
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   256
  by (simp add: algebra_simps)
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   257
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   258
lemma dvd_add_times_triv_left_iff [simp]:
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   259
  "a dvd c * a + b \<longleftrightarrow> a dvd b"
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   260
proof -
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   261
  have "a dvd a * c + b \<longleftrightarrow> a dvd b" (is "?P \<longleftrightarrow> ?Q")
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   262
  proof
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   263
    assume ?Q then show ?P by simp
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   264
  next
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   265
    assume ?P
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   266
    then obtain d where "a * c + b = a * d" ..
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   267
    then have "a * c + b - a * c = a * d - a * c" by simp
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   268
    then have "b = a * d - a * c" by simp
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   269
    then have "b = a * (d - c)" by (simp add: algebra_simps) 
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   270
    then show ?Q ..
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   271
  qed
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   272
  then show "a dvd c * a + b \<longleftrightarrow> a dvd b" by (simp add: ac_simps)
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   273
qed
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   274
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   275
lemma dvd_add_times_triv_right_iff [simp]:
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   276
  "a dvd b + c * a \<longleftrightarrow> a dvd b"
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   277
  using dvd_add_times_triv_left_iff [of a c b] by (simp add: ac_simps)
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   278
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   279
lemma dvd_add_triv_left_iff [simp]:
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   280
  "a dvd a + b \<longleftrightarrow> a dvd b"
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   281
  using dvd_add_times_triv_left_iff [of a 1 b] by simp
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   282
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   283
lemma dvd_add_triv_right_iff [simp]:
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   284
  "a dvd b + a \<longleftrightarrow> a dvd b"
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   285
  using dvd_add_times_triv_right_iff [of a b 1] by simp
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   286
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   287
lemma dvd_add_right_iff:
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   288
  assumes "a dvd b"
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   289
  shows "a dvd b + c \<longleftrightarrow> a dvd c" (is "?P \<longleftrightarrow> ?Q")
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   290
proof
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   291
  assume ?P then obtain d where "b + c = a * d" ..
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   292
  moreover from `a dvd b` obtain e where "b = a * e" ..
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   293
  ultimately have "a * e + c = a * d" by simp
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   294
  then have "a * e + c - a * e = a * d - a * e" by simp
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   295
  then have "c = a * d - a * e" by simp
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   296
  then have "c = a * (d - e)" by (simp add: algebra_simps)
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   297
  then show ?Q ..
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   298
next
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   299
  assume ?Q with assms show ?P by simp
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   300
qed
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   301
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   302
lemma dvd_add_left_iff:
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   303
  assumes "a dvd c"
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   304
  shows "a dvd b + c \<longleftrightarrow> a dvd b"
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   305
  using assms dvd_add_right_iff [of a c b] by (simp add: ac_simps)
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   306
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   307
end
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   308
22390
378f34b1e380 now using "class"
haftmann
parents: 21328
diff changeset
   309
class ring = semiring + ab_group_add
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   310
begin
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   311
27516
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
   312
subclass semiring_0_cancel ..
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   313
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   314
text {* Distribution rules *}
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   315
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   316
lemma minus_mult_left: "- (a * b) = - a * b"
49962
a8cc904a6820 Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents: 44921
diff changeset
   317
by (rule minus_unique) (simp add: distrib_right [symmetric]) 
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   318
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   319
lemma minus_mult_right: "- (a * b) = a * - b"
49962
a8cc904a6820 Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents: 44921
diff changeset
   320
by (rule minus_unique) (simp add: distrib_left [symmetric]) 
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   321
29407
5ef7e97fd9e4 move lemmas mult_minus{left,right} inside class ring
huffman
parents: 29406
diff changeset
   322
text{*Extract signs from products*}
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 52435
diff changeset
   323
lemmas mult_minus_left [simp] = minus_mult_left [symmetric]
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 52435
diff changeset
   324
lemmas mult_minus_right [simp] = minus_mult_right [symmetric]
29407
5ef7e97fd9e4 move lemmas mult_minus{left,right} inside class ring
huffman
parents: 29406
diff changeset
   325
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   326
lemma minus_mult_minus [simp]: "- a * - b = a * b"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
   327
by simp
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   328
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   329
lemma minus_mult_commute: "- a * b = a * - b"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
   330
by simp
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
   331
58776
95e58e04e534 use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
hoelzl
parents: 58649
diff changeset
   332
lemma right_diff_distrib [algebra_simps]:
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 54225
diff changeset
   333
  "a * (b - c) = a * b - a * c"
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 54225
diff changeset
   334
  using distrib_left [of a b "-c "] by simp
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
   335
58776
95e58e04e534 use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
hoelzl
parents: 58649
diff changeset
   336
lemma left_diff_distrib [algebra_simps]:
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 54225
diff changeset
   337
  "(a - b) * c = a * c - b * c"
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 54225
diff changeset
   338
  using distrib_right [of a "- b" c] by simp
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   339
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 52435
diff changeset
   340
lemmas ring_distribs =
49962
a8cc904a6820 Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents: 44921
diff changeset
   341
  distrib_left distrib_right left_diff_distrib right_diff_distrib
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   342
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   343
lemma eq_add_iff1:
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   344
  "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
   345
by (simp add: algebra_simps)
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   346
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   347
lemma eq_add_iff2:
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   348
  "a * e + c = b * e + d \<longleftrightarrow> c = (b - a) * e + d"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
   349
by (simp add: algebra_simps)
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   350
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   351
end
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   352
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 52435
diff changeset
   353
lemmas ring_distribs =
49962
a8cc904a6820 Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents: 44921
diff changeset
   354
  distrib_left distrib_right left_diff_distrib right_diff_distrib
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   355
22390
378f34b1e380 now using "class"
haftmann
parents: 21328
diff changeset
   356
class comm_ring = comm_semiring + ab_group_add
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   357
begin
14738
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents: 14603
diff changeset
   358
27516
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
   359
subclass ring ..
28141
193c3ea0f63b instances comm_semiring_0_cancel < comm_semiring_0, comm_ring < comm_semiring_0_cancel
huffman
parents: 27651
diff changeset
   360
subclass comm_semiring_0_cancel ..
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   361
44350
63cddfbc5a09 replace lemma realpow_two_diff with new lemma square_diff_square_factored
huffman
parents: 44346
diff changeset
   362
lemma square_diff_square_factored:
63cddfbc5a09 replace lemma realpow_two_diff with new lemma square_diff_square_factored
huffman
parents: 44346
diff changeset
   363
  "x * x - y * y = (x + y) * (x - y)"
63cddfbc5a09 replace lemma realpow_two_diff with new lemma square_diff_square_factored
huffman
parents: 44346
diff changeset
   364
  by (simp add: algebra_simps)
63cddfbc5a09 replace lemma realpow_two_diff with new lemma square_diff_square_factored
huffman
parents: 44346
diff changeset
   365
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   366
end
14738
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents: 14603
diff changeset
   367
22390
378f34b1e380 now using "class"
haftmann
parents: 21328
diff changeset
   368
class ring_1 = ring + zero_neq_one + monoid_mult
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   369
begin
14265
95b42e69436c HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff changeset
   370
27516
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
   371
subclass semiring_1_cancel ..
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   372
44346
00dd3c4dabe0 rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy
huffman
parents: 44064
diff changeset
   373
lemma square_diff_one_factored:
00dd3c4dabe0 rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy
huffman
parents: 44064
diff changeset
   374
  "x * x - 1 = (x + 1) * (x - 1)"
00dd3c4dabe0 rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy
huffman
parents: 44064
diff changeset
   375
  by (simp add: algebra_simps)
00dd3c4dabe0 rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy
huffman
parents: 44064
diff changeset
   376
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   377
end
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   378
22390
378f34b1e380 now using "class"
haftmann
parents: 21328
diff changeset
   379
class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   380
begin
14738
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents: 14603
diff changeset
   381
27516
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
   382
subclass ring_1 ..
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
   383
subclass comm_semiring_1_cancel ..
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   384
59816
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   385
subclass comm_semiring_1_diff_distrib
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   386
  by unfold_locales (simp add: algebra_simps)
58647
fce800afeec7 more facts about abstract divisibility
haftmann
parents: 58198
diff changeset
   387
29465
b2cfb5d0a59e change dvd_minus_iff, minus_dvd_iff from [iff] to [simp] (due to problems with Library/Primes.thy)
huffman
parents: 29461
diff changeset
   388
lemma dvd_minus_iff [simp]: "x dvd - y \<longleftrightarrow> x dvd y"
29408
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   389
proof
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   390
  assume "x dvd - y"
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   391
  then have "x dvd - 1 * - y" by (rule dvd_mult)
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   392
  then show "x dvd y" by simp
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   393
next
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   394
  assume "x dvd y"
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   395
  then have "x dvd - 1 * y" by (rule dvd_mult)
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   396
  then show "x dvd - y" by simp
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   397
qed
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   398
29465
b2cfb5d0a59e change dvd_minus_iff, minus_dvd_iff from [iff] to [simp] (due to problems with Library/Primes.thy)
huffman
parents: 29461
diff changeset
   399
lemma minus_dvd_iff [simp]: "- x dvd y \<longleftrightarrow> x dvd y"
29408
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   400
proof
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   401
  assume "- x dvd y"
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   402
  then obtain k where "y = - x * k" ..
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   403
  then have "y = x * - k" by simp
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   404
  then show "x dvd y" ..
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   405
next
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   406
  assume "x dvd y"
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   407
  then obtain k where "y = x * k" ..
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   408
  then have "y = - x * - k" by simp
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   409
  then show "- x dvd y" ..
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   410
qed
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   411
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 54225
diff changeset
   412
lemma dvd_diff [simp]:
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 54225
diff changeset
   413
  "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 54225
diff changeset
   414
  using dvd_add [of x y "- z"] by simp
29409
f0a8fe83bc07 add lemma dvd_diff to class comm_ring_1
huffman
parents: 29408
diff changeset
   415
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   416
end
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   417
59833
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   418
class semiring_no_zero_divisors = semiring_0 +
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   419
  assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   420
begin
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   421
59833
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   422
lemma divisors_zero:
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   423
  assumes "a * b = 0"
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   424
  shows "a = 0 \<or> b = 0"
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   425
proof (rule classical)
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   426
  assume "\<not> (a = 0 \<or> b = 0)"
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   427
  then have "a \<noteq> 0" and "b \<noteq> 0" by auto
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   428
  with no_zero_divisors have "a * b \<noteq> 0" by blast
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   429
  with assms show ?thesis by simp
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   430
qed
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   431
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   432
lemma mult_eq_0_iff [simp]:
58952
5d82cdef6c1b equivalence rules for structures without zero divisors
haftmann
parents: 58889
diff changeset
   433
  shows "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   434
proof (cases "a = 0 \<or> b = 0")
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   435
  case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   436
    then show ?thesis using no_zero_divisors by simp
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   437
next
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   438
  case True then show ?thesis by auto
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   439
qed
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   440
58952
5d82cdef6c1b equivalence rules for structures without zero divisors
haftmann
parents: 58889
diff changeset
   441
end
5d82cdef6c1b equivalence rules for structures without zero divisors
haftmann
parents: 58889
diff changeset
   442
60516
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   443
class semiring_no_zero_divisors_cancel = semiring_no_zero_divisors +
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   444
  assumes mult_cancel_right [simp]: "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   445
    and mult_cancel_left [simp]: "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
58952
5d82cdef6c1b equivalence rules for structures without zero divisors
haftmann
parents: 58889
diff changeset
   446
begin
5d82cdef6c1b equivalence rules for structures without zero divisors
haftmann
parents: 58889
diff changeset
   447
5d82cdef6c1b equivalence rules for structures without zero divisors
haftmann
parents: 58889
diff changeset
   448
lemma mult_left_cancel:
5d82cdef6c1b equivalence rules for structures without zero divisors
haftmann
parents: 58889
diff changeset
   449
  "c \<noteq> 0 \<Longrightarrow> c * a = c * b \<longleftrightarrow> a = b"
5d82cdef6c1b equivalence rules for structures without zero divisors
haftmann
parents: 58889
diff changeset
   450
  by simp 
56217
dc429a5b13c4 Some rationalisation of basic lemmas
paulson <lp15@cam.ac.uk>
parents: 55912
diff changeset
   451
58952
5d82cdef6c1b equivalence rules for structures without zero divisors
haftmann
parents: 58889
diff changeset
   452
lemma mult_right_cancel:
5d82cdef6c1b equivalence rules for structures without zero divisors
haftmann
parents: 58889
diff changeset
   453
  "c \<noteq> 0 \<Longrightarrow> a * c = b * c \<longleftrightarrow> a = b"
5d82cdef6c1b equivalence rules for structures without zero divisors
haftmann
parents: 58889
diff changeset
   454
  by simp 
56217
dc429a5b13c4 Some rationalisation of basic lemmas
paulson <lp15@cam.ac.uk>
parents: 55912
diff changeset
   455
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   456
end
22990
775e9de3db48 added classes ring_no_zero_divisors and dom (non-commutative version of idom);
huffman
parents: 22987
diff changeset
   457
60516
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   458
class ring_no_zero_divisors = ring + semiring_no_zero_divisors
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   459
begin
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   460
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   461
subclass semiring_no_zero_divisors_cancel
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   462
proof
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   463
  fix a b c
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   464
  have "a * c = b * c \<longleftrightarrow> (a - b) * c = 0"
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   465
    by (simp add: algebra_simps)
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   466
  also have "\<dots> \<longleftrightarrow> c = 0 \<or> a = b"
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   467
    by auto
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   468
  finally show "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b" .
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   469
  have "c * a = c * b \<longleftrightarrow> c * (a - b) = 0"
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   470
    by (simp add: algebra_simps)
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   471
  also have "\<dots> \<longleftrightarrow> c = 0 \<or> a = b"
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   472
    by auto
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   473
  finally show "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b" .
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   474
qed
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   475
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   476
end
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   477
23544
4b4165cb3e0d rename class dom to ring_1_no_zero_divisors
huffman
parents: 23527
diff changeset
   478
class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
26274
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   479
begin
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   480
36970
fb3fdb4b585e remove simp attribute from square_eq_1_iff
huffman
parents: 36821
diff changeset
   481
lemma square_eq_1_iff:
36821
9207505d1ee5 move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents: 36719
diff changeset
   482
  "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"
9207505d1ee5 move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents: 36719
diff changeset
   483
proof -
9207505d1ee5 move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents: 36719
diff changeset
   484
  have "(x - 1) * (x + 1) = x * x - 1"
9207505d1ee5 move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents: 36719
diff changeset
   485
    by (simp add: algebra_simps)
9207505d1ee5 move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents: 36719
diff changeset
   486
  hence "x * x = 1 \<longleftrightarrow> (x - 1) * (x + 1) = 0"
9207505d1ee5 move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents: 36719
diff changeset
   487
    by simp
9207505d1ee5 move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents: 36719
diff changeset
   488
  thus ?thesis
9207505d1ee5 move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents: 36719
diff changeset
   489
    by (simp add: eq_neg_iff_add_eq_0)
9207505d1ee5 move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents: 36719
diff changeset
   490
qed
9207505d1ee5 move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents: 36719
diff changeset
   491
26274
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   492
lemma mult_cancel_right1 [simp]:
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   493
  "c = b * c \<longleftrightarrow> c = 0 \<or> b = 1"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
   494
by (insert mult_cancel_right [of 1 c b], force)
26274
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   495
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   496
lemma mult_cancel_right2 [simp]:
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   497
  "a * c = c \<longleftrightarrow> c = 0 \<or> a = 1"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
   498
by (insert mult_cancel_right [of a c 1], simp)
26274
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   499
 
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   500
lemma mult_cancel_left1 [simp]:
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   501
  "c = c * b \<longleftrightarrow> c = 0 \<or> b = 1"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
   502
by (insert mult_cancel_left [of c 1 b], force)
26274
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   503
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   504
lemma mult_cancel_left2 [simp]:
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   505
  "c * a = c \<longleftrightarrow> c = 0 \<or> a = 1"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
   506
by (insert mult_cancel_left [of c a 1], simp)
26274
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   507
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   508
end
22990
775e9de3db48 added classes ring_no_zero_divisors and dom (non-commutative version of idom);
huffman
parents: 22987
diff changeset
   509
59910
815de5506080 semidom contains distributive minus, by convention
haftmann
parents: 59865
diff changeset
   510
class semidom = comm_semiring_1_diff_distrib + semiring_no_zero_divisors
59833
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   511
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   512
class idom = comm_ring_1 + semiring_no_zero_divisors
25186
f4d1ebffd025 localized further
haftmann
parents: 25152
diff changeset
   513
begin
14421
ee97b6463cb4 new Ring_and_Field hierarchy, eliminating redundant axioms
paulson
parents: 14398
diff changeset
   514
59833
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   515
subclass semidom ..
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   516
27516
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
   517
subclass ring_1_no_zero_divisors ..
22990
775e9de3db48 added classes ring_no_zero_divisors and dom (non-commutative version of idom);
huffman
parents: 22987
diff changeset
   518
29981
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   519
lemma dvd_mult_cancel_right [simp]:
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   520
  "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   521
proof -
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   522
  have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 57512
diff changeset
   523
    unfolding dvd_def by (simp add: ac_simps)
29981
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   524
  also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   525
    unfolding dvd_def by simp
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   526
  finally show ?thesis .
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   527
qed
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   528
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   529
lemma dvd_mult_cancel_left [simp]:
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   530
  "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b"
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   531
proof -
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   532
  have "c * a dvd c * b \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 57512
diff changeset
   533
    unfolding dvd_def by (simp add: ac_simps)
29981
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   534
  also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   535
    unfolding dvd_def by simp
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   536
  finally show ?thesis .
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   537
qed
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   538
60516
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   539
lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> a = b \<or> a = - b"
59833
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   540
proof
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   541
  assume "a * a = b * b"
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   542
  then have "(a - b) * (a + b) = 0"
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   543
    by (simp add: algebra_simps)
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   544
  then show "a = b \<or> a = - b"
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   545
    by (simp add: eq_neg_iff_add_eq_0)
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   546
next
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   547
  assume "a = b \<or> a = - b"
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   548
  then show "a * a = b * b" by auto
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   549
qed
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   550
25186
f4d1ebffd025 localized further
haftmann
parents: 25152
diff changeset
   551
end
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   552
35302
4bc6b4d70e08 tuned text
haftmann
parents: 35216
diff changeset
   553
text {*
4bc6b4d70e08 tuned text
haftmann
parents: 35216
diff changeset
   554
  The theory of partially ordered rings is taken from the books:
4bc6b4d70e08 tuned text
haftmann
parents: 35216
diff changeset
   555
  \begin{itemize}
4bc6b4d70e08 tuned text
haftmann
parents: 35216
diff changeset
   556
  \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
4bc6b4d70e08 tuned text
haftmann
parents: 35216
diff changeset
   557
  \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
4bc6b4d70e08 tuned text
haftmann
parents: 35216
diff changeset
   558
  \end{itemize}
4bc6b4d70e08 tuned text
haftmann
parents: 35216
diff changeset
   559
  Most of the used notions can also be looked up in 
4bc6b4d70e08 tuned text
haftmann
parents: 35216
diff changeset
   560
  \begin{itemize}
54703
499f92dc6e45 more antiquotations;
wenzelm
parents: 54489
diff changeset
   561
  \item @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
35302
4bc6b4d70e08 tuned text
haftmann
parents: 35216
diff changeset
   562
  \item \emph{Algebra I} by van der Waerden, Springer.
4bc6b4d70e08 tuned text
haftmann
parents: 35216
diff changeset
   563
  \end{itemize}
4bc6b4d70e08 tuned text
haftmann
parents: 35216
diff changeset
   564
*}
4bc6b4d70e08 tuned text
haftmann
parents: 35216
diff changeset
   565
60353
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   566
class divide =
60429
d3d1e185cd63 uniform _ div _ as infix syntax for ring division
haftmann
parents: 60353
diff changeset
   567
  fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "div" 70)
60353
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   568
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   569
setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   570
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   571
context semiring
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   572
begin
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   573
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   574
lemma [field_simps]:
60429
d3d1e185cd63 uniform _ div _ as infix syntax for ring division
haftmann
parents: 60353
diff changeset
   575
  shows distrib_left_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
d3d1e185cd63 uniform _ div _ as infix syntax for ring division
haftmann
parents: 60353
diff changeset
   576
    and distrib_right_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
60353
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   577
  by (rule distrib_left distrib_right)+
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   578
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   579
end
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   580
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   581
context ring
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   582
begin
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   583
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   584
lemma [field_simps]:
60429
d3d1e185cd63 uniform _ div _ as infix syntax for ring division
haftmann
parents: 60353
diff changeset
   585
  shows left_diff_distrib_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
d3d1e185cd63 uniform _ div _ as infix syntax for ring division
haftmann
parents: 60353
diff changeset
   586
    and right_diff_distrib_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
60353
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   587
  by (rule left_diff_distrib right_diff_distrib)+
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   588
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   589
end
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   590
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   591
setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   592
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   593
class semidom_divide = semidom + divide +
60429
d3d1e185cd63 uniform _ div _ as infix syntax for ring division
haftmann
parents: 60353
diff changeset
   594
  assumes nonzero_mult_divide_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> (a * b) div b = a"
d3d1e185cd63 uniform _ div _ as infix syntax for ring division
haftmann
parents: 60353
diff changeset
   595
  assumes divide_zero [simp]: "a div 0 = 0"
60353
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   596
begin
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   597
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   598
lemma nonzero_mult_divide_cancel_left [simp]:
60429
d3d1e185cd63 uniform _ div _ as infix syntax for ring division
haftmann
parents: 60353
diff changeset
   599
  "a \<noteq> 0 \<Longrightarrow> (a * b) div a = b"
60353
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   600
  using nonzero_mult_divide_cancel_right [of a b] by (simp add: ac_simps)
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   601
60516
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   602
subclass semiring_no_zero_divisors_cancel
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   603
proof
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   604
  fix a b c
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   605
  { fix a b c
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   606
    show "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   607
    proof (cases "c = 0")
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   608
      case True then show ?thesis by simp
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   609
    next
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   610
      case False
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   611
      { assume "a * c = b * c"
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   612
        then have "a * c div c = b * c div c"
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   613
          by simp
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   614
        with False have "a = b"
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   615
          by simp
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   616
      } then show ?thesis by auto
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   617
    qed
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   618
  }
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   619
  from this [of a c b]
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   620
  show "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   621
    by (simp add: ac_simps)
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   622
qed
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   623
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   624
lemma div_self [simp]:
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   625
  assumes "a \<noteq> 0"
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   626
  shows "a div a = 1"
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   627
  using assms nonzero_mult_divide_cancel_left [of a 1] by simp
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   628
60353
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   629
end
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   630
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   631
class idom_divide = idom + semidom_divide
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   632
60517
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   633
class algebraic_semidom = semidom_divide
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   634
begin
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   635
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   636
lemma dvd_div_mult_self [simp]:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   637
  "a dvd b \<Longrightarrow> b div a * a = b"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   638
  by (cases "a = 0") (auto elim: dvdE simp add: ac_simps)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   639
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   640
lemma dvd_mult_div_cancel [simp]:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   641
  "a dvd b \<Longrightarrow> a * (b div a) = b"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   642
  using dvd_div_mult_self [of a b] by (simp add: ac_simps)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   643
  
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   644
lemma div_mult_swap:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   645
  assumes "c dvd b"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   646
  shows "a * (b div c) = (a * b) div c"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   647
proof (cases "c = 0")
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   648
  case True then show ?thesis by simp
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   649
next
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   650
  case False from assms obtain d where "b = c * d" ..
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   651
  moreover from False have "a * divide (d * c) c = ((a * d) * c) div c"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   652
    by simp
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   653
  ultimately show ?thesis by (simp add: ac_simps)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   654
qed
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   655
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   656
lemma dvd_div_mult:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   657
  assumes "c dvd b"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   658
  shows "b div c * a = (b * a) div c"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   659
  using assms div_mult_swap [of c b a] by (simp add: ac_simps)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   660
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   661
  
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   662
text \<open>Units: invertible elements in a ring\<close>
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   663
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   664
abbreviation is_unit :: "'a \<Rightarrow> bool"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   665
where
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   666
  "is_unit a \<equiv> a dvd 1"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   667
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   668
lemma not_is_unit_0 [simp]:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   669
  "\<not> is_unit 0"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   670
  by simp
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   671
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   672
lemma unit_imp_dvd [dest]: 
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   673
  "is_unit b \<Longrightarrow> b dvd a"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   674
  by (rule dvd_trans [of _ 1]) simp_all
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   675
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   676
lemma unit_dvdE:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   677
  assumes "is_unit a"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   678
  obtains c where "a \<noteq> 0" and "b = a * c"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   679
proof -
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   680
  from assms have "a dvd b" by auto
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   681
  then obtain c where "b = a * c" ..
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   682
  moreover from assms have "a \<noteq> 0" by auto
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   683
  ultimately show thesis using that by blast
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   684
qed
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   685
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   686
lemma dvd_unit_imp_unit:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   687
  "a dvd b \<Longrightarrow> is_unit b \<Longrightarrow> is_unit a"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   688
  by (rule dvd_trans)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   689
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   690
lemma unit_div_1_unit [simp, intro]:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   691
  assumes "is_unit a"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   692
  shows "is_unit (1 div a)"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   693
proof -
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   694
  from assms have "1 = 1 div a * a" by simp
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   695
  then show "is_unit (1 div a)" by (rule dvdI)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   696
qed
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   697
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   698
lemma is_unitE [elim?]:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   699
  assumes "is_unit a"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   700
  obtains b where "a \<noteq> 0" and "b \<noteq> 0"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   701
    and "is_unit b" and "1 div a = b" and "1 div b = a"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   702
    and "a * b = 1" and "c div a = c * b"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   703
proof (rule that)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   704
  def b \<equiv> "1 div a"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   705
  then show "1 div a = b" by simp
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   706
  from b_def `is_unit a` show "is_unit b" by simp
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   707
  from `is_unit a` and `is_unit b` show "a \<noteq> 0" and "b \<noteq> 0" by auto
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   708
  from b_def `is_unit a` show "a * b = 1" by simp
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   709
  then have "1 = a * b" ..
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   710
  with b_def `b \<noteq> 0` show "1 div b = a" by simp
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   711
  from `is_unit a` have "a dvd c" ..
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   712
  then obtain d where "c = a * d" ..
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   713
  with `a \<noteq> 0` `a * b = 1` show "c div a = c * b"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   714
    by (simp add: mult.assoc mult.left_commute [of a])
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   715
qed
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   716
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   717
lemma unit_prod [intro]:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   718
  "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a * b)"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   719
  by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono) 
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   720
  
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   721
lemma unit_div [intro]:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   722
  "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div b)"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   723
  by (erule is_unitE [of b a]) (simp add: ac_simps unit_prod)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   724
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   725
lemma mult_unit_dvd_iff:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   726
  assumes "is_unit b"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   727
  shows "a * b dvd c \<longleftrightarrow> a dvd c"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   728
proof
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   729
  assume "a * b dvd c"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   730
  with assms show "a dvd c"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   731
    by (simp add: dvd_mult_left)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   732
next
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   733
  assume "a dvd c"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   734
  then obtain k where "c = a * k" ..
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   735
  with assms have "c = (a * b) * (1 div b * k)"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   736
    by (simp add: mult_ac)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   737
  then show "a * b dvd c" by (rule dvdI)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   738
qed
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   739
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   740
lemma dvd_mult_unit_iff:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   741
  assumes "is_unit b"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   742
  shows "a dvd c * b \<longleftrightarrow> a dvd c"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   743
proof
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   744
  assume "a dvd c * b"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   745
  with assms have "c * b dvd c * (b * (1 div b))"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   746
    by (subst mult_assoc [symmetric]) simp
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   747
  also from `is_unit b` have "b * (1 div b) = 1" by (rule is_unitE) simp
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   748
  finally have "c * b dvd c" by simp
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   749
  with `a dvd c * b` show "a dvd c" by (rule dvd_trans)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   750
next
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   751
  assume "a dvd c"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   752
  then show "a dvd c * b" by simp
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   753
qed
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   754
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   755
lemma div_unit_dvd_iff:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   756
  "is_unit b \<Longrightarrow> a div b dvd c \<longleftrightarrow> a dvd c"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   757
  by (erule is_unitE [of _ a]) (auto simp add: mult_unit_dvd_iff)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   758
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   759
lemma dvd_div_unit_iff:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   760
  "is_unit b \<Longrightarrow> a dvd c div b \<longleftrightarrow> a dvd c"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   761
  by (erule is_unitE [of _ c]) (simp add: dvd_mult_unit_iff)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   762
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   763
lemmas unit_dvd_iff = mult_unit_dvd_iff div_unit_dvd_iff
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   764
  dvd_mult_unit_iff dvd_div_unit_iff -- \<open>FIXME consider fact collection\<close>
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   765
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   766
lemma unit_mult_div_div [simp]:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   767
  "is_unit a \<Longrightarrow> b * (1 div a) = b div a"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   768
  by (erule is_unitE [of _ b]) simp
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   769
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   770
lemma unit_div_mult_self [simp]:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   771
  "is_unit a \<Longrightarrow> b div a * a = b"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   772
  by (rule dvd_div_mult_self) auto
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   773
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   774
lemma unit_div_1_div_1 [simp]:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   775
  "is_unit a \<Longrightarrow> 1 div (1 div a) = a"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   776
  by (erule is_unitE) simp
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   777
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   778
lemma unit_div_mult_swap:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   779
  "is_unit c \<Longrightarrow> a * (b div c) = (a * b) div c"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   780
  by (erule unit_dvdE [of _ b]) (simp add: mult.left_commute [of _ c])
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   781
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   782
lemma unit_div_commute:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   783
  "is_unit b \<Longrightarrow> (a div b) * c = (a * c) div b"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   784
  using unit_div_mult_swap [of b c a] by (simp add: ac_simps)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   785
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   786
lemma unit_eq_div1:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   787
  "is_unit b \<Longrightarrow> a div b = c \<longleftrightarrow> a = c * b"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   788
  by (auto elim: is_unitE)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   789
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   790
lemma unit_eq_div2:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   791
  "is_unit b \<Longrightarrow> a = c div b \<longleftrightarrow> a * b = c"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   792
  using unit_eq_div1 [of b c a] by auto
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   793
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   794
lemma unit_mult_left_cancel:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   795
  assumes "is_unit a"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   796
  shows "a * b = a * c \<longleftrightarrow> b = c" (is "?P \<longleftrightarrow> ?Q")
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   797
  using assms mult_cancel_left [of a b c] by auto 
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   798
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   799
lemma unit_mult_right_cancel:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   800
  "is_unit a \<Longrightarrow> b * a = c * a \<longleftrightarrow> b = c"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   801
  using unit_mult_left_cancel [of a b c] by (auto simp add: ac_simps)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   802
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   803
lemma unit_div_cancel:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   804
  assumes "is_unit a"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   805
  shows "b div a = c div a \<longleftrightarrow> b = c"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   806
proof -
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   807
  from assms have "is_unit (1 div a)" by simp
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   808
  then have "b * (1 div a) = c * (1 div a) \<longleftrightarrow> b = c"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   809
    by (rule unit_mult_right_cancel)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   810
  with assms show ?thesis by simp
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   811
qed
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   812
  
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   813
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   814
text \<open>Associated elements in a ring – an equivalence relation induced by the quasi-order divisibility \<close>
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   815
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   816
definition associated :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   817
where
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   818
  "associated a b \<longleftrightarrow> a dvd b \<and> b dvd a"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   819
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   820
lemma associatedI:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   821
  "a dvd b \<Longrightarrow> b dvd a \<Longrightarrow> associated a b"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   822
  by (simp add: associated_def)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   823
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   824
lemma associatedD1:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   825
  "associated a b \<Longrightarrow> a dvd b"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   826
  by (simp add: associated_def)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   827
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   828
lemma associatedD2:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   829
  "associated a b \<Longrightarrow> b dvd a"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   830
  by (simp add: associated_def)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   831
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   832
lemma associated_refl [simp]:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   833
  "associated a a"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   834
  by (auto intro: associatedI)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   835
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   836
lemma associated_sym:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   837
  "associated b a \<longleftrightarrow> associated a b"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   838
  by (auto intro: associatedI dest: associatedD1 associatedD2)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   839
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   840
lemma associated_trans:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   841
  "associated a b \<Longrightarrow> associated b c \<Longrightarrow> associated a c"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   842
  by (auto intro: associatedI dvd_trans dest: associatedD1 associatedD2)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   843
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   844
lemma associated_0 [simp]:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   845
  "associated 0 b \<longleftrightarrow> b = 0"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   846
  "associated a 0 \<longleftrightarrow> a = 0"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   847
  by (auto dest: associatedD1 associatedD2)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   848
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   849
lemma associated_unit:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   850
  "associated a b \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   851
  using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   852
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   853
lemma is_unit_associatedI:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   854
  assumes "is_unit c" and "a = c * b"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   855
  shows "associated a b"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   856
proof (rule associatedI)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   857
  from `a = c * b` show "b dvd a" by auto
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   858
  from `is_unit c` obtain d where "c * d = 1" by (rule is_unitE)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   859
  moreover from `a = c * b` have "d * a = d * (c * b)" by simp
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   860
  ultimately have "b = a * d" by (simp add: ac_simps)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   861
  then show "a dvd b" ..
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   862
qed
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   863
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   864
lemma associated_is_unitE:
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   865
  assumes "associated a b"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   866
  obtains c where "is_unit c" and "a = c * b"
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   867
proof (cases "b = 0")
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   868
  case True with assms have "is_unit 1" and "a = 1 * b" by simp_all
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   869
  with that show thesis .
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   870
next
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   871
  case False
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   872
  from assms have "a dvd b" and "b dvd a" by (auto dest: associatedD1 associatedD2)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   873
  then obtain c d where "b = a * d" and "a = b * c" by (blast elim: dvdE)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   874
  then have "a = c * b" and "(c * d) * b = 1 * b" by (simp_all add: ac_simps)
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   875
  with False have "c * d = 1" using mult_cancel_right [of "c * d" b 1] by simp
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   876
  then have "is_unit c" by auto
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   877
  with `a = c * b` that show thesis by blast
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   878
qed
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   879
  
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   880
lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff 
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   881
  dvd_div_unit_iff unit_div_mult_swap unit_div_commute
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   882
  unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel 
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   883
  unit_eq_div1 unit_eq_div2
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   884
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   885
end
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   886
38642
8fa437809c67 dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents: 37767
diff changeset
   887
class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +
8fa437809c67 dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents: 37767
diff changeset
   888
  assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
8fa437809c67 dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents: 37767
diff changeset
   889
  assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   890
begin
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   891
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   892
lemma mult_mono:
38642
8fa437809c67 dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents: 37767
diff changeset
   893
  "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   894
apply (erule mult_right_mono [THEN order_trans], assumption)
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   895
apply (erule mult_left_mono, assumption)
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   896
done
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   897
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   898
lemma mult_mono':
38642
8fa437809c67 dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents: 37767
diff changeset
   899
  "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   900
apply (rule mult_mono)
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   901
apply (fast intro: order_trans)+
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   902
done
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   903
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   904
end
21199
2d83f93c3580 * Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents: 20633
diff changeset
   905
38642
8fa437809c67 dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents: 37767
diff changeset
   906
class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   907
begin
14268
5cf13e80be0e Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents: 14267
diff changeset
   908
27516
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
   909
subclass semiring_0_cancel ..
23521
195fe3fe2831 added ordered_ring and ordered_semiring
obua
parents: 23496
diff changeset
   910
56536
aefb4a8da31f made mult_nonneg_nonneg a simp rule
nipkow
parents: 56480
diff changeset
   911
lemma mult_nonneg_nonneg[simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   912
using mult_left_mono [of 0 b a] by simp
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   913
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   914
lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   915
using mult_left_mono [of b 0 a] by simp
30692
44ea10bc07a7 clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents: 30650
diff changeset
   916
44ea10bc07a7 clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents: 30650
diff changeset
   917
lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0"
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   918
using mult_right_mono [of a 0 b] by simp
30692
44ea10bc07a7 clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents: 30650
diff changeset
   919
44ea10bc07a7 clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents: 30650
diff changeset
   920
text {* Legacy - use @{text mult_nonpos_nonneg} *}
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   921
lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0" 
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   922
by (drule mult_right_mono [of b 0], auto)
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   923
26234
1f6e28a88785 clarified proposition
haftmann
parents: 26193
diff changeset
   924
lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0" 
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
   925
by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   926
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   927
end
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   928
38642
8fa437809c67 dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents: 37767
diff changeset
   929
class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   930
begin
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   931
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34146
diff changeset
   932
subclass ordered_cancel_semiring ..
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34146
diff changeset
   933
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34146
diff changeset
   934
subclass ordered_comm_monoid_add ..
25304
7491c00f0915 removed subclass edge ordered_ring < lordered_ring
haftmann
parents: 25267
diff changeset
   935
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   936
lemma mult_left_less_imp_less:
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   937
  "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
   938
by (force simp add: mult_left_mono not_le [symmetric])
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   939
 
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   940
lemma mult_right_less_imp_less:
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   941
  "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
   942
by (force simp add: mult_right_mono not_le [symmetric])
23521
195fe3fe2831 added ordered_ring and ordered_semiring
obua
parents: 23496
diff changeset
   943
25186
f4d1ebffd025 localized further
haftmann
parents: 25152
diff changeset
   944
end
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   945
35043
07dbdf60d5ad dropped accidental duplication of "lin" prefix from cs. 108662d50512
haftmann
parents: 35032
diff changeset
   946
class linordered_semiring_1 = linordered_semiring + semiring_1
36622
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36348
diff changeset
   947
begin
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36348
diff changeset
   948
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36348
diff changeset
   949
lemma convex_bound_le:
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36348
diff changeset
   950
  assumes "x \<le> a" "y \<le> a" "0 \<le> u" "0 \<le> v" "u + v = 1"
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36348
diff changeset
   951
  shows "u * x + v * y \<le> a"
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36348
diff changeset
   952
proof-
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36348
diff changeset
   953
  from assms have "u * x + v * y \<le> u * a + v * a"
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36348
diff changeset
   954
    by (simp add: add_mono mult_left_mono)
49962
a8cc904a6820 Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents: 44921
diff changeset
   955
  thus ?thesis using assms unfolding distrib_right[symmetric] by simp
36622
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36348
diff changeset
   956
qed
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36348
diff changeset
   957
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36348
diff changeset
   958
end
35043
07dbdf60d5ad dropped accidental duplication of "lin" prefix from cs. 108662d50512
haftmann
parents: 35032
diff changeset
   959
07dbdf60d5ad dropped accidental duplication of "lin" prefix from cs. 108662d50512
haftmann
parents: 35032
diff changeset
   960
class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +
25062
af5ef0d4d655 global class syntax
haftmann
parents: 24748
diff changeset
   961
  assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
af5ef0d4d655 global class syntax
haftmann
parents: 24748
diff changeset
   962
  assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   963
begin
14341
a09441bd4f1e Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents: 14334
diff changeset
   964
27516
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
   965
subclass semiring_0_cancel ..
14940
b9ab8babd8b3 Further development of matrix theory
obua
parents: 14770
diff changeset
   966
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34146
diff changeset
   967
subclass linordered_semiring
28823
dcbef866c9e2 tuned unfold_locales invocation
haftmann
parents: 28559
diff changeset
   968
proof
23550
d4f1d6ef119c convert instance proofs to Isar style
huffman
parents: 23544
diff changeset
   969
  fix a b c :: 'a
d4f1d6ef119c convert instance proofs to Isar style
huffman
parents: 23544
diff changeset
   970
  assume A: "a \<le> b" "0 \<le> c"
d4f1d6ef119c convert instance proofs to Isar style
huffman
parents: 23544
diff changeset
   971
  from A show "c * a \<le> c * b"
25186
f4d1ebffd025 localized further
haftmann
parents: 25152
diff changeset
   972
    unfolding le_less
f4d1ebffd025 localized further
haftmann
parents: 25152
diff changeset
   973
    using mult_strict_left_mono by (cases "c = 0") auto
23550
d4f1d6ef119c convert instance proofs to Isar style
huffman
parents: 23544
diff changeset
   974
  from A show "a * c \<le> b * c"
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   975
    unfolding le_less
25186
f4d1ebffd025 localized further
haftmann
parents: 25152
diff changeset
   976
    using mult_strict_right_mono by (cases "c = 0") auto
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   977
qed
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   978
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   979
lemma mult_left_le_imp_le:
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   980
  "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
   981
by (force simp add: mult_strict_left_mono _not_less [symmetric])
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   982
 
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   983
lemma mult_right_le_imp_le:
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   984
  "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
   985
by (force simp add: mult_strict_right_mono not_less [symmetric])
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   986
56544
b60d5d119489 made mult_pos_pos a simp rule
nipkow
parents: 56536
diff changeset
   987
lemma mult_pos_pos[simp]: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   988
using mult_strict_left_mono [of 0 b a] by simp
30692
44ea10bc07a7 clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents: 30650
diff changeset
   989
44ea10bc07a7 clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents: 30650
diff changeset
   990
lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   991
using mult_strict_left_mono [of b 0 a] by simp
30692
44ea10bc07a7 clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents: 30650
diff changeset
   992
44ea10bc07a7 clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents: 30650
diff changeset
   993
lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0"
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   994
using mult_strict_right_mono [of a 0 b] by simp
30692
44ea10bc07a7 clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents: 30650
diff changeset
   995
44ea10bc07a7 clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents: 30650
diff changeset
   996
text {* Legacy - use @{text mult_neg_pos} *}
44ea10bc07a7 clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents: 30650
diff changeset
   997
lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0" 
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   998
by (drule mult_strict_right_mono [of b 0], auto)
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   999
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1000
lemma zero_less_mult_pos:
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1001
  "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
30692
44ea10bc07a7 clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents: 30650
diff changeset
  1002
apply (cases "b\<le>0")
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1003
 apply (auto simp add: le_less not_less)
30692
44ea10bc07a7 clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents: 30650
diff changeset
  1004
apply (drule_tac mult_pos_neg [of a b])
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1005
 apply (auto dest: less_not_sym)
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1006
done
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1007
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1008
lemma zero_less_mult_pos2:
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1009
  "0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
30692
44ea10bc07a7 clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents: 30650
diff changeset
  1010
apply (cases "b\<le>0")
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1011
 apply (auto simp add: le_less not_less)
30692
44ea10bc07a7 clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents: 30650
diff changeset
  1012
apply (drule_tac mult_pos_neg2 [of a b])
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1013
 apply (auto dest: less_not_sym)
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1014
done
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1015
26193
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1016
text{*Strict monotonicity in both arguments*}
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1017
lemma mult_strict_mono:
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1018
  assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c"
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1019
  shows "a * c < b * d"
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1020
  using assms apply (cases "c=0")
56544
b60d5d119489 made mult_pos_pos a simp rule
nipkow
parents: 56536
diff changeset
  1021
  apply (simp)
26193
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1022
  apply (erule mult_strict_right_mono [THEN less_trans])
30692
44ea10bc07a7 clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents: 30650
diff changeset
  1023
  apply (force simp add: le_less)
26193
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1024
  apply (erule mult_strict_left_mono, assumption)
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1025
  done
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1026
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1027
text{*This weaker variant has more natural premises*}
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1028
lemma mult_strict_mono':
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1029
  assumes "a < b" and "c < d" and "0 \<le> a" and "0 \<le> c"
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1030
  shows "a * c < b * d"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
  1031
by (rule mult_strict_mono) (insert assms, auto)
26193
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1032
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1033
lemma mult_less_le_imp_less:
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1034
  assumes "a < b" and "c \<le> d" and "0 \<le> a" and "0 < c"
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1035
  shows "a * c < b * d"
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1036
  using assms apply (subgoal_tac "a * c < b * c")
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1037
  apply (erule less_le_trans)
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1038
  apply (erule mult_left_mono)
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1039
  apply simp
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1040
  apply (erule mult_strict_right_mono)
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1041
  apply assumption
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1042
  done
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1043
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1044
lemma mult_le_less_imp_less:
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1045
  assumes "a \<le> b" and "c < d" and "0 < a" and "0 \<le> c"
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1046
  shows "a * c < b * d"
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1047
  using assms apply (subgoal_tac "a * c \<le> b * c")
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1048
  apply (erule le_less_trans)
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1049
  apply (erule mult_strict_left_mono)
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1050
  apply simp
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1051
  apply (erule mult_right_mono)
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1052
  apply simp
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1053
  done
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1054
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1055
end
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1056
35097
4554bb2abfa3 dropped last occurence of the linlinordered accident
haftmann
parents: 35092
diff changeset
  1057
class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1
36622
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36348
diff changeset
  1058
begin
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36348
diff changeset
  1059
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36348
diff changeset
  1060
subclass linordered_semiring_1 ..
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36348
diff changeset
  1061
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36348
diff changeset
  1062
lemma convex_bound_lt:
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36348
diff changeset
  1063
  assumes "x < a" "y < a" "0 \<le> u" "0 \<le> v" "u + v = 1"
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36348
diff changeset
  1064
  shows "u * x + v * y < a"
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36348
diff changeset
  1065
proof -
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36348
diff changeset
  1066
  from assms have "u * x + v * y < u * a + v * a"
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36348
diff changeset
  1067
    by (cases "u = 0")
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36348
diff changeset
  1068
       (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)
49962
a8cc904a6820 Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents: 44921
diff changeset
  1069
  thus ?thesis using assms unfolding distrib_right[symmetric] by simp
36622
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36348
diff changeset
  1070
qed
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36348
diff changeset
  1071
e393a91f86df Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents: 36348
diff changeset
  1072
end
33319
74f0dcc0b5fb moved algebraic classes to Ring_and_Field
haftmann
parents: 32960
diff changeset
  1073
38642
8fa437809c67 dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents: 37767
diff changeset
  1074
class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add + 
8fa437809c67 dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents: 37767
diff changeset
  1075
  assumes comm_mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
25186
f4d1ebffd025 localized further
haftmann
parents: 25152
diff changeset
  1076
begin
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
  1077
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34146
diff changeset
  1078
subclass ordered_semiring
28823
dcbef866c9e2 tuned unfold_locales invocation
haftmann
parents: 28559
diff changeset
  1079
proof
21199
2d83f93c3580 * Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents: 20633
diff changeset
  1080
  fix a b c :: 'a
23550
d4f1d6ef119c convert instance proofs to Isar style
huffman
parents: 23544
diff changeset
  1081
  assume "a \<le> b" "0 \<le> c"
38642
8fa437809c67 dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents: 37767
diff changeset
  1082
  thus "c * a \<le> c * b" by (rule comm_mult_left_mono)
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 56544
diff changeset
  1083
  thus "a * c \<le> b * c" by (simp only: mult.commute)
21199
2d83f93c3580 * Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents: 20633
diff changeset
  1084
qed
14265
95b42e69436c HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff changeset
  1085
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
  1086
end
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
  1087
38642
8fa437809c67 dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents: 37767
diff changeset
  1088
class ordered_cancel_comm_semiring = ordered_comm_semiring + cancel_comm_monoid_add
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
  1089
begin
14265
95b42e69436c HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff changeset
  1090
38642
8fa437809c67 dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents: 37767
diff changeset
  1091
subclass comm_semiring_0_cancel ..
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34146
diff changeset
  1092
subclass ordered_comm_semiring ..
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34146
diff changeset
  1093
subclass ordered_cancel_semiring ..
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
  1094
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
  1095
end
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
  1096
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34146
diff changeset
  1097
class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +
38642
8fa437809c67 dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents: 37767
diff changeset
  1098
  assumes comm_mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
  1099
begin
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
  1100
35043
07dbdf60d5ad dropped accidental duplication of "lin" prefix from cs. 108662d50512
haftmann
parents: 35032
diff changeset
  1101
subclass linordered_semiring_strict
28823
dcbef866c9e2 tuned unfold_locales invocation
haftmann
parents: 28559
diff changeset
  1102
proof
23550
d4f1d6ef119c convert instance proofs to Isar style
huffman
parents: 23544
diff changeset
  1103
  fix a b c :: 'a
d4f1d6ef119c convert instance proofs to Isar style
huffman
parents: 23544
diff changeset
  1104
  assume "a < b" "0 < c"
38642
8fa437809c67 dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents: 37767
diff changeset
  1105
  thus "c * a < c * b" by (rule comm_mult_strict_left_mono)
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 56544
diff changeset
  1106
  thus "a * c < b * c" by (simp only: mult.commute)
23550
d4f1d6ef119c convert instance proofs to Isar style
huffman
parents: 23544
diff changeset
  1107
qed
14272
5efbb548107d Tidying of the integer development; towards removing the
paulson
parents: 14270
diff changeset
  1108
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34146
diff changeset
  1109
subclass ordered_cancel_comm_semiring
28823
dcbef866c9e2 tuned unfold_locales invocation
haftmann
parents: 28559
diff changeset
  1110
proof
23550
d4f1d6ef119c convert instance proofs to Isar style
huffman
parents: 23544
diff changeset
  1111
  fix a b c :: 'a
d4f1d6ef119c convert instance proofs to Isar style
huffman
parents: 23544
diff changeset
  1112
  assume "a \<le> b" "0 \<le> c"
d4f1d6ef119c convert instance proofs to Isar style
huffman
parents: 23544
diff changeset
  1113
  thus "c * a \<le> c * b"
25186
f4d1ebffd025 localized further
haftmann
parents: 25152
diff changeset
  1114
    unfolding le_less
26193
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1115
    using mult_strict_left_mono by (cases "c = 0") auto
23550
d4f1d6ef119c convert instance proofs to Isar style
huffman
parents: 23544
diff changeset
  1116
qed
14272
5efbb548107d Tidying of the integer development; towards removing the
paulson
parents: 14270
diff changeset
  1117
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
  1118
end
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1119
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34146
diff changeset
  1120
class ordered_ring = ring + ordered_cancel_semiring 
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
  1121
begin
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1122
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34146
diff changeset
  1123
subclass ordered_ab_group_add ..
14270
342451d763f9 More re-organising of numerical theorems
paulson
parents: 14269
diff changeset
  1124
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1125
lemma less_add_iff1:
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1126
  "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
  1127
by (simp add: algebra_simps)
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1128
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1129
lemma less_add_iff2:
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1130
  "a * e + c < b * e + d \<longleftrightarrow> c < (b - a) * e + d"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
  1131
by (simp add: algebra_simps)
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1132
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1133
lemma le_add_iff1:
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1134
  "a * e + c \<le> b * e + d \<longleftrightarrow> (a - b) * e + c \<le> d"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
  1135
by (simp add: algebra_simps)
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1136
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1137
lemma le_add_iff2:
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1138
  "a * e + c \<le> b * e + d \<longleftrightarrow> c \<le> (b - a) * e + d"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
  1139
by (simp add: algebra_simps)
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1140
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1141
lemma mult_left_mono_neg:
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1142
  "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1143
  apply (drule mult_left_mono [of _ _ "- c"])
35216
7641e8d831d2 get rid of many duplicate simp rule warnings
huffman
parents: 35097
diff changeset
  1144
  apply simp_all
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1145
  done
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1146
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1147
lemma mult_right_mono_neg:
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1148
  "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1149
  apply (drule mult_right_mono [of _ _ "- c"])
35216
7641e8d831d2 get rid of many duplicate simp rule warnings
huffman
parents: 35097
diff changeset
  1150
  apply simp_all
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1151
  done
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1152
30692
44ea10bc07a7 clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents: 30650
diff changeset
  1153
lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1154
using mult_right_mono_neg [of a 0 b] by simp
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1155
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1156
lemma split_mult_pos_le:
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1157
  "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b"
56536
aefb4a8da31f made mult_nonneg_nonneg a simp rule
nipkow
parents: 56480
diff changeset
  1158
by (auto simp add: mult_nonpos_nonpos)
25186
f4d1ebffd025 localized further
haftmann
parents: 25152
diff changeset
  1159
f4d1ebffd025 localized further
haftmann
parents: 25152
diff changeset
  1160
end
14270
342451d763f9 More re-organising of numerical theorems
paulson
parents: 14269
diff changeset
  1161
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34146
diff changeset
  1162
class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if
25304
7491c00f0915 removed subclass edge ordered_ring < lordered_ring
haftmann
parents: 25267
diff changeset
  1163
begin
7491c00f0915 removed subclass edge ordered_ring < lordered_ring
haftmann
parents: 25267
diff changeset
  1164
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34146
diff changeset
  1165
subclass ordered_ring ..
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34146
diff changeset
  1166
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34146
diff changeset
  1167
subclass ordered_ab_group_add_abs
28823
dcbef866c9e2 tuned unfold_locales invocation
haftmann
parents: 28559
diff changeset
  1168
proof
25304
7491c00f0915 removed subclass edge ordered_ring < lordered_ring
haftmann
parents: 25267
diff changeset
  1169
  fix a b
7491c00f0915 removed subclass edge ordered_ring < lordered_ring
haftmann
parents: 25267
diff changeset
  1170
  show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 54225
diff changeset
  1171
    by (auto simp add: abs_if not_le not_less algebra_simps simp del: add.commute dest: add_neg_neg add_nonneg_nonneg)
35216
7641e8d831d2 get rid of many duplicate simp rule warnings
huffman
parents: 35097
diff changeset
  1172
qed (auto simp add: abs_if)
25304
7491c00f0915 removed subclass edge ordered_ring < lordered_ring
haftmann
parents: 25267
diff changeset
  1173
35631
0b8a5fd339ab generalize some lemmas from class linordered_ring_strict to linordered_ring
huffman
parents: 35302
diff changeset
  1174
lemma zero_le_square [simp]: "0 \<le> a * a"
0b8a5fd339ab generalize some lemmas from class linordered_ring_strict to linordered_ring
huffman
parents: 35302
diff changeset
  1175
  using linear [of 0 a]
56536
aefb4a8da31f made mult_nonneg_nonneg a simp rule
nipkow
parents: 56480
diff changeset
  1176
  by (auto simp add: mult_nonpos_nonpos)
35631
0b8a5fd339ab generalize some lemmas from class linordered_ring_strict to linordered_ring
huffman
parents: 35302
diff changeset
  1177
0b8a5fd339ab generalize some lemmas from class linordered_ring_strict to linordered_ring
huffman
parents: 35302
diff changeset
  1178
lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
0b8a5fd339ab generalize some lemmas from class linordered_ring_strict to linordered_ring
huffman
parents: 35302
diff changeset
  1179
  by (simp add: not_less)
0b8a5fd339ab generalize some lemmas from class linordered_ring_strict to linordered_ring
huffman
parents: 35302
diff changeset
  1180
25304
7491c00f0915 removed subclass edge ordered_ring < lordered_ring
haftmann
parents: 25267
diff changeset
  1181
end
23521
195fe3fe2831 added ordered_ring and ordered_semiring
obua
parents: 23496
diff changeset
  1182
35043
07dbdf60d5ad dropped accidental duplication of "lin" prefix from cs. 108662d50512
haftmann
parents: 35032
diff changeset
  1183
class linordered_ring_strict = ring + linordered_semiring_strict
25304
7491c00f0915 removed subclass edge ordered_ring < lordered_ring
haftmann
parents: 25267
diff changeset
  1184
  + ordered_ab_group_add + abs_if
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1185
begin
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 14341
diff changeset
  1186
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34146
diff changeset
  1187
subclass linordered_ring ..
25304
7491c00f0915 removed subclass edge ordered_ring < lordered_ring
haftmann
parents: 25267
diff changeset
  1188
30692
44ea10bc07a7 clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents: 30650
diff changeset
  1189
lemma mult_strict_left_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
44ea10bc07a7 clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents: 30650
diff changeset
  1190
using mult_strict_left_mono [of b a "- c"] by simp
44ea10bc07a7 clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents: 30650
diff changeset
  1191
44ea10bc07a7 clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents: 30650
diff changeset
  1192
lemma mult_strict_right_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"
44ea10bc07a7 clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents: 30650
diff changeset
  1193
using mult_strict_right_mono [of b a "- c"] by simp
44ea10bc07a7 clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents: 30650
diff changeset
  1194
44ea10bc07a7 clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents: 30650
diff changeset
  1195
lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1196
using mult_strict_right_mono_neg [of a 0 b] by simp
14738
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents: 14603
diff changeset
  1197
25917
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1198
subclass ring_no_zero_divisors
28823
dcbef866c9e2 tuned unfold_locales invocation
haftmann
parents: 28559
diff changeset
  1199
proof
25917
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1200
  fix a b
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1201
  assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff)
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1202
  assume "b \<noteq> 0" then have B: "b < 0 \<or> 0 < b" by (simp add: neq_iff)
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1203
  have "a * b < 0 \<or> 0 < a * b"
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1204
  proof (cases "a < 0")
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1205
    case True note A' = this
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1206
    show ?thesis proof (cases "b < 0")
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1207
      case True with A'
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1208
      show ?thesis by (auto dest: mult_neg_neg)
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1209
    next
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1210
      case False with B have "0 < b" by auto
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1211
      with A' show ?thesis by (auto dest: mult_strict_right_mono)
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1212
    qed
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1213
  next
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1214
    case False with A have A': "0 < a" by auto
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1215
    show ?thesis proof (cases "b < 0")
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1216
      case True with A'
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1217
      show ?thesis by (auto dest: mult_strict_right_mono_neg)
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1218
    next
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1219
      case False with B have "0 < b" by auto
56544
b60d5d119489 made mult_pos_pos a simp rule
nipkow
parents: 56536
diff changeset
  1220
      with A' show ?thesis by auto
25917
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1221
    qed
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1222
  qed
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1223
  then show "a * b \<noteq> 0" by (simp add: neq_iff)
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1224
qed
25304
7491c00f0915 removed subclass edge ordered_ring < lordered_ring
haftmann
parents: 25267
diff changeset
  1225
56480
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56217
diff changeset
  1226
lemma zero_less_mult_iff: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56217
diff changeset
  1227
  by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
56544
b60d5d119489 made mult_pos_pos a simp rule
nipkow
parents: 56536
diff changeset
  1228
     (auto simp add: mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2)
22990
775e9de3db48 added classes ring_no_zero_divisors and dom (non-commutative version of idom);
huffman
parents: 22987
diff changeset
  1229
56480
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56217
diff changeset
  1230
lemma zero_le_mult_iff: "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56217
diff changeset
  1231
  by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
14265
95b42e69436c HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff changeset
  1232
95b42e69436c HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff changeset
  1233
lemma mult_less_0_iff:
25917
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1234
  "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
35216
7641e8d831d2 get rid of many duplicate simp rule warnings
huffman
parents: 35097
diff changeset
  1235
  apply (insert zero_less_mult_iff [of "-a" b])
7641e8d831d2 get rid of many duplicate simp rule warnings
huffman
parents: 35097
diff changeset
  1236
  apply force
25917
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1237
  done
14265
95b42e69436c HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff changeset
  1238
95b42e69436c HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff changeset
  1239
lemma mult_le_0_iff:
25917
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1240
  "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1241
  apply (insert zero_le_mult_iff [of "-a" b]) 
35216
7641e8d831d2 get rid of many duplicate simp rule warnings
huffman
parents: 35097
diff changeset
  1242
  apply force
25917
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1243
  done
d6c920623afc further localization
haftmann
parents: 25762
diff changeset
  1244
26193
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1245
text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1246
   also with the relations @{text "\<le>"} and equality.*}
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1247
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1248
text{*These ``disjunction'' versions produce two cases when the comparison is
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1249
 an assumption, but effectively four when the comparison is a goal.*}
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1250
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1251
lemma mult_less_cancel_right_disj:
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1252
  "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1253
  apply (cases "c = 0")
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1254
  apply (auto simp add: neq_iff mult_strict_right_mono 
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1255
                      mult_strict_right_mono_neg)
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1256
  apply (auto simp add: not_less 
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1257
                      not_le [symmetric, of "a*c"]
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1258
                      not_le [symmetric, of a])
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1259
  apply (erule_tac [!] notE)
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1260
  apply (auto simp add: less_imp_le mult_right_mono 
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1261
                      mult_right_mono_neg)
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1262
  done
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1263
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1264
lemma mult_less_cancel_left_disj:
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1265
  "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1266
  apply (cases "c = 0")
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1267
  apply (auto simp add: neq_iff mult_strict_left_mono 
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
  1268
                      mult_strict_left_mono_neg)
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset