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