# HG changeset patch
# User wenzelm
# Date 1166023991 -3600
# Node ID 016eff9c5699d75c224bd29ad7821772ff518f5f
# Parent  b8166438c7726c17abd573c97f0963361888fc1f
simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
put signature into canonical order;

diff -r b8166438c772 -r 016eff9c5699 src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Wed Dec 13 16:32:20 2006 +0100
+++ b/src/HOL/hologic.ML	Wed Dec 13 16:33:11 2006 +0100
@@ -11,8 +11,8 @@
   val typeT: typ
   val boolN: string
   val boolT: typ
+  val true_const: term
   val false_const: term
-  val true_const: term
   val mk_setT: typ -> typ
   val dest_setT: typ -> typ
   val Trueprop: term
@@ -33,23 +33,23 @@
   val dest_not: term -> term
   val dest_concls: term -> term list
   val eq_const: typ -> term
+  val mk_eq: term * term -> term
+  val dest_eq: term -> term * term
   val all_const: typ -> term
+  val mk_all: string * typ * term -> term
+  val list_all: (string * typ) list * term -> term
   val exists_const: typ -> term
+  val mk_exists: string * typ * term -> term
   val choice_const: typ -> term
   val Collect_const: typ -> term
-  val mk_eq: term * term -> term
-  val dest_eq: term -> term * term
-  val mk_all: string * typ * term -> term
-  val list_all: (string * typ) list * term -> term
-  val mk_exists: string * typ * term -> term
   val mk_Collect: string * typ * term -> term
+  val class_eq: string
   val mk_mem: term * term -> term
   val dest_mem: term -> term * term
   val mk_UNIV: typ -> term
   val mk_binop: string -> term * term -> term
   val mk_binrel: string -> term * term -> term
   val dest_bin: string -> typ -> term -> term * term
-  val class_eq: string
   val unitT: typ
   val is_unitT: typ -> bool
   val unit: term
@@ -61,9 +61,9 @@
   val dest_prod: term -> term * term
   val mk_fst: term -> term
   val mk_snd: term -> term
+  val split_const: typ * typ * typ -> term
   val mk_split: term -> term
   val prodT_factors: typ -> typ list
-  val split_const: typ * typ * typ -> term
   val mk_tuple: typ -> term list -> term
   val natT: typ
   val zero: term
@@ -78,25 +78,25 @@
   val B1_const: term
   val mk_bit: int -> term
   val dest_bit: term -> int
+  val intT: typ
   val pls_const: term
   val min_const: term
   val bit_const: term
-  val number_of_const: typ -> term
   val mk_numeral: IntInf.int -> term
   val dest_numeral: term -> IntInf.int
+  val number_of_const: typ -> term
   val mk_number: typ -> IntInf.int -> term
   val dest_number: term -> typ * IntInf.int
-  val intT: typ
   val realT: typ
-  val listT: typ -> typ
-  val mk_list: typ -> term list -> term
-  val dest_list: term -> term list
   val nibbleT: typ
   val mk_nibble: int -> term
   val dest_nibble: term -> int
   val charT: typ
   val mk_char: int -> term
   val dest_char: term -> int
+  val listT: typ -> typ
+  val mk_list: typ -> term list -> term
+  val dest_list: term -> term list
   val stringT: typ
   val mk_string: string -> term
   val dest_string: term -> string
@@ -324,25 +324,19 @@
 and min_const = Const ("Numeral.Min", intT)
 and bit_const = Const ("Numeral.Bit", [intT, bitT] ---> intT);
 
-fun number_of_const T = Const ("Numeral.number_of", intT --> T);
+fun mk_numeral 0 = pls_const
+  | mk_numeral ~1 = min_const
+  | mk_numeral i =
+      let val (q, r) = IntInf.divMod (i, 2)
+      in bit_const $ mk_numeral q $ mk_bit (IntInf.toInt r) end;
 
-val mk_numeral =
-  let
-    fun mk_bit n = if n = 0 then B0_const else B1_const;
-    fun bin_of n =
-      if n = 0 then pls_const
-      else if n = ~1 then min_const
-      else
-        let
-          val (q, r) = IntInf.divMod (n, 2);
-        in bit_const $ bin_of q $ mk_bit r end;
-  in bin_of end;
+fun dest_numeral (Const ("Numeral.Pls", _)) = 0
+  | dest_numeral (Const ("Numeral.Min", _)) = ~1
+  | dest_numeral (Const ("Numeral.Bit", _) $ bs $ b) =
+      2 * dest_numeral bs + IntInf.fromInt (dest_bit b)
+  | dest_numeral t = raise TERM ("dest_numeral", [t]);
 
-fun dest_numeral (Const ("Numeral.Pls", _)) = IntInf.fromInt 0
-  | dest_numeral (Const ("Numeral.Min", _)) = IntInf.fromInt ~1
-  | dest_numeral (Const ("Numeral.Bit", _) $ bs $ b) =
-      IntInf.fromInt (dest_bit b) + (2 * dest_numeral bs)
-  | dest_numeral t = raise TERM ("dest_numeral", [t]);
+fun number_of_const T = Const ("Numeral.number_of", intT --> T);
 
 fun mk_number T 0 = Const ("HOL.zero", T)
   | mk_number T 1 = Const ("HOL.one", T)
@@ -353,6 +347,7 @@
   | dest_number (Const ("Numeral.number_of", Type ("fun", [_, T])) $ t) = (T, dest_numeral t)
   | dest_number t = raise TERM ("dest_number", [t]);
 
+
 (* real *)
 
 val realT = Type ("RealDef.real", []);