src/HOL/Rings.thy
author haftmann
Tue, 22 May 2018 18:14:29 +0000
changeset 68252 8b284d24f434
parent 68251 54a127873735
child 68253 a8660a39e304
permissions -rw-r--r--
automatic classical rule to derive a dvd b from b mod a = 0
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
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
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
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
    21
text \<open>For the \<open>combine_numerals\<close> simproc\<close>
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
    22
lemma combine_common_factor: "a * e + (b * e + c) = (a + b) * e + c"
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
    23
  by (simp add: distrib_right ac_simps)
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
    24
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
    25
end
14504
7a3d80e276d4 new type class abelian_group
paulson
parents: 14475
diff changeset
    26
22390
378f34b1e380 now using "class"
haftmann
parents: 21328
diff changeset
    27
class mult_zero = times + zero +
25062
af5ef0d4d655 global class syntax
haftmann
parents: 24748
diff changeset
    28
  assumes mult_zero_left [simp]: "0 * a = 0"
af5ef0d4d655 global class syntax
haftmann
parents: 24748
diff changeset
    29
  assumes mult_zero_right [simp]: "a * 0 = 0"
58195
1fee63e0377d added various facts
haftmann
parents: 57514
diff changeset
    30
begin
1fee63e0377d added various facts
haftmann
parents: 57514
diff changeset
    31
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
    32
lemma mult_not_zero: "a * b \<noteq> 0 \<Longrightarrow> a \<noteq> 0 \<and> b \<noteq> 0"
58195
1fee63e0377d added various facts
haftmann
parents: 57514
diff changeset
    33
  by auto
1fee63e0377d added various facts
haftmann
parents: 57514
diff changeset
    34
1fee63e0377d added various facts
haftmann
parents: 57514
diff changeset
    35
end
21199
2d83f93c3580 * Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents: 20633
diff changeset
    36
58198
099ca49b5231 generalized
haftmann
parents: 58195
diff changeset
    37
class semiring_0 = semiring + comm_monoid_add + mult_zero
099ca49b5231 generalized
haftmann
parents: 58195
diff changeset
    38
29904
856f16a3b436 add class cancel_comm_monoid_add
huffman
parents: 29833
diff changeset
    39
class semiring_0_cancel = semiring + cancel_comm_monoid_add
25186
f4d1ebffd025 localized further
haftmann
parents: 25152
diff changeset
    40
begin
14504
7a3d80e276d4 new type class abelian_group
paulson
parents: 14475
diff changeset
    41
25186
f4d1ebffd025 localized further
haftmann
parents: 25152
diff changeset
    42
subclass semiring_0
28823
dcbef866c9e2 tuned unfold_locales invocation
haftmann
parents: 28559
diff changeset
    43
proof
21199
2d83f93c3580 * Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents: 20633
diff changeset
    44
  fix a :: 'a
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
    45
  have "0 * a + 0 * a = 0 * a + 0"
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
    46
    by (simp add: distrib_right [symmetric])
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
    47
  then show "0 * a = 0"
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
    48
    by (simp only: add_left_cancel)
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
    49
  have "a * 0 + a * 0 = a * 0 + 0"
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
    50
    by (simp add: distrib_left [symmetric])
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
    51
  then show "a * 0 = 0"
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
    52
    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
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
    64
  show "(a + b) * c = a * c + b * c"
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
    65
    by (simp add: distrib)
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
    66
  have "a * (b + c) = (b + c) * a"
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
    67
    by (simp add: ac_simps)
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
    68
  also have "\<dots> = b * a + c * a"
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
    69
    by (simp only: distrib)
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
    70
  also have "\<dots> = a * b + a * c"
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
    71
    by (simp add: ac_simps)
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
    72
  finally show "a * (b + c) = a * b + a * c"
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
    73
    by blast
14504
7a3d80e276d4 new type class abelian_group
paulson
parents: 14475
diff changeset
    74
qed
7a3d80e276d4 new type class abelian_group
paulson
parents: 14475
diff changeset
    75
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
    76
end
14504
7a3d80e276d4 new type class abelian_group
paulson
parents: 14475
diff changeset
    77
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
    78
class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
    79
begin
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
    80
27516
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
    81
subclass semiring_0 ..
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
    82
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
    83
end
14504
7a3d80e276d4 new type class abelian_group
paulson
parents: 14475
diff changeset
    84
29904
856f16a3b436 add class cancel_comm_monoid_add
huffman
parents: 29833
diff changeset
    85
class comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_add
25186
f4d1ebffd025 localized further
haftmann
parents: 25152
diff changeset
    86
begin
14940
b9ab8babd8b3 Further development of matrix theory
obua
parents: 14770
diff changeset
    87
27516
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
    88
subclass semiring_0_cancel ..
14940
b9ab8babd8b3 Further development of matrix theory
obua
parents: 14770
diff changeset
    89
28141
193c3ea0f63b instances comm_semiring_0_cancel < comm_semiring_0, comm_ring < comm_semiring_0_cancel
huffman
parents: 27651
diff changeset
    90
subclass comm_semiring_0 ..
193c3ea0f63b instances comm_semiring_0_cancel < comm_semiring_0, comm_ring < comm_semiring_0_cancel
huffman
parents: 27651
diff changeset
    91
25186
f4d1ebffd025 localized further
haftmann
parents: 25152
diff changeset
    92
end
21199
2d83f93c3580 * Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents: 20633
diff changeset
    93
22390
378f34b1e380 now using "class"
haftmann
parents: 21328
diff changeset
    94
class zero_neq_one = zero + one +
25062
af5ef0d4d655 global class syntax
haftmann
parents: 24748
diff changeset
    95
  assumes zero_neq_one [simp]: "0 \<noteq> 1"
26193
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
    96
begin
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
    97
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
    98
lemma one_neq_zero [simp]: "1 \<noteq> 0"
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
    99
  by (rule not_sym) (rule zero_neq_one)
26193
37a7eb7fd5f7 continued localization
haftmann
parents: 25917
diff changeset
   100
54225
8a49a5a30284 generalized of_bool conversion
haftmann
parents: 54147
diff changeset
   101
definition of_bool :: "bool \<Rightarrow> 'a"
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   102
  where "of_bool p = (if p then 1 else 0)"
54225
8a49a5a30284 generalized of_bool conversion
haftmann
parents: 54147
diff changeset
   103
8a49a5a30284 generalized of_bool conversion
haftmann
parents: 54147
diff changeset
   104
lemma of_bool_eq [simp, code]:
8a49a5a30284 generalized of_bool conversion
haftmann
parents: 54147
diff changeset
   105
  "of_bool False = 0"
8a49a5a30284 generalized of_bool conversion
haftmann
parents: 54147
diff changeset
   106
  "of_bool True = 1"
8a49a5a30284 generalized of_bool conversion
haftmann
parents: 54147
diff changeset
   107
  by (simp_all add: of_bool_def)
8a49a5a30284 generalized of_bool conversion
haftmann
parents: 54147
diff changeset
   108
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   109
lemma of_bool_eq_iff: "of_bool p = of_bool q \<longleftrightarrow> p = q"
54225
8a49a5a30284 generalized of_bool conversion
haftmann
parents: 54147
diff changeset
   110
  by (simp add: of_bool_def)
8a49a5a30284 generalized of_bool conversion
haftmann
parents: 54147
diff changeset
   111
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   112
lemma split_of_bool [split]: "P (of_bool p) \<longleftrightarrow> (p \<longrightarrow> P 1) \<and> (\<not> p \<longrightarrow> P 0)"
55187
6d0d93316daf split rules for of_bool, similar to if
haftmann
parents: 54703
diff changeset
   113
  by (cases p) simp_all
6d0d93316daf split rules for of_bool, similar to if
haftmann
parents: 54703
diff changeset
   114
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   115
lemma split_of_bool_asm: "P (of_bool p) \<longleftrightarrow> \<not> (p \<and> \<not> P 1 \<or> \<not> p \<and> \<not> P 0)"
55187
6d0d93316daf split rules for of_bool, similar to if
haftmann
parents: 54703
diff changeset
   116
  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
   117
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
   118
end
14265
95b42e69436c HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff changeset
   119
22390
378f34b1e380 now using "class"
haftmann
parents: 21328
diff changeset
   120
class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
66816
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66810
diff changeset
   121
begin
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66810
diff changeset
   122
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66810
diff changeset
   123
