src/HOL/Divides.thy
author haftmann
Sun Oct 08 22:28:21 2017 +0200 (20 months ago)
changeset 66808 1907167b6038
parent 66806 a4e82b58d833
child 66810 cc2b490f9dc4
permissions -rw-r--r--
elementary definition of division on natural numbers
     1 (*  Title:      HOL/Divides.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1999  University of Cambridge
     4 *)
     5 
     6 section \<open>More on quotient and remainder\<close>
     7 
     8 theory Divides
     9 imports Parity
    10 begin
    11 
    12 subsection \<open>Numeral division with a pragmatic type class\<close>
    13 
    14 text \<open>
    15   The following type class contains everything necessary to formulate
    16   a division algorithm in ring structures with numerals, restricted
    17   to its positive segments.  This is its primary motivation, and it
    18   could surely be formulated using a more fine-grained, more algebraic
    19   and less technical class hierarchy.
    20 \<close>
    21 
    22 class unique_euclidean_semiring_numeral = unique_euclidean_semiring + linordered_semidom +
    23   assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
    24     and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
    25     and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
    26     and mod_less_eq_dividend: "0 \<le> a \<Longrightarrow> a mod b \<le> a"
    27     and pos_mod_bound: "0 < b \<Longrightarrow> a mod b < b"
    28     and pos_mod_sign: "0 < b \<Longrightarrow> 0 \<le> a mod b"
    29     and mod_mult2_eq: "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
    30     and div_mult2_eq: "0 \<le> c \<Longrightarrow> a div (b * c) = a div b div c"
    31   assumes discrete: "a < b \<longleftrightarrow> a + 1 \<le> b"
    32   fixes divmod :: "num \<Rightarrow> num \<Rightarrow> 'a \<times> 'a"
    33     and divmod_step :: "num \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a"
    34   assumes divmod_def: "divmod m n = (numeral m div numeral n, numeral m mod numeral n)"
    35     and divmod_step_def: "divmod_step l qr = (let (q, r) = qr
    36     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
    37     else (2 * q, r))"
    38     \<comment> \<open>These are conceptually definitions but force generated code
    39     to be monomorphic wrt. particular instances of this class which
    40     yields a significant speedup.\<close>
    41 begin
    42 
    43 subclass unique_euclidean_semiring_parity
    44 proof
    45   fix a
    46   show "a mod 2 = 0 \<or> a mod 2 = 1"
    47   proof (rule ccontr)
    48     assume "\<not> (a mod 2 = 0 \<or> a mod 2 = 1)"
    49     then have "a mod 2 \<noteq> 0" and "a mod 2 \<noteq> 1" by simp_all
    50     have "0 < 2" by simp
    51     with pos_mod_bound pos_mod_sign have "0 \<le> a mod 2" "a mod 2 < 2" by simp_all
    52     with \<open>a mod 2 \<noteq> 0\<close> have "0 < a mod 2" by simp
    53     with discrete have "1 \<le> a mod 2" by simp
    54     with \<open>a mod 2 \<noteq> 1\<close> have "1 < a mod 2" by simp
    55     with discrete have "2 \<le> a mod 2" by simp
    56     with \<open>a mod 2 < 2\<close> show False by simp
    57   qed
    58 next
    59   show "1 mod 2 = 1"
    60     by (rule mod_less) simp_all
    61 next
    62   show "0 \<noteq> 2"
    63     by simp
    64 qed
    65 
    66 lemma divmod_digit_1:
    67   assumes "0 \<le> a" "0 < b" and "b \<le> a mod (2 * b)"
    68   shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P")
    69     and "a mod (2 * b) - b = a mod b" (is "?Q")
    70 proof -
    71   from assms mod_less_eq_dividend [of a "2 * b"] have "b \<le> a"
    72     by (auto intro: trans)
    73   with \<open>0 < b\<close> have "0 < a div b" by (auto intro: div_positive)
    74   then have [simp]: "1 \<le> a div b" by (simp add: discrete)
    75   with \<open>0 < b\<close> have mod_less: "a mod b < b" by (simp add: pos_mod_bound)
    76   define w where "w = a div b mod 2"
    77   with parity have w_exhaust: "w = 0 \<or> w = 1" by auto
    78   have mod_w: "a mod (2 * b) = a mod b + b * w"
    79     by (simp add: w_def mod_mult2_eq ac_simps)
    80   from assms w_exhaust have "w = 1"
    81     by (auto simp add: mod_w) (insert mod_less, auto)
    82   with mod_w have mod: "a mod (2 * b) = a mod b + b" by simp
    83   have "2 * (a div (2 * b)) = a div b - w"
    84     by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
    85   with \<open>w = 1\<close> have div: "2 * (a div (2 * b)) = a div b - 1" by simp
    86   then show ?P and ?Q
    87     by (simp_all add: div mod add_implies_diff [symmetric])
    88 qed
    89 
    90 lemma divmod_digit_0:
    91   assumes "0 < b" and "a mod (2 * b) < b"
    92   shows "2 * (a div (2 * b)) = a div b" (is "?P")
    93     and "a mod (2 * b) = a mod b" (is "?Q")
    94 proof -
    95   define w where "w = a div b mod 2"
    96   with parity have w_exhaust: "w = 0 \<or> w = 1" by auto
    97   have mod_w: "a mod (2 * b) = a mod b + b * w"
    98     by (simp add: w_def mod_mult2_eq ac_simps)
    99   moreover have "b \<le> a mod b + b"
   100   proof -
   101     from \<open>0 < b\<close> pos_mod_sign have "0 \<le> a mod b" by blast
   102     then have "0 + b \<le> a mod b + b" by (rule add_right_mono)
   103     then show ?thesis by simp
   104   qed
   105   moreover note assms w_exhaust
   106   ultimately have "w = 0" by auto
   107   with mod_w have mod: "a mod (2 * b) = a mod b" by simp
   108   have "2 * (a div (2 * b)) = a div b - w"
   109     by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
   110   with \<open>w = 0\<close> have div: "2 * (a div (2 * b)) = a div b" by simp
   111   then show ?P and ?Q
   112     by (simp_all add: div mod)
   113 qed
   114 
   115 lemma fst_divmod:
   116   "fst (divmod m n) = numeral m div numeral n"
   117   by (simp add: divmod_def)
   118 
   119 lemma snd_divmod:
   120   "snd (divmod m n) = numeral m mod numeral n"
   121   by (simp add: divmod_def)
   122 
   123 text \<open>
   124   This is a formulation of one step (referring to one digit position)
   125   in school-method division: compare the dividend at the current
   126   digit position with the remainder from previous division steps
   127   and evaluate accordingly.
   128 \<close>
   129 
   130 lemma divmod_step_eq [simp]:
   131   "divmod_step l (q, r) = (if numeral l \<le> r
   132     then (2 * q + 1, r - numeral l) else (2 * q, r))"
   133   by (simp add: divmod_step_def)
   134 
   135 text \<open>
   136   This is a formulation of school-method division.
   137   If the divisor is smaller than the dividend, terminate.
   138   If not, shift the dividend to the right until termination
   139   occurs and then reiterate single division steps in the
   140   opposite direction.
   141 \<close>
   142 
   143 lemma divmod_divmod_step:
   144   "divmod m n = (if m < n then (0, numeral m)
   145     else divmod_step n (divmod m (Num.Bit0 n)))"
   146 proof (cases "m < n")
   147   case True then have "numeral m < numeral n" by simp
   148   then show ?thesis
   149     by (simp add: prod_eq_iff div_less mod_less fst_divmod snd_divmod)
   150 next
   151   case False
   152   have "divmod m n =
   153     divmod_step n (numeral m div (2 * numeral n),
   154       numeral m mod (2 * numeral n))"
   155   proof (cases "numeral n \<le> numeral m mod (2 * numeral n)")
   156     case True
   157     with divmod_step_eq
   158       have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
   159         (2 * (numeral m div (2 * numeral n)) + 1, numeral m mod (2 * numeral n) - numeral n)"
   160         by simp
   161     moreover from True divmod_digit_1 [of "numeral m" "numeral n"]
   162       have "2 * (numeral m div (2 * numeral n)) + 1 = numeral m div numeral n"
   163       and "numeral m mod (2 * numeral n) - numeral n = numeral m mod numeral n"
   164       by simp_all
   165     ultimately show ?thesis by (simp only: divmod_def)
   166   next
   167     case False then have *: "numeral m mod (2 * numeral n) < numeral n"
   168       by (simp add: not_le)
   169     with divmod_step_eq
   170       have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
   171         (2 * (numeral m div (2 * numeral n)), numeral m mod (2 * numeral n))"
   172         by auto
   173     moreover from * divmod_digit_0 [of "numeral n" "numeral m"]
   174       have "2 * (numeral m div (2 * numeral n)) = numeral m div numeral n"
   175       and "numeral m mod (2 * numeral n) = numeral m mod numeral n"
   176       by (simp_all only: zero_less_numeral)
   177     ultimately show ?thesis by (simp only: divmod_def)
   178   qed
   179   then have "divmod m n =
   180     divmod_step n (numeral m div numeral (Num.Bit0 n),
   181       numeral m mod numeral (Num.Bit0 n))"
   182     by (simp only: numeral.simps distrib mult_1)
   183   then have "divmod m n = divmod_step n (divmod m (Num.Bit0 n))"
   184     by (simp add: divmod_def)
   185   with False show ?thesis by simp
   186 qed
   187 
   188 text \<open>The division rewrite proper -- first, trivial results involving \<open>1\<close>\<close>
   189 
   190 lemma divmod_trivial [simp]:
   191   "divmod Num.One Num.One = (numeral Num.One, 0)"
   192   "divmod (Num.Bit0 m) Num.One = (numeral (Num.Bit0 m), 0)"
   193   "divmod (Num.Bit1 m) Num.One = (numeral (Num.Bit1 m), 0)"
   194   "divmod num.One (num.Bit0 n) = (0, Numeral1)"
   195   "divmod num.One (num.Bit1 n) = (0, Numeral1)"
   196   using divmod_divmod_step [of "Num.One"] by (simp_all add: divmod_def)
   197 
   198 text \<open>Division by an even number is a right-shift\<close>
   199 
   200 lemma divmod_cancel [simp]:
   201   "divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))" (is ?P)
   202   "divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r + 1))" (is ?Q)
   203 proof -
   204   have *: "\<And>q. numeral (Num.Bit0 q) = 2 * numeral q"
   205     "\<And>q. numeral (Num.Bit1 q) = 2 * numeral q + 1"
   206     by (simp_all only: numeral_mult numeral.simps distrib) simp_all
   207   have "1 div 2 = 0" "1 mod 2 = 1" by (auto intro: div_less mod_less)
   208   then show ?P and ?Q
   209     by (simp_all add: fst_divmod snd_divmod prod_eq_iff split_def * [of m] * [of n] mod_mult_mult1
   210       div_mult2_eq [of _ _ 2] mod_mult2_eq [of _ _ 2]
   211       add.commute del: numeral_times_numeral)
   212 qed
   213 
   214 text \<open>The really hard work\<close>
   215 
   216 lemma divmod_steps [simp]:
   217   "divmod (num.Bit0 m) (num.Bit1 n) =
   218       (if m \<le> n then (0, numeral (num.Bit0 m))
   219        else divmod_step (num.Bit1 n)
   220              (divmod (num.Bit0 m)
   221                (num.Bit0 (num.Bit1 n))))"
   222   "divmod (num.Bit1 m) (num.Bit1 n) =
   223       (if m < n then (0, numeral (num.Bit1 m))
   224        else divmod_step (num.Bit1 n)
   225              (divmod (num.Bit1 m)
   226                (num.Bit0 (num.Bit1 n))))"
   227   by (simp_all add: divmod_divmod_step)
   228 
   229 lemmas divmod_algorithm_code = divmod_step_eq divmod_trivial divmod_cancel divmod_steps  
   230 
   231 text \<open>Special case: divisibility\<close>
   232 
   233 definition divides_aux :: "'a \<times> 'a \<Rightarrow> bool"
   234 where
   235   "divides_aux qr \<longleftrightarrow> snd qr = 0"
   236 
   237 lemma divides_aux_eq [simp]:
   238   "divides_aux (q, r) \<longleftrightarrow> r = 0"
   239   by (simp add: divides_aux_def)
   240 
   241 lemma dvd_numeral_simp [simp]:
   242   "numeral m dvd numeral n \<longleftrightarrow> divides_aux (divmod n m)"
   243   by (simp add: divmod_def mod_eq_0_iff_dvd)
   244 
   245 text \<open>Generic computation of quotient and remainder\<close>  
   246 
   247 lemma numeral_div_numeral [simp]: 
   248   "numeral k div numeral l = fst (divmod k l)"
   249   by (simp add: fst_divmod)
   250 
   251 lemma numeral_mod_numeral [simp]: 
   252   "numeral k mod numeral l = snd (divmod k l)"
   253   by (simp add: snd_divmod)
   254 
   255 lemma one_div_numeral [simp]:
   256   "1 div numeral n = fst (divmod num.One n)"
   257   by (simp add: fst_divmod)
   258 
   259 lemma one_mod_numeral [simp]:
   260   "1 mod numeral n = snd (divmod num.One n)"
   261   by (simp add: snd_divmod)
   262 
   263 text \<open>Computing congruences modulo \<open>2 ^ q\<close>\<close>
   264 
   265 lemma cong_exp_iff_simps:
   266   "numeral n mod numeral Num.One = 0
   267     \<longleftrightarrow> True"
   268   "numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) = 0
   269     \<longleftrightarrow> numeral n mod numeral q = 0"
   270   "numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) = 0
   271     \<longleftrightarrow> False"
   272   "numeral m mod numeral Num.One = (numeral n mod numeral Num.One)
   273     \<longleftrightarrow> True"
   274   "numeral Num.One mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
   275     \<longleftrightarrow> True"
   276   "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
   277     \<longleftrightarrow> False"
   278   "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
   279     \<longleftrightarrow> (numeral n mod numeral q) = 0"
   280   "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
   281     \<longleftrightarrow> False"
   282   "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
   283     \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
   284   "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
   285     \<longleftrightarrow> False"
   286   "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
   287     \<longleftrightarrow> (numeral m mod numeral q) = 0"
   288   "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
   289     \<longleftrightarrow> False"
   290   "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
   291     \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
   292   by (auto simp add: case_prod_beta dest: arg_cong [of _ _ even])
   293 
   294 end
   295 
   296 hide_fact (open) div_less mod_less mod_less_eq_dividend mod_mult2_eq div_mult2_eq
   297 
   298 
   299 subsection \<open>Division on @{typ nat}\<close>
   300 
   301 instantiation nat :: unique_euclidean_semiring_numeral
   302 begin
   303 
   304 definition divmod_nat :: "num \<Rightarrow> num \<Rightarrow> nat \<times> nat"
   305 where
   306   divmod'_nat_def: "divmod_nat m n = (numeral m div numeral n, numeral m mod numeral n)"
   307 
   308 definition divmod_step_nat :: "num \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
   309 where
   310   "divmod_step_nat l qr = (let (q, r) = qr
   311     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
   312     else (2 * q, r))"
   313 
   314 instance by standard
   315   (auto simp add: divmod'_nat_def divmod_step_nat_def div_greater_zero_iff div_mult2_eq mod_mult2_eq)
   316 
   317 end
   318 
   319 declare divmod_algorithm_code [where ?'a = nat, code]
   320 
   321 lemma odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
   322   by (auto elim: oddE)
   323 
   324 lemma even_Suc_div_two [simp]:
   325   "even n \<Longrightarrow> Suc n div 2 = n div 2"
   326   using even_succ_div_two [of n] by simp
   327 
   328 lemma odd_Suc_div_two [simp]:
   329   "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
   330   using odd_succ_div_two [of n] by simp
   331 
   332 lemma odd_two_times_div_two_nat [simp]:
   333   assumes "odd n"
   334   shows "2 * (n div 2) = n - (1 :: nat)"
   335 proof -
   336   from assms have "2 * (n div 2) + 1 = n"
   337     by (rule odd_two_times_div_two_succ)
   338   then have "Suc (2 * (n div 2)) - 1 = n - 1"
   339     by simp
   340   then show ?thesis
   341     by simp
   342 qed
   343 
   344 lemma parity_induct [case_names zero even odd]:
   345   assumes zero: "P 0"
   346   assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
   347   assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
   348   shows "P n"
   349 proof (induct n rule: less_induct)
   350   case (less n)
   351   show "P n"
   352   proof (cases "n = 0")
   353     case True with zero show ?thesis by simp
   354   next
   355     case False
   356     with less have hyp: "P (n div 2)" by simp
   357     show ?thesis
   358     proof (cases "even n")
   359       case True
   360       with hyp even [of "n div 2"] show ?thesis
   361         by simp
   362     next
   363       case False
   364       with hyp odd [of "n div 2"] show ?thesis
   365         by simp
   366     qed
   367   qed
   368 qed
   369 
   370 lemma mod_2_not_eq_zero_eq_one_nat:
   371   fixes n :: nat
   372   shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
   373   by (fact not_mod_2_eq_0_eq_1)
   374 
   375 lemma Suc_0_div_numeral [simp]:
   376   fixes k l :: num
   377   shows "Suc 0 div numeral k = fst (divmod Num.One k)"
   378   by (simp_all add: fst_divmod)
   379 
   380 lemma Suc_0_mod_numeral [simp]:
   381   fixes k l :: num
   382   shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
   383   by (simp_all add: snd_divmod)
   384 
   385 definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat"
   386   where "divmod_nat m n = (m div n, m mod n)"
   387 
   388 lemma fst_divmod_nat [simp]:
   389   "fst (divmod_nat m n) = m div n"
   390   by (simp add: divmod_nat_def)
   391 
   392 lemma snd_divmod_nat [simp]:
   393   "snd (divmod_nat m n) = m mod n"
   394   by (simp add: divmod_nat_def)
   395 
   396 lemma divmod_nat_if [code]:
   397   "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
   398     let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
   399   by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
   400 
   401 lemma [code]:
   402   "m div n = fst (divmod_nat m n)"
   403   "m mod n = snd (divmod_nat m n)"
   404   by simp_all
   405 
   406 
   407 subsection \<open>Division on @{typ int}\<close>
   408 
   409 context
   410 begin
   411 
   412 inductive eucl_rel_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool"
   413   where eucl_rel_int_by0: "eucl_rel_int k 0 (0, k)"
   414   | eucl_rel_int_dividesI: "l \<noteq> 0 \<Longrightarrow> k = q * l \<Longrightarrow> eucl_rel_int k l (q, 0)"
   415   | eucl_rel_int_remainderI: "sgn r = sgn l \<Longrightarrow> \<bar>r\<bar> < \<bar>l\<bar>
   416       \<Longrightarrow> k = q * l + r \<Longrightarrow> eucl_rel_int k l (q, r)"
   417 
   418 lemma eucl_rel_int_iff:    
   419   "eucl_rel_int k l (q, r) \<longleftrightarrow> 
   420     k = l * q + r \<and>
   421      (if 0 < l then 0 \<le> r \<and> r < l else if l < 0 then l < r \<and> r \<le> 0 else q = 0)"
   422   by (cases "r = 0")
   423     (auto elim!: eucl_rel_int.cases intro: eucl_rel_int_by0 eucl_rel_int_dividesI eucl_rel_int_remainderI
   424     simp add: ac_simps sgn_1_pos sgn_1_neg)
   425 
   426 lemma unique_quotient_lemma:
   427   "b * q' + r' \<le> b * q + r \<Longrightarrow> 0 \<le> r' \<Longrightarrow> r' < b \<Longrightarrow> r < b \<Longrightarrow> q' \<le> (q::int)"
   428 apply (subgoal_tac "r' + b * (q'-q) \<le> r")
   429  prefer 2 apply (simp add: right_diff_distrib)
   430 apply (subgoal_tac "0 < b * (1 + q - q') ")
   431 apply (erule_tac [2] order_le_less_trans)
   432  prefer 2 apply (simp add: right_diff_distrib distrib_left)
   433 apply (subgoal_tac "b * q' < b * (1 + q) ")
   434  prefer 2 apply (simp add: right_diff_distrib distrib_left)
   435 apply (simp add: mult_less_cancel_left)
   436 done
   437 
   438 lemma unique_quotient_lemma_neg:
   439   "b * q' + r' \<le> b*q + r \<Longrightarrow> r \<le> 0 \<Longrightarrow> b < r \<Longrightarrow> b < r' \<Longrightarrow> q \<le> (q'::int)"
   440   by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma) auto
   441 
   442 lemma unique_quotient:
   443   "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> q = q'"
   444   apply (simp add: eucl_rel_int_iff linorder_neq_iff split: if_split_asm)
   445   apply (blast intro: order_antisym
   446     dest: order_eq_refl [THEN unique_quotient_lemma]
   447     order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
   448   done
   449 
   450 lemma unique_remainder:
   451   "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> r = r'"
   452 apply (subgoal_tac "q = q'")
   453  apply (simp add: eucl_rel_int_iff)
   454 apply (blast intro: unique_quotient)
   455 done
   456 
   457 end
   458 
   459 instantiation int :: "{idom_modulo, normalization_semidom}"
   460 begin
   461 
   462 definition normalize_int :: "int \<Rightarrow> int"
   463   where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
   464 
   465 definition unit_factor_int :: "int \<Rightarrow> int"
   466   where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
   467 
   468 definition divide_int :: "int \<Rightarrow> int \<Rightarrow> int"
   469   where "k div l = (if l = 0 \<or> k = 0 then 0
   470     else if k > 0 \<and> l > 0 \<or> k < 0 \<and> l < 0
   471       then int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
   472       else
   473         if l dvd k then - int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
   474         else - int (Suc (nat \<bar>k\<bar> div nat \<bar>l\<bar>)))"
   475 
   476 definition modulo_int :: "int \<Rightarrow> int \<Rightarrow> int"
   477   where "k mod l = (if l = 0 then k else if l dvd k then 0
   478     else if k > 0 \<and> l > 0 \<or> k < 0 \<and> l < 0
   479       then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)
   480       else sgn l * (\<bar>l\<bar> - int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)))"
   481 
   482 lemma eucl_rel_int:
   483   "eucl_rel_int k l (k div l, k mod l)"
   484 proof (cases k rule: int_cases3)
   485   case zero
   486   then show ?thesis
   487     by (simp add: eucl_rel_int_iff divide_int_def modulo_int_def)
   488 next
   489   case (pos n)
   490   then show ?thesis
   491     using div_mult_mod_eq [of n]
   492     by (cases l rule: int_cases3)
   493       (auto simp del: of_nat_mult of_nat_add
   494         simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
   495         eucl_rel_int_iff divide_int_def modulo_int_def int_dvd_iff)
   496 next
   497   case (neg n)
   498   then show ?thesis
   499     using div_mult_mod_eq [of n]
   500     by (cases l rule: int_cases3)
   501       (auto simp del: of_nat_mult of_nat_add
   502         simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
   503         eucl_rel_int_iff divide_int_def modulo_int_def int_dvd_iff)
   504 qed
   505 
   506 lemma divmod_int_unique:
   507   assumes "eucl_rel_int k l (q, r)"
   508   shows div_int_unique: "k div l = q" and mod_int_unique: "k mod l = r"
   509   using assms eucl_rel_int [of k l]
   510   using unique_quotient [of k l] unique_remainder [of k l]
   511   by auto
   512 
   513 instance proof
   514   fix k l :: int
   515   show "k div l * l + k mod l = k"
   516     using eucl_rel_int [of k l]
   517     unfolding eucl_rel_int_iff by (simp add: ac_simps)
   518 next
   519   fix k :: int show "k div 0 = 0"
   520     by (rule div_int_unique, simp add: eucl_rel_int_iff)
   521 next
   522   fix k l :: int
   523   assume "l \<noteq> 0"
   524   then show "k * l div l = k"
   525     by (auto simp add: eucl_rel_int_iff ac_simps intro: div_int_unique [of _ _ _ 0])
   526 qed (auto simp add: sgn_mult mult_sgn_abs abs_eq_iff')
   527 
   528 end
   529 
   530 ML \<open>
   531 structure Cancel_Div_Mod_Int = Cancel_Div_Mod
   532 (
   533   val div_name = @{const_name divide};
   534   val mod_name = @{const_name modulo};
   535   val mk_binop = HOLogic.mk_binop;
   536   val mk_sum = Arith_Data.mk_sum HOLogic.intT;
   537   val dest_sum = Arith_Data.dest_sum;
   538 
   539   val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
   540 
   541   val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
   542     @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
   543 )
   544 \<close>
   545 
   546 simproc_setup cancel_div_mod_int ("(k::int) + l") =
   547   \<open>K Cancel_Div_Mod_Int.proc\<close>
   548 
   549 lemma is_unit_int:
   550   "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
   551   by auto
   552 
   553 lemma zdiv_int:
   554   "int (a div b) = int a div int b"
   555   by (simp add: divide_int_def)
   556 
   557 lemma zmod_int:
   558   "int (a mod b) = int a mod int b"
   559   by (simp add: modulo_int_def int_dvd_iff)
   560 
   561 lemma div_abs_eq_div_nat:
   562   "\<bar>k\<bar> div \<bar>l\<bar> = int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)"
   563   by (simp add: divide_int_def)
   564 
   565 lemma mod_abs_eq_div_nat:
   566   "\<bar>k\<bar> mod \<bar>l\<bar> = int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)"
   567   by (simp add: modulo_int_def dvd_int_unfold_dvd_nat)
   568 
   569 lemma div_sgn_abs_cancel:
   570   fixes k l v :: int
   571   assumes "v \<noteq> 0"
   572   shows "(sgn v * \<bar>k\<bar>) div (sgn v * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
   573 proof -
   574   from assms have "sgn v = - 1 \<or> sgn v = 1"
   575     by (cases "v \<ge> 0") auto
   576   then show ?thesis
   577     using assms unfolding divide_int_def [of "sgn v * \<bar>k\<bar>" "sgn v * \<bar>l\<bar>"]
   578     by (fastforce simp add: not_less div_abs_eq_div_nat)
   579 qed
   580 
   581 lemma div_eq_sgn_abs:
   582   fixes k l v :: int
   583   assumes "sgn k = sgn l"
   584   shows "k div l = \<bar>k\<bar> div \<bar>l\<bar>"
   585 proof (cases "l = 0")
   586   case True
   587   then show ?thesis
   588     by simp
   589 next
   590   case False
   591   with assms have "(sgn k * \<bar>k\<bar>) div (sgn l * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
   592     by (simp add: div_sgn_abs_cancel)
   593   then show ?thesis
   594     by (simp add: sgn_mult_abs)
   595 qed
   596 
   597 lemma div_dvd_sgn_abs:
   598   fixes k l :: int
   599   assumes "l dvd k"
   600   shows "k div l = (sgn k * sgn l) * (\<bar>k\<bar> div \<bar>l\<bar>)"
   601 proof (cases "k = 0")
   602   case True
   603   then show ?thesis
   604     by simp
   605 next
   606   case False
   607   show ?thesis
   608   proof (cases "sgn l = sgn k")
   609     case True
   610     then show ?thesis
   611       by (simp add: div_eq_sgn_abs)
   612   next
   613     case False
   614     with \<open>k \<noteq> 0\<close> assms show ?thesis
   615       unfolding divide_int_def [of k l]
   616         by (auto simp add: zdiv_int)
   617   qed
   618 qed
   619 
   620 lemma div_noneq_sgn_abs:
   621   fixes k l :: int
   622   assumes "l \<noteq> 0"
   623   assumes "sgn k \<noteq> sgn l"
   624   shows "k div l = - (\<bar>k\<bar> div \<bar>l\<bar>) - of_bool (\<not> l dvd k)"
   625   using assms
   626   by (simp only: divide_int_def [of k l], auto simp add: not_less zdiv_int)
   627   
   628 lemma sgn_mod:
   629   fixes k l :: int
   630   assumes "l \<noteq> 0" "\<not> l dvd k"
   631   shows "sgn (k mod l) = sgn l"
   632 proof -
   633   from \<open>\<not> l dvd k\<close>
   634   have "k mod l \<noteq> 0"
   635     by (simp add: dvd_eq_mod_eq_0)
   636   show ?thesis
   637     using \<open>l \<noteq> 0\<close> \<open>\<not> l dvd k\<close>
   638     unfolding modulo_int_def [of k l]
   639     by (auto simp add: sgn_1_pos sgn_1_neg mod_greater_zero_iff_not_dvd nat_dvd_iff not_less
   640       zless_nat_eq_int_zless [symmetric] elim: nonpos_int_cases)
   641 qed
   642 
   643 lemma abs_mod_less:
   644   fixes k l :: int
   645   assumes "l \<noteq> 0"
   646   shows "\<bar>k mod l\<bar> < \<bar>l\<bar>"
   647   using assms unfolding modulo_int_def [of k l]
   648   by (auto simp add: not_less int_dvd_iff mod_greater_zero_iff_not_dvd elim: pos_int_cases neg_int_cases nonneg_int_cases nonpos_int_cases)
   649 
   650 instantiation int :: unique_euclidean_ring
   651 begin
   652 
   653 definition [simp]:
   654   "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
   655 
   656 definition [simp]:
   657   "uniqueness_constraint_int (k :: int) l \<longleftrightarrow> unit_factor k = unit_factor l"
   658   
   659 instance proof
   660   fix l q r:: int
   661   assume "uniqueness_constraint r l"
   662     and "euclidean_size r < euclidean_size l"
   663   then have "sgn r = sgn l" and "\<bar>r\<bar> < \<bar>l\<bar>"
   664     by simp_all
   665   then have "eucl_rel_int (q * l + r) l (q, r)"
   666     by (rule eucl_rel_int_remainderI) simp
   667   then show "(q * l + r) div l = q"
   668     by (rule div_int_unique)
   669 qed (use mult_le_mono2 [of 1] in \<open>auto simp add: abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>)
   670 
   671 end
   672 
   673 text\<open>Basic laws about division and remainder\<close>
   674 
   675 lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
   676   using eucl_rel_int [of a b]
   677   by (auto simp add: eucl_rel_int_iff prod_eq_iff)
   678 
   679 lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1]
   680    and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2]
   681 
   682 lemma neg_mod_conj: "b < (0::int) \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b"
   683   using eucl_rel_int [of a b]
   684   by (auto simp add: eucl_rel_int_iff prod_eq_iff)
   685 
   686 lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1]
   687    and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2]
   688 
   689 
   690 subsubsection \<open>General Properties of div and mod\<close>
   691 
   692 lemma div_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a div b = 0"
   693 apply (rule div_int_unique)
   694 apply (auto simp add: eucl_rel_int_iff)
   695 done
   696 
   697 lemma div_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a div b = 0"
   698 apply (rule div_int_unique)
   699 apply (auto simp add: eucl_rel_int_iff)
   700 done
   701 
   702 lemma div_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a div b = -1"
   703 apply (rule div_int_unique)
   704 apply (auto simp add: eucl_rel_int_iff)
   705 done
   706 
   707 lemma div_positive_int:
   708   "k div l > 0" if "k \<ge> l" and "l > 0" for k l :: int
   709   using that by (simp add: divide_int_def div_positive)
   710 
   711 (*There is no div_neg_pos_trivial because  0 div b = 0 would supersede it*)
   712 
   713 lemma mod_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a mod b = a"
   714 apply (rule_tac q = 0 in mod_int_unique)
   715 apply (auto simp add: eucl_rel_int_iff)
   716 done
   717 
   718 lemma mod_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a mod b = a"
   719 apply (rule_tac q = 0 in mod_int_unique)
   720 apply (auto simp add: eucl_rel_int_iff)
   721 done
   722 
   723 lemma mod_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a mod b = a+b"
   724 apply (rule_tac q = "-1" in mod_int_unique)
   725 apply (auto simp add: eucl_rel_int_iff)
   726 done
   727 
   728 text\<open>There is no \<open>mod_neg_pos_trivial\<close>.\<close>
   729 
   730 
   731 subsubsection \<open>Laws for div and mod with Unary Minus\<close>
   732 
   733 lemma zminus1_lemma:
   734      "eucl_rel_int a b (q, r) ==> b \<noteq> 0
   735       ==> eucl_rel_int (-a) b (if r=0 then -q else -q - 1,
   736                           if r=0 then 0 else b-r)"
   737 by (force simp add: eucl_rel_int_iff right_diff_distrib)
   738 
   739 
   740 lemma zdiv_zminus1_eq_if:
   741      "b \<noteq> (0::int)
   742       ==> (-a) div b =
   743           (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
   744 by (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN div_int_unique])
   745 
   746 lemma zmod_zminus1_eq_if:
   747      "(-a::int) mod b = (if a mod b = 0 then 0 else  b - (a mod b))"
   748 apply (case_tac "b = 0", simp)
   749 apply (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN mod_int_unique])
   750 done
   751 
   752 lemma zmod_zminus1_not_zero:
   753   fixes k l :: int
   754   shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
   755   by (simp add: mod_eq_0_iff_dvd)
   756 
   757 lemma zmod_zminus2_not_zero:
   758   fixes k l :: int
   759   shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
   760   by (simp add: mod_eq_0_iff_dvd)
   761 
   762 lemma zdiv_zminus2_eq_if:
   763      "b \<noteq> (0::int)
   764       ==> a div (-b) =
   765           (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
   766 by (simp add: zdiv_zminus1_eq_if div_minus_right)
   767 
   768 lemma zmod_zminus2_eq_if:
   769      "a mod (-b::int) = (if a mod b = 0 then 0 else  (a mod b) - b)"
   770 by (simp add: zmod_zminus1_eq_if mod_minus_right)
   771 
   772 
   773 subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
   774 
   775 lemma zdiv_mono1: "[| a \<le> a';  0 < (b::int) |] ==> a div b \<le> a' div b"
   776 using mult_div_mod_eq [symmetric, of a b]
   777 using mult_div_mod_eq [symmetric, of a' b]
   778 apply -
   779 apply (rule unique_quotient_lemma)
   780 apply (erule subst)
   781 apply (erule subst, simp_all)
   782 done
   783 
   784 lemma zdiv_mono1_neg: "[| a \<le> a';  (b::int) < 0 |] ==> a' div b \<le> a div b"
   785 using mult_div_mod_eq [symmetric, of a b]
   786 using mult_div_mod_eq [symmetric, of a' b]
   787 apply -
   788 apply (rule unique_quotient_lemma_neg)
   789 apply (erule subst)
   790 apply (erule subst, simp_all)
   791 done
   792 
   793 
   794 subsubsection \<open>Monotonicity in the Second Argument (Divisor)\<close>
   795 
   796 lemma q_pos_lemma:
   797      "[| 0 \<le> b'*q' + r'; r' < b';  0 < b' |] ==> 0 \<le> (q'::int)"
   798 apply (subgoal_tac "0 < b'* (q' + 1) ")
   799  apply (simp add: zero_less_mult_iff)
   800 apply (simp add: distrib_left)
   801 done
   802 
   803 lemma zdiv_mono2_lemma:
   804      "[| b*q + r = b'*q' + r';  0 \<le> b'*q' + r';
   805          r' < b';  0 \<le> r;  0 < b';  b' \<le> b |]
   806       ==> q \<le> (q'::int)"
   807 apply (frule q_pos_lemma, assumption+)
   808 apply (subgoal_tac "b*q < b* (q' + 1) ")
   809  apply (simp add: mult_less_cancel_left)
   810 apply (subgoal_tac "b*q = r' - r + b'*q'")
   811  prefer 2 apply simp
   812 apply (simp (no_asm_simp) add: distrib_left)
   813 apply (subst add.commute, rule add_less_le_mono, arith)
   814 apply (rule mult_right_mono, auto)
   815 done
   816 
   817 lemma zdiv_mono2:
   818      "[| (0::int) \<le> a;  0 < b';  b' \<le> b |] ==> a div b \<le> a div b'"
   819 apply (subgoal_tac "b \<noteq> 0")
   820   prefer 2 apply arith
   821 using mult_div_mod_eq [symmetric, of a b]
   822 using mult_div_mod_eq [symmetric, of a b']
   823 apply -
   824 apply (rule zdiv_mono2_lemma)
   825 apply (erule subst)
   826 apply (erule subst, simp_all)
   827 done
   828 
   829 lemma q_neg_lemma:
   830      "[| b'*q' + r' < 0;  0 \<le> r';  0 < b' |] ==> q' \<le> (0::int)"
   831 apply (subgoal_tac "b'*q' < 0")
   832  apply (simp add: mult_less_0_iff, arith)
   833 done
   834 
   835 lemma zdiv_mono2_neg_lemma:
   836      "[| b*q + r = b'*q' + r';  b'*q' + r' < 0;
   837          r < b;  0 \<le> r';  0 < b';  b' \<le> b |]
   838       ==> q' \<le> (q::int)"
   839 apply (frule q_neg_lemma, assumption+)
   840 apply (subgoal_tac "b*q' < b* (q + 1) ")
   841  apply (simp add: mult_less_cancel_left)
   842 apply (simp add: distrib_left)
   843 apply (subgoal_tac "b*q' \<le> b'*q'")
   844  prefer 2 apply (simp add: mult_right_mono_neg, arith)
   845 done
   846 
   847 lemma zdiv_mono2_neg:
   848      "[| a < (0::int);  0 < b';  b' \<le> b |] ==> a div b' \<le> a div b"
   849 using mult_div_mod_eq [symmetric, of a b]
   850 using mult_div_mod_eq [symmetric, of a b']
   851 apply -
   852 apply (rule zdiv_mono2_neg_lemma)
   853 apply (erule subst)
   854 apply (erule subst, simp_all)
   855 done
   856 
   857 
   858 subsubsection \<open>More Algebraic Laws for div and mod\<close>
   859 
   860 text\<open>proving (a*b) div c = a * (b div c) + a * (b mod c)\<close>
   861 
   862 lemma zmult1_lemma:
   863      "[| eucl_rel_int b c (q, r) |]
   864       ==> eucl_rel_int (a * b) c (a*q + a*r div c, a*r mod c)"
   865 by (auto simp add: split_ifs eucl_rel_int_iff linorder_neq_iff distrib_left ac_simps)
   866 
   867 lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
   868 apply (case_tac "c = 0", simp)
   869 apply (blast intro: eucl_rel_int [THEN zmult1_lemma, THEN div_int_unique])
   870 done
   871 
   872 text\<open>proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c)\<close>
   873 
   874 lemma zadd1_lemma:
   875      "[| eucl_rel_int a c (aq, ar);  eucl_rel_int b c (bq, br) |]
   876       ==> eucl_rel_int (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
   877 by (force simp add: split_ifs eucl_rel_int_iff linorder_neq_iff distrib_left)
   878 
   879 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
   880 lemma zdiv_zadd1_eq:
   881      "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
   882 apply (case_tac "c = 0", simp)
   883 apply (blast intro: zadd1_lemma [OF eucl_rel_int eucl_rel_int] div_int_unique)
   884 done
   885 
   886 lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
   887 by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
   888 
   889 (* REVISIT: should this be generalized to all semiring_div types? *)
   890 lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
   891 
   892 
   893 subsubsection \<open>Proving  @{term "a div (b * c) = (a div b) div c"}\<close>
   894 
   895 (*The condition c>0 seems necessary.  Consider that 7 div ~6 = ~2 but
   896   7 div 2 div ~3 = 3 div ~3 = ~1.  The subcase (a div b) mod c = 0 seems
   897   to cause particular problems.*)
   898 
   899 text\<open>first, four lemmas to bound the remainder for the cases b<0 and b>0\<close>
   900 
   901 lemma zmult2_lemma_aux1: "[| (0::int) < c;  b < r;  r \<le> 0 |] ==> b * c < b * (q mod c) + r"
   902 apply (subgoal_tac "b * (c - q mod c) < r * 1")
   903  apply (simp add: algebra_simps)
   904 apply (rule order_le_less_trans)
   905  apply (erule_tac [2] mult_strict_right_mono)
   906  apply (rule mult_left_mono_neg)
   907   using add1_zle_eq[of "q mod c"]apply(simp add: algebra_simps)
   908  apply (simp)
   909 apply (simp)
   910 done
   911 
   912 lemma zmult2_lemma_aux2:
   913      "[| (0::int) < c;   b < r;  r \<le> 0 |] ==> b * (q mod c) + r \<le> 0"
   914 apply (subgoal_tac "b * (q mod c) \<le> 0")
   915  apply arith
   916 apply (simp add: mult_le_0_iff)
   917 done
   918 
   919 lemma zmult2_lemma_aux3: "[| (0::int) < c;  0 \<le> r;  r < b |] ==> 0 \<le> b * (q mod c) + r"
   920 apply (subgoal_tac "0 \<le> b * (q mod c) ")
   921 apply arith
   922 apply (simp add: zero_le_mult_iff)
   923 done
   924 
   925 lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 \<le> r; r < b |] ==> b * (q mod c) + r < b * c"
   926 apply (subgoal_tac "r * 1 < b * (c - q mod c) ")
   927  apply (simp add: right_diff_distrib)
   928 apply (rule order_less_le_trans)
   929  apply (erule mult_strict_right_mono)
   930  apply (rule_tac [2] mult_left_mono)
   931   apply simp
   932  using add1_zle_eq[of "q mod c"] apply (simp add: algebra_simps)
   933 apply simp
   934 done
   935 
   936 lemma zmult2_lemma: "[| eucl_rel_int a b (q, r); 0 < c |]
   937       ==> eucl_rel_int a (b * c) (q div c, b*(q mod c) + r)"
   938 by (auto simp add: mult.assoc eucl_rel_int_iff linorder_neq_iff
   939                    zero_less_mult_iff distrib_left [symmetric]
   940                    zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: if_split_asm)
   941 
   942 lemma zdiv_zmult2_eq:
   943   fixes a b c :: int
   944   shows "0 \<le> c \<Longrightarrow> a div (b * c) = (a div b) div c"
   945 apply (case_tac "b = 0", simp)
   946 apply (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN div_int_unique])
   947 done
   948 
   949 lemma zmod_zmult2_eq:
   950   fixes a b c :: int
   951   shows "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
   952 apply (case_tac "b = 0", simp)
   953 apply (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN mod_int_unique])
   954 done
   955 
   956 lemma div_pos_geq:
   957   fixes k l :: int
   958   assumes "0 < l" and "l \<le> k"
   959   shows "k div l = (k - l) div l + 1"
   960 proof -
   961   have "k = (k - l) + l" by simp
   962   then obtain j where k: "k = j + l" ..
   963   with assms show ?thesis by (simp add: div_add_self2)
   964 qed
   965 
   966 lemma mod_pos_geq:
   967   fixes k l :: int
   968   assumes "0 < l" and "l \<le> k"
   969   shows "k mod l = (k - l) mod l"
   970 proof -
   971   have "k = (k - l) + l" by simp
   972   then obtain j where k: "k = j + l" ..
   973   with assms show ?thesis by simp
   974 qed
   975 
   976 
   977 subsubsection \<open>Splitting Rules for div and mod\<close>
   978 
   979 text\<open>The proofs of the two lemmas below are essentially identical\<close>
   980 
   981 lemma split_pos_lemma:
   982  "0<k ==>
   983     P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"
   984 apply (rule iffI, clarify)
   985  apply (erule_tac P="P x y" for x y in rev_mp)
   986  apply (subst mod_add_eq [symmetric])
   987  apply (subst zdiv_zadd1_eq)
   988  apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)
   989 txt\<open>converse direction\<close>
   990 apply (drule_tac x = "n div k" in spec)
   991 apply (drule_tac x = "n mod k" in spec, simp)
   992 done
   993 
   994 lemma split_neg_lemma:
   995  "k<0 ==>
   996     P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"
   997 apply (rule iffI, clarify)
   998  apply (erule_tac P="P x y" for x y in rev_mp)
   999  apply (subst mod_add_eq [symmetric])
  1000  apply (subst zdiv_zadd1_eq)
  1001  apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)
  1002 txt\<open>converse direction\<close>
  1003 apply (drule_tac x = "n div k" in spec)
  1004 apply (drule_tac x = "n mod k" in spec, simp)
  1005 done
  1006 
  1007 lemma split_zdiv:
  1008  "P(n div k :: int) =
  1009   ((k = 0 --> P 0) &
  1010    (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i)) &
  1011    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i)))"
  1012 apply (case_tac "k=0", simp)
  1013 apply (simp only: linorder_neq_iff)
  1014 apply (erule disjE)
  1015  apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"]
  1016                       split_neg_lemma [of concl: "%x y. P x"])
  1017 done
  1018 
  1019 lemma split_zmod:
  1020  "P(n mod k :: int) =
  1021   ((k = 0 --> P n) &
  1022    (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P j)) &
  1023    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P j)))"
  1024 apply (case_tac "k=0", simp)
  1025 apply (simp only: linorder_neq_iff)
  1026 apply (erule disjE)
  1027  apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"]
  1028                       split_neg_lemma [of concl: "%x y. P y"])
  1029 done
  1030 
  1031 text \<open>Enable (lin)arith to deal with @{const divide} and @{const modulo}
  1032   when these are applied to some constant that is of the form
  1033   @{term "numeral k"}:\<close>
  1034 declare split_zdiv [of _ _ "numeral k", arith_split] for k
  1035 declare split_zmod [of _ _ "numeral k", arith_split] for k
  1036 
  1037 
  1038 subsubsection \<open>Computing \<open>div\<close> and \<open>mod\<close> with shifting\<close>
  1039 
  1040 lemma pos_eucl_rel_int_mult_2:
  1041   assumes "0 \<le> b"
  1042   assumes "eucl_rel_int a b (q, r)"
  1043   shows "eucl_rel_int (1 + 2*a) (2*b) (q, 1 + 2*r)"
  1044   using assms unfolding eucl_rel_int_iff by auto
  1045 
  1046 lemma neg_eucl_rel_int_mult_2:
  1047   assumes "b \<le> 0"
  1048   assumes "eucl_rel_int (a + 1) b (q, r)"
  1049   shows "eucl_rel_int (1 + 2*a) (2*b) (q, 2*r - 1)"
  1050   using assms unfolding eucl_rel_int_iff by auto
  1051 
  1052 text\<open>computing div by shifting\<close>
  1053 
  1054 lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a"
  1055   using pos_eucl_rel_int_mult_2 [OF _ eucl_rel_int]
  1056   by (rule div_int_unique)
  1057 
  1058 lemma neg_zdiv_mult_2:
  1059   assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"
  1060   using neg_eucl_rel_int_mult_2 [OF A eucl_rel_int]
  1061   by (rule div_int_unique)
  1062 
  1063 (* FIXME: add rules for negative numerals *)
  1064 lemma zdiv_numeral_Bit0 [simp]:
  1065   "numeral (Num.Bit0 v) div numeral (Num.Bit0 w) =
  1066     numeral v div (numeral w :: int)"
  1067   unfolding numeral.simps unfolding mult_2 [symmetric]
  1068   by (rule div_mult_mult1, simp)
  1069 
  1070 lemma zdiv_numeral_Bit1 [simp]:
  1071   "numeral (Num.Bit1 v) div numeral (Num.Bit0 w) =
  1072     (numeral v div (numeral w :: int))"
  1073   unfolding numeral.simps
  1074   unfolding mult_2 [symmetric] add.commute [of _ 1]
  1075   by (rule pos_zdiv_mult_2, simp)
  1076 
  1077 lemma pos_zmod_mult_2:
  1078   fixes a b :: int
  1079   assumes "0 \<le> a"
  1080   shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)"
  1081   using pos_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
  1082   by (rule mod_int_unique)
  1083 
  1084 lemma neg_zmod_mult_2:
  1085   fixes a b :: int
  1086   assumes "a \<le> 0"
  1087   shows "(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1"
  1088   using neg_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
  1089   by (rule mod_int_unique)
  1090 
  1091 (* FIXME: add rules for negative numerals *)
  1092 lemma zmod_numeral_Bit0 [simp]:
  1093   "numeral (Num.Bit0 v) mod numeral (Num.Bit0 w) =
  1094     (2::int) * (numeral v mod numeral w)"
  1095   unfolding numeral_Bit0 [of v] numeral_Bit0 [of w]
  1096   unfolding mult_2 [symmetric] by (rule mod_mult_mult1)
  1097 
  1098 lemma zmod_numeral_Bit1 [simp]:
  1099   "numeral (Num.Bit1 v) mod numeral (Num.Bit0 w) =
  1100     2 * (numeral v mod numeral w) + (1::int)"
  1101   unfolding numeral_Bit1 [of v] numeral_Bit0 [of w]
  1102   unfolding mult_2 [symmetric] add.commute [of _ 1]
  1103   by (rule pos_zmod_mult_2, simp)
  1104 
  1105 lemma zdiv_eq_0_iff:
  1106  "(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")
  1107 proof
  1108   assume ?L
  1109   have "?L \<longrightarrow> ?R" by (rule split_zdiv[THEN iffD2]) simp
  1110   with \<open>?L\<close> show ?R by blast
  1111 next
  1112   assume ?R thus ?L
  1113     by(auto simp: div_pos_pos_trivial div_neg_neg_trivial)
  1114 qed
  1115 
  1116 lemma zmod_trival_iff:
  1117   fixes i k :: int
  1118   shows "i mod k = i \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i"
  1119 proof -
  1120   have "i mod k = i \<longleftrightarrow> i div k = 0"
  1121     by safe (insert div_mult_mod_eq [of i k], auto)
  1122   with zdiv_eq_0_iff
  1123   show ?thesis
  1124     by simp
  1125 qed
  1126 
  1127   
  1128 subsubsection \<open>Quotients of Signs\<close>
  1129 
  1130 lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"
  1131 by (simp add: divide_int_def)
  1132 
  1133 lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
  1134 by (simp add: modulo_int_def)
  1135 
  1136 lemma div_neg_pos_less0: "[| a < (0::int);  0 < b |] ==> a div b < 0"
  1137 apply (subgoal_tac "a div b \<le> -1", force)
  1138 apply (rule order_trans)
  1139 apply (rule_tac a' = "-1" in zdiv_mono1)
  1140 apply (auto simp add: div_eq_minus1)
  1141 done
  1142 
  1143 lemma div_nonneg_neg_le0: "[| (0::int) \<le> a; b < 0 |] ==> a div b \<le> 0"
  1144 by (drule zdiv_mono1_neg, auto)
  1145 
  1146 lemma div_nonpos_pos_le0: "[| (a::int) \<le> 0; b > 0 |] ==> a div b \<le> 0"
  1147 by (drule zdiv_mono1, auto)
  1148 
  1149 text\<open>Now for some equivalences of the form \<open>a div b >=< 0 \<longleftrightarrow> \<dots>\<close>
  1150 conditional upon the sign of \<open>a\<close> or \<open>b\<close>. There are many more.
  1151 They should all be simp rules unless that causes too much search.\<close>
  1152 
  1153 lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)"
  1154 apply auto
  1155 apply (drule_tac [2] zdiv_mono1)
  1156 apply (auto simp add: linorder_neq_iff)
  1157 apply (simp (no_asm_use) add: linorder_not_less [symmetric])
  1158 apply (blast intro: div_neg_pos_less0)
  1159 done
  1160 
  1161 lemma pos_imp_zdiv_pos_iff:
  1162   "0<k \<Longrightarrow> 0 < (i::int) div k \<longleftrightarrow> k \<le> i"
  1163 using pos_imp_zdiv_nonneg_iff[of k i] zdiv_eq_0_iff[of i k]
  1164 by arith
  1165 
  1166 lemma neg_imp_zdiv_nonneg_iff:
  1167   "b < (0::int) ==> (0 \<le> a div b) = (a \<le> (0::int))"
  1168 apply (subst div_minus_minus [symmetric])
  1169 apply (subst pos_imp_zdiv_nonneg_iff, auto)
  1170 done
  1171 
  1172 (*But not (a div b \<le> 0 iff a\<le>0); consider a=1, b=2 when a div b = 0.*)
  1173 lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)"
  1174 by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff)
  1175 
  1176 (*Again the law fails for \<le>: consider a = -1, b = -2 when a div b = 0*)
  1177 lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)"
  1178 by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)
  1179 
  1180 lemma nonneg1_imp_zdiv_pos_iff:
  1181   "(0::int) <= a \<Longrightarrow> (a div b > 0) = (a >= b & b>0)"
  1182 apply rule
  1183  apply rule
  1184   using div_pos_pos_trivial[of a b]apply arith
  1185  apply(cases "b=0")apply simp
  1186  using div_nonneg_neg_le0[of a b]apply arith
  1187 using int_one_le_iff_zero_less[of "a div b"] zdiv_mono1[of b a b]apply simp
  1188 done
  1189 
  1190 lemma zmod_le_nonneg_dividend: "(m::int) \<ge> 0 ==> m mod k \<le> m"
  1191 apply (rule split_zmod[THEN iffD2])
  1192 apply(fastforce dest: q_pos_lemma intro: split_mult_pos_le)
  1193 done
  1194 
  1195 
  1196 subsubsection \<open>Computation of Division and Remainder\<close>
  1197 
  1198 instantiation int :: unique_euclidean_semiring_numeral
  1199 begin
  1200 
  1201 definition divmod_int :: "num \<Rightarrow> num \<Rightarrow> int \<times> int"
  1202 where
  1203   "divmod_int m n = (numeral m div numeral n, numeral m mod numeral n)"
  1204 
  1205 definition divmod_step_int :: "num \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int"
  1206 where
  1207   "divmod_step_int l qr = (let (q, r) = qr
  1208     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
  1209     else (2 * q, r))"
  1210 
  1211 instance
  1212   by standard (auto intro: zmod_le_nonneg_dividend simp add: divmod_int_def divmod_step_int_def
  1213     pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial zmod_zmult2_eq zdiv_zmult2_eq)
  1214 
  1215 end
  1216 
  1217 declare divmod_algorithm_code [where ?'a = int, code]
  1218 
  1219 context
  1220 begin
  1221   
  1222 qualified definition adjust_div :: "int \<times> int \<Rightarrow> int"
  1223 where
  1224   "adjust_div qr = (let (q, r) = qr in q + of_bool (r \<noteq> 0))"
  1225 
  1226 qualified lemma adjust_div_eq [simp, code]:
  1227   "adjust_div (q, r) = q + of_bool (r \<noteq> 0)"
  1228   by (simp add: adjust_div_def)
  1229 
  1230 qualified definition adjust_mod :: "int \<Rightarrow> int \<Rightarrow> int"
  1231 where
  1232   [simp]: "adjust_mod l r = (if r = 0 then 0 else l - r)"
  1233 
  1234 lemma minus_numeral_div_numeral [simp]:
  1235   "- numeral m div numeral n = - (adjust_div (divmod m n) :: int)"
  1236 proof -
  1237   have "int (fst (divmod m n)) = fst (divmod m n)"
  1238     by (simp only: fst_divmod divide_int_def) auto
  1239   then show ?thesis
  1240     by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
  1241 qed
  1242 
  1243 lemma minus_numeral_mod_numeral [simp]:
  1244   "- numeral m mod numeral n = adjust_mod (numeral n) (snd (divmod m n) :: int)"
  1245 proof -
  1246   have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
  1247     using that by (simp only: snd_divmod modulo_int_def) auto
  1248   then show ?thesis
  1249     by (auto simp add: split_def Let_def adjust_div_def divides_aux_def modulo_int_def)
  1250 qed
  1251 
  1252 lemma numeral_div_minus_numeral [simp]:
  1253   "numeral m div - numeral n = - (adjust_div (divmod m n) :: int)"
  1254 proof -
  1255   have "int (fst (divmod m n)) = fst (divmod m n)"
  1256     by (simp only: fst_divmod divide_int_def) auto
  1257   then show ?thesis
  1258     by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
  1259 qed
  1260   
  1261 lemma numeral_mod_minus_numeral [simp]:
  1262   "numeral m mod - numeral n = - adjust_mod (numeral n) (snd (divmod m n) :: int)"
  1263 proof -
  1264   have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
  1265     using that by (simp only: snd_divmod modulo_int_def) auto
  1266   then show ?thesis
  1267     by (auto simp add: split_def Let_def adjust_div_def divides_aux_def modulo_int_def)
  1268 qed
  1269 
  1270 lemma minus_one_div_numeral [simp]:
  1271   "- 1 div numeral n = - (adjust_div (divmod Num.One n) :: int)"
  1272   using minus_numeral_div_numeral [of Num.One n] by simp  
  1273 
  1274 lemma minus_one_mod_numeral [simp]:
  1275   "- 1 mod numeral n = adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
  1276   using minus_numeral_mod_numeral [of Num.One n] by simp
  1277 
  1278 lemma one_div_minus_numeral [simp]:
  1279   "1 div - numeral n = - (adjust_div (divmod Num.One n) :: int)"
  1280   using numeral_div_minus_numeral [of Num.One n] by simp
  1281   
  1282 lemma one_mod_minus_numeral [simp]:
  1283   "1 mod - numeral n = - adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
  1284   using numeral_mod_minus_numeral [of Num.One n] by simp
  1285 
  1286 end
  1287 
  1288 
  1289 subsubsection \<open>Further properties\<close>
  1290 
  1291 text \<open>Simplify expresions in which div and mod combine numerical constants\<close>
  1292 
  1293 lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
  1294   by (rule div_int_unique [of a b q r]) (simp add: eucl_rel_int_iff)
  1295 
  1296 lemma int_div_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a div b = q"
  1297   by (rule div_int_unique [of a b q r],
  1298     simp add: eucl_rel_int_iff)
  1299 
  1300 lemma int_mod_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a mod b = r"
  1301   by (rule mod_int_unique [of a b q r],
  1302     simp add: eucl_rel_int_iff)
  1303 
  1304 lemma int_mod_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a mod b = r"
  1305   by (rule mod_int_unique [of a b q r],
  1306     simp add: eucl_rel_int_iff)
  1307 
  1308 lemma abs_div: "(y::int) dvd x \<Longrightarrow> \<bar>x div y\<bar> = \<bar>x\<bar> div \<bar>y\<bar>"
  1309 by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
  1310 
  1311 text\<open>Suggested by Matthias Daum\<close>
  1312 lemma int_power_div_base:
  1313      "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"
  1314 apply (subgoal_tac "k ^ m = k ^ ((m - Suc 0) + Suc 0)")
  1315  apply (erule ssubst)
  1316  apply (simp only: power_add)
  1317  apply simp_all
  1318 done
  1319 
  1320 text \<open>Distributive laws for function \<open>nat\<close>.\<close>
  1321 
  1322 lemma nat_div_distrib: "0 \<le> x \<Longrightarrow> nat (x div y) = nat x div nat y"
  1323 apply (rule linorder_cases [of y 0])
  1324 apply (simp add: div_nonneg_neg_le0)
  1325 apply simp
  1326 apply (simp add: nat_eq_iff pos_imp_zdiv_nonneg_iff zdiv_int)
  1327 done
  1328 
  1329 (*Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't*)
  1330 lemma nat_mod_distrib:
  1331   "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x mod y) = nat x mod nat y"
  1332 apply (case_tac "y = 0", simp)
  1333 apply (simp add: nat_eq_iff zmod_int)
  1334 done
  1335 
  1336 text  \<open>transfer setup\<close>
  1337 
  1338 lemma transfer_nat_int_functions:
  1339     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
  1340     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
  1341   by (auto simp add: nat_div_distrib nat_mod_distrib)
  1342 
  1343 lemma transfer_nat_int_function_closures:
  1344     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
  1345     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
  1346   apply (cases "y = 0")
  1347   apply (auto simp add: pos_imp_zdiv_nonneg_iff)
  1348   apply (cases "y = 0")
  1349   apply auto
  1350 done
  1351 
  1352 declare transfer_morphism_nat_int [transfer add return:
  1353   transfer_nat_int_functions
  1354   transfer_nat_int_function_closures
  1355 ]
  1356 
  1357 lemma transfer_int_nat_functions:
  1358     "(int x) div (int y) = int (x div y)"
  1359     "(int x) mod (int y) = int (x mod y)"
  1360   by (auto simp add: zdiv_int zmod_int)
  1361 
  1362 lemma transfer_int_nat_function_closures:
  1363     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
  1364     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
  1365   by (simp_all only: is_nat_def transfer_nat_int_function_closures)
  1366 
  1367 declare transfer_morphism_int_nat [transfer add return:
  1368   transfer_int_nat_functions
  1369   transfer_int_nat_function_closures
  1370 ]
  1371 
  1372 text\<open>Suggested by Matthias Daum\<close>
  1373 lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
  1374 apply (subgoal_tac "nat x div nat k < nat x")
  1375  apply (simp add: nat_div_distrib [symmetric])
  1376 apply (rule div_less_dividend, simp_all)
  1377 done
  1378 
  1379 lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \<le> x"
  1380   shows "\<exists>q. x = y + n * q"
  1381 proof-
  1382   from xy have th: "int x - int y = int (x - y)" by simp
  1383   from xyn have "int x mod int n = int y mod int n"
  1384     by (simp add: zmod_int [symmetric])
  1385   hence "int n dvd int x - int y" by (simp only: mod_eq_dvd_iff [symmetric])
  1386   hence "n dvd x - y" by (simp add: th zdvd_int)
  1387   then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith
  1388 qed
  1389 
  1390 lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)"
  1391   (is "?lhs = ?rhs")
  1392 proof
  1393   assume H: "x mod n = y mod n"
  1394   {assume xy: "x \<le> y"
  1395     from H have th: "y mod n = x mod n" by simp
  1396     from nat_mod_eq_lemma[OF th xy] have ?rhs
  1397       apply clarify  apply (rule_tac x="q" in exI) by (rule exI[where x="0"], simp)}
  1398   moreover
  1399   {assume xy: "y \<le> x"
  1400     from nat_mod_eq_lemma[OF H xy] have ?rhs
  1401       apply clarify  apply (rule_tac x="0" in exI) by (rule_tac x="q" in exI, simp)}
  1402   ultimately  show ?rhs using linear[of x y] by blast
  1403 next
  1404   assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast
  1405   hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp
  1406   thus  ?lhs by simp
  1407 qed
  1408 
  1409 
  1410 subsubsection \<open>Dedicated simproc for calculation\<close>
  1411 
  1412 text \<open>
  1413   There is space for improvement here: the calculation itself
  1414   could be carried out outside the logic, and a generic simproc
  1415   (simplifier setup) for generic calculation would be helpful. 
  1416 \<close>
  1417 
  1418 simproc_setup numeral_divmod
  1419   ("0 div 0 :: 'a :: unique_euclidean_semiring_numeral" | "0 mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
  1420    "0 div 1 :: 'a :: unique_euclidean_semiring_numeral" | "0 mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
  1421    "0 div - 1 :: int" | "0 mod - 1 :: int" |
  1422    "0 div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "0 mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
  1423    "0 div - numeral b :: int" | "0 mod - numeral b :: int" |
  1424    "1 div 0 :: 'a :: unique_euclidean_semiring_numeral" | "1 mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
  1425    "1 div 1 :: 'a :: unique_euclidean_semiring_numeral" | "1 mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
  1426    "1 div - 1 :: int" | "1 mod - 1 :: int" |
  1427    "1 div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "1 mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
  1428    "1 div - numeral b :: int" |"1 mod - numeral b :: int" |
  1429    "- 1 div 0 :: int" | "- 1 mod 0 :: int" | "- 1 div 1 :: int" | "- 1 mod 1 :: int" |
  1430    "- 1 div - 1 :: int" | "- 1 mod - 1 :: int" | "- 1 div numeral b :: int" | "- 1 mod numeral b :: int" |
  1431    "- 1 div - numeral b :: int" | "- 1 mod - numeral b :: int" |
  1432    "numeral a div 0 :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
  1433    "numeral a div 1 :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
  1434    "numeral a div - 1 :: int" | "numeral a mod - 1 :: int" |
  1435    "numeral a div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
  1436    "numeral a div - numeral b :: int" | "numeral a mod - numeral b :: int" |
  1437    "- numeral a div 0 :: int" | "- numeral a mod 0 :: int" |
  1438    "- numeral a div 1 :: int" | "- numeral a mod 1 :: int" |
  1439    "- numeral a div - 1 :: int" | "- numeral a mod - 1 :: int" |
  1440    "- numeral a div numeral b :: int" | "- numeral a mod numeral b :: int" |
  1441    "- numeral a div - numeral b :: int" | "- numeral a mod - numeral b :: int") =
  1442 \<open> let
  1443     val if_cong = the (Code.get_case_cong @{theory} @{const_name If});
  1444     fun successful_rewrite ctxt ct =
  1445       let
  1446         val thm = Simplifier.rewrite ctxt ct
  1447       in if Thm.is_reflexive thm then NONE else SOME thm end;
  1448   in fn phi =>
  1449     let
  1450       val simps = Morphism.fact phi (@{thms div_0 mod_0 div_by_0 mod_by_0 div_by_1 mod_by_1
  1451         one_div_numeral one_mod_numeral minus_one_div_numeral minus_one_mod_numeral
  1452         one_div_minus_numeral one_mod_minus_numeral
  1453         numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral
  1454         numeral_div_minus_numeral numeral_mod_minus_numeral
  1455         div_minus_minus mod_minus_minus Divides.adjust_div_eq of_bool_eq one_neq_zero
  1456         numeral_neq_zero neg_equal_0_iff_equal arith_simps arith_special divmod_trivial
  1457         divmod_cancel divmod_steps divmod_step_eq fst_conv snd_conv numeral_One
  1458         case_prod_beta rel_simps Divides.adjust_mod_def div_minus1_right mod_minus1_right
  1459         minus_minus numeral_times_numeral mult_zero_right mult_1_right}
  1460         @ [@{lemma "0 = 0 \<longleftrightarrow> True" by simp}]);
  1461       fun prepare_simpset ctxt = HOL_ss |> Simplifier.simpset_map ctxt
  1462         (Simplifier.add_cong if_cong #> fold Simplifier.add_simp simps)
  1463     in fn ctxt => successful_rewrite (Simplifier.put_simpset (prepare_simpset ctxt) ctxt) end
  1464   end;
  1465 \<close>
  1466 
  1467 
  1468 subsubsection \<open>Code generation\<close>
  1469 
  1470 lemma [code]:
  1471   fixes k :: int
  1472   shows 
  1473     "k div 0 = 0"
  1474     "k mod 0 = k"
  1475     "0 div k = 0"
  1476     "0 mod k = 0"
  1477     "k div Int.Pos Num.One = k"
  1478     "k mod Int.Pos Num.One = 0"
  1479     "k div Int.Neg Num.One = - k"
  1480     "k mod Int.Neg Num.One = 0"
  1481     "Int.Pos m div Int.Pos n = (fst (divmod m n) :: int)"
  1482     "Int.Pos m mod Int.Pos n = (snd (divmod m n) :: int)"
  1483     "Int.Neg m div Int.Pos n = - (Divides.adjust_div (divmod m n) :: int)"
  1484     "Int.Neg m mod Int.Pos n = Divides.adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
  1485     "Int.Pos m div Int.Neg n = - (Divides.adjust_div (divmod m n) :: int)"
  1486     "Int.Pos m mod Int.Neg n = - Divides.adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
  1487     "Int.Neg m div Int.Neg n = (fst (divmod m n) :: int)"
  1488     "Int.Neg m mod Int.Neg n = - (snd (divmod m n) :: int)"
  1489   by simp_all
  1490 
  1491 code_identifier
  1492   code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  1493 
  1494 lemma dvd_eq_mod_eq_0_numeral:
  1495   "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semidom_modulo)"
  1496   by (fact dvd_eq_mod_eq_0)
  1497 
  1498 declare minus_div_mult_eq_mod [symmetric, nitpick_unfold]
  1499 
  1500 
  1501 subsubsection \<open>Lemmas of doubtful value\<close>
  1502 
  1503 lemma mod_mult_self3':
  1504   "Suc (k * n + m) mod n = Suc m mod n"
  1505   by (fact Suc_mod_mult_self3)
  1506 
  1507 lemma mod_Suc_eq_Suc_mod:
  1508   "Suc m mod n = Suc (m mod n) mod n"
  1509   by (simp add: mod_simps)
  1510 
  1511 lemma div_geq:
  1512   "m div n = Suc ((m - n) div n)" if "0 < n" and " \<not> m < n" for m n :: nat
  1513   by (rule le_div_geq) (use that in \<open>simp_all add: not_less\<close>)
  1514 
  1515 lemma mod_geq:
  1516   "m mod n = (m - n) mod n" if "\<not> m < n" for m n :: nat
  1517   by (rule le_mod_geq) (use that in \<open>simp add: not_less\<close>)
  1518 
  1519 lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
  1520   by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
  1521 
  1522 lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
  1523 
  1524 (*Loses information, namely we also have r<d provided d is nonzero*)
  1525 lemma mod_eqD:
  1526   fixes m d r q :: nat
  1527   assumes "m mod d = r"
  1528   shows "\<exists>q. m = r + q * d"
  1529 proof -
  1530   from div_mult_mod_eq obtain q where "q * d + m mod d = m" by blast
  1531   with assms have "m = r + q * d" by simp
  1532   then show ?thesis ..
  1533 qed
  1534 
  1535 end