src/HOL/Euclidean_Division.thy
author haftmann
Sun Oct 08 22:28:21 2017 +0200 (21 months ago)
changeset 66806 a4e82b58d833
parent 66798 39bb2462e681
child 66807 c3631f32dfeb
permissions -rw-r--r--
abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
haftmann@64785
     1
(*  Title:      HOL/Euclidean_Division.thy
haftmann@64785
     2
    Author:     Manuel Eberl, TU Muenchen
haftmann@64785
     3
    Author:     Florian Haftmann, TU Muenchen
haftmann@64785
     4
*)
haftmann@64785
     5
haftmann@64785
     6
section \<open>Uniquely determined division in euclidean (semi)rings\<close>
haftmann@64785
     7
haftmann@64785
     8
theory Euclidean_Division
haftmann@64785
     9
  imports Nat_Transfer
haftmann@64785
    10
begin
haftmann@64785
    11
haftmann@64785
    12
subsection \<open>Quotient and remainder in integral domains\<close>
haftmann@64785
    13
haftmann@64785
    14
class semidom_modulo = algebraic_semidom + semiring_modulo
haftmann@64785
    15
begin
haftmann@64785
    16
haftmann@64785
    17
lemma mod_0 [simp]: "0 mod a = 0"
haftmann@64785
    18
  using div_mult_mod_eq [of 0 a] by simp
haftmann@64785
    19
haftmann@64785
    20
lemma mod_by_0 [simp]: "a mod 0 = a"
haftmann@64785
    21
  using div_mult_mod_eq [of a 0] by simp
haftmann@64785
    22
haftmann@64785
    23
lemma mod_by_1 [simp]:
haftmann@64785
    24
  "a mod 1 = 0"
haftmann@64785
    25
proof -
haftmann@64785
    26
  from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp
haftmann@64785
    27
  then have "a + a mod 1 = a + 0" by simp
haftmann@64785
    28
  then show ?thesis by (rule add_left_imp_eq)
haftmann@64785
    29
qed
haftmann@64785
    30
haftmann@64785
    31
lemma mod_self [simp]:
haftmann@64785
    32
  "a mod a = 0"
haftmann@64785
    33
  using div_mult_mod_eq [of a a] by simp
haftmann@64785
    34
haftmann@64785
    35
lemma dvd_imp_mod_0 [simp]:
haftmann@64785
    36
  assumes "a dvd b"
haftmann@64785
    37
  shows "b mod a = 0"
haftmann@64785
    38
  using assms minus_div_mult_eq_mod [of b a] by simp
haftmann@64785
    39
haftmann@64785
    40
lemma mod_0_imp_dvd: 
haftmann@64785
    41
  assumes "a mod b = 0"
haftmann@64785
    42
  shows   "b dvd a"
haftmann@64785
    43
proof -
haftmann@64785
    44
  have "b dvd ((a div b) * b)" by simp
haftmann@64785
    45
  also have "(a div b) * b = a"
haftmann@64785
    46
    using div_mult_mod_eq [of a b] by (simp add: assms)
haftmann@64785
    47
  finally show ?thesis .
haftmann@64785
    48
qed
haftmann@64785
    49
haftmann@64785
    50
lemma mod_eq_0_iff_dvd:
haftmann@64785
    51
  "a mod b = 0 \<longleftrightarrow> b dvd a"
haftmann@64785
    52
  by (auto intro: mod_0_imp_dvd)
haftmann@64785
    53
haftmann@64785
    54
lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
haftmann@64785
    55
  "a dvd b \<longleftrightarrow> b mod a = 0"
haftmann@64785
    56
  by (simp add: mod_eq_0_iff_dvd)
haftmann@64785
    57
haftmann@64785
    58
lemma dvd_mod_iff: 
haftmann@64785
    59
  assumes "c dvd b"
haftmann@64785
    60
  shows "c dvd a mod b \<longleftrightarrow> c dvd a"
haftmann@64785
    61
proof -
haftmann@64785
    62
  from assms have "(c dvd a mod b) \<longleftrightarrow> (c dvd ((a div b) * b + a mod b))" 
haftmann@64785
    63
    by (simp add: dvd_add_right_iff)
haftmann@64785
    64
  also have "(a div b) * b + a mod b = a"
haftmann@64785
    65
    using div_mult_mod_eq [of a b] by simp
haftmann@64785
    66
  finally show ?thesis .
haftmann@64785
    67
qed
haftmann@64785
    68
haftmann@64785
    69
lemma dvd_mod_imp_dvd:
haftmann@64785
    70
  assumes "c dvd a mod b" and "c dvd b"
haftmann@64785
    71
  shows "c dvd a"
haftmann@64785
    72
  using assms dvd_mod_iff [of c b a] by simp
haftmann@64785
    73
haftmann@64785
    74
end
haftmann@64785
    75
haftmann@64785
    76
class idom_modulo = idom + semidom_modulo
haftmann@64785
    77
begin
haftmann@64785
    78
haftmann@64785
    79
subclass idom_divide ..
haftmann@64785
    80
haftmann@64785
    81
lemma div_diff [simp]:
haftmann@64785
    82
  "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> (a - b) div c = a div c - b div c"
haftmann@64785
    83
  using div_add [of _  _ "- b"] by (simp add: dvd_neg_div)
haftmann@64785
    84
haftmann@64785
    85
end
haftmann@64785
    86
haftmann@64785
    87
  
haftmann@64785
    88
subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close>
haftmann@64785
    89
  
haftmann@64785
    90
class euclidean_semiring = semidom_modulo + normalization_semidom + 
haftmann@64785
    91
  fixes euclidean_size :: "'a \<Rightarrow> nat"
haftmann@64785
    92
  assumes size_0 [simp]: "euclidean_size 0 = 0"
