src/Provers/Arith/abel_cancel.ML
author wenzelm
Sun Mar 07 12:19:47 2010 +0100 (2010-03-07)
changeset 35625 9c818cab0dd0
parent 35267 8dfd816713c6
child 35762 af3ff2ba4c54
permissions -rw-r--r--
modernized structure Object_Logic;
haftmann@24584
     1
(*  Title:      Provers/Arith/abel_cancel.ML
paulson@5589
     2
    ID:         $Id$
paulson@5589
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@5589
     4
    Copyright   1998  University of Cambridge
paulson@5589
     5
wenzelm@20055
     6
Simplification procedures for abelian groups (e.g. integers, reals,
wenzelm@20055
     7
polymorphic types).
paulson@5589
     8
wenzelm@13462
     9
- Cancel complementary terms in sums
paulson@5589
    10
- Cancel like terms on opposite sides of relations
paulson@5589
    11
*)
paulson@5589
    12
paulson@5589
    13
signature ABEL_CANCEL =
paulson@5589
    14
sig
wenzelm@27250
    15
  val eq_reflection   : thm           (*object-equality to meta-equality*)
wenzelm@27250
    16
  val T               : typ           (*the type of group elements*)
nipkow@16569
    17
  val cancel_ss       : simpset       (*abelian group cancel simpset*)
wenzelm@27250
    18
  val sum_pats        : cterm list
nipkow@16569
    19
  val eqI_rules       : thm list
nipkow@16569
    20
  val dest_eqI        : thm -> term
paulson@5589
    21
end;
paulson@5589
    22
paulson@5589
    23
paulson@5589
    24
functor Abel_Cancel (Data: ABEL_CANCEL) =
paulson@5589
    25
struct
paulson@5589
    26
wenzelm@5728
    27
open Data;
wenzelm@5728
    28
wenzelm@20055
    29
(* FIXME dependent on abstract syntax *)
wenzelm@20055
    30
haftmann@35267
    31
fun zero t = Const (@{const_name Groups.zero}, t);
haftmann@35267
    32
fun minus t = Const (@{const_name Groups.uminus}, t --> t);
paulson@5589
    33
haftmann@35267
    34
fun add_terms pos (Const (@{const_name Groups.plus}, _) $ x $ y, ts) =
wenzelm@20055
    35
      add_terms pos (x, add_terms pos (y, ts))
haftmann@35267
    36
  | add_terms pos (Const (@{const_name Groups.minus}, _) $ x $ y, ts) =
wenzelm@20055
    37
      add_terms pos (x, add_terms (not pos) (y, ts))
haftmann@35267
    38
  | add_terms pos (Const (@{const_name Groups.uminus}, _) $ x, ts) =
wenzelm@20055
    39
      add_terms (not pos) (x, ts)
wenzelm@20055
    40
  | add_terms pos (x, ts) = (pos,x) :: ts;
paulson@5589
    41
wenzelm@20055
    42
fun terms fml = add_terms true (fml, []);
paulson@5589
    43
haftmann@35267
    44
fun zero1 pt (u as (c as Const(@{const_name Groups.plus},_)) $ x $ y) =
nipkow@16569
    45
      (case zero1 pt x of NONE => (case zero1 pt y of NONE => NONE
nipkow@16569
    46
                                   | SOME z => SOME(c $ x $ z))
nipkow@16569
    47
       | SOME z => SOME(c $ z $ y))
haftmann@35267
    48
  | zero1 (pos,t) (u as (c as Const(@{const_name Groups.minus},_)) $ x $ y) =
nipkow@16569
    49
      (case zero1 (pos,t) x of
nipkow@16569
    50
         NONE => (case zero1 (not pos,t) y of NONE => NONE
nipkow@16569
    51
                  | SOME z => SOME(c $ x $ z))
nipkow@16569
    52
       | SOME z => SOME(c $ z $ y))
haftmann@35267
    53
  | zero1 (pos,t) (u as (c as Const(@{const_name Groups.uminus},_)) $ x) =
