src/HOL/Euclidean_Division.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (19 months ago)
changeset 67003 49850a679c2c
parent 66886 960509bfd47e
child 67051 e7e54a0b9197
permissions -rw-r--r--
more robust sorted_entries;
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@66817
     6
section \<open>Division in euclidean (semi)rings\<close>
haftmann@64785
     7
haftmann@64785
     8
theory Euclidean_Division
haftmann@66817
     9
  imports Int Lattices_Big
haftmann@64785
    10
begin
haftmann@64785
    11
haftmann@64785
    12
subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close>
haftmann@64785
    13
  
haftmann@66817
    14
class euclidean_semiring = semidom_modulo + 
haftmann@64785
    15
  fixes euclidean_size :: "'a \<Rightarrow> nat"
haftmann@64785
    16
  assumes size_0 [simp]: "euclidean_size 0 = 0"
haftmann@64785
    17
  assumes mod_size_less: 
haftmann@64785
    18
    "b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b"
haftmann@64785
    19
  assumes size_mult_mono:
haftmann@64785
    20
    "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
haftmann@64785
    21
begin
haftmann@64785
    22
haftmann@66840
    23
lemma euclidean_size_eq_0_iff [simp]:
haftmann@66840
    24
  "euclidean_size b = 0 \<longleftrightarrow> b = 0"
haftmann@66840
    25
proof
haftmann@66840
    26
  assume "b = 0"
haftmann@66840
    27
  then show "euclidean_size b = 0"
haftmann@66840
    28
    by simp
haftmann@66840
    29
next
haftmann@66840
    30
  assume "euclidean_size b = 0"
haftmann@66840
    31
  show "b = 0"
haftmann@66840
    32
  proof (rule ccontr)
haftmann@66840
    33
    assume "b \<noteq> 0"
haftmann@66840
    34
    with mod_size_less have "euclidean_size (b mod b) < euclidean_size b" .
haftmann@66840
    35
    with \<open>euclidean_size b = 0\<close> show False
haftmann@66840
    36
      by simp
haftmann@66840
    37
  qed
haftmann@66840
    38
qed
haftmann@66840
    39
haftmann@66840
    40
lemma euclidean_size_greater_0_iff [simp]:
haftmann@66840
    41
  "euclidean_size b > 0 \<longleftrightarrow> b \<noteq> 0"
haftmann@66840
    42
  using euclidean_size_eq_0_iff [symmetric, of b] by safe simp
haftmann@66840
    43
haftmann@64785
    44
lemma size_mult_mono': "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (b * a)"
haftmann@64785
    45
  by (subst mult.commute) (rule size_mult_mono)
haftmann@64785
    46
haftmann@64785
    47
lemma dvd_euclidean_size_eq_imp_dvd:
haftmann@64785
    48
  assumes "a \<noteq> 0" and "euclidean_size a = euclidean_size b"
haftmann@64785
    49
    and "b dvd a" 
haftmann@64785
    50
  shows "a dvd b"
haftmann@64785
    51
proof (rule ccontr)
haftmann@64785
    52
  assume "\<not> a dvd b"
haftmann@64785
    53
  hence "b mod a \<noteq> 0" using mod_0_imp_dvd [of b a] by blast
haftmann@64785
    54
  then have "b mod a \<noteq> 0" by (simp add: mod_eq_0_iff_dvd)
haftmann@64785
    55
  from \<open>b dvd a\<close> have "b dvd b mod a" by (simp add: dvd_mod_iff)
haftmann@64785
    56
  then obtain c where "b mod a = b * c" unfolding dvd_def by blast
haftmann@64785
    57
    with \<open>b mod a \<noteq> 0\<close> have "c \<noteq> 0" by auto
haftmann@64785
    58
  with \<open>b mod a = b * c\<close> have "euclidean_size (b mod a) \<ge> euclidean_size b"
haftmann@64785
    59
    using size_mult_mono by force
haftmann@64785
    60
  moreover from \<open>\<not> a dvd b\<close> and \<open>a \<noteq> 0\<close>
haftmann@64785
    61
  have "euclidean_size (b mod a) < euclidean_size a"
haftmann@64785
    62
    using mod_size_less by blast
haftmann@64785
    63
  ultimately show False using \<open>euclidean_size a = euclidean_size b\<close>
haftmann@64785
    64
    by simp
haftmann@64785
    65
qed
haftmann@64785
    66
haftmann@64785
    67
lemma euclidean_size_times_unit:
haftmann@64785
    68
  assumes "is_unit a"
haftmann@64785
    69
  shows   "euclidean_size (a * b) = euclidean_size b"
haftmann@64785
    70
proof (rule antisym)
haftmann@64785
    71
  from assms have [simp]: "a \<noteq> 0" by auto
