src/Provers/Arith/abel_cancel.ML
 author wenzelm Mon, 16 Nov 1998 13:54:35 +0100 changeset 5897 b3548f939dd2 parent 5728 1d1175ef2d56 child 6391 0da748358eff permissions -rw-r--r--
removed genelim.ML;
```
(*  Title:      Provers/Arith/abel_cancel.ML
ID:         \$Id\$
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

Simplification procedures for abelian groups (e.g. integers, reals)

- Cancel complementary terms in sums
- Cancel like terms on opposite sides of relations
*)

signature ABEL_CANCEL =
sig
val ss		: simpset	(*basic simpset of object-logtic*)
val eq_reflection	: thm		(*object-equality to meta-equality*)

val thy		: theory	(*the theory of the group*)
val T			: typ		(*the type of group elements*)

val zero		: term

val eq_diff_eq 	: thm
val eqI_rules		: thm list
val dest_eqI		: thm -> term

val diff_def		: thm
val minus_minus	: thm
val minus_0		: thm

val cancel_simps	: thm list
end;

functor Abel_Cancel (Data: ABEL_CANCEL) =
struct

open Data;

(*prove while suppressing timing information*)
fun prove ct = setmp Goals.proof_timing false (prove_goalw_cterm [] ct);

val plus = Const ("op +", [Data.T,Data.T] ---> Data.T);
val minus = Const ("uminus", Data.T --> Data.T);

(*Cancel corresponding terms on the two sides of the equation, NOT on
the same side!*)
val cancel_ss =
Data.cancel_simps;

fun mk_sum []  = Data.zero
| mk_sum tms = foldr1 (fn (x,y) => plus \$ x \$ y) tms;

(*We map -t to t and (in other cases) t to -t.  No need to check the type of
uminus, since the simproc is only called on sums of type T.*)
fun negate (Const("uminus",_) \$ t) = t
| negate t                       = minus \$ t;

(*Flatten a formula built from +, binary - and unary -.
No need to check types PROVIDED they are checked upon entry!*)
fun add_terms neg (Const ("op +", _) \$ x \$ y, ts) =
| add_terms neg (Const ("op -", _) \$ x \$ y, ts) =
| add_terms neg (Const ("uminus", _) \$ x, ts) =
| add_terms neg (x, ts) =
(if neg then negate x else x) :: ts;

fun terms fml = add_terms false (fml, []);

exception Cancel;

(*Cancels just the first occurrence of u, leaving the rest unchanged*)
fun cancelled (u, t::ts) = if u aconv t then ts else t :: cancelled(u,ts)
| cancelled _          = raise Cancel;

val trace = ref false;

(*Make a simproc to cancel complementary terms in sums.  Examples:
x-x = 0    x+(y-x) = y   -x+(y+(x+z)) = y+z
It will unfold the definition of diff and associate to the right if
necessary.  Rewriting is faster if the formula is already
in that form.
*)

fun sum_proc sg _ lhs =
let val _ = if !trace then writeln ("cancel_sums: LHS = " ^
string_of_cterm (cterm_of sg lhs))
else ()
val rhs = mk_sum (cancelled (head',tail))
val _ = if !trace then
writeln ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
else ()
val ct = Thm.cterm_of sg (Logic.mk_equals (lhs, rhs))
val thm = prove ct
(fn _ => [rtac eq_reflection 1,
simp_tac prepare_ss 1,
IF_UNSOLVED (simp_tac cancel_ss 1),
IF_UNSOLVED (simp_tac inverse_ss 1)])
handle ERROR =>
error("cancel_sums simproc:\nfailed to prove " ^
string_of_cterm ct)
in Some thm end
handle Cancel => None;

val sum_conv =
Simplifier.mk_simproc "cancel_sums"
[("x + y", Data.T), ("x - y", Data.T)])
sum_proc;

(*A simproc to cancel like terms on the opposite sides of relations:
(x + y - z < -z + x) = (y < 0)
Works for (=) and (<=) as well as (<), if the necessary rules are supplied.
Reduces the problem to subtraction and calls the previous simproc.
*)

(*Cancel the FIRST occurrence of a term.  If it's repeated, then repeated
calls to the simproc will be needed.*)
fun cancel1 ([], u)    = raise Match (*impossible: it's a common term*)
| cancel1 (t::ts, u) = if t aconv u then ts
else t :: cancel1 (ts,u);

val sum_cancel_ss = Data.ss addsimprocs [sum_conv]

fun rel_proc sg _ (lhs as (rel\$lt\$rt)) =
let val _ = if !trace then writeln ("cancel_relations: LHS = " ^
string_of_cterm (cterm_of sg lhs))
else ()
val ltms = terms lt
and rtms = terms rt
val common = (*inter_term miscounts repetitions, so squash them*)
gen_distinct (op aconv) (inter_term (ltms, rtms))
val _ = if null common then raise Cancel  (*nothing to do*)
else ()

fun cancelled tms = mk_sum (foldl cancel1 (tms, common))

val lt' = cancelled ltms
and rt' = cancelled rtms

val rhs = rel\$lt'\$rt'
val _ = if !trace then
writeln ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
else ()
val ct = Thm.cterm_of sg (Logic.mk_equals (lhs,rhs))

val thm = prove ct
(fn _ => [rtac eq_reflection 1,
resolve_tac eqI_rules 1,
simp_tac prepare_ss 1,
simp_tac sum_cancel_ss 1,