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