author | huffman |
Fri, 20 Jul 2012 10:53:25 +0200 | |
changeset 48372 | 868dc809c8a2 |
parent 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 |
|
48372
868dc809c8a2
make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
huffman
parents:
42361
diff
changeset
|
16 |
val mk_plus: term * term -> term |
4291 | 17 |
val mk_bal: term * term -> term |
18 |
val dest_bal: term -> term * term |
|
19 |
(*rules*) |
|
17613 | 20 |
val norm_tac: simpset -> tactic (*AC0 etc.*) |
48372
868dc809c8a2
make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
huffman
parents:
42361
diff
changeset
|
21 |
val cancel_rule: thm (* x + A ~~ x + B == A ~~ 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 |
(* the simplification procedure *) |
|
50 |
||
20044
92cc2f4c7335
simprocs: no theory argument -- use simpset context instead;
wenzelm
parents:
17613
diff
changeset
|
51 |
fun proc ss t = |
4291 | 52 |
(case try Data.dest_bal t of |
15531 | 53 |
NONE => NONE |
54 |
| SOME bal => |
|
4291 | 55 |
let |
42361 | 56 |
val thy = Proof_Context.theory_of (Simplifier.the_context ss); |
35408 | 57 |
val (ts, us) = pairself (sort Term_Ord.term_ord o Data.dest_sum) bal; |
4291 | 58 |
val (ts', us', vs) = cancel ts us []; |
59 |
in |
|
15531 | 60 |
if null vs then NONE |
48372
868dc809c8a2
make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
huffman
parents:
42361
diff
changeset
|
61 |
else |
868dc809c8a2
make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
huffman
parents:
42361
diff
changeset
|
62 |
let |
868dc809c8a2
make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
huffman
parents:
42361
diff
changeset
|
63 |
val cert = Thm.cterm_of thy |
868dc809c8a2
make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
huffman
parents:
42361
diff
changeset
|
64 |
val t' = Data.mk_sum ts' |
868dc809c8a2
make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
huffman
parents:
42361
diff
changeset
|
65 |
val u' = Data.mk_sum us' |
868dc809c8a2
make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
huffman
parents:
42361
diff
changeset
|
66 |
val v = Data.mk_sum vs |
868dc809c8a2
make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
huffman
parents:
42361
diff
changeset
|
67 |
val t1 = Data.mk_bal (Data.mk_plus (v, t'), Data.mk_plus (v, u')) |
868dc809c8a2
make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
huffman
parents:
42361
diff
changeset
|
68 |
val t2 = Data.mk_bal (t', u') |
868dc809c8a2
make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
huffman
parents:
42361
diff
changeset
|
69 |
val goal1 = Thm.cterm_of thy (Logic.mk_equals (t, t1)) |
868dc809c8a2
make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
huffman
parents:
42361
diff
changeset
|
70 |
val goal2 = Thm.cterm_of thy (Logic.mk_equals (t1, t2)) |
868dc809c8a2
make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
huffman
parents:
42361
diff
changeset
|
71 |
val thm1 = Goal.prove_internal [] goal1 (K (Data.norm_tac ss)) |
868dc809c8a2
make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
huffman
parents:
42361
diff
changeset
|
72 |
val thm2 = Goal.prove_internal [] goal2 (K (rtac Data.cancel_rule 1)) |
868dc809c8a2
make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
huffman
parents:
42361
diff
changeset
|
73 |
in |
868dc809c8a2
make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
huffman
parents:
42361
diff
changeset
|
74 |
SOME (Thm.transitive thm1 thm2) |
868dc809c8a2
make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
huffman
parents:
42361
diff
changeset
|
75 |
end |
4291 | 76 |
end); |
77 |
||
78 |
end; |