haftmann@64785
    93
  assumes mod_size_less: 
haftmann@64785
    94
    "b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b"
haftmann@64785
    95
  assumes size_mult_mono:
haftmann@64785
    96
    "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
haftmann@64785
    97
begin
haftmann@64785
    98
haftmann@64785
    99
lemma size_mult_mono': "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (b * a)"
haftmann@64785
   100
  by (subst mult.commute) (rule size_mult_mono)
haftmann@64785
   101
haftmann@64785
   102
lemma euclidean_size_normalize [simp]:
haftmann@64785
   103
  "euclidean_size (normalize a) = euclidean_size a"
haftmann@64785
   104
proof (cases "a = 0")
haftmann@64785
   105
  case True
haftmann@64785
   106
  then show ?thesis
haftmann@64785
   107
    by simp
haftmann@64785
   108
next
haftmann@64785
   109
  case [simp]: False
haftmann@64785
   110
  have "euclidean_size (normalize a) \<le> euclidean_size (normalize a * unit_factor a)"
haftmann@64785
   111
    by (rule size_mult_mono) simp
haftmann@64785
   112
  moreover have "euclidean_size a \<le> euclidean_size (a * (1 div unit_factor a))"
haftmann@64785
   113
    by (rule size_mult_mono) simp
haftmann@64785
   114
  ultimately show ?thesis
haftmann@64785
   115
    by simp
haftmann@64785
   116
qed
haftmann@64785
   117
haftmann@64785
   118
lemma dvd_euclidean_size_eq_imp_dvd:
haftmann@64785
   119
  assumes "a \<noteq> 0" and "euclidean_size a = euclidean_size b"
haftmann@64785
   120
    and "b dvd a" 
haftmann@64785
   121
  shows "a dvd b"
haftmann@64785
   122
proof (rule ccontr)
haftmann@64785
   123
  assume "\<not> a dvd b"
haftmann@64785
   124
  hence "b mod a \<noteq> 0" using mod_0_imp_dvd [of b a] by blast
haftmann@64785
   125
  then have "b mod a \<noteq> 0" by (simp add: mod_eq_0_iff_dvd)
haftmann@64785
   126
  from \<open>b dvd a\<close> have "b dvd b mod a" by (simp add: dvd_mod_iff)
haftmann@64785
   127
  then obtain c where "b mod a = b * c" unfolding dvd_def by blast
haftmann@64785
   128
    with \<open>b mod a \<noteq> 0\<close> have "c \<noteq> 0" by auto
haftmann@64785
   129
  with \<open>b mod a = b * c\<close> have "euclidean_size (b mod a) \<ge> euclidean_size b"
haftmann@64785
   130
    using size_mult_mono by force
haftmann@64785
   131
  moreover from \<open>\<not> a dvd b\<close> and \<open>a \<noteq> 0\<close>
haftmann@64785
   132
  have "euclidean_size (b mod a) < euclidean_size a"
haftmann@64785
   133
    using mod_size_less by blast
haftmann@64785
   134
  ultimately show False using \<open>euclidean_size a = euclidean_size b\<close>
haftmann@64785
   135
    by simp
haftmann@64785
   136
qed
haftmann@64785
   137
haftmann@64785
   138
lemma euclidean_size_times_unit:
haftmann@64785
   139
  assumes "is_unit a"
haftmann@64785
   140
  shows   "euclidean_size (a * b) = euclidean_size b"
haftmann@64785
   141
proof (rule antisym)
haftmann@64785
   142
  from assms have [simp]: "a \<noteq> 0" by auto
