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