--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Provers/Arith/abel_cancel.ML Thu Oct 01 18:19:34 1998 +0200
@@ -0,0 +1,193 @@
+(* Title: Provers/Arith/abel_cancel.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+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 mk_eq : term * term -> term (*create an equality proposition*)
+ val mk_meta_eq: thm -> 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 add_cancel_21 : thm
+ val add_cancel_end : thm
+ val add_left_cancel : thm
+ val add_assoc : thm
+ val add_commute : thm
+ val add_left_commute : thm
+ val add_0 : thm
+ val add_0_right : thm
+
+ val eq_diff_eq : thm
+ val eqI_rules : thm list
+ val dest_eqI : thm -> term
+
+ val diff_def : thm
+ val minus_add_distrib : thm
+ val minus_minus : thm
+ val minus_0 : thm
+
+ val add_inverses : thm list
+ val cancel_simps : thm list
+end;
+
+
+functor Abel_Cancel (Data: ABEL_CANCEL) =
+let open Data in
+struct
+
+ val prepare_ss = Data.ss addsimps [add_assoc, diff_def,
+ minus_add_distrib, minus_minus,
+ minus_0, add_0, add_0_right];
+
+ (*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.ss addsimps [add_cancel_21, add_cancel_end, minus_minus] @
+ Data.cancel_simps;
+
+ val inverse_ss = Data.ss addsimps Data.add_inverses;
+
+ 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 (x, add_terms neg (y, ts))
+ | add_terms neg (Const ("op -", _) $ x $ y, ts) =
+ add_terms neg (x, add_terms (not neg) (y, ts))
+ | add_terms neg (Const ("uminus", _) $ x, ts) =
+ add_terms (not neg) (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 (head::tail) = terms lhs
+ val head' = negate head
+ val rhs = mk_sum (cancelled (head',tail))
+ and chead' = Thm.cterm_of sg head'
+ val _ = if !trace then
+ writeln ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
+ else ()
+ val ct = Thm.cterm_of sg (Data.mk_eq (lhs, rhs))
+ val thm = prove ct
+ (fn _ => [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 (Data.mk_meta_eq thm) end
+ handle Cancel => None;
+
+
+ val sum_conv =
+ Simplifier.mk_simproc "cancel_sums"
+ (map (Thm.read_cterm (sign_of Data.thy))
+ [("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]
+ addsimps [add_0, add_0_right];
+
+ val add_ac_ss = Data.ss addsimps [add_assoc,add_commute,add_left_commute];
+
+ 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 (Data.mk_eq (lhs,rhs))
+
+ val thm = prove ct
+ (fn _ => [resolve_tac eqI_rules 1,
+ simp_tac prepare_ss 1,
+ simp_tac sum_cancel_ss 1,
+ IF_UNSOLVED (simp_tac add_ac_ss 1)])
+ handle ERROR =>
+ error("cancel_relations simproc:\nfailed to prove " ^
+ string_of_cterm ct)
+ in Some (Data.mk_meta_eq thm) end
+ handle Cancel => None;
+
+ val rel_conv =
+ Simplifier.mk_simproc "cancel_relations"
+ (map (Thm.cterm_of (sign_of Data.thy) o Data.dest_eqI) eqI_rules)
+ rel_proc;
+
+ end
+end;
+