haftmann@64785
    72
  thus "euclidean_size (a * b) \<ge> euclidean_size b" by (rule size_mult_mono')
haftmann@64785
    73
  from assms have "is_unit (1 div a)" by simp
haftmann@64785
    74
  hence "1 div a \<noteq> 0" by (intro notI) simp_all
haftmann@64785
    75
  hence "euclidean_size (a * b) \<le> euclidean_size ((1 div a) * (a * b))"
haftmann@64785
    76
    by (rule size_mult_mono')
haftmann@64785
    77
  also from assms have "(1 div a) * (a * b) = b"
haftmann@64785
    78
    by (simp add: algebra_simps unit_div_mult_swap)
haftmann@64785
    79
  finally show "euclidean_size (a * b) \<le> euclidean_size b" .
haftmann@64785
    80
qed
haftmann@64785
    81
haftmann@64785
    82
lemma euclidean_size_unit:
haftmann@64785
    83
  "is_unit a \<Longrightarrow> euclidean_size a = euclidean_size 1"
haftmann@64785
    84
  using euclidean_size_times_unit [of a 1] by simp
haftmann@64785
    85
haftmann@64785
    86
lemma unit_iff_euclidean_size: 
haftmann@64785
    87
  "is_unit a \<longleftrightarrow> euclidean_size a = euclidean_size 1 \<and> a \<noteq> 0"
haftmann@64785
    88
proof safe
haftmann@64785
    89
  assume A: "a \<noteq> 0" and B: "euclidean_size a = euclidean_size 1"
haftmann@64785
    90
  show "is_unit a"
haftmann@64785
    91
    by (rule dvd_euclidean_size_eq_imp_dvd [OF A B]) simp_all
haftmann@64785
    92
qed (auto intro: euclidean_size_unit)
haftmann@64785
    93
haftmann@64785
    94
lemma euclidean_size_times_nonunit:
haftmann@64785
    95
  assumes "a \<noteq> 0" "b \<noteq> 0" "\<not> is_unit a"
haftmann@64785
    96
  shows   "euclidean_size b < euclidean_size (a * b)"
haftmann@64785
    97
proof (rule ccontr)
haftmann@64785
    98
  assume "\<not>euclidean_size b < euclidean_size (a * b)"
haftmann@64785
    99
  with size_mult_mono'[OF assms(1), of b] 
haftmann@64785
   100
    have eq: "euclidean_size (a * b) = euclidean_size b" by simp
haftmann@64785
   101
  have "a * b dvd b"
haftmann@64785
   102
    by (rule dvd_euclidean_size_eq_imp_dvd [OF _ eq]) (insert assms, simp_all)
haftmann@64785
   103
  hence "a * b dvd 1 * b" by simp
haftmann@64785
   104
  with \<open>b \<noteq> 0\<close> have "is_unit a" by (subst (asm) dvd_times_right_cancel_iff)
haftmann@64785
   105
  with assms(3) show False by contradiction
haftmann@64785
   106
qed
haftmann@64785
   107
haftmann@64785
   108
lemma dvd_imp_size_le:
haftmann@64785
   109
  assumes "a dvd b" "b \<noteq> 0" 
haftmann@64785
   110
  shows   "euclidean_size a \<le> euclidean_size b"
haftmann@64785
   111
  using assms by (auto elim!: dvdE simp: size_mult_mono)
haftmann@64785
   112
haftmann@64785
   113
lemma dvd_proper_imp_size_less:
haftmann@64785
   114
  assumes "a dvd b" "\<not> b dvd a" "b \<noteq> 0" 
haftmann@64785
   115
  shows   "euclidean_size a < euclidean_size b"
haftmann@64785
   116
proof -
haftmann@64785
   117
  from assms(1) obtain c where "b = a * c" by (erule dvdE)
haftmann@64785
   118
  hence z: "b = c * a" by (simp add: mult.commute)
haftmann@64785
   119
  from z assms have "\<not>is_unit c" by (auto simp: mult.commute mult_unit_dvd_iff)
haftmann@64785
   120
  with z assms show ?thesis
haftmann@64785
   121
    by (auto intro!: euclidean_size_times_nonunit)
haftmann@64785
   122
qed
haftmann@64785
   123
haftmann@66798
   124
lemma unit_imp_mod_eq_0:
haftmann@66798
   125
  "a mod b = 0" if "is_unit b"
haftmann@66798
   126
  using that by (simp add: mod_eq_0_iff_dvd unit_imp_dvd)
haftmann@66798
   127
haftmann@64785
   128
end
haftmann@64785
   129
haftmann@64785
   130
class euclidean_ring = idom_modulo + euclidean_semiring
haftmann@66886
   131
begin
haftmann@66886
   132
haftmann@66886
   133
lemma dvd_diff_commute:
haftmann@66886
   134
  "a dvd c - b \<longleftrightarrow> a dvd b - c"
haftmann@66886
   135
proof -
haftmann@66886
   136
  have "a dvd c - b \<longleftrightarrow> a dvd (c - b) * - 1"
haftmann@66886
   137
    by (subst dvd_mult_unit_iff) simp_all
haftmann@66886
   138
  then show ?thesis
haftmann@66886
   139
    by simp
haftmann@66886
   140
qed
haftmann@66886
   141
 
haftmann@66886
   142
end
haftmann@64785
   143
haftmann@66840
   144
haftmann@66806
   145
subsection \<open>Euclidean (semi)rings with cancel rules\<close>
haftmann@66806
   146
haftmann@66806
   147
class euclidean_semiring_cancel = euclidean_semiring +
haftmann@66806
   148
  assumes div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
haftmann@66806
   149
  and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
haftmann@66806
   150
begin
haftmann@66806
   151
haftmann@66806
   152
lemma div_mult_self2 [simp]:
haftmann@66806
   153
  assumes "b \<noteq> 0"
haftmann@66806
   154
  shows "(a + b * c) div b = c + a div b"
haftmann@66806
   155
  using assms div_mult_self1 [of b a c] by (simp add: mult.commute)
haftmann@66806
   156
haftmann@66806
   157
lemma div_mult_self3 [simp]:
haftmann@66806
   158
  assumes "b \<noteq> 0"
haftmann@66806
   159
  shows "(c * b + a) div b = c + a div b"
haftmann@66806
   160
  using assms by (simp add: add.commute)
haftmann@66806
   161
haftmann@66806
   162
lemma div_mult_self4 [simp]:
haftmann@66806
   163
  assumes "b \<noteq> 0"
haftmann@66806
   164
  shows "(b * c + a) div b = c + a div b"
haftmann@66806
   165
  using assms by (simp add: add.commute)
haftmann@66806
   166
haftmann@66806
   167
lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b"
haftmann@66806
   168
proof (cases "b = 0")
haftmann@66806
   169
  case True then show ?thesis by simp
haftmann@66806
   170
next
haftmann@66806
   171
  case False
haftmann@66806
   172
  have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b"
haftmann@66806
   173
    by (simp add: div_mult_mod_eq)
haftmann@66806
   174
  also from False div_mult_self1 [of b a c] have
haftmann@66806
   175
    "\<dots> = (c + a div b) * b + (a + c * b) mod b"
haftmann@66806
   176
      by (simp add: algebra_simps)
haftmann@66806
   177
  finally have "a = a div b * b + (a + c * b) mod b"
haftmann@66806
   178
    by (simp add: add.commute [of a] add.assoc distrib_right)
haftmann@66806
   179
  then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
haftmann@66806
   180
    by (simp add: div_mult_mod_eq)
haftmann@66806
   181
  then show ?thesis by simp
haftmann@66806
   182
qed
haftmann@66806
   183
haftmann@66806
   184
lemma mod_mult_self2 [simp]:
haftmann@66806
   185
  "(a + b * c) mod b = a mod b"
haftmann@66806
   186
  by (simp add: mult.commute [of b])
haftmann@66806
   187
haftmann@66806
   188
lemma mod_mult_self3 [simp]:
haftmann@66806
   189
  "(c * b + a) mod b = a mod b"
haftmann@66806
   190
  by (simp add: add.commute)
haftmann@66806
   191
haftmann@66806
   192
lemma mod_mult_self4 [simp]:
haftmann@66806
   193
  "(b * c + a) mod b = a mod b"
haftmann@66806
   194
  by (simp add: add.commute)
haftmann@66806
   195
haftmann@66806
   196
lemma mod_mult_self1_is_0 [simp]:
haftmann@66806
   197
  "b * a mod b = 0"
haftmann@66806
   198
  using mod_mult_self2 [of 0 b a] by simp
haftmann@66806
   199
haftmann@66806
   200
lemma mod_mult_self2_is_0 [simp]:
haftmann@66806
   201
  "a * b mod b = 0"
haftmann@66806
   202
  using mod_mult_self1 [of 0 a b] by simp
haftmann@66806
   203
haftmann@66806
   204
lemma div_add_self1:
haftmann@66806
   205
  assumes "b \<noteq> 0"
haftmann@66806
   206
  shows "(b + a) div b = a div b + 1"
haftmann@66806
   207
  using assms div_mult_self1 [of b a 1] by (simp add: add.commute)
haftmann@66806
   208
haftmann@66806
   209
lemma div_add_self2:
haftmann@66806
   210
  assumes "b \<noteq> 0"
haftmann@66806
   211
  shows "(a + b) div b = a div b + 1"
haftmann@66806
   212
  using assms div_add_self1 [of b a] by (simp add: add.commute)
haftmann@66806
   213
haftmann@66806
   214
lemma mod_add_self1 [simp]:
haftmann@66806
   215
  "(b + a) mod b = a mod b"
haftmann@66806
   216
  using mod_mult_self1 [of a 1 b] by (simp add: add.commute)
haftmann@66806
   217
haftmann@66806
   218
lemma mod_add_self2 [simp]:
haftmann@66806
   219
  "(a + b) mod b = a mod b"
haftmann@66806
   220
  using mod_mult_self1 [of a 1 b] by simp
haftmann@66806
   221
haftmann@66806
   222
lemma mod_div_trivial [simp]:
haftmann@66806
   223
  "a mod b div b = 0"
haftmann@66806
   224
proof (cases "b = 0")
haftmann@66806
   225
  assume "b = 0"
haftmann@66806
   226
  thus ?thesis by simp
haftmann@66806
   227
next
haftmann@66806
   228
  assume "b \<noteq> 0"
haftmann@66806
   229
  hence "a div b + a mod b div b = (a mod b + a div b * b) div b"
haftmann@66806
   230
    by (rule div_mult_self1 [symmetric])
haftmann@66806
   231
  also have "\<dots> = a div b"
haftmann@66806
   232
    by (simp only: mod_div_mult_eq)
haftmann@66806
   233
  also have "\<dots> = a div b + 0"
haftmann@66806
   234
    by simp
haftmann@66806
   235
  finally show ?thesis
haftmann@66806
   236
    by (rule add_left_imp_eq)
haftmann@66806
   237
qed
haftmann@66806
   238
haftmann@66806
   239
lemma mod_mod_trivial [simp]:
haftmann@66806
   240
  "a mod b mod b = a mod b"
haftmann@66806
   241
proof -
haftmann@66806
   242
  have "a mod b mod b = (a mod b + a div b * b) mod b"
haftmann@66806
   243
    by (simp only: mod_mult_self1)
haftmann@66806
   244
  also have "\<dots> = a mod b"
haftmann@66806
   245
    by (simp only: mod_div_mult_eq)
haftmann@66806
   246
  finally show ?thesis .
haftmann@66806
   247
qed
haftmann@66806
   248
haftmann@66806
   249
lemma mod_mod_cancel:
haftmann@66806
   250
  assumes "c dvd b"
haftmann@66806
   251
  shows "a mod b mod c = a mod c"
haftmann@66806
   252
proof -
haftmann@66806
   253
  from \<open>c dvd b\<close> obtain k where "b = c * k"
haftmann@66806
   254
    by (rule dvdE)
haftmann@66806
   255
  have "a mod b mod c = a mod (c * k) mod c"
haftmann@66806
   256
    by (simp only: \<open>b = c * k\<close>)
haftmann@66806
   257
  also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
haftmann@66806
   258
    by (simp only: mod_mult_self1)
haftmann@66806
   259
  also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
haftmann@66806
   260
    by (simp only: ac_simps)
haftmann@66806
   261
  also have "\<dots> = a mod c"
haftmann@66806
   262
    by (simp only: div_mult_mod_eq)
haftmann@66806
   263
  finally show ?thesis .
haftmann@66806
   264
qed
haftmann@66806
   265
haftmann@66806
   266
lemma div_mult_mult2 [simp]:
haftmann@66806
   267
  "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
haftmann@66806
   268
  by (drule div_mult_mult1) (simp add: mult.commute)
haftmann@66806
   269
haftmann@66806
   270
lemma div_mult_mult1_if [simp]:
haftmann@66806
   271
  "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"
haftmann@66806
   272
  by simp_all
haftmann@66806
   273
haftmann@66806
   274
lemma mod_mult_mult1:
haftmann@66806
   275
  "(c * a) mod (c * b) = c * (a mod b)"
haftmann@66806
   276
proof (cases "c = 0")
haftmann@66806
   277
  case True then show ?thesis by simp
haftmann@66806
   278
next
haftmann@66806
   279
  case False
haftmann@66806
   280
  from div_mult_mod_eq
haftmann@66806
   281
  have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
haftmann@66806
   282
  with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
haftmann@66806
   283
    = c * a + c * (a mod b)" by (simp add: algebra_simps)
haftmann@66806
   284
  with div_mult_mod_eq show ?thesis by simp
haftmann@66806
   285
qed
haftmann@66806
   286
haftmann@66806
   287
lemma mod_mult_mult2:
haftmann@66806
   288
  "(a * c) mod (b * c) = (a mod b) * c"
haftmann@66806
   289
  using mod_mult_mult1 [of c a b] by (simp add: mult.commute)
haftmann@66806
   290
haftmann@66806
   291
lemma mult_mod_left: "(a mod b) * c = (a * c) mod (b * c)"
haftmann@66806
   292
  by (fact mod_mult_mult2 [symmetric])
haftmann@66806
   293
haftmann@66806
   294
lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)"
haftmann@66806
   295
  by (fact mod_mult_mult1 [symmetric])
haftmann@66806
   296
haftmann@66806
   297
lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
haftmann@66806
   298
  unfolding dvd_def by (auto simp add: mod_mult_mult1)
haftmann@66806
   299
haftmann@66806
   300
lemma div_plus_div_distrib_dvd_left:
haftmann@66806
   301
  "c dvd a \<Longrightarrow> (a + b) div c = a div c + b div c"
haftmann@66806
   302
  by (cases "c = 0") (auto elim: dvdE)
haftmann@66806
   303
haftmann@66806
   304
lemma div_plus_div_distrib_dvd_right:
haftmann@66806
   305
  "c dvd b \<Longrightarrow> (a + b) div c = a div c + b div c"
haftmann@66806
   306
  using div_plus_div_distrib_dvd_left [of c b a]
haftmann@66806
   307
  by (simp add: ac_simps)
haftmann@66806
   308
haftmann@66806
   309
named_theorems mod_simps
haftmann@66806
   310
haftmann@66806
   311
text \<open>Addition respects modular equivalence.\<close>
haftmann@66806
   312
haftmann@66806
   313
lemma mod_add_left_eq [mod_simps]:
haftmann@66806
   314
  "(a mod c + b) mod c = (a + b) mod c"
haftmann@66806
   315
proof -
haftmann@66806
   316
  have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
haftmann@66806
   317
    by (simp only: div_mult_mod_eq)
haftmann@66806
   318
  also have "\<dots> = (a mod c + b + a div c * c) mod c"
haftmann@66806
   319
    by (simp only: ac_simps)
haftmann@66806
   320
  also have "\<dots> = (a mod c + b) mod c"
haftmann@66806
   321
    by (rule mod_mult_self1)
haftmann@66806
   322
  finally show ?thesis
haftmann@66806
   323
    by (rule sym)
haftmann@66806
   324
qed
haftmann@66806
   325
haftmann@66806
   326
lemma mod_add_right_eq [mod_simps]:
haftmann@66806
   327
  "(a + b mod c) mod c = (a + b) mod c"
haftmann@66806
   328
  using mod_add_left_eq [of b c a] by (simp add: ac_simps)
haftmann@66806
   329
haftmann@66806
   330
lemma mod_add_eq:
haftmann@66806
   331
  "(a mod c + b mod c) mod c = (a + b) mod c"
haftmann@66806
   332
  by (simp add: mod_add_left_eq mod_add_right_eq)
haftmann@66806
   333
haftmann@66806
   334
lemma mod_sum_eq [mod_simps]:
haftmann@66806
   335
  "(\<Sum>i\<in>A. f i mod a) mod a = sum f A mod a"
haftmann@66806
   336
proof (induct A rule: infinite_finite_induct)
haftmann@66806
   337
  case (insert i A)
haftmann@66806
   338
  then have "(\<Sum>i\<in>insert i A. f i mod a) mod a
haftmann@66806
   339
    = (f i mod a + (\<Sum>i\<in>A. f i mod a)) mod a"
haftmann@66806
   340
    by simp
haftmann@66806
   341
  also have "\<dots> = (f i + (\<Sum>i\<in>A. f i mod a) mod a) mod a"
haftmann@66806
   342
    by (simp add: mod_simps)
haftmann@66806
   343
  also have "\<dots> = (f i + (\<Sum>i\<in>A. f i) mod a) mod a"
haftmann@66806
   344
    by (simp add: insert.hyps)
haftmann@66806
   345
  finally show ?case
haftmann@66806
   346
    by (simp add: insert.hyps mod_simps)
haftmann@66806
   347
qed simp_all
haftmann@66806
   348
haftmann@66806
   349
lemma mod_add_cong:
haftmann@66806
   350
  assumes "a mod c = a' mod c"
haftmann@66806
   351
  assumes "b mod c = b' mod c"
haftmann@66806
   352
  shows "(a + b) mod c = (a' + b') mod c"
haftmann@66806
   353
proof -
haftmann@66806
   354
  have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
haftmann@66806
   355
    unfolding assms ..
haftmann@66806
   356
  then show ?thesis
haftmann@66806
   357
    by (simp add: mod_add_eq)
haftmann@66806
   358
qed
haftmann@66806
   359
haftmann@66806
   360
text \<open>Multiplication respects modular equivalence.\<close>
haftmann@66806
   361
haftmann@66806
   362
lemma mod_mult_left_eq [mod_simps]:
haftmann@66806
   363
  "((a mod c) * b) mod c = (a * b) mod c"
haftmann@66806
   364
proof -
haftmann@66806
   365
  have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
haftmann@66806
   366
    by (simp only: div_mult_mod_eq)
haftmann@66806
   367
  also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
haftmann@66806
   368
    by (simp only: algebra_simps)
haftmann@66806
   369
  also have "\<dots> = (a mod c * b) mod c"
haftmann@66806
   370
    by (rule mod_mult_self1)
haftmann@66806
   371
  finally show ?thesis
haftmann@66806
   372
    by (rule sym)
haftmann@66806
   373
qed
haftmann@66806
   374
haftmann@66806
   375
lemma mod_mult_right_eq [mod_simps]:
haftmann@66806
   376
  "(a * (b mod c)) mod c = (a * b) mod c"
haftmann@66806
   377
  using mod_mult_left_eq [of b c a] by (simp add: ac_simps)
haftmann@66806
   378
haftmann@66806
   379
lemma mod_mult_eq:
haftmann@66806
   380
  "((a mod c) * (b mod c)) mod c = (a * b) mod c"
haftmann@66806
   381
  by (simp add: mod_mult_left_eq mod_mult_right_eq)
haftmann@66806
   382
haftmann@66806
   383
lemma mod_prod_eq [mod_simps]:
haftmann@66806
   384
  "(\<Prod>i\<in>A. f i mod a) mod a = prod f A mod a"
haftmann@66806
   385
proof (induct A rule: infinite_finite_induct)
haftmann@66806
   386
  case (insert i A)
haftmann@66806
   387
  then have "(\<Prod>i\<in>insert i A. f i mod a) mod a
haftmann@66806
   388
    = (f i mod a * (\<Prod>i\<in>A. f i mod a)) mod a"
haftmann@66806
   389
    by simp
haftmann@66806
   390
  also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i mod a) mod a)) mod a"
haftmann@66806
   391
    by (simp add: mod_simps)
haftmann@66806
   392
  also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i) mod a)) mod a"
haftmann@66806
   393
    by (simp add: insert.hyps)
haftmann@66806
   394
  finally show ?case
haftmann@66806
   395
    by (simp add: insert.hyps mod_simps)
haftmann@66806
   396
qed simp_all
haftmann@66806
   397
