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