src/HOL/IntDiv.thy
 author haftmann Thu Oct 29 22:13:09 2009 +0100 (2009-10-29) changeset 33340 a165b97f3658 parent 33318 ddd97d9dfbfb permissions -rw-r--r--
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
 wenzelm@23164  1 (* Title: HOL/IntDiv.thy  wenzelm@23164  2  Author: Lawrence C Paulson, Cambridge University Computer Laboratory  wenzelm@23164  3  Copyright 1999 University of Cambridge  wenzelm@23164  4 *)  wenzelm@23164  5 haftmann@29651  6 header{* The Division Operators div and mod *}  wenzelm@23164  7 wenzelm@23164  8 theory IntDiv  haftmann@25919  9 imports Int Divides FunDef  haftmann@33340  10 uses  haftmann@33340  11  "~~/src/Provers/Arith/assoc_fold.ML"  haftmann@33340  12  "~~/src/Provers/Arith/cancel_numerals.ML"  haftmann@33340  13  "~~/src/Provers/Arith/combine_numerals.ML"  haftmann@33340  14  "~~/src/Provers/Arith/cancel_numeral_factor.ML"  haftmann@33340  15  "~~/src/Provers/Arith/extract_common_term.ML"  haftmann@33340  16  ("Tools/numeral_simprocs.ML")  haftmann@33340  17  ("Tools/nat_numeral_simprocs.ML")  wenzelm@23164  18 begin  wenzelm@23164  19 haftmann@33340  20 definition divmod_int_rel :: "int \ int \ int \ int \ bool" where  wenzelm@23164  21  --{*definition of quotient and remainder*}  haftmann@33340  22  [code]: "divmod_int_rel a b = ($$q, r). a = b * q + r \  haftmann@29651  23  (if 0 < b then 0 \ r \ r < b else b < r \ r \ 0))"  wenzelm@23164  24 haftmann@29651  25 definition adjust :: "int \ int \ int \ int \ int" where  wenzelm@23164  26  --{*for the division algorithm*}  haftmann@29651  27  [code]: "adjust b = (\(q, r). if 0 \ r - b then (2 * q + 1, r - b)  haftmann@29651  28  else (2 * q, r))"  wenzelm@23164  29 wenzelm@23164  30 text{*algorithm for the case @{text "a\0, b>0"}*}  haftmann@29651  31 function posDivAlg :: "int \ int \ int \ int" where  haftmann@29651  32  "posDivAlg a b = (if a < b \ b \ 0 then (0, a)  haftmann@29651  33  else adjust b (posDivAlg a (2 * b)))"  wenzelm@23164  34 by auto  haftmann@33340  35 termination by (relation "measure (\(a, b). nat (a - b + 1))")  haftmann@33340  36  (auto simp add: mult_2)  wenzelm@23164  37 wenzelm@23164  38 text{*algorithm for the case @{text "a<0, b>0"}*}  haftmann@29651  39 function negDivAlg :: "int \ int \ int \ int" where  haftmann@29651  40  "negDivAlg a b = (if 0 \a + b \ b \ 0 then (-1, a + b)  haftmann@29651  41  else adjust b (negDivAlg a (2 * b)))"  wenzelm@23164  42 by auto  haftmann@33340  43 termination by (relation "measure (\(a, b). nat (- a - b))")  haftmann@33340  44  (auto simp add: mult_2)  wenzelm@23164  45 wenzelm@23164  46 text{*algorithm for the general case @{term "b\0"}*}  haftmann@29651  47 definition negateSnd :: "int \ int \ int \ int" where  haftmann@32069  48  [code_unfold]: "negateSnd = apsnd uminus"  wenzelm@23164  49 haftmann@33340  50 definition divmod_int :: "int \ int \ int \ int" where  wenzelm@23164  51  --{*The full division algorithm considers all possible signs for a, b  wenzelm@23164  52  including the special case @{text "a=0, b<0"} because  wenzelm@23164  53  @{term negDivAlg} requires @{term "a<0"}.*}  haftmann@33340  54  "divmod_int a b = (if 0 \ a then if 0 \ b then posDivAlg a b  haftmann@29651  55  else if a = 0 then (0, 0)  wenzelm@23164  56  else negateSnd (negDivAlg (-a) (-b))  wenzelm@23164  57  else  haftmann@29651  58  if 0 < b then negDivAlg a b  haftmann@29651  59  else negateSnd (posDivAlg (-a) (-b)))"  wenzelm@23164  60 haftmann@25571  61 instantiation int :: Divides.div  haftmann@25571  62 begin  haftmann@25571  63 haftmann@25571  64 definition  haftmann@33340  65  "a div b = fst (divmod_int a b)"  haftmann@25571  66 haftmann@25571  67 definition  haftmann@33340  68  "a mod b = snd (divmod_int a b)"  haftmann@25571  69 haftmann@25571  70 instance ..  haftmann@25571  71 haftmann@25571  72 end  wenzelm@23164  73 haftmann@33340  74 lemma divmod_int_mod_div:  haftmann@33340  75  "divmod_int p q = (p div q, p mod q)"  haftmann@33340  76  by (auto simp add: div_int_def mod_int_def)  wenzelm@23164  77 wenzelm@23164  78 text{*  wenzelm@23164  79 Here is the division algorithm in ML:  wenzelm@23164  80 wenzelm@23164  81 \begin{verbatim}  wenzelm@23164  82  fun posDivAlg (a,b) =  wenzelm@23164  83  if ar-b then (2*q+1, r-b) else (2*q, r)  wenzelm@32960  86  end  wenzelm@23164  87 wenzelm@23164  88  fun negDivAlg (a,b) =  wenzelm@23164  89  if 0\a+b then (~1,a+b)  wenzelm@23164  90  else let val (q,r) = negDivAlg(a, 2*b)  wenzelm@32960  91  in if 0\r-b then (2*q+1, r-b) else (2*q, r)  wenzelm@32960  92  end;  wenzelm@23164  93 wenzelm@23164  94  fun negateSnd (q,r:int) = (q,~r);  wenzelm@23164  95 haftmann@29651  96  fun divmod (a,b) = if 0\a then  wenzelm@32960  97  if b>0 then posDivAlg (a,b)  wenzelm@32960  98  else if a=0 then (0,0)  wenzelm@32960  99  else negateSnd (negDivAlg (~a,~b))  wenzelm@32960  100  else  wenzelm@32960  101  if 0 b*q + r; 0 \ r'; r' < b; r < b |]  wenzelm@23164  112  ==> q' \ (q::int)"  wenzelm@23164  113 apply (subgoal_tac "r' + b * (q'-q) \ r")  wenzelm@23164  114  prefer 2 apply (simp add: right_diff_distrib)  wenzelm@23164  115 apply (subgoal_tac "0 < b * (1 + q - q') ")  wenzelm@23164  116 apply (erule_tac [2] order_le_less_trans)  wenzelm@23164  117  prefer 2 apply (simp add: right_diff_distrib right_distrib)  wenzelm@23164  118 apply (subgoal_tac "b * q' < b * (1 + q) ")  wenzelm@23164  119  prefer 2 apply (simp add: right_diff_distrib right_distrib)  wenzelm@23164  120 apply (simp add: mult_less_cancel_left)  wenzelm@23164  121 done  wenzelm@23164  122 wenzelm@23164  123 lemma unique_quotient_lemma_neg:  wenzelm@23164  124  "[| b*q' + r' \ b*q + r; r \ 0; b < r; b < r' |]  wenzelm@23164  125  ==> q \ (q'::int)"  wenzelm@23164  126 by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma,  wenzelm@23164  127  auto)  wenzelm@23164  128 wenzelm@23164  129 lemma unique_quotient:  haftmann@33340  130  "[| divmod_int_rel a b (q, r); divmod_int_rel a b (q', r'); b \ 0 |]  wenzelm@23164  131  ==> q = q'"  haftmann@33340  132 apply (simp add: divmod_int_rel_def linorder_neq_iff split: split_if_asm)  wenzelm@23164  133 apply (blast intro: order_antisym  wenzelm@23164  134  dest: order_eq_refl [THEN unique_quotient_lemma]  wenzelm@23164  135  order_eq_refl [THEN unique_quotient_lemma_neg] sym)+  wenzelm@23164  136 done  wenzelm@23164  137 wenzelm@23164  138 wenzelm@23164  139 lemma unique_remainder:  haftmann@33340  140  "[| divmod_int_rel a b (q, r); divmod_int_rel a b (q', r'); b \ 0 |]  wenzelm@23164  141  ==> r = r'"  wenzelm@23164  142 apply (subgoal_tac "q = q'")  haftmann@33340  143  apply (simp add: divmod_int_rel_def)  wenzelm@23164  144 apply (blast intro: unique_quotient)  wenzelm@23164  145 done  wenzelm@23164  146 wenzelm@23164  147 wenzelm@23164  148 subsection{*Correctness of @{term posDivAlg}, the Algorithm for Non-Negative Dividends*}  wenzelm@23164  149 wenzelm@23164  150 text{*And positive divisors*}  wenzelm@23164  151 wenzelm@23164  152 lemma adjust_eq [simp]:  wenzelm@23164  153  "adjust b (q,r) =  wenzelm@23164  154  (let diff = r-b in  wenzelm@32960  155  if 0 \ diff then (2*q + 1, diff)  wenzelm@23164  156  else (2*q, r))"  wenzelm@23164  157 by (simp add: Let_def adjust_def)  wenzelm@23164  158 wenzelm@23164  159 declare posDivAlg.simps [simp del]  wenzelm@23164  160 wenzelm@23164  161 text{*use with a simproc to avoid repeatedly proving the premise*}  wenzelm@23164  162 lemma posDivAlg_eqn:  wenzelm@23164  163  "0 < b ==>  wenzelm@23164  164  posDivAlg a b = (if a a" and "0 < b"  haftmann@33340  170  shows "divmod_int_rel a b (posDivAlg a b)"  wenzelm@23164  171 using prems apply (induct a b rule: posDivAlg.induct)  wenzelm@23164  172 apply auto  haftmann@33340  173 apply (simp add: divmod_int_rel_def)  wenzelm@23164  174 apply (subst posDivAlg_eqn, simp add: right_distrib)  wenzelm@23164  175 apply (case_tac "a < b")  wenzelm@23164  176 apply simp_all  wenzelm@23164  177 apply (erule splitE)  haftmann@33340  178 apply (auto simp add: right_distrib Let_def mult_ac mult_2_right)  wenzelm@23164  179 done  wenzelm@23164  180 wenzelm@23164  181 wenzelm@23164  182 subsection{*Correctness of @{term negDivAlg}, the Algorithm for Negative Dividends*}  wenzelm@23164  183 wenzelm@23164  184 text{*And positive divisors*}  wenzelm@23164  185 wenzelm@23164  186 declare negDivAlg.simps [simp del]  wenzelm@23164  187 wenzelm@23164  188 text{*use with a simproc to avoid repeatedly proving the premise*}  wenzelm@23164  189 lemma negDivAlg_eqn:  wenzelm@23164  190  "0 < b ==>  wenzelm@23164  191  negDivAlg a b =  wenzelm@23164  192  (if 0\a+b then (-1,a+b) else adjust b (negDivAlg a (2*b)))"  wenzelm@23164  193 by (rule negDivAlg.simps [THEN trans], simp)  wenzelm@23164  194 wenzelm@23164  195 (*Correctness of negDivAlg: it computes quotients correctly  wenzelm@23164  196  It doesn't work if a=0 because the 0/b equals 0, not -1*)  wenzelm@23164  197 lemma negDivAlg_correct:  wenzelm@23164  198  assumes "a < 0" and "b > 0"  haftmann@33340  199  shows "divmod_int_rel a b (negDivAlg a b)"  wenzelm@23164  200 using prems apply (induct a b rule: negDivAlg.induct)  wenzelm@23164  201 apply (auto simp add: linorder_not_le)  haftmann@33340  202 apply (simp add: divmod_int_rel_def)  wenzelm@23164  203 apply (subst negDivAlg_eqn, assumption)  wenzelm@23164  204 apply (case_tac "a + b < (0\int)")  wenzelm@23164  205 apply simp_all  wenzelm@23164  206 apply (erule splitE)  haftmann@33340  207 apply (auto simp add: right_distrib Let_def mult_ac mult_2_right)  wenzelm@23164  208 done  wenzelm@23164  209 wenzelm@23164  210 wenzelm@23164  211 subsection{*Existence Shown by Proving the Division Algorithm to be Correct*}  wenzelm@23164  212 wenzelm@23164  213 (*the case a=0*)  haftmann@33340  214 lemma divmod_int_rel_0: "b \ 0 ==> divmod_int_rel 0 b (0, 0)"  haftmann@33340  215 by (auto simp add: divmod_int_rel_def linorder_neq_iff)  wenzelm@23164  216 wenzelm@23164  217 lemma posDivAlg_0 [simp]: "posDivAlg 0 b = (0, 0)"  wenzelm@23164  218 by (subst posDivAlg.simps, auto)  wenzelm@23164  219 wenzelm@23164  220 lemma negDivAlg_minus1 [simp]: "negDivAlg -1 b = (-1, b - 1)"  wenzelm@23164  221 by (subst negDivAlg.simps, auto)  wenzelm@23164  222 wenzelm@23164  223 lemma negateSnd_eq [simp]: "negateSnd(q,r) = (q,-r)"  wenzelm@23164  224 by (simp add: negateSnd_def)  wenzelm@23164  225 haftmann@33340  226 lemma divmod_int_rel_neg: "divmod_int_rel (-a) (-b) qr ==> divmod_int_rel a b (negateSnd qr)"  haftmann@33340  227 by (auto simp add: split_ifs divmod_int_rel_def)  wenzelm@23164  228 haftmann@33340  229 lemma divmod_int_correct: "b \ 0 ==> divmod_int_rel a b (divmod_int a b)"  haftmann@33340  230 by (force simp add: linorder_neq_iff divmod_int_rel_0 divmod_int_def divmod_int_rel_neg  wenzelm@23164  231  posDivAlg_correct negDivAlg_correct)  wenzelm@23164  232 wenzelm@23164  233 text{*Arbitrary definitions for division by zero. Useful to simplify  wenzelm@23164  234  certain equations.*}  wenzelm@23164  235 wenzelm@23164  236 lemma DIVISION_BY_ZERO [simp]: "a div (0::int) = 0 & a mod (0::int) = a"  haftmann@33340  237 by (simp add: div_int_def mod_int_def divmod_int_def posDivAlg.simps)  wenzelm@23164  238 wenzelm@23164  239 wenzelm@23164  240 text{*Basic laws about division and remainder*}  wenzelm@23164  241 wenzelm@23164  242 lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"  wenzelm@23164  243 apply (case_tac "b = 0", simp)  haftmann@33340  244 apply (cut_tac a = a and b = b in divmod_int_correct)  haftmann@33340  245 apply (auto simp add: divmod_int_rel_def div_int_def mod_int_def)  wenzelm@23164  246 done  wenzelm@23164  247 wenzelm@23164  248 lemma zdiv_zmod_equality: "(b * (a div b) + (a mod b)) + k = (a::int)+k"  wenzelm@23164  249 by(simp add: zmod_zdiv_equality[symmetric])  wenzelm@23164  250 wenzelm@23164  251 lemma zdiv_zmod_equality2: "((a div b) * b + (a mod b)) + k = (a::int)+k"  wenzelm@23164  252 by(simp add: mult_commute zmod_zdiv_equality[symmetric])  wenzelm@23164  253 wenzelm@23164  254 text {* Tool setup *}  wenzelm@23164  255 wenzelm@26480  256 ML {*  haftmann@30934  257 local  wenzelm@23164  258 haftmann@33340  259 fun mk_number T n = HOLogic.number_of_const T  HOLogic.mk_numeral n;  haftmann@33340  260 haftmann@33340  261 fun find_first_numeral past (t::terms) =  haftmann@33340  262  ((snd (HOLogic.dest_number t), rev past @ terms)  haftmann@33340  263  handle TERM _ => find_first_numeral (t::past) terms)  haftmann@33340  264  | find_first_numeral past [] = raise TERM("find_first_numeral", []);  haftmann@33340  265 haftmann@33340  266 val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};  haftmann@33340  267 haftmann@33340  268 fun mk_minus t =  haftmann@33340  269  let val T = Term.fastype_of t  haftmann@33340  270  in Const (@{const_name HOL.uminus}, T --> T)  t end;  haftmann@33340  271 haftmann@33340  272 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)  haftmann@33340  273 fun mk_sum T [] = mk_number T 0  haftmann@33340  274  | mk_sum T [t,u] = mk_plus (t, u)  haftmann@33340  275  | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);  haftmann@33340  276 haftmann@33340  277 (*this version ALWAYS includes a trailing zero*)  haftmann@33340  278 fun long_mk_sum T [] = mk_number T 0  haftmann@33340  279  | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);  haftmann@33340  280 haftmann@33340  281 val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} Term.dummyT;  haftmann@33340  282 haftmann@33340  283 (*decompose additions AND subtractions as a sum*)  haftmann@33340  284 fun dest_summing (pos, Const (@{const_name HOL.plus}, _)  t  u, ts) =  haftmann@33340  285  dest_summing (pos, t, dest_summing (pos, u, ts))  haftmann@33340  286  | dest_summing (pos, Const (@{const_name HOL.minus}, _)  t  u, ts) =  haftmann@33340  287  dest_summing (pos, t, dest_summing (not pos, u, ts))  haftmann@33340  288  | dest_summing (pos, t, ts) =  haftmann@33340  289  if pos then t::ts else mk_minus t :: ts;  haftmann@33340  290 haftmann@33340  291 fun dest_sum t = dest_summing (true, t, []);  haftmann@33340  292 haftmann@30934  293 structure CancelDivMod = CancelDivModFun(struct  haftmann@30934  294 haftmann@30934  295  val div_name = @{const_name div};  haftmann@30934  296  val mod_name = @{const_name mod};  wenzelm@23164  297  val mk_binop = HOLogic.mk_binop;  haftmann@33340  298  val mk_sum = mk_sum HOLogic.intT;  haftmann@33340  299  val dest_sum = dest_sum;  haftmann@30934  300 haftmann@30934  301  val div_mod_eqs = map mk_meta_eq [@{thm zdiv_zmod_equality}, @{thm zdiv_zmod_equality2}];  haftmann@30934  302 wenzelm@23164  303  val trans = trans;  haftmann@30934  304 haftmann@30934  305  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac  haftmann@30934  306  (@{thm diff_minus} :: @{thms add_0s} @ @{thms add_ac}))  haftmann@30934  307 wenzelm@23164  308 end)  wenzelm@23164  309 wenzelm@23164  310 in  wenzelm@23164  311 wenzelm@32010  312 val cancel_div_mod_int_proc = Simplifier.simproc @{theory}  haftmann@30934  313  "cancel_zdiv_zmod" ["(k::int) + l"] (K CancelDivMod.proc);  wenzelm@23164  314 haftmann@30934  315 val _ = Addsimprocs [cancel_div_mod_int_proc];  wenzelm@23164  316 haftmann@30934  317 end  wenzelm@23164  318 *}  wenzelm@23164  319 wenzelm@23164  320 lemma pos_mod_conj : "(0::int) < b ==> 0 \ a mod b & a mod b < b"  haftmann@33340  321 apply (cut_tac a = a and b = b in divmod_int_correct)  haftmann@33340  322 apply (auto simp add: divmod_int_rel_def mod_int_def)  wenzelm@23164  323 done  wenzelm@23164  324 wenzelm@23164  325 lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1, standard]  wenzelm@23164  326  and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2, standard]  wenzelm@23164  327 wenzelm@23164  328 lemma neg_mod_conj : "b < (0::int) ==> a mod b \ 0 & b < a mod b"  haftmann@33340  329 apply (cut_tac a = a and b = b in divmod_int_correct)  haftmann@33340  330 apply (auto simp add: divmod_int_rel_def div_int_def mod_int_def)  wenzelm@23164  331 done  wenzelm@23164  332 wenzelm@23164  333 lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1, standard]  wenzelm@23164  334  and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2, standard]  wenzelm@23164  335 wenzelm@23164  336 wenzelm@23164  337 wenzelm@23164  338 subsection{*General Properties of div and mod*}  wenzelm@23164  339 haftmann@33340  340 lemma divmod_int_rel_div_mod: "b \ 0 ==> divmod_int_rel a b (a div b, a mod b)"  wenzelm@23164  341 apply (cut_tac a = a and b = b in zmod_zdiv_equality)  haftmann@33340  342 apply (force simp add: divmod_int_rel_def linorder_neq_iff)  wenzelm@23164  343 done  wenzelm@23164  344 haftmann@33340  345 lemma divmod_int_rel_div: "[| divmod_int_rel a b (q, r); b \ 0 |] ==> a div b = q"  haftmann@33340  346 by (simp add: divmod_int_rel_div_mod [THEN unique_quotient])  wenzelm@23164  347 haftmann@33340  348 lemma divmod_int_rel_mod: "[| divmod_int_rel a b (q, r); b \ 0 |] ==> a mod b = r"  haftmann@33340  349 by (simp add: divmod_int_rel_div_mod [THEN unique_remainder])  wenzelm@23164  350 wenzelm@23164  351 lemma div_pos_pos_trivial: "[| (0::int) \ a; a < b |] ==> a div b = 0"  haftmann@33340  352 apply (rule divmod_int_rel_div)  haftmann@33340  353 apply (auto simp add: divmod_int_rel_def)  wenzelm@23164  354 done  wenzelm@23164  355 wenzelm@23164  356 lemma div_neg_neg_trivial: "[| a \ (0::int); b < a |] ==> a div b = 0"  haftmann@33340  357 apply (rule divmod_int_rel_div)  haftmann@33340  358 apply (auto simp add: divmod_int_rel_def)  wenzelm@23164  359 done  wenzelm@23164  360 wenzelm@23164  361 lemma div_pos_neg_trivial: "[| (0::int) < a; a+b \ 0 |] ==> a div b = -1"  haftmann@33340  362 apply (rule divmod_int_rel_div)  haftmann@33340  363 apply (auto simp add: divmod_int_rel_def)  wenzelm@23164  364 done  wenzelm@23164  365 wenzelm@23164  366 (*There is no div_neg_pos_trivial because 0 div b = 0 would supersede it*)  wenzelm@23164  367 wenzelm@23164  368 lemma mod_pos_pos_trivial: "[| (0::int) \ a; a < b |] ==> a mod b = a"  haftmann@33340  369 apply (rule_tac q = 0 in divmod_int_rel_mod)  haftmann@33340  370 apply (auto simp add: divmod_int_rel_def)  wenzelm@23164  371 done  wenzelm@23164  372 wenzelm@23164  373 lemma mod_neg_neg_trivial: "[| a \ (0::int); b < a |] ==> a mod b = a"  haftmann@33340  374 apply (rule_tac q = 0 in divmod_int_rel_mod)  haftmann@33340  375 apply (auto simp add: divmod_int_rel_def)  wenzelm@23164  376 done  wenzelm@23164  377 wenzelm@23164  378 lemma mod_pos_neg_trivial: "[| (0::int) < a; a+b \ 0 |] ==> a mod b = a+b"  haftmann@33340  379 apply (rule_tac q = "-1" in divmod_int_rel_mod)  haftmann@33340  380 apply (auto simp add: divmod_int_rel_def)  wenzelm@23164  381 done  wenzelm@23164  382 wenzelm@23164  383 text{*There is no @{text mod_neg_pos_trivial}.*}  wenzelm@23164  384 wenzelm@23164  385 wenzelm@23164  386 (*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*)  wenzelm@23164  387 lemma zdiv_zminus_zminus [simp]: "(-a) div (-b) = a div (b::int)"  wenzelm@23164  388 apply (case_tac "b = 0", simp)  haftmann@33340  389 apply (simp add: divmod_int_rel_div_mod [THEN divmod_int_rel_neg, simplified,  haftmann@33340  390  THEN divmod_int_rel_div, THEN sym])  wenzelm@23164  391 wenzelm@23164  392 done  wenzelm@23164  393 wenzelm@23164  394 (*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*)  wenzelm@23164  395 lemma zmod_zminus_zminus [simp]: "(-a) mod (-b) = - (a mod (b::int))"  wenzelm@23164  396 apply (case_tac "b = 0", simp)  haftmann@33340  397 apply (subst divmod_int_rel_div_mod [THEN divmod_int_rel_neg, simplified, THEN divmod_int_rel_mod],  wenzelm@23164  398  auto)  wenzelm@23164  399 done  wenzelm@23164  400 wenzelm@23164  401 wenzelm@23164  402 subsection{*Laws for div and mod with Unary Minus*}  wenzelm@23164  403 wenzelm@23164  404 lemma zminus1_lemma:  haftmann@33340  405  "divmod_int_rel a b (q, r)  haftmann@33340  406  ==> divmod_int_rel (-a) b (if r=0 then -q else -q - 1,  haftmann@29651  407  if r=0 then 0 else b-r)"  haftmann@33340  408 by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_diff_distrib)  wenzelm@23164  409 wenzelm@23164  410 wenzelm@23164  411 lemma zdiv_zminus1_eq_if:  wenzelm@23164  412  "b \ (0::int)  wenzelm@23164  413  ==> (-a) div b =  wenzelm@23164  414  (if a mod b = 0 then - (a div b) else - (a div b) - 1)"  haftmann@33340  415 by (blast intro: divmod_int_rel_div_mod [THEN zminus1_lemma, THEN divmod_int_rel_div])  wenzelm@23164  416 wenzelm@23164  417 lemma zmod_zminus1_eq_if:  wenzelm@23164  418  "(-a::int) mod b = (if a mod b = 0 then 0 else b - (a mod b))"  wenzelm@23164  419 apply (case_tac "b = 0", simp)  haftmann@33340  420 apply (blast intro: divmod_int_rel_div_mod [THEN zminus1_lemma, THEN divmod_int_rel_mod])  wenzelm@23164  421 done  wenzelm@23164  422 haftmann@29936  423 lemma zmod_zminus1_not_zero:  haftmann@29936  424  fixes k l :: int  haftmann@29936  425  shows "- k mod l \ 0 \ k mod l \ 0"  haftmann@29936  426  unfolding zmod_zminus1_eq_if by auto  haftmann@29936  427 wenzelm@23164  428 lemma zdiv_zminus2: "a div (-b) = (-a::int) div b"  wenzelm@23164  429 by (cut_tac a = "-a" in zdiv_zminus_zminus, auto)  wenzelm@23164  430 wenzelm@23164  431 lemma zmod_zminus2: "a mod (-b) = - ((-a::int) mod b)"  wenzelm@23164  432 by (cut_tac a = "-a" and b = b in zmod_zminus_zminus, auto)  wenzelm@23164  433 wenzelm@23164  434 lemma zdiv_zminus2_eq_if:  wenzelm@23164  435  "b \ (0::int)  wenzelm@23164  436  ==> a div (-b) =  wenzelm@23164  437  (if a mod b = 0 then - (a div b) else - (a div b) - 1)"  wenzelm@23164  438 by (simp add: zdiv_zminus1_eq_if zdiv_zminus2)  wenzelm@23164  439 wenzelm@23164  440 lemma zmod_zminus2_eq_if:  wenzelm@23164  441  "a mod (-b::int) = (if a mod b = 0 then 0 else (a mod b) - b)"  wenzelm@23164  442 by (simp add: zmod_zminus1_eq_if zmod_zminus2)  wenzelm@23164  443 haftmann@29936  444 lemma zmod_zminus2_not_zero:  haftmann@29936  445  fixes k l :: int  haftmann@29936  446  shows "k mod - l \ 0 \ k mod l \ 0"  haftmann@29936  447  unfolding zmod_zminus2_eq_if by auto  haftmann@29936  448 wenzelm@23164  449 wenzelm@23164  450 subsection{*Division of a Number by Itself*}  wenzelm@23164  451 wenzelm@23164  452 lemma self_quotient_aux1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 \ q"  wenzelm@23164  453 apply (subgoal_tac "0 < a*q")  wenzelm@23164  454  apply (simp add: zero_less_mult_iff, arith)  wenzelm@23164  455 done  wenzelm@23164  456 wenzelm@23164  457 lemma self_quotient_aux2: "[| (0::int) < a; a = r + a*q; 0 \ r |] ==> q \ 1"  wenzelm@23164  458 apply (subgoal_tac "0 \ a* (1-q) ")  wenzelm@23164  459  apply (simp add: zero_le_mult_iff)  wenzelm@23164  460 apply (simp add: right_diff_distrib)  wenzelm@23164  461 done  wenzelm@23164  462 haftmann@33340  463 lemma self_quotient: "[| divmod_int_rel a a (q, r); a \ (0::int) |] ==> q = 1"  haftmann@33340  464 apply (simp add: split_ifs divmod_int_rel_def linorder_neq_iff)  wenzelm@23164  465 apply (rule order_antisym, safe, simp_all)  wenzelm@23164  466 apply (rule_tac [3] a = "-a" and r = "-r" in self_quotient_aux1)  wenzelm@23164  467 apply (rule_tac a = "-a" and r = "-r" in self_quotient_aux2)  wenzelm@23164  468 apply (force intro: self_quotient_aux1 self_quotient_aux2 simp add: add_commute)+  wenzelm@23164  469 done  wenzelm@23164  470 haftmann@33340  471 lemma self_remainder: "[| divmod_int_rel a a (q, r); a \ (0::int) |] ==> r = 0"  wenzelm@23164  472 apply (frule self_quotient, assumption)  haftmann@33340  473 apply (simp add: divmod_int_rel_def)  wenzelm@23164  474 done  wenzelm@23164  475 wenzelm@23164  476 lemma zdiv_self [simp]: "a \ 0 ==> a div a = (1::int)"  haftmann@33340  477 by (simp add: divmod_int_rel_div_mod [THEN self_quotient])  wenzelm@23164  478 wenzelm@23164  479 (*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *)  wenzelm@23164  480 lemma zmod_self [simp]: "a mod a = (0::int)"  wenzelm@23164  481 apply (case_tac "a = 0", simp)  haftmann@33340  482 apply (simp add: divmod_int_rel_div_mod [THEN self_remainder])  wenzelm@23164  483 done  wenzelm@23164  484 wenzelm@23164  485 wenzelm@23164  486 subsection{*Computation of Division and Remainder*}  wenzelm@23164  487 wenzelm@23164  488 lemma zdiv_zero [simp]: "(0::int) div b = 0"  haftmann@33340  489 by (simp add: div_int_def divmod_int_def)  wenzelm@23164  490 wenzelm@23164  491 lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"  haftmann@33340  492 by (simp add: div_int_def divmod_int_def)  wenzelm@23164  493 wenzelm@23164  494 lemma zmod_zero [simp]: "(0::int) mod b = 0"  haftmann@33340  495 by (simp add: mod_int_def divmod_int_def)  wenzelm@23164  496 wenzelm@23164  497 lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"  haftmann@33340  498 by (simp add: mod_int_def divmod_int_def)  wenzelm@23164  499 wenzelm@23164  500 text{*a positive, b positive *}  wenzelm@23164  501 wenzelm@23164  502 lemma div_pos_pos: "[| 0 < a; 0 \ b |] ==> a div b = fst (posDivAlg a b)"  haftmann@33340  503 by (simp add: div_int_def divmod_int_def)  wenzelm@23164  504 wenzelm@23164  505 lemma mod_pos_pos: "[| 0 < a; 0 \ b |] ==> a mod b = snd (posDivAlg a b)"  haftmann@33340  506 by (simp add: mod_int_def divmod_int_def)  wenzelm@23164  507 wenzelm@23164  508 text{*a negative, b positive *}  wenzelm@23164  509 wenzelm@23164  510 lemma div_neg_pos: "[| a < 0; 0 < b |] ==> a div b = fst (negDivAlg a b)"  haftmann@33340  511 by (simp add: div_int_def divmod_int_def)  wenzelm@23164  512 wenzelm@23164  513 lemma mod_neg_pos: "[| a < 0; 0 < b |] ==> a mod b = snd (negDivAlg a b)"  haftmann@33340  514 by (simp add: mod_int_def divmod_int_def)  wenzelm@23164  515 wenzelm@23164  516 text{*a positive, b negative *}  wenzelm@23164  517 wenzelm@23164  518 lemma div_pos_neg:  wenzelm@23164  519  "[| 0 < a; b < 0 |] ==> a div b = fst (negateSnd (negDivAlg (-a) (-b)))"  haftmann@33340  520 by (simp add: div_int_def divmod_int_def)  wenzelm@23164  521 wenzelm@23164  522 lemma mod_pos_neg:  wenzelm@23164  523  "[| 0 < a; b < 0 |] ==> a mod b = snd (negateSnd (negDivAlg (-a) (-b)))"  haftmann@33340  524 by (simp add: mod_int_def divmod_int_def)  wenzelm@23164  525 wenzelm@23164  526 text{*a negative, b negative *}  wenzelm@23164  527 wenzelm@23164  528 lemma div_neg_neg:  wenzelm@23164  529  "[| a < 0; b \ 0 |] ==> a div b = fst (negateSnd (posDivAlg (-a) (-b)))"  haftmann@33340  530 by (simp add: div_int_def divmod_int_def)  wenzelm@23164  531 wenzelm@23164  532 lemma mod_neg_neg:  wenzelm@23164  533  "[| a < 0; b \ 0 |] ==> a mod b = snd (negateSnd (posDivAlg (-a) (-b)))"  haftmann@33340  534 by (simp add: mod_int_def divmod_int_def)  wenzelm@23164  535 wenzelm@23164  536 text {*Simplify expresions in which div and mod combine numerical constants*}  wenzelm@23164  537 haftmann@33340  538 lemma divmod_int_relI:  huffman@24481  539  "\a == b * q + r; if 0 < b then 0 \ r \ r < b else b < r \ r \ 0\  haftmann@33340  540  \ divmod_int_rel a b (q, r)"  haftmann@33340  541  unfolding divmod_int_rel_def by simp  huffman@24481  542 haftmann@33340  543 lemmas divmod_int_rel_div_eq = divmod_int_relI [THEN divmod_int_rel_div, THEN eq_reflection]  haftmann@33340  544 lemmas divmod_int_rel_mod_eq = divmod_int_relI [THEN divmod_int_rel_mod, THEN eq_reflection]  huffman@24481  545 lemmas arithmetic_simps =  huffman@24481  546  arith_simps  huffman@24481  547  add_special  huffman@24481  548  OrderedGroup.add_0_left  huffman@24481  549  OrderedGroup.add_0_right  huffman@24481  550  mult_zero_left  huffman@24481  551  mult_zero_right  huffman@24481  552  mult_1_left  huffman@24481  553  mult_1_right  huffman@24481  554 huffman@24481  555 (* simprocs adapted from HOL/ex/Binary.thy *)  huffman@24481  556 ML {*  huffman@24481  557 local  haftmann@30517  558  val mk_number = HOLogic.mk_number HOLogic.intT;  haftmann@30517  559  fun mk_cert u k l = @{term "plus :: int \ int \ int"}   haftmann@30517  560  (@{term "times :: int \ int \ int"}  u  mk_number k)   haftmann@30517  561  mk_number l;  haftmann@30517  562  fun prove ctxt prop = Goal.prove ctxt [] [] prop  haftmann@30517  563  (K (ALLGOALS (full_simp_tac (HOL_basic_ss addsimps @{thms arithmetic_simps}))));  huffman@24481  564  fun binary_proc proc ss ct =  huffman@24481  565  (case Thm.term_of ct of  huffman@24481  566  _  t  u =>  huffman@24481  567  (case try (pairself ((snd o HOLogic.dest_number))) (t, u) of  huffman@24481  568  SOME args => proc (Simplifier.the_context ss) args  huffman@24481  569  | NONE => NONE)  huffman@24481  570  | _ => NONE);  huffman@24481  571 in  haftmann@30517  572  fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>  haftmann@30517  573  if n = 0 then NONE  haftmann@30517  574  else let val (k, l) = Integer.div_mod m n;  haftmann@30517  575  in SOME (rule OF [prove ctxt (Logic.mk_equals (t, mk_cert u k l))]) end);  haftmann@30517  576 end  huffman@24481  577 *}  huffman@24481  578 huffman@24481  579 simproc_setup binary_int_div ("number_of m div number_of n :: int") =  haftmann@33340  580  {* K (divmod_proc (@{thm divmod_int_rel_div_eq})) *}  huffman@24481  581 huffman@24481  582 simproc_setup binary_int_mod ("number_of m mod number_of n :: int") =  haftmann@33340  583  {* K (divmod_proc (@{thm divmod_int_rel_mod_eq})) *}  huffman@24481  584 wenzelm@23164  585 lemmas posDivAlg_eqn_number_of [simp] =  wenzelm@23164  586  posDivAlg_eqn [of "number_of v" "number_of w", standard]  wenzelm@23164  587 wenzelm@23164  588 lemmas negDivAlg_eqn_number_of [simp] =  wenzelm@23164  589  negDivAlg_eqn [of "number_of v" "number_of w", standard]  wenzelm@23164  590 wenzelm@23164  591 wenzelm@23164  592 text{*Special-case simplification *}  wenzelm@23164  593 wenzelm@23164  594 lemma zmod_minus1_right [simp]: "a mod (-1::int) = 0"  wenzelm@23164  595 apply (cut_tac a = a and b = "-1" in neg_mod_sign)  wenzelm@23164  596 apply (cut_tac [2] a = a and b = "-1" in neg_mod_bound)  wenzelm@23164  597 apply (auto simp del: neg_mod_sign neg_mod_bound)  wenzelm@23164  598 done  wenzelm@23164  599 wenzelm@23164  600 lemma zdiv_minus1_right [simp]: "a div (-1::int) = -a"  wenzelm@23164  601 by (cut_tac a = a and b = "-1" in zmod_zdiv_equality, auto)  wenzelm@23164  602 wenzelm@23164  603 (** The last remaining special cases for constant arithmetic:  wenzelm@23164  604  1 div z and 1 mod z **)  wenzelm@23164  605 wenzelm@23164  606 lemmas div_pos_pos_1_number_of [simp] =  wenzelm@23164  607  div_pos_pos [OF int_0_less_1, of "number_of w", standard]  wenzelm@23164  608 wenzelm@23164  609 lemmas div_pos_neg_1_number_of [simp] =  wenzelm@23164  610  div_pos_neg [OF int_0_less_1, of "number_of w", standard]  wenzelm@23164  611 wenzelm@23164  612 lemmas mod_pos_pos_1_number_of [simp] =  wenzelm@23164  613  mod_pos_pos [OF int_0_less_1, of "number_of w", standard]  wenzelm@23164  614 wenzelm@23164  615 lemmas mod_pos_neg_1_number_of [simp] =  wenzelm@23164  616  mod_pos_neg [OF int_0_less_1, of "number_of w", standard]  wenzelm@23164  617 wenzelm@23164  618 wenzelm@23164  619 lemmas posDivAlg_eqn_1_number_of [simp] =  wenzelm@23164  620  posDivAlg_eqn [of concl: 1 "number_of w", standard]  wenzelm@23164  621 wenzelm@23164  622 lemmas negDivAlg_eqn_1_number_of [simp] =  wenzelm@23164  623  negDivAlg_eqn [of concl: 1 "number_of w", standard]  wenzelm@23164  624 wenzelm@23164  625 wenzelm@23164  626 wenzelm@23164  627 subsection{*Monotonicity in the First Argument (Dividend)*}  wenzelm@23164  628 wenzelm@23164  629 lemma zdiv_mono1: "[| a \ a'; 0 < (b::int) |] ==> a div b \ a' div b"  wenzelm@23164  630 apply (cut_tac a = a and b = b in zmod_zdiv_equality)  wenzelm@23164  631 apply (cut_tac a = a' and b = b in zmod_zdiv_equality)  wenzelm@23164  632 apply (rule unique_quotient_lemma)  wenzelm@23164  633 apply (erule subst)  wenzelm@23164  634 apply (erule subst, simp_all)  wenzelm@23164  635 done  wenzelm@23164  636 wenzelm@23164  637 lemma zdiv_mono1_neg: "[| a \ a'; (b::int) < 0 |] ==> a' div b \ a div b"  wenzelm@23164  638 apply (cut_tac a = a and b = b in zmod_zdiv_equality)  wenzelm@23164  639 apply (cut_tac a = a' and b = b in zmod_zdiv_equality)  wenzelm@23164  640 apply (rule unique_quotient_lemma_neg)  wenzelm@23164  641 apply (erule subst)  wenzelm@23164  642 apply (erule subst, simp_all)  wenzelm@23164  643 done  wenzelm@23164  644 wenzelm@23164  645 wenzelm@23164  646 subsection{*Monotonicity in the Second Argument (Divisor)*}  wenzelm@23164  647 wenzelm@23164  648 lemma q_pos_lemma:  wenzelm@23164  649  "[| 0 \ b'*q' + r'; r' < b'; 0 < b' |] ==> 0 \ (q'::int)"  wenzelm@23164  650 apply (subgoal_tac "0 < b'* (q' + 1) ")  wenzelm@23164  651  apply (simp add: zero_less_mult_iff)  wenzelm@23164  652 apply (simp add: right_distrib)  wenzelm@23164  653 done  wenzelm@23164  654 wenzelm@23164  655 lemma zdiv_mono2_lemma:  wenzelm@23164  656  "[| b*q + r = b'*q' + r'; 0 \ b'*q' + r';  wenzelm@23164  657  r' < b'; 0 \ r; 0 < b'; b' \ b |]  wenzelm@23164  658  ==> q \ (q'::int)"  wenzelm@23164  659 apply (frule q_pos_lemma, assumption+)  wenzelm@23164  660 apply (subgoal_tac "b*q < b* (q' + 1) ")  wenzelm@23164  661  apply (simp add: mult_less_cancel_left)  wenzelm@23164  662 apply (subgoal_tac "b*q = r' - r + b'*q'")  wenzelm@23164  663  prefer 2 apply simp  wenzelm@23164  664 apply (simp (no_asm_simp) add: right_distrib)  wenzelm@23164  665 apply (subst add_commute, rule zadd_zless_mono, arith)  wenzelm@23164  666 apply (rule mult_right_mono, auto)  wenzelm@23164  667 done  wenzelm@23164  668 wenzelm@23164  669 lemma zdiv_mono2:  wenzelm@23164  670  "[| (0::int) \ a; 0 < b'; b' \ b |] ==> a div b \ a div b'"  wenzelm@23164  671 apply (subgoal_tac "b \ 0")  wenzelm@23164  672  prefer 2 apply arith  wenzelm@23164  673 apply (cut_tac a = a and b = b in zmod_zdiv_equality)  wenzelm@23164  674 apply (cut_tac a = a and b = b' in zmod_zdiv_equality)  wenzelm@23164  675 apply (rule zdiv_mono2_lemma)  wenzelm@23164  676 apply (erule subst)  wenzelm@23164  677 apply (erule subst, simp_all)  wenzelm@23164  678 done  wenzelm@23164  679 wenzelm@23164  680 lemma q_neg_lemma:  wenzelm@23164  681  "[| b'*q' + r' < 0; 0 \ r'; 0 < b' |] ==> q' \ (0::int)"  wenzelm@23164  682 apply (subgoal_tac "b'*q' < 0")  wenzelm@23164  683  apply (simp add: mult_less_0_iff, arith)  wenzelm@23164  684 done  wenzelm@23164  685 wenzelm@23164  686 lemma zdiv_mono2_neg_lemma:  wenzelm@23164  687  "[| b*q + r = b'*q' + r'; b'*q' + r' < 0;  wenzelm@23164  688  r < b; 0 \ r'; 0 < b'; b' \ b |]  wenzelm@23164  689  ==> q' \ (q::int)"  wenzelm@23164  690 apply (frule q_neg_lemma, assumption+)  wenzelm@23164  691 apply (subgoal_tac "b*q' < b* (q + 1) ")  wenzelm@23164  692  apply (simp add: mult_less_cancel_left)  wenzelm@23164  693 apply (simp add: right_distrib)  wenzelm@23164  694 apply (subgoal_tac "b*q' \ b'*q'")  wenzelm@23164  695  prefer 2 apply (simp add: mult_right_mono_neg, arith)  wenzelm@23164  696 done  wenzelm@23164  697 wenzelm@23164  698 lemma zdiv_mono2_neg:  wenzelm@23164  699  "[| a < (0::int); 0 < b'; b' \ b |] ==> a div b' \ a div b"  wenzelm@23164  700 apply (cut_tac a = a and b = b in zmod_zdiv_equality)  wenzelm@23164  701 apply (cut_tac a = a and b = b' in zmod_zdiv_equality)  wenzelm@23164  702 apply (rule zdiv_mono2_neg_lemma)  wenzelm@23164  703 apply (erule subst)  wenzelm@23164  704 apply (erule subst, simp_all)  wenzelm@23164  705 done  wenzelm@23164  706 haftmann@25942  707 wenzelm@23164  708 subsection{*More Algebraic Laws for div and mod*}  wenzelm@23164  709 wenzelm@23164  710 text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *}  wenzelm@23164  711 wenzelm@23164  712 lemma zmult1_lemma:  haftmann@33340  713  "[| divmod_int_rel b c (q, r); c \ 0 |]  haftmann@33340  714  ==> divmod_int_rel (a * b) c (a*q + a*r div c, a*r mod c)"  haftmann@33340  715 by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_distrib mult_ac)  wenzelm@23164  716 wenzelm@23164  717 lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"  wenzelm@23164  718 apply (case_tac "c = 0", simp)  haftmann@33340  719 apply (blast intro: divmod_int_rel_div_mod [THEN zmult1_lemma, THEN divmod_int_rel_div])  wenzelm@23164  720 done  wenzelm@23164  721 wenzelm@23164  722 lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)"  wenzelm@23164  723 apply (case_tac "c = 0", simp)  haftmann@33340  724 apply (blast intro: divmod_int_rel_div_mod [THEN zmult1_lemma, THEN divmod_int_rel_mod])  wenzelm@23164  725 done  wenzelm@23164  726 huffman@29403  727 lemma zmod_zdiv_trivial: "(a mod b) div b = (0::int)"  haftmann@27651  728 apply (case_tac "b = 0", simp)  haftmann@27651  729 apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)  haftmann@27651  730 done  haftmann@27651  731 haftmann@27651  732 text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}  haftmann@27651  733 haftmann@27651  734 lemma zadd1_lemma:  haftmann@33340  735  "[| divmod_int_rel a c (aq, ar); divmod_int_rel b c (bq, br); c \ 0 |]  haftmann@33340  736  ==> divmod_int_rel (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"  haftmann@33340  737 by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_distrib)  haftmann@27651  738 haftmann@27651  739 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)  haftmann@27651  740 lemma zdiv_zadd1_eq:  haftmann@27651  741  "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"  haftmann@27651  742 apply (case_tac "c = 0", simp)  haftmann@33340  743 apply (blast intro: zadd1_lemma [OF divmod_int_rel_div_mod divmod_int_rel_div_mod] divmod_int_rel_div)  haftmann@27651  744 done  haftmann@27651  745 huffman@29405  746 instance int :: ring_div  haftmann@27651  747 proof  haftmann@27651  748  fix a b c :: int  haftmann@27651  749  assume not0: "b \ 0"  haftmann@27651  750  show "(a + c * b) div b = c + a div b"  haftmann@27651  751  unfolding zdiv_zadd1_eq [of a "c * b"] using not0  nipkow@30181  752  by (simp add: zmod_zmult1_eq zmod_zdiv_trivial zdiv_zmult1_eq)  haftmann@30930  753 next  haftmann@30930  754  fix a b c :: int  haftmann@30930  755  assume "a \ 0"  haftmann@30930  756  then show "(a * b) div (a * c) = b div c"  haftmann@30930  757  proof (cases "b \ 0 \ c \ 0")  haftmann@30930  758  case False then show ?thesis by auto  haftmann@30930  759  next  haftmann@30930  760  case True then have "b \ 0" and "c \ 0" by auto  haftmann@30930  761  with a \ 0  haftmann@33340  762  have "\q r. divmod_int_rel b c (q, r) \ divmod_int_rel (a * b) (a * c) (q, a * r)"  haftmann@33340  763  apply (auto simp add: divmod_int_rel_def)  haftmann@30930  764  apply (auto simp add: algebra_simps)  haftmann@33340  765  apply (auto simp add: zero_less_mult_iff zero_le_mult_iff mult_le_0_iff mult_commute [of a] mult_less_cancel_right)  haftmann@30930  766  done  haftmann@33340  767  moreover with c \ 0 divmod_int_rel_div_mod have "divmod_int_rel b c (b div c, b mod c)" by auto  haftmann@33340  768  ultimately have "divmod_int_rel (a * b) (a * c) (b div c, a * (b mod c))" .  haftmann@30930  769  moreover from a \ 0 c \ 0 have "a * c \ 0" by simp  haftmann@33340  770  ultimately show ?thesis by (rule divmod_int_rel_div)  haftmann@30930  771  qed  haftmann@27651  772 qed auto  haftmann@25942  773 haftmann@29651  774 lemma posDivAlg_div_mod:  haftmann@29651  775  assumes "k \ 0"  haftmann@29651  776  and "l \ 0"  haftmann@29651  777  shows "posDivAlg k l = (k div l, k mod l)"  haftmann@29651  778 proof (cases "l = 0")  haftmann@29651  779  case True then show ?thesis by (simp add: posDivAlg.simps)  haftmann@29651  780 next  haftmann@29651  781  case False with assms posDivAlg_correct  haftmann@33340  782  have "divmod_int_rel k l (fst (posDivAlg k l), snd (posDivAlg k l))"  haftmann@29651  783  by simp  haftmann@33340  784  from divmod_int_rel_div [OF this l \ 0] divmod_int_rel_mod [OF this l \ 0]  haftmann@29651  785  show ?thesis by simp  haftmann@29651  786 qed  haftmann@29651  787 haftmann@29651  788 lemma negDivAlg_div_mod:  haftmann@29651  789  assumes "k < 0"  haftmann@29651  790  and "l > 0"  haftmann@29651  791  shows "negDivAlg k l = (k div l, k mod l)"  haftmann@29651  792 proof -  haftmann@29651  793  from assms have "l \ 0" by simp  haftmann@29651  794  from assms negDivAlg_correct  haftmann@33340  795  have "divmod_int_rel k l (fst (negDivAlg k l), snd (negDivAlg k l))"  haftmann@29651  796  by simp  haftmann@33340  797  from divmod_int_rel_div [OF this l \ 0] divmod_int_rel_mod [OF this l \ 0]  haftmann@29651  798  show ?thesis by simp  haftmann@29651  799 qed  haftmann@29651  800 wenzelm@23164  801 lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"  huffman@29403  802 by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)  wenzelm@23164  803 huffman@29403  804 (* REVISIT: should this be generalized to all semiring_div types? *)  wenzelm@23164  805 lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]  wenzelm@23164  806 nipkow@23983  807 wenzelm@23164  808 subsection{*Proving @{term "a div (b*c) = (a div b) div c"} *}  wenzelm@23164  809 wenzelm@23164  810 (*The condition c>0 seems necessary. Consider that 7 div ~6 = ~2 but  wenzelm@23164  811  7 div 2 div ~3 = 3 div ~3 = ~1. The subcase (a div b) mod c = 0 seems  wenzelm@23164  812  to cause particular problems.*)  wenzelm@23164  813 wenzelm@23164  814 text{*first, four lemmas to bound the remainder for the cases b<0 and b>0 *}  wenzelm@23164  815 wenzelm@23164  816 lemma zmult2_lemma_aux1: "[| (0::int) < c; b < r; r \ 0 |] ==> b*c < b*(q mod c) + r"  wenzelm@23164  817 apply (subgoal_tac "b * (c - q mod c) < r * 1")  nipkow@29667  818  apply (simp add: algebra_simps)  wenzelm@23164  819 apply (rule order_le_less_trans)  nipkow@29667  820  apply (erule_tac [2] mult_strict_right_mono)  nipkow@29667  821  apply (rule mult_left_mono_neg)  nipkow@29667  822  using add1_zle_eq[of "q mod c"]apply(simp add: algebra_simps pos_mod_bound)  nipkow@29667  823  apply (simp)  nipkow@29667  824 apply (simp)  wenzelm@23164  825 done  wenzelm@23164  826 wenzelm@23164  827 lemma zmult2_lemma_aux2:  wenzelm@23164  828  "[| (0::int) < c; b < r; r \ 0 |] ==> b * (q mod c) + r \ 0"  wenzelm@23164  829 apply (subgoal_tac "b * (q mod c) \ 0")  wenzelm@23164  830  apply arith  wenzelm@23164  831 apply (simp add: mult_le_0_iff)  wenzelm@23164  832 done  wenzelm@23164  833 wenzelm@23164  834 lemma zmult2_lemma_aux3: "[| (0::int) < c; 0 \ r; r < b |] ==> 0 \ b * (q mod c) + r"  wenzelm@23164  835 apply (subgoal_tac "0 \ b * (q mod c) ")  wenzelm@23164  836 apply arith  wenzelm@23164  837 apply (simp add: zero_le_mult_iff)  wenzelm@23164  838 done  wenzelm@23164  839 wenzelm@23164  840 lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 \ r; r < b |] ==> b * (q mod c) + r < b * c"  wenzelm@23164  841 apply (subgoal_tac "r * 1 < b * (c - q mod c) ")  nipkow@29667  842  apply (simp add: right_diff_distrib)  wenzelm@23164  843 apply (rule order_less_le_trans)  nipkow@29667  844  apply (erule mult_strict_right_mono)  nipkow@29667  845  apply (rule_tac [2] mult_left_mono)  nipkow@29667  846  apply simp  nipkow@29667  847  using add1_zle_eq[of "q mod c"] apply (simp add: algebra_simps pos_mod_bound)  nipkow@29667  848 apply simp  wenzelm@23164  849 done  wenzelm@23164  850 haftmann@33340  851 lemma zmult2_lemma: "[| divmod_int_rel a b (q, r); b \ 0; 0 < c |]  haftmann@33340  852  ==> divmod_int_rel a (b * c) (q div c, b*(q mod c) + r)"  haftmann@33340  853 by (auto simp add: mult_ac divmod_int_rel_def linorder_neq_iff  wenzelm@23164  854  zero_less_mult_iff right_distrib [symmetric]  wenzelm@23164  855  zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4)  wenzelm@23164  856 wenzelm@23164  857 lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c"  wenzelm@23164  858 apply (case_tac "b = 0", simp)  haftmann@33340  859 apply (force simp add: divmod_int_rel_div_mod [THEN zmult2_lemma, THEN divmod_int_rel_div])  wenzelm@23164  860 done  wenzelm@23164  861 wenzelm@23164  862 lemma zmod_zmult2_eq:  wenzelm@23164  863  "(0::int) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b"  wenzelm@23164  864 apply (case_tac "b = 0", simp)  haftmann@33340  865 apply (force simp add: divmod_int_rel_div_mod [THEN zmult2_lemma, THEN divmod_int_rel_mod])  wenzelm@23164  866 done  wenzelm@23164  867 wenzelm@23164  868 wenzelm@23164  869 subsection {*Splitting Rules for div and mod*}  wenzelm@23164  870 wenzelm@23164  871 text{*The proofs of the two lemmas below are essentially identical*}  wenzelm@23164  872 wenzelm@23164  873 lemma split_pos_lemma:  wenzelm@23164  874  "0  wenzelm@23164  875  P(n div k :: int)(n mod k) = (\i j. 0\j & j P i j)"  wenzelm@23164  876 apply (rule iffI, clarify)  wenzelm@23164  877  apply (erule_tac P="P ?x ?y" in rev_mp)  nipkow@29948  878  apply (subst mod_add_eq)  wenzelm@23164  879  apply (subst zdiv_zadd1_eq)  wenzelm@23164  880  apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)  wenzelm@23164  881 txt{*converse direction*}  wenzelm@23164  882 apply (drule_tac x = "n div k" in spec)  wenzelm@23164  883 apply (drule_tac x = "n mod k" in spec, simp)  wenzelm@23164  884 done  wenzelm@23164  885 wenzelm@23164  886 lemma split_neg_lemma:  wenzelm@23164  887  "k<0 ==>  wenzelm@23164  888  P(n div k :: int)(n mod k) = (\i j. k0 & n = k*i + j --> P i j)"  wenzelm@23164  889 apply (rule iffI, clarify)  wenzelm@23164  890  apply (erule_tac P="P ?x ?y" in rev_mp)  nipkow@29948  891  apply (subst mod_add_eq)  wenzelm@23164  892  apply (subst zdiv_zadd1_eq)  wenzelm@23164  893  apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)  wenzelm@23164  894 txt{*converse direction*}  wenzelm@23164  895 apply (drule_tac x = "n div k" in spec)  wenzelm@23164  896 apply (drule_tac x = "n mod k" in spec, simp)  wenzelm@23164  897 done  wenzelm@23164  898 wenzelm@23164  899 lemma split_zdiv:  wenzelm@23164  900  "P(n div k :: int) =  wenzelm@23164  901  ((k = 0 --> P 0) &  wenzelm@23164  902  (0 (\i j. 0\j & j P i)) &  wenzelm@23164  903  (k<0 --> (\i j. k0 & n = k*i + j --> P i)))"  wenzelm@23164  904 apply (case_tac "k=0", simp)  wenzelm@23164  905 apply (simp only: linorder_neq_iff)  wenzelm@23164  906 apply (erule disjE)  wenzelm@23164  907  apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"]  wenzelm@23164  908  split_neg_lemma [of concl: "%x y. P x"])  wenzelm@23164  909 done  wenzelm@23164  910 wenzelm@23164  911 lemma split_zmod:  wenzelm@23164  912  "P(n mod k :: int) =  wenzelm@23164  913  ((k = 0 --> P n) &  wenzelm@23164  914  (0 (\i j. 0\j & j P j)) &  wenzelm@23164  915  (k<0 --> (\i j. k0 & n = k*i + j --> P j)))"  wenzelm@23164  916 apply (case_tac "k=0", simp)  wenzelm@23164  917 apply (simp only: linorder_neq_iff)  wenzelm@23164  918 apply (erule disjE)  wenzelm@23164  919  apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"]  wenzelm@23164  920  split_neg_lemma [of concl: "%x y. P y"])  wenzelm@23164  921 done  wenzelm@23164  922 wenzelm@23164  923 (* Enable arith to deal with div 2 and mod 2: *)  wenzelm@23164  924 declare split_zdiv [of _ _ "number_of k", simplified, standard, arith_split]  wenzelm@23164  925 declare split_zmod [of _ _ "number_of k", simplified, standard, arith_split]  wenzelm@23164  926 wenzelm@23164  927 wenzelm@23164  928 subsection{*Speeding up the Division Algorithm with Shifting*}  wenzelm@23164  929 wenzelm@23164  930 text{*computing div by shifting *}  wenzelm@23164  931 wenzelm@23164  932 lemma pos_zdiv_mult_2: "(0::int) \ a ==> (1 + 2*b) div (2*a) = b div a"  wenzelm@23164  933 proof cases  wenzelm@23164  934  assume "a=0"  wenzelm@23164  935  thus ?thesis by simp  wenzelm@23164  936 next  wenzelm@23164  937  assume "a\0" and le_a: "0\a"  wenzelm@23164  938  hence a_pos: "1 \ a" by arith  haftmann@30652  939  hence one_less_a2: "1 < 2 * a" by arith  wenzelm@23164  940  hence le_2a: "2 * (1 + b mod a) \ 2 * a"  haftmann@30652  941  unfolding mult_le_cancel_left  haftmann@30652  942  by (simp add: add1_zle_eq add_commute [of 1])  wenzelm@23164  943  with a_pos have "0 \ b mod a" by simp  wenzelm@23164  944  hence le_addm: "0 \ 1 mod (2*a) + 2*(b mod a)"  wenzelm@23164  945  by (simp add: mod_pos_pos_trivial one_less_a2)  wenzelm@23164  946  with le_2a  wenzelm@23164  947  have "(1 mod (2*a) + 2*(b mod a)) div (2*a) = 0"  wenzelm@23164  948  by (simp add: div_pos_pos_trivial le_addm mod_pos_pos_trivial one_less_a2  wenzelm@23164  949  right_distrib)  wenzelm@23164  950  thus ?thesis  wenzelm@23164  951  by (subst zdiv_zadd1_eq,  haftmann@30930  952  simp add: mod_mult_mult1 one_less_a2  wenzelm@23164  953  div_pos_pos_trivial)  wenzelm@23164  954 qed  wenzelm@23164  955 wenzelm@23164  956 lemma neg_zdiv_mult_2: "a \ (0::int) ==> (1 + 2*b) div (2*a) = (b+1) div a"  wenzelm@23164  957 apply (subgoal_tac " (1 + 2* (-b - 1)) div (2 * (-a)) = (-b - 1) div (-a) ")  wenzelm@23164  958 apply (rule_tac [2] pos_zdiv_mult_2)  haftmann@33340  959 apply (auto simp add: right_diff_distrib)  wenzelm@23164  960 apply (subgoal_tac " (-1 - (2 * b)) = - (1 + (2 * b))")  haftmann@33340  961 apply (simp only: zdiv_zminus_zminus diff_minus minus_add_distrib [symmetric])  haftmann@33340  962 apply (simp_all add: algebra_simps)  haftmann@33340  963 apply (simp only: ab_diff_minus minus_add_distrib [symmetric] number_of_Min zdiv_zminus_zminus)  wenzelm@23164  964 done  wenzelm@23164  965 huffman@26086  966 lemma zdiv_number_of_Bit0 [simp]:  huffman@26086  967  "number_of (Int.Bit0 v) div number_of (Int.Bit0 w) =  huffman@26086  968  number_of v div (number_of w :: int)"  haftmann@33340  969 by (simp only: number_of_eq numeral_simps) (simp add: mult_2 [symmetric])  huffman@26086  970 huffman@26086  971 lemma zdiv_number_of_Bit1 [simp]:  huffman@26086  972  "number_of (Int.Bit1 v) div number_of (Int.Bit0 w) =  huffman@26086  973  (if (0::int) \ number_of w  wenzelm@23164  974  then number_of v div (number_of w)  wenzelm@23164  975  else (number_of v + (1::int)) div (number_of w))"  wenzelm@23164  976 apply (simp only: number_of_eq numeral_simps UNIV_I split: split_if)  haftmann@33340  977 apply (simp add: pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac mult_2 [symmetric])  wenzelm@23164  978 done  wenzelm@23164  979 wenzelm@23164  980 wenzelm@23164  981 subsection{*Computing mod by Shifting (proofs resemble those for div)*}  wenzelm@23164  982 wenzelm@23164  983 lemma pos_zmod_mult_2:  haftmann@33340  984  fixes a b :: int  haftmann@33340  985  assumes "0 \ a"  haftmann@33340  986  shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)"  haftmann@33340  987 proof (cases "0 < a")  haftmann@33340  988  case False with assms show ?thesis by simp  haftmann@33340  989 next  haftmann@33340  990  case True  haftmann@33340  991  then have "b mod a < a" by (rule pos_mod_bound)  haftmann@33340  992  then have "1 + b mod a \ a" by simp  haftmann@33340  993  then have A: "2 * (1 + b mod a) \ 2 * a" by simp  haftmann@33340  994  from 0 < a have "0 \ b mod a" by (rule pos_mod_sign)  haftmann@33340  995  then have B: "0 \ 1 + 2 * (b mod a)" by simp  haftmann@33340  996  have "((1\int) mod ((2\int) * a) + (2\int) * b mod ((2\int) * a)) mod ((2\int) * a) = (1\int) + (2\int) * (b mod a)"  haftmann@33340  997  using 0 < a and A  haftmann@33340  998  by (auto simp add: mod_mult_mult1 mod_pos_pos_trivial ring_distribs intro!: mod_pos_pos_trivial B)  haftmann@33340  999  then show ?thesis by (subst mod_add_eq)  haftmann@33340  1000 qed  wenzelm@23164  1001 wenzelm@23164  1002 lemma neg_zmod_mult_2:  haftmann@33340  1003  fixes a b :: int  haftmann@33340  1004  assumes "a \ 0"  haftmann@33340  1005  shows "(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1"  haftmann@33340  1006 proof -  haftmann@33340  1007  from assms have "0 \ - a" by auto  haftmann@33340  1008  then have "(1 + 2 * (- b - 1)) mod (2 * (- a)) = 1 + 2 * ((- b - 1) mod (- a))"  haftmann@33340  1009  by (rule pos_zmod_mult_2)  haftmann@33340  1010  then show ?thesis by (simp add: zmod_zminus2 algebra_simps)  haftmann@33340  1011  (simp add: diff_minus add_ac)  haftmann@33340  1012 qed  wenzelm@23164  1013 huffman@26086  1014 lemma zmod_number_of_Bit0 [simp]:  huffman@26086  1015  "number_of (Int.Bit0 v) mod number_of (Int.Bit0 w) =  huffman@26086  1016  (2::int) * (number_of v mod number_of w)"  huffman@26086  1017 apply (simp only: number_of_eq numeral_simps)  haftmann@30930  1018 apply (simp add: mod_mult_mult1 pos_zmod_mult_2  haftmann@33340  1019  neg_zmod_mult_2 add_ac mult_2 [symmetric])  huffman@26086  1020 done  huffman@26086  1021 huffman@26086  1022 lemma zmod_number_of_Bit1 [simp]:  huffman@26086  1023  "number_of (Int.Bit1 v) mod number_of (Int.Bit0 w) =  huffman@26086  1024  (if (0::int) \ number_of w  wenzelm@23164  1025  then 2 * (number_of v mod number_of w) + 1  wenzelm@23164  1026  else 2 * ((number_of v + (1::int)) mod number_of w) - 1)"  huffman@26086  1027 apply (simp only: number_of_eq numeral_simps)  haftmann@30930  1028 apply (simp add: mod_mult_mult1 pos_zmod_mult_2  haftmann@33340  1029  neg_zmod_mult_2 add_ac mult_2 [symmetric])  wenzelm@23164  1030 done  wenzelm@23164  1031 wenzelm@23164  1032 wenzelm@23164  1033 subsection{*Quotients of Signs*}  wenzelm@23164  1034 wenzelm@23164  1035 lemma div_neg_pos_less0: "[| a < (0::int); 0 < b |] ==> a div b < 0"  wenzelm@23164  1036 apply (subgoal_tac "a div b \ -1", force)  wenzelm@23164  1037 apply (rule order_trans)  wenzelm@23164  1038 apply (rule_tac a' = "-1" in zdiv_mono1)  nipkow@29948  1039 apply (auto simp add: div_eq_minus1)  wenzelm@23164  1040 done  wenzelm@23164  1041 nipkow@30323  1042 lemma div_nonneg_neg_le0: "[| (0::int) \ a; b < 0 |] ==> a div b \ 0"  wenzelm@23164  1043 by (drule zdiv_mono1_neg, auto)  wenzelm@23164  1044 nipkow@30323  1045 lemma div_nonpos_pos_le0: "[| (a::int) \ 0; b > 0 |] ==> a div b \ 0"  nipkow@30323  1046 by (drule zdiv_mono1, auto)  nipkow@30323  1047 wenzelm@23164  1048 lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \ a div b) = (0 \ a)"  wenzelm@23164  1049 apply auto  wenzelm@23164  1050 apply (drule_tac [2] zdiv_mono1)  wenzelm@23164  1051 apply (auto simp add: linorder_neq_iff)  wenzelm@23164  1052 apply (simp (no_asm_use) add: linorder_not_less [symmetric])  wenzelm@23164  1053 apply (blast intro: div_neg_pos_less0)  wenzelm@23164  1054 done  wenzelm@23164  1055 wenzelm@23164  1056 lemma neg_imp_zdiv_nonneg_iff:  wenzelm@23164  1057  "b < (0::int) ==> (0 \ a div b) = (a \ (0::int))"  wenzelm@23164  1058 apply (subst zdiv_zminus_zminus [symmetric])  wenzelm@23164  1059 apply (subst pos_imp_zdiv_nonneg_iff, auto)  wenzelm@23164  1060 done  wenzelm@23164  1061 wenzelm@23164  1062 (*But not (a div b \ 0 iff a\0); consider a=1, b=2 when a div b = 0.*)  wenzelm@23164  1063 lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)"  wenzelm@23164  1064 by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff)  wenzelm@23164  1065 wenzelm@23164  1066 (*Again the law fails for \: consider a = -1, b = -2 when a div b = 0*)  wenzelm@23164  1067 lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)"  wenzelm@23164  1068 by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)  wenzelm@23164  1069 wenzelm@23164  1070 wenzelm@23164  1071 subsection {* The Divides Relation *}  wenzelm@23164  1072 wenzelm@23164  1073 lemmas zdvd_iff_zmod_eq_0_number_of [simp] =  nipkow@30042  1074  dvd_eq_mod_eq_0 [of "number_of x::int" "number_of y::int", standard]  wenzelm@23164  1075 wenzelm@23164  1076 lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"  huffman@31662  1077  by (rule dvd_mod) (* TODO: remove *)  wenzelm@23164  1078 wenzelm@23164  1079 lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"  huffman@31662  1080  by (rule dvd_mod_imp_dvd) (* TODO: remove *)  wenzelm@23164  1081 wenzelm@23164  1082 lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"  wenzelm@23164  1083  using zmod_zdiv_equality[where a="m" and b="n"]  nipkow@29667  1084  by (simp add: algebra_simps)  wenzelm@23164  1085 wenzelm@23164  1086 lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"  wenzelm@23164  1087 apply (induct "y", auto)  wenzelm@23164  1088 apply (rule zmod_zmult1_eq [THEN trans])  wenzelm@23164  1089 apply (simp (no_asm_simp))  nipkow@29948  1090 apply (rule mod_mult_eq [symmetric])  wenzelm@23164  1091 done  wenzelm@23164  1092 huffman@23365  1093 lemma zdiv_int: "int (a div b) = (int a) div (int b)"  wenzelm@23164  1094 apply (subst split_div, auto)  wenzelm@23164  1095 apply (subst split_zdiv, auto)  huffman@23365  1096 apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in IntDiv.unique_quotient)  haftmann@33340  1097 apply (auto simp add: IntDiv.divmod_int_rel_def of_nat_mult)  wenzelm@23164  1098 done  wenzelm@23164  1099 wenzelm@23164  1100 lemma zmod_int: "int (a mod b) = (int a) mod (int b)"  huffman@23365  1101 apply (subst split_mod, auto)  huffman@23365  1102 apply (subst split_zmod, auto)  huffman@23365  1103 apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia  huffman@23365  1104  in unique_remainder)  haftmann@33340  1105 apply (auto simp add: IntDiv.divmod_int_rel_def of_nat_mult)  huffman@23365  1106 done  wenzelm@23164  1107 nipkow@30180  1108 lemma abs_div: "(y::int) dvd x \ abs (x div y) = abs x div abs y"  nipkow@30180  1109 by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)  nipkow@30180  1110 haftmann@33318  1111 lemma zdvd_mult_div_cancel:"(n::int) dvd m \ n * (m div n) = m"  haftmann@33318  1112 apply (subgoal_tac "m mod n = 0")  haftmann@33318  1113  apply (simp add: zmult_div_cancel)  haftmann@33318  1114 apply (simp only: dvd_eq_mod_eq_0)  haftmann@33318  1115 done  haftmann@33318  1116 wenzelm@23164  1117 text{*Suggested by Matthias Daum*}  wenzelm@23164  1118 lemma int_power_div_base:  wenzelm@23164  1119  "\0 < m; 0 < k\ \ k ^ m div k = (k::int) ^ (m - Suc 0)"  huffman@30079  1120 apply (subgoal_tac "k ^ m = k ^ ((m - Suc 0) + Suc 0)")  wenzelm@23164  1121  apply (erule ssubst)  wenzelm@23164  1122  apply (simp only: power_add)  wenzelm@23164  1123  apply simp_all  wenzelm@23164  1124 done  wenzelm@23164  1125 haftmann@23853  1126 text {* by Brian Huffman *}  haftmann@23853  1127 lemma zminus_zmod: "- ((x::int) mod m) mod m = - x mod m"  huffman@29405  1128 by (rule mod_minus_eq [symmetric])  haftmann@23853  1129 haftmann@23853  1130 lemma zdiff_zmod_left: "(x mod m - y) mod m = (x - y) mod (m::int)"  huffman@29405  1131 by (rule mod_diff_left_eq [symmetric])  haftmann@23853  1132 haftmann@23853  1133 lemma zdiff_zmod_right: "(x - y mod m) mod m = (x - y) mod (m::int)"  huffman@29405  1134 by (rule mod_diff_right_eq [symmetric])  haftmann@23853  1135 haftmann@23853  1136 lemmas zmod_simps =  nipkow@30034  1137  mod_add_left_eq [symmetric]  nipkow@30034  1138  mod_add_right_eq [symmetric]  haftmann@30930  1139  zmod_zmult1_eq [symmetric]  haftmann@30930  1140  mod_mult_left_eq [symmetric]  haftmann@30930  1141  zpower_zmod  haftmann@23853  1142  zminus_zmod zdiff_zmod_left zdiff_zmod_right  haftmann@23853  1143 huffman@29045  1144 text {* Distributive laws for function @{text nat}. *}  huffman@29045  1145 huffman@29045  1146 lemma nat_div_distrib: "0 \ x \ nat (x div y) = nat x div nat y"  huffman@29045  1147 apply (rule linorder_cases [of y 0])  huffman@29045  1148 apply (simp add: div_nonneg_neg_le0)  huffman@29045  1149 apply simp  huffman@29045  1150 apply (simp add: nat_eq_iff pos_imp_zdiv_nonneg_iff zdiv_int)  huffman@29045  1151 done  huffman@29045  1152 huffman@29045  1153 (*Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't*)  huffman@29045  1154 lemma nat_mod_distrib:  huffman@29045  1155  "\0 \ x; 0 \ y\ \ nat (x mod y) = nat x mod nat y"  huffman@29045  1156 apply (case_tac "y = 0", simp add: DIVISION_BY_ZERO)  huffman@29045  1157 apply (simp add: nat_eq_iff zmod_int)  huffman@29045  1158 done  huffman@29045  1159 huffman@29045  1160 text{*Suggested by Matthias Daum*}  huffman@29045  1161 lemma int_div_less_self: "\0 < x; 1 < k\ \ x div k < (x::int)"  huffman@29045  1162 apply (subgoal_tac "nat x div nat k < nat x")  huffman@29045  1163  apply (simp (asm_lr) add: nat_div_distrib [symmetric])  huffman@29045  1164 apply (rule Divides.div_less_dividend, simp_all)  huffman@29045  1165 done  huffman@29045  1166 haftmann@23853  1167 text {* code generator setup *}  wenzelm@23164  1168 haftmann@26507  1169 context ring_1  haftmann@26507  1170 begin  haftmann@26507  1171 haftmann@28562  1172 lemma of_int_num [code]:  haftmann@26507  1173  "of_int k = (if k = 0 then 0 else if k < 0 then  haftmann@26507  1174  - of_int (- k) else let  haftmann@33340  1175  (l, m) = divmod_int k 2;  haftmann@26507  1176  l' = of_int l  haftmann@26507  1177  in if m = 0 then l' + l' else l' + l' + 1)"  haftmann@26507  1178 proof -  haftmann@26507  1179  have aux1: "k mod (2\int) \ (0\int) \  haftmann@26507  1180  of_int k = of_int (k div 2 * 2 + 1)"  haftmann@26507  1181  proof -  haftmann@26507  1182  have "k mod 2 < 2" by (auto intro: pos_mod_bound)  haftmann@26507  1183  moreover have "0 \ k mod 2" by (auto intro: pos_mod_sign)  haftmann@26507  1184  moreover assume "k mod 2 \ 0"  haftmann@26507  1185  ultimately have "k mod 2 = 1" by arith  haftmann@26507  1186  moreover have "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp  haftmann@26507  1187  ultimately show ?thesis by auto  haftmann@26507  1188  qed  haftmann@26507  1189  have aux2: "\x. of_int 2 * x = x + x"  haftmann@26507  1190  proof -  haftmann@26507  1191  fix x  haftmann@26507  1192  have int2: "(2::int) = 1 + 1" by arith  haftmann@26507  1193  show "of_int 2 * x = x + x"  haftmann@26507  1194  unfolding int2 of_int_add left_distrib by simp  haftmann@26507  1195  qed  haftmann@26507  1196  have aux3: "\x. x * of_int 2 = x + x"  haftmann@26507  1197  proof -  haftmann@26507  1198  fix x  haftmann@26507  1199  have int2: "(2::int) = 1 + 1" by arith  haftmann@26507  1200  show "x * of_int 2 = x + x"  haftmann@26507  1201  unfolding int2 of_int_add right_distrib by simp  haftmann@26507  1202  qed  haftmann@33340  1203  from aux1 show ?thesis by (auto simp add: divmod_int_mod_div Let_def aux2 aux3)  haftmann@26507  1204 qed  haftmann@26507  1205 haftmann@26507  1206 end  haftmann@26507  1207 chaieb@27667  1208 lemma zmod_eq_dvd_iff: "(x::int) mod n = y mod n \ n dvd x - y"  chaieb@27667  1209 proof  chaieb@27667  1210  assume H: "x mod n = y mod n"  chaieb@27667  1211  hence "x mod n - y mod n = 0" by simp  chaieb@27667  1212  hence "(x mod n - y mod n) mod n = 0" by simp  nipkow@30034  1213  hence "(x - y) mod n = 0" by (simp add: mod_diff_eq[symmetric])  nipkow@30042  1214  thus "n dvd x - y" by (simp add: dvd_eq_mod_eq_0)  chaieb@27667  1215 next  chaieb@27667  1216  assume H: "n dvd x - y"  chaieb@27667  1217  then obtain k where k: "x-y = n*k" unfolding dvd_def by blast  chaieb@27667  1218  hence "x = n*k + y" by simp  chaieb@27667  1219  hence "x mod n = (n*k + y) mod n" by simp  nipkow@30034  1220  thus "x mod n = y mod n" by (simp add: mod_add_left_eq)  chaieb@27667  1221 qed  chaieb@27667  1222 chaieb@27667  1223 lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \ x"  chaieb@27667  1224  shows "\q. x = y + n * q"  chaieb@27667  1225 proof-  chaieb@27667  1226  from xy have th: "int x - int y = int (x - y)" by simp  chaieb@27667  1227  from xyn have "int x mod int n = int y mod int n"  chaieb@27667  1228  by (simp add: zmod_int[symmetric])  chaieb@27667  1229  hence "int n dvd int x - int y" by (simp only: zmod_eq_dvd_iff[symmetric])  chaieb@27667  1230  hence "n dvd x - y" by (simp add: th zdvd_int)  chaieb@27667  1231  then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith  chaieb@27667  1232 qed  chaieb@27667  1233 chaieb@27667  1234 lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \ (\q1 q2. x + n * q1 = y + n * q2)"  chaieb@27667  1235  (is "?lhs = ?rhs")  chaieb@27667  1236 proof  chaieb@27667  1237  assume H: "x mod n = y mod n"  chaieb@27667  1238  {assume xy: "x \ y"  chaieb@27667  1239  from H have th: "y mod n = x mod n" by simp  chaieb@27667  1240  from nat_mod_eq_lemma[OF th xy] have ?rhs  chaieb@27667  1241  apply clarify apply (rule_tac x="q" in exI) by (rule exI[where x="0"], simp)}  chaieb@27667  1242  moreover  chaieb@27667  1243  {assume xy: "y \ x"  chaieb@27667  1244  from nat_mod_eq_lemma[OF H xy] have ?rhs  chaieb@27667  1245  apply clarify apply (rule_tac x="0" in exI) by (rule_tac x="q" in exI, simp)}  chaieb@27667  1246  ultimately show ?rhs using linear[of x y] by blast  chaieb@27667  1247 next  chaieb@27667  1248  assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast  chaieb@27667  1249  hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp  chaieb@27667  1250  thus ?lhs by simp  chaieb@27667  1251 qed  chaieb@27667  1252 haftmann@33296  1253 lemma div_nat_number_of [simp]:  haftmann@33296  1254  "(number_of v :: nat) div number_of v' =  haftmann@33296  1255  (if neg (number_of v :: int) then 0  haftmann@33296  1256  else nat (number_of v div number_of v'))"  haftmann@33296  1257  unfolding nat_number_of_def number_of_is_id neg_def  haftmann@33296  1258  by (simp add: nat_div_distrib)  haftmann@33296  1259 haftmann@33296  1260 lemma one_div_nat_number_of [simp]:  haftmann@33296  1261  "Suc 0 div number_of v' = nat (1 div number_of v')"  haftmann@33296  1262 by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric])  haftmann@33296  1263 haftmann@33296  1264 lemma mod_nat_number_of [simp]:  haftmann@33296  1265  "(number_of v :: nat) mod number_of v' =  haftmann@33296  1266  (if neg (number_of v :: int) then 0  haftmann@33296  1267  else if neg (number_of v' :: int) then number_of v  haftmann@33296  1268  else nat (number_of v mod number_of v'))"  haftmann@33296  1269  unfolding nat_number_of_def number_of_is_id neg_def  haftmann@33296  1270  by (simp add: nat_mod_distrib)  haftmann@33296  1271 haftmann@33296  1272 lemma one_mod_nat_number_of [simp]:  haftmann@33296  1273  "Suc 0 mod number_of v' =  haftmann@33296  1274  (if neg (number_of v' :: int) then Suc 0  haftmann@33296  1275  else nat (1 mod number_of v'))"  haftmann@33296  1276 by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric])  haftmann@33296  1277 haftmann@33296  1278 lemmas dvd_eq_mod_eq_0_number_of =  haftmann@33296  1279  dvd_eq_mod_eq_0 [of "number_of x" "number_of y", standard]  haftmann@33296  1280 haftmann@33296  1281 declare dvd_eq_mod_eq_0_number_of [simp]  haftmann@33296  1282 haftmann@29936  1283 haftmann@33318  1284 subsection {* Transfer setup *}  haftmann@33318  1285 haftmann@33318  1286 lemma transfer_nat_int_functions:  haftmann@33318  1287  "(x::int) >= 0 \ y >= 0 \ (nat x) div (nat y) = nat (x div y)"  haftmann@33318  1288  "(x::int) >= 0 \ y >= 0 \ (nat x) mod (nat y) = nat (x mod y)"  haftmann@33318  1289  by (auto simp add: nat_div_distrib nat_mod_distrib)  haftmann@33318  1290 haftmann@33318  1291 lemma transfer_nat_int_function_closures:  haftmann@33318  1292  "(x::int) >= 0 \ y >= 0 \ x div y >= 0"  haftmann@33318  1293  "(x::int) >= 0 \ y >= 0 \ x mod y >= 0"  haftmann@33318  1294  apply (cases "y = 0")  haftmann@33318  1295  apply (auto simp add: pos_imp_zdiv_nonneg_iff)  haftmann@33318  1296  apply (cases "y = 0")  haftmann@33318  1297  apply auto  haftmann@33318  1298 done  haftmann@33318  1299 haftmann@33318  1300 declare TransferMorphism_nat_int[transfer add return:  haftmann@33318  1301  transfer_nat_int_functions  haftmann@33318  1302  transfer_nat_int_function_closures  haftmann@33318  1303 ]  haftmann@33318  1304 haftmann@33318  1305 lemma transfer_int_nat_functions:  haftmann@33318  1306  "(int x) div (int y) = int (x div y)"  haftmann@33318  1307  "(int x) mod (int y) = int (x mod y)"  haftmann@33318  1308  by (auto simp add: zdiv_int zmod_int)  haftmann@33318  1309 haftmann@33318  1310 lemma transfer_int_nat_function_closures:  haftmann@33318  1311  "is_nat x \ is_nat y \ is_nat (x div y)"  haftmann@33318  1312  "is_nat x \ is_nat y \ is_nat (x mod y)"  haftmann@33318  1313  by (simp_all only: is_nat_def transfer_nat_int_function_closures)  haftmann@33318  1314 haftmann@33318  1315 declare TransferMorphism_int_nat[transfer add return:  haftmann@33318  1316  transfer_int_nat_functions  haftmann@33318  1317  transfer_int_nat_function_closures  haftmann@33318  1318 ]  haftmann@33318  1319 haftmann@33318  1320 haftmann@29936  1321 subsection {* Code generation *}  haftmann@29936  1322 haftmann@29936  1323 definition pdivmod :: "int \ int \ int \ int" where  haftmann@29936  1324  "pdivmod k l = (\k\ div \l\, \k\ mod \l$$"  haftmann@29936  1325 haftmann@29936  1326 lemma pdivmod_posDivAlg [code]:  haftmann@29936  1327  "pdivmod k l = (if l = 0 then (0, \k\) else posDivAlg \k\ \l\)"  haftmann@29936  1328 by (subst posDivAlg_div_mod) (simp_all add: pdivmod_def)  haftmann@29936  1329 haftmann@33340  1330 lemma divmod_int_pdivmod: "divmod_int k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else  haftmann@29936  1331  apsnd ((op *) (sgn l)) (if 0 < l \ 0 \ k \ l < 0 \ k < 0  haftmann@29936  1332  then pdivmod k l  haftmann@29936  1333  else (let (r, s) = pdivmod k l in  haftmann@29936  1334  if s = 0 then (- r, 0) else (- r - 1, \l\ - s))))"  haftmann@29936  1335 proof -  haftmann@29936  1336  have aux: "\q::int. - k = l * q \ k = l * - q" by auto  haftmann@29936  1337  show ?thesis  haftmann@33340  1338  by (simp add: divmod_int_mod_div pdivmod_def)  haftmann@29936  1339  (auto simp add: aux not_less not_le zdiv_zminus1_eq_if  haftmann@29936  1340  zmod_zminus1_eq_if zdiv_zminus2_eq_if zmod_zminus2_eq_if)  haftmann@29936  1341 qed  haftmann@29936  1342 haftmann@33340  1343 lemma divmod_int_code [code]: "divmod_int k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else  haftmann@29936  1344  apsnd ((op *) (sgn l)) (if sgn k = sgn l  haftmann@29936  1345  then pdivmod k l  haftmann@29936  1346  else (let (r, s) = pdivmod k l in  haftmann@29936  1347  if s = 0 then (- r, 0) else (- r - 1, \l\ - s))))"  haftmann@29936  1348 proof -  haftmann@29936  1349  have "k \ 0 \ l \ 0 \ 0 < l \ 0 \ k \ l < 0 \ k < 0 \ sgn k = sgn l"  haftmann@29936  1350  by (auto simp add: not_less sgn_if)  haftmann@33340  1351  then show ?thesis by (simp add: divmod_int_pdivmod)  haftmann@29936  1352 qed  haftmann@29936  1353 wenzelm@23164  1354 code_modulename SML  wenzelm@23164  1355  IntDiv Integer  wenzelm@23164  1356 wenzelm@23164  1357 code_modulename OCaml  wenzelm@23164  1358  IntDiv Integer  wenzelm@23164  1359 wenzelm@23164  1360 code_modulename Haskell  haftmann@24195  1361  IntDiv Integer  wenzelm@23164  1362 haftmann@33340  1363 haftmann@33340  1364 haftmann@33340  1365 subsection {* Proof Tools setup; Combination and Cancellation Simprocs *}  haftmann@33340  1366 haftmann@33340  1367 declare split_div[of _ _ "number_of k", standard, arith_split]  haftmann@33340  1368 declare split_mod[of _ _ "number_of k", standard, arith_split]  haftmann@33340  1369 haftmann@33340  1370 haftmann@33340  1371 subsubsection{*For @{text combine_numerals}*}  haftmann@33340  1372 haftmann@33340  1373 lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"  haftmann@33340  1374 by (simp add: add_mult_distrib)  haftmann@33340  1375 haftmann@33340  1376 haftmann@33340  1377 subsubsection{*For @{text cancel_numerals}*}  haftmann@33340  1378 haftmann@33340  1379 lemma nat_diff_add_eq1:  haftmann@33340  1380  "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"  haftmann@33340  1381 by (simp split add: nat_diff_split add: add_mult_distrib)  haftmann@33340  1382 haftmann@33340  1383 lemma nat_diff_add_eq2:  haftmann@33340  1384  "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"  haftmann@33340  1385 by (simp split add: nat_diff_split add: add_mult_distrib)  haftmann@33340  1386 haftmann@33340  1387 lemma nat_eq_add_iff1:  haftmann@33340  1388  "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)"  haftmann@33340  1389 by (auto split add: nat_diff_split simp add: add_mult_distrib)  haftmann@33340  1390 haftmann@33340  1391 lemma nat_eq_add_iff2:  haftmann@33340  1392  "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)"  haftmann@33340  1393 by (auto split add: nat_diff_split simp add: add_mult_distrib)  haftmann@33340  1394 haftmann@33340  1395 lemma nat_less_add_iff1:  haftmann@33340  1396  "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)"  haftmann@33340  1397 by (auto split add: nat_diff_split simp add: add_mult_distrib)  haftmann@33340  1398 haftmann@33340  1399 lemma nat_less_add_iff2:  haftmann@33340  1400  "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)"  haftmann@33340  1401 by (auto split add: nat_diff_split simp add: add_mult_distrib)  haftmann@33340  1402 haftmann@33340  1403 lemma nat_le_add_iff1:  haftmann@33340  1404  "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"  haftmann@33340  1405 by (auto split add: nat_diff_split simp add: add_mult_distrib)  haftmann@33340  1406 haftmann@33340  1407 lemma nat_le_add_iff2:  haftmann@33340  1408  "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"  haftmann@33340  1409 by (auto split add: nat_diff_split simp add: add_mult_distrib)  haftmann@33340  1410 haftmann@33340  1411 haftmann@33340  1412 subsubsection{*For @{text cancel_numeral_factors} *}  haftmann@33340  1413 haftmann@33340  1414 lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"  haftmann@33340  1415 by auto  haftmann@33340  1416 haftmann@33340  1417 lemma nat_mult_less_cancel1: "(0::nat) < k ==> (k*m < k*n) = (m (k*m = k*n) = (m=n)"  haftmann@33340  1421 by auto  haftmann@33340  1422 haftmann@33340  1423 lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)"  haftmann@33340  1424 by auto  haftmann@33340  1425 haftmann@33340  1426 lemma nat_mult_dvd_cancel_disj[simp]:  haftmann@33340  1427  "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))"  haftmann@33340  1428 by(auto simp: dvd_eq_mod_eq_0 mod_mult_distrib2[symmetric])  haftmann@33340  1429 haftmann@33340  1430 lemma nat_mult_dvd_cancel1: "0 < k \ (k*m) dvd (k*n::nat) = (m dvd n)"  haftmann@33340  1431 by(auto)  haftmann@33340  1432 haftmann@33340  1433 haftmann@33340  1434 subsubsection{*For @{text cancel_factor} *}  haftmann@33340  1435 haftmann@33340  1436 lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)"  haftmann@33340  1437 by auto  haftmann@33340  1438 haftmann@33340  1439 lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1},  haftmann@33340  1457  @{thm nat_0}, @{thm nat_1},  haftmann@33340  1458  @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},  haftmann@33340  1459  @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},  haftmann@33340  1460  @{thm le_Suc_number_of}, @{thm le_number_of_Suc},  haftmann@33340  1461  @{thm less_Suc_number_of}, @{thm less_number_of_Suc},  haftmann@33340  1462  @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},  haftmann@33340  1463  @{thm mult_Suc}, @{thm mult_Suc_right},  haftmann@33340  1464  @{thm add_Suc}, @{thm add_Suc_right},  haftmann@33340  1465  @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},  haftmann@33340  1466  @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of},  haftmann@33340  1467  @{thm if_True}, @{thm if_False}])  haftmann@33340  1468  #> Lin_Arith.add_simprocs (Numeral_Simprocs.assoc_fold_simproc  haftmann@33340  1469  :: Numeral_Simprocs.combine_numerals  haftmann@33340  1470  :: Numeral_Simprocs.cancel_numerals)  haftmann@33340  1471  #> Lin_Arith.add_simprocs (Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals))  haftmann@33340  1472 *}  haftmann@33340  1473 wenzelm@23164  1474 end `