src/HOL/Divides.thy
 author haftmann Sun Sep 21 16:56:11 2014 +0200 (2014-09-21) changeset 58410 6d46ad54a2ab parent 57514 bdc2c6b40bf2 child 58511 97aec08d6f28 permissions -rw-r--r--
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
     1 (*  Title:      HOL/Divides.thy

     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

     3     Copyright   1999  University of Cambridge

     4 *)

     5

     6 header {* The division operators div and mod *}

     7

     8 theory Divides

     9 imports Nat_Transfer

    10 begin

    11

    12 subsection {* Syntactic division operations *}

    13

    14 class div = dvd +

    15   fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70)

    16     and mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70)

    17

    18

    19 subsection {* Abstract division in commutative semirings. *}

    20

    21 class semiring_div = comm_semiring_1_cancel + no_zero_divisors + div +

    22   assumes mod_div_equality: "a div b * b + a mod b = a"

    23     and div_by_0 [simp]: "a div 0 = 0"

    24     and div_0 [simp]: "0 div a = 0"

    25     and div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"

    26     and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"

    27 begin

    28

    29 text {* @{const div} and @{const mod} *}

    30

    31 lemma mod_div_equality2: "b * (a div b) + a mod b = a"

    32   unfolding mult.commute [of b]

    33   by (rule mod_div_equality)

    34

    35 lemma mod_div_equality': "a mod b + a div b * b = a"

    36   using mod_div_equality [of a b]

    37   by (simp only: ac_simps)

    38

    39 lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c"

    40   by (simp add: mod_div_equality)

    41

    42 lemma div_mod_equality2: "(b * (a div b) + a mod b) + c = a + c"

    43   by (simp add: mod_div_equality2)

    44

    45 lemma mod_by_0 [simp]: "a mod 0 = a"

    46   using mod_div_equality [of a zero] by simp

    47

    48 lemma mod_0 [simp]: "0 mod a = 0"

    49   using mod_div_equality [of zero a] div_0 by simp

    50

    51 lemma div_mult_self2 [simp]:

    52   assumes "b \<noteq> 0"

    53   shows "(a + b * c) div b = c + a div b"

    54   using assms div_mult_self1 [of b a c] by (simp add: mult.commute)

    55

    56 lemma div_mult_self3 [simp]:

    57   assumes "b \<noteq> 0"

    58   shows "(c * b + a) div b = c + a div b"

    59   using assms by (simp add: add.commute)

    60

    61 lemma div_mult_self4 [simp]:

    62   assumes "b \<noteq> 0"

    63   shows "(b * c + a) div b = c + a div b"

    64   using assms by (simp add: add.commute)

    65

    66 lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b"

    67 proof (cases "b = 0")

    68   case True then show ?thesis by simp

    69 next

    70   case False

    71   have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b"

    72     by (simp add: mod_div_equality)

    73   also from False div_mult_self1 [of b a c] have

    74     "\<dots> = (c + a div b) * b + (a + c * b) mod b"

    75       by (simp add: algebra_simps)

    76   finally have "a = a div b * b + (a + c * b) mod b"

    77     by (simp add: add.commute [of a] add.assoc distrib_right)

    78   then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"

    79     by (simp add: mod_div_equality)

    80   then show ?thesis by simp

    81 qed

    82

    83 lemma mod_mult_self2 [simp]:

    84   "(a + b * c) mod b = a mod b"

    85   by (simp add: mult.commute [of b])

    86

    87 lemma mod_mult_self3 [simp]:

    88   "(c * b + a) mod b = a mod b"

    89   by (simp add: add.commute)

    90

    91 lemma mod_mult_self4 [simp]:

    92   "(b * c + a) mod b = a mod b"

    93   by (simp add: add.commute)

    94

    95 lemma div_mult_self1_is_id [simp]: "b \<noteq> 0 \<Longrightarrow> b * a div b = a"

    96   using div_mult_self2 [of b 0 a] by simp

    97

    98 lemma div_mult_self2_is_id [simp]: "b \<noteq> 0 \<Longrightarrow> a * b div b = a"

    99   using div_mult_self1 [of b 0 a] by simp

   100

   101 lemma mod_mult_self1_is_0 [simp]: "b * a mod b = 0"

   102   using mod_mult_self2 [of 0 b a] by simp

   103

   104 lemma mod_mult_self2_is_0 [simp]: "a * b mod b = 0"

   105   using mod_mult_self1 [of 0 a b] by simp

   106

   107 lemma div_by_1 [simp]: "a div 1 = a"

   108   using div_mult_self2_is_id [of 1 a] zero_neq_one by simp

   109

   110 lemma mod_by_1 [simp]: "a mod 1 = 0"

   111 proof -

   112   from mod_div_equality [of a one] div_by_1 have "a + a mod 1 = a" by simp

   113   then have "a + a mod 1 = a + 0" by simp

   114   then show ?thesis by (rule add_left_imp_eq)

   115 qed

   116

   117 lemma mod_self [simp]: "a mod a = 0"

   118   using mod_mult_self2_is_0 [of 1] by simp

   119

   120 lemma div_self [simp]: "a \<noteq> 0 \<Longrightarrow> a div a = 1"

   121   using div_mult_self2_is_id [of _ 1] by simp

   122

   123 lemma div_add_self1 [simp]:

   124   assumes "b \<noteq> 0"

   125   shows "(b + a) div b = a div b + 1"

   126   using assms div_mult_self1 [of b a 1] by (simp add: add.commute)

   127

   128 lemma div_add_self2 [simp]:

   129   assumes "b \<noteq> 0"

   130   shows "(a + b) div b = a div b + 1"

   131   using assms div_add_self1 [of b a] by (simp add: add.commute)

   132

   133 lemma mod_add_self1 [simp]:

   134   "(b + a) mod b = a mod b"

   135   using mod_mult_self1 [of a 1 b] by (simp add: add.commute)

   136

   137 lemma mod_add_self2 [simp]:

   138   "(a + b) mod b = a mod b"

   139   using mod_mult_self1 [of a 1 b] by simp

   140

   141 lemma mod_div_decomp:

   142   fixes a b

   143   obtains q r where "q = a div b" and "r = a mod b"

   144     and "a = q * b + r"

   145 proof -

   146   from mod_div_equality have "a = a div b * b + a mod b" by simp

   147   moreover have "a div b = a div b" ..

   148   moreover have "a mod b = a mod b" ..

   149   note that ultimately show thesis by blast

   150 qed

   151

   152 lemma dvd_eq_mod_eq_0 [code]: "a dvd b \<longleftrightarrow> b mod a = 0"

   153 proof

   154   assume "b mod a = 0"

   155   with mod_div_equality [of b a] have "b div a * a = b" by simp

   156   then have "b = a * (b div a)" unfolding mult.commute ..

   157   then have "\<exists>c. b = a * c" ..

   158   then show "a dvd b" unfolding dvd_def .

   159 next

   160   assume "a dvd b"

   161   then have "\<exists>c. b = a * c" unfolding dvd_def .

   162   then obtain c where "b = a * c" ..

   163   then have "b mod a = a * c mod a" by simp

   164   then have "b mod a = c * a mod a" by (simp add: mult.commute)

   165   then show "b mod a = 0" by simp

   166 qed

   167

   168 lemma mod_div_trivial [simp]: "a mod b div b = 0"

   169 proof (cases "b = 0")

   170   assume "b = 0"

   171   thus ?thesis by simp

   172 next

   173   assume "b \<noteq> 0"

   174   hence "a div b + a mod b div b = (a mod b + a div b * b) div b"

   175     by (rule div_mult_self1 [symmetric])

   176   also have "\<dots> = a div b"

   177     by (simp only: mod_div_equality')

   178   also have "\<dots> = a div b + 0"

   179     by simp

   180   finally show ?thesis

   181     by (rule add_left_imp_eq)

   182 qed

   183

   184 lemma mod_mod_trivial [simp]: "a mod b mod b = a mod b"

   185 proof -

   186   have "a mod b mod b = (a mod b + a div b * b) mod b"

   187     by (simp only: mod_mult_self1)

   188   also have "\<dots> = a mod b"

   189     by (simp only: mod_div_equality')

   190   finally show ?thesis .

   191 qed

   192

   193 lemma dvd_imp_mod_0: "a dvd b \<Longrightarrow> b mod a = 0"

   194 by (rule dvd_eq_mod_eq_0[THEN iffD1])

   195

   196 lemma dvd_div_mult_self: "a dvd b \<Longrightarrow> (b div a) * a = b"

   197 by (subst (2) mod_div_equality [of b a, symmetric]) (simp add:dvd_imp_mod_0)

   198

   199 lemma dvd_mult_div_cancel: "a dvd b \<Longrightarrow> a * (b div a) = b"

   200 by (drule dvd_div_mult_self) (simp add: mult.commute)

   201

   202 lemma dvd_div_mult: "a dvd b \<Longrightarrow> (b div a) * c = b * c div a"

   203 apply (cases "a = 0")

   204  apply simp

   205 apply (auto simp: dvd_def mult.assoc)

   206 done

   207

   208 lemma div_dvd_div[simp]:

   209   "a dvd b \<Longrightarrow> a dvd c \<Longrightarrow> (b div a dvd c div a) = (b dvd c)"

   210 apply (cases "a = 0")

   211  apply simp

   212 apply (unfold dvd_def)

   213 apply auto

   214  apply(blast intro:mult.assoc[symmetric])

   215 apply(fastforce simp add: mult.assoc)

   216 done

   217

   218 lemma dvd_mod_imp_dvd: "[| k dvd m mod n;  k dvd n |] ==> k dvd m"

   219   apply (subgoal_tac "k dvd (m div n) *n + m mod n")

   220    apply (simp add: mod_div_equality)

   221   apply (simp only: dvd_add dvd_mult)

   222   done

   223

   224 text {* Addition respects modular equivalence. *}

   225

   226 lemma mod_add_left_eq: "(a + b) mod c = (a mod c + b) mod c"

   227 proof -

   228   have "(a + b) mod c = (a div c * c + a mod c + b) mod c"

   229     by (simp only: mod_div_equality)

   230   also have "\<dots> = (a mod c + b + a div c * c) mod c"

   231     by (simp only: ac_simps)

   232   also have "\<dots> = (a mod c + b) mod c"

   233     by (rule mod_mult_self1)

   234   finally show ?thesis .

   235 qed

   236

   237 lemma mod_add_right_eq: "(a + b) mod c = (a + b mod c) mod c"

   238 proof -

   239   have "(a + b) mod c = (a + (b div c * c + b mod c)) mod c"

   240     by (simp only: mod_div_equality)

   241   also have "\<dots> = (a + b mod c + b div c * c) mod c"

   242     by (simp only: ac_simps)

   243   also have "\<dots> = (a + b mod c) mod c"

   244     by (rule mod_mult_self1)

   245   finally show ?thesis .

   246 qed

   247

   248 lemma mod_add_eq: "(a + b) mod c = (a mod c + b mod c) mod c"

   249 by (rule trans [OF mod_add_left_eq mod_add_right_eq])

   250

   251 lemma mod_add_cong:

   252   assumes "a mod c = a' mod c"

   253   assumes "b mod c = b' mod c"

   254   shows "(a + b) mod c = (a' + b') mod c"

   255 proof -

   256   have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"

   257     unfolding assms ..

   258   thus ?thesis

   259     by (simp only: mod_add_eq [symmetric])

   260 qed

   261

   262 lemma div_add [simp]: "z dvd x \<Longrightarrow> z dvd y

   263   \<Longrightarrow> (x + y) div z = x div z + y div z"

   264 by (cases "z = 0", simp, unfold dvd_def, auto simp add: algebra_simps)

   265

   266 text {* Multiplication respects modular equivalence. *}

   267

   268 lemma mod_mult_left_eq: "(a * b) mod c = ((a mod c) * b) mod c"

   269 proof -

   270   have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"

   271     by (simp only: mod_div_equality)

   272   also have "\<dots> = (a mod c * b + a div c * b * c) mod c"

   273     by (simp only: algebra_simps)

   274   also have "\<dots> = (a mod c * b) mod c"

   275     by (rule mod_mult_self1)

   276   finally show ?thesis .

   277 qed

   278

   279 lemma mod_mult_right_eq: "(a * b) mod c = (a * (b mod c)) mod c"

   280 proof -

   281   have "(a * b) mod c = (a * (b div c * c + b mod c)) mod c"

   282     by (simp only: mod_div_equality)

   283   also have "\<dots> = (a * (b mod c) + a * (b div c) * c) mod c"

   284     by (simp only: algebra_simps)

   285   also have "\<dots> = (a * (b mod c)) mod c"

   286     by (rule mod_mult_self1)

   287   finally show ?thesis .

   288 qed

   289

   290 lemma mod_mult_eq: "(a * b) mod c = ((a mod c) * (b mod c)) mod c"

   291 by (rule trans [OF mod_mult_left_eq mod_mult_right_eq])

   292

   293 lemma mod_mult_cong:

   294   assumes "a mod c = a' mod c"

   295   assumes "b mod c = b' mod c"

   296   shows "(a * b) mod c = (a' * b') mod c"

   297 proof -

   298   have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"

   299     unfolding assms ..

   300   thus ?thesis

   301     by (simp only: mod_mult_eq [symmetric])

   302 qed

   303

   304 text {* Exponentiation respects modular equivalence. *}

   305

   306 lemma power_mod: "(a mod b)^n mod b = a^n mod b"

   307 apply (induct n, simp_all)

   308 apply (rule mod_mult_right_eq [THEN trans])

   309 apply (simp (no_asm_simp))

   310 apply (rule mod_mult_eq [symmetric])

   311 done

   312

   313 lemma mod_mod_cancel:

   314   assumes "c dvd b"

   315   shows "a mod b mod c = a mod c"

   316 proof -

   317   from c dvd b obtain k where "b = c * k"

   318     by (rule dvdE)

   319   have "a mod b mod c = a mod (c * k) mod c"

   320     by (simp only: b = c * k)

   321   also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"

   322     by (simp only: mod_mult_self1)

   323   also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"

   324     by (simp only: ac_simps ac_simps)

   325   also have "\<dots> = a mod c"

   326     by (simp only: mod_div_equality)

   327   finally show ?thesis .

   328 qed

   329

   330 lemma div_mult_div_if_dvd:

   331   "y dvd x \<Longrightarrow> z dvd w \<Longrightarrow> (x div y) * (w div z) = (x * w) div (y * z)"

   332   apply (cases "y = 0", simp)

   333   apply (cases "z = 0", simp)

   334   apply (auto elim!: dvdE simp add: algebra_simps)

   335   apply (subst mult.assoc [symmetric])

   336   apply (simp add: no_zero_divisors)

   337   done

   338

   339 lemma div_mult_swap:

   340   assumes "c dvd b"

   341   shows "a * (b div c) = (a * b) div c"

   342 proof -

   343   from assms have "b div c * (a div 1) = b * a div (c * 1)"

   344     by (simp only: div_mult_div_if_dvd one_dvd)

   345   then show ?thesis by (simp add: mult.commute)

   346 qed

   347

   348 lemma div_mult_mult2 [simp]:

   349   "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"

   350   by (drule div_mult_mult1) (simp add: mult.commute)

   351

   352 lemma div_mult_mult1_if [simp]:

   353   "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"

   354   by simp_all

   355

   356 lemma mod_mult_mult1:

   357   "(c * a) mod (c * b) = c * (a mod b)"

   358 proof (cases "c = 0")

   359   case True then show ?thesis by simp

   360 next

   361   case False

   362   from mod_div_equality

   363   have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .

   364   with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)

   365     = c * a + c * (a mod b)" by (simp add: algebra_simps)

   366   with mod_div_equality show ?thesis by simp

   367 qed

   368

   369 lemma mod_mult_mult2:

   370   "(a * c) mod (b * c) = (a mod b) * c"

   371   using mod_mult_mult1 [of c a b] by (simp add: mult.commute)

   372

   373 lemma mult_mod_left: "(a mod b) * c = (a * c) mod (b * c)"

   374   by (fact mod_mult_mult2 [symmetric])

   375

   376 lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)"

   377   by (fact mod_mult_mult1 [symmetric])

   378

   379 lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"

   380   unfolding dvd_def by (auto simp add: mod_mult_mult1)

   381

   382 lemma dvd_mod_iff: "k dvd n \<Longrightarrow> k dvd (m mod n) \<longleftrightarrow> k dvd m"

   383 by (blast intro: dvd_mod_imp_dvd dvd_mod)

   384

   385 lemma div_power:

   386   "y dvd x \<Longrightarrow> (x div y) ^ n = x ^ n div y ^ n"

   387 apply (induct n)

   388  apply simp

   389 apply(simp add: div_mult_div_if_dvd dvd_power_same)

   390 done

   391

   392 lemma dvd_div_eq_mult:

   393   assumes "a \<noteq> 0" and "a dvd b"

   394   shows "b div a = c \<longleftrightarrow> b = c * a"

   395 proof

   396   assume "b = c * a"

   397   then show "b div a = c" by (simp add: assms)

   398 next

   399   assume "b div a = c"

   400   then have "b div a * a = c * a" by simp

   401   moreover from a dvd b have "b div a * a = b" by (simp add: dvd_div_mult_self)

   402   ultimately show "b = c * a" by simp

   403 qed

   404

   405 lemma dvd_div_div_eq_mult:

   406   assumes "a \<noteq> 0" "c \<noteq> 0" and "a dvd b" "c dvd d"

   407   shows "b div a = d div c \<longleftrightarrow> b * c = a * d"

   408   using assms by (auto simp add: mult.commute [of _ a] dvd_div_mult_self dvd_div_eq_mult div_mult_swap intro: sym)

   409

   410 end

   411

   412 class ring_div = semiring_div + comm_ring_1

   413 begin

   414

   415 subclass ring_1_no_zero_divisors ..

   416

   417 text {* Negation respects modular equivalence. *}

   418

   419 lemma mod_minus_eq: "(- a) mod b = (- (a mod b)) mod b"

   420 proof -

   421   have "(- a) mod b = (- (a div b * b + a mod b)) mod b"

   422     by (simp only: mod_div_equality)

   423   also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"

   424     by (simp add: ac_simps)

   425   also have "\<dots> = (- (a mod b)) mod b"

   426     by (rule mod_mult_self1)

   427   finally show ?thesis .

   428 qed

   429

   430 lemma mod_minus_cong:

   431   assumes "a mod b = a' mod b"

   432   shows "(- a) mod b = (- a') mod b"

   433 proof -

   434   have "(- (a mod b)) mod b = (- (a' mod b)) mod b"

   435     unfolding assms ..

   436   thus ?thesis

   437     by (simp only: mod_minus_eq [symmetric])

   438 qed

   439

   440 text {* Subtraction respects modular equivalence. *}

   441

   442 lemma mod_diff_left_eq:

   443   "(a - b) mod c = (a mod c - b) mod c"

   444   using mod_add_cong [of a c "a mod c" "- b" "- b"] by simp

   445

   446 lemma mod_diff_right_eq:

   447   "(a - b) mod c = (a - b mod c) mod c"

   448   using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b] by simp

   449

   450 lemma mod_diff_eq:

   451   "(a - b) mod c = (a mod c - b mod c) mod c"

   452   using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b] by simp

   453

   454 lemma mod_diff_cong:

   455   assumes "a mod c = a' mod c"

   456   assumes "b mod c = b' mod c"

   457   shows "(a - b) mod c = (a' - b') mod c"

   458   using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"] by simp

   459

   460 lemma dvd_neg_div: "y dvd x \<Longrightarrow> -x div y = - (x div y)"

   461 apply (case_tac "y = 0") apply simp

   462 apply (auto simp add: dvd_def)

   463 apply (subgoal_tac "-(y * k) = y * - k")

   464  apply (simp only:)

   465  apply (erule div_mult_self1_is_id)

   466 apply simp

   467 done

   468

   469 lemma dvd_div_neg: "y dvd x \<Longrightarrow> x div -y = - (x div y)"

   470 apply (case_tac "y = 0") apply simp

   471 apply (auto simp add: dvd_def)

   472 apply (subgoal_tac "y * k = -y * -k")

   473  apply (erule ssubst, rule div_mult_self1_is_id)

   474  apply simp

   475 apply simp

   476 done

   477

   478 lemma div_minus_minus [simp]: "(-a) div (-b) = a div b"

   479   using div_mult_mult1 [of "- 1" a b]

   480   unfolding neg_equal_0_iff_equal by simp

   481

   482 lemma mod_minus_minus [simp]: "(-a) mod (-b) = - (a mod b)"

   483   using mod_mult_mult1 [of "- 1" a b] by simp

   484

   485 lemma div_minus_right: "a div (-b) = (-a) div b"

   486   using div_minus_minus [of "-a" b] by simp

   487

   488 lemma mod_minus_right: "a mod (-b) = - ((-a) mod b)"

   489   using mod_minus_minus [of "-a" b] by simp

   490

   491 lemma div_minus1_right [simp]: "a div (-1) = -a"

   492   using div_minus_right [of a 1] by simp

   493

   494 lemma mod_minus1_right [simp]: "a mod (-1) = 0"

   495   using mod_minus_right [of a 1] by simp

   496

   497 lemma minus_mod_self2 [simp]:

   498   "(a - b) mod b = a mod b"

   499   by (simp add: mod_diff_right_eq)

   500

   501 lemma minus_mod_self1 [simp]:

   502   "(b - a) mod b = - a mod b"

   503   using mod_add_self2 [of "- a" b] by simp

   504

   505 end

   506

   507 class semiring_div_parity = semiring_div + semiring_numeral +

   508   assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"

   509 begin

   510

   511 lemma parity_cases [case_names even odd]:

   512   assumes "a mod 2 = 0 \<Longrightarrow> P"

   513   assumes "a mod 2 = 1 \<Longrightarrow> P"

   514   shows P

   515   using assms parity by blast

   516

   517 lemma not_mod_2_eq_0_eq_1 [simp]:

   518   "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"

   519   by (cases a rule: parity_cases) simp_all

   520

   521 lemma not_mod_2_eq_1_eq_0 [simp]:

   522   "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"

   523   by (cases a rule: parity_cases) simp_all

   524

   525 end

   526

   527

   528 subsection {* Generic numeral division with a pragmatic type class *}

   529

   530 text {*

   531   The following type class contains everything necessary to formulate

   532   a division algorithm in ring structures with numerals, restricted

   533   to its positive segments.  This is its primary motiviation, and it

   534   could surely be formulated using a more fine-grained, more algebraic

   535   and less technical class hierarchy.

   536 *}

   537

   538 class semiring_numeral_div = linordered_semidom + minus + semiring_div +

   539   assumes diff_invert_add1: "a + b = c \<Longrightarrow> a = c - b"

   540     and le_add_diff_inverse2: "b \<le> a \<Longrightarrow> a - b + b = a"

   541   assumes mult_div_cancel: "b * (a div b) = a - a mod b"

   542     and div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"

   543     and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"

   544     and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"

   545     and mod_less_eq_dividend: "0 \<le> a \<Longrightarrow> a mod b \<le> a"

   546     and pos_mod_bound: "0 < b \<Longrightarrow> a mod b < b"

   547     and pos_mod_sign: "0 < b \<Longrightarrow> 0 \<le> a mod b"

   548     and mod_mult2_eq: "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"

   549     and div_mult2_eq: "0 \<le> c \<Longrightarrow> a div (b * c) = a div b div c"

   550   assumes discrete: "a < b \<longleftrightarrow> a + 1 \<le> b"

   551 begin

   552

   553 lemma diff_zero [simp]:

   554   "a - 0 = a"

   555   by (rule diff_invert_add1 [symmetric]) simp

   556

   557 subclass semiring_div_parity

   558 proof

   559   fix a

   560   show "a mod 2 = 0 \<or> a mod 2 = 1"

   561   proof (rule ccontr)

   562     assume "\<not> (a mod 2 = 0 \<or> a mod 2 = 1)"

   563     then have "a mod 2 \<noteq> 0" and "a mod 2 \<noteq> 1" by simp_all

   564     have "0 < 2" by simp

   565     with pos_mod_bound pos_mod_sign have "0 \<le> a mod 2" "a mod 2 < 2" by simp_all

   566     with a mod 2 \<noteq> 0 have "0 < a mod 2" by simp

   567     with discrete have "1 \<le> a mod 2" by simp

   568     with a mod 2 \<noteq> 1 have "1 < a mod 2" by simp

   569     with discrete have "2 \<le> a mod 2" by simp

   570     with a mod 2 < 2 show False by simp

   571   qed

   572 qed

   573

   574 lemma divmod_digit_1:

   575   assumes "0 \<le> a" "0 < b" and "b \<le> a mod (2 * b)"

   576   shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P")

   577     and "a mod (2 * b) - b = a mod b" (is "?Q")

   578 proof -

   579   from assms mod_less_eq_dividend [of a "2 * b"] have "b \<le> a"

   580     by (auto intro: trans)

   581   with 0 < b have "0 < a div b" by (auto intro: div_positive)

   582   then have [simp]: "1 \<le> a div b" by (simp add: discrete)

   583   with 0 < b have mod_less: "a mod b < b" by (simp add: pos_mod_bound)

   584   def w \<equiv> "a div b mod 2" with parity have w_exhaust: "w = 0 \<or> w = 1" by auto

   585   have mod_w: "a mod (2 * b) = a mod b + b * w"

   586     by (simp add: w_def mod_mult2_eq ac_simps)

   587   from assms w_exhaust have "w = 1"

   588     by (auto simp add: mod_w) (insert mod_less, auto)

   589   with mod_w have mod: "a mod (2 * b) = a mod b + b" by simp

   590   have "2 * (a div (2 * b)) = a div b - w"

   591     by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)

   592   with w = 1 have div: "2 * (a div (2 * b)) = a div b - 1" by simp

   593   then show ?P and ?Q

   594     by (simp_all add: div mod diff_invert_add1 [symmetric] le_add_diff_inverse2)

   595 qed

   596

   597 lemma divmod_digit_0:

   598   assumes "0 < b" and "a mod (2 * b) < b"

   599   shows "2 * (a div (2 * b)) = a div b" (is "?P")

   600     and "a mod (2 * b) = a mod b" (is "?Q")

   601 proof -

   602   def w \<equiv> "a div b mod 2" with parity have w_exhaust: "w = 0 \<or> w = 1" by auto

   603   have mod_w: "a mod (2 * b) = a mod b + b * w"

   604     by (simp add: w_def mod_mult2_eq ac_simps)

   605   moreover have "b \<le> a mod b + b"

   606   proof -

   607     from 0 < b pos_mod_sign have "0 \<le> a mod b" by blast

   608     then have "0 + b \<le> a mod b + b" by (rule add_right_mono)

   609     then show ?thesis by simp

   610   qed

   611   moreover note assms w_exhaust

   612   ultimately have "w = 0" by auto

   613   with mod_w have mod: "a mod (2 * b) = a mod b" by simp

   614   have "2 * (a div (2 * b)) = a div b - w"

   615     by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)

   616   with w = 0 have div: "2 * (a div (2 * b)) = a div b" by simp

   617   then show ?P and ?Q

   618     by (simp_all add: div mod)

   619 qed

   620

   621 definition divmod :: "num \<Rightarrow> num \<Rightarrow> 'a \<times> 'a"

   622 where

   623   "divmod m n = (numeral m div numeral n, numeral m mod numeral n)"

   624

   625 lemma fst_divmod [simp]:

   626   "fst (divmod m n) = numeral m div numeral n"

   627   by (simp add: divmod_def)

   628

   629 lemma snd_divmod [simp]:

   630   "snd (divmod m n) = numeral m mod numeral n"

   631   by (simp add: divmod_def)

   632

   633 definition divmod_step :: "num \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a"

   634 where

   635   "divmod_step l qr = (let (q, r) = qr

   636     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)

   637     else (2 * q, r))"

   638

   639 text {*

   640   This is a formulation of one step (referring to one digit position)

   641   in school-method division: compare the dividend at the current

   642   digit position with the remainder from previous division steps

   643   and evaluate accordingly.

   644 *}

   645

   646 lemma divmod_step_eq [code]:

   647   "divmod_step l (q, r) = (if numeral l \<le> r

   648     then (2 * q + 1, r - numeral l) else (2 * q, r))"

   649   by (simp add: divmod_step_def)

   650

   651 lemma divmod_step_simps [simp]:

   652   "r < numeral l \<Longrightarrow> divmod_step l (q, r) = (2 * q, r)"

   653   "numeral l \<le> r \<Longrightarrow> divmod_step l (q, r) = (2 * q + 1, r - numeral l)"

   654   by (auto simp add: divmod_step_eq not_le)

   655

   656 text {*

   657   This is a formulation of school-method division.

   658   If the divisor is smaller than the dividend, terminate.

   659   If not, shift the dividend to the right until termination

   660   occurs and then reiterate single division steps in the

   661   opposite direction.

   662 *}

   663

   664 lemma divmod_divmod_step [code]:

   665   "divmod m n = (if m < n then (0, numeral m)

   666     else divmod_step n (divmod m (Num.Bit0 n)))"

   667 proof (cases "m < n")

   668   case True then have "numeral m < numeral n" by simp

   669   then show ?thesis

   670     by (simp add: prod_eq_iff div_less mod_less)

   671 next

   672   case False

   673   have "divmod m n =

   674     divmod_step n (numeral m div (2 * numeral n),

   675       numeral m mod (2 * numeral n))"

   676   proof (cases "numeral n \<le> numeral m mod (2 * numeral n)")

   677     case True

   678     with divmod_step_simps

   679       have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =

   680         (2 * (numeral m div (2 * numeral n)) + 1, numeral m mod (2 * numeral n) - numeral n)"

   681         by blast

   682     moreover from True divmod_digit_1 [of "numeral m" "numeral n"]

   683       have "2 * (numeral m div (2 * numeral n)) + 1 = numeral m div numeral n"

   684       and "numeral m mod (2 * numeral n) - numeral n = numeral m mod numeral n"

   685       by simp_all

   686     ultimately show ?thesis by (simp only: divmod_def)

   687   next

   688     case False then have *: "numeral m mod (2 * numeral n) < numeral n"

   689       by (simp add: not_le)

   690     with divmod_step_simps

   691       have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =

   692         (2 * (numeral m div (2 * numeral n)), numeral m mod (2 * numeral n))"

   693         by blast

   694     moreover from * divmod_digit_0 [of "numeral n" "numeral m"]

   695       have "2 * (numeral m div (2 * numeral n)) = numeral m div numeral n"

   696       and "numeral m mod (2 * numeral n) = numeral m mod numeral n"

   697       by (simp_all only: zero_less_numeral)

   698     ultimately show ?thesis by (simp only: divmod_def)

   699   qed

   700   then have "divmod m n =

   701     divmod_step n (numeral m div numeral (Num.Bit0 n),

   702       numeral m mod numeral (Num.Bit0 n))"

   703     by (simp only: numeral.simps distrib mult_1)

   704   then have "divmod m n = divmod_step n (divmod m (Num.Bit0 n))"

   705     by (simp add: divmod_def)

   706   with False show ?thesis by simp

   707 qed

   708

   709 lemma divmod_cancel [code]:

   710   "divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))" (is ?P)

   711   "divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r + 1))" (is ?Q)

   712 proof -

   713   have *: "\<And>q. numeral (Num.Bit0 q) = 2 * numeral q"

   714     "\<And>q. numeral (Num.Bit1 q) = 2 * numeral q + 1"

   715     by (simp_all only: numeral_mult numeral.simps distrib) simp_all

   716   have "1 div 2 = 0" "1 mod 2 = 1" by (auto intro: div_less mod_less)

   717   then show ?P and ?Q

   718     by (simp_all add: prod_eq_iff split_def * [of m] * [of n] mod_mult_mult1

   719       div_mult2_eq [of _ _ 2] mod_mult2_eq [of _ _ 2] add.commute del: numeral_times_numeral)

   720  qed

   721

   722 end

   723

   724 hide_fact (open) diff_invert_add1 le_add_diff_inverse2 diff_zero

   725   -- {* restore simple accesses for more general variants of theorems *}

   726

   727

   728 subsection {* Division on @{typ nat} *}

   729

   730 text {*

   731   We define @{const div} and @{const mod} on @{typ nat} by means

   732   of a characteristic relation with two input arguments

   733   @{term "m\<Colon>nat"}, @{term "n\<Colon>nat"} and two output arguments

   734   @{term "q\<Colon>nat"}(uotient) and @{term "r\<Colon>nat"}(emainder).

   735 *}

   736

   737 definition divmod_nat_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool" where

   738   "divmod_nat_rel m n qr \<longleftrightarrow>

   739     m = fst qr * n + snd qr \<and>

   740       (if n = 0 then fst qr = 0 else if n > 0 then 0 \<le> snd qr \<and> snd qr < n else n < snd qr \<and> snd qr \<le> 0)"

   741

   742 text {* @{const divmod_nat_rel} is total: *}

   743

   744 lemma divmod_nat_rel_ex:

   745   obtains q r where "divmod_nat_rel m n (q, r)"

   746 proof (cases "n = 0")

   747   case True  with that show thesis

   748     by (auto simp add: divmod_nat_rel_def)

   749 next

   750   case False

   751   have "\<exists>q r. m = q * n + r \<and> r < n"

   752   proof (induct m)

   753     case 0 with n \<noteq> 0

   754     have "(0\<Colon>nat) = 0 * n + 0 \<and> 0 < n" by simp

   755     then show ?case by blast

   756   next

   757     case (Suc m) then obtain q' r'

   758       where m: "m = q' * n + r'" and n: "r' < n" by auto

   759     then show ?case proof (cases "Suc r' < n")

   760       case True

   761       from m n have "Suc m = q' * n + Suc r'" by simp

   762       with True show ?thesis by blast

   763     next

   764       case False then have "n \<le> Suc r'" by auto

   765       moreover from n have "Suc r' \<le> n" by auto

   766       ultimately have "n = Suc r'" by auto

   767       with m have "Suc m = Suc q' * n + 0" by simp

   768       with n \<noteq> 0 show ?thesis by blast

   769     qed

   770   qed

   771   with that show thesis

   772     using n \<noteq> 0 by (auto simp add: divmod_nat_rel_def)

   773 qed

   774

   775 text {* @{const divmod_nat_rel} is injective: *}

   776

   777 lemma divmod_nat_rel_unique:

   778   assumes "divmod_nat_rel m n qr"

   779     and "divmod_nat_rel m n qr'"

   780   shows "qr = qr'"

   781 proof (cases "n = 0")

   782   case True with assms show ?thesis

   783     by (cases qr, cases qr')

   784       (simp add: divmod_nat_rel_def)

   785 next

   786   case False

   787   have aux: "\<And>q r q' r'. q' * n + r' = q * n + r \<Longrightarrow> r < n \<Longrightarrow> q' \<le> (q\<Colon>nat)"

   788   apply (rule leI)

   789   apply (subst less_iff_Suc_add)

   790   apply (auto simp add: add_mult_distrib)

   791   done

   792   from n \<noteq> 0 assms have *: "fst qr = fst qr'"

   793     by (auto simp add: divmod_nat_rel_def intro: order_antisym dest: aux sym)

   794   with assms have "snd qr = snd qr'"

   795     by (simp add: divmod_nat_rel_def)

   796   with * show ?thesis by (cases qr, cases qr') simp

   797 qed

   798

   799 text {*

   800   We instantiate divisibility on the natural numbers by

   801   means of @{const divmod_nat_rel}:

   802 *}

   803

   804 definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where

   805   "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)"

   806

   807 lemma divmod_nat_rel_divmod_nat:

   808   "divmod_nat_rel m n (divmod_nat m n)"

   809 proof -

   810   from divmod_nat_rel_ex

   811     obtain qr where rel: "divmod_nat_rel m n qr" .

   812   then show ?thesis

   813   by (auto simp add: divmod_nat_def intro: theI elim: divmod_nat_rel_unique)

   814 qed

   815

   816 lemma divmod_nat_unique:

   817   assumes "divmod_nat_rel m n qr"

   818   shows "divmod_nat m n = qr"

   819   using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)

   820

   821 instantiation nat :: semiring_div

   822 begin

   823

   824 definition div_nat where

   825   "m div n = fst (divmod_nat m n)"

   826

   827 lemma fst_divmod_nat [simp]:

   828   "fst (divmod_nat m n) = m div n"

   829   by (simp add: div_nat_def)

   830

   831 definition mod_nat where

   832   "m mod n = snd (divmod_nat m n)"

   833

   834 lemma snd_divmod_nat [simp]:

   835   "snd (divmod_nat m n) = m mod n"

   836   by (simp add: mod_nat_def)

   837

   838 lemma divmod_nat_div_mod:

   839   "divmod_nat m n = (m div n, m mod n)"

   840   by (simp add: prod_eq_iff)

   841

   842 lemma div_nat_unique:

   843   assumes "divmod_nat_rel m n (q, r)"

   844   shows "m div n = q"

   845   using assms by (auto dest!: divmod_nat_unique simp add: prod_eq_iff)

   846

   847 lemma mod_nat_unique:

   848   assumes "divmod_nat_rel m n (q, r)"

   849   shows "m mod n = r"

   850   using assms by (auto dest!: divmod_nat_unique simp add: prod_eq_iff)

   851

   852 lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)"

   853   using divmod_nat_rel_divmod_nat by (simp add: divmod_nat_div_mod)

   854

   855 lemma divmod_nat_zero: "divmod_nat m 0 = (0, m)"

   856   by (simp add: divmod_nat_unique divmod_nat_rel_def)

   857

   858 lemma divmod_nat_zero_left: "divmod_nat 0 n = (0, 0)"

   859   by (simp add: divmod_nat_unique divmod_nat_rel_def)

   860

   861 lemma divmod_nat_base: "m < n \<Longrightarrow> divmod_nat m n = (0, m)"

   862   by (simp add: divmod_nat_unique divmod_nat_rel_def)

   863

   864 lemma divmod_nat_step:

   865   assumes "0 < n" and "n \<le> m"

   866   shows "divmod_nat m n = (Suc ((m - n) div n), (m - n) mod n)"

   867 proof (rule divmod_nat_unique)

   868   have "divmod_nat_rel (m - n) n ((m - n) div n, (m - n) mod n)"

   869     by (rule divmod_nat_rel)

   870   thus "divmod_nat_rel m n (Suc ((m - n) div n), (m - n) mod n)"

   871     unfolding divmod_nat_rel_def using assms by auto

   872 qed

   873

   874 text {* The ''recursion'' equations for @{const div} and @{const mod} *}

   875

   876 lemma div_less [simp]:

   877   fixes m n :: nat

   878   assumes "m < n"

   879   shows "m div n = 0"

   880   using assms divmod_nat_base by (simp add: prod_eq_iff)

   881

   882 lemma le_div_geq:

   883   fixes m n :: nat

   884   assumes "0 < n" and "n \<le> m"

   885   shows "m div n = Suc ((m - n) div n)"

   886   using assms divmod_nat_step by (simp add: prod_eq_iff)

   887

   888 lemma mod_less [simp]:

   889   fixes m n :: nat

   890   assumes "m < n"

   891   shows "m mod n = m"

   892   using assms divmod_nat_base by (simp add: prod_eq_iff)

   893

   894 lemma le_mod_geq:

   895   fixes m n :: nat

   896   assumes "n \<le> m"

   897   shows "m mod n = (m - n) mod n"

   898   using assms divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)

   899

   900 instance proof

   901   fix m n :: nat

   902   show "m div n * n + m mod n = m"

   903     using divmod_nat_rel [of m n] by (simp add: divmod_nat_rel_def)

   904 next

   905   fix m n q :: nat

   906   assume "n \<noteq> 0"

   907   then show "(q + m * n) div n = m + q div n"

   908     by (induct m) (simp_all add: le_div_geq)

   909 next

   910   fix m n q :: nat

   911   assume "m \<noteq> 0"

   912   hence "\<And>a b. divmod_nat_rel n q (a, b) \<Longrightarrow> divmod_nat_rel (m * n) (m * q) (a, m * b)"

   913     unfolding divmod_nat_rel_def

   914     by (auto split: split_if_asm, simp_all add: algebra_simps)

   915   moreover from divmod_nat_rel have "divmod_nat_rel n q (n div q, n mod q)" .

   916   ultimately have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))" .

   917   thus "(m * n) div (m * q) = n div q" by (rule div_nat_unique)

   918 next

   919   fix n :: nat show "n div 0 = 0"

   920     by (simp add: div_nat_def divmod_nat_zero)

   921 next

   922   fix n :: nat show "0 div n = 0"

   923     by (simp add: div_nat_def divmod_nat_zero_left)

   924 qed

   925

   926 end

   927

   928 lemma divmod_nat_if [code]: "divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else

   929   let (q, r) = divmod_nat (m - n) n in (Suc q, r))"

   930   by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)

   931

   932 text {* Simproc for cancelling @{const div} and @{const mod} *}

   933

   934 ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"

   935

   936 ML {*

   937 structure Cancel_Div_Mod_Nat = Cancel_Div_Mod

   938 (

   939   val div_name = @{const_name div};

   940   val mod_name = @{const_name mod};

   941   val mk_binop = HOLogic.mk_binop;

   942   val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};

   943   val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;

   944   fun mk_sum [] = HOLogic.zero

   945     | mk_sum [t] = t

   946     | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);

   947   fun dest_sum tm =

   948     if HOLogic.is_zero tm then []

   949     else

   950       (case try HOLogic.dest_Suc tm of

   951         SOME t => HOLogic.Suc_zero :: dest_sum t

   952       | NONE =>

   953           (case try dest_plus tm of

   954             SOME (t, u) => dest_sum t @ dest_sum u

   955           | NONE => [tm]));

   956

   957   val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];

   958

   959   val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac

   960     (@{thm add_0_left} :: @{thm add_0_right} :: @{thms ac_simps}))

   961 )

   962 *}

   963

   964 simproc_setup cancel_div_mod_nat ("(m::nat) + n") = {* K Cancel_Div_Mod_Nat.proc *}

   965

   966

   967 subsubsection {* Quotient *}

   968

   969 lemma div_geq: "0 < n \<Longrightarrow>  \<not> m < n \<Longrightarrow> m div n = Suc ((m - n) div n)"

   970 by (simp add: le_div_geq linorder_not_less)

   971

   972 lemma div_if: "0 < n \<Longrightarrow> m div n = (if m < n then 0 else Suc ((m - n) div n))"

   973 by (simp add: div_geq)

   974

   975 lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"

   976 by simp

   977

   978 lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"

   979 by simp

   980

   981 lemma div_positive:

   982   fixes m n :: nat

   983   assumes "n > 0"

   984   assumes "m \<ge> n"

   985   shows "m div n > 0"

   986 proof -

   987   from m \<ge> n obtain q where "m = n + q"

   988     by (auto simp add: le_iff_add)

   989   with n > 0 show ?thesis by simp

   990 qed

   991

   992

   993 subsubsection {* Remainder *}

   994

   995 lemma mod_less_divisor [simp]:

   996   fixes m n :: nat

   997   assumes "n > 0"

   998   shows "m mod n < (n::nat)"

   999   using assms divmod_nat_rel [of m n] unfolding divmod_nat_rel_def by auto

  1000

  1001 lemma mod_Suc_le_divisor [simp]:

  1002   "m mod Suc n \<le> n"

  1003   using mod_less_divisor [of "Suc n" m] by arith

  1004

  1005 lemma mod_less_eq_dividend [simp]:

  1006   fixes m n :: nat

  1007   shows "m mod n \<le> m"

  1008 proof (rule add_leD2)

  1009   from mod_div_equality have "m div n * n + m mod n = m" .

  1010   then show "m div n * n + m mod n \<le> m" by auto

  1011 qed

  1012

  1013 lemma mod_geq: "\<not> m < (n\<Colon>nat) \<Longrightarrow> m mod n = (m - n) mod n"

  1014 by (simp add: le_mod_geq linorder_not_less)

  1015

  1016 lemma mod_if: "m mod (n\<Colon>nat) = (if m < n then m else (m - n) mod n)"

  1017 by (simp add: le_mod_geq)

  1018

  1019 lemma mod_1 [simp]: "m mod Suc 0 = 0"

  1020 by (induct m) (simp_all add: mod_geq)

  1021

  1022 (* a simple rearrangement of mod_div_equality: *)

  1023 lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"

  1024   using mod_div_equality2 [of n m] by arith

  1025

  1026 lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)"

  1027   apply (drule mod_less_divisor [where m = m])

  1028   apply simp

  1029   done

  1030

  1031 subsubsection {* Quotient and Remainder *}

  1032

  1033 lemma divmod_nat_rel_mult1_eq:

  1034   "divmod_nat_rel b c (q, r)

  1035    \<Longrightarrow> divmod_nat_rel (a * b) c (a * q + a * r div c, a * r mod c)"

  1036 by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps)

  1037

  1038 lemma div_mult1_eq:

  1039   "(a * b) div c = a * (b div c) + a * (b mod c) div (c::nat)"

  1040 by (blast intro: divmod_nat_rel_mult1_eq [THEN div_nat_unique] divmod_nat_rel)

  1041

  1042 lemma divmod_nat_rel_add1_eq:

  1043   "divmod_nat_rel a c (aq, ar) \<Longrightarrow> divmod_nat_rel b c (bq, br)

  1044    \<Longrightarrow> divmod_nat_rel (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)"

  1045 by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps)

  1046

  1047 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)

  1048 lemma div_add1_eq:

  1049   "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"

  1050 by (blast intro: divmod_nat_rel_add1_eq [THEN div_nat_unique] divmod_nat_rel)

  1051

  1052 lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"

  1053   apply (cut_tac m = q and n = c in mod_less_divisor)

  1054   apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)

  1055   apply (erule_tac P = "%x. ?lhs < ?rhs x" in ssubst)

  1056   apply (simp add: add_mult_distrib2)

  1057   done

  1058

  1059 lemma divmod_nat_rel_mult2_eq:

  1060   "divmod_nat_rel a b (q, r)

  1061    \<Longrightarrow> divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"

  1062 by (auto simp add: mult.commute mult.left_commute divmod_nat_rel_def add_mult_distrib2 [symmetric] mod_lemma)

  1063

  1064 lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"

  1065 by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_nat_unique])

  1066

  1067 lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)"

  1068 by (auto simp add: mult.commute divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN mod_nat_unique])

  1069

  1070

  1071 subsubsection {* Further Facts about Quotient and Remainder *}

  1072

  1073 lemma div_1 [simp]: "m div Suc 0 = m"

  1074 by (induct m) (simp_all add: div_geq)

  1075

  1076 (* Monotonicity of div in first argument *)

  1077 lemma div_le_mono [rule_format (no_asm)]:

  1078     "\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"

  1079 apply (case_tac "k=0", simp)

  1080 apply (induct "n" rule: nat_less_induct, clarify)

  1081 apply (case_tac "n<k")

  1082 (* 1  case n<k *)

  1083 apply simp

  1084 (* 2  case n >= k *)

  1085 apply (case_tac "m<k")

  1086 (* 2.1  case m<k *)

  1087 apply simp

  1088 (* 2.2  case m>=k *)

  1089 apply (simp add: div_geq diff_le_mono)

  1090 done

  1091

  1092 (* Antimonotonicity of div in second argument *)

  1093 lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"

  1094 apply (subgoal_tac "0<n")

  1095  prefer 2 apply simp

  1096 apply (induct_tac k rule: nat_less_induct)

  1097 apply (rename_tac "k")

  1098 apply (case_tac "k<n", simp)

  1099 apply (subgoal_tac "~ (k<m) ")

  1100  prefer 2 apply simp

  1101 apply (simp add: div_geq)

  1102 apply (subgoal_tac "(k-n) div n \<le> (k-m) div n")

  1103  prefer 2

  1104  apply (blast intro: div_le_mono diff_le_mono2)

  1105 apply (rule le_trans, simp)

  1106 apply (simp)

  1107 done

  1108

  1109 lemma div_le_dividend [simp]: "m div n \<le> (m::nat)"

  1110 apply (case_tac "n=0", simp)

  1111 apply (subgoal_tac "m div n \<le> m div 1", simp)

  1112 apply (rule div_le_mono2)

  1113 apply (simp_all (no_asm_simp))

  1114 done

  1115

  1116 (* Similar for "less than" *)

  1117 lemma div_less_dividend [simp]:

  1118   "\<lbrakk>(1::nat) < n; 0 < m\<rbrakk> \<Longrightarrow> m div n < m"

  1119 apply (induct m rule: nat_less_induct)

  1120 apply (rename_tac "m")

  1121 apply (case_tac "m<n", simp)

  1122 apply (subgoal_tac "0<n")

  1123  prefer 2 apply simp

  1124 apply (simp add: div_geq)

  1125 apply (case_tac "n<m")

  1126  apply (subgoal_tac "(m-n) div n < (m-n) ")

  1127   apply (rule impI less_trans_Suc)+

  1128 apply assumption

  1129   apply (simp_all)

  1130 done

  1131

  1132 text{*A fact for the mutilated chess board*}

  1133 lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"

  1134 apply (case_tac "n=0", simp)

  1135 apply (induct "m" rule: nat_less_induct)

  1136 apply (case_tac "Suc (na) <n")

  1137 (* case Suc(na) < n *)

  1138 apply (frule lessI [THEN less_trans], simp add: less_not_refl3)

  1139 (* case n \<le> Suc(na) *)

  1140 apply (simp add: linorder_not_less le_Suc_eq mod_geq)

  1141 apply (auto simp add: Suc_diff_le le_mod_geq)

  1142 done

  1143

  1144 lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"

  1145 by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)

  1146

  1147 lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]

  1148

  1149 (*Loses information, namely we also have r<d provided d is nonzero*)

  1150 lemma mod_eqD:

  1151   fixes m d r q :: nat

  1152   assumes "m mod d = r"

  1153   shows "\<exists>q. m = r + q * d"

  1154 proof -

  1155   from mod_div_equality obtain q where "q * d + m mod d = m" by blast

  1156   with assms have "m = r + q * d" by simp

  1157   then show ?thesis ..

  1158 qed

  1159

  1160 lemma split_div:

  1161  "P(n div k :: nat) =

  1162  ((k = 0 \<longrightarrow> P 0) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P i)))"

  1163  (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")

  1164 proof

  1165   assume P: ?P

  1166   show ?Q

  1167   proof (cases)

  1168     assume "k = 0"

  1169     with P show ?Q by simp

  1170   next

  1171     assume not0: "k \<noteq> 0"

  1172     thus ?Q

  1173     proof (simp, intro allI impI)

  1174       fix i j

  1175       assume n: "n = k*i + j" and j: "j < k"

  1176       show "P i"

  1177       proof (cases)

  1178         assume "i = 0"

  1179         with n j P show "P i" by simp

  1180       next

  1181         assume "i \<noteq> 0"

  1182         with not0 n j P show "P i" by(simp add:ac_simps)

  1183       qed

  1184     qed

  1185   qed

  1186 next

  1187   assume Q: ?Q

  1188   show ?P

  1189   proof (cases)

  1190     assume "k = 0"

  1191     with Q show ?P by simp

  1192   next

  1193     assume not0: "k \<noteq> 0"

  1194     with Q have R: ?R by simp

  1195     from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]

  1196     show ?P by simp

  1197   qed

  1198 qed

  1199

  1200 lemma split_div_lemma:

  1201   assumes "0 < n"

  1202   shows "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> q = ((m\<Colon>nat) div n)" (is "?lhs \<longleftrightarrow> ?rhs")

  1203 proof

  1204   assume ?rhs

  1205   with mult_div_cancel have nq: "n * q = m - (m mod n)" by simp

  1206   then have A: "n * q \<le> m" by simp

  1207   have "n - (m mod n) > 0" using mod_less_divisor assms by auto

  1208   then have "m < m + (n - (m mod n))" by simp

  1209   then have "m < n + (m - (m mod n))" by simp

  1210   with nq have "m < n + n * q" by simp

  1211   then have B: "m < n * Suc q" by simp

  1212   from A B show ?lhs ..

  1213 next

  1214   assume P: ?lhs

  1215   then have "divmod_nat_rel m n (q, m - n * q)"

  1216     unfolding divmod_nat_rel_def by (auto simp add: ac_simps)

  1217   with divmod_nat_rel_unique divmod_nat_rel [of m n]

  1218   have "(q, m - n * q) = (m div n, m mod n)" by auto

  1219   then show ?rhs by simp

  1220 qed

  1221

  1222 theorem split_div':

  1223   "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>

  1224    (\<exists>q. (n * q \<le> m \<and> m < n * (Suc q)) \<and> P q))"

  1225   apply (case_tac "0 < n")

  1226   apply (simp only: add: split_div_lemma)

  1227   apply simp_all

  1228   done

  1229

  1230 lemma split_mod:

  1231  "P(n mod k :: nat) =

  1232  ((k = 0 \<longrightarrow> P n) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P j)))"

  1233  (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")

  1234 proof

  1235   assume P: ?P

  1236   show ?Q

  1237   proof (cases)

  1238     assume "k = 0"

  1239     with P show ?Q by simp

  1240   next

  1241     assume not0: "k \<noteq> 0"

  1242     thus ?Q

  1243     proof (simp, intro allI impI)

  1244       fix i j

  1245       assume "n = k*i + j" "j < k"

  1246       thus "P j" using not0 P by(simp add:ac_simps ac_simps)

  1247     qed

  1248   qed

  1249 next

  1250   assume Q: ?Q

  1251   show ?P

  1252   proof (cases)

  1253     assume "k = 0"

  1254     with Q show ?P by simp

  1255   next

  1256     assume not0: "k \<noteq> 0"

  1257     with Q have R: ?R by simp

  1258     from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]

  1259     show ?P by simp

  1260   qed

  1261 qed

  1262

  1263 theorem mod_div_equality': "(m::nat) mod n = m - (m div n) * n"

  1264   using mod_div_equality [of m n] by arith

  1265

  1266 lemma div_mod_equality': "(m::nat) div n * n = m - m mod n"

  1267   using mod_div_equality [of m n] by arith

  1268 (* FIXME: very similar to mult_div_cancel *)

  1269

  1270 lemma div_eq_dividend_iff: "a \<noteq> 0 \<Longrightarrow> (a :: nat) div b = a \<longleftrightarrow> b = 1"

  1271   apply rule

  1272   apply (cases "b = 0")

  1273   apply simp_all

  1274   apply (metis (full_types) One_nat_def Suc_lessI div_less_dividend less_not_refl3)

  1275   done

  1276

  1277

  1278 subsubsection {* An induction'' law for modulus arithmetic. *}

  1279

  1280 lemma mod_induct_0:

  1281   assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"

  1282   and base: "P i" and i: "i<p"

  1283   shows "P 0"

  1284 proof (rule ccontr)

  1285   assume contra: "\<not>(P 0)"

  1286   from i have p: "0<p" by simp

  1287   have "\<forall>k. 0<k \<longrightarrow> \<not> P (p-k)" (is "\<forall>k. ?A k")

  1288   proof

  1289     fix k

  1290     show "?A k"

  1291     proof (induct k)

  1292       show "?A 0" by simp  -- "by contradiction"

  1293     next

  1294       fix n

  1295       assume ih: "?A n"

  1296       show "?A (Suc n)"

  1297       proof (clarsimp)

  1298         assume y: "P (p - Suc n)"

  1299         have n: "Suc n < p"

  1300         proof (rule ccontr)

  1301           assume "\<not>(Suc n < p)"

  1302           hence "p - Suc n = 0"

  1303             by simp

  1304           with y contra show "False"

  1305             by simp

  1306         qed

  1307         hence n2: "Suc (p - Suc n) = p-n" by arith

  1308         from p have "p - Suc n < p" by arith

  1309         with y step have z: "P ((Suc (p - Suc n)) mod p)"

  1310           by blast

  1311         show "False"

  1312         proof (cases "n=0")

  1313           case True

  1314           with z n2 contra show ?thesis by simp

  1315         next

  1316           case False

  1317           with p have "p-n < p" by arith

  1318           with z n2 False ih show ?thesis by simp

  1319         qed

  1320       qed

  1321     qed

  1322   qed

  1323   moreover

  1324   from i obtain k where "0<k \<and> i+k=p"

  1325     by (blast dest: less_imp_add_positive)

  1326   hence "0<k \<and> i=p-k" by auto

  1327   moreover

  1328   note base

  1329   ultimately

  1330   show "False" by blast

  1331 qed

  1332

  1333 lemma mod_induct:

  1334   assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"

  1335   and base: "P i" and i: "i<p" and j: "j<p"

  1336   shows "P j"

  1337 proof -

  1338   have "\<forall>j<p. P j"

  1339   proof

  1340     fix j

  1341     show "j<p \<longrightarrow> P j" (is "?A j")

  1342     proof (induct j)

  1343       from step base i show "?A 0"

  1344         by (auto elim: mod_induct_0)

  1345     next

  1346       fix k

  1347       assume ih: "?A k"

  1348       show "?A (Suc k)"

  1349       proof

  1350         assume suc: "Suc k < p"

  1351         hence k: "k<p" by simp

  1352         with ih have "P k" ..

  1353         with step k have "P (Suc k mod p)"

  1354           by blast

  1355         moreover

  1356         from suc have "Suc k mod p = Suc k"

  1357           by simp

  1358         ultimately

  1359         show "P (Suc k)" by simp

  1360       qed

  1361     qed

  1362   qed

  1363   with j show ?thesis by blast

  1364 qed

  1365

  1366 lemma div2_Suc_Suc [simp]: "Suc (Suc m) div 2 = Suc (m div 2)"

  1367   by (simp add: numeral_2_eq_2 le_div_geq)

  1368

  1369 lemma mod2_Suc_Suc [simp]: "Suc (Suc m) mod 2 = m mod 2"

  1370   by (simp add: numeral_2_eq_2 le_mod_geq)

  1371

  1372 lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"

  1373 by (simp add: mult_2 [symmetric])

  1374

  1375 lemma mod2_gr_0 [simp]: "0 < (m\<Colon>nat) mod 2 \<longleftrightarrow> m mod 2 = 1"

  1376 proof -

  1377   { fix n :: nat have  "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (cases n) simp_all }

  1378   moreover have "m mod 2 < 2" by simp

  1379   ultimately have "m mod 2 = 0 \<or> m mod 2 = 1" .

  1380   then show ?thesis by auto

  1381 qed

  1382

  1383 text{*These lemmas collapse some needless occurrences of Suc:

  1384     at least three Sucs, since two and fewer are rewritten back to Suc again!

  1385     We already have some rules to simplify operands smaller than 3.*}

  1386

  1387 lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"

  1388 by (simp add: Suc3_eq_add_3)

  1389

  1390 lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"

  1391 by (simp add: Suc3_eq_add_3)

  1392

  1393 lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"

  1394 by (simp add: Suc3_eq_add_3)

  1395

  1396 lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"

  1397 by (simp add: Suc3_eq_add_3)

  1398

  1399 lemmas Suc_div_eq_add3_div_numeral [simp] = Suc_div_eq_add3_div [of _ "numeral v"] for v

  1400 lemmas Suc_mod_eq_add3_mod_numeral [simp] = Suc_mod_eq_add3_mod [of _ "numeral v"] for v

  1401

  1402

  1403 lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1"

  1404 apply (induct "m")

  1405 apply (simp_all add: mod_Suc)

  1406 done

  1407

  1408 declare Suc_times_mod_eq [of "numeral w", simp] for w

  1409

  1410 lemma Suc_div_le_mono [simp]: "n div k \<le> (Suc n) div k"

  1411 by (simp add: div_le_mono)

  1412

  1413 lemma Suc_n_div_2_gt_zero [simp]: "(0::nat) < n ==> 0 < (n + 1) div 2"

  1414 by (cases n) simp_all

  1415

  1416 lemma div_2_gt_zero [simp]: assumes A: "(1::nat) < n" shows "0 < n div 2"

  1417 proof -

  1418   from A have B: "0 < n - 1" and C: "n - 1 + 1 = n" by simp_all

  1419   from Suc_n_div_2_gt_zero [OF B] C show ?thesis by simp

  1420 qed

  1421

  1422   (* Potential use of algebra : Equality modulo n*)

  1423 lemma mod_mult_self3 [simp]: "(k*n + m) mod n = m mod (n::nat)"

  1424 by (simp add: ac_simps ac_simps)

  1425

  1426 lemma mod_mult_self4 [simp]: "Suc (k*n + m) mod n = Suc m mod n"

  1427 proof -

  1428   have "Suc (k * n + m) mod n = (k * n + Suc m) mod n" by simp

  1429   also have "... = Suc m mod n" by (rule mod_mult_self3)

  1430   finally show ?thesis .

  1431 qed

  1432

  1433 lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n"

  1434 apply (subst mod_Suc [of m])

  1435 apply (subst mod_Suc [of "m mod n"], simp)

  1436 done

  1437

  1438 lemma mod_2_not_eq_zero_eq_one_nat:

  1439   fixes n :: nat

  1440   shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"

  1441   by simp

  1442

  1443 instance nat :: semiring_numeral_div

  1444   by intro_classes (auto intro: div_positive simp add: mult_div_cancel mod_mult2_eq div_mult2_eq)

  1445

  1446

  1447 subsection {* Division on @{typ int} *}

  1448

  1449 definition divmod_int_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" where

  1450     --{*definition of quotient and remainder*}

  1451   "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>

  1452     (if 0 < b then 0 \<le> r \<and> r < b else if b < 0 then b < r \<and> r \<le> 0 else q = 0))"

  1453

  1454 text {*

  1455   The following algorithmic devlopment actually echos what has already

  1456   been developed in class @{class semiring_numeral_div}.  In the long

  1457   run it seems better to derive division on @{typ int} just from

  1458   division on @{typ nat} and instantiate @{class semiring_numeral_div}

  1459   accordingly.

  1460 *}

  1461

  1462 definition adjust :: "int \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int" where

  1463     --{*for the division algorithm*}

  1464     "adjust b = (\<lambda>(q, r). if 0 \<le> r - b then (2 * q + 1, r - b)

  1465                          else (2 * q, r))"

  1466

  1467 text{*algorithm for the case @{text "a\<ge>0, b>0"}*}

  1468 function posDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where

  1469   "posDivAlg a b = (if a < b \<or>  b \<le> 0 then (0, a)

  1470      else adjust b (posDivAlg a (2 * b)))"

  1471 by auto

  1472 termination by (relation "measure (\<lambda>(a, b). nat (a - b + 1))")

  1473   (auto simp add: mult_2)

  1474

  1475 text{*algorithm for the case @{text "a<0, b>0"}*}

  1476 function negDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where

  1477   "negDivAlg a b = (if 0 \<le>a + b \<or> b \<le> 0  then (-1, a + b)

  1478      else adjust b (negDivAlg a (2 * b)))"

  1479 by auto

  1480 termination by (relation "measure (\<lambda>(a, b). nat (- a - b))")

  1481   (auto simp add: mult_2)

  1482

  1483 text{*algorithm for the general case @{term "b\<noteq>0"}*}

  1484

  1485 definition divmod_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where

  1486     --{*The full division algorithm considers all possible signs for a, b

  1487        including the special case @{text "a=0, b<0"} because

  1488        @{term negDivAlg} requires @{term "a<0"}.*}

  1489   "divmod_int a b = (if 0 \<le> a then if 0 \<le> b then posDivAlg a b

  1490                   else if a = 0 then (0, 0)

  1491                        else apsnd uminus (negDivAlg (-a) (-b))

  1492                else

  1493                   if 0 < b then negDivAlg a b

  1494                   else apsnd uminus (posDivAlg (-a) (-b)))"

  1495

  1496 instantiation int :: Divides.div

  1497 begin

  1498

  1499 definition div_int where

  1500   "a div b = fst (divmod_int a b)"

  1501

  1502 lemma fst_divmod_int [simp]:

  1503   "fst (divmod_int a b) = a div b"

  1504   by (simp add: div_int_def)

  1505

  1506 definition mod_int where

  1507   "a mod b = snd (divmod_int a b)"

  1508

  1509 lemma snd_divmod_int [simp]:

  1510   "snd (divmod_int a b) = a mod b"

  1511   by (simp add: mod_int_def)

  1512

  1513 instance ..

  1514

  1515 end

  1516

  1517 lemma divmod_int_mod_div:

  1518   "divmod_int p q = (p div q, p mod q)"

  1519   by (simp add: prod_eq_iff)

  1520

  1521 text{*

  1522 Here is the division algorithm in ML:

  1523

  1524 \begin{verbatim}

  1525     fun posDivAlg (a,b) =

  1526       if a<b then (0,a)

  1527       else let val (q,r) = posDivAlg(a, 2*b)

  1528                in  if 0\<le>r-b then (2*q+1, r-b) else (2*q, r)

  1529            end

  1530

  1531     fun negDivAlg (a,b) =

  1532       if 0\<le>a+b then (~1,a+b)

  1533       else let val (q,r) = negDivAlg(a, 2*b)

  1534                in  if 0\<le>r-b then (2*q+1, r-b) else (2*q, r)

  1535            end;

  1536

  1537     fun negateSnd (q,r:int) = (q,~r);

  1538

  1539     fun divmod (a,b) = if 0\<le>a then

  1540                           if b>0 then posDivAlg (a,b)

  1541                            else if a=0 then (0,0)

  1542                                 else negateSnd (negDivAlg (~a,~b))

  1543                        else

  1544                           if 0<b then negDivAlg (a,b)

  1545                           else        negateSnd (posDivAlg (~a,~b));

  1546 \end{verbatim}

  1547 *}

  1548

  1549

  1550 subsubsection {* Uniqueness and Monotonicity of Quotients and Remainders *}

  1551

  1552 lemma unique_quotient_lemma:

  1553      "[| b*q' + r'  \<le> b*q + r;  0 \<le> r';  r' < b;  r < b |]

  1554       ==> q' \<le> (q::int)"

  1555 apply (subgoal_tac "r' + b * (q'-q) \<le> r")

  1556  prefer 2 apply (simp add: right_diff_distrib)

  1557 apply (subgoal_tac "0 < b * (1 + q - q') ")

  1558 apply (erule_tac [2] order_le_less_trans)

  1559  prefer 2 apply (simp add: right_diff_distrib distrib_left)

  1560 apply (subgoal_tac "b * q' < b * (1 + q) ")

  1561  prefer 2 apply (simp add: right_diff_distrib distrib_left)

  1562 apply (simp add: mult_less_cancel_left)

  1563 done

  1564

  1565 lemma unique_quotient_lemma_neg:

  1566      "[| b*q' + r' \<le> b*q + r;  r \<le> 0;  b < r;  b < r' |]

  1567       ==> q \<le> (q'::int)"

  1568 by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma,

  1569     auto)

  1570

  1571 lemma unique_quotient:

  1572      "[| divmod_int_rel a b (q, r); divmod_int_rel a b (q', r') |]

  1573       ==> q = q'"

  1574 apply (simp add: divmod_int_rel_def linorder_neq_iff split: split_if_asm)

  1575 apply (blast intro: order_antisym

  1576              dest: order_eq_refl [THEN unique_quotient_lemma]

  1577              order_eq_refl [THEN unique_quotient_lemma_neg] sym)+

  1578 done

  1579

  1580

  1581 lemma unique_remainder:

  1582      "[| divmod_int_rel a b (q, r); divmod_int_rel a b (q', r') |]

  1583       ==> r = r'"

  1584 apply (subgoal_tac "q = q'")

  1585  apply (simp add: divmod_int_rel_def)

  1586 apply (blast intro: unique_quotient)

  1587 done

  1588

  1589

  1590 subsubsection {* Correctness of @{term posDivAlg}, the Algorithm for Non-Negative Dividends *}

  1591

  1592 text{*And positive divisors*}

  1593

  1594 lemma adjust_eq [simp]:

  1595      "adjust b (q, r) =

  1596       (let diff = r - b in

  1597         if 0 \<le> diff then (2 * q + 1, diff)

  1598                      else (2*q, r))"

  1599   by (simp add: Let_def adjust_def)

  1600

  1601 declare posDivAlg.simps [simp del]

  1602

  1603 text{*use with a simproc to avoid repeatedly proving the premise*}

  1604 lemma posDivAlg_eqn:

  1605      "0 < b ==>

  1606       posDivAlg a b = (if a<b then (0,a) else adjust b (posDivAlg a (2*b)))"

  1607 by (rule posDivAlg.simps [THEN trans], simp)

  1608

  1609 text{*Correctness of @{term posDivAlg}: it computes quotients correctly*}

  1610 theorem posDivAlg_correct:

  1611   assumes "0 \<le> a" and "0 < b"

  1612   shows "divmod_int_rel a b (posDivAlg a b)"

  1613   using assms

  1614   apply (induct a b rule: posDivAlg.induct)

  1615   apply auto

  1616   apply (simp add: divmod_int_rel_def)

  1617   apply (subst posDivAlg_eqn, simp add: distrib_left)

  1618   apply (case_tac "a < b")

  1619   apply simp_all

  1620   apply (erule splitE)

  1621   apply (auto simp add: distrib_left Let_def ac_simps mult_2_right)

  1622   done

  1623

  1624

  1625 subsubsection {* Correctness of @{term negDivAlg}, the Algorithm for Negative Dividends *}

  1626

  1627 text{*And positive divisors*}

  1628

  1629 declare negDivAlg.simps [simp del]

  1630

  1631 text{*use with a simproc to avoid repeatedly proving the premise*}

  1632 lemma negDivAlg_eqn:

  1633      "0 < b ==>

  1634       negDivAlg a b =

  1635        (if 0\<le>a+b then (-1,a+b) else adjust b (negDivAlg a (2*b)))"

  1636 by (rule negDivAlg.simps [THEN trans], simp)

  1637

  1638 (*Correctness of negDivAlg: it computes quotients correctly

  1639   It doesn't work if a=0 because the 0/b equals 0, not -1*)

  1640 lemma negDivAlg_correct:

  1641   assumes "a < 0" and "b > 0"

  1642   shows "divmod_int_rel a b (negDivAlg a b)"

  1643   using assms

  1644   apply (induct a b rule: negDivAlg.induct)

  1645   apply (auto simp add: linorder_not_le)

  1646   apply (simp add: divmod_int_rel_def)

  1647   apply (subst negDivAlg_eqn, assumption)

  1648   apply (case_tac "a + b < (0\<Colon>int)")

  1649   apply simp_all

  1650   apply (erule splitE)

  1651   apply (auto simp add: distrib_left Let_def ac_simps mult_2_right)

  1652   done

  1653

  1654

  1655 subsubsection {* Existence Shown by Proving the Division Algorithm to be Correct *}

  1656

  1657 (*the case a=0*)

  1658 lemma divmod_int_rel_0: "divmod_int_rel 0 b (0, 0)"

  1659 by (auto simp add: divmod_int_rel_def linorder_neq_iff)

  1660

  1661 lemma posDivAlg_0 [simp]: "posDivAlg 0 b = (0, 0)"

  1662 by (subst posDivAlg.simps, auto)

  1663

  1664 lemma posDivAlg_0_right [simp]: "posDivAlg a 0 = (0, a)"

  1665 by (subst posDivAlg.simps, auto)

  1666

  1667 lemma negDivAlg_minus1 [simp]: "negDivAlg (- 1) b = (- 1, b - 1)"

  1668 by (subst negDivAlg.simps, auto)

  1669

  1670 lemma divmod_int_rel_neg: "divmod_int_rel (-a) (-b) qr ==> divmod_int_rel a b (apsnd uminus qr)"

  1671 by (auto simp add: divmod_int_rel_def)

  1672

  1673 lemma divmod_int_correct: "divmod_int_rel a b (divmod_int a b)"

  1674 apply (cases "b = 0", simp add: divmod_int_def divmod_int_rel_def)

  1675 by (force simp add: linorder_neq_iff divmod_int_rel_0 divmod_int_def divmod_int_rel_neg

  1676                     posDivAlg_correct negDivAlg_correct)

  1677

  1678 lemma divmod_int_unique:

  1679   assumes "divmod_int_rel a b qr"

  1680   shows "divmod_int a b = qr"

  1681   using assms divmod_int_correct [of a b]

  1682   using unique_quotient [of a b] unique_remainder [of a b]

  1683   by (metis pair_collapse)

  1684

  1685 lemma divmod_int_rel_div_mod: "divmod_int_rel a b (a div b, a mod b)"

  1686   using divmod_int_correct by (simp add: divmod_int_mod_div)

  1687

  1688 lemma div_int_unique: "divmod_int_rel a b (q, r) \<Longrightarrow> a div b = q"

  1689   by (simp add: divmod_int_rel_div_mod [THEN unique_quotient])

  1690

  1691 lemma mod_int_unique: "divmod_int_rel a b (q, r) \<Longrightarrow> a mod b = r"

  1692   by (simp add: divmod_int_rel_div_mod [THEN unique_remainder])

  1693

  1694 instance int :: ring_div

  1695 proof

  1696   fix a b :: int

  1697   show "a div b * b + a mod b = a"

  1698     using divmod_int_rel_div_mod [of a b]

  1699     unfolding divmod_int_rel_def by (simp add: mult.commute)

  1700 next

  1701   fix a b c :: int

  1702   assume "b \<noteq> 0"

  1703   hence "divmod_int_rel (a + c * b) b (c + a div b, a mod b)"

  1704     using divmod_int_rel_div_mod [of a b]

  1705     unfolding divmod_int_rel_def by (auto simp: algebra_simps)

  1706   thus "(a + c * b) div b = c + a div b"

  1707     by (rule div_int_unique)

  1708 next

  1709   fix a b c :: int

  1710   assume "c \<noteq> 0"

  1711   hence "\<And>q r. divmod_int_rel a b (q, r)

  1712     \<Longrightarrow> divmod_int_rel (c * a) (c * b) (q, c * r)"

  1713     unfolding divmod_int_rel_def

  1714     by - (rule linorder_cases [of 0 b], auto simp: algebra_simps

  1715       mult_less_0_iff zero_less_mult_iff mult_strict_right_mono

  1716       mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff)

  1717   hence "divmod_int_rel (c * a) (c * b) (a div b, c * (a mod b))"

  1718     using divmod_int_rel_div_mod [of a b] .

  1719   thus "(c * a) div (c * b) = a div b"

  1720     by (rule div_int_unique)

  1721 next

  1722   fix a :: int show "a div 0 = 0"

  1723     by (rule div_int_unique, simp add: divmod_int_rel_def)

  1724 next

  1725   fix a :: int show "0 div a = 0"

  1726     by (rule div_int_unique, auto simp add: divmod_int_rel_def)

  1727 qed

  1728

  1729 text{*Basic laws about division and remainder*}

  1730

  1731 lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"

  1732   by (fact mod_div_equality2 [symmetric])

  1733

  1734 text {* Tool setup *}

  1735

  1736 (* FIXME: Theorem list add_0s doesn't exist, because Numeral0 has gone. *)

  1737 lemmas add_0s = add_0_left add_0_right

  1738

  1739 ML {*

  1740 structure Cancel_Div_Mod_Int = Cancel_Div_Mod

  1741 (

  1742   val div_name = @{const_name div};

  1743   val mod_name = @{const_name mod};

  1744   val mk_binop = HOLogic.mk_binop;

  1745   val mk_sum = Arith_Data.mk_sum HOLogic.intT;

  1746   val dest_sum = Arith_Data.dest_sum;

  1747

  1748   val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];

  1749

  1750   val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac

  1751     (@{thm diff_conv_add_uminus} :: @{thms add_0s} @ @{thms ac_simps}))

  1752 )

  1753 *}

  1754

  1755 simproc_setup cancel_div_mod_int ("(k::int) + l") = {* K Cancel_Div_Mod_Int.proc *}

  1756

  1757 lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"

  1758   using divmod_int_correct [of a b]

  1759   by (auto simp add: divmod_int_rel_def prod_eq_iff)

  1760

  1761 lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1]

  1762    and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2]

  1763

  1764 lemma neg_mod_conj: "b < (0::int) \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b"

  1765   using divmod_int_correct [of a b]

  1766   by (auto simp add: divmod_int_rel_def prod_eq_iff)

  1767

  1768 lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1]

  1769    and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2]

  1770

  1771

  1772 subsubsection {* General Properties of div and mod *}

  1773

  1774 lemma div_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a div b = 0"

  1775 apply (rule div_int_unique)

  1776 apply (auto simp add: divmod_int_rel_def)

  1777 done

  1778

  1779 lemma div_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a div b = 0"

  1780 apply (rule div_int_unique)

  1781 apply (auto simp add: divmod_int_rel_def)

  1782 done

  1783

  1784 lemma div_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a div b = -1"

  1785 apply (rule div_int_unique)

  1786 apply (auto simp add: divmod_int_rel_def)

  1787 done

  1788

  1789 (*There is no div_neg_pos_trivial because  0 div b = 0 would supersede it*)

  1790

  1791 lemma mod_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a mod b = a"

  1792 apply (rule_tac q = 0 in mod_int_unique)

  1793 apply (auto simp add: divmod_int_rel_def)

  1794 done

  1795

  1796 lemma mod_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a mod b = a"

  1797 apply (rule_tac q = 0 in mod_int_unique)

  1798 apply (auto simp add: divmod_int_rel_def)

  1799 done

  1800

  1801 lemma mod_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a mod b = a+b"

  1802 apply (rule_tac q = "-1" in mod_int_unique)

  1803 apply (auto simp add: divmod_int_rel_def)

  1804 done

  1805

  1806 text{*There is no @{text mod_neg_pos_trivial}.*}

  1807

  1808

  1809 subsubsection {* Laws for div and mod with Unary Minus *}

  1810

  1811 lemma zminus1_lemma:

  1812      "divmod_int_rel a b (q, r) ==> b \<noteq> 0

  1813       ==> divmod_int_rel (-a) b (if r=0 then -q else -q - 1,

  1814                           if r=0 then 0 else b-r)"

  1815 by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_diff_distrib)

  1816

  1817

  1818 lemma zdiv_zminus1_eq_if:

  1819      "b \<noteq> (0::int)

  1820       ==> (-a) div b =

  1821           (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"

  1822 by (blast intro: divmod_int_rel_div_mod [THEN zminus1_lemma, THEN div_int_unique])

  1823

  1824 lemma zmod_zminus1_eq_if:

  1825      "(-a::int) mod b = (if a mod b = 0 then 0 else  b - (a mod b))"

  1826 apply (case_tac "b = 0", simp)

  1827 apply (blast intro: divmod_int_rel_div_mod [THEN zminus1_lemma, THEN mod_int_unique])

  1828 done

  1829

  1830 lemma zmod_zminus1_not_zero:

  1831   fixes k l :: int

  1832   shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"

  1833   unfolding zmod_zminus1_eq_if by auto

  1834

  1835 lemma zdiv_zminus2_eq_if:

  1836      "b \<noteq> (0::int)

  1837       ==> a div (-b) =

  1838           (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"

  1839 by (simp add: zdiv_zminus1_eq_if div_minus_right)

  1840

  1841 lemma zmod_zminus2_eq_if:

  1842      "a mod (-b::int) = (if a mod b = 0 then 0 else  (a mod b) - b)"

  1843 by (simp add: zmod_zminus1_eq_if mod_minus_right)

  1844

  1845 lemma zmod_zminus2_not_zero:

  1846   fixes k l :: int

  1847   shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"

  1848   unfolding zmod_zminus2_eq_if by auto

  1849

  1850

  1851 subsubsection {* Computation of Division and Remainder *}

  1852

  1853 lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"

  1854 by (simp add: div_int_def divmod_int_def)

  1855

  1856 lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"

  1857 by (simp add: mod_int_def divmod_int_def)

  1858

  1859 text{*a positive, b positive *}

  1860

  1861 lemma div_pos_pos: "[| 0 < a;  0 \<le> b |] ==> a div b = fst (posDivAlg a b)"

  1862 by (simp add: div_int_def divmod_int_def)

  1863

  1864 lemma mod_pos_pos: "[| 0 < a;  0 \<le> b |] ==> a mod b = snd (posDivAlg a b)"

  1865 by (simp add: mod_int_def divmod_int_def)

  1866

  1867 text{*a negative, b positive *}

  1868

  1869 lemma div_neg_pos: "[| a < 0;  0 < b |] ==> a div b = fst (negDivAlg a b)"

  1870 by (simp add: div_int_def divmod_int_def)

  1871

  1872 lemma mod_neg_pos: "[| a < 0;  0 < b |] ==> a mod b = snd (negDivAlg a b)"

  1873 by (simp add: mod_int_def divmod_int_def)

  1874

  1875 text{*a positive, b negative *}

  1876

  1877 lemma div_pos_neg:

  1878      "[| 0 < a;  b < 0 |] ==> a div b = fst (apsnd uminus (negDivAlg (-a) (-b)))"

  1879 by (simp add: div_int_def divmod_int_def)

  1880

  1881 lemma mod_pos_neg:

  1882      "[| 0 < a;  b < 0 |] ==> a mod b = snd (apsnd uminus (negDivAlg (-a) (-b)))"

  1883 by (simp add: mod_int_def divmod_int_def)

  1884

  1885 text{*a negative, b negative *}

  1886

  1887 lemma div_neg_neg:

  1888      "[| a < 0;  b \<le> 0 |] ==> a div b = fst (apsnd uminus (posDivAlg (-a) (-b)))"

  1889 by (simp add: div_int_def divmod_int_def)

  1890

  1891 lemma mod_neg_neg:

  1892      "[| a < 0;  b \<le> 0 |] ==> a mod b = snd (apsnd uminus (posDivAlg (-a) (-b)))"

  1893 by (simp add: mod_int_def divmod_int_def)

  1894

  1895 text {*Simplify expresions in which div and mod combine numerical constants*}

  1896

  1897 lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"

  1898   by (rule div_int_unique [of a b q r]) (simp add: divmod_int_rel_def)

  1899

  1900 lemma int_div_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a div b = q"

  1901   by (rule div_int_unique [of a b q r],

  1902     simp add: divmod_int_rel_def)

  1903

  1904 lemma int_mod_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a mod b = r"

  1905   by (rule mod_int_unique [of a b q r],

  1906     simp add: divmod_int_rel_def)

  1907

  1908 lemma int_mod_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a mod b = r"

  1909   by (rule mod_int_unique [of a b q r],

  1910     simp add: divmod_int_rel_def)

  1911

  1912 text {*

  1913   numeral simprocs -- high chance that these can be replaced

  1914   by divmod algorithm from @{class semiring_numeral_div}

  1915 *}

  1916

  1917 ML {*

  1918 local

  1919   val mk_number = HOLogic.mk_number HOLogic.intT

  1920   val plus = @{term "plus :: int \<Rightarrow> int \<Rightarrow> int"}

  1921   val times = @{term "times :: int \<Rightarrow> int \<Rightarrow> int"}

  1922   val zero = @{term "0 :: int"}

  1923   val less = @{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"}

  1924   val le = @{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"}

  1925   val simps = @{thms arith_simps} @ @{thms rel_simps} @ [@{thm numeral_1_eq_1 [symmetric]}]

  1926   fun prove ctxt goal = (writeln "prove"; Goal.prove ctxt [] [] (HOLogic.mk_Trueprop goal)

  1927     (K (ALLGOALS (full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps)))));

  1928   fun binary_proc proc ctxt ct =

  1929     (case Thm.term_of ct of

  1930       _ $t$ u =>

  1931       (case try (pairself ((snd o HOLogic.dest_number))) (t, u) of

  1932         SOME args => proc ctxt args

  1933       | NONE => NONE)

  1934     | _ => NONE);

  1935 in

  1936   fun divmod_proc posrule negrule =

  1937     binary_proc (fn ctxt => fn ((a, t), (b, u)) =>

  1938       if b = 0 then NONE else let

  1939         val (q, r) = pairself mk_number (Integer.div_mod a b)

  1940         val goal1 = HOLogic.mk_eq (t, plus $(times$ u $q)$ r)

  1941         val (goal2, goal3, rule) = if b > 0

  1942           then (le $zero$ r, less $r$ u, posrule RS eq_reflection)

  1943           else (le $r$ zero, less $u$ r, negrule RS eq_reflection)

  1944       in SOME (rule OF map (prove ctxt) [goal1, goal2, goal3]) end)

  1945 end

  1946 *}

  1947

  1948 simproc_setup binary_int_div

  1949   ("numeral m div numeral n :: int" |

  1950    "numeral m div - numeral n :: int" |

  1951    "- numeral m div numeral n :: int" |

  1952    "- numeral m div - numeral n :: int") =

  1953   {* K (divmod_proc @{thm int_div_pos_eq} @{thm int_div_neg_eq}) *}

  1954

  1955 simproc_setup binary_int_mod

  1956   ("numeral m mod numeral n :: int" |

  1957    "numeral m mod - numeral n :: int" |

  1958    "- numeral m mod numeral n :: int" |

  1959    "- numeral m mod - numeral n :: int") =

  1960   {* K (divmod_proc @{thm int_mod_pos_eq} @{thm int_mod_neg_eq}) *}

  1961

  1962 lemmas posDivAlg_eqn_numeral [simp] =

  1963     posDivAlg_eqn [of "numeral v" "numeral w", OF zero_less_numeral] for v w

  1964

  1965 lemmas negDivAlg_eqn_numeral [simp] =

  1966     negDivAlg_eqn [of "numeral v" "- numeral w", OF zero_less_numeral] for v w

  1967

  1968

  1969 text {* Special-case simplification: @{text "\<plusminus>1 div z"} and @{text "\<plusminus>1 mod z"} *}

  1970

  1971 lemma [simp]:

  1972   shows div_one_bit0: "1 div numeral (Num.Bit0 v) = (0 :: int)"

  1973     and mod_one_bit0: "1 mod numeral (Num.Bit0 v) = (1 :: int)"

  1974     and div_one_bit1: "1 div numeral (Num.Bit1 v) = (0 :: int)"

  1975     and mod_one_bit1: "1 mod numeral (Num.Bit1 v) = (1 :: int)"

  1976     and div_one_neg_numeral: "1 div - numeral v = (- 1 :: int)"

  1977     and mod_one_neg_numeral: "1 mod - numeral v = (1 :: int) - numeral v"

  1978   by (simp_all del: arith_special

  1979     add: div_pos_pos mod_pos_pos div_pos_neg mod_pos_neg posDivAlg_eqn)

  1980

  1981 lemma [simp]:

  1982   shows div_neg_one_numeral: "- 1 div numeral v = (- 1 :: int)"

  1983     and mod_neg_one_numeral: "- 1 mod numeral v = numeral v - (1 :: int)"

  1984     and div_neg_one_neg_bit0: "- 1 div - numeral (Num.Bit0 v) = (0 :: int)"

  1985     and mod_neg_one_neb_bit0: "- 1 mod - numeral (Num.Bit0 v) = (- 1 :: int)"

  1986     and div_neg_one_neg_bit1: "- 1 div - numeral (Num.Bit1 v) = (0 :: int)"

  1987     and mod_neg_one_neb_bit1: "- 1 mod - numeral (Num.Bit1 v) = (- 1 :: int)"

  1988   by (simp_all add: div_eq_minus1 zmod_minus1)

  1989

  1990

  1991 subsubsection {* Monotonicity in the First Argument (Dividend) *}

  1992

  1993 lemma zdiv_mono1: "[| a \<le> a';  0 < (b::int) |] ==> a div b \<le> a' div b"

  1994 apply (cut_tac a = a and b = b in zmod_zdiv_equality)

  1995 apply (cut_tac a = a' and b = b in zmod_zdiv_equality)

  1996 apply (rule unique_quotient_lemma)

  1997 apply (erule subst)

  1998 apply (erule subst, simp_all)

  1999 done

  2000

  2001 lemma zdiv_mono1_neg: "[| a \<le> a';  (b::int) < 0 |] ==> a' div b \<le> a div b"

  2002 apply (cut_tac a = a and b = b in zmod_zdiv_equality)

  2003 apply (cut_tac a = a' and b = b in zmod_zdiv_equality)

  2004 apply (rule unique_quotient_lemma_neg)

  2005 apply (erule subst)

  2006 apply (erule subst, simp_all)

  2007 done

  2008

  2009

  2010 subsubsection {* Monotonicity in the Second Argument (Divisor) *}

  2011

  2012 lemma q_pos_lemma:

  2013      "[| 0 \<le> b'*q' + r'; r' < b';  0 < b' |] ==> 0 \<le> (q'::int)"

  2014 apply (subgoal_tac "0 < b'* (q' + 1) ")

  2015  apply (simp add: zero_less_mult_iff)

  2016 apply (simp add: distrib_left)

  2017 done

  2018

  2019 lemma zdiv_mono2_lemma:

  2020      "[| b*q + r = b'*q' + r';  0 \<le> b'*q' + r';

  2021          r' < b';  0 \<le> r;  0 < b';  b' \<le> b |]

  2022       ==> q \<le> (q'::int)"

  2023 apply (frule q_pos_lemma, assumption+)

  2024 apply (subgoal_tac "b*q < b* (q' + 1) ")

  2025  apply (simp add: mult_less_cancel_left)

  2026 apply (subgoal_tac "b*q = r' - r + b'*q'")

  2027  prefer 2 apply simp

  2028 apply (simp (no_asm_simp) add: distrib_left)

  2029 apply (subst add.commute, rule add_less_le_mono, arith)

  2030 apply (rule mult_right_mono, auto)

  2031 done

  2032

  2033 lemma zdiv_mono2:

  2034      "[| (0::int) \<le> a;  0 < b';  b' \<le> b |] ==> a div b \<le> a div b'"

  2035 apply (subgoal_tac "b \<noteq> 0")

  2036  prefer 2 apply arith

  2037 apply (cut_tac a = a and b = b in zmod_zdiv_equality)

  2038 apply (cut_tac a = a and b = b' in zmod_zdiv_equality)

  2039 apply (rule zdiv_mono2_lemma)

  2040 apply (erule subst)

  2041 apply (erule subst, simp_all)

  2042 done

  2043

  2044 lemma q_neg_lemma:

  2045      "[| b'*q' + r' < 0;  0 \<le> r';  0 < b' |] ==> q' \<le> (0::int)"

  2046 apply (subgoal_tac "b'*q' < 0")

  2047  apply (simp add: mult_less_0_iff, arith)

  2048 done

  2049

  2050 lemma zdiv_mono2_neg_lemma:

  2051      "[| b*q + r = b'*q' + r';  b'*q' + r' < 0;

  2052          r < b;  0 \<le> r';  0 < b';  b' \<le> b |]

  2053       ==> q' \<le> (q::int)"

  2054 apply (frule q_neg_lemma, assumption+)

  2055 apply (subgoal_tac "b*q' < b* (q + 1) ")

  2056  apply (simp add: mult_less_cancel_left)

  2057 apply (simp add: distrib_left)

  2058 apply (subgoal_tac "b*q' \<le> b'*q'")

  2059  prefer 2 apply (simp add: mult_right_mono_neg, arith)

  2060 done

  2061

  2062 lemma zdiv_mono2_neg:

  2063      "[| a < (0::int);  0 < b';  b' \<le> b |] ==> a div b' \<le> a div b"

  2064 apply (cut_tac a = a and b = b in zmod_zdiv_equality)

  2065 apply (cut_tac a = a and b = b' in zmod_zdiv_equality)

  2066 apply (rule zdiv_mono2_neg_lemma)

  2067 apply (erule subst)

  2068 apply (erule subst, simp_all)

  2069 done

  2070

  2071

  2072 subsubsection {* More Algebraic Laws for div and mod *}

  2073

  2074 text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *}

  2075

  2076 lemma zmult1_lemma:

  2077      "[| divmod_int_rel b c (q, r) |]

  2078       ==> divmod_int_rel (a * b) c (a*q + a*r div c, a*r mod c)"

  2079 by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left ac_simps)

  2080

  2081 lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"

  2082 apply (case_tac "c = 0", simp)

  2083 apply (blast intro: divmod_int_rel_div_mod [THEN zmult1_lemma, THEN div_int_unique])

  2084 done

  2085

  2086 text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}

  2087

  2088 lemma zadd1_lemma:

  2089      "[| divmod_int_rel a c (aq, ar);  divmod_int_rel b c (bq, br) |]

  2090       ==> divmod_int_rel (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"

  2091 by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left)

  2092

  2093 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)

  2094 lemma zdiv_zadd1_eq:

  2095      "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"

  2096 apply (case_tac "c = 0", simp)

  2097 apply (blast intro: zadd1_lemma [OF divmod_int_rel_div_mod divmod_int_rel_div_mod] div_int_unique)

  2098 done

  2099

  2100 lemma posDivAlg_div_mod:

  2101   assumes "k \<ge> 0"

  2102   and "l \<ge> 0"

  2103   shows "posDivAlg k l = (k div l, k mod l)"

  2104 proof (cases "l = 0")

  2105   case True then show ?thesis by (simp add: posDivAlg.simps)

  2106 next

  2107   case False with assms posDivAlg_correct

  2108     have "divmod_int_rel k l (fst (posDivAlg k l), snd (posDivAlg k l))"

  2109     by simp

  2110   from div_int_unique [OF this] mod_int_unique [OF this]

  2111   show ?thesis by simp

  2112 qed

  2113

  2114 lemma negDivAlg_div_mod:

  2115   assumes "k < 0"

  2116   and "l > 0"

  2117   shows "negDivAlg k l = (k div l, k mod l)"

  2118 proof -

  2119   from assms have "l \<noteq> 0" by simp

  2120   from assms negDivAlg_correct

  2121     have "divmod_int_rel k l (fst (negDivAlg k l), snd (negDivAlg k l))"

  2122     by simp

  2123   from div_int_unique [OF this] mod_int_unique [OF this]

  2124   show ?thesis by simp

  2125 qed

  2126

  2127 lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"

  2128 by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)

  2129

  2130 (* REVISIT: should this be generalized to all semiring_div types? *)

  2131 lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]

  2132

  2133 lemma zmod_zdiv_equality':

  2134   "(m\<Colon>int) mod n = m - (m div n) * n"

  2135   using mod_div_equality [of m n] by arith

  2136

  2137

  2138 subsubsection {* Proving  @{term "a div (b * c) = (a div b) div c"} *}

  2139

  2140 (*The condition c>0 seems necessary.  Consider that 7 div ~6 = ~2 but

  2141   7 div 2 div ~3 = 3 div ~3 = ~1.  The subcase (a div b) mod c = 0 seems

  2142   to cause particular problems.*)

  2143

  2144 text{*first, four lemmas to bound the remainder for the cases b<0 and b>0 *}

  2145

  2146 lemma zmult2_lemma_aux1: "[| (0::int) < c;  b < r;  r \<le> 0 |] ==> b * c < b * (q mod c) + r"

  2147 apply (subgoal_tac "b * (c - q mod c) < r * 1")

  2148  apply (simp add: algebra_simps)

  2149 apply (rule order_le_less_trans)

  2150  apply (erule_tac [2] mult_strict_right_mono)

  2151  apply (rule mult_left_mono_neg)

  2152   using add1_zle_eq[of "q mod c"]apply(simp add: algebra_simps)

  2153  apply (simp)

  2154 apply (simp)

  2155 done

  2156

  2157 lemma zmult2_lemma_aux2:

  2158      "[| (0::int) < c;   b < r;  r \<le> 0 |] ==> b * (q mod c) + r \<le> 0"

  2159 apply (subgoal_tac "b * (q mod c) \<le> 0")

  2160  apply arith

  2161 apply (simp add: mult_le_0_iff)

  2162 done

  2163

  2164 lemma zmult2_lemma_aux3: "[| (0::int) < c;  0 \<le> r;  r < b |] ==> 0 \<le> b * (q mod c) + r"

  2165 apply (subgoal_tac "0 \<le> b * (q mod c) ")

  2166 apply arith

  2167 apply (simp add: zero_le_mult_iff)

  2168 done

  2169

  2170 lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 \<le> r; r < b |] ==> b * (q mod c) + r < b * c"

  2171 apply (subgoal_tac "r * 1 < b * (c - q mod c) ")

  2172  apply (simp add: right_diff_distrib)

  2173 apply (rule order_less_le_trans)

  2174  apply (erule mult_strict_right_mono)

  2175  apply (rule_tac [2] mult_left_mono)

  2176   apply simp

  2177  using add1_zle_eq[of "q mod c"] apply (simp add: algebra_simps)

  2178 apply simp

  2179 done

  2180

  2181 lemma zmult2_lemma: "[| divmod_int_rel a b (q, r); 0 < c |]

  2182       ==> divmod_int_rel a (b * c) (q div c, b*(q mod c) + r)"

  2183 by (auto simp add: mult.assoc divmod_int_rel_def linorder_neq_iff

  2184                    zero_less_mult_iff distrib_left [symmetric]

  2185                    zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: split_if_asm)

  2186

  2187 lemma zdiv_zmult2_eq:

  2188   fixes a b c :: int

  2189   shows "0 \<le> c \<Longrightarrow> a div (b * c) = (a div b) div c"

  2190 apply (case_tac "b = 0", simp)

  2191 apply (force simp add: le_less divmod_int_rel_div_mod [THEN zmult2_lemma, THEN div_int_unique])

  2192 done

  2193

  2194 lemma zmod_zmult2_eq:

  2195   fixes a b c :: int

  2196   shows "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"

  2197 apply (case_tac "b = 0", simp)

  2198 apply (force simp add: le_less divmod_int_rel_div_mod [THEN zmult2_lemma, THEN mod_int_unique])

  2199 done

  2200

  2201 lemma div_pos_geq:

  2202   fixes k l :: int

  2203   assumes "0 < l" and "l \<le> k"

  2204   shows "k div l = (k - l) div l + 1"

  2205 proof -

  2206   have "k = (k - l) + l" by simp

  2207   then obtain j where k: "k = j + l" ..

  2208   with assms show ?thesis by simp

  2209 qed

  2210

  2211 lemma mod_pos_geq:

  2212   fixes k l :: int

  2213   assumes "0 < l" and "l \<le> k"

  2214   shows "k mod l = (k - l) mod l"

  2215 proof -

  2216   have "k = (k - l) + l" by simp

  2217   then obtain j where k: "k = j + l" ..

  2218   with assms show ?thesis by simp

  2219 qed

  2220

  2221

  2222 subsubsection {* Splitting Rules for div and mod *}

  2223

  2224 text{*The proofs of the two lemmas below are essentially identical*}

  2225

  2226 lemma split_pos_lemma:

  2227  "0<k ==>

  2228     P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"

  2229 apply (rule iffI, clarify)

  2230  apply (erule_tac P="P ?x ?y" in rev_mp)

  2231  apply (subst mod_add_eq)

  2232  apply (subst zdiv_zadd1_eq)

  2233  apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)

  2234 txt{*converse direction*}

  2235 apply (drule_tac x = "n div k" in spec)

  2236 apply (drule_tac x = "n mod k" in spec, simp)

  2237 done

  2238

  2239 lemma split_neg_lemma:

  2240  "k<0 ==>

  2241     P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"

  2242 apply (rule iffI, clarify)

  2243  apply (erule_tac P="P ?x ?y" in rev_mp)

  2244  apply (subst mod_add_eq)

  2245  apply (subst zdiv_zadd1_eq)

  2246  apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)

  2247 txt{*converse direction*}

  2248 apply (drule_tac x = "n div k" in spec)

  2249 apply (drule_tac x = "n mod k" in spec, simp)

  2250 done

  2251

  2252 lemma split_zdiv:

  2253  "P(n div k :: int) =

  2254   ((k = 0 --> P 0) &

  2255    (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i)) &

  2256    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i)))"

  2257 apply (case_tac "k=0", simp)

  2258 apply (simp only: linorder_neq_iff)

  2259 apply (erule disjE)

  2260  apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"]

  2261                       split_neg_lemma [of concl: "%x y. P x"])

  2262 done

  2263

  2264 lemma split_zmod:

  2265  "P(n mod k :: int) =

  2266   ((k = 0 --> P n) &

  2267    (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P j)) &

  2268    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P j)))"

  2269 apply (case_tac "k=0", simp)

  2270 apply (simp only: linorder_neq_iff)

  2271 apply (erule disjE)

  2272  apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"]

  2273                       split_neg_lemma [of concl: "%x y. P y"])

  2274 done

  2275

  2276 text {* Enable (lin)arith to deal with @{const div} and @{const mod}

  2277   when these are applied to some constant that is of the form

  2278   @{term "numeral k"}: *}

  2279 declare split_zdiv [of _ _ "numeral k", arith_split] for k

  2280 declare split_zmod [of _ _ "numeral k", arith_split] for k

  2281

  2282

  2283 subsubsection {* Computing @{text "div"} and @{text "mod"} with shifting *}

  2284

  2285 lemma pos_divmod_int_rel_mult_2:

  2286   assumes "0 \<le> b"

  2287   assumes "divmod_int_rel a b (q, r)"

  2288   shows "divmod_int_rel (1 + 2*a) (2*b) (q, 1 + 2*r)"

  2289   using assms unfolding divmod_int_rel_def by auto

  2290

  2291 declaration {* K (Lin_Arith.add_simps @{thms uminus_numeral_One}) *}

  2292

  2293 lemma neg_divmod_int_rel_mult_2:

  2294   assumes "b \<le> 0"

  2295   assumes "divmod_int_rel (a + 1) b (q, r)"

  2296   shows "divmod_int_rel (1 + 2*a) (2*b) (q, 2*r - 1)"

  2297   using assms unfolding divmod_int_rel_def by auto

  2298

  2299 text{*computing div by shifting *}

  2300

  2301 lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a"

  2302   using pos_divmod_int_rel_mult_2 [OF _ divmod_int_rel_div_mod]

  2303   by (rule div_int_unique)

  2304

  2305 lemma neg_zdiv_mult_2:

  2306   assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"

  2307   using neg_divmod_int_rel_mult_2 [OF A divmod_int_rel_div_mod]

  2308   by (rule div_int_unique)

  2309

  2310 (* FIXME: add rules for negative numerals *)

  2311 lemma zdiv_numeral_Bit0 [simp]:

  2312   "numeral (Num.Bit0 v) div numeral (Num.Bit0 w) =

  2313     numeral v div (numeral w :: int)"

  2314   unfolding numeral.simps unfolding mult_2 [symmetric]

  2315   by (rule div_mult_mult1, simp)

  2316

  2317 lemma zdiv_numeral_Bit1 [simp]:

  2318   "numeral (Num.Bit1 v) div numeral (Num.Bit0 w) =

  2319     (numeral v div (numeral w :: int))"

  2320   unfolding numeral.simps

  2321   unfolding mult_2 [symmetric] add.commute [of _ 1]

  2322   by (rule pos_zdiv_mult_2, simp)

  2323

  2324 lemma pos_zmod_mult_2:

  2325   fixes a b :: int

  2326   assumes "0 \<le> a"

  2327   shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)"

  2328   using pos_divmod_int_rel_mult_2 [OF assms divmod_int_rel_div_mod]

  2329   by (rule mod_int_unique)

  2330

  2331 lemma neg_zmod_mult_2:

  2332   fixes a b :: int

  2333   assumes "a \<le> 0"

  2334   shows "(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1"

  2335   using neg_divmod_int_rel_mult_2 [OF assms divmod_int_rel_div_mod]

  2336   by (rule mod_int_unique)

  2337

  2338 (* FIXME: add rules for negative numerals *)

  2339 lemma zmod_numeral_Bit0 [simp]:

  2340   "numeral (Num.Bit0 v) mod numeral (Num.Bit0 w) =

  2341     (2::int) * (numeral v mod numeral w)"

  2342   unfolding numeral_Bit0 [of v] numeral_Bit0 [of w]

  2343   unfolding mult_2 [symmetric] by (rule mod_mult_mult1)

  2344

  2345 lemma zmod_numeral_Bit1 [simp]:

  2346   "numeral (Num.Bit1 v) mod numeral (Num.Bit0 w) =

  2347     2 * (numeral v mod numeral w) + (1::int)"

  2348   unfolding numeral_Bit1 [of v] numeral_Bit0 [of w]

  2349   unfolding mult_2 [symmetric] add.commute [of _ 1]

  2350   by (rule pos_zmod_mult_2, simp)

  2351

  2352 lemma zdiv_eq_0_iff:

  2353  "(i::int) div k = 0 \<longleftrightarrow> k=0 \<or> 0\<le>i \<and> i<k \<or> i\<le>0 \<and> k<i" (is "?L = ?R")

  2354 proof

  2355   assume ?L

  2356   have "?L \<longrightarrow> ?R" by (rule split_zdiv[THEN iffD2]) simp

  2357   with ?L show ?R by blast

  2358 next

  2359   assume ?R thus ?L

  2360     by(auto simp: div_pos_pos_trivial div_neg_neg_trivial)

  2361 qed

  2362

  2363

  2364 subsubsection {* Quotients of Signs *}

  2365

  2366 lemma div_neg_pos_less0: "[| a < (0::int);  0 < b |] ==> a div b < 0"

  2367 apply (subgoal_tac "a div b \<le> -1", force)

  2368 apply (rule order_trans)

  2369 apply (rule_tac a' = "-1" in zdiv_mono1)

  2370 apply (auto simp add: div_eq_minus1)

  2371 done

  2372

  2373 lemma div_nonneg_neg_le0: "[| (0::int) \<le> a; b < 0 |] ==> a div b \<le> 0"

  2374 by (drule zdiv_mono1_neg, auto)

  2375

  2376 lemma div_nonpos_pos_le0: "[| (a::int) \<le> 0; b > 0 |] ==> a div b \<le> 0"

  2377 by (drule zdiv_mono1, auto)

  2378

  2379 text{* Now for some equivalences of the form @{text"a div b >=< 0 \<longleftrightarrow> \<dots>"}

  2380 conditional upon the sign of @{text a} or @{text b}. There are many more.

  2381 They should all be simp rules unless that causes too much search. *}

  2382

  2383 lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)"

  2384 apply auto

  2385 apply (drule_tac [2] zdiv_mono1)

  2386 apply (auto simp add: linorder_neq_iff)

  2387 apply (simp (no_asm_use) add: linorder_not_less [symmetric])

  2388 apply (blast intro: div_neg_pos_less0)

  2389 done

  2390

  2391 lemma neg_imp_zdiv_nonneg_iff:

  2392   "b < (0::int) ==> (0 \<le> a div b) = (a \<le> (0::int))"

  2393 apply (subst div_minus_minus [symmetric])

  2394 apply (subst pos_imp_zdiv_nonneg_iff, auto)

  2395 done

  2396

  2397 (*But not (a div b \<le> 0 iff a\<le>0); consider a=1, b=2 when a div b = 0.*)

  2398 lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)"

  2399 by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff)

  2400

  2401 lemma pos_imp_zdiv_pos_iff:

  2402   "0<k \<Longrightarrow> 0 < (i::int) div k \<longleftrightarrow> k \<le> i"

  2403 using pos_imp_zdiv_nonneg_iff[of k i] zdiv_eq_0_iff[of i k]

  2404 by arith

  2405

  2406 (*Again the law fails for \<le>: consider a = -1, b = -2 when a div b = 0*)

  2407 lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)"

  2408 by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)

  2409

  2410 lemma nonneg1_imp_zdiv_pos_iff:

  2411   "(0::int) <= a \<Longrightarrow> (a div b > 0) = (a >= b & b>0)"

  2412 apply rule

  2413  apply rule

  2414   using div_pos_pos_trivial[of a b]apply arith

  2415  apply(cases "b=0")apply simp

  2416  using div_nonneg_neg_le0[of a b]apply arith

  2417 using int_one_le_iff_zero_less[of "a div b"] zdiv_mono1[of b a b]apply simp

  2418 done

  2419

  2420 lemma zmod_le_nonneg_dividend: "(m::int) \<ge> 0 ==> m mod k \<le> m"

  2421 apply (rule split_zmod[THEN iffD2])

  2422 apply(fastforce dest: q_pos_lemma intro: split_mult_pos_le)

  2423 done

  2424

  2425

  2426 subsubsection {* The Divides Relation *}

  2427

  2428 lemma dvd_neg_numeral_left [simp]:

  2429   fixes y :: "'a::comm_ring_1"

  2430   shows "(- numeral k) dvd y \<longleftrightarrow> (numeral k) dvd y"

  2431   by (fact minus_dvd_iff)

  2432

  2433 lemma dvd_neg_numeral_right [simp]:

  2434   fixes x :: "'a::comm_ring_1"

  2435   shows "x dvd (- numeral k) \<longleftrightarrow> x dvd (numeral k)"

  2436   by (fact dvd_minus_iff)

  2437

  2438 lemmas dvd_eq_mod_eq_0_numeral [simp] =

  2439   dvd_eq_mod_eq_0 [of "numeral x" "numeral y"] for x y

  2440

  2441

  2442 subsubsection {* Further properties *}

  2443

  2444 lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"

  2445   using zmod_zdiv_equality[where a="m" and b="n"]

  2446   by (simp add: algebra_simps) (* FIXME: generalize *)

  2447

  2448 lemma zdiv_int: "int (a div b) = (int a) div (int b)"

  2449 apply (subst split_div, auto)

  2450 apply (subst split_zdiv, auto)

  2451 apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in unique_quotient)

  2452 apply (auto simp add: divmod_int_rel_def of_nat_mult)

  2453 done

  2454

  2455 lemma zmod_int: "int (a mod b) = (int a) mod (int b)"

  2456 apply (subst split_mod, auto)

  2457 apply (subst split_zmod, auto)

  2458 apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia

  2459        in unique_remainder)

  2460 apply (auto simp add: divmod_int_rel_def of_nat_mult)

  2461 done

  2462

  2463 lemma abs_div: "(y::int) dvd x \<Longrightarrow> abs (x div y) = abs x div abs y"

  2464 by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)

  2465

  2466 text{*Suggested by Matthias Daum*}

  2467 lemma int_power_div_base:

  2468      "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"

  2469 apply (subgoal_tac "k ^ m = k ^ ((m - Suc 0) + Suc 0)")

  2470  apply (erule ssubst)

  2471  apply (simp only: power_add)

  2472  apply simp_all

  2473 done

  2474

  2475 text {* by Brian Huffman *}

  2476 lemma zminus_zmod: "- ((x::int) mod m) mod m = - x mod m"

  2477 by (rule mod_minus_eq [symmetric])

  2478

  2479 lemma zdiff_zmod_left: "(x mod m - y) mod m = (x - y) mod (m::int)"

  2480 by (rule mod_diff_left_eq [symmetric])

  2481

  2482 lemma zdiff_zmod_right: "(x - y mod m) mod m = (x - y) mod (m::int)"

  2483 by (rule mod_diff_right_eq [symmetric])

  2484

  2485 lemmas zmod_simps =

  2486   mod_add_left_eq  [symmetric]

  2487   mod_add_right_eq [symmetric]

  2488   mod_mult_right_eq[symmetric]

  2489   mod_mult_left_eq [symmetric]

  2490   power_mod

  2491   zminus_zmod zdiff_zmod_left zdiff_zmod_right

  2492

  2493 text {* Distributive laws for function @{text nat}. *}

  2494

  2495 lemma nat_div_distrib: "0 \<le> x \<Longrightarrow> nat (x div y) = nat x div nat y"

  2496 apply (rule linorder_cases [of y 0])

  2497 apply (simp add: div_nonneg_neg_le0)

  2498 apply simp

  2499 apply (simp add: nat_eq_iff pos_imp_zdiv_nonneg_iff zdiv_int)

  2500 done

  2501

  2502 (*Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't*)

  2503 lemma nat_mod_distrib:

  2504   "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x mod y) = nat x mod nat y"

  2505 apply (case_tac "y = 0", simp)

  2506 apply (simp add: nat_eq_iff zmod_int)

  2507 done

  2508

  2509 text  {* transfer setup *}

  2510

  2511 lemma transfer_nat_int_functions:

  2512     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"

  2513     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"

  2514   by (auto simp add: nat_div_distrib nat_mod_distrib)

  2515

  2516 lemma transfer_nat_int_function_closures:

  2517     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"

  2518     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"

  2519   apply (cases "y = 0")

  2520   apply (auto simp add: pos_imp_zdiv_nonneg_iff)

  2521   apply (cases "y = 0")

  2522   apply auto

  2523 done

  2524

  2525 declare transfer_morphism_nat_int [transfer add return:

  2526   transfer_nat_int_functions

  2527   transfer_nat_int_function_closures

  2528 ]

  2529

  2530 lemma transfer_int_nat_functions:

  2531     "(int x) div (int y) = int (x div y)"

  2532     "(int x) mod (int y) = int (x mod y)"

  2533   by (auto simp add: zdiv_int zmod_int)

  2534

  2535 lemma transfer_int_nat_function_closures:

  2536     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"

  2537     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"

  2538   by (simp_all only: is_nat_def transfer_nat_int_function_closures)

  2539

  2540 declare transfer_morphism_int_nat [transfer add return:

  2541   transfer_int_nat_functions

  2542   transfer_int_nat_function_closures

  2543 ]

  2544

  2545 text{*Suggested by Matthias Daum*}

  2546 lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"

  2547 apply (subgoal_tac "nat x div nat k < nat x")

  2548  apply (simp add: nat_div_distrib [symmetric])

  2549 apply (rule Divides.div_less_dividend, simp_all)

  2550 done

  2551

  2552 lemma zmod_eq_dvd_iff: "(x::int) mod n = y mod n \<longleftrightarrow> n dvd x - y"

  2553 proof

  2554   assume H: "x mod n = y mod n"

  2555   hence "x mod n - y mod n = 0" by simp

  2556   hence "(x mod n - y mod n) mod n = 0" by simp

  2557   hence "(x - y) mod n = 0" by (simp add: mod_diff_eq[symmetric])

  2558   thus "n dvd x - y" by (simp add: dvd_eq_mod_eq_0)

  2559 next

  2560   assume H: "n dvd x - y"

  2561   then obtain k where k: "x-y = n*k" unfolding dvd_def by blast

  2562   hence "x = n*k + y" by simp

  2563   hence "x mod n = (n*k + y) mod n" by simp

  2564   thus "x mod n = y mod n" by (simp add: mod_add_left_eq)

  2565 qed

  2566

  2567 lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y  mod n" and xy:"y \<le> x"

  2568   shows "\<exists>q. x = y + n * q"

  2569 proof-

  2570   from xy have th: "int x - int y = int (x - y)" by simp

  2571   from xyn have "int x mod int n = int y mod int n"

  2572     by (simp add: zmod_int [symmetric])

  2573   hence "int n dvd int x - int y" by (simp only: zmod_eq_dvd_iff[symmetric])

  2574   hence "n dvd x - y" by (simp add: th zdvd_int)

  2575   then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith

  2576 qed

  2577

  2578 lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)"

  2579   (is "?lhs = ?rhs")

  2580 proof

  2581   assume H: "x mod n = y mod n"

  2582   {assume xy: "x \<le> y"

  2583     from H have th: "y mod n = x mod n" by simp

  2584     from nat_mod_eq_lemma[OF th xy] have ?rhs

  2585       apply clarify  apply (rule_tac x="q" in exI) by (rule exI[where x="0"], simp)}

  2586   moreover

  2587   {assume xy: "y \<le> x"

  2588     from nat_mod_eq_lemma[OF H xy] have ?rhs

  2589       apply clarify  apply (rule_tac x="0" in exI) by (rule_tac x="q" in exI, simp)}

  2590   ultimately  show ?rhs using linear[of x y] by blast

  2591 next

  2592   assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast

  2593   hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp

  2594   thus  ?lhs by simp

  2595 qed

  2596

  2597 text {*

  2598   This re-embedding of natural division on integers goes back to the

  2599   time when numerals had been signed numerals.  It should

  2600   now be replaced by the algorithm developed in @{class semiring_numeral_div}.

  2601 *}

  2602

  2603 lemma div_nat_numeral [simp]:

  2604   "(numeral v :: nat) div numeral v' = nat (numeral v div numeral v')"

  2605   by (simp add: nat_div_distrib)

  2606

  2607 lemma one_div_nat_numeral [simp]:

  2608   "Suc 0 div numeral v' = nat (1 div numeral v')"

  2609   by (subst nat_div_distrib, simp_all)

  2610

  2611 lemma mod_nat_numeral [simp]:

  2612   "(numeral v :: nat) mod numeral v' = nat (numeral v mod numeral v')"

  2613   by (simp add: nat_mod_distrib)

  2614

  2615 lemma one_mod_nat_numeral [simp]:

  2616   "Suc 0 mod numeral v' = nat (1 mod numeral v')"

  2617   by (subst nat_mod_distrib) simp_all

  2618

  2619 instance int :: semiring_numeral_div

  2620   by intro_classes (auto intro: zmod_le_nonneg_dividend

  2621     simp add: zmult_div_cancel

  2622     pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial

  2623     zmod_zmult2_eq zdiv_zmult2_eq)

  2624

  2625

  2626 subsubsection {* Tools setup *}

  2627

  2628 text {* Nitpick *}

  2629

  2630 lemmas [nitpick_unfold] = dvd_eq_mod_eq_0 mod_div_equality' zmod_zdiv_equality'

  2631

  2632

  2633 subsubsection {* Code generation *}

  2634

  2635 definition divmod_abs :: "int \<Rightarrow> int \<Rightarrow> int \<times> int"

  2636 where

  2637   "divmod_abs k l = (\<bar>k\<bar> div \<bar>l\<bar>, \<bar>k\<bar> mod \<bar>l\<bar>)"

  2638

  2639 lemma fst_divmod_abs [simp]:

  2640   "fst (divmod_abs k l) = \<bar>k\<bar> div \<bar>l\<bar>"

  2641   by (simp add: divmod_abs_def)

  2642

  2643 lemma snd_divmod_abs [simp]:

  2644   "snd (divmod_abs k l) = \<bar>k\<bar> mod \<bar>l\<bar>"

  2645   by (simp add: divmod_abs_def)

  2646

  2647 lemma divmod_abs_code [code]:

  2648   "divmod_abs (Int.Pos k) (Int.Pos l) = divmod k l"

  2649   "divmod_abs (Int.Neg k) (Int.Neg l) = divmod k l"

  2650   "divmod_abs (Int.Neg k) (Int.Pos l) = divmod k l"

  2651   "divmod_abs (Int.Pos k) (Int.Neg l) = divmod k l"

  2652   "divmod_abs j 0 = (0, \<bar>j\<bar>)"

  2653   "divmod_abs 0 j = (0, 0)"

  2654   by (simp_all add: prod_eq_iff)

  2655

  2656 lemma divmod_int_divmod_abs:

  2657   "divmod_int k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else

  2658   apsnd ((op *) (sgn l)) (if 0 < l \<and> 0 \<le> k \<or> l < 0 \<and> k < 0

  2659     then divmod_abs k l

  2660     else (let (r, s) = divmod_abs k l in

  2661        if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"

  2662 proof -

  2663   have aux: "\<And>q::int. - k = l * q \<longleftrightarrow> k = l * - q" by auto

  2664   show ?thesis

  2665     by (simp add: prod_eq_iff split_def Let_def)

  2666       (auto simp add: aux not_less not_le zdiv_zminus1_eq_if

  2667       zmod_zminus1_eq_if zdiv_zminus2_eq_if zmod_zminus2_eq_if)

  2668 qed

  2669

  2670 lemma divmod_int_code [code]:

  2671   "divmod_int k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else

  2672   apsnd ((op *) (sgn l)) (if sgn k = sgn l

  2673     then divmod_abs k l

  2674     else (let (r, s) = divmod_abs k l in

  2675       if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"

  2676 proof -

  2677   have "k \<noteq> 0 \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> 0 < l \<and> 0 \<le> k \<or> l < 0 \<and> k < 0 \<longleftrightarrow> sgn k = sgn l"

  2678     by (auto simp add: not_less sgn_if)

  2679   then show ?thesis by (simp add: divmod_int_divmod_abs)

  2680 qed

  2681

  2682 hide_const (open) divmod_abs

  2683

  2684 code_identifier

  2685   code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith

  2686

  2687 end

  2688
`