src/HOL/Divides.thy
 author paulson Tue Jun 23 16:55:28 2015 +0100 (2015-06-23) changeset 60562 24af00b010cf parent 60517 f16e4fb20652 child 60685 cb21b7022b00 permissions -rw-r--r--
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
     1 (*  Title:      HOL/Divides.thy

     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

     3     Copyright   1999  University of Cambridge

     4 *)

     5

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

     7

     8 theory Divides

     9 imports Parity

    10 begin

    11

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

    13

    14 class div = dvd + divide +

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

    16

    17 class semiring_div = semidom + div +

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

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

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

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

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

    23 begin

    24

    25 subclass algebraic_semidom

    26 proof

    27   fix b a

    28   assume "b \<noteq> 0"

    29   then show "a * b div b = a"

    30     using div_mult_self1 [of b 0 a] by (simp add: ac_simps)

    31 qed simp

    32

    33 lemma power_not_zero: -- \<open>FIXME cf. @{text field_power_not_zero}\<close>

    34   "a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0"

    35   by (induct n) (simp_all add: no_zero_divisors)

    36

    37 lemma semiring_div_power_eq_0_iff: -- \<open>FIXME cf. @{text power_eq_0_iff}, @{text power_eq_0_nat_iff}\<close>

    38   "n \<noteq> 0 \<Longrightarrow> a ^ n = 0 \<longleftrightarrow> a = 0"

    39   using power_not_zero [of a n] by (auto simp add: zero_power)

    40

    41 text {* @{const divide} and @{const mod} *}

    42

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

    44   unfolding mult.commute [of b]

    45   by (rule mod_div_equality)

    46

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

    48   using mod_div_equality [of a b]

    49   by (simp only: ac_simps)

    50

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

    52   by (simp add: mod_div_equality)

    53

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

    55   by (simp add: mod_div_equality2)

    56

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

    58   using mod_div_equality [of a zero] by simp

    59

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

    61   using mod_div_equality [of zero a] div_0 by simp

    62

    63 lemma div_mult_self2 [simp]:

    64   assumes "b \<noteq> 0"

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

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

    67

    68 lemma div_mult_self3 [simp]:

    69   assumes "b \<noteq> 0"

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

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

    72

    73 lemma div_mult_self4 [simp]:

    74   assumes "b \<noteq> 0"

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

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

    77

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

    79 proof (cases "b = 0")

    80   case True then show ?thesis by simp

    81 next

    82   case False

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

    84     by (simp add: mod_div_equality)

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

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

    87       by (simp add: algebra_simps)

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

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

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

    91     by (simp add: mod_div_equality)

    92   then show ?thesis by simp

    93 qed

    94

    95 lemma mod_mult_self2 [simp]:

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

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

    98

    99 lemma mod_mult_self3 [simp]:

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

   101   by (simp add: add.commute)

   102

   103 lemma mod_mult_self4 [simp]:

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

   105   by (simp add: add.commute)

   106

   107 lemma div_mult_self1_is_id:

   108   "b \<noteq> 0 \<Longrightarrow> b * a div b = a"

   109   by (fact nonzero_mult_divide_cancel_left)

   110

   111 lemma div_mult_self2_is_id:

   112   "b \<noteq> 0 \<Longrightarrow> a * b div b = a"

   113   by (fact nonzero_mult_divide_cancel_right)

   114

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

   116   using mod_mult_self2 [of 0 b a] by simp

   117

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

   119   using mod_mult_self1 [of 0 a b] by simp

   120

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

   122   using div_mult_self2_is_id [of 1 a] zero_neq_one by simp

   123

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

   125 proof -

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

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

   128   then show ?thesis by (rule add_left_imp_eq)

   129 qed

   130

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

   132   using mod_mult_self2_is_0 [of 1] by simp

   133

   134 lemma div_add_self1 [simp]:

   135   assumes "b \<noteq> 0"

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

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

   138

   139 lemma div_add_self2 [simp]:

   140   assumes "b \<noteq> 0"

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

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

   143

   144 lemma mod_add_self1 [simp]:

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

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

   147

   148 lemma mod_add_self2 [simp]:

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

   150   using mod_mult_self1 [of a 1 b] by simp

   151

   152 lemma mod_div_decomp:

   153   fixes a b

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

   155     and "a = q * b + r"

   156 proof -

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

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

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

   160   note that ultimately show thesis by blast

   161 qed

   162

   163 lemma dvd_imp_mod_0 [simp]:

   164   assumes "a dvd b"

   165   shows "b mod a = 0"

   166 proof -

   167   from assms obtain c where "b = a * c" ..

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

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

   170 qed

   171

   172 lemma mod_eq_0_iff_dvd:

   173   "a mod b = 0 \<longleftrightarrow> b dvd a"

   174 proof

   175   assume "b dvd a"

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

   177 next

   178   assume "a mod b = 0"

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

   180   then have "a = b * (a div b)" by (simp add: ac_simps)

   181   then show "b dvd a" ..

   182 qed

   183

   184 lemma dvd_eq_mod_eq_0 [code]:

   185   "a dvd b \<longleftrightarrow> b mod a = 0"

   186   by (simp add: mod_eq_0_iff_dvd)

   187

   188 lemma mod_div_trivial [simp]:

   189   "a mod b div b = 0"

   190 proof (cases "b = 0")

   191   assume "b = 0"

   192   thus ?thesis by simp

   193 next

   194   assume "b \<noteq> 0"

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

   196     by (rule div_mult_self1 [symmetric])

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

   198     by (simp only: mod_div_equality')

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

   200     by simp

   201   finally show ?thesis

   202     by (rule add_left_imp_eq)

   203 qed

   204

   205 lemma mod_mod_trivial [simp]:

   206   "a mod b mod b = a mod b"

   207 proof -

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

   209     by (simp only: mod_mult_self1)

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

   211     by (simp only: mod_div_equality')

   212   finally show ?thesis .

   213 qed

   214

   215 lemma div_dvd_div [simp]:

   216   assumes "a dvd b" and "a dvd c"

   217   shows "b div a dvd c div a \<longleftrightarrow> b dvd c"

   218 using assms apply (cases "a = 0")

   219 apply auto

   220 apply (unfold dvd_def)

   221 apply auto

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

   223 apply(fastforce simp add: mult.assoc)

   224 done

   225

   226 lemma dvd_mod_imp_dvd:

   227   assumes "k dvd m mod n" and "k dvd n"

   228   shows "k dvd m"

   229 proof -

   230   from assms have "k dvd (m div n) * n + m mod n"

   231     by (simp only: dvd_add dvd_mult)

   232   then show ?thesis by (simp add: mod_div_equality)

   233 qed

   234

   235 text {* Addition respects modular equivalence. *}

   236

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

   238 proof -

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

   240     by (simp only: mod_div_equality)

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

   242     by (simp only: ac_simps)

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

   244     by (rule mod_mult_self1)

   245   finally show ?thesis .

   246 qed

   247

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

   249 proof -

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

   251     by (simp only: mod_div_equality)

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

   253     by (simp only: ac_simps)

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

   255     by (rule mod_mult_self1)

   256   finally show ?thesis .

   257 qed

   258

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

   260 by (rule trans [OF mod_add_left_eq mod_add_right_eq])

   261

   262 lemma mod_add_cong:

   263   assumes "a mod c = a' mod c"

   264   assumes "b mod c = b' mod c"

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

   266 proof -

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

   268     unfolding assms ..

   269   thus ?thesis

   270     by (simp only: mod_add_eq [symmetric])

   271 qed

   272

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

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

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

   276

   277 text {* Multiplication respects modular equivalence. *}

   278

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

   280 proof -

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

   282     by (simp only: mod_div_equality)

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

   284     by (simp only: algebra_simps)

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

   286     by (rule mod_mult_self1)

   287   finally show ?thesis .

   288 qed

   289

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

   291 proof -

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

   293     by (simp only: mod_div_equality)

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

   295     by (simp only: algebra_simps)

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

   297     by (rule mod_mult_self1)

   298   finally show ?thesis .

   299 qed

   300

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

   302 by (rule trans [OF mod_mult_left_eq mod_mult_right_eq])

   303

   304 lemma mod_mult_cong:

   305   assumes "a mod c = a' mod c"

   306   assumes "b mod c = b' mod c"

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

   308 proof -

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

   310     unfolding assms ..

   311   thus ?thesis

   312     by (simp only: mod_mult_eq [symmetric])

   313 qed

   314

   315 text {* Exponentiation respects modular equivalence. *}

   316

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

   318 apply (induct n, simp_all)

   319 apply (rule mod_mult_right_eq [THEN trans])

   320 apply (simp (no_asm_simp))

   321 apply (rule mod_mult_eq [symmetric])

   322 done

   323

   324 lemma mod_mod_cancel:

   325   assumes "c dvd b"

   326   shows "a mod b mod c = a mod c"

   327 proof -

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

   329     by (rule dvdE)

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

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

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

   333     by (simp only: mod_mult_self1)

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

   335     by (simp only: ac_simps)

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

   337     by (simp only: mod_div_equality)

   338   finally show ?thesis .

   339 qed

   340

   341 lemma div_mult_div_if_dvd:

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

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

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

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

   346   apply (subst mult.assoc [symmetric])

   347   apply (simp add: no_zero_divisors)

   348   done

   349

   350 lemma div_mult_mult2 [simp]:

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

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

   353

   354 lemma div_mult_mult1_if [simp]:

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

   356   by simp_all

   357

   358 lemma mod_mult_mult1:

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

   360 proof (cases "c = 0")

   361   case True then show ?thesis by simp

   362 next

   363   case False

   364   from mod_div_equality

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

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

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

   368   with mod_div_equality show ?thesis by simp

   369 qed

   370

   371 lemma mod_mult_mult2:

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

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

   374

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

   376   by (fact mod_mult_mult2 [symmetric])

   377

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

   379   by (fact mod_mult_mult1 [symmetric])

   380

   381 lemma dvd_times_left_cancel_iff [simp]: -- \<open>FIXME generalize\<close>

   382   assumes "c \<noteq> 0"

   383   shows "c * a dvd c * b \<longleftrightarrow> a dvd b"

   384 proof -

   385   have "(c * b) mod (c * a) = 0 \<longleftrightarrow> b mod a = 0" (is "?P \<longleftrightarrow> ?Q")

   386     using assms by (simp add: mod_mult_mult1)

   387   then show ?thesis by (simp add: mod_eq_0_iff_dvd)

   388 qed

   389

   390 lemma dvd_times_right_cancel_iff [simp]: -- \<open>FIXME generalize\<close>

   391   assumes "c \<noteq> 0"

   392   shows "a * c dvd b * c \<longleftrightarrow> a dvd b"

   393   using assms dvd_times_left_cancel_iff [of c a b] by (simp add: ac_simps)

   394

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

   396   unfolding dvd_def by (auto simp add: mod_mult_mult1)

   397

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

   399 by (blast intro: dvd_mod_imp_dvd dvd_mod)

   400

   401 lemma div_power:

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

   403 apply (induct n)

   404  apply simp

   405 apply(simp add: div_mult_div_if_dvd dvd_power_same)

   406 done

   407

   408 lemma dvd_div_eq_mult:

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

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

   411 proof

   412   assume "b = c * a"

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

   414 next

   415   assume "b div a = c"

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

   417   moreover from a dvd b have "b div a * a = b" by simp

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

   419 qed

   420

   421 lemma dvd_div_div_eq_mult:

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

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

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

   425

   426 end

   427

   428 class ring_div = comm_ring_1 + semiring_div

   429 begin

   430

   431 subclass idom_divide ..

   432

   433 text {* Negation respects modular equivalence. *}

   434

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

   436 proof -

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

   438     by (simp only: mod_div_equality)

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

   440     by (simp add: ac_simps)

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

   442     by (rule mod_mult_self1)

   443   finally show ?thesis .

   444 qed

   445

   446 lemma mod_minus_cong:

   447   assumes "a mod b = a' mod b"

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

   449 proof -

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

   451     unfolding assms ..

   452   thus ?thesis

   453     by (simp only: mod_minus_eq [symmetric])

   454 qed

   455

   456 text {* Subtraction respects modular equivalence. *}

   457

   458 lemma mod_diff_left_eq:

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

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

   461

   462 lemma mod_diff_right_eq:

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

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

   465

   466 lemma mod_diff_eq:

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

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

   469

   470 lemma mod_diff_cong:

   471   assumes "a mod c = a' mod c"

   472   assumes "b mod c = b' mod c"

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

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

   475

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

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

   478 apply (auto simp add: dvd_def)

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

   480  apply (simp only:)

   481  apply (erule div_mult_self1_is_id)

   482 apply simp

   483 done

   484

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

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

   487 apply (auto simp add: dvd_def)

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

   489  apply (erule ssubst, rule div_mult_self1_is_id)

   490  apply simp

   491 apply simp

   492 done

   493

   494 lemma div_diff[simp]:

   495   "\<lbrakk> z dvd x; z dvd y\<rbrakk> \<Longrightarrow> (x - y) div z = x div z - y div z"

   496 using div_add[where y = "- z" for z]

   497 by (simp add: dvd_neg_div)

   498

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

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

   501   unfolding neg_equal_0_iff_equal by simp

   502

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

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

   505

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

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

   508

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

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

   511

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

   513   using div_minus_right [of a 1] by simp

   514

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

   516   using mod_minus_right [of a 1] by simp

   517

   518 lemma minus_mod_self2 [simp]:

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

   520   by (simp add: mod_diff_right_eq)

   521

   522 lemma minus_mod_self1 [simp]:

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

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

   525

   526 end

   527

   528

   529 subsubsection {* Parity and division *}

   530

   531 class semiring_div_parity = semiring_div + comm_semiring_1_cancel + numeral +

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

   533   assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"

   534   assumes zero_not_eq_two: "0 \<noteq> 2"

   535 begin

   536

   537 lemma parity_cases [case_names even odd]:

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

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

   540   shows P

   541   using assms parity by blast

   542

   543 lemma one_div_two_eq_zero [simp]:

   544   "1 div 2 = 0"

   545 proof (cases "2 = 0")

   546   case True then show ?thesis by simp

   547 next

   548   case False

   549   from mod_div_equality have "1 div 2 * 2 + 1 mod 2 = 1" .

   550   with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp

   551   then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff)

   552   then have "1 div 2 = 0 \<or> 2 = 0" by simp

   553   with False show ?thesis by auto

   554 qed

   555

   556 lemma not_mod_2_eq_0_eq_1 [simp]:

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

   558   by (cases a rule: parity_cases) simp_all

   559

   560 lemma not_mod_2_eq_1_eq_0 [simp]:

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

   562   by (cases a rule: parity_cases) simp_all

   563

   564 subclass semiring_parity

   565 proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)

   566   show "1 mod 2 = 1"

   567     by (fact one_mod_two_eq_one)

   568 next

   569   fix a b

   570   assume "a mod 2 = 1"

   571   moreover assume "b mod 2 = 1"

   572   ultimately show "(a + b) mod 2 = 0"

   573     using mod_add_eq [of a b 2] by simp

   574 next

   575   fix a b

   576   assume "(a * b) mod 2 = 0"

   577   then have "(a mod 2) * (b mod 2) = 0"

   578     by (cases "a mod 2 = 0") (simp_all add: mod_mult_eq [of a b 2])

   579   then show "a mod 2 = 0 \<or> b mod 2 = 0"

   580     by (rule divisors_zero)

   581 next

   582   fix a

   583   assume "a mod 2 = 1"

   584   then have "a = a div 2 * 2 + 1" using mod_div_equality [of a 2] by simp

   585   then show "\<exists>b. a = b + 1" ..

   586 qed

   587

   588 lemma even_iff_mod_2_eq_zero:

   589   "even a \<longleftrightarrow> a mod 2 = 0"

   590   by (fact dvd_eq_mod_eq_0)

   591

   592 lemma even_succ_div_two [simp]:

   593   "even a \<Longrightarrow> (a + 1) div 2 = a div 2"

   594   by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)

   595

   596 lemma odd_succ_div_two [simp]:

   597   "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"

   598   by (auto elim!: oddE simp add: zero_not_eq_two [symmetric] add.assoc)

   599

   600 lemma even_two_times_div_two:

   601   "even a \<Longrightarrow> 2 * (a div 2) = a"

   602   by (fact dvd_mult_div_cancel)

   603

   604 lemma odd_two_times_div_two_succ [simp]:

   605   "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"

   606   using mod_div_equality2 [of 2 a] by (simp add: even_iff_mod_2_eq_zero)

   607

   608 end

   609

   610

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

   612

   613 text {*

   614   The following type class contains everything necessary to formulate

   615   a division algorithm in ring structures with numerals, restricted

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

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

   618   and less technical class hierarchy.

   619 *}

   620

   621 class semiring_numeral_div = semiring_div + comm_semiring_1_cancel + linordered_semidom +

   622   assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"

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

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

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

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

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

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

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

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

   631 begin

   632

   633 lemma mult_div_cancel:

   634   "b * (a div b) = a - a mod b"

   635 proof -

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

   637     using mod_div_equality [of a b] by (simp add: ac_simps)

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

   639     by simp

   640   then show ?thesis

   641     by simp

   642 qed

   643

   644 subclass semiring_div_parity

   645 proof

   646   fix a

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

   648   proof (rule ccontr)

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

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

   651     have "0 < 2" by simp

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

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

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

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

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

   657     with a mod 2 < 2 show False by simp

   658   qed

   659 next

   660   show "1 mod 2 = 1"

   661     by (rule mod_less) simp_all

   662 next

   663   show "0 \<noteq> 2"

   664     by simp

   665 qed

   666

   667 lemma divmod_digit_1:

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

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

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

   671 proof -

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

   673     by (auto intro: trans)

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

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

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

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

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

   679     by (simp add: w_def mod_mult2_eq ac_simps)

   680   from assms w_exhaust have "w = 1"

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

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

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

   684     by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)

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

   686   then show ?P and ?Q

   687     by (simp_all add: div mod add_implies_diff [symmetric] le_add_diff_inverse2)

   688 qed

   689

   690 lemma divmod_digit_0:

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

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

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

   694 proof -

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

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

   697     by (simp add: w_def mod_mult2_eq ac_simps)

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

   699   proof -

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

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

   702     then show ?thesis by simp

   703   qed

   704   moreover note assms w_exhaust

   705   ultimately have "w = 0" by auto

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

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

   708     by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)

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

   710   then show ?P and ?Q

   711     by (simp_all add: div mod)

   712 qed

   713

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

   715 where

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

   717

   718 lemma fst_divmod [simp]:

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

   720   by (simp add: divmod_def)

   721

   722 lemma snd_divmod [simp]:

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

   724   by (simp add: divmod_def)

   725

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

   727 where

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

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

   730     else (2 * q, r))"

   731

   732 text {*

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

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

   735   digit position with the remainder from previous division steps

   736   and evaluate accordingly.

   737 *}

   738

   739 lemma divmod_step_eq [code]:

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

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

   742   by (simp add: divmod_step_def)

   743

   744 lemma divmod_step_simps [simp]:

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

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

   747   by (auto simp add: divmod_step_eq not_le)

   748

   749 text {*

   750   This is a formulation of school-method division.

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

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

   753   occurs and then reiterate single division steps in the

   754   opposite direction.

   755 *}

   756

   757 lemma divmod_divmod_step [code]:

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

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

   760 proof (cases "m < n")

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

   762   then show ?thesis

   763     by (simp add: prod_eq_iff div_less mod_less)

   764 next

   765   case False

   766   have "divmod m n =

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

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

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

   770     case True

   771     with divmod_step_simps

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

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

   774         by blast

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

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

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

   778       by simp_all

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

   780   next

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

   782       by (simp add: not_le)

   783     with divmod_step_simps

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

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

   786         by blast

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

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

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

   790       by (simp_all only: zero_less_numeral)

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

   792   qed

   793   then have "divmod m n =

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

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

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

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

   798     by (simp add: divmod_def)

   799   with False show ?thesis by simp

   800 qed

   801

   802 lemma divmod_eq [simp]:

   803   "m < n \<Longrightarrow> divmod m n = (0, numeral m)"

   804   "n \<le> m \<Longrightarrow> divmod m n = divmod_step n (divmod m (Num.Bit0 n))"

   805   by (auto simp add: divmod_divmod_step [of m n])

   806

   807 lemma divmod_cancel [simp, code]:

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

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

   810 proof -

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

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

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

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

   815   then show ?P and ?Q

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

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

   818 qed

   819

   820 text {* Special case: divisibility *}

   821

   822 definition divides_aux :: "'a \<times> 'a \<Rightarrow> bool"

   823 where

   824   "divides_aux qr \<longleftrightarrow> snd qr = 0"

   825

   826 lemma divides_aux_eq [simp]:

   827   "divides_aux (q, r) \<longleftrightarrow> r = 0"

   828   by (simp add: divides_aux_def)

   829

   830 lemma dvd_numeral_simp [simp]:

   831   "numeral m dvd numeral n \<longleftrightarrow> divides_aux (divmod n m)"

   832   by (simp add: divmod_def mod_eq_0_iff_dvd)

   833

   834 end

   835

   836

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

   838

   839 text {*

   840   We define @{const divide} and @{const mod} on @{typ nat} by means

   841   of a characteristic relation with two input arguments

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

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

   844 *}

   845

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

   847   "divmod_nat_rel m n qr \<longleftrightarrow>

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

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

   850

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

   852

   853 lemma divmod_nat_rel_ex:

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

   855 proof (cases "n = 0")

   856   case True  with that show thesis

   857     by (auto simp add: divmod_nat_rel_def)

   858 next

   859   case False

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

   861   proof (induct m)

   862     case 0 with n \<noteq> 0

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

   864     then show ?case by blast

   865   next

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

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

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

   869       case True

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

   871       with True show ?thesis by blast

   872     next

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

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

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

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

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

   878     qed

   879   qed

   880   with that show thesis

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

   882 qed

   883

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

   885

   886 lemma divmod_nat_rel_unique:

   887   assumes "divmod_nat_rel m n qr"

   888     and "divmod_nat_rel m n qr'"

   889   shows "qr = qr'"

   890 proof (cases "n = 0")

   891   case True with assms show ?thesis

   892     by (cases qr, cases qr')

   893       (simp add: divmod_nat_rel_def)

   894 next

   895   case False

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

   897   apply (rule leI)

   898   apply (subst less_iff_Suc_add)

   899   apply (auto simp add: add_mult_distrib)

   900   done

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

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

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

   904     by (simp add: divmod_nat_rel_def)

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

   906 qed

   907

   908 text {*

   909   We instantiate divisibility on the natural numbers by

   910   means of @{const divmod_nat_rel}:

   911 *}

   912

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

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

   915

   916 lemma divmod_nat_rel_divmod_nat:

   917   "divmod_nat_rel m n (divmod_nat m n)"

   918 proof -

   919   from divmod_nat_rel_ex

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

   921   then show ?thesis

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

   923 qed

   924

   925 lemma divmod_nat_unique:

   926   assumes "divmod_nat_rel m n qr"

   927   shows "divmod_nat m n = qr"

   928   using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)

   929

   930 instantiation nat :: semiring_div

   931 begin

   932

   933 definition divide_nat where

   934   div_nat_def: "m div n = fst (divmod_nat m n)"

   935

   936 definition mod_nat where

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

   938

   939 lemma fst_divmod_nat [simp]:

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

   941   by (simp add: div_nat_def)

   942

   943 lemma snd_divmod_nat [simp]:

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

   945   by (simp add: mod_nat_def)

   946

   947 lemma divmod_nat_div_mod:

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

   949   by (simp add: prod_eq_iff)

   950

   951 lemma div_nat_unique:

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

   953   shows "m div n = q"

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

   955

   956 lemma mod_nat_unique:

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

   958   shows "m mod n = r"

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

   960

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

   962   using divmod_nat_rel_divmod_nat by (simp add: divmod_nat_div_mod)

   963

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

   965   by (simp add: divmod_nat_unique divmod_nat_rel_def)

   966

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

   968   by (simp add: divmod_nat_unique divmod_nat_rel_def)

   969

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

   971   by (simp add: divmod_nat_unique divmod_nat_rel_def)

   972

   973 lemma divmod_nat_step:

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

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

   976 proof (rule divmod_nat_unique)

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

   978     by (rule divmod_nat_rel)

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

   980     unfolding divmod_nat_rel_def using assms by auto

   981 qed

   982

   983 text {* The ''recursion'' equations for @{const divide} and @{const mod} *}

   984

   985 lemma div_less [simp]:

   986   fixes m n :: nat

   987   assumes "m < n"

   988   shows "m div n = 0"

   989   using assms divmod_nat_base by (simp add: prod_eq_iff)

   990

   991 lemma le_div_geq:

   992   fixes m n :: nat

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

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

   995   using assms divmod_nat_step by (simp add: prod_eq_iff)

   996

   997 lemma mod_less [simp]:

   998   fixes m n :: nat

   999   assumes "m < n"

  1000   shows "m mod n = m"

  1001   using assms divmod_nat_base by (simp add: prod_eq_iff)

  1002

  1003 lemma le_mod_geq:

  1004   fixes m n :: nat

  1005   assumes "n \<le> m"

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

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

  1008

  1009 instance proof

  1010   fix m n :: nat

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

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

  1013 next

  1014   fix m n q :: nat

  1015   assume "n \<noteq> 0"

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

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

  1018 next

  1019   fix m n q :: nat

  1020   assume "m \<noteq> 0"

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

  1022     unfolding divmod_nat_rel_def

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

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

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

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

  1027 next

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

  1029     by (simp add: div_nat_def divmod_nat_zero)

  1030 next

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

  1032     by (simp add: div_nat_def divmod_nat_zero_left)

  1033 qed

  1034

  1035 end

  1036

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

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

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

  1040

  1041 text {* Simproc for cancelling @{const divide} and @{const mod} *}

  1042

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

  1044

  1045 ML {*

  1046 structure Cancel_Div_Mod_Nat = Cancel_Div_Mod

  1047 (

  1048   val div_name = @{const_name divide};

  1049   val mod_name = @{const_name mod};

  1050   val mk_binop = HOLogic.mk_binop;

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

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

  1053   fun mk_sum [] = HOLogic.zero

  1054     | mk_sum [t] = t

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

  1056   fun dest_sum tm =

  1057     if HOLogic.is_zero tm then []

  1058     else

  1059       (case try HOLogic.dest_Suc tm of

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

  1061       | NONE =>

  1062           (case try dest_plus tm of

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

  1064           | NONE => [tm]));

  1065

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

  1067

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

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

  1070 )

  1071 *}

  1072

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

  1074

  1075

  1076 subsubsection {* Quotient *}

  1077

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

  1079 by (simp add: le_div_geq linorder_not_less)

  1080

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

  1082 by (simp add: div_geq)

  1083

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

  1085 by simp

  1086

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

  1088 by simp

  1089

  1090 lemma div_positive:

  1091   fixes m n :: nat

  1092   assumes "n > 0"

  1093   assumes "m \<ge> n"

  1094   shows "m div n > 0"

  1095 proof -

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

  1097     by (auto simp add: le_iff_add)

  1098   with n > 0 show ?thesis by simp

  1099 qed

  1100

  1101 lemma div_eq_0_iff: "(a div b::nat) = 0 \<longleftrightarrow> a < b \<or> b = 0"

  1102   by (metis div_less div_positive div_by_0 gr0I less_numeral_extra(3) not_less)

  1103

  1104 subsubsection {* Remainder *}

  1105

  1106 lemma mod_less_divisor [simp]:

  1107   fixes m n :: nat

  1108   assumes "n > 0"

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

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

  1111

  1112 lemma mod_Suc_le_divisor [simp]:

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

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

  1115

  1116 lemma mod_less_eq_dividend [simp]:

  1117   fixes m n :: nat

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

  1119 proof (rule add_leD2)

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

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

  1122 qed

  1123

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

  1125 by (simp add: le_mod_geq linorder_not_less)

  1126

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

  1128 by (simp add: le_mod_geq)

  1129

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

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

  1132

  1133 (* a simple rearrangement of mod_div_equality: *)

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

  1135   using mod_div_equality2 [of n m] by arith

  1136

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

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

  1139   apply simp

  1140   done

  1141

  1142 subsubsection {* Quotient and Remainder *}

  1143

  1144 lemma divmod_nat_rel_mult1_eq:

  1145   "divmod_nat_rel b c (q, r)

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

  1147 by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps)

  1148

  1149 lemma div_mult1_eq:

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

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

  1152

  1153 lemma divmod_nat_rel_add1_eq:

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

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

  1156 by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps)

  1157

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

  1159 lemma div_add1_eq:

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

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

  1162

  1163 lemma divmod_nat_rel_mult2_eq:

  1164   assumes "divmod_nat_rel a b (q, r)"

  1165   shows "divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"

  1166 proof -

  1167   { assume "r < b" and "0 < c"

  1168     then have "b * (q mod c) + r < b * c"

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

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

  1171       apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)

  1172       apply (simp add: add_mult_distrib2)

  1173       done

  1174     then have "r + b * (q mod c) < b * c"

  1175       by (simp add: ac_simps)

  1176   } with assms show ?thesis

  1177     by (auto simp add: divmod_nat_rel_def algebra_simps add_mult_distrib2 [symmetric])

  1178 qed

  1179

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

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

  1182

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

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

  1185

  1186 instance nat :: semiring_numeral_div

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

  1188

  1189

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

  1191

  1192 lemma div_1 [simp]:

  1193   "m div Suc 0 = m"

  1194   using div_by_1 [of m] by simp

  1195

  1196 (* Monotonicity of div in first argument *)

  1197 lemma div_le_mono [rule_format (no_asm)]:

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

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

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

  1201 apply (case_tac "n<k")

  1202 (* 1  case n<k *)

  1203 apply simp

  1204 (* 2  case n >= k *)

  1205 apply (case_tac "m<k")

  1206 (* 2.1  case m<k *)

  1207 apply simp

  1208 (* 2.2  case m>=k *)

  1209 apply (simp add: div_geq diff_le_mono)

  1210 done

  1211

  1212 (* Antimonotonicity of div in second argument *)

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

  1214 apply (subgoal_tac "0<n")

  1215  prefer 2 apply simp

  1216 apply (induct_tac k rule: nat_less_induct)

  1217 apply (rename_tac "k")

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

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

  1220  prefer 2 apply simp

  1221 apply (simp add: div_geq)

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

  1223  prefer 2

  1224  apply (blast intro: div_le_mono diff_le_mono2)

  1225 apply (rule le_trans, simp)

  1226 apply (simp)

  1227 done

  1228

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

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

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

  1232 apply (rule div_le_mono2)

  1233 apply (simp_all (no_asm_simp))

  1234 done

  1235

  1236 (* Similar for "less than" *)

  1237 lemma div_less_dividend [simp]:

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

  1239 apply (induct m rule: nat_less_induct)

  1240 apply (rename_tac "m")

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

  1242 apply (subgoal_tac "0<n")

  1243  prefer 2 apply simp

  1244 apply (simp add: div_geq)

  1245 apply (case_tac "n<m")

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

  1247   apply (rule impI less_trans_Suc)+

  1248 apply assumption

  1249   apply (simp_all)

  1250 done

  1251

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

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

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

  1255 apply (induct "m" rule: nat_less_induct)

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

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

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

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

  1260 apply (simp add: linorder_not_less le_Suc_eq mod_geq)

  1261 apply (auto simp add: Suc_diff_le le_mod_geq)

  1262 done

  1263

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

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

  1266

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

  1268

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

  1270 lemma mod_eqD:

  1271   fixes m d r q :: nat

  1272   assumes "m mod d = r"

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

  1274 proof -

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

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

  1277   then show ?thesis ..

  1278 qed

  1279

  1280 lemma split_div:

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

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

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

  1284 proof

  1285   assume P: ?P

  1286   show ?Q

  1287   proof (cases)

  1288     assume "k = 0"

  1289     with P show ?Q by simp

  1290   next

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

  1292     thus ?Q

  1293     proof (simp, intro allI impI)

  1294       fix i j

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

  1296       show "P i"

  1297       proof (cases)

  1298         assume "i = 0"

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

  1300       next

  1301         assume "i \<noteq> 0"

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

  1303       qed

  1304     qed

  1305   qed

  1306 next

  1307   assume Q: ?Q

  1308   show ?P

  1309   proof (cases)

  1310     assume "k = 0"

  1311     with Q show ?P by simp

  1312   next

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

  1314     with Q have R: ?R by simp

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

  1316     show ?P by simp

  1317   qed

  1318 qed

  1319

  1320 lemma split_div_lemma:

  1321   assumes "0 < n"

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

  1323 proof

  1324   assume ?rhs

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

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

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

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

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

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

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

  1332   from A B show ?lhs ..

  1333 next

  1334   assume P: ?lhs

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

  1336     unfolding divmod_nat_rel_def by (auto simp add: ac_simps)

  1337   with divmod_nat_rel_unique divmod_nat_rel [of m n]

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

  1339   then show ?rhs by simp

  1340 qed

  1341

  1342 theorem split_div':

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

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

  1345   apply (case_tac "0 < n")

  1346   apply (simp only: add: split_div_lemma)

  1347   apply simp_all

  1348   done

  1349

  1350 lemma split_mod:

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

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

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

  1354 proof

  1355   assume P: ?P

  1356   show ?Q

  1357   proof (cases)

  1358     assume "k = 0"

  1359     with P show ?Q by simp

  1360   next

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

  1362     thus ?Q

  1363     proof (simp, intro allI impI)

  1364       fix i j

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

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

  1367     qed

  1368   qed

  1369 next

  1370   assume Q: ?Q

  1371   show ?P

  1372   proof (cases)

  1373     assume "k = 0"

  1374     with Q show ?P by simp

  1375   next

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

  1377     with Q have R: ?R by simp

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

  1379     show ?P by simp

  1380   qed

  1381 qed

  1382

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

  1384   using mod_div_equality [of m n] by arith

  1385

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

  1387   using mod_div_equality [of m n] by arith

  1388 (* FIXME: very similar to mult_div_cancel *)

  1389

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

  1391   apply rule

  1392   apply (cases "b = 0")

  1393   apply simp_all

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

  1395   done

  1396

  1397

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

  1399

  1400 lemma mod_induct_0:

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

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

  1403   shows "P 0"

  1404 proof (rule ccontr)

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

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

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

  1408   proof

  1409     fix k

  1410     show "?A k"

  1411     proof (induct k)

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

  1413     next

  1414       fix n

  1415       assume ih: "?A n"

  1416       show "?A (Suc n)"

  1417       proof (clarsimp)

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

  1419         have n: "Suc n < p"

  1420         proof (rule ccontr)

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

  1422           hence "p - Suc n = 0"

  1423             by simp

  1424           with y contra show "False"

  1425             by simp

  1426         qed

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

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

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

  1430           by blast

  1431         show "False"

  1432         proof (cases "n=0")

  1433           case True

  1434           with z n2 contra show ?thesis by simp

  1435         next

  1436           case False

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

  1438           with z n2 False ih show ?thesis by simp

  1439         qed

  1440       qed

  1441     qed

  1442   qed

  1443   moreover

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

  1445     by (blast dest: less_imp_add_positive)

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

  1447   moreover

  1448   note base

  1449   ultimately

  1450   show "False" by blast

  1451 qed

  1452

  1453 lemma mod_induct:

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

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

  1456   shows "P j"

  1457 proof -

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

  1459   proof

  1460     fix j

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

  1462     proof (induct j)

  1463       from step base i show "?A 0"

  1464         by (auto elim: mod_induct_0)

  1465     next

  1466       fix k

  1467       assume ih: "?A k"

  1468       show "?A (Suc k)"

  1469       proof

  1470         assume suc: "Suc k < p"

  1471         hence k: "k<p" by simp

  1472         with ih have "P k" ..

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

  1474           by blast

  1475         moreover

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

  1477           by simp

  1478         ultimately

  1479         show "P (Suc k)" by simp

  1480       qed

  1481     qed

  1482   qed

  1483   with j show ?thesis by blast

  1484 qed

  1485

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

  1487   by (simp add: numeral_2_eq_2 le_div_geq)

  1488

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

  1490   by (simp add: numeral_2_eq_2 le_mod_geq)

  1491

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

  1493 by (simp add: mult_2 [symmetric])

  1494

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

  1496 proof -

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

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

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

  1500   then show ?thesis by auto

  1501 qed

  1502

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

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

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

  1506

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

  1508 by (simp add: Suc3_eq_add_3)

  1509

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

  1511 by (simp add: Suc3_eq_add_3)

  1512

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

  1514 by (simp add: Suc3_eq_add_3)

  1515

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

  1517 by (simp add: Suc3_eq_add_3)

  1518

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

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

  1521

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

  1523 apply (induct "m")

  1524 apply (simp_all add: mod_Suc)

  1525 done

  1526

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

  1528

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

  1530 by (simp add: div_le_mono)

  1531

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

  1533 by (cases n) simp_all

  1534

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

  1536 proof -

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

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

  1539 qed

  1540

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

  1542 proof -

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

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

  1545   finally show ?thesis .

  1546 qed

  1547

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

  1549 apply (subst mod_Suc [of m])

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

  1551 done

  1552

  1553 lemma mod_2_not_eq_zero_eq_one_nat:

  1554   fixes n :: nat

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

  1556   by (fact not_mod_2_eq_0_eq_1)

  1557

  1558 lemma even_Suc_div_two [simp]:

  1559   "even n \<Longrightarrow> Suc n div 2 = n div 2"

  1560   using even_succ_div_two [of n] by simp

  1561

  1562 lemma odd_Suc_div_two [simp]:

  1563   "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"

  1564   using odd_succ_div_two [of n] by simp

  1565

  1566 lemma odd_two_times_div_two_nat [simp]:

  1567   assumes "odd n"

  1568   shows "2 * (n div 2) = n - (1 :: nat)"

  1569 proof -

  1570   from assms have "2 * (n div 2) + 1 = n"

  1571     by (rule odd_two_times_div_two_succ)

  1572   then have "Suc (2 * (n div 2)) - 1 = n - 1"

  1573     by simp

  1574   then show ?thesis

  1575     by simp

  1576 qed

  1577

  1578 lemma odd_Suc_minus_one [simp]:

  1579   "odd n \<Longrightarrow> Suc (n - Suc 0) = n"

  1580   by (auto elim: oddE)

  1581

  1582 lemma parity_induct [case_names zero even odd]:

  1583   assumes zero: "P 0"

  1584   assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"

  1585   assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"

  1586   shows "P n"

  1587 proof (induct n rule: less_induct)

  1588   case (less n)

  1589   show "P n"

  1590   proof (cases "n = 0")

  1591     case True with zero show ?thesis by simp

  1592   next

  1593     case False

  1594     with less have hyp: "P (n div 2)" by simp

  1595     show ?thesis

  1596     proof (cases "even n")

  1597       case True

  1598       with hyp even [of "n div 2"] show ?thesis

  1599         by simp

  1600     next

  1601       case False

  1602       with hyp odd [of "n div 2"] show ?thesis

  1603         by simp

  1604     qed

  1605   qed

  1606 qed

  1607

  1608

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

  1610

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

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

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

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

  1615

  1616 text {*

  1617   The following algorithmic devlopment actually echos what has already

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

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

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

  1621   accordingly.

  1622 *}

  1623

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

  1625     --{*for the division algorithm*}

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

  1627                          else (2 * q, r))"

  1628

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

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

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

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

  1633 by auto

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

  1635   (auto simp add: mult_2)

  1636

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

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

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

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

  1641 by auto

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

  1643   (auto simp add: mult_2)

  1644

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

  1646

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

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

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

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

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

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

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

  1654                else

  1655                   if 0 < b then negDivAlg a b

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

  1657

  1658 instantiation int :: ring_div

  1659 begin

  1660

  1661 definition divide_int where

  1662   div_int_def: "a div b = fst (divmod_int a b)"

  1663

  1664 definition mod_int where

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

  1666

  1667 lemma fst_divmod_int [simp]:

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

  1669   by (simp add: div_int_def)

  1670

  1671 lemma snd_divmod_int [simp]:

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

  1673   by (simp add: mod_int_def)

  1674

  1675 lemma divmod_int_mod_div:

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

  1677   by (simp add: prod_eq_iff)

  1678

  1679 text{*

  1680 Here is the division algorithm in ML:

  1681

  1682 \begin{verbatim}

  1683     fun posDivAlg (a,b) =

  1684       if a<b then (0,a)

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

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

  1687            end

  1688

  1689     fun negDivAlg (a,b) =

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

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

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

  1693            end;

  1694

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

  1696

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

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

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

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

  1701                        else

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

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

  1704 \end{verbatim}

  1705 *}

  1706

  1707

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

  1709

  1710 lemma unique_quotient_lemma:

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

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

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

  1714  prefer 2 apply (simp add: right_diff_distrib)

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

  1716 apply (erule_tac [2] order_le_less_trans)

  1717  prefer 2 apply (simp add: right_diff_distrib distrib_left)

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

  1719  prefer 2 apply (simp add: right_diff_distrib distrib_left)

  1720 apply (simp add: mult_less_cancel_left)

  1721 done

  1722

  1723 lemma unique_quotient_lemma_neg:

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

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

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

  1727     auto)

  1728

  1729 lemma unique_quotient:

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

  1731       ==> q = q'"

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

  1733 apply (blast intro: order_antisym

  1734              dest: order_eq_refl [THEN unique_quotient_lemma]

  1735              order_eq_refl [THEN unique_quotient_lemma_neg] sym)+

  1736 done

  1737

  1738

  1739 lemma unique_remainder:

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

  1741       ==> r = r'"

  1742 apply (subgoal_tac "q = q'")

  1743  apply (simp add: divmod_int_rel_def)

  1744 apply (blast intro: unique_quotient)

  1745 done

  1746

  1747

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

  1749

  1750 text{*And positive divisors*}

  1751

  1752 lemma adjust_eq [simp]:

  1753      "adjust b (q, r) =

  1754       (let diff = r - b in

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

  1756                      else (2*q, r))"

  1757   by (simp add: Let_def adjust_def)

  1758

  1759 declare posDivAlg.simps [simp del]

  1760

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

  1762 lemma posDivAlg_eqn:

  1763      "0 < b ==>

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

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

  1766

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

  1768 theorem posDivAlg_correct:

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

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

  1771   using assms

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

  1773   apply auto

  1774   apply (simp add: divmod_int_rel_def)

  1775   apply (subst posDivAlg_eqn, simp add: distrib_left)

  1776   apply (case_tac "a < b")

  1777   apply simp_all

  1778   apply (erule splitE)

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

  1780   done

  1781

  1782

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

  1784

  1785 text{*And positive divisors*}

  1786

  1787 declare negDivAlg.simps [simp del]

  1788

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

  1790 lemma negDivAlg_eqn:

  1791      "0 < b ==>

  1792       negDivAlg a b =

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

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

  1795

  1796 (*Correctness of negDivAlg: it computes quotients correctly

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

  1798 lemma negDivAlg_correct:

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

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

  1801   using assms

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

  1803   apply (auto simp add: linorder_not_le)

  1804   apply (simp add: divmod_int_rel_def)

  1805   apply (subst negDivAlg_eqn, assumption)

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

  1807   apply simp_all

  1808   apply (erule splitE)

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

  1810   done

  1811

  1812

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

  1814

  1815 (*the case a=0*)

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

  1817 by (auto simp add: divmod_int_rel_def linorder_neq_iff)

  1818

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

  1820 by (subst posDivAlg.simps, auto)

  1821

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

  1823 by (subst posDivAlg.simps, auto)

  1824

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

  1826 by (subst negDivAlg.simps, auto)

  1827

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

  1829 by (auto simp add: divmod_int_rel_def)

  1830

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

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

  1833 by (force simp add: linorder_neq_iff divmod_int_rel_0 divmod_int_def divmod_int_rel_neg

  1834                     posDivAlg_correct negDivAlg_correct)

  1835

  1836 lemma divmod_int_unique:

  1837   assumes "divmod_int_rel a b qr"

  1838   shows "divmod_int a b = qr"

  1839   using assms divmod_int_correct [of a b]

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

  1841   by (metis pair_collapse)

  1842

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

  1844   using divmod_int_correct by (simp add: divmod_int_mod_div)

  1845

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

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

  1848

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

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

  1851

  1852 instance

  1853 proof

  1854   fix a b :: int

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

  1856     using divmod_int_rel_div_mod [of a b]

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

  1858 next

  1859   fix a b c :: int

  1860   assume "b \<noteq> 0"

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

  1862     using divmod_int_rel_div_mod [of a b]

  1863     unfolding divmod_int_rel_def by (auto simp: algebra_simps)

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

  1865     by (rule div_int_unique)

  1866 next

  1867   fix a b c :: int

  1868   assume "c \<noteq> 0"

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

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

  1871     unfolding divmod_int_rel_def

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

  1873       mult_less_0_iff zero_less_mult_iff mult_strict_right_mono

  1874       mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff)

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

  1876     using divmod_int_rel_div_mod [of a b] .

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

  1878     by (rule div_int_unique)

  1879 next

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

  1881     by (rule div_int_unique, simp add: divmod_int_rel_def)

  1882 next

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

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

  1885 qed

  1886

  1887 end

  1888

  1889 lemma is_unit_int:

  1890   "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"

  1891   by auto

  1892

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

  1894

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

  1896   by (fact mod_div_equality2 [symmetric])

  1897

  1898 text {* Tool setup *}

  1899

  1900 ML {*

  1901 structure Cancel_Div_Mod_Int = Cancel_Div_Mod

  1902 (

  1903   val div_name = @{const_name Rings.divide};

  1904   val mod_name = @{const_name mod};

  1905   val mk_binop = HOLogic.mk_binop;

  1906   val mk_sum = Arith_Data.mk_sum HOLogic.intT;

  1907   val dest_sum = Arith_Data.dest_sum;

  1908

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

  1910

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

  1912     (@{thm diff_conv_add_uminus} :: @{thms add_0_left add_0_right} @ @{thms ac_simps}))

  1913 )

  1914 *}

  1915

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

  1917

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

  1919   using divmod_int_correct [of a b]

  1920   by (auto simp add: divmod_int_rel_def prod_eq_iff)

  1921

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

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

  1924

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

  1926   using divmod_int_correct [of a b]

  1927   by (auto simp add: divmod_int_rel_def prod_eq_iff)

  1928

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

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

  1931

  1932

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

  1934

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

  1936 apply (rule div_int_unique)

  1937 apply (auto simp add: divmod_int_rel_def)

  1938 done

  1939

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

  1941 apply (rule div_int_unique)

  1942 apply (auto simp add: divmod_int_rel_def)

  1943 done

  1944

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

  1946 apply (rule div_int_unique)

  1947 apply (auto simp add: divmod_int_rel_def)

  1948 done

  1949

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

  1951

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

  1953 apply (rule_tac q = 0 in mod_int_unique)

  1954 apply (auto simp add: divmod_int_rel_def)

  1955 done

  1956

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

  1958 apply (rule_tac q = 0 in mod_int_unique)

  1959 apply (auto simp add: divmod_int_rel_def)

  1960 done

  1961

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

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

  1964 apply (auto simp add: divmod_int_rel_def)

  1965 done

  1966

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

  1968

  1969

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

  1971

  1972 lemma zminus1_lemma:

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

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

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

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

  1977

  1978

  1979 lemma zdiv_zminus1_eq_if:

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

  1981       ==> (-a) div b =

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

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

  1984

  1985 lemma zmod_zminus1_eq_if:

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

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

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

  1989 done

  1990

  1991 lemma zmod_zminus1_not_zero:

  1992   fixes k l :: int

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

  1994   unfolding zmod_zminus1_eq_if by auto

  1995

  1996 lemma zdiv_zminus2_eq_if:

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

  1998       ==> a div (-b) =

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

  2000 by (simp add: zdiv_zminus1_eq_if div_minus_right)

  2001

  2002 lemma zmod_zminus2_eq_if:

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

  2004 by (simp add: zmod_zminus1_eq_if mod_minus_right)

  2005

  2006 lemma zmod_zminus2_not_zero:

  2007   fixes k l :: int

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

  2009   unfolding zmod_zminus2_eq_if by auto

  2010

  2011

  2012 subsubsection {* Computation of Division and Remainder *}

  2013

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

  2015 by (simp add: div_int_def divmod_int_def)

  2016

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

  2018 by (simp add: mod_int_def divmod_int_def)

  2019

  2020 text{*a positive, b positive *}

  2021

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

  2023 by (simp add: div_int_def divmod_int_def)

  2024

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

  2026 by (simp add: mod_int_def divmod_int_def)

  2027

  2028 text{*a negative, b positive *}

  2029

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

  2031 by (simp add: div_int_def divmod_int_def)

  2032

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

  2034 by (simp add: mod_int_def divmod_int_def)

  2035

  2036 text{*a positive, b negative *}

  2037

  2038 lemma div_pos_neg:

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

  2040 by (simp add: div_int_def divmod_int_def)

  2041

  2042 lemma mod_pos_neg:

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

  2044 by (simp add: mod_int_def divmod_int_def)

  2045

  2046 text{*a negative, b negative *}

  2047

  2048 lemma div_neg_neg:

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

  2050 by (simp add: div_int_def divmod_int_def)

  2051

  2052 lemma mod_neg_neg:

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

  2054 by (simp add: mod_int_def divmod_int_def)

  2055

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

  2057

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

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

  2060

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

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

  2063     simp add: divmod_int_rel_def)

  2064

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

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

  2067     simp add: divmod_int_rel_def)

  2068

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

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

  2071     simp add: divmod_int_rel_def)

  2072

  2073 text {*

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

  2075   by divmod algorithm from @{class semiring_numeral_div}

  2076 *}

  2077

  2078 ML {*

  2079 local

  2080   val mk_number = HOLogic.mk_number HOLogic.intT

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

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

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

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

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

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

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

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

  2089   fun binary_proc proc ctxt ct =

  2090     (case Thm.term_of ct of

  2091       _ $t$ u =>

  2092       (case try (apply2 ((snd o HOLogic.dest_number))) (t, u) of

  2093         SOME args => proc ctxt args

  2094       | NONE => NONE)

  2095     | _ => NONE);

  2096 in

  2097   fun divmod_proc posrule negrule =

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

  2099       if b = 0 then NONE

  2100       else

  2101         let

  2102           val (q, r) = apply2 mk_number (Integer.div_mod a b)

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

  2104           val (goal2, goal3, rule) =

  2105             if b > 0

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

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

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

  2109 end

  2110 *}

  2111

  2112 simproc_setup binary_int_div

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

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

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

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

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

  2118

  2119 simproc_setup binary_int_mod

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

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

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

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

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

  2125

  2126 lemmas posDivAlg_eqn_numeral [simp] =

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

  2128

  2129 lemmas negDivAlg_eqn_numeral [simp] =

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

  2131

  2132

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

  2134

  2135 lemma [simp]:

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

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

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

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

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

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

  2142   by (simp_all del: arith_special

  2143     add: div_pos_pos mod_pos_pos div_pos_neg mod_pos_neg posDivAlg_eqn)

  2144

  2145 lemma [simp]:

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

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

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

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

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

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

  2152   by (simp_all add: div_eq_minus1 zmod_minus1)

  2153

  2154

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

  2156

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

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

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

  2160 apply (rule unique_quotient_lemma)

  2161 apply (erule subst)

  2162 apply (erule subst, simp_all)

  2163 done

  2164

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

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

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

  2168 apply (rule unique_quotient_lemma_neg)

  2169 apply (erule subst)

  2170 apply (erule subst, simp_all)

  2171 done

  2172

  2173

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

  2175

  2176 lemma q_pos_lemma:

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

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

  2179  apply (simp add: zero_less_mult_iff)

  2180 apply (simp add: distrib_left)

  2181 done

  2182

  2183 lemma zdiv_mono2_lemma:

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

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

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

  2187 apply (frule q_pos_lemma, assumption+)

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

  2189  apply (simp add: mult_less_cancel_left)

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

  2191  prefer 2 apply simp

  2192 apply (simp (no_asm_simp) add: distrib_left)

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

  2194 apply (rule mult_right_mono, auto)

  2195 done

  2196

  2197 lemma zdiv_mono2:

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

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

  2200  prefer 2 apply arith

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

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

  2203 apply (rule zdiv_mono2_lemma)

  2204 apply (erule subst)

  2205 apply (erule subst, simp_all)

  2206 done

  2207

  2208 lemma q_neg_lemma:

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

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

  2211  apply (simp add: mult_less_0_iff, arith)

  2212 done

  2213

  2214 lemma zdiv_mono2_neg_lemma:

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

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

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

  2218 apply (frule q_neg_lemma, assumption+)

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

  2220  apply (simp add: mult_less_cancel_left)

  2221 apply (simp add: distrib_left)

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

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

  2224 done

  2225

  2226 lemma zdiv_mono2_neg:

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

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

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

  2230 apply (rule zdiv_mono2_neg_lemma)

  2231 apply (erule subst)

  2232 apply (erule subst, simp_all)

  2233 done

  2234

  2235

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

  2237

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

  2239

  2240 lemma zmult1_lemma:

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

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

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

  2244

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

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

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

  2248 done

  2249

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

  2251

  2252 lemma zadd1_lemma:

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

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

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

  2256

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

  2258 lemma zdiv_zadd1_eq:

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

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

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

  2262 done

  2263

  2264 lemma posDivAlg_div_mod:

  2265   assumes "k \<ge> 0"

  2266   and "l \<ge> 0"

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

  2268 proof (cases "l = 0")

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

  2270 next

  2271   case False with assms posDivAlg_correct

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

  2273     by simp

  2274   from div_int_unique [OF this] mod_int_unique [OF this]

  2275   show ?thesis by simp

  2276 qed

  2277

  2278 lemma negDivAlg_div_mod:

  2279   assumes "k < 0"

  2280   and "l > 0"

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

  2282 proof -

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

  2284   from assms negDivAlg_correct

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

  2286     by simp

  2287   from div_int_unique [OF this] mod_int_unique [OF this]

  2288   show ?thesis by simp

  2289 qed

  2290

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

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

  2293

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

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

  2296

  2297 lemma zmod_zdiv_equality':

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

  2299   using mod_div_equality [of m n] by arith

  2300

  2301

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

  2303

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

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

  2306   to cause particular problems.*)

  2307

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

  2309

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

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

  2312  apply (simp add: algebra_simps)

  2313 apply (rule order_le_less_trans)

  2314  apply (erule_tac [2] mult_strict_right_mono)

  2315  apply (rule mult_left_mono_neg)

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

  2317  apply (simp)

  2318 apply (simp)

  2319 done

  2320

  2321 lemma zmult2_lemma_aux2:

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

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

  2324  apply arith

  2325 apply (simp add: mult_le_0_iff)

  2326 done

  2327

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

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

  2330 apply arith

  2331 apply (simp add: zero_le_mult_iff)

  2332 done

  2333

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

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

  2336  apply (simp add: right_diff_distrib)

  2337 apply (rule order_less_le_trans)

  2338  apply (erule mult_strict_right_mono)

  2339  apply (rule_tac [2] mult_left_mono)

  2340   apply simp

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

  2342 apply simp

  2343 done

  2344

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

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

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

  2348                    zero_less_mult_iff distrib_left [symmetric]

  2349                    zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: split_if_asm)

  2350

  2351 lemma zdiv_zmult2_eq:

  2352   fixes a b c :: int

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

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

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

  2356 done

  2357

  2358 lemma zmod_zmult2_eq:

  2359   fixes a b c :: int

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

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

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

  2363 done

  2364

  2365 lemma div_pos_geq:

  2366   fixes k l :: int

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

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

  2369 proof -

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

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

  2372   with assms show ?thesis by simp

  2373 qed

  2374

  2375 lemma mod_pos_geq:

  2376   fixes k l :: int

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

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

  2379 proof -

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

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

  2382   with assms show ?thesis by simp

  2383 qed

  2384

  2385

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

  2387

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

  2389

  2390 lemma split_pos_lemma:

  2391  "0<k ==>

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

  2393 apply (rule iffI, clarify)

  2394  apply (erule_tac P="P x y" for x y in rev_mp)

  2395  apply (subst mod_add_eq)

  2396  apply (subst zdiv_zadd1_eq)

  2397  apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)

  2398 txt{*converse direction*}

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

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

  2401 done

  2402

  2403 lemma split_neg_lemma:

  2404  "k<0 ==>

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

  2406 apply (rule iffI, clarify)

  2407  apply (erule_tac P="P x y" for x y in rev_mp)

  2408  apply (subst mod_add_eq)

  2409  apply (subst zdiv_zadd1_eq)

  2410  apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)

  2411 txt{*converse direction*}

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

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

  2414 done

  2415

  2416 lemma split_zdiv:

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

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

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

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

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

  2422 apply (simp only: linorder_neq_iff)

  2423 apply (erule disjE)

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

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

  2426 done

  2427

  2428 lemma split_zmod:

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

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

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

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

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

  2434 apply (simp only: linorder_neq_iff)

  2435 apply (erule disjE)

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

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

  2438 done

  2439

  2440 text {* Enable (lin)arith to deal with @{const divide} and @{const mod}

  2441   when these are applied to some constant that is of the form

  2442   @{term "numeral k"}: *}

  2443 declare split_zdiv [of _ _ "numeral k", arith_split] for k

  2444 declare split_zmod [of _ _ "numeral k", arith_split] for k

  2445

  2446

  2447 subsubsection {* Computing @{text "div"} and @{text "mod"} with shifting *}

  2448

  2449 lemma pos_divmod_int_rel_mult_2:

  2450   assumes "0 \<le> b"

  2451   assumes "divmod_int_rel a b (q, r)"

  2452   shows "divmod_int_rel (1 + 2*a) (2*b) (q, 1 + 2*r)"

  2453   using assms unfolding divmod_int_rel_def by auto

  2454

  2455 declaration {* K (Lin_Arith.add_simps @{thms uminus_numeral_One}) *}

  2456

  2457 lemma neg_divmod_int_rel_mult_2:

  2458   assumes "b \<le> 0"

  2459   assumes "divmod_int_rel (a + 1) b (q, r)"

  2460   shows "divmod_int_rel (1 + 2*a) (2*b) (q, 2*r - 1)"

  2461   using assms unfolding divmod_int_rel_def by auto

  2462

  2463 text{*computing div by shifting *}

  2464

  2465 lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a"

  2466   using pos_divmod_int_rel_mult_2 [OF _ divmod_int_rel_div_mod]

  2467   by (rule div_int_unique)

  2468

  2469 lemma neg_zdiv_mult_2:

  2470   assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"

  2471   using neg_divmod_int_rel_mult_2 [OF A divmod_int_rel_div_mod]

  2472   by (rule div_int_unique)

  2473

  2474 (* FIXME: add rules for negative numerals *)

  2475 lemma zdiv_numeral_Bit0 [simp]:

  2476   "numeral (Num.Bit0 v) div numeral (Num.Bit0 w) =

  2477     numeral v div (numeral w :: int)"

  2478   unfolding numeral.simps unfolding mult_2 [symmetric]

  2479   by (rule div_mult_mult1, simp)

  2480

  2481 lemma zdiv_numeral_Bit1 [simp]:

  2482   "numeral (Num.Bit1 v) div numeral (Num.Bit0 w) =

  2483     (numeral v div (numeral w :: int))"

  2484   unfolding numeral.simps

  2485   unfolding mult_2 [symmetric] add.commute [of _ 1]

  2486   by (rule pos_zdiv_mult_2, simp)

  2487

  2488 lemma pos_zmod_mult_2:

  2489   fixes a b :: int

  2490   assumes "0 \<le> a"

  2491   shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)"

  2492   using pos_divmod_int_rel_mult_2 [OF assms divmod_int_rel_div_mod]

  2493   by (rule mod_int_unique)

  2494

  2495 lemma neg_zmod_mult_2:

  2496   fixes a b :: int

  2497   assumes "a \<le> 0"

  2498   shows "(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1"

  2499   using neg_divmod_int_rel_mult_2 [OF assms divmod_int_rel_div_mod]

  2500   by (rule mod_int_unique)

  2501

  2502 (* FIXME: add rules for negative numerals *)

  2503 lemma zmod_numeral_Bit0 [simp]:

  2504   "numeral (Num.Bit0 v) mod numeral (Num.Bit0 w) =

  2505     (2::int) * (numeral v mod numeral w)"

  2506   unfolding numeral_Bit0 [of v] numeral_Bit0 [of w]

  2507   unfolding mult_2 [symmetric] by (rule mod_mult_mult1)

  2508

  2509 lemma zmod_numeral_Bit1 [simp]:

  2510   "numeral (Num.Bit1 v) mod numeral (Num.Bit0 w) =

  2511     2 * (numeral v mod numeral w) + (1::int)"

  2512   unfolding numeral_Bit1 [of v] numeral_Bit0 [of w]

  2513   unfolding mult_2 [symmetric] add.commute [of _ 1]

  2514   by (rule pos_zmod_mult_2, simp)

  2515

  2516 lemma zdiv_eq_0_iff:

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

  2518 proof

  2519   assume ?L

  2520   have "?L \<longrightarrow> ?R" by (rule split_zdiv[THEN iffD2]) simp

  2521   with ?L show ?R by blast

  2522 next

  2523   assume ?R thus ?L

  2524     by(auto simp: div_pos_pos_trivial div_neg_neg_trivial)

  2525 qed

  2526

  2527

  2528 subsubsection {* Quotients of Signs *}

  2529

  2530 lemma div_neg_pos_less0: "[| a < (0::int);  0 < b |] ==> a div b < 0"

  2531 apply (subgoal_tac "a div b \<le> -1", force)

  2532 apply (rule order_trans)

  2533 apply (rule_tac a' = "-1" in zdiv_mono1)

  2534 apply (auto simp add: div_eq_minus1)

  2535 done

  2536

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

  2538 by (drule zdiv_mono1_neg, auto)

  2539

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

  2541 by (drule zdiv_mono1, auto)

  2542

  2543 text{* Now for some equivalences of the form @{text"a div b >=< 0 \<longleftrightarrow> \<dots>"}

  2544 conditional upon the sign of @{text a} or @{text b}. There are many more.

  2545 They should all be simp rules unless that causes too much search. *}

  2546

  2547 lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)"

  2548 apply auto

  2549 apply (drule_tac [2] zdiv_mono1)

  2550 apply (auto simp add: linorder_neq_iff)

  2551 apply (simp (no_asm_use) add: linorder_not_less [symmetric])

  2552 apply (blast intro: div_neg_pos_less0)

  2553 done

  2554

  2555 lemma neg_imp_zdiv_nonneg_iff:

  2556   "b < (0::int) ==> (0 \<le> a div b) = (a \<le> (0::int))"

  2557 apply (subst div_minus_minus [symmetric])

  2558 apply (subst pos_imp_zdiv_nonneg_iff, auto)

  2559 done

  2560

  2561 (*But not (a div b \<le> 0 iff a\<le>0); consider a=1, b=2 when a div b = 0.*)

  2562 lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)"

  2563 by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff)

  2564

  2565 lemma pos_imp_zdiv_pos_iff:

  2566   "0<k \<Longrightarrow> 0 < (i::int) div k \<longleftrightarrow> k \<le> i"

  2567 using pos_imp_zdiv_nonneg_iff[of k i] zdiv_eq_0_iff[of i k]

  2568 by arith

  2569

  2570 (*Again the law fails for \<le>: consider a = -1, b = -2 when a div b = 0*)

  2571 lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)"

  2572 by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)

  2573

  2574 lemma nonneg1_imp_zdiv_pos_iff:

  2575   "(0::int) <= a \<Longrightarrow> (a div b > 0) = (a >= b & b>0)"

  2576 apply rule

  2577  apply rule

  2578   using div_pos_pos_trivial[of a b]apply arith

  2579  apply(cases "b=0")apply simp

  2580  using div_nonneg_neg_le0[of a b]apply arith

  2581 using int_one_le_iff_zero_less[of "a div b"] zdiv_mono1[of b a b]apply simp

  2582 done

  2583

  2584 lemma zmod_le_nonneg_dividend: "(m::int) \<ge> 0 ==> m mod k \<le> m"

  2585 apply (rule split_zmod[THEN iffD2])

  2586 apply(fastforce dest: q_pos_lemma intro: split_mult_pos_le)

  2587 done

  2588

  2589

  2590 subsubsection {* The Divides Relation *}

  2591

  2592 lemma dvd_eq_mod_eq_0_numeral:

  2593   "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semiring_div)"

  2594   by (fact dvd_eq_mod_eq_0)

  2595

  2596

  2597 subsubsection {* Further properties *}

  2598

  2599 lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"

  2600   using zmod_zdiv_equality[where a="m" and b="n"]

  2601   by (simp add: algebra_simps) (* FIXME: generalize *)

  2602

  2603 instance int :: semiring_numeral_div

  2604   by intro_classes (auto intro: zmod_le_nonneg_dividend

  2605     simp add: zmult_div_cancel

  2606     pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial

  2607     zmod_zmult2_eq zdiv_zmult2_eq)

  2608

  2609 lemma zdiv_int: "int (a div b) = (int a) div (int b)"

  2610 apply (subst split_div, auto)

  2611 apply (subst split_zdiv, auto)

  2612 apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in unique_quotient)

  2613 apply (auto simp add: divmod_int_rel_def of_nat_mult)

  2614 done

  2615

  2616 lemma zmod_int: "int (a mod b) = (int a) mod (int b)"

  2617 apply (subst split_mod, auto)

  2618 apply (subst split_zmod, auto)

  2619 apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia

  2620        in unique_remainder)

  2621 apply (auto simp add: divmod_int_rel_def of_nat_mult)

  2622 done

  2623

  2624 lemma abs_div: "(y::int) dvd x \<Longrightarrow> abs (x div y) = abs x div abs y"

  2625 by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)

  2626

  2627 text{*Suggested by Matthias Daum*}

  2628 lemma int_power_div_base:

  2629      "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"

  2630 apply (subgoal_tac "k ^ m = k ^ ((m - Suc 0) + Suc 0)")

  2631  apply (erule ssubst)

  2632  apply (simp only: power_add)

  2633  apply simp_all

  2634 done

  2635

  2636 text {* by Brian Huffman *}

  2637 lemma zminus_zmod: "- ((x::int) mod m) mod m = - x mod m"

  2638 by (rule mod_minus_eq [symmetric])

  2639

  2640 lemma zdiff_zmod_left: "(x mod m - y) mod m = (x - y) mod (m::int)"

  2641 by (rule mod_diff_left_eq [symmetric])

  2642

  2643 lemma zdiff_zmod_right: "(x - y mod m) mod m = (x - y) mod (m::int)"

  2644 by (rule mod_diff_right_eq [symmetric])

  2645

  2646 lemmas zmod_simps =

  2647   mod_add_left_eq  [symmetric]

  2648   mod_add_right_eq [symmetric]

  2649   mod_mult_right_eq[symmetric]

  2650   mod_mult_left_eq [symmetric]

  2651   power_mod

  2652   zminus_zmod zdiff_zmod_left zdiff_zmod_right

  2653

  2654 text {* Distributive laws for function @{text nat}. *}

  2655

  2656 lemma nat_div_distrib: "0 \<le> x \<Longrightarrow> nat (x div y) = nat x div nat y"

  2657 apply (rule linorder_cases [of y 0])

  2658 apply (simp add: div_nonneg_neg_le0)

  2659 apply simp

  2660 apply (simp add: nat_eq_iff pos_imp_zdiv_nonneg_iff zdiv_int)

  2661 done

  2662

  2663 (*Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't*)

  2664 lemma nat_mod_distrib:

  2665   "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x mod y) = nat x mod nat y"

  2666 apply (case_tac "y = 0", simp)

  2667 apply (simp add: nat_eq_iff zmod_int)

  2668 done

  2669

  2670 text  {* transfer setup *}

  2671

  2672 lemma transfer_nat_int_functions:

  2673     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"

  2674     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"

  2675   by (auto simp add: nat_div_distrib nat_mod_distrib)

  2676

  2677 lemma transfer_nat_int_function_closures:

  2678     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"

  2679     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"

  2680   apply (cases "y = 0")

  2681   apply (auto simp add: pos_imp_zdiv_nonneg_iff)

  2682   apply (cases "y = 0")

  2683   apply auto

  2684 done

  2685

  2686 declare transfer_morphism_nat_int [transfer add return:

  2687   transfer_nat_int_functions

  2688   transfer_nat_int_function_closures

  2689 ]

  2690

  2691 lemma transfer_int_nat_functions:

  2692     "(int x) div (int y) = int (x div y)"

  2693     "(int x) mod (int y) = int (x mod y)"

  2694   by (auto simp add: zdiv_int zmod_int)

  2695

  2696 lemma transfer_int_nat_function_closures:

  2697     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"

  2698     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"

  2699   by (simp_all only: is_nat_def transfer_nat_int_function_closures)

  2700

  2701 declare transfer_morphism_int_nat [transfer add return:

  2702   transfer_int_nat_functions

  2703   transfer_int_nat_function_closures

  2704 ]

  2705

  2706 text{*Suggested by Matthias Daum*}

  2707 lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"

  2708 apply (subgoal_tac "nat x div nat k < nat x")

  2709  apply (simp add: nat_div_distrib [symmetric])

  2710 apply (rule Divides.div_less_dividend, simp_all)

  2711 done

  2712

  2713 lemma zmod_eq_dvd_iff: "(x::int) mod n = y mod n \<longleftrightarrow> n dvd x - y"

  2714 proof

  2715   assume H: "x mod n = y mod n"

  2716   hence "x mod n - y mod n = 0" by simp

  2717   hence "(x mod n - y mod n) mod n = 0" by simp

  2718   hence "(x - y) mod n = 0" by (simp add: mod_diff_eq[symmetric])

  2719   thus "n dvd x - y" by (simp add: dvd_eq_mod_eq_0)

  2720 next

  2721   assume H: "n dvd x - y"

  2722   then obtain k where k: "x-y = n*k" unfolding dvd_def by blast

  2723   hence "x = n*k + y" by simp

  2724   hence "x mod n = (n*k + y) mod n" by simp

  2725   thus "x mod n = y mod n" by (simp add: mod_add_left_eq)

  2726 qed

  2727

  2728 lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y  mod n" and xy:"y \<le> x"

  2729   shows "\<exists>q. x = y + n * q"

  2730 proof-

  2731   from xy have th: "int x - int y = int (x - y)" by simp

  2732   from xyn have "int x mod int n = int y mod int n"

  2733     by (simp add: zmod_int [symmetric])

  2734   hence "int n dvd int x - int y" by (simp only: zmod_eq_dvd_iff[symmetric])

  2735   hence "n dvd x - y" by (simp add: th zdvd_int)

  2736   then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith

  2737 qed

  2738

  2739 lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)"

  2740   (is "?lhs = ?rhs")

  2741 proof

  2742   assume H: "x mod n = y mod n"

  2743   {assume xy: "x \<le> y"

  2744     from H have th: "y mod n = x mod n" by simp

  2745     from nat_mod_eq_lemma[OF th xy] have ?rhs

  2746       apply clarify  apply (rule_tac x="q" in exI) by (rule exI[where x="0"], simp)}

  2747   moreover

  2748   {assume xy: "y \<le> x"

  2749     from nat_mod_eq_lemma[OF H xy] have ?rhs

  2750       apply clarify  apply (rule_tac x="0" in exI) by (rule_tac x="q" in exI, simp)}

  2751   ultimately  show ?rhs using linear[of x y] by blast

  2752 next

  2753   assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast

  2754   hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp

  2755   thus  ?lhs by simp

  2756 qed

  2757

  2758 text {*

  2759   This re-embedding of natural division on integers goes back to the

  2760   time when numerals had been signed numerals.  It should

  2761   now be replaced by the algorithm developed in @{class semiring_numeral_div}.

  2762 *}

  2763

  2764 lemma div_nat_numeral [simp]:

  2765   "(numeral v :: nat) div numeral v' = nat (numeral v div numeral v')"

  2766   by (simp add: nat_div_distrib)

  2767

  2768 lemma one_div_nat_numeral [simp]:

  2769   "Suc 0 div numeral v' = nat (1 div numeral v')"

  2770   by (subst nat_div_distrib, simp_all)

  2771

  2772 lemma mod_nat_numeral [simp]:

  2773   "(numeral v :: nat) mod numeral v' = nat (numeral v mod numeral v')"

  2774   by (simp add: nat_mod_distrib)

  2775

  2776 lemma one_mod_nat_numeral [simp]:

  2777   "Suc 0 mod numeral v' = nat (1 mod numeral v')"

  2778   by (subst nat_mod_distrib) simp_all

  2779

  2780

  2781 subsubsection {* Tools setup *}

  2782

  2783 text {* Nitpick *}

  2784

  2785 lemmas [nitpick_unfold] = dvd_eq_mod_eq_0 mod_div_equality' zmod_zdiv_equality'

  2786

  2787

  2788 subsubsection {* Code generation *}

  2789

  2790 definition divmod_abs :: "int \<Rightarrow> int \<Rightarrow> int \<times> int"

  2791 where

  2792   "divmod_abs k l = (\<bar>k\<bar> div \<bar>l\<bar>, \<bar>k\<bar> mod \<bar>l\<bar>)"

  2793

  2794 lemma fst_divmod_abs [simp]:

  2795   "fst (divmod_abs k l) = \<bar>k\<bar> div \<bar>l\<bar>"

  2796   by (simp add: divmod_abs_def)

  2797

  2798 lemma snd_divmod_abs [simp]:

  2799   "snd (divmod_abs k l) = \<bar>k\<bar> mod \<bar>l\<bar>"

  2800   by (simp add: divmod_abs_def)

  2801

  2802 lemma divmod_abs_code [code]:

  2803   "divmod_abs (Int.Pos k) (Int.Pos l) = divmod k l"

  2804   "divmod_abs (Int.Neg k) (Int.Neg l) = divmod k l"

  2805   "divmod_abs (Int.Neg k) (Int.Pos l) = divmod k l"

  2806   "divmod_abs (Int.Pos k) (Int.Neg l) = divmod k l"

  2807   "divmod_abs j 0 = (0, \<bar>j\<bar>)"

  2808   "divmod_abs 0 j = (0, 0)"

  2809   by (simp_all add: prod_eq_iff)

  2810

  2811 lemma divmod_int_divmod_abs:

  2812   "divmod_int k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else

  2813   apsnd ((op *) (sgn l)) (if 0 < l \<and> 0 \<le> k \<or> l < 0 \<and> k < 0

  2814     then divmod_abs k l

  2815     else (let (r, s) = divmod_abs k l in

  2816        if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"

  2817 proof -

  2818   have aux: "\<And>q::int. - k = l * q \<longleftrightarrow> k = l * - q" by auto

  2819   show ?thesis

  2820     by (simp add: prod_eq_iff split_def Let_def)

  2821       (auto simp add: aux not_less not_le zdiv_zminus1_eq_if

  2822       zmod_zminus1_eq_if zdiv_zminus2_eq_if zmod_zminus2_eq_if)

  2823 qed

  2824

  2825 lemma divmod_int_code [code]:

  2826   "divmod_int k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else

  2827   apsnd ((op *) (sgn l)) (if sgn k = sgn l

  2828     then divmod_abs k l

  2829     else (let (r, s) = divmod_abs k l in

  2830       if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"

  2831 proof -

  2832   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"

  2833     by (auto simp add: not_less sgn_if)

  2834   then show ?thesis by (simp add: divmod_int_divmod_abs)

  2835 qed

  2836

  2837 hide_const (open) divmod_abs

  2838

  2839 code_identifier

  2840   code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith

  2841

  2842 end
`