src/HOL/Divides.thy
 author wenzelm Tue Sep 03 01:12:40 2013 +0200 (2013-09-03) changeset 53374 a14d2a854c02 parent 53199 7a9fe70c8b0a child 54221 56587960e444 permissions -rw-r--r--
tuned proofs -- clarified flow of facts wrt. calculation;
     1 (*  Title:      HOL/Divides.thy

     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

     3     Copyright   1999  University of Cambridge

     4 *)

     5

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

     7

     8 theory Divides

     9 imports Nat_Transfer

    10 begin

    11

    12 subsection {* Syntactic division operations *}

    13

    14 class div = dvd +

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

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

    17

    18

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

    20

    21 class semiring_div = comm_semiring_1_cancel + no_zero_divisors + div +

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

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

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

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

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

    27 begin

    28

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

    30

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

    32   unfolding mult_commute [of b]

    33   by (rule mod_div_equality)

    34

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

    36   using mod_div_equality [of a b]

    37   by (simp only: add_ac)

    38

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

    40   by (simp add: mod_div_equality)

    41

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

    43   by (simp add: mod_div_equality2)

    44

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

    46   using mod_div_equality [of a zero] by simp

    47

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

    49   using mod_div_equality [of zero a] div_0 by simp

    50

    51 lemma div_mult_self2 [simp]:

    52   assumes "b \<noteq> 0"

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

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

    55

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

    57 proof (cases "b = 0")

    58   case True then show ?thesis by simp

    59 next

    60   case False

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

    62     by (simp add: mod_div_equality)

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

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

    65       by (simp add: algebra_simps)

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

    67     by (simp add: add_commute [of a] add_assoc distrib_right)

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

    69     by (simp add: mod_div_equality)

    70   then show ?thesis by simp

    71 qed

    72

    73 lemma mod_mult_self2 [simp]: "(a + b * c) mod b = a mod b"

    74   by (simp add: mult_commute [of b])

    75

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

    77   using div_mult_self2 [of b 0 a] by simp

    78

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

    80   using div_mult_self1 [of b 0 a] by simp

    81

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

    83   using mod_mult_self2 [of 0 b a] by simp

    84

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

    86   using mod_mult_self1 [of 0 a b] by simp

    87

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

    89   using div_mult_self2_is_id [of 1 a] zero_neq_one by simp

    90

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

    92 proof -

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

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

    95   then show ?thesis by (rule add_left_imp_eq)

    96 qed

    97

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

    99   using mod_mult_self2_is_0 [of 1] by simp

   100

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

   102   using div_mult_self2_is_id [of _ 1] by simp

   103

   104 lemma div_add_self1 [simp]:

   105   assumes "b \<noteq> 0"

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

   107   using assms div_mult_self1 [of b a 1] by (simp add: add_commute)

   108

   109 lemma div_add_self2 [simp]:

   110   assumes "b \<noteq> 0"

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

   112   using assms div_add_self1 [of b a] by (simp add: add_commute)

   113

   114 lemma mod_add_self1 [simp]:

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

   116   using mod_mult_self1 [of a 1 b] by (simp add: add_commute)

   117

   118 lemma mod_add_self2 [simp]:

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

   120   using mod_mult_self1 [of a 1 b] by simp

   121

   122 lemma mod_div_decomp:

   123   fixes a b

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

   125     and "a = q * b + r"

   126 proof -

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

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

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

   130   note that ultimately show thesis by blast

   131 qed

   132

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

   134 proof

   135   assume "b mod a = 0"

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

   137   then have "b = a * (b div a)" unfolding mult_commute ..

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

   139   then show "a dvd b" unfolding dvd_def .

   140 next

   141   assume "a dvd b"

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

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

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

   145   then have "b mod a = c * a mod a" by (simp add: mult_commute)

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

   147 qed

   148

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

   150 proof (cases "b = 0")

   151   assume "b = 0"

   152   thus ?thesis by simp

   153 next

   154   assume "b \<noteq> 0"

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

   156     by (rule div_mult_self1 [symmetric])

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

   158     by (simp only: mod_div_equality')

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

   160     by simp

   161   finally show ?thesis

   162     by (rule add_left_imp_eq)

   163 qed

   164

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

   166 proof -

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

   168     by (simp only: mod_mult_self1)

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

   170     by (simp only: mod_div_equality')

   171   finally show ?thesis .

   172 qed

   173

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

   175 by (rule dvd_eq_mod_eq_0[THEN iffD1])

   176

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

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

   179

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

   181 by (drule dvd_div_mult_self) (simp add: mult_commute)

   182

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

   184 apply (cases "a = 0")

   185  apply simp

   186 apply (auto simp: dvd_def mult_assoc)

   187 done

   188

   189 lemma div_dvd_div[simp]:

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

   191 apply (cases "a = 0")

   192  apply simp

   193 apply (unfold dvd_def)

   194 apply auto

   195  apply(blast intro:mult_assoc[symmetric])

   196 apply(fastforce simp add: mult_assoc)

   197 done

   198

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

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

   201    apply (simp add: mod_div_equality)

   202   apply (simp only: dvd_add dvd_mult)

   203   done

   204

   205 text {* Addition respects modular equivalence. *}

   206

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

   208 proof -

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

   210     by (simp only: mod_div_equality)

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

   212     by (simp only: add_ac)

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

   214     by (rule mod_mult_self1)

   215   finally show ?thesis .

   216 qed

   217

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

   219 proof -

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

   221     by (simp only: mod_div_equality)

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

   223     by (simp only: add_ac)

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

   225     by (rule mod_mult_self1)

   226   finally show ?thesis .

   227 qed

   228

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

   230 by (rule trans [OF mod_add_left_eq mod_add_right_eq])

   231

   232 lemma mod_add_cong:

   233   assumes "a mod c = a' mod c"

   234   assumes "b mod c = b' mod c"

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

   236 proof -

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

   238     unfolding assms ..

   239   thus ?thesis

   240     by (simp only: mod_add_eq [symmetric])

   241 qed

   242

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

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

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

   246

   247 text {* Multiplication respects modular equivalence. *}

   248

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

   250 proof -

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

   252     by (simp only: mod_div_equality)

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

   254     by (simp only: algebra_simps)

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

   256     by (rule mod_mult_self1)

   257   finally show ?thesis .

   258 qed

   259

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

   261 proof -

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

   263     by (simp only: mod_div_equality)

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

   265     by (simp only: algebra_simps)

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

   267     by (rule mod_mult_self1)

   268   finally show ?thesis .

   269 qed

   270

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

   272 by (rule trans [OF mod_mult_left_eq mod_mult_right_eq])

   273

   274 lemma mod_mult_cong:

   275   assumes "a mod c = a' mod c"

   276   assumes "b mod c = b' mod c"

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

   278 proof -

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

   280     unfolding assms ..

   281   thus ?thesis

   282     by (simp only: mod_mult_eq [symmetric])

   283 qed

   284

   285 text {* Exponentiation respects modular equivalence. *}

   286

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

   288 apply (induct n, simp_all)

   289 apply (rule mod_mult_right_eq [THEN trans])

   290 apply (simp (no_asm_simp))

   291 apply (rule mod_mult_eq [symmetric])

   292 done

   293

   294 lemma mod_mod_cancel:

   295   assumes "c dvd b"

   296   shows "a mod b mod c = a mod c"

   297 proof -

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

   299     by (rule dvdE)

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

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

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

   303     by (simp only: mod_mult_self1)

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

   305     by (simp only: add_ac mult_ac)

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

   307     by (simp only: mod_div_equality)

   308   finally show ?thesis .

   309 qed

   310

   311 lemma div_mult_div_if_dvd:

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

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

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

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

   316   apply (subst mult_assoc [symmetric])

   317   apply (simp add: no_zero_divisors)

   318   done

   319

   320 lemma div_mult_swap:

   321   assumes "c dvd b"

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

   323 proof -

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

   325     by (simp only: div_mult_div_if_dvd one_dvd)

   326   then show ?thesis by (simp add: mult_commute)

   327 qed

   328

   329 lemma div_mult_mult2 [simp]:

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

   331   by (drule div_mult_mult1) (simp add: mult_commute)

   332

   333 lemma div_mult_mult1_if [simp]:

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

   335   by simp_all

   336

   337 lemma mod_mult_mult1:

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

   339 proof (cases "c = 0")

   340   case True then show ?thesis by simp

   341 next

   342   case False

   343   from mod_div_equality

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

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

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

   347   with mod_div_equality show ?thesis by simp

   348 qed

   349

   350 lemma mod_mult_mult2:

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

   352   using mod_mult_mult1 [of c a b] by (simp add: mult_commute)

   353

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

   355   by (fact mod_mult_mult2 [symmetric])

   356

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

   358   by (fact mod_mult_mult1 [symmetric])

   359

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

   361   unfolding dvd_def by (auto simp add: mod_mult_mult1)

   362

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

   364 by (blast intro: dvd_mod_imp_dvd dvd_mod)

   365

   366 lemma div_power:

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

   368 apply (induct n)

   369  apply simp

   370 apply(simp add: div_mult_div_if_dvd dvd_power_same)

   371 done

   372

   373 lemma dvd_div_eq_mult:

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

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

   376 proof

   377   assume "b = c * a"

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

   379 next

   380   assume "b div a = c"

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

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

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

   384 qed

   385

   386 lemma dvd_div_div_eq_mult:

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

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

   389   using assms by (auto simp add: mult_commute [of _ a] dvd_div_mult_self dvd_div_eq_mult div_mult_swap intro: sym)

   390

   391 end

   392

   393 class ring_div = semiring_div + comm_ring_1

   394 begin

   395

   396 subclass ring_1_no_zero_divisors ..

   397

   398 text {* Negation respects modular equivalence. *}

   399

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

   401 proof -

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

   403     by (simp only: mod_div_equality)

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

   405     by (simp only: minus_add_distrib minus_mult_left add_ac)

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

   407     by (rule mod_mult_self1)

   408   finally show ?thesis .

   409 qed

   410

   411 lemma mod_minus_cong:

   412   assumes "a mod b = a' mod b"

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

   414 proof -

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

   416     unfolding assms ..

   417   thus ?thesis

   418     by (simp only: mod_minus_eq [symmetric])

   419 qed

   420

   421 text {* Subtraction respects modular equivalence. *}

   422

   423 lemma mod_diff_left_eq: "(a - b) mod c = (a mod c - b) mod c"

   424   unfolding diff_minus

   425   by (intro mod_add_cong mod_minus_cong) simp_all

   426

   427 lemma mod_diff_right_eq: "(a - b) mod c = (a - b mod c) mod c"

   428   unfolding diff_minus

   429   by (intro mod_add_cong mod_minus_cong) simp_all

   430

   431 lemma mod_diff_eq: "(a - b) mod c = (a mod c - b mod c) mod c"

   432   unfolding diff_minus

   433   by (intro mod_add_cong mod_minus_cong) simp_all

   434

   435 lemma mod_diff_cong:

   436   assumes "a mod c = a' mod c"

   437   assumes "b mod c = b' mod c"

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

   439   unfolding diff_minus using assms

   440   by (intro mod_add_cong mod_minus_cong)

   441

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

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

   444 apply (auto simp add: dvd_def)

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

   446  apply (erule ssubst)

   447  apply (erule div_mult_self1_is_id)

   448 apply simp

   449 done

   450

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

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

   453 apply (auto simp add: dvd_def)

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

   455  apply (erule ssubst)

   456  apply (rule div_mult_self1_is_id)

   457  apply simp

   458 apply simp

   459 done

   460

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

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

   463   unfolding neg_equal_0_iff_equal by simp

   464

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

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

   467

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

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

   470

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

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

   473

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

   475   using div_minus_right [of a 1] by simp

   476

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

   478   using mod_minus_right [of a 1] by simp

   479

   480 end

   481

   482

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

   484

   485 text {*

   486   The following type class contains everything necessary to formulate

   487   a division algorithm in ring structures with numerals, restricted

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

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

   490   and less technical class hierarchy.

   491 *}

   492

   493

   494 class semiring_numeral_div = linordered_semidom + minus + semiring_div +

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

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

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

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

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

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

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

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

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

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

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

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

   507 begin

   508

   509 lemma diff_zero [simp]:

   510   "a - 0 = a"

   511   by (rule diff_invert_add1 [symmetric]) simp

   512

   513 lemma parity:

   514   "a mod 2 = 0 \<or> a mod 2 = 1"

   515 proof (rule ccontr)

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

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

   518   have "0 < 2" by simp

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

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

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

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

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

   524   with a mod 2 < 2 show False by simp

   525 qed

   526

   527 lemma divmod_digit_1:

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

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

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

   531 proof -

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

   533     by (auto intro: trans)

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

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

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

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

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

   539     by (simp add: w_def mod_mult2_eq ac_simps)

   540   from assms w_exhaust have "w = 1"

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

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

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

   544     by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)

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

   546   then show ?P and ?Q

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

   548 qed

   549

   550 lemma divmod_digit_0:

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

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

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

   554 proof -

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

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

   557     by (simp add: w_def mod_mult2_eq ac_simps)

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

   559   proof -

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

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

   562     then show ?thesis by simp

   563   qed

   564   moreover note assms w_exhaust

   565   ultimately have "w = 0" by auto

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

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

   568     by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)

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

   570   then show ?P and ?Q

   571     by (simp_all add: div mod)

   572 qed

   573

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

   575 where

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

   577

   578 lemma fst_divmod [simp]:

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

   580   by (simp add: divmod_def)

   581

   582 lemma snd_divmod [simp]:

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

   584   by (simp add: divmod_def)

   585

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

   587 where

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

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

   590     else (2 * q, r))"

   591

   592 text {*

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

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

   595   digit position with the remainder from previous division steps

   596   and evaluate accordingly.

   597 *}

   598

   599 lemma divmod_step_eq [code]:

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

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

   602   by (simp add: divmod_step_def)

   603

   604 lemma divmod_step_simps [simp]:

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

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

   607   by (auto simp add: divmod_step_eq not_le)

   608

   609 text {*

   610   This is a formulation of school-method division.

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

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

   613   occurs and then reiterate single division steps in the

   614   opposite direction.

   615 *}

   616

   617 lemma divmod_divmod_step [code]:

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

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

   620 proof (cases "m < n")

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

   622   then show ?thesis

   623     by (simp add: prod_eq_iff div_less mod_less)

   624 next

   625   case False

   626   have "divmod m n =

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

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

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

   630     case True

   631     with divmod_step_simps

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

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

   634         by blast

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

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

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

   638       by simp_all

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

   640   next

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

   642       by (simp add: not_le)

   643     with divmod_step_simps

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

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

   646         by blast

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

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

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

   650       by (simp_all only: zero_less_numeral)

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

   652   qed

   653   then have "divmod m n =

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

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

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

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

   658     by (simp add: divmod_def)

   659   with False show ?thesis by simp

   660 qed

   661

   662 lemma divmod_cancel [code]:

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

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

   665 proof -

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

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

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

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

   670   then show ?P and ?Q

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

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

   673  qed

   674

   675 end

   676

   677 hide_fact (open) diff_invert_add1 le_add_diff_inverse2 diff_zero

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

   679

   680

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

   682

   683 text {*

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

   685   of a characteristic relation with two input arguments

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

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

   688 *}

   689

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

   691   "divmod_nat_rel m n qr \<longleftrightarrow>

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

   693       (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)"

   694

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

   696

   697 lemma divmod_nat_rel_ex:

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

   699 proof (cases "n = 0")

   700   case True  with that show thesis

   701     by (auto simp add: divmod_nat_rel_def)

   702 next

   703   case False

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

   705   proof (induct m)

   706     case 0 with n \<noteq> 0

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

   708     then show ?case by blast

   709   next

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

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

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

   713       case True

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

   715       with True show ?thesis by blast

   716     next

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

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

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

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

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

   722     qed

   723   qed

   724   with that show thesis

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

   726 qed

   727

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

   729

   730 lemma divmod_nat_rel_unique:

   731   assumes "divmod_nat_rel m n qr"

   732     and "divmod_nat_rel m n qr'"

   733   shows "qr = qr'"

   734 proof (cases "n = 0")

   735   case True with assms show ?thesis

   736     by (cases qr, cases qr')

   737       (simp add: divmod_nat_rel_def)

   738 next

   739   case False

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

   741   apply (rule leI)

   742   apply (subst less_iff_Suc_add)

   743   apply (auto simp add: add_mult_distrib)

   744   done

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

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

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

   748     by (simp add: divmod_nat_rel_def)

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

   750 qed

   751

   752 text {*

   753   We instantiate divisibility on the natural numbers by

   754   means of @{const divmod_nat_rel}:

   755 *}

   756

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

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

   759

   760 lemma divmod_nat_rel_divmod_nat:

   761   "divmod_nat_rel m n (divmod_nat m n)"

   762 proof -

   763   from divmod_nat_rel_ex

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

   765   then show ?thesis

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

   767 qed

   768

   769 lemma divmod_nat_unique:

   770   assumes "divmod_nat_rel m n qr"

   771   shows "divmod_nat m n = qr"

   772   using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)

   773

   774 instantiation nat :: semiring_div

   775 begin

   776

   777 definition div_nat where

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

   779

   780 lemma fst_divmod_nat [simp]:

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

   782   by (simp add: div_nat_def)

   783

   784 definition mod_nat where

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

   786

   787 lemma snd_divmod_nat [simp]:

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

   789   by (simp add: mod_nat_def)

   790

   791 lemma divmod_nat_div_mod:

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

   793   by (simp add: prod_eq_iff)

   794

   795 lemma div_nat_unique:

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

   797   shows "m div n = q"

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

   799

   800 lemma mod_nat_unique:

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

   802   shows "m mod n = r"

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

   804

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

   806   using divmod_nat_rel_divmod_nat by (simp add: divmod_nat_div_mod)

   807

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

   809   by (simp add: divmod_nat_unique divmod_nat_rel_def)

   810

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

   812   by (simp add: divmod_nat_unique divmod_nat_rel_def)

   813

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

   815   by (simp add: divmod_nat_unique divmod_nat_rel_def)

   816

   817 lemma divmod_nat_step:

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

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

   820 proof (rule divmod_nat_unique)

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

   822     by (rule divmod_nat_rel)

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

   824     unfolding divmod_nat_rel_def using assms by auto

   825 qed

   826

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

   828

   829 lemma div_less [simp]:

   830   fixes m n :: nat

   831   assumes "m < n"

   832   shows "m div n = 0"

   833   using assms divmod_nat_base by (simp add: prod_eq_iff)

   834

   835 lemma le_div_geq:

   836   fixes m n :: nat

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

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

   839   using assms divmod_nat_step by (simp add: prod_eq_iff)

   840

   841 lemma mod_less [simp]:

   842   fixes m n :: nat

   843   assumes "m < n"

   844   shows "m mod n = m"

   845   using assms divmod_nat_base by (simp add: prod_eq_iff)

   846

   847 lemma le_mod_geq:

   848   fixes m n :: nat

   849   assumes "n \<le> m"

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

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

   852

   853 instance proof

   854   fix m n :: nat

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

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

   857 next

   858   fix m n q :: nat

   859   assume "n \<noteq> 0"

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

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

   862 next

   863   fix m n q :: nat

   864   assume "m \<noteq> 0"

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

   866     unfolding divmod_nat_rel_def

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

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

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

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

   871 next

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

   873     by (simp add: div_nat_def divmod_nat_zero)

   874 next

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

   876     by (simp add: div_nat_def divmod_nat_zero_left)

   877 qed

   878

   879 end

   880

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

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

   883   by (simp add: prod_eq_iff prod_case_beta not_less le_div_geq le_mod_geq)

   884

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

   886

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

   888

   889 ML {*

   890 structure Cancel_Div_Mod_Nat = Cancel_Div_Mod

   891 (

   892   val div_name = @{const_name div};

   893   val mod_name = @{const_name mod};

   894   val mk_binop = HOLogic.mk_binop;

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

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

   897   fun mk_sum [] = HOLogic.zero

   898     | mk_sum [t] = t

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

   900   fun dest_sum tm =

   901     if HOLogic.is_zero tm then []

   902     else

   903       (case try HOLogic.dest_Suc tm of

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

   905       | NONE =>

   906           (case try dest_plus tm of

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

   908           | NONE => [tm]));

   909

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

   911

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

   913     (@{thm add_0_left} :: @{thm add_0_right} :: @{thms add_ac}))

   914 )

   915 *}

   916

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

   918

   919

   920 subsubsection {* Quotient *}

   921

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

   923 by (simp add: le_div_geq linorder_not_less)

   924

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

   926 by (simp add: div_geq)

   927

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

   929 by simp

   930

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

   932 by simp

   933

   934 lemma div_positive:

   935   fixes m n :: nat

   936   assumes "n > 0"

   937   assumes "m \<ge> n"

   938   shows "m div n > 0"

   939 proof -

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

   941     by (auto simp add: le_iff_add)

   942   with n > 0 show ?thesis by simp

   943 qed

   944

   945

   946 subsubsection {* Remainder *}

   947

   948 lemma mod_less_divisor [simp]:

   949   fixes m n :: nat

   950   assumes "n > 0"

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

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

   953

   954 lemma mod_Suc_le_divisor [simp]:

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

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

   957

   958 lemma mod_less_eq_dividend [simp]:

   959   fixes m n :: nat

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

   961 proof (rule add_leD2)

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

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

   964 qed

   965

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

   967 by (simp add: le_mod_geq linorder_not_less)

   968

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

   970 by (simp add: le_mod_geq)

   971

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

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

   974

   975 (* a simple rearrangement of mod_div_equality: *)

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

   977   using mod_div_equality2 [of n m] by arith

   978

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

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

   981   apply simp

   982   done

   983

   984 subsubsection {* Quotient and Remainder *}

   985

   986 lemma divmod_nat_rel_mult1_eq:

   987   "divmod_nat_rel b c (q, r)

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

   989 by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps)

   990

   991 lemma div_mult1_eq:

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

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

   994

   995 lemma divmod_nat_rel_add1_eq:

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

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

   998 by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps)

   999

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

  1001 lemma div_add1_eq:

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

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

  1004

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

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

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

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

  1009   apply (simp add: add_mult_distrib2)

  1010   done

  1011

  1012 lemma divmod_nat_rel_mult2_eq:

  1013   "divmod_nat_rel a b (q, r)

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

  1015 by (auto simp add: mult_ac divmod_nat_rel_def add_mult_distrib2 [symmetric] mod_lemma)

  1016

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

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

  1019

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

  1021 by (auto simp add: mult_commute divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN mod_nat_unique])

  1022

  1023

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

  1025

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

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

  1028

  1029 (* Monotonicity of div in first argument *)

  1030 lemma div_le_mono [rule_format (no_asm)]:

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

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

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

  1034 apply (case_tac "n<k")

  1035 (* 1  case n<k *)

  1036 apply simp

  1037 (* 2  case n >= k *)

  1038 apply (case_tac "m<k")

  1039 (* 2.1  case m<k *)

  1040 apply simp

  1041 (* 2.2  case m>=k *)

  1042 apply (simp add: div_geq diff_le_mono)

  1043 done

  1044

  1045 (* Antimonotonicity of div in second argument *)

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

  1047 apply (subgoal_tac "0<n")

  1048  prefer 2 apply simp

  1049 apply (induct_tac k rule: nat_less_induct)

  1050 apply (rename_tac "k")

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

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

  1053  prefer 2 apply simp

  1054 apply (simp add: div_geq)

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

  1056  prefer 2

  1057  apply (blast intro: div_le_mono diff_le_mono2)

  1058 apply (rule le_trans, simp)

  1059 apply (simp)

  1060 done

  1061

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

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

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

  1065 apply (rule div_le_mono2)

  1066 apply (simp_all (no_asm_simp))

  1067 done

  1068

  1069 (* Similar for "less than" *)

  1070 lemma div_less_dividend [simp]:

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

  1072 apply (induct m rule: nat_less_induct)

  1073 apply (rename_tac "m")

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

  1075 apply (subgoal_tac "0<n")

  1076  prefer 2 apply simp

  1077 apply (simp add: div_geq)

  1078 apply (case_tac "n<m")

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

  1080   apply (rule impI less_trans_Suc)+

  1081 apply assumption

  1082   apply (simp_all)

  1083 done

  1084

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

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

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

  1088 apply (induct "m" rule: nat_less_induct)

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

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

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

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

  1093 apply (simp add: linorder_not_less le_Suc_eq mod_geq)

  1094 apply (auto simp add: Suc_diff_le le_mod_geq)

  1095 done

  1096

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

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

  1099

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

  1101

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

  1103 lemma mod_eqD: "(m mod d = r) ==> \<exists>q::nat. m = r + q*d"

  1104   apply (cut_tac a = m in mod_div_equality)

  1105   apply (simp only: add_ac)

  1106   apply (blast intro: sym)

  1107   done

  1108

  1109 lemma split_div:

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

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

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

  1113 proof

  1114   assume P: ?P

  1115   show ?Q

  1116   proof (cases)

  1117     assume "k = 0"

  1118     with P show ?Q by simp

  1119   next

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

  1121     thus ?Q

  1122     proof (simp, intro allI impI)

  1123       fix i j

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

  1125       show "P i"

  1126       proof (cases)

  1127         assume "i = 0"

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

  1129       next

  1130         assume "i \<noteq> 0"

  1131         with not0 n j P show "P i" by(simp add:add_ac)

  1132       qed

  1133     qed

  1134   qed

  1135 next

  1136   assume Q: ?Q

  1137   show ?P

  1138   proof (cases)

  1139     assume "k = 0"

  1140     with Q show ?P by simp

  1141   next

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

  1143     with Q have R: ?R by simp

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

  1145     show ?P by simp

  1146   qed

  1147 qed

  1148

  1149 lemma split_div_lemma:

  1150   assumes "0 < n"

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

  1152 proof

  1153   assume ?rhs

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

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

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

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

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

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

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

  1161   from A B show ?lhs ..

  1162 next

  1163   assume P: ?lhs

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

  1165     unfolding divmod_nat_rel_def by (auto simp add: mult_ac)

  1166   with divmod_nat_rel_unique divmod_nat_rel [of m n]

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

  1168   then show ?rhs by simp

  1169 qed

  1170

  1171 theorem split_div':

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

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

  1174   apply (case_tac "0 < n")

  1175   apply (simp only: add: split_div_lemma)

  1176   apply simp_all

  1177   done

  1178

  1179 lemma split_mod:

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

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

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

  1183 proof

  1184   assume P: ?P

  1185   show ?Q

  1186   proof (cases)

  1187     assume "k = 0"

  1188     with P show ?Q by simp

  1189   next

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

  1191     thus ?Q

  1192     proof (simp, intro allI impI)

  1193       fix i j

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

  1195       thus "P j" using not0 P by(simp add:add_ac mult_ac)

  1196     qed

  1197   qed

  1198 next

  1199   assume Q: ?Q

  1200   show ?P

  1201   proof (cases)

  1202     assume "k = 0"

  1203     with Q show ?P by simp

  1204   next

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

  1206     with Q have R: ?R by simp

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

  1208     show ?P by simp

  1209   qed

  1210 qed

  1211

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

  1213   using mod_div_equality [of m n] by arith

  1214

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

  1216   using mod_div_equality [of m n] by arith

  1217 (* FIXME: very similar to mult_div_cancel *)

  1218

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

  1220   apply rule

  1221   apply (cases "b = 0")

  1222   apply simp_all

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

  1224   done

  1225

  1226

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

  1228

  1229 lemma mod_induct_0:

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

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

  1232   shows "P 0"

  1233 proof (rule ccontr)

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

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

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

  1237   proof

  1238     fix k

  1239     show "?A k"

  1240     proof (induct k)

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

  1242     next

  1243       fix n

  1244       assume ih: "?A n"

  1245       show "?A (Suc n)"

  1246       proof (clarsimp)

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

  1248         have n: "Suc n < p"

  1249         proof (rule ccontr)

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

  1251           hence "p - Suc n = 0"

  1252             by simp

  1253           with y contra show "False"

  1254             by simp

  1255         qed

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

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

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

  1259           by blast

  1260         show "False"

  1261         proof (cases "n=0")

  1262           case True

  1263           with z n2 contra show ?thesis by simp

  1264         next

  1265           case False

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

  1267           with z n2 False ih show ?thesis by simp

  1268         qed

  1269       qed

  1270     qed

  1271   qed

  1272   moreover

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

  1274     by (blast dest: less_imp_add_positive)

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

  1276   moreover

  1277   note base

  1278   ultimately

  1279   show "False" by blast

  1280 qed

  1281

  1282 lemma mod_induct:

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

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

  1285   shows "P j"

  1286 proof -

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

  1288   proof

  1289     fix j

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

  1291     proof (induct j)

  1292       from step base i show "?A 0"

  1293         by (auto elim: mod_induct_0)

  1294     next

  1295       fix k

  1296       assume ih: "?A k"

  1297       show "?A (Suc k)"

  1298       proof

  1299         assume suc: "Suc k < p"

  1300         hence k: "k<p" by simp

  1301         with ih have "P k" ..

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

  1303           by blast

  1304         moreover

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

  1306           by simp

  1307         ultimately

  1308         show "P (Suc k)" by simp

  1309       qed

  1310     qed

  1311   qed

  1312   with j show ?thesis by blast

  1313 qed

  1314

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

  1316   by (simp add: numeral_2_eq_2 le_div_geq)

  1317

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

  1319   by (simp add: numeral_2_eq_2 le_mod_geq)

  1320

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

  1322 by (simp add: mult_2 [symmetric])

  1323

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

  1325 proof -

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

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

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

  1329   then show ?thesis by auto

  1330 qed

  1331

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

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

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

  1335

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

  1337 by (simp add: Suc3_eq_add_3)

  1338

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

  1340 by (simp add: Suc3_eq_add_3)

  1341

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

  1343 by (simp add: Suc3_eq_add_3)

  1344

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

  1346 by (simp add: Suc3_eq_add_3)

  1347

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

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

  1350

  1351

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

  1353 apply (induct "m")

  1354 apply (simp_all add: mod_Suc)

  1355 done

  1356

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

  1358

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

  1360 by (simp add: div_le_mono)

  1361

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

  1363 by (cases n) simp_all

  1364

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

  1366 proof -

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

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

  1369 qed

  1370

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

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

  1373 by (simp add: mult_ac add_ac)

  1374

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

  1376 proof -

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

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

  1379   finally show ?thesis .

  1380 qed

  1381

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

  1383 apply (subst mod_Suc [of m])

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

  1385 done

  1386

  1387 lemma mod_2_not_eq_zero_eq_one_nat:

  1388   fixes n :: nat

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

  1390   by simp

  1391

  1392 instance nat :: semiring_numeral_div

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

  1394

  1395

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

  1397

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

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

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

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

  1402

  1403 text {*

  1404   The following algorithmic devlopment actually echos what has already

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

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

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

  1408   accordingly.

  1409 *}

  1410

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

  1412     --{*for the division algorithm*}

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

  1414                          else (2 * q, r))"

  1415

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

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

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

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

  1420 by auto

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

  1422   (auto simp add: mult_2)

  1423

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

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

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

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

  1428 by auto

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

  1430   (auto simp add: mult_2)

  1431

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

  1433

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

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

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

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

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

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

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

  1441                else

  1442                   if 0 < b then negDivAlg a b

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

  1444

  1445 instantiation int :: Divides.div

  1446 begin

  1447

  1448 definition div_int where

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

  1450

  1451 lemma fst_divmod_int [simp]:

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

  1453   by (simp add: div_int_def)

  1454

  1455 definition mod_int where

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

  1457

  1458 lemma snd_divmod_int [simp]:

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

  1460   by (simp add: mod_int_def)

  1461

  1462 instance ..

  1463

  1464 end

  1465

  1466 lemma divmod_int_mod_div:

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

  1468   by (simp add: prod_eq_iff)

  1469

  1470 text{*

  1471 Here is the division algorithm in ML:

  1472

  1473 \begin{verbatim}

  1474     fun posDivAlg (a,b) =

  1475       if a<b then (0,a)

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

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

  1478            end

  1479

  1480     fun negDivAlg (a,b) =

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

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

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

  1484            end;

  1485

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

  1487

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

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

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

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

  1492                        else

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

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

  1495 \end{verbatim}

  1496 *}

  1497

  1498

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

  1500

  1501 lemma unique_quotient_lemma:

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

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

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

  1505  prefer 2 apply (simp add: right_diff_distrib)

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

  1507 apply (erule_tac [2] order_le_less_trans)

  1508  prefer 2 apply (simp add: right_diff_distrib distrib_left)

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

  1510  prefer 2 apply (simp add: right_diff_distrib distrib_left)

  1511 apply (simp add: mult_less_cancel_left)

  1512 done

  1513

  1514 lemma unique_quotient_lemma_neg:

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

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

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

  1518     auto)

  1519

  1520 lemma unique_quotient:

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

  1522       ==> q = q'"

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

  1524 apply (blast intro: order_antisym

  1525              dest: order_eq_refl [THEN unique_quotient_lemma]

  1526              order_eq_refl [THEN unique_quotient_lemma_neg] sym)+

  1527 done

  1528

  1529

  1530 lemma unique_remainder:

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

  1532       ==> r = r'"

  1533 apply (subgoal_tac "q = q'")

  1534  apply (simp add: divmod_int_rel_def)

  1535 apply (blast intro: unique_quotient)

  1536 done

  1537

  1538

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

  1540

  1541 text{*And positive divisors*}

  1542

  1543 lemma adjust_eq [simp]:

  1544      "adjust b (q, r) =

  1545       (let diff = r - b in

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

  1547                      else (2*q, r))"

  1548   by (simp add: Let_def adjust_def)

  1549

  1550 declare posDivAlg.simps [simp del]

  1551

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

  1553 lemma posDivAlg_eqn:

  1554      "0 < b ==>

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

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

  1557

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

  1559 theorem posDivAlg_correct:

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

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

  1562   using assms

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

  1564   apply auto

  1565   apply (simp add: divmod_int_rel_def)

  1566   apply (subst posDivAlg_eqn, simp add: distrib_left)

  1567   apply (case_tac "a < b")

  1568   apply simp_all

  1569   apply (erule splitE)

  1570   apply (auto simp add: distrib_left Let_def mult_ac mult_2_right)

  1571   done

  1572

  1573

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

  1575

  1576 text{*And positive divisors*}

  1577

  1578 declare negDivAlg.simps [simp del]

  1579

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

  1581 lemma negDivAlg_eqn:

  1582      "0 < b ==>

  1583       negDivAlg a b =

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

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

  1586

  1587 (*Correctness of negDivAlg: it computes quotients correctly

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

  1589 lemma negDivAlg_correct:

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

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

  1592   using assms

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

  1594   apply (auto simp add: linorder_not_le)

  1595   apply (simp add: divmod_int_rel_def)

  1596   apply (subst negDivAlg_eqn, assumption)

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

  1598   apply simp_all

  1599   apply (erule splitE)

  1600   apply (auto simp add: distrib_left Let_def mult_ac mult_2_right)

  1601   done

  1602

  1603

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

  1605

  1606 (*the case a=0*)

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

  1608 by (auto simp add: divmod_int_rel_def linorder_neq_iff)

  1609

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

  1611 by (subst posDivAlg.simps, auto)

  1612

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

  1614 by (subst posDivAlg.simps, auto)

  1615

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

  1617 by (subst negDivAlg.simps, auto)

  1618

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

  1620 by (auto simp add: divmod_int_rel_def)

  1621

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

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

  1624 by (force simp add: linorder_neq_iff divmod_int_rel_0 divmod_int_def divmod_int_rel_neg

  1625                     posDivAlg_correct negDivAlg_correct)

  1626

  1627 lemma divmod_int_unique:

  1628   assumes "divmod_int_rel a b qr"

  1629   shows "divmod_int a b = qr"

  1630   using assms divmod_int_correct [of a b]

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

  1632   by (metis pair_collapse)

  1633

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

  1635   using divmod_int_correct by (simp add: divmod_int_mod_div)

  1636

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

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

  1639

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

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

  1642

  1643 instance int :: ring_div

  1644 proof

  1645   fix a b :: int

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

  1647     using divmod_int_rel_div_mod [of a b]

  1648     unfolding divmod_int_rel_def by (simp add: mult_commute)

  1649 next

  1650   fix a b c :: int

  1651   assume "b \<noteq> 0"

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

  1653     using divmod_int_rel_div_mod [of a b]

  1654     unfolding divmod_int_rel_def by (auto simp: algebra_simps)

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

  1656     by (rule div_int_unique)

  1657 next

  1658   fix a b c :: int

  1659   assume "c \<noteq> 0"

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

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

  1662     unfolding divmod_int_rel_def

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

  1664       mult_less_0_iff zero_less_mult_iff mult_strict_right_mono

  1665       mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff)

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

  1667     using divmod_int_rel_div_mod [of a b] .

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

  1669     by (rule div_int_unique)

  1670 next

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

  1672     by (rule div_int_unique, simp add: divmod_int_rel_def)

  1673 next

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

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

  1676 qed

  1677

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

  1679

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

  1681   by (fact mod_div_equality2 [symmetric])

  1682

  1683 text {* Tool setup *}

  1684

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

  1686 lemmas add_0s = add_0_left add_0_right

  1687

  1688 ML {*

  1689 structure Cancel_Div_Mod_Int = Cancel_Div_Mod

  1690 (

  1691   val div_name = @{const_name div};

  1692   val mod_name = @{const_name mod};

  1693   val mk_binop = HOLogic.mk_binop;

  1694   val mk_sum = Arith_Data.mk_sum HOLogic.intT;

  1695   val dest_sum = Arith_Data.dest_sum;

  1696

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

  1698

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

  1700     (@{thm diff_minus} :: @{thms add_0s} @ @{thms add_ac}))

  1701 )

  1702 *}

  1703

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

  1705

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

  1707   using divmod_int_correct [of a b]

  1708   by (auto simp add: divmod_int_rel_def prod_eq_iff)

  1709

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

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

  1712

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

  1714   using divmod_int_correct [of a b]

  1715   by (auto simp add: divmod_int_rel_def prod_eq_iff)

  1716

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

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

  1719

  1720

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

  1722

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

  1724 apply (rule div_int_unique)

  1725 apply (auto simp add: divmod_int_rel_def)

  1726 done

  1727

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

  1729 apply (rule div_int_unique)

  1730 apply (auto simp add: divmod_int_rel_def)

  1731 done

  1732

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

  1734 apply (rule div_int_unique)

  1735 apply (auto simp add: divmod_int_rel_def)

  1736 done

  1737

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

  1739

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

  1741 apply (rule_tac q = 0 in mod_int_unique)

  1742 apply (auto simp add: divmod_int_rel_def)

  1743 done

  1744

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

  1746 apply (rule_tac q = 0 in mod_int_unique)

  1747 apply (auto simp add: divmod_int_rel_def)

  1748 done

  1749

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

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

  1752 apply (auto simp add: divmod_int_rel_def)

  1753 done

  1754

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

  1756

  1757

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

  1759

  1760 lemma zminus1_lemma:

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

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

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

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

  1765

  1766

  1767 lemma zdiv_zminus1_eq_if:

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

  1769       ==> (-a) div b =

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

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

  1772

  1773 lemma zmod_zminus1_eq_if:

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

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

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

  1777 done

  1778

  1779 lemma zmod_zminus1_not_zero:

  1780   fixes k l :: int

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

  1782   unfolding zmod_zminus1_eq_if by auto

  1783

  1784 lemma zdiv_zminus2_eq_if:

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

  1786       ==> a div (-b) =

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

  1788 by (simp add: zdiv_zminus1_eq_if div_minus_right)

  1789

  1790 lemma zmod_zminus2_eq_if:

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

  1792 by (simp add: zmod_zminus1_eq_if mod_minus_right)

  1793

  1794 lemma zmod_zminus2_not_zero:

  1795   fixes k l :: int

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

  1797   unfolding zmod_zminus2_eq_if by auto

  1798

  1799

  1800 subsubsection {* Computation of Division and Remainder *}

  1801

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

  1803 by (simp add: div_int_def divmod_int_def)

  1804

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

  1806 by (simp add: mod_int_def divmod_int_def)

  1807

  1808 text{*a positive, b positive *}

  1809

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

  1811 by (simp add: div_int_def divmod_int_def)

  1812

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

  1814 by (simp add: mod_int_def divmod_int_def)

  1815

  1816 text{*a negative, b positive *}

  1817

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

  1819 by (simp add: div_int_def divmod_int_def)

  1820

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

  1822 by (simp add: mod_int_def divmod_int_def)

  1823

  1824 text{*a positive, b negative *}

  1825

  1826 lemma div_pos_neg:

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

  1828 by (simp add: div_int_def divmod_int_def)

  1829

  1830 lemma mod_pos_neg:

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

  1832 by (simp add: mod_int_def divmod_int_def)

  1833

  1834 text{*a negative, b negative *}

  1835

  1836 lemma div_neg_neg:

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

  1838 by (simp add: div_int_def divmod_int_def)

  1839

  1840 lemma mod_neg_neg:

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

  1842 by (simp add: mod_int_def divmod_int_def)

  1843

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

  1845

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

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

  1848

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

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

  1851     simp add: divmod_int_rel_def)

  1852

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

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

  1855     simp add: divmod_int_rel_def)

  1856

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

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

  1859     simp add: divmod_int_rel_def)

  1860

  1861 text {*

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

  1863   by divmod algorithm from @{class semiring_numeral_div}

  1864 *}

  1865

  1866 ML {*

  1867 local

  1868   val mk_number = HOLogic.mk_number HOLogic.intT

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

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

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

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

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

  1874   val simps = @{thms arith_simps} @ @{thms rel_simps} @

  1875     map (fn th => th RS sym) [@{thm numeral_1_eq_1}]

  1876   fun prove ctxt goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop goal)

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

  1878   fun binary_proc proc ctxt ct =

  1879     (case Thm.term_of ct of

  1880       _ $t$ u =>

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

  1882         SOME args => proc ctxt args

  1883       | NONE => NONE)

  1884     | _ => NONE);

  1885 in

  1886   fun divmod_proc posrule negrule =

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

  1888       if b = 0 then NONE else let

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

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

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

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

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

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

  1895 end

  1896 *}

  1897

  1898 simproc_setup binary_int_div

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

  1900    "numeral m div neg_numeral n :: int" |

  1901    "neg_numeral m div numeral n :: int" |

  1902    "neg_numeral m div neg_numeral n :: int") =

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

  1904

  1905 simproc_setup binary_int_mod

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

  1907    "numeral m mod neg_numeral n :: int" |

  1908    "neg_numeral m mod numeral n :: int" |

  1909    "neg_numeral m mod neg_numeral n :: int") =

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

  1911

  1912 lemmas posDivAlg_eqn_numeral [simp] =

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

  1914

  1915 lemmas negDivAlg_eqn_numeral [simp] =

  1916     negDivAlg_eqn [of "numeral v" "neg_numeral w", OF zero_less_numeral] for v w

  1917

  1918

  1919 text{*Special-case simplification *}

  1920

  1921 (** The last remaining special cases for constant arithmetic:

  1922     1 div z and 1 mod z **)

  1923

  1924 lemmas div_pos_pos_1_numeral [simp] =

  1925   div_pos_pos [OF zero_less_one, of "numeral w", OF zero_le_numeral] for w

  1926

  1927 lemmas div_pos_neg_1_numeral [simp] =

  1928   div_pos_neg [OF zero_less_one, of "neg_numeral w",

  1929   OF neg_numeral_less_zero] for w

  1930

  1931 lemmas mod_pos_pos_1_numeral [simp] =

  1932   mod_pos_pos [OF zero_less_one, of "numeral w", OF zero_le_numeral] for w

  1933

  1934 lemmas mod_pos_neg_1_numeral [simp] =

  1935   mod_pos_neg [OF zero_less_one, of "neg_numeral w",

  1936   OF neg_numeral_less_zero] for w

  1937

  1938 lemmas posDivAlg_eqn_1_numeral [simp] =

  1939     posDivAlg_eqn [of concl: 1 "numeral w", OF zero_less_numeral] for w

  1940

  1941 lemmas negDivAlg_eqn_1_numeral [simp] =

  1942     negDivAlg_eqn [of concl: 1 "numeral w", OF zero_less_numeral] for w

  1943

  1944

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

  1946

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

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

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

  1950 apply (rule unique_quotient_lemma)

  1951 apply (erule subst)

  1952 apply (erule subst, simp_all)

  1953 done

  1954

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

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

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

  1958 apply (rule unique_quotient_lemma_neg)

  1959 apply (erule subst)

  1960 apply (erule subst, simp_all)

  1961 done

  1962

  1963

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

  1965

  1966 lemma q_pos_lemma:

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

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

  1969  apply (simp add: zero_less_mult_iff)

  1970 apply (simp add: distrib_left)

  1971 done

  1972

  1973 lemma zdiv_mono2_lemma:

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

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

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

  1977 apply (frule q_pos_lemma, assumption+)

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

  1979  apply (simp add: mult_less_cancel_left)

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

  1981  prefer 2 apply simp

  1982 apply (simp (no_asm_simp) add: distrib_left)

  1983 apply (subst add_commute, rule add_less_le_mono, arith)

  1984 apply (rule mult_right_mono, auto)

  1985 done

  1986

  1987 lemma zdiv_mono2:

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

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

  1990  prefer 2 apply arith

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

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

  1993 apply (rule zdiv_mono2_lemma)

  1994 apply (erule subst)

  1995 apply (erule subst, simp_all)

  1996 done

  1997

  1998 lemma q_neg_lemma:

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

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

  2001  apply (simp add: mult_less_0_iff, arith)

  2002 done

  2003

  2004 lemma zdiv_mono2_neg_lemma:

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

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

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

  2008 apply (frule q_neg_lemma, assumption+)

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

  2010  apply (simp add: mult_less_cancel_left)

  2011 apply (simp add: distrib_left)

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

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

  2014 done

  2015

  2016 lemma zdiv_mono2_neg:

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

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

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

  2020 apply (rule zdiv_mono2_neg_lemma)

  2021 apply (erule subst)

  2022 apply (erule subst, simp_all)

  2023 done

  2024

  2025

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

  2027

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

  2029

  2030 lemma zmult1_lemma:

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

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

  2033 by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left mult_ac)

  2034

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

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

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

  2038 done

  2039

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

  2041

  2042 lemma zadd1_lemma:

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

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

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

  2046

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

  2048 lemma zdiv_zadd1_eq:

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

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

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

  2052 done

  2053

  2054 lemma posDivAlg_div_mod:

  2055   assumes "k \<ge> 0"

  2056   and "l \<ge> 0"

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

  2058 proof (cases "l = 0")

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

  2060 next

  2061   case False with assms posDivAlg_correct

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

  2063     by simp

  2064   from div_int_unique [OF this] mod_int_unique [OF this]

  2065   show ?thesis by simp

  2066 qed

  2067

  2068 lemma negDivAlg_div_mod:

  2069   assumes "k < 0"

  2070   and "l > 0"

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

  2072 proof -

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

  2074   from assms negDivAlg_correct

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

  2076     by simp

  2077   from div_int_unique [OF this] mod_int_unique [OF this]

  2078   show ?thesis by simp

  2079 qed

  2080

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

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

  2083

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

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

  2086

  2087 lemma zmod_zdiv_equality':

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

  2089   using mod_div_equality [of m n] by arith

  2090

  2091

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

  2093

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

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

  2096   to cause particular problems.*)

  2097

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

  2099

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

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

  2102  apply (simp add: algebra_simps)

  2103 apply (rule order_le_less_trans)

  2104  apply (erule_tac [2] mult_strict_right_mono)

  2105  apply (rule mult_left_mono_neg)

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

  2107  apply (simp)

  2108 apply (simp)

  2109 done

  2110

  2111 lemma zmult2_lemma_aux2:

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

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

  2114  apply arith

  2115 apply (simp add: mult_le_0_iff)

  2116 done

  2117

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

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

  2120 apply arith

  2121 apply (simp add: zero_le_mult_iff)

  2122 done

  2123

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

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

  2126  apply (simp add: right_diff_distrib)

  2127 apply (rule order_less_le_trans)

  2128  apply (erule mult_strict_right_mono)

  2129  apply (rule_tac [2] mult_left_mono)

  2130   apply simp

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

  2132 apply simp

  2133 done

  2134

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

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

  2137 by (auto simp add: mult_ac divmod_int_rel_def linorder_neq_iff

  2138                    zero_less_mult_iff distrib_left [symmetric]

  2139                    zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: split_if_asm)

  2140

  2141 lemma zdiv_zmult2_eq:

  2142   fixes a b c :: int

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

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

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

  2146 done

  2147

  2148 lemma zmod_zmult2_eq:

  2149   fixes a b c :: int

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

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

  2152 apply (force simp add: le_less divmod_int_rel_div_mod [THEN zmult2_lemma, THEN mod_int_unique])

  2153 done

  2154

  2155 lemma div_pos_geq:

  2156   fixes k l :: int

  2157   assumes "0 < l" and "l \<le> k"

  2158   shows "k div l = (k - l) div l + 1"

  2159 proof -

  2160   have "k = (k - l) + l" by simp

  2161   then obtain j where k: "k = j + l" ..

  2162   with assms show ?thesis by simp

  2163 qed

  2164

  2165 lemma mod_pos_geq:

  2166   fixes k l :: int

  2167   assumes "0 < l" and "l \<le> k"

  2168   shows "k mod l = (k - l) mod l"

  2169 proof -

  2170   have "k = (k - l) + l" by simp

  2171   then obtain j where k: "k = j + l" ..

  2172   with assms show ?thesis by simp

  2173 qed

  2174

  2175

  2176 subsubsection {* Splitting Rules for div and mod *}

  2177

  2178 text{*The proofs of the two lemmas below are essentially identical*}

  2179

  2180 lemma split_pos_lemma:

  2181  "0<k ==>

  2182     P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"

  2183 apply (rule iffI, clarify)

  2184  apply (erule_tac P="P ?x ?y" in rev_mp)

  2185  apply (subst mod_add_eq)

  2186  apply (subst zdiv_zadd1_eq)

  2187  apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)

  2188 txt{*converse direction*}

  2189 apply (drule_tac x = "n div k" in spec)

  2190 apply (drule_tac x = "n mod k" in spec, simp)

  2191 done

  2192

  2193 lemma split_neg_lemma:

  2194  "k<0 ==>

  2195     P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"

  2196 apply (rule iffI, clarify)

  2197  apply (erule_tac P="P ?x ?y" in rev_mp)

  2198  apply (subst mod_add_eq)

  2199  apply (subst zdiv_zadd1_eq)

  2200  apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)

  2201 txt{*converse direction*}

  2202 apply (drule_tac x = "n div k" in spec)

  2203 apply (drule_tac x = "n mod k" in spec, simp)

  2204 done

  2205

  2206 lemma split_zdiv:

  2207  "P(n div k :: int) =

  2208   ((k = 0 --> P 0) &

  2209    (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i)) &

  2210    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i)))"

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

  2212 apply (simp only: linorder_neq_iff)

  2213 apply (erule disjE)

  2214  apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"]

  2215                       split_neg_lemma [of concl: "%x y. P x"])

  2216 done

  2217

  2218 lemma split_zmod:

  2219  "P(n mod k :: int) =

  2220   ((k = 0 --> P n) &

  2221    (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P j)) &

  2222    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P j)))"

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

  2224 apply (simp only: linorder_neq_iff)

  2225 apply (erule disjE)

  2226  apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"]

  2227                       split_neg_lemma [of concl: "%x y. P y"])

  2228 done

  2229

  2230 text {* Enable (lin)arith to deal with @{const div} and @{const mod}

  2231   when these are applied to some constant that is of the form

  2232   @{term "numeral k"}: *}

  2233 declare split_zdiv [of _ _ "numeral k", arith_split] for k

  2234 declare split_zmod [of _ _ "numeral k", arith_split] for k

  2235

  2236

  2237 subsubsection {* Computing @{text "div"} and @{text "mod"} with shifting *}

  2238

  2239 lemma pos_divmod_int_rel_mult_2:

  2240   assumes "0 \<le> b"

  2241   assumes "divmod_int_rel a b (q, r)"

  2242   shows "divmod_int_rel (1 + 2*a) (2*b) (q, 1 + 2*r)"

  2243   using assms unfolding divmod_int_rel_def by auto

  2244

  2245 lemma neg_divmod_int_rel_mult_2:

  2246   assumes "b \<le> 0"

  2247   assumes "divmod_int_rel (a + 1) b (q, r)"

  2248   shows "divmod_int_rel (1 + 2*a) (2*b) (q, 2*r - 1)"

  2249   using assms unfolding divmod_int_rel_def by auto

  2250

  2251 text{*computing div by shifting *}

  2252

  2253 lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a"

  2254   using pos_divmod_int_rel_mult_2 [OF _ divmod_int_rel_div_mod]

  2255   by (rule div_int_unique)

  2256

  2257 lemma neg_zdiv_mult_2:

  2258   assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"

  2259   using neg_divmod_int_rel_mult_2 [OF A divmod_int_rel_div_mod]

  2260   by (rule div_int_unique)

  2261

  2262 (* FIXME: add rules for negative numerals *)

  2263 lemma zdiv_numeral_Bit0 [simp]:

  2264   "numeral (Num.Bit0 v) div numeral (Num.Bit0 w) =

  2265     numeral v div (numeral w :: int)"

  2266   unfolding numeral.simps unfolding mult_2 [symmetric]

  2267   by (rule div_mult_mult1, simp)

  2268

  2269 lemma zdiv_numeral_Bit1 [simp]:

  2270   "numeral (Num.Bit1 v) div numeral (Num.Bit0 w) =

  2271     (numeral v div (numeral w :: int))"

  2272   unfolding numeral.simps

  2273   unfolding mult_2 [symmetric] add_commute [of _ 1]

  2274   by (rule pos_zdiv_mult_2, simp)

  2275

  2276 lemma pos_zmod_mult_2:

  2277   fixes a b :: int

  2278   assumes "0 \<le> a"

  2279   shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)"

  2280   using pos_divmod_int_rel_mult_2 [OF assms divmod_int_rel_div_mod]

  2281   by (rule mod_int_unique)

  2282

  2283 lemma neg_zmod_mult_2:

  2284   fixes a b :: int

  2285   assumes "a \<le> 0"

  2286   shows "(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1"

  2287   using neg_divmod_int_rel_mult_2 [OF assms divmod_int_rel_div_mod]

  2288   by (rule mod_int_unique)

  2289

  2290 (* FIXME: add rules for negative numerals *)

  2291 lemma zmod_numeral_Bit0 [simp]:

  2292   "numeral (Num.Bit0 v) mod numeral (Num.Bit0 w) =

  2293     (2::int) * (numeral v mod numeral w)"

  2294   unfolding numeral_Bit0 [of v] numeral_Bit0 [of w]

  2295   unfolding mult_2 [symmetric] by (rule mod_mult_mult1)

  2296

  2297 lemma zmod_numeral_Bit1 [simp]:

  2298   "numeral (Num.Bit1 v) mod numeral (Num.Bit0 w) =

  2299     2 * (numeral v mod numeral w) + (1::int)"

  2300   unfolding numeral_Bit1 [of v] numeral_Bit0 [of w]

  2301   unfolding mult_2 [symmetric] add_commute [of _ 1]

  2302   by (rule pos_zmod_mult_2, simp)

  2303

  2304 lemma zdiv_eq_0_iff:

  2305  "(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")

  2306 proof

  2307   assume ?L

  2308   have "?L \<longrightarrow> ?R" by (rule split_zdiv[THEN iffD2]) simp

  2309   with ?L show ?R by blast

  2310 next

  2311   assume ?R thus ?L

  2312     by(auto simp: div_pos_pos_trivial div_neg_neg_trivial)

  2313 qed

  2314

  2315

  2316 subsubsection {* Quotients of Signs *}

  2317

  2318 lemma div_neg_pos_less0: "[| a < (0::int);  0 < b |] ==> a div b < 0"

  2319 apply (subgoal_tac "a div b \<le> -1", force)

  2320 apply (rule order_trans)

  2321 apply (rule_tac a' = "-1" in zdiv_mono1)

  2322 apply (auto simp add: div_eq_minus1)

  2323 done

  2324

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

  2326 by (drule zdiv_mono1_neg, auto)

  2327

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

  2329 by (drule zdiv_mono1, auto)

  2330

  2331 text{* Now for some equivalences of the form @{text"a div b >=< 0 \<longleftrightarrow> \<dots>"}

  2332 conditional upon the sign of @{text a} or @{text b}. There are many more.

  2333 They should all be simp rules unless that causes too much search. *}

  2334

  2335 lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)"

  2336 apply auto

  2337 apply (drule_tac [2] zdiv_mono1)

  2338 apply (auto simp add: linorder_neq_iff)

  2339 apply (simp (no_asm_use) add: linorder_not_less [symmetric])

  2340 apply (blast intro: div_neg_pos_less0)

  2341 done

  2342

  2343 lemma neg_imp_zdiv_nonneg_iff:

  2344   "b < (0::int) ==> (0 \<le> a div b) = (a \<le> (0::int))"

  2345 apply (subst div_minus_minus [symmetric])

  2346 apply (subst pos_imp_zdiv_nonneg_iff, auto)

  2347 done

  2348

  2349 (*But not (a div b \<le> 0 iff a\<le>0); consider a=1, b=2 when a div b = 0.*)

  2350 lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)"

  2351 by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff)

  2352

  2353 lemma pos_imp_zdiv_pos_iff:

  2354   "0<k \<Longrightarrow> 0 < (i::int) div k \<longleftrightarrow> k \<le> i"

  2355 using pos_imp_zdiv_nonneg_iff[of k i] zdiv_eq_0_iff[of i k]

  2356 by arith

  2357

  2358 (*Again the law fails for \<le>: consider a = -1, b = -2 when a div b = 0*)

  2359 lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)"

  2360 by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)

  2361

  2362 lemma nonneg1_imp_zdiv_pos_iff:

  2363   "(0::int) <= a \<Longrightarrow> (a div b > 0) = (a >= b & b>0)"

  2364 apply rule

  2365  apply rule

  2366   using div_pos_pos_trivial[of a b]apply arith

  2367  apply(cases "b=0")apply simp

  2368  using div_nonneg_neg_le0[of a b]apply arith

  2369 using int_one_le_iff_zero_less[of "a div b"] zdiv_mono1[of b a b]apply simp

  2370 done

  2371

  2372 lemma zmod_le_nonneg_dividend: "(m::int) \<ge> 0 ==> m mod k \<le> m"

  2373 apply (rule split_zmod[THEN iffD2])

  2374 apply(fastforce dest: q_pos_lemma intro: split_mult_pos_le)

  2375 done

  2376

  2377

  2378 subsubsection {* The Divides Relation *}

  2379

  2380 lemma dvd_neg_numeral_left [simp]:

  2381   fixes y :: "'a::comm_ring_1"

  2382   shows "(neg_numeral k) dvd y \<longleftrightarrow> (numeral k) dvd y"

  2383   unfolding neg_numeral_def minus_dvd_iff ..

  2384

  2385 lemma dvd_neg_numeral_right [simp]:

  2386   fixes x :: "'a::comm_ring_1"

  2387   shows "x dvd (neg_numeral k) \<longleftrightarrow> x dvd (numeral k)"

  2388   unfolding neg_numeral_def dvd_minus_iff ..

  2389

  2390 lemmas dvd_eq_mod_eq_0_numeral [simp] =

  2391   dvd_eq_mod_eq_0 [of "numeral x" "numeral y"] for x y

  2392

  2393

  2394 subsubsection {* Further properties *}

  2395

  2396 lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"

  2397   using zmod_zdiv_equality[where a="m" and b="n"]

  2398   by (simp add: algebra_simps) (* FIXME: generalize *)

  2399

  2400 lemma zdiv_int: "int (a div b) = (int a) div (int b)"

  2401 apply (subst split_div, auto)

  2402 apply (subst split_zdiv, auto)

  2403 apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in unique_quotient)

  2404 apply (auto simp add: divmod_int_rel_def of_nat_mult)

  2405 done

  2406

  2407 lemma zmod_int: "int (a mod b) = (int a) mod (int b)"

  2408 apply (subst split_mod, auto)

  2409 apply (subst split_zmod, auto)

  2410 apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia

  2411        in unique_remainder)

  2412 apply (auto simp add: divmod_int_rel_def of_nat_mult)

  2413 done

  2414

  2415 lemma abs_div: "(y::int) dvd x \<Longrightarrow> abs (x div y) = abs x div abs y"

  2416 by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)

  2417

  2418 text{*Suggested by Matthias Daum*}

  2419 lemma int_power_div_base:

  2420      "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"

  2421 apply (subgoal_tac "k ^ m = k ^ ((m - Suc 0) + Suc 0)")

  2422  apply (erule ssubst)

  2423  apply (simp only: power_add)

  2424  apply simp_all

  2425 done

  2426

  2427 text {* by Brian Huffman *}

  2428 lemma zminus_zmod: "- ((x::int) mod m) mod m = - x mod m"

  2429 by (rule mod_minus_eq [symmetric])

  2430

  2431 lemma zdiff_zmod_left: "(x mod m - y) mod m = (x - y) mod (m::int)"

  2432 by (rule mod_diff_left_eq [symmetric])

  2433

  2434 lemma zdiff_zmod_right: "(x - y mod m) mod m = (x - y) mod (m::int)"

  2435 by (rule mod_diff_right_eq [symmetric])

  2436

  2437 lemmas zmod_simps =

  2438   mod_add_left_eq  [symmetric]

  2439   mod_add_right_eq [symmetric]

  2440   mod_mult_right_eq[symmetric]

  2441   mod_mult_left_eq [symmetric]

  2442   power_mod

  2443   zminus_zmod zdiff_zmod_left zdiff_zmod_right

  2444

  2445 text {* Distributive laws for function @{text nat}. *}

  2446

  2447 lemma nat_div_distrib: "0 \<le> x \<Longrightarrow> nat (x div y) = nat x div nat y"

  2448 apply (rule linorder_cases [of y 0])

  2449 apply (simp add: div_nonneg_neg_le0)

  2450 apply simp

  2451 apply (simp add: nat_eq_iff pos_imp_zdiv_nonneg_iff zdiv_int)

  2452 done

  2453

  2454 (*Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't*)

  2455 lemma nat_mod_distrib:

  2456   "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x mod y) = nat x mod nat y"

  2457 apply (case_tac "y = 0", simp)

  2458 apply (simp add: nat_eq_iff zmod_int)

  2459 done

  2460

  2461 text  {* transfer setup *}

  2462

  2463 lemma transfer_nat_int_functions:

  2464     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"

  2465     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"

  2466   by (auto simp add: nat_div_distrib nat_mod_distrib)

  2467

  2468 lemma transfer_nat_int_function_closures:

  2469     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"

  2470     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"

  2471   apply (cases "y = 0")

  2472   apply (auto simp add: pos_imp_zdiv_nonneg_iff)

  2473   apply (cases "y = 0")

  2474   apply auto

  2475 done

  2476

  2477 declare transfer_morphism_nat_int [transfer add return:

  2478   transfer_nat_int_functions

  2479   transfer_nat_int_function_closures

  2480 ]

  2481

  2482 lemma transfer_int_nat_functions:

  2483     "(int x) div (int y) = int (x div y)"

  2484     "(int x) mod (int y) = int (x mod y)"

  2485   by (auto simp add: zdiv_int zmod_int)

  2486

  2487 lemma transfer_int_nat_function_closures:

  2488     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"

  2489     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"

  2490   by (simp_all only: is_nat_def transfer_nat_int_function_closures)

  2491

  2492 declare transfer_morphism_int_nat [transfer add return:

  2493   transfer_int_nat_functions

  2494   transfer_int_nat_function_closures

  2495 ]

  2496

  2497 text{*Suggested by Matthias Daum*}

  2498 lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"

  2499 apply (subgoal_tac "nat x div nat k < nat x")

  2500  apply (simp add: nat_div_distrib [symmetric])

  2501 apply (rule Divides.div_less_dividend, simp_all)

  2502 done

  2503

  2504 lemma zmod_eq_dvd_iff: "(x::int) mod n = y mod n \<longleftrightarrow> n dvd x - y"

  2505 proof

  2506   assume H: "x mod n = y mod n"

  2507   hence "x mod n - y mod n = 0" by simp

  2508   hence "(x mod n - y mod n) mod n = 0" by simp

  2509   hence "(x - y) mod n = 0" by (simp add: mod_diff_eq[symmetric])

  2510   thus "n dvd x - y" by (simp add: dvd_eq_mod_eq_0)

  2511 next

  2512   assume H: "n dvd x - y"

  2513   then obtain k where k: "x-y = n*k" unfolding dvd_def by blast

  2514   hence "x = n*k + y" by simp

  2515   hence "x mod n = (n*k + y) mod n" by simp

  2516   thus "x mod n = y mod n" by (simp add: mod_add_left_eq)

  2517 qed

  2518

  2519 lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y  mod n" and xy:"y \<le> x"

  2520   shows "\<exists>q. x = y + n * q"

  2521 proof-

  2522   from xy have th: "int x - int y = int (x - y)" by simp

  2523   from xyn have "int x mod int n = int y mod int n"

  2524     by (simp add: zmod_int [symmetric])

  2525   hence "int n dvd int x - int y" by (simp only: zmod_eq_dvd_iff[symmetric])

  2526   hence "n dvd x - y" by (simp add: th zdvd_int)

  2527   then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith

  2528 qed

  2529

  2530 lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)"

  2531   (is "?lhs = ?rhs")

  2532 proof

  2533   assume H: "x mod n = y mod n"

  2534   {assume xy: "x \<le> y"

  2535     from H have th: "y mod n = x mod n" by simp

  2536     from nat_mod_eq_lemma[OF th xy] have ?rhs

  2537       apply clarify  apply (rule_tac x="q" in exI) by (rule exI[where x="0"], simp)}

  2538   moreover

  2539   {assume xy: "y \<le> x"

  2540     from nat_mod_eq_lemma[OF H xy] have ?rhs

  2541       apply clarify  apply (rule_tac x="0" in exI) by (rule_tac x="q" in exI, simp)}

  2542   ultimately  show ?rhs using linear[of x y] by blast

  2543 next

  2544   assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast

  2545   hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp

  2546   thus  ?lhs by simp

  2547 qed

  2548

  2549 text {*

  2550   This re-embedding of natural division on integers goes back to the

  2551   time when numerals had been signed numerals.  It should

  2552   now be replaced by the algorithm developed in @{class semiring_numeral_div}.

  2553 *}

  2554

  2555 lemma div_nat_numeral [simp]:

  2556   "(numeral v :: nat) div numeral v' = nat (numeral v div numeral v')"

  2557   by (simp add: nat_div_distrib)

  2558

  2559 lemma one_div_nat_numeral [simp]:

  2560   "Suc 0 div numeral v' = nat (1 div numeral v')"

  2561   by (subst nat_div_distrib, simp_all)

  2562

  2563 lemma mod_nat_numeral [simp]:

  2564   "(numeral v :: nat) mod numeral v' = nat (numeral v mod numeral v')"

  2565   by (simp add: nat_mod_distrib)

  2566

  2567 lemma one_mod_nat_numeral [simp]:

  2568   "Suc 0 mod numeral v' = nat (1 mod numeral v')"

  2569   by (subst nat_mod_distrib) simp_all

  2570

  2571 lemma mod_2_not_eq_zero_eq_one_int:

  2572   fixes k :: int

  2573   shows "k mod 2 \<noteq> 0 \<longleftrightarrow> k mod 2 = 1"

  2574   by auto

  2575

  2576 instance int :: semiring_numeral_div

  2577   by intro_classes (auto intro: zmod_le_nonneg_dividend

  2578     simp add: zmult_div_cancel

  2579     pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial

  2580     zmod_zmult2_eq zdiv_zmult2_eq)

  2581

  2582

  2583 subsubsection {* Tools setup *}

  2584

  2585 text {* Nitpick *}

  2586

  2587 lemmas [nitpick_unfold] = dvd_eq_mod_eq_0 mod_div_equality' zmod_zdiv_equality'

  2588

  2589

  2590 subsubsection {* Code generation *}

  2591

  2592 definition divmod_abs :: "int \<Rightarrow> int \<Rightarrow> int \<times> int"

  2593 where

  2594   "divmod_abs k l = (\<bar>k\<bar> div \<bar>l\<bar>, \<bar>k\<bar> mod \<bar>l\<bar>)"

  2595

  2596 lemma fst_divmod_abs [simp]:

  2597   "fst (divmod_abs k l) = \<bar>k\<bar> div \<bar>l\<bar>"

  2598   by (simp add: divmod_abs_def)

  2599

  2600 lemma snd_divmod_abs [simp]:

  2601   "snd (divmod_abs k l) = \<bar>k\<bar> mod \<bar>l\<bar>"

  2602   by (simp add: divmod_abs_def)

  2603

  2604 lemma divmod_abs_code [code]:

  2605   "divmod_abs (Int.Pos k) (Int.Pos l) = divmod k l"

  2606   "divmod_abs (Int.Neg k) (Int.Neg l) = divmod k l"

  2607   "divmod_abs (Int.Neg k) (Int.Pos l) = divmod k l"

  2608   "divmod_abs (Int.Pos k) (Int.Neg l) = divmod k l"

  2609   "divmod_abs j 0 = (0, \<bar>j\<bar>)"

  2610   "divmod_abs 0 j = (0, 0)"

  2611   by (simp_all add: prod_eq_iff)

  2612

  2613 lemma divmod_int_divmod_abs:

  2614   "divmod_int k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else

  2615   apsnd ((op *) (sgn l)) (if 0 < l \<and> 0 \<le> k \<or> l < 0 \<and> k < 0

  2616     then divmod_abs k l

  2617     else (let (r, s) = divmod_abs k l in

  2618        if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"

  2619 proof -

  2620   have aux: "\<And>q::int. - k = l * q \<longleftrightarrow> k = l * - q" by auto

  2621   show ?thesis

  2622     by (simp add: prod_eq_iff split_def Let_def)

  2623       (auto simp add: aux not_less not_le zdiv_zminus1_eq_if

  2624       zmod_zminus1_eq_if zdiv_zminus2_eq_if zmod_zminus2_eq_if)

  2625 qed

  2626

  2627 lemma divmod_int_code [code]:

  2628   "divmod_int k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else

  2629   apsnd ((op *) (sgn l)) (if sgn k = sgn l

  2630     then divmod_abs k l

  2631     else (let (r, s) = divmod_abs k l in

  2632       if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"

  2633 proof -

  2634   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"

  2635     by (auto simp add: not_less sgn_if)

  2636   then show ?thesis by (simp add: divmod_int_divmod_abs)

  2637 qed

  2638

  2639 hide_const (open) divmod_abs

  2640

  2641 code_identifier

  2642   code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith

  2643

  2644 end

  2645
`