haftmann@64785
   143
  thus "euclidean_size (a * b) \<ge> euclidean_size b" by (rule size_mult_mono')
haftmann@64785
   144
  from assms have "is_unit (1 div a)" by simp
haftmann@64785
   145
  hence "1 div a \<noteq> 0" by (intro notI) simp_all
haftmann@64785
   146
  hence "euclidean_size (a * b) \<le> euclidean_size ((1 div a) * (a * b))"
haftmann@64785
   147
    by (rule size_mult_mono')
haftmann@64785
   148
  also from assms have "(1 div a) * (a * b) = b"
haftmann@64785
   149
    by (simp add: algebra_simps unit_div_mult_swap)
haftmann@64785
   150
  finally show "euclidean_size (a * b) \<le> euclidean_size b" .
haftmann@64785
   151
qed
haftmann@64785
   152
haftmann@64785
   153
lemma euclidean_size_unit:
haftmann@64785
   154
  "is_unit a \<Longrightarrow> euclidean_size a = euclidean_size 1"
haftmann@64785
   155
  using euclidean_size_times_unit [of a 1] by simp
haftmann@64785
   156
haftmann@64785
   157
lemma unit_iff_euclidean_size: 
haftmann@64785
   158
  "is_unit a \<longleftrightarrow> euclidean_size a = euclidean_size 1 \<and> a \<noteq> 0"
haftmann@64785
   159
proof safe
haftmann@64785
   160
  assume A: "a \<noteq> 0" and B: "euclidean_size a = euclidean_size 1"
haftmann@64785
   161
  show "is_unit a"
haftmann@64785
   162
    by (rule dvd_euclidean_size_eq_imp_dvd [OF A B]) simp_all
haftmann@64785
   163
qed (auto intro: euclidean_size_unit)
haftmann@64785
   164
haftmann@64785
   165
lemma euclidean_size_times_nonunit:
haftmann@64785
   166
  assumes "a \<noteq> 0" "b \<noteq> 0" "\<not> is_unit a"
haftmann@64785
   167
  shows   "euclidean_size b < euclidean_size (a * b)"
haftmann@64785
   168
proof (rule ccontr)
haftmann@64785
   169
  assume "\<not>euclidean_size b < euclidean_size (a * b)"
haftmann@64785
   170
  with size_mult_mono'[OF assms(1), of b] 
haftmann@64785
   171
    have eq: "euclidean_size (a * b) = euclidean_size b" by simp
haftmann@64785
   172
  have "a * b dvd b"
haftmann@64785
   173
    by (rule dvd_euclidean_size_eq_imp_dvd [OF _ eq]) (insert assms, simp_all)
haftmann@64785
   174
  hence "a * b dvd 1 * b" by simp
haftmann@64785
   175
  with \<open>b \<noteq> 0\<close> have "is_unit a" by (subst (asm) dvd_times_right_cancel_iff)
haftmann@64785
   176
  with assms(3) show False by contradiction
haftmann@64785
   177
qed
haftmann@64785
   178
haftmann@64785
   179
lemma dvd_imp_size_le:
haftmann@64785
   180
  assumes "a dvd b" "b \<noteq> 0" 
haftmann@64785
   181
  shows   "euclidean_size a \<le> euclidean_size b"
haftmann@64785
   182
  using assms by (auto elim!: dvdE simp: size_mult_mono)
haftmann@64785
   183
haftmann@64785
   184
lemma dvd_proper_imp_size_less:
haftmann@64785
   185
  assumes "a dvd b" "\<not> b dvd a" "b \<noteq> 0" 
haftmann@64785
   186
  shows   "euclidean_size a < euclidean_size b"
haftmann@64785
   187
proof -
haftmann@64785
   188
  from assms(1) obtain c where "b = a * c" by (erule dvdE)
haftmann@64785
   189
  hence z: "b = c * a" by (simp add: mult.commute)
haftmann@64785
   190
  from z assms have "\<not>is_unit c" by (auto simp: mult.commute mult_unit_dvd_iff)
haftmann@64785
   191
  with z assms show ?thesis
haftmann@64785
   192
    by (auto intro!: euclidean_size_times_nonunit)
haftmann@64785
   193
qed
haftmann@64785
   194
haftmann@66798
   195
lemma unit_imp_mod_eq_0:
haftmann@66798
   196
  "a mod b = 0" if "is_unit b"
haftmann@66798
   197
  using that by (simp add: mod_eq_0_iff_dvd unit_imp_dvd)
haftmann@66798
   198
haftmann@64785
   199
end
haftmann@64785
   200
haftmann@64785
   201
class euclidean_ring = idom_modulo + euclidean_semiring
haftmann@64785
   202
haftmann@64785
   203
  
haftmann@66806
   204
subsection \<open>Euclidean (semi)rings with cancel rules\<close>
haftmann@66806
   205
haftmann@66806
   206
class euclidean_semiring_cancel = euclidean_semiring +
haftmann@66806
   207
  assumes div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
haftmann@66806
   208
  and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
haftmann@66806
   209
begin
haftmann@66806
   210
haftmann@66806
   211
lemma div_mult_self2 [simp]:
haftmann@66806
   212
  assumes "b \<noteq> 0"
haftmann@66806
   213
  shows "(a + b * c) div b = c + a div b"
haftmann@66806
   214
  using assms div_mult_self1 [of b a c] by (simp add: mult.commute)
haftmann@66806
   215
haftmann@66806
   216
lemma div_mult_self3 [simp]:
haftmann@66806
   217
  assumes "b \<noteq> 0"
haftmann@66806
   218
  shows "(c * b + a) div b = c + a div b"
haftmann@66806
   219
  using assms by (simp add: add.commute)
haftmann@66806
   220
haftmann@66806
   221
lemma div_mult_self4 [simp]:
haftmann@66806
   222
  assumes "b \<noteq> 0"
haftmann@66806
   223
  shows "(b * c + a) div b = c + a div b"
haftmann@66806
   224
  using assms by (simp add: add.commute)
haftmann@66806
   225
haftmann@66806
   226
lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b"
haftmann@66806
   227
proof (cases "b = 0")
haftmann@66806
   228
  case True then show ?thesis by simp
haftmann@66806
   229
next
haftmann@66806
   230
  case False
haftmann@66806
   231
  have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b"
haftmann@66806
   232
    by (simp add: div_mult_mod_eq)
haftmann@66806
   233
  also from False div_mult_self1 [of b a c] have
haftmann@66806
   234
    "\<dots> = (c + a div b) * b + (a + c * b) mod b"
haftmann@66806
   235
      by (simp add: algebra_simps)
haftmann@66806
   236
  finally have "a = a div b * b + (a + c * b) mod b"
haftmann@66806
   237
    by (simp add: add.commute [of a] add.assoc distrib_right)
haftmann@66806
   238
  then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
haftmann@66806
   239
    by (simp add: div_mult_mod_eq)
haftmann@66806
   240
  then show ?thesis by simp
haftmann@66806
   241
qed
haftmann@66806
   242
haftmann@66806
   243
lemma mod_mult_self2 [simp]:
haftmann@66806
   244
  "(a + b * c) mod b = a mod b"
haftmann@66806
   245
  by (simp add: mult.commute [of b])
haftmann@66806
   246
haftmann@66806
   247
lemma mod_mult_self3 [simp]:
haftmann@66806
   248
  "(c * b + a) mod b = a mod b"
haftmann@66806
   249
  by (simp add: add.commute)
haftmann@66806
   250
haftmann@66806
   251
lemma mod_mult_self4 [simp]:
haftmann@66806
   252
  "(b * c + a) mod b = a mod b"
haftmann@66806
   253
  by (simp add: add.commute)
haftmann@66806
   254
haftmann@66806
   255
lemma mod_mult_self1_is_0 [simp]:
haftmann@66806
   256
  "b * a mod b = 0"
haftmann@66806
   257
  using mod_mult_self2 [of 0 b a] by simp
haftmann@66806
   258
haftmann@66806
   259
lemma mod_mult_self2_is_0 [simp]:
haftmann@66806
   260
  "a * b mod b = 0"
haftmann@66806
   261
  using mod_mult_self1 [of 0 a b] by simp
haftmann@66806
   262
haftmann@66806
   263
lemma div_add_self1:
haftmann@66806
   264
  assumes "b \<noteq> 0"
haftmann@66806
   265
  shows "(b + a) div b = a div b + 1"
haftmann@66806
   266
  using assms div_mult_self1 [of b a 1] by (simp add: add.commute)
haftmann@66806
   267
haftmann@66806
   268
lemma div_add_self2:
haftmann@66806
   269
  assumes "b \<noteq> 0"
haftmann@66806
   270
  shows "(a + b) div b = a div b + 1"
haftmann@66806
   271
  using assms div_add_self1 [of b a] by (simp add: add.commute)
haftmann@66806
   272
haftmann@66806
   273
lemma mod_add_self1 [simp]:
haftmann@66806
   274
  "(b + a) mod b = a mod b"
haftmann@66806
   275
  using mod_mult_self1 [of a 1 b] by (simp add: add.commute)
haftmann@66806
   276
haftmann@66806
   277
lemma mod_add_self2 [simp]:
haftmann@66806
   278
  "(a + b) mod b = a mod b"
haftmann@66806
   279
  using mod_mult_self1 [of a 1 b] by simp
haftmann@66806
   280
haftmann@66806
   281
lemma mod_div_trivial [simp]:
haftmann@66806
   282
  "a mod b div b = 0"
haftmann@66806
   283
proof (cases "b = 0")
haftmann@66806
   284
  assume "b = 0"
haftmann@66806
   285
  thus ?thesis by simp
haftmann@66806
   286
next
haftmann@66806
   287
  assume "b \<noteq> 0"
haftmann@66806
   288
  hence "a div b + a mod b div b = (a mod b + a div b * b) div b"
haftmann@66806
   289
    by (rule div_mult_self1 [symmetric])
haftmann@66806
   290
  also have "\<dots> = a div b"
haftmann@66806
   291
    by (simp only: mod_div_mult_eq)
haftmann@66806
   292
  also have "\<dots> = a div b + 0"
haftmann@66806
   293
    by simp
haftmann@66806
   294
  finally show ?thesis
haftmann@66806
   295
    by (rule add_left_imp_eq)
haftmann@66806
   296
qed
haftmann@66806
   297
haftmann@66806
   298
lemma mod_mod_trivial [simp]:
haftmann@66806
   299
  "a mod b mod b = a mod b"
haftmann@66806
   300
proof -
haftmann@66806
   301
  have "a mod b mod b = (a mod b + a div b * b) mod b"
haftmann@66806
   302
    by (simp only: mod_mult_self1)
haftmann@66806
   303
  also have "\<dots> = a mod b"
haftmann@66806
   304
    by (simp only: mod_div_mult_eq)
haftmann@66806
   305
  finally show ?thesis .
haftmann@66806
   306
qed
haftmann@66806
   307
haftmann@66806
   308
lemma mod_mod_cancel:
haftmann@66806
   309
  assumes "c dvd b"
haftmann@66806
   310
  shows "a mod b mod c = a mod c"
haftmann@66806
   311
proof -
haftmann@66806
   312
  from \<open>c dvd b\<close> obtain k where "b = c * k"
haftmann@66806
   313
    by (rule dvdE)
haftmann@66806
   314
  have "a mod b mod c = a mod (c * k) mod c"
haftmann@66806
   315
    by (simp only: \<open>b = c * k\<close>)
haftmann@66806
   316
  also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
haftmann@66806
   317
    by (simp only: mod_mult_self1)
haftmann@66806
   318
  also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
haftmann@66806
   319
    by (simp only: ac_simps)
haftmann@66806
   320
  also have "\<dots> = a mod c"
haftmann@66806
   321
    by (simp only: div_mult_mod_eq)
haftmann@66806
   322
  finally show ?thesis .
haftmann@66806
   323
qed
haftmann@66806
   324
haftmann@66806
   325
lemma div_mult_mult2 [simp]:
haftmann@66806
   326
  "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
haftmann@66806
   327
  by (drule div_mult_mult1) (simp add: mult.commute)
haftmann@66806
   328
haftmann@66806
   329
lemma div_mult_mult1_if [simp]:
haftmann@66806
   330
  "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"
haftmann@66806
   331
  by simp_all
haftmann@66806
   332
haftmann@66806
   333
lemma mod_mult_mult1:
haftmann@66806
   334
  "(c * a) mod (c * b) = c * (a mod b)"
haftmann@66806
   335
proof (cases "c = 0")
haftmann@66806
   336
  case True then show ?thesis by simp
haftmann@66806
   337
next
haftmann@66806
   338
  case False
haftmann@66806
   339
  from div_mult_mod_eq
haftmann@66806
   340
  have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
haftmann@66806
   341
  with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
haftmann@66806
   342
    = c * a + c * (a mod b)" by (simp add: algebra_simps)
haftmann@66806
   343
  with div_mult_mod_eq show ?thesis by simp
haftmann@66806
   344
qed
haftmann@66806
   345
haftmann@66806
   346
lemma mod_mult_mult2:
haftmann@66806
   347
  "(a * c) mod (b * c) = (a mod b) * c"
haftmann@66806
   348
  using mod_mult_mult1 [of c a b] by (simp add: mult.commute)
haftmann@66806
   349
haftmann@66806
   350
lemma mult_mod_left: "(a mod b) * c = (a * c) mod (b * c)"
haftmann@66806
   351
  by (fact mod_mult_mult2 [symmetric])
haftmann@66806
   352
haftmann@66806
   353
lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)"
haftmann@66806
   354
  by (fact mod_mult_mult1 [symmetric])
haftmann@66806
   355
haftmann@66806
   356
lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
haftmann@66806
   357
  unfolding dvd_def by (auto simp add: mod_mult_mult1)
haftmann@66806
   358
haftmann@66806
   359
lemma div_plus_div_distrib_dvd_left:
haftmann@66806
   360
  "c dvd a \<Longrightarrow> (a + b) div c = a div c + b div c"
haftmann@66806
   361
  by (cases "c = 0") (auto elim: dvdE)
haftmann@66806
   362
haftmann@66806
   363
lemma div_plus_div_distrib_dvd_right:
haftmann@66806
   364
  "c dvd b \<Longrightarrow> (a + b) div c = a div c + b div c"
haftmann@66806
   365
  using div_plus_div_distrib_dvd_left [of c b a]
haftmann@66806
   366
  by (simp add: ac_simps)
haftmann@66806
   367
haftmann@66806
   368
named_theorems mod_simps
haftmann@66806
   369
haftmann@66806
   370
text \<open>Addition respects modular equivalence.\<close>
haftmann@66806
   371
haftmann@66806
   372
lemma mod_add_left_eq [mod_simps]:
haftmann@66806
   373
  "(a mod c + b) mod c = (a + b) mod c"
haftmann@66806
   374
proof -
haftmann@66806
   375
  have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
haftmann@66806
   376
    by (simp only: div_mult_mod_eq)
haftmann@66806
   377
  also have "\<dots> = (a mod c + b + a div c * c) mod c"
haftmann@66806
   378
    by (simp only: ac_simps)
haftmann@66806
   379
  also have "\<dots> = (a mod c + b) mod c"
haftmann@66806
   380
    by (rule mod_mult_self1)
haftmann@66806
   381
  finally show ?thesis
haftmann@66806
   382
    by (rule sym)
haftmann@66806
   383
qed
haftmann@66806
   384
haftmann@66806
   385
lemma mod_add_right_eq [mod_simps]:
haftmann@66806
   386
  "(a + b mod c) mod c = (a + b) mod c"
haftmann@66806
   387
  using mod_add_left_eq [of b c a] by (simp add: ac_simps)
haftmann@66806
   388
haftmann@66806
   389
lemma mod_add_eq:
haftmann@66806
   390
  "(a mod c + b mod c) mod c = (a + b) mod c"
haftmann@66806
   391
  by (simp add: mod_add_left_eq mod_add_right_eq)
haftmann@66806
   392
haftmann@66806
   393
lemma mod_sum_eq [mod_simps]:
haftmann@66806
   394
  "(\<Sum>i\<in>A. f i mod a) mod a = sum f A mod a"
haftmann@66806
   395
proof (induct A rule: infinite_finite_induct)
haftmann@66806
   396
  case (insert i A)
haftmann@66806
   397
  then have "(\<Sum>i\<in>insert i A. f i mod a) mod a
haftmann@66806
   398
    = (f i mod a + (\<Sum>i\<in>A. f i mod a)) mod a"
haftmann@66806
   399
    by simp
haftmann@66806
   400
  also have "\<dots> = (f i + (\<Sum>i\<in>A. f i mod a) mod a) mod a"
haftmann@66806
   401
    by (simp add: mod_simps)
haftmann@66806
   402
  also have "\<dots> = (f i + (\<Sum>i\<in>A. f i) mod a) mod a"
haftmann@66806
   403
    by (simp add: insert.hyps)
haftmann@66806
   404
  finally show ?case
haftmann@66806
   405
    by (simp add: insert.hyps mod_simps)
haftmann@66806
   406
qed simp_all
haftmann@66806
   407
haftmann@66806
   408
lemma mod_add_cong:
haftmann@66806
   409
  assumes "a mod c = a' mod c"
haftmann@66806
   410
  assumes "b mod c = b' mod c"
haftmann@66806
   411
  shows "(a + b) mod c = (a' + b') mod c"
haftmann@66806
   412
proof -
haftmann@66806
   413
  have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
haftmann@66806
   414
    unfolding assms ..
haftmann@66806
   415
  then show ?thesis
haftmann@66806
   416
    by (simp add: mod_add_eq)
haftmann@66806
   417
qed
haftmann@66806
   418
haftmann@66806
   419
text \<open>Multiplication respects modular equivalence.\<close>
haftmann@66806
   420
haftmann@66806
   421
lemma mod_mult_left_eq [mod_simps]:
haftmann@66806
   422
  "((a mod c) * b) mod c = (a * b) mod c"
haftmann@66806
   423
proof -
haftmann@66806
   424
  have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
haftmann@66806
   425
    by (simp only: div_mult_mod_eq)
haftmann@66806
   426
  also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
haftmann@66806
   427
    by (simp only: algebra_simps)
haftmann@66806
   428
  also have "\<dots> = (a mod c * b) mod c"
haftmann@66806
   429
    by (rule mod_mult_self1)
haftmann@66806
   430
  finally show ?thesis
haftmann@66806
   431
    by (rule sym)
haftmann@66806
   432
qed
haftmann@66806
   433
haftmann@66806
   434
lemma mod_mult_right_eq [mod_simps]:
haftmann@66806
   435
  "(a * (b mod c)) mod c = (a * b) mod c"
haftmann@66806
   436
  using mod_mult_left_eq [of b c a] by (simp add: ac_simps)
haftmann@66806
   437
haftmann@66806
   438
lemma mod_mult_eq:
haftmann@66806
   439
  "((a mod c) * (b mod c)) mod c = (a * b) mod c"
haftmann@66806
   440
  by (simp add: mod_mult_left_eq mod_mult_right_eq)
haftmann@66806
   441
haftmann@66806
   442
lemma mod_prod_eq [mod_simps]:
haftmann@66806
   443
  "(\<Prod>i\<in>A. f i mod a) mod a = prod f A mod a"
haftmann@66806
   444
proof (induct A rule: infinite_finite_induct)
haftmann@66806
   445
  case (insert i A)
haftmann@66806
   446
  then have "(\<Prod>i\<in>insert i A. f i mod a) mod a
haftmann@66806
   447
    = (f i mod a * (\<Prod>i\<in>A. f i mod a)) mod a"
haftmann@66806
   448
    by simp
haftmann@66806
   449
  also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i mod a) mod a)) mod a"
