5589
|
1 |
(* Title: Provers/Arith/abel_cancel.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1998 University of Cambridge
|
|
5 |
|
|
6 |
Simplification procedures for abelian groups (e.g. integers, reals)
|
|
7 |
|
|
8 |
- Cancel complementary terms in sums
|
|
9 |
- Cancel like terms on opposite sides of relations
|
|
10 |
*)
|
|
11 |
|
|
12 |
|
|
13 |
signature ABEL_CANCEL =
|
|
14 |
sig
|
5610
|
15 |
val ss : simpset (*basic simpset of object-logtic*)
|
|
16 |
val eq_reflection : thm (*object-equality to meta-equality*)
|
5589
|
17 |
|
5610
|
18 |
val thy : theory (*the theory of the group*)
|
|
19 |
val T : typ (*the type of group elements*)
|
5589
|
20 |
|
5610
|
21 |
val zero : term
|
5589
|
22 |
val add_cancel_21 : thm
|
|
23 |
val add_cancel_end : thm
|
|
24 |
val add_left_cancel : thm
|
5610
|
25 |
val add_assoc : thm
|
|
26 |
val add_commute : thm
|
|
27 |
val add_left_commute : thm
|
|
28 |
val add_0 : thm
|
|
29 |
val add_0_right : thm
|
5589
|
30 |
|
|
31 |
val eq_diff_eq : thm
|
|
32 |
val eqI_rules : thm list
|
|
33 |
val dest_eqI : thm -> term
|
|
34 |
|
|
35 |
val diff_def : thm
|
|
36 |
val minus_add_distrib : thm
|
|
37 |
val minus_minus : thm
|
|
38 |
val minus_0 : thm
|
|
39 |
|
|
40 |
val add_inverses : thm list
|
|
41 |
val cancel_simps : thm list
|
|
42 |
end;
|
|
43 |
|
|
44 |
|
|
45 |
functor Abel_Cancel (Data: ABEL_CANCEL) =
|
|
46 |
let open Data in
|
|
47 |
struct
|
|
48 |
|
|
49 |
val prepare_ss = Data.ss addsimps [add_assoc, diff_def,
|
|
50 |
minus_add_distrib, minus_minus,
|
|
51 |
minus_0, add_0, add_0_right];
|
|
52 |
|
|
53 |
(*prove while suppressing timing information*)
|
|
54 |
fun prove ct = setmp Goals.proof_timing false (prove_goalw_cterm [] ct);
|
|
55 |
|
|
56 |
val plus = Const ("op +", [Data.T,Data.T] ---> Data.T);
|
|
57 |
val minus = Const ("uminus", Data.T --> Data.T);
|
|
58 |
|
|
59 |
(*Cancel corresponding terms on the two sides of the equation, NOT on
|
|
60 |
the same side!*)
|
|
61 |
val cancel_ss =
|
|
62 |
Data.ss addsimps [add_cancel_21, add_cancel_end, minus_minus] @
|
|
63 |
Data.cancel_simps;
|
|
64 |
|
|
65 |
val inverse_ss = Data.ss addsimps Data.add_inverses;
|
|
66 |
|
|
67 |
fun mk_sum [] = Data.zero
|
|
68 |
| mk_sum tms = foldr1 (fn (x,y) => plus $ x $ y) tms;
|
|
69 |
|
|
70 |
(*We map -t to t and (in other cases) t to -t. No need to check the type of
|
|
71 |
uminus, since the simproc is only called on sums of type T.*)
|
|
72 |
fun negate (Const("uminus",_) $ t) = t
|
|
73 |
| negate t = minus $ t;
|
|
74 |
|
|
75 |
(*Flatten a formula built from +, binary - and unary -.
|
|
76 |
No need to check types PROVIDED they are checked upon entry!*)
|
|
77 |
fun add_terms neg (Const ("op +", _) $ x $ y, ts) =
|
|
78 |
add_terms neg (x, add_terms neg (y, ts))
|
|
79 |
| add_terms neg (Const ("op -", _) $ x $ y, ts) =
|
|
80 |
add_terms neg (x, add_terms (not neg) (y, ts))
|
|
81 |
| add_terms neg (Const ("uminus", _) $ x, ts) =
|
|
82 |
add_terms (not neg) (x, ts)
|
|
83 |
| add_terms neg (x, ts) =
|
|
84 |
(if neg then negate x else x) :: ts;
|
|
85 |
|
|
86 |
fun terms fml = add_terms false (fml, []);
|
|
87 |
|
|
88 |
exception Cancel;
|
|
89 |
|
|
90 |
(*Cancels just the first occurrence of u, leaving the rest unchanged*)
|
|
91 |
fun cancelled (u, t::ts) = if u aconv t then ts else t :: cancelled(u,ts)
|
|
92 |
| cancelled _ = raise Cancel;
|
|
93 |
|
|
94 |
|
|
95 |
val trace = ref false;
|
|
96 |
|
|
97 |
(*Make a simproc to cancel complementary terms in sums. Examples:
|
|
98 |
x-x = 0 x+(y-x) = y -x+(y+(x+z)) = y+z
|
|
99 |
It will unfold the definition of diff and associate to the right if
|
|
100 |
necessary. Rewriting is faster if the formula is already
|
|
101 |
in that form.
|
|
102 |
*)
|
|
103 |
|
|
104 |
fun sum_proc sg _ lhs =
|
|
105 |
let val _ = if !trace then writeln ("cancel_sums: LHS = " ^
|
|
106 |
string_of_cterm (cterm_of sg lhs))
|
|
107 |
else ()
|
|
108 |
val (head::tail) = terms lhs
|
|
109 |
val head' = negate head
|
|
110 |
val rhs = mk_sum (cancelled (head',tail))
|
|
111 |
and chead' = Thm.cterm_of sg head'
|
|
112 |
val _ = if !trace then
|
|
113 |
writeln ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
|
|
114 |
else ()
|
5610
|
115 |
val ct = Thm.cterm_of sg (Logic.mk_equals (lhs, rhs))
|
5589
|
116 |
val thm = prove ct
|
5610
|
117 |
(fn _ => [rtac eq_reflection 1,
|
|
118 |
simp_tac prepare_ss 1,
|
5589
|
119 |
IF_UNSOLVED (simp_tac cancel_ss 1),
|
|
120 |
IF_UNSOLVED (simp_tac inverse_ss 1)])
|
|
121 |
handle ERROR =>
|
|
122 |
error("cancel_sums simproc:\nfailed to prove " ^
|
|
123 |
string_of_cterm ct)
|
5610
|
124 |
in Some thm end
|
5589
|
125 |
handle Cancel => None;
|
|
126 |
|
|
127 |
|
|
128 |
val sum_conv =
|
|
129 |
Simplifier.mk_simproc "cancel_sums"
|
|
130 |
(map (Thm.read_cterm (sign_of Data.thy))
|
|
131 |
[("x + y", Data.T), ("x - y", Data.T)])
|
|
132 |
sum_proc;
|
|
133 |
|
|
134 |
|
|
135 |
(*A simproc to cancel like terms on the opposite sides of relations:
|
|
136 |
(x + y - z < -z + x) = (y < 0)
|
|
137 |
Works for (=) and (<=) as well as (<), if the necessary rules are supplied.
|
|
138 |
Reduces the problem to subtraction and calls the previous simproc.
|
|
139 |
*)
|
|
140 |
|
|
141 |
(*Cancel the FIRST occurrence of a term. If it's repeated, then repeated
|
|
142 |
calls to the simproc will be needed.*)
|
|
143 |
fun cancel1 ([], u) = raise Match (*impossible: it's a common term*)
|
|
144 |
| cancel1 (t::ts, u) = if t aconv u then ts
|
|
145 |
else t :: cancel1 (ts,u);
|
|
146 |
|
|
147 |
|
|
148 |
val sum_cancel_ss = Data.ss addsimprocs [sum_conv]
|
|
149 |
addsimps [add_0, add_0_right];
|
|
150 |
|
|
151 |
val add_ac_ss = Data.ss addsimps [add_assoc,add_commute,add_left_commute];
|
|
152 |
|
|
153 |
fun rel_proc sg _ (lhs as (rel$lt$rt)) =
|
|
154 |
let val _ = if !trace then writeln ("cancel_relations: LHS = " ^
|
|
155 |
string_of_cterm (cterm_of sg lhs))
|
|
156 |
else ()
|
|
157 |
val ltms = terms lt
|
|
158 |
and rtms = terms rt
|
|
159 |
val common = (*inter_term miscounts repetitions, so squash them*)
|
|
160 |
gen_distinct (op aconv) (inter_term (ltms, rtms))
|
|
161 |
val _ = if null common then raise Cancel (*nothing to do*)
|
|
162 |
else ()
|
|
163 |
|
|
164 |
fun cancelled tms = mk_sum (foldl cancel1 (tms, common))
|
|
165 |
|
|
166 |
val lt' = cancelled ltms
|
|
167 |
and rt' = cancelled rtms
|
|
168 |
|
|
169 |
val rhs = rel$lt'$rt'
|
|
170 |
val _ = if !trace then
|
|
171 |
writeln ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
|
|
172 |
else ()
|
5610
|
173 |
val ct = Thm.cterm_of sg (Logic.mk_equals (lhs,rhs))
|
5589
|
174 |
|
|
175 |
val thm = prove ct
|
5610
|
176 |
(fn _ => [rtac eq_reflection 1,
|
|
177 |
resolve_tac eqI_rules 1,
|
5589
|
178 |
simp_tac prepare_ss 1,
|
|
179 |
simp_tac sum_cancel_ss 1,
|
|
180 |
IF_UNSOLVED (simp_tac add_ac_ss 1)])
|
|
181 |
handle ERROR =>
|
|
182 |
error("cancel_relations simproc:\nfailed to prove " ^
|
|
183 |
string_of_cterm ct)
|
5610
|
184 |
in Some thm end
|
5589
|
185 |
handle Cancel => None;
|
|
186 |
|
|
187 |
val rel_conv =
|
|
188 |
Simplifier.mk_simproc "cancel_relations"
|
|
189 |
(map (Thm.cterm_of (sign_of Data.thy) o Data.dest_eqI) eqI_rules)
|
|
190 |
rel_proc;
|
|
191 |
|
|
192 |
end
|
|
193 |
end;
|
|
194 |
|