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