haftmann@66806
   450
    by (simp add: mod_simps)
haftmann@66806
   451
  also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i) mod a)) mod a"
haftmann@66806
   452
    by (simp add: insert.hyps)
haftmann@66806
   453
  finally show ?case
haftmann@66806
   454
    by (simp add: insert.hyps mod_simps)
haftmann@66806
   455
qed simp_all
haftmann@66806
   456
haftmann@66806
   457
lemma mod_mult_cong:
haftmann@66806
   458
  assumes "a mod c = a' mod c"
haftmann@66806
   459
  assumes "b mod c = b' mod c"
haftmann@66806
   460
  shows "(a * b) mod c = (a' * b') mod c"
haftmann@66806
   461
proof -
haftmann@66806
   462
  have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
haftmann@66806
   463
    unfolding assms ..
haftmann@66806
   464
  then show ?thesis
haftmann@66806
   465
    by (simp add: mod_mult_eq)
haftmann@66806
   466
qed
haftmann@66806
   467
haftmann@66806
   468
text \<open>Exponentiation respects modular equivalence.\<close>
haftmann@66806
   469
haftmann@66806
   470
lemma power_mod [mod_simps]: 
haftmann@66806
   471
  "((a mod b) ^ n) mod b = (a ^ n) mod b"
haftmann@66806
   472
