src/Provers/Arith/abstract_numerals.ML

patch to "display"

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