|
1 (* Title: ZF/int_arith.ML |
|
2 ID: $Id$ |
|
3 Author: Larry Paulson |
|
4 Copyright 2000 University of Cambridge |
|
5 |
|
6 Simprocs for linear arithmetic. |
|
7 *) |
|
8 |
|
9 |
|
10 (** To simplify inequalities involving integer negation and literals, |
|
11 such as -x = #3 |
|
12 **) |
|
13 |
|
14 Addsimps [inst "y" "integ_of(?w)" zminus_equation, |
|
15 inst "x" "integ_of(?w)" equation_zminus]; |
|
16 |
|
17 AddIffs [inst "y" "integ_of(?w)" zminus_zless, |
|
18 inst "x" "integ_of(?w)" zless_zminus]; |
|
19 |
|
20 AddIffs [inst "y" "integ_of(?w)" zminus_zle, |
|
21 inst "x" "integ_of(?w)" zle_zminus]; |
|
22 |
|
23 Addsimps [inst "s" "integ_of(?w)" (thm "Let_def")]; |
|
24 |
|
25 (*** Simprocs for numeric literals ***) |
|
26 |
|
27 (** Combining of literal coefficients in sums of products **) |
|
28 |
|
29 Goal "(x $< y) <-> (x$-y $< #0)"; |
|
30 by (simp_tac (simpset() addsimps zcompare_rls) 1); |
|
31 qed "zless_iff_zdiff_zless_0"; |
|
32 |
|
33 Goal "[| x: int; y: int |] ==> (x = y) <-> (x$-y = #0)"; |
|
34 by (asm_simp_tac (simpset() addsimps zcompare_rls) 1); |
|
35 qed "eq_iff_zdiff_eq_0"; |
|
36 |
|
37 Goal "(x $<= y) <-> (x$-y $<= #0)"; |
|
38 by (asm_simp_tac (simpset() addsimps zcompare_rls) 1); |
|
39 qed "zle_iff_zdiff_zle_0"; |
|
40 |
|
41 |
|
42 (** For combine_numerals **) |
|
43 |
|
44 Goal "i$*u $+ (j$*u $+ k) = (i$+j)$*u $+ k"; |
|
45 by (simp_tac (simpset() addsimps [zadd_zmult_distrib]@zadd_ac) 1); |
|
46 qed "left_zadd_zmult_distrib"; |
|
47 |
|
48 |
|
49 (** For cancel_numerals **) |
|
50 |
|
51 val rel_iff_rel_0_rls = map (inst "y" "?u$+?v") |
|
52 [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, |
|
53 zle_iff_zdiff_zle_0] @ |
|
54 map (inst "y" "n") |
|
55 [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, |
|
56 zle_iff_zdiff_zle_0]; |
|
57 |
|
58 Goal "(i$*u $+ m = j$*u $+ n) <-> ((i$-j)$*u $+ m = intify(n))"; |
|
59 by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1); |
|
60 by (simp_tac (simpset() addsimps zcompare_rls) 1); |
|
61 by (simp_tac (simpset() addsimps zadd_ac) 1); |
|
62 qed "eq_add_iff1"; |
|
63 |
|
64 Goal "(i$*u $+ m = j$*u $+ n) <-> (intify(m) = (j$-i)$*u $+ n)"; |
|
65 by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1); |
|
66 by (simp_tac (simpset() addsimps zcompare_rls) 1); |
|
67 by (simp_tac (simpset() addsimps zadd_ac) 1); |
|
68 qed "eq_add_iff2"; |
|
69 |
|
70 Goal "(i$*u $+ m $< j$*u $+ n) <-> ((i$-j)$*u $+ m $< n)"; |
|
71 by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@ |
|
72 zadd_ac@rel_iff_rel_0_rls) 1); |
|
73 qed "less_add_iff1"; |
|
74 |
|
75 Goal "(i$*u $+ m $< j$*u $+ n) <-> (m $< (j$-i)$*u $+ n)"; |
|
76 by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@ |
|
77 zadd_ac@rel_iff_rel_0_rls) 1); |
|
78 qed "less_add_iff2"; |
|
79 |
|
80 Goal "(i$*u $+ m $<= j$*u $+ n) <-> ((i$-j)$*u $+ m $<= n)"; |
|
81 by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1); |
|
82 by (simp_tac (simpset() addsimps zcompare_rls) 1); |
|
83 by (simp_tac (simpset() addsimps zadd_ac) 1); |
|
84 qed "le_add_iff1"; |
|
85 |
|
86 Goal "(i$*u $+ m $<= j$*u $+ n) <-> (m $<= (j$-i)$*u $+ n)"; |
|
87 by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1); |
|
88 by (simp_tac (simpset() addsimps zcompare_rls) 1); |
|
89 by (simp_tac (simpset() addsimps zadd_ac) 1); |
|
90 qed "le_add_iff2"; |
|
91 |
|
92 |
|
93 structure Int_Numeral_Simprocs = |
|
94 struct |
|
95 |
|
96 (*Utilities*) |
|
97 |
|
98 val integ_of_const = Const ("Bin.integ_of", iT --> iT); |
|
99 |
|
100 fun mk_numeral n = integ_of_const $ NumeralSyntax.mk_bin n; |
|
101 |
|
102 (*Decodes a binary INTEGER*) |
|
103 fun dest_numeral (Const("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]); |
|
107 |
|
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", []); |
|
112 |
|
113 val zero = mk_numeral 0; |
|
114 val mk_plus = FOLogic.mk_binop "Int.zadd"; |
|
115 |
|
116 val iT = Ind_Syntax.iT; |
|
117 |
|
118 val zminus_const = Const ("Int.zminus", iT --> iT); |
|
119 |
|
120 (*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*) |
|
121 fun mk_sum [] = zero |
|
122 | mk_sum [t,u] = mk_plus (t, u) |
|
123 | mk_sum (t :: ts) = mk_plus (t, mk_sum ts); |
|
124 |
|
125 (*this version ALWAYS includes a trailing zero*) |
|
126 fun long_mk_sum [] = zero |
|
127 | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts); |
|
128 |
|
129 val dest_plus = FOLogic.dest_bin "Int.zadd" iT; |
|
130 |
|
131 (*decompose additions AND subtractions as a sum*) |
|
132 fun dest_summing (pos, Const ("Int.zadd", _) $ t $ u, ts) = |
|
133 dest_summing (pos, t, dest_summing (pos, u, ts)) |
|
134 | dest_summing (pos, Const ("Int.zdiff", _) $ t $ u, ts) = |
|
135 dest_summing (pos, t, dest_summing (not pos, u, ts)) |
|
136 | dest_summing (pos, t, ts) = |
|
137 if pos then t::ts else zminus_const$t :: ts; |
|
138 |
|
139 fun dest_sum t = dest_summing (true, t, []); |
|
140 |
|
141 val mk_diff = FOLogic.mk_binop "Int.zdiff"; |
|
142 val dest_diff = FOLogic.dest_bin "Int.zdiff" iT; |
|
143 |
|
144 val one = mk_numeral 1; |
|
145 val mk_times = FOLogic.mk_binop "Int.zmult"; |
|
146 |
|
147 fun mk_prod [] = one |
|
148 | mk_prod [t] = t |
|
149 | mk_prod (t :: ts) = if t = one then mk_prod ts |
|
150 else mk_times (t, mk_prod ts); |
|
151 |
|
152 val dest_times = FOLogic.dest_bin "Int.zmult" iT; |
|
153 |
|
154 fun dest_prod t = |
|
155 let val (t,u) = dest_times t |
|
156 in dest_prod t @ dest_prod u end |
|
157 handle TERM _ => [t]; |
|
158 |
|
159 (*DON'T do the obvious simplifications; that would create special cases*) |
|
160 fun mk_coeff (k, t) = mk_times (mk_numeral k, t); |
|
161 |
|
162 (*Express t as a product of (possibly) a numeral with other sorted terms*) |
|
163 fun dest_coeff sign (Const ("Int.zminus", _) $ t) = dest_coeff (~sign) t |
|
164 | dest_coeff sign t = |
|
165 let val ts = sort Term.term_ord (dest_prod t) |
|
166 val (n, ts') = find_first_numeral [] ts |
|
167 handle TERM _ => (1, ts) |
|
168 in (sign*n, mk_prod ts') end; |
|
169 |
|
170 (*Find first coefficient-term THAT MATCHES u*) |
|
171 fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) |
|
172 | find_first_coeff past u (t::terms) = |
|
173 let val (n,u') = dest_coeff 1 t |
|
174 in if u aconv u' then (n, rev past @ terms) |
|
175 else find_first_coeff (t::past) u terms |
|
176 end |
|
177 handle TERM _ => find_first_coeff (t::past) u terms; |
|
178 |
|
179 |
|
180 (*Simplify #1*n and n*#1 to n*) |
|
181 val add_0s = [zadd_0_intify, zadd_0_right_intify]; |
|
182 |
|
183 val mult_1s = [zmult_1_intify, zmult_1_right_intify, |
|
184 zmult_minus1, zmult_minus1_right]; |
|
185 |
|
186 val tc_rules = [integ_of_type, intify_in_int, |
|
187 int_of_type, zadd_type, zdiff_type, zmult_type] @ |
|
188 thms "bin.intros"; |
|
189 val intifys = [intify_ident, zadd_intify1, zadd_intify2, |
|
190 zdiff_intify1, zdiff_intify2, zmult_intify1, zmult_intify2, |
|
191 zless_intify1, zless_intify2, zle_intify1, zle_intify2]; |
|
192 |
|
193 (*To perform binary arithmetic*) |
|
194 val bin_simps = [add_integ_of_left] @ bin_arith_simps @ bin_rel_simps; |
|
195 |
|
196 (*To evaluate binary negations of coefficients*) |
|
197 val zminus_simps = NCons_simps @ |
|
198 [integ_of_minus RS sym, |
|
199 bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min, |
|
200 bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min]; |
|
201 |
|
202 (*To let us treat subtraction as addition*) |
|
203 val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus]; |
|
204 |
|
205 (*push the unary minus down: - x * y = x * - y *) |
|
206 val int_minus_mult_eq_1_to_2 = |
|
207 [zmult_zminus, zmult_zminus_right RS sym] MRS trans |> standard; |
|
208 |
|
209 (*to extract again any uncancelled minuses*) |
|
210 val int_minus_from_mult_simps = |
|
211 [zminus_zminus, zmult_zminus, zmult_zminus_right]; |
|
212 |
|
213 (*combine unary minus with numeric literals, however nested within a product*) |
|
214 val int_mult_minus_simps = |
|
215 [zmult_assoc, zmult_zminus RS sym, int_minus_mult_eq_1_to_2]; |
|
216 |
|
217 fun prep_simproc (name, pats, proc) = |
|
218 Simplifier.simproc (the_context ()) name pats proc; |
|
219 |
|
220 structure CancelNumeralsCommon = |
|
221 struct |
|
222 val mk_sum = (fn T:typ => mk_sum) |
|
223 val dest_sum = dest_sum |
|
224 val mk_coeff = mk_coeff |
|
225 val dest_coeff = dest_coeff 1 |
|
226 val find_first_coeff = find_first_coeff [] |
|
227 fun trans_tac _ = ArithData.gen_trans_tac iff_trans |
|
228 |
|
229 val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ zadd_ac |
|
230 val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys |
|
231 val norm_ss3 = ZF_ss addsimps int_minus_from_mult_simps @ zadd_ac @ zmult_ac @ tc_rules @ intifys |
|
232 fun norm_tac ss = |
|
233 ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1)) |
|
234 THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2)) |
|
235 THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss3)) |
|
236 |
|
237 val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys |
|
238 fun numeral_simp_tac ss = |
|
239 ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) |
|
240 THEN ALLGOALS (SIMPSET' (fn simpset => asm_simp_tac (Simplifier.inherit_context ss simpset))) |
|
241 val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s @ mult_1s) |
|
242 end; |
|
243 |
|
244 |
|
245 structure EqCancelNumerals = CancelNumeralsFun |
|
246 (open CancelNumeralsCommon |
|
247 val prove_conv = ArithData.prove_conv "inteq_cancel_numerals" |
|
248 val mk_bal = FOLogic.mk_eq |
|
249 val dest_bal = FOLogic.dest_eq |
|
250 val bal_add1 = eq_add_iff1 RS iff_trans |
|
251 val bal_add2 = eq_add_iff2 RS iff_trans |
|
252 ); |
|
253 |
|
254 structure LessCancelNumerals = CancelNumeralsFun |
|
255 (open CancelNumeralsCommon |
|
256 val prove_conv = ArithData.prove_conv "intless_cancel_numerals" |
|
257 val mk_bal = FOLogic.mk_binrel "Int.zless" |
|
258 val dest_bal = FOLogic.dest_bin "Int.zless" iT |
|
259 val bal_add1 = less_add_iff1 RS iff_trans |
|
260 val bal_add2 = less_add_iff2 RS iff_trans |
|
261 ); |
|
262 |
|
263 structure LeCancelNumerals = CancelNumeralsFun |
|
264 (open CancelNumeralsCommon |
|
265 val prove_conv = ArithData.prove_conv "intle_cancel_numerals" |
|
266 val mk_bal = FOLogic.mk_binrel "Int.zle" |
|
267 val dest_bal = FOLogic.dest_bin "Int.zle" iT |
|
268 val bal_add1 = le_add_iff1 RS iff_trans |
|
269 val bal_add2 = le_add_iff2 RS iff_trans |
|
270 ); |
|
271 |
|
272 val cancel_numerals = |
|
273 map prep_simproc |
|
274 [("inteq_cancel_numerals", |
|
275 ["l $+ m = n", "l = m $+ n", |
|
276 "l $- m = n", "l = m $- n", |
|
277 "l $* m = n", "l = m $* n"], |
|
278 K EqCancelNumerals.proc), |
|
279 ("intless_cancel_numerals", |
|
280 ["l $+ m $< n", "l $< m $+ n", |
|
281 "l $- m $< n", "l $< m $- n", |
|
282 "l $* m $< n", "l $< m $* n"], |
|
283 K LessCancelNumerals.proc), |
|
284 ("intle_cancel_numerals", |
|
285 ["l $+ m $<= n", "l $<= m $+ n", |
|
286 "l $- m $<= n", "l $<= m $- n", |
|
287 "l $* m $<= n", "l $<= m $* n"], |
|
288 K LeCancelNumerals.proc)]; |
|
289 |
|
290 |
|
291 (*version without the hyps argument*) |
|
292 fun prove_conv_nohyps name tacs sg = ArithData.prove_conv name tacs sg []; |
|
293 |
|
294 structure CombineNumeralsData = |
|
295 struct |
|
296 type coeff = IntInf.int |
|
297 val iszero = (fn x : IntInf.int => x = 0) |
|
298 val add = IntInf.+ |
|
299 val mk_sum = (fn T:typ => long_mk_sum) (*to work for #2*x $+ #3*x *) |
|
300 val dest_sum = dest_sum |
|
301 val mk_coeff = mk_coeff |
|
302 val dest_coeff = dest_coeff 1 |
|
303 val left_distrib = left_zadd_zmult_distrib RS trans |
|
304 val prove_conv = prove_conv_nohyps "int_combine_numerals" |
|
305 fun trans_tac _ = ArithData.gen_trans_tac trans |
|
306 |
|
307 val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ zadd_ac @ intifys |
|
308 val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys |
|
309 val norm_ss3 = ZF_ss addsimps int_minus_from_mult_simps @ zadd_ac @ zmult_ac @ tc_rules @ intifys |
|
310 fun norm_tac ss = |
|
311 ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1)) |
|
312 THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2)) |
|
313 THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss3)) |
|
314 |
|
315 val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys |
|
316 fun numeral_simp_tac ss = |
|
317 ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) |
|
318 val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s @ mult_1s) |
|
319 end; |
|
320 |
|
321 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); |
|
322 |
|
323 val combine_numerals = |
|
324 prep_simproc ("int_combine_numerals", ["i $+ j", "i $- j"], K CombineNumerals.proc); |
|
325 |
|
326 |
|
327 |
|
328 (** Constant folding for integer multiplication **) |
|
329 |
|
330 (*The trick is to regard products as sums, e.g. #3 $* x $* #4 as |
|
331 the "sum" of #3, x, #4; the literals are then multiplied*) |
|
332 |
|
333 |
|
334 structure CombineNumeralsProdData = |
|
335 struct |
|
336 type coeff = IntInf.int |
|
337 val iszero = (fn x : IntInf.int => x = 0) |
|
338 val add = IntInf.* |
|
339 val mk_sum = (fn T:typ => mk_prod) |
|
340 val dest_sum = dest_prod |
|
341 fun mk_coeff(k,t) = if t=one then mk_numeral k |
|
342 else raise TERM("mk_coeff", []) |
|
343 fun dest_coeff t = (dest_numeral t, one) (*We ONLY want pure numerals.*) |
|
344 val left_distrib = zmult_assoc RS sym RS trans |
|
345 val prove_conv = prove_conv_nohyps "int_combine_numerals_prod" |
|
346 fun trans_tac _ = ArithData.gen_trans_tac trans |
|
347 |
|
348 |
|
349 |
|
350 val norm_ss1 = ZF_ss addsimps mult_1s @ diff_simps @ zminus_simps |
|
351 val norm_ss2 = ZF_ss addsimps [zmult_zminus_right RS sym] @ |
|
352 bin_simps @ zmult_ac @ tc_rules @ intifys |
|
353 fun norm_tac ss = |
|
354 ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1)) |
|
355 THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2)) |
|
356 |
|
357 val numeral_simp_ss = ZF_ss addsimps bin_simps @ tc_rules @ intifys |
|
358 fun numeral_simp_tac ss = |
|
359 ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) |
|
360 val simplify_meta_eq = ArithData.simplify_meta_eq (mult_1s); |
|
361 end; |
|
362 |
|
363 |
|
364 structure CombineNumeralsProd = CombineNumeralsFun(CombineNumeralsProdData); |
|
365 |
|
366 val combine_numerals_prod = |
|
367 prep_simproc ("int_combine_numerals_prod", ["i $* j"], K CombineNumeralsProd.proc); |
|
368 |
|
369 end; |
|
370 |
|
371 |
|
372 Addsimprocs Int_Numeral_Simprocs.cancel_numerals; |
|
373 Addsimprocs [Int_Numeral_Simprocs.combine_numerals, |
|
374 Int_Numeral_Simprocs.combine_numerals_prod]; |
|
375 |
|
376 |
|
377 (*examples:*) |
|
378 (* |
|
379 print_depth 22; |
|
380 set timing; |
|
381 set trace_simp; |
|
382 fun test s = (Goal s; by (Asm_simp_tac 1)); |
|
383 val sg = #sign (rep_thm (topthm())); |
|
384 val t = FOLogic.dest_Trueprop (Logic.strip_assums_concl(getgoal 1)); |
|
385 val (t,_) = FOLogic.dest_eq t; |
|
386 |
|
387 (*combine_numerals_prod (products of separate literals) *) |
|
388 test "#5 $* x $* #3 = y"; |
|
389 |
|
390 test "y2 $+ ?x42 = y $+ y2"; |
|
391 |
|
392 test "oo : int ==> l $+ (l $+ #2) $+ oo = oo"; |
|
393 |
|
394 test "#9$*x $+ y = x$*#23 $+ z"; |
|
395 test "y $+ x = x $+ z"; |
|
396 |
|
397 test "x : int ==> x $+ y $+ z = x $+ z"; |
|
398 test "x : int ==> y $+ (z $+ x) = z $+ x"; |
|
399 test "z : int ==> x $+ y $+ z = (z $+ y) $+ (x $+ w)"; |
|
400 test "z : int ==> x$*y $+ z = (z $+ y) $+ (y$*x $+ w)"; |
|
401 |
|
402 test "#-3 $* x $+ y $<= x $* #2 $+ z"; |
|
403 test "y $+ x $<= x $+ z"; |
|
404 test "x $+ y $+ z $<= x $+ z"; |
|
405 |
|
406 test "y $+ (z $+ x) $< z $+ x"; |
|
407 test "x $+ y $+ z $< (z $+ y) $+ (x $+ w)"; |
|
408 test "x$*y $+ z $< (z $+ y) $+ (y$*x $+ w)"; |
|
409 |
|
410 test "l $+ #2 $+ #2 $+ #2 $+ (l $+ #2) $+ (oo $+ #2) = uu"; |
|
411 test "u : int ==> #2 $* u = u"; |
|
412 test "(i $+ j $+ #12 $+ k) $- #15 = y"; |
|
413 test "(i $+ j $+ #12 $+ k) $- #5 = y"; |
|
414 |
|
415 test "y $- b $< b"; |
|
416 test "y $- (#3 $* b $+ c) $< b $- #2 $* c"; |
|
417 |
|
418 test "(#2 $* x $- (u $* v) $+ y) $- v $* #3 $* u = w"; |
|
419 test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u $* #4 = w"; |
|
420 test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u = w"; |
|
421 test "u $* v $- (x $* u $* v $+ (u $* v) $* #4 $+ y) = w"; |
|
422 |
|
423 test "(i $+ j $+ #12 $+ k) = u $+ #15 $+ y"; |
|
424 test "(i $+ j $* #2 $+ #12 $+ k) = j $+ #5 $+ y"; |
|
425 |
|
426 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"; |
|
427 |
|
428 test "a $+ $-(b$+c) $+ b = d"; |
|
429 test "a $+ $-(b$+c) $- b = d"; |
|
430 |
|
431 (*negative numerals*) |
|
432 test "(i $+ j $+ #-2 $+ k) $- (u $+ #5 $+ y) = zz"; |
|
433 test "(i $+ j $+ #-3 $+ k) $< u $+ #5 $+ y"; |
|
434 test "(i $+ j $+ #3 $+ k) $< u $+ #-6 $+ y"; |
|
435 test "(i $+ j $+ #-12 $+ k) $- #15 = y"; |
|
436 test "(i $+ j $+ #12 $+ k) $- #-15 = y"; |
|
437 test "(i $+ j $+ #-12 $+ k) $- #-15 = y"; |
|
438 |
|
439 (*Multiplying separated numerals*) |
|
440 Goal "#6 $* ($# x $* #2) = uu"; |
|
441 Goal "#4 $* ($# x $* $# x) $* (#2 $* $# x) = uu"; |
|
442 *) |
|
443 |