src/Provers/Arith/abel_cancel.ML
author wenzelm
Tue Aug 06 11:22:05 2002 +0200 (2002-08-06)
changeset 13462 56610e2ba220
parent 12262 11ff5f47df6e
child 13480 bb72bd43c6c3
permissions -rw-r--r--
sane interface for simprocs;
paulson@5589
     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
paulson@5589
     6
Simplification procedures for abelian groups (e.g. integers, reals)
paulson@5589
     7
wenzelm@13462
     8
- Cancel complementary terms in sums
paulson@5589
     9
- Cancel like terms on opposite sides of relations
paulson@5589
    10
*)
paulson@5589
    11
paulson@5589
    12
paulson@5589
    13
signature ABEL_CANCEL =
paulson@5589
    14
sig
wenzelm@13462
    15
  val ss                : simpset       (*basic simpset of object-logtic*)
wenzelm@13462
    16
  val eq_reflection     : thm           (*object-equality to meta-equality*)
paulson@5589
    17
wenzelm@13462
    18
  val sg_ref            : Sign.sg_ref   (*signature of the theory of the group*)
wenzelm@13462
    19
  val T                 : typ           (*the type of group elements*)
paulson@5589
    20
wenzelm@13462
    21
  val zero              : term
paulson@7586
    22
  val restrict_to_left  : thm
wenzelm@13462
    23
  val add_cancel_21     : thm
wenzelm@13462
    24
  val add_cancel_end    : thm
wenzelm@13462
    25
  val add_left_cancel   : thm
wenzelm@13462
    26
  val add_assoc         : thm
wenzelm@13462
    27
  val add_commute       : thm
wenzelm@13462
    28
  val add_left_commute  : thm
wenzelm@13462
    29
  val add_0             : thm
wenzelm@13462
    30
  val add_0_right       : thm
paulson@5589
    31
wenzelm@13462
    32
  val eq_diff_eq        : thm
wenzelm@13462
    33
  val eqI_rules         : thm list
wenzelm@13462
    34
  val dest_eqI          : thm -> term
paulson@5589
    35
wenzelm@13462
    36
  val diff_def          : thm
wenzelm@13462
    37
  val minus_add_distrib : thm
wenzelm@13462
    38
  val minus_minus       : thm
wenzelm@13462
    39
  val minus_0           : thm
paulson@5589
    40
wenzelm@13462
    41
  val add_inverses      : thm list
wenzelm@13462
    42
  val cancel_simps      : thm list
paulson@5589
    43
end;
paulson@5589
    44
paulson@5589
    45
paulson@5589
    46
functor Abel_Cancel (Data: ABEL_CANCEL) =
paulson@5589
    47
struct
paulson@5589
    48
wenzelm@5728
    49
open Data;
wenzelm@5728
    50
wenzelm@13462
    51
 val prepare_ss = Data.ss addsimps [add_assoc, diff_def,
wenzelm@13462
    52
                                    minus_add_distrib, minus_minus,
wenzelm@13462
    53
                                    minus_0, add_0, add_0_right];
paulson@5589
    54
paulson@5589
    55
 (*prove while suppressing timing information*)
wenzelm@8999
    56
 fun prove ct = setmp Library.timing false (prove_goalw_cterm [] ct);
paulson@5589
    57
paulson@5589
    58
 val plus = Const ("op +", [Data.T,Data.T] ---> Data.T);
paulson@5589
    59
 val minus = Const ("uminus", Data.T --> Data.T);
paulson@5589
    60
paulson@5589
    61
 (*Cancel corresponding terms on the two sides of the equation, NOT on
paulson@5589
    62
   the same side!*)
wenzelm@13462
    63
 val cancel_ss =
wenzelm@13462
    64
   Data.ss addsimps [add_cancel_21, add_cancel_end, minus_minus] @
paulson@7586
    65
                    (map (fn th => th RS restrict_to_left) Data.cancel_simps);
paulson@5589
    66
paulson@7586
    67
 val inverse_ss = Data.ss addsimps Data.add_inverses @ Data.cancel_simps;
paulson@5589
    68
paulson@5589
    69
 fun mk_sum []  = Data.zero
