# HG changeset patch
# User haftmann
# Date 1164990151 -3600
# Node ID f9fd69d96c4e0626be5026bc21f1f96f74d41cf1
# Parent  3d4bfc7f6363fe2a28d6f60df5177ab009f9c46d
slight cleanup in hologic.ML

diff -r 3d4bfc7f6363 -r f9fd69d96c4e src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Dec 01 17:22:30 2006 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Fri Dec 01 17:22:31 2006 +0100
@@ -414,7 +414,7 @@
         val Ts = map (typ_of_dtyp descr' sorts) cargs;
         val k = length (filter is_rec_type cargs);
         val t = if k = 0 then HOLogic.zero else
-          foldl1 plus (map Bound (k - 1 downto 0) @ [HOLogic.mk_nat 1])
+          foldl1 plus (map Bound (k - 1 downto 0) @ [HOLogic.Suc_zero])
       in
         foldr (fn (T, t') => Abs ("x", T, t')) t (Ts @ replicate k HOLogic.natT)
       end;
diff -r 3d4bfc7f6363 -r f9fd69d96c4e src/HOL/Tools/datatype_prop.ML
--- a/src/HOL/Tools/datatype_prop.ML	Fri Dec 01 17:22:30 2006 +0100
+++ b/src/HOL/Tools/datatype_prop.ML	Fri Dec 01 17:22:31 2006 +0100
@@ -377,7 +377,7 @@
         val ts = map (fn ((r, s), T) => List.nth (size_consts, dest_DtRec r) $
           Free (s, T)) (recs ~~ rec_tnames ~~ recTs);
         val t = if ts = [] then HOLogic.zero else
-          foldl1 plus (ts @ [HOLogic.mk_nat 1])
+          foldl1 plus (ts @ [HOLogic.Suc_zero])
       in
         HOLogic.mk_Trueprop (HOLogic.mk_eq (size_const $
           list_comb (Const (cname, Ts ---> T), map Free (tnames ~~ Ts)), t))
diff -r 3d4bfc7f6363 -r f9fd69d96c4e src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Fri Dec 01 17:22:30 2006 +0100
+++ b/src/HOL/arith_data.ML	Fri Dec 01 17:22:31 2006 +0100
@@ -16,7 +16,6 @@
 
 (* mk_sum, mk_norm_sum *)
 
-val one = HOLogic.mk_nat 1;
 val mk_plus = HOLogic.mk_binop "HOL.plus";
 
 fun mk_sum [] = HOLogic.zero
@@ -25,7 +24,7 @@
 
 (*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
 fun mk_norm_sum ts =
-  let val (ones, sums) = List.partition (equal one) ts in
+  let val (ones, sums) = List.partition (equal HOLogic.Suc_zero) ts in
     funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
   end;
 
@@ -37,7 +36,7 @@
   if HOLogic.is_zero tm then []
   else
     (case try HOLogic.dest_Suc tm of
-      SOME t => one :: dest_sum t
+      SOME t => HOLogic.Suc_zero :: dest_sum t
     | NONE =>
         (case try dest_plus tm of
           SOME (t, u) => dest_sum t @ dest_sum u
diff -r 3d4bfc7f6363 -r f9fd69d96c4e src/HOL/ex/reflection.ML
--- a/src/HOL/ex/reflection.ML	Fri Dec 01 17:22:30 2006 +0100
+++ b/src/HOL/ex/reflection.ML	Fri Dec 01 17:22:31 2006 +0100
@@ -190,7 +190,7 @@
 		     (AList.delete (op =) (xn,0) tml)
        val th = (instantiate 
 		     ([],
-		      [(cert vs, cvs),(cert n, t' |> index_of |> HOLogic.mk_nat |> cert)]
+		      [(cert vs, cvs),(cert n, t' |> index_of |> IntInf.fromInt |> HOLogic.mk_nat |> cert)]
 		      @cts) eq) RS sym
       in hd (Variable.export ctxt' ctxt [th])
       end)
diff -r 3d4bfc7f6363 -r f9fd69d96c4e src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Fri Dec 01 17:22:30 2006 +0100
+++ b/src/HOL/hologic.ML	Fri Dec 01 17:22:31 2006 +0100
@@ -43,13 +43,13 @@
   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
@@ -70,8 +70,9 @@
   val is_zero: term -> bool
   val mk_Suc: term -> term
   val dest_Suc: term -> term
-  val mk_nat: int -> term
-  val dest_nat: term -> int
+  val Suc_zero: term
+  val mk_nat: IntInf.int -> term
+  val dest_nat: term -> IntInf.int
   val intT: typ
   val mk_int: IntInf.int -> term
   val realT: typ
@@ -288,11 +289,13 @@
 fun dest_Suc (Const ("Suc", _) $ t) = t
   | dest_Suc t = raise TERM ("dest_Suc", [t]);
 
+val Suc_zero = mk_Suc zero;
+
 fun mk_nat 0 = zero
-  | mk_nat n = mk_Suc (mk_nat (n - 1));
+  | mk_nat n = mk_Suc (mk_nat (IntInf.- (n, 1)));
 
 fun dest_nat (Const ("HOL.zero", _)) = 0
-  | dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1
+  | dest_nat (Const ("Suc", _) $ t) = IntInf.+ (dest_nat t, 1)
   | dest_nat t = raise TERM ("dest_nat", [t]);