src/HOL/Divides.thy
author haftmann
Tue Dec 20 15:39:13 2016 +0100 (2016-12-20)
changeset 64630 96015aecfeba
parent 64593 50c715579715
child 64635 255741c5f862
permissions -rw-r--r--
emphasize dedicated rewrite rules for congruences
     1 (*  Title:      HOL/Divides.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1999  University of Cambridge
     4 *)
     5 
     6 section \<open>Quotient and remainder\<close>
     7 
     8 theory Divides
     9 imports Parity
    10 begin
    11 
    12 subsection \<open>Quotient and remainder in integral domains\<close>
    13 
    14 class semidom_modulo = algebraic_semidom + semiring_modulo
    15 begin
    16 
    17 lemma mod_0 [simp]: "0 mod a = 0"
    18   using div_mult_mod_eq [of 0 a] by simp
    19 
    20 lemma mod_by_0 [simp]: "a mod 0 = a"
    21   using div_mult_mod_eq [of a 0] by simp
    22 
    23 lemma mod_by_1 [simp]:
    24   "a mod 1 = 0"
    25 proof -
    26   from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp
    27   then have "a + a mod 1 = a + 0" by simp
    28   then show ?thesis by (rule add_left_imp_eq)
    29 qed
    30 
    31 lemma mod_self [simp]:
    32   "a mod a = 0"
    33   using div_mult_mod_eq [of a a] by simp
    34 
    35 lemma dvd_imp_mod_0 [simp]:
    36   assumes "a dvd b"
    37   shows "b mod a = 0"
    38   using assms minus_div_mult_eq_mod [of b a] by simp
    39 
    40 lemma mod_0_imp_dvd: 
    41   assumes "a mod b = 0"
    42   shows   "b dvd a"
    43 proof -
    44   have "b dvd ((a div b) * b)" by simp
    45   also have "(a div b) * b = a"
    46     using div_mult_mod_eq [of a b] by (simp add: assms)
    47   finally show ?thesis .
    48 qed
    49 
    50 lemma mod_eq_0_iff_dvd:
    51   "a mod b = 0 \<longleftrightarrow> b dvd a"
    52   by (auto intro: mod_0_imp_dvd)
    53 
    54 lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
    55   "a dvd b \<longleftrightarrow> b mod a = 0"
    56   by (simp add: mod_eq_0_iff_dvd)
    57 
    58 lemma dvd_mod_iff: 
    59   assumes "c dvd b"
    60   shows "c dvd a mod b \<longleftrightarrow> c dvd a"
    61 proof -
    62   from assms have "(c dvd a mod b) \<longleftrightarrow> (c dvd ((a div b) * b + a mod b))" 
    63     by (simp add: dvd_add_right_iff)
    64   also have "(a div b) * b + a mod b = a"
    65     using div_mult_mod_eq [of a b] by simp
    66   finally show ?thesis .
    67 qed
    68 
    69 lemma dvd_mod_imp_dvd:
    70   assumes "c dvd a mod b" and "c dvd b"
    71   shows "c dvd a"
    72   using assms dvd_mod_iff [of c b a] by simp
    73 
    74 end
    75 
    76 class idom_modulo = idom + semidom_modulo
    77 begin
    78 
    79 subclass idom_divide ..
    80 
    81 lemma div_diff [simp]:
    82   "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> (a - b) div c = a div c - b div c"
    83   using div_add [of _  _ "- b"] by (simp add: dvd_neg_div)
    84 
    85 end
    86 
    87 
    88 subsection \<open>Quotient and remainder in integral domains with additional properties\<close>
    89 
    90 class semiring_div = semidom_modulo +
    91   assumes div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
    92     and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
    93 begin
    94 
    95 lemma div_mult_self2 [simp]:
    96   assumes "b \<noteq> 0"
    97   shows "(a + b * c) div b = c + a div b"
    98   using assms div_mult_self1 [of b a c] by (simp add: mult.commute)
    99 
   100 lemma div_mult_self3 [simp]:
   101   assumes "b \<noteq> 0"
   102   shows "(c * b + a) div b = c + a div b"
   103   using assms by (simp add: add.commute)
   104 
   105 lemma div_mult_self4 [simp]:
   106   assumes "b \<noteq> 0"
   107   shows "(b * c + a) div b = c + a div b"
   108   using assms by (simp add: add.commute)
   109 
   110 lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b"
   111 proof (cases "b = 0")
   112   case True then show ?thesis by simp
   113 next
   114   case False
   115   have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b"
   116     by (simp add: div_mult_mod_eq)
   117   also from False div_mult_self1 [of b a c] have
   118     "\<dots> = (c + a div b) * b + (a + c * b) mod b"
   119       by (simp add: algebra_simps)
   120   finally have "a = a div b * b + (a + c * b) mod b"
   121     by (simp add: add.commute [of a] add.assoc distrib_right)
   122   then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
   123     by (simp add: div_mult_mod_eq)
   124   then show ?thesis by simp
   125 qed
   126 
   127 lemma mod_mult_self2 [simp]:
   128   "(a + b * c) mod b = a mod b"
   129   by (simp add: mult.commute [of b])
   130 
   131 lemma mod_mult_self3 [simp]:
   132   "(c * b + a) mod b = a mod b"
   133   by (simp add: add.commute)
   134 
   135 lemma mod_mult_self4 [simp]:
   136   "(b * c + a) mod b = a mod b"
   137   by (simp add: add.commute)
   138 
   139 lemma mod_mult_self1_is_0 [simp]:
   140   "b * a mod b = 0"
   141   using mod_mult_self2 [of 0 b a] by simp
   142 
   143 lemma mod_mult_self2_is_0 [simp]:
   144   "a * b mod b = 0"
   145   using mod_mult_self1 [of 0 a b] by simp
   146 
   147 lemma div_add_self1:
   148   assumes "b \<noteq> 0"
   149   shows "(b + a) div b = a div b + 1"
   150   using assms div_mult_self1 [of b a 1] by (simp add: add.commute)
   151 
   152 lemma div_add_self2:
   153   assumes "b \<noteq> 0"
   154   shows "(a + b) div b = a div b + 1"
   155   using assms div_add_self1 [of b a] by (simp add: add.commute)
   156 
   157 lemma mod_add_self1 [simp]:
   158   "(b + a) mod b = a mod b"
   159   using mod_mult_self1 [of a 1 b] by (simp add: add.commute)
   160 
   161 lemma mod_add_self2 [simp]:
   162   "(a + b) mod b = a mod b"
   163   using mod_mult_self1 [of a 1 b] by simp
   164 
   165 lemma mod_div_trivial [simp]:
   166   "a mod b div b = 0"
   167 proof (cases "b = 0")
   168   assume "b = 0"
   169   thus ?thesis by simp
   170 next
   171   assume "b \<noteq> 0"
   172   hence "a div b + a mod b div b = (a mod b + a div b * b) div b"
   173     by (rule div_mult_self1 [symmetric])
   174   also have "\<dots> = a div b"
   175     by (simp only: mod_div_mult_eq)
   176   also have "\<dots> = a div b + 0"
   177     by simp
   178   finally show ?thesis
   179     by (rule add_left_imp_eq)
   180 qed
   181 
   182 lemma mod_mod_trivial [simp]:
   183   "a mod b mod b = a mod b"
   184 proof -
   185   have "a mod b mod b = (a mod b + a div b * b) mod b"
   186     by (simp only: mod_mult_self1)
   187   also have "\<dots> = a mod b"
   188     by (simp only: mod_div_mult_eq)
   189   finally show ?thesis .
   190 qed
   191 
   192 lemma mod_mod_cancel:
   193   assumes "c dvd b"
   194   shows "a mod b mod c = a mod c"
   195 proof -
   196   from \<open>c dvd b\<close> obtain k where "b = c * k"
   197     by (rule dvdE)
   198   have "a mod b mod c = a mod (c * k) mod c"
   199     by (simp only: \<open>b = c * k\<close>)
   200   also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
   201     by (simp only: mod_mult_self1)
   202   also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
   203     by (simp only: ac_simps)
   204   also have "\<dots> = a mod c"
   205     by (simp only: div_mult_mod_eq)
   206   finally show ?thesis .
   207 qed
   208 
   209 lemma div_mult_mult2 [simp]:
   210   "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
   211   by (drule div_mult_mult1) (simp add: mult.commute)
   212 
   213 lemma div_mult_mult1_if [simp]:
   214   "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"
   215   by simp_all
   216 
   217 lemma mod_mult_mult1:
   218   "(c * a) mod (c * b) = c * (a mod b)"
   219 proof (cases "c = 0")
   220   case True then show ?thesis by simp
   221 next
   222   case False
   223   from div_mult_mod_eq
   224   have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
   225   with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
   226     = c * a + c * (a mod b)" by (simp add: algebra_simps)
   227   with div_mult_mod_eq show ?thesis by simp
   228 qed
   229 
   230 lemma mod_mult_mult2:
   231   "(a * c) mod (b * c) = (a mod b) * c"
   232   using mod_mult_mult1 [of c a b] by (simp add: mult.commute)
   233 
   234 lemma mult_mod_left: "(a mod b) * c = (a * c) mod (b * c)"
   235   by (fact mod_mult_mult2 [symmetric])
   236 
   237 lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)"
   238   by (fact mod_mult_mult1 [symmetric])
   239 
   240 lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
   241   unfolding dvd_def by (auto simp add: mod_mult_mult1)
   242 
   243 named_theorems mod_simps
   244 
   245 text \<open>Addition respects modular equivalence.\<close>
   246 
   247 lemma mod_add_left_eq [mod_simps]:
   248   "(a mod c + b) mod c = (a + b) mod c"
   249 proof -
   250   have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
   251     by (simp only: div_mult_mod_eq)
   252   also have "\<dots> = (a mod c + b + a div c * c) mod c"
   253     by (simp only: ac_simps)
   254   also have "\<dots> = (a mod c + b) mod c"
   255     by (rule mod_mult_self1)
   256   finally show ?thesis
   257     by (rule sym)
   258 qed
   259 
   260 lemma mod_add_right_eq [mod_simps]:
   261   "(a + b mod c) mod c = (a + b) mod c"
   262   using mod_add_left_eq [of b c a] by (simp add: ac_simps)
   263 
   264 lemma mod_add_eq:
   265   "(a mod c + b mod c) mod c = (a + b) mod c"
   266   by (simp add: mod_add_left_eq mod_add_right_eq)
   267 
   268 lemma mod_sum_eq [mod_simps]:
   269   "(\<Sum>i\<in>A. f i mod a) mod a = sum f A mod a"
   270 proof (induct A rule: infinite_finite_induct)
   271   case (insert i A)
   272   then have "(\<Sum>i\<in>insert i A. f i mod a) mod a
   273     = (f i mod a + (\<Sum>i\<in>A. f i mod a)) mod a"
   274     by simp
   275   also have "\<dots> = (f i + (\<Sum>i\<in>A. f i mod a) mod a) mod a"
   276     by (simp add: mod_simps)
   277   also have "\<dots> = (f i + (\<Sum>i\<in>A. f i) mod a) mod a"
   278     by (simp add: insert.hyps)
   279   finally show ?case
   280     by (simp add: insert.hyps mod_simps)
   281 qed simp_all
   282 
   283 lemma mod_add_cong:
   284   assumes "a mod c = a' mod c"
   285   assumes "b mod c = b' mod c"
   286   shows "(a + b) mod c = (a' + b') mod c"
   287 proof -
   288   have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
   289     unfolding assms ..
   290   then show ?thesis
   291     by (simp add: mod_add_eq)
   292 qed
   293 
   294 text \<open>Multiplication respects modular equivalence.\<close>
   295 
   296 lemma mod_mult_left_eq [mod_simps]:
   297   "((a mod c) * b) mod c = (a * b) mod c"
   298 proof -
   299   have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
   300     by (simp only: div_mult_mod_eq)
   301   also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
   302     by (simp only: algebra_simps)
   303   also have "\<dots> = (a mod c * b) mod c"
   304     by (rule mod_mult_self1)
   305   finally show ?thesis
   306     by (rule sym)
   307 qed
   308 
   309 lemma mod_mult_right_eq [mod_simps]:
   310   "(a * (b mod c)) mod c = (a * b) mod c"
   311   using mod_mult_left_eq [of b c a] by (simp add: ac_simps)
   312 
   313 lemma mod_mult_eq:
   314   "((a mod c) * (b mod c)) mod c = (a * b) mod c"
   315   by (simp add: mod_mult_left_eq mod_mult_right_eq)
   316 
   317 lemma mod_prod_eq [mod_simps]:
   318   "(\<Prod>i\<in>A. f i mod a) mod a = prod f A mod a"
   319 proof (induct A rule: infinite_finite_induct)
   320   case (insert i A)
   321   then have "(\<Prod>i\<in>insert i A. f i mod a) mod a
   322     = (f i mod a * (\<Prod>i\<in>A. f i mod a)) mod a"
   323     by simp
   324   also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i mod a) mod a)) mod a"
   325     by (simp add: mod_simps)
   326   also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i) mod a)) mod a"
   327     by (simp add: insert.hyps)
   328   finally show ?case
   329     by (simp add: insert.hyps mod_simps)
   330 qed simp_all
   331 
   332 lemma mod_mult_cong:
   333   assumes "a mod c = a' mod c"
   334   assumes "b mod c = b' mod c"
   335   shows "(a * b) mod c = (a' * b') mod c"
   336 proof -
   337   have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
   338     unfolding assms ..
   339   then show ?thesis
   340     by (simp add: mod_mult_eq)
   341 qed
   342 
   343 text \<open>Exponentiation respects modular equivalence.\<close>
   344 
   345 lemma power_mod [mod_simps]: 
   346   "((a mod b) ^ n) mod b = (a ^ n) mod b"
   347 proof (induct n)
   348   case 0
   349   then show ?case by simp
   350 next
   351   case (Suc n)
   352   have "(a mod b) ^ Suc n mod b = (a mod b) * ((a mod b) ^ n mod b) mod b"
   353     by (simp add: mod_mult_right_eq)
   354   with Suc show ?case
   355     by (simp add: mod_mult_left_eq mod_mult_right_eq)
   356 qed
   357 
   358 end
   359 
   360 class ring_div = comm_ring_1 + semiring_div
   361 begin
   362 
   363 subclass idom_divide ..
   364 
   365 lemma div_minus_minus [simp]: "(- a) div (- b) = a div b"
   366   using div_mult_mult1 [of "- 1" a b] by simp
   367 
   368 lemma mod_minus_minus [simp]: "(- a) mod (- b) = - (a mod b)"
   369   using mod_mult_mult1 [of "- 1" a b] by simp
   370 
   371 lemma div_minus_right: "a div (- b) = (- a) div b"
   372   using div_minus_minus [of "- a" b] by simp
   373 
   374 lemma mod_minus_right: "a mod (- b) = - ((- a) mod b)"
   375   using mod_minus_minus [of "- a" b] by simp
   376 
   377 lemma div_minus1_right [simp]: "a div (- 1) = - a"
   378   using div_minus_right [of a 1] by simp
   379 
   380 lemma mod_minus1_right [simp]: "a mod (- 1) = 0"
   381   using mod_minus_right [of a 1] by simp
   382 
   383 text \<open>Negation respects modular equivalence.\<close>
   384 
   385 lemma mod_minus_eq [mod_simps]:
   386   "(- (a mod b)) mod b = (- a) mod b"
   387 proof -
   388   have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
   389     by (simp only: div_mult_mod_eq)
   390   also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
   391     by (simp add: ac_simps)
   392   also have "\<dots> = (- (a mod b)) mod b"
   393     by (rule mod_mult_self1)
   394   finally show ?thesis
   395     by (rule sym)
   396 qed
   397 
   398 lemma mod_minus_cong:
   399   assumes "a mod b = a' mod b"
   400   shows "(- a) mod b = (- a') mod b"
   401 proof -
   402   have "(- (a mod b)) mod b = (- (a' mod b)) mod b"
   403     unfolding assms ..
   404   then show ?thesis
   405     by (simp add: mod_minus_eq)
   406 qed
   407 
   408 text \<open>Subtraction respects modular equivalence.\<close>
   409 
   410 lemma mod_diff_left_eq [mod_simps]:
   411   "(a mod c - b) mod c = (a - b) mod c"
   412   using mod_add_cong [of a c "a mod c" "- b" "- b"]
   413   by simp
   414 
   415 lemma mod_diff_right_eq [mod_simps]:
   416   "(a - b mod c) mod c = (a - b) mod c"
   417   using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
   418   by simp
   419 
   420 lemma mod_diff_eq:
   421   "(a mod c - b mod c) mod c = (a - b) mod c"
   422   using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
   423   by simp
   424 
   425 lemma mod_diff_cong:
   426   assumes "a mod c = a' mod c"
   427   assumes "b mod c = b' mod c"
   428   shows "(a - b) mod c = (a' - b') mod c"
   429   using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"]
   430   by simp
   431 
   432 lemma minus_mod_self2 [simp]:
   433   "(a - b) mod b = a mod b"
   434   using mod_diff_right_eq [of a b b]
   435   by (simp add: mod_diff_right_eq)
   436 
   437 lemma minus_mod_self1 [simp]:
   438   "(b - a) mod b = - a mod b"
   439   using mod_add_self2 [of "- a" b] by simp
   440 
   441 end
   442 
   443 
   444 subsection \<open>Parity\<close>
   445 
   446 class semiring_div_parity = semiring_div + comm_semiring_1_cancel + numeral +
   447   assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
   448   assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
   449   assumes zero_not_eq_two: "0 \<noteq> 2"
   450 begin
   451 
   452 lemma parity_cases [case_names even odd]:
   453   assumes "a mod 2 = 0 \<Longrightarrow> P"
   454   assumes "a mod 2 = 1 \<Longrightarrow> P"
   455   shows P
   456   using assms parity by blast
   457 
   458 lemma one_div_two_eq_zero [simp]:
   459   "1 div 2 = 0"
   460 proof (cases "2 = 0")
   461   case True then show ?thesis by simp
   462 next
   463   case False
   464   from div_mult_mod_eq have "1 div 2 * 2 + 1 mod 2 = 1" .
   465   with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
   466   then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff)
   467   then have "1 div 2 = 0 \<or> 2 = 0" by simp
   468   with False show ?thesis by auto
   469 qed
   470 
   471 lemma not_mod_2_eq_0_eq_1 [simp]:
   472   "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
   473   by (cases a rule: parity_cases) simp_all
   474 
   475 lemma not_mod_2_eq_1_eq_0 [simp]:
   476   "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
   477   by (cases a rule: parity_cases) simp_all
   478 
   479 subclass semiring_parity
   480 proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
   481   show "1 mod 2 = 1"
   482     by (fact one_mod_two_eq_one)
   483 next
   484   fix a b
   485   assume "a mod 2 = 1"
   486   moreover assume "b mod 2 = 1"
   487   ultimately show "(a + b) mod 2 = 0"
   488     using mod_add_eq [of a 2 b] by simp
   489 next
   490   fix a b
   491   assume "(a * b) mod 2 = 0"
   492   then have "(a mod 2) * (b mod 2) mod 2 = 0"
   493     by (simp add: mod_mult_eq)
   494   then have "(a mod 2) * (b mod 2) = 0"
   495     by (cases "a mod 2 = 0") simp_all
   496   then show "a mod 2 = 0 \<or> b mod 2 = 0"
   497     by (rule divisors_zero)
   498 next
   499   fix a
   500   assume "a mod 2 = 1"
   501   then have "a = a div 2 * 2 + 1"
   502     using div_mult_mod_eq [of a 2] by simp
   503   then show "\<exists>b. a = b + 1" ..
   504 qed
   505 
   506 lemma even_iff_mod_2_eq_zero:
   507   "even a \<longleftrightarrow> a mod 2 = 0"
   508   by (fact dvd_eq_mod_eq_0)
   509 
   510 lemma odd_iff_mod_2_eq_one:
   511   "odd a \<longleftrightarrow> a mod 2 = 1"
   512   by (auto simp add: even_iff_mod_2_eq_zero)
   513 
   514 lemma even_succ_div_two [simp]:
   515   "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
   516   by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
   517 
   518 lemma odd_succ_div_two [simp]:
   519   "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
   520   by (auto elim!: oddE simp add: zero_not_eq_two [symmetric] add.assoc)
   521 
   522 lemma even_two_times_div_two:
   523   "even a \<Longrightarrow> 2 * (a div 2) = a"
   524   by (fact dvd_mult_div_cancel)
   525 
   526 lemma odd_two_times_div_two_succ [simp]:
   527   "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
   528   using mult_div_mod_eq [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
   529  
   530 end
   531 
   532 
   533 subsection \<open>Numeral division with a pragmatic type class\<close>
   534 
   535 text \<open>
   536   The following type class contains everything necessary to formulate
   537   a division algorithm in ring structures with numerals, restricted
   538   to its positive segments.  This is its primary motiviation, and it
   539   could surely be formulated using a more fine-grained, more algebraic
   540   and less technical class hierarchy.
   541 \<close>
   542 
   543 class semiring_numeral_div = semiring_div + comm_semiring_1_cancel + linordered_semidom +
   544   assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
   545     and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
   546     and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
   547     and mod_less_eq_dividend: "0 \<le> a \<Longrightarrow> a mod b \<le> a"
   548     and pos_mod_bound: "0 < b \<Longrightarrow> a mod b < b"
   549     and pos_mod_sign: "0 < b \<Longrightarrow> 0 \<le> a mod b"
   550     and mod_mult2_eq: "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
   551     and div_mult2_eq: "0 \<le> c \<Longrightarrow> a div (b * c) = a div b div c"
   552   assumes discrete: "a < b \<longleftrightarrow> a + 1 \<le> b"
   553   fixes divmod :: "num \<Rightarrow> num \<Rightarrow> 'a \<times> 'a"
   554     and divmod_step :: "num \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a"
   555   assumes divmod_def: "divmod m n = (numeral m div numeral n, numeral m mod numeral n)"
   556     and divmod_step_def: "divmod_step l qr = (let (q, r) = qr
   557     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
   558     else (2 * q, r))"
   559     \<comment> \<open>These are conceptually definitions but force generated code
   560     to be monomorphic wrt. particular instances of this class which
   561     yields a significant speedup.\<close>
   562 
   563 begin
   564 
   565 subclass semiring_div_parity
   566 proof
   567   fix a
   568   show "a mod 2 = 0 \<or> a mod 2 = 1"
   569   proof (rule ccontr)
   570     assume "\<not> (a mod 2 = 0 \<or> a mod 2 = 1)"
   571     then have "a mod 2 \<noteq> 0" and "a mod 2 \<noteq> 1" by simp_all
   572     have "0 < 2" by simp
   573     with pos_mod_bound pos_mod_sign have "0 \<le> a mod 2" "a mod 2 < 2" by simp_all
   574     with \<open>a mod 2 \<noteq> 0\<close> have "0 < a mod 2" by simp
   575     with discrete have "1 \<le> a mod 2" by simp
   576     with \<open>a mod 2 \<noteq> 1\<close> have "1 < a mod 2" by simp
   577     with discrete have "2 \<le> a mod 2" by simp
   578     with \<open>a mod 2 < 2\<close> show False by simp
   579   qed
   580 next
   581   show "1 mod 2 = 1"
   582     by (rule mod_less) simp_all
   583 next
   584   show "0 \<noteq> 2"
   585     by simp
   586 qed
   587 
   588 lemma divmod_digit_1:
   589   assumes "0 \<le> a" "0 < b" and "b \<le> a mod (2 * b)"
   590   shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P")
   591     and "a mod (2 * b) - b = a mod b" (is "?Q")
   592 proof -
   593   from assms mod_less_eq_dividend [of a "2 * b"] have "b \<le> a"
   594     by (auto intro: trans)
   595   with \<open>0 < b\<close> have "0 < a div b" by (auto intro: div_positive)
   596   then have [simp]: "1 \<le> a div b" by (simp add: discrete)
   597   with \<open>0 < b\<close> have mod_less: "a mod b < b" by (simp add: pos_mod_bound)
   598   define w where "w = a div b mod 2"
   599   with parity have w_exhaust: "w = 0 \<or> w = 1" by auto
   600   have mod_w: "a mod (2 * b) = a mod b + b * w"
   601     by (simp add: w_def mod_mult2_eq ac_simps)
   602   from assms w_exhaust have "w = 1"
   603     by (auto simp add: mod_w) (insert mod_less, auto)
   604   with mod_w have mod: "a mod (2 * b) = a mod b + b" by simp
   605   have "2 * (a div (2 * b)) = a div b - w"
   606     by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
   607   with \<open>w = 1\<close> have div: "2 * (a div (2 * b)) = a div b - 1" by simp
   608   then show ?P and ?Q
   609     by (simp_all add: div mod add_implies_diff [symmetric])
   610 qed
   611 
   612 lemma divmod_digit_0:
   613   assumes "0 < b" and "a mod (2 * b) < b"
   614   shows "2 * (a div (2 * b)) = a div b" (is "?P")
   615     and "a mod (2 * b) = a mod b" (is "?Q")
   616 proof -
   617   define w where "w = a div b mod 2"
   618   with parity have w_exhaust: "w = 0 \<or> w = 1" by auto
   619   have mod_w: "a mod (2 * b) = a mod b + b * w"
   620     by (simp add: w_def mod_mult2_eq ac_simps)
   621   moreover have "b \<le> a mod b + b"
   622   proof -
   623     from \<open>0 < b\<close> pos_mod_sign have "0 \<le> a mod b" by blast
   624     then have "0 + b \<le> a mod b + b" by (rule add_right_mono)
   625     then show ?thesis by simp
   626   qed
   627   moreover note assms w_exhaust
   628   ultimately have "w = 0" by auto
   629   with mod_w have mod: "a mod (2 * b) = a mod b" by simp
   630   have "2 * (a div (2 * b)) = a div b - w"
   631     by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
   632   with \<open>w = 0\<close> have div: "2 * (a div (2 * b)) = a div b" by simp
   633   then show ?P and ?Q
   634     by (simp_all add: div mod)
   635 qed
   636 
   637 lemma fst_divmod:
   638   "fst (divmod m n) = numeral m div numeral n"
   639   by (simp add: divmod_def)
   640 
   641 lemma snd_divmod:
   642   "snd (divmod m n) = numeral m mod numeral n"
   643   by (simp add: divmod_def)
   644 
   645 text \<open>
   646   This is a formulation of one step (referring to one digit position)
   647   in school-method division: compare the dividend at the current
   648   digit position with the remainder from previous division steps
   649   and evaluate accordingly.
   650 \<close>
   651 
   652 lemma divmod_step_eq [simp]:
   653   "divmod_step l (q, r) = (if numeral l \<le> r
   654     then (2 * q + 1, r - numeral l) else (2 * q, r))"
   655   by (simp add: divmod_step_def)
   656 
   657 text \<open>
   658   This is a formulation of school-method division.
   659   If the divisor is smaller than the dividend, terminate.
   660   If not, shift the dividend to the right until termination
   661   occurs and then reiterate single division steps in the
   662   opposite direction.
   663 \<close>
   664 
   665 lemma divmod_divmod_step:
   666   "divmod m n = (if m < n then (0, numeral m)
   667     else divmod_step n (divmod m (Num.Bit0 n)))"
   668 proof (cases "m < n")
   669   case True then have "numeral m < numeral n" by simp
   670   then show ?thesis
   671     by (simp add: prod_eq_iff div_less mod_less fst_divmod snd_divmod)
   672 next
   673   case False
   674   have "divmod m n =
   675     divmod_step n (numeral m div (2 * numeral n),
   676       numeral m mod (2 * numeral n))"
   677   proof (cases "numeral n \<le> numeral m mod (2 * numeral n)")
   678     case True
   679     with divmod_step_eq
   680       have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
   681         (2 * (numeral m div (2 * numeral n)) + 1, numeral m mod (2 * numeral n) - numeral n)"
   682         by simp
   683     moreover from True divmod_digit_1 [of "numeral m" "numeral n"]
   684       have "2 * (numeral m div (2 * numeral n)) + 1 = numeral m div numeral n"
   685       and "numeral m mod (2 * numeral n) - numeral n = numeral m mod numeral n"
   686       by simp_all
   687     ultimately show ?thesis by (simp only: divmod_def)
   688   next
   689     case False then have *: "numeral m mod (2 * numeral n) < numeral n"
   690       by (simp add: not_le)
   691     with divmod_step_eq
   692       have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
   693         (2 * (numeral m div (2 * numeral n)), numeral m mod (2 * numeral n))"
   694         by auto
   695     moreover from * divmod_digit_0 [of "numeral n" "numeral m"]
   696       have "2 * (numeral m div (2 * numeral n)) = numeral m div numeral n"
   697       and "numeral m mod (2 * numeral n) = numeral m mod numeral n"
   698       by (simp_all only: zero_less_numeral)
   699     ultimately show ?thesis by (simp only: divmod_def)
   700   qed
   701   then have "divmod m n =
   702     divmod_step n (numeral m div numeral (Num.Bit0 n),
   703       numeral m mod numeral (Num.Bit0 n))"
   704     by (simp only: numeral.simps distrib mult_1)
   705   then have "divmod m n = divmod_step n (divmod m (Num.Bit0 n))"
   706     by (simp add: divmod_def)
   707   with False show ?thesis by simp
   708 qed
   709 
   710 text \<open>The division rewrite proper -- first, trivial results involving \<open>1\<close>\<close>
   711 
   712 lemma divmod_trivial [simp]:
   713   "divmod Num.One Num.One = (numeral Num.One, 0)"
   714   "divmod (Num.Bit0 m) Num.One = (numeral (Num.Bit0 m), 0)"
   715   "divmod (Num.Bit1 m) Num.One = (numeral (Num.Bit1 m), 0)"
   716   "divmod num.One (num.Bit0 n) = (0, Numeral1)"
   717   "divmod num.One (num.Bit1 n) = (0, Numeral1)"
   718   using divmod_divmod_step [of "Num.One"] by (simp_all add: divmod_def)
   719 
   720 text \<open>Division by an even number is a right-shift\<close>
   721 
   722 lemma divmod_cancel [simp]:
   723   "divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))" (is ?P)
   724   "divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r + 1))" (is ?Q)
   725 proof -
   726   have *: "\<And>q. numeral (Num.Bit0 q) = 2 * numeral q"
   727     "\<And>q. numeral (Num.Bit1 q) = 2 * numeral q + 1"
   728     by (simp_all only: numeral_mult numeral.simps distrib) simp_all
   729   have "1 div 2 = 0" "1 mod 2 = 1" by (auto intro: div_less mod_less)
   730   then show ?P and ?Q
   731     by (simp_all add: fst_divmod snd_divmod prod_eq_iff split_def * [of m] * [of n] mod_mult_mult1
   732       div_mult2_eq [of _ _ 2] mod_mult2_eq [of _ _ 2]
   733       add.commute del: numeral_times_numeral)
   734 qed
   735 
   736 text \<open>The really hard work\<close>
   737 
   738 lemma divmod_steps [simp]:
   739   "divmod (num.Bit0 m) (num.Bit1 n) =
   740       (if m \<le> n then (0, numeral (num.Bit0 m))
   741        else divmod_step (num.Bit1 n)
   742              (divmod (num.Bit0 m)
   743                (num.Bit0 (num.Bit1 n))))"
   744   "divmod (num.Bit1 m) (num.Bit1 n) =
   745       (if m < n then (0, numeral (num.Bit1 m))
   746        else divmod_step (num.Bit1 n)
   747              (divmod (num.Bit1 m)
   748                (num.Bit0 (num.Bit1 n))))"
   749   by (simp_all add: divmod_divmod_step)
   750 
   751 lemmas divmod_algorithm_code = divmod_step_eq divmod_trivial divmod_cancel divmod_steps  
   752 
   753 text \<open>Special case: divisibility\<close>
   754 
   755 definition divides_aux :: "'a \<times> 'a \<Rightarrow> bool"
   756 where
   757   "divides_aux qr \<longleftrightarrow> snd qr = 0"
   758 
   759 lemma divides_aux_eq [simp]:
   760   "divides_aux (q, r) \<longleftrightarrow> r = 0"
   761   by (simp add: divides_aux_def)
   762 
   763 lemma dvd_numeral_simp [simp]:
   764   "numeral m dvd numeral n \<longleftrightarrow> divides_aux (divmod n m)"
   765   by (simp add: divmod_def mod_eq_0_iff_dvd)
   766 
   767 text \<open>Generic computation of quotient and remainder\<close>  
   768 
   769 lemma numeral_div_numeral [simp]: 
   770   "numeral k div numeral l = fst (divmod k l)"
   771   by (simp add: fst_divmod)
   772 
   773 lemma numeral_mod_numeral [simp]: 
   774   "numeral k mod numeral l = snd (divmod k l)"
   775   by (simp add: snd_divmod)
   776 
   777 lemma one_div_numeral [simp]:
   778   "1 div numeral n = fst (divmod num.One n)"
   779   by (simp add: fst_divmod)
   780 
   781 lemma one_mod_numeral [simp]:
   782   "1 mod numeral n = snd (divmod num.One n)"
   783   by (simp add: snd_divmod)
   784 
   785 text \<open>Computing congruences modulo \<open>2 ^ q\<close>\<close>
   786 
   787 lemma cong_exp_iff_simps:
   788   "numeral n mod numeral Num.One = 0
   789     \<longleftrightarrow> True"
   790   "numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) = 0
   791     \<longleftrightarrow> numeral n mod numeral q = 0"
   792   "numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) = 0
   793     \<longleftrightarrow> False"
   794   "numeral m mod numeral Num.One = (numeral n mod numeral Num.One)
   795     \<longleftrightarrow> True"
   796   "numeral Num.One mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
   797     \<longleftrightarrow> True"
   798   "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
   799     \<longleftrightarrow> False"
   800   "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
   801     \<longleftrightarrow> (numeral n mod numeral q) = 0"
   802   "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
   803     \<longleftrightarrow> False"
   804   "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
   805     \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
   806   "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
   807     \<longleftrightarrow> False"
   808   "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
   809     \<longleftrightarrow> (numeral m mod numeral q) = 0"
   810   "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
   811     \<longleftrightarrow> False"
   812   "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
   813     \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
   814   by (auto simp add: case_prod_beta dest: arg_cong [of _ _ even])
   815 
   816 end
   817 
   818 
   819 subsection \<open>Division on @{typ nat}\<close>
   820 
   821 context
   822 begin
   823 
   824 text \<open>
   825   We define @{const divide} and @{const modulo} on @{typ nat} by means
   826   of a characteristic relation with two input arguments
   827   @{term "m::nat"}, @{term "n::nat"} and two output arguments
   828   @{term "q::nat"}(uotient) and @{term "r::nat"}(emainder).
   829 \<close>
   830 
   831 definition divmod_nat_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool" where
   832   "divmod_nat_rel m n qr \<longleftrightarrow>
   833     m = fst qr * n + snd qr \<and>
   834       (if n = 0 then fst qr = 0 else if n > 0 then 0 \<le> snd qr \<and> snd qr < n else n < snd qr \<and> snd qr \<le> 0)"
   835 
   836 text \<open>@{const divmod_nat_rel} is total:\<close>
   837 
   838 qualified lemma divmod_nat_rel_ex:
   839   obtains q r where "divmod_nat_rel m n (q, r)"
   840 proof (cases "n = 0")
   841   case True  with that show thesis
   842     by (auto simp add: divmod_nat_rel_def)
   843 next
   844   case False
   845   have "\<exists>q r. m = q * n + r \<and> r < n"
   846   proof (induct m)
   847     case 0 with \<open>n \<noteq> 0\<close>
   848     have "(0::nat) = 0 * n + 0 \<and> 0 < n" by simp
   849     then show ?case by blast
   850   next
   851     case (Suc m) then obtain q' r'
   852       where m: "m = q' * n + r'" and n: "r' < n" by auto
   853     then show ?case proof (cases "Suc r' < n")
   854       case True
   855       from m n have "Suc m = q' * n + Suc r'" by simp
   856       with True show ?thesis by blast
   857     next
   858       case False then have "n \<le> Suc r'"
   859         by (simp add: not_less)
   860       moreover from n have "Suc r' \<le> n"
   861         by (simp add: Suc_le_eq)
   862       ultimately have "n = Suc r'" by auto
   863       with m have "Suc m = Suc q' * n + 0" by simp
   864       with \<open>n \<noteq> 0\<close> show ?thesis by blast
   865     qed
   866   qed
   867   with that show thesis
   868     using \<open>n \<noteq> 0\<close> by (auto simp add: divmod_nat_rel_def)
   869 qed
   870 
   871 text \<open>@{const divmod_nat_rel} is injective:\<close>
   872 
   873 qualified lemma divmod_nat_rel_unique:
   874   assumes "divmod_nat_rel m n qr"
   875     and "divmod_nat_rel m n qr'"
   876   shows "qr = qr'"
   877 proof (cases "n = 0")
   878   case True with assms show ?thesis
   879     by (cases qr, cases qr')
   880       (simp add: divmod_nat_rel_def)
   881 next
   882   case False
   883   have aux: "\<And>q r q' r'. q' * n + r' = q * n + r \<Longrightarrow> r < n \<Longrightarrow> q' \<le> (q::nat)"
   884   apply (rule leI)
   885   apply (subst less_iff_Suc_add)
   886   apply (auto simp add: add_mult_distrib)
   887   done
   888   from \<open>n \<noteq> 0\<close> assms have *: "fst qr = fst qr'"
   889     by (auto simp add: divmod_nat_rel_def intro: order_antisym dest: aux sym split: if_splits)
   890   with assms have "snd qr = snd qr'"
   891     by (simp add: divmod_nat_rel_def)
   892   with * show ?thesis by (cases qr, cases qr') simp
   893 qed
   894 
   895 text \<open>
   896   We instantiate divisibility on the natural numbers by
   897   means of @{const divmod_nat_rel}:
   898 \<close>
   899 
   900 qualified definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
   901   "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)"
   902 
   903 qualified lemma divmod_nat_rel_divmod_nat:
   904   "divmod_nat_rel m n (divmod_nat m n)"
   905 proof -
   906   from divmod_nat_rel_ex
   907     obtain qr where rel: "divmod_nat_rel m n qr" .
   908   then show ?thesis
   909   by (auto simp add: divmod_nat_def intro: theI elim: divmod_nat_rel_unique)
   910 qed
   911 
   912 qualified lemma divmod_nat_unique:
   913   assumes "divmod_nat_rel m n qr"
   914   shows "divmod_nat m n = qr"
   915   using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
   916 
   917 qualified lemma divmod_nat_zero: "divmod_nat m 0 = (0, m)"
   918   by (simp add: divmod_nat_unique divmod_nat_rel_def)
   919 
   920 qualified lemma divmod_nat_zero_left: "divmod_nat 0 n = (0, 0)"
   921   by (simp add: divmod_nat_unique divmod_nat_rel_def)
   922 
   923 qualified lemma divmod_nat_base: "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
   924   by (simp add: divmod_nat_unique divmod_nat_rel_def)
   925 
   926 qualified lemma divmod_nat_step:
   927   assumes "0 < n" and "n \<le> m"
   928   shows "divmod_nat m n = apfst Suc (divmod_nat (m - n) n)"
   929 proof (rule divmod_nat_unique)
   930   have "divmod_nat_rel (m - n) n (divmod_nat (m - n) n)"
   931     by (fact divmod_nat_rel_divmod_nat)
   932   then show "divmod_nat_rel m n (apfst Suc (divmod_nat (m - n) n))"
   933     unfolding divmod_nat_rel_def using assms
   934       by (auto split: if_splits simp add: algebra_simps)
   935 qed
   936 
   937 end
   938 
   939 instantiation nat :: "{semidom_modulo, normalization_semidom}"
   940 begin
   941 
   942 definition normalize_nat :: "nat \<Rightarrow> nat"
   943   where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
   944 
   945 definition unit_factor_nat :: "nat \<Rightarrow> nat"
   946   where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
   947 
   948 lemma unit_factor_simps [simp]:
   949   "unit_factor 0 = (0::nat)"
   950   "unit_factor (Suc n) = 1"
   951   by (simp_all add: unit_factor_nat_def)
   952 
   953 definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   954   where div_nat_def: "m div n = fst (Divides.divmod_nat m n)"
   955 
   956 definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   957   where mod_nat_def: "m mod n = snd (Divides.divmod_nat m n)"
   958 
   959 lemma fst_divmod_nat [simp]:
   960   "fst (Divides.divmod_nat m n) = m div n"
   961   by (simp add: div_nat_def)
   962 
   963 lemma snd_divmod_nat [simp]:
   964   "snd (Divides.divmod_nat m n) = m mod n"
   965   by (simp add: mod_nat_def)
   966 
   967 lemma divmod_nat_div_mod:
   968   "Divides.divmod_nat m n = (m div n, m mod n)"
   969   by (simp add: prod_eq_iff)
   970 
   971 lemma div_nat_unique:
   972   assumes "divmod_nat_rel m n (q, r)"
   973   shows "m div n = q"
   974   using assms
   975   by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
   976 
   977 lemma mod_nat_unique:
   978   assumes "divmod_nat_rel m n (q, r)"
   979   shows "m mod n = r"
   980   using assms
   981   by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
   982 
   983 lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)"
   984   using Divides.divmod_nat_rel_divmod_nat
   985   by (simp add: divmod_nat_div_mod)
   986 
   987 text \<open>The ''recursion'' equations for @{const divide} and @{const modulo}\<close>
   988 
   989 lemma div_less [simp]:
   990   fixes m n :: nat
   991   assumes "m < n"
   992   shows "m div n = 0"
   993   using assms Divides.divmod_nat_base by (simp add: prod_eq_iff)
   994 
   995 lemma le_div_geq:
   996   fixes m n :: nat
   997   assumes "0 < n" and "n \<le> m"
   998   shows "m div n = Suc ((m - n) div n)"
   999   using assms Divides.divmod_nat_step by (simp add: prod_eq_iff)
  1000 
  1001 lemma mod_less [simp]:
  1002   fixes m n :: nat
  1003   assumes "m < n"
  1004   shows "m mod n = m"
  1005   using assms Divides.divmod_nat_base by (simp add: prod_eq_iff)
  1006 
  1007 lemma le_mod_geq:
  1008   fixes m n :: nat
  1009   assumes "n \<le> m"
  1010   shows "m mod n = (m - n) mod n"
  1011   using assms Divides.divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)
  1012 
  1013 lemma mod_less_divisor [simp]:
  1014   fixes m n :: nat
  1015   assumes "n > 0"
  1016   shows "m mod n < n"
  1017   using assms divmod_nat_rel [of m n] unfolding divmod_nat_rel_def
  1018   by (auto split: if_splits)
  1019 
  1020 lemma mod_le_divisor [simp]:
  1021   fixes m n :: nat
  1022   assumes "n > 0"
  1023   shows "m mod n \<le> n"
  1024 proof (rule less_imp_le)
  1025   from assms show "m mod n < n"
  1026     by simp
  1027 qed
  1028 
  1029 instance proof
  1030   fix m n :: nat
  1031   show "m div n * n + m mod n = m"
  1032     using divmod_nat_rel [of m n] by (simp add: divmod_nat_rel_def)
  1033 next
  1034   fix n :: nat show "n div 0 = 0"
  1035     by (simp add: div_nat_def Divides.divmod_nat_zero)
  1036 next
  1037   fix m n :: nat
  1038   assume "n \<noteq> 0"
  1039   then show "m * n div n = m"
  1040     by (auto simp add: divmod_nat_rel_def intro: div_nat_unique [of _ _ _ 0])
  1041 qed (simp_all add: unit_factor_nat_def)
  1042 
  1043 end
  1044 
  1045 instance nat :: semiring_div
  1046 proof
  1047   fix m n q :: nat
  1048   assume "n \<noteq> 0"
  1049   then show "(q + m * n) div n = m + q div n"
  1050     by (induct m) (simp_all add: le_div_geq)
  1051 next
  1052   fix m n q :: nat
  1053   assume "m \<noteq> 0"
  1054   then have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))"
  1055     using div_mult_mod_eq [of n q]
  1056     by (auto simp add: divmod_nat_rel_def algebra_simps distrib_left [symmetric] simp del: distrib_left)
  1057   then show "(m * n) div (m * q) = n div q"
  1058     by (rule div_nat_unique)
  1059 qed
  1060 
  1061 lemma div_by_Suc_0 [simp]:
  1062   "m div Suc 0 = m"
  1063   using div_by_1 [of m] by simp
  1064 
  1065 lemma mod_by_Suc_0 [simp]:
  1066   "m mod Suc 0 = 0"
  1067   using mod_by_1 [of m] by simp
  1068 
  1069 lemma mod_greater_zero_iff_not_dvd:
  1070   fixes m n :: nat
  1071   shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
  1072   by (simp add: dvd_eq_mod_eq_0)
  1073 
  1074 text \<open>Simproc for cancelling @{const divide} and @{const modulo}\<close>
  1075 
  1076 lemma (in semiring_modulo) cancel_div_mod_rules:
  1077   "((a div b) * b + a mod b) + c = a + c"
  1078   "(b * (a div b) + a mod b) + c = a + c"
  1079   by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
  1080 
  1081 ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
  1082 
  1083 ML \<open>
  1084 structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
  1085 (
  1086   val div_name = @{const_name divide};
  1087   val mod_name = @{const_name modulo};
  1088   val mk_binop = HOLogic.mk_binop;
  1089   val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
  1090   val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
  1091   fun mk_sum [] = HOLogic.zero
  1092     | mk_sum [t] = t
  1093     | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
  1094   fun dest_sum tm =
  1095     if HOLogic.is_zero tm then []
  1096     else
  1097       (case try HOLogic.dest_Suc tm of
  1098         SOME t => HOLogic.Suc_zero :: dest_sum t
  1099       | NONE =>
  1100           (case try dest_plus tm of
  1101             SOME (t, u) => dest_sum t @ dest_sum u
  1102           | NONE => [tm]));
  1103 
  1104   val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
  1105 
  1106   val prove_eq_sums = Arith_Data.prove_conv2 all_tac
  1107     (Arith_Data.simp_all_tac @{thms add_0_left add_0_right ac_simps})
  1108 )
  1109 \<close>
  1110 
  1111 simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
  1112   \<open>K Cancel_Div_Mod_Nat.proc\<close>
  1113 
  1114 lemma divmod_nat_if [code]:
  1115   "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
  1116     let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
  1117   by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
  1118 
  1119 lemma mod_Suc_eq [mod_simps]:
  1120   "Suc (m mod n) mod n = Suc m mod n"
  1121 proof -
  1122   have "(m mod n + 1) mod n = (m + 1) mod n"
  1123     by (simp only: mod_simps)
  1124   then show ?thesis
  1125     by simp
  1126 qed
  1127 
  1128 lemma mod_Suc_Suc_eq [mod_simps]:
  1129   "Suc (Suc (m mod n)) mod n = Suc (Suc m) mod n"
  1130 proof -
  1131   have "(m mod n + 2) mod n = (m + 2) mod n"
  1132     by (simp only: mod_simps)
  1133   then show ?thesis
  1134     by simp
  1135 qed
  1136 
  1137 
  1138 subsubsection \<open>Quotient\<close>
  1139 
  1140 lemma div_geq: "0 < n \<Longrightarrow>  \<not> m < n \<Longrightarrow> m div n = Suc ((m - n) div n)"
  1141 by (simp add: le_div_geq linorder_not_less)
  1142 
  1143 lemma div_if: "0 < n \<Longrightarrow> m div n = (if m < n then 0 else Suc ((m - n) div n))"
  1144 by (simp add: div_geq)
  1145 
  1146 lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
  1147 by simp
  1148 
  1149 lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
  1150 by simp
  1151 
  1152 lemma div_positive:
  1153   fixes m n :: nat
  1154   assumes "n > 0"
  1155   assumes "m \<ge> n"
  1156   shows "m div n > 0"
  1157 proof -
  1158   from \<open>m \<ge> n\<close> obtain q where "m = n + q"
  1159     by (auto simp add: le_iff_add)
  1160   with \<open>n > 0\<close> show ?thesis by (simp add: div_add_self1)
  1161 qed
  1162 
  1163 lemma div_eq_0_iff: "(a div b::nat) = 0 \<longleftrightarrow> a < b \<or> b = 0"
  1164   by auto (metis div_positive less_numeral_extra(3) not_less)
  1165 
  1166 
  1167 subsubsection \<open>Remainder\<close>
  1168 
  1169 lemma mod_Suc_le_divisor [simp]:
  1170   "m mod Suc n \<le> n"
  1171   using mod_less_divisor [of "Suc n" m] by arith
  1172 
  1173 lemma mod_less_eq_dividend [simp]:
  1174   fixes m n :: nat
  1175   shows "m mod n \<le> m"
  1176 proof (rule add_leD2)
  1177   from div_mult_mod_eq have "m div n * n + m mod n = m" .
  1178   then show "m div n * n + m mod n \<le> m" by auto
  1179 qed
  1180 
  1181 lemma mod_geq: "\<not> m < (n::nat) \<Longrightarrow> m mod n = (m - n) mod n"
  1182 by (simp add: le_mod_geq linorder_not_less)
  1183 
  1184 lemma mod_if: "m mod (n::nat) = (if m < n then m else (m - n) mod n)"
  1185 by (simp add: le_mod_geq)
  1186 
  1187 
  1188 subsubsection \<open>Quotient and Remainder\<close>
  1189 
  1190 lemma divmod_nat_rel_mult1_eq:
  1191   "divmod_nat_rel b c (q, r)
  1192    \<Longrightarrow> divmod_nat_rel (a * b) c (a * q + a * r div c, a * r mod c)"
  1193 by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps)
  1194 
  1195 lemma div_mult1_eq:
  1196   "(a * b) div c = a * (b div c) + a * (b mod c) div (c::nat)"
  1197 by (blast intro: divmod_nat_rel_mult1_eq [THEN div_nat_unique] divmod_nat_rel)
  1198 
  1199 lemma divmod_nat_rel_add1_eq:
  1200   "divmod_nat_rel a c (aq, ar) \<Longrightarrow> divmod_nat_rel b c (bq, br)
  1201    \<Longrightarrow> divmod_nat_rel (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)"
  1202 by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps)
  1203 
  1204 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
  1205 lemma div_add1_eq:
  1206   "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
  1207 by (blast intro: divmod_nat_rel_add1_eq [THEN div_nat_unique] divmod_nat_rel)
  1208 
  1209 lemma divmod_nat_rel_mult2_eq:
  1210   assumes "divmod_nat_rel a b (q, r)"
  1211   shows "divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"
  1212 proof -
  1213   { assume "r < b" and "0 < c"
  1214     then have "b * (q mod c) + r < b * c"
  1215       apply (cut_tac m = q and n = c in mod_less_divisor)
  1216       apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
  1217       apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
  1218       apply (simp add: add_mult_distrib2)
  1219       done
  1220     then have "r + b * (q mod c) < b * c"
  1221       by (simp add: ac_simps)
  1222   } with assms show ?thesis
  1223     by (auto simp add: divmod_nat_rel_def algebra_simps add_mult_distrib2 [symmetric])
  1224 qed
  1225 
  1226 lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"
  1227 by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_nat_unique])
  1228 
  1229 lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)"
  1230 by (auto simp add: mult.commute divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN mod_nat_unique])
  1231 
  1232 instantiation nat :: semiring_numeral_div
  1233 begin
  1234 
  1235 definition divmod_nat :: "num \<Rightarrow> num \<Rightarrow> nat \<times> nat"
  1236 where
  1237   divmod'_nat_def: "divmod_nat m n = (numeral m div numeral n, numeral m mod numeral n)"
  1238 
  1239 definition divmod_step_nat :: "num \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
  1240 where
  1241   "divmod_step_nat l qr = (let (q, r) = qr
  1242     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
  1243     else (2 * q, r))"
  1244 
  1245 instance
  1246   by standard (auto intro: div_positive simp add: divmod'_nat_def divmod_step_nat_def mod_mult2_eq div_mult2_eq)
  1247 
  1248 end
  1249 
  1250 declare divmod_algorithm_code [where ?'a = nat, code]
  1251   
  1252 
  1253 subsubsection \<open>Further Facts about Quotient and Remainder\<close>
  1254 
  1255 lemma div_le_mono:
  1256   fixes m n k :: nat
  1257   assumes "m \<le> n"
  1258   shows "m div k \<le> n div k"
  1259 proof -
  1260   from assms obtain q where "n = m + q"
  1261     by (auto simp add: le_iff_add)
  1262   then show ?thesis
  1263     by (simp add: div_add1_eq [of m q k])
  1264 qed
  1265 
  1266 (* Antimonotonicity of div in second argument *)
  1267 lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"
  1268 apply (subgoal_tac "0<n")
  1269  prefer 2 apply simp
  1270 apply (induct_tac k rule: nat_less_induct)
  1271 apply (rename_tac "k")
  1272 apply (case_tac "k<n", simp)
  1273 apply (subgoal_tac "~ (k<m) ")
  1274  prefer 2 apply simp
  1275 apply (simp add: div_geq)
  1276 apply (subgoal_tac "(k-n) div n \<le> (k-m) div n")
  1277  prefer 2
  1278  apply (blast intro: div_le_mono diff_le_mono2)
  1279 apply (rule le_trans, simp)
  1280 apply (simp)
  1281 done
  1282 
  1283 lemma div_le_dividend [simp]: "m div n \<le> (m::nat)"
  1284 apply (case_tac "n=0", simp)
  1285 apply (subgoal_tac "m div n \<le> m div 1", simp)
  1286 apply (rule div_le_mono2)
  1287 apply (simp_all (no_asm_simp))
  1288 done
  1289 
  1290 (* Similar for "less than" *)
  1291 lemma div_less_dividend [simp]:
  1292   "\<lbrakk>(1::nat) < n; 0 < m\<rbrakk> \<Longrightarrow> m div n < m"
  1293 apply (induct m rule: nat_less_induct)
  1294 apply (rename_tac "m")
  1295 apply (case_tac "m<n", simp)
  1296 apply (subgoal_tac "0<n")
  1297  prefer 2 apply simp
  1298 apply (simp add: div_geq)
  1299 apply (case_tac "n<m")
  1300  apply (subgoal_tac "(m-n) div n < (m-n) ")
  1301   apply (rule impI less_trans_Suc)+
  1302 apply assumption
  1303   apply (simp_all)
  1304 done
  1305 
  1306 text\<open>A fact for the mutilated chess board\<close>
  1307 lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"
  1308 apply (case_tac "n=0", simp)
  1309 apply (induct "m" rule: nat_less_induct)
  1310 apply (case_tac "Suc (na) <n")
  1311 (* case Suc(na) < n *)
  1312 apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
  1313 (* case n \<le> Suc(na) *)
  1314 apply (simp add: linorder_not_less le_Suc_eq mod_geq)
  1315 apply (auto simp add: Suc_diff_le le_mod_geq)
  1316 done
  1317 
  1318 lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
  1319 by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
  1320 
  1321 lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
  1322 
  1323 (*Loses information, namely we also have r<d provided d is nonzero*)
  1324 lemma mod_eqD:
  1325   fixes m d r q :: nat
  1326   assumes "m mod d = r"
  1327   shows "\<exists>q. m = r + q * d"
  1328 proof -
  1329   from div_mult_mod_eq obtain q where "q * d + m mod d = m" by blast
  1330   with assms have "m = r + q * d" by simp
  1331   then show ?thesis ..
  1332 qed
  1333 
  1334 lemma split_div:
  1335  "P(n div k :: nat) =
  1336  ((k = 0 \<longrightarrow> P 0) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P i)))"
  1337  (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
  1338 proof
  1339   assume P: ?P
  1340   show ?Q
  1341   proof (cases)
  1342     assume "k = 0"
  1343     with P show ?Q by simp
  1344   next
  1345     assume not0: "k \<noteq> 0"
  1346     thus ?Q
  1347     proof (simp, intro allI impI)
  1348       fix i j
  1349       assume n: "n = k*i + j" and j: "j < k"
  1350       show "P i"
  1351       proof (cases)
  1352         assume "i = 0"
  1353         with n j P show "P i" by simp
  1354       next
  1355         assume "i \<noteq> 0"
  1356         with not0 n j P show "P i" by(simp add:ac_simps)
  1357       qed
  1358     qed
  1359   qed
  1360 next
  1361   assume Q: ?Q
  1362   show ?P
  1363   proof (cases)
  1364     assume "k = 0"
  1365     with Q show ?P by simp
  1366   next
  1367     assume not0: "k \<noteq> 0"
  1368     with Q have R: ?R by simp
  1369     from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
  1370     show ?P by simp
  1371   qed
  1372 qed
  1373 
  1374 lemma split_div_lemma:
  1375   assumes "0 < n"
  1376   shows "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> q = ((m::nat) div n)" (is "?lhs \<longleftrightarrow> ?rhs")
  1377 proof
  1378   assume ?rhs
  1379   with minus_mod_eq_mult_div [symmetric] have nq: "n * q = m - (m mod n)" by simp
  1380   then have A: "n * q \<le> m" by simp
  1381   have "n - (m mod n) > 0" using mod_less_divisor assms by auto
  1382   then have "m < m + (n - (m mod n))" by simp
  1383   then have "m < n + (m - (m mod n))" by simp
  1384   with nq have "m < n + n * q" by simp
  1385   then have B: "m < n * Suc q" by simp
  1386   from A B show ?lhs ..
  1387 next
  1388   assume P: ?lhs
  1389   then have "divmod_nat_rel m n (q, m - n * q)"
  1390     unfolding divmod_nat_rel_def by (auto simp add: ac_simps)
  1391   then have "m div n = q"
  1392     by (rule div_nat_unique)
  1393   then show ?rhs by simp
  1394 qed
  1395 
  1396 theorem split_div':
  1397   "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>
  1398    (\<exists>q. (n * q \<le> m \<and> m < n * (Suc q)) \<and> P q))"
  1399   apply (cases "0 < n")
  1400   apply (simp only: add: split_div_lemma)
  1401   apply simp_all
  1402   done
  1403 
  1404 lemma split_mod:
  1405  "P(n mod k :: nat) =
  1406  ((k = 0 \<longrightarrow> P n) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P j)))"
  1407  (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
  1408 proof
  1409   assume P: ?P
  1410   show ?Q
  1411   proof (cases)
  1412     assume "k = 0"
  1413     with P show ?Q by simp
  1414   next
  1415     assume not0: "k \<noteq> 0"
  1416     thus ?Q
  1417     proof (simp, intro allI impI)
  1418       fix i j
  1419       assume "n = k*i + j" "j < k"
  1420       thus "P j" using not0 P by (simp add: ac_simps)
  1421     qed
  1422   qed
  1423 next
  1424   assume Q: ?Q
  1425   show ?P
  1426   proof (cases)
  1427     assume "k = 0"
  1428     with Q show ?P by simp
  1429   next
  1430     assume not0: "k \<noteq> 0"
  1431     with Q have R: ?R by simp
  1432     from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
  1433     show ?P by simp
  1434   qed
  1435 qed
  1436 
  1437 lemma div_eq_dividend_iff: "a \<noteq> 0 \<Longrightarrow> (a :: nat) div b = a \<longleftrightarrow> b = 1"
  1438   apply rule
  1439   apply (cases "b = 0")
  1440   apply simp_all
  1441   apply (metis (full_types) One_nat_def Suc_lessI div_less_dividend less_not_refl3)
  1442   done
  1443 
  1444 lemma (in field_char_0) of_nat_div:
  1445   "of_nat (m div n) = ((of_nat m - of_nat (m mod n)) / of_nat n)"
  1446 proof -
  1447   have "of_nat (m div n) = ((of_nat (m div n * n + m mod n) - of_nat (m mod n)) / of_nat n :: 'a)"
  1448     unfolding of_nat_add by (cases "n = 0") simp_all
  1449   then show ?thesis
  1450     by simp
  1451 qed
  1452 
  1453 
  1454 subsubsection \<open>An ``induction'' law for modulus arithmetic.\<close>
  1455 
  1456 lemma mod_induct_0:
  1457   assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
  1458   and base: "P i" and i: "i<p"
  1459   shows "P 0"
  1460 proof (rule ccontr)
  1461   assume contra: "\<not>(P 0)"
  1462   from i have p: "0<p" by simp
  1463   have "\<forall>k. 0<k \<longrightarrow> \<not> P (p-k)" (is "\<forall>k. ?A k")
  1464   proof
  1465     fix k
  1466     show "?A k"
  1467     proof (induct k)
  1468       show "?A 0" by simp  \<comment> "by contradiction"
  1469     next
  1470       fix n
  1471       assume ih: "?A n"
  1472       show "?A (Suc n)"
  1473       proof (clarsimp)
  1474         assume y: "P (p - Suc n)"
  1475         have n: "Suc n < p"
  1476         proof (rule ccontr)
  1477           assume "\<not>(Suc n < p)"
  1478           hence "p - Suc n = 0"
  1479             by simp
  1480           with y contra show "False"
  1481             by simp
  1482         qed
  1483         hence n2: "Suc (p - Suc n) = p-n" by arith
  1484         from p have "p - Suc n < p" by arith
  1485         with y step have z: "P ((Suc (p - Suc n)) mod p)"
  1486           by blast
  1487         show "False"
  1488         proof (cases "n=0")
  1489           case True
  1490           with z n2 contra show ?thesis by simp
  1491         next
  1492           case False
  1493           with p have "p-n < p" by arith
  1494           with z n2 False ih show ?thesis by simp
  1495         qed
  1496       qed
  1497     qed
  1498   qed
  1499   moreover
  1500   from i obtain k where "0<k \<and> i+k=p"
  1501     by (blast dest: less_imp_add_positive)
  1502   hence "0<k \<and> i=p-k" by auto
  1503   moreover
  1504   note base
  1505   ultimately
  1506   show "False" by blast
  1507 qed
  1508 
  1509 lemma mod_induct:
  1510   assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
  1511   and base: "P i" and i: "i<p" and j: "j<p"
  1512   shows "P j"
  1513 proof -
  1514   have "\<forall>j<p. P j"
  1515   proof
  1516     fix j
  1517     show "j<p \<longrightarrow> P j" (is "?A j")
  1518     proof (induct j)
  1519       from step base i show "?A 0"
  1520         by (auto elim: mod_induct_0)
  1521     next
  1522       fix k
  1523       assume ih: "?A k"
  1524       show "?A (Suc k)"
  1525       proof
  1526         assume suc: "Suc k < p"
  1527         hence k: "k<p" by simp
  1528         with ih have "P k" ..
  1529         with step k have "P (Suc k mod p)"
  1530           by blast
  1531         moreover
  1532         from suc have "Suc k mod p = Suc k"
  1533           by simp
  1534         ultimately
  1535         show "P (Suc k)" by simp
  1536       qed
  1537     qed
  1538   qed
  1539   with j show ?thesis by blast
  1540 qed
  1541 
  1542 lemma div2_Suc_Suc [simp]: "Suc (Suc m) div 2 = Suc (m div 2)"
  1543   by (simp add: numeral_2_eq_2 le_div_geq)
  1544 
  1545 lemma mod2_Suc_Suc [simp]: "Suc (Suc m) mod 2 = m mod 2"
  1546   by (simp add: numeral_2_eq_2 le_mod_geq)
  1547 
  1548 lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
  1549 by (simp add: mult_2 [symmetric])
  1550 
  1551 lemma mod2_gr_0 [simp]: "0 < (m::nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
  1552 proof -
  1553   { fix n :: nat have  "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (cases n) simp_all }
  1554   moreover have "m mod 2 < 2" by simp
  1555   ultimately have "m mod 2 = 0 \<or> m mod 2 = 1" .
  1556   then show ?thesis by auto
  1557 qed
  1558 
  1559 text\<open>These lemmas collapse some needless occurrences of Suc:
  1560     at least three Sucs, since two and fewer are rewritten back to Suc again!
  1561     We already have some rules to simplify operands smaller than 3.\<close>
  1562 
  1563 lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
  1564 by (simp add: Suc3_eq_add_3)
  1565 
  1566 lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
  1567 by (simp add: Suc3_eq_add_3)
  1568 
  1569 lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
  1570 by (simp add: Suc3_eq_add_3)
  1571 
  1572 lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
  1573 by (simp add: Suc3_eq_add_3)
  1574 
  1575 lemmas Suc_div_eq_add3_div_numeral [simp] = Suc_div_eq_add3_div [of _ "numeral v"] for v
  1576 lemmas Suc_mod_eq_add3_mod_numeral [simp] = Suc_mod_eq_add3_mod [of _ "numeral v"] for v
  1577 
  1578 lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1"
  1579 apply (induct "m")
  1580 apply (simp_all add: mod_Suc)
  1581 done
  1582 
  1583 declare Suc_times_mod_eq [of "numeral w", simp] for w
  1584 
  1585 lemma Suc_div_le_mono [simp]: "n div k \<le> (Suc n) div k"
  1586 by (simp add: div_le_mono)
  1587 
  1588 lemma Suc_n_div_2_gt_zero [simp]: "(0::nat) < n ==> 0 < (n + 1) div 2"
  1589 by (cases n) simp_all
  1590 
  1591 lemma div_2_gt_zero [simp]: assumes A: "(1::nat) < n" shows "0 < n div 2"
  1592 proof -
  1593   from A have B: "0 < n - 1" and C: "n - 1 + 1 = n" by simp_all
  1594   from Suc_n_div_2_gt_zero [OF B] C show ?thesis by simp
  1595 qed
  1596 
  1597 lemma mod_mult_self4 [simp]: "Suc (k*n + m) mod n = Suc m mod n"
  1598 proof -
  1599   have "Suc (k * n + m) mod n = (k * n + Suc m) mod n" by simp
  1600   also have "... = Suc m mod n" by (rule mod_mult_self3)
  1601   finally show ?thesis .
  1602 qed
  1603 
  1604 lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n"
  1605 apply (subst mod_Suc [of m])
  1606 apply (subst mod_Suc [of "m mod n"], simp)
  1607 done
  1608 
  1609 lemma mod_2_not_eq_zero_eq_one_nat:
  1610   fixes n :: nat
  1611   shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
  1612   by (fact not_mod_2_eq_0_eq_1)
  1613 
  1614 lemma even_Suc_div_two [simp]:
  1615   "even n \<Longrightarrow> Suc n div 2 = n div 2"
  1616   using even_succ_div_two [of n] by simp
  1617 
  1618 lemma odd_Suc_div_two [simp]:
  1619   "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
  1620   using odd_succ_div_two [of n] by simp
  1621 
  1622 lemma odd_two_times_div_two_nat [simp]:
  1623   assumes "odd n"
  1624   shows "2 * (n div 2) = n - (1 :: nat)"
  1625 proof -
  1626   from assms have "2 * (n div 2) + 1 = n"
  1627     by (rule odd_two_times_div_two_succ)
  1628   then have "Suc (2 * (n div 2)) - 1 = n - 1"
  1629     by simp
  1630   then show ?thesis
  1631     by simp
  1632 qed
  1633 
  1634 lemma parity_induct [case_names zero even odd]:
  1635   assumes zero: "P 0"
  1636   assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
  1637   assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
  1638   shows "P n"
  1639 proof (induct n rule: less_induct)
  1640   case (less n)
  1641   show "P n"
  1642   proof (cases "n = 0")
  1643     case True with zero show ?thesis by simp
  1644   next
  1645     case False
  1646     with less have hyp: "P (n div 2)" by simp
  1647     show ?thesis
  1648     proof (cases "even n")
  1649       case True
  1650       with hyp even [of "n div 2"] show ?thesis
  1651         by simp
  1652     next
  1653       case False
  1654       with hyp odd [of "n div 2"] show ?thesis
  1655         by simp
  1656     qed
  1657   qed
  1658 qed
  1659 
  1660 lemma Suc_0_div_numeral [simp]:
  1661   fixes k l :: num
  1662   shows "Suc 0 div numeral k = fst (divmod Num.One k)"
  1663   by (simp_all add: fst_divmod)
  1664 
  1665 lemma Suc_0_mod_numeral [simp]:
  1666   fixes k l :: num
  1667   shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
  1668   by (simp_all add: snd_divmod)
  1669 
  1670 
  1671 subsection \<open>Division on @{typ int}\<close>
  1672 
  1673 context
  1674 begin
  1675 
  1676 definition divmod_int_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" \<comment> \<open>definition of quotient and remainder\<close>
  1677   where "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
  1678     (if 0 < b then 0 \<le> r \<and> r < b else if b < 0 then b < r \<and> r \<le> 0 else q = 0))"
  1679 
  1680 lemma unique_quotient_lemma:
  1681   "b * q' + r' \<le> b * q + r \<Longrightarrow> 0 \<le> r' \<Longrightarrow> r' < b \<Longrightarrow> r < b \<Longrightarrow> q' \<le> (q::int)"
  1682 apply (subgoal_tac "r' + b * (q'-q) \<le> r")
  1683  prefer 2 apply (simp add: right_diff_distrib)
  1684 apply (subgoal_tac "0 < b * (1 + q - q') ")
  1685 apply (erule_tac [2] order_le_less_trans)
  1686  prefer 2 apply (simp add: right_diff_distrib distrib_left)
  1687 apply (subgoal_tac "b * q' < b * (1 + q) ")
  1688  prefer 2 apply (simp add: right_diff_distrib distrib_left)
  1689 apply (simp add: mult_less_cancel_left)
  1690 done
  1691 
  1692 lemma unique_quotient_lemma_neg:
  1693   "b * q' + r' \<le> b*q + r \<Longrightarrow> r \<le> 0 \<Longrightarrow> b < r \<Longrightarrow> b < r' \<Longrightarrow> q \<le> (q'::int)"
  1694   by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma) auto
  1695 
  1696 lemma unique_quotient:
  1697   "divmod_int_rel a b (q, r) \<Longrightarrow> divmod_int_rel a b (q', r') \<Longrightarrow> q = q'"
  1698 apply (simp add: divmod_int_rel_def linorder_neq_iff split: if_split_asm)
  1699 apply (blast intro: order_antisym
  1700              dest: order_eq_refl [THEN unique_quotient_lemma]
  1701              order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
  1702 done
  1703 
  1704 lemma unique_remainder:
  1705   "divmod_int_rel a b (q, r) \<Longrightarrow> divmod_int_rel a b (q', r') \<Longrightarrow> r = r'"
  1706 apply (subgoal_tac "q = q'")
  1707  apply (simp add: divmod_int_rel_def)
  1708 apply (blast intro: unique_quotient)
  1709 done
  1710 
  1711 end
  1712 
  1713 instantiation int :: "{idom_modulo, normalization_semidom}"
  1714 begin
  1715 
  1716 definition normalize_int :: "int \<Rightarrow> int"
  1717   where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
  1718 
  1719 definition unit_factor_int :: "int \<Rightarrow> int"
  1720   where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
  1721 
  1722 definition divide_int :: "int \<Rightarrow> int \<Rightarrow> int"
  1723   where "k div l = (if l = 0 \<or> k = 0 then 0
  1724     else if k > 0 \<and> l > 0 \<or> k < 0 \<and> l < 0
  1725       then int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
  1726       else
  1727         if l dvd k then - int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
  1728         else - int (Suc (nat \<bar>k\<bar> div nat \<bar>l\<bar>)))"
  1729 
  1730 definition modulo_int :: "int \<Rightarrow> int \<Rightarrow> int"
  1731   where "k mod l = (if l = 0 then k else if l dvd k then 0
  1732     else if k > 0 \<and> l > 0 \<or> k < 0 \<and> l < 0
  1733       then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)
  1734       else sgn l * (\<bar>l\<bar> - int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)))"
  1735 
  1736 lemma divmod_int_rel:
  1737   "divmod_int_rel k l (k div l, k mod l)"
  1738 proof (cases k rule: int_cases3)
  1739   case zero
  1740   then show ?thesis
  1741     by (simp add: divmod_int_rel_def divide_int_def modulo_int_def)
  1742 next
  1743   case (pos n)
  1744   then show ?thesis
  1745     using div_mult_mod_eq [of n]
  1746     by (cases l rule: int_cases3)
  1747       (auto simp del: of_nat_mult of_nat_add
  1748         simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
  1749         divmod_int_rel_def divide_int_def modulo_int_def int_dvd_iff)
  1750 next
  1751   case (neg n)
  1752   then show ?thesis
  1753     using div_mult_mod_eq [of n]
  1754     by (cases l rule: int_cases3)
  1755       (auto simp del: of_nat_mult of_nat_add
  1756         simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
  1757         divmod_int_rel_def divide_int_def modulo_int_def int_dvd_iff)
  1758 qed
  1759 
  1760 lemma divmod_int_unique:
  1761   assumes "divmod_int_rel k l (q, r)"
  1762   shows div_int_unique: "k div l = q" and mod_int_unique: "k mod l = r"
  1763   using assms divmod_int_rel [of k l]
  1764   using unique_quotient [of k l] unique_remainder [of k l]
  1765   by auto
  1766 
  1767 instance proof
  1768   fix k l :: int
  1769   show "k div l * l + k mod l = k"
  1770     using divmod_int_rel [of k l]
  1771     unfolding divmod_int_rel_def by (simp add: ac_simps)
  1772 next
  1773   fix k :: int show "k div 0 = 0"
  1774     by (rule div_int_unique, simp add: divmod_int_rel_def)
  1775 next
  1776   fix k l :: int
  1777   assume "l \<noteq> 0"
  1778   then show "k * l div l = k"
  1779     by (auto simp add: divmod_int_rel_def ac_simps intro: div_int_unique [of _ _ _ 0])
  1780 qed (simp_all add: sgn_mult mult_sgn_abs abs_sgn_eq)
  1781 
  1782 end
  1783 
  1784 lemma is_unit_int:
  1785   "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
  1786   by auto
  1787 
  1788 instance int :: ring_div
  1789 proof
  1790   fix k l s :: int
  1791   assume "l \<noteq> 0"
  1792   then have "divmod_int_rel (k + s * l) l (s + k div l, k mod l)"
  1793     using divmod_int_rel [of k l]
  1794     unfolding divmod_int_rel_def by (auto simp: algebra_simps)
  1795   then show "(k + s * l) div l = s + k div l"
  1796     by (rule div_int_unique)
  1797 next
  1798   fix k l s :: int
  1799   assume "s \<noteq> 0"
  1800   have "\<And>q r. divmod_int_rel k l (q, r)
  1801     \<Longrightarrow> divmod_int_rel (s * k) (s * l) (q, s * r)"
  1802     unfolding divmod_int_rel_def
  1803     by (rule linorder_cases [of 0 l])
  1804       (use \<open>s \<noteq> 0\<close> in \<open>auto simp: algebra_simps
  1805       mult_less_0_iff zero_less_mult_iff mult_strict_right_mono
  1806       mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff\<close>)
  1807   then have "divmod_int_rel (s * k) (s * l) (k div l, s * (k mod l))"
  1808     using divmod_int_rel [of k l] .
  1809   then show "(s * k) div (s * l) = k div l"
  1810     by (rule div_int_unique)
  1811 qed
  1812 
  1813 ML \<open>
  1814 structure Cancel_Div_Mod_Int = Cancel_Div_Mod
  1815 (
  1816   val div_name = @{const_name divide};
  1817   val mod_name = @{const_name modulo};
  1818   val mk_binop = HOLogic.mk_binop;
  1819   val mk_sum = Arith_Data.mk_sum HOLogic.intT;
  1820   val dest_sum = Arith_Data.dest_sum;
  1821 
  1822   val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
  1823 
  1824   val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
  1825     @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
  1826 )
  1827 \<close>
  1828 
  1829 simproc_setup cancel_div_mod_int ("(k::int) + l") =
  1830   \<open>K Cancel_Div_Mod_Int.proc\<close>
  1831 
  1832 
  1833 text\<open>Basic laws about division and remainder\<close>
  1834 
  1835 lemma zdiv_int: "int (a div b) = int a div int b"
  1836   by (simp add: divide_int_def)
  1837 
  1838 lemma zmod_int: "int (a mod b) = int a mod int b"
  1839   by (simp add: modulo_int_def int_dvd_iff)
  1840 
  1841 lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
  1842   using divmod_int_rel [of a b]
  1843   by (auto simp add: divmod_int_rel_def prod_eq_iff)
  1844 
  1845 lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1]
  1846    and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2]
  1847 
  1848 lemma neg_mod_conj: "b < (0::int) \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b"
  1849   using divmod_int_rel [of a b]
  1850   by (auto simp add: divmod_int_rel_def prod_eq_iff)
  1851 
  1852 lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1]
  1853    and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2]
  1854 
  1855 
  1856 subsubsection \<open>General Properties of div and mod\<close>
  1857 
  1858 lemma div_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a div b = 0"
  1859 apply (rule div_int_unique)
  1860 apply (auto simp add: divmod_int_rel_def)
  1861 done
  1862 
  1863 lemma div_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a div b = 0"
  1864 apply (rule div_int_unique)
  1865 apply (auto simp add: divmod_int_rel_def)
  1866 done
  1867 
  1868 lemma div_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a div b = -1"
  1869 apply (rule div_int_unique)
  1870 apply (auto simp add: divmod_int_rel_def)
  1871 done
  1872 
  1873 (*There is no div_neg_pos_trivial because  0 div b = 0 would supersede it*)
  1874 
  1875 lemma mod_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a mod b = a"
  1876 apply (rule_tac q = 0 in mod_int_unique)
  1877 apply (auto simp add: divmod_int_rel_def)
  1878 done
  1879 
  1880 lemma mod_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a mod b = a"
  1881 apply (rule_tac q = 0 in mod_int_unique)
  1882 apply (auto simp add: divmod_int_rel_def)
  1883 done
  1884 
  1885 lemma mod_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a mod b = a+b"
  1886 apply (rule_tac q = "-1" in mod_int_unique)
  1887 apply (auto simp add: divmod_int_rel_def)
  1888 done
  1889 
  1890 text\<open>There is no \<open>mod_neg_pos_trivial\<close>.\<close>
  1891 
  1892 
  1893 subsubsection \<open>Laws for div and mod with Unary Minus\<close>
  1894 
  1895 lemma zminus1_lemma:
  1896      "divmod_int_rel a b (q, r) ==> b \<noteq> 0
  1897       ==> divmod_int_rel (-a) b (if r=0 then -q else -q - 1,
  1898                           if r=0 then 0 else b-r)"
  1899 by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_diff_distrib)
  1900 
  1901 
  1902 lemma zdiv_zminus1_eq_if:
  1903      "b \<noteq> (0::int)
  1904       ==> (-a) div b =
  1905           (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
  1906 by (blast intro: divmod_int_rel [THEN zminus1_lemma, THEN div_int_unique])
  1907 
  1908 lemma zmod_zminus1_eq_if:
  1909      "(-a::int) mod b = (if a mod b = 0 then 0 else  b - (a mod b))"
  1910 apply (case_tac "b = 0", simp)
  1911 apply (blast intro: divmod_int_rel [THEN zminus1_lemma, THEN mod_int_unique])
  1912 done
  1913 
  1914 lemma zmod_zminus1_not_zero:
  1915   fixes k l :: int
  1916   shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
  1917   by (simp add: mod_eq_0_iff_dvd)
  1918 
  1919 lemma zmod_zminus2_not_zero:
  1920   fixes k l :: int
  1921   shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
  1922   by (simp add: mod_eq_0_iff_dvd)
  1923 
  1924 lemma zdiv_zminus2_eq_if:
  1925      "b \<noteq> (0::int)
  1926       ==> a div (-b) =
  1927           (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
  1928 by (simp add: zdiv_zminus1_eq_if div_minus_right)
  1929 
  1930 lemma zmod_zminus2_eq_if:
  1931      "a mod (-b::int) = (if a mod b = 0 then 0 else  (a mod b) - b)"
  1932 by (simp add: zmod_zminus1_eq_if mod_minus_right)
  1933 
  1934 
  1935 subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
  1936 
  1937 lemma zdiv_mono1: "[| a \<le> a';  0 < (b::int) |] ==> a div b \<le> a' div b"
  1938 using mult_div_mod_eq [symmetric, of a b]
  1939 using mult_div_mod_eq [symmetric, of a' b]
  1940 apply -
  1941 apply (rule unique_quotient_lemma)
  1942 apply (erule subst)
  1943 apply (erule subst, simp_all)
  1944 done
  1945 
  1946 lemma zdiv_mono1_neg: "[| a \<le> a';  (b::int) < 0 |] ==> a' div b \<le> a div b"
  1947 using mult_div_mod_eq [symmetric, of a b]
  1948 using mult_div_mod_eq [symmetric, of a' b]
  1949 apply -
  1950 apply (rule unique_quotient_lemma_neg)
  1951 apply (erule subst)
  1952 apply (erule subst, simp_all)
  1953 done
  1954 
  1955 
  1956 subsubsection \<open>Monotonicity in the Second Argument (Divisor)\<close>
  1957 
  1958 lemma q_pos_lemma:
  1959      "[| 0 \<le> b'*q' + r'; r' < b';  0 < b' |] ==> 0 \<le> (q'::int)"
  1960 apply (subgoal_tac "0 < b'* (q' + 1) ")
  1961  apply (simp add: zero_less_mult_iff)
  1962 apply (simp add: distrib_left)
  1963 done
  1964 
  1965 lemma zdiv_mono2_lemma:
  1966      "[| b*q + r = b'*q' + r';  0 \<le> b'*q' + r';
  1967          r' < b';  0 \<le> r;  0 < b';  b' \<le> b |]
  1968       ==> q \<le> (q'::int)"
  1969 apply (frule q_pos_lemma, assumption+)
  1970 apply (subgoal_tac "b*q < b* (q' + 1) ")
  1971  apply (simp add: mult_less_cancel_left)
  1972 apply (subgoal_tac "b*q = r' - r + b'*q'")
  1973  prefer 2 apply simp
  1974 apply (simp (no_asm_simp) add: distrib_left)
  1975 apply (subst add.commute, rule add_less_le_mono, arith)
  1976 apply (rule mult_right_mono, auto)
  1977 done
  1978 
  1979 lemma zdiv_mono2:
  1980      "[| (0::int) \<le> a;  0 < b';  b' \<le> b |] ==> a div b \<le> a div b'"
  1981 apply (subgoal_tac "b \<noteq> 0")
  1982   prefer 2 apply arith
  1983 using mult_div_mod_eq [symmetric, of a b]
  1984 using mult_div_mod_eq [symmetric, of a b']
  1985 apply -
  1986 apply (rule zdiv_mono2_lemma)
  1987 apply (erule subst)
  1988 apply (erule subst, simp_all)
  1989 done
  1990 
  1991 lemma q_neg_lemma:
  1992      "[| b'*q' + r' < 0;  0 \<le> r';  0 < b' |] ==> q' \<le> (0::int)"
  1993 apply (subgoal_tac "b'*q' < 0")
  1994  apply (simp add: mult_less_0_iff, arith)
  1995 done
  1996 
  1997 lemma zdiv_mono2_neg_lemma:
  1998      "[| b*q + r = b'*q' + r';  b'*q' + r' < 0;
  1999          r < b;  0 \<le> r';  0 < b';  b' \<le> b |]
  2000       ==> q' \<le> (q::int)"
  2001 apply (frule q_neg_lemma, assumption+)
  2002 apply (subgoal_tac "b*q' < b* (q + 1) ")
  2003  apply (simp add: mult_less_cancel_left)
  2004 apply (simp add: distrib_left)
  2005 apply (subgoal_tac "b*q' \<le> b'*q'")
  2006  prefer 2 apply (simp add: mult_right_mono_neg, arith)
  2007 done
  2008 
  2009 lemma zdiv_mono2_neg:
  2010      "[| a < (0::int);  0 < b';  b' \<le> b |] ==> a div b' \<le> a div b"
  2011 using mult_div_mod_eq [symmetric, of a b]
  2012 using mult_div_mod_eq [symmetric, of a b']
  2013 apply -
  2014 apply (rule zdiv_mono2_neg_lemma)
  2015 apply (erule subst)
  2016 apply (erule subst, simp_all)
  2017 done
  2018 
  2019 
  2020 subsubsection \<open>More Algebraic Laws for div and mod\<close>
  2021 
  2022 text\<open>proving (a*b) div c = a * (b div c) + a * (b mod c)\<close>
  2023 
  2024 lemma zmult1_lemma:
  2025      "[| divmod_int_rel b c (q, r) |]
  2026       ==> divmod_int_rel (a * b) c (a*q + a*r div c, a*r mod c)"
  2027 by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left ac_simps)
  2028 
  2029 lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
  2030 apply (case_tac "c = 0", simp)
  2031 apply (blast intro: divmod_int_rel [THEN zmult1_lemma, THEN div_int_unique])
  2032 done
  2033 
  2034 text\<open>proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c)\<close>
  2035 
  2036 lemma zadd1_lemma:
  2037      "[| divmod_int_rel a c (aq, ar);  divmod_int_rel b c (bq, br) |]
  2038       ==> divmod_int_rel (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
  2039 by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left)
  2040 
  2041 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
  2042 lemma zdiv_zadd1_eq:
  2043      "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
  2044 apply (case_tac "c = 0", simp)
  2045 apply (blast intro: zadd1_lemma [OF divmod_int_rel divmod_int_rel] div_int_unique)
  2046 done
  2047 
  2048 lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
  2049 by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
  2050 
  2051 (* REVISIT: should this be generalized to all semiring_div types? *)
  2052 lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
  2053 
  2054 
  2055 subsubsection \<open>Proving  @{term "a div (b * c) = (a div b) div c"}\<close>
  2056 
  2057 (*The condition c>0 seems necessary.  Consider that 7 div ~6 = ~2 but
  2058   7 div 2 div ~3 = 3 div ~3 = ~1.  The subcase (a div b) mod c = 0 seems
  2059   to cause particular problems.*)
  2060 
  2061 text\<open>first, four lemmas to bound the remainder for the cases b<0 and b>0\<close>
  2062 
  2063 lemma zmult2_lemma_aux1: "[| (0::int) < c;  b < r;  r \<le> 0 |] ==> b * c < b * (q mod c) + r"
  2064 apply (subgoal_tac "b * (c - q mod c) < r * 1")
  2065  apply (simp add: algebra_simps)
  2066 apply (rule order_le_less_trans)
  2067  apply (erule_tac [2] mult_strict_right_mono)
  2068  apply (rule mult_left_mono_neg)
  2069   using add1_zle_eq[of "q mod c"]apply(simp add: algebra_simps)
  2070  apply (simp)
  2071 apply (simp)
  2072 done
  2073 
  2074 lemma zmult2_lemma_aux2:
  2075      "[| (0::int) < c;   b < r;  r \<le> 0 |] ==> b * (q mod c) + r \<le> 0"
  2076 apply (subgoal_tac "b * (q mod c) \<le> 0")
  2077  apply arith
  2078 apply (simp add: mult_le_0_iff)
  2079 done
  2080 
  2081 lemma zmult2_lemma_aux3: "[| (0::int) < c;  0 \<le> r;  r < b |] ==> 0 \<le> b * (q mod c) + r"
  2082 apply (subgoal_tac "0 \<le> b * (q mod c) ")
  2083 apply arith
  2084 apply (simp add: zero_le_mult_iff)
  2085 done
  2086 
  2087 lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 \<le> r; r < b |] ==> b * (q mod c) + r < b * c"
  2088 apply (subgoal_tac "r * 1 < b * (c - q mod c) ")
  2089  apply (simp add: right_diff_distrib)
  2090 apply (rule order_less_le_trans)
  2091  apply (erule mult_strict_right_mono)
  2092  apply (rule_tac [2] mult_left_mono)
  2093   apply simp
  2094  using add1_zle_eq[of "q mod c"] apply (simp add: algebra_simps)
  2095 apply simp
  2096 done
  2097 
  2098 lemma zmult2_lemma: "[| divmod_int_rel a b (q, r); 0 < c |]
  2099       ==> divmod_int_rel a (b * c) (q div c, b*(q mod c) + r)"
  2100 by (auto simp add: mult.assoc divmod_int_rel_def linorder_neq_iff
  2101                    zero_less_mult_iff distrib_left [symmetric]
  2102                    zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: if_split_asm)
  2103 
  2104 lemma zdiv_zmult2_eq:
  2105   fixes a b c :: int
  2106   shows "0 \<le> c \<Longrightarrow> a div (b * c) = (a div b) div c"
  2107 apply (case_tac "b = 0", simp)
  2108 apply (force simp add: le_less divmod_int_rel [THEN zmult2_lemma, THEN div_int_unique])
  2109 done
  2110 
  2111 lemma zmod_zmult2_eq:
  2112   fixes a b c :: int
  2113   shows "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
  2114 apply (case_tac "b = 0", simp)
  2115 apply (force simp add: le_less divmod_int_rel [THEN zmult2_lemma, THEN mod_int_unique])
  2116 done
  2117 
  2118 lemma div_pos_geq:
  2119   fixes k l :: int
  2120   assumes "0 < l" and "l \<le> k"
  2121   shows "k div l = (k - l) div l + 1"
  2122 proof -
  2123   have "k = (k - l) + l" by simp
  2124   then obtain j where k: "k = j + l" ..
  2125   with assms show ?thesis by (simp add: div_add_self2)
  2126 qed
  2127 
  2128 lemma mod_pos_geq:
  2129   fixes k l :: int
  2130   assumes "0 < l" and "l \<le> k"
  2131   shows "k mod l = (k - l) mod l"
  2132 proof -
  2133   have "k = (k - l) + l" by simp
  2134   then obtain j where k: "k = j + l" ..
  2135   with assms show ?thesis by simp
  2136 qed
  2137 
  2138 
  2139 subsubsection \<open>Splitting Rules for div and mod\<close>
  2140 
  2141 text\<open>The proofs of the two lemmas below are essentially identical\<close>
  2142 
  2143 lemma split_pos_lemma:
  2144  "0<k ==>
  2145     P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"
  2146 apply (rule iffI, clarify)
  2147  apply (erule_tac P="P x y" for x y in rev_mp)
  2148  apply (subst mod_add_eq [symmetric])
  2149  apply (subst zdiv_zadd1_eq)
  2150  apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)
  2151 txt\<open>converse direction\<close>
  2152 apply (drule_tac x = "n div k" in spec)
  2153 apply (drule_tac x = "n mod k" in spec, simp)
  2154 done
  2155 
  2156 lemma split_neg_lemma:
  2157  "k<0 ==>
  2158     P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"
  2159 apply (rule iffI, clarify)
  2160  apply (erule_tac P="P x y" for x y in rev_mp)
  2161  apply (subst mod_add_eq [symmetric])
  2162  apply (subst zdiv_zadd1_eq)
  2163  apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)
  2164 txt\<open>converse direction\<close>
  2165 apply (drule_tac x = "n div k" in spec)
  2166 apply (drule_tac x = "n mod k" in spec, simp)
  2167 done
  2168 
  2169 lemma split_zdiv:
  2170  "P(n div k :: int) =
  2171   ((k = 0 --> P 0) &
  2172    (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i)) &
  2173    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i)))"
  2174 apply (case_tac "k=0", simp)
  2175 apply (simp only: linorder_neq_iff)
  2176 apply (erule disjE)
  2177  apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"]
  2178                       split_neg_lemma [of concl: "%x y. P x"])
  2179 done
  2180 
  2181 lemma split_zmod:
  2182  "P(n mod k :: int) =
  2183   ((k = 0 --> P n) &
  2184    (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P j)) &
  2185    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P j)))"
  2186 apply (case_tac "k=0", simp)
  2187 apply (simp only: linorder_neq_iff)
  2188 apply (erule disjE)
  2189  apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"]
  2190                       split_neg_lemma [of concl: "%x y. P y"])
  2191 done
  2192 
  2193 text \<open>Enable (lin)arith to deal with @{const divide} and @{const modulo}
  2194   when these are applied to some constant that is of the form
  2195   @{term "numeral k"}:\<close>
  2196 declare split_zdiv [of _ _ "numeral k", arith_split] for k
  2197 declare split_zmod [of _ _ "numeral k", arith_split] for k
  2198 
  2199 
  2200 subsubsection \<open>Computing \<open>div\<close> and \<open>mod\<close> with shifting\<close>
  2201 
  2202 lemma pos_divmod_int_rel_mult_2:
  2203   assumes "0 \<le> b"
  2204   assumes "divmod_int_rel a b (q, r)"
  2205   shows "divmod_int_rel (1 + 2*a) (2*b) (q, 1 + 2*r)"
  2206   using assms unfolding divmod_int_rel_def by auto
  2207 
  2208 lemma neg_divmod_int_rel_mult_2:
  2209   assumes "b \<le> 0"
  2210   assumes "divmod_int_rel (a + 1) b (q, r)"
  2211   shows "divmod_int_rel (1 + 2*a) (2*b) (q, 2*r - 1)"
  2212   using assms unfolding divmod_int_rel_def by auto
  2213 
  2214 text\<open>computing div by shifting\<close>
  2215 
  2216 lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a"
  2217   using pos_divmod_int_rel_mult_2 [OF _ divmod_int_rel]
  2218   by (rule div_int_unique)
  2219 
  2220 lemma neg_zdiv_mult_2:
  2221   assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"
  2222   using neg_divmod_int_rel_mult_2 [OF A divmod_int_rel]
  2223   by (rule div_int_unique)
  2224 
  2225 (* FIXME: add rules for negative numerals *)
  2226 lemma zdiv_numeral_Bit0 [simp]:
  2227   "numeral (Num.Bit0 v) div numeral (Num.Bit0 w) =
  2228     numeral v div (numeral w :: int)"
  2229   unfolding numeral.simps unfolding mult_2 [symmetric]
  2230   by (rule div_mult_mult1, simp)
  2231 
  2232 lemma zdiv_numeral_Bit1 [simp]:
  2233   "numeral (Num.Bit1 v) div numeral (Num.Bit0 w) =
  2234     (numeral v div (numeral w :: int))"
  2235   unfolding numeral.simps
  2236   unfolding mult_2 [symmetric] add.commute [of _ 1]
  2237   by (rule pos_zdiv_mult_2, simp)
  2238 
  2239 lemma pos_zmod_mult_2:
  2240   fixes a b :: int
  2241   assumes "0 \<le> a"
  2242   shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)"
  2243   using pos_divmod_int_rel_mult_2 [OF assms divmod_int_rel]
  2244   by (rule mod_int_unique)
  2245 
  2246 lemma neg_zmod_mult_2:
  2247   fixes a b :: int
  2248   assumes "a \<le> 0"
  2249   shows "(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1"
  2250   using neg_divmod_int_rel_mult_2 [OF assms divmod_int_rel]
  2251   by (rule mod_int_unique)
  2252 
  2253 (* FIXME: add rules for negative numerals *)
  2254 lemma zmod_numeral_Bit0 [simp]:
  2255   "numeral (Num.Bit0 v) mod numeral (Num.Bit0 w) =
  2256     (2::int) * (numeral v mod numeral w)"
  2257   unfolding numeral_Bit0 [of v] numeral_Bit0 [of w]
  2258   unfolding mult_2 [symmetric] by (rule mod_mult_mult1)
  2259 
  2260 lemma zmod_numeral_Bit1 [simp]:
  2261   "numeral (Num.Bit1 v) mod numeral (Num.Bit0 w) =
  2262     2 * (numeral v mod numeral w) + (1::int)"
  2263   unfolding numeral_Bit1 [of v] numeral_Bit0 [of w]
  2264   unfolding mult_2 [symmetric] add.commute [of _ 1]
  2265   by (rule pos_zmod_mult_2, simp)
  2266 
  2267 lemma zdiv_eq_0_iff:
  2268  "(i::int) div k = 0 \<longleftrightarrow> k=0 \<or> 0\<le>i \<and> i<k \<or> i\<le>0 \<and> k<i" (is "?L = ?R")
  2269 proof
  2270   assume ?L
  2271   have "?L \<longrightarrow> ?R" by (rule split_zdiv[THEN iffD2]) simp
  2272   with \<open>?L\<close> show ?R by blast
  2273 next
  2274   assume ?R thus ?L
  2275     by(auto simp: div_pos_pos_trivial div_neg_neg_trivial)
  2276 qed
  2277 
  2278 lemma zmod_trival_iff:
  2279   fixes i k :: int
  2280   shows "i mod k = i \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i"
  2281 proof -
  2282   have "i mod k = i \<longleftrightarrow> i div k = 0"
  2283     by safe (insert div_mult_mod_eq [of i k], auto)
  2284   with zdiv_eq_0_iff
  2285   show ?thesis
  2286     by simp
  2287 qed
  2288 
  2289 subsubsection \<open>Quotients of Signs\<close>
  2290 
  2291 lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"
  2292 by (simp add: divide_int_def)
  2293 
  2294 lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
  2295 by (simp add: modulo_int_def)
  2296 
  2297 lemma div_neg_pos_less0: "[| a < (0::int);  0 < b |] ==> a div b < 0"
  2298 apply (subgoal_tac "a div b \<le> -1", force)
  2299 apply (rule order_trans)
  2300 apply (rule_tac a' = "-1" in zdiv_mono1)
  2301 apply (auto simp add: div_eq_minus1)
  2302 done
  2303 
  2304 lemma div_nonneg_neg_le0: "[| (0::int) \<le> a; b < 0 |] ==> a div b \<le> 0"
  2305 by (drule zdiv_mono1_neg, auto)
  2306 
  2307 lemma div_nonpos_pos_le0: "[| (a::int) \<le> 0; b > 0 |] ==> a div b \<le> 0"
  2308 by (drule zdiv_mono1, auto)
  2309 
  2310 text\<open>Now for some equivalences of the form \<open>a div b >=< 0 \<longleftrightarrow> \<dots>\<close>
  2311 conditional upon the sign of \<open>a\<close> or \<open>b\<close>. There are many more.
  2312 They should all be simp rules unless that causes too much search.\<close>
  2313 
  2314 lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)"
  2315 apply auto
  2316 apply (drule_tac [2] zdiv_mono1)
  2317 apply (auto simp add: linorder_neq_iff)
  2318 apply (simp (no_asm_use) add: linorder_not_less [symmetric])
  2319 apply (blast intro: div_neg_pos_less0)
  2320 done
  2321 
  2322 lemma pos_imp_zdiv_pos_iff:
  2323   "0<k \<Longrightarrow> 0 < (i::int) div k \<longleftrightarrow> k \<le> i"
  2324 using pos_imp_zdiv_nonneg_iff[of k i] zdiv_eq_0_iff[of i k]
  2325 by arith
  2326 
  2327 lemma neg_imp_zdiv_nonneg_iff:
  2328   "b < (0::int) ==> (0 \<le> a div b) = (a \<le> (0::int))"
  2329 apply (subst div_minus_minus [symmetric])
  2330 apply (subst pos_imp_zdiv_nonneg_iff, auto)
  2331 done
  2332 
  2333 (*But not (a div b \<le> 0 iff a\<le>0); consider a=1, b=2 when a div b = 0.*)
  2334 lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)"
  2335 by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff)
  2336 
  2337 (*Again the law fails for \<le>: consider a = -1, b = -2 when a div b = 0*)
  2338 lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)"
  2339 by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)
  2340 
  2341 lemma nonneg1_imp_zdiv_pos_iff:
  2342   "(0::int) <= a \<Longrightarrow> (a div b > 0) = (a >= b & b>0)"
  2343 apply rule
  2344  apply rule
  2345   using div_pos_pos_trivial[of a b]apply arith
  2346  apply(cases "b=0")apply simp
  2347  using div_nonneg_neg_le0[of a b]apply arith
  2348 using int_one_le_iff_zero_less[of "a div b"] zdiv_mono1[of b a b]apply simp
  2349 done
  2350 
  2351 lemma zmod_le_nonneg_dividend: "(m::int) \<ge> 0 ==> m mod k \<le> m"
  2352 apply (rule split_zmod[THEN iffD2])
  2353 apply(fastforce dest: q_pos_lemma intro: split_mult_pos_le)
  2354 done
  2355 
  2356 
  2357 subsubsection \<open>Computation of Division and Remainder\<close>
  2358 
  2359 instantiation int :: semiring_numeral_div
  2360 begin
  2361 
  2362 definition divmod_int :: "num \<Rightarrow> num \<Rightarrow> int \<times> int"
  2363 where
  2364   "divmod_int m n = (numeral m div numeral n, numeral m mod numeral n)"
  2365 
  2366 definition divmod_step_int :: "num \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int"
  2367 where
  2368   "divmod_step_int l qr = (let (q, r) = qr
  2369     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
  2370     else (2 * q, r))"
  2371 
  2372 instance
  2373   by standard (auto intro: zmod_le_nonneg_dividend simp add: divmod_int_def divmod_step_int_def
  2374     pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial zmod_zmult2_eq zdiv_zmult2_eq)
  2375 
  2376 end
  2377 
  2378 declare divmod_algorithm_code [where ?'a = int, code]
  2379 
  2380 context
  2381 begin
  2382   
  2383 qualified definition adjust_div :: "int \<times> int \<Rightarrow> int"
  2384 where
  2385   "adjust_div qr = (let (q, r) = qr in q + of_bool (r \<noteq> 0))"
  2386 
  2387 qualified lemma adjust_div_eq [simp, code]:
  2388   "adjust_div (q, r) = q + of_bool (r \<noteq> 0)"
  2389   by (simp add: adjust_div_def)
  2390 
  2391 qualified definition adjust_mod :: "int \<Rightarrow> int \<Rightarrow> int"
  2392 where
  2393   [simp]: "adjust_mod l r = (if r = 0 then 0 else l - r)"
  2394 
  2395 lemma minus_numeral_div_numeral [simp]:
  2396   "- numeral m div numeral n = - (adjust_div (divmod m n) :: int)"
  2397 proof -
  2398   have "int (fst (divmod m n)) = fst (divmod m n)"
  2399     by (simp only: fst_divmod divide_int_def) auto
  2400   then show ?thesis
  2401     by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
  2402 qed
  2403 
  2404 lemma minus_numeral_mod_numeral [simp]:
  2405   "- numeral m mod numeral n = adjust_mod (numeral n) (snd (divmod m n) :: int)"
  2406 proof -
  2407   have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
  2408     using that by (simp only: snd_divmod modulo_int_def) auto
  2409   then show ?thesis
  2410     by (auto simp add: split_def Let_def adjust_div_def divides_aux_def modulo_int_def)
  2411 qed
  2412 
  2413 lemma numeral_div_minus_numeral [simp]:
  2414   "numeral m div - numeral n = - (adjust_div (divmod m n) :: int)"
  2415 proof -
  2416   have "int (fst (divmod m n)) = fst (divmod m n)"
  2417     by (simp only: fst_divmod divide_int_def) auto
  2418   then show ?thesis
  2419     by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
  2420 qed
  2421   
  2422 lemma numeral_mod_minus_numeral [simp]:
  2423   "numeral m mod - numeral n = - adjust_mod (numeral n) (snd (divmod m n) :: int)"
  2424 proof -
  2425   have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
  2426     using that by (simp only: snd_divmod modulo_int_def) auto
  2427   then show ?thesis
  2428     by (auto simp add: split_def Let_def adjust_div_def divides_aux_def modulo_int_def)
  2429 qed
  2430 
  2431 lemma minus_one_div_numeral [simp]:
  2432   "- 1 div numeral n = - (adjust_div (divmod Num.One n) :: int)"
  2433   using minus_numeral_div_numeral [of Num.One n] by simp  
  2434 
  2435 lemma minus_one_mod_numeral [simp]:
  2436   "- 1 mod numeral n = adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
  2437   using minus_numeral_mod_numeral [of Num.One n] by simp
  2438 
  2439 lemma one_div_minus_numeral [simp]:
  2440   "1 div - numeral n = - (adjust_div (divmod Num.One n) :: int)"
  2441   using numeral_div_minus_numeral [of Num.One n] by simp
  2442   
  2443 lemma one_mod_minus_numeral [simp]:
  2444   "1 mod - numeral n = - adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
  2445   using numeral_mod_minus_numeral [of Num.One n] by simp
  2446 
  2447 end
  2448 
  2449 
  2450 subsubsection \<open>Further properties\<close>
  2451 
  2452 text \<open>Simplify expresions in which div and mod combine numerical constants\<close>
  2453 
  2454 lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
  2455   by (rule div_int_unique [of a b q r]) (simp add: divmod_int_rel_def)
  2456 
  2457 lemma int_div_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a div b = q"
  2458   by (rule div_int_unique [of a b q r],
  2459     simp add: divmod_int_rel_def)
  2460 
  2461 lemma int_mod_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a mod b = r"
  2462   by (rule mod_int_unique [of a b q r],
  2463     simp add: divmod_int_rel_def)
  2464 
  2465 lemma int_mod_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a mod b = r"
  2466   by (rule mod_int_unique [of a b q r],
  2467     simp add: divmod_int_rel_def)
  2468 
  2469 lemma abs_div: "(y::int) dvd x \<Longrightarrow> \<bar>x div y\<bar> = \<bar>x\<bar> div \<bar>y\<bar>"
  2470 by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
  2471 
  2472 text\<open>Suggested by Matthias Daum\<close>
  2473 lemma int_power_div_base:
  2474      "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"
  2475 apply (subgoal_tac "k ^ m = k ^ ((m - Suc 0) + Suc 0)")
  2476  apply (erule ssubst)
  2477  apply (simp only: power_add)
  2478  apply simp_all
  2479 done
  2480 
  2481 text \<open>Distributive laws for function \<open>nat\<close>.\<close>
  2482 
  2483 lemma nat_div_distrib: "0 \<le> x \<Longrightarrow> nat (x div y) = nat x div nat y"
  2484 apply (rule linorder_cases [of y 0])
  2485 apply (simp add: div_nonneg_neg_le0)
  2486 apply simp
  2487 apply (simp add: nat_eq_iff pos_imp_zdiv_nonneg_iff zdiv_int)
  2488 done
  2489 
  2490 (*Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't*)
  2491 lemma nat_mod_distrib:
  2492   "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x mod y) = nat x mod nat y"
  2493 apply (case_tac "y = 0", simp)
  2494 apply (simp add: nat_eq_iff zmod_int)
  2495 done
  2496 
  2497 text  \<open>transfer setup\<close>
  2498 
  2499 lemma transfer_nat_int_functions:
  2500     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
  2501     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
  2502   by (auto simp add: nat_div_distrib nat_mod_distrib)
  2503 
  2504 lemma transfer_nat_int_function_closures:
  2505     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
  2506     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
  2507   apply (cases "y = 0")
  2508   apply (auto simp add: pos_imp_zdiv_nonneg_iff)
  2509   apply (cases "y = 0")
  2510   apply auto
  2511 done
  2512 
  2513 declare transfer_morphism_nat_int [transfer add return:
  2514   transfer_nat_int_functions
  2515   transfer_nat_int_function_closures
  2516 ]
  2517 
  2518 lemma transfer_int_nat_functions:
  2519     "(int x) div (int y) = int (x div y)"
  2520     "(int x) mod (int y) = int (x mod y)"
  2521   by (auto simp add: zdiv_int zmod_int)
  2522 
  2523 lemma transfer_int_nat_function_closures:
  2524     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
  2525     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
  2526   by (simp_all only: is_nat_def transfer_nat_int_function_closures)
  2527 
  2528 declare transfer_morphism_int_nat [transfer add return:
  2529   transfer_int_nat_functions
  2530   transfer_int_nat_function_closures
  2531 ]
  2532 
  2533 text\<open>Suggested by Matthias Daum\<close>
  2534 lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
  2535 apply (subgoal_tac "nat x div nat k < nat x")
  2536  apply (simp add: nat_div_distrib [symmetric])
  2537 apply (rule Divides.div_less_dividend, simp_all)
  2538 done
  2539 
  2540 lemma (in ring_div) mod_eq_dvd_iff:
  2541   "a mod c = b mod c \<longleftrightarrow> c dvd a - b" (is "?P \<longleftrightarrow> ?Q")
  2542 proof
  2543   assume ?P
  2544   then have "(a mod c - b mod c) mod c = 0"
  2545     by simp
  2546   then show ?Q
  2547     by (simp add: dvd_eq_mod_eq_0 mod_simps)
  2548 next
  2549   assume ?Q
  2550   then obtain d where d: "a - b = c * d" ..
  2551   then have "a = c * d + b"
  2552     by (simp add: algebra_simps)
  2553   then show ?P by simp
  2554 qed
  2555 
  2556 lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \<le> x"
  2557   shows "\<exists>q. x = y + n * q"
  2558 proof-
  2559   from xy have th: "int x - int y = int (x - y)" by simp
  2560   from xyn have "int x mod int n = int y mod int n"
  2561     by (simp add: zmod_int [symmetric])
  2562   hence "int n dvd int x - int y" by (simp only: mod_eq_dvd_iff [symmetric])
  2563   hence "n dvd x - y" by (simp add: th zdvd_int)
  2564   then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith
  2565 qed
  2566 
  2567 lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)"
  2568   (is "?lhs = ?rhs")
  2569 proof
  2570   assume H: "x mod n = y mod n"
  2571   {assume xy: "x \<le> y"
  2572     from H have th: "y mod n = x mod n" by simp
  2573     from nat_mod_eq_lemma[OF th xy] have ?rhs
  2574       apply clarify  apply (rule_tac x="q" in exI) by (rule exI[where x="0"], simp)}
  2575   moreover
  2576   {assume xy: "y \<le> x"
  2577     from nat_mod_eq_lemma[OF H xy] have ?rhs
  2578       apply clarify  apply (rule_tac x="0" in exI) by (rule_tac x="q" in exI, simp)}
  2579   ultimately  show ?rhs using linear[of x y] by blast
  2580 next
  2581   assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast
  2582   hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp
  2583   thus  ?lhs by simp
  2584 qed
  2585 
  2586 subsubsection \<open>Dedicated simproc for calculation\<close>
  2587 
  2588 text \<open>
  2589   There is space for improvement here: the calculation itself
  2590   could be carried outside the logic, and a generic simproc
  2591   (simplifier setup) for generic calculation would be helpful. 
  2592 \<close>
  2593 
  2594 simproc_setup numeral_divmod
  2595   ("0 div 0 :: 'a :: semiring_numeral_div" | "0 mod 0 :: 'a :: semiring_numeral_div" |
  2596    "0 div 1 :: 'a :: semiring_numeral_div" | "0 mod 1 :: 'a :: semiring_numeral_div" |
  2597    "0 div - 1 :: int" | "0 mod - 1 :: int" |
  2598    "0 div numeral b :: 'a :: semiring_numeral_div" | "0 mod numeral b :: 'a :: semiring_numeral_div" |
  2599    "0 div - numeral b :: int" | "0 mod - numeral b :: int" |
  2600    "1 div 0 :: 'a :: semiring_numeral_div" | "1 mod 0 :: 'a :: semiring_numeral_div" |
  2601    "1 div 1 :: 'a :: semiring_numeral_div" | "1 mod 1 :: 'a :: semiring_numeral_div" |
  2602    "1 div - 1 :: int" | "1 mod - 1 :: int" |
  2603    "1 div numeral b :: 'a :: semiring_numeral_div" | "1 mod numeral b :: 'a :: semiring_numeral_div" |
  2604    "1 div - numeral b :: int" |"1 mod - numeral b :: int" |
  2605    "- 1 div 0 :: int" | "- 1 mod 0 :: int" | "- 1 div 1 :: int" | "- 1 mod 1 :: int" |
  2606    "- 1 div - 1 :: int" | "- 1 mod - 1 :: int" | "- 1 div numeral b :: int" | "- 1 mod numeral b :: int" |
  2607    "- 1 div - numeral b :: int" | "- 1 mod - numeral b :: int" |
  2608    "numeral a div 0 :: 'a :: semiring_numeral_div" | "numeral a mod 0 :: 'a :: semiring_numeral_div" |
  2609    "numeral a div 1 :: 'a :: semiring_numeral_div" | "numeral a mod 1 :: 'a :: semiring_numeral_div" |
  2610    "numeral a div - 1 :: int" | "numeral a mod - 1 :: int" |
  2611    "numeral a div numeral b :: 'a :: semiring_numeral_div" | "numeral a mod numeral b :: 'a :: semiring_numeral_div" |
  2612    "numeral a div - numeral b :: int" | "numeral a mod - numeral b :: int" |
  2613    "- numeral a div 0 :: int" | "- numeral a mod 0 :: int" |
  2614    "- numeral a div 1 :: int" | "- numeral a mod 1 :: int" |
  2615    "- numeral a div - 1 :: int" | "- numeral a mod - 1 :: int" |
  2616    "- numeral a div numeral b :: int" | "- numeral a mod numeral b :: int" |
  2617    "- numeral a div - numeral b :: int" | "- numeral a mod - numeral b :: int") =
  2618 \<open> let
  2619     val if_cong = the (Code.get_case_cong @{theory} @{const_name If});
  2620     fun successful_rewrite ctxt ct =
  2621       let
  2622         val thm = Simplifier.rewrite ctxt ct
  2623       in if Thm.is_reflexive thm then NONE else SOME thm end;
  2624   in fn phi =>
  2625     let
  2626       val simps = Morphism.fact phi (@{thms div_0 mod_0 div_by_0 mod_by_0 div_by_1 mod_by_1
  2627         one_div_numeral one_mod_numeral minus_one_div_numeral minus_one_mod_numeral
  2628         one_div_minus_numeral one_mod_minus_numeral
  2629         numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral
  2630         numeral_div_minus_numeral numeral_mod_minus_numeral
  2631         div_minus_minus mod_minus_minus Divides.adjust_div_eq of_bool_eq one_neq_zero
  2632         numeral_neq_zero neg_equal_0_iff_equal arith_simps arith_special divmod_trivial
  2633         divmod_cancel divmod_steps divmod_step_eq fst_conv snd_conv numeral_One
  2634         case_prod_beta rel_simps Divides.adjust_mod_def div_minus1_right mod_minus1_right
  2635         minus_minus numeral_times_numeral mult_zero_right mult_1_right}
  2636         @ [@{lemma "0 = 0 \<longleftrightarrow> True" by simp}]);
  2637       fun prepare_simpset ctxt = HOL_ss |> Simplifier.simpset_map ctxt
  2638         (Simplifier.add_cong if_cong #> fold Simplifier.add_simp simps)
  2639     in fn ctxt => successful_rewrite (Simplifier.put_simpset (prepare_simpset ctxt) ctxt) end
  2640   end;
  2641 \<close>
  2642 
  2643 
  2644 subsubsection \<open>Code generation\<close>
  2645 
  2646 lemma [code]:
  2647   fixes k :: int
  2648   shows 
  2649     "k div 0 = 0"
  2650     "k mod 0 = k"
  2651     "0 div k = 0"
  2652     "0 mod k = 0"
  2653     "k div Int.Pos Num.One = k"
  2654     "k mod Int.Pos Num.One = 0"
  2655     "k div Int.Neg Num.One = - k"
  2656     "k mod Int.Neg Num.One = 0"
  2657     "Int.Pos m div Int.Pos n = (fst (divmod m n) :: int)"
  2658     "Int.Pos m mod Int.Pos n = (snd (divmod m n) :: int)"
  2659     "Int.Neg m div Int.Pos n = - (Divides.adjust_div (divmod m n) :: int)"
  2660     "Int.Neg m mod Int.Pos n = Divides.adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
  2661     "Int.Pos m div Int.Neg n = - (Divides.adjust_div (divmod m n) :: int)"
  2662     "Int.Pos m mod Int.Neg n = - Divides.adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
  2663     "Int.Neg m div Int.Neg n = (fst (divmod m n) :: int)"
  2664     "Int.Neg m mod Int.Neg n = - (snd (divmod m n) :: int)"
  2665   by simp_all
  2666 
  2667 code_identifier
  2668   code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  2669 
  2670 lemma dvd_eq_mod_eq_0_numeral:
  2671   "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semiring_div)"
  2672   by (fact dvd_eq_mod_eq_0)
  2673 
  2674 declare minus_div_mult_eq_mod [symmetric, nitpick_unfold]
  2675 
  2676 end