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