1 (* Title: HOL/Integ/simproc |
1 (* Title: HOL/Integ/simproc |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1998 University of Cambridge |
4 Copyright 1998 University of Cambridge |
5 |
5 |
6 Simplification procedures for abelian groups (e.g. integers, reals) |
6 Apply Abel_Cancel to the integers |
7 *) |
7 *) |
8 |
8 |
9 |
9 |
|
10 (*** Two lemmas needed for the simprocs ***) |
10 |
11 |
11 (*Deletion of other terms in the formula, seeking the -x at the front of z*) |
12 (*Deletion of other terms in the formula, seeking the -x at the front of z*) |
12 Goal "((x::int) + (y + z) = y + u) = ((x + z) = u)"; |
13 val zadd_cancel_21 = prove_goal IntDef.thy |
13 by (stac zadd_left_commute 1); |
14 "((x::int) + (y + z) = y + u) = ((x + z) = u)" |
14 by (rtac zadd_left_cancel 1); |
15 (fn _ => [stac zadd_left_commute 1, |
15 qed "zadd_cancel_21"; |
16 rtac zadd_left_cancel 1]); |
16 |
17 |
17 (*A further rule to deal with the case that |
18 (*A further rule to deal with the case that |
18 everything gets cancelled on the right.*) |
19 everything gets cancelled on the right.*) |
19 Goal "((x::int) + (y + z) = y) = (x = -z)"; |
20 val zadd_cancel_end = prove_goal IntDef.thy |
20 by (stac zadd_left_commute 1); |
21 "((x::int) + (y + z) = y) = (x = -z)" |
21 by (res_inst_tac [("t", "y")] (zadd_nat0_right RS subst) 1 |
22 (fn _ => [stac zadd_left_commute 1, |
22 THEN stac zadd_left_cancel 1); |
23 res_inst_tac [("t", "y")] (zadd_nat0_right RS subst) 1, |
23 by (simp_tac (simpset() addsimps [eq_zdiff_eq RS sym]) 1); |
24 stac zadd_left_cancel 1, |
24 qed "zadd_cancel_minus"; |
25 simp_tac (simpset() addsimps [eq_zdiff_eq RS sym]) 1]); |
25 |
26 |
26 |
27 |
27 val prepare_ss = HOL_ss addsimps [zadd_assoc, zdiff_def, |
28 structure Int_Cancel_Data = |
28 zminus_zadd_distrib, zminus_zminus, |
29 struct |
29 zminus_nat0, zadd_nat0, zadd_nat0_right]; |
30 val ss = HOL_ss |
|
31 val mk_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq |
|
32 fun mk_meta_eq r = r RS eq_reflection |
|
33 |
|
34 val thy = IntDef.thy |
|
35 val T = Type ("IntDef.int", []) |
|
36 val zero = Const ("IntDef.int", HOLogic.natT --> T) $ HOLogic.zero |
|
37 val add_cancel_21 = zadd_cancel_21 |
|
38 val add_cancel_end = zadd_cancel_end |
|
39 val add_left_cancel = zadd_left_cancel |
|
40 val add_assoc = zadd_assoc |
|
41 val add_commute = zadd_commute |
|
42 val add_left_commute = zadd_left_commute |
|
43 val add_0 = zadd_nat0 |
|
44 val add_0_right = zadd_nat0_right |
|
45 |
|
46 val eq_diff_eq = eq_zdiff_eq |
|
47 val eqI_rules = [zless_eqI, zeq_eqI, zle_eqI] |
|
48 fun dest_eqI th = |
|
49 #1 (HOLogic.dest_bin "op =" HOLogic.boolT |
|
50 (HOLogic.dest_Trueprop (concl_of th))) |
|
51 |
|
52 val diff_def = zdiff_def |
|
53 val minus_add_distrib = zminus_zadd_distrib |
|
54 val minus_minus = zminus_zminus |
|
55 val minus_0 = zminus_nat0 |
|
56 val add_inverses = [zadd_zminus_inverse, zadd_zminus_inverse2]; |
|
57 val cancel_simps = [zadd_zminus_cancel, zminus_zadd_cancel] |
|
58 end; |
|
59 |
|
60 structure Int_Cancel = Abel_Cancel (Int_Cancel_Data); |
|
61 |
|
62 Addsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv]; |
30 |
63 |
31 |
64 |
32 |
|
33 (*prove while suppressing timing information*) |
|
34 fun prove ct = setmp Goals.proof_timing false (prove_goalw_cterm [] ct); |
|
35 |
|
36 |
|
37 (*This one cancels complementary terms in sums. Examples: |
|
38 x-x = 0 x+(y-x) = y -x+(y+(x+z)) = y+z |
|
39 It will unfold the definition of diff and associate to the right if |
|
40 necessary. With big formulae, rewriting is faster if the formula is already |
|
41 in that form. |
|
42 *) |
|
43 structure Sum_Cancel = |
|
44 struct |
|
45 |
|
46 val thy = IntDef.thy; |
|
47 |
|
48 val intT = Type ("IntDef.int", []); |
|
49 |
|
50 val zplus = Const ("op +", [intT,intT] ---> intT); |
|
51 val zminus = Const ("uminus", intT --> intT); |
|
52 |
|
53 val zero = Const ("IntDef.int", HOLogic.natT --> intT) $ HOLogic.zero; |
|
54 |
|
55 (*These rules eliminate the first two terms, if they cancel*) |
|
56 val cancel_laws = |
|
57 [zadd_zminus_inverse_nat, zadd_zminus_inverse_nat2, |
|
58 zadd_zminus_cancel, zminus_zadd_cancel, |
|
59 zadd_cancel_21, zadd_cancel_minus, zminus_zminus]; |
|
60 |
|
61 |
|
62 val cancel_ss = HOL_ss addsimps cancel_laws; |
|
63 |
|
64 fun mk_sum [] = zero |
|
65 | mk_sum tms = foldr1 (fn (x,y) => zplus $ x $ y) tms; |
|
66 |
|
67 (*We map -t to t and (in other cases) t to -t. No need to check the type of |
|
68 uminus, since the simproc is only called on integer sums.*) |
|
69 fun negate (Const("uminus",_) $ t) = t |
|
70 | negate t = zminus $ t; |
|
71 |
|
72 (*Flatten a formula built from +, binary - and unary -. |
|
73 No need to check types PROVIDED they are checked upon entry!*) |
|
74 fun add_terms neg (Const ("op +", _) $ x $ y, ts) = |
|
75 add_terms neg (x, add_terms neg (y, ts)) |
|
76 | add_terms neg (Const ("op -", _) $ x $ y, ts) = |
|
77 add_terms neg (x, add_terms (not neg) (y, ts)) |
|
78 | add_terms neg (Const ("uminus", _) $ x, ts) = |
|
79 add_terms (not neg) (x, ts) |
|
80 | add_terms neg (x, ts) = |
|
81 (if neg then negate x else x) :: ts; |
|
82 |
|
83 fun terms fml = add_terms false (fml, []); |
|
84 |
|
85 exception Cancel; |
|
86 |
|
87 (*Cancels just the first occurrence of head', leaving the rest unchanged*) |
|
88 fun cancelled head' tail = |
|
89 let fun find ([], _) = raise Cancel |
|
90 | find (t::ts, heads) = if head' aconv t then rev heads @ ts |
|
91 else find (ts, t::heads) |
|
92 in mk_sum (find (tail, [])) end; |
|
93 |
|
94 |
|
95 val trace = ref false; |
|
96 |
|
97 fun proc sg _ lhs = |
|
98 let val _ = if !trace then writeln ("cancel_sums: LHS = " ^ |
|
99 string_of_cterm (cterm_of sg lhs)) |
|
100 else () |
|
101 val (head::tail) = terms lhs |
|
102 val head' = negate head |
|
103 val rhs = cancelled head' tail |
|
104 and chead' = Thm.cterm_of sg head' |
|
105 val _ = if !trace then |
|
106 writeln ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs)) |
|
107 else () |
|
108 val ct = Thm.cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))) |
|
109 val thm = prove ct |
|
110 (fn _ => [simp_tac prepare_ss 1, |
|
111 IF_UNSOLVED (simp_tac cancel_ss 1)]) |
|
112 handle ERROR => |
|
113 error("cancel_sums simproc:\nThe error(s) above occurred while trying to prove " ^ |
|
114 string_of_cterm ct) |
|
115 in Some (mk_meta_eq thm) end |
|
116 handle Cancel => None; |
|
117 |
|
118 |
|
119 val conv = |
|
120 Simplifier.mk_simproc "cancel_sums" |
|
121 (map (Thm.read_cterm (sign_of thy)) |
|
122 [("x + y", intT), ("x - y", intT)]) |
|
123 proc; |
|
124 |
|
125 end; |
|
126 |
|
127 |
|
128 |
|
129 Addsimprocs [Sum_Cancel.conv]; |
|
130 |
|
131 |
|
132 (** The idea is to cancel like terms on opposite sides via subtraction **) |
|
133 |
|
134 Goal "(x::int) - y = x' - y' ==> (x<y) = (x'<y')"; |
|
135 by (asm_simp_tac (simpset() addsimps [zless_def]) 1); |
|
136 qed "zless_eqI"; |
|
137 |
|
138 Goal "(x::int) - y = x' - y' ==> (y<=x) = (y'<=x')"; |
|
139 bd zless_eqI 1; |
|
140 by (asm_simp_tac (simpset() addsimps [zle_def]) 1); |
|
141 qed "zle_eqI"; |
|
142 |
|
143 Goal "(x::int) - y = x' - y' ==> (x=y) = (x'=y')"; |
|
144 by Safe_tac; |
|
145 by (asm_full_simp_tac (simpset() addsimps [eq_zdiff_eq]) 1); |
|
146 by (asm_full_simp_tac (simpset() addsimps [zdiff_eq_eq]) 1); |
|
147 qed "zeq_eqI"; |
|
148 |
|
149 |
|
150 |
|
151 (** For simplifying relations **) |
|
152 |
|
153 structure Rel_Cancel = |
|
154 struct |
|
155 |
|
156 (*Cancel the FIRST occurrence of a term. If it's repeated, then repeated |
|
157 calls to the simproc will be needed.*) |
|
158 fun cancel1 ([], u) = raise Match (*impossible: it's a common term*) |
|
159 | cancel1 (t::ts, u) = if t aconv u then ts |
|
160 else t :: cancel1 (ts,u); |
|
161 |
|
162 |
|
163 exception Relation; |
|
164 |
|
165 val trace = ref false; |
|
166 |
|
167 val sum_cancel_ss = HOL_ss addsimprocs [Sum_Cancel.conv] |
|
168 addsimps [zadd_nat0, zadd_nat0_right]; |
|
169 |
|
170 fun proc sg _ (lhs as (rel$lt$rt)) = |
|
171 let val _ = if !trace then writeln ("cancel_relations: LHS = " ^ |
|
172 string_of_cterm (cterm_of sg lhs)) |
|
173 else () |
|
174 val ltms = Sum_Cancel.terms lt |
|
175 and rtms = Sum_Cancel.terms rt |
|
176 val common = gen_distinct (op aconv) |
|
177 (inter_term (ltms, rtms)) |
|
178 val _ = if null common then raise Relation (*nothing to do*) |
|
179 else () |
|
180 |
|
181 fun cancelled tms = Sum_Cancel.mk_sum (foldl cancel1 (tms, common)) |
|
182 |
|
183 val lt' = cancelled ltms |
|
184 and rt' = cancelled rtms |
|
185 |
|
186 val rhs = rel$lt'$rt' |
|
187 val _ = if !trace then |
|
188 writeln ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs)) |
|
189 else () |
|
190 val ct = Thm.cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))) |
|
191 |
|
192 val thm = prove ct |
|
193 (fn _ => [resolve_tac [zless_eqI, zeq_eqI, zle_eqI] 1, |
|
194 simp_tac prepare_ss 1, |
|
195 simp_tac sum_cancel_ss 1, |
|
196 IF_UNSOLVED |
|
197 (simp_tac (HOL_ss addsimps zadd_ac) 1)]) |
|
198 handle ERROR => |
|
199 error("cancel_relations simproc:\nThe error(s) above occurred while trying to prove " ^ |
|
200 string_of_cterm ct) |
|
201 in Some (mk_meta_eq thm) end |
|
202 handle Relation => None; |
|
203 |
|
204 |
|
205 val conv = |
|
206 Simplifier.mk_simproc "cancel_relations" |
|
207 (map (Thm.read_cterm (sign_of thy)) |
|
208 [("x < (y::int)", HOLogic.boolT), |
|
209 ("x = (y::int)", HOLogic.boolT), |
|
210 ("x <= (y::int)", HOLogic.boolT)]) |
|
211 proc; |
|
212 |
|
213 end; |
|
214 |
|
215 |
|
216 |
|
217 Addsimprocs [Rel_Cancel.conv]; |
|