|
1 (* Title: HOL/Integ/simproc |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1998 University of Cambridge |
|
5 |
|
6 Simplification procedures for the integers |
|
7 |
|
8 This one cancels complementary terms in sums. Examples: |
|
9 x + (y + -x) = x + (-x + y) = y |
|
10 -x + (y + (x + z)) = -x + (x + (y + z)) = y + z |
|
11 |
|
12 Should be used with zdiff_def (to eliminate subtraction) and zadd_ac. |
|
13 *) |
|
14 |
|
15 |
|
16 structure Int_Cancel = |
|
17 struct |
|
18 |
|
19 val intT = Type ("IntDef.int", []); |
|
20 |
|
21 val zplus = Const ("op +", [intT,intT] ---> intT); |
|
22 val zminus = Const ("uminus", intT --> intT); |
|
23 |
|
24 val ssubst_left = read_instantiate [("P", "%x. ?lhs x = ?rhs")] ssubst; |
|
25 |
|
26 fun inst_left_commute ct = instantiate' [] [None, Some ct] zadd_left_commute; |
|
27 |
|
28 (*Can LOOP, so include only if the first occurrence at the very end*) |
|
29 fun inst_commute ct = instantiate' [] [None, Some ct] zadd_commute; |
|
30 |
|
31 fun terms (t as f$x$y) = |
|
32 if f=zplus then x :: terms y else [t] |
|
33 | terms t = [t]; |
|
34 |
|
35 val mk_sum = foldr1 (fn (x,y) => zplus $ x $ y); |
|
36 |
|
37 (*We map -t to t and (in other cases) t to -t. No need to check the type of |
|
38 uminus, since the simproc is only called on integer sums.*) |
|
39 fun negate (Const("uminus",_) $ t) = t |
|
40 | negate t = zminus $ t; |
|
41 |
|
42 (*These rules eliminate the first two terms, if they cancel*) |
|
43 val cancel_laws = [zadd_zminus_cancel, zminus_zadd_cancel]; |
|
44 |
|
45 exception Cancel; |
|
46 |
|
47 (*Cancels just the first occurrence of head', leaving the rest unchanged*) |
|
48 fun cancelled head' tail = |
|
49 let fun find ([], _) = raise Cancel |
|
50 | find (t::ts, heads) = if head' aconv t then rev heads @ ts |
|
51 else find (ts, t::heads) |
|
52 in mk_sum (find (tail, [])) end; |
|
53 |
|
54 |
|
55 val trace = ref false; |
|
56 |
|
57 fun proc sg _ lhs = |
|
58 let val _ = if !trace then prs ("lhs = " ^ string_of_cterm (cterm_of sg lhs)) |
|
59 else () |
|
60 val (head::tail) = terms lhs |
|
61 val head' = negate head |
|
62 val rhs = cancelled head' tail |
|
63 and chead' = Thm.cterm_of sg head' |
|
64 val comms = [inst_left_commute chead' RS ssubst_left, |
|
65 inst_commute chead' RS ssubst_left] |
|
66 val _ = if !trace then |
|
67 writeln ("rhs = " ^ string_of_cterm (Thm.cterm_of sg rhs)) |
|
68 else () |
|
69 val ct = Thm.cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))) |
|
70 (*Simplification is much faster than substitution, but loops for terms |
|
71 like (x + (-x + (-x + y))). Substitution finds the outermost -x, so |
|
72 is seems not to loop, and the counter prevents looping for sure.*) |
|
73 fun cancel_tac 0 = no_tac |
|
74 | cancel_tac n = |
|
75 (resolve_tac cancel_laws 1 ORELSE |
|
76 resolve_tac comms 1 THEN cancel_tac (n-1)); |
|
77 val thm = prove_goalw_cterm [] ct |
|
78 (fn _ => [cancel_tac (length tail + 1)]) |
|
79 handle ERROR => |
|
80 error("The error(s) above occurred while trying to prove " ^ |
|
81 string_of_cterm ct) |
|
82 in Some (meta_eq thm) end |
|
83 handle Cancel => None; |
|
84 |
|
85 |
|
86 val conv = |
|
87 Simplifier.mk_simproc "cancel_sums" |
|
88 [Thm.read_cterm (sign_of IntDef.thy) ("x + (y + (z::int))", intT)] |
|
89 proc; |
|
90 |
|
91 end; |
|
92 |
|
93 |
|
94 Addsimprocs [Int_Cancel.conv]; |
|
95 |