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