paulson@5589
    70
   | mk_sum tms = foldr1 (fn (x,y) => plus $ x $ y) tms;
paulson@5589
    71
paulson@5589
    72
 (*We map -t to t and (in other cases) t to -t.  No need to check the type of
paulson@5589
    73
   uminus, since the simproc is only called on sums of type T.*)
paulson@5589
    74
 fun negate (Const("uminus",_) $ t) = t
paulson@5589
    75
   | negate t                       = minus $ t;
paulson@5589
    76
paulson@5589
    77
 (*Flatten a formula built from +, binary - and unary -.
paulson@5589
    78
   No need to check types PROVIDED they are checked upon entry!*)
paulson@5589
    79
 fun add_terms neg (Const ("op +", _) $ x $ y, ts) =
wenzelm@13462
    80
         add_terms neg (x, add_terms neg (y, ts))
paulson@5589
    81
   | add_terms neg (Const ("op -", _) $ x $ y, ts) =
wenzelm@13462
    82
         add_terms neg (x, add_terms (not neg) (y, ts))
wenzelm@13462
    83
   | add_terms neg (Const ("uminus", _) $ x, ts) =
wenzelm@13462
    84
         add_terms (not neg) (x, ts)
wenzelm@13462
    85
   | add_terms neg (x, ts) =
wenzelm@13462
    86
         (if neg then negate x else x) :: ts;
paulson@5589
    87
paulson@5589
    88
 fun terms fml = add_terms false (fml, []);
paulson@5589
    89
paulson@5589
    90
 exception Cancel;
paulson@5589
    91
paulson@5589
    92
 (*Cancels just the first occurrence of u, leaving the rest unchanged*)
paulson@5589
    93
 fun cancelled (u, t::ts) = if u aconv t then ts else t :: cancelled(u,ts)
paulson@5589
    94
   | cancelled _          = raise Cancel;
paulson@5589
    95
paulson@5589
    96
paulson@5589
    97
 val trace = ref false;
paulson@5589
    98
paulson@5589
    99
 (*Make a simproc to cancel complementary terms in sums.  Examples:
paulson@5589
   100
    x-x = 0    x+(y-x) = y   -x+(y+(x+z)) = y+z
wenzelm@13462
   101
   It will unfold the definition of diff and associate to the right if
paulson@5589
   102
   necessary.  Rewriting is faster if the formula is already
paulson@5589
   103
   in that form.
paulson@5589
   104
 *)
paulson@5589
   105
paulson@5589
   106
 fun sum_proc sg _ lhs =
wenzelm@13462
   107
   let val _ = if !trace then tracing ("cancel_sums: LHS = " ^
wenzelm@13462
   108
                                       string_of_cterm (cterm_of sg lhs))
wenzelm@13462
   109
               else ()
paulson@5589
   110
       val (head::tail) = terms lhs
paulson@5589
   111
       val head' = negate head
