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