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