src/HOL/Rings.thy
author hoelzl
Wed, 10 Feb 2016 18:43:19 +0100
changeset 62376 85f38d5f8807
parent 62366 95c6cf433c91
child 62377 ace69956d018
permissions -rw-r--r--
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
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
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
    10
section \<open>Rings\<close>
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
62366
95c6cf433c91 more theorems
haftmann
parents: 62349
diff changeset
    13
imports Groups Set
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
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61762
diff changeset
    21
text\<open>For the \<open>combine_numerals\<close> simproc\<close>
25152
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
60562
24af00b010cf Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents: 60529
diff changeset
    98
  "of_bool p = (if p then 1 else 0)"
54225
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
60562
24af00b010cf Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents: 60529
diff changeset
   116
24af00b010cf Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents: 60529
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
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   121
text \<open>Abstract divisibility\<close>
27651
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"
60562
24af00b010cf Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents: 60529
diff changeset
   133
  unfolding dvd_def by blast
27651
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
62349
7c23469b5118 cleansed junk-producing interpretations for gcd/lcm on nat altogether
haftmann
parents: 62347
diff changeset
   148
lemma dvd_trans [trans]:
27651
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
62366
95c6cf433c91 more theorems
haftmann
parents: 62349
diff changeset
   158
lemma subset_divisors_dvd:
95c6cf433c91 more theorems
haftmann
parents: 62349
diff changeset
   159
  "{c. c dvd a} \<subseteq> {c. c dvd b} \<longleftrightarrow> a dvd b"
95c6cf433c91 more theorems
haftmann
parents: 62349
diff changeset
   160
  by (auto simp add: subset_iff intro: dvd_trans)
95c6cf433c91 more theorems
haftmann
parents: 62349
diff changeset
   161
95c6cf433c91 more theorems
haftmann
parents: 62349
diff changeset
   162
lemma strict_subset_divisors_dvd:
95c6cf433c91 more theorems
haftmann
parents: 62349
diff changeset
   163
  "{c. c dvd a} \<subset> {c. c dvd b} \<longleftrightarrow> a dvd b \<and> \<not> b dvd a"
95c6cf433c91 more theorems
haftmann
parents: 62349
diff changeset
   164
  by (auto simp add: subset_iff intro: dvd_trans)
95c6cf433c91 more theorems
haftmann
parents: 62349
diff changeset
   165
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   166
lemma one_dvd [simp]:
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   167
  "1 dvd a"
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   168
  by (auto intro!: dvdI)
28559
55c003a5600a tuned default rules of (dvd)
haftmann
parents: 28141
diff changeset
   169
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   170
lemma dvd_mult [simp]:
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   171
  "a dvd c \<Longrightarrow> a dvd (b * c)"
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   172
  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
   173
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   174
lemma dvd_mult2 [simp]:
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   175
  "a dvd b \<Longrightarrow> a dvd (b * c)"
60562
24af00b010cf Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents: 60529
diff changeset
   176
  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
   177
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   178
lemma dvd_triv_right [simp]:
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   179
  "a dvd b * a"
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   180
  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
   181
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   182
lemma dvd_triv_left [simp]:
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   183
  "a dvd a * b"
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   184
  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
   185
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   186
lemma mult_dvd_mono:
30042
31039ee583fa Removed subsumed lemmas
nipkow
parents: 29981
diff changeset
   187
  assumes "a dvd b"
31039ee583fa Removed subsumed lemmas
nipkow
parents: 29981
diff changeset
   188
    and "c dvd d"
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   189
  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
   190
proof -
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   191
  from \<open>a dvd b\<close> obtain b' where "b = a * b'" ..
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   192
  moreover from \<open>c dvd d\<close> 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
   193
  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
   194
  then show ?thesis ..
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   195
qed
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   196
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   197
lemma dvd_mult_left:
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   198
  "a * b dvd c \<Longrightarrow> a dvd c"
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   199
  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
   200
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   201
lemma dvd_mult_right:
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   202
  "a * b dvd c \<Longrightarrow> b dvd c"
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   203
  using dvd_mult_left [of b a c] by (simp add: ac_simps)
60562
24af00b010cf Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents: 60529
diff changeset
   204
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   205
end
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   206
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   207
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
   208
begin
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   209
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   210
subclass semiring_1 ..
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   211
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   212
lemma dvd_0_left_iff [simp]:
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   213
  "0 dvd a \<longleftrightarrow> a = 0"
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   214
  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
   215
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   216
lemma dvd_0_right [iff]:
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   217
  "a dvd 0"
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   218
proof
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   219
  show "0 = a * 0" by simp
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   220
qed
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   221
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   222
lemma dvd_0_left:
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   223
  "0 dvd a \<Longrightarrow> a = 0"
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   224
  by simp
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   225
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   226
lemma dvd_add [simp]:
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   227
  assumes "a dvd b" and "a dvd c"
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   228
  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
   229
proof -
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   230
  from \<open>a dvd b\<close> obtain b' where "b = a * b'" ..
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   231
  moreover from \<open>a dvd c\<close> obtain c' where "c = a * c'" ..
49962
a8cc904a6820 Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents: 44921
diff changeset
   232
  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
   233
  then show ?thesis ..
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   234
qed
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   235
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   236
end
14421
ee97b6463cb4 new Ring_and_Field hierarchy, eliminating redundant axioms
paulson
parents: 14398
diff changeset
   237
29904
856f16a3b436 add class cancel_comm_monoid_add
huffman
parents: 29833
diff changeset
   238
class semiring_1_cancel = semiring + cancel_comm_monoid_add
856f16a3b436 add class cancel_comm_monoid_add
huffman
parents: 29833
diff changeset
   239
  + zero_neq_one + monoid_mult
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   240
begin
14940
b9ab8babd8b3 Further development of matrix theory
obua
parents: 14770
diff changeset
   241
27516
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
   242
subclass semiring_0_cancel ..
25512
4134f7c782e2 using intro_locales instead of unfold_locales if appropriate
haftmann
parents: 25450
diff changeset
   243
27516
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
   244
subclass semiring_1 ..
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   245
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   246
end
21199
2d83f93c3580 * Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents: 20633
diff changeset
   247
60562
24af00b010cf Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents: 60529
diff changeset
   248
class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add +
24af00b010cf Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents: 60529
diff changeset
   249
                               zero_neq_one + comm_monoid_mult +
24af00b010cf Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents: 60529
diff changeset
   250
  assumes right_diff_distrib' [algebra_simps]: "a * (b - c) = a * b - a * c"
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   251
begin
14738
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents: 14603
diff changeset
   252