nipkow@16569
    54
      (case zero1 (not pos,t) x of NONE => NONE
nipkow@16569
    55
       | SOME z => SOME(c $ z))
nipkow@16569
    56
  | zero1 (pos,t) u =
nipkow@16569
    57
      if pos andalso (t aconv u) then SOME(zero(fastype_of t)) else NONE
paulson@5589
    58
wenzelm@20055
    59
exception Cancel;
paulson@5589
    60
nipkow@16569
    61
fun find_common _ [] _ = raise Cancel
nipkow@16569
    62
  | find_common opp ((p,l)::ls) rs =
nipkow@16569
    63
      let val pr = if opp then not p else p
nipkow@16569
    64
      in if exists (fn (q,r) => pr = q andalso l aconv r) rs then (p,l)
nipkow@16569
    65
         else find_common opp ls rs
nipkow@16569
    66
      end
paulson@5589
    67
nipkow@16569
    68
(* turns t1(t) OP t2(t) into t1(0) OP t2(0) where OP can be +, -, =, etc.
nipkow@16569
    69
   If OP = +, it must be t2(-t) rather than t2(t)
nipkow@16569
    70
*)
wenzelm@20055
    71
fun cancel t =
wenzelm@20055
    72
  let
wenzelm@20055
    73
    val c $ lhs $ rhs = t
haftmann@35267
    74
    val opp = case c of Const(@{const_name Groups.plus},_) => true | _ => false;
wenzelm@20055
    75
    val (pos,l) = find_common opp (terms lhs) (terms rhs)
wenzelm@20055
    76
    val posr = if opp then not pos else pos
wenzelm@20055
    77
    val t' = c $ (the(zero1 (pos,l) lhs)) $ (the(zero1 (posr,l) rhs))
nipkow@16569
    78
  in t' end;
nipkow@16569
    79
nipkow@16569
    80
wenzelm@20055
    81
(*A simproc to cancel complementary terms in arbitrary sums.*)
wenzelm@20055
    82
fun sum_proc ss t =
wenzelm@20055
    83
   let
wenzelm@20055
    84
     val t' = cancel t
wenzelm@20055
    85
     val thm =
wenzelm@20055
    86
       Goal.prove (Simplifier.the_context ss) [] [] (Logic.mk_equals (t, t'))
wenzelm@20055
    87
         (fn _ => simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
wenzelm@20055
    88
   in SOME thm end handle Cancel => NONE;
paulson@5589
    89
wenzelm@20055
    90
val sum_conv =
wenzelm@20055
    91
  Simplifier.mk_simproc "cancel_sums"
wenzelm@27250
    92
    (map (Drule.cterm_fun Logic.varify) Data.sum_pats) (K sum_proc);
paulson@5589
    93
paulson@5589
    94
wenzelm@20055
    95
(*A simproc to cancel like terms on the opposite sides of relations:
wenzelm@20055
    96
   (x + y - z < -z + x) = (y < 0)
wenzelm@20055
    97
  Works for (=) and (<=) as well as (<), if the necessary rules are supplied.
wenzelm@20055
    98
  Reduces the problem to subtraction.*)
wenzelm@20055
    99
fun rel_proc ss t =
wenzelm@20055
   100
  let
wenzelm@20055
   101
    val t' = cancel t
wenzelm@20055
   102
    val thm = Goal.prove (Simplifier.the_context ss) [] [] (Logic.mk_equals (t, t'))
wenzelm@20055
   103
      (fn _ => rtac eq_reflection 1 THEN
wenzelm@20055
   104
                    resolve_tac eqI_rules 1 THEN
wenzelm@20055
   105
                    simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
wenzelm@20055
   106
   in SOME thm end handle Cancel => NONE;
paulson@5589
   107
wenzelm@20055
   108
val rel_conv =
wenzelm@20055
   109
  Simplifier.mk_simproc "cancel_relations"
wenzelm@27250
   110
    (map (fn th => Thm.cterm_of (Thm.theory_of_thm th) (Data.dest_eqI th)) eqI_rules) (K rel_proc);
paulson@5589
   111
paulson@5589
   112
end;