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