haftmann@66806
   398
lemma mod_mult_cong:
haftmann@66806
   399
  assumes "a mod c = a' mod c"
haftmann@66806
   400
  assumes "b mod c = b' mod c"
haftmann@66806
   401
  shows "(a * b) mod c = (a' * b') mod c"
haftmann@66806
   402
proof -
haftmann@66806
   403
  have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
haftmann@66806
   404
    unfolding assms ..
haftmann@66806
   405
  then show ?thesis
haftmann@66806
   406
    by (simp add: mod_mult_eq)
haftmann@66806
   407
qed
haftmann@66806
   408
haftmann@66806
   409
text \<open>Exponentiation respects modular equivalence.\<close>
haftmann@66806
   410
haftmann@66806
   411
lemma power_mod [mod_simps]: 
haftmann@66806
   412
  "((a mod b) ^ n) mod b = (a ^ n) mod b"
haftmann@66806
   413
proof (induct n)
haftmann@66806
   414
  case 0
haftmann@66806
   415
  then show ?case by simp
haftmann@66806
   416
next
haftmann@66806
   417
  case (Suc n)
haftmann@66806
   418
  have "(a mod b) ^ Suc n mod b = (a mod b) * ((a mod b) ^ n mod b) mod b"
haftmann@66806
   419
    by (simp add: mod_mult_right_eq)
haftmann@66806
   420
  with Suc show ?case
haftmann@66806
   421
    by (simp add: mod_mult_left_eq mod_mult_right_eq)
haftmann@66806
   422
qed
haftmann@66806
   423
haftmann@66806
   424
end
haftmann@66806
   425
haftmann@66806
   426
haftmann@66806
   427
class euclidean_ring_cancel = euclidean_ring + euclidean_semiring_cancel
haftmann@66806
   428
begin
haftmann@66806
   429
haftmann@66806
   430
subclass idom_divide ..
haftmann@66806
   431
haftmann@66806
   432
lemma div_minus_minus [simp]: "(- a) div (- b) = a div b"
haftmann@66806
   433
  using div_mult_mult1 [of "- 1" a b] by simp
haftmann@66806
   434
haftmann@66806
   435
lemma mod_minus_minus [simp]: "(- a) mod (- b) = - (a mod b)"
haftmann@66806
   436
  using mod_mult_mult1 [of "- 1" a b] by simp
haftmann@66806
   437
haftmann@66806
   438
lemma div_minus_right: "a div (- b) = (- a) div b"
haftmann@66806
   439
  using div_minus_minus [of "- a" b] by simp
haftmann@66806
   440
haftmann@66806
   441
lemma mod_minus_right: "a mod (- b) = - ((- a) mod b)"
haftmann@66806
   442
  using mod_minus_minus [of "- a" b] by simp
haftmann@66806
   443
haftmann@66806
   444
lemma div_minus1_right [simp]: "a div (- 1) = - a"
haftmann@66806
   445
  using div_minus_right [of a 1] by simp
haftmann@66806
   446
haftmann@66806
   447
lemma mod_minus1_right [simp]: "a mod (- 1) = 0"
haftmann@66806
   448
  using mod_minus_right [of a 1] by simp
haftmann@66806
   449
haftmann@66806
   450
text \<open>Negation respects modular equivalence.\<close>
haftmann@66806
   451
haftmann@66806
   452
lemma mod_minus_eq [mod_simps]:
haftmann@66806
   453
  "(- (a mod b)) mod b = (- a) mod b"
haftmann@66806
   454
proof -
haftmann@66806
   455
  have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
haftmann@66806
   456
    by (simp only: div_mult_mod_eq)
haftmann@66806
   457
  also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
haftmann@66806
   458
    by (simp add: ac_simps)
haftmann@66806
   459
  also have "\<dots> = (- (a mod b)) mod b"
haftmann@66806
   460
    by (rule mod_mult_self1)
haftmann@66806
   461
  finally show ?thesis
haftmann@66806
   462
    by (rule sym)
haftmann@66806
   463
qed
haftmann@66806
   464
haftmann@66806
   465
lemma mod_minus_cong:
haftmann@66806
   466
  assumes "a mod b = a' mod b"
haftmann@66806
   467
  shows "(- a) mod b = (- a') mod b"
haftmann@66806
   468
proof -
haftmann@66806
   469
  have "(- (a mod b)) mod b = (- (a' mod b)) mod b"
haftmann@66806
   470
    unfolding assms ..
haftmann@66806
   471
  then show ?thesis
haftmann@66806
   472
    by (simp add: mod_minus_eq)
haftmann@66806
   473
qed
haftmann@66806
   474
haftmann@66806
   475
text \<open>Subtraction respects modular equivalence.\<close>
haftmann@66806
   476
haftmann@66806
   477
lemma mod_diff_left_eq [mod_simps]:
haftmann@66806
   478
  "(a mod c - b) mod c = (a - b) mod c"
haftmann@66806
   479
  using mod_add_cong [of a c "a mod c" "- b" "- b"]
haftmann@66806
   480
  by simp
haftmann@66806
   481
haftmann@66806
   482
lemma mod_diff_right_eq [mod_simps]:
haftmann@66806
   483
  "(a - b mod c) mod c = (a - b) mod c"
haftmann@66806
   484
  using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
haftmann@66806
   485
  by simp
haftmann@66806
   486
haftmann@66806
   487
lemma mod_diff_eq:
haftmann@66806
   488
  "(a mod c - b mod c) mod c = (a - b) mod c"
haftmann@66806
   489
  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
   490
  by simp
haftmann@66806
   491
haftmann@66806
   492
lemma mod_diff_cong:
haftmann@66806
   493
  assumes "a mod c = a' mod c"
haftmann@66806
   494
  assumes "b mod c = b' mod c"
haftmann@66806
   495
  shows "(a - b) mod c = (a' - b') mod c"
haftmann@66806
   496
  using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"]
haftmann@66806
   497
  by simp
haftmann@66806
   498
haftmann@66806
   499
lemma minus_mod_self2 [simp]:
haftmann@66806
   500
  "(a - b) mod b = a mod b"
haftmann@66806
   501
  using mod_diff_right_eq [of a b b]
haftmann@66806
   502
  by (simp add: mod_diff_right_eq)
haftmann@66806
   503
haftmann@66806
   504
lemma minus_mod_self1 [simp]:
haftmann@66806
   505
  "(b - a) mod b = - a mod b"
haftmann@66806
   506
  using mod_add_self2 [of "- a" b] by simp
haftmann@66806
   507
haftmann@66806
   508
lemma mod_eq_dvd_iff:
haftmann@66806
   509
  "a mod c = b mod c \<longleftrightarrow> c dvd a - b" (is "?P \<longleftrightarrow> ?Q")
haftmann@66806
   510
proof
haftmann@66806
   511
  assume ?P
haftmann@66806
   512
  then have "(a mod c - b mod c) mod c = 0"
haftmann@66806
   513
    by simp
haftmann@66806
   514
  then show ?Q
haftmann@66806
   515
    by (simp add: dvd_eq_mod_eq_0 mod_simps)
haftmann@66806
   516
next
haftmann@66806
   517
  assume ?Q
haftmann@66806
   518
  then obtain d where d: "a - b = c * d" ..
haftmann@66806
   519
  then have "a = c * d + b"
haftmann@66806
   520
    by (simp add: algebra_simps)
haftmann@66806
   521
  then show ?P by simp
haftmann@66806
   522
qed
haftmann@66806
   523
haftmann@66837
   524
lemma mod_eqE:
haftmann@66837
   525
  assumes "a mod c = b mod c"
haftmann@66837
   526
  obtains d where "b = a + c * d"
haftmann@66837
   527
proof -
haftmann@66837
   528
  from assms have "c dvd a - b"
haftmann@66837
   529
    by (simp add: mod_eq_dvd_iff)
haftmann@66837
   530
  then obtain d where "a - b = c * d" ..
haftmann@66837
   531
  then have "b = a + c * - d"
haftmann@66837
   532
    by (simp add: algebra_simps)
haftmann@66837
   533
  with that show thesis .
haftmann@66837
   534
qed
haftmann@66837
   535
haftmann@66806
   536
end
haftmann@66806
   537
haftmann@66806
   538
  
haftmann@64785
   539
subsection \<open>Uniquely determined division\<close>
haftmann@64785
   540
  
haftmann@64785
   541
class unique_euclidean_semiring = euclidean_semiring + 
haftmann@66840
   542
  assumes euclidean_size_mult: "euclidean_size (a * b) = euclidean_size a * euclidean_size b"
haftmann@66838
   543
  fixes division_segment :: "'a \<Rightarrow> 'a"
haftmann@66839
   544
  assumes is_unit_division_segment [simp]: "is_unit (division_segment a)"
haftmann@66838
   545
    and division_segment_mult:
haftmann@66838
   546
    "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> division_segment (a * b) = division_segment a * division_segment b"
haftmann@66838
   547
    and division_segment_mod:
haftmann@66838
   548
    "b \<noteq> 0 \<Longrightarrow> \<not> b dvd a \<Longrightarrow> division_segment (a mod b) = division_segment b"
haftmann@64785
   549
  assumes div_bounded:
haftmann@66838
   550
    "b \<noteq> 0 \<Longrightarrow> division_segment r = division_segment b
haftmann@64785
   551
    \<Longrightarrow> euclidean_size r < euclidean_size b
haftmann@64785
   552
    \<Longrightarrow> (q * b + r) div b = q"
haftmann@64785
   553
begin
haftmann@64785
   554
haftmann@66839
   555
lemma division_segment_not_0 [simp]:
haftmann@66839
   556
  "division_segment a \<noteq> 0"
haftmann@66839
   557
  using is_unit_division_segment [of a] is_unitE [of "division_segment a"] by blast
haftmann@66839
   558
haftmann@64785
   559
lemma divmod_cases [case_names divides remainder by0]:
haftmann@64785
   560
  obtains 
haftmann@64785
   561
    (divides) q where "b \<noteq> 0"
haftmann@64785
   562
      and "a div b = q"
haftmann@64785
   563
      and "a mod b = 0"
haftmann@64785
   564
      and "a = q * b"
haftmann@66814
   565
  | (remainder) q r where "b \<noteq> 0"
haftmann@66838
   566
      and "division_segment r = division_segment b"
haftmann@64785
   567
      and "euclidean_size r < euclidean_size b"
haftmann@66814
   568
      and "r \<noteq> 0"
haftmann@64785
   569
      and "a div b = q"
haftmann@64785
   570
      and "a mod b = r"
haftmann@64785
   571
      and "a = q * b + r"
haftmann@64785
   572
  | (by0) "b = 0"
haftmann@64785
   573
proof (cases "b = 0")
haftmann@64785
   574
  case True
haftmann@64785
   575
  then show thesis
haftmann@64785
   576
  by (rule by0)
haftmann@64785
   577
next
haftmann@64785
   578
  case False
haftmann@64785
   579
  show thesis
haftmann@64785
   580
  proof (cases "b dvd a")
haftmann@64785
   581
    case True
haftmann@64785
   582
    then obtain q where "a = b * q" ..
haftmann@64785
   583
    with \<open>b \<noteq> 0\<close> divides
haftmann@64785
   584
    show thesis
haftmann@64785
   585
      by (simp add: ac_simps)
haftmann@64785
   586
  next
haftmann@64785
   587
    case False
haftmann@64785
   588
    then have "a mod b \<noteq> 0"
haftmann@64785
   589
      by (simp add: mod_eq_0_iff_dvd)
haftmann@66838
   590
    moreover from \<open>b \<noteq> 0\<close> \<open>\<not> b dvd a\<close> have "division_segment (a mod b) = division_segment b"
haftmann@66838
   591
      by (rule division_segment_mod)
haftmann@64785
   592
    moreover have "euclidean_size (a mod b) < euclidean_size b"
haftmann@64785
   593
      using \<open>b \<noteq> 0\<close> by (rule mod_size_less)
haftmann@64785
   594
    moreover have "a = a div b * b + a mod b"
haftmann@64785
   595
      by (simp add: div_mult_mod_eq)
haftmann@64785
   596
    ultimately show thesis
haftmann@66838
   597
      using \<open>b \<noteq> 0\<close> by (blast intro!: remainder)
haftmann@64785
   598
  qed
haftmann@64785
   599
qed
haftmann@64785
   600
haftmann@64785
   601
lemma div_eqI:
haftmann@66838
   602
  "a div b = q" if "b \<noteq> 0" "division_segment r = division_segment b"
haftmann@64785
   603
    "euclidean_size r < euclidean_size b" "q * b + r = a"
haftmann@64785
   604
proof -
haftmann@64785
   605
  from that have "(q * b + r) div b = q"
haftmann@64785
   606
    by (auto intro: div_bounded)
