Logical operations on numerals (see also HOL/hologic.ML).

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/numeral.ML	Thu Jul 05 00:06:12 2007 +0200
@@ -0,0 +1,55 @@
+(*  Title:      HOL/Tools/numeral.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Logical operations on numerals (see also HOL/hologic.ML).
+*)
+
+signature NUMERAL =
+sig
+  val mk_cnumeral: integer -> cterm
+  val mk_cnumber: ctyp -> integer -> cterm
+end;
+
+structure Numeral: NUMERAL =
+struct
+
+(* numeral *)
+
+fun mk_cbit 0 = @{cterm "Numeral.bit.B0"}
+  | mk_cbit 1 = @{cterm "Numeral.bit.B1"}
+  | mk_cbit _ = raise CTERM ("mk_cbit", []);
+
+fun mk_cnumeral 0 = @{cterm "Numeral.Pls"}
+  | mk_cnumeral ~1 = @{cterm "Numeral.Min"}
+  | mk_cnumeral i =
+      let val (q, r) = Integer.divmod i 2 in
+        Thm.capply (Thm.capply @{cterm "Numeral.Bit"} (mk_cnumeral q))
+          (mk_cbit (Integer.machine_int r))
+      end;
+
+
+(* number *)
+
+local
+
+val zero = @{cpat "0"};
+val zeroT = Thm.ctyp_of_term zero;
+
+val one = @{cpat "1"};
+val oneT = Thm.ctyp_of_term one;
+
+val number_of = @{cpat "number_of"};
+val numberT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term number_of)));
+
+fun instT T V = Thm.instantiate_cterm ([(V, T)], []);
+
+in
+
+fun mk_cnumber T 0 = instT T zeroT zero
+  | mk_cnumber T 1 = instT T oneT one
+  | mk_cnumber T i = Thm.capply (instT T numberT number_of) (mk_cnumeral i);
+
+end;
+
+end;