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