# HG changeset patch
# User paulson
# Date 1003744535 -7200
# Node ID 66d4f20eb3fce9908ce5fdf8812df34c737706cc
# Parent  56db9f3a6b3ecca721a1e16a7f4f7be1e973a68b
New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1,
binary numerals in literal arithmetic.

diff -r 56db9f3a6b3e -r 66d4f20eb3fc src/Provers/Arith/abstract_numerals.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Provers/Arith/abstract_numerals.ML	Mon Oct 22 11:55:35 2001 +0200
@@ -0,0 +1,68 @@
+(*  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;