lemma (in semiring_1) of_bool_conj:
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66810
diff changeset
   124
  "of_bool (P \<and> Q) = of_bool P * of_bool Q"
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66810
diff changeset
   125
  by auto
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66810
diff changeset
   126
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66810
diff changeset
   127
end
14504
7a3d80e276d4 new type class abelian_group
paulson
parents: 14475
diff changeset
   128
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   129
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
   130
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   131
class dvd = times
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   132
begin
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   133
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   134
definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "dvd" 50)
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   135
  where "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
   136
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   137
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
   138
  unfolding dvd_def ..
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   139
68251
54a127873735 consider dvdE for automated classical proving
haftmann
parents: 67689
diff changeset
   140
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
   141
  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
   142
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   143
end
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   144
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   145
context comm_monoid_mult
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   146
begin
14738
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents: 14603
diff changeset
   147
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   148
subclass dvd .
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   149
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   150
lemma dvd_refl [simp]: "a dvd a"
28559
55c003a5600a tuned default rules of (dvd)
haftmann
parents: 28141
diff changeset
   151
proof
55c003a5600a tuned default rules of (dvd)
haftmann
parents: 28141
diff changeset
   152
  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
   153
qed
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   154
62349
7c23469b5118 cleansed junk-producing interpretations for gcd/lcm on nat altogether
haftmann
parents: 62347
diff changeset
   155
lemma dvd_trans [trans]:
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   156
  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
   157
  shows "a dvd c"
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   158
proof -
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   159
  from assms obtain v where "b = a * v"
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   160
    by (auto elim!: dvdE)
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   161
  moreover from assms obtain w where "c = b * w"
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   162
    by (auto elim!: dvdE)
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   163
  ultimately have "c = a * (v * w)"
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   164
    by (simp add: mult.assoc)
28559
55c003a5600a tuned default rules of (dvd)
haftmann
parents: 28141
diff changeset
   165
  then show ?thesis ..
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   166
qed
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   167
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   168
lemma subset_divisors_dvd: "{c. c dvd a} \<subseteq> {c. c dvd b} \<longleftrightarrow> a dvd b"
62366
95c6cf433c91 more theorems
haftmann
parents: 62349
diff changeset
   169
  by (auto simp add: subset_iff intro: dvd_trans)
95c6cf433c91 more theorems
haftmann
parents: 62349
diff changeset
   170
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   171
lemma strict_subset_divisors_dvd: "{c. c dvd a} \<subset> {c. c dvd b} \<longleftrightarrow> a dvd b \<and> \<not> b dvd a"
62366
95c6cf433c91 more theorems
haftmann
parents: 62349
diff changeset
   172
  by (auto simp add: subset_iff intro: dvd_trans)
95c6cf433c91 more theorems
haftmann
parents: 62349
diff changeset
   173
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   174
lemma one_dvd [simp]: "1 dvd a"
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   175
  by (auto intro!: dvdI)
28559
55c003a5600a tuned default rules of (dvd)
haftmann
parents: 28141
diff changeset
   176
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   177
lemma dvd_mult [simp]: "a dvd c \<Longrightarrow> a dvd (b * c)"
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   178
  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
   179
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   180
lemma dvd_mult2 [simp]: "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
   181
  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
   182
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   183
lemma dvd_triv_right [simp]: "a dvd b * a"
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   184
  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
   185
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   186
lemma dvd_triv_left [simp]: "a dvd a * b"
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   187
  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
   188
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   189
lemma mult_dvd_mono:
30042
31039ee583fa Removed subsumed lemmas
nipkow
parents: 29981
diff changeset
   190
  assumes "a dvd b"
31039ee583fa Removed subsumed lemmas
nipkow
parents: 29981
diff changeset
   191
    and "c dvd d"
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   192
  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
   193
proof -
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   194
  from \<open>a dvd b\<close> obtain b' where "b = a * b'" ..
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   195
  moreover from \<open>c dvd d\<close> obtain d' where "d = c * d'" ..
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   196
  ultimately have "b * d = (a * c) * (b' * d')"
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   197
    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
   198
  then show ?thesis ..
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   199
qed
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   200
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   201
lemma dvd_mult_left: "a * b dvd c \<Longrightarrow> a dvd c"
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   202
  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
   203
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   204
lemma dvd_mult_right: "a * b dvd c \<Longrightarrow> b dvd c"
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   205
  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
   206
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   207
end
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   208
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   209
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
   210
begin
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   211
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   212
subclass semiring_1 ..
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27516
diff changeset
   213
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   214
lemma dvd_0_left_iff [simp]: "0 dvd a \<longleftrightarrow> a = 0"
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   215
  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
   216
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   217
lemma dvd_0_right [iff]: "a dvd 0"
59009
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
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   222
lemma dvd_0_left: "0 dvd a \<Longrightarrow> a = 0"
59009
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   223
  by simp
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   224
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   225
lemma dvd_add [simp]:
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   226
  assumes "a dvd b" and "a dvd c"
348561aa3869 generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents: 59000
diff changeset
   227
  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
   228
proof -
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   229
  from \<open>a dvd b\<close> obtain b' where "b = a * b'" ..
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   230
  moreover from \<open>a dvd c\<close> obtain c' where "c = a * c'" ..
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   231
  ultimately have "b + c = a * (b' + c')"
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   232
    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
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   248
class comm_semiring_1_cancel =
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   249
  comm_semiring + cancel_comm_monoid_add + zero_neq_one + comm_monoid_mult +
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
   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
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   257
lemma left_diff_distrib' [algebra_simps]: "(b - c) * a = b * a - c * a"
59816
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   258
  by (simp add: algebra_simps)
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   259
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   260
lemma dvd_add_times_triv_left_iff [simp]: "a dvd c * a + b \<longleftrightarrow> a dvd b"
59816
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   261
proof -
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   262
  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
   263
  proof
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   264
    assume ?Q
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   265
    then show ?P by simp
59816
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   266
  next
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   267
    assume ?P
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   268
    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
   269
    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
   270
    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
   271
    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
   272
    then show ?Q ..
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   273
  qed
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   274
  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
   275
qed
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   276
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   277
lemma dvd_add_times_triv_right_iff [simp]: "a dvd b + c * a \<longleftrightarrow> a dvd b"
59816
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   278
  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
   279
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   280
lemma dvd_add_triv_left_iff [simp]: "a dvd a + b \<longleftrightarrow> a dvd b"
59816
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   281
  using dvd_add_times_triv_left_iff [of a 1 b] by simp
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   282
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   283
lemma dvd_add_triv_right_iff [simp]: "a dvd b + a \<longleftrightarrow> a dvd b"
59816
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   284
  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
   285
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   286
lemma dvd_add_right_iff:
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   287
  assumes "a dvd b"
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   288
  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
   289
proof
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   290
  assume ?P
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   291
  then obtain d where "b + c = a * d" ..
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   292
  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
   293
  ultimately have "a * e + c = a * d" by simp
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   294
  then have "a * e + c - a * e = a * d - a * e" by simp
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   295
  then have "c = a * d - a * e" by simp
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   296
  then have "c = a * (d - e)" by (simp add: algebra_simps)
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   297
  then show ?Q ..
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   298
next
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   299
  assume ?Q
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   300
  with assms show ?P by simp
59816
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   301
qed
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   302
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   303
lemma dvd_add_left_iff: "a dvd c \<Longrightarrow> a dvd b + c \<longleftrightarrow> a dvd b"
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   304
  using dvd_add_right_iff [of a c b] by (simp add: ac_simps)
59816
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   305
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   306
end
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   307
22390
378f34b1e380 now using "class"
haftmann
parents: 21328
diff changeset
   308
class ring = semiring + ab_group_add
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   309
begin
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   310
27516
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
   311
subclass semiring_0_cancel ..
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   312
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   313
text \<open>Distribution rules\<close>
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   314
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   315
lemma minus_mult_left: "- (a * b) = - a * b"
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   316
  by (rule minus_unique) (simp add: distrib_right [symmetric])
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   317
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   318
lemma minus_mult_right: "- (a * b) = a * - b"
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   319
  by (rule minus_unique) (simp add: distrib_left [symmetric])
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   320
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   321
text \<open>Extract signs from products\<close>
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 52435
diff changeset
   322