proof (induct n)
haftmann@66806
   473
  case 0
haftmann@66806
   474
  then show ?case by simp
haftmann@66806
   475
next
haftmann@66806
   476
  case (Suc n)
haftmann@66806
   477
  have "(a mod b) ^ Suc n mod b = (a mod b) * ((a mod b) ^ n mod b) mod b"
haftmann@66806
   478
    by (simp add: mod_mult_right_eq)
haftmann@66806
   479
  with Suc show ?case
haftmann@66806
   480
    by (simp add: mod_mult_left_eq mod_mult_right_eq)
haftmann@66806
   481
qed
haftmann@66806
   482
haftmann@66806
   483
end
haftmann@66806
   484
haftmann@66806
   485
haftmann@66806
   486
class euclidean_ring_cancel = euclidean_ring + euclidean_semiring_cancel
haftmann@66806
   487
begin
haftmann@66806
   488
haftmann@66806
   489
subclass idom_divide ..
haftmann@66806
   490
haftmann@66806
   491
lemma div_minus_minus [simp]: "(- a) div (- b) = a div b"
haftmann@66806
   492
  using div_mult_mult1 [of "- 1" a b] by simp
haftmann@66806
   493
haftmann@66806
   494
lemma mod_minus_minus [simp]: "(- a) mod (- b) = - (a mod b)"
haftmann@66806
   495
  using mod_mult_mult1 [of "- 1" a b] by simp
