1 (* Title: ZF/int_arith.ML
4 Copyright 2000 University of Cambridge
6 Simprocs for linear arithmetic.
10 (** To simplify inequalities involving integer negation and literals,
14 Addsimps [OldGoals.inst "y" "integ_of(?w)" @{thm zminus_equation},
15 OldGoals.inst "x" "integ_of(?w)" @{thm equation_zminus}];
17 AddIffs [OldGoals.inst "y" "integ_of(?w)" @{thm zminus_zless},
18 OldGoals.inst "x" "integ_of(?w)" @{thm zless_zminus}];
20 AddIffs [OldGoals.inst "y" "integ_of(?w)" @{thm zminus_zle},
21 OldGoals.inst "x" "integ_of(?w)" @{thm zle_zminus}];
23 Addsimps [OldGoals.inst "s" "integ_of(?w)" @{thm Let_def}];
25 (*** Simprocs for numeric literals ***)
27 (** Combining of literal coefficients in sums of products **)
29 Goal "(x $< y) <-> (x$-y $< #0)";
30 by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
31 qed "zless_iff_zdiff_zless_0";
33 Goal "[| x: int; y: int |] ==> (x = y) <-> (x$-y = #0)";
34 by (asm_simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
35 qed "eq_iff_zdiff_eq_0";
37 Goal "(x $<= y) <-> (x$-y $<= #0)";
38 by (asm_simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
39 qed "zle_iff_zdiff_zle_0";
42 (** For combine_numerals **)
44 Goal "i$*u $+ (j$*u $+ k) = (i$+j)$*u $+ k";
45 by (simp_tac (simpset() addsimps [@{thm zadd_zmult_distrib}]@ @{thms zadd_ac}) 1);
46 qed "left_zadd_zmult_distrib";
49 (** For cancel_numerals **)
51 val rel_iff_rel_0_rls = map (OldGoals.inst "y" "?u$+?v")
52 [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
53 zle_iff_zdiff_zle_0] @
54 map (OldGoals.inst "y" "n")
55 [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
58 Goal "(i$*u $+ m = j$*u $+ n) <-> ((i$-j)$*u $+ m = intify(n))";
59 by (simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]) 1);
60 by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
61 by (simp_tac (simpset() addsimps @{thms zadd_ac}) 1);
64 Goal "(i$*u $+ m = j$*u $+ n) <-> (intify(m) = (j$-i)$*u $+ n)";
65 by (simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]) 1);
66 by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
67 by (simp_tac (simpset() addsimps @{thms zadd_ac}) 1);
70 Goal "(i$*u $+ m $< j$*u $+ n) <-> ((i$-j)$*u $+ m $< n)";
71 by (asm_simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]@
72 @{thms zadd_ac} @ rel_iff_rel_0_rls) 1);
75 Goal "(i$*u $+ m $< j$*u $+ n) <-> (m $< (j$-i)$*u $+ n)";
76 by (asm_simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]@
77 @{thms zadd_ac} @ rel_iff_rel_0_rls) 1);
80 Goal "(i$*u $+ m $<= j$*u $+ n) <-> ((i$-j)$*u $+ m $<= n)";
81 by (simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]) 1);
82 by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
83 by (simp_tac (simpset() addsimps @{thms zadd_ac}) 1);
86 Goal "(i$*u $+ m $<= j$*u $+ n) <-> (m $<= (j$-i)$*u $+ n)";
87 by (simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]) 1);
88 by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
89 by (simp_tac (simpset() addsimps @{thms zadd_ac}) 1);
93 structure Int_Numeral_Simprocs =
98 val integ_of_const = Const (@{const_name "Bin.integ_of"}, @{typ "i => i"});
100 fun mk_numeral n = integ_of_const $ NumeralSyntax.mk_bin n;
102 (*Decodes a binary INTEGER*)
103 fun dest_numeral (Const(@{const_name "Bin.integ_of"}, _) $ w) =
104 (NumeralSyntax.dest_bin w
105 handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
106 | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
108 fun find_first_numeral past (t::terms) =
109 ((dest_numeral t, rev past @ terms)
110 handle TERM _ => find_first_numeral (t::past) terms)
111 | find_first_numeral past [] = raise TERM("find_first_numeral", []);
113 val zero = mk_numeral 0;
114 val mk_plus = FOLogic.mk_binop @{const_name "zadd"};
116 val zminus_const = Const (@{const_name "zminus"}, @{typ "i => i"});
118 (*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
120 | mk_sum [t,u] = mk_plus (t, u)
121 | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
123 (*this version ALWAYS includes a trailing zero*)
124 fun long_mk_sum [] = zero
125 | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
127 val dest_plus = FOLogic.dest_bin @{const_name "zadd"} @{typ i};
129 (*decompose additions AND subtractions as a sum*)
130 fun dest_summing (pos, Const (@{const_name "zadd"}, _) $ t $ u, ts) =
131 dest_summing (pos, t, dest_summing (pos, u, ts))
132 | dest_summing (pos, Const (@{const_name "zdiff"}, _) $ t $ u, ts) =
133 dest_summing (pos, t, dest_summing (not pos, u, ts))
134 | dest_summing (pos, t, ts) =
135 if pos then t::ts else zminus_const$t :: ts;
137 fun dest_sum t = dest_summing (true, t, []);
139 val mk_diff = FOLogic.mk_binop @{const_name "zdiff"};
140 val dest_diff = FOLogic.dest_bin @{const_name "zdiff"} @{typ i};
142 val one = mk_numeral 1;
143 val mk_times = FOLogic.mk_binop @{const_name "zmult"};
147 | mk_prod (t :: ts) = if t = one then mk_prod ts
148 else mk_times (t, mk_prod ts);
150 val dest_times = FOLogic.dest_bin @{const_name "zmult"} @{typ i};
153 let val (t,u) = dest_times t
154 in dest_prod t @ dest_prod u end
155 handle TERM _ => [t];
157 (*DON'T do the obvious simplifications; that would create special cases*)
158 fun mk_coeff (k, t) = mk_times (mk_numeral k, t);
160 (*Express t as a product of (possibly) a numeral with other sorted terms*)
161 fun dest_coeff sign (Const (@{const_name "zminus"}, _) $ t) = dest_coeff (~sign) t
162 | dest_coeff sign t =
163 let val ts = sort Term.term_ord (dest_prod t)
164 val (n, ts') = find_first_numeral [] ts
165 handle TERM _ => (1, ts)
166 in (sign*n, mk_prod ts') end;
168 (*Find first coefficient-term THAT MATCHES u*)
169 fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
170 | find_first_coeff past u (t::terms) =
171 let val (n,u') = dest_coeff 1 t
172 in if u aconv u' then (n, rev past @ terms)
173 else find_first_coeff (t::past) u terms
175 handle TERM _ => find_first_coeff (t::past) u terms;
178 (*Simplify #1*n and n*#1 to n*)
179 val add_0s = [@{thm zadd_0_intify}, @{thm zadd_0_right_intify}];
181 val mult_1s = [@{thm zmult_1_intify}, @{thm zmult_1_right_intify},
182 @{thm zmult_minus1}, @{thm zmult_minus1_right}];
184 val tc_rules = [@{thm integ_of_type}, @{thm intify_in_int},
185 @{thm int_of_type}, @{thm zadd_type}, @{thm zdiff_type}, @{thm zmult_type}] @
187 val intifys = [@{thm intify_ident}, @{thm zadd_intify1}, @{thm zadd_intify2},
188 @{thm zdiff_intify1}, @{thm zdiff_intify2}, @{thm zmult_intify1}, @{thm zmult_intify2},
189 @{thm zless_intify1}, @{thm zless_intify2}, @{thm zle_intify1}, @{thm zle_intify2}];
191 (*To perform binary arithmetic*)
192 val bin_simps = [@{thm add_integ_of_left}] @ @{thms bin_arith_simps} @ @{thms bin_rel_simps};
194 (*To evaluate binary negations of coefficients*)
195 val zminus_simps = @{thms NCons_simps} @
196 [@{thm integ_of_minus} RS sym,
197 @{thm bin_minus_1}, @{thm bin_minus_0}, @{thm bin_minus_Pls}, @{thm bin_minus_Min},
198 @{thm bin_pred_1}, @{thm bin_pred_0}, @{thm bin_pred_Pls}, @{thm bin_pred_Min}];
200 (*To let us treat subtraction as addition*)
201 val diff_simps = [@{thm zdiff_def}, @{thm zminus_zadd_distrib}, @{thm zminus_zminus}];
203 (*push the unary minus down: - x * y = x * - y *)
204 val int_minus_mult_eq_1_to_2 =
205 [@{thm zmult_zminus}, @{thm zmult_zminus_right} RS sym] MRS trans |> standard;
207 (*to extract again any uncancelled minuses*)
208 val int_minus_from_mult_simps =
209 [@{thm zminus_zminus}, @{thm zmult_zminus}, @{thm zmult_zminus_right}];
211 (*combine unary minus with numeric literals, however nested within a product*)
212 val int_mult_minus_simps =
213 [@{thm zmult_assoc}, @{thm zmult_zminus} RS sym, int_minus_mult_eq_1_to_2];
215 fun prep_simproc (name, pats, proc) =
216 Simplifier.simproc (the_context ()) name pats proc;
218 structure CancelNumeralsCommon =
220 val mk_sum = (fn T:typ => mk_sum)
221 val dest_sum = dest_sum
222 val mk_coeff = mk_coeff
223 val dest_coeff = dest_coeff 1
224 val find_first_coeff = find_first_coeff []
225 fun trans_tac _ = ArithData.gen_trans_tac iff_trans
227 val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac}
228 val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys
229 val norm_ss3 = ZF_ss addsimps int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys
231 ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1))
232 THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2))
233 THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss3))
235 val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys
236 fun numeral_simp_tac ss =
237 ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
238 THEN ALLGOALS (SIMPSET' (fn simpset => asm_simp_tac (Simplifier.inherit_context ss simpset)))
239 val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s @ mult_1s)
243 structure EqCancelNumerals = CancelNumeralsFun
244 (open CancelNumeralsCommon
245 val prove_conv = ArithData.prove_conv "inteq_cancel_numerals"
246 val mk_bal = FOLogic.mk_eq
247 val dest_bal = FOLogic.dest_eq
248 val bal_add1 = eq_add_iff1 RS iff_trans
249 val bal_add2 = eq_add_iff2 RS iff_trans
252 structure LessCancelNumerals = CancelNumeralsFun
253 (open CancelNumeralsCommon
254 val prove_conv = ArithData.prove_conv "intless_cancel_numerals"
255 val mk_bal = FOLogic.mk_binrel @{const_name "zless"}
256 val dest_bal = FOLogic.dest_bin @{const_name "zless"} @{typ i}
257 val bal_add1 = less_add_iff1 RS iff_trans
258 val bal_add2 = less_add_iff2 RS iff_trans
261 structure LeCancelNumerals = CancelNumeralsFun
262 (open CancelNumeralsCommon
263 val prove_conv = ArithData.prove_conv "intle_cancel_numerals"
264 val mk_bal = FOLogic.mk_binrel @{const_name "zle"}
265 val dest_bal = FOLogic.dest_bin @{const_name "zle"} @{typ i}
266 val bal_add1 = le_add_iff1 RS iff_trans
267 val bal_add2 = le_add_iff2 RS iff_trans
270 val cancel_numerals =
272 [("inteq_cancel_numerals",
273 ["l $+ m = n", "l = m $+ n",
274 "l $- m = n", "l = m $- n",
275 "l $* m = n", "l = m $* n"],
276 K EqCancelNumerals.proc),
277 ("intless_cancel_numerals",
278 ["l $+ m $< n", "l $< m $+ n",
279 "l $- m $< n", "l $< m $- n",
280 "l $* m $< n", "l $< m $* n"],
281 K LessCancelNumerals.proc),
282 ("intle_cancel_numerals",
283 ["l $+ m $<= n", "l $<= m $+ n",
284 "l $- m $<= n", "l $<= m $- n",
285 "l $* m $<= n", "l $<= m $* n"],
286 K LeCancelNumerals.proc)];
289 (*version without the hyps argument*)
290 fun prove_conv_nohyps name tacs sg = ArithData.prove_conv name tacs sg [];
292 structure CombineNumeralsData =
295 val iszero = (fn x => x = 0)
297 val mk_sum = (fn T:typ => long_mk_sum) (*to work for #2*x $+ #3*x *)
298 val dest_sum = dest_sum
299 val mk_coeff = mk_coeff
300 val dest_coeff = dest_coeff 1
301 val left_distrib = left_zadd_zmult_distrib RS trans
302 val prove_conv = prove_conv_nohyps "int_combine_numerals"
303 fun trans_tac _ = ArithData.gen_trans_tac trans
305 val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac} @ intifys
306 val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys
307 val norm_ss3 = ZF_ss addsimps int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys
309 ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1))
310 THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2))
311 THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss3))
313 val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys
314 fun numeral_simp_tac ss =
315 ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
316 val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s @ mult_1s)
319 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
321 val combine_numerals =
322 prep_simproc ("int_combine_numerals", ["i $+ j", "i $- j"], K CombineNumerals.proc);
326 (** Constant folding for integer multiplication **)
328 (*The trick is to regard products as sums, e.g. #3 $* x $* #4 as
329 the "sum" of #3, x, #4; the literals are then multiplied*)
332 structure CombineNumeralsProdData =
335 val iszero = (fn x => x = 0)
337 val mk_sum = (fn T:typ => mk_prod)
338 val dest_sum = dest_prod
339 fun mk_coeff(k,t) = if t=one then mk_numeral k
340 else raise TERM("mk_coeff", [])
341 fun dest_coeff t = (dest_numeral t, one) (*We ONLY want pure numerals.*)
342 val left_distrib = @{thm zmult_assoc} RS sym RS trans
343 val prove_conv = prove_conv_nohyps "int_combine_numerals_prod"
344 fun trans_tac _ = ArithData.gen_trans_tac trans
348 val norm_ss1 = ZF_ss addsimps mult_1s @ diff_simps @ zminus_simps
349 val norm_ss2 = ZF_ss addsimps [@{thm zmult_zminus_right} RS sym] @
350 bin_simps @ @{thms zmult_ac} @ tc_rules @ intifys
352 ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1))
353 THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2))
355 val numeral_simp_ss = ZF_ss addsimps bin_simps @ tc_rules @ intifys
356 fun numeral_simp_tac ss =
357 ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
358 val simplify_meta_eq = ArithData.simplify_meta_eq (mult_1s);
362 structure CombineNumeralsProd = CombineNumeralsFun(CombineNumeralsProdData);
364 val combine_numerals_prod =
365 prep_simproc ("int_combine_numerals_prod", ["i $* j"], K CombineNumeralsProd.proc);
370 Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
371 Addsimprocs [Int_Numeral_Simprocs.combine_numerals,
372 Int_Numeral_Simprocs.combine_numerals_prod];
380 fun test s = (Goal s; by (Asm_simp_tac 1));
381 val sg = #sign (rep_thm (topthm()));
382 val t = FOLogic.dest_Trueprop (Logic.strip_assums_concl(getgoal 1));
383 val (t,_) = FOLogic.dest_eq t;
385 (*combine_numerals_prod (products of separate literals) *)
386 test "#5 $* x $* #3 = y";
388 test "y2 $+ ?x42 = y $+ y2";
390 test "oo : int ==> l $+ (l $+ #2) $+ oo = oo";
392 test "#9$*x $+ y = x$*#23 $+ z";
393 test "y $+ x = x $+ z";
395 test "x : int ==> x $+ y $+ z = x $+ z";
396 test "x : int ==> y $+ (z $+ x) = z $+ x";
397 test "z : int ==> x $+ y $+ z = (z $+ y) $+ (x $+ w)";
398 test "z : int ==> x$*y $+ z = (z $+ y) $+ (y$*x $+ w)";
400 test "#-3 $* x $+ y $<= x $* #2 $+ z";
401 test "y $+ x $<= x $+ z";
402 test "x $+ y $+ z $<= x $+ z";
404 test "y $+ (z $+ x) $< z $+ x";
405 test "x $+ y $+ z $< (z $+ y) $+ (x $+ w)";
406 test "x$*y $+ z $< (z $+ y) $+ (y$*x $+ w)";
408 test "l $+ #2 $+ #2 $+ #2 $+ (l $+ #2) $+ (oo $+ #2) = uu";
409 test "u : int ==> #2 $* u = u";
410 test "(i $+ j $+ #12 $+ k) $- #15 = y";
411 test "(i $+ j $+ #12 $+ k) $- #5 = y";
414 test "y $- (#3 $* b $+ c) $< b $- #2 $* c";
416 test "(#2 $* x $- (u $* v) $+ y) $- v $* #3 $* u = w";
417 test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u $* #4 = w";
418 test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u = w";
419 test "u $* v $- (x $* u $* v $+ (u $* v) $* #4 $+ y) = w";
421 test "(i $+ j $+ #12 $+ k) = u $+ #15 $+ y";
422 test "(i $+ j $* #2 $+ #12 $+ k) = j $+ #5 $+ y";
424 test "#2 $* y $+ #3 $* z $+ #6 $* w $+ #2 $* y $+ #3 $* z $+ #2 $* u = #2 $* y' $+ #3 $* z' $+ #6 $* w' $+ #2 $* y' $+ #3 $* z' $+ u $+ vv";
426 test "a $+ $-(b$+c) $+ b = d";
427 test "a $+ $-(b$+c) $- b = d";
429 (*negative numerals*)
430 test "(i $+ j $+ #-2 $+ k) $- (u $+ #5 $+ y) = zz";
431 test "(i $+ j $+ #-3 $+ k) $< u $+ #5 $+ y";
432 test "(i $+ j $+ #3 $+ k) $< u $+ #-6 $+ y";
433 test "(i $+ j $+ #-12 $+ k) $- #15 = y";
434 test "(i $+ j $+ #12 $+ k) $- #-15 = y";
435 test "(i $+ j $+ #-12 $+ k) $- #-15 = y";
437 (*Multiplying separated numerals*)
438 Goal "#6 $* ($# x $* #2) = uu";
439 Goal "#4 $* ($# x $* $# x) $* (#2 $* $# x) = uu";