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