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