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