paulson@10536
|
1 |
(* Title: HOL/int_factor_simprocs.ML
|
paulson@10536
|
2 |
ID: $Id$
|
paulson@10536
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
paulson@10536
|
4 |
Copyright 2000 University of Cambridge
|
paulson@10536
|
5 |
|
paulson@14390
|
6 |
Factor cancellation simprocs for the integers (and for fields).
|
paulson@10536
|
7 |
|
paulson@14378
|
8 |
This file can't be combined with int_arith1 because it requires IntDiv.thy.
|
paulson@10536
|
9 |
*)
|
paulson@10536
|
10 |
|
paulson@14390
|
11 |
|
paulson@14390
|
12 |
(*To quote from Provers/Arith/cancel_numeral_factor.ML:
|
paulson@14390
|
13 |
|
paulson@14390
|
14 |
Cancels common coefficients in balanced expressions:
|
paulson@14390
|
15 |
|
paulson@14390
|
16 |
u*#m ~~ u'*#m' == #n*u ~~ #n'*u'
|
paulson@14390
|
17 |
|
paulson@14390
|
18 |
where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /)
|
paulson@14390
|
19 |
and d = gcd(m,m') and n=m/d and n'=m'/d.
|
paulson@14390
|
20 |
*)
|
paulson@14390
|
21 |
|
paulson@14390
|
22 |
val rel_number_of = [eq_number_of_eq, less_number_of_eq_neg, le_number_of_eq];
|
paulson@14390
|
23 |
|
paulson@14390
|
24 |
(** Factor cancellation theorems for integer division (div, not /) **)
|
paulson@10536
|
25 |
|
paulson@11868
|
26 |
Goal "!!k::int. k~=0 ==> (k*m) div (k*n) = (m div n)";
|
wenzelm@13462
|
27 |
by (stac zdiv_zmult_zmult1 1);
|
wenzelm@13462
|
28 |
by Auto_tac;
|
paulson@10536
|
29 |
qed "int_mult_div_cancel1";
|
paulson@10536
|
30 |
|
paulson@10703
|
31 |
(*For ExtractCommonTermFun, cancelling common factors*)
|
paulson@11868
|
32 |
Goal "(k*m) div (k*n) = (if k = (0::int) then 0 else m div n)";
|
wenzelm@13462
|
33 |
by (simp_tac (simpset() addsimps [int_mult_div_cancel1]) 1);
|
paulson@10703
|
34 |
qed "int_mult_div_cancel_disj";
|
paulson@10703
|
35 |
|
paulson@14378
|
36 |
|
paulson@10536
|
37 |
local
|
paulson@10536
|
38 |
open Int_Numeral_Simprocs
|
paulson@10536
|
39 |
in
|
paulson@10536
|
40 |
|
paulson@10536
|
41 |
structure CancelNumeralFactorCommon =
|
paulson@10536
|
42 |
struct
|
wenzelm@13462
|
43 |
val mk_coeff = mk_coeff
|
wenzelm@13462
|
44 |
val dest_coeff = dest_coeff 1
|
paulson@10536
|
45 |
val trans_tac = trans_tac
|
wenzelm@13462
|
46 |
val norm_tac =
|
paulson@14390
|
47 |
ALLGOALS (simp_tac (HOL_ss addsimps minus_from_mult_simps @ mult_1s))
|
paulson@14387
|
48 |
THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@mult_minus_simps))
|
paulson@14387
|
49 |
THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac))
|
paulson@14390
|
50 |
val numeral_simp_tac =
|
paulson@14390
|
51 |
ALLGOALS (simp_tac (HOL_ss addsimps rel_number_of@bin_simps))
|
paulson@14390
|
52 |
val simplify_meta_eq =
|
paulson@14390
|
53 |
Int_Numeral_Simprocs.simplify_meta_eq
|
paulson@14390
|
54 |
[add_0, add_0_right,
|
paulson@14390
|
55 |
mult_zero_left, mult_zero_right, mult_1, mult_1_right];
|
paulson@10536
|
56 |
end
|
paulson@10536
|
57 |
|
paulson@14390
|
58 |
(*Version for integer division*)
|
paulson@10536
|
59 |
structure DivCancelNumeralFactor = CancelNumeralFactorFun
|
paulson@10536
|
60 |
(open CancelNumeralFactorCommon
|
wenzelm@13485
|
61 |
val prove_conv = Bin_Simprocs.prove_conv
|
paulson@10536
|
62 |
val mk_bal = HOLogic.mk_binop "Divides.op div"
|
paulson@10536
|
63 |
val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
|
paulson@10536
|
64 |
val cancel = int_mult_div_cancel1 RS trans
|
paulson@10536
|
65 |
val neg_exchanges = false
|
paulson@10536
|
66 |
)
|
paulson@10536
|
67 |
|
paulson@14390
|
68 |
(*Version for fields*)
|
paulson@14390
|
69 |
structure FieldDivCancelNumeralFactor = CancelNumeralFactorFun
|
paulson@14390
|
70 |
(open CancelNumeralFactorCommon
|
paulson@14390
|
71 |
val prove_conv = Bin_Simprocs.prove_conv
|
paulson@14390
|
72 |
val mk_bal = HOLogic.mk_binop "HOL.divide"
|
paulson@14390
|
73 |
val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
|
paulson@14390
|
74 |
val cancel = mult_divide_cancel_left RS trans
|
paulson@14390
|
75 |
val neg_exchanges = false
|
paulson@14390
|
76 |
)
|
paulson@14390
|
77 |
|
paulson@14390
|
78 |
(*Version for ordered rings: mult_cancel_left requires an ordering*)
|
paulson@10536
|
79 |
structure EqCancelNumeralFactor = CancelNumeralFactorFun
|
paulson@10536
|
80 |
(open CancelNumeralFactorCommon
|
wenzelm@13485
|
81 |
val prove_conv = Bin_Simprocs.prove_conv
|
paulson@10536
|
82 |
val mk_bal = HOLogic.mk_eq
|
paulson@14390
|
83 |
val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
|
paulson@14378
|
84 |
val cancel = mult_cancel_left RS trans
|
paulson@10536
|
85 |
val neg_exchanges = false
|
paulson@10536
|
86 |
)
|
paulson@10536
|
87 |
|
paulson@14390
|
88 |
(*Version for (unordered) fields*)
|
paulson@14390
|
89 |
structure FieldEqCancelNumeralFactor = CancelNumeralFactorFun
|
paulson@14390
|
90 |
(open CancelNumeralFactorCommon
|
paulson@14390
|
91 |
val prove_conv = Bin_Simprocs.prove_conv
|
paulson@14390
|
92 |
val mk_bal = HOLogic.mk_eq
|
paulson@14390
|
93 |
val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
|
paulson@14390
|
94 |
val cancel = field_mult_cancel_left RS trans
|
paulson@14390
|
95 |
val neg_exchanges = false
|
paulson@14390
|
96 |
)
|
paulson@14390
|
97 |
|
paulson@10536
|
98 |
structure LessCancelNumeralFactor = CancelNumeralFactorFun
|
paulson@10536
|
99 |
(open CancelNumeralFactorCommon
|
wenzelm@13485
|
100 |
val prove_conv = Bin_Simprocs.prove_conv
|
paulson@10536
|
101 |
val mk_bal = HOLogic.mk_binrel "op <"
|
paulson@14390
|
102 |
val dest_bal = HOLogic.dest_bin "op <" Term.dummyT
|
paulson@14378
|
103 |
val cancel = mult_less_cancel_left RS trans
|
paulson@10536
|
104 |
val neg_exchanges = true
|
paulson@10536
|
105 |
)
|
paulson@10536
|
106 |
|
paulson@10536
|
107 |
structure LeCancelNumeralFactor = CancelNumeralFactorFun
|
paulson@10536
|
108 |
(open CancelNumeralFactorCommon
|
wenzelm@13485
|
109 |
val prove_conv = Bin_Simprocs.prove_conv
|
paulson@10536
|
110 |
val mk_bal = HOLogic.mk_binrel "op <="
|
paulson@14390
|
111 |
val dest_bal = HOLogic.dest_bin "op <=" Term.dummyT
|
paulson@14378
|
112 |
val cancel = mult_le_cancel_left RS trans
|
paulson@10536
|
113 |
val neg_exchanges = true
|
paulson@10536
|
114 |
)
|
paulson@10536
|
115 |
|
paulson@14390
|
116 |
val ring_cancel_numeral_factors =
|
paulson@11868
|
117 |
map Bin_Simprocs.prep_simproc
|
paulson@14390
|
118 |
[("ring_eq_cancel_numeral_factor",
|
obua@14738
|
119 |
["(l::'a::{ordered_idom,number_ring}) * m = n",
|
obua@14738
|
120 |
"(l::'a::{ordered_idom,number_ring}) = m * n"],
|
paulson@10536
|
121 |
EqCancelNumeralFactor.proc),
|
paulson@14390
|
122 |
("ring_less_cancel_numeral_factor",
|
obua@14738
|
123 |
["(l::'a::{ordered_idom,number_ring}) * m < n",
|
obua@14738
|
124 |
"(l::'a::{ordered_idom,number_ring}) < m * n"],
|
paulson@10536
|
125 |
LessCancelNumeralFactor.proc),
|
paulson@14390
|
126 |
("ring_le_cancel_numeral_factor",
|
obua@14738
|
127 |
["(l::'a::{ordered_idom,number_ring}) * m <= n",
|
obua@14738
|
128 |
"(l::'a::{ordered_idom,number_ring}) <= m * n"],
|
paulson@10536
|
129 |
LeCancelNumeralFactor.proc),
|
paulson@14390
|
130 |
("int_div_cancel_numeral_factors",
|
paulson@14390
|
131 |
["((l::int) * m) div n", "(l::int) div (m * n)"],
|
paulson@10536
|
132 |
DivCancelNumeralFactor.proc)];
|
paulson@10536
|
133 |
|
paulson@14390
|
134 |
|
paulson@14390
|
135 |
val field_cancel_numeral_factors =
|
paulson@14390
|
136 |
map Bin_Simprocs.prep_simproc
|
paulson@14390
|
137 |
[("field_eq_cancel_numeral_factor",
|
paulson@14390
|
138 |
["(l::'a::{field,number_ring}) * m = n",
|
paulson@14390
|
139 |
"(l::'a::{field,number_ring}) = m * n"],
|
paulson@14390
|
140 |
FieldEqCancelNumeralFactor.proc),
|
paulson@14390
|
141 |
("field_cancel_numeral_factor",
|
paulson@14426
|
142 |
["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
|
paulson@14426
|
143 |
"(l::'a::{division_by_zero,field,number_ring}) / (m * n)",
|
paulson@14426
|
144 |
"((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"],
|
paulson@14390
|
145 |
FieldDivCancelNumeralFactor.proc)]
|
paulson@14390
|
146 |
|
paulson@10536
|
147 |
end;
|
paulson@10536
|
148 |
|
paulson@14390
|
149 |
Addsimprocs ring_cancel_numeral_factors;
|
paulson@14390
|
150 |
Addsimprocs field_cancel_numeral_factors;
|
paulson@10536
|
151 |
|
paulson@10536
|
152 |
(*examples:
|
paulson@10536
|
153 |
print_depth 22;
|
paulson@10536
|
154 |
set timing;
|
paulson@10536
|
155 |
set trace_simp;
|
wenzelm@13462
|
156 |
fun test s = (Goal s; by (Simp_tac 1));
|
paulson@10536
|
157 |
|
wenzelm@11704
|
158 |
test "9*x = 12 * (y::int)";
|
wenzelm@11704
|
159 |
test "(9*x) div (12 * (y::int)) = z";
|
wenzelm@11704
|
160 |
test "9*x < 12 * (y::int)";
|
wenzelm@11704
|
161 |
test "9*x <= 12 * (y::int)";
|
paulson@10536
|
162 |
|
wenzelm@11704
|
163 |
test "-99*x = 132 * (y::int)";
|
wenzelm@11704
|
164 |
test "(-99*x) div (132 * (y::int)) = z";
|
wenzelm@11704
|
165 |
test "-99*x < 132 * (y::int)";
|
wenzelm@11704
|
166 |
test "-99*x <= 132 * (y::int)";
|
paulson@10536
|
167 |
|
wenzelm@11704
|
168 |
test "999*x = -396 * (y::int)";
|
wenzelm@11704
|
169 |
test "(999*x) div (-396 * (y::int)) = z";
|
wenzelm@11704
|
170 |
test "999*x < -396 * (y::int)";
|
wenzelm@11704
|
171 |
test "999*x <= -396 * (y::int)";
|
paulson@10536
|
172 |
|
wenzelm@11704
|
173 |
test "-99*x = -81 * (y::int)";
|
wenzelm@11704
|
174 |
test "(-99*x) div (-81 * (y::int)) = z";
|
wenzelm@11704
|
175 |
test "-99*x <= -81 * (y::int)";
|
wenzelm@11704
|
176 |
test "-99*x < -81 * (y::int)";
|
paulson@10536
|
177 |
|
wenzelm@11704
|
178 |
test "-2 * x = -1 * (y::int)";
|
wenzelm@11704
|
179 |
test "-2 * x = -(y::int)";
|
wenzelm@11704
|
180 |
test "(-2 * x) div (-1 * (y::int)) = z";
|
wenzelm@11704
|
181 |
test "-2 * x < -(y::int)";
|
wenzelm@11704
|
182 |
test "-2 * x <= -1 * (y::int)";
|
wenzelm@11704
|
183 |
test "-x < -23 * (y::int)";
|
wenzelm@11704
|
184 |
test "-x <= -23 * (y::int)";
|
paulson@10536
|
185 |
*)
|
paulson@10536
|
186 |
|
paulson@14390
|
187 |
(*And the same examples for fields such as rat or real:
|
paulson@14390
|
188 |
test "0 <= (y::rat) * -2";
|
paulson@14390
|
189 |
test "9*x = 12 * (y::rat)";
|
paulson@14390
|
190 |
test "(9*x) / (12 * (y::rat)) = z";
|
paulson@14390
|
191 |
test "9*x < 12 * (y::rat)";
|
paulson@14390
|
192 |
test "9*x <= 12 * (y::rat)";
|
paulson@14390
|
193 |
|
paulson@14390
|
194 |
test "-99*x = 132 * (y::rat)";
|
paulson@14390
|
195 |
test "(-99*x) / (132 * (y::rat)) = z";
|
paulson@14390
|
196 |
test "-99*x < 132 * (y::rat)";
|
paulson@14390
|
197 |
test "-99*x <= 132 * (y::rat)";
|
paulson@14390
|
198 |
|
paulson@14390
|
199 |
test "999*x = -396 * (y::rat)";
|
paulson@14390
|
200 |
test "(999*x) / (-396 * (y::rat)) = z";
|
paulson@14390
|
201 |
test "999*x < -396 * (y::rat)";
|
paulson@14390
|
202 |
test "999*x <= -396 * (y::rat)";
|
paulson@14390
|
203 |
|
paulson@14390
|
204 |
test "(- ((2::rat) * x) <= 2 * y)";
|
paulson@14390
|
205 |
test "-99*x = -81 * (y::rat)";
|
paulson@14390
|
206 |
test "(-99*x) / (-81 * (y::rat)) = z";
|
paulson@14390
|
207 |
test "-99*x <= -81 * (y::rat)";
|
paulson@14390
|
208 |
test "-99*x < -81 * (y::rat)";
|
paulson@14390
|
209 |
|
paulson@14390
|
210 |
test "-2 * x = -1 * (y::rat)";
|
paulson@14390
|
211 |
test "-2 * x = -(y::rat)";
|
paulson@14390
|
212 |
test "(-2 * x) / (-1 * (y::rat)) = z";
|
paulson@14390
|
213 |
test "-2 * x < -(y::rat)";
|
paulson@14390
|
214 |
test "-2 * x <= -1 * (y::rat)";
|
paulson@14390
|
215 |
test "-x < -23 * (y::rat)";
|
paulson@14390
|
216 |
test "-x <= -23 * (y::rat)";
|
paulson@14390
|
217 |
*)
|
paulson@14390
|
218 |
|
paulson@10703
|
219 |
|
paulson@10703
|
220 |
(** Declarations for ExtractCommonTerm **)
|
paulson@10703
|
221 |
|
paulson@10703
|
222 |
local
|
paulson@10703
|
223 |
open Int_Numeral_Simprocs
|
paulson@10703
|
224 |
in
|
paulson@10703
|
225 |
|
paulson@10703
|
226 |
(*Find first term that matches u*)
|
wenzelm@13462
|
227 |
fun find_first past u [] = raise TERM("find_first", [])
|
paulson@10703
|
228 |
| find_first past u (t::terms) =
|
wenzelm@13462
|
229 |
if u aconv t then (rev past @ terms)
|
paulson@10703
|
230 |
else find_first (t::past) u terms
|
wenzelm@13462
|
231 |
handle TERM _ => find_first (t::past) u terms;
|
paulson@10703
|
232 |
|
paulson@10703
|
233 |
(*Final simplification: cancel + and * *)
|
wenzelm@13462
|
234 |
fun cancel_simplify_meta_eq cancel_th th =
|
wenzelm@13462
|
235 |
Int_Numeral_Simprocs.simplify_meta_eq
|
paulson@14387
|
236 |
[mult_1, mult_1_right]
|
paulson@10703
|
237 |
(([th, cancel_th]) MRS trans);
|
paulson@10703
|
238 |
|
paulson@14426
|
239 |
(*At present, long_mk_prod creates Numeral1, so this requires the axclass
|
paulson@14426
|
240 |
number_ring*)
|
paulson@10703
|
241 |
structure CancelFactorCommon =
|
paulson@10703
|
242 |
struct
|
wenzelm@13462
|
243 |
val mk_sum = long_mk_prod
|
wenzelm@13462
|
244 |
val dest_sum = dest_prod
|
wenzelm@13462
|
245 |
val mk_coeff = mk_coeff
|
wenzelm@13462
|
246 |
val dest_coeff = dest_coeff
|
wenzelm@13462
|
247 |
val find_first = find_first []
|
paulson@10703
|
248 |
val trans_tac = trans_tac
|
paulson@14387
|
249 |
val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac))
|
paulson@10703
|
250 |
end;
|
paulson@10703
|
251 |
|
obua@14738
|
252 |
(*mult_cancel_left requires an ordered comm_ring_1, such as int. The version in
|
paulson@14387
|
253 |
rat_arith.ML works for all fields.*)
|
paulson@10703
|
254 |
structure EqCancelFactor = ExtractCommonTermFun
|
paulson@10703
|
255 |
(open CancelFactorCommon
|
wenzelm@13485
|
256 |
val prove_conv = Bin_Simprocs.prove_conv
|
paulson@10703
|
257 |
val mk_bal = HOLogic.mk_eq
|
paulson@10703
|
258 |
val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
|
paulson@14378
|
259 |
val simplify_meta_eq = cancel_simplify_meta_eq mult_cancel_left
|
paulson@10703
|
260 |
);
|
paulson@10703
|
261 |
|
paulson@14387
|
262 |
(*int_mult_div_cancel_disj is for integer division (div). The version in
|
paulson@14387
|
263 |
rat_arith.ML works for all fields, using real division (/).*)
|
paulson@10703
|
264 |
structure DivideCancelFactor = ExtractCommonTermFun
|
paulson@10703
|
265 |
(open CancelFactorCommon
|
wenzelm@13485
|
266 |
val prove_conv = Bin_Simprocs.prove_conv
|
paulson@10703
|
267 |
val mk_bal = HOLogic.mk_binop "Divides.op div"
|
paulson@10703
|
268 |
val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
|
paulson@10703
|
269 |
val simplify_meta_eq = cancel_simplify_meta_eq int_mult_div_cancel_disj
|
paulson@10703
|
270 |
);
|
paulson@10703
|
271 |
|
wenzelm@13462
|
272 |
val int_cancel_factor =
|
paulson@11868
|
273 |
map Bin_Simprocs.prep_simproc
|
paulson@14390
|
274 |
[("ring_eq_cancel_factor", ["(l::int) * m = n", "(l::int) = m * n"],
|
paulson@14390
|
275 |
EqCancelFactor.proc),
|
paulson@14390
|
276 |
("int_divide_cancel_factor", ["((l::int) * m) div n", "(l::int) div (m*n)"],
|
paulson@10703
|
277 |
DivideCancelFactor.proc)];
|
paulson@10703
|
278 |
|
paulson@14390
|
279 |
(** Versions for all fields, including unordered ones (type complex).*)
|
paulson@14390
|
280 |
|
paulson@14390
|
281 |
structure FieldEqCancelFactor = ExtractCommonTermFun
|
paulson@14390
|
282 |
(open CancelFactorCommon
|
paulson@14390
|
283 |
val prove_conv = Bin_Simprocs.prove_conv
|
paulson@14390
|
284 |
val mk_bal = HOLogic.mk_eq
|
paulson@14390
|
285 |
val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
|
paulson@14390
|
286 |
val simplify_meta_eq = cancel_simplify_meta_eq field_mult_cancel_left
|
paulson@14390
|
287 |
);
|
paulson@14390
|
288 |
|
paulson@14390
|
289 |
structure FieldDivideCancelFactor = ExtractCommonTermFun
|
paulson@14390
|
290 |
(open CancelFactorCommon
|
paulson@14390
|
291 |
val prove_conv = Bin_Simprocs.prove_conv
|
paulson@14390
|
292 |
val mk_bal = HOLogic.mk_binop "HOL.divide"
|
paulson@14390
|
293 |
val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
|
paulson@14390
|
294 |
val simplify_meta_eq = cancel_simplify_meta_eq mult_divide_cancel_eq_if
|
paulson@14390
|
295 |
);
|
paulson@14390
|
296 |
|
paulson@14426
|
297 |
(*The number_ring class is necessary because the simprocs refer to the
|
paulson@14426
|
298 |
binary number 1. FIXME: probably they could use 1 instead.*)
|
paulson@14390
|
299 |
val field_cancel_factor =
|
paulson@14390
|
300 |
map Bin_Simprocs.prep_simproc
|
paulson@14390
|
301 |
[("field_eq_cancel_factor",
|
paulson@14426
|
302 |
["(l::'a::{field,number_ring}) * m = n",
|
paulson@14426
|
303 |
"(l::'a::{field,number_ring}) = m * n"],
|
paulson@14390
|
304 |
FieldEqCancelFactor.proc),
|
paulson@14390
|
305 |
("field_divide_cancel_factor",
|
paulson@14426
|
306 |
["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
|
paulson@14426
|
307 |
"(l::'a::{division_by_zero,field,number_ring}) / (m * n)"],
|
paulson@14390
|
308 |
FieldDivideCancelFactor.proc)];
|
paulson@14390
|
309 |
|
paulson@10703
|
310 |
end;
|
paulson@10703
|
311 |
|
paulson@10703
|
312 |
Addsimprocs int_cancel_factor;
|
paulson@14390
|
313 |
Addsimprocs field_cancel_factor;
|
paulson@10703
|
314 |
|
paulson@10703
|
315 |
|
paulson@10703
|
316 |
(*examples:
|
paulson@10703
|
317 |
print_depth 22;
|
paulson@10703
|
318 |
set timing;
|
paulson@10703
|
319 |
set trace_simp;
|
wenzelm@13462
|
320 |
fun test s = (Goal s; by (Asm_simp_tac 1));
|
paulson@10703
|
321 |
|
paulson@10703
|
322 |
test "x*k = k*(y::int)";
|
wenzelm@13462
|
323 |
test "k = k*(y::int)";
|
paulson@10703
|
324 |
test "a*(b*c) = (b::int)";
|
paulson@10703
|
325 |
test "a*(b*c) = d*(b::int)*(x*a)";
|
paulson@10703
|
326 |
|
paulson@10703
|
327 |
test "(x*k) div (k*(y::int)) = (uu::int)";
|
wenzelm@13462
|
328 |
test "(k) div (k*(y::int)) = (uu::int)";
|
paulson@10703
|
329 |
test "(a*(b*c)) div ((b::int)) = (uu::int)";
|
paulson@10703
|
330 |
test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)";
|
paulson@10703
|
331 |
*)
|
paulson@10703
|
332 |
|
paulson@14390
|
333 |
(*And the same examples for fields such as rat or real:
|
paulson@14390
|
334 |
print_depth 22;
|
paulson@14390
|
335 |
set timing;
|
paulson@14390
|
336 |
set trace_simp;
|
paulson@14390
|
337 |
fun test s = (Goal s; by (Asm_simp_tac 1));
|
paulson@14390
|
338 |
|
paulson@14390
|
339 |
test "x*k = k*(y::rat)";
|
paulson@14390
|
340 |
test "k = k*(y::rat)";
|
paulson@14390
|
341 |
test "a*(b*c) = (b::rat)";
|
paulson@14390
|
342 |
test "a*(b*c) = d*(b::rat)*(x*a)";
|
paulson@14390
|
343 |
|
paulson@14390
|
344 |
|
paulson@14390
|
345 |
test "(x*k) / (k*(y::rat)) = (uu::rat)";
|
paulson@14390
|
346 |
test "(k) / (k*(y::rat)) = (uu::rat)";
|
paulson@14390
|
347 |
test "(a*(b*c)) / ((b::rat)) = (uu::rat)";
|
paulson@14390
|
348 |
test "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)";
|
paulson@14390
|
349 |
|
paulson@14390
|
350 |
(*FIXME: what do we do about this?*)
|
paulson@14390
|
351 |
test "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z";
|
paulson@14390
|
352 |
*)
|