paulson@5589
   112
       val rhs = mk_sum (cancelled (head',tail))
paulson@5589
   113
       and chead' = Thm.cterm_of sg head'
wenzelm@13462
   114
       val _ = if !trace then
wenzelm@13462
   115
                 tracing ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
wenzelm@13462
   116
               else ()
paulson@5610
   117
       val ct = Thm.cterm_of sg (Logic.mk_equals (lhs, rhs))
wenzelm@13462
   118
       val thm = prove ct
wenzelm@13462
   119
                   (fn _ => [rtac eq_reflection 1,
wenzelm@13462
   120
                             simp_tac prepare_ss 1,
wenzelm@13462
   121
                             IF_UNSOLVED (simp_tac cancel_ss 1),
wenzelm@13462
   122
                             IF_UNSOLVED (simp_tac inverse_ss 1)])
wenzelm@13462
   123
         handle ERROR =>
wenzelm@13462
   124
         error("cancel_sums simproc:\nfailed to prove " ^
wenzelm@13462
   125
               string_of_cterm ct)
paulson@5610
   126
   in Some thm end
paulson@5589
   127
   handle Cancel => None;
paulson@5589
   128
paulson@5589
   129
wenzelm@13462
   130
 val sum_conv =
paulson@5589
   131
     Simplifier.mk_simproc "cancel_sums"
wenzelm@9419
   132
       (map (Thm.read_cterm (Sign.deref sg_ref))
wenzelm@13462
   133
        [("x + y", Data.T), ("x - y", Data.T)])  (* FIXME depends on concrete syntax !???!!??! *)
paulson@5589
   134
       sum_proc;
paulson@5589
   135
paulson@5589
   136
paulson@5589
   137
 (*A simproc to cancel like terms on the opposite sides of relations:
paulson@5589
   138
     (x + y - z < -z + x) = (y < 0)
paulson@5589
   139
   Works for (=) and (<=) as well as (<), if the necessary rules are supplied.
paulson@5589
   140
   Reduces the problem to subtraction and calls the previous simproc.
paulson@5589
   141
 *)
paulson@5589
   142
paulson@5589
   143
 (*Cancel the FIRST occurrence of a term.  If it's repeated, then repeated
paulson@5589
   144
   calls to the simproc will be needed.*)
paulson@5589
   145
 fun cancel1 ([], u)    = raise Match (*impossible: it's a common term*)
paulson@5589
   146
   | cancel1 (t::ts, u) = if t aconv u then ts
wenzelm@13462
   147
                          else t :: cancel1 (ts,u);
paulson@5589
   148
paulson@5589
   149
paulson@5589
   150
 val sum_cancel_ss = Data.ss addsimprocs [sum_conv]
wenzelm@13462
   151
                             addsimps    [add_0, add_0_right];
paulson@5589
   152
paulson@5589
   153
 val add_ac_ss = Data.ss addsimps [add_assoc,add_commute,add_left_commute];
paulson@5589
   154
paulson@5589
   155
 fun rel_proc sg _ (lhs as (rel$lt$rt)) =
wenzelm@13462
   156
   let val _ = if !trace then tracing ("cancel_relations: LHS = " ^
wenzelm@13462
   157
                                       string_of_cterm (cterm_of sg lhs))
wenzelm@13462
   158
               else ()
paulson@5589
   159
       val ltms = terms lt
paulson@5589
   160
       and rtms = terms rt
paulson@5589
   161
       val common = (*inter_term miscounts repetitions, so squash them*)
wenzelm@13462
   162
                    gen_distinct (op aconv) (inter_term (ltms, rtms))
paulson@5589
   163
       val _ = if null common then raise Cancel  (*nothing to do*)
wenzelm@13462
   164
                                   else ()
paulson@5589
   165
paulson@5589
   166
       fun cancelled tms = mk_sum (foldl cancel1 (tms, common))
paulson@5589
   167
paulson@5589
   168
       val lt' = cancelled ltms
paulson@5589
   169
       and rt' = cancelled rtms
paulson@5589
   170
paulson@5589
   171
       val rhs = rel$lt'$rt'
wenzelm@13462
   172
       val _ = if !trace then
wenzelm@13462
   173
                 tracing ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
wenzelm@13462
   174
               else ()
paulson@5610
   175
       val ct = Thm.cterm_of sg (Logic.mk_equals (lhs,rhs))
paulson@5589
   176
wenzelm@13462
   177
       val thm = prove ct
wenzelm@13462
   178
                   (fn _ => [rtac eq_reflection 1,
wenzelm@13462
   179
                             resolve_tac eqI_rules 1,
wenzelm@13462
   180
                             simp_tac prepare_ss 1,
wenzelm@13462
   181
                             simp_tac sum_cancel_ss 1,
wenzelm@13462
   182
                             IF_UNSOLVED (simp_tac add_ac_ss 1)])
wenzelm@13462
   183
         handle ERROR =>
wenzelm@13462
   184
         error("cancel_relations simproc:\nfailed to prove " ^
wenzelm@13462
   185
               string_of_cterm ct)
paulson@5610
   186
   in Some thm end
paulson@5589
   187
   handle Cancel => None;
paulson@5589
   188
wenzelm@13462
   189
 val rel_conv =
wenzelm@13462
   190
     Simplifier.simproc_i (Sign.deref sg_ref) "cancel_relations"
wenzelm@13462
   191
       (map Data.dest_eqI eqI_rules) rel_proc;
paulson@5589
   192
paulson@5589
   193
end;