author | wenzelm |
Sat, 08 Jul 2006 12:54:30 +0200 | |
changeset 20044 | 92cc2f4c7335 |
parent 17613 | 072c21e31b42 |
child 29269 | 5c25a2012975 |
permissions | -rw-r--r-- |
4291 | 1 |
(* Title: Provers/Arith/cancel_sums.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen |
|
4 |
||
5 |
Cancel common summands of balanced expressions: |
|
6 |
||
7 |
A + x + B ~~ A' + x + B' == A + B ~~ A' + B' |
|
8 |
||
9 |
where + is AC0 and ~~ an appropriate balancing operation (e.g. =, <=, <, -). |
|
10 |
*) |
|
11 |
||
12 |
signature CANCEL_SUMS_DATA = |
|
13 |
sig |
|
14 |
(*abstract syntax*) |
|
15 |
val mk_sum: term list -> term |
|
16 |
val dest_sum: term -> term list |
|
17 |
val mk_bal: term * term -> term |
|
18 |
val dest_bal: term -> term * term |
|
19 |
(*rules*) |
|
20044
92cc2f4c7335
simprocs: no theory argument -- use simpset context instead;
wenzelm
parents:
17613
diff
changeset
|
20 |
val prove_conv: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm |
17613 | 21 |
val norm_tac: simpset -> tactic (*AC0 etc.*) |
22 |
val uncancel_tac: cterm -> tactic (*apply A ~~ B == x + A ~~ x + B*) |
|
4291 | 23 |
end; |
24 |
||
25 |
signature CANCEL_SUMS = |
|
26 |
sig |
|
20044
92cc2f4c7335
simprocs: no theory argument -- use simpset context instead;
wenzelm
parents:
17613
diff
changeset
|
27 |
val proc: simpset -> term -> thm option |
4291 | 28 |
end; |
29 |
||
30 |
||
31 |
functor CancelSumsFun(Data: CANCEL_SUMS_DATA): CANCEL_SUMS = |
|
32 |
struct |
|
33 |
||
34 |
||
35 |
(* cancel *) |
|
36 |
||
37 |
fun cons1 x (xs, y, z) = (x :: xs, y, z); |
|
38 |
fun cons2 y (x, ys, z) = (x, y :: ys, z); |
|
39 |
fun cons12 x y (xs, ys, z) = (x :: xs, y :: ys, z); |
|
40 |
||
4346 | 41 |
(*symmetric difference of multisets -- assumed to be sorted wrt. Logic.term_ord*) |
4291 | 42 |
fun cancel ts [] vs = (ts, [], vs) |
43 |
| cancel [] us vs = ([], us, vs) |
|
44 |
| cancel (t :: ts) (u :: us) vs = |
|
4452 | 45 |
(case Term.term_ord (t, u) of |
4346 | 46 |
EQUAL => cancel ts us (t :: vs) |
4291 | 47 |
| LESS => cons1 t (cancel ts (u :: us) vs) |
48 |
| GREATER => cons2 u (cancel (t :: ts) us vs)); |
|
49 |
||
50 |
||
51 |
(* uncancel *) |
|
52 |
||
53 |
fun uncancel_sums_tac _ [] = all_tac |
|
17613 | 54 |
| uncancel_sums_tac thy (t :: ts) = |
55 |
Data.uncancel_tac (Thm.cterm_of thy t) THEN |
|
56 |
uncancel_sums_tac thy ts; |
|
4291 | 57 |
|
58 |
||
59 |
(* the simplification procedure *) |
|
60 |
||
20044
92cc2f4c7335
simprocs: no theory argument -- use simpset context instead;
wenzelm
parents:
17613
diff
changeset
|
61 |
fun proc ss t = |
4291 | 62 |
(case try Data.dest_bal t of |
15531 | 63 |
NONE => NONE |
64 |
| SOME bal => |
|
4291 | 65 |
let |
20044
92cc2f4c7335
simprocs: no theory argument -- use simpset context instead;
wenzelm
parents:
17613
diff
changeset
|
66 |
val thy = ProofContext.theory_of (Simplifier.the_context ss); |
4452 | 67 |
val (ts, us) = pairself (sort Term.term_ord o Data.dest_sum) bal; |
4291 | 68 |
val (ts', us', vs) = cancel ts us []; |
69 |
in |
|
15531 | 70 |
if null vs then NONE |
71 |
else SOME |
|
20044
92cc2f4c7335
simprocs: no theory argument -- use simpset context instead;
wenzelm
parents:
17613
diff
changeset
|
72 |
(Data.prove_conv (uncancel_sums_tac thy vs) Data.norm_tac ss |
4291 | 73 |
(t, Data.mk_bal (Data.mk_sum ts', Data.mk_sum us'))) |
74 |
end); |
|
75 |
||
76 |
end; |