lemmas mult_minus_left [simp] = minus_mult_left [symmetric]
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 52435
diff changeset
   323
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
   324
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   325
lemma minus_mult_minus [simp]: "- a * - b = a * b"
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   326
  by simp
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   327
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   328
lemma minus_mult_commute: "- a * b = a * - b"
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   329
  by simp
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
   330
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   331
lemma right_diff_distrib [algebra_simps]: "a * (b - c) = a * b - a * c"
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 54225
diff changeset
   332
  using distrib_left [of a b "-c "] by simp
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29465
diff changeset
   333
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   334
lemma left_diff_distrib [algebra_simps]: "(a - b) * c = a * c - b * c"
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 54225
diff changeset
   335
  using distrib_right [of a "- b" c] by simp
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   336
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   337
lemmas ring_distribs = distrib_left distrib_right left_diff_distrib right_diff_distrib
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   338
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   339
lemma eq_add_iff1: "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   340
  by (simp add: algebra_simps)
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   341
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   342
lemma eq_add_iff2: "a * e + c = b * e + d \<longleftrightarrow> c = (b - a) * e + d"
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   343
  by (simp add: algebra_simps)
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   344
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   345
end
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   346
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   347
lemmas ring_distribs = distrib_left distrib_right left_diff_distrib right_diff_distrib
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   348
22390
378f34b1e380 now using "class"
haftmann
parents: 21328
diff changeset
   349
class comm_ring = comm_semiring + ab_group_add
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   350
begin
14738
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents: 14603
diff changeset
   351
27516
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
   352
subclass ring ..
28141
193c3ea0f63b instances comm_semiring_0_cancel < comm_semiring_0, comm_ring < comm_semiring_0_cancel
huffman
parents: 27651
diff changeset
   353
subclass comm_semiring_0_cancel ..
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   354
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   355
lemma square_diff_square_factored: "x * x - y * y = (x + y) * (x - y)"
44350
63cddfbc5a09 replace lemma realpow_two_diff with new lemma square_diff_square_factored
huffman
parents: 44346
diff changeset
   356
  by (simp add: algebra_simps)
63cddfbc5a09 replace lemma realpow_two_diff with new lemma square_diff_square_factored
huffman
parents: 44346
diff changeset
   357
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   358
end
14738
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents: 14603
diff changeset
   359
22390
378f34b1e380 now using "class"
haftmann
parents: 21328
diff changeset
   360
class ring_1 = ring + zero_neq_one + monoid_mult
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   361
begin
14265
95b42e69436c HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff changeset
   362
27516
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
   363
subclass semiring_1_cancel ..
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   364
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   365
lemma square_diff_one_factored: "x * x - 1 = (x + 1) * (x - 1)"
44346
00dd3c4dabe0 rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy
huffman
parents: 44064
diff changeset
   366
  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
   367
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   368
end
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   369
22390
378f34b1e380 now using "class"
haftmann
parents: 21328
diff changeset
   370
class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   371
begin
14738
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents: 14603
diff changeset
   372
27516
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
   373
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
   374
subclass comm_semiring_1_cancel
59816
034b13f4efae distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents: 59557
diff changeset
   375
  by unfold_locales (simp add: algebra_simps)
58647
fce800afeec7 more facts about abstract divisibility
haftmann
parents: 58198
diff changeset
   376
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
   377
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
   378
proof
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   379
  assume "x dvd - y"
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   380
  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
   381
  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
   382
next
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   383
  assume "x dvd y"
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   384
  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
   385
  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
   386
qed
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   387
29465
b2cfb5d0a59e change dvd_minus_iff, minus_dvd_iff from [iff] to [simp] (due to problems with Library/Primes.thy)
huffman
parents: 29461
diff changeset
   388
lemma 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
   389
proof
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   390
  assume "- x dvd y"
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   391
  then 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
   392
  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
   393
  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
   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 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
   397
  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
   398
  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
   399
qed
6d10cf26b5dc add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents: 29407
diff changeset
   400
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   401
lemma dvd_diff [simp]: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 54225
diff changeset
   402
  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
   403
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   404
end
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   405
59833
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   406
class semiring_no_zero_divisors = semiring_0 +
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   407
  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
   408
begin
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   409
59833
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   410
lemma divisors_zero:
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   411
  assumes "a * b = 0"
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   412
  shows "a = 0 \<or> b = 0"
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   413
proof (rule classical)
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   414
  assume "\<not> ?thesis"
59833
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   415
  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
   416
  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
   417
  with assms show ?thesis by simp
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   418
qed
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   419
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   420
lemma mult_eq_0_iff [simp]: "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   421
proof (cases "a = 0 \<or> b = 0")
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   422
  case False
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   423
  then have "a \<noteq> 0" and "b \<noteq> 0" by auto
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   424
    then show ?thesis using no_zero_divisors by simp
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   425
next
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   426
  case True
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   427
  then show ?thesis by auto
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   428
qed
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   429
58952
5d82cdef6c1b equivalence rules for structures without zero divisors
haftmann
parents: 58889
diff changeset
   430
end
5d82cdef6c1b equivalence rules for structures without zero divisors
haftmann
parents: 58889
diff changeset
   431
62481
b5d8e57826df tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents: 62390
diff changeset
   432
class semiring_1_no_zero_divisors = semiring_1 + semiring_no_zero_divisors
b5d8e57826df tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents: 62390
diff changeset
   433
60516
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   434
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
   435
  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
   436
    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
   437
begin
5d82cdef6c1b equivalence rules for structures without zero divisors
haftmann
parents: 58889
diff changeset
   438
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   439
lemma mult_left_cancel: "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
   440
  by simp
56217
dc429a5b13c4 Some rationalisation of basic lemmas
paulson <lp15@cam.ac.uk>
parents: 55912
diff changeset
   441
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   442
lemma mult_right_cancel: "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
   443
  by simp
56217
dc429a5b13c4 Some rationalisation of basic lemmas
paulson <lp15@cam.ac.uk>
parents: 55912
diff changeset
   444
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   445
end
22990
775e9de3db48 added classes ring_no_zero_divisors and dom (non-commutative version of idom);
huffman
parents: 22987
diff changeset
   446
60516
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   447
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
   448
begin
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   449
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   450
subclass semiring_no_zero_divisors_cancel
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   451
proof
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   452
  fix a b c
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   453
  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
   454
    by (simp add: algebra_simps)
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   455
  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
   456
    by auto
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   457
  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
   458
  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
   459
    by (simp add: algebra_simps)
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   460
  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
   461
    by auto
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   462
  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
   463
qed
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   464
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   465
end
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   466
23544
4b4165cb3e0d rename class dom to ring_1_no_zero_divisors
huffman
parents: 23527
diff changeset
   467
class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
26274
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   468
begin
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   469
62481
b5d8e57826df tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents: 62390
diff changeset
   470
subclass semiring_1_no_zero_divisors ..
b5d8e57826df tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents: 62390
diff changeset
   471
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   472
lemma square_eq_1_iff: "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"
36821
9207505d1ee5 move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents: 36719
diff changeset
   473
proof -
9207505d1ee5 move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents: 36719
diff changeset
   474
  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
   475
    by (simp add: algebra_simps)
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   476
  then have "x * x = 1 \<longleftrightarrow> (x - 1) * (x + 1) = 0"
36821
9207505d1ee5 move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents: 36719
diff changeset
   477
    by simp
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   478
  then show ?thesis
36821
9207505d1ee5 move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents: 36719
diff changeset
   479
    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
   480
qed
9207505d1ee5 move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents: 36719
diff changeset
   481
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   482
lemma mult_cancel_right1 [simp]: "c = b * c \<longleftrightarrow> c = 0 \<or> b = 1"
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   483
  using mult_cancel_right [of 1 c b] by auto
26274
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   484
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   485
lemma mult_cancel_right2 [simp]: "a * c = c \<longleftrightarrow> c = 0 \<or> a = 1"
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   486
  using mult_cancel_right [of a c 1] 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
   487
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   488
lemma mult_cancel_left1 [simp]: "c = c * b \<longleftrightarrow> c = 0 \<or> b = 1"
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   489
  using mult_cancel_left [of c 1 b] by force
26274
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   490
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   491
lemma mult_cancel_left2 [simp]: "c * a = c \<longleftrightarrow> c = 0 \<or> a = 1"
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   492
  using mult_cancel_left [of c a 1] by simp
26274
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   493
2bdb61a28971 continued localization
haftmann
parents: 26234
diff changeset
   494
end
22990
775e9de3db48 added classes ring_no_zero_divisors and dom (non-commutative version of idom);
huffman
parents: 22987
diff changeset
   495
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
   496