haftmann@64785
   607
  with that show ?thesis
haftmann@64785
   608
    by simp
haftmann@64785
   609
qed
haftmann@64785
   610
haftmann@64785
   611
lemma mod_eqI:
haftmann@66838
   612
  "a mod b = r" if "b \<noteq> 0" "division_segment r = division_segment b"
haftmann@64785
   613
    "euclidean_size r < euclidean_size b" "q * b + r = a" 
haftmann@64785
   614
proof -
haftmann@64785
   615
  from that have "a div b = q"
haftmann@64785
   616
    by (rule div_eqI)
haftmann@64785
   617
  moreover have "a div b * b + a mod b = a"
haftmann@64785
   618
    by (fact div_mult_mod_eq)
haftmann@64785
   619
  ultimately have "a div b * b + a mod b = a div b * b + r"
haftmann@64785
   620
    using \<open>q * b + r = a\<close> by simp
haftmann@64785
   621
  then show ?thesis
haftmann@64785
   622
    by simp
haftmann@64785
   623
qed
haftmann@64785
   624
haftmann@66806
   625
subclass euclidean_semiring_cancel
haftmann@66806
   626
proof
haftmann@66806
   627
  show "(a + c * b) div b = c + a div b" if "b \<noteq> 0" for a b c
haftmann@66806
   628
  proof (cases a b rule: divmod_cases)
haftmann@66806
   629
    case by0
haftmann@66806
   630
    with \<open>b \<noteq> 0\<close> show ?thesis
haftmann@66806
   631
      by simp
haftmann@66806
   632
  next
haftmann@66806
   633
    case (divides q)
haftmann@66806
   634
    then show ?thesis
haftmann@66806
   635
      by (simp add: ac_simps)
haftmann@66806
   636
  next
haftmann@66806
   637
    case (remainder q r)
haftmann@66806
   638
    then show ?thesis
haftmann@66806
   639
      by (auto intro: div_eqI simp add: algebra_simps)
haftmann@66806
   640
  qed
haftmann@66806
   641
next
haftmann@66806
   642
  show"(c * a) div (c * b) = a div b" if "c \<noteq> 0" for a b c
haftmann@66806
   643
  proof (cases a b rule: divmod_cases)
haftmann@66806
   644
    case by0
haftmann@66806
   645
    then show ?thesis
haftmann@66806
   646
      by simp
haftmann@66806
   647
  next
haftmann@66806
   648
    case (divides q)
haftmann@66806
   649
    with \<open>c \<noteq> 0\<close> show ?thesis
haftmann@66806
   650
      by (simp add: mult.left_commute [of c])
haftmann@66806
   651
  next
haftmann@66806
   652
    case (remainder q r)
haftmann@66806
   653
    from \<open>b \<noteq> 0\<close> \<open>c \<noteq> 0\<close> have "b * c \<noteq> 0"
haftmann@66806
   654
      by simp
haftmann@66806
   655
    from remainder \<open>c \<noteq> 0\<close>
haftmann@66838
   656
    have "division_segment (r * c) = division_segment (b * c)"
haftmann@66806
   657
      and "euclidean_size (r * c) < euclidean_size (b * c)"
haftmann@66840
   658
      by (simp_all add: division_segment_mult division_segment_mod euclidean_size_mult)
haftmann@66806
   659
    with remainder show ?thesis
haftmann@66806
   660
      by (auto intro!: div_eqI [of _ "c * (a mod b)"] simp add: algebra_simps)
haftmann@66806
   661
        (use \<open>b * c \<noteq> 0\<close> in simp)
haftmann@66806
   662
  qed
haftmann@66806
   663
qed
haftmann@66806
   664
haftmann@66814
   665
lemma div_mult1_eq:
haftmann@66814
   666
  "(a * b) div c = a * (b div c) + a * (b mod c) div c"
haftmann@66814
   667
proof (cases "a * (b mod c)" c rule: divmod_cases)
haftmann@66814
   668
  case (divides q)
haftmann@66814
   669
  have "a * b = a * (b div c * c + b mod c)"
haftmann@66814
   670
    by (simp add: div_mult_mod_eq)
haftmann@66814
   671
  also have "\<dots> = (a * (b div c) + q) * c"
haftmann@66814
   672
    using divides by (simp add: algebra_simps)
haftmann@66814
   673
  finally have "(a * b) div c = \<dots> div c"
haftmann@66814
   674
    by simp
haftmann@66814
   675
  with divides show ?thesis
haftmann@66814
   676
    by simp
haftmann@66814
   677
next
haftmann@66814
   678
  case (remainder q r)
haftmann@66814
   679
  from remainder(1-3) show ?thesis
haftmann@66814
   680
  proof (rule div_eqI)
haftmann@66814
   681
    have "a * b = a * (b div c * c + b mod c)"
haftmann@66814
   682
      by (simp add: div_mult_mod_eq)
haftmann@66814
   683
    also have "\<dots> = a * c * (b div c) + q * c + r"
haftmann@66814
   684
      using remainder by (simp add: algebra_simps)
haftmann@66814
   685
    finally show "(a * (b div c) + a * (b mod c) div c) * c + r = a * b"
haftmann@66814
   686
      using remainder(5-7) by (simp add: algebra_simps)
haftmann@66814
   687
  qed
haftmann@66814
   688
next
haftmann@66814
   689
  case by0
haftmann@66814
   690
  then show ?thesis
haftmann@66814
   691
    by simp
haftmann@66814
   692
qed
haftmann@66814
   693
haftmann@66814
   694
lemma div_add1_eq:
haftmann@66814
   695
  "(a + b) div c = a div c + b div c + (a mod c + b mod c) div c"
haftmann@66814
   696
proof (cases "a mod c + b mod c" c rule: divmod_cases)
haftmann@66814
   697
  case (divides q)
haftmann@66814
   698
  have "a + b = (a div c * c + a mod c) + (b div c * c + b mod c)"
haftmann@66814
   699
    using mod_mult_div_eq [of a c] mod_mult_div_eq [of b c] by (simp add: ac_simps)
haftmann@66814
   700
  also have "\<dots> = (a div c + b div c) * c + (a mod c + b mod c)"
haftmann@66814
   701
    by (simp add: algebra_simps)
haftmann@66814
   702
  also have "\<dots> = (a div c + b div c + q) * c"
haftmann@66814
   703
    using divides by (simp add: algebra_simps)
haftmann@66814
   704
  finally have "(a + b) div c = (a div c + b div c + q) * c div c"
haftmann@66814
   705
    by simp
haftmann@66814
   706
  with divides show ?thesis
haftmann@66814
   707
    by simp
haftmann@66814
   708
next
haftmann@66814
   709
  case (remainder q r)
haftmann@66814
   710
  from remainder(1-3) show ?thesis
haftmann@66814
   711
  proof (rule div_eqI)
haftmann@66814
   712
    have "(a div c + b div c + q) * c + r + (a mod c + b mod c) =
haftmann@66814
   713
        (a div c * c + a mod c) + (b div c * c + b mod c) + q * c + r"
haftmann@66814
   714
      by (simp add: algebra_simps)
haftmann@66814
   715
    also have "\<dots> = a + b + (a mod c + b mod c)"
haftmann@66814
   716
      by (simp add: div_mult_mod_eq remainder) (simp add: ac_simps)
haftmann@66814
   717
    finally show "(a div c + b div c + (a mod c + b mod c) div c) * c + r = a + b"
haftmann@66814
   718
      using remainder by simp
haftmann@66814
   719
  qed
haftmann@66814
   720
next
haftmann@66814
   721
  case by0
haftmann@66814
   722
  then show ?thesis
haftmann@66814
   723
    by simp
haftmann@66814
   724
qed
haftmann@66814
   725
haftmann@66886
   726
lemma div_eq_0_iff:
haftmann@66886
   727
  "a div b = 0 \<longleftrightarrow> euclidean_size a < euclidean_size b \<or> b = 0" (is "_ \<longleftrightarrow> ?P")
haftmann@66886
   728
  if "division_segment a = division_segment b"
haftmann@66886
   729
proof
haftmann@66886
   730
  assume ?P
haftmann@66886
   731
  with that show "a div b = 0"
haftmann@66886
   732
    by (cases "b = 0") (auto intro: div_eqI)
haftmann@66886
   733
next
haftmann@66886
   734
  assume "a div b = 0"
haftmann@66886
   735
  then have "a mod b = a"
haftmann@66886
   736
    using div_mult_mod_eq [of a b] by simp
haftmann@66886
   737
  with mod_size_less [of b a] show ?P
haftmann@66886
   738
    by auto
haftmann@66886
   739
qed
haftmann@66886
   740
haftmann@64785
   741
end
haftmann@64785
   742
haftmann@64785
   743
class unique_euclidean_ring = euclidean_ring + unique_euclidean_semiring
haftmann@66806
   744
begin
haftmann@66806
   745
  
haftmann@66806
   746
subclass euclidean_ring_cancel ..
haftmann@64785
   747
haftmann@64785
   748
end
haftmann@66806
   749
haftmann@66808
   750
haftmann@66808
   751
subsection \<open>Euclidean division on @{typ nat}\<close>
haftmann@66808
   752
haftmann@66816
   753
instantiation nat :: normalization_semidom
haftmann@66808
   754
begin
haftmann@66808
   755
haftmann@66808
   756
definition normalize_nat :: "nat \<Rightarrow> nat"
haftmann@66808
   757
  where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
haftmann@66808
   758
haftmann@66808
   759
definition unit_factor_nat :: "nat \<Rightarrow> nat"
haftmann@66808
   760
  where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
haftmann@66808
   761
haftmann@66808
   762
lemma unit_factor_simps [simp]:
haftmann@66808
   763
  "unit_factor 0 = (0::nat)"
haftmann@66808
   764
  "unit_factor (Suc n) = 1"
haftmann@66808
   765
  by (simp_all add: unit_factor_nat_def)
haftmann@66808
   766
haftmann@66816
   767
definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
haftmann@66816
   768
  where "m div n = (if n = 0 then 0 else Max {k::nat. k * n \<le> m})"
haftmann@66816
   769
haftmann@66816
   770
instance
haftmann@66816
   771
  by standard (auto simp add: divide_nat_def ac_simps unit_factor_nat_def intro: Max_eqI)
haftmann@66816
   772
haftmann@66816
   773
end
haftmann@66816
   774
haftmann@66816
   775
instantiation nat :: unique_euclidean_semiring
haftmann@66816
   776
begin
haftmann@66816
   777
haftmann@66808
   778
definition euclidean_size_nat :: "nat \<Rightarrow> nat"
haftmann@66808
   779
  where [simp]: "euclidean_size_nat = id"
haftmann@66808
   780
haftmann@66838
   781
definition division_segment_nat :: "nat \<Rightarrow> nat"
haftmann@66838
   782
  where [simp]: "division_segment_nat n = 1"
haftmann@66808
   783
haftmann@66808
   784
definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
haftmann@66808
   785
  where "m mod n = m - (m div n * (n::nat))"
haftmann@66808
   786
haftmann@66808
   787
instance proof
haftmann@66808
   788
  fix m n :: nat
haftmann@66808
   789
  have ex: "\<exists>k. k * n \<le> l" for l :: nat
haftmann@66808
   790
    by (rule exI [of _ 0]) simp
haftmann@66808
   791
  have fin: "finite {k. k * n \<le> l}" if "n > 0" for l
haftmann@66808
   792
  proof -
haftmann@66808
   793
    from that have "{k. k * n \<le> l} \<subseteq> {k. k \<le> l}"
haftmann@66808
   794
      by (cases n) auto
haftmann@66808
   795
    then show ?thesis
haftmann@66808
   796
      by (rule finite_subset) simp
haftmann@66808
   797
  qed
haftmann@66808
   798
  have mult_div_unfold: "n * (m div n) = Max {l. l \<le> m \<and> n dvd l}"
haftmann@66808
   799
  proof (cases "n = 0")
haftmann@66808
   800
    case True
haftmann@66808
   801
    moreover have "{l. l = 0 \<and> l \<le> m} = {0::nat}"
haftmann@66808
   802
      by auto
haftmann@66808
   803
    ultimately show ?thesis
haftmann@66808
   804
      by simp
haftmann@66808
   805
  next
haftmann@66808
   806
    case False
haftmann@66808
   807
    with ex [of m] fin have "n * Max {k. k * n \<le> m} = Max (times n ` {k. k * n \<le> m})"
haftmann@66808
   808
      by (auto simp add: nat_mult_max_right intro: hom_Max_commute)
haftmann@66808
   809
    also have "times n ` {k. k * n \<le> m} = {l. l \<le> m \<and> n dvd l}"
haftmann@66808
   810
      by (auto simp add: ac_simps elim!: dvdE)
