--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/simproc.ML Fri Sep 18 14:39:51 1998 +0200
@@ -0,0 +1,95 @@
+(* Title: HOL/Integ/simproc
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Simplification procedures for the integers
+
+This one cancels complementary terms in sums. Examples:
+ x + (y + -x) = x + (-x + y) = y
+ -x + (y + (x + z)) = -x + (x + (y + z)) = y + z
+
+Should be used with zdiff_def (to eliminate subtraction) and zadd_ac.
+*)
+
+
+structure Int_Cancel =
+struct
+
+val intT = Type ("IntDef.int", []);
+
+val zplus = Const ("op +", [intT,intT] ---> intT);
+val zminus = Const ("uminus", intT --> intT);
+
+val ssubst_left = read_instantiate [("P", "%x. ?lhs x = ?rhs")] ssubst;
+
+fun inst_left_commute ct = instantiate' [] [None, Some ct] zadd_left_commute;
+
+(*Can LOOP, so include only if the first occurrence at the very end*)
+fun inst_commute ct = instantiate' [] [None, Some ct] zadd_commute;
+
+fun terms (t as f$x$y) =
+ if f=zplus then x :: terms y else [t]
+ | terms t = [t];
+
+val mk_sum = foldr1 (fn (x,y) => zplus $ x $ y);
+
+(*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 integer sums.*)
+fun negate (Const("uminus",_) $ t) = t
+ | negate t = zminus $ t;
+
+(*These rules eliminate the first two terms, if they cancel*)
+val cancel_laws = [zadd_zminus_cancel, zminus_zadd_cancel];
+
+exception Cancel;
+
+(*Cancels just the first occurrence of head', leaving the rest unchanged*)
+fun cancelled head' tail =
+ let fun find ([], _) = raise Cancel
+ | find (t::ts, heads) = if head' aconv t then rev heads @ ts
+ else find (ts, t::heads)
+ in mk_sum (find (tail, [])) end;
+
+
+val trace = ref false;
+
+fun proc sg _ lhs =
+ let val _ = if !trace then prs ("lhs = " ^ string_of_cterm (cterm_of sg lhs))
+ else ()
+ val (head::tail) = terms lhs
+ val head' = negate head
+ val rhs = cancelled head' tail
+ and chead' = Thm.cterm_of sg head'
+ val comms = [inst_left_commute chead' RS ssubst_left,
+ inst_commute chead' RS ssubst_left]
+ val _ = if !trace then
+ writeln ("rhs = " ^ string_of_cterm (Thm.cterm_of sg rhs))
+ else ()
+ val ct = Thm.cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
+ (*Simplification is much faster than substitution, but loops for terms
+ like (x + (-x + (-x + y))). Substitution finds the outermost -x, so
+ is seems not to loop, and the counter prevents looping for sure.*)
+ fun cancel_tac 0 = no_tac
+ | cancel_tac n =
+ (resolve_tac cancel_laws 1 ORELSE
+ resolve_tac comms 1 THEN cancel_tac (n-1));
+ val thm = prove_goalw_cterm [] ct
+ (fn _ => [cancel_tac (length tail + 1)])
+ handle ERROR =>
+ error("The error(s) above occurred while trying to prove " ^
+ string_of_cterm ct)
+ in Some (meta_eq thm) end
+ handle Cancel => None;
+
+
+val conv =
+ Simplifier.mk_simproc "cancel_sums"
+ [Thm.read_cterm (sign_of IntDef.thy) ("x + (y + (z::int))", intT)]
+ proc;
+
+end;
+
+
+Addsimprocs [Int_Cancel.conv];
+
--- a/src/HOL/ROOT.ML Fri Sep 18 14:39:08 1998 +0200
+++ b/src/HOL/ROOT.ML Fri Sep 18 14:39:51 1998 +0200
@@ -64,6 +64,8 @@
cd "$ISABELLE_HOME/src/HOL";
cd "Integ";
+use_thy "IntDef";
+use "simproc";
use_thy "Bin";
cd "..";
@@ -72,4 +74,6 @@
print_depth 8;
+Goal "True"; (*leave subgoal package empty*)
+
val HOL_build_completed = (); (*indicate successful build*)