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