1 (* Title: HOL/Tools/abel_cancel.ML |
|
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 Copyright 1998 University of Cambridge |
|
4 |
|
5 Simplification procedures for abelian groups: |
|
6 - Cancel complementary terms in sums. |
|
7 - Cancel like terms on opposite sides of relations. |
|
8 *) |
|
9 |
|
10 signature ABEL_CANCEL = |
|
11 sig |
|
12 val sum_proc: simpset -> cterm -> thm option |
|
13 val rel_proc: simpset -> cterm -> thm option |
|
14 end; |
|
15 |
|
16 structure Abel_Cancel: ABEL_CANCEL = |
|
17 struct |
|
18 |
|
19 (** compute cancellation **) |
|
20 |
|
21 fun add_atoms pos (Const (@{const_name Groups.plus}, _) $ x $ y) = |
|
22 add_atoms pos x #> add_atoms pos y |
|
23 | add_atoms pos (Const (@{const_name Groups.minus}, _) $ x $ y) = |
|
24 add_atoms pos x #> add_atoms (not pos) y |
|
25 | add_atoms pos (Const (@{const_name Groups.uminus}, _) $ x) = |
|
26 add_atoms (not pos) x |
|
27 | add_atoms pos (Const (@{const_name Groups.zero}, _)) = I |
|
28 | add_atoms pos x = cons (pos, x); |
|
29 |
|
30 fun atoms t = add_atoms true t []; |
|
31 |
|
32 fun zerofy pt ((c as Const (@{const_name Groups.plus}, _)) $ x $ y) = |
|
33 (case zerofy pt x of NONE => |
|
34 (case zerofy pt y of NONE => NONE |
|
35 | SOME z => SOME (c $ x $ z)) |
|
36 | SOME z => SOME (c $ z $ y)) |
|
37 | zerofy pt ((c as Const (@{const_name Groups.minus}, _)) $ x $ y) = |
|
38 (case zerofy pt x of NONE => |
|
39 (case zerofy (apfst not pt) y of NONE => NONE |
|
40 | SOME z => SOME (c $ x $ z)) |
|
41 | SOME z => SOME (c $ z $ y)) |
|
42 | zerofy pt ((c as Const (@{const_name Groups.uminus}, _)) $ x) = |
|
43 (case zerofy (apfst not pt) x of NONE => NONE |
|
44 | SOME z => SOME (c $ z)) |
|
45 | zerofy (pos, t) u = |
|
46 if pos andalso (t aconv u) |
|
47 then SOME (Const (@{const_name Groups.zero}, fastype_of t)) |
|
48 else NONE |
|
49 |
|
50 exception Cancel; |
|
51 |
|
52 fun find_common _ [] _ = raise Cancel |
|
53 | find_common opp ((p, l) :: ls) rs = |
|
54 let val pr = if opp then not p else p |
|
55 in if exists (fn (q, r) => pr = q andalso l aconv r) rs then (p, l) |
|
56 else find_common opp ls rs |
|
57 end |
|
58 |
|
59 (* turns t1(t) OP t2(t) into t1(0) OP t2(0) where OP can be +, -, =, etc. |
|
60 If OP = +, it must be t2(-t) rather than t2(t) |
|
61 *) |
|
62 fun cancel (c $ lhs $ rhs) = |
|
63 let |
|
64 val opp = case c of Const(@{const_name Groups.plus}, _) => true | _ => false; |
|
65 val (pos, l) = find_common opp (atoms lhs) (atoms rhs); |
|
66 val posr = if opp then not pos else pos; |
|
67 in c $ the (zerofy (pos, l) lhs) $ the (zerofy (posr, l) rhs) end; |
|
68 |
|
69 |
|
70 (** prove cancellation **) |
|
71 |
|
72 fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a') |
|
73 [@{const_name Groups.zero}, @{const_name Groups.plus}, |
|
74 @{const_name Groups.uminus}, @{const_name Groups.minus}] |
|
75 | agrp_ord _ = ~1; |
|
76 |
|
77 fun less_agrp (a, b) = (Term_Ord.term_lpo agrp_ord (a, b) = LESS); |
|
78 |
|
79 fun solve (_ $ (Const (@{const_name Groups.plus}, _) $ _ $ _) $ _) = |
|
80 SOME @{thm add_assoc [THEN eq_reflection]} |
|
81 | solve (_ $ x $ (Const (@{const_name Groups.plus}, _) $ y $ _)) = |
|
82 if less_agrp (y, x) then |
|
83 SOME @{thm add_left_commute [THEN eq_reflection]} |
|
84 else NONE |
|
85 | solve (_ $ x $ y) = |
|
86 if less_agrp (y, x) then |
|
87 SOME @{thm add_commute [THEN eq_reflection]} else |
|
88 NONE |
|
89 | solve _ = NONE; |
|
90 |
|
91 val simproc = Simplifier.simproc_global @{theory} |
|
92 "add_ac_proc" ["x + y::'a::ab_semigroup_add"] ((K o K) solve); |
|
93 |
|
94 val cancel_ss = (HOL_basic_ss |> Simplifier.set_termless less_agrp) |
|
95 addsimprocs [simproc] addsimps |
|
96 [@{thm add_0_left}, @{thm add_0_right}, @{thm diff_minus}, |
|
97 @{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero}, |
|
98 @{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel}, |
|
99 @{thm minus_add_cancel}]; |
|
100 |
|
101 fun cancel_simp_tac ss = simp_tac (Simplifier.inherit_context ss cancel_ss); |
|
102 |
|
103 |
|
104 (** simprocs **) |
|
105 |
|
106 (* cancel complementary terms in arbitrary sums *) |
|
107 |
|
108 fun sum_proc ss ct = |
|
109 let |
|
110 val t = Thm.term_of ct; |
|
111 val prop = Logic.mk_equals (t, cancel t); |
|
112 val thm = Goal.prove (Simplifier.the_context ss) [] [] prop |
|
113 (fn _ => cancel_simp_tac ss 1) |
|
114 in SOME thm end handle Cancel => NONE; |
|
115 |
|
116 |
|
117 (* cancel like terms on the opposite sides of relations: |
|
118 (x + y - z < -z + x) = (y < 0) |
|
119 Works for (=) and (<=) as well as (<), if the necessary rules are supplied. |
|
120 Reduces the problem to subtraction. *) |
|
121 |
|
122 fun rel_proc ss ct = |
|
123 let |
|
124 val t = Thm.term_of ct; |
|
125 val prop = Logic.mk_equals (t, cancel t); |
|
126 val thm = Goal.prove (Simplifier.the_context ss) [] [] prop |
|
127 (fn _ => rtac @{thm eq_reflection} 1 THEN |
|
128 resolve_tac [@{thm diff_eq_diff_less}, @{thm diff_eq_diff_less_eq}, @{thm diff_eq_diff_eq}] 1 THEN |
|
129 cancel_simp_tac ss 1) |
|
130 in SOME thm end handle Cancel => NONE; |
|
131 |
|
132 end; |
|