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