src/HOL/hologic.ML

--- a/src/HOL/hologic.ML	Tue Sep 21 11:11:09 1999 +0200
+++ b/src/HOL/hologic.ML	Tue Sep 21 14:13:45 1999 +0200
@@ -60,6 +60,8 @@
   val pls_const: term
   val min_const: term
   val bit_const: term
+  val int_of: int list -> int
+  val dest_binum: term -> int
 end;
 
 
@@ -230,4 +232,18 @@
 and min_const = Const ("Numeral.bin.Min", binT)
 and bit_const = Const ("Numeral.bin.Bit", [binT, boolT] ---> binT);
 
+fun int_of [] = 0
+  | int_of (b :: bs) = b + 2 * int_of bs;
+
+fun dest_bit (Const ("False", _)) = 0
+  | dest_bit (Const ("True", _)) = 1
+  | dest_bit t = raise TERM("dest_bit", [t]);
+
+fun bin_of (Const ("Numeral.bin.Pls", _)) = []
+  | bin_of (Const ("Numeral.bin.Min", _)) = [~1]
+  | bin_of (Const ("Numeral.bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
+  | bin_of t = raise TERM("bin_of", [t]);
+
+val dest_binum = int_of o bin_of;
+
 end;