author | skalberg |
Sun, 13 Feb 2005 17:15:14 +0100 | |
changeset 15531 | 08c8dad8e399 |
parent 15183 | 66da80cad4a2 |
child 15570 | 8d8c70b41bab |
permissions | -rw-r--r-- |
14756 | 1 |
(* Title: HOL/OrderedGroup.ML |
5589 | 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 |
||
13462 | 8 |
- Cancel complementary terms in sums |
5589 | 9 |
- Cancel like terms on opposite sides of relations |
14756 | 10 |
|
5589 | 11 |
*) |
12 |
||
14756 | 13 |
(* Modificaton in May 2004 by Steven Obua: polymorphic types work also now *) |
5589 | 14 |
|
15 |
signature ABEL_CANCEL = |
|
16 |
sig |
|
15104 | 17 |
val ss : simpset (*basic simpset of object-logic*) |
13462 | 18 |
val eq_reflection : thm (*object-equality to meta-equality*) |
5589 | 19 |
|
13462 | 20 |
val sg_ref : Sign.sg_ref (*signature of the theory of the group*) |
21 |
val T : typ (*the type of group elements*) |
|
5589 | 22 |
|
7586 | 23 |
val restrict_to_left : thm |
13462 | 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 |
|
5589 | 32 |
|
13462 | 33 |
val eq_diff_eq : thm |
34 |
val eqI_rules : thm list |
|
35 |
val dest_eqI : thm -> term |
|
5589 | 36 |
|
13462 | 37 |
val diff_def : thm |
38 |
val minus_add_distrib : thm |
|
39 |
val minus_minus : thm |
|
40 |
val minus_0 : thm |
|
5589 | 41 |
|
13462 | 42 |
val add_inverses : thm list |
43 |
val cancel_simps : thm list |
|
5589 | 44 |
end; |
45 |
||
46 |
||
47 |
functor Abel_Cancel (Data: ABEL_CANCEL) = |
|
48 |
struct |
|
49 |
||
5728
1d1175ef2d56
eliminated 'let ... in structure ...' to make SML/NJ 0.93 happy;
wenzelm
parents:
5610
diff
changeset
|
50 |
open Data; |
1d1175ef2d56
eliminated 'let ... in structure ...' to make SML/NJ 0.93 happy;
wenzelm
parents:
5610
diff
changeset
|
51 |
|
13462 | 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]; |
|
5589 | 55 |
|
14756 | 56 |
|
57 |
fun zero t = Const ("0", t); |
|
58 |
fun plus t = Const ("op +", [t,t] ---> t); |
|
59 |
fun minus t = Const ("uminus", t --> t); |
|
5589 | 60 |
|
61 |
(*Cancel corresponding terms on the two sides of the equation, NOT on |
|
62 |
the same side!*) |
|
13462 | 63 |
val cancel_ss = |
64 |
Data.ss addsimps [add_cancel_21, add_cancel_end, minus_minus] @ |
|
7586 | 65 |
(map (fn th => th RS restrict_to_left) Data.cancel_simps); |
5589 | 66 |
|
7586 | 67 |
val inverse_ss = Data.ss addsimps Data.add_inverses @ Data.cancel_simps; |
5589 | 68 |
|
14756 | 69 |
fun mk_sum ty [] = zero ty |
70 |
| mk_sum ty tms = foldr1 (fn (x,y) => (plus ty) $ x $ y) tms; |
|
5589 | 71 |
|
72 |
(*We map -t to t and (in other cases) t to -t. No need to check the type of |
|
73 |
uminus, since the simproc is only called on sums of type T.*) |
|
74 |
fun negate (Const("uminus",_) $ t) = t |
|
14756 | 75 |
| negate t = (minus (fastype_of t)) $ t; |
5589 | 76 |
|
77 |
(*Flatten a formula built from +, binary - and unary -. |
|
78 |
No need to check types PROVIDED they are checked upon entry!*) |
|
79 |
fun add_terms neg (Const ("op +", _) $ x $ y, ts) = |
|
13462 | 80 |
add_terms neg (x, add_terms neg (y, ts)) |
5589 | 81 |
| add_terms neg (Const ("op -", _) $ x $ y, ts) = |
13462 | 82 |
add_terms neg (x, add_terms (not neg) (y, ts)) |
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; |
|
5589 | 87 |
|
88 |
fun terms fml = add_terms false (fml, []); |
|
89 |
||
90 |
exception Cancel; |
|
91 |
||
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; |
|
98 |
||
99 |
(*Make a simproc to cancel complementary terms in sums. Examples: |
|
100 |
x-x = 0 x+(y-x) = y -x+(y+(x+z)) = y+z |
|
13462 | 101 |
It will unfold the definition of diff and associate to the right if |
5589 | 102 |
necessary. Rewriting is faster if the formula is already |
103 |
in that form. |
|
104 |
*) |
|
105 |
||
106 |
fun sum_proc sg _ lhs = |
|
13462 | 107 |
let val _ = if !trace then tracing ("cancel_sums: LHS = " ^ |
108 |
string_of_cterm (cterm_of sg lhs)) |
|
109 |
else () |
|
5589 | 110 |
val (head::tail) = terms lhs |
111 |
val head' = negate head |
|
14756 | 112 |
val rhs = mk_sum (fastype_of head) (cancelled (head',tail)) |
5589 | 113 |
and chead' = Thm.cterm_of sg head' |
13462 | 114 |
val _ = if !trace then |
115 |
tracing ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs)) |
|
116 |
else () |
|
13480
bb72bd43c6c3
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
wenzelm
parents:
13462
diff
changeset
|
117 |
val thm = Tactic.prove sg [] [] (Logic.mk_equals (lhs, rhs)) |
bb72bd43c6c3
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
wenzelm
parents:
13462
diff
changeset
|
118 |
(fn _ => rtac eq_reflection 1 THEN |
bb72bd43c6c3
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
wenzelm
parents:
13462
diff
changeset
|
119 |
simp_tac prepare_ss 1 THEN |
bb72bd43c6c3
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
wenzelm
parents:
13462
diff
changeset
|
120 |
IF_UNSOLVED (simp_tac cancel_ss 1) THEN |
bb72bd43c6c3
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
wenzelm
parents:
13462
diff
changeset
|
121 |
IF_UNSOLVED (simp_tac inverse_ss 1)) |
15531 | 122 |
in SOME thm end |
123 |
handle Cancel => NONE; |
|
5589 | 124 |
|
125 |
||
13462 | 126 |
val sum_conv = |
5589 | 127 |
Simplifier.mk_simproc "cancel_sums" |
15027 | 128 |
(map (Thm.cterm_fun Logic.varify o Thm.read_cterm (Sign.deref sg_ref)) |
13462 | 129 |
[("x + y", Data.T), ("x - y", Data.T)]) (* FIXME depends on concrete syntax !???!!??! *) |
5589 | 130 |
sum_proc; |
131 |
||
132 |
||
133 |
(*A simproc to cancel like terms on the opposite sides of relations: |
|
134 |
(x + y - z < -z + x) = (y < 0) |
|
135 |
Works for (=) and (<=) as well as (<), if the necessary rules are supplied. |
|
136 |
Reduces the problem to subtraction and calls the previous simproc. |
|
137 |
*) |
|
138 |
||
139 |
(*Cancel the FIRST occurrence of a term. If it's repeated, then repeated |
|
140 |
calls to the simproc will be needed.*) |
|
141 |
fun cancel1 ([], u) = raise Match (*impossible: it's a common term*) |
|
142 |
| cancel1 (t::ts, u) = if t aconv u then ts |
|
13462 | 143 |
else t :: cancel1 (ts,u); |
5589 | 144 |
|
145 |
||
146 |
val sum_cancel_ss = Data.ss addsimprocs [sum_conv] |
|
13462 | 147 |
addsimps [add_0, add_0_right]; |
5589 | 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)) = |
|
13462 | 152 |
let val _ = if !trace then tracing ("cancel_relations: LHS = " ^ |
153 |
string_of_cterm (cterm_of sg lhs)) |
|
154 |
else () |
|
5589 | 155 |
val ltms = terms lt |
156 |
and rtms = terms rt |
|
14756 | 157 |
val ty = fastype_of lt |
5589 | 158 |
val common = (*inter_term miscounts repetitions, so squash them*) |
13462 | 159 |
gen_distinct (op aconv) (inter_term (ltms, rtms)) |
5589 | 160 |
val _ = if null common then raise Cancel (*nothing to do*) |
13462 | 161 |
else () |
5589 | 162 |
|
14756 | 163 |
fun cancelled tms = mk_sum ty (foldl cancel1 (tms, common)) |
5589 | 164 |
|
165 |
val lt' = cancelled ltms |
|
166 |
and rt' = cancelled rtms |
|
167 |
||
168 |
val rhs = rel$lt'$rt' |
|
15183 | 169 |
val _ = if lhs aconv rhs then raise Cancel (*nothing to do*) |
170 |
else () |
|
13462 | 171 |
val _ = if !trace then |
172 |
tracing ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs)) |
|
173 |
else () |
|
5589 | 174 |
|
13480
bb72bd43c6c3
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
wenzelm
parents:
13462
diff
changeset
|
175 |
val thm = Tactic.prove sg [] [] (Logic.mk_equals (lhs, rhs)) |
bb72bd43c6c3
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
wenzelm
parents:
13462
diff
changeset
|
176 |
(fn _ => rtac eq_reflection 1 THEN |
bb72bd43c6c3
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
wenzelm
parents:
13462
diff
changeset
|
177 |
resolve_tac eqI_rules 1 THEN |
bb72bd43c6c3
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
wenzelm
parents:
13462
diff
changeset
|
178 |
simp_tac prepare_ss 1 THEN |
bb72bd43c6c3
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
wenzelm
parents:
13462
diff
changeset
|
179 |
simp_tac sum_cancel_ss 1 THEN |
bb72bd43c6c3
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
wenzelm
parents:
13462
diff
changeset
|
180 |
IF_UNSOLVED (simp_tac add_ac_ss 1)) |
15531 | 181 |
in SOME thm end |
182 |
handle Cancel => NONE; |
|
5589 | 183 |
|
13462 | 184 |
val rel_conv = |
185 |
Simplifier.simproc_i (Sign.deref sg_ref) "cancel_relations" |
|
186 |
(map Data.dest_eqI eqI_rules) rel_proc; |
|
5589 | 187 |
|
188 |
end; |
|
14756 | 189 |
|
190 |