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