src/HOL/Tools/abel_cancel.ML
author haftmann
Wed Dec 08 13:34:50 2010 +0100 (2010-12-08)
changeset 41075 4bed56dc95fb
parent 38715 6513ea67d95d
child 45464 5a5a6e6c6789
permissions -rw-r--r--
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann@37884
     1
(*  Title:      HOL/Tools/abel_cancel.ML
paulson@5589
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@5589
     3
    Copyright   1998  University of Cambridge
paulson@5589
     4
haftmann@37884
     5
Simplification procedures for abelian groups:
haftmann@37884
     6
- Cancel complementary terms in sums.
haftmann@37884
     7
- Cancel like terms on opposite sides of relations.
paulson@5589
     8
*)
paulson@5589
     9
paulson@5589
    10
signature ABEL_CANCEL =
paulson@5589
    11
sig
haftmann@37890
    12
  val sum_proc: simpset -> cterm -> thm option
haftmann@37890
    13
  val rel_proc: simpset -> cterm -> thm option
paulson@5589
    14
end;
paulson@5589
    15
haftmann@37884
    16
structure Abel_Cancel: ABEL_CANCEL =
paulson@5589
    17
struct
paulson@5589
    18
haftmann@37894
    19
(** compute cancellation **)
wenzelm@5728
    20
haftmann@37894
    21
fun add_atoms pos (Const (@{const_name Groups.plus}, _) $ x $ y) =
haftmann@37894
    22
      add_atoms pos x #> add_atoms pos y
haftmann@37894
    23
  | add_atoms pos (Const (@{const_name Groups.minus}, _) $ x $ y) =
haftmann@37894
    24
      add_atoms pos x #> add_atoms (not pos) y
haftmann@37894
    25
  | add_atoms pos (Const (@{const_name Groups.uminus}, _) $ x) =
haftmann@37894
    26
      add_atoms (not pos) x
haftmann@37894
    27
  | add_atoms pos x = cons (pos, x);
haftmann@37884
    28
haftmann@37896
    29
fun atoms t = add_atoms true t [];
paulson@5589
    30
haftmann@37896
    31
fun zerofy pt ((c as Const (@{const_name Groups.plus}, _)) $ x $ y) =
haftmann@37896
    32
      (case zerofy pt x of NONE =>
haftmann@37896
    33
        (case zerofy pt y of NONE => NONE
haftmann@37896
    34
         | SOME z => SOME (c $ x $ z))
haftmann@37894
    35
       | SOME z => SOME (c $ z $ y))
haftmann@37896
    36
  | zerofy pt ((c as Const (@{const_name Groups.minus}, _)) $ x $ y) =
haftmann@37896
    37
      (case zerofy pt x of NONE =>
haftmann@37896
    38
        (case zerofy (apfst not pt) y of NONE => NONE
haftmann@37896
    39
         | SOME z => SOME (c $ x $ z))
haftmann@37894
    40
       | SOME z => SOME (c $ z $ y))
haftmann@37896
    41
  | zerofy pt ((c as Const (@{const_name Groups.uminus}, _)) $ x) =
haftmann@37896
    42
      (case zerofy (apfst not pt) x of NONE => NONE
haftmann@37894
    43
       | SOME z => SOME (c $ z))
haftmann@37896
    44
  | zerofy (pos, t) u =
haftmann@37894
    45
      if pos andalso (t aconv u)
haftmann@37894
    46
        then SOME (Const (@{const_name Groups.zero}, fastype_of t))
haftmann@37894
    47
        else NONE
paulson@5589
    48
wenzelm@20055
    49
exception Cancel;
paulson@5589
    50
nipkow@16569
    51
fun find_common _ [] _ = raise Cancel
haftmann@37894
    52
  | find_common opp ((p, l) :: ls) rs =
nipkow@16569
    53
      let val pr = if opp then not p else p
haftmann@37894
    54
      in if exists (fn (q, r) => pr = q andalso l aconv r) rs then (p, l)
nipkow@16569
    55
         else find_common opp ls rs
nipkow@16569
    56
      end
paulson@5589
    57
nipkow@16569
    58
(* turns t1(t) OP t2(t) into t1(0) OP t2(0) where OP can be +, -, =, etc.
nipkow@16569
    59
   If OP = +, it must be t2(-t) rather than t2(t)
nipkow@16569
    60
*)
haftmann@37896
    61
fun cancel (c $ lhs $ rhs) =
wenzelm@20055
    62
  let
haftmann@37894
    63
    val opp = case c of Const(@{const_name Groups.plus}, _) => true | _ => false;
haftmann@37894
    64
    val (pos, l) = find_common opp (atoms lhs) (atoms rhs);
