6 Simplification procedures for abelian groups (e.g. integers, reals) |
6 Simplification procedures for abelian groups (e.g. integers, reals) |
7 |
7 |
8 - Cancel complementary terms in sums |
8 - Cancel complementary terms in sums |
9 - Cancel like terms on opposite sides of relations |
9 - Cancel like terms on opposite sides of relations |
10 |
10 |
|
11 Modification in May 2004 by Steven Obua: polymorphic types work also now |
|
12 Modification in June 2005 by Tobias Nipkow: cancel_sums works in general now |
|
13 (using Clemens Ballarin's code for ordered rewriting in abelian groups) |
|
14 and the whole file is reduced to a fraction of its former size. |
11 *) |
15 *) |
12 |
|
13 (* Modification in May 2004 by Steven Obua: polymorphic types work also now *) |
|
14 |
16 |
15 signature ABEL_CANCEL = |
17 signature ABEL_CANCEL = |
16 sig |
18 sig |
17 val ss : simpset (*basic simpset of object-logic*) |
19 val cancel_ss : simpset (*abelian group cancel simpset*) |
18 val eq_reflection : thm (*object-equality to meta-equality*) |
20 val thy_ref : theory_ref (*signature of the theory of the group*) |
19 |
21 val T : typ (*the type of group elements*) |
20 val thy_ref : theory_ref (*signature of the theory of the group*) |
22 val eq_reflection : thm (*object-equality to meta-equality*) |
21 val T : typ (*the type of group elements*) |
23 val eqI_rules : thm list |
22 |
24 val dest_eqI : thm -> term |
23 val restrict_to_left : thm |
|
24 val add_cancel_21 : thm |
|
25 val add_cancel_end : thm |
|
26 val add_left_cancel : thm |
|
27 val add_assoc : thm |
|
28 val add_commute : thm |
|
29 val add_left_commute : thm |
|
30 val add_0 : thm |
|
31 val add_0_right : thm |
|
32 |
|
33 val eq_diff_eq : thm |
|
34 val eqI_rules : thm list |
|
35 val dest_eqI : thm -> term |
|
36 |
|
37 val diff_def : thm |
|
38 val minus_add_distrib : thm |
|
39 val minus_minus : thm |
|
40 val minus_0 : thm |
|
41 |
|
42 val add_inverses : thm list |
|
43 val cancel_simps : thm list |
|
44 end; |
25 end; |
45 |
26 |
46 |
27 |
47 functor Abel_Cancel (Data: ABEL_CANCEL) = |
28 functor Abel_Cancel (Data: ABEL_CANCEL) = |
48 struct |
29 struct |
49 |
30 |
50 open Data; |
31 open Data; |
51 |
32 |
52 val prepare_ss = Data.ss addsimps [add_assoc, diff_def, |
|
53 minus_add_distrib, minus_minus, |
|
54 minus_0, add_0, add_0_right]; |
|
55 |
|
56 |
|
57 fun zero t = Const ("0", t); |
33 fun zero t = Const ("0", t); |
58 fun plus t = Const ("op +", [t,t] ---> t); |
|
59 fun minus t = Const ("uminus", t --> t); |
34 fun minus t = Const ("uminus", t --> t); |
60 |
35 |
61 (*Cancel corresponding terms on the two sides of the equation, NOT on |
36 fun add_terms pos (Const ("op +", _) $ x $ y, ts) = |
62 the same side!*) |
37 add_terms pos (x, add_terms pos (y, ts)) |
63 val cancel_ss = |
38 | add_terms pos (Const ("op -", _) $ x $ y, ts) = |
64 Data.ss addsimps [add_cancel_21, add_cancel_end, minus_minus] @ |
39 add_terms pos (x, add_terms (not pos) (y, ts)) |
65 (map (fn th => th RS restrict_to_left) Data.cancel_simps); |
40 | add_terms pos (Const ("uminus", _) $ x, ts) = |
|
41 add_terms (not pos) (x, ts) |
|
42 | add_terms pos (x, ts) = (pos,x) :: ts; |
66 |
43 |
67 val inverse_ss = Data.ss addsimps Data.add_inverses @ Data.cancel_simps; |
44 fun terms fml = add_terms true (fml, []); |
68 |
45 |
69 fun mk_sum ty [] = zero ty |
46 fun zero1 pt (u as (c as Const("op +",_)) $ x $ y) = |
70 | mk_sum ty tms = foldr1 (fn (x,y) => (plus ty) $ x $ y) tms; |
47 (case zero1 pt x of NONE => (case zero1 pt y of NONE => NONE |
71 |
48 | SOME z => SOME(c $ x $ z)) |
72 (*We map -t to t and (in other cases) t to -t. No need to check the type of |
49 | SOME z => SOME(c $ z $ y)) |
73 uminus, since the simproc is only called on sums of type T.*) |
50 | zero1 (pos,t) (u as (c as Const("op -",_)) $ x $ y) = |
74 fun negate (Const("uminus",_) $ t) = t |
51 (case zero1 (pos,t) x of |
75 | negate t = (minus (fastype_of t)) $ t; |
52 NONE => (case zero1 (not pos,t) y of NONE => NONE |
76 |
53 | SOME z => SOME(c $ x $ z)) |
77 (*Flatten a formula built from +, binary - and unary -. |
54 | SOME z => SOME(c $ z $ y)) |
78 No need to check types PROVIDED they are checked upon entry!*) |
55 | zero1 (pos,t) (u as (c as Const("uminus",_)) $ x) = |
79 fun add_terms neg (Const ("op +", _) $ x $ y, ts) = |
56 (case zero1 (not pos,t) x of NONE => NONE |
80 add_terms neg (x, add_terms neg (y, ts)) |
57 | SOME z => SOME(c $ z)) |
81 | add_terms neg (Const ("op -", _) $ x $ y, ts) = |
58 | zero1 (pos,t) u = |
82 add_terms neg (x, add_terms (not neg) (y, ts)) |
59 if pos andalso (t aconv u) then SOME(zero(fastype_of t)) else NONE |
83 | add_terms neg (Const ("uminus", _) $ x, ts) = |
|
84 add_terms (not neg) (x, ts) |
|
85 | add_terms neg (x, ts) = |
|
86 (if neg then negate x else x) :: ts; |
|
87 |
|
88 fun terms fml = add_terms false (fml, []); |
|
89 |
60 |
90 exception Cancel; |
61 exception Cancel; |
91 |
62 |
92 (*Cancels just the first occurrence of u, leaving the rest unchanged*) |
|
93 fun cancelled (u, t::ts) = if u aconv t then ts else t :: cancelled(u,ts) |
|
94 | cancelled _ = raise Cancel; |
|
95 |
|
96 |
|
97 val trace = ref false; |
63 val trace = ref false; |
98 |
64 |
99 (*Make a simproc to cancel complementary terms in sums. Examples: |
65 fun find_common _ [] _ = raise Cancel |
100 x-x = 0 x+(y-x) = y -x+(y+(x+z)) = y+z |
66 | find_common opp ((p,l)::ls) rs = |
101 It will unfold the definition of diff and associate to the right if |
67 let val pr = if opp then not p else p |
102 necessary. Rewriting is faster if the formula is already |
68 in if exists (fn (q,r) => pr = q andalso l aconv r) rs then (p,l) |
103 in that form. |
69 else find_common opp ls rs |
104 *) |
70 end |
105 |
71 |
106 fun sum_proc sg _ lhs = |
72 (* turns t1(t) OP t2(t) into t1(0) OP t2(0) where OP can be +, -, =, etc. |
107 let val _ = if !trace then tracing ("cancel_sums: LHS = " ^ |
73 If OP = +, it must be t2(-t) rather than t2(t) |
108 string_of_cterm (cterm_of sg lhs)) |
74 *) |
109 else () |
75 fun cancel sg t = |
110 val (head::tail) = terms lhs |
76 let val _ = if !trace |
111 val head' = negate head |
77 then tracing ("Abel cancel: " ^ string_of_cterm (cterm_of sg t)) |
112 val rhs = mk_sum (fastype_of head) (cancelled (head',tail)) |
78 else () |
113 and chead' = Thm.cterm_of sg head' |
79 val c $ lhs $ rhs = t |
114 val _ = if !trace then |
80 val opp = case c of Const("op +",_) => true | _ => false; |
115 tracing ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs)) |
81 val (pos,l) = find_common opp (terms lhs) (terms rhs) |
116 else () |
82 val posr = if opp then not pos else pos |
117 val thm = Tactic.prove sg [] [] (Logic.mk_equals (lhs, rhs)) |
83 val t' = c $ (the(zero1 (pos,l) lhs)) $ (the(zero1 (posr,l) rhs)) |
118 (fn _ => rtac eq_reflection 1 THEN |
84 val _ = if !trace |
119 simp_tac prepare_ss 1 THEN |
85 then tracing ("cancelled: " ^ string_of_cterm (cterm_of sg t')) |
120 IF_UNSOLVED (simp_tac cancel_ss 1) THEN |
86 else () |
121 IF_UNSOLVED (simp_tac inverse_ss 1)) |
87 in t' end; |
|
88 |
|
89 (* A simproc to cancel complementary terms in arbitrary sums. *) |
|
90 |
|
91 fun sum_proc sg _ t = |
|
92 let val t' = cancel sg t |
|
93 val thm = Tactic.prove sg [] [] (Logic.mk_equals (t, t')) |
|
94 (fn _ => simp_tac cancel_ss 1) |
122 in SOME thm end |
95 in SOME thm end |
123 handle Cancel => NONE; |
96 handle Cancel => NONE; |
124 |
|
125 |
97 |
126 val sum_conv = |
98 val sum_conv = |
127 Simplifier.mk_simproc "cancel_sums" |
99 Simplifier.mk_simproc "cancel_sums" |
128 (map (Drule.cterm_fun Logic.varify o Thm.read_cterm (Theory.deref thy_ref)) |
100 (map (Drule.cterm_fun Logic.varify o Thm.read_cterm (Theory.deref thy_ref)) |
129 [("x + y", Data.T), ("x - y", Data.T)]) (* FIXME depends on concrete syntax !???!!??! *) |
101 [("x + y", Data.T), ("x - y", Data.T)]) (* FIXME depends on concrete syntax !???!!??! *) |
131 |
103 |
132 |
104 |
133 (*A simproc to cancel like terms on the opposite sides of relations: |
105 (*A simproc to cancel like terms on the opposite sides of relations: |
134 (x + y - z < -z + x) = (y < 0) |
106 (x + y - z < -z + x) = (y < 0) |
135 Works for (=) and (<=) as well as (<), if the necessary rules are supplied. |
107 Works for (=) and (<=) as well as (<), if the necessary rules are supplied. |
136 Reduces the problem to subtraction and calls the previous simproc. |
108 Reduces the problem to subtraction. |
137 *) |
109 *) |
138 |
110 |
139 (*Cancel the FIRST occurrence of a term. If it's repeated, then repeated |
111 fun rel_proc sg _ t = |
140 calls to the simproc will be needed.*) |
112 let val t' = cancel sg t |
141 fun cancel1 ([], u) = raise Match (*impossible: it's a common term*) |
113 val thm = Tactic.prove sg [] [] (Logic.mk_equals (t, t')) |
142 | cancel1 (t::ts, u) = if t aconv u then ts |
|
143 else t :: cancel1 (ts,u); |
|
144 |
|
145 |
|
146 val sum_cancel_ss = Data.ss addsimprocs [sum_conv] |
|
147 addsimps [add_0, add_0_right]; |
|
148 |
|
149 val add_ac_ss = Data.ss addsimps [add_assoc,add_commute,add_left_commute]; |
|
150 |
|
151 fun rel_proc sg _ (lhs as (rel$lt$rt)) = |
|
152 let val _ = if !trace then tracing ("cancel_relations: LHS = " ^ |
|
153 string_of_cterm (cterm_of sg lhs)) |
|
154 else () |
|
155 val ltms = terms lt |
|
156 and rtms = terms rt |
|
157 val ty = fastype_of lt |
|
158 val common = (*inter_term miscounts repetitions, so squash them*) |
|
159 gen_distinct (op aconv) (inter_term (ltms, rtms)) |
|
160 val _ = if null common then raise Cancel (*nothing to do*) |
|
161 else () |
|
162 |
|
163 fun cancelled tms = mk_sum ty (Library.foldl cancel1 (tms, common)) |
|
164 |
|
165 val lt' = cancelled ltms |
|
166 and rt' = cancelled rtms |
|
167 |
|
168 val rhs = rel$lt'$rt' |
|
169 val _ = if lhs aconv rhs then raise Cancel (*nothing to do*) |
|
170 else () |
|
171 val _ = if !trace then |
|
172 tracing ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs)) |
|
173 else () |
|
174 |
|
175 val thm = Tactic.prove sg [] [] (Logic.mk_equals (lhs, rhs)) |
|
176 (fn _ => rtac eq_reflection 1 THEN |
114 (fn _ => rtac eq_reflection 1 THEN |
177 resolve_tac eqI_rules 1 THEN |
115 resolve_tac eqI_rules 1 THEN |
178 simp_tac prepare_ss 1 THEN |
116 simp_tac cancel_ss 1) |
179 simp_tac sum_cancel_ss 1 THEN |
|
180 IF_UNSOLVED (simp_tac add_ac_ss 1)) |
|
181 in SOME thm end |
117 in SOME thm end |
182 handle Cancel => NONE; |
118 handle Cancel => NONE; |
183 |
119 |
184 val rel_conv = |
120 val rel_conv = |
185 Simplifier.simproc_i (Theory.deref thy_ref) "cancel_relations" |
121 Simplifier.simproc_i (Theory.deref thy_ref) "cancel_relations" |
186 (map Data.dest_eqI eqI_rules) rel_proc; |
122 (map Data.dest_eqI eqI_rules) rel_proc; |
187 |
123 |
188 end; |
124 end; |
189 |
|
190 |
|