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