src/HOL/Divides.thy
author Thomas Sewell <thomas.sewell@nicta.com.au>
Wed Jun 11 14:24:23 2014 +1000 (2014-06-11)
changeset 57492 74bf65a1910a
parent 55440 721b4561007a
child 57512 cc97b347b301
permissions -rw-r--r--
Hypsubst preserves equality hypotheses

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