simprocs: no theory argument -- use simpset context instead;
authorwenzelm
Sat, 08 Jul 2006 12:54:43 +0200
changeset 20055 24c127b97ab5
parent 20054 24d176b8f240
child 20056 0698a403a066
simprocs: no theory argument -- use simpset context instead; misc cleanup;
src/Provers/Arith/abel_cancel.ML
src/Provers/Arith/assoc_fold.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;
--- 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)";
-*)