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