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
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
paulson@5589
     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
paulson@5610
    15
  val ss		: simpset	(*basic simpset of object-logtic*)
paulson@5610
    16
  val eq_reflection	: thm		(*object-equality to meta-equality*)
paulson@5589
    17
paulson@5610
    18
  val thy		: theory	(*the theory of the group*)
paulson@5610
    19
  val T			: typ		(*the type of group elements*)
paulson@5589
    20
paulson@5610
    21
  val zero		: term
paulson@7586
    22
  val restrict_to_left  : thm
paulson@5589
    23
  val add_cancel_21	: thm
paulson@5589
    24
  val add_cancel_end	: thm
paulson@5589
    25
  val add_left_cancel	: thm
paulson@5610
    26
  val add_assoc		: thm
paulson@5610
    27
  val add_commute 	: thm
paulson@5610
    28
  val add_left_commute 	: thm
paulson@5610
    29
  val add_0 		: thm
paulson@5610
    30
  val add_0_right 	: thm
paulson@5589
    31
paulson@5589
    32
  val eq_diff_eq 	: thm
paulson@5589
    33
  val eqI_rules		: thm list
paulson@5589
    34
  val dest_eqI		: thm -> term
paulson@5589
    35
paulson@5589
    36
  val diff_def		: thm
paulson@5589
    37
  val minus_add_distrib	: thm
paulson@5589
    38
  val minus_minus	: thm
paulson@5589
    39
  val minus_0		: thm
paulson@5589
    40
paulson@5589
    41
  val add_inverses	: thm list
paulson@5589
    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
paulson@5589
    51
 val prepare_ss = Data.ss addsimps [add_assoc, diff_def, 
paulson@5589
    52
				    minus_add_distrib, minus_minus,
paulson@5589
    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!*)
paulson@5589
    63
 val cancel_ss = 
paulson@7586
    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) =
paulson@5589
    80
	 add_terms neg (x, add_terms neg (y, ts))
paulson@5589
    81
   | add_terms neg (Const ("op -", _) $ x $ y, ts) =
paulson@5589
    82
	 add_terms neg (x, add_terms (not neg) (y, ts))
paulson@5589
    83
   | add_terms neg (Const ("uminus", _) $ x, ts) = 
paulson@5589
    84
	 add_terms (not neg) (x, ts)
paulson@5589
    85
   | add_terms neg (x, ts) = 
paulson@5589
    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
paulson@5589
   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 =
paulson@5589
   107
   let val _ = if !trace then writeln ("cancel_sums: LHS = " ^ 
paulson@5589
   108
				       string_of_cterm (cterm_of sg lhs))
paulson@5589
   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'
paulson@5589
   114
       val _ = if !trace then 
paulson@5589
   115
		 writeln ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
paulson@5589
   116
	       else ()
paulson@5610
   117
       val ct = Thm.cterm_of sg (Logic.mk_equals (lhs, rhs))
paulson@5589
   118
       val thm = prove ct 
paulson@5610
   119
		   (fn _ => [rtac eq_reflection 1,
paulson@5610
   120
			     simp_tac prepare_ss 1,
paulson@5589
   121
			     IF_UNSOLVED (simp_tac cancel_ss 1),
paulson@5589
   122
			     IF_UNSOLVED (simp_tac inverse_ss 1)])
paulson@5589
   123
	 handle ERROR =>
paulson@5589
   124
	 error("cancel_sums simproc:\nfailed to prove " ^
paulson@5589
   125
	       string_of_cterm ct)
paulson@5610
   126
   in Some thm end
paulson@5589
   127
   handle Cancel => None;
paulson@5589
   128
paulson@5589
   129
paulson@5589
   130
 val sum_conv = 
paulson@5589
   131
     Simplifier.mk_simproc "cancel_sums"
wenzelm@6391
   132
       (map (Thm.read_cterm (Theory.sign_of Data.thy)) 
paulson@5589
   133
	[("x + y", Data.T), ("x - y", Data.T)])
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
paulson@5589
   147
			  else t :: cancel1 (ts,u);
paulson@5589
   148
paulson@5589
   149
paulson@5589
   150
 val sum_cancel_ss = Data.ss addsimprocs [sum_conv]
paulson@5589
   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)) =
paulson@5589
   156
   let val _ = if !trace then writeln ("cancel_relations: LHS = " ^ 
paulson@5589
   157
				       string_of_cterm (cterm_of sg lhs))
paulson@5589
   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*)
paulson@5589
   162
		    gen_distinct (op aconv) (inter_term (ltms, rtms))
paulson@5589
   163
       val _ = if null common then raise Cancel  (*nothing to do*)
paulson@5589
   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'
paulson@5589
   172
       val _ = if !trace then 
paulson@5589
   173
		 writeln ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
paulson@5589
   174
	       else ()
paulson@5610
   175
       val ct = Thm.cterm_of sg (Logic.mk_equals (lhs,rhs))
paulson@5589
   176
paulson@5589
   177
       val thm = prove ct 
paulson@5610
   178
		   (fn _ => [rtac eq_reflection 1,
paulson@5610
   179
			     resolve_tac eqI_rules 1,
paulson@5589
   180
			     simp_tac prepare_ss 1,
paulson@5589
   181
			     simp_tac sum_cancel_ss 1,
paulson@5589
   182
			     IF_UNSOLVED (simp_tac add_ac_ss 1)])
paulson@5589
   183
	 handle ERROR =>
paulson@5589
   184
	 error("cancel_relations simproc:\nfailed to prove " ^
paulson@5589
   185
	       string_of_cterm ct)
paulson@5610
   186
   in Some thm end
paulson@5589
   187
   handle Cancel => None;
paulson@5589
   188
paulson@5589
   189
 val rel_conv = 
paulson@5589
   190
     Simplifier.mk_simproc "cancel_relations"
wenzelm@6391
   191
       (map (Thm.cterm_of (Theory.sign_of Data.thy) o Data.dest_eqI) eqI_rules)
paulson@5589
   192
       rel_proc;
paulson@5589
   193
paulson@5589
   194
end;