27516
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
   253
subclass semiring_1_cancel ..
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
   254
subclass comm_semiring_0_cancel ..
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
   255
subclass comm_semiring_1 ..
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   256
59816
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   257
lemma left_diff_distrib' [algebra_simps]:
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   258
  "(b - c) * a = b * a - c * a"
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   259
  by (simp add: algebra_simps)
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   260
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   261
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
   262
  "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
   263
proof -
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   264
  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
   265
  proof
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   266
    assume ?Q then show ?P by simp
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   267
  next
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   268
    assume ?P
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   269
    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
   270
    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
   271
    then have "b = a * d - a * c" by simp
60562
24af00b010cf Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents: 60529
diff changeset
   272
    then have "b = a * (d - c)" by (simp add: algebra_simps)
59816
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   273
    then show ?Q ..
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   274
  qed
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   275
  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
   276
qed
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   277
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   278
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
   279
  "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
   280
  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
   281
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   282
lemma dvd_add_triv_left_iff [simp]:
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   283
  "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
   284
  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
   285
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   286
lemma dvd_add_triv_right_iff [simp]:
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   287
  "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
   288
  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
   289
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   290
lemma dvd_add_right_iff:
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   291
  assumes "a dvd b"
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   292
  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
   293
proof
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   294
  assume ?P then obtain d where "b + c = a * d" ..
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   295
  moreover from \<open>a dvd b\<close> obtain e where "b = a * e" ..
59816
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   296
  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
   297
  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
   298
  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
   299
  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
   300
  then show ?Q ..
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   301
next
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   302
  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
   303
qed
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   304
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   305
lemma dvd_add_left_iff:
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   306
  assumes "a dvd c"
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   307
  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
   308
  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
   309
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   310
end
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   311
22390
378f34b1e380 now using "class"
haftmann
parents: 21328
diff changeset
   312
class ring = semiring + ab_group_add
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   313
begin
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   314
27516
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
   315
subclass semiring_0_cancel ..
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   316
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   317
text \<open>Distribution rules\<close>
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   318
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   319
lemma minus_mult_left: "- (a * b) = - a * b"
60562
24af00b010cf Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents: 60529
diff changeset
   320
by (rule minus_unique) (simp add: distrib_right [symmetric])
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   321
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   322
lemma minus_mult_right: "- (a * b) = a * - b"
60562
24af00b010cf Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents: 60529
diff changeset
   323
by (rule minus_unique) (simp add: distrib_left [symmetric])
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   324
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   325
text\<open>Extract signs from products\<close>
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 52435
diff changeset
   326
lemmas mult_minus_left [simp] = minus_mult_left [symmetric]
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 52435
diff changeset
   327
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
   328
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   329
lemma minus_mult_minus [simp]: "- a * - b = a * b"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
   330
by simp
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   331
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   332
lemma minus_mult_commute: "- a * b = a * - b"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
   333
by simp
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
   334
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
   335
lemma right_diff_distrib [algebra_simps]:
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 54225
diff changeset
   336
  "a * (b - c) = a * b - a * c"
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 54225
diff changeset
   337
  using distrib_left [of a b "-c "] by simp
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
   338
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
   339
lemma left_diff_distrib [algebra_simps]:
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 54225
diff changeset
   340
  "(a - b) * c = a * c - b * c"
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 54225
diff changeset
   341
  using distrib_right [of a "- b" c] by simp
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   342
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 52435
diff changeset
   343
lemmas ring_distribs =
49962
a8cc904a6820 Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents: 44921
diff changeset
   344
  distrib_left distrib_right left_diff_distrib right_diff_distrib
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   345
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   346
lemma eq_add_iff1:
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   347
  "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
   348
by (simp add: algebra_simps)
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   349
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   350
lemma eq_add_iff2:
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   351
  "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
   352
by (simp add: algebra_simps)
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   353
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   354
end
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   355
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 52435
diff changeset
   356
lemmas ring_distribs =
49962
a8cc904a6820 Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents: 44921
diff changeset
   357
  distrib_left distrib_right left_diff_distrib right_diff_distrib
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   358
22390
378f34b1e380 now using "class"
haftmann
parents: 21328
diff changeset
   359
class comm_ring = comm_semiring + ab_group_add
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   360
begin
14738
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents: 14603
diff changeset
   361
27516
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
   362
subclass ring ..
28141
193c3ea0f63b instances comm_semiring_0_cancel < comm_semiring_0, comm_ring < comm_semiring_0_cancel
huffman
parents: 27651
diff changeset
   363
subclass comm_semiring_0_cancel ..
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   364
44350
63cddfbc5a09 replace lemma realpow_two_diff with new lemma square_diff_square_factored
huffman
parents: 44346
diff changeset
   365
lemma square_diff_square_factored:
63cddfbc5a09 replace lemma realpow_two_diff with new lemma square_diff_square_factored
huffman
parents: 44346
diff changeset
   366
  "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
   367
  by (simp add: algebra_simps)
63cddfbc5a09 replace lemma realpow_two_diff with new lemma square_diff_square_factored
huffman
parents: 44346
diff changeset
   368
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   369
end
14738
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents: 14603
diff changeset
   370
22390
378f34b1e380 now using "class"
haftmann
parents: 21328
diff changeset
   371
class ring_1 = ring + zero_neq_one + monoid_mult
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   372
begin
14265
95b42e69436c HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff changeset
   373
27516
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
   374
subclass semiring_1_cancel ..
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   375
44346
00dd3c4dabe0 rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy
huffman
parents: 44064
diff changeset
   376
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
   377
  "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
   378
  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
   379
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   380
end
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   381
22390
378f34b1e380 now using "class"
haftmann
parents: 21328
diff changeset
   382
class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   383
begin
14738
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents: 14603
diff changeset
   384
27516
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
   385
subclass ring_1 ..
60562
24af00b010cf Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents: 60529
diff changeset
   386
subclass comm_semiring_1_cancel
59816
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   387
  by unfold_locales (simp add: algebra_simps)
58647
fce800afeec7 more facts about abstract divisibility
haftmann
parents: 58198
diff changeset
   388
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
   389
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
   390
proof
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   391
  assume "x dvd - y"
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   392
  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
   393
  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
   394
next
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   395
  assume "x dvd y"
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   396
  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
   397
  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
   398
qed
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   399
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
   400
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
   401
proof
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   402
  assume "- x dvd y"
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   403
  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
   404
  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
   405
  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
   406
next
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   407
  assume "x dvd y"
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   408
  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
   409
  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
   410
  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
   411