haftmann@37894
    65
    val posr = if opp then not pos else pos;
haftmann@37896
    66
  in c $ the (zerofy (pos, l) lhs) $ the (zerofy (posr, l) rhs) end;
nipkow@16569
    67
nipkow@16569
    68
haftmann@37894
    69
(** prove cancellation **)
haftmann@37894
    70
haftmann@37894
    71
fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a')
haftmann@37894
    72
      [@{const_name Groups.zero}, @{const_name Groups.plus},
haftmann@37894
    73
        @{const_name Groups.uminus}, @{const_name Groups.minus}]
haftmann@37894
    74
  | agrp_ord _ = ~1;
haftmann@37894
    75
haftmann@37894
    76
fun less_agrp (a, b) = (Term_Ord.term_lpo agrp_ord (a, b) = LESS);
haftmann@37894
    77
haftmann@37894
    78
fun solve (_ $ (Const (@{const_name Groups.plus}, _) $ _ $ _) $ _) =
haftmann@37894
    79
      SOME @{thm add_assoc [THEN eq_reflection]}
haftmann@37894
    80
  | solve (_ $ x $ (Const (@{const_name Groups.plus}, _) $ y $ _)) =
haftmann@37894
    81
      if less_agrp (y, x) then
haftmann@37894
    82
        SOME @{thm add_left_commute [THEN eq_reflection]}
haftmann@37894
    83
        else NONE
haftmann@37894
    84
  | solve (_ $ x $ y) =
haftmann@37894
    85
      if less_agrp (y, x) then
haftmann@37894
    86
        SOME @{thm add_commute [THEN eq_reflection]} else
haftmann@37894
    87
        NONE
haftmann@37894
    88
  | solve _ = NONE;
haftmann@37894
    89
  
wenzelm@38715
    90
val simproc = Simplifier.simproc_global @{theory}
haftmann@37894
    91
  "add_ac_proc" ["x + y::'a::ab_semigroup_add"] ((K o K) solve);
haftmann@37894
    92
haftmann@37894
    93
val cancel_ss = HOL_basic_ss settermless less_agrp
haftmann@37894
    94
  addsimprocs [simproc] addsimps
haftmann@37894
    95
  [@{thm add_0_left}, @{thm add_0_right}, @{thm diff_minus},
haftmann@37894
    96
   @{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero},
haftmann@37894
    97
   @{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel},
haftmann@37894
    98
   @{thm minus_add_cancel}];
haftmann@37894
    99
haftmann@37894
   100
fun cancel_simp_tac ss = simp_tac (Simplifier.inherit_context ss cancel_ss);
haftmann@37894
   101
haftmann@37894
   102
haftmann@37894
   103
(** simprocs **)
haftmann@37894
   104
haftmann@37894
   105
(* cancel complementary terms in arbitrary sums *)
haftmann@37894
   106
haftmann@37890
   107
fun sum_proc ss ct =
haftmann@37890
   108
  let
haftmann@37890
   109
    val t = Thm.term_of ct;
haftmann@37896
   110
    val prop = Logic.mk_equals (t, cancel t);
haftmann@37896
   111
    val thm = Goal.prove (Simplifier.the_context ss) [] [] prop
haftmann@37896
   112
      (fn _ => cancel_simp_tac ss 1)
haftmann@37890
   113
  in SOME thm end handle Cancel => NONE;
paulson@5589
   114
paulson@5589
   115
haftmann@37894
   116
(* cancel like terms on the opposite sides of relations:
haftmann@37894
   117
    (x + y - z < -z + x) = (y < 0)
haftmann@37894
   118
   Works for (=) and (<=) as well as (<), if the necessary rules are supplied.
haftmann@37894
   119
   Reduces the problem to subtraction. *)
haftmann@37894
   120
haftmann@37890
   121
fun rel_proc ss ct =
wenzelm@20055
   122
  let
haftmann@37890
   123
    val t = Thm.term_of ct;
haftmann@37896
   124
    val prop = Logic.mk_equals (t, cancel t);
haftmann@37896
   125
    val thm = Goal.prove (Simplifier.the_context ss) [] [] prop
haftmann@37884
   126
      (fn _ => rtac @{thm eq_reflection} 1 THEN
haftmann@37896
   127
        resolve_tac [@{thm diff_eq_diff_less}, @{thm diff_eq_diff_less_eq}, @{thm diff_eq_diff_eq}] 1 THEN
haftmann@37896
   128
        cancel_simp_tac ss 1)
haftmann@37890
   129
  in SOME thm end handle Cancel => NONE;
paulson@5589
   130
paulson@5589
   131
end;