class semidom = comm_semiring_1_cancel + semiring_no_zero_divisors
62481
b5d8e57826df tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents: 62390
diff changeset
   497
begin
b5d8e57826df tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents: 62390
diff changeset
   498
b5d8e57826df tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents: 62390
diff changeset
   499
subclass semiring_1_no_zero_divisors ..
b5d8e57826df tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents: 62390
diff changeset
   500
b5d8e57826df tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents: 62390
diff changeset
   501
end
59833
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   502
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   503
class idom = comm_ring_1 + semiring_no_zero_divisors
25186
f4d1ebffd025 localized further
haftmann
parents: 25152
diff changeset
   504
begin
14421
ee97b6463cb4 new Ring_and_Field hierarchy, eliminating redundant axioms
paulson
parents: 14398
diff changeset
   505
59833
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   506
subclass semidom ..
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   507
27516
9a5d4a8d4aac by intro_locales -> ..
huffman
parents: 26274
diff changeset
   508
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
   509
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   510
lemma dvd_mult_cancel_right [simp]: "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"
29981
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   511
proof -
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   512
  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
   513
    unfolding dvd_def by (simp add: ac_simps)
29981
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   514
  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
   515
    unfolding dvd_def by simp
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   516
  finally show ?thesis .
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   517
qed
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   518
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   519
lemma dvd_mult_cancel_left [simp]: "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b"
29981
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   520
proof -
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   521
  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
   522
    unfolding dvd_def by (simp add: ac_simps)
29981
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   523
  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
   524
    unfolding dvd_def by simp
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   525
  finally show ?thesis .
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   526
qed
7d0ed261b712 generalize int_dvd_cancel_factor simproc to idom class
huffman
parents: 29949
diff changeset
   527
60516
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   528
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
   529
proof
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   530
  assume "a * a = b * b"
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   531
  then have "(a - b) * (a + b) = 0"
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   532
    by (simp add: algebra_simps)
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   533
  then show "a = b \<or> a = - b"
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   534
    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
   535
next
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   536
  assume "a = b \<or> a = - b"
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   537
  then show "a * a = b * b" by auto
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   538
qed
ab828c2c5d67 clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents: 59832
diff changeset
   539
25186
f4d1ebffd025 localized further
haftmann
parents: 25152
diff changeset
   540
end
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
   541
64290
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   542
class idom_abs_sgn = idom + abs + sgn +
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   543
  assumes sgn_mult_abs: "sgn a * \<bar>a\<bar> = a"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   544
    and sgn_sgn [simp]: "sgn (sgn a) = sgn a"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   545
    and abs_abs [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   546
    and abs_0 [simp]: "\<bar>0\<bar> = 0"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   547
    and sgn_0 [simp]: "sgn 0 = 0"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   548
    and sgn_1 [simp]: "sgn 1 = 1"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   549
    and sgn_minus_1: "sgn (- 1) = - 1"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   550
    and sgn_mult: "sgn (a * b) = sgn a * sgn b"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   551
begin
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   552
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   553
lemma sgn_eq_0_iff:
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   554
  "sgn a = 0 \<longleftrightarrow> a = 0"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   555
proof -
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   556
  { assume "sgn a = 0"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   557
    then have "sgn a * \<bar>a\<bar> = 0"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   558
      by simp
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   559
    then have "a = 0"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   560
      by (simp add: sgn_mult_abs)
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   561
  } then show ?thesis
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   562
    by auto
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   563
qed
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   564
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   565
lemma abs_eq_0_iff:
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   566
  "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   567
proof -
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   568
  { assume "\<bar>a\<bar> = 0"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   569
    then have "sgn a * \<bar>a\<bar> = 0"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   570
      by simp
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   571
    then have "a = 0"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   572
      by (simp add: sgn_mult_abs)
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   573
  } then show ?thesis
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   574
    by auto
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   575
qed
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   576
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   577
lemma abs_mult_sgn:
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   578
  "\<bar>a\<bar> * sgn a = a"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   579
  using sgn_mult_abs [of a] by (simp add: ac_simps)
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   580
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   581
lemma abs_1 [simp]:
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   582
  "\<bar>1\<bar> = 1"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   583
  using sgn_mult_abs [of 1] by simp
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   584
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   585
lemma sgn_abs [simp]:
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   586
  "\<bar>sgn a\<bar> = of_bool (a \<noteq> 0)"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   587
  using sgn_mult_abs [of "sgn a"] mult_cancel_left [of "sgn a" "\<bar>sgn a\<bar>" 1]
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   588
  by (auto simp add: sgn_eq_0_iff)
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   589
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   590
lemma abs_sgn [simp]:
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   591
  "sgn \<bar>a\<bar> = of_bool (a \<noteq> 0)"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   592
  using sgn_mult_abs [of "\<bar>a\<bar>"] mult_cancel_right [of "sgn \<bar>a\<bar>" "\<bar>a\<bar>" 1]
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   593
  by (auto simp add: abs_eq_0_iff)
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   594
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   595
lemma abs_mult:
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   596
  "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   597
proof (cases "a = 0 \<or> b = 0")
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   598
  case True
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   599
  then show ?thesis
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   600
    by auto
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   601
next
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   602
  case False
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   603
  then have *: "sgn (a * b) \<noteq> 0"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   604
    by (simp add: sgn_eq_0_iff)
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   605
  from abs_mult_sgn [of "a * b"] abs_mult_sgn [of a] abs_mult_sgn [of b]
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   606
  have "\<bar>a * b\<bar> * sgn (a * b) = \<bar>a\<bar> * sgn a * \<bar>b\<bar> * sgn b"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   607
    by (simp add: ac_simps)
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   608
  then have "\<bar>a * b\<bar> * sgn (a * b) = \<bar>a\<bar> * \<bar>b\<bar> * sgn (a * b)"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   609
    by (simp add: sgn_mult ac_simps)
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   610
  with * show ?thesis
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   611
    by simp
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   612
qed
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   613
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   614
lemma sgn_minus [simp]:
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   615
  "sgn (- a) = - sgn a"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   616
proof -
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   617
  from sgn_minus_1 have "sgn (- 1 * a) = - 1 * sgn a"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   618
    by (simp only: sgn_mult)
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   619
  then show ?thesis
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   620
    by simp
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   621
qed
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   622
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   623
lemma abs_minus [simp]:
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   624
  "\<bar>- a\<bar> = \<bar>a\<bar>"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   625
proof -
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   626
  have [simp]: "\<bar>- 1\<bar> = 1"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   627
    using sgn_mult_abs [of "- 1"] by simp
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   628
  then have "\<bar>- 1 * a\<bar> = 1 * \<bar>a\<bar>"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   629
    by (simp only: abs_mult)
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   630
  then show ?thesis
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   631
    by simp
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   632
qed
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   633
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   634
end
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 64242
diff changeset
   635
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   636
text \<open>
35302
4bc6b4d70e08 tuned text
haftmann
parents: 35216
diff changeset
   637
  The theory of partially ordered rings is taken from the books:
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   638
    \<^item> \<^emph>\<open>Lattice Theory\<close> by Garret Birkhoff, American Mathematical Society, 1979
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   639
    \<^item> \<^emph>\<open>Partially Ordered Algebraic Systems\<close>, Pergamon Press, 1963
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   640
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
   641
  Most of the used notions can also be looked up in
63680
6e1e8b5abbfa more symbols;
wenzelm
parents: 63588
diff changeset
   642
    \<^item> \<^url>\<open>http://www.mathworld.com\<close> by Eric Weisstein et. al.
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   643
    \<^item> \<^emph>\<open>Algebra I\<close> by van der Waerden, Springer
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   644
\<close>
35302
4bc6b4d70e08 tuned text
haftmann
parents: 35216
diff changeset
   645
63950
cdc1e59aa513 syntactic type class for operation mod named after mod;
haftmann
parents: 63947
diff changeset
   646
text \<open>Syntactic division operator\<close>
cdc1e59aa513 syntactic type class for operation mod named after mod;
haftmann
parents: 63947
diff changeset
   647
60353
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   648
class divide =
60429
d3d1e185cd63 uniform _ div _ as infix syntax for ring division
haftmann
parents: 60353
diff changeset
   649
  fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "div" 70)