qed
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   412
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 54225
diff changeset
   413
lemma dvd_diff [simp]:
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 54225
diff changeset
   414
  "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
   415
  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
   416
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   417
end
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   418
59833
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   419
class semiring_no_zero_divisors = semiring_0 +
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   420
  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
   421
begin
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   422
59833
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   423
lemma divisors_zero:
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   424
  assumes "a * b = 0"
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   425
  shows "a = 0 \<or> b = 0"
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   426
proof (rule classical)
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   427
  assume "\<not> (a = 0 \<or> b = 0)"
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   428
  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
   429
  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
   430
  with assms show ?thesis by simp
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   431
qed
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   432
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   433
lemma mult_eq_0_iff [simp]:
58952
5d82cdef6c1b equivalence rules for structures without zero divisors
haftmann
parents: 58889
diff changeset
   434
  shows "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   435
proof (cases "a = 0 \<or> b = 0")
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   436
  case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   437
    then show ?thesis using no_zero_divisors by simp
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   438
next
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   439
  case True then show ?thesis by auto
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   440
qed
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   441
58952
5d82cdef6c1b equivalence rules for structures without zero divisors
haftmann
parents: 58889
diff changeset
   442
end
5d82cdef6c1b equivalence rules for structures without zero divisors
haftmann
parents: 58889
diff changeset
   443
60516
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   444
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
   445
  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
   446
    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
   447
begin
5d82cdef6c1b equivalence rules for structures without zero divisors
haftmann
parents: 58889
diff changeset
   448
5d82cdef6c1b equivalence rules for structures without zero divisors
haftmann
parents: 58889
diff changeset
   449
lemma mult_left_cancel:
5d82cdef6c1b equivalence rules for structures without zero divisors
haftmann
parents: 58889
diff changeset
   450
  "c \<noteq> 0 \<Longrightarrow> c * a = c * b \<longleftrightarrow> a = b"
60562
24af00b010cf Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents: 60529
diff changeset
   451
  by simp
56217
dc429a5b13c4 Some rationalisation of basic lemmas
paulson <lp15@cam.ac.uk>
parents: 55912
diff changeset
   452
58952
5d82cdef6c1b equivalence rules for structures without zero divisors
haftmann
parents: 58889
diff changeset
   453
lemma mult_right_cancel:
5d82cdef6c1b equivalence rules for structures without zero divisors
haftmann
parents: 58889
diff changeset
   454
  "c \<noteq> 0 \<Longrightarrow> a * c = b * c \<longleftrightarrow> a = b"
60562
24af00b010cf Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents: 60529
diff changeset
   455
  by simp
56217
dc429a5b13c4 Some rationalisation of basic lemmas
paulson <lp15@cam.ac.uk>
parents: 55912
diff changeset
   456
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   457
end
22990
775e9de3db48 added classes ring_no_zero_divisors and dom (non-commutative version of idom);
huffman
parents: 22987
diff changeset
   458
60516
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   459
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
   460
begin
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   461
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   462
subclass semiring_no_zero_divisors_cancel
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   463
proof
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   464
  fix a b c
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   465
  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
   466
    by (simp add: algebra_simps)
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   467
  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
   468
    by auto
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   469
  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
   470
  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
   471
    by (simp add: algebra_simps)
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   472
  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
   473
    by auto
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   474
  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
   475
qed
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   476
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   477
end
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   478
23544
4b4165cb3e0d rename class dom to ring_1_no_zero_divisors
huffman
parents: 23527
diff changeset
   479
class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
26274
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   480
begin
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   481
36970
fb3fdb4b585e remove simp attribute from square_eq_1_iff
huffman
parents: 36821
diff changeset
   482
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
   483
  "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
   484
proof -
9207505d1ee5 move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents: 36719
diff changeset
   485
  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
   486
    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
   487
  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
   488
    by simp
9207505d1ee5 move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents: 36719
diff changeset
   489
  thus ?thesis
9207505d1ee5 move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents: 36719
diff changeset
   490
    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
   491
qed
9207505d1ee5 move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents: 36719
diff changeset
   492
26274
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   493
lemma mult_cancel_right1 [simp]:
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   494
  "c = b * c \<longleftrightarrow> c = 0 \<or> b = 1"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
   495
by (insert mult_cancel_right [of 1 c b], force)
26274
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   496
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   497
lemma mult_cancel_right2 [simp]:
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   498
  "a * c = c \<longleftrightarrow> c = 0 \<or> a = 1"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
   499
by (insert mult_cancel_right [of a c 1], simp)
60562
24af00b010cf Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents: 60529
diff changeset
   500
26274
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   501
lemma mult_cancel_left1 [simp]:
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   502
  "c = c * b \<longleftrightarrow> c = 0 \<or> b = 1"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
   503
by (insert mult_cancel_left [of c 1 b], force)
26274
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   504
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   505
lemma mult_cancel_left2 [simp]:
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   506
  "c * a = c \<longleftrightarrow> c = 0 \<or> a = 1"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
   507
by (insert mult_cancel_left [of c a 1], simp)
26274
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   508
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   509
end
22990
775e9de3db48 added classes ring_no_zero_divisors and dom (non-commutative version of idom);
huffman
parents: 22987
diff changeset
   510
60562
24af00b010cf Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents: 60529
diff changeset
   511
class semidom = comm_semiring_1_cancel + semiring_no_zero_divisors
59833
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   512
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   513
class idom = comm_ring_1 + semiring_no_zero_divisors
25186
f4d1ebffd025 localized further
haftmann
parents: 25152
diff changeset
   514
begin
14421
ee97b6463cb4 new Ring_and_Field hierarchy, eliminating redundant axioms
paulson
parents: 14398
diff changeset
   515
59833
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   516
subclass semidom ..
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   517
27516
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
   518
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
   519
29981
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   520
lemma dvd_mult_cancel_right [simp]:
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   521
  "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
   522
proof -
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   523
  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
   524
    unfolding dvd_def by (simp add: ac_simps)
29981
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   525
  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
   526
    unfolding dvd_def by simp
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   527
  finally show ?thesis .
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   528
qed
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   529
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   530
lemma dvd_mult_cancel_left [simp]:
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   531
  "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
   532
proof -
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   533
  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
   534
    unfolding dvd_def by (simp add: ac_simps)
29981
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   535
  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
   536
    unfolding dvd_def by simp
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   537
  finally show ?thesis .
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   538
qed
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   539
60516
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   540
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
   541
