# HG changeset patch
# User wenzelm
# Date 1116317304 -7200
# Node ID 201f6738480fd0e60a4a5ccc46efa386822872b9
# Parent  c4e8a6af2235ef33f9f349a47d64939b64b4e0e4
obsolete;

diff -r c4e8a6af2235 -r 201f6738480f src/Provers/Arith/abstract_numerals.ML
--- a/src/Provers/Arith/abstract_numerals.ML	Tue May 17 10:05:15 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,68 +0,0 @@
-(*  Title:      Provers/Arith/abstract_numerals.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   2001  University of Cambridge
-
-Simproc to extend simplification of numeric literals to cover abstract 0 and
-1.  For example, in the two-operand case, it eliminates the need to declare
-separate rules for the 9 combinations of 0, 1, numeral.  Given a term, it 
-replaces all abstract 0s and 1s by the corresponding numerals.  
-
-The resulting equality should immediately be combined with an equation to
-force numerical evaluation, since otherwise the literal 0s and 1s will
-probably be written back to their abstract forms.
-*)
-
-signature ABSTRACT_NUMERALS_DATA =
-sig
-  (*abstract syntax*)
-  val dest_eq: thm -> term * term
-  val is_numeral: term -> bool
-  (*rules*)
-  val numeral_0_eq_0: thm
-  val numeral_1_eq_1: thm
-  (*proof tools*)
-  val prove_conv: tactic list -> Sign.sg -> term * term -> thm option
-  val norm_tac: thm list -> tactic    (*proves the initial lemma*)
-  val simplify_meta_eq: thm -> thm -> thm    (*simplifies the final theorem*)
-end;
-
-
-(*The returned simproc requires as its first argument a theorem
-  of the form f(number_of x, ...) = ...x... *)
-functor AbstractNumeralsFun(Data: ABSTRACT_NUMERALS_DATA):
-  sig
-  val proc: thm -> Sign.sg -> thm list -> term -> thm option
-  end 
-=
-struct
-
-val (numeral0, abstract0) = Data.dest_eq Data.numeral_0_eq_0
-val (numeral1, abstract1) = Data.dest_eq Data.numeral_1_eq_1
-
-(*convert abstract numbers to numerals, leave other numerals alone,
-  reject other terms*)
-fun convert x =
-    if Data.is_numeral x then x
-    else if x = abstract0 then numeral0
-    else if x = abstract1 then numeral1
-    else raise TERM("abstract_numerals", []) ;
-
-(*the simplification procedure*)
-fun proc f_number_of_eq sg _ t =
-  let val (f,args) = strip_comb t
-      val t' = list_comb(f, map convert args)
-  in
-      if t aconv t' then   (*trivial, so do nothing*)
-	 raise TERM("abstract_numerals", []) 
-      else 
-      apsome (Data.simplify_meta_eq f_number_of_eq)
-	 (Data.prove_conv 
-           [Data.norm_tac [Data.numeral_0_eq_0, Data.numeral_1_eq_1]] sg
-                          (t, t'))
-  end
-  handle TERM _ => NONE
-       | TYPE _ => NONE;   (*Typically (if thy doesn't include Numeral)
-			     Undeclared type constructor "Numeral.bin"*)
-
-end;