60353
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   650
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   651
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
   652
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   653
context semiring
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   654
begin
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   655
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   656
lemma [field_simps]:
60429
d3d1e185cd63 uniform _ div _ as infix syntax for ring division
haftmann
parents: 60353
diff changeset
   657
  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
   658
    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
   659
  by (rule distrib_left distrib_right)+
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   660
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   661
end
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   662
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   663
context ring
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   664
begin
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   665
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   666
lemma [field_simps]:
60429
d3d1e185cd63 uniform _ div _ as infix syntax for ring division
haftmann
parents: 60353
diff changeset
   667
  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
   668
    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
   669
  by (rule left_diff_distrib right_diff_distrib)+
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   670
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   671
end
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   672
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   673
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
   674
63950
cdc1e59aa513 syntactic type class for operation mod named after mod;
haftmann
parents: 63947
diff changeset
   675
text \<open>Algebraic classes with division\<close>
cdc1e59aa513 syntactic type class for operation mod named after mod;
haftmann
parents: 63947
diff changeset
   676
  
60353
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   677
class semidom_divide = semidom + divide +
64240
eabf80376aab more standardized names
haftmann
parents: 64239
diff changeset
   678
  assumes nonzero_mult_div_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> (a * b) div b = a"
eabf80376aab more standardized names
haftmann
parents: 64239
diff changeset
   679
  assumes div_by_0 [simp]: "a div 0 = 0"
60353
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   680
begin
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   681
64240
eabf80376aab more standardized names
haftmann
parents: 64239
diff changeset
   682
lemma nonzero_mult_div_cancel_left [simp]: "a \<noteq> 0 \<Longrightarrow> (a * b) div a = b"
eabf80376aab more standardized names
haftmann
parents: 64239
diff changeset
   683
  using nonzero_mult_div_cancel_right [of a b] by (simp add: ac_simps)
60353
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   684
60516
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   685
subclass semiring_no_zero_divisors_cancel
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   686
proof
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   687
  show *: "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b" for a b c
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   688
  proof (cases "c = 0")
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   689
    case True
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   690
    then show ?thesis by simp
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   691
  next
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   692
    case False
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   693
    have "a = b" if "a * c = b * c"
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   694
    proof -
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   695
      from that have "a * c div c = b * c div c"
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   696
        by simp
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   697
      with False show ?thesis
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   698
        by simp
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   699
    qed
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   700
    then show ?thesis by auto
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   701
  qed
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   702
  show "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b" for a b c
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   703
    using * [of a c b] by (simp add: ac_simps)
60516
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   704
qed
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   705
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   706
lemma div_self [simp]: "a \<noteq> 0 \<Longrightarrow> a div a = 1"
64240
eabf80376aab more standardized names
haftmann
parents: 64239
diff changeset
   707
  using nonzero_mult_div_cancel_left [of a 1] by simp
60516
0826b7025d07 generalized some theorems about integral domains and moved to HOL theories
haftmann
parents: 60429
diff changeset
   708
64240
eabf80376aab more standardized names
haftmann
parents: 64239
diff changeset
   709
lemma div_0 [simp]: "0 div a = 0"
60570
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   710
proof (cases "a = 0")
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   711
  case True
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   712
  then show ?thesis by simp
60570
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   713
next
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   714
  case False
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   715
  then have "a * 0 div a = 0"
64240
eabf80376aab more standardized names
haftmann
parents: 64239
diff changeset
   716
    by (rule nonzero_mult_div_cancel_left)
60570
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   717
  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
   718
qed
60570
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   719
64240
eabf80376aab more standardized names
haftmann
parents: 64239
diff changeset
   720
lemma div_by_1 [simp]: "a div 1 = a"
eabf80376aab more standardized names
haftmann
parents: 64239
diff changeset
   721
  using nonzero_mult_div_cancel_left [of 1 a] by simp
60690
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   722
64591
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
   723
lemma dvd_div_eq_0_iff:
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
   724
  assumes "b dvd a"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
   725
  shows "a div b = 0 \<longleftrightarrow> a = 0"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
   726
  using assms by (elim dvdE, cases "b = 0") simp_all  
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
   727
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
   728
lemma dvd_div_eq_cancel:
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
   729
  "a div c = b div c \<Longrightarrow> c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> a = b"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
   730
  by (elim dvdE, cases "c = 0") simp_all
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
   731
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
   732
lemma dvd_div_eq_iff:
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
   733
  "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> a div c = b div c \<longleftrightarrow> a = b"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
   734
  by (elim dvdE, cases "c = 0") simp_all
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
   735
60867
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   736
end
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   737
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   738
class idom_divide = idom + semidom_divide
64591
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
   739
begin
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
   740
64592
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   741
lemma dvd_neg_div:
64591
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
   742
  assumes "b dvd a"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
   743
  shows "- a div b = - (a div b)"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
   744
proof (cases "b = 0")
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
   745
  case True
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
   746
  then show ?thesis by simp
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
   747
next
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
   748
  case False
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
   749
  from assms obtain c where "a = b * c" ..
64592
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   750
  then have "- a div b = (b * - c) div b"
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   751
    by simp
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   752
  from False also have "\<dots> = - c"
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   753
    by (rule nonzero_mult_div_cancel_left)  
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   754
  with False \<open>a = b * c\<close> show ?thesis
64591
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
   755
    by simp
64592
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   756
qed
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   757
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   758
lemma dvd_div_neg:
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   759
  assumes "b dvd a"
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   760
  shows "a div - b = - (a div b)"
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   761
proof (cases "b = 0")
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   762
  case True
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   763
  then show ?thesis by simp
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   764
next
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   765
  case False
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   766
  then have "- b \<noteq> 0"
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   767
    by simp
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   768
  from assms obtain c where "a = b * c" ..
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   769
  then have "a div - b = (- b * - c) div - b"
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   770
    by simp
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   771
  from \<open>- b \<noteq> 0\<close> also have "\<dots> = - c"
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   772
    by (rule nonzero_mult_div_cancel_left)  
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   773
  with False \<open>a = b * c\<close> show ?thesis
64591
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
   774
    by simp
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
   775
qed
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
   776
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
   777
end
60867
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   778
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   779
class algebraic_semidom = semidom_divide
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   780
begin
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   781
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   782
text \<open>
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   783
  Class @{class algebraic_semidom} enriches a integral domain
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   784
  by notions from algebra, like units in a ring.
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   785
  It is a separate class to avoid spoiling fields with notions
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   786
  which are degenerated there.
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   787
\<close>
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   788
60690
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   789
lemma dvd_times_left_cancel_iff [simp]:
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   790
  assumes "a \<noteq> 0"
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   791
  shows "a * b dvd a * c \<longleftrightarrow> b dvd c"
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   792
    (is "?lhs \<longleftrightarrow> ?rhs")
60690
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   793
proof
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   794
  assume ?lhs
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   795
  then obtain d where "a * c = a * b * d" ..
60690
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   796
  with assms have "c = b * d" by (simp add: ac_simps)
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   797
  then show ?rhs ..
60690
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   798
next
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   799
  assume ?rhs
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   800
  then obtain d where "c = b * d" ..
60690
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   801
  then have "a * c = a * b * d" by (simp add: ac_simps)
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   802
  then show ?lhs ..
60690
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   803
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
   804
60690
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   805
lemma dvd_times_right_cancel_iff [simp]:
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   806
  assumes "a \<noteq> 0"
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   807
  shows "b * a dvd c * a \<longleftrightarrow> b dvd c"
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   808
  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
   809
60690
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   810
lemma div_dvd_iff_mult:
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   811
  assumes "b \<noteq> 0" and "b dvd a"
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   812
  shows "a div b dvd c \<longleftrightarrow> a dvd c * b"
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   813
proof -
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   814
  from \<open>b dvd a\<close> obtain d where "a = b * d" ..
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   815
  with \<open>b \<noteq> 0\<close> show ?thesis by (simp add: ac_simps)
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   816
qed
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   817
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   818
lemma dvd_div_iff_mult:
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   819
  assumes "c \<noteq> 0" and "c dvd b"
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   820
  shows "a dvd b div c \<longleftrightarrow> a * c dvd b"
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   821
proof -
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   822
  from \<open>c dvd b\<close> obtain d where "b = c * d" ..
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   823
  with \<open>c \<noteq> 0\<close> show ?thesis by (simp add: mult.commute [of a])
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   824
qed
a9e45c9588c3 tuned facts
haftmann
parents: 60688
diff changeset
   825
60867
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   826
lemma div_dvd_div [simp]:
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   827
  assumes "a dvd b" and "a dvd c"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   828
  shows "b div a dvd c div a \<longleftrightarrow> b dvd c"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   829
