|
1 (* Title: HOL/Tools/group_cancel.ML |
|
2 Author: Brian Huffman, TU Munich |
|
3 |
|
4 Simplification procedures for abelian groups: |
|
5 - Cancel complementary terms in sums. |
|
6 - Cancel like terms on opposite sides of relations. |
|
7 *) |
|
8 |
|
9 signature GROUP_CANCEL = |
|
10 sig |
|
11 val cancel_diff_conv: conv |
|
12 val cancel_eq_conv: conv |
|
13 val cancel_le_conv: conv |
|
14 val cancel_less_conv: conv |
|
15 val cancel_add_conv: conv |
|
16 end |
|
17 |
|
18 structure Group_Cancel: GROUP_CANCEL = |
|
19 struct |
|
20 |
|
21 val add1 = @{lemma "(A::'a::comm_monoid_add) == k + a ==> A + b == k + (a + b)" |
|
22 by (simp only: add_ac)} |
|
23 val add2 = @{lemma "(B::'a::comm_monoid_add) == k + b ==> a + B == k + (a + b)" |
|
24 by (simp only: add_ac)} |
|
25 val sub1 = @{lemma "(A::'a::ab_group_add) == k + a ==> A - b == k + (a - b)" |
|
26 by (simp only: add_diff_eq)} |
|
27 val sub2 = @{lemma "(B::'a::ab_group_add) == k + b ==> a - B == - k + (a - b)" |
|
28 by (simp only: diff_minus minus_add add_ac)} |
|
29 val neg1 = @{lemma "(A::'a::ab_group_add) == k + a ==> - A == - k + - a" |
|
30 by (simp only: minus_add_distrib)} |
|
31 val rule0 = @{lemma "(a::'a::comm_monoid_add) == a + 0" |
|
32 by (simp only: add_0_right)} |
|
33 val minus_minus = mk_meta_eq @{thm minus_minus} |
|
34 |
|
35 fun move_to_front path = Conv.every_conv |
|
36 [Conv.rewr_conv (Library.foldl (op RS) (rule0, path)), |
|
37 Conv.arg1_conv (Conv.repeat_conv (Conv.rewr_conv minus_minus))] |
|
38 |
|
39 fun add_atoms pos path (Const (@{const_name Groups.plus}, _) $ x $ y) = |
|
40 add_atoms pos (add1::path) x #> add_atoms pos (add2::path) y |
|
41 | add_atoms pos path (Const (@{const_name Groups.minus}, _) $ x $ y) = |
|
42 add_atoms pos (sub1::path) x #> add_atoms (not pos) (sub2::path) y |
|
43 | add_atoms pos path (Const (@{const_name Groups.uminus}, _) $ x) = |
|
44 add_atoms (not pos) (neg1::path) x |
|
45 | add_atoms _ _ (Const (@{const_name Groups.zero}, _)) = I |
|
46 | add_atoms pos path x = cons ((pos, x), path) |
|
47 |
|
48 fun atoms t = add_atoms true [] t [] |
|
49 |
|
50 val coeff_ord = prod_ord bool_ord Term_Ord.term_ord |
|
51 |
|
52 exception Cancel |
|
53 |
|
54 fun find_common ord xs ys = |
|
55 let |
|
56 fun find (xs as (x, px)::xs') (ys as (y, py)::ys') = |
|
57 (case ord (x, y) of |
|
58 EQUAL => (px, py) |
|
59 | LESS => find xs' ys |
|
60 | GREATER => find xs ys') |
|
61 | find _ _ = raise Cancel |
|
62 fun ord' ((x, _), (y, _)) = ord (x, y) |
|
63 in |
|
64 find (sort ord' xs) (sort ord' ys) |
|
65 end |
|
66 |
|
67 fun cancel_conv rule ct = |
|
68 let |
|
69 val ((_, lhs), rhs) = (apfst dest_comb o dest_comb) (Thm.term_of ct) |
|
70 val (lpath, rpath) = find_common coeff_ord (atoms lhs) (atoms rhs) |
|
71 val lconv = move_to_front lpath |
|
72 val rconv = move_to_front rpath |
|
73 val conv1 = Conv.combination_conv (Conv.arg_conv lconv) rconv |
|
74 val conv = conv1 then_conv Conv.rewr_conv rule |
|
75 in conv ct handle Cancel => raise CTERM ("no_conversion", []) end |
|
76 |
|
77 val cancel_diff_conv = cancel_conv (mk_meta_eq @{thm add_diff_cancel_left}) |
|
78 val cancel_eq_conv = cancel_conv (mk_meta_eq @{thm add_left_cancel}) |
|
79 val cancel_le_conv = cancel_conv (mk_meta_eq @{thm add_le_cancel_left}) |
|
80 val cancel_less_conv = cancel_conv (mk_meta_eq @{thm add_less_cancel_left}) |
|
81 |
|
82 val diff_minus_eq_add = mk_meta_eq @{thm diff_minus_eq_add} |
|
83 val add_eq_diff_minus = Thm.symmetric diff_minus_eq_add |
|
84 val cancel_add_conv = Conv.every_conv |
|
85 [Conv.rewr_conv add_eq_diff_minus, |
|
86 cancel_diff_conv, |
|
87 Conv.rewr_conv diff_minus_eq_add] |
|
88 |
|
89 end |