# HG changeset patch
# User paulson
# Date 977148015 -3600
# Node ID 9a5d5df29e5cd0e2086fbaa1eee4e6c7f6a4de7f
# Parent  9e4a0e84d0d6eb61c7819758b27ea28dda3607a4
new simproc for cancelling common factors, etc.

diff -r 9e4a0e84d0d6 -r 9a5d5df29e5c src/Provers/Arith/extract_common_term.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Provers/Arith/extract_common_term.ML	Mon Dec 18 15:00:15 2000 +0100
@@ -0,0 +1,77 @@
+(*  Title:      Provers/Arith/extract_common_term.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2000  University of Cambridge
+
+Extract common terms in balanced expressions:
+
+     i + u + j ~~ i' + u + j'  ==  u + (i + j) ~~ u + (i' + j')
+     i + u     ~~ u            ==  u + i       ~~ u + 0
+
+where ~~ is an appropriate balancing operation (e.g. =, <=, <, -) and 0 is a 
+suitable identity for +.
+
+This massaged formula is then simplified in a user-specified way.
+*)
+
+signature EXTRACT_COMMON_TERM_DATA =
+sig
+  (*abstract syntax*)
+  val mk_sum: term list -> term
+  val dest_sum: term -> term list
+  val mk_bal: term * term -> term
+  val dest_bal: term -> term * term
+  val find_first: term -> term list -> term list
+  (*proof tools*)
+  val prove_conv: tactic list -> Sign.sg -> 
+                  thm list -> term * term -> thm option
+  val norm_tac: tactic                (*proves the result*)
+  val simplify_meta_eq: thm -> thm    (*simplifies the result*)
+end;
+
+
+functor ExtractCommonTermFun(Data: EXTRACT_COMMON_TERM_DATA):
+  sig
+  val proc: Sign.sg -> thm list -> term -> thm option
+  end 
+=
+struct
+
+(*Store the term t in the table*)
+fun update_by_coeff (tab, t) = Termtab.update ((t, ()), tab);
+
+(*a left-to-right scan of terms1, seeking a term u that is also in terms2*)
+fun find_common (terms1,terms2) =
+  let val tab2 = foldl update_by_coeff (Termtab.empty, terms2)
+      fun seek [] = raise TERM("find_common", []) 
+	| seek (u::terms) =
+	      if is_some (Termtab.lookup (tab2, u)) then u
+	      else seek terms
+  in  seek terms1 end;
+
+(*the simplification procedure*)
+fun proc sg hyps t =
+  let (*first freeze any Vars in the term to prevent flex-flex problems*)
+      val rand_s = gensym"_"
+      fun mk_inst (var as Var((a,i),T))  = 
+	    (var,  Free((a ^ rand_s ^ string_of_int i), T))
+      val t' = subst_atomic (map mk_inst (term_vars t)) t
+      val (t1,t2) = Data.dest_bal t' 
+      val terms1 = Data.dest_sum t1
+      and terms2 = Data.dest_sum t2
+      val u = find_common (terms1,terms2)
+      val terms1' = Data.find_first u terms1
+      and terms2' = Data.find_first u terms2
+      val reshape = 
+	    Data.prove_conv [Data.norm_tac] sg hyps
+	        (t', 
+		 Data.mk_bal (Data.mk_sum (u::terms1'), 
+		              Data.mk_sum (u::terms2')))
+  in
+      apsome Data.simplify_meta_eq reshape
+  end
+  handle TERM _ => None
+       | TYPE _ => None;   (*Typically (if thy doesn't include Numeral)
+			     Undeclared type constructor "Numeral.bin"*)
+
+end;