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