haftmann@66806
   496
haftmann@66806
   497
lemma div_minus_right: "a div (- b) = (- a) div b"
haftmann@66806
   498
  using div_minus_minus [of "- a" b] by simp
haftmann@66806
   499
haftmann@66806
   500
lemma mod_minus_right: "a mod (- b) = - ((- a) mod b)"
haftmann@66806
   501
  using mod_minus_minus [of "- a" b] by simp
haftmann@66806
   502
haftmann@66806
   503
lemma div_minus1_right [simp]: "a div (- 1) = - a"
haftmann@66806
   504
  using div_minus_right [of a 1] by simp
haftmann@66806
   505
haftmann@66806
   506
lemma mod_minus1_right [simp]: "a mod (- 1) = 0"
haftmann@66806
   507
  using mod_minus_right [of a 1] by simp
haftmann@66806
   508
haftmann@66806
   509
text \<open>Negation respects modular equivalence.\<close>
haftmann@66806
   510
haftmann@66806
   511
lemma mod_minus_eq [mod_simps]:
haftmann@66806
   512
  "(- (a mod b)) mod b = (- a) mod b"
haftmann@66806
   513
proof -
haftmann@66806
   514
  have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
haftmann@66806
   515
    by (simp only: div_mult_mod_eq)
haftmann@66806
   516
  also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
haftmann@66806
   517
    by (simp add: ac_simps)
haftmann@66806
   518
  also have "\<dots> = (- (a mod b)) mod b"
haftmann@66806
   519
    by (rule mod_mult_self1)
haftmann@66806
   520
  finally show ?thesis
haftmann@66806
   521
    by (rule sym)
haftmann@66806
   522
qed
haftmann@66806
   523
haftmann@66806
   524
lemma mod_minus_cong:
haftmann@66806
   525
  assumes "a mod b = a' mod b"
haftmann@66806
   526
  shows "(- a) mod b = (- a') mod b"
haftmann@66806
   527
proof -
haftmann@66806
   528
  have "(- (a mod b)) mod b = (- (a' mod b)) mod b"
haftmann@66806
   529
    unfolding assms ..
haftmann@66806
   530
  then show ?thesis
haftmann@66806
   531
    by (simp add: mod_minus_eq)
haftmann@66806
   532
qed
haftmann@66806
   533
haftmann@66806
   534
text \<open>Subtraction respects modular equivalence.\<close>
haftmann@66806
   535
haftmann@66806
   536
