src/HOL/Divides.thy
author haftmann
Sat Dec 17 15:22:14 2016 +0100 (2016-12-17)
changeset 64593 50c715579715
parent 64592 7759f1766189
child 64630 96015aecfeba
permissions -rw-r--r--
reoriented congruence rules in non-explosive direction
     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 end
   786 
   787 
   788 subsection \<open>Division on @{typ nat}\<close>
   789 
   790 context
   791 begin
   792 
   793 text \<open>
   794   We define @{const divide} and @{const modulo} on @{typ nat} by means
   795   of a characteristic relation with two input arguments
   796   @{term "m::nat"}, @{term "n::nat"} and two output arguments
   797   @{term "q::nat"}(uotient) and @{term "r::nat"}(emainder).
   798 \<close>
   799 
   800 definition divmod_nat_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool" where
   801   "divmod_nat_rel m n qr \<longleftrightarrow>
   802     m = fst qr * n + snd qr \<and>
   803       (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)"
   804 
   805 text \<open>@{const divmod_nat_rel} is total:\<close>
   806 
   807 qualified lemma divmod_nat_rel_ex:
   808   obtains q r where "divmod_nat_rel m n (q, r)"
   809 proof (cases "n = 0")
   810   case True  with that show thesis
   811     by (auto simp add: divmod_nat_rel_def)
   812 next
   813   case False
   814   have "\<exists>q r. m = q * n + r \<and> r < n"
   815   proof (induct m)
   816     case 0 with \<open>n \<noteq> 0\<close>
   817     have "(0::nat) = 0 * n + 0 \<and> 0 < n" by simp
   818     then show ?case by blast
   819   next
   820     case (Suc m) then obtain q' r'
   821       where m: "m = q' * n + r'" and n: "r' < n" by auto
   822     then show ?case proof (cases "Suc r' < n")
   823       case True
   824       from m n have "Suc m = q' * n + Suc r'" by simp
   825       with True show ?thesis by blast
   826     next
   827       case False then have "n \<le> Suc r'"
   828         by (simp add: not_less)
   829       moreover from n have "Suc r' \<le> n"
   830         by (simp add: Suc_le_eq)
   831       ultimately have "n = Suc r'" by auto
   832       with m have "Suc m = Suc q' * n + 0" by simp
   833       with \<open>n \<noteq> 0\<close> show ?thesis by blast
   834     qed
   835   qed
   836   with that show thesis
   837     using \<open>n \<noteq> 0\<close> by (auto simp add: divmod_nat_rel_def)
   838 qed
   839 
   840 text \<open>@{const divmod_nat_rel} is injective:\<close>
   841 
   842 qualified lemma divmod_nat_rel_unique:
   843   assumes "divmod_nat_rel m n qr"
   844     and "divmod_nat_rel m n qr'"
   845   shows "qr = qr'"
   846 proof (cases "n = 0")
   847   case True with assms show ?thesis
   848     by (cases qr, cases qr')
   849       (simp add: divmod_nat_rel_def)
   850 next
   851   case False
   852   have aux: "\<And>q r q' r'. q' * n + r' = q * n + r \<Longrightarrow> r < n \<Longrightarrow> q' \<le> (q::nat)"
   853   apply (rule leI)
   854   apply (subst less_iff_Suc_add)
   855   apply (auto simp add: add_mult_distrib)
   856   done
   857   from \<open>n \<noteq> 0\<close> assms have *: "fst qr = fst qr'"
   858     by (auto simp add: divmod_nat_rel_def intro: order_antisym dest: aux sym split: if_splits)
   859   with assms have "snd qr = snd qr'"
   860     by (simp add: divmod_nat_rel_def)
   861   with * show ?thesis by (cases qr, cases qr') simp
   862 qed
   863 
   864 text \<open>
   865   We instantiate divisibility on the natural numbers by
   866   means of @{const divmod_nat_rel}:
   867 \<close>
   868 
   869 qualified definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
   870   "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)"
   871 
   872 qualified lemma divmod_nat_rel_divmod_nat:
   873   "divmod_nat_rel m n (divmod_nat m n)"
   874 proof -
   875   from divmod_nat_rel_ex
   876     obtain qr where rel: "divmod_nat_rel m n qr" .
   877   then show ?thesis
   878   by (auto simp add: divmod_nat_def intro: theI elim: divmod_nat_rel_unique)
   879 qed
   880 
   881 qualified lemma divmod_nat_unique:
   882   assumes "divmod_nat_rel m n qr"
   883   shows "divmod_nat m n = qr"
   884   using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
   885 
   886 qualified lemma divmod_nat_zero: "divmod_nat m 0 = (0, m)"
   887   by (simp add: divmod_nat_unique divmod_nat_rel_def)
   888 
   889 qualified lemma divmod_nat_zero_left: "divmod_nat 0 n = (0, 0)"
   890   by (simp add: divmod_nat_unique divmod_nat_rel_def)
   891 
   892 qualified lemma divmod_nat_base: "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
   893   by (simp add: divmod_nat_unique divmod_nat_rel_def)
   894 
   895 qualified lemma divmod_nat_step:
   896   assumes "0 < n" and "n \<le> m"
   897   shows "divmod_nat m n = apfst Suc (divmod_nat (m - n) n)"
   898 proof (rule divmod_nat_unique)
   899   have "divmod_nat_rel (m - n) n (divmod_nat (m - n) n)"
   900     by (fact divmod_nat_rel_divmod_nat)
   901   then show "divmod_nat_rel m n (apfst Suc (divmod_nat (m - n) n))"
   902     unfolding divmod_nat_rel_def using assms
   903       by (auto split: if_splits simp add: algebra_simps)
   904 qed
   905 
   906 end
   907 
   908 instantiation nat :: "{semidom_modulo, normalization_semidom}"
   909 begin
   910 
   911 definition normalize_nat :: "nat \<Rightarrow> nat"
   912   where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
   913 
   914 definition unit_factor_nat :: "nat \<Rightarrow> nat"
   915   where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
   916 
   917 lemma unit_factor_simps [simp]:
   918   "unit_factor 0 = (0::nat)"
   919   "unit_factor (Suc n) = 1"
   920   by (simp_all add: unit_factor_nat_def)
   921 
   922 definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   923   where div_nat_def: "m div n = fst (Divides.divmod_nat m n)"
   924 
   925 definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   926   where mod_nat_def: "m mod n = snd (Divides.divmod_nat m n)"
   927 
   928 lemma fst_divmod_nat [simp]:
   929   "fst (Divides.divmod_nat m n) = m div n"
   930   by (simp add: div_nat_def)
   931 
   932 lemma snd_divmod_nat [simp]:
   933   "snd (Divides.divmod_nat m n) = m mod n"
   934   by (simp add: mod_nat_def)
   935 
   936 lemma divmod_nat_div_mod:
   937   "Divides.divmod_nat m n = (m div n, m mod n)"
   938   by (simp add: prod_eq_iff)
   939 
   940 lemma div_nat_unique:
   941   assumes "divmod_nat_rel m n (q, r)"
   942   shows "m div n = q"
   943   using assms
   944   by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
   945 
   946 lemma mod_nat_unique:
   947   assumes "divmod_nat_rel m n (q, r)"
   948   shows "m mod n = r"
   949   using assms
   950   by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
   951 
   952 lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)"
   953   using Divides.divmod_nat_rel_divmod_nat
   954   by (simp add: divmod_nat_div_mod)
   955 
   956 text \<open>The ''recursion'' equations for @{const divide} and @{const modulo}\<close>
   957 
   958 lemma div_less [simp]:
   959   fixes m n :: nat
   960   assumes "m < n"
   961   shows "m div n = 0"
   962   using assms Divides.divmod_nat_base by (simp add: prod_eq_iff)
   963 
   964 lemma le_div_geq:
   965   fixes m n :: nat
   966   assumes "0 < n" and "n \<le> m"
   967   shows "m div n = Suc ((m - n) div n)"
   968   using assms Divides.divmod_nat_step by (simp add: prod_eq_iff)
   969 
   970 lemma mod_less [simp]:
   971   fixes m n :: nat
   972   assumes "m < n"
   973   shows "m mod n = m"
   974   using assms Divides.divmod_nat_base by (simp add: prod_eq_iff)
   975 
   976 lemma le_mod_geq:
   977   fixes m n :: nat
   978   assumes "n \<le> m"
   979   shows "m mod n = (m - n) mod n"
   980   using assms Divides.divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)
   981 
   982 lemma mod_less_divisor [simp]:
   983   fixes m n :: nat
   984   assumes "n > 0"
   985   shows "m mod n < n"
   986   using assms divmod_nat_rel [of m n] unfolding divmod_nat_rel_def
   987   by (auto split: if_splits)
   988 
   989 lemma mod_le_divisor [simp]:
   990   fixes m n :: nat
   991   assumes "n > 0"
   992   shows "m mod n \<le> n"
   993 proof (rule less_imp_le)
   994   from assms show "m mod n < n"
   995     by simp
   996 qed
   997 
   998 instance proof
   999   fix m n :: nat
  1000   show "m div n * n + m mod n = m"
  1001     using divmod_nat_rel [of m n] by (simp add: divmod_nat_rel_def)
  1002 next
  1003   fix n :: nat show "n div 0 = 0"
  1004     by (simp add: div_nat_def Divides.divmod_nat_zero)
  1005 next
  1006   fix m n :: nat
  1007   assume "n \<noteq> 0"
  1008   then show "m * n div n = m"
  1009     by (auto simp add: divmod_nat_rel_def intro: div_nat_unique [of _ _ _ 0])
  1010 qed (simp_all add: unit_factor_nat_def)
  1011 
  1012 end
  1013 
  1014 instance nat :: semiring_div
  1015 proof
  1016   fix m n q :: nat
  1017   assume "n \<noteq> 0"
  1018   then show "(q + m * n) div n = m + q div n"
  1019     by (induct m) (simp_all add: le_div_geq)
  1020 next
  1021   fix m n q :: nat
  1022   assume "m \<noteq> 0"
  1023   then have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))"
  1024     using div_mult_mod_eq [of n q]
  1025     by (auto simp add: divmod_nat_rel_def algebra_simps distrib_left [symmetric] simp del: distrib_left)
  1026   then show "(m * n) div (m * q) = n div q"
  1027     by (rule div_nat_unique)
  1028 qed
  1029 
  1030 lemma div_by_Suc_0 [simp]:
  1031   "m div Suc 0 = m"
  1032   using div_by_1 [of m] by simp
  1033 
  1034 lemma mod_by_Suc_0 [simp]:
  1035   "m mod Suc 0 = 0"
  1036   using mod_by_1 [of m] by simp
  1037 
  1038 lemma mod_greater_zero_iff_not_dvd:
  1039   fixes m n :: nat
  1040   shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
  1041   by (simp add: dvd_eq_mod_eq_0)
  1042 
  1043 text \<open>Simproc for cancelling @{const divide} and @{const modulo}\<close>
  1044 
  1045 lemma (in semiring_modulo) cancel_div_mod_rules:
  1046   "((a div b) * b + a mod b) + c = a + c"
  1047   "(b * (a div b) + a mod b) + c = a + c"
  1048   by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
  1049 
  1050 ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
  1051 
  1052 ML \<open>
  1053 structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
  1054 (
  1055   val div_name = @{const_name divide};
  1056   val mod_name = @{const_name modulo};
  1057   val mk_binop = HOLogic.mk_binop;
  1058   val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
  1059   val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
  1060   fun mk_sum [] = HOLogic.zero
  1061     | mk_sum [t] = t
  1062     | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
  1063   fun dest_sum tm =
  1064     if HOLogic.is_zero tm then []
  1065     else
  1066       (case try HOLogic.dest_Suc tm of
  1067         SOME t => HOLogic.Suc_zero :: dest_sum t
  1068       | NONE =>
  1069           (case try dest_plus tm of
  1070             SOME (t, u) => dest_sum t @ dest_sum u
  1071           | NONE => [tm]));
  1072 
  1073   val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
  1074 
  1075   val prove_eq_sums = Arith_Data.prove_conv2 all_tac
  1076     (Arith_Data.simp_all_tac @{thms add_0_left add_0_right ac_simps})
  1077 )
  1078 \<close>
  1079 
  1080 simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
  1081   \<open>K Cancel_Div_Mod_Nat.proc\<close>
  1082 
  1083 lemma divmod_nat_if [code]:
  1084   "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
  1085     let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
  1086   by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
  1087 
  1088 lemma mod_Suc_eq [mod_simps]:
  1089   "Suc (m mod n) mod n = Suc m mod n"
  1090 proof -
  1091   have "(m mod n + 1) mod n = (m + 1) mod n"
  1092     by (simp only: mod_simps)
  1093   then show ?thesis
  1094     by simp
  1095 qed
  1096 
  1097 lemma mod_Suc_Suc_eq [mod_simps]:
  1098   "Suc (Suc (m mod n)) mod n = Suc (Suc m) mod n"
  1099 proof -
  1100   have "(m mod n + 2) mod n = (m + 2) mod n"
  1101     by (simp only: mod_simps)
  1102   then show ?thesis
  1103     by simp
  1104 qed
  1105 
  1106 
  1107 subsubsection \<open>Quotient\<close>
  1108 
  1109 lemma div_geq: "0 < n \<Longrightarrow>  \<not> m < n \<Longrightarrow> m div n = Suc ((m - n) div n)"
  1110 by (simp add: le_div_geq linorder_not_less)
  1111 
  1112 lemma div_if: "0 < n \<Longrightarrow> m div n = (if m < n then 0 else Suc ((m - n) div n))"
  1113 by (simp add: div_geq)
  1114 
  1115 lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
  1116 by simp
  1117 
  1118 lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
  1119 by simp
  1120 
  1121 lemma div_positive:
  1122   fixes m n :: nat
  1123   assumes "n > 0"
  1124   assumes "m \<ge> n"
  1125   shows "m div n > 0"
  1126 proof -
  1127   from \<open>m \<ge> n\<close> obtain q where "m = n + q"
  1128     by (auto simp add: le_iff_add)
  1129   with \<open>n > 0\<close> show ?thesis by (simp add: div_add_self1)
  1130 qed
  1131 
  1132 lemma div_eq_0_iff: "(a div b::nat) = 0 \<longleftrightarrow> a < b \<or> b = 0"
  1133   by auto (metis div_positive less_numeral_extra(3) not_less)
  1134 
  1135 
  1136 subsubsection \<open>Remainder\<close>
  1137 
  1138 lemma mod_Suc_le_divisor [simp]:
  1139   "m mod Suc n \<le> n"
  1140   using mod_less_divisor [of "Suc n" m] by arith
  1141 
  1142 lemma mod_less_eq_dividend [simp]:
  1143   fixes m n :: nat
  1144   shows "m mod n \<le> m"
  1145 proof (rule add_leD2)
  1146   from div_mult_mod_eq have "m div n * n + m mod n = m" .
  1147   then show "m div n * n + m mod n \<le> m" by auto
  1148 qed
  1149 
  1150 lemma mod_geq: "\<not> m < (n::nat) \<Longrightarrow> m mod n = (m - n) mod n"
  1151 by (simp add: le_mod_geq linorder_not_less)
  1152 
  1153 lemma mod_if: "m mod (n::nat) = (if m < n then m else (m - n) mod n)"
  1154 by (simp add: le_mod_geq)
  1155 
  1156 
  1157 subsubsection \<open>Quotient and Remainder\<close>
  1158 
  1159 lemma divmod_nat_rel_mult1_eq:
  1160   "divmod_nat_rel b c (q, r)
  1161    \<Longrightarrow> divmod_nat_rel (a * b) c (a * q + a * r div c, a * r mod c)"
  1162 by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps)
  1163 
  1164 lemma div_mult1_eq:
  1165   "(a * b) div c = a * (b div c) + a * (b mod c) div (c::nat)"
  1166 by (blast intro: divmod_nat_rel_mult1_eq [THEN div_nat_unique] divmod_nat_rel)
  1167 
  1168 lemma divmod_nat_rel_add1_eq:
  1169   "divmod_nat_rel a c (aq, ar) \<Longrightarrow> divmod_nat_rel b c (bq, br)
  1170    \<Longrightarrow> divmod_nat_rel (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)"
  1171 by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps)
  1172 
  1173 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
  1174 lemma div_add1_eq:
  1175   "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
  1176 by (blast intro: divmod_nat_rel_add1_eq [THEN div_nat_unique] divmod_nat_rel)
  1177 
  1178 lemma divmod_nat_rel_mult2_eq:
  1179   assumes "divmod_nat_rel a b (q, r)"
  1180   shows "divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"
  1181 proof -
  1182   { assume "r < b" and "0 < c"
  1183     then have "b * (q mod c) + r < b * c"
  1184       apply (cut_tac m = q and n = c in mod_less_divisor)
  1185       apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
  1186       apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
  1187       apply (simp add: add_mult_distrib2)
  1188       done
  1189     then have "r + b * (q mod c) < b * c"
  1190       by (simp add: ac_simps)
  1191   } with assms show ?thesis
  1192     by (auto simp add: divmod_nat_rel_def algebra_simps add_mult_distrib2 [symmetric])
  1193 qed
  1194 
  1195 lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"
  1196 by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_nat_unique])
  1197 
  1198 lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)"
  1199 by (auto simp add: mult.commute divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN mod_nat_unique])
  1200 
  1201 instantiation nat :: semiring_numeral_div
  1202 begin
  1203 
  1204 definition divmod_nat :: "num \<Rightarrow> num \<Rightarrow> nat \<times> nat"
  1205 where
  1206   divmod'_nat_def: "divmod_nat m n = (numeral m div numeral n, numeral m mod numeral n)"
  1207 
  1208 definition divmod_step_nat :: "num \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
  1209 where
  1210   "divmod_step_nat l qr = (let (q, r) = qr
  1211     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
  1212     else (2 * q, r))"
  1213 
  1214 instance
  1215   by standard (auto intro: div_positive simp add: divmod'_nat_def divmod_step_nat_def mod_mult2_eq div_mult2_eq)
  1216 
  1217 end
  1218 
  1219 declare divmod_algorithm_code [where ?'a = nat, code]
  1220   
  1221 
  1222 subsubsection \<open>Further Facts about Quotient and Remainder\<close>
  1223 
  1224 lemma div_le_mono:
  1225   fixes m n k :: nat
  1226   assumes "m \<le> n"
  1227   shows "m div k \<le> n div k"
  1228 proof -
  1229   from assms obtain q where "n = m + q"
  1230     by (auto simp add: le_iff_add)
  1231   then show ?thesis
  1232     by (simp add: div_add1_eq [of m q k])
  1233 qed
  1234 
  1235 (* Antimonotonicity of div in second argument *)
  1236 lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"
  1237 apply (subgoal_tac "0<n")
  1238  prefer 2 apply simp
  1239 apply (induct_tac k rule: nat_less_induct)
  1240 apply (rename_tac "k")
  1241 apply (case_tac "k<n", simp)
  1242 apply (subgoal_tac "~ (k<m) ")
  1243  prefer 2 apply simp
  1244 apply (simp add: div_geq)
  1245 apply (subgoal_tac "(k-n) div n \<le> (k-m) div n")
  1246  prefer 2
  1247  apply (blast intro: div_le_mono diff_le_mono2)
  1248 apply (rule le_trans, simp)
  1249 apply (simp)
  1250 done
  1251 
  1252 lemma div_le_dividend [simp]: "m div n \<le> (m::nat)"
  1253 apply (case_tac "n=0", simp)
  1254 apply (subgoal_tac "m div n \<le> m div 1", simp)
  1255 apply (rule div_le_mono2)
  1256 apply (simp_all (no_asm_simp))
  1257 done
  1258 
  1259 (* Similar for "less than" *)
  1260 lemma div_less_dividend [simp]:
  1261   "\<lbrakk>(1::nat) < n; 0 < m\<rbrakk> \<Longrightarrow> m div n < m"
  1262 apply (induct m rule: nat_less_induct)
  1263 apply (rename_tac "m")
  1264 apply (case_tac "m<n", simp)
  1265 apply (subgoal_tac "0<n")
  1266  prefer 2 apply simp
  1267 apply (simp add: div_geq)
  1268 apply (case_tac "n<m")
  1269  apply (subgoal_tac "(m-n) div n < (m-n) ")
  1270   apply (rule impI less_trans_Suc)+
  1271 apply assumption
  1272   apply (simp_all)
  1273 done
  1274 
  1275 text\<open>A fact for the mutilated chess board\<close>
  1276 lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"
  1277 apply (case_tac "n=0", simp)
  1278 apply (induct "m" rule: nat_less_induct)
  1279 apply (case_tac "Suc (na) <n")
  1280 (* case Suc(na) < n *)
  1281 apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
  1282 (* case n \<le> Suc(na) *)
  1283 apply (simp add: linorder_not_less le_Suc_eq mod_geq)
  1284 apply (auto simp add: Suc_diff_le le_mod_geq)
  1285 done
  1286 
  1287 lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
  1288 by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
  1289 
  1290 lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
  1291 
  1292 (*Loses information, namely we also have r<d provided d is nonzero*)
  1293 lemma mod_eqD:
  1294   fixes m d r q :: nat
  1295   assumes "m mod d = r"
  1296   shows "\<exists>q. m = r + q * d"
  1297 proof -
  1298   from div_mult_mod_eq obtain q where "q * d + m mod d = m" by blast
  1299   with assms have "m = r + q * d" by simp
  1300   then show ?thesis ..
  1301 qed
  1302 
  1303 lemma split_div:
  1304  "P(n div k :: nat) =
  1305  ((k = 0 \<longrightarrow> P 0) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P i)))"
  1306  (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
  1307 proof
  1308   assume P: ?P
  1309   show ?Q
  1310   proof (cases)
  1311     assume "k = 0"
  1312     with P show ?Q by simp
  1313   next
  1314     assume not0: "k \<noteq> 0"
  1315     thus ?Q
  1316     proof (simp, intro allI impI)
  1317       fix i j
  1318       assume n: "n = k*i + j" and j: "j < k"
  1319       show "P i"
  1320       proof (cases)
  1321         assume "i = 0"
  1322         with n j P show "P i" by simp
  1323       next
  1324         assume "i \<noteq> 0"
  1325         with not0 n j P show "P i" by(simp add:ac_simps)
  1326       qed
  1327     qed
  1328   qed
  1329 next
  1330   assume Q: ?Q
  1331   show ?P
  1332   proof (cases)
  1333     assume "k = 0"
  1334     with Q show ?P by simp
  1335   next
  1336     assume not0: "k \<noteq> 0"
  1337     with Q have R: ?R by simp
  1338     from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
  1339     show ?P by simp
  1340   qed
  1341 qed
  1342 
  1343 lemma split_div_lemma:
  1344   assumes "0 < n"
  1345   shows "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> q = ((m::nat) div n)" (is "?lhs \<longleftrightarrow> ?rhs")
  1346 proof
  1347   assume ?rhs
  1348   with minus_mod_eq_mult_div [symmetric] have nq: "n * q = m - (m mod n)" by simp
  1349   then have A: "n * q \<le> m" by simp
  1350   have "n - (m mod n) > 0" using mod_less_divisor assms by auto
  1351   then have "m < m + (n - (m mod n))" by simp
  1352   then have "m < n + (m - (m mod n))" by simp
  1353   with nq have "m < n + n * q" by simp
  1354   then have B: "m < n * Suc q" by simp
  1355   from A B show ?lhs ..
  1356 next
  1357   assume P: ?lhs
  1358   then have "divmod_nat_rel m n (q, m - n * q)"
  1359     unfolding divmod_nat_rel_def by (auto simp add: ac_simps)
  1360   then have "m div n = q"
  1361     by (rule div_nat_unique)
  1362   then show ?rhs by simp
  1363 qed
  1364 
  1365 theorem split_div':
  1366   "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>
  1367    (\<exists>q. (n * q \<le> m \<and> m < n * (Suc q)) \<and> P q))"
  1368   apply (cases "0 < n")
  1369   apply (simp only: add: split_div_lemma)
  1370   apply simp_all
  1371   done
  1372 
  1373 lemma split_mod:
  1374  "P(n mod k :: nat) =
  1375  ((k = 0 \<longrightarrow> P n) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P j)))"
  1376  (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
  1377 proof
  1378   assume P: ?P
  1379   show ?Q
  1380   proof (cases)
  1381     assume "k = 0"
  1382     with P show ?Q by simp
  1383   next
  1384     assume not0: "k \<noteq> 0"
  1385     thus ?Q
  1386     proof (simp, intro allI impI)
  1387       fix i j
  1388       assume "n = k*i + j" "j < k"
  1389       thus "P j" using not0 P by (simp add: ac_simps)
  1390     qed
  1391   qed
  1392 next
  1393   assume Q: ?Q
  1394   show ?P
  1395   proof (cases)
  1396     assume "k = 0"
  1397     with Q show ?P by simp
  1398   next
  1399     assume not0: "k \<noteq> 0"
  1400     with Q have R: ?R by simp
  1401     from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
  1402     show ?P by simp
  1403   qed
  1404 qed
  1405 
  1406 lemma div_eq_dividend_iff: "a \<noteq> 0 \<Longrightarrow> (a :: nat) div b = a \<longleftrightarrow> b = 1"
  1407   apply rule
  1408   apply (cases "b = 0")
  1409   apply simp_all
  1410   apply (metis (full_types) One_nat_def Suc_lessI div_less_dividend less_not_refl3)
  1411   done
  1412 
  1413 lemma (in field_char_0) of_nat_div:
  1414   "of_nat (m div n) = ((of_nat m - of_nat (m mod n)) / of_nat n)"
  1415 proof -
  1416   have "of_nat (m div n) = ((of_nat (m div n * n + m mod n) - of_nat (m mod n)) / of_nat n :: 'a)"
  1417     unfolding of_nat_add by (cases "n = 0") simp_all
  1418   then show ?thesis
  1419     by simp
  1420 qed
  1421 
  1422 
  1423 subsubsection \<open>An ``induction'' law for modulus arithmetic.\<close>
  1424 
  1425 lemma mod_induct_0:
  1426   assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
  1427   and base: "P i" and i: "i<p"
  1428   shows "P 0"
  1429 proof (rule ccontr)
  1430   assume contra: "\<not>(P 0)"
  1431   from i have p: "0<p" by simp
  1432   have "\<forall>k. 0<k \<longrightarrow> \<not> P (p-k)" (is "\<forall>k. ?A k")
  1433   proof
  1434     fix k
  1435     show "?A k"
  1436     proof (induct k)
  1437       show "?A 0" by simp  \<comment> "by contradiction"
  1438     next
  1439       fix n
  1440       assume ih: "?A n"
  1441       show "?A (Suc n)"
  1442       proof (clarsimp)
  1443         assume y: "P (p - Suc n)"
  1444         have n: "Suc n < p"
  1445         proof (rule ccontr)
  1446           assume "\<not>(Suc n < p)"
  1447           hence "p - Suc n = 0"
  1448             by simp
  1449           with y contra show "False"
  1450             by simp
  1451         qed
  1452         hence n2: "Suc (p - Suc n) = p-n" by arith
  1453         from p have "p - Suc n < p" by arith
  1454         with y step have z: "P ((Suc (p - Suc n)) mod p)"
  1455           by blast
  1456         show "False"
  1457         proof (cases "n=0")
  1458           case True
  1459           with z n2 contra show ?thesis by simp
  1460         next
  1461           case False
  1462           with p have "p-n < p" by arith
  1463           with z n2 False ih show ?thesis by simp
  1464         qed
  1465       qed
  1466     qed
  1467   qed
  1468   moreover
  1469   from i obtain k where "0<k \<and> i+k=p"
  1470     by (blast dest: less_imp_add_positive)
  1471   hence "0<k \<and> i=p-k" by auto
  1472   moreover
  1473   note base
  1474   ultimately
  1475   show "False" by blast
  1476 qed
  1477 
  1478 lemma mod_induct:
  1479   assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
  1480   and base: "P i" and i: "i<p" and j: "j<p"
  1481   shows "P j"
  1482 proof -
  1483   have "\<forall>j<p. P j"
  1484   proof
  1485     fix j
  1486     show "j<p \<longrightarrow> P j" (is "?A j")
  1487     proof (induct j)
  1488       from step base i show "?A 0"
  1489         by (auto elim: mod_induct_0)
  1490     next
  1491       fix k
  1492       assume ih: "?A k"
  1493       show "?A (Suc k)"
  1494       proof
  1495         assume suc: "Suc k < p"
  1496         hence k: "k<p" by simp
  1497         with ih have "P k" ..
  1498         with step k have "P (Suc k mod p)"
  1499           by blast
  1500         moreover
  1501         from suc have "Suc k mod p = Suc k"
  1502           by simp
  1503         ultimately
  1504         show "P (Suc k)" by simp
  1505       qed
  1506     qed
  1507   qed
  1508   with j show ?thesis by blast
  1509 qed
  1510 
  1511 lemma div2_Suc_Suc [simp]: "Suc (Suc m) div 2 = Suc (m div 2)"
  1512   by (simp add: numeral_2_eq_2 le_div_geq)
  1513 
  1514 lemma mod2_Suc_Suc [simp]: "Suc (Suc m) mod 2 = m mod 2"
  1515   by (simp add: numeral_2_eq_2 le_mod_geq)
  1516 
  1517 lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
  1518 by (simp add: mult_2 [symmetric])
  1519 
  1520 lemma mod2_gr_0 [simp]: "0 < (m::nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
  1521 proof -
  1522   { fix n :: nat have  "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (cases n) simp_all }
  1523   moreover have "m mod 2 < 2" by simp
  1524   ultimately have "m mod 2 = 0 \<or> m mod 2 = 1" .
  1525   then show ?thesis by auto
  1526 qed
  1527 
  1528 text\<open>These lemmas collapse some needless occurrences of Suc:
  1529     at least three Sucs, since two and fewer are rewritten back to Suc again!
  1530     We already have some rules to simplify operands smaller than 3.\<close>
  1531 
  1532 lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
  1533 by (simp add: Suc3_eq_add_3)
  1534 
  1535 lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
  1536 by (simp add: Suc3_eq_add_3)
  1537 
  1538 lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
  1539 by (simp add: Suc3_eq_add_3)
  1540 
  1541 lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
  1542 by (simp add: Suc3_eq_add_3)
  1543 
  1544 lemmas Suc_div_eq_add3_div_numeral [simp] = Suc_div_eq_add3_div [of _ "numeral v"] for v
  1545 lemmas Suc_mod_eq_add3_mod_numeral [simp] = Suc_mod_eq_add3_mod [of _ "numeral v"] for v
  1546 
  1547 lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1"
  1548 apply (induct "m")
  1549 apply (simp_all add: mod_Suc)
  1550 done
  1551 
  1552 declare Suc_times_mod_eq [of "numeral w", simp] for w
  1553 
  1554 lemma Suc_div_le_mono [simp]: "n div k \<le> (Suc n) div k"
  1555 by (simp add: div_le_mono)
  1556 
  1557 lemma Suc_n_div_2_gt_zero [simp]: "(0::nat) < n ==> 0 < (n + 1) div 2"
  1558 by (cases n) simp_all
  1559 
  1560 lemma div_2_gt_zero [simp]: assumes A: "(1::nat) < n" shows "0 < n div 2"
  1561 proof -
  1562   from A have B: "0 < n - 1" and C: "n - 1 + 1 = n" by simp_all
  1563   from Suc_n_div_2_gt_zero [OF B] C show ?thesis by simp
  1564 qed
  1565 
  1566 lemma mod_mult_self4 [simp]: "Suc (k*n + m) mod n = Suc m mod n"
  1567 proof -
  1568   have "Suc (k * n + m) mod n = (k * n + Suc m) mod n" by simp
  1569   also have "... = Suc m mod n" by (rule mod_mult_self3)
  1570   finally show ?thesis .
  1571 qed
  1572 
  1573 lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n"
  1574 apply (subst mod_Suc [of m])
  1575 apply (subst mod_Suc [of "m mod n"], simp)
  1576 done
  1577 
  1578 lemma mod_2_not_eq_zero_eq_one_nat:
  1579   fixes n :: nat
  1580   shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
  1581   by (fact not_mod_2_eq_0_eq_1)
  1582 
  1583 lemma even_Suc_div_two [simp]:
  1584   "even n \<Longrightarrow> Suc n div 2 = n div 2"
  1585   using even_succ_div_two [of n] by simp
  1586 
  1587 lemma odd_Suc_div_two [simp]:
  1588   "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
  1589   using odd_succ_div_two [of n] by simp
  1590 
  1591 lemma odd_two_times_div_two_nat [simp]:
  1592   assumes "odd n"
  1593   shows "2 * (n div 2) = n - (1 :: nat)"
  1594 proof -
  1595   from assms have "2 * (n div 2) + 1 = n"
  1596     by (rule odd_two_times_div_two_succ)
  1597   then have "Suc (2 * (n div 2)) - 1 = n - 1"
  1598     by simp
  1599   then show ?thesis
  1600     by simp
  1601 qed
  1602 
  1603 lemma parity_induct [case_names zero even odd]:
  1604   assumes zero: "P 0"
  1605   assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
  1606   assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
  1607   shows "P n"
  1608 proof (induct n rule: less_induct)
  1609   case (less n)
  1610   show "P n"
  1611   proof (cases "n = 0")
  1612     case True with zero show ?thesis by simp
  1613   next
  1614     case False
  1615     with less have hyp: "P (n div 2)" by simp
  1616     show ?thesis
  1617     proof (cases "even n")
  1618       case True
  1619       with hyp even [of "n div 2"] show ?thesis
  1620         by simp
  1621     next
  1622       case False
  1623       with hyp odd [of "n div 2"] show ?thesis
  1624         by simp
  1625     qed
  1626   qed
  1627 qed
  1628 
  1629 lemma Suc_0_div_numeral [simp]:
  1630   fixes k l :: num
  1631   shows "Suc 0 div numeral k = fst (divmod Num.One k)"
  1632   by (simp_all add: fst_divmod)
  1633 
  1634 lemma Suc_0_mod_numeral [simp]:
  1635   fixes k l :: num
  1636   shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
  1637   by (simp_all add: snd_divmod)
  1638 
  1639 lemma cut_eq_simps: \<comment> \<open>rewriting equivalence on \<open>n mod 2 ^ q\<close>\<close>
  1640   fixes m n q :: num
  1641   shows
  1642     "numeral n mod numeral Num.One = (0::nat)
  1643       \<longleftrightarrow> True"
  1644     "numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) = (0::nat)
  1645       \<longleftrightarrow> numeral n mod numeral q = (0::nat)"
  1646     "numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) = (0::nat)
  1647       \<longleftrightarrow> False"
  1648     "numeral m mod numeral Num.One = (numeral n mod numeral Num.One :: nat)
  1649       \<longleftrightarrow> True"
  1650     "numeral Num.One mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q) :: nat)
  1651       \<longleftrightarrow> True"
  1652     "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) :: nat)
  1653       \<longleftrightarrow> False"
  1654     "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) :: nat)
  1655       \<longleftrightarrow> (numeral n mod numeral q :: nat) = 0"
  1656     "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q) :: nat)
  1657       \<longleftrightarrow> False"
  1658     "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) :: nat)
  1659       \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q :: nat)"
  1660     "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) :: nat)
  1661       \<longleftrightarrow> False"
  1662     "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q) :: nat)
  1663       \<longleftrightarrow> (numeral m mod numeral q :: nat) = 0"
  1664     "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) :: nat)
  1665       \<longleftrightarrow> False"
  1666     "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) :: nat)
  1667       \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q :: nat)"
  1668   by (auto simp add: case_prod_beta Suc_double_not_eq_double double_not_eq_Suc_double)
  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