cancel complementary terms as arguments to sup/inf in boolean algebras
authorAndreas Lochbihler
Wed Nov 11 09:21:56 2015 +0100 (2015-11-11)
changeset 6162990f54d9e63f2
parent 61628 8dd2bd4fe30b
child 61630 608520e0e8e2
cancel complementary terms as arguments to sup/inf in boolean algebras
NEWS
src/HOL/Lattices.thy
src/HOL/Tools/boolean_algebra_cancel.ML
     1.1 --- a/NEWS	Wed Nov 11 09:06:30 2015 +0100
     1.2 +++ b/NEWS	Wed Nov 11 09:21:56 2015 +0100
     1.3 @@ -462,6 +462,10 @@
     1.4  than the former separate constants, hence infix syntax (_ / _) is usually
     1.5  not available during instantiation.
     1.6  
     1.7 +* New cancellation simprocs for boolean algebras to cancel
     1.8 +complementary terms for sup and inf. For example, "sup x (sup y (- x))"
     1.9 +simplifies to "top". INCOMPATIBILITY.
    1.10 +
    1.11  * Library/Multiset:
    1.12    - Renamed multiset inclusion operators:
    1.13        < ~> <#
     2.1 --- a/src/HOL/Lattices.thy	Wed Nov 11 09:06:30 2015 +0100
     2.2 +++ b/src/HOL/Lattices.thy	Wed Nov 11 09:21:56 2015 +0100
     2.3 @@ -707,8 +707,44 @@
     2.4    then show ?thesis by simp
     2.5  qed
     2.6  
     2.7 +lemma sup_cancel_left1: "sup (sup x a) (sup (- x) b) = top"
     2.8 +by(simp add: inf_sup_aci sup_compl_top)
     2.9 +
    2.10 +lemma sup_cancel_left2: "sup (sup (- x) a) (sup x b) = top"
    2.11 +by(simp add: inf_sup_aci sup_compl_top)
    2.12 +
    2.13 +lemma inf_cancel_left1: "inf (inf x a) (inf (- x) b) = bot"
    2.14 +by(simp add: inf_sup_aci inf_compl_bot)
    2.15 +
    2.16 +lemma inf_cancel_left2: "inf (inf (- x) a) (inf x b) = bot"
    2.17 +by(simp add: inf_sup_aci inf_compl_bot)
    2.18 +
    2.19 +declare inf_compl_bot [simp] sup_compl_top [simp]
    2.20 +
    2.21 +lemma sup_compl_top_left1 [simp]: "sup (- x) (sup x y) = top"
    2.22 +by(simp add: sup_assoc[symmetric])
    2.23 +
    2.24 +lemma sup_compl_top_left2 [simp]: "sup x (sup (- x) y) = top"
    2.25 +using sup_compl_top_left1[of "- x" y] by simp
    2.26 +
    2.27 +lemma inf_compl_bot_left1 [simp]: "inf (- x) (inf x y) = bot"
    2.28 +by(simp add: inf_assoc[symmetric])
    2.29 +
    2.30 +lemma inf_compl_bot_left2 [simp]: "inf x (inf (- x) y) = bot"
    2.31 +using inf_compl_bot_left1[of "- x" y] by simp
    2.32 +
    2.33 +lemma inf_compl_bot_right [simp]: "inf x (inf y (- x)) = bot"
    2.34 +by(subst inf_left_commute) simp
    2.35 +
    2.36  end
    2.37  
    2.38 +ML_file "Tools/boolean_algebra_cancel.ML"
    2.39 +
    2.40 +simproc_setup boolean_algebra_cancel_sup ("sup a b::'a::boolean_algebra") =
    2.41 +  {* fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_sup_conv *}
    2.42 +
    2.43 +simproc_setup boolean_algebra_cancel_inf ("inf a b::'a::boolean_algebra") =
    2.44 +  {* fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_inf_conv *}
    2.45  
    2.46  subsection \<open>@{text "min/max"} as special case of lattice\<close>
    2.47  
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/boolean_algebra_cancel.ML	Wed Nov 11 09:21:56 2015 +0100
     3.3 @@ -0,0 +1,81 @@
     3.4 +(*  Title:      boolean_algebra_cancel.ML
     3.5 +    Author:     Andreas Lochbihler, ETH Zurich
     3.6 +
     3.7 +Simplification procedures for boolean algebras:
     3.8 +- Cancel complementary terms sup and inf.
     3.9 +*)
    3.10 +
    3.11 +signature BOOLEAN_ALGEBRA_CANCEL =
    3.12 +sig
    3.13 +  val cancel_sup_conv: conv
    3.14 +  val cancel_inf_conv: conv
    3.15 +end
    3.16 +
    3.17 +structure Boolean_Algebra_Cancel: BOOLEAN_ALGEBRA_CANCEL =
    3.18 +struct
    3.19 +val sup1 = @{lemma "(A::'a::semilattice_sup) == sup k a ==> sup A b == sup k (sup a b)"
    3.20 +      by (simp only: ac_simps)}
    3.21 +val sup2 = @{lemma "(B::'a::semilattice_sup) == sup k b ==> sup a B == sup k (sup a b)"
    3.22 +      by (simp only: ac_simps)}
    3.23 +val sup0 = @{lemma "(a::'a::bounded_semilattice_sup_bot) == sup a bot" by (simp)}
    3.24 +
    3.25 +val inf1 = @{lemma "(A::'a::semilattice_inf) == inf k a ==> inf A b == inf k (inf a b)"
    3.26 +      by (simp only: ac_simps)}
    3.27 +val inf2 = @{lemma "(B::'a::semilattice_inf) == inf k b ==> inf a B == inf k (inf a b)"
    3.28 +      by (simp only: ac_simps)}
    3.29 +val inf0 = @{lemma "(a::'a::bounded_semilattice_inf_top) == inf a top" by (simp)}
    3.30 +
    3.31 +fun move_to_front rule path = Conv.rewr_conv (Library.foldl (op RS) (rule, path))
    3.32 +
    3.33 +fun add_atoms sup pos path (t as Const (@{const_name Lattices.sup}, _) $ x $ y) =
    3.34 +    if sup then
    3.35 +      add_atoms sup pos (sup1::path) x #> add_atoms sup pos (sup2::path) y
    3.36 +    else cons ((pos, t), path)
    3.37 +  | add_atoms sup pos path (t as Const (@{const_name Lattices.inf}, _) $ x $ y) =
    3.38 +    if not sup then
    3.39 +      add_atoms sup pos (inf1::path) x #> add_atoms sup pos (inf2::path) y
    3.40 +    else cons ((pos, t), path)
    3.41 +  | add_atoms _ _ _ (Const (@{const_name Orderings.bot}, _)) = I
    3.42 +  | add_atoms _ _ _ (Const (@{const_name Orderings.top}, _)) = I
    3.43 +  | add_atoms _ pos path (Const (@{const_name Groups.uminus}, _) $ x) = cons ((not pos, x), path)
    3.44 +  | add_atoms _ pos path x = cons ((pos, x), path);
    3.45 +
    3.46 +fun atoms sup pos t = add_atoms sup pos [] t []
    3.47 +
    3.48 +val coeff_ord = prod_ord bool_ord Term_Ord.term_ord
    3.49 +
    3.50 +fun find_common ord xs ys =
    3.51 +  let
    3.52 +    fun find (xs as (x, px)::xs') (ys as (y, py)::ys') =
    3.53 +        (case ord (x, y) of
    3.54 +          EQUAL => SOME (fst x, px, py)
    3.55 +        | LESS => find xs' ys
    3.56 +        | GREATER => find xs ys')
    3.57 +      | find _ _ = NONE
    3.58 +    fun ord' ((x, _), (y, _)) = ord (x, y)
    3.59 +  in
    3.60 +    find (sort ord' xs) (sort ord' ys)
    3.61 +  end
    3.62 +
    3.63 +fun cancel_conv sup rule ct =
    3.64 +  let
    3.65 +    val rule0 = if sup then sup0 else inf0
    3.66 +    fun cancel1_conv (pos, lpath, rpath) =
    3.67 +      let
    3.68 +        val lconv = move_to_front rule0 lpath
    3.69 +        val rconv = move_to_front rule0 rpath
    3.70 +        val conv1 = Conv.combination_conv (Conv.arg_conv lconv) rconv
    3.71 +      in
    3.72 +        conv1 then_conv Conv.rewr_conv (rule pos)
    3.73 +      end
    3.74 +    val ((_, lhs), rhs) = (apfst dest_comb o dest_comb) (Thm.term_of ct)
    3.75 +    val common = find_common coeff_ord (atoms sup true lhs) (atoms sup false rhs)
    3.76 +    val conv =
    3.77 +      case common of NONE => Conv.no_conv
    3.78 +      | SOME x => cancel1_conv x
    3.79 +  in conv ct end
    3.80 +
    3.81 +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})
    3.82 +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})
    3.83 +
    3.84 +end
    3.85 \ No newline at end of file