lemma mod_diff_left_eq [mod_simps]:
haftmann@66806
   537
  "(a mod c - b) mod c = (a - b) mod c"
haftmann@66806
   538
  using mod_add_cong [of a c "a mod c" "- b" "- b"]
haftmann@66806
   539
  by simp
haftmann@66806
   540
haftmann@66806
   541
lemma mod_diff_right_eq [mod_simps]:
haftmann@66806
   542
  "(a - b mod c) mod c = (a - b) mod c"
haftmann@66806
   543
  using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
haftmann@66806
   544
  by simp
haftmann@66806
   545
haftmann@66806
   546
lemma mod_diff_eq:
haftmann@66806
   547
  "(a mod c - b mod c) mod c = (a - b) mod c"
haftmann@66806
   548
  using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
haftmann@66806
   549
  by simp
haftmann@66806
   550
haftmann@66806
   551
lemma mod_diff_cong:
haftmann@66806
   552
  assumes "a mod c = a' mod c"
haftmann@66806
   553
  assumes "b mod c = b' mod c"
haftmann@66806
   554
  shows "(a - b) mod c = (a' - b') mod c"
haftmann@66806
   555
  using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"]
haftmann@66806
   556
  by simp
haftmann@66806
   557
haftmann@66806
   558
lemma minus_mod_self2 [simp]:
haftmann@66806
   559
  "(a - b) mod b = a mod b"
haftmann@66806
   560
  using mod_diff_right_eq [of a b b]
haftmann@66806
   561
  by (simp add: mod_diff_right_eq)
haftmann@66806
   562
haftmann@66806
   563
lemma minus_mod_self1 [simp]:
haftmann@66806
   564
  "(b - a) mod b = - a mod b"
haftmann@66806
   565
  using mod_add_self2 [of "- a" b] by simp
haftmann@66806
   566
haftmann@66806
   567
lemma mod_eq_dvd_iff:
haftmann@66806
   568
  "a mod c = b mod c \<longleftrightarrow> c dvd a - b" (is "?P \<longleftrightarrow> ?Q")
haftmann@66806
   569
proof
haftmann@66806
   570
  assume ?P
haftmann@66806
   571
  then have "(a mod c - b mod c) mod c = 0"
haftmann@66806
   572
    by simp
haftmann@66806
   573
  then show ?Q
haftmann@66806
   574
    by (simp add: dvd_eq_mod_eq_0 mod_simps)
haftmann@66806
   575
next
haftmann@66806
   576
  assume ?Q
haftmann@66806
   577
  then obtain d where d: "a - b = c * d" ..
haftmann@66806
   578
  then have "a = c * d + b"
haftmann@66806
   579
    by (simp add: algebra_simps)
haftmann@66806
   580
  then show ?P by simp
haftmann@66806
   581
qed
haftmann@66806
   582
haftmann@66806
   583
end
haftmann@66806
   584
haftmann@66806
   585
  
haftmann@64785
   586
subsection \<open>Uniquely determined division\<close>
haftmann@64785
   587
  
haftmann@64785
   588
class unique_euclidean_semiring = euclidean_semiring + 
haftmann@64785
   589
  fixes uniqueness_constraint :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
haftmann@64785
   590
  assumes size_mono_mult:
haftmann@64785
   591
    "b \<noteq> 0 \<Longrightarrow> euclidean_size a < euclidean_size c
haftmann@64785
   592
      \<Longrightarrow> euclidean_size (a * b) < euclidean_size (c * b)"
haftmann@64785
   593
    -- \<open>FIXME justify\<close>
haftmann@64785
   594
  assumes uniqueness_constraint_mono_mult:
haftmann@64785
   595
    "uniqueness_constraint a b \<Longrightarrow> uniqueness_constraint (a * c) (b * c)"
haftmann@64785
   596
  assumes uniqueness_constraint_mod:
haftmann@64785
   597
    "b \<noteq> 0 \<Longrightarrow> \<not> b dvd a \<Longrightarrow> uniqueness_constraint (a mod b) b"
haftmann@64785
   598
  assumes div_bounded:
haftmann@64785
   599
    "b \<noteq> 0 \<Longrightarrow> uniqueness_constraint r b
haftmann@64785
   600
    \<Longrightarrow> euclidean_size r < euclidean_size b
haftmann@64785
   601
    \<Longrightarrow> (q * b + r) div b = q"
haftmann@64785
   602
begin
haftmann@64785
   603
haftmann@64785
   604
lemma divmod_cases [case_names divides remainder by0]:
haftmann@64785
   605
  obtains 
haftmann@64785
   606
    (divides) q where "b \<noteq> 0"
haftmann@64785
   607
      and "a div b = q"
haftmann@64785
   608
      and "a mod b = 0"
haftmann@64785
   609
      and "a = q * b"
haftmann@64785
   610
  | (remainder) q r where "b \<noteq> 0" and "r \<noteq> 0"
haftmann@64785
   611
      and "uniqueness_constraint r b"
haftmann@64785
   612
      and "euclidean_size r < euclidean_size b"
haftmann@64785
   613
      and "a div b = q"
haftmann@64785
   614
      and "a mod b = r"
haftmann@64785
   615
      and "a = q * b + r"
haftmann@64785
   616
  | (by0) "b = 0"
haftmann@64785
   617
proof (cases "b = 0")
haftmann@64785
   618
  case True
haftmann@64785
   619
  then show thesis
haftmann@64785
   620
  by (rule by0)
haftmann@64785
   621
next
haftmann@64785
   622
  case False
haftmann@64785
   623
  show thesis
haftmann@64785
   624
  proof (cases "b dvd a")
haftmann@64785
   625
    case True
haftmann@64785
   626
    then obtain q where "a = b * q" ..
