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