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