proof (cases "a = 0")
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   830
  case True
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   831
  with assms show ?thesis by simp
60867
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   832
next
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   833
  case False
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   834
  moreover from assms obtain k l where "b = a * k" and "c = a * l"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   835
    by (auto elim!: dvdE)
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   836
  ultimately show ?thesis by simp
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   837
qed
60353
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   838
60867
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   839
lemma div_add [simp]:
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   840
  assumes "c dvd a" and "c dvd b"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   841
  shows "(a + b) div c = a div c + b div c"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   842
proof (cases "c = 0")
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   843
  case True
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   844
  then show ?thesis by simp
60867
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   845
next
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   846
  case False
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   847
  moreover from assms obtain k l where "a = c * k" and "b = c * l"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   848
    by (auto elim!: dvdE)
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   849
  moreover have "c * k + c * l = c * (k + l)"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   850
    by (simp add: algebra_simps)
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   851
  ultimately show ?thesis
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   852
    by simp
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   853
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
   854
60867
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   855
lemma div_mult_div_if_dvd:
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   856
  assumes "b dvd a" and "d dvd c"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   857
  shows "(a div b) * (c div d) = (a * c) div (b * d)"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   858
proof (cases "b = 0 \<or> c = 0")
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   859
  case True
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   860
  with assms show ?thesis by auto
60867
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   861
next
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   862
  case False
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   863
  moreover from assms obtain k l where "a = b * k" and "c = d * l"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   864
    by (auto elim!: dvdE)
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   865
  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
   866
    by (simp add: ac_simps)
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   867
  ultimately show ?thesis by simp
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   868
qed
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   869
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   870
lemma dvd_div_eq_mult:
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   871
  assumes "a \<noteq> 0" and "a dvd b"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   872
  shows "b div a = c \<longleftrightarrow> b = c * a"
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   873
    (is "?lhs \<longleftrightarrow> ?rhs")
60867
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   874
proof
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   875
  assume ?rhs
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   876
  then show ?lhs by (simp add: assms)
60867
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   877
next
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   878
  assume ?lhs
60867
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   879
  then have "b div a * a = c * a" by simp
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   880
  moreover from assms have "b div a * a = b"
60867
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   881
    by (auto elim!: dvdE simp add: ac_simps)
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   882
  ultimately show ?rhs by simp
60867
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   883
qed
60688
01488b559910 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents: 60685
diff changeset
   884
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   885
lemma dvd_div_mult_self [simp]: "a dvd b \<Longrightarrow> b div a * a = 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
   886
  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
   887
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   888
lemma dvd_mult_div_cancel [simp]: "a dvd b \<Longrightarrow> a * (b div a) = 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
   889
  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
   890
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
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
   892
  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
   893
  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
   894
proof (cases "c = 0")
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   895
  case True
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   896
  then show ?thesis 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
   897
next
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   898
  case False
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   899
  from assms obtain d where "b = c * d" ..
60517
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   900
  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
   901
    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
   902
  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
   903
qed
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   904
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   905
lemma dvd_div_mult: "c dvd b \<Longrightarrow> b div c * a = (b * a) div c"
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   906
  using div_mult_swap [of c b a] by (simp add: ac_simps)
60517
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   907
60570
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   908
lemma dvd_div_mult2_eq:
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   909
  assumes "b * c dvd a"
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   910
  shows "a div (b * c) = a div b div c"
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   911
proof -
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   912
  from assms obtain k where "a = b * c * k" ..
60570
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   913
  then show ?thesis
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   914
    by (cases "b = 0 \<or> c = 0") (auto, simp add: ac_simps)
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   915
qed
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
   916
60867
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   917
lemma dvd_div_div_eq_mult:
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   918
  assumes "a \<noteq> 0" "c \<noteq> 0" and "a dvd b" "c dvd d"
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   919
  shows "b div a = d div c \<longleftrightarrow> b * c = a * d"
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   920
    (is "?lhs \<longleftrightarrow> ?rhs")
60867
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   921
proof -
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   922
  from assms have "a * c \<noteq> 0" by simp
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   923
  then have "?lhs \<longleftrightarrow> b div a * (a * c) = d div c * (a * c)"
60867
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   924
    by simp
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   925
  also have "\<dots> \<longleftrightarrow> (a * (b div a)) * c = (c * (d div c)) * a"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   926
    by (simp add: ac_simps)
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   927
  also have "\<dots> \<longleftrightarrow> (a * b div a) * c = (c * d div c) * a"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   928
    using assms by (simp add: div_mult_swap)
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   929
  also have "\<dots> \<longleftrightarrow> ?rhs"
60867
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   930
    using assms by (simp add: ac_simps)
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   931
  finally show ?thesis .
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   932
qed
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60758
diff changeset
   933
63359
99b51ba8da1c More lemmas on Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents: 63325
diff changeset
   934
lemma dvd_mult_imp_div:
99b51ba8da1c More lemmas on Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents: 63325
diff changeset
   935
  assumes "a * c dvd b"
99b51ba8da1c More lemmas on Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents: 63325
diff changeset
   936
  shows "a dvd b div c"
99b51ba8da1c More lemmas on Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents: 63325
diff changeset
   937
proof (cases "c = 0")
99b51ba8da1c More lemmas on Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents: 63325
diff changeset
   938
  case True then show ?thesis by simp
99b51ba8da1c More lemmas on Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents: 63325
diff changeset
   939
next
99b51ba8da1c More lemmas on Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents: 63325
diff changeset
   940
  case False
99b51ba8da1c More lemmas on Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents: 63325
diff changeset
   941
  from \<open>a * c dvd b\<close> obtain d where "b = a * c * d" ..
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   942
  with False show ?thesis
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
   943
    by (simp add: mult.commute [of a] mult.assoc)
63359
99b51ba8da1c More lemmas on Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents: 63325
diff changeset
   944
qed
99b51ba8da1c More lemmas on Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents: 63325
diff changeset
   945
64592
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   946
lemma div_div_eq_right:
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   947
  assumes "c dvd b" "b dvd a"
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   948
  shows   "a div (b div c) = a div b * c"
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   949
proof (cases "c = 0 \<or> b = 0")
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   950
  case True
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   951
  then show ?thesis
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   952
    by auto
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   953
next
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   954
  case False
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   955
  from assms obtain r s where "b = c * r" and "a = c * r * s"
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   956
    by (blast elim: dvdE)
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   957
  moreover with False have "r \<noteq> 0"
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   958
    by auto
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   959
  ultimately show ?thesis using False
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   960
    by simp (simp add: mult.commute [of _ r] mult.assoc mult.commute [of c])
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   961
qed
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   962
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   963
lemma div_div_div_same:
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   964
  assumes "d dvd b" "b dvd a"
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   965
  shows   "(a div d) div (b div d) = a div b"
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   966
proof (cases "b = 0 \<or> d = 0")
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   967
  case True
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   968
  with assms show ?thesis
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   969
    by auto
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   970
next
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   971
  case False
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   972
  from assms obtain r s
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   973
    where "a = d * r * s" and "b = d * r"
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   974
    by (blast elim: dvdE)
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   975
  with False show ?thesis
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   976
    by simp (simp add: ac_simps)
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   977
qed
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64591
diff changeset
   978
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
   979
60517
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   980
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
   981
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   982
abbreviation is_unit :: "'a \<Rightarrow> bool"
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   983
  where "is_unit a \<equiv> a dvd 1"
60517
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   984
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   985
lemma not_is_unit_0 [simp]: "\<not> is_unit 0"
60517
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   986
  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
   987
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
   988
lemma unit_imp_dvd [dest]: "is_unit b \<Longrightarrow> b dvd a"
60517
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   989
  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
   990
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   991
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
   992
  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
   993
  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
   994
proof -
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
   995
  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
   996
  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
   997
  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
   998
  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
   999
qed
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
  1000
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
  1001
lemma dvd_unit_imp_unit: "a dvd b \<Longrightarrow> is_unit b \<Longrightarrow> is_unit a"
60517
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
  1002
  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
  1003
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
  1004
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
  1005
  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
  1006
  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
  1007
proof -
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
  1008
  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
  1009
  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
  1010
qed
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
  1011
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
  1012
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
  1013
  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
  1014
  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
  1015
    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
  1016
    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
  1017
proof (rule that)
63040
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62626
diff changeset
  1018
  define b where "b = 1 div a"
