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