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