--- 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;