# HG changeset patch # User wenzelm # Date 1152356083 -7200 # Node ID 24c127b97ab555420358cb18d1659250d5799400 # Parent 24d176b8f240b96442cbe8ed16d699bfeb40e930 simprocs: no theory argument -- use simpset context instead; misc cleanup; diff -r 24d176b8f240 -r 24c127b97ab5 src/Provers/Arith/abel_cancel.ML --- a/src/Provers/Arith/abel_cancel.ML Sat Jul 08 12:54:42 2006 +0200 +++ b/src/Provers/Arith/abel_cancel.ML Sat Jul 08 12:54:43 2006 +0200 @@ -3,15 +3,11 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge -Simplification procedures for abelian groups (e.g. integers, reals) +Simplification procedures for abelian groups (e.g. integers, reals, +polymorphic types). - Cancel complementary terms in sums - Cancel like terms on opposite sides of relations - -Modification in May 2004 by Steven Obua: polymorphic types work also now -Modification in June 2005 by Tobias Nipkow: cancel_sums works in general now -(using Clemens Ballarin's code for ordered rewriting in abelian groups) -and the whole file is reduced to a fraction of its former size. *) signature ABEL_CANCEL = @@ -30,18 +26,20 @@ open Data; - fun zero t = Const ("0", t); - fun minus t = Const ("HOL.uminus", t --> t); +(* FIXME dependent on abstract syntax *) + +fun zero t = Const ("0", t); +fun minus t = Const ("HOL.uminus", t --> t); - fun add_terms pos (Const ("HOL.plus", _) $ x $ y, ts) = - add_terms pos (x, add_terms pos (y, ts)) - | add_terms pos (Const ("HOL.minus", _) $ x $ y, ts) = - add_terms pos (x, add_terms (not pos) (y, ts)) - | add_terms pos (Const ("HOL.uminus", _) $ x, ts) = - add_terms (not pos) (x, ts) - | add_terms pos (x, ts) = (pos,x) :: ts; +fun add_terms pos (Const ("HOL.plus", _) $ x $ y, ts) = + add_terms pos (x, add_terms pos (y, ts)) + | add_terms pos (Const ("HOL.minus", _) $ x $ y, ts) = + add_terms pos (x, add_terms (not pos) (y, ts)) + | add_terms pos (Const ("HOL.uminus", _) $ x, ts) = + add_terms (not pos) (x, ts) + | add_terms pos (x, ts) = (pos,x) :: ts; - fun terms fml = add_terms true (fml, []); +fun terms fml = add_terms true (fml, []); fun zero1 pt (u as (c as Const("HOL.plus",_)) $ x $ y) = (case zero1 pt x of NONE => (case zero1 pt y of NONE => NONE @@ -58,9 +56,7 @@ | zero1 (pos,t) u = if pos andalso (t aconv u) then SOME(zero(fastype_of t)) else NONE - exception Cancel; - - val trace = ref false; +exception Cancel; fun find_common _ [] _ = raise Cancel | find_common opp ((p,l)::ls) rs = @@ -72,53 +68,47 @@ (* turns t1(t) OP t2(t) into t1(0) OP t2(0) where OP can be +, -, =, etc. If OP = +, it must be t2(-t) rather than t2(t) *) -fun cancel sg t = - let val _ = if !trace - then tracing ("Abel cancel: " ^ string_of_cterm (cterm_of sg t)) - else () - val c $ lhs $ rhs = t - val opp = case c of Const("HOL.plus",_) => true | _ => false; - val (pos,l) = find_common opp (terms lhs) (terms rhs) - val posr = if opp then not pos else pos - val t' = c $ (the(zero1 (pos,l) lhs)) $ (the(zero1 (posr,l) rhs)) - val _ = if !trace - then tracing ("cancelled: " ^ string_of_cterm (cterm_of sg t')) - else () +fun cancel t = + let + val c $ lhs $ rhs = t + val opp = case c of Const("HOL.plus",_) => true | _ => false; + val (pos,l) = find_common opp (terms lhs) (terms rhs) + val posr = if opp then not pos else pos + val t' = c $ (the(zero1 (pos,l) lhs)) $ (the(zero1 (posr,l) rhs)) in t' end; -(* A simproc to cancel complementary terms in arbitrary sums. *) -fun sum_proc sg ss t = - let val t' = cancel sg t - val thm = Goal.prove sg [] [] (Logic.mk_equals (t, t')) - (fn _ => simp_tac (Simplifier.inherit_context ss cancel_ss) 1) - in SOME thm end - handle Cancel => NONE; +(*A simproc to cancel complementary terms in arbitrary sums.*) +fun sum_proc ss t = + let + val t' = cancel t + val thm = + Goal.prove (Simplifier.the_context ss) [] [] (Logic.mk_equals (t, t')) + (fn _ => simp_tac (Simplifier.inherit_context ss cancel_ss) 1) + in SOME thm end handle Cancel => NONE; - val sum_conv = - Simplifier.mk_simproc "cancel_sums" - (map (Drule.cterm_fun Logic.varify o Thm.read_cterm (Theory.deref thy_ref)) - [("x + y", Data.T), ("x - y", Data.T)]) (* FIXME depends on concrete syntax !???!!??! *) - sum_proc; +val sum_conv = + Simplifier.mk_simproc "cancel_sums" + (map (Drule.cterm_fun Logic.varify o Thm.read_cterm (Theory.deref thy_ref)) + [("x + y", Data.T), ("x - y", Data.T)]) (* FIXME depends on concrete syntax *) + (K 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. - *) +(*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.*) +fun rel_proc ss t = + let + val t' = cancel t + val thm = Goal.prove (Simplifier.the_context ss) [] [] (Logic.mk_equals (t, t')) + (fn _ => rtac eq_reflection 1 THEN + resolve_tac eqI_rules 1 THEN + simp_tac (Simplifier.inherit_context ss cancel_ss) 1) + in SOME thm end handle Cancel => NONE; - fun rel_proc sg ss t = - let val t' = cancel sg t - val thm = Goal.prove sg [] [] (Logic.mk_equals (t, t')) - (fn _ => rtac eq_reflection 1 THEN - resolve_tac eqI_rules 1 THEN - simp_tac (Simplifier.inherit_context ss cancel_ss) 1) - in SOME thm end - handle Cancel => NONE; - - val rel_conv = - Simplifier.mk_simproc "cancel_relations" - (map (Thm.cterm_of (Theory.deref thy_ref) o Data.dest_eqI) eqI_rules) rel_proc; +val rel_conv = + Simplifier.mk_simproc "cancel_relations" + (map (Thm.cterm_of (Theory.deref thy_ref) o Data.dest_eqI) eqI_rules) (K rel_proc); end; diff -r 24d176b8f240 -r 24c127b97ab5 src/Provers/Arith/assoc_fold.ML --- a/src/Provers/Arith/assoc_fold.ML Sat Jul 08 12:54:42 2006 +0200 +++ b/src/Provers/Arith/assoc_fold.ML Sat Jul 08 12:54:43 2006 +0200 @@ -3,70 +3,51 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1999 University of Cambridge -Simplification procedure for associative operators + and * on numeric types - -Performs constant folding when the literals are separated, as in 3+n+4. +Simplification procedure for associative operators + and * on numeric +types. Performs constant folding when the literals are separated, as +in 3+n+4. *) - signature ASSOC_FOLD_DATA = sig - val ss : simpset (*basic simpset of object-logtic*) - val eq_reflection : thm (*object-equality to meta-equality*) - val thy_ref : theory_ref (*the operator's signature*) - val add_ac : thm list (*AC-rewrites for plus*) + val assoc_ss: simpset + val eq_reflection: thm end; +signature ASSOC_FOLD = +sig + val proc: simpset -> term -> thm option +end; -functor Assoc_Fold (Data: ASSOC_FOLD_DATA) = +functor Assoc_Fold(Data: ASSOC_FOLD_DATA): ASSOC_FOLD = struct - val assoc_ss = Data.ss addsimps Data.add_ac; - - exception Assoc_fail; - - fun mk_sum plus [] = raise Assoc_fail - | mk_sum plus tms = foldr1 (fn (x,y) => plus $ x $ y) tms; +exception Assoc_fail; - (*Separate the literals from the other terms being combined*) - fun sift_terms plus (t, (lits,others)) = - case t of - Const("Numeral.number_of", _) $ _ => - (t::lits, others) (*new literal*) - | (f as Const _) $ x $ y => - if f = plus - then sift_terms plus (x, sift_terms plus (y, (lits,others))) - else (lits, t::others) (*arbitrary summand*) - | _ => (lits, t::others); +fun mk_sum plus [] = raise Assoc_fail + | mk_sum plus tms = foldr1 (fn (x, y) => plus $ x $ y) tms; - val trace = ref false; +(*Separate the literals from the other terms being combined*) +fun sift_terms plus (t, (lits,others)) = + (case t of + Const("Numeral.number_of", _) $ _ => (* FIXME logic dependent *) + (t::lits, others) (*new literal*) + | (f as Const _) $ x $ y => + if f = plus + then sift_terms plus (x, sift_terms plus (y, (lits,others))) + else (lits, t::others) (*arbitrary summand*) + | _ => (lits, t::others)); - (*Make a simproc to combine all literals in a associative nest*) - fun proc thy ss lhs = - let fun show t = string_of_cterm (Thm.cterm_of thy t) - val _ = if !trace then tracing ("assoc_fold simproc: LHS = " ^ show lhs) - else () - val plus = - (case lhs of f $ _ $ _ => f | _ => error "Assoc_fold: bad pattern") - val (lits,others) = sift_terms plus (lhs, ([],[])) - val _ = if length lits < 2 - then raise Assoc_fail (*we can't reduce the number of terms*) - else () - val rhs = plus $ mk_sum plus lits $ mk_sum plus others - val _ = if !trace then tracing ("RHS = " ^ show rhs) else () - val th = Goal.prove thy [] [] (Logic.mk_equals (lhs, rhs)) - (fn _ => rtac Data.eq_reflection 1 THEN - simp_tac (Simplifier.inherit_context ss assoc_ss) 1) - in SOME th end - handle Assoc_fail => NONE; +(*A simproc to combine all literals in a associative nest*) +fun proc ss lhs = + let + val plus = (case lhs of f $ _ $ _ => f | _ => error "Assoc_fold: bad pattern") + val (lits, others) = sift_terms plus (lhs, ([],[])) + val _ = length lits < 2 andalso raise Assoc_fail (*we can't reduce the number of terms*) + val rhs = plus $ mk_sum plus lits $ mk_sum plus others + val th = Goal.prove (Simplifier.the_context ss) [] [] (Logic.mk_equals (lhs, rhs)) + (fn _ => rtac Data.eq_reflection 1 THEN + simp_tac (Simplifier.inherit_context ss Data.assoc_ss) 1) + in SOME th end handle Assoc_fail => NONE; end; - - -(*test data: -set timing; - -Goal "(#3 * (a * #34)) * (#2 * b * #9) = (x::int)"; - -Goal "a + b + c + d + e + f + g + h + i + j + k + l + m + n + oo + p + q + r + s + t + u + v + (w + x + y + z + a + #2 + b + #2 + c + #2 + d + #2 + e) + #2 + f + (#2 + g + #2 + h + #2 + i) + #2 + (j + #2 + k + #2 + l + #2 + m + #2) + n + #2 + (oo + #2 + p + #2 + q + #2 + r) + #2 + s + #2 + t + #2 + u + #2 + v + #2 + w + #2 + x + #2 + y + #2 + z + #2 = (uu::nat)"; -*)