# HG changeset patch # User paulson # Date 907259275 -7200 # Node ID d283d61205481f3bcc94d0e9c6a20b2d54831d0a # Parent e4439230af67d5da06e8bf76ce87b52ebab1f8cf now invokes functor diff -r e4439230af67 -r d283d6120548 src/HOL/Integ/simproc.ML --- 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'<=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];