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