|
1 (* Title: boolean_algebra_cancel.ML |
|
2 Author: Andreas Lochbihler, ETH Zurich |
|
3 |
|
4 Simplification procedures for boolean algebras: |
|
5 - Cancel complementary terms sup and inf. |
|
6 *) |
|
7 |
|
8 signature BOOLEAN_ALGEBRA_CANCEL = |
|
9 sig |
|
10 val cancel_sup_conv: conv |
|
11 val cancel_inf_conv: conv |
|
12 end |
|
13 |
|
14 structure Boolean_Algebra_Cancel: BOOLEAN_ALGEBRA_CANCEL = |
|
15 struct |
|
16 val sup1 = @{lemma "(A::'a::semilattice_sup) == sup k a ==> sup A b == sup k (sup a b)" |
|
17 by (simp only: ac_simps)} |
|
18 val sup2 = @{lemma "(B::'a::semilattice_sup) == sup k b ==> sup a B == sup k (sup a b)" |
|
19 by (simp only: ac_simps)} |
|
20 val sup0 = @{lemma "(a::'a::bounded_semilattice_sup_bot) == sup a bot" by (simp)} |
|
21 |
|
22 val inf1 = @{lemma "(A::'a::semilattice_inf) == inf k a ==> inf A b == inf k (inf a b)" |
|
23 by (simp only: ac_simps)} |
|
24 val inf2 = @{lemma "(B::'a::semilattice_inf) == inf k b ==> inf a B == inf k (inf a b)" |
|
25 by (simp only: ac_simps)} |
|
26 val inf0 = @{lemma "(a::'a::bounded_semilattice_inf_top) == inf a top" by (simp)} |
|
27 |
|
28 fun move_to_front rule path = Conv.rewr_conv (Library.foldl (op RS) (rule, path)) |
|
29 |
|
30 fun add_atoms sup pos path (t as Const (@{const_name Lattices.sup}, _) $ x $ y) = |
|
31 if sup then |
|
32 add_atoms sup pos (sup1::path) x #> add_atoms sup pos (sup2::path) y |
|
33 else cons ((pos, t), path) |
|
34 | add_atoms sup pos path (t as Const (@{const_name Lattices.inf}, _) $ x $ y) = |
|
35 if not sup then |
|
36 add_atoms sup pos (inf1::path) x #> add_atoms sup pos (inf2::path) y |
|
37 else cons ((pos, t), path) |
|
38 | add_atoms _ _ _ (Const (@{const_name Orderings.bot}, _)) = I |
|
39 | add_atoms _ _ _ (Const (@{const_name Orderings.top}, _)) = I |
|
40 | add_atoms _ pos path (Const (@{const_name Groups.uminus}, _) $ x) = cons ((not pos, x), path) |
|
41 | add_atoms _ pos path x = cons ((pos, x), path); |
|
42 |
|
43 fun atoms sup pos t = add_atoms sup pos [] t [] |
|
44 |
|
45 val coeff_ord = prod_ord bool_ord Term_Ord.term_ord |
|
46 |
|
47 fun find_common ord xs ys = |
|
48 let |
|
49 fun find (xs as (x, px)::xs') (ys as (y, py)::ys') = |
|
50 (case ord (x, y) of |
|
51 EQUAL => SOME (fst x, px, py) |
|
52 | LESS => find xs' ys |
|
53 | GREATER => find xs ys') |
|
54 | find _ _ = NONE |
|
55 fun ord' ((x, _), (y, _)) = ord (x, y) |
|
56 in |
|
57 find (sort ord' xs) (sort ord' ys) |
|
58 end |
|
59 |
|
60 fun cancel_conv sup rule ct = |
|
61 let |
|
62 val rule0 = if sup then sup0 else inf0 |
|
63 fun cancel1_conv (pos, lpath, rpath) = |
|
64 let |
|
65 val lconv = move_to_front rule0 lpath |
|
66 val rconv = move_to_front rule0 rpath |
|
67 val conv1 = Conv.combination_conv (Conv.arg_conv lconv) rconv |
|
68 in |
|
69 conv1 then_conv Conv.rewr_conv (rule pos) |
|
70 end |
|
71 val ((_, lhs), rhs) = (apfst dest_comb o dest_comb) (Thm.term_of ct) |
|
72 val common = find_common coeff_ord (atoms sup true lhs) (atoms sup false rhs) |
|
73 val conv = |
|
74 case common of NONE => Conv.no_conv |
|
75 | SOME x => cancel1_conv x |
|
76 in conv ct end |
|
77 |
|
78 val cancel_sup_conv = cancel_conv true (fn pos => if pos then mk_meta_eq @{thm sup_cancel_left1} else mk_meta_eq @{thm sup_cancel_left2}) |
|
79 val cancel_inf_conv = cancel_conv false (fn pos => if pos then mk_meta_eq @{thm inf_cancel_left1} else mk_meta_eq @{thm inf_cancel_left2}) |
|
80 |
|
81 end |