proof
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   542
  assume "a * a = b * b"
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   543
  then have "(a - b) * (a + b) = 0"
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   544
    by (simp add: algebra_simps)
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   545
  then show "a = b \<or> a = - b"
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   546
    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
   547
next
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   548
  assume "a = b \<or> a = - b"
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   549
  then show "a * a = b * b" by auto
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   550
qed
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   551
25186
f4d1ebffd025 localized further
haftmann
parents: 25152
diff changeset
   552
end
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   553
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   554
text \<open>
35302
4bc6b4d70e08 tuned text
haftmann
parents: 35216
diff changeset
   555
  The theory of partially ordered rings is taken from the books:
4bc6b4d70e08 tuned text
haftmann
parents: 35216
diff changeset
   556
  \begin{itemize}
60562
24af00b010cf Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents: 60529
diff changeset
   557
  \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979
35302
4bc6b4d70e08 tuned text
haftmann
parents: 35216
diff changeset
   558
  \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
4bc6b4d70e08 tuned text
haftmann
parents: 35216
diff changeset
   559
  \end{itemize}
60562
24af00b010cf Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents: 60529
diff changeset
   560
  Most of the used notions can also be looked up in
35302
4bc6b4d70e08 tuned text
haftmann
parents: 35216
diff changeset
   561
  \begin{itemize}
54703
499f92dc6e45 more antiquotations;
wenzelm
parents: 54489
diff changeset
   562
  \item @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
35302
4bc6b4d70e08 tuned text
haftmann
parents: 35216
diff changeset
   563
  \item \emph{Algebra I} by van der Waerden, Springer.
4bc6b4d70e08 tuned text
haftmann
parents: 35216
diff changeset
   564
  \end{itemize}
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   565
\<close>
35302
4bc6b4d70e08 tuned text
haftmann
parents: 35216
diff changeset
   566
60353
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   567
class divide =
60429
d3d1e185cd63 uniform _ div _ as infix syntax for ring division
haftmann
parents: 60353
diff changeset
   568
  fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "div" 70)
60353
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   569
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   570
setup \<open>Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"})\<close>
60353
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   571
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   572
context semiring
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   573
begin
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   574
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   575
lemma [field_simps]:
60429
d3d1e185cd63 uniform _ div _ as infix syntax for ring division
haftmann
parents: 60353
diff changeset
   576
  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
   577
    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
   578
  by (rule distrib_left distrib_right)+
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   579
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   580
end
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   581
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   582
context ring
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   583
begin
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   584
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   585
lemma [field_simps]:
60429
d3d1e185cd63 uniform _ div _ as infix syntax for ring division
haftmann
parents: 60353
diff changeset
   586
  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
   587
    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
   588
  by (rule left_diff_distrib right_diff_distrib)+
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   589
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   590
end
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   591
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   592
setup \<open>Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"})\<close>
60353
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   593
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   594
class semidom_divide = semidom + divide +
60429
d3d1e185cd63 uniform _ div _ as infix syntax for ring division
haftmann
parents: 60353
diff changeset
   595
  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
   596
  assumes divide_zero [simp]: "a div 0 = 0"
60353
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   597
begin
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   598
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   599
lemma nonzero_mult_divide_cancel_left [simp]:
60429
d3d1e185cd63 uniform _ div _ as infix syntax for ring division
haftmann
parents: 60353
diff changeset
   600
  "a \<noteq> 0 \<Longrightarrow> (a * b) div a = b"
60353
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   601
  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
   602
60516
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   603
subclass semiring_no_zero_divisors_cancel
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   604
proof
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
  { fix a b c
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   607
    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
   608
    proof (cases "c = 0")
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   609
      case True then show ?thesis by simp
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   610
    next
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   611
      case False
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   612
      { assume "a * c = b * c"
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   613
        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
   614
          by simp
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   615
        with False have "a = b"
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   616
          by simp
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   617
      } then show ?thesis by auto
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   618
    qed
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   619
  }
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   620
  from this [of a c b]
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   621
  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
   622
    by (simp add: ac_simps)
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   623
qed
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   624
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   625
lemma div_self [simp]:
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   626
  assumes "a \<noteq> 0"
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   627
  shows "a div a = 1"
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   628
  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
   629
60570
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   630
lemma divide_zero_left [simp]:
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   631
  "0 div a = 0"
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   632
proof (cases "a = 0")
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   633
  case True then show ?thesis by simp
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   634
next
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   635
  case False then have "a * 0 div a = 0"
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   636
    by (rule nonzero_mult_divide_cancel_left)
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   637
  then show ?thesis by simp
62376
85f38d5f8807 Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents: 62366
diff changeset
   638
qed
60570
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   639
60690
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   640
lemma divide_1 [simp]:
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   641
  "a div 1 = a"
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   642
  using nonzero_mult_divide_cancel_left [of 1 a] by simp
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   643
60867
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   644
end
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   645
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   646
class idom_divide = idom + semidom_divide
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   647
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   648
class algebraic_semidom = semidom_divide
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   649
begin
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   650
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   651
text \<open>
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   652
  Class @{class algebraic_semidom} enriches a integral domain
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   653
  by notions from algebra, like units in a ring.
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   654
  It is a separate class to avoid spoiling fields with notions
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   655
  which are degenerated there.
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   656
\<close>
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   657
60690
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   658
lemma dvd_times_left_cancel_iff [simp]:
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   659
  assumes "a \<noteq> 0"
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   660
  shows "a * b dvd a * c \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   661
proof
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   662
  assume ?P then obtain d where "a * c = a * b * d" ..
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   663
  with assms have "c = b * d" by (simp add: ac_simps)
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   664
  then show ?Q ..
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   665
next
62376
85f38d5f8807 Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents: 62366
diff changeset
   666
  assume ?Q then obtain d where "c = b * d" ..
60690
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   667
  then have "a * c = a * b * d" by (simp add: ac_simps)
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   668
  then show ?P ..
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   669
qed
62376
85f38d5f8807 Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents: 62366
diff changeset
   670
60690
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   671
lemma dvd_times_right_cancel_iff [simp]:
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   672
  assumes "a \<noteq> 0"
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   673
  shows "b * a dvd c * a \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   674
using dvd_times_left_cancel_iff [of a b c] assms by (simp add: ac_simps)
62376
85f38d5f8807 Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents: 62366
diff changeset
   675
