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