obsolete;
authorwenzelm
Tue May 17 10:08:24 2005 +0200 (2005-05-17)
changeset 15969201f6738480f
parent 15968 c4e8a6af2235
child 15970 b8855873d234
obsolete;
src/Provers/Arith/abstract_numerals.ML
     1.1 --- a/src/Provers/Arith/abstract_numerals.ML	Tue May 17 10:05:15 2005 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,68 +0,0 @@
     1.4 -(*  Title:      Provers/Arith/abstract_numerals.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   2001  University of Cambridge
     1.8 -
     1.9 -Simproc to extend simplification of numeric literals to cover abstract 0 and
    1.10 -1.  For example, in the two-operand case, it eliminates the need to declare
    1.11 -separate rules for the 9 combinations of 0, 1, numeral.  Given a term, it 
    1.12 -replaces all abstract 0s and 1s by the corresponding numerals.  
    1.13 -
    1.14 -The resulting equality should immediately be combined with an equation to
    1.15 -force numerical evaluation, since otherwise the literal 0s and 1s will
    1.16 -probably be written back to their abstract forms.
    1.17 -*)
    1.18 -
    1.19 -signature ABSTRACT_NUMERALS_DATA =
    1.20 -sig
    1.21 -  (*abstract syntax*)
    1.22 -  val dest_eq: thm -> term * term
    1.23 -  val is_numeral: term -> bool
    1.24 -  (*rules*)
    1.25 -  val numeral_0_eq_0: thm
    1.26 -  val numeral_1_eq_1: thm
    1.27 -  (*proof tools*)
    1.28 -  val prove_conv: tactic list -> Sign.sg -> term * term -> thm option
    1.29 -  val norm_tac: thm list -> tactic    (*proves the initial lemma*)
    1.30 -  val simplify_meta_eq: thm -> thm -> thm    (*simplifies the final theorem*)
    1.31 -end;
    1.32 -
    1.33 -
    1.34 -(*The returned simproc requires as its first argument a theorem
    1.35 -  of the form f(number_of x, ...) = ...x... *)
    1.36 -functor AbstractNumeralsFun(Data: ABSTRACT_NUMERALS_DATA):
    1.37 -  sig
    1.38 -  val proc: thm -> Sign.sg -> thm list -> term -> thm option
    1.39 -  end 
    1.40 -=
    1.41 -struct
    1.42 -
    1.43 -val (numeral0, abstract0) = Data.dest_eq Data.numeral_0_eq_0
    1.44 -val (numeral1, abstract1) = Data.dest_eq Data.numeral_1_eq_1
    1.45 -
    1.46 -(*convert abstract numbers to numerals, leave other numerals alone,
    1.47 -  reject other terms*)
    1.48 -fun convert x =
    1.49 -    if Data.is_numeral x then x
    1.50 -    else if x = abstract0 then numeral0
    1.51 -    else if x = abstract1 then numeral1
    1.52 -    else raise TERM("abstract_numerals", []) ;
    1.53 -
    1.54 -(*the simplification procedure*)
    1.55 -fun proc f_number_of_eq sg _ t =
    1.56 -  let val (f,args) = strip_comb t
    1.57 -      val t' = list_comb(f, map convert args)
    1.58 -  in
    1.59 -      if t aconv t' then   (*trivial, so do nothing*)
    1.60 -	 raise TERM("abstract_numerals", []) 
    1.61 -      else 
    1.62 -      apsome (Data.simplify_meta_eq f_number_of_eq)
    1.63 -	 (Data.prove_conv 
    1.64 -           [Data.norm_tac [Data.numeral_0_eq_0, Data.numeral_1_eq_1]] sg
    1.65 -                          (t, t'))
    1.66 -  end
    1.67 -  handle TERM _ => NONE
    1.68 -       | TYPE _ => NONE;   (*Typically (if thy doesn't include Numeral)
    1.69 -			     Undeclared type constructor "Numeral.bin"*)
    1.70 -
    1.71 -end;