60690
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   676
lemma div_dvd_iff_mult:
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   677
  assumes "b \<noteq> 0" and "b dvd a"
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   678
  shows "a div b dvd c \<longleftrightarrow> a dvd c * b"
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   679
proof -
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   680
  from \<open>b dvd a\<close> obtain d where "a = b * d" ..
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   681
  with \<open>b \<noteq> 0\<close> show ?thesis by (simp add: ac_simps)
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   682
qed
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   683
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   684
lemma dvd_div_iff_mult:
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   685
  assumes "c \<noteq> 0" and "c dvd b"
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   686
  shows "a dvd b div c \<longleftrightarrow> a * c dvd b"
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   687
proof -
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   688
  from \<open>c dvd b\<close> obtain d where "b = c * d" ..
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   689
  with \<open>c \<noteq> 0\<close> show ?thesis by (simp add: mult.commute [of a])
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   690
qed
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   691
60867
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   692
lemma div_dvd_div [simp]:
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   693
  assumes "a dvd b" and "a dvd c"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   694
  shows "b div a dvd c div a \<longleftrightarrow> b dvd c"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   695
proof (cases "a = 0")
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   696
  case True with assms show ?thesis by simp
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   697
next
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   698
  case False
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   699
  moreover from assms obtain k l where "b = a * k" and "c = a * l"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   700
    by (auto elim!: dvdE)
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   701
  ultimately show ?thesis by simp
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   702
qed
60353
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   703
60867
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   704
lemma div_add [simp]:
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   705
  assumes "c dvd a" and "c dvd b"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   706
  shows "(a + b) div c = a div c + b div c"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   707
proof (cases "c = 0")
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   708
  case True then show ?thesis by simp
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   709
next
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   710
  case False
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   711
  moreover from assms obtain k l where "a = c * k" and "b = c * l"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   712
    by (auto elim!: dvdE)
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   713
  moreover have "c * k + c * l = c * (k + l)"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   714
    by (simp add: algebra_simps)
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   715
  ultimately show ?thesis
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   716
    by simp
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   717
qed
60517
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   718
60867
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   719
lemma div_mult_div_if_dvd:
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   720
  assumes "b dvd a" and "d dvd c"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   721
  shows "(a div b) * (c div d) = (a * c) div (b * d)"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   722
proof (cases "b = 0 \<or> c = 0")
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   723
  case True with assms show ?thesis by auto
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   724
next
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   725
  case False
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   726
  moreover from assms obtain k l where "a = b * k" and "c = d * l"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   727
    by (auto elim!: dvdE)
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   728
  moreover have "b * k * (d * l) div (b * d) = (b * d) * (k * l) div (b * d)"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   729
    by (simp add: ac_simps)
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   730
  ultimately show ?thesis by simp
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   731
qed
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   732
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   733
lemma dvd_div_eq_mult:
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   734
  assumes "a \<noteq> 0" and "a dvd b"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   735
  shows "b div a = c \<longleftrightarrow> b = c * a"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   736
proof
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   737
  assume "b = c * a"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   738
  then show "b div a = c" by (simp add: assms)
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   739
next
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   740
  assume "b div a = c"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   741
  then have "b div a * a = c * a" by simp
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   742
  moreover from \<open>a \<noteq> 0\<close> \<open>a dvd b\<close> have "b div a * a = b"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   743
    by (auto elim!: dvdE simp add: ac_simps)
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   744
  ultimately show "b = c * a" by simp
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   745
qed
60688
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
   746
60517
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   747
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
   748
  "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
   749
  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
   750
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   751
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
   752
  "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
   753
  using dvd_div_mult_self [of a b] by (simp add: ac_simps)
60562
24af00b010cf Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents: 60529
diff changeset
   754
60517
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_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
   756
  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
   757
  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
   758
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
   759
  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
   760
next
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   761
  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
   762
  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
   763
    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
   764
  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
   765
qed
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   766
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   767
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
   768
  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
   769
  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
   770
  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
   771
60570
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   772
lemma dvd_div_mult2_eq:
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   773
  assumes "b * c dvd a"
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   774
  shows "a div (b * c) = a div b div c"
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   775
using assms proof
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   776
  fix k
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   777
  assume "a = b * c * k"
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   778
  then show ?thesis
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   779
    by (cases "b = 0 \<or> c = 0") (auto, simp add: ac_simps)
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   780
qed
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   781
60867
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   782
lemma dvd_div_div_eq_mult:
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   783
  assumes "a \<noteq> 0" "c \<noteq> 0" and "a dvd b" "c dvd d"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   784
  shows "b div a = d div c \<longleftrightarrow> b * c = a * d" (is "?P \<longleftrightarrow> ?Q")
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   785
proof -
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   786
  from assms have "a * c \<noteq> 0" by simp
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   787
  then have "?P \<longleftrightarrow> b div a * (a * c) = d div c * (a * c)"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   788
    by simp
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   789
  also have "\<dots> \<longleftrightarrow> (a * (b div a)) * c = (c * (d div c)) * a"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   790
    by (simp add: ac_simps)
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   791
  also have "\<dots> \<longleftrightarrow> (a * b div a) * c = (c * d div c) * a"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   792
    using assms by (simp add: div_mult_swap)
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   793
  also have "\<dots> \<longleftrightarrow> ?Q"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   794
    using assms by (simp add: ac_simps)
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   795
  finally show ?thesis .
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   796
qed
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   797
60562
24af00b010cf Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents: 60529
diff changeset
   798
60517
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   799
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
   800
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   801
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
   802
where
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   803
  "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
   804
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   805
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
   806
  "\<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
   807
  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
60562
24af00b010cf Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents: 60529
diff changeset
   809
lemma unit_imp_dvd [dest]:
60517
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   810
  "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
   811
  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
   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
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
   814
  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
   815
  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
   816
proof -
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   817
  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
   818
  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
   819
  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
   820
  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
   821
qed
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   822
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   823
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
   824
  "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
   825
  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
   826
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   827
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
   828
  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
   829
  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
   830
proof -
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   831
  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
   832
  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
   833
qed
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   834
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   835
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
   836
  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
   837
  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
   838
    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
   839
    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
   840
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
   841
  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
   842
  then show "1 div a = b" by simp
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   843
  from b_def \<open>is_unit a\<close> show "is_unit b" by simp
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   844
  from \<open>is_unit a\<close> and \<open>is_unit b\<close> show "a \<noteq> 0" and "b \<noteq> 0" by auto
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   845
  from b_def \<open>is_unit a\<close> show "a * b = 1" by simp
60517
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   846
  then have "1 = a * b" ..
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   847
  with b_def \<open>b \<noteq> 0\<close> show "1 div b = a" by simp
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   848
  from \<open>is_unit a\<close> have "a dvd c" ..