haftmann@66808
   811
    finally show ?thesis
haftmann@66808
   812
      using False by (simp add: divide_nat_def ac_simps)
haftmann@66808
   813
  qed
haftmann@66808
   814
  have less_eq: "m div n * n \<le> m"
haftmann@66808
   815
    by (auto simp add: mult_div_unfold ac_simps intro: Max.boundedI)
haftmann@66808
   816
  then show "m div n * n + m mod n = m"
haftmann@66808
   817
    by (simp add: modulo_nat_def)
haftmann@66808
   818
  assume "n \<noteq> 0" 
haftmann@66808
   819
  show "euclidean_size (m mod n) < euclidean_size n"
haftmann@66808
   820
  proof -
haftmann@66808
   821
    have "m < Suc (m div n) * n"
haftmann@66808
   822
    proof (rule ccontr)
haftmann@66808
   823
      assume "\<not> m < Suc (m div n) * n"
haftmann@66808
   824
      then have "Suc (m div n) * n \<le> m"
haftmann@66808
   825
        by (simp add: not_less)
haftmann@66808
   826
      moreover from \<open>n \<noteq> 0\<close> have "Max {k. k * n \<le> m} < Suc (m div n)"
haftmann@66808
   827
        by (simp add: divide_nat_def)
haftmann@66808
   828
      with \<open>n \<noteq> 0\<close> ex fin have "\<And>k. k * n \<le> m \<Longrightarrow> k < Suc (m div n)"
haftmann@66808
   829
        by auto
haftmann@66808
   830
      ultimately have "Suc (m div n) < Suc (m div n)"
haftmann@66808
   831
        by blast
haftmann@66808
   832
      then show False
haftmann@66808
   833
        by simp
haftmann@66808
   834
    qed
haftmann@66808
   835
    with \<open>n \<noteq> 0\<close> show ?thesis
haftmann@66808
   836
      by (simp add: modulo_nat_def)
haftmann@66808
   837
  qed
haftmann@66808
   838
  show "euclidean_size m \<le> euclidean_size (m * n)"
haftmann@66808
   839
    using \<open>n \<noteq> 0\<close> by (cases n) simp_all
haftmann@66808
   840
  fix q r :: nat
haftmann@66808
   841
  show "(q * n + r) div n = q" if "euclidean_size r < euclidean_size n"
haftmann@66808
   842
  proof -
haftmann@66808
   843
    from that have "r < n"
haftmann@66808
   844
      by simp
haftmann@66808
   845
    have "k \<le> q" if "k * n \<le> q * n + r" for k
haftmann@66808
   846
    proof (rule ccontr)
haftmann@66808
   847
      assume "\<not> k \<le> q"
haftmann@66808
   848
      then have "q < k"
haftmann@66808
   849
        by simp
haftmann@66808
   850
      then obtain l where "k = Suc (q + l)"
haftmann@66808
   851
        by (auto simp add: less_iff_Suc_add)
haftmann@66808
   852
      with \<open>r < n\<close> that show False
haftmann@66808
   853
        by (simp add: algebra_simps)
haftmann@66808
   854
    qed
haftmann@66808
   855
    with \<open>n \<noteq> 0\<close> ex fin show ?thesis
haftmann@66808
   856
      by (auto simp add: divide_nat_def Max_eq_iff)
haftmann@66808
   857
  qed
haftmann@66816
   858
qed simp_all
haftmann@66808
   859
haftmann@66806
   860
end
haftmann@66808
   861
haftmann@66808
   862
text \<open>Tool support\<close>
haftmann@66808
   863
haftmann@66808
   864
ML \<open>
haftmann@66808
   865
structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
haftmann@66808
   866
(
haftmann@66808
   867
  val div_name = @{const_name divide};
haftmann@66808
   868
  val mod_name = @{const_name modulo};
haftmann@66808
   869
  val mk_binop = HOLogic.mk_binop;
haftmann@66808
   870
  val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
haftmann@66813
   871
  val mk_sum = Arith_Data.mk_sum;
haftmann@66808
   872
  fun dest_sum tm =
haftmann@66808
   873
    if HOLogic.is_zero tm then []
haftmann@66808
   874
    else
haftmann@66808
   875
      (case try HOLogic.dest_Suc tm of
haftmann@66808
   876
        SOME t => HOLogic.Suc_zero :: dest_sum t
haftmann@66808
   877
      | NONE =>
haftmann@66808
   878
          (case try dest_plus tm of
haftmann@66808
   879
            SOME (t, u) => dest_sum t @ dest_sum u
haftmann@66808
   880
          | NONE => [tm]));
haftmann@66808
   881
haftmann@66808
   882
  val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
haftmann@66808
   883
haftmann@66808
   884
  val prove_eq_sums = Arith_Data.prove_conv2 all_tac
haftmann@66808
   885
    (Arith_Data.simp_all_tac @{thms add_0_left add_0_right ac_simps})
haftmann@66808
   886
)
haftmann@66808
   887
\<close>
haftmann@66808
   888
haftmann@66808
   889
simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
haftmann@66808
   890
  \<open>K Cancel_Div_Mod_Nat.proc\<close>
haftmann@66808
   891
haftmann@66808
   892
lemma div_nat_eqI:
haftmann@66808
   893
  "m div n = q" if "n * q \<le> m" and "m < n * Suc q" for m n q :: nat
haftmann@66808
   894
  by (rule div_eqI [of _ "m - n * q"]) (use that in \<open>simp_all add: algebra_simps\<close>)
haftmann@66808
   895
haftmann@66808
   896
lemma mod_nat_eqI:
haftmann@66808
   897
  "m mod n = r" if "r < n" and "r \<le> m" and "n dvd m - r" for m n r :: nat
haftmann@66808
   898
  by (rule mod_eqI [of _ _ "(m - r) div n"]) (use that in \<open>simp_all add: algebra_simps\<close>)
haftmann@66808
   899
haftmann@66808
   900
lemma div_mult_self_is_m [simp]:
haftmann@66808
   901
  "m * n div n = m" if "n > 0" for m n :: nat
haftmann@66808
   902
  using that by simp
haftmann@66808
   903
haftmann@66808
   904
lemma div_mult_self1_is_m [simp]:
haftmann@66808
   905
  "n * m div n = m" if "n > 0" for m n :: nat
haftmann@66808
   906
  using that by simp
haftmann@66808
   907
haftmann@66808
   908
lemma mod_less_divisor [simp]:
haftmann@66808
   909
  "m mod n < n" if "n > 0" for m n :: nat
haftmann@66808
   910
  using mod_size_less [of n m] that by simp
haftmann@66808
   911
haftmann@66808
   912
lemma mod_le_divisor [simp]:
haftmann@66808
   913
  "m mod n \<le> n" if "n > 0" for m n :: nat
haftmann@66808
   914
  using that by (auto simp add: le_less)
haftmann@66808
   915
haftmann@66808
   916
lemma div_times_less_eq_dividend [simp]:
haftmann@66808
   917
  "m div n * n \<le> m" for m n :: nat
haftmann@66808
   918
  by (simp add: minus_mod_eq_div_mult [symmetric])
haftmann@66808
   919
haftmann@66808
   920
lemma times_div_less_eq_dividend [simp]:
haftmann@66808
   921
  "n * (m div n) \<le> m" for m n :: nat
haftmann@66808
   922
  using div_times_less_eq_dividend [of m n]
haftmann@66808
   923
  by (simp add: ac_simps)
haftmann@66808
   924
haftmann@66808
   925
lemma dividend_less_div_times:
haftmann@66808
   926
  "m < n + (m div n) * n" if "0 < n" for m n :: nat
haftmann@66808
   927
proof -
haftmann@66808
   928
  from that have "m mod n < n"
haftmann@66808
   929
    by simp
haftmann@66808
   930
  then show ?thesis
haftmann@66808
   931
    by (simp add: minus_mod_eq_div_mult [symmetric])
haftmann@66808
   932
qed
haftmann@66808
   933
haftmann@66808
   934
lemma dividend_less_times_div:
haftmann@66808
   935
  "m < n + n * (m div n)" if "0 < n" for m n :: nat
haftmann@66808
   936
  using dividend_less_div_times [of n m] that
haftmann@66808
   937
  by (simp add: ac_simps)
haftmann@66808
   938
haftmann@66808
   939
lemma mod_Suc_le_divisor [simp]:
haftmann@66808
   940
  "m mod Suc n \<le> n"
haftmann@66808
   941
  using mod_less_divisor [of "Suc n" m] by arith
haftmann@66808
   942
haftmann@66808
   943
lemma mod_less_eq_dividend [simp]:
haftmann@66808
   944
  "m mod n \<le> m" for m n :: nat
haftmann@66808
   945
proof (rule add_leD2)
haftmann@66808
   946
  from div_mult_mod_eq have "m div n * n + m mod n = m" .
haftmann@66808
   947
  then show "m div n * n + m mod n \<le> m" by auto
haftmann@66808
   948
qed
haftmann@66808
   949
haftmann@66808
   950
lemma
haftmann@66808
   951
  div_less [simp]: "m div n = 0"
haftmann@66808
   952
  and mod_less [simp]: "m mod n = m"
haftmann@66808
   953
  if "m < n" for m n :: nat
haftmann@66808
   954
  using that by (auto intro: div_eqI mod_eqI) 
haftmann@66808
   955
haftmann@66808
   956
lemma le_div_geq:
haftmann@66808
   957
  "m div n = Suc ((m - n) div n)" if "0 < n" and "n \<le> m" for m n :: nat
haftmann@66808
   958
proof -
haftmann@66808
   959
  from \<open>n \<le> m\<close> obtain q where "m = n + q"
haftmann@66808
   960
    by (auto simp add: le_iff_add)
haftmann@66808
   961
  with \<open>0 < n\<close> show ?thesis
haftmann@66808
   962
    by (simp add: div_add_self1)
haftmann@66808
   963
qed
haftmann@66808
   964
haftmann@66808
   965
lemma le_mod_geq:
haftmann@66808
   966
  "m mod n = (m - n) mod n" if "n \<le> m" for m n :: nat
haftmann@66808
   967
proof -
haftmann@66808
   968
  from \<open>n \<le> m\<close> obtain q where "m = n + q"
haftmann@66808
   969
    by (auto simp add: le_iff_add)
haftmann@66808
   970
  then show ?thesis
haftmann@66808
   971
    by simp
haftmann@66808
   972
qed
haftmann@66808
   973
haftmann@66808
   974
lemma div_if:
haftmann@66808
   975
  "m div n = (if m < n \<or> n = 0 then 0 else Suc ((m - n) div n))"
haftmann@66808
   976
  by (simp add: le_div_geq)
haftmann@66808
   977
haftmann@66808
   978
lemma mod_if:
haftmann@66808
   979
  "m mod n = (if m < n then m else (m - n) mod n)" for m n :: nat
haftmann@66808
   980
  by (simp add: le_mod_geq)
haftmann@66808
   981
haftmann@66808
   982
lemma div_eq_0_iff:
haftmann@66808
   983
  "m div n = 0 \<longleftrightarrow> m < n \<or> n = 0" for m n :: nat
haftmann@66886
   984
  by (simp add: div_eq_0_iff)
haftmann@66808
   985
haftmann@66808
   986
lemma div_greater_zero_iff:
haftmann@66808
   987
  "m div n > 0 \<longleftrightarrow> n \<le> m \<and> n > 0" for m n :: nat
haftmann@66808
   988
  using div_eq_0_iff [of m n] by auto
haftmann@66808
   989
haftmann@66808
   990
lemma mod_greater_zero_iff_not_dvd:
haftmann@66808
   991
  "m mod n > 0 \<longleftrightarrow> \<not> n dvd m" for m n :: nat
haftmann@66808
   992
  by (simp add: dvd_eq_mod_eq_0)
haftmann@66808
   993
haftmann@66808
   994
lemma div_by_Suc_0 [simp]:
haftmann@66808
   995
  "m div Suc 0 = m"
haftmann@66808
   996
  using div_by_1 [of m] by simp
haftmann@66808
   997
haftmann@66808
   998
lemma mod_by_Suc_0 [simp]:
haftmann@66808
   999
  "m mod Suc 0 = 0"
haftmann@66808
  1000
  using mod_by_1 [of m] by simp
haftmann@66808
  1001
haftmann@66808
  1002
lemma div2_Suc_Suc [simp]:
haftmann@66808
  1003
  "Suc (Suc m) div 2 = Suc (m div 2)"
haftmann@66808
  1004
  by (simp add: numeral_2_eq_2 le_div_geq)
haftmann@66808
  1005
haftmann@66808
  1006
lemma Suc_n_div_2_gt_zero [simp]:
haftmann@66808
  1007
  "0 < Suc n div 2" if "n > 0" for n :: nat
