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