60517
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   849
  then obtain d where "c = a * d" ..
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   850
  with \<open>a \<noteq> 0\<close> \<open>a * b = 1\<close> show "c div a = c * b"
60517
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   851
    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
   852
qed
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   853
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   854
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
   855
  "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a * b)"
60562
24af00b010cf Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents: 60529
diff changeset
   856
  by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono)
24af00b010cf Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents: 60529
diff changeset
   857
62366
95c6cf433c91 more theorems
haftmann
parents: 62349
diff changeset
   858
lemma is_unit_mult_iff:
95c6cf433c91 more theorems
haftmann
parents: 62349
diff changeset
   859
  "is_unit (a * b) \<longleftrightarrow> is_unit a \<and> is_unit b" (is "?P \<longleftrightarrow> ?Q")
95c6cf433c91 more theorems
haftmann
parents: 62349
diff changeset
   860
  by (auto dest: dvd_mult_left dvd_mult_right)
95c6cf433c91 more theorems
haftmann
parents: 62349
diff changeset
   861
60517
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   862
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
   863
  "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
   864
  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
   865
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   866
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
   867
  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
   868
  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
   869
proof
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   870
  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
   871
  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
   872
    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
   873
next
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   874
  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
   875
  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
   876
  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
   877
    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
   878
  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
   879
qed
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   880
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   881
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
   882
  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
   883
  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
   884
proof
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   885
  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
   886
  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
   887
    by (subst mult_assoc [symmetric]) simp
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   888
  also from \<open>is_unit b\<close> have "b * (1 div b) = 1" by (rule is_unitE) simp
60517
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   889
  finally have "c * b dvd c" by simp
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   890
  with \<open>a dvd c * b\<close> show "a dvd c" by (rule dvd_trans)
60517
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   891
next
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   892
  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
   893
  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
   894
qed
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   895
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   896
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
   897
  "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
   898
  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
   899
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   900
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
   901
  "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
   902
  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
   903
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   904
lemmas unit_dvd_iff = mult_unit_dvd_iff div_unit_dvd_iff
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61762
diff changeset
   905
  dvd_mult_unit_iff dvd_div_unit_iff \<comment> \<open>FIXME consider fact collection\<close>
60517
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   906
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   907
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
   908
  "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
   909
  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
   910
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   911
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
   912
  "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
   913
  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
   914
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   915
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
   916
  "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
   917
  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
   918
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   919
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
   920
  "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
   921
  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
   922
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   923
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
   924
  "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
   925
  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
   926
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   927
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
   928
  "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
   929
  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
   930
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   931
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
   932
  "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
   933
  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
   934
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   935
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
   936
  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
   937
  shows "a * b = a * c \<longleftrightarrow> b = c" (is "?P \<longleftrightarrow> ?Q")
60562
24af00b010cf Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents: 60529
diff changeset
   938
  using assms mult_cancel_left [of a b c] by auto
60517
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   939
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   940
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
   941
  "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
   942
  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
   943
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   944
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
   945
  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
   946
  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
   947
proof -
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   948
  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
   949
  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
   950
    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
   951
  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
   952
qed
60562
24af00b010cf Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents: 60529
diff changeset
   953
60570
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   954
lemma is_unit_div_mult2_eq:
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   955
  assumes "is_unit b" and "is_unit c"
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   956
  shows "a div (b * c) = a div b div c"
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   957
proof -
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   958
  from assms have "is_unit (b * c)" by (simp add: unit_prod)
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   959
  then have "b * c dvd a"
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   960
    by (rule unit_imp_dvd)
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   961
  then show ?thesis
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   962
    by (rule dvd_div_mult2_eq)
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   963
qed
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   964
60562
24af00b010cf Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents: 60529
diff changeset
   965
lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff
60517
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   966
  dvd_div_unit_iff unit_div_mult_swap unit_div_commute
60562
24af00b010cf Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents: 60529
diff changeset
   967
  unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel
60517
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   968
  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
   969
60685
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
   970
lemma is_unit_divide_mult_cancel_left:
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
   971
  assumes "a \<noteq> 0" and "is_unit b"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
   972
  shows "a div (a * b) = 1 div b"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
   973
proof -
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
   974
  from assms have "a div (a * b) = a div a div b"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
   975
    by (simp add: mult_unit_dvd_iff dvd_div_mult2_eq)
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
   976
  with assms show ?thesis by simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
   977
qed
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
   978
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
   979
lemma is_unit_divide_mult_cancel_right:
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
   980
  assumes "a \<noteq> 0" and "is_unit b"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
   981
  shows "a div (b * a) = 1 div b"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
   982
  using assms is_unit_divide_mult_cancel_left [of a b] by (simp add: ac_simps)
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
   983
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
   984
end
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
   985
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
   986
class normalization_semidom = algebraic_semidom +
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
   987
  fixes normalize :: "'a \<Rightarrow> 'a"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
   988
    and unit_factor :: "'a \<Rightarrow> 'a"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
   989
  assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
   990
  assumes normalize_0 [simp]: "normalize 0 = 0"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
   991
    and unit_factor_0 [simp]: "unit_factor 0 = 0"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
   992
  assumes is_unit_normalize:
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
   993
    "is_unit a  \<Longrightarrow> normalize a = 1"
62376
85f38d5f8807 Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents: 62366
diff changeset
   994
  assumes unit_factor_is_unit [iff]:
60685
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
   995
    "a \<noteq> 0 \<Longrightarrow> is_unit (unit_factor a)"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
   996
  assumes unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
   997
begin
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
   998
60688
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
   999
text \<open>
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1000
  Class @{class normalization_semidom} cultivates the idea that
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1001
  each integral domain can be split into equivalence classes
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1002
  whose representants are associated, i.e. divide each other.
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1003
  @{const normalize} specifies a canonical representant for each equivalence
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1004
  class.  The rationale behind this is that it is easier to reason about equality
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1005
  than equivalences, hence we prefer to think about equality of normalized
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1006
  values rather than associated elements.
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1007
\<close>
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1008
60685
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1009
lemma unit_factor_dvd [simp]:
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1010
  "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd b"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1011
  by (rule unit_imp_dvd) simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1012
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1013
lemma unit_factor_self [simp]:
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1014
  "unit_factor a dvd a"
62376
85f38d5f8807 Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents: 62366
diff changeset
  1015
  by (cases "a = 0") simp_all
85f38d5f8807 Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents: 62366
diff changeset
  1016
