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