haftmann@64785
   627
    with \<open>b \<noteq> 0\<close> divides
haftmann@64785
   628
    show thesis
haftmann@64785
   629
      by (simp add: ac_simps)
haftmann@64785
   630
  next
haftmann@64785
   631
    case False
haftmann@64785
   632
    then have "a mod b \<noteq> 0"
haftmann@64785
   633
      by (simp add: mod_eq_0_iff_dvd)
haftmann@64785
   634
    moreover from \<open>b \<noteq> 0\<close> \<open>\<not> b dvd a\<close> have "uniqueness_constraint (a mod b) b"
haftmann@64785
   635
      by (rule uniqueness_constraint_mod)
haftmann@64785
   636
    moreover have "euclidean_size (a mod b) < euclidean_size b"
haftmann@64785
   637
      using \<open>b \<noteq> 0\<close> by (rule mod_size_less)
haftmann@64785
   638
    moreover have "a = a div b * b + a mod b"
haftmann@64785
   639
      by (simp add: div_mult_mod_eq)
haftmann@64785
   640
    ultimately show thesis
haftmann@64785
   641
      using \<open>b \<noteq> 0\<close> by (blast intro: remainder)
haftmann@64785
   642
  qed
haftmann@64785
   643
qed
haftmann@64785
   644
haftmann@64785
   645
lemma div_eqI:
haftmann@64785
   646
  "a div b = q" if "b \<noteq> 0" "uniqueness_constraint r b"
haftmann@64785
   647
    "euclidean_size r < euclidean_size b" "q * b + r = a"
haftmann@64785
   648
proof -
haftmann@64785
   649
  from that have "(q * b + r) div b = q"
haftmann@64785
   650
    by (auto intro: div_bounded)
haftmann@64785
   651
  with that show ?thesis
haftmann@64785
   652
    by simp
haftmann@64785
   653
qed
haftmann@64785
   654
haftmann@64785
   655
lemma mod_eqI:
haftmann@64785
   656
  "a mod b = r" if "b \<noteq> 0" "uniqueness_constraint r b"
haftmann@64785
   657
    "euclidean_size r < euclidean_size b" "q * b + r = a" 
haftmann@64785
   658
proof -
haftmann@64785
   659
  from that have "a div b = q"
haftmann@64785
   660
    by (rule div_eqI)
haftmann@64785
   661
  moreover have "a div b * b + a mod b = a"
haftmann@64785
   662
    by (fact div_mult_mod_eq)
haftmann@64785
   663
  ultimately have "a div b * b + a mod b = a div b * b + r"
haftmann@64785
   664
    using \<open>q * b + r = a\<close> by simp
haftmann@64785
   665
  then show ?thesis
haftmann@64785
   666
    by simp
haftmann@64785
   667
qed
haftmann@64785
   668
haftmann@66806
   669
subclass euclidean_semiring_cancel
haftmann@66806
   670
proof
haftmann@66806
   671
  show "(a + c * b) div b = c + a div b" if "b \<noteq> 0" for a b c
haftmann@66806
   672
  proof (cases a b rule: divmod_cases)
haftmann@66806
   673
    case by0
haftmann@66806
   674
    with \<open>b \<noteq> 0\<close> show ?thesis
haftmann@66806
   675
      by simp
haftmann@66806
   676
  next
haftmann@66806
   677
    case (divides q)
haftmann@66806
   678
    then show ?thesis
haftmann@66806
   679
      by (simp add: ac_simps)
haftmann@66806
   680
  next
haftmann@66806
   681
    case (remainder q r)
haftmann@66806
   682
    then show ?thesis
haftmann@66806
   683
      by (auto intro: div_eqI simp add: algebra_simps)
haftmann@66806
   684
  qed
haftmann@66806
   685
next
haftmann@66806
   686
  show"(c * a) div (c * b) = a div b" if "c \<noteq> 0" for a b c
haftmann@66806
   687
  proof (cases a b rule: divmod_cases)
haftmann@66806
   688
    case by0
haftmann@66806
   689
    then show ?thesis
haftmann@66806
   690
      by simp
haftmann@66806
   691
  next
haftmann@66806
   692
    case (divides q)
haftmann@66806
   693
    with \<open>c \<noteq> 0\<close> show ?thesis
haftmann@66806
   694
      by (simp add: mult.left_commute [of c])
haftmann@66806
   695
  next
haftmann@66806
   696
    case (remainder q r)
haftmann@66806
   697
    from \<open>b \<noteq> 0\<close> \<open>c \<noteq> 0\<close> have "b * c \<noteq> 0"
haftmann@66806
   698
      by simp
haftmann@66806
   699
    from remainder \<open>c \<noteq> 0\<close>
haftmann@66806
   700
    have "uniqueness_constraint (r * c) (b * c)"
haftmann@66806
   701
      and "euclidean_size (r * c) < euclidean_size (b * c)"
haftmann@66806
   702
      by (simp_all add: uniqueness_constraint_mono_mult uniqueness_constraint_mod size_mono_mult)
haftmann@66806
   703
    with remainder show ?thesis
haftmann@66806
   704
      by (auto intro!: div_eqI [of _ "c * (a mod b)"] simp add: algebra_simps)
haftmann@66806
   705
        (use \<open>b * c \<noteq> 0\<close> in simp)
haftmann@66806
   706
  qed
haftmann@66806
   707
qed
haftmann@66806
   708
haftmann@64785
   709
end
haftmann@64785
   710
haftmann@64785
   711
class unique_euclidean_ring = euclidean_ring + unique_euclidean_semiring
haftmann@66806
   712
begin
haftmann@66806
   713
  
haftmann@66806
   714
subclass euclidean_ring_cancel ..
haftmann@64785
   715
haftmann@64785
   716
end
haftmann@66806
   717
haftmann@66806
   718
end