60685
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1017
lemma normalize_mult_unit_factor [simp]:
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1018
  "normalize a * unit_factor a = a"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1019
  using unit_factor_mult_normalize [of a] by (simp add: ac_simps)
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1020
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1021
lemma normalize_eq_0_iff [simp]:
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1022
  "normalize a = 0 \<longleftrightarrow> a = 0" (is "?P \<longleftrightarrow> ?Q")
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1023
proof
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1024
  assume ?P
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1025
  moreover have "unit_factor a * normalize a = a" by simp
62376
85f38d5f8807 Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents: 62366
diff changeset
  1026
  ultimately show ?Q by simp
60685
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1027
next
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1028
  assume ?Q then show ?P by simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1029
qed
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1030
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1031
lemma unit_factor_eq_0_iff [simp]:
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1032
  "unit_factor a = 0 \<longleftrightarrow> a = 0" (is "?P \<longleftrightarrow> ?Q")
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1033
proof
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1034
  assume ?P
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1035
  moreover have "unit_factor a * normalize a = a" by simp
62376
85f38d5f8807 Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents: 62366
diff changeset
  1036
  ultimately show ?Q by simp
60685
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1037
next
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1038
  assume ?Q then show ?P by simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1039
qed
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1040
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1041
lemma is_unit_unit_factor:
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1042
  assumes "is_unit a" shows "unit_factor a = a"
62376
85f38d5f8807 Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents: 62366
diff changeset
  1043
proof -
60685
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1044
  from assms have "normalize a = 1" by (rule is_unit_normalize)
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1045
  moreover from unit_factor_mult_normalize have "unit_factor a * normalize a = a" .
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1046
  ultimately show ?thesis by simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1047
qed
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1048
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1049
lemma unit_factor_1 [simp]:
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1050
  "unit_factor 1 = 1"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1051
  by (rule is_unit_unit_factor) simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1052
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1053
lemma normalize_1 [simp]:
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1054
  "normalize 1 = 1"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1055
  by (rule is_unit_normalize) simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1056
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1057
lemma normalize_1_iff:
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1058
  "normalize a = 1 \<longleftrightarrow> is_unit a" (is "?P \<longleftrightarrow> ?Q")
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1059
proof
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1060
  assume ?Q then show ?P by (rule is_unit_normalize)
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1061
next
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1062
  assume ?P
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1063
  then have "a \<noteq> 0" by auto
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1064
  from \<open>?P\<close> have "unit_factor a * normalize a = unit_factor a * 1"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1065
    by simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1066
  then have "unit_factor a = a"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1067
    by simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1068
  moreover have "is_unit (unit_factor a)"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1069
    using \<open>a \<noteq> 0\<close> by simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1070
  ultimately show ?Q by simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1071
qed
62376
85f38d5f8807 Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents: 62366
diff changeset
  1072
60685
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1073
lemma div_normalize [simp]:
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1074
  "a div normalize a = unit_factor a"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1075
proof (cases "a = 0")
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1076
  case True then show ?thesis by simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1077
next
62376
85f38d5f8807 Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents: 62366
diff changeset
  1078
  case False then have "normalize a \<noteq> 0" by simp
60685
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1079
  with nonzero_mult_divide_cancel_right
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1080
  have "unit_factor a * normalize a div normalize a = unit_factor a" by blast
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1081
  then show ?thesis by simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1082
qed
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1083
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1084
lemma div_unit_factor [simp]:
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1085
  "a div unit_factor a = normalize a"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1086
proof (cases "a = 0")
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1087
  case True then show ?thesis by simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1088
next
62376
85f38d5f8807 Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents: 62366
diff changeset
  1089
  case False then have "unit_factor a \<noteq> 0" by simp
60685
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1090
  with nonzero_mult_divide_cancel_left
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1091
  have "unit_factor a * normalize a div unit_factor a = normalize a" by blast
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1092
  then show ?thesis by simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1093
qed
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1094
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1095
lemma normalize_div [simp]:
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1096
  "normalize a div a = 1 div unit_factor a"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1097
proof (cases "a = 0")
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1098
  case True then show ?thesis by simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1099
next
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1100
  case False
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1101
  have "normalize a div a = normalize a div (unit_factor a * normalize a)"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1102
    by simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1103
  also have "\<dots> = 1 div unit_factor a"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1104
    using False by (subst is_unit_divide_mult_cancel_right) simp_all
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1105
  finally show ?thesis .
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1106
qed
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1107
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1108
lemma mult_one_div_unit_factor [simp]:
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1109
  "a * (1 div unit_factor b) = a div unit_factor b"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1110
  by (cases "b = 0") simp_all
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1111
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1112
lemma normalize_mult:
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1113
  "normalize (a * b) = normalize a * normalize b"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1114
proof (cases "a = 0 \<or> b = 0")
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1115
  case True then show ?thesis by auto
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1116
next
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1117
  case False
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1118
  from unit_factor_mult_normalize have "unit_factor (a * b) * normalize (a * b) = a * b" .
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1119
  then have "normalize (a * b) = a * b div unit_factor (a * b)" by simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1120
  also have "\<dots> = a * b div unit_factor (b * a)" by (simp add: ac_simps)
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1121
  also have "\<dots> = a * b div unit_factor b div unit_factor a"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1122
    using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric])
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1123
  also have "\<dots> = a * (b div unit_factor b) div unit_factor a"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1124
    using False by (subst unit_div_mult_swap) simp_all
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1125
  also have "\<dots> = normalize a * normalize b"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1126
    using False by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric])
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1127
  finally show ?thesis .
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1128
qed
62376
85f38d5f8807 Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents: 62366
diff changeset
  1129
60685
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1130
lemma unit_factor_idem [simp]:
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1131
  "unit_factor (unit_factor a) = unit_factor a"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1132
  by (cases "a = 0") (auto intro: is_unit_unit_factor)
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1133
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1134
lemma normalize_unit_factor [simp]:
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1135
  "a \<noteq> 0 \<Longrightarrow> normalize (unit_factor a) = 1"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1136
  by (rule is_unit_normalize) simp
62376
85f38d5f8807 Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents: 62366
diff changeset
  1137
60685
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1138
lemma normalize_idem [simp]:
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1139
  "normalize (normalize a) = normalize a"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1140
proof (cases "a = 0")
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1141
  case True then show ?thesis by simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1142
next
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1143
  case False
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1144
  have "normalize a = normalize (unit_factor a * normalize a)" by simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1145
  also have "\<dots> = normalize (unit_factor a) * normalize (normalize a)"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1146
    by (simp only: normalize_mult)
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1147
  finally show ?thesis using False by simp_all
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1148
qed
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1149
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1150
lemma unit_factor_normalize [simp]:
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1151
  assumes "a \<noteq> 0"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1152
  shows "unit_factor (normalize a) = 1"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1153
