src/HOL/Divides.thy
author haftmann
Sat Jul 05 11:01:53 2014 +0200 (2014-07-05)
changeset 57514 bdc2c6b40bf2
parent 57512 cc97b347b301
child 58410 6d46ad54a2ab
permissions -rw-r--r--
prefer ac_simps collections over separate name bindings for add and mult
     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: ac_simps)
    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: ac_simps)
   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: ac_simps)
   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: ac_simps ac_simps)
   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 add: ac_simps)
   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 ac_simps}))
   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.commute mult.left_commute 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:
  1151   fixes m d r q :: nat
  1152   assumes "m mod d = r"
  1153   shows "\<exists>q. m = r + q * d"
  1154 proof -
  1155   from mod_div_equality obtain q where "q * d + m mod d = m" by blast
  1156   with assms have "m = r + q * d" by simp
  1157   then show ?thesis ..
  1158 qed
  1159 
  1160 lemma split_div:
  1161  "P(n div k :: nat) =
  1162  ((k = 0 \<longrightarrow> P 0) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P i)))"
  1163  (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
  1164 proof
  1165   assume P: ?P
  1166   show ?Q
  1167   proof (cases)
  1168     assume "k = 0"
  1169     with P show ?Q by simp
  1170   next
  1171     assume not0: "k \<noteq> 0"
  1172     thus ?Q
  1173     proof (simp, intro allI impI)
  1174       fix i j
  1175       assume n: "n = k*i + j" and j: "j < k"
  1176       show "P i"
  1177       proof (cases)
  1178         assume "i = 0"
  1179         with n j P show "P i" by simp
  1180       next
  1181         assume "i \<noteq> 0"
  1182         with not0 n j P show "P i" by(simp add:ac_simps)
  1183       qed
  1184     qed
  1185   qed
  1186 next
  1187   assume Q: ?Q
  1188   show ?P
  1189   proof (cases)
  1190     assume "k = 0"
  1191     with Q show ?P by simp
  1192   next
  1193     assume not0: "k \<noteq> 0"
  1194     with Q have R: ?R by simp
  1195     from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
  1196     show ?P by simp
  1197   qed
  1198 qed
  1199 
  1200 lemma split_div_lemma:
  1201   assumes "0 < n"
  1202   shows "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> q = ((m\<Colon>nat) div n)" (is "?lhs \<longleftrightarrow> ?rhs")
  1203 proof
  1204   assume ?rhs
  1205   with mult_div_cancel have nq: "n * q = m - (m mod n)" by simp
  1206   then have A: "n * q \<le> m" by simp
  1207   have "n - (m mod n) > 0" using mod_less_divisor assms by auto
  1208   then have "m < m + (n - (m mod n))" by simp
  1209   then have "m < n + (m - (m mod n))" by simp
  1210   with nq have "m < n + n * q" by simp
  1211   then have B: "m < n * Suc q" by simp
  1212   from A B show ?lhs ..
  1213 next
  1214   assume P: ?lhs
  1215   then have "divmod_nat_rel m n (q, m - n * q)"
  1216     unfolding divmod_nat_rel_def by (auto simp add: ac_simps)
  1217   with divmod_nat_rel_unique divmod_nat_rel [of m n]
  1218   have "(q, m - n * q) = (m div n, m mod n)" by auto
  1219   then show ?rhs by simp
  1220 qed
  1221 
  1222 theorem split_div':
  1223   "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>
  1224    (\<exists>q. (n * q \<le> m \<and> m < n * (Suc q)) \<and> P q))"
  1225   apply (case_tac "0 < n")
  1226   apply (simp only: add: split_div_lemma)
  1227   apply simp_all
  1228   done
  1229 
  1230 lemma split_mod:
  1231  "P(n mod k :: nat) =
  1232  ((k = 0 \<longrightarrow> P n) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P j)))"
  1233  (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
  1234 proof
  1235   assume P: ?P
  1236   show ?Q
  1237   proof (cases)
  1238     assume "k = 0"
  1239     with P show ?Q by simp
  1240   next
  1241     assume not0: "k \<noteq> 0"
  1242     thus ?Q
  1243     proof (simp, intro allI impI)
  1244       fix i j
  1245       assume "n = k*i + j" "j < k"
  1246       thus "P j" using not0 P by(simp add:ac_simps ac_simps)
  1247     qed
  1248   qed
  1249 next
  1250   assume Q: ?Q
  1251   show ?P
  1252   proof (cases)
  1253     assume "k = 0"
  1254     with Q show ?P by simp
  1255   next
  1256     assume not0: "k \<noteq> 0"
  1257     with Q have R: ?R by simp
  1258     from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
  1259     show ?P by simp
  1260   qed
  1261 qed
  1262 
  1263 theorem mod_div_equality': "(m::nat) mod n = m - (m div n) * n"
  1264   using mod_div_equality [of m n] by arith
  1265 
  1266 lemma div_mod_equality': "(m::nat) div n * n = m - m mod n"
  1267   using mod_div_equality [of m n] by arith
  1268 (* FIXME: very similar to mult_div_cancel *)
  1269 
  1270 lemma div_eq_dividend_iff: "a \<noteq> 0 \<Longrightarrow> (a :: nat) div b = a \<longleftrightarrow> b = 1"
  1271   apply rule
  1272   apply (cases "b = 0")
  1273   apply simp_all
  1274   apply (metis (full_types) One_nat_def Suc_lessI div_less_dividend less_not_refl3)
  1275   done
  1276 
  1277 
  1278 subsubsection {* An ``induction'' law for modulus arithmetic. *}
  1279 
  1280 lemma mod_induct_0:
  1281   assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
  1282   and base: "P i" and i: "i<p"
  1283   shows "P 0"
  1284 proof (rule ccontr)
  1285   assume contra: "\<not>(P 0)"
  1286   from i have p: "0<p" by simp
  1287   have "\<forall>k. 0<k \<longrightarrow> \<not> P (p-k)" (is "\<forall>k. ?A k")
  1288   proof
  1289     fix k
  1290     show "?A k"
  1291     proof (induct k)
  1292       show "?A 0" by simp  -- "by contradiction"
  1293     next
  1294       fix n
  1295       assume ih: "?A n"
  1296       show "?A (Suc n)"
  1297       proof (clarsimp)
  1298         assume y: "P (p - Suc n)"
  1299         have n: "Suc n < p"
  1300         proof (rule ccontr)
  1301           assume "\<not>(Suc n < p)"
  1302           hence "p - Suc n = 0"
  1303             by simp
  1304           with y contra show "False"
  1305             by simp
  1306         qed
  1307         hence n2: "Suc (p - Suc n) = p-n" by arith
  1308         from p have "p - Suc n < p" by arith
  1309         with y step have z: "P ((Suc (p - Suc n)) mod p)"
  1310           by blast
  1311         show "False"
  1312         proof (cases "n=0")
  1313           case True
  1314           with z n2 contra show ?thesis by simp
  1315         next
  1316           case False
  1317           with p have "p-n < p" by arith
  1318           with z n2 False ih show ?thesis by simp
  1319         qed
  1320       qed
  1321     qed
  1322   qed
  1323   moreover
  1324   from i obtain k where "0<k \<and> i+k=p"
  1325     by (blast dest: less_imp_add_positive)
  1326   hence "0<k \<and> i=p-k" by auto
  1327   moreover
  1328   note base
  1329   ultimately
  1330   show "False" by blast
  1331 qed
  1332 
  1333 lemma mod_induct:
  1334   assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
  1335   and base: "P i" and i: "i<p" and j: "j<p"
  1336   shows "P j"
  1337 proof -
  1338   have "\<forall>j<p. P j"
  1339   proof
  1340     fix j
  1341     show "j<p \<longrightarrow> P j" (is "?A j")
  1342     proof (induct j)
  1343       from step base i show "?A 0"
  1344         by (auto elim: mod_induct_0)
  1345     next
  1346       fix k
  1347       assume ih: "?A k"
  1348       show "?A (Suc k)"
  1349       proof
  1350         assume suc: "Suc k < p"
  1351         hence k: "k<p" by simp
  1352         with ih have "P k" ..
  1353         with step k have "P (Suc k mod p)"
  1354           by blast
  1355         moreover
  1356         from suc have "Suc k mod p = Suc k"
  1357           by simp
  1358         ultimately
  1359         show "P (Suc k)" by simp
  1360       qed
  1361     qed
  1362   qed
  1363   with j show ?thesis by blast
  1364 qed
  1365 
  1366 lemma div2_Suc_Suc [simp]: "Suc (Suc m) div 2 = Suc (m div 2)"
  1367   by (simp add: numeral_2_eq_2 le_div_geq)
  1368 
  1369 lemma mod2_Suc_Suc [simp]: "Suc (Suc m) mod 2 = m mod 2"
  1370   by (simp add: numeral_2_eq_2 le_mod_geq)
  1371 
  1372 lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
  1373 by (simp add: mult_2 [symmetric])
  1374 
  1375 lemma mod2_gr_0 [simp]: "0 < (m\<Colon>nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
  1376 proof -
  1377   { fix n :: nat have  "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (cases n) simp_all }
  1378   moreover have "m mod 2 < 2" by simp
  1379   ultimately have "m mod 2 = 0 \<or> m mod 2 = 1" .
  1380   then show ?thesis by auto
  1381 qed
  1382 
  1383 text{*These lemmas collapse some needless occurrences of Suc:
  1384     at least three Sucs, since two and fewer are rewritten back to Suc again!
  1385     We already have some rules to simplify operands smaller than 3.*}
  1386 
  1387 lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
  1388 by (simp add: Suc3_eq_add_3)
  1389 
  1390 lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
  1391 by (simp add: Suc3_eq_add_3)
  1392 
  1393 lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
  1394 by (simp add: Suc3_eq_add_3)
  1395 
  1396 lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
  1397 by (simp add: Suc3_eq_add_3)
  1398 
  1399 lemmas Suc_div_eq_add3_div_numeral [simp] = Suc_div_eq_add3_div [of _ "numeral v"] for v
  1400 lemmas Suc_mod_eq_add3_mod_numeral [simp] = Suc_mod_eq_add3_mod [of _ "numeral v"] for v
  1401 
  1402 
  1403 lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1" 
  1404 apply (induct "m")
  1405 apply (simp_all add: mod_Suc)
  1406 done
  1407 
  1408 declare Suc_times_mod_eq [of "numeral w", simp] for w
  1409 
  1410 lemma Suc_div_le_mono [simp]: "n div k \<le> (Suc n) div k"
  1411 by (simp add: div_le_mono)
  1412 
  1413 lemma Suc_n_div_2_gt_zero [simp]: "(0::nat) < n ==> 0 < (n + 1) div 2"
  1414 by (cases n) simp_all
  1415 
  1416 lemma div_2_gt_zero [simp]: assumes A: "(1::nat) < n" shows "0 < n div 2"
  1417 proof -
  1418   from A have B: "0 < n - 1" and C: "n - 1 + 1 = n" by simp_all
  1419   from Suc_n_div_2_gt_zero [OF B] C show ?thesis by simp 
  1420 qed
  1421 
  1422   (* Potential use of algebra : Equality modulo n*)
  1423 lemma mod_mult_self3 [simp]: "(k*n + m) mod n = m mod (n::nat)"
  1424 by (simp add: ac_simps ac_simps)
  1425 
  1426 lemma mod_mult_self4 [simp]: "Suc (k*n + m) mod n = Suc m mod n"
  1427 proof -
  1428   have "Suc (k * n + m) mod n = (k * n + Suc m) mod n" by simp
  1429   also have "... = Suc m mod n" by (rule mod_mult_self3) 
  1430   finally show ?thesis .
  1431 qed
  1432 
  1433 lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n"
  1434 apply (subst mod_Suc [of m]) 
  1435 apply (subst mod_Suc [of "m mod n"], simp) 
  1436 done
  1437 
  1438 lemma mod_2_not_eq_zero_eq_one_nat:
  1439   fixes n :: nat
  1440   shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
  1441   by simp
  1442 
  1443 instance nat :: semiring_numeral_div
  1444   by intro_classes (auto intro: div_positive simp add: mult_div_cancel mod_mult2_eq div_mult2_eq)
  1445 
  1446 
  1447 subsection {* Division on @{typ int} *}
  1448 
  1449 definition divmod_int_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" where
  1450     --{*definition of quotient and remainder*}
  1451   "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
  1452     (if 0 < b then 0 \<le> r \<and> r < b else if b < 0 then b < r \<and> r \<le> 0 else q = 0))"
  1453 
  1454 text {*
  1455   The following algorithmic devlopment actually echos what has already
  1456   been developed in class @{class semiring_numeral_div}.  In the long
  1457   run it seems better to derive division on @{typ int} just from
  1458   division on @{typ nat} and instantiate @{class semiring_numeral_div}
  1459   accordingly.
  1460 *}
  1461 
  1462 definition adjust :: "int \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int" where
  1463     --{*for the division algorithm*}
  1464     "adjust b = (\<lambda>(q, r). if 0 \<le> r - b then (2 * q + 1, r - b)
  1465                          else (2 * q, r))"
  1466 
  1467 text{*algorithm for the case @{text "a\<ge>0, b>0"}*}
  1468 function posDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
  1469   "posDivAlg a b = (if a < b \<or>  b \<le> 0 then (0, a)
  1470      else adjust b (posDivAlg a (2 * b)))"
  1471 by auto
  1472 termination by (relation "measure (\<lambda>(a, b). nat (a - b + 1))")
  1473   (auto simp add: mult_2)
  1474 
  1475 text{*algorithm for the case @{text "a<0, b>0"}*}
  1476 function negDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
  1477   "negDivAlg a b = (if 0 \<le>a + b \<or> b \<le> 0  then (-1, a + b)
  1478      else adjust b (negDivAlg a (2 * b)))"
  1479 by auto
  1480 termination by (relation "measure (\<lambda>(a, b). nat (- a - b))")
  1481   (auto simp add: mult_2)
  1482 
  1483 text{*algorithm for the general case @{term "b\<noteq>0"}*}
  1484 
  1485 definition divmod_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
  1486     --{*The full division algorithm considers all possible signs for a, b
  1487        including the special case @{text "a=0, b<0"} because 
  1488        @{term negDivAlg} requires @{term "a<0"}.*}
  1489   "divmod_int a b = (if 0 \<le> a then if 0 \<le> b then posDivAlg a b
  1490                   else if a = 0 then (0, 0)
  1491                        else apsnd uminus (negDivAlg (-a) (-b))
  1492                else 
  1493                   if 0 < b then negDivAlg a b
  1494                   else apsnd uminus (posDivAlg (-a) (-b)))"
  1495 
  1496 instantiation int :: Divides.div
  1497 begin
  1498 
  1499 definition div_int where
  1500   "a div b = fst (divmod_int a b)"
  1501 
  1502 lemma fst_divmod_int [simp]:
  1503   "fst (divmod_int a b) = a div b"
  1504   by (simp add: div_int_def)
  1505 
  1506 definition mod_int where
  1507   "a mod b = snd (divmod_int a b)"
  1508 
  1509 lemma snd_divmod_int [simp]:
  1510   "snd (divmod_int a b) = a mod b"
  1511   by (simp add: mod_int_def)
  1512 
  1513 instance ..
  1514 
  1515 end
  1516 
  1517 lemma divmod_int_mod_div:
  1518   "divmod_int p q = (p div q, p mod q)"
  1519   by (simp add: prod_eq_iff)
  1520 
  1521 text{*
  1522 Here is the division algorithm in ML:
  1523 
  1524 \begin{verbatim}
  1525     fun posDivAlg (a,b) =
  1526       if a<b then (0,a)
  1527       else let val (q,r) = posDivAlg(a, 2*b)
  1528                in  if 0\<le>r-b then (2*q+1, r-b) else (2*q, r)
  1529            end
  1530 
  1531     fun negDivAlg (a,b) =
  1532       if 0\<le>a+b then (~1,a+b)
  1533       else let val (q,r) = negDivAlg(a, 2*b)
  1534                in  if 0\<le>r-b then (2*q+1, r-b) else (2*q, r)
  1535            end;
  1536 
  1537     fun negateSnd (q,r:int) = (q,~r);
  1538 
  1539     fun divmod (a,b) = if 0\<le>a then 
  1540                           if b>0 then posDivAlg (a,b) 
  1541                            else if a=0 then (0,0)
  1542                                 else negateSnd (negDivAlg (~a,~b))
  1543                        else 
  1544                           if 0<b then negDivAlg (a,b)
  1545                           else        negateSnd (posDivAlg (~a,~b));
  1546 \end{verbatim}
  1547 *}
  1548 
  1549 
  1550 subsubsection {* Uniqueness and Monotonicity of Quotients and Remainders *}
  1551 
  1552 lemma unique_quotient_lemma:
  1553      "[| b*q' + r'  \<le> b*q + r;  0 \<le> r';  r' < b;  r < b |]  
  1554       ==> q' \<le> (q::int)"
  1555 apply (subgoal_tac "r' + b * (q'-q) \<le> r")
  1556  prefer 2 apply (simp add: right_diff_distrib)
  1557 apply (subgoal_tac "0 < b * (1 + q - q') ")
  1558 apply (erule_tac [2] order_le_less_trans)
  1559  prefer 2 apply (simp add: right_diff_distrib distrib_left)
  1560 apply (subgoal_tac "b * q' < b * (1 + q) ")
  1561  prefer 2 apply (simp add: right_diff_distrib distrib_left)
  1562 apply (simp add: mult_less_cancel_left)
  1563 done
  1564 
  1565 lemma unique_quotient_lemma_neg:
  1566      "[| b*q' + r' \<le> b*q + r;  r \<le> 0;  b < r;  b < r' |]  
  1567       ==> q \<le> (q'::int)"
  1568 by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma, 
  1569     auto)
  1570 
  1571 lemma unique_quotient:
  1572      "[| divmod_int_rel a b (q, r); divmod_int_rel a b (q', r') |]  
  1573       ==> q = q'"
  1574 apply (simp add: divmod_int_rel_def linorder_neq_iff split: split_if_asm)
  1575 apply (blast intro: order_antisym
  1576              dest: order_eq_refl [THEN unique_quotient_lemma] 
  1577              order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
  1578 done
  1579 
  1580 
  1581 lemma unique_remainder:
  1582      "[| divmod_int_rel a b (q, r); divmod_int_rel a b (q', r') |]  
  1583       ==> r = r'"
  1584 apply (subgoal_tac "q = q'")
  1585  apply (simp add: divmod_int_rel_def)
  1586 apply (blast intro: unique_quotient)
  1587 done
  1588 
  1589 
  1590 subsubsection {* Correctness of @{term posDivAlg}, the Algorithm for Non-Negative Dividends *}
  1591 
  1592 text{*And positive divisors*}
  1593 
  1594 lemma adjust_eq [simp]:
  1595      "adjust b (q, r) = 
  1596       (let diff = r - b in  
  1597         if 0 \<le> diff then (2 * q + 1, diff)   
  1598                      else (2*q, r))"
  1599   by (simp add: Let_def adjust_def)
  1600 
  1601 declare posDivAlg.simps [simp del]
  1602 
  1603 text{*use with a simproc to avoid repeatedly proving the premise*}
  1604 lemma posDivAlg_eqn:
  1605      "0 < b ==>  
  1606       posDivAlg a b = (if a<b then (0,a) else adjust b (posDivAlg a (2*b)))"
  1607 by (rule posDivAlg.simps [THEN trans], simp)
  1608 
  1609 text{*Correctness of @{term posDivAlg}: it computes quotients correctly*}
  1610 theorem posDivAlg_correct:
  1611   assumes "0 \<le> a" and "0 < b"
  1612   shows "divmod_int_rel a b (posDivAlg a b)"
  1613   using assms
  1614   apply (induct a b rule: posDivAlg.induct)
  1615   apply auto
  1616   apply (simp add: divmod_int_rel_def)
  1617   apply (subst posDivAlg_eqn, simp add: distrib_left)
  1618   apply (case_tac "a < b")
  1619   apply simp_all
  1620   apply (erule splitE)
  1621   apply (auto simp add: distrib_left Let_def ac_simps mult_2_right)
  1622   done
  1623 
  1624 
  1625 subsubsection {* Correctness of @{term negDivAlg}, the Algorithm for Negative Dividends *}
  1626 
  1627 text{*And positive divisors*}
  1628 
  1629 declare negDivAlg.simps [simp del]
  1630 
  1631 text{*use with a simproc to avoid repeatedly proving the premise*}
  1632 lemma negDivAlg_eqn:
  1633      "0 < b ==>  
  1634       negDivAlg a b =       
  1635        (if 0\<le>a+b then (-1,a+b) else adjust b (negDivAlg a (2*b)))"
  1636 by (rule negDivAlg.simps [THEN trans], simp)
  1637 
  1638 (*Correctness of negDivAlg: it computes quotients correctly
  1639   It doesn't work if a=0 because the 0/b equals 0, not -1*)
  1640 lemma negDivAlg_correct:
  1641   assumes "a < 0" and "b > 0"
  1642   shows "divmod_int_rel a b (negDivAlg a b)"
  1643   using assms
  1644   apply (induct a b rule: negDivAlg.induct)
  1645   apply (auto simp add: linorder_not_le)
  1646   apply (simp add: divmod_int_rel_def)
  1647   apply (subst negDivAlg_eqn, assumption)
  1648   apply (case_tac "a + b < (0\<Colon>int)")
  1649   apply simp_all
  1650   apply (erule splitE)
  1651   apply (auto simp add: distrib_left Let_def ac_simps mult_2_right)
  1652   done
  1653 
  1654 
  1655 subsubsection {* Existence Shown by Proving the Division Algorithm to be Correct *}
  1656 
  1657 (*the case a=0*)
  1658 lemma divmod_int_rel_0: "divmod_int_rel 0 b (0, 0)"
  1659 by (auto simp add: divmod_int_rel_def linorder_neq_iff)
  1660 
  1661 lemma posDivAlg_0 [simp]: "posDivAlg 0 b = (0, 0)"
  1662 by (subst posDivAlg.simps, auto)
  1663 
  1664 lemma posDivAlg_0_right [simp]: "posDivAlg a 0 = (0, a)"
  1665 by (subst posDivAlg.simps, auto)
  1666 
  1667 lemma negDivAlg_minus1 [simp]: "negDivAlg -1 b = (-1, b - 1)"
  1668 by (subst negDivAlg.simps, auto)
  1669 
  1670 lemma divmod_int_rel_neg: "divmod_int_rel (-a) (-b) qr ==> divmod_int_rel a b (apsnd uminus qr)"
  1671 by (auto simp add: divmod_int_rel_def)
  1672 
  1673 lemma divmod_int_correct: "divmod_int_rel a b (divmod_int a b)"
  1674 apply (cases "b = 0", simp add: divmod_int_def divmod_int_rel_def)
  1675 by (force simp add: linorder_neq_iff divmod_int_rel_0 divmod_int_def divmod_int_rel_neg
  1676                     posDivAlg_correct negDivAlg_correct)
  1677 
  1678 lemma divmod_int_unique:
  1679   assumes "divmod_int_rel a b qr" 
  1680   shows "divmod_int a b = qr"
  1681   using assms divmod_int_correct [of a b]
  1682   using unique_quotient [of a b] unique_remainder [of a b]
  1683   by (metis pair_collapse)
  1684 
  1685 lemma divmod_int_rel_div_mod: "divmod_int_rel a b (a div b, a mod b)"
  1686   using divmod_int_correct by (simp add: divmod_int_mod_div)
  1687 
  1688 lemma div_int_unique: "divmod_int_rel a b (q, r) \<Longrightarrow> a div b = q"
  1689   by (simp add: divmod_int_rel_div_mod [THEN unique_quotient])
  1690 
  1691 lemma mod_int_unique: "divmod_int_rel a b (q, r) \<Longrightarrow> a mod b = r"
  1692   by (simp add: divmod_int_rel_div_mod [THEN unique_remainder])
  1693 
  1694 instance int :: ring_div
  1695 proof
  1696   fix a b :: int
  1697   show "a div b * b + a mod b = a"
  1698     using divmod_int_rel_div_mod [of a b]
  1699     unfolding divmod_int_rel_def by (simp add: mult.commute)
  1700 next
  1701   fix a b c :: int
  1702   assume "b \<noteq> 0"
  1703   hence "divmod_int_rel (a + c * b) b (c + a div b, a mod b)"
  1704     using divmod_int_rel_div_mod [of a b]
  1705     unfolding divmod_int_rel_def by (auto simp: algebra_simps)
  1706   thus "(a + c * b) div b = c + a div b"
  1707     by (rule div_int_unique)
  1708 next
  1709   fix a b c :: int
  1710   assume "c \<noteq> 0"
  1711   hence "\<And>q r. divmod_int_rel a b (q, r)
  1712     \<Longrightarrow> divmod_int_rel (c * a) (c * b) (q, c * r)"
  1713     unfolding divmod_int_rel_def
  1714     by - (rule linorder_cases [of 0 b], auto simp: algebra_simps
  1715       mult_less_0_iff zero_less_mult_iff mult_strict_right_mono
  1716       mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff)
  1717   hence "divmod_int_rel (c * a) (c * b) (a div b, c * (a mod b))"
  1718     using divmod_int_rel_div_mod [of a b] .
  1719   thus "(c * a) div (c * b) = a div b"
  1720     by (rule div_int_unique)
  1721 next
  1722   fix a :: int show "a div 0 = 0"
  1723     by (rule div_int_unique, simp add: divmod_int_rel_def)
  1724 next
  1725   fix a :: int show "0 div a = 0"
  1726     by (rule div_int_unique, auto simp add: divmod_int_rel_def)
  1727 qed
  1728 
  1729 text{*Basic laws about division and remainder*}
  1730 
  1731 lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
  1732   by (fact mod_div_equality2 [symmetric])
  1733 
  1734 text {* Tool setup *}
  1735 
  1736 (* FIXME: Theorem list add_0s doesn't exist, because Numeral0 has gone. *)
  1737 lemmas add_0s = add_0_left add_0_right
  1738 
  1739 ML {*
  1740 structure Cancel_Div_Mod_Int = Cancel_Div_Mod
  1741 (
  1742   val div_name = @{const_name div};
  1743   val mod_name = @{const_name mod};
  1744   val mk_binop = HOLogic.mk_binop;
  1745   val mk_sum = Arith_Data.mk_sum HOLogic.intT;
  1746   val dest_sum = Arith_Data.dest_sum;
  1747 
  1748   val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
  1749 
  1750   val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac 
  1751     (@{thm diff_conv_add_uminus} :: @{thms add_0s} @ @{thms ac_simps}))
  1752 )
  1753 *}
  1754 
  1755 simproc_setup cancel_div_mod_int ("(k::int) + l") = {* K Cancel_Div_Mod_Int.proc *}
  1756 
  1757 lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
  1758   using divmod_int_correct [of a b]
  1759   by (auto simp add: divmod_int_rel_def prod_eq_iff)
  1760 
  1761 lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1]
  1762    and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2]
  1763 
  1764 lemma neg_mod_conj: "b < (0::int) \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b"
  1765   using divmod_int_correct [of a b]
  1766   by (auto simp add: divmod_int_rel_def prod_eq_iff)
  1767 
  1768 lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1]
  1769    and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2]
  1770 
  1771 
  1772 subsubsection {* General Properties of div and mod *}
  1773 
  1774 lemma div_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a div b = 0"
  1775 apply (rule div_int_unique)
  1776 apply (auto simp add: divmod_int_rel_def)
  1777 done
  1778 
  1779 lemma div_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a div b = 0"
  1780 apply (rule div_int_unique)
  1781 apply (auto simp add: divmod_int_rel_def)
  1782 done
  1783 
  1784 lemma div_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a div b = -1"
  1785 apply (rule div_int_unique)
  1786 apply (auto simp add: divmod_int_rel_def)
  1787 done
  1788 
  1789 (*There is no div_neg_pos_trivial because  0 div b = 0 would supersede it*)
  1790 
  1791 lemma mod_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a mod b = a"
  1792 apply (rule_tac q = 0 in mod_int_unique)
  1793 apply (auto simp add: divmod_int_rel_def)
  1794 done
  1795 
  1796 lemma mod_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a mod b = a"
  1797 apply (rule_tac q = 0 in mod_int_unique)
  1798 apply (auto simp add: divmod_int_rel_def)
  1799 done
  1800 
  1801 lemma mod_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a mod b = a+b"
  1802 apply (rule_tac q = "-1" in mod_int_unique)
  1803 apply (auto simp add: divmod_int_rel_def)
  1804 done
  1805 
  1806 text{*There is no @{text mod_neg_pos_trivial}.*}
  1807 
  1808 
  1809 subsubsection {* Laws for div and mod with Unary Minus *}
  1810 
  1811 lemma zminus1_lemma:
  1812      "divmod_int_rel a b (q, r) ==> b \<noteq> 0
  1813       ==> divmod_int_rel (-a) b (if r=0 then -q else -q - 1,  
  1814                           if r=0 then 0 else b-r)"
  1815 by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_diff_distrib)
  1816 
  1817 
  1818 lemma zdiv_zminus1_eq_if:
  1819      "b \<noteq> (0::int)  
  1820       ==> (-a) div b =  
  1821           (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
  1822 by (blast intro: divmod_int_rel_div_mod [THEN zminus1_lemma, THEN div_int_unique])
  1823 
  1824 lemma zmod_zminus1_eq_if:
  1825      "(-a::int) mod b = (if a mod b = 0 then 0 else  b - (a mod b))"
  1826 apply (case_tac "b = 0", simp)
  1827 apply (blast intro: divmod_int_rel_div_mod [THEN zminus1_lemma, THEN mod_int_unique])
  1828 done
  1829 
  1830 lemma zmod_zminus1_not_zero:
  1831   fixes k l :: int
  1832   shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
  1833   unfolding zmod_zminus1_eq_if by auto
  1834 
  1835 lemma zdiv_zminus2_eq_if:
  1836      "b \<noteq> (0::int)  
  1837       ==> a div (-b) =  
  1838           (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
  1839 by (simp add: zdiv_zminus1_eq_if div_minus_right)
  1840 
  1841 lemma zmod_zminus2_eq_if:
  1842      "a mod (-b::int) = (if a mod b = 0 then 0 else  (a mod b) - b)"
  1843 by (simp add: zmod_zminus1_eq_if mod_minus_right)
  1844 
  1845 lemma zmod_zminus2_not_zero:
  1846   fixes k l :: int
  1847   shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
  1848   unfolding zmod_zminus2_eq_if by auto 
  1849 
  1850 
  1851 subsubsection {* Computation of Division and Remainder *}
  1852 
  1853 lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"
  1854 by (simp add: div_int_def divmod_int_def)
  1855 
  1856 lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
  1857 by (simp add: mod_int_def divmod_int_def)
  1858 
  1859 text{*a positive, b positive *}
  1860 
  1861 lemma div_pos_pos: "[| 0 < a;  0 \<le> b |] ==> a div b = fst (posDivAlg a b)"
  1862 by (simp add: div_int_def divmod_int_def)
  1863 
  1864 lemma mod_pos_pos: "[| 0 < a;  0 \<le> b |] ==> a mod b = snd (posDivAlg a b)"
  1865 by (simp add: mod_int_def divmod_int_def)
  1866 
  1867 text{*a negative, b positive *}
  1868 
  1869 lemma div_neg_pos: "[| a < 0;  0 < b |] ==> a div b = fst (negDivAlg a b)"
  1870 by (simp add: div_int_def divmod_int_def)
  1871 
  1872 lemma mod_neg_pos: "[| a < 0;  0 < b |] ==> a mod b = snd (negDivAlg a b)"
  1873 by (simp add: mod_int_def divmod_int_def)
  1874 
  1875 text{*a positive, b negative *}
  1876 
  1877 lemma div_pos_neg:
  1878      "[| 0 < a;  b < 0 |] ==> a div b = fst (apsnd uminus (negDivAlg (-a) (-b)))"
  1879 by (simp add: div_int_def divmod_int_def)
  1880 
  1881 lemma mod_pos_neg:
  1882      "[| 0 < a;  b < 0 |] ==> a mod b = snd (apsnd uminus (negDivAlg (-a) (-b)))"
  1883 by (simp add: mod_int_def divmod_int_def)
  1884 
  1885 text{*a negative, b negative *}
  1886 
  1887 lemma div_neg_neg:
  1888      "[| a < 0;  b \<le> 0 |] ==> a div b = fst (apsnd uminus (posDivAlg (-a) (-b)))"
  1889 by (simp add: div_int_def divmod_int_def)
  1890 
  1891 lemma mod_neg_neg:
  1892      "[| a < 0;  b \<le> 0 |] ==> a mod b = snd (apsnd uminus (posDivAlg (-a) (-b)))"
  1893 by (simp add: mod_int_def divmod_int_def)
  1894 
  1895 text {*Simplify expresions in which div and mod combine numerical constants*}
  1896 
  1897 lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
  1898   by (rule div_int_unique [of a b q r]) (simp add: divmod_int_rel_def)
  1899 
  1900 lemma int_div_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a div b = q"
  1901   by (rule div_int_unique [of a b q r],
  1902     simp add: divmod_int_rel_def)
  1903 
  1904 lemma int_mod_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<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 lemma int_mod_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a mod b = r"
  1909   by (rule mod_int_unique [of a b q r],
  1910     simp add: divmod_int_rel_def)
  1911 
  1912 text {*
  1913   numeral simprocs -- high chance that these can be replaced
  1914   by divmod algorithm from @{class semiring_numeral_div}
  1915 *}
  1916 
  1917 ML {*
  1918 local
  1919   val mk_number = HOLogic.mk_number HOLogic.intT
  1920   val plus = @{term "plus :: int \<Rightarrow> int \<Rightarrow> int"}
  1921   val times = @{term "times :: int \<Rightarrow> int \<Rightarrow> int"}
  1922   val zero = @{term "0 :: int"}
  1923   val less = @{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"}
  1924   val le = @{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"}
  1925   val simps = @{thms arith_simps} @ @{thms rel_simps} @ [@{thm numeral_1_eq_1 [symmetric]}]
  1926   fun prove ctxt goal = (writeln "prove"; Goal.prove ctxt [] [] (HOLogic.mk_Trueprop goal)
  1927     (K (ALLGOALS (full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps)))));
  1928   fun binary_proc proc ctxt ct =
  1929     (case Thm.term_of ct of
  1930       _ $ t $ u =>
  1931       (case try (pairself (`(snd o HOLogic.dest_number))) (t, u) of
  1932         SOME args => proc ctxt args
  1933       | NONE => NONE)
  1934     | _ => NONE);
  1935 in
  1936   fun divmod_proc posrule negrule =
  1937     binary_proc (fn ctxt => fn ((a, t), (b, u)) =>
  1938       if b = 0 then NONE else let
  1939         val (q, r) = pairself mk_number (Integer.div_mod a b)
  1940         val goal1 = HOLogic.mk_eq (t, plus $ (times $ u $ q) $ r)
  1941         val (goal2, goal3, rule) = if b > 0
  1942           then (le $ zero $ r, less $ r $ u, posrule RS eq_reflection)
  1943           else (le $ r $ zero, less $ u $ r, negrule RS eq_reflection)
  1944       in SOME (rule OF map (prove ctxt) [goal1, goal2, goal3]) end)
  1945 end
  1946 *}
  1947 
  1948 simproc_setup binary_int_div
  1949   ("numeral m div numeral n :: int" |
  1950    "numeral m div - numeral n :: int" |
  1951    "- numeral m div numeral n :: int" |
  1952    "- numeral m div - numeral n :: int") =
  1953   {* K (divmod_proc @{thm int_div_pos_eq} @{thm int_div_neg_eq}) *}
  1954 
  1955 simproc_setup binary_int_mod
  1956   ("numeral m mod numeral n :: int" |
  1957    "numeral m mod - numeral n :: int" |
  1958    "- numeral m mod numeral n :: int" |
  1959    "- numeral m mod - numeral n :: int") =
  1960   {* K (divmod_proc @{thm int_mod_pos_eq} @{thm int_mod_neg_eq}) *}
  1961 
  1962 lemmas posDivAlg_eqn_numeral [simp] =
  1963     posDivAlg_eqn [of "numeral v" "numeral w", OF zero_less_numeral] for v w
  1964 
  1965 lemmas negDivAlg_eqn_numeral [simp] =
  1966     negDivAlg_eqn [of "numeral v" "- numeral w", OF zero_less_numeral] for v w
  1967 
  1968 
  1969 text {* Special-case simplification: @{text "\<plusminus>1 div z"} and @{text "\<plusminus>1 mod z"} *}
  1970 
  1971 lemma [simp]:
  1972   shows div_one_bit0: "1 div numeral (Num.Bit0 v) = (0 :: int)"
  1973     and mod_one_bit0: "1 mod numeral (Num.Bit0 v) = (1 :: int)"
  1974     and div_one_bit1: "1 div numeral (Num.Bit1 v) = (0 :: int)"
  1975     and mod_one_bit1: "1 mod numeral (Num.Bit1 v) = (1 :: int)"
  1976     and div_one_neg_numeral: "1 div - numeral v = (- 1 :: int)"
  1977     and mod_one_neg_numeral: "1 mod - numeral v = (1 :: int) - numeral v"
  1978   by (simp_all del: arith_special
  1979     add: div_pos_pos mod_pos_pos div_pos_neg mod_pos_neg posDivAlg_eqn)
  1980 
  1981 lemma [simp]:
  1982   shows div_neg_one_numeral: "- 1 div numeral v = (- 1 :: int)"
  1983     and mod_neg_one_numeral: "- 1 mod numeral v = numeral v - (1 :: int)"
  1984     and div_neg_one_neg_bit0: "- 1 div - numeral (Num.Bit0 v) = (0 :: int)"
  1985     and mod_neg_one_neb_bit0: "- 1 mod - numeral (Num.Bit0 v) = (- 1 :: int)"
  1986     and div_neg_one_neg_bit1: "- 1 div - numeral (Num.Bit1 v) = (0 :: int)"
  1987     and mod_neg_one_neb_bit1: "- 1 mod - numeral (Num.Bit1 v) = (- 1 :: int)"
  1988   by (simp_all add: div_eq_minus1 zmod_minus1)
  1989 
  1990 
  1991 subsubsection {* Monotonicity in the First Argument (Dividend) *}
  1992 
  1993 lemma zdiv_mono1: "[| a \<le> a';  0 < (b::int) |] ==> a div b \<le> a' div b"
  1994 apply (cut_tac a = a and b = b in zmod_zdiv_equality)
  1995 apply (cut_tac a = a' and b = b in zmod_zdiv_equality)
  1996 apply (rule unique_quotient_lemma)
  1997 apply (erule subst)
  1998 apply (erule subst, simp_all)
  1999 done
  2000 
  2001 lemma zdiv_mono1_neg: "[| a \<le> a';  (b::int) < 0 |] ==> a' div b \<le> a div b"
  2002 apply (cut_tac a = a and b = b in zmod_zdiv_equality)
  2003 apply (cut_tac a = a' and b = b in zmod_zdiv_equality)
  2004 apply (rule unique_quotient_lemma_neg)
  2005 apply (erule subst)
  2006 apply (erule subst, simp_all)
  2007 done
  2008 
  2009 
  2010 subsubsection {* Monotonicity in the Second Argument (Divisor) *}
  2011 
  2012 lemma q_pos_lemma:
  2013      "[| 0 \<le> b'*q' + r'; r' < b';  0 < b' |] ==> 0 \<le> (q'::int)"
  2014 apply (subgoal_tac "0 < b'* (q' + 1) ")
  2015  apply (simp add: zero_less_mult_iff)
  2016 apply (simp add: distrib_left)
  2017 done
  2018 
  2019 lemma zdiv_mono2_lemma:
  2020      "[| b*q + r = b'*q' + r';  0 \<le> b'*q' + r';   
  2021          r' < b';  0 \<le> r;  0 < b';  b' \<le> b |]   
  2022       ==> q \<le> (q'::int)"
  2023 apply (frule q_pos_lemma, assumption+) 
  2024 apply (subgoal_tac "b*q < b* (q' + 1) ")
  2025  apply (simp add: mult_less_cancel_left)
  2026 apply (subgoal_tac "b*q = r' - r + b'*q'")
  2027  prefer 2 apply simp
  2028 apply (simp (no_asm_simp) add: distrib_left)
  2029 apply (subst add.commute, rule add_less_le_mono, arith)
  2030 apply (rule mult_right_mono, auto)
  2031 done
  2032 
  2033 lemma zdiv_mono2:
  2034      "[| (0::int) \<le> a;  0 < b';  b' \<le> b |] ==> a div b \<le> a div b'"
  2035 apply (subgoal_tac "b \<noteq> 0")
  2036  prefer 2 apply arith
  2037 apply (cut_tac a = a and b = b in zmod_zdiv_equality)
  2038 apply (cut_tac a = a and b = b' in zmod_zdiv_equality)
  2039 apply (rule zdiv_mono2_lemma)
  2040 apply (erule subst)
  2041 apply (erule subst, simp_all)
  2042 done
  2043 
  2044 lemma q_neg_lemma:
  2045      "[| b'*q' + r' < 0;  0 \<le> r';  0 < b' |] ==> q' \<le> (0::int)"
  2046 apply (subgoal_tac "b'*q' < 0")
  2047  apply (simp add: mult_less_0_iff, arith)
  2048 done
  2049 
  2050 lemma zdiv_mono2_neg_lemma:
  2051      "[| b*q + r = b'*q' + r';  b'*q' + r' < 0;   
  2052          r < b;  0 \<le> r';  0 < b';  b' \<le> b |]   
  2053       ==> q' \<le> (q::int)"
  2054 apply (frule q_neg_lemma, assumption+) 
  2055 apply (subgoal_tac "b*q' < b* (q + 1) ")
  2056  apply (simp add: mult_less_cancel_left)
  2057 apply (simp add: distrib_left)
  2058 apply (subgoal_tac "b*q' \<le> b'*q'")
  2059  prefer 2 apply (simp add: mult_right_mono_neg, arith)
  2060 done
  2061 
  2062 lemma zdiv_mono2_neg:
  2063      "[| a < (0::int);  0 < b';  b' \<le> b |] ==> a div b' \<le> a div b"
  2064 apply (cut_tac a = a and b = b in zmod_zdiv_equality)
  2065 apply (cut_tac a = a and b = b' in zmod_zdiv_equality)
  2066 apply (rule zdiv_mono2_neg_lemma)
  2067 apply (erule subst)
  2068 apply (erule subst, simp_all)
  2069 done
  2070 
  2071 
  2072 subsubsection {* More Algebraic Laws for div and mod *}
  2073 
  2074 text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *}
  2075 
  2076 lemma zmult1_lemma:
  2077      "[| divmod_int_rel b c (q, r) |]  
  2078       ==> divmod_int_rel (a * b) c (a*q + a*r div c, a*r mod c)"
  2079 by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left ac_simps)
  2080 
  2081 lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
  2082 apply (case_tac "c = 0", simp)
  2083 apply (blast intro: divmod_int_rel_div_mod [THEN zmult1_lemma, THEN div_int_unique])
  2084 done
  2085 
  2086 text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
  2087 
  2088 lemma zadd1_lemma:
  2089      "[| divmod_int_rel a c (aq, ar);  divmod_int_rel b c (bq, br) |]  
  2090       ==> divmod_int_rel (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
  2091 by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left)
  2092 
  2093 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
  2094 lemma zdiv_zadd1_eq:
  2095      "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
  2096 apply (case_tac "c = 0", simp)
  2097 apply (blast intro: zadd1_lemma [OF divmod_int_rel_div_mod divmod_int_rel_div_mod] div_int_unique)
  2098 done
  2099 
  2100 lemma posDivAlg_div_mod:
  2101   assumes "k \<ge> 0"
  2102   and "l \<ge> 0"
  2103   shows "posDivAlg k l = (k div l, k mod l)"
  2104 proof (cases "l = 0")
  2105   case True then show ?thesis by (simp add: posDivAlg.simps)
  2106 next
  2107   case False with assms posDivAlg_correct
  2108     have "divmod_int_rel k l (fst (posDivAlg k l), snd (posDivAlg k l))"
  2109     by simp
  2110   from div_int_unique [OF this] mod_int_unique [OF this]
  2111   show ?thesis by simp
  2112 qed
  2113 
  2114 lemma negDivAlg_div_mod:
  2115   assumes "k < 0"
  2116   and "l > 0"
  2117   shows "negDivAlg k l = (k div l, k mod l)"
  2118 proof -
  2119   from assms have "l \<noteq> 0" by simp
  2120   from assms negDivAlg_correct
  2121     have "divmod_int_rel k l (fst (negDivAlg k l), snd (negDivAlg k l))"
  2122     by simp
  2123   from div_int_unique [OF this] mod_int_unique [OF this]
  2124   show ?thesis by simp
  2125 qed
  2126 
  2127 lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
  2128 by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
  2129 
  2130 (* REVISIT: should this be generalized to all semiring_div types? *)
  2131 lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
  2132 
  2133 lemma zmod_zdiv_equality':
  2134   "(m\<Colon>int) mod n = m - (m div n) * n"
  2135   using mod_div_equality [of m n] by arith
  2136 
  2137 
  2138 subsubsection {* Proving  @{term "a div (b * c) = (a div b) div c"} *}
  2139 
  2140 (*The condition c>0 seems necessary.  Consider that 7 div ~6 = ~2 but
  2141   7 div 2 div ~3 = 3 div ~3 = ~1.  The subcase (a div b) mod c = 0 seems
  2142   to cause particular problems.*)
  2143 
  2144 text{*first, four lemmas to bound the remainder for the cases b<0 and b>0 *}
  2145 
  2146 lemma zmult2_lemma_aux1: "[| (0::int) < c;  b < r;  r \<le> 0 |] ==> b * c < b * (q mod c) + r"
  2147 apply (subgoal_tac "b * (c - q mod c) < r * 1")
  2148  apply (simp add: algebra_simps)
  2149 apply (rule order_le_less_trans)
  2150  apply (erule_tac [2] mult_strict_right_mono)
  2151  apply (rule mult_left_mono_neg)
  2152   using add1_zle_eq[of "q mod c"]apply(simp add: algebra_simps)
  2153  apply (simp)
  2154 apply (simp)
  2155 done
  2156 
  2157 lemma zmult2_lemma_aux2:
  2158      "[| (0::int) < c;   b < r;  r \<le> 0 |] ==> b * (q mod c) + r \<le> 0"
  2159 apply (subgoal_tac "b * (q mod c) \<le> 0")
  2160  apply arith
  2161 apply (simp add: mult_le_0_iff)
  2162 done
  2163 
  2164 lemma zmult2_lemma_aux3: "[| (0::int) < c;  0 \<le> r;  r < b |] ==> 0 \<le> b * (q mod c) + r"
  2165 apply (subgoal_tac "0 \<le> b * (q mod c) ")
  2166 apply arith
  2167 apply (simp add: zero_le_mult_iff)
  2168 done
  2169 
  2170 lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 \<le> r; r < b |] ==> b * (q mod c) + r < b * c"
  2171 apply (subgoal_tac "r * 1 < b * (c - q mod c) ")
  2172  apply (simp add: right_diff_distrib)
  2173 apply (rule order_less_le_trans)
  2174  apply (erule mult_strict_right_mono)
  2175  apply (rule_tac [2] mult_left_mono)
  2176   apply simp
  2177  using add1_zle_eq[of "q mod c"] apply (simp add: algebra_simps)
  2178 apply simp
  2179 done
  2180 
  2181 lemma zmult2_lemma: "[| divmod_int_rel a b (q, r); 0 < c |]  
  2182       ==> divmod_int_rel a (b * c) (q div c, b*(q mod c) + r)"
  2183 by (auto simp add: mult.assoc divmod_int_rel_def linorder_neq_iff
  2184                    zero_less_mult_iff distrib_left [symmetric] 
  2185                    zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: split_if_asm)
  2186 
  2187 lemma zdiv_zmult2_eq:
  2188   fixes a b c :: int
  2189   shows "0 \<le> c \<Longrightarrow> a div (b * c) = (a div b) div c"
  2190 apply (case_tac "b = 0", simp)
  2191 apply (force simp add: le_less divmod_int_rel_div_mod [THEN zmult2_lemma, THEN div_int_unique])
  2192 done
  2193 
  2194 lemma zmod_zmult2_eq:
  2195   fixes a b c :: int
  2196   shows "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
  2197 apply (case_tac "b = 0", simp)
  2198 apply (force simp add: le_less divmod_int_rel_div_mod [THEN zmult2_lemma, THEN mod_int_unique])
  2199 done
  2200 
  2201 lemma div_pos_geq:
  2202   fixes k l :: int
  2203   assumes "0 < l" and "l \<le> k"
  2204   shows "k div l = (k - l) div l + 1"
  2205 proof -
  2206   have "k = (k - l) + l" by simp
  2207   then obtain j where k: "k = j + l" ..
  2208   with assms show ?thesis by simp
  2209 qed
  2210 
  2211 lemma mod_pos_geq:
  2212   fixes k l :: int
  2213   assumes "0 < l" and "l \<le> k"
  2214   shows "k mod l = (k - l) mod l"
  2215 proof -
  2216   have "k = (k - l) + l" by simp
  2217   then obtain j where k: "k = j + l" ..
  2218   with assms show ?thesis by simp
  2219 qed
  2220 
  2221 
  2222 subsubsection {* Splitting Rules for div and mod *}
  2223 
  2224 text{*The proofs of the two lemmas below are essentially identical*}
  2225 
  2226 lemma split_pos_lemma:
  2227  "0<k ==> 
  2228     P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"
  2229 apply (rule iffI, clarify)
  2230  apply (erule_tac P="P ?x ?y" in rev_mp)  
  2231  apply (subst mod_add_eq) 
  2232  apply (subst zdiv_zadd1_eq) 
  2233  apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)  
  2234 txt{*converse direction*}
  2235 apply (drule_tac x = "n div k" in spec) 
  2236 apply (drule_tac x = "n mod k" in spec, simp)
  2237 done
  2238 
  2239 lemma split_neg_lemma:
  2240  "k<0 ==>
  2241     P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"
  2242 apply (rule iffI, clarify)
  2243  apply (erule_tac P="P ?x ?y" in rev_mp)  
  2244  apply (subst mod_add_eq) 
  2245  apply (subst zdiv_zadd1_eq) 
  2246  apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)  
  2247 txt{*converse direction*}
  2248 apply (drule_tac x = "n div k" in spec) 
  2249 apply (drule_tac x = "n mod k" in spec, simp)
  2250 done
  2251 
  2252 lemma split_zdiv:
  2253  "P(n div k :: int) =
  2254   ((k = 0 --> P 0) & 
  2255    (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i)) & 
  2256    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i)))"
  2257 apply (case_tac "k=0", simp)
  2258 apply (simp only: linorder_neq_iff)
  2259 apply (erule disjE) 
  2260  apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"] 
  2261                       split_neg_lemma [of concl: "%x y. P x"])
  2262 done
  2263 
  2264 lemma split_zmod:
  2265  "P(n mod k :: int) =
  2266   ((k = 0 --> P n) & 
  2267    (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P j)) & 
  2268    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P j)))"
  2269 apply (case_tac "k=0", simp)
  2270 apply (simp only: linorder_neq_iff)
  2271 apply (erule disjE) 
  2272  apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"] 
  2273                       split_neg_lemma [of concl: "%x y. P y"])
  2274 done
  2275 
  2276 text {* Enable (lin)arith to deal with @{const div} and @{const mod}
  2277   when these are applied to some constant that is of the form
  2278   @{term "numeral k"}: *}
  2279 declare split_zdiv [of _ _ "numeral k", arith_split] for k
  2280 declare split_zmod [of _ _ "numeral k", arith_split] for k
  2281 
  2282 
  2283 subsubsection {* Computing @{text "div"} and @{text "mod"} with shifting *}
  2284 
  2285 lemma pos_divmod_int_rel_mult_2:
  2286   assumes "0 \<le> b"
  2287   assumes "divmod_int_rel a b (q, r)"
  2288   shows "divmod_int_rel (1 + 2*a) (2*b) (q, 1 + 2*r)"
  2289   using assms unfolding divmod_int_rel_def by auto
  2290 
  2291 declaration {* K (Lin_Arith.add_simps @{thms uminus_numeral_One}) *}
  2292 
  2293 lemma neg_divmod_int_rel_mult_2:
  2294   assumes "b \<le> 0"
  2295   assumes "divmod_int_rel (a + 1) b (q, r)"
  2296   shows "divmod_int_rel (1 + 2*a) (2*b) (q, 2*r - 1)"
  2297   using assms unfolding divmod_int_rel_def by auto
  2298 
  2299 text{*computing div by shifting *}
  2300 
  2301 lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a"
  2302   using pos_divmod_int_rel_mult_2 [OF _ divmod_int_rel_div_mod]
  2303   by (rule div_int_unique)
  2304 
  2305 lemma neg_zdiv_mult_2: 
  2306   assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"
  2307   using neg_divmod_int_rel_mult_2 [OF A divmod_int_rel_div_mod]
  2308   by (rule div_int_unique)
  2309 
  2310 (* FIXME: add rules for negative numerals *)
  2311 lemma zdiv_numeral_Bit0 [simp]:
  2312   "numeral (Num.Bit0 v) div numeral (Num.Bit0 w) =
  2313     numeral v div (numeral w :: int)"
  2314   unfolding numeral.simps unfolding mult_2 [symmetric]
  2315   by (rule div_mult_mult1, simp)
  2316 
  2317 lemma zdiv_numeral_Bit1 [simp]:
  2318   "numeral (Num.Bit1 v) div numeral (Num.Bit0 w) =  
  2319     (numeral v div (numeral w :: int))"
  2320   unfolding numeral.simps
  2321   unfolding mult_2 [symmetric] add.commute [of _ 1]
  2322   by (rule pos_zdiv_mult_2, simp)
  2323 
  2324 lemma pos_zmod_mult_2:
  2325   fixes a b :: int
  2326   assumes "0 \<le> a"
  2327   shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)"
  2328   using pos_divmod_int_rel_mult_2 [OF assms divmod_int_rel_div_mod]
  2329   by (rule mod_int_unique)
  2330 
  2331 lemma neg_zmod_mult_2:
  2332   fixes a b :: int
  2333   assumes "a \<le> 0"
  2334   shows "(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1"
  2335   using neg_divmod_int_rel_mult_2 [OF assms divmod_int_rel_div_mod]
  2336   by (rule mod_int_unique)
  2337 
  2338 (* FIXME: add rules for negative numerals *)
  2339 lemma zmod_numeral_Bit0 [simp]:
  2340   "numeral (Num.Bit0 v) mod numeral (Num.Bit0 w) =  
  2341     (2::int) * (numeral v mod numeral w)"
  2342   unfolding numeral_Bit0 [of v] numeral_Bit0 [of w]
  2343   unfolding mult_2 [symmetric] by (rule mod_mult_mult1)
  2344 
  2345 lemma zmod_numeral_Bit1 [simp]:
  2346   "numeral (Num.Bit1 v) mod numeral (Num.Bit0 w) =
  2347     2 * (numeral v mod numeral w) + (1::int)"
  2348   unfolding numeral_Bit1 [of v] numeral_Bit0 [of w]
  2349   unfolding mult_2 [symmetric] add.commute [of _ 1]
  2350   by (rule pos_zmod_mult_2, simp)
  2351 
  2352 lemma zdiv_eq_0_iff:
  2353  "(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")
  2354 proof
  2355   assume ?L
  2356   have "?L \<longrightarrow> ?R" by (rule split_zdiv[THEN iffD2]) simp
  2357   with `?L` show ?R by blast
  2358 next
  2359   assume ?R thus ?L
  2360     by(auto simp: div_pos_pos_trivial div_neg_neg_trivial)
  2361 qed
  2362 
  2363 
  2364 subsubsection {* Quotients of Signs *}
  2365 
  2366 lemma div_neg_pos_less0: "[| a < (0::int);  0 < b |] ==> a div b < 0"
  2367 apply (subgoal_tac "a div b \<le> -1", force)
  2368 apply (rule order_trans)
  2369 apply (rule_tac a' = "-1" in zdiv_mono1)
  2370 apply (auto simp add: div_eq_minus1)
  2371 done
  2372 
  2373 lemma div_nonneg_neg_le0: "[| (0::int) \<le> a; b < 0 |] ==> a div b \<le> 0"
  2374 by (drule zdiv_mono1_neg, auto)
  2375 
  2376 lemma div_nonpos_pos_le0: "[| (a::int) \<le> 0; b > 0 |] ==> a div b \<le> 0"
  2377 by (drule zdiv_mono1, auto)
  2378 
  2379 text{* Now for some equivalences of the form @{text"a div b >=< 0 \<longleftrightarrow> \<dots>"}
  2380 conditional upon the sign of @{text a} or @{text b}. There are many more.
  2381 They should all be simp rules unless that causes too much search. *}
  2382 
  2383 lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)"
  2384 apply auto
  2385 apply (drule_tac [2] zdiv_mono1)
  2386 apply (auto simp add: linorder_neq_iff)
  2387 apply (simp (no_asm_use) add: linorder_not_less [symmetric])
  2388 apply (blast intro: div_neg_pos_less0)
  2389 done
  2390 
  2391 lemma neg_imp_zdiv_nonneg_iff:
  2392   "b < (0::int) ==> (0 \<le> a div b) = (a \<le> (0::int))"
  2393 apply (subst div_minus_minus [symmetric])
  2394 apply (subst pos_imp_zdiv_nonneg_iff, auto)
  2395 done
  2396 
  2397 (*But not (a div b \<le> 0 iff a\<le>0); consider a=1, b=2 when a div b = 0.*)
  2398 lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)"
  2399 by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff)
  2400 
  2401 lemma pos_imp_zdiv_pos_iff:
  2402   "0<k \<Longrightarrow> 0 < (i::int) div k \<longleftrightarrow> k \<le> i"
  2403 using pos_imp_zdiv_nonneg_iff[of k i] zdiv_eq_0_iff[of i k]
  2404 by arith
  2405 
  2406 (*Again the law fails for \<le>: consider a = -1, b = -2 when a div b = 0*)
  2407 lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)"
  2408 by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)
  2409 
  2410 lemma nonneg1_imp_zdiv_pos_iff:
  2411   "(0::int) <= a \<Longrightarrow> (a div b > 0) = (a >= b & b>0)"
  2412 apply rule
  2413  apply rule
  2414   using div_pos_pos_trivial[of a b]apply arith
  2415  apply(cases "b=0")apply simp
  2416  using div_nonneg_neg_le0[of a b]apply arith
  2417 using int_one_le_iff_zero_less[of "a div b"] zdiv_mono1[of b a b]apply simp
  2418 done
  2419 
  2420 lemma zmod_le_nonneg_dividend: "(m::int) \<ge> 0 ==> m mod k \<le> m"
  2421 apply (rule split_zmod[THEN iffD2])
  2422 apply(fastforce dest: q_pos_lemma intro: split_mult_pos_le)
  2423 done
  2424 
  2425 
  2426 subsubsection {* The Divides Relation *}
  2427 
  2428 lemma dvd_neg_numeral_left [simp]:
  2429   fixes y :: "'a::comm_ring_1"
  2430   shows "(- numeral k) dvd y \<longleftrightarrow> (numeral k) dvd y"
  2431   by (fact minus_dvd_iff)
  2432 
  2433 lemma dvd_neg_numeral_right [simp]:
  2434   fixes x :: "'a::comm_ring_1"
  2435   shows "x dvd (- numeral k) \<longleftrightarrow> x dvd (numeral k)"
  2436   by (fact dvd_minus_iff)
  2437 
  2438 lemmas dvd_eq_mod_eq_0_numeral [simp] =
  2439   dvd_eq_mod_eq_0 [of "numeral x" "numeral y"] for x y
  2440 
  2441 
  2442 subsubsection {* Further properties *}
  2443 
  2444 lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"
  2445   using zmod_zdiv_equality[where a="m" and b="n"]
  2446   by (simp add: algebra_simps) (* FIXME: generalize *)
  2447 
  2448 lemma zdiv_int: "int (a div b) = (int a) div (int b)"
  2449 apply (subst split_div, auto)
  2450 apply (subst split_zdiv, auto)
  2451 apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in unique_quotient)
  2452 apply (auto simp add: divmod_int_rel_def of_nat_mult)
  2453 done
  2454 
  2455 lemma zmod_int: "int (a mod b) = (int a) mod (int b)"
  2456 apply (subst split_mod, auto)
  2457 apply (subst split_zmod, auto)
  2458 apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia 
  2459        in unique_remainder)
  2460 apply (auto simp add: divmod_int_rel_def of_nat_mult)
  2461 done
  2462 
  2463 lemma abs_div: "(y::int) dvd x \<Longrightarrow> abs (x div y) = abs x div abs y"
  2464 by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
  2465 
  2466 text{*Suggested by Matthias Daum*}
  2467 lemma int_power_div_base:
  2468      "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"
  2469 apply (subgoal_tac "k ^ m = k ^ ((m - Suc 0) + Suc 0)")
  2470  apply (erule ssubst)
  2471  apply (simp only: power_add)
  2472  apply simp_all
  2473 done
  2474 
  2475 text {* by Brian Huffman *}
  2476 lemma zminus_zmod: "- ((x::int) mod m) mod m = - x mod m"
  2477 by (rule mod_minus_eq [symmetric])
  2478 
  2479 lemma zdiff_zmod_left: "(x mod m - y) mod m = (x - y) mod (m::int)"
  2480 by (rule mod_diff_left_eq [symmetric])
  2481 
  2482 lemma zdiff_zmod_right: "(x - y mod m) mod m = (x - y) mod (m::int)"
  2483 by (rule mod_diff_right_eq [symmetric])
  2484 
  2485 lemmas zmod_simps =
  2486   mod_add_left_eq  [symmetric]
  2487   mod_add_right_eq [symmetric]
  2488   mod_mult_right_eq[symmetric]
  2489   mod_mult_left_eq [symmetric]
  2490   power_mod
  2491   zminus_zmod zdiff_zmod_left zdiff_zmod_right
  2492 
  2493 text {* Distributive laws for function @{text nat}. *}
  2494 
  2495 lemma nat_div_distrib: "0 \<le> x \<Longrightarrow> nat (x div y) = nat x div nat y"
  2496 apply (rule linorder_cases [of y 0])
  2497 apply (simp add: div_nonneg_neg_le0)
  2498 apply simp
  2499 apply (simp add: nat_eq_iff pos_imp_zdiv_nonneg_iff zdiv_int)
  2500 done
  2501 
  2502 (*Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't*)
  2503 lemma nat_mod_distrib:
  2504   "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x mod y) = nat x mod nat y"
  2505 apply (case_tac "y = 0", simp)
  2506 apply (simp add: nat_eq_iff zmod_int)
  2507 done
  2508 
  2509 text  {* transfer setup *}
  2510 
  2511 lemma transfer_nat_int_functions:
  2512     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
  2513     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
  2514   by (auto simp add: nat_div_distrib nat_mod_distrib)
  2515 
  2516 lemma transfer_nat_int_function_closures:
  2517     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
  2518     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
  2519   apply (cases "y = 0")
  2520   apply (auto simp add: pos_imp_zdiv_nonneg_iff)
  2521   apply (cases "y = 0")
  2522   apply auto
  2523 done
  2524 
  2525 declare transfer_morphism_nat_int [transfer add return:
  2526   transfer_nat_int_functions
  2527   transfer_nat_int_function_closures
  2528 ]
  2529 
  2530 lemma transfer_int_nat_functions:
  2531     "(int x) div (int y) = int (x div y)"
  2532     "(int x) mod (int y) = int (x mod y)"
  2533   by (auto simp add: zdiv_int zmod_int)
  2534 
  2535 lemma transfer_int_nat_function_closures:
  2536     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
  2537     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
  2538   by (simp_all only: is_nat_def transfer_nat_int_function_closures)
  2539 
  2540 declare transfer_morphism_int_nat [transfer add return:
  2541   transfer_int_nat_functions
  2542   transfer_int_nat_function_closures
  2543 ]
  2544 
  2545 text{*Suggested by Matthias Daum*}
  2546 lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
  2547 apply (subgoal_tac "nat x div nat k < nat x")
  2548  apply (simp add: nat_div_distrib [symmetric])
  2549 apply (rule Divides.div_less_dividend, simp_all)
  2550 done
  2551 
  2552 lemma zmod_eq_dvd_iff: "(x::int) mod n = y mod n \<longleftrightarrow> n dvd x - y"
  2553 proof
  2554   assume H: "x mod n = y mod n"
  2555   hence "x mod n - y mod n = 0" by simp
  2556   hence "(x mod n - y mod n) mod n = 0" by simp 
  2557   hence "(x - y) mod n = 0" by (simp add: mod_diff_eq[symmetric])
  2558   thus "n dvd x - y" by (simp add: dvd_eq_mod_eq_0)
  2559 next
  2560   assume H: "n dvd x - y"
  2561   then obtain k where k: "x-y = n*k" unfolding dvd_def by blast
  2562   hence "x = n*k + y" by simp
  2563   hence "x mod n = (n*k + y) mod n" by simp
  2564   thus "x mod n = y mod n" by (simp add: mod_add_left_eq)
  2565 qed
  2566 
  2567 lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y  mod n" and xy:"y \<le> x"
  2568   shows "\<exists>q. x = y + n * q"
  2569 proof-
  2570   from xy have th: "int x - int y = int (x - y)" by simp 
  2571   from xyn have "int x mod int n = int y mod int n" 
  2572     by (simp add: zmod_int [symmetric])
  2573   hence "int n dvd int x - int y" by (simp only: zmod_eq_dvd_iff[symmetric]) 
  2574   hence "n dvd x - y" by (simp add: th zdvd_int)
  2575   then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith
  2576 qed
  2577 
  2578 lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)" 
  2579   (is "?lhs = ?rhs")
  2580 proof
  2581   assume H: "x mod n = y mod n"
  2582   {assume xy: "x \<le> y"
  2583     from H have th: "y mod n = x mod n" by simp
  2584     from nat_mod_eq_lemma[OF th xy] have ?rhs 
  2585       apply clarify  apply (rule_tac x="q" in exI) by (rule exI[where x="0"], simp)}
  2586   moreover
  2587   {assume xy: "y \<le> x"
  2588     from nat_mod_eq_lemma[OF H xy] have ?rhs 
  2589       apply clarify  apply (rule_tac x="0" in exI) by (rule_tac x="q" in exI, simp)}
  2590   ultimately  show ?rhs using linear[of x y] by blast  
  2591 next
  2592   assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast
  2593   hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp
  2594   thus  ?lhs by simp
  2595 qed
  2596 
  2597 text {*
  2598   This re-embedding of natural division on integers goes back to the
  2599   time when numerals had been signed numerals.  It should
  2600   now be replaced by the algorithm developed in @{class semiring_numeral_div}.  
  2601 *}
  2602 
  2603 lemma div_nat_numeral [simp]:
  2604   "(numeral v :: nat) div numeral v' = nat (numeral v div numeral v')"
  2605   by (simp add: nat_div_distrib)
  2606 
  2607 lemma one_div_nat_numeral [simp]:
  2608   "Suc 0 div numeral v' = nat (1 div numeral v')"
  2609   by (subst nat_div_distrib, simp_all)
  2610 
  2611 lemma mod_nat_numeral [simp]:
  2612   "(numeral v :: nat) mod numeral v' = nat (numeral v mod numeral v')"
  2613   by (simp add: nat_mod_distrib)
  2614 
  2615 lemma one_mod_nat_numeral [simp]:
  2616   "Suc 0 mod numeral v' = nat (1 mod numeral v')"
  2617   by (subst nat_mod_distrib) simp_all
  2618 
  2619 instance int :: semiring_numeral_div
  2620   by intro_classes (auto intro: zmod_le_nonneg_dividend
  2621     simp add: zmult_div_cancel
  2622     pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial
  2623     zmod_zmult2_eq zdiv_zmult2_eq)
  2624 
  2625 
  2626 subsubsection {* Tools setup *}
  2627 
  2628 text {* Nitpick *}
  2629 
  2630 lemmas [nitpick_unfold] = dvd_eq_mod_eq_0 mod_div_equality' zmod_zdiv_equality'
  2631 
  2632 
  2633 subsubsection {* Code generation *}
  2634 
  2635 definition divmod_abs :: "int \<Rightarrow> int \<Rightarrow> int \<times> int"
  2636 where
  2637   "divmod_abs k l = (\<bar>k\<bar> div \<bar>l\<bar>, \<bar>k\<bar> mod \<bar>l\<bar>)"
  2638 
  2639 lemma fst_divmod_abs [simp]:
  2640   "fst (divmod_abs k l) = \<bar>k\<bar> div \<bar>l\<bar>"
  2641   by (simp add: divmod_abs_def)
  2642 
  2643 lemma snd_divmod_abs [simp]:
  2644   "snd (divmod_abs k l) = \<bar>k\<bar> mod \<bar>l\<bar>"
  2645   by (simp add: divmod_abs_def)
  2646 
  2647 lemma divmod_abs_code [code]:
  2648   "divmod_abs (Int.Pos k) (Int.Pos l) = divmod k l"
  2649   "divmod_abs (Int.Neg k) (Int.Neg l) = divmod k l"
  2650   "divmod_abs (Int.Neg k) (Int.Pos l) = divmod k l"
  2651   "divmod_abs (Int.Pos k) (Int.Neg l) = divmod k l"
  2652   "divmod_abs j 0 = (0, \<bar>j\<bar>)"
  2653   "divmod_abs 0 j = (0, 0)"
  2654   by (simp_all add: prod_eq_iff)
  2655 
  2656 lemma divmod_int_divmod_abs:
  2657   "divmod_int k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
  2658   apsnd ((op *) (sgn l)) (if 0 < l \<and> 0 \<le> k \<or> l < 0 \<and> k < 0
  2659     then divmod_abs k l
  2660     else (let (r, s) = divmod_abs k l in
  2661        if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
  2662 proof -
  2663   have aux: "\<And>q::int. - k = l * q \<longleftrightarrow> k = l * - q" by auto
  2664   show ?thesis
  2665     by (simp add: prod_eq_iff split_def Let_def)
  2666       (auto simp add: aux not_less not_le zdiv_zminus1_eq_if
  2667       zmod_zminus1_eq_if zdiv_zminus2_eq_if zmod_zminus2_eq_if)
  2668 qed
  2669 
  2670 lemma divmod_int_code [code]:
  2671   "divmod_int k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
  2672   apsnd ((op *) (sgn l)) (if sgn k = sgn l
  2673     then divmod_abs k l
  2674     else (let (r, s) = divmod_abs k l in
  2675       if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
  2676 proof -
  2677   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"
  2678     by (auto simp add: not_less sgn_if)
  2679   then show ?thesis by (simp add: divmod_int_divmod_abs)
  2680 qed
  2681 
  2682 hide_const (open) divmod_abs
  2683 
  2684 code_identifier
  2685   code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  2686 
  2687 end
  2688