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