proof -
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1154
  from assms have "normalize a \<noteq> 0" by simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1155
  have "unit_factor (normalize a) * normalize (normalize a) = normalize a"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1156
    by (simp only: unit_factor_mult_normalize)
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1157
  then have "unit_factor (normalize a) * normalize a = normalize a"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1158
    by simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1159
  with \<open>normalize a \<noteq> 0\<close>
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1160
  have "unit_factor (normalize a) * normalize a div normalize a = normalize a div normalize a"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1161
    by simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1162
  with \<open>normalize a \<noteq> 0\<close>
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1163
  show ?thesis by simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1164
qed
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1165
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1166
lemma dvd_unit_factor_div:
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1167
  assumes "b dvd a"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1168
  shows "unit_factor (a div b) = unit_factor a div unit_factor b"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1169
proof -
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1170
  from assms have "a = a div b * b"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1171
    by simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1172
  then have "unit_factor a = unit_factor (a div b * b)"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1173
    by simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1174
  then show ?thesis
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1175
    by (cases "b = 0") (simp_all add: unit_factor_mult)
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1176
qed
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1177
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1178
lemma dvd_normalize_div:
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1179
  assumes "b dvd a"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1180
  shows "normalize (a div b) = normalize a div normalize b"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1181
proof -
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1182
  from assms have "a = a div b * b"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1183
    by simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1184
  then have "normalize a = normalize (a div b * b)"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1185
    by simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1186
  then show ?thesis
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1187
    by (cases "b = 0") (simp_all add: normalize_mult)
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1188
qed
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1189
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1190
lemma normalize_dvd_iff [simp]:
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1191
  "normalize a dvd b \<longleftrightarrow> a dvd b"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1192
proof -
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1193
  have "normalize a dvd b \<longleftrightarrow> unit_factor a * normalize a dvd b"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1194
    using mult_unit_dvd_iff [of "unit_factor a" "normalize a" b]
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1195
      by (cases "a = 0") simp_all
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1196
  then show ?thesis by simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1197
qed
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1198
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1199
lemma dvd_normalize_iff [simp]:
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1200
  "a dvd normalize b \<longleftrightarrow> a dvd b"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1201
proof -
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1202
  have "a dvd normalize  b \<longleftrightarrow> a dvd normalize b * unit_factor b"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1203
    using dvd_mult_unit_iff [of "unit_factor b" a "normalize b"]
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1204
      by (cases "b = 0") simp_all
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1205
  then show ?thesis by simp
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1206
qed
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1207
60688
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1208
text \<open>
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1209
  We avoid an explicit definition of associated elements but prefer
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1210
  explicit normalisation instead.  In theory we could define an abbreviation
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1211
  like @{prop "associated a b \<longleftrightarrow> normalize a = normalize b"} but this is
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1212
  counterproductive without suggestive infix syntax, which we do not want
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1213
  to sacrifice for this purpose here.
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1214
\<close>
60685
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1215
60688
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1216
lemma associatedI:
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1217
  assumes "a dvd b" and "b dvd a"
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1218
  shows "normalize a = normalize b"
60685
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1219
proof (cases "a = 0 \<or> b = 0")
60688
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1220
  case True with assms show ?thesis by auto
60685
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1221
next
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1222
  case False
60688
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1223
  from \<open>a dvd b\<close> obtain c where b: "b = a * c" ..
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1224
  moreover from \<open>b dvd a\<close> obtain d where a: "a = b * d" ..
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1225
  ultimately have "b * 1 = b * (c * d)" by (simp add: ac_simps)
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1226
  with False have "1 = c * d"
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1227
    unfolding mult_cancel_left by simp
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1228
  then have "is_unit c" and "is_unit d" by auto
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1229
  with a b show ?thesis by (simp add: normalize_mult is_unit_normalize)
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1230
qed
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1231
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1232
lemma associatedD1:
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1233
  "normalize a = normalize b \<Longrightarrow> a dvd b"
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1234
  using dvd_normalize_iff [of _ b, symmetric] normalize_dvd_iff [of a _, symmetric]
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1235
  by simp
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1236
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1237
lemma associatedD2:
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1238
  "normalize a = normalize b \<Longrightarrow> b dvd a"
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1239
  using dvd_normalize_iff [of _ a, symmetric] normalize_dvd_iff [of b _, symmetric]
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1240
  by simp
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1241
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1242
lemma associated_unit:
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1243
  "normalize a = normalize b \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b"
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1244
  using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2)
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1245
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1246
lemma associated_iff_dvd:
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1247
  "normalize a = normalize b \<longleftrightarrow> a dvd b \<and> b dvd a" (is "?P \<longleftrightarrow> ?Q")
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1248
proof
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1249
  assume ?Q then show ?P by (auto intro!: associatedI)
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1250
next
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1251
  assume ?P
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1252
  then have "unit_factor a * normalize a = unit_factor a * normalize b"
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1253
    by simp
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1254
  then have *: "normalize b * unit_factor a = a"
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1255
    by (simp add: ac_simps)
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1256
  show ?Q
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1257
  proof (cases "a = 0 \<or> b = 0")
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1258
    case True with \<open>?P\<close> show ?thesis by auto
60685
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1259
  next
62376
85f38d5f8807 Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents: 62366
diff changeset
  1260
    case False
60688
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1261
    then have "b dvd normalize b * unit_factor a" and "normalize b * unit_factor a dvd b"
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1262
      by (simp_all add: mult_unit_dvd_iff dvd_mult_unit_iff)
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1263
    with * show ?thesis by simp
60685
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1264
  qed
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1265
qed
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1266
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1267
lemma associated_eqI:
60688
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1268
  assumes "a dvd b" and "b dvd a"
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1269
  assumes "normalize a = a" and "normalize b = b"
60685
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1270
  shows "a = b"
60688
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1271
proof -
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1272
  from assms have "normalize a = normalize b"
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1273
    unfolding associated_iff_dvd by simp
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1274
  with \<open>normalize a = a\<close> have "a = normalize b" by simp
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
  1275
  with \<open>normalize b = b\<close> show "a = b" by simp
60685
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1276
qed
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1277
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1278
end
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1279
62376
85f38d5f8807 Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents: 62366
diff changeset
  1280
class ordered_semiring = semiring + ordered_comm_monoid_add +
38642
8fa437809c67 dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents: 37767
diff changeset
  1281
  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
  1282
  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
  1283
begin
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
  1284