60517
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
  1019
  then show "1 div a = b" by simp
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
  1020
  from assms b_def show "is_unit b" by simp
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
  1021
  with assms show "a \<noteq> 0" and "b \<noteq> 0" by auto
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
  1022
  from assms b_def 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
  1023
  then have "1 = a * b" ..
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
  1024
  with b_def \<open>b \<noteq> 0\<close> show "1 div b = a" by simp
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
  1025
  from assms 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
  1026
  then obtain d where "c = a * d" ..
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
  1027
  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
  1028
    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
  1029
qed
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
  1030
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
  1031
lemma unit_prod [intro]: "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
  1032
  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
  1033
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
  1034
lemma is_unit_mult_iff: "is_unit (a * b) \<longleftrightarrow> is_unit a \<and> is_unit b"
62366
95c6cf433c91 more theorems
haftmann
parents: 62349
diff changeset
  1035
  by (auto dest: dvd_mult_left dvd_mult_right)
95c6cf433c91 more theorems
haftmann
parents: 62349
diff changeset
  1036
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
  1037
lemma unit_div [intro]: "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div 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
  1038
  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
  1039
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
  1040
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
  1041
  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
  1042
  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
  1043
proof
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
  1044
  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
  1045
  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
  1046
    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
  1047
next
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
  1048
  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
  1049
  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
  1050
  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
  1051
    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
  1052
  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
  1053
qed
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
  1054
63924
f91766530e13 more generic algebraic lemmas
haftmann
parents: 63680
diff changeset
  1055
lemma mult_unit_dvd_iff': "is_unit a \<Longrightarrow> (a * b) dvd c \<longleftrightarrow> b dvd c"
f91766530e13 more generic algebraic lemmas
haftmann
parents: 63680
diff changeset
  1056
  using mult_unit_dvd_iff [of a b c] by (simp add: ac_simps)
f91766530e13 more generic algebraic lemmas
haftmann
parents: 63680
diff changeset
  1057
60517
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
  1058
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
  1059
  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
  1060
  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
  1061
proof
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
  1062
  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
  1063
  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
  1064
    by (subst mult_assoc [symmetric]) simp
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
  1065
  also from assms have "b * (1 div b) = 1"
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
  1066
    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
  1067
  finally have "c * b dvd c" by simp
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
  1068
  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
  1069
next
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
  1070
  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
  1071
  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
  1072
qed
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
  1073
63924
f91766530e13 more generic algebraic lemmas
haftmann
parents: 63680
diff changeset
  1074
lemma dvd_mult_unit_iff': "is_unit b \<Longrightarrow> a dvd b * c \<longleftrightarrow> a dvd c"
f91766530e13 more generic algebraic lemmas
haftmann
parents: 63680
diff changeset
  1075
  using dvd_mult_unit_iff [of b a c] by (simp add: ac_simps)
f91766530e13 more generic algebraic lemmas
haftmann
parents: 63680
diff changeset
  1076
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
  1077
lemma div_unit_dvd_iff: "is_unit b \<Longrightarrow> a div b dvd c \<longleftrightarrow> 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
  1078
  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
  1079
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
  1080
lemma dvd_div_unit_iff: "is_unit b \<Longrightarrow> a dvd c div b \<longleftrightarrow> 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
  1081
  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
  1082
63924
f91766530e13 more generic algebraic lemmas
haftmann
parents: 63680
diff changeset
  1083
lemmas unit_dvd_iff = mult_unit_dvd_iff mult_unit_dvd_iff'
f91766530e13 more generic algebraic lemmas
haftmann
parents: 63680
diff changeset
  1084
  dvd_mult_unit_iff dvd_mult_unit_iff' 
f91766530e13 more generic algebraic lemmas
haftmann
parents: 63680
diff changeset
  1085
  div_unit_dvd_iff dvd_div_unit_iff (* FIXME consider named_theorems *)
60517
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
  1086
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
  1087
lemma unit_mult_div_div [simp]: "is_unit a \<Longrightarrow> b * (1 div a) = b div a"
60517
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
  1088
  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
  1089
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
  1090
lemma unit_div_mult_self [simp]: "is_unit a \<Longrightarrow> b div a * a = 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
  1091
  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
  1092
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
  1093
lemma unit_div_1_div_1 [simp]: "is_unit a \<Longrightarrow> 1 div (1 div a) = a"
60517
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
  1094
  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
  1095
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
  1096
lemma unit_div_mult_swap: "is_unit c \<Longrightarrow> a * (b div c) = (a * b) div 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
  1097
  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
  1098
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
  1099
lemma unit_div_commute: "is_unit b \<Longrightarrow> (a div b) * c = (a * c) div 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
  1100
  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
  1101
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
  1102
lemma unit_eq_div1: "is_unit b \<Longrightarrow> a div b = c \<longleftrightarrow> 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
  1103
  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
  1104
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
  1105
lemma unit_eq_div2: "is_unit b \<Longrightarrow> a = c div b \<longleftrightarrow> a * b = 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
  1106
  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
  1107
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
  1108
lemma unit_mult_left_cancel: "is_unit a \<Longrightarrow> a * b = a * c \<longleftrightarrow> b = c"
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
  1109
  using 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
  1110
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
  1111
lemma unit_mult_right_cancel: "is_unit a \<Longrightarrow> b * a = c * a \<longleftrightarrow> b = 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
  1112
  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
  1113
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
  1114
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
  1115
  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
  1116
  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
  1117
proof -
f16e4fb20652 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents: 60516
diff changeset
  1118
  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
  1119
  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
  1120
    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
  1121
  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
  1122
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
  1123
60570
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
  1124
lemma is_unit_div_mult2_eq:
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
  1125
  assumes "is_unit b" and "is_unit c"
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
  1126
  shows "a div (b * c) = a div b div c"
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
  1127
proof -
63325
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
  1128
  from assms have "is_unit (b * c)"
1086d56cde86 misc tuning and modernization;
wenzelm
parents: 63040
diff changeset
  1129
    by (simp add: unit_prod)
60570
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
  1130
  then have "b * c dvd a"
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
  1131
    by (rule unit_imp_dvd)
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
  1132
  then show ?thesis
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
  1133
    by (rule dvd_div_mult2_eq)
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
  1134
qed
7ed2cde6806d more theorems
haftmann
parents: 60562
diff changeset
  1135
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
  1136
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
  1137
  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
  1138
  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
  1139
  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
  1140
64240
eabf80376aab more standardized names
haftmann
parents: 64239
diff changeset
  1141
lemma is_unit_div_mult_cancel_left:
60685
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1142
  assumes "a \<noteq> 0" and "is_unit b"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1143
  shows "a div (a * b) = 1 div b"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1144
proof -
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1145
  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
  1146
    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
  1147
  with assms show ?thesis by simp
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
64240
eabf80376aab more standardized names
haftmann
parents: 64239
diff changeset
  1150
lemma is_unit_div_mult_cancel_right:
60685
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1151
  assumes "a \<noteq> 0" and "is_unit b"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1152
  shows "a div (b * a) = 1 div b"
64240
eabf80376aab more standardized names
haftmann
parents: 64239
diff changeset
  1153
  using assms is_unit_div_mult_cancel_left [of a b] by (simp add: ac_simps)
60685
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1154
64591
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
  1155
lemma unit_div_eq_0_iff:
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
  1156
  assumes "is_unit b"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
  1157
  shows "a div b = 0 \<longleftrightarrow> a = 0"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
  1158
  by (rule dvd_div_eq_0_iff) (insert assms, auto)  
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
  1159
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
  1160
lemma div_mult_unit2:
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
  1161
  "is_unit c \<Longrightarrow> b dvd a \<Longrightarrow> a div (b * c) = a div b div c"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
  1162
  by (rule dvd_div_mult2_eq) (simp_all add: mult_unit_dvd_iff)
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64290
diff changeset
  1163
