src/HOL/hologic.ML
changeset 15965 f422f8283491
parent 15945 08e8d3fb9343
child 16835 2e7d7ec7a268
     1.1 --- a/src/HOL/hologic.ML	Mon May 16 09:35:05 2005 +0200
     1.2 +++ b/src/HOL/hologic.ML	Mon May 16 10:29:15 2005 +0200
     1.3 @@ -17,6 +17,7 @@
     1.4    val not_const: term
     1.5    val mk_setT: typ -> typ
     1.6    val dest_setT: typ -> typ
     1.7 +  val Trueprop: term
     1.8    val mk_Trueprop: term -> term
     1.9    val dest_Trueprop: term -> term
    1.10    val conj: term
    1.11 @@ -70,7 +71,7 @@
    1.12    val mk_nat: int -> term
    1.13    val dest_nat: term -> int
    1.14    val intT: typ
    1.15 -  val mk_int: int -> term
    1.16 +  val mk_int: IntInf.int -> term
    1.17    val realT: typ
    1.18    val bitT: typ
    1.19    val B0_const: term
    1.20 @@ -80,11 +81,9 @@
    1.21    val min_const: term
    1.22    val bit_const: term
    1.23    val number_of_const: typ -> term
    1.24 -  val int_of: int list -> int
    1.25 -  val intinf_of: int list -> IntInf.int
    1.26 -  val dest_binum: term -> int
    1.27 -  val mk_bin: int -> term
    1.28 -  val mk_bin_from_intinf: IntInf.int -> term
    1.29 +  val int_of: int list -> IntInf.int 
    1.30 +  val dest_binum: term -> IntInf.int
    1.31 +  val mk_bin: IntInf.int -> term
    1.32    val bin_of : term -> int list
    1.33    val mk_list: ('a -> term) -> typ -> 'a list -> term
    1.34    val dest_list: term -> term list
    1.35 @@ -311,12 +310,8 @@
    1.36  
    1.37  fun number_of_const T = Const ("Numeral.number_of", binT --> T);
    1.38  
    1.39 -
    1.40 -fun int_of [] = 0
    1.41 -  | int_of (b :: bs) = b + 2 * int_of bs;
    1.42 -
    1.43 -fun intinf_of [] = IntInf.fromInt 0
    1.44 -  | intinf_of (b :: bs) = IntInf.+ (IntInf.fromInt b, IntInf.*(IntInf.fromInt 2, intinf_of bs));
    1.45 +fun int_of [] = 0 
    1.46 +  | int_of (b :: bs) = IntInf.fromInt b + (2 * int_of bs);
    1.47  
    1.48  (*When called from a print translation, the Numeral qualifier will probably have
    1.49    been removed from Bit, bin.B0, etc.*)
    1.50 @@ -338,22 +333,18 @@
    1.51    | mk_bit 1 = B1_const
    1.52    | mk_bit _ = sys_error "mk_bit";
    1.53  
    1.54 -fun mk_bin_from_intinf  n =
    1.55 +fun mk_bin  n =
    1.56      let
    1.57 -	val zero = IntInf.fromInt 0
    1.58 -	val minus_one = IntInf.fromInt ~1
    1.59 -	val two = IntInf.fromInt 2
    1.60 -
    1.61 -	fun mk_bit n = if n = zero then B0_const else B1_const
    1.62 +	fun mk_bit n = if n = 0 then B0_const else B1_const
    1.63  								 
    1.64  	fun bin_of n = 
    1.65 -	    if n = zero then pls_const
    1.66 -	    else if n = minus_one then min_const
    1.67 +	    if n = 0 then pls_const
    1.68 +	    else if n = ~1 then min_const
    1.69  	    else 
    1.70  		let 
    1.71 -		    (*val (q,r) = IntInf.divMod (n, two): doesn't work in SML 10.0.7, but in newer versions!*)
    1.72 -	            val q = IntInf.div (n, two)
    1.73 -		    val r = IntInf.mod (n, two)
    1.74 +		    (*val (q,r) = IntInf.divMod (n, 2): doesn't work in SML 10.0.7, but in newer versions!  FIXME: put this back after new SML released!*)
    1.75 +	            val q = IntInf.div (n, 2)
    1.76 +		    val r = IntInf.mod (n, 2)
    1.77  		in
    1.78  		    bit_const $ bin_of q $ mk_bit r
    1.79  		end
    1.80 @@ -361,8 +352,6 @@
    1.81  	bin_of n
    1.82      end
    1.83  
    1.84 -val mk_bin = mk_bin_from_intinf o IntInf.fromInt;
    1.85 -
    1.86  
    1.87  (* int *)
    1.88