--- a/src/HOL/Integ/simproc.ML Thu Oct 01 18:27:17 1998 +0200
+++ b/src/HOL/Integ/simproc.ML Thu Oct 01 18:27:55 1998 +0200
@@ -3,215 +3,62 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
-Simplification procedures for abelian groups (e.g. integers, reals)
+Apply Abel_Cancel to the integers
*)
+(*** Two lemmas needed for the simprocs ***)
(*Deletion of other terms in the formula, seeking the -x at the front of z*)
-Goal "((x::int) + (y + z) = y + u) = ((x + z) = u)";
-by (stac zadd_left_commute 1);
-by (rtac zadd_left_cancel 1);
-qed "zadd_cancel_21";
+val zadd_cancel_21 = prove_goal IntDef.thy
+ "((x::int) + (y + z) = y + u) = ((x + z) = u)"
+ (fn _ => [stac zadd_left_commute 1,
+ rtac zadd_left_cancel 1]);
(*A further rule to deal with the case that
everything gets cancelled on the right.*)
-Goal "((x::int) + (y + z) = y) = (x = -z)";
-by (stac zadd_left_commute 1);
-by (res_inst_tac [("t", "y")] (zadd_nat0_right RS subst) 1
- THEN stac zadd_left_cancel 1);
-by (simp_tac (simpset() addsimps [eq_zdiff_eq RS sym]) 1);
-qed "zadd_cancel_minus";
-
-
-val prepare_ss = HOL_ss addsimps [zadd_assoc, zdiff_def,
- zminus_zadd_distrib, zminus_zminus,
- zminus_nat0, zadd_nat0, zadd_nat0_right];
-
-
-
-(*prove while suppressing timing information*)
-fun prove ct = setmp Goals.proof_timing false (prove_goalw_cterm [] ct);
-
-
-(*This one cancels 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. With big formulae, rewriting is faster if the formula is already
- in that form.
-*)
-structure Sum_Cancel =
-struct
-
-val thy = IntDef.thy;
-
-val intT = Type ("IntDef.int", []);
-
-val zplus = Const ("op +", [intT,intT] ---> intT);
-val zminus = Const ("uminus", intT --> intT);
-
-val zero = Const ("IntDef.int", HOLogic.natT --> intT) $ HOLogic.zero;
-
-(*These rules eliminate the first two terms, if they cancel*)
-val cancel_laws =
- [zadd_zminus_inverse_nat, zadd_zminus_inverse_nat2,
- zadd_zminus_cancel, zminus_zadd_cancel,
- zadd_cancel_21, zadd_cancel_minus, zminus_zminus];
-
-
-val cancel_ss = HOL_ss addsimps cancel_laws;
-
-fun mk_sum [] = zero
- | mk_sum tms = foldr1 (fn (x,y) => zplus $ 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 integer sums.*)
-fun negate (Const("uminus",_) $ t) = t
- | negate t = zminus $ 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 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 writeln ("cancel_sums: 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 _ = 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)))
- val thm = prove ct
- (fn _ => [simp_tac prepare_ss 1,
- IF_UNSOLVED (simp_tac cancel_ss 1)])
- handle ERROR =>
- error("cancel_sums simproc:\nThe error(s) above occurred while trying to prove " ^
- string_of_cterm ct)
- in Some (mk_meta_eq thm) end
- handle Cancel => None;
+val zadd_cancel_end = prove_goal IntDef.thy
+ "((x::int) + (y + z) = y) = (x = -z)"
+ (fn _ => [stac zadd_left_commute 1,
+ res_inst_tac [("t", "y")] (zadd_nat0_right RS subst) 1,
+ stac zadd_left_cancel 1,
+ simp_tac (simpset() addsimps [eq_zdiff_eq RS sym]) 1]);
-val conv =
- Simplifier.mk_simproc "cancel_sums"
- (map (Thm.read_cterm (sign_of thy))
- [("x + y", intT), ("x - y", intT)])
- proc;
+structure Int_Cancel_Data =
+struct
+ val ss = HOL_ss
+ val mk_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq
+ fun mk_meta_eq r = r RS eq_reflection
+ val thy = IntDef.thy
+ val T = Type ("IntDef.int", [])
+ val zero = Const ("IntDef.int", HOLogic.natT --> T) $ HOLogic.zero
+ val add_cancel_21 = zadd_cancel_21
+ val add_cancel_end = zadd_cancel_end
+ val add_left_cancel = zadd_left_cancel
+ val add_assoc = zadd_assoc
+ val add_commute = zadd_commute
+ val add_left_commute = zadd_left_commute
+ val add_0 = zadd_nat0
+ val add_0_right = zadd_nat0_right
+
+ val eq_diff_eq = eq_zdiff_eq
+ val eqI_rules = [zless_eqI, zeq_eqI, zle_eqI]
+ fun dest_eqI th =
+ #1 (HOLogic.dest_bin "op =" HOLogic.boolT
+ (HOLogic.dest_Trueprop (concl_of th)))
+
+ val diff_def = zdiff_def
+ val minus_add_distrib = zminus_zadd_distrib
+ val minus_minus = zminus_zminus
+ val minus_0 = zminus_nat0
+ val add_inverses = [zadd_zminus_inverse, zadd_zminus_inverse2];
+ val cancel_simps = [zadd_zminus_cancel, zminus_zadd_cancel]
end;
-
-
-Addsimprocs [Sum_Cancel.conv];
-
-
-(** The idea is to cancel like terms on opposite sides via subtraction **)
-
-Goal "(x::int) - y = x' - y' ==> (x<y) = (x'<y')";
-by (asm_simp_tac (simpset() addsimps [zless_def]) 1);
-qed "zless_eqI";
+structure Int_Cancel = Abel_Cancel (Int_Cancel_Data);
-Goal "(x::int) - y = x' - y' ==> (y<=x) = (y'<=x')";
-bd zless_eqI 1;
-by (asm_simp_tac (simpset() addsimps [zle_def]) 1);
-qed "zle_eqI";
-
-Goal "(x::int) - y = x' - y' ==> (x=y) = (x'=y')";
-by Safe_tac;
-by (asm_full_simp_tac (simpset() addsimps [eq_zdiff_eq]) 1);
-by (asm_full_simp_tac (simpset() addsimps [zdiff_eq_eq]) 1);
-qed "zeq_eqI";
-
+Addsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv];
-(** For simplifying relations **)
-
-structure Rel_Cancel =
-struct
-
-(*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);
-
-
-exception Relation;
-
-val trace = ref false;
-
-val sum_cancel_ss = HOL_ss addsimprocs [Sum_Cancel.conv]
- addsimps [zadd_nat0, zadd_nat0_right];
-
-fun 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 = Sum_Cancel.terms lt
- and rtms = Sum_Cancel.terms rt
- val common = gen_distinct (op aconv)
- (inter_term (ltms, rtms))
- val _ = if null common then raise Relation (*nothing to do*)
- else ()
-
- fun cancelled tms = Sum_Cancel.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 (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
-
- val thm = prove ct
- (fn _ => [resolve_tac [zless_eqI, zeq_eqI, zle_eqI] 1,
- simp_tac prepare_ss 1,
- simp_tac sum_cancel_ss 1,
- IF_UNSOLVED
- (simp_tac (HOL_ss addsimps zadd_ac) 1)])
- handle ERROR =>
- error("cancel_relations simproc:\nThe error(s) above occurred while trying to prove " ^
- string_of_cterm ct)
- in Some (mk_meta_eq thm) end
- handle Relation => None;
-
-
-val conv =
- Simplifier.mk_simproc "cancel_relations"
- (map (Thm.read_cterm (sign_of thy))
- [("x < (y::int)", HOLogic.boolT),
- ("x = (y::int)", HOLogic.boolT),
- ("x <= (y::int)", HOLogic.boolT)])
- proc;
-
-end;
-
-
-
-Addsimprocs [Rel_Cancel.conv];