67051
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1164
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1165
text \<open>Coprimality\<close>
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1166
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1167
definition coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1168
  where "coprime a b \<longleftrightarrow> (\<forall>c. c dvd a \<longrightarrow> c dvd b \<longrightarrow> is_unit c)"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1169
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1170
lemma coprimeI:
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1171
  assumes "\<And>c. c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> is_unit c"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1172
  shows "coprime a b"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1173
  using assms by (auto simp: coprime_def)
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1174
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1175
lemma not_coprimeI:
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1176
  assumes "c dvd a" and "c dvd b" and "\<not> is_unit c"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1177
  shows "\<not> coprime a b"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1178
  using assms by (auto simp: coprime_def)
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1179
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1180
lemma coprime_common_divisor:
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1181
  "is_unit c" if "coprime a b" and "c dvd a" and "c dvd b"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1182
  using that by (auto simp: coprime_def)
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1183
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1184
lemma not_coprimeE:
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1185
  assumes "\<not> coprime a b"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1186
  obtains c where "c dvd a" and "c dvd b" and "\<not> is_unit c"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1187
  using assms by (auto simp: coprime_def)
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1188
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1189
lemma coprime_imp_coprime:
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1190
  "coprime a b" if "coprime c d"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1191
    and "\<And>e. \<not> is_unit e \<Longrightarrow> e dvd a \<Longrightarrow> e dvd b \<Longrightarrow> e dvd c"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1192
    and "\<And>e. \<not> is_unit e \<Longrightarrow> e dvd a \<Longrightarrow> e dvd b \<Longrightarrow> e dvd d"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1193
proof (rule coprimeI)
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1194
  fix e
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1195
  assume "e dvd a" and "e dvd b"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1196
  with that have "e dvd c" and "e dvd d"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1197
    by (auto intro: dvd_trans)
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1198
  with \<open>coprime c d\<close> show "is_unit e"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1199
    by (rule coprime_common_divisor)
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1200
qed
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1201
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1202
lemma coprime_divisors:
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1203
  "coprime a b" if "a dvd c" "b dvd d" and "coprime c d"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1204
using \<open>coprime c d\<close> proof (rule coprime_imp_coprime)
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1205
  fix e
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1206
  assume "e dvd a" then show "e dvd c"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1207
    using \<open>a dvd c\<close> by (rule dvd_trans)
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1208
  assume "e dvd b" then show "e dvd d"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1209
    using \<open>b dvd d\<close> by (rule dvd_trans)
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1210
qed
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1211
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1212
lemma coprime_self [simp]:
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1213
  "coprime a a \<longleftrightarrow> is_unit a" (is "?P \<longleftrightarrow> ?Q")
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1214
proof
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1215
  assume ?P
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1216
  then show ?Q
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1217
    by (rule coprime_common_divisor) simp_all
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1218
next
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1219
  assume ?Q
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1220
  show ?P
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1221
    by (rule coprimeI) (erule dvd_unit_imp_unit, rule \<open>?Q\<close>)
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1222
qed
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1223
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1224
lemma coprime_commute [ac_simps]:
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1225
  "coprime b a \<longleftrightarrow> coprime a b"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1226
  unfolding coprime_def by auto
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1227
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1228
lemma is_unit_left_imp_coprime:
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1229
  "coprime a b" if "is_unit a"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1230
proof (rule coprimeI)
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1231
  fix c
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1232
  assume "c dvd a"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1233
  with that show "is_unit c"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1234
    by (auto intro: dvd_unit_imp_unit)
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1235
qed
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1236
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1237
lemma is_unit_right_imp_coprime:
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1238
  "coprime a b" if "is_unit b"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1239
  using that is_unit_left_imp_coprime [of b a] by (simp add: ac_simps)
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1240
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1241
lemma coprime_1_left [simp]:
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1242
  "coprime 1 a"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1243
  by (rule coprimeI)
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1244
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1245
lemma coprime_1_right [simp]:
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1246
  "coprime a 1"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1247
  by (rule coprimeI)
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1248
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1249
lemma coprime_0_left_iff [simp]:
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1250
  "coprime 0 a \<longleftrightarrow> is_unit a"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1251
  by (auto intro: coprimeI dvd_unit_imp_unit coprime_common_divisor [of 0 a a])
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1252
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1253
lemma coprime_0_right_iff [simp]:
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1254
  "coprime a 0 \<longleftrightarrow> is_unit a"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1255
  using coprime_0_left_iff [of a] by (simp add: ac_simps)
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1256
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1257
lemma coprime_mult_self_left_iff [simp]:
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1258
  "coprime (c * a) (c * b) \<longleftrightarrow> is_unit c \<and> coprime a b"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1259
  by (auto intro: coprime_common_divisor)
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1260
    (rule coprimeI, auto intro: coprime_common_divisor simp add: dvd_mult_unit_iff')+
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1261
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1262
lemma coprime_mult_self_right_iff [simp]:
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1263
  "coprime (a * c) (b * c) \<longleftrightarrow> is_unit c \<and> coprime a b"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1264
  using coprime_mult_self_left_iff [of c a b] by (simp add: ac_simps)
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 66937
diff changeset
  1265
67234
ab10ea1d6fd0 Some lemmas on complex numbers and coprimality
eberlm <eberlm@in.tum.de>
parents: 67226
diff changeset
  1266
lemma coprime_absorb_left:
ab10ea1d6fd0 Some lemmas on complex numbers and coprimality
eberlm <eberlm@in.tum.de>
parents: 67226
diff changeset
  1267
  assumes "x dvd y"
ab10ea1d6fd0 Some lemmas on complex numbers and coprimality
eberlm <eberlm@in.tum.de>
parents: 67226
diff changeset
  1268
  shows   "coprime x y \<longleftrightarrow> is_unit x"
ab10ea1d6fd0 Some lemmas on complex numbers and coprimality
eberlm <eberlm@in.tum.de>
parents: 67226
diff changeset
  1269
  using assms coprime_common_divisor is_unit_left_imp_coprime by auto
ab10ea1d6fd0 Some lemmas on complex numbers and coprimality
eberlm <eberlm@in.tum.de>
parents: 67226
diff changeset
  1270
ab10ea1d6fd0 Some lemmas on complex numbers and coprimality
eberlm <eberlm@in.tum.de>
parents: 67226
diff changeset
  1271
lemma coprime_absorb_right:
ab10ea1d6fd0 Some lemmas on complex numbers and coprimality
eberlm <eberlm@in.tum.de>
parents: 67226
diff changeset
  1272
  assumes "y dvd x"
ab10ea1d6fd0 Some lemmas on complex numbers and coprimality
eberlm <eberlm@in.tum.de>
parents: 67226
diff changeset
  1273
  shows   "coprime x y \<longleftrightarrow> is_unit y"
ab10ea1d6fd0 Some lemmas on complex numbers and coprimality
eberlm <eberlm@in.tum.de>
parents: 67226
diff changeset
  1274
  using assms coprime_common_divisor is_unit_right_imp_coprime by auto
ab10ea1d6fd0 Some lemmas on complex numbers and coprimality
eberlm <eberlm@in.tum.de>
parents: 67226
diff changeset
  1275
60685
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1276
end
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1277
64848
c50db2128048 slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
haftmann
parents: 64713
diff changeset
  1278
class unit_factor =
c50db2128048 slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
haftmann
parents: 64713
diff changeset
  1279
  fixes unit_factor :: "'a \<Rightarrow> 'a"
c50db2128048 slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
haftmann
parents: 64713
diff changeset
  1280
c50db2128048 slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
haftmann
parents: 64713
diff changeset
  1281
class semidom_divide_unit_factor = semidom_divide + unit_factor +
c50db2128048 slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
haftmann
parents: 64713
diff changeset
  1282
  assumes unit_factor_0 [simp]: "unit_factor 0 = 0"
c50db2128048 slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
haftmann
parents: 64713
diff changeset
  1283
    and is_unit_unit_factor: "a dvd 1 \<Longrightarrow> unit_factor a = a"
c50db2128048 slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
haftmann
parents: 64713
diff changeset
  1284
    and unit_factor_is_unit: "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd 1"
c50db2128048 slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
haftmann
parents: 64713
diff changeset
  1285
    and unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
67226
ec32cdaab97b isabelle update_cartouches -c -t;
wenzelm
parents: 67084
diff changeset
  1286
  \<comment> \<open>This fine-grained hierarchy will later on allow lean normalization of polynomials\<close>
64848
c50db2128048 slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
haftmann
parents: 64713
diff changeset
  1287
  
c50db2128048 slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
haftmann
parents: 64713
diff changeset
  1288
class normalization_semidom = algebraic_semidom + semidom_divide_unit_factor +
60685
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1289
  fixes normalize :: "'a \<Rightarrow> 'a"
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615
diff changeset
  1290
  assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a"
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63456
diff changeset
  1291
    and normalize_0 [simp]: "normalize 0 = 0"
60685
cb21b7022b00 moved normalization and unit_factor into Main HOL corpus
haftmann
parents: 60615