haftmann@66808
  1008
  using that by (cases n) simp_all
haftmann@66808
  1009
haftmann@66808
  1010
lemma div_2_gt_zero [simp]:
haftmann@66808
  1011
  "0 < n div 2" if "Suc 0 < n" for n :: nat
haftmann@66808
  1012
  using that Suc_n_div_2_gt_zero [of "n - 1"] by simp
haftmann@66808
  1013
haftmann@66808
  1014
lemma mod2_Suc_Suc [simp]:
haftmann@66808
  1015
  "Suc (Suc m) mod 2 = m mod 2"
haftmann@66808
  1016
  by (simp add: numeral_2_eq_2 le_mod_geq)
haftmann@66808
  1017
haftmann@66808
  1018
lemma add_self_div_2 [simp]:
haftmann@66808
  1019
  "(m + m) div 2 = m" for m :: nat
haftmann@66808
  1020
  by (simp add: mult_2 [symmetric])
haftmann@66808
  1021
haftmann@66808
  1022
lemma add_self_mod_2 [simp]:
haftmann@66808
  1023
  "(m + m) mod 2 = 0" for m :: nat
haftmann@66808
  1024
  by (simp add: mult_2 [symmetric])
haftmann@66808
  1025
haftmann@66808
  1026
lemma mod2_gr_0 [simp]:
haftmann@66808
  1027
  "0 < m mod 2 \<longleftrightarrow> m mod 2 = 1" for m :: nat
haftmann@66808
  1028
proof -
haftmann@66808
  1029
  have "m mod 2 < 2"
haftmann@66808
  1030
    by (rule mod_less_divisor) simp
haftmann@66808
  1031
  then have "m mod 2 = 0 \<or> m mod 2 = 1"
haftmann@66808
  1032
    by arith
haftmann@66808
  1033
  then show ?thesis
haftmann@66808
  1034
    by auto     
haftmann@66808
  1035
qed
haftmann@66808
  1036
haftmann@66808
  1037
lemma mod_Suc_eq [mod_simps]:
haftmann@66808
  1038
  "Suc (m mod n) mod n = Suc m mod n"
haftmann@66808
  1039
proof -
haftmann@66808
  1040
  have "(m mod n + 1) mod n = (m + 1) mod n"
haftmann@66808
  1041
    by (simp only: mod_simps)
haftmann@66808
  1042
  then show ?thesis
haftmann@66808
  1043
    by simp
haftmann@66808
  1044
qed
haftmann@66808
  1045
haftmann@66808
  1046
lemma mod_Suc_Suc_eq [mod_simps]:
haftmann@66808
  1047
  "Suc (Suc (m mod n)) mod n = Suc (Suc m) mod n"
haftmann@66808
  1048
proof -
haftmann@66808
  1049
  have "(m mod n + 2) mod n = (m + 2) mod n"
haftmann@66808
  1050
    by (simp only: mod_simps)
haftmann@66808
  1051
  then show ?thesis
haftmann@66808
  1052
    by simp
haftmann@66808
  1053
qed
haftmann@66808
  1054
haftmann@66808
  1055
lemma
haftmann@66808
  1056
  Suc_mod_mult_self1 [simp]: "Suc (m + k * n) mod n = Suc m mod n"
haftmann@66808
  1057
  and Suc_mod_mult_self2 [simp]: "Suc (m + n * k) mod n = Suc m mod n"
haftmann@66808
  1058
  and Suc_mod_mult_self3 [simp]: "Suc (k * n + m) mod n = Suc m mod n"
haftmann@66808
  1059
  and Suc_mod_mult_self4 [simp]: "Suc (n * k + m) mod n = Suc m mod n"
haftmann@66808
  1060
  by (subst mod_Suc_eq [symmetric], simp add: mod_simps)+
haftmann@66808
  1061
haftmann@66808
  1062
context
haftmann@66808
  1063
  fixes m n q :: nat
haftmann@66808
  1064
begin
haftmann@66808
  1065
haftmann@66808
  1066
private lemma eucl_rel_mult2:
haftmann@66808
  1067
  "m mod n + n * (m div n mod q) < n * q"
haftmann@66808
  1068
  if "n > 0" and "q > 0"
haftmann@66808
  1069
proof -
haftmann@66808
  1070
  from \<open>n > 0\<close> have "m mod n < n"
haftmann@66808
  1071
    by (rule mod_less_divisor)
haftmann@66808
  1072
  from \<open>q > 0\<close> have "m div n mod q < q"
haftmann@66808
  1073
    by (rule mod_less_divisor)
haftmann@66808
  1074
  then obtain s where "q = Suc (m div n mod q + s)"
haftmann@66808
  1075
    by (blast dest: less_imp_Suc_add)
haftmann@66808
  1076
  moreover have "m mod n + n * (m div n mod q) < n * Suc (m div n mod q + s)"
haftmann@66808
  1077
    using \<open>m mod n < n\<close> by (simp add: add_mult_distrib2)
haftmann@66808
  1078
  ultimately show ?thesis
haftmann@66808
  1079
    by simp
haftmann@66808
  1080
qed
haftmann@66808
  1081
haftmann@66808
  1082
lemma div_mult2_eq:
haftmann@66808
  1083
  "m div (n * q) = (m div n) div q"
haftmann@66808
  1084
proof (cases "n = 0 \<or> q = 0")
haftmann@66808
  1085
  case True
haftmann@66808
  1086
  then show ?thesis
haftmann@66808
  1087
    by auto
haftmann@66808
  1088
next
haftmann@66808
  1089
  case False
haftmann@66808
  1090
  with eucl_rel_mult2 show ?thesis
haftmann@66808
  1091
    by (auto intro: div_eqI [of _ "n * (m div n mod q) + m mod n"]
haftmann@66808
  1092
      simp add: algebra_simps add_mult_distrib2 [symmetric])
haftmann@66808
  1093
qed
haftmann@66808
  1094
haftmann@66808
  1095
lemma mod_mult2_eq:
haftmann@66808
  1096
  "m mod (n * q) = n * (m div n mod q) + m mod n"
haftmann@66808
  1097
proof (cases "n = 0 \<or> q = 0")
haftmann@66808
  1098
  case True
haftmann@66808
  1099
  then show ?thesis
haftmann@66808
  1100
    by auto
haftmann@66808
  1101
next
haftmann@66808
  1102
  case False
haftmann@66808
  1103
  with eucl_rel_mult2 show ?thesis
haftmann@66808
  1104
    by (auto intro: mod_eqI [of _ _ "(m div n) div q"]
haftmann@66808
  1105
      simp add: algebra_simps add_mult_distrib2 [symmetric])
haftmann@66808
  1106
qed
haftmann@66808
  1107
haftmann@66808
  1108
end
haftmann@66808
  1109
haftmann@66808
  1110
lemma div_le_mono:
haftmann@66808
  1111
  "m div k \<le> n div k" if "m \<le> n" for m n k :: nat
haftmann@66808
  1112
proof -
haftmann@66808
  1113
  from that obtain q where "n = m + q"
haftmann@66808
  1114
    by (auto simp add: le_iff_add)
haftmann@66808
  1115
  then show ?thesis
haftmann@66808
  1116
    by (simp add: div_add1_eq [of m q k])
haftmann@66808
  1117
qed
haftmann@66808
  1118
haftmann@66808
  1119
text \<open>Antimonotonicity of @{const divide} in second argument\<close>
haftmann@66808
  1120
haftmann@66808
  1121
lemma div_le_mono2:
haftmann@66808
  1122
  "k div n \<le> k div m" if "0 < m" and "m \<le> n" for m n k :: nat
haftmann@66808
  1123
using that proof (induct k arbitrary: m rule: less_induct)
haftmann@66808
  1124
  case (less k)
haftmann@66808
  1125
  show ?case
haftmann@66808
  1126
  proof (cases "n \<le> k")
haftmann@66808
  1127
    case False
haftmann@66808
  1128
    then show ?thesis
haftmann@66808
  1129
      by simp
haftmann@66808
  1130
  next
haftmann@66808
  1131
    case True
haftmann@66808
  1132
    have "(k - n) div n \<le> (k - m) div n"
haftmann@66808
  1133
      using less.prems
haftmann@66808
  1134
      by (blast intro: div_le_mono diff_le_mono2)
haftmann@66808
  1135
    also have "\<dots> \<le> (k - m) div m"
haftmann@66808
  1136
      using \<open>n \<le> k\<close> less.prems less.hyps [of "k - m" m]
haftmann@66808
  1137
      by simp
haftmann@66808
  1138
    finally show ?thesis
haftmann@66808
  1139
      using \<open>n \<le> k\<close> less.prems
haftmann@66808
  1140
      by (simp add: le_div_geq)
haftmann@66808
  1141
  qed
haftmann@66808
  1142
qed
haftmann@66808
  1143
haftmann@66808
  1144
lemma div_le_dividend [simp]:
haftmann@66808
  1145
  "m div n \<le> m" for m n :: nat
haftmann@66808
  1146
  using div_le_mono2 [of 1 n m] by (cases "n = 0") simp_all
haftmann@66808
  1147
haftmann@66808
  1148
lemma div_less_dividend [simp]:
haftmann@66808
  1149
  "m div n < m" if "1 < n" and "0 < m" for m n :: nat
haftmann@66808
  1150
using that proof (induct m rule: less_induct)
haftmann@66808
  1151
  case (less m)
haftmann@66808
  1152
  show ?case
haftmann@66808
  1153
  proof (cases "n < m")
haftmann@66808
  1154
    case False
haftmann@66808
  1155
    with less show ?thesis
haftmann@66808
  1156
      by (cases "n = m") simp_all
haftmann@66808
  1157
  next
haftmann@66808
  1158
    case True
haftmann@66808
  1159
    then show ?thesis
haftmann@66808
  1160
      using less.hyps [of "m - n"] less.prems
haftmann@66808
  1161
      by (simp add: le_div_geq)
haftmann@66808
  1162
  qed
haftmann@66808
  1163
qed
haftmann@66808
  1164
haftmann@66808
  1165
lemma div_eq_dividend_iff:
haftmann@66808
  1166
  "m div n = m \<longleftrightarrow> n = 1" if "m > 0" for m n :: nat
haftmann@66808
  1167
proof
haftmann@66808
  1168
  assume "n = 1"
haftmann@66808
  1169
  then show "m div n = m"
haftmann@66808
  1170
    by simp
haftmann@66808
  1171
next
haftmann@66808
  1172
  assume P: "m div n = m"
haftmann@66808
  1173
  show "n = 1"
haftmann@66808
  1174
  proof (rule ccontr)
haftmann@66808
  1175
    have "n \<noteq> 0"
haftmann@66808
  1176
      by (rule ccontr) (use that P in auto)
haftmann@66808
  1177
    moreover assume "n \<noteq> 1"
haftmann@66808
  1178
    ultimately have "n > 1"
haftmann@66808
  1179
      by simp
haftmann@66808
  1180
    with that have "m div n < m"
haftmann@66808
  1181
      by simp
haftmann@66808
  1182
    with P show False
haftmann@66808
  1183
      by simp
haftmann@66808
  1184
  qed
haftmann@66808
  1185
qed
haftmann@66808
  1186
haftmann@66808
  1187
lemma less_mult_imp_div_less:
haftmann@66808
  1188
  "m div n < i" if "m < i * n" for m n i :: nat
haftmann@66808
  1189
proof -
haftmann@66808
  1190
  from that have "i * n > 0"
haftmann@66808
  1191
    by (cases "i * n = 0") simp_all
haftmann@66808
  1192
  then have "i > 0" and "n > 0"
haftmann@66808
  1193
    by simp_all
haftmann@66808
  1194
  have "m div n * n \<le> m"
haftmann@66808
  1195
    by simp
haftmann@66808
  1196
  then have "m div n * n < i * n"
haftmann@66808
  1197
    using that by (rule le_less_trans)
haftmann@66808
  1198
  with \<open>n > 0\<close> show ?thesis
haftmann@66808
  1199
    by simp
haftmann@66808
  1200
qed
haftmann@66808
  1201
haftmann@66808
  1202
text \<open>A fact for the mutilated chess board\<close>
haftmann@66808
  1203
haftmann@66808
  1204
lemma mod_Suc:
haftmann@66808
  1205
  "Suc m mod n = (if Suc (m mod n) = n then 0 else Suc (m mod n))" (is "_ = ?rhs")
haftmann@66808
  1206
proof (cases "n = 0")
haftmann@66808
  1207
  case True
haftmann@66808
  1208
  then show ?thesis
haftmann@66808
  1209
    by simp
haftmann@66808
  1210
next
haftmann@66808
  1211
  case False
haftmann@66808
  1212
  have "Suc m mod n = Suc (m mod n) mod n"
