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