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