src/HOL/Divides.thy
author haftmann
Sun Oct 08 22:28:21 2017 +0200 (21 months ago)
changeset 66810 cc2b490f9dc4
parent 66808 1907167b6038
child 66814 a24cde9588bb
permissions -rw-r--r--
generalized simproc
     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 lemma is_unit_int:
   531   "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
   532   by auto
   533 
   534 lemma zdiv_int:
   535   "int (a div b) = int a div int b"
   536   by (simp add: divide_int_def)
   537 
   538 lemma zmod_int:
   539   "int (a mod b) = int a mod int b"
   540   by (simp add: modulo_int_def int_dvd_iff)
   541 
   542 lemma div_abs_eq_div_nat:
   543   "\<bar>k\<bar> div \<bar>l\<bar> = int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)"
   544   by (simp add: divide_int_def)
   545 
   546 lemma mod_abs_eq_div_nat:
   547   "\<bar>k\<bar> mod \<bar>l\<bar> = int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)"
   548   by (simp add: modulo_int_def dvd_int_unfold_dvd_nat)
   549 
   550 lemma div_sgn_abs_cancel:
   551   fixes k l v :: int
   552   assumes "v \<noteq> 0"
   553   shows "(sgn v * \<bar>k\<bar>) div (sgn v * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
   554 proof -
   555   from assms have "sgn v = - 1 \<or> sgn v = 1"
   556     by (cases "v \<ge> 0") auto
   557   then show ?thesis
   558     using assms unfolding divide_int_def [of "sgn v * \<bar>k\<bar>" "sgn v * \<bar>l\<bar>"]
   559     by (fastforce simp add: not_less div_abs_eq_div_nat)
   560 qed
   561 
   562 lemma div_eq_sgn_abs:
   563   fixes k l v :: int
   564   assumes "sgn k = sgn l"
   565   shows "k div l = \<bar>k\<bar> div \<bar>l\<bar>"
   566 proof (cases "l = 0")
   567   case True
   568   then show ?thesis
   569     by simp
   570 next
   571   case False
   572   with assms have "(sgn k * \<bar>k\<bar>) div (sgn l * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
   573     by (simp add: div_sgn_abs_cancel)
   574   then show ?thesis
   575     by (simp add: sgn_mult_abs)
   576 qed
   577 
   578 lemma div_dvd_sgn_abs:
   579   fixes k l :: int
   580   assumes "l dvd k"
   581   shows "k div l = (sgn k * sgn l) * (\<bar>k\<bar> div \<bar>l\<bar>)"
   582 proof (cases "k = 0")
   583   case True
   584   then show ?thesis
   585     by simp
   586 next
   587   case False
   588   show ?thesis
   589   proof (cases "sgn l = sgn k")
   590     case True
   591     then show ?thesis
   592       by (simp add: div_eq_sgn_abs)
   593   next
   594     case False
   595     with \<open>k \<noteq> 0\<close> assms show ?thesis
   596       unfolding divide_int_def [of k l]
   597         by (auto simp add: zdiv_int)
   598   qed
   599 qed
   600 
   601 lemma div_noneq_sgn_abs:
   602   fixes k l :: int
   603   assumes "l \<noteq> 0"
   604   assumes "sgn k \<noteq> sgn l"
   605   shows "k div l = - (\<bar>k\<bar> div \<bar>l\<bar>) - of_bool (\<not> l dvd k)"
   606   using assms
   607   by (simp only: divide_int_def [of k l], auto simp add: not_less zdiv_int)
   608   
   609 lemma sgn_mod:
   610   fixes k l :: int
   611   assumes "l \<noteq> 0" "\<not> l dvd k"
   612   shows "sgn (k mod l) = sgn l"
   613 proof -
   614   from \<open>\<not> l dvd k\<close>
   615   have "k mod l \<noteq> 0"
   616     by (simp add: dvd_eq_mod_eq_0)
   617   show ?thesis
   618     using \<open>l \<noteq> 0\<close> \<open>\<not> l dvd k\<close>
   619     unfolding modulo_int_def [of k l]
   620     by (auto simp add: sgn_1_pos sgn_1_neg mod_greater_zero_iff_not_dvd nat_dvd_iff not_less
   621       zless_nat_eq_int_zless [symmetric] elim: nonpos_int_cases)
   622 qed
   623 
   624 lemma abs_mod_less:
   625   fixes k l :: int
   626   assumes "l \<noteq> 0"
   627   shows "\<bar>k mod l\<bar> < \<bar>l\<bar>"
   628   using assms unfolding modulo_int_def [of k l]
   629   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)
   630 
   631 instantiation int :: unique_euclidean_ring
   632 begin
   633 
   634 definition [simp]:
   635   "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
   636 
   637 definition [simp]:
   638   "uniqueness_constraint_int (k :: int) l \<longleftrightarrow> unit_factor k = unit_factor l"
   639   
   640 instance proof
   641   fix l q r:: int
   642   assume "uniqueness_constraint r l"
   643     and "euclidean_size r < euclidean_size l"
   644   then have "sgn r = sgn l" and "\<bar>r\<bar> < \<bar>l\<bar>"
   645     by simp_all
   646   then have "eucl_rel_int (q * l + r) l (q, r)"
   647     by (rule eucl_rel_int_remainderI) simp
   648   then show "(q * l + r) div l = q"
   649     by (rule div_int_unique)
   650 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>)
   651 
   652 end
   653 
   654 text\<open>Basic laws about division and remainder\<close>
   655 
   656 lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
   657   using eucl_rel_int [of a b]
   658   by (auto simp add: eucl_rel_int_iff prod_eq_iff)
   659 
   660 lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1]
   661    and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2]
   662 
   663 lemma neg_mod_conj: "b < (0::int) \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b"
   664   using eucl_rel_int [of a b]
   665   by (auto simp add: eucl_rel_int_iff prod_eq_iff)
   666 
   667 lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1]
   668    and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2]
   669 
   670 
   671 subsubsection \<open>General Properties of div and mod\<close>
   672 
   673 lemma div_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a div b = 0"
   674 apply (rule div_int_unique)
   675 apply (auto simp add: eucl_rel_int_iff)
   676 done
   677 
   678 lemma div_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a div b = 0"
   679 apply (rule div_int_unique)
   680 apply (auto simp add: eucl_rel_int_iff)
   681 done
   682 
   683 lemma div_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a div b = -1"
   684 apply (rule div_int_unique)
   685 apply (auto simp add: eucl_rel_int_iff)
   686 done
   687 
   688 lemma div_positive_int:
   689   "k div l > 0" if "k \<ge> l" and "l > 0" for k l :: int
   690   using that by (simp add: divide_int_def div_positive)
   691 
   692 (*There is no div_neg_pos_trivial because  0 div b = 0 would supersede it*)
   693 
   694 lemma mod_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a mod b = a"
   695 apply (rule_tac q = 0 in mod_int_unique)
   696 apply (auto simp add: eucl_rel_int_iff)
   697 done
   698 
   699 lemma mod_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a mod b = a"
   700 apply (rule_tac q = 0 in mod_int_unique)
   701 apply (auto simp add: eucl_rel_int_iff)
   702 done
   703 
   704 lemma mod_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a mod b = a+b"
   705 apply (rule_tac q = "-1" in mod_int_unique)
   706 apply (auto simp add: eucl_rel_int_iff)
   707 done
   708 
   709 text\<open>There is no \<open>mod_neg_pos_trivial\<close>.\<close>
   710 
   711 
   712 subsubsection \<open>Laws for div and mod with Unary Minus\<close>
   713 
   714 lemma zminus1_lemma:
   715      "eucl_rel_int a b (q, r) ==> b \<noteq> 0
   716       ==> eucl_rel_int (-a) b (if r=0 then -q else -q - 1,
   717                           if r=0 then 0 else b-r)"
   718 by (force simp add: eucl_rel_int_iff right_diff_distrib)
   719 
   720 
   721 lemma zdiv_zminus1_eq_if:
   722      "b \<noteq> (0::int)
   723       ==> (-a) div b =
   724           (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
   725 by (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN div_int_unique])
   726 
   727 lemma zmod_zminus1_eq_if:
   728      "(-a::int) mod b = (if a mod b = 0 then 0 else  b - (a mod b))"
   729 apply (case_tac "b = 0", simp)
   730 apply (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN mod_int_unique])
   731 done
   732 
   733 lemma zmod_zminus1_not_zero:
   734   fixes k l :: int
   735   shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
   736   by (simp add: mod_eq_0_iff_dvd)
   737 
   738 lemma zmod_zminus2_not_zero:
   739   fixes k l :: int
   740   shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
   741   by (simp add: mod_eq_0_iff_dvd)
   742 
   743 lemma zdiv_zminus2_eq_if:
   744      "b \<noteq> (0::int)
   745       ==> a div (-b) =
   746           (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
   747 by (simp add: zdiv_zminus1_eq_if div_minus_right)
   748 
   749 lemma zmod_zminus2_eq_if:
   750      "a mod (-b::int) = (if a mod b = 0 then 0 else  (a mod b) - b)"
   751 by (simp add: zmod_zminus1_eq_if mod_minus_right)
   752 
   753 
   754 subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
   755 
   756 lemma zdiv_mono1: "[| a \<le> a';  0 < (b::int) |] ==> a div b \<le> a' div b"
   757 using mult_div_mod_eq [symmetric, of a b]
   758 using mult_div_mod_eq [symmetric, of a' b]
   759 apply -
   760 apply (rule unique_quotient_lemma)
   761 apply (erule subst)
   762 apply (erule subst, simp_all)
   763 done
   764 
   765 lemma zdiv_mono1_neg: "[| a \<le> a';  (b::int) < 0 |] ==> a' div b \<le> a div b"
   766 using mult_div_mod_eq [symmetric, of a b]
   767 using mult_div_mod_eq [symmetric, of a' b]
   768 apply -
   769 apply (rule unique_quotient_lemma_neg)
   770 apply (erule subst)
   771 apply (erule subst, simp_all)
   772 done
   773 
   774 
   775 subsubsection \<open>Monotonicity in the Second Argument (Divisor)\<close>
   776 
   777 lemma q_pos_lemma:
   778      "[| 0 \<le> b'*q' + r'; r' < b';  0 < b' |] ==> 0 \<le> (q'::int)"
   779 apply (subgoal_tac "0 < b'* (q' + 1) ")
   780  apply (simp add: zero_less_mult_iff)
   781 apply (simp add: distrib_left)
   782 done
   783 
   784 lemma zdiv_mono2_lemma:
   785      "[| b*q + r = b'*q' + r';  0 \<le> b'*q' + r';
   786          r' < b';  0 \<le> r;  0 < b';  b' \<le> b |]
   787       ==> q \<le> (q'::int)"
   788 apply (frule q_pos_lemma, assumption+)
   789 apply (subgoal_tac "b*q < b* (q' + 1) ")
   790  apply (simp add: mult_less_cancel_left)
   791 apply (subgoal_tac "b*q = r' - r + b'*q'")
   792  prefer 2 apply simp
   793 apply (simp (no_asm_simp) add: distrib_left)
   794 apply (subst add.commute, rule add_less_le_mono, arith)
   795 apply (rule mult_right_mono, auto)
   796 done
   797 
   798 lemma zdiv_mono2:
   799      "[| (0::int) \<le> a;  0 < b';  b' \<le> b |] ==> a div b \<le> a div b'"
   800 apply (subgoal_tac "b \<noteq> 0")
   801   prefer 2 apply arith
   802 using mult_div_mod_eq [symmetric, of a b]
   803 using mult_div_mod_eq [symmetric, of a b']
   804 apply -
   805 apply (rule zdiv_mono2_lemma)
   806 apply (erule subst)
   807 apply (erule subst, simp_all)
   808 done
   809 
   810 lemma q_neg_lemma:
   811      "[| b'*q' + r' < 0;  0 \<le> r';  0 < b' |] ==> q' \<le> (0::int)"
   812 apply (subgoal_tac "b'*q' < 0")
   813  apply (simp add: mult_less_0_iff, arith)
   814 done
   815 
   816 lemma zdiv_mono2_neg_lemma:
   817      "[| b*q + r = b'*q' + r';  b'*q' + r' < 0;
   818          r < b;  0 \<le> r';  0 < b';  b' \<le> b |]
   819       ==> q' \<le> (q::int)"
   820 apply (frule q_neg_lemma, assumption+)
   821 apply (subgoal_tac "b*q' < b* (q + 1) ")
   822  apply (simp add: mult_less_cancel_left)
   823 apply (simp add: distrib_left)
   824 apply (subgoal_tac "b*q' \<le> b'*q'")
   825  prefer 2 apply (simp add: mult_right_mono_neg, arith)
   826 done
   827 
   828 lemma zdiv_mono2_neg:
   829      "[| a < (0::int);  0 < b';  b' \<le> b |] ==> a div b' \<le> a div b"
   830 using mult_div_mod_eq [symmetric, of a b]
   831 using mult_div_mod_eq [symmetric, of a b']
   832 apply -
   833 apply (rule zdiv_mono2_neg_lemma)
   834 apply (erule subst)
   835 apply (erule subst, simp_all)
   836 done
   837 
   838 
   839 subsubsection \<open>More Algebraic Laws for div and mod\<close>
   840 
   841 text\<open>proving (a*b) div c = a * (b div c) + a * (b mod c)\<close>
   842 
   843 lemma zmult1_lemma:
   844      "[| eucl_rel_int b c (q, r) |]
   845       ==> eucl_rel_int (a * b) c (a*q + a*r div c, a*r mod c)"
   846 by (auto simp add: split_ifs eucl_rel_int_iff linorder_neq_iff distrib_left ac_simps)
   847 
   848 lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
   849 apply (case_tac "c = 0", simp)
   850 apply (blast intro: eucl_rel_int [THEN zmult1_lemma, THEN div_int_unique])
   851 done
   852 
   853 text\<open>proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c)\<close>
   854 
   855 lemma zadd1_lemma:
   856      "[| eucl_rel_int a c (aq, ar);  eucl_rel_int b c (bq, br) |]
   857       ==> eucl_rel_int (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
   858 by (force simp add: split_ifs eucl_rel_int_iff linorder_neq_iff distrib_left)
   859 
   860 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
   861 lemma zdiv_zadd1_eq:
   862      "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
   863 apply (case_tac "c = 0", simp)
   864 apply (blast intro: zadd1_lemma [OF eucl_rel_int eucl_rel_int] div_int_unique)
   865 done
   866 
   867 lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
   868 by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
   869 
   870 (* REVISIT: should this be generalized to all semiring_div types? *)
   871 lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
   872 
   873 
   874 subsubsection \<open>Proving  @{term "a div (b * c) = (a div b) div c"}\<close>
   875 
   876 (*The condition c>0 seems necessary.  Consider that 7 div ~6 = ~2 but
   877   7 div 2 div ~3 = 3 div ~3 = ~1.  The subcase (a div b) mod c = 0 seems
   878   to cause particular problems.*)
   879 
   880 text\<open>first, four lemmas to bound the remainder for the cases b<0 and b>0\<close>
   881 
   882 lemma zmult2_lemma_aux1: "[| (0::int) < c;  b < r;  r \<le> 0 |] ==> b * c < b * (q mod c) + r"
   883 apply (subgoal_tac "b * (c - q mod c) < r * 1")
   884  apply (simp add: algebra_simps)
   885 apply (rule order_le_less_trans)
   886  apply (erule_tac [2] mult_strict_right_mono)
   887  apply (rule mult_left_mono_neg)
   888   using add1_zle_eq[of "q mod c"]apply(simp add: algebra_simps)
   889  apply (simp)
   890 apply (simp)
   891 done
   892 
   893 lemma zmult2_lemma_aux2:
   894      "[| (0::int) < c;   b < r;  r \<le> 0 |] ==> b * (q mod c) + r \<le> 0"
   895 apply (subgoal_tac "b * (q mod c) \<le> 0")
   896  apply arith
   897 apply (simp add: mult_le_0_iff)
   898 done
   899 
   900 lemma zmult2_lemma_aux3: "[| (0::int) < c;  0 \<le> r;  r < b |] ==> 0 \<le> b * (q mod c) + r"
   901 apply (subgoal_tac "0 \<le> b * (q mod c) ")
   902 apply arith
   903 apply (simp add: zero_le_mult_iff)
   904 done
   905 
   906 lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 \<le> r; r < b |] ==> b * (q mod c) + r < b * c"
   907 apply (subgoal_tac "r * 1 < b * (c - q mod c) ")
   908  apply (simp add: right_diff_distrib)
   909 apply (rule order_less_le_trans)
   910  apply (erule mult_strict_right_mono)
   911  apply (rule_tac [2] mult_left_mono)
   912   apply simp
   913  using add1_zle_eq[of "q mod c"] apply (simp add: algebra_simps)
   914 apply simp
   915 done
   916 
   917 lemma zmult2_lemma: "[| eucl_rel_int a b (q, r); 0 < c |]
   918       ==> eucl_rel_int a (b * c) (q div c, b*(q mod c) + r)"
   919 by (auto simp add: mult.assoc eucl_rel_int_iff linorder_neq_iff
   920                    zero_less_mult_iff distrib_left [symmetric]
   921                    zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: if_split_asm)
   922 
   923 lemma zdiv_zmult2_eq:
   924   fixes a b c :: int
   925   shows "0 \<le> c \<Longrightarrow> a div (b * c) = (a div b) div c"
   926 apply (case_tac "b = 0", simp)
   927 apply (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN div_int_unique])
   928 done
   929 
   930 lemma zmod_zmult2_eq:
   931   fixes a b c :: int
   932   shows "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
   933 apply (case_tac "b = 0", simp)
   934 apply (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN mod_int_unique])
   935 done
   936 
   937 lemma div_pos_geq:
   938   fixes k l :: int
   939   assumes "0 < l" and "l \<le> k"
   940   shows "k div l = (k - l) div l + 1"
   941 proof -
   942   have "k = (k - l) + l" by simp
   943   then obtain j where k: "k = j + l" ..
   944   with assms show ?thesis by (simp add: div_add_self2)
   945 qed
   946 
   947 lemma mod_pos_geq:
   948   fixes k l :: int
   949   assumes "0 < l" and "l \<le> k"
   950   shows "k mod l = (k - l) mod l"
   951 proof -
   952   have "k = (k - l) + l" by simp
   953   then obtain j where k: "k = j + l" ..
   954   with assms show ?thesis by simp
   955 qed
   956 
   957 
   958 subsubsection \<open>Splitting Rules for div and mod\<close>
   959 
   960 text\<open>The proofs of the two lemmas below are essentially identical\<close>
   961 
   962 lemma split_pos_lemma:
   963  "0<k ==>
   964     P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"
   965 apply (rule iffI, clarify)
   966  apply (erule_tac P="P x y" for x y in rev_mp)
   967  apply (subst mod_add_eq [symmetric])
   968  apply (subst zdiv_zadd1_eq)
   969  apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)
   970 txt\<open>converse direction\<close>
   971 apply (drule_tac x = "n div k" in spec)
   972 apply (drule_tac x = "n mod k" in spec, simp)
   973 done
   974 
   975 lemma split_neg_lemma:
   976  "k<0 ==>
   977     P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"
   978 apply (rule iffI, clarify)
   979  apply (erule_tac P="P x y" for x y in rev_mp)
   980  apply (subst mod_add_eq [symmetric])
   981  apply (subst zdiv_zadd1_eq)
   982  apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)
   983 txt\<open>converse direction\<close>
   984 apply (drule_tac x = "n div k" in spec)
   985 apply (drule_tac x = "n mod k" in spec, simp)
   986 done
   987 
   988 lemma split_zdiv:
   989  "P(n div k :: int) =
   990   ((k = 0 --> P 0) &
   991    (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i)) &
   992    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i)))"
   993 apply (case_tac "k=0", simp)
   994 apply (simp only: linorder_neq_iff)
   995 apply (erule disjE)
   996  apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"]
   997                       split_neg_lemma [of concl: "%x y. P x"])
   998 done
   999 
  1000 lemma split_zmod:
  1001  "P(n mod k :: int) =
  1002   ((k = 0 --> P n) &
  1003    (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P j)) &
  1004    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P j)))"
  1005 apply (case_tac "k=0", simp)
  1006 apply (simp only: linorder_neq_iff)
  1007 apply (erule disjE)
  1008  apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"]
  1009                       split_neg_lemma [of concl: "%x y. P y"])
  1010 done
  1011 
  1012 text \<open>Enable (lin)arith to deal with @{const divide} and @{const modulo}
  1013   when these are applied to some constant that is of the form
  1014   @{term "numeral k"}:\<close>
  1015 declare split_zdiv [of _ _ "numeral k", arith_split] for k
  1016 declare split_zmod [of _ _ "numeral k", arith_split] for k
  1017 
  1018 
  1019 subsubsection \<open>Computing \<open>div\<close> and \<open>mod\<close> with shifting\<close>
  1020 
  1021 lemma pos_eucl_rel_int_mult_2:
  1022   assumes "0 \<le> b"
  1023   assumes "eucl_rel_int a b (q, r)"
  1024   shows "eucl_rel_int (1 + 2*a) (2*b) (q, 1 + 2*r)"
  1025   using assms unfolding eucl_rel_int_iff by auto
  1026 
  1027 lemma neg_eucl_rel_int_mult_2:
  1028   assumes "b \<le> 0"
  1029   assumes "eucl_rel_int (a + 1) b (q, r)"
  1030   shows "eucl_rel_int (1 + 2*a) (2*b) (q, 2*r - 1)"
  1031   using assms unfolding eucl_rel_int_iff by auto
  1032 
  1033 text\<open>computing div by shifting\<close>
  1034 
  1035 lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a"
  1036   using pos_eucl_rel_int_mult_2 [OF _ eucl_rel_int]
  1037   by (rule div_int_unique)
  1038 
  1039 lemma neg_zdiv_mult_2:
  1040   assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"
  1041   using neg_eucl_rel_int_mult_2 [OF A eucl_rel_int]
  1042   by (rule div_int_unique)
  1043 
  1044 (* FIXME: add rules for negative numerals *)
  1045 lemma zdiv_numeral_Bit0 [simp]:
  1046   "numeral (Num.Bit0 v) div numeral (Num.Bit0 w) =
  1047     numeral v div (numeral w :: int)"
  1048   unfolding numeral.simps unfolding mult_2 [symmetric]
  1049   by (rule div_mult_mult1, simp)
  1050 
  1051 lemma zdiv_numeral_Bit1 [simp]:
  1052   "numeral (Num.Bit1 v) div numeral (Num.Bit0 w) =
  1053     (numeral v div (numeral w :: int))"
  1054   unfolding numeral.simps
  1055   unfolding mult_2 [symmetric] add.commute [of _ 1]
  1056   by (rule pos_zdiv_mult_2, simp)
  1057 
  1058 lemma pos_zmod_mult_2:
  1059   fixes a b :: int
  1060   assumes "0 \<le> a"
  1061   shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)"
  1062   using pos_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
  1063   by (rule mod_int_unique)
  1064 
  1065 lemma neg_zmod_mult_2:
  1066   fixes a b :: int
  1067   assumes "a \<le> 0"
  1068   shows "(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1"
  1069   using neg_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
  1070   by (rule mod_int_unique)
  1071 
  1072 (* FIXME: add rules for negative numerals *)
  1073 lemma zmod_numeral_Bit0 [simp]:
  1074   "numeral (Num.Bit0 v) mod numeral (Num.Bit0 w) =
  1075     (2::int) * (numeral v mod numeral w)"
  1076   unfolding numeral_Bit0 [of v] numeral_Bit0 [of w]
  1077   unfolding mult_2 [symmetric] by (rule mod_mult_mult1)
  1078 
  1079 lemma zmod_numeral_Bit1 [simp]:
  1080   "numeral (Num.Bit1 v) mod numeral (Num.Bit0 w) =
  1081     2 * (numeral v mod numeral w) + (1::int)"
  1082   unfolding numeral_Bit1 [of v] numeral_Bit0 [of w]
  1083   unfolding mult_2 [symmetric] add.commute [of _ 1]
  1084   by (rule pos_zmod_mult_2, simp)
  1085 
  1086 lemma zdiv_eq_0_iff:
  1087  "(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")
  1088 proof
  1089   assume ?L
  1090   have "?L \<longrightarrow> ?R" by (rule split_zdiv[THEN iffD2]) simp
  1091   with \<open>?L\<close> show ?R by blast
  1092 next
  1093   assume ?R thus ?L
  1094     by(auto simp: div_pos_pos_trivial div_neg_neg_trivial)
  1095 qed
  1096 
  1097 lemma zmod_trival_iff:
  1098   fixes i k :: int
  1099   shows "i mod k = i \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i"
  1100 proof -
  1101   have "i mod k = i \<longleftrightarrow> i div k = 0"
  1102     by safe (insert div_mult_mod_eq [of i k], auto)
  1103   with zdiv_eq_0_iff
  1104   show ?thesis
  1105     by simp
  1106 qed
  1107 
  1108   
  1109 subsubsection \<open>Quotients of Signs\<close>
  1110 
  1111 lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"
  1112 by (simp add: divide_int_def)
  1113 
  1114 lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
  1115 by (simp add: modulo_int_def)
  1116 
  1117 lemma div_neg_pos_less0: "[| a < (0::int);  0 < b |] ==> a div b < 0"
  1118 apply (subgoal_tac "a div b \<le> -1", force)
  1119 apply (rule order_trans)
  1120 apply (rule_tac a' = "-1" in zdiv_mono1)
  1121 apply (auto simp add: div_eq_minus1)
  1122 done
  1123 
  1124 lemma div_nonneg_neg_le0: "[| (0::int) \<le> a; b < 0 |] ==> a div b \<le> 0"
  1125 by (drule zdiv_mono1_neg, auto)
  1126 
  1127 lemma div_nonpos_pos_le0: "[| (a::int) \<le> 0; b > 0 |] ==> a div b \<le> 0"
  1128 by (drule zdiv_mono1, auto)
  1129 
  1130 text\<open>Now for some equivalences of the form \<open>a div b >=< 0 \<longleftrightarrow> \<dots>\<close>
  1131 conditional upon the sign of \<open>a\<close> or \<open>b\<close>. There are many more.
  1132 They should all be simp rules unless that causes too much search.\<close>
  1133 
  1134 lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)"
  1135 apply auto
  1136 apply (drule_tac [2] zdiv_mono1)
  1137 apply (auto simp add: linorder_neq_iff)
  1138 apply (simp (no_asm_use) add: linorder_not_less [symmetric])
  1139 apply (blast intro: div_neg_pos_less0)
  1140 done
  1141 
  1142 lemma pos_imp_zdiv_pos_iff:
  1143   "0<k \<Longrightarrow> 0 < (i::int) div k \<longleftrightarrow> k \<le> i"
  1144 using pos_imp_zdiv_nonneg_iff[of k i] zdiv_eq_0_iff[of i k]
  1145 by arith
  1146 
  1147 lemma neg_imp_zdiv_nonneg_iff:
  1148   "b < (0::int) ==> (0 \<le> a div b) = (a \<le> (0::int))"
  1149 apply (subst div_minus_minus [symmetric])
  1150 apply (subst pos_imp_zdiv_nonneg_iff, auto)
  1151 done
  1152 
  1153 (*But not (a div b \<le> 0 iff a\<le>0); consider a=1, b=2 when a div b = 0.*)
  1154 lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)"
  1155 by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff)
  1156 
  1157 (*Again the law fails for \<le>: consider a = -1, b = -2 when a div b = 0*)
  1158 lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)"
  1159 by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)
  1160 
  1161 lemma nonneg1_imp_zdiv_pos_iff:
  1162   "(0::int) <= a \<Longrightarrow> (a div b > 0) = (a >= b & b>0)"
  1163 apply rule
  1164  apply rule
  1165   using div_pos_pos_trivial[of a b]apply arith
  1166  apply(cases "b=0")apply simp
  1167  using div_nonneg_neg_le0[of a b]apply arith
  1168 using int_one_le_iff_zero_less[of "a div b"] zdiv_mono1[of b a b]apply simp
  1169 done
  1170 
  1171 lemma zmod_le_nonneg_dividend: "(m::int) \<ge> 0 ==> m mod k \<le> m"
  1172 apply (rule split_zmod[THEN iffD2])
  1173 apply(fastforce dest: q_pos_lemma intro: split_mult_pos_le)
  1174 done
  1175 
  1176 
  1177 subsubsection \<open>Computation of Division and Remainder\<close>
  1178 
  1179 instantiation int :: unique_euclidean_semiring_numeral
  1180 begin
  1181 
  1182 definition divmod_int :: "num \<Rightarrow> num \<Rightarrow> int \<times> int"
  1183 where
  1184   "divmod_int m n = (numeral m div numeral n, numeral m mod numeral n)"
  1185 
  1186 definition divmod_step_int :: "num \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int"
  1187 where
  1188   "divmod_step_int l qr = (let (q, r) = qr
  1189     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
  1190     else (2 * q, r))"
  1191 
  1192 instance
  1193   by standard (auto intro: zmod_le_nonneg_dividend simp add: divmod_int_def divmod_step_int_def
  1194     pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial zmod_zmult2_eq zdiv_zmult2_eq)
  1195 
  1196 end
  1197 
  1198 declare divmod_algorithm_code [where ?'a = int, code]
  1199 
  1200 context
  1201 begin
  1202   
  1203 qualified definition adjust_div :: "int \<times> int \<Rightarrow> int"
  1204 where
  1205   "adjust_div qr = (let (q, r) = qr in q + of_bool (r \<noteq> 0))"
  1206 
  1207 qualified lemma adjust_div_eq [simp, code]:
  1208   "adjust_div (q, r) = q + of_bool (r \<noteq> 0)"
  1209   by (simp add: adjust_div_def)
  1210 
  1211 qualified definition adjust_mod :: "int \<Rightarrow> int \<Rightarrow> int"
  1212 where
  1213   [simp]: "adjust_mod l r = (if r = 0 then 0 else l - r)"
  1214 
  1215 lemma minus_numeral_div_numeral [simp]:
  1216   "- numeral m div numeral n = - (adjust_div (divmod m n) :: int)"
  1217 proof -
  1218   have "int (fst (divmod m n)) = fst (divmod m n)"
  1219     by (simp only: fst_divmod divide_int_def) auto
  1220   then show ?thesis
  1221     by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
  1222 qed
  1223 
  1224 lemma minus_numeral_mod_numeral [simp]:
  1225   "- numeral m mod numeral n = adjust_mod (numeral n) (snd (divmod m n) :: int)"
  1226 proof -
  1227   have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
  1228     using that by (simp only: snd_divmod modulo_int_def) auto
  1229   then show ?thesis
  1230     by (auto simp add: split_def Let_def adjust_div_def divides_aux_def modulo_int_def)
  1231 qed
  1232 
  1233 lemma numeral_div_minus_numeral [simp]:
  1234   "numeral m div - numeral n = - (adjust_div (divmod m n) :: int)"
  1235 proof -
  1236   have "int (fst (divmod m n)) = fst (divmod m n)"
  1237     by (simp only: fst_divmod divide_int_def) auto
  1238   then show ?thesis
  1239     by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
  1240 qed
  1241   
  1242 lemma numeral_mod_minus_numeral [simp]:
  1243   "numeral m mod - numeral n = - adjust_mod (numeral n) (snd (divmod m n) :: int)"
  1244 proof -
  1245   have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
  1246     using that by (simp only: snd_divmod modulo_int_def) auto
  1247   then show ?thesis
  1248     by (auto simp add: split_def Let_def adjust_div_def divides_aux_def modulo_int_def)
  1249 qed
  1250 
  1251 lemma minus_one_div_numeral [simp]:
  1252   "- 1 div numeral n = - (adjust_div (divmod Num.One n) :: int)"
  1253   using minus_numeral_div_numeral [of Num.One n] by simp  
  1254 
  1255 lemma minus_one_mod_numeral [simp]:
  1256   "- 1 mod numeral n = adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
  1257   using minus_numeral_mod_numeral [of Num.One n] by simp
  1258 
  1259 lemma one_div_minus_numeral [simp]:
  1260   "1 div - numeral n = - (adjust_div (divmod Num.One n) :: int)"
  1261   using numeral_div_minus_numeral [of Num.One n] by simp
  1262   
  1263 lemma one_mod_minus_numeral [simp]:
  1264   "1 mod - numeral n = - adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
  1265   using numeral_mod_minus_numeral [of Num.One n] by simp
  1266 
  1267 end
  1268 
  1269 
  1270 subsubsection \<open>Further properties\<close>
  1271 
  1272 text \<open>Simplify expresions in which div and mod combine numerical constants\<close>
  1273 
  1274 lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
  1275   by (rule div_int_unique [of a b q r]) (simp add: eucl_rel_int_iff)
  1276 
  1277 lemma int_div_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a div b = q"
  1278   by (rule div_int_unique [of a b q r],
  1279     simp add: eucl_rel_int_iff)
  1280 
  1281 lemma int_mod_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a mod b = r"
  1282   by (rule mod_int_unique [of a b q r],
  1283     simp add: eucl_rel_int_iff)
  1284 
  1285 lemma int_mod_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a mod b = r"
  1286   by (rule mod_int_unique [of a b q r],
  1287     simp add: eucl_rel_int_iff)
  1288 
  1289 lemma abs_div: "(y::int) dvd x \<Longrightarrow> \<bar>x div y\<bar> = \<bar>x\<bar> div \<bar>y\<bar>"
  1290 by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
  1291 
  1292 text\<open>Suggested by Matthias Daum\<close>
  1293 lemma int_power_div_base:
  1294      "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"
  1295 apply (subgoal_tac "k ^ m = k ^ ((m - Suc 0) + Suc 0)")
  1296  apply (erule ssubst)
  1297  apply (simp only: power_add)
  1298  apply simp_all
  1299 done
  1300 
  1301 text \<open>Distributive laws for function \<open>nat\<close>.\<close>
  1302 
  1303 lemma nat_div_distrib: "0 \<le> x \<Longrightarrow> nat (x div y) = nat x div nat y"
  1304 apply (rule linorder_cases [of y 0])
  1305 apply (simp add: div_nonneg_neg_le0)
  1306 apply simp
  1307 apply (simp add: nat_eq_iff pos_imp_zdiv_nonneg_iff zdiv_int)
  1308 done
  1309 
  1310 (*Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't*)
  1311 lemma nat_mod_distrib:
  1312   "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x mod y) = nat x mod nat y"
  1313 apply (case_tac "y = 0", simp)
  1314 apply (simp add: nat_eq_iff zmod_int)
  1315 done
  1316 
  1317 text  \<open>transfer setup\<close>
  1318 
  1319 lemma transfer_nat_int_functions:
  1320     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
  1321     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
  1322   by (auto simp add: nat_div_distrib nat_mod_distrib)
  1323 
  1324 lemma transfer_nat_int_function_closures:
  1325     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
  1326     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
  1327   apply (cases "y = 0")
  1328   apply (auto simp add: pos_imp_zdiv_nonneg_iff)
  1329   apply (cases "y = 0")
  1330   apply auto
  1331 done
  1332 
  1333 declare transfer_morphism_nat_int [transfer add return:
  1334   transfer_nat_int_functions
  1335   transfer_nat_int_function_closures
  1336 ]
  1337 
  1338 lemma transfer_int_nat_functions:
  1339     "(int x) div (int y) = int (x div y)"
  1340     "(int x) mod (int y) = int (x mod y)"
  1341   by (auto simp add: zdiv_int zmod_int)
  1342 
  1343 lemma transfer_int_nat_function_closures:
  1344     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
  1345     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
  1346   by (simp_all only: is_nat_def transfer_nat_int_function_closures)
  1347 
  1348 declare transfer_morphism_int_nat [transfer add return:
  1349   transfer_int_nat_functions
  1350   transfer_int_nat_function_closures
  1351 ]
  1352 
  1353 text\<open>Suggested by Matthias Daum\<close>
  1354 lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
  1355 apply (subgoal_tac "nat x div nat k < nat x")
  1356  apply (simp add: nat_div_distrib [symmetric])
  1357 apply (rule div_less_dividend, simp_all)
  1358 done
  1359 
  1360 lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \<le> x"
  1361   shows "\<exists>q. x = y + n * q"
  1362 proof-
  1363   from xy have th: "int x - int y = int (x - y)" by simp
  1364   from xyn have "int x mod int n = int y mod int n"
  1365     by (simp add: zmod_int [symmetric])
  1366   hence "int n dvd int x - int y" by (simp only: mod_eq_dvd_iff [symmetric])
  1367   hence "n dvd x - y" by (simp add: th zdvd_int)
  1368   then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith
  1369 qed
  1370 
  1371 lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)"
  1372   (is "?lhs = ?rhs")
  1373 proof
  1374   assume H: "x mod n = y mod n"
  1375   {assume xy: "x \<le> y"
  1376     from H have th: "y mod n = x mod n" by simp
  1377     from nat_mod_eq_lemma[OF th xy] have ?rhs
  1378       apply clarify  apply (rule_tac x="q" in exI) by (rule exI[where x="0"], simp)}
  1379   moreover
  1380   {assume xy: "y \<le> x"
  1381     from nat_mod_eq_lemma[OF H xy] have ?rhs
  1382       apply clarify  apply (rule_tac x="0" in exI) by (rule_tac x="q" in exI, simp)}
  1383   ultimately  show ?rhs using linear[of x y] by blast
  1384 next
  1385   assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast
  1386   hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp
  1387   thus  ?lhs by simp
  1388 qed
  1389 
  1390 
  1391 subsubsection \<open>Dedicated simproc for calculation\<close>
  1392 
  1393 text \<open>
  1394   There is space for improvement here: the calculation itself
  1395   could be carried out outside the logic, and a generic simproc
  1396   (simplifier setup) for generic calculation would be helpful. 
  1397 \<close>
  1398 
  1399 simproc_setup numeral_divmod
  1400   ("0 div 0 :: 'a :: unique_euclidean_semiring_numeral" | "0 mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
  1401    "0 div 1 :: 'a :: unique_euclidean_semiring_numeral" | "0 mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
  1402    "0 div - 1 :: int" | "0 mod - 1 :: int" |
  1403    "0 div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "0 mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
  1404    "0 div - numeral b :: int" | "0 mod - numeral b :: int" |
  1405    "1 div 0 :: 'a :: unique_euclidean_semiring_numeral" | "1 mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
  1406    "1 div 1 :: 'a :: unique_euclidean_semiring_numeral" | "1 mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
  1407    "1 div - 1 :: int" | "1 mod - 1 :: int" |
  1408    "1 div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "1 mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
  1409    "1 div - numeral b :: int" |"1 mod - numeral b :: int" |
  1410    "- 1 div 0 :: int" | "- 1 mod 0 :: int" | "- 1 div 1 :: int" | "- 1 mod 1 :: int" |
  1411    "- 1 div - 1 :: int" | "- 1 mod - 1 :: int" | "- 1 div numeral b :: int" | "- 1 mod numeral b :: int" |
  1412    "- 1 div - numeral b :: int" | "- 1 mod - numeral b :: int" |
  1413    "numeral a div 0 :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
  1414    "numeral a div 1 :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
  1415    "numeral a div - 1 :: int" | "numeral a mod - 1 :: int" |
  1416    "numeral a div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
  1417    "numeral a div - numeral b :: int" | "numeral a mod - numeral b :: int" |
  1418    "- numeral a div 0 :: int" | "- numeral a mod 0 :: int" |
  1419    "- numeral a div 1 :: int" | "- numeral a mod 1 :: int" |
  1420    "- numeral a div - 1 :: int" | "- numeral a mod - 1 :: int" |
  1421    "- numeral a div numeral b :: int" | "- numeral a mod numeral b :: int" |
  1422    "- numeral a div - numeral b :: int" | "- numeral a mod - numeral b :: int") =
  1423 \<open> let
  1424     val if_cong = the (Code.get_case_cong @{theory} @{const_name If});
  1425     fun successful_rewrite ctxt ct =
  1426       let
  1427         val thm = Simplifier.rewrite ctxt ct
  1428       in if Thm.is_reflexive thm then NONE else SOME thm end;
  1429   in fn phi =>
  1430     let
  1431       val simps = Morphism.fact phi (@{thms div_0 mod_0 div_by_0 mod_by_0 div_by_1 mod_by_1
  1432         one_div_numeral one_mod_numeral minus_one_div_numeral minus_one_mod_numeral
  1433         one_div_minus_numeral one_mod_minus_numeral
  1434         numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral
  1435         numeral_div_minus_numeral numeral_mod_minus_numeral
  1436         div_minus_minus mod_minus_minus Divides.adjust_div_eq of_bool_eq one_neq_zero
  1437         numeral_neq_zero neg_equal_0_iff_equal arith_simps arith_special divmod_trivial
  1438         divmod_cancel divmod_steps divmod_step_eq fst_conv snd_conv numeral_One
  1439         case_prod_beta rel_simps Divides.adjust_mod_def div_minus1_right mod_minus1_right
  1440         minus_minus numeral_times_numeral mult_zero_right mult_1_right}
  1441         @ [@{lemma "0 = 0 \<longleftrightarrow> True" by simp}]);
  1442       fun prepare_simpset ctxt = HOL_ss |> Simplifier.simpset_map ctxt
  1443         (Simplifier.add_cong if_cong #> fold Simplifier.add_simp simps)
  1444     in fn ctxt => successful_rewrite (Simplifier.put_simpset (prepare_simpset ctxt) ctxt) end
  1445   end;
  1446 \<close>
  1447 
  1448 
  1449 subsubsection \<open>Code generation\<close>
  1450 
  1451 lemma [code]:
  1452   fixes k :: int
  1453   shows 
  1454     "k div 0 = 0"
  1455     "k mod 0 = k"
  1456     "0 div k = 0"
  1457     "0 mod k = 0"
  1458     "k div Int.Pos Num.One = k"
  1459     "k mod Int.Pos Num.One = 0"
  1460     "k div Int.Neg Num.One = - k"
  1461     "k mod Int.Neg Num.One = 0"
  1462     "Int.Pos m div Int.Pos n = (fst (divmod m n) :: int)"
  1463     "Int.Pos m mod Int.Pos n = (snd (divmod m n) :: int)"
  1464     "Int.Neg m div Int.Pos n = - (Divides.adjust_div (divmod m n) :: int)"
  1465     "Int.Neg m mod Int.Pos n = Divides.adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
  1466     "Int.Pos m div Int.Neg n = - (Divides.adjust_div (divmod m n) :: int)"
  1467     "Int.Pos m mod Int.Neg n = - Divides.adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
  1468     "Int.Neg m div Int.Neg n = (fst (divmod m n) :: int)"
  1469     "Int.Neg m mod Int.Neg n = - (snd (divmod m n) :: int)"
  1470   by simp_all
  1471 
  1472 code_identifier
  1473   code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  1474 
  1475 lemma dvd_eq_mod_eq_0_numeral:
  1476   "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semidom_modulo)"
  1477   by (fact dvd_eq_mod_eq_0)
  1478 
  1479 declare minus_div_mult_eq_mod [symmetric, nitpick_unfold]
  1480 
  1481 
  1482 subsubsection \<open>Lemmas of doubtful value\<close>
  1483 
  1484 lemma mod_mult_self3':
  1485   "Suc (k * n + m) mod n = Suc m mod n"
  1486   by (fact Suc_mod_mult_self3)
  1487 
  1488 lemma mod_Suc_eq_Suc_mod:
  1489   "Suc m mod n = Suc (m mod n) mod n"
  1490   by (simp add: mod_simps)
  1491 
  1492 lemma div_geq:
  1493   "m div n = Suc ((m - n) div n)" if "0 < n" and " \<not> m < n" for m n :: nat
  1494   by (rule le_div_geq) (use that in \<open>simp_all add: not_less\<close>)
  1495 
  1496 lemma mod_geq:
  1497   "m mod n = (m - n) mod n" if "\<not> m < n" for m n :: nat
  1498   by (rule le_mod_geq) (use that in \<open>simp add: not_less\<close>)
  1499 
  1500 lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
  1501   by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
  1502 
  1503 lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
  1504 
  1505 (*Loses information, namely we also have r<d provided d is nonzero*)
  1506 lemma mod_eqD:
  1507   fixes m d r q :: nat
  1508   assumes "m mod d = r"
  1509   shows "\<exists>q. m = r + q * d"
  1510 proof -
  1511   from div_mult_mod_eq obtain q where "q * d + m mod d = m" by blast
  1512   with assms have "m = r + q * d" by simp
  1513   then show ?thesis ..
  1514 qed
  1515 
  1516 end