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