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