--- 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;
--- 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)";
-*)