haftmann@66808
  1213
    by (simp add: mod_simps)
haftmann@66808
  1214
  also have "\<dots> = ?rhs"
haftmann@66808
  1215
    using False by (auto intro!: mod_nat_eqI intro: neq_le_trans simp add: Suc_le_eq)
haftmann@66808
  1216
  finally show ?thesis .
haftmann@66808
  1217
qed
haftmann@66808
  1218
haftmann@66808
  1219
lemma Suc_times_mod_eq:
haftmann@66808
  1220
  "Suc (m * n) mod m = 1" if "Suc 0 < m"
haftmann@66808
  1221
  using that by (simp add: mod_Suc)
haftmann@66808
  1222
haftmann@66808
  1223
lemma Suc_times_numeral_mod_eq [simp]:
haftmann@66808
  1224
  "Suc (numeral k * n) mod numeral k = 1" if "numeral k \<noteq> (1::nat)"
haftmann@66808
  1225
  by (rule Suc_times_mod_eq) (use that in simp)
haftmann@66808
  1226
haftmann@66808
  1227
lemma Suc_div_le_mono [simp]:
haftmann@66808
  1228
  "m div n \<le> Suc m div n"
haftmann@66808
  1229
  by (simp add: div_le_mono)
haftmann@66808
  1230
haftmann@66808
  1231
text \<open>These lemmas collapse some needless occurrences of Suc:
haftmann@66808
  1232
  at least three Sucs, since two and fewer are rewritten back to Suc again!
haftmann@66808
  1233
  We already have some rules to simplify operands smaller than 3.\<close>
haftmann@66808
  1234
haftmann@66808
  1235
lemma div_Suc_eq_div_add3 [simp]:
haftmann@66808
  1236
  "m div Suc (Suc (Suc n)) = m div (3 + n)"
haftmann@66808
  1237
  by (simp add: Suc3_eq_add_3)
haftmann@66808
  1238
haftmann@66808
  1239
lemma mod_Suc_eq_mod_add3 [simp]:
haftmann@66808
  1240
  "m mod Suc (Suc (Suc n)) = m mod (3 + n)"
haftmann@66808
  1241
  by (simp add: Suc3_eq_add_3)
haftmann@66808
  1242
haftmann@66808
  1243
lemma Suc_div_eq_add3_div:
haftmann@66808
  1244
  "Suc (Suc (Suc m)) div n = (3 + m) div n"
haftmann@66808
  1245
  by (simp add: Suc3_eq_add_3)
haftmann@66808
  1246
haftmann@66808
  1247
lemma Suc_mod_eq_add3_mod:
haftmann@66808
  1248
  "Suc (Suc (Suc m)) mod n = (3 + m) mod n"
haftmann@66808
  1249
  by (simp add: Suc3_eq_add_3)
haftmann@66808
  1250
haftmann@66808
  1251
lemmas Suc_div_eq_add3_div_numeral [simp] =
haftmann@66808
  1252
  Suc_div_eq_add3_div [of _ "numeral v"] for v
haftmann@66808
  1253
haftmann@66808
  1254
lemmas Suc_mod_eq_add3_mod_numeral [simp] =
haftmann@66808
  1255
  Suc_mod_eq_add3_mod [of _ "numeral v"] for v
haftmann@66808
  1256
haftmann@66808
  1257
lemma (in field_char_0) of_nat_div:
haftmann@66808
  1258
  "of_nat (m div n) = ((of_nat m - of_nat (m mod n)) / of_nat n)"
haftmann@66808
  1259
proof -
haftmann@66808
  1260
  have "of_nat (m div n) = ((of_nat (m div n * n + m mod n) - of_nat (m mod n)) / of_nat n :: 'a)"
haftmann@66808
  1261
    unfolding of_nat_add by (cases "n = 0") simp_all
haftmann@66808
  1262
  then show ?thesis
haftmann@66808
  1263
    by simp
haftmann@66808
  1264
qed
haftmann@66808
  1265
haftmann@66808
  1266
text \<open>An ``induction'' law for modulus arithmetic.\<close>
haftmann@66808
  1267
haftmann@66808
  1268
lemma mod_induct [consumes 3, case_names step]:
haftmann@66808
  1269
  "P m" if "P n" and "n < p" and "m < p"
haftmann@66808
  1270
    and step: "\<And>n. n < p \<Longrightarrow> P n \<Longrightarrow> P (Suc n mod p)"
haftmann@66808
  1271
using \<open>m < p\<close> proof (induct m)
haftmann@66808
  1272
  case 0
haftmann@66808
  1273
  show ?case
haftmann@66808
  1274
  proof (rule ccontr)
haftmann@66808
  1275
    assume "\<not> P 0"
haftmann@66808
  1276
    from \<open>n < p\<close> have "0 < p"
haftmann@66808
  1277
      by simp
haftmann@66808
  1278
    from \<open>n < p\<close> obtain m where "0 < m" and "p = n + m"
haftmann@66808
  1279
      by (blast dest: less_imp_add_positive)
haftmann@66808
  1280
    with \<open>P n\<close> have "P (p - m)"
haftmann@66808
  1281
      by simp
haftmann@66808
  1282
    moreover have "\<not> P (p - m)"
haftmann@66808
  1283
    using \<open>0 < m\<close> proof (induct m)
haftmann@66808
  1284
      case 0
haftmann@66808
  1285
      then show ?case
haftmann@66808
  1286
        by simp
haftmann@66808
  1287
    next
haftmann@66808
  1288
      case (Suc m)
haftmann@66808
  1289
      show ?case
haftmann@66808
  1290
      proof
haftmann@66808
  1291
        assume P: "P (p - Suc m)"
haftmann@66808
  1292
        with \<open>\<not> P 0\<close> have "Suc m < p"
haftmann@66808
  1293
          by (auto intro: ccontr) 
haftmann@66808
  1294
        then have "Suc (p - Suc m) = p - m"
haftmann@66808
  1295
          by arith
haftmann@66808
  1296
        moreover from \<open>0 < p\<close> have "p - Suc m < p"
haftmann@66808
  1297
          by arith
haftmann@66808
  1298
        with P step have "P ((Suc (p - Suc m)) mod p)"
haftmann@66808
  1299
          by blast
haftmann@66808
  1300
        ultimately show False
haftmann@66808
  1301
          using \<open>\<not> P 0\<close> Suc.hyps by (cases "m = 0") simp_all
haftmann@66808
  1302
      qed
haftmann@66808
  1303
    qed
haftmann@66808
  1304
    ultimately show False
haftmann@66808
  1305
      by blast
haftmann@66808
  1306
  qed
haftmann@66808
  1307
next
haftmann@66808
  1308
  case (Suc m)
haftmann@66808
  1309
  then have "m < p" and mod: "Suc m mod p = Suc m"
haftmann@66808
  1310
    by simp_all
haftmann@66808
  1311
  from \<open>m < p\<close> have "P m"
haftmann@66808
  1312
    by (rule Suc.hyps)
haftmann@66808
  1313
  with \<open>m < p\<close> have "P (Suc m mod p)"
haftmann@66808
  1314
    by (rule step)
haftmann@66808
  1315
  with mod show ?case
haftmann@66808
  1316
    by simp
haftmann@66808
  1317
qed
haftmann@66808
  1318
haftmann@66808
  1319
lemma split_div:
haftmann@66808
  1320
  "P (m div n) \<longleftrightarrow> (n = 0 \<longrightarrow> P 0) \<and> (n \<noteq> 0 \<longrightarrow>
haftmann@66808
  1321
     (\<forall>i j. j < n \<longrightarrow> m = n * i + j \<longrightarrow> P i))"
haftmann@66808
  1322
     (is "?P = ?Q") for m n :: nat
haftmann@66808
  1323
proof (cases "n = 0")
haftmann@66808
  1324
  case True
haftmann@66808
  1325
  then show ?thesis
haftmann@66808
  1326
    by simp
haftmann@66808
  1327
next
haftmann@66808
  1328
  case False
haftmann@66808
  1329
  show ?thesis
haftmann@66808
  1330
  proof
haftmann@66808
  1331
    assume ?P
haftmann@66808
  1332
    with False show ?Q
haftmann@66808
  1333
      by auto
haftmann@66808
  1334
  next
haftmann@66808
  1335
    assume ?Q
haftmann@66808
  1336
    with False have *: "\<And>i j. j < n \<Longrightarrow> m = n * i + j \<Longrightarrow> P i"
haftmann@66808
  1337
      by simp
haftmann@66808
  1338
    with False show ?P
haftmann@66808
  1339
      by (auto intro: * [of "m mod n"])
haftmann@66808
  1340
  qed
haftmann@66808
  1341
qed
haftmann@66808
  1342
haftmann@66808
  1343
lemma split_div':
haftmann@66808
  1344
  "P (m div n) \<longleftrightarrow> n = 0 \<and> P 0 \<or> (\<exists>q. (n * q \<le> m \<and> m < n * Suc q) \<and> P q)"
haftmann@66808
  1345
proof (cases "n = 0")
haftmann@66808
  1346
  case True
haftmann@66808
  1347
  then show ?thesis
haftmann@66808
  1348
    by simp
haftmann@66808
  1349
next
haftmann@66808
  1350
  case False
haftmann@66808
  1351
  then have "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> m div n = q" for q
haftmann@66808
  1352
    by (auto intro: div_nat_eqI dividend_less_times_div)
haftmann@66808
  1353
  then show ?thesis
haftmann@66808
  1354
    by auto
haftmann@66808
  1355
qed
haftmann@66808
  1356
haftmann@66808
  1357
lemma split_mod:
haftmann@66808
  1358
  "P (m mod n) \<longleftrightarrow> (n = 0 \<longrightarrow> P m) \<and> (n \<noteq> 0 \<longrightarrow>
haftmann@66808
  1359
     (\<forall>i j. j < n \<longrightarrow> m = n * i + j \<longrightarrow> P j))"
haftmann@66808
  1360
     (is "?P \<longleftrightarrow> ?Q") for m n :: nat
haftmann@66808
  1361
proof (cases "n = 0")
haftmann@66808
  1362
  case True
haftmann@66808
  1363
  then show ?thesis
haftmann@66808
  1364
    by simp
haftmann@66808
  1365
next
haftmann@66808
  1366
  case False
haftmann@66808
  1367
  show ?thesis
haftmann@66808
  1368
  proof
haftmann@66808
  1369
    assume ?P
haftmann@66808
  1370
    with False show ?Q
haftmann@66808
  1371
      by auto
haftmann@66808
  1372
  next
haftmann@66808
  1373
    assume ?Q
haftmann@66808
  1374
    with False have *: "\<And>i j. j < n \<Longrightarrow> m = n * i + j \<Longrightarrow> P j"
haftmann@66808
  1375
      by simp
haftmann@66808
  1376
    with False show ?P
haftmann@66808
  1377
      by (auto intro: * [of _ "m div n"])
haftmann@66808
  1378
  qed
haftmann@66808
  1379
qed
haftmann@66808
  1380
haftmann@66808
  1381
haftmann@66816
  1382
subsection \<open>Euclidean division on @{typ int}\<close>
haftmann@66816
  1383
haftmann@66816
  1384
instantiation int :: normalization_semidom
haftmann@66816
  1385
begin
haftmann@66816
  1386
haftmann@66816
  1387
definition normalize_int :: "int \<Rightarrow> int"
haftmann@66816
  1388
  where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
haftmann@66816
  1389
haftmann@66816
  1390
definition unit_factor_int :: "int \<Rightarrow> int"
haftmann@66816
  1391
  where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
haftmann@66816
  1392
haftmann@66816
  1393
definition divide_int :: "int \<Rightarrow> int \<Rightarrow> int"
haftmann@66816
  1394
  where "k div l = (if l = 0 then 0
haftmann@66816
  1395
    else if sgn k = sgn l
haftmann@66816
  1396
      then int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
haftmann@66816
  1397
      else - int (nat \<bar>k\<bar> div nat \<bar>l\<bar> + of_bool (\<not> l dvd k)))"
haftmann@66816
  1398
haftmann@66816
  1399
lemma divide_int_unfold:
haftmann@66816
  1400
  "(sgn k * int m) div (sgn l * int n) =
haftmann@66816
  1401
   (if sgn l = 0 \<or> sgn k = 0 \<or> n = 0 then 0
haftmann@66816
  1402
    else if sgn k = sgn l
haftmann@66816
  1403
      then int (m div n)
haftmann@66816
  1404
      else - int (m div n + of_bool (\<not> n dvd m)))"
haftmann@66816
  1405
  by (auto simp add: divide_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
haftmann@66816
  1406
    nat_mult_distrib dvd_int_iff)
haftmann@66816
  1407
haftmann@66816
  1408
