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