instance proof
haftmann@66816
  1409
  fix k :: int show "k div 0 = 0"
haftmann@66816
  1410
  by (simp add: divide_int_def)
haftmann@66816
  1411
next
haftmann@66816
  1412
  fix k l :: int
haftmann@66816
  1413
  assume "l \<noteq> 0"
haftmann@66816
  1414
  obtain n m and s t where k: "k = sgn s * int n" and l: "l = sgn t * int m" 
haftmann@66816
  1415
    by (blast intro: int_sgnE elim: that)
haftmann@66816
  1416
  then have "k * l = sgn (s * t) * int (n * m)"
haftmann@66816
  1417
    by (simp add: ac_simps sgn_mult)
haftmann@66816
  1418
  with k l \<open>l \<noteq> 0\<close> show "k * l div l = k"
haftmann@66816
  1419
    by (simp only: divide_int_unfold)
haftmann@66816
  1420
      (auto simp add: algebra_simps sgn_mult sgn_1_pos sgn_0_0)
haftmann@66816
  1421
qed (auto simp add: sgn_mult mult_sgn_abs abs_eq_iff')
haftmann@66816
  1422
haftmann@66816
  1423
end
haftmann@66816
  1424
haftmann@66838
  1425
instantiation int :: idom_modulo
haftmann@66816
  1426
begin
haftmann@66816
  1427
haftmann@66816
  1428
definition modulo_int :: "int \<Rightarrow> int \<Rightarrow> int"
haftmann@66816
  1429
  where "k mod l = (if l = 0 then k
haftmann@66816
  1430
    else if sgn k = sgn l
haftmann@66816
  1431
      then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)
haftmann@66816
  1432
      else sgn l * (\<bar>l\<bar> * of_bool (\<not> l dvd k) - int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)))"
haftmann@66816
  1433
haftmann@66816
  1434
lemma modulo_int_unfold:
haftmann@66816
  1435
  "(sgn k * int m) mod (sgn l * int n) =
haftmann@66816
  1436
   (if sgn l = 0 \<or> sgn k = 0 \<or> n = 0 then sgn k * int m
haftmann@66816
  1437
    else if sgn k = sgn l
haftmann@66816
  1438
      then sgn l * int (m mod n)
haftmann@66816
  1439
      else sgn l * (int (n * of_bool (\<not> n dvd m)) - int (m mod n)))"
haftmann@66816
  1440
  by (auto simp add: modulo_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
haftmann@66816
  1441
    nat_mult_distrib dvd_int_iff)
haftmann@66816
  1442
haftmann@66838
  1443
instance proof
haftmann@66838
  1444
  fix k l :: int
haftmann@66838
  1445
  obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 
haftmann@66838
  1446
    by (blast intro: int_sgnE elim: that)
haftmann@66838
  1447
  then show "k div l * l + k mod l = k"
haftmann@66838
  1448
    by (auto simp add: divide_int_unfold modulo_int_unfold algebra_simps dest!: sgn_not_eq_imp)
haftmann@66838
  1449
       (simp_all add: of_nat_mult [symmetric] of_nat_add [symmetric]
haftmann@66838
  1450
         distrib_left [symmetric] minus_mult_right
haftmann@66838
  1451
         del: of_nat_mult minus_mult_right [symmetric])
haftmann@66838
  1452
qed
haftmann@66838
  1453
haftmann@66838
  1454
end
haftmann@66838
  1455
haftmann@66838
  1456
instantiation int :: unique_euclidean_ring
haftmann@66838
  1457
begin
haftmann@66838
  1458
haftmann@66838
  1459
definition euclidean_size_int :: "int \<Rightarrow> nat"
haftmann@66838
  1460
  where [simp]: "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
haftmann@66838
  1461
haftmann@66838
  1462
definition division_segment_int :: "int \<Rightarrow> int"
haftmann@66838
  1463
  where "division_segment_int k = (if k \<ge> 0 then 1 else - 1)"
haftmann@66838
  1464
haftmann@66838
  1465
lemma division_segment_eq_sgn:
haftmann@66838
  1466
  "division_segment k = sgn k" if "k \<noteq> 0" for k :: int
haftmann@66838
  1467
  using that by (simp add: division_segment_int_def)
haftmann@66838
  1468
haftmann@66838
  1469
lemma abs_division_segment [simp]:
haftmann@66838
  1470
  "\<bar>division_segment k\<bar> = 1" for k :: int
haftmann@66838
  1471
  by (simp add: division_segment_int_def)
haftmann@66838
  1472
haftmann@66816
  1473
lemma abs_mod_less:
haftmann@66816
  1474
  "\<bar>k mod l\<bar> < \<bar>l\<bar>" if "l \<noteq> 0" for k l :: int
haftmann@66816
  1475
proof -
haftmann@66816
  1476
  obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 
haftmann@66816
  1477
    by (blast intro: int_sgnE elim: that)
haftmann@66816
  1478
  with that show ?thesis
haftmann@66816
  1479
    by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg
haftmann@66816
  1480
      abs_mult mod_greater_zero_iff_not_dvd)
haftmann@66816
  1481
qed
haftmann@66816
  1482
haftmann@66816
  1483
lemma sgn_mod:
haftmann@66816
  1484
  "sgn (k mod l) = sgn l" if "l \<noteq> 0" "\<not> l dvd k" for k l :: int
haftmann@66816
  1485
proof -
haftmann@66816
  1486
  obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 
haftmann@66816
  1487
    by (blast intro: int_sgnE elim: that)
haftmann@66816
  1488
  with that show ?thesis
haftmann@66816
  1489
    by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg
haftmann@66816
  1490
      sgn_mult mod_eq_0_iff_dvd int_dvd_iff)
haftmann@66816
  1491
qed
haftmann@66816
  1492
haftmann@66816
  1493
instance proof
haftmann@66816
  1494
  fix k l :: int
haftmann@66838
  1495
  show "division_segment (k mod l) = division_segment l" if
haftmann@66838
  1496
    "l \<noteq> 0" and "\<not> l dvd k"
haftmann@66838
  1497
    using that by (simp add: division_segment_eq_sgn dvd_eq_mod_eq_0 sgn_mod)
haftmann@66816
  1498
next
haftmann@66816
  1499
  fix l q r :: int
haftmann@66816
  1500
  obtain n m and s t
haftmann@66816
  1501
     where l: "l = sgn s * int n" and q: "q = sgn t * int m"
haftmann@66816
  1502
    by (blast intro: int_sgnE elim: that)
haftmann@66816
  1503
  assume \<open>l \<noteq> 0\<close>
haftmann@66816
  1504
  with l have "s \<noteq> 0" and "n > 0"
haftmann@66816
  1505
    by (simp_all add: sgn_0_0)
haftmann@66838
  1506
  assume "division_segment r = division_segment l"
haftmann@66816
  1507
  moreover have "r = sgn r * \<bar>r\<bar>"
haftmann@66816
  1508
    by (simp add: sgn_mult_abs)
haftmann@66816
  1509
  moreover define u where "u = nat \<bar>r\<bar>"
haftmann@66816
  1510
  ultimately have "r = sgn l * int u"
haftmann@66838
  1511
    using division_segment_eq_sgn \<open>l \<noteq> 0\<close> by (cases "r = 0") simp_all
haftmann@66816
  1512
  with l \<open>n > 0\<close> have r: "r = sgn s * int u"
haftmann@66816
  1513
    by (simp add: sgn_mult)
haftmann@66816
  1514
  assume "euclidean_size r < euclidean_size l"
haftmann@66816
  1515
  with l r \<open>s \<noteq> 0\<close> have "u < n"
haftmann@66816
  1516
    by (simp add: abs_mult)
haftmann@66816
  1517
  show "(q * l + r) div l = q"
haftmann@66816
  1518
  proof (cases "q = 0 \<or> r = 0")
haftmann@66816
  1519
    case True
haftmann@66816
  1520
    then show ?thesis
haftmann@66816
  1521
    proof
haftmann@66816
  1522
      assume "q = 0"
haftmann@66816
  1523
      then show ?thesis
haftmann@66816
  1524
        using l r \<open>u < n\<close> by (simp add: divide_int_unfold)
haftmann@66816
  1525
    next
haftmann@66816
  1526
      assume "r = 0"
haftmann@66816
  1527
      from \<open>r = 0\<close> have *: "q * l + r = sgn (t * s) * int (n * m)"
haftmann@66816
  1528
        using q l by (simp add: ac_simps sgn_mult)
haftmann@66816
  1529
      from \<open>s \<noteq> 0\<close> \<open>n > 0\<close> show ?thesis
haftmann@66816
  1530
        by (simp only: *, simp only: q l divide_int_unfold)
haftmann@66816
  1531
          (auto simp add: sgn_mult sgn_0_0 sgn_1_pos)
haftmann@66816
  1532
    qed
haftmann@66816
  1533
  next
haftmann@66816
  1534
    case False
haftmann@66816
  1535
    with q r have "t \<noteq> 0" and "m > 0" and "s \<noteq> 0" and "u > 0"
haftmann@66816
  1536
      by (simp_all add: sgn_0_0)
haftmann@66816
  1537
    moreover from \<open>0 < m\<close> \<open>u < n\<close> have "u \<le> m * n"
haftmann@66816
  1538
      using mult_le_less_imp_less [of 1 m u n] by simp
haftmann@66816
  1539
    ultimately have *: "q * l + r = sgn (s * t)
haftmann@66816
  1540
      * int (if t < 0 then m * n - u else m * n + u)"
haftmann@66816
  1541
      using l q r
haftmann@66816
  1542
      by (simp add: sgn_mult algebra_simps of_nat_diff)
haftmann@66816
  1543
    have "(m * n - u) div n = m - 1" if "u > 0"
haftmann@66816
  1544
      using \<open>0 < m\<close> \<open>u < n\<close> that
haftmann@66816
  1545
      by (auto intro: div_nat_eqI simp add: algebra_simps)
haftmann@66816
  1546
    moreover have "n dvd m * n - u \<longleftrightarrow> n dvd u"
haftmann@66816
  1547
      using \<open>u \<le> m * n\<close> dvd_diffD1 [of n "m * n" u]
haftmann@66816
  1548
      by auto
haftmann@66816
  1549
    ultimately show ?thesis
haftmann@66816
  1550
      using \<open>s \<noteq> 0\<close> \<open>m > 0\<close> \<open>u > 0\<close> \<open>u < n\<close> \<open>u \<le> m * n\<close>
haftmann@66816
  1551
      by (simp only: *, simp only: l q divide_int_unfold)
haftmann@66816
  1552
        (auto simp add: sgn_mult sgn_0_0 sgn_1_pos algebra_simps dest: dvd_imp_le)
haftmann@66816
  1553
  qed
haftmann@66838
  1554
qed (use mult_le_mono2 [of 1] in \<open>auto simp add: division_segment_int_def not_le sign_simps abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>)
haftmann@66816
  1555
haftmann@66816
  1556
end
haftmann@66816
  1557
haftmann@66816
  1558
lemma pos_mod_bound [simp]:
haftmann@66816
  1559
  "k mod l < l" if "l > 0" for k l :: int
haftmann@66816
  1560
proof -
haftmann@66816
  1561
  obtain m and s where "k = sgn s * int m"
haftmann@66816
  1562
    by (blast intro: int_sgnE elim: that)
haftmann@66816
  1563
  moreover from that obtain n where "l = sgn 1 * int n"
haftmann@66816
  1564
    by (cases l) auto
haftmann@66816
  1565
  ultimately show ?thesis
haftmann@66816
  1566
    using that by (simp only: modulo_int_unfold)
haftmann@66816
  1567
      (simp add: mod_greater_zero_iff_not_dvd)
haftmann@66816
  1568
qed
haftmann@66816
  1569
haftmann@66816
  1570
lemma pos_mod_sign [simp]:
haftmann@66816
  1571
  "0 \<le> k mod l" if "l > 0" for k l :: int
haftmann@66816
  1572
proof -
haftmann@66816
  1573
  obtain m and s where "k = sgn s * int m"
haftmann@66816
  1574
    by (blast intro: int_sgnE elim: that)
haftmann@66816
  1575
  moreover from that obtain n where "l = sgn 1 * int n"
haftmann@66816
  1576
    by (cases l) auto
haftmann@66816
  1577
  ultimately show ?thesis
haftmann@66816
  1578
    using that by (simp only: modulo_int_unfold) simp
haftmann@66816
  1579
qed
haftmann@66816
  1580
haftmann@66816
  1581
haftmann@66808
  1582
subsection \<open>Code generation\<close>
haftmann@66808
  1583
haftmann@66808
  1584
code_identifier
haftmann@66808
  1585
  code_module Euclidean_Division \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
haftmann@66808
  1586
haftmann@66808
  1587
end