abstract size function in hologic.ML

--- a/src/HOL/List.thy	Thu May 17 19:49:16 2007 +0200
+++ b/src/HOL/List.thy	Thu May 17 19:49:17 2007 +0200
@@ -320,7 +320,7 @@
     fun prove_neq() =
       let
         val Type(_,listT::_) = eqT;
-        val size = Const("Nat.size", listT --> HOLogic.natT);
+        val size = HOLogic.size_const listT;
         val eq_len = HOLogic.mk_eq (size $ lhs, size $ rhs);
         val neq_len = HOLogic.mk_Trueprop (HOLogic.Not $ eq_len);
         val thm = Goal.prove (Simplifier.the_context ss) [] [] neq_len

--- a/src/HOL/Tools/datatype_abs_proofs.ML	Thu May 17 19:49:16 2007 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Thu May 17 19:49:17 2007 +0200
@@ -399,14 +399,15 @@
     val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
 
-    val size_name = "Nat.size";
+    val Const (size_name, _) = HOLogic.size_const dummyT;
     val size_names = replicate (length (hd descr)) size_name @
       map (Sign.full_name thy1) (DatatypeProp.indexify_names
         (map (fn T => name_of_typ T ^ "_size") (Library.drop (length (hd descr), recTs))));
     val def_names = map (fn s => s ^ "_def") (DatatypeProp.indexify_names
       (map (fn T => name_of_typ T ^ "_size") recTs));
 
-    fun plus (t1, t2) = Const ("HOL.plus", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2;
+    fun plus (t1, t2) =
+      Const ("HOL.plus_class.plus", HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
 
     fun make_sizefun (_, cargs) =
       let
@@ -423,11 +424,10 @@
 
     fun instance_size_class tyco thy =
       let
-        val size_sort = ["Nat.size"];
         val n = Sign.arity_number thy tyco;
       in
         thy
-        |> AxClass.prove_arity (tyco, replicate n HOLogic.typeS, size_sort)
+        |> AxClass.prove_arity (tyco, replicate n HOLogic.typeS, [HOLogic.class_size])
              (ClassPackage.intro_classes_tac [])
       end
 

--- a/src/HOL/Tools/datatype_package.ML	Thu May 17 19:49:16 2007 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Thu May 17 19:49:17 2007 +0200
@@ -562,11 +562,10 @@
 
     fun instance_size_class tyco thy =
       let
-        val size_sort = ["Nat.size"];
         val n = Sign.arity_number thy tyco;
       in
         thy
-        |> AxClass.prove_arity (tyco, replicate n HOLogic.typeS, size_sort)
+        |> AxClass.prove_arity (tyco, replicate n HOLogic.typeS, [HOLogic.class_size])
              (ClassPackage.intro_classes_tac [])
       end
 

--- a/src/HOL/Tools/datatype_prop.ML	Thu May 17 19:49:16 2007 +0200
+++ b/src/HOL/Tools/datatype_prop.ML	Thu May 17 19:49:17 2007 +0200
@@ -353,26 +353,26 @@
 
 fun make_size descr sorts thy =
   let
-    val descr' = List.concat descr;
+    val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
 
-    val size_name = "Nat.size";
+    val Const (size_name, _) = HOLogic.size_const dummyT;
     val size_names = replicate (length (hd descr)) size_name @
       map (Sign.intern_const thy) (indexify_names
         (map (fn T => name_of_typ T ^ "_size") (Library.drop (length (hd descr), recTs))));
     val size_consts = map (fn (s, T) =>
       Const (s, T --> HOLogic.natT)) (size_names ~~ recTs);
 
-    fun plus (t1, t2) = Const ("HOL.plus", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2;
+    fun plus (t1, t2) = Const ("HOL.plus_class.plus", HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
 
     fun make_size_eqn size_const T (cname, cargs) =
       let
-        val recs = List.filter is_rec_type cargs;
+        val recs = filter is_rec_type cargs;
         val Ts = map (typ_of_dtyp descr' sorts) cargs;
         val recTs = map (typ_of_dtyp descr' sorts) recs;
         val tnames = make_tnames Ts;
-        val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs));
-        val ts = map (fn ((r, s), T) => List.nth (size_consts, dest_DtRec r) $
+        val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
+        val ts = map (fn ((r, s), T) => 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.Suc_zero])

--- a/src/HOL/hologic.ML	Thu May 17 19:49:16 2007 +0200
+++ b/src/HOL/hologic.ML	Thu May 17 19:49:17 2007 +0200
@@ -73,6 +73,8 @@
   val Suc_zero: term
   val mk_nat: IntInf.int -> term
   val dest_nat: term -> IntInf.int
+  val class_size: string
+  val size_const: typ -> term
   val bitT: typ
   val B0_const: term
   val B1_const: term
@@ -281,9 +283,9 @@
 
 val natT = Type ("nat", []);
 
-val zero = Const ("HOL.zero", natT);
+val zero = Const ("HOL.zero_class.zero", natT);
 
-fun is_zero (Const ("HOL.zero", _)) = true
+fun is_zero (Const ("HOL.zero_class.zero", _)) = true
   | is_zero _ = false;
 
 fun mk_Suc t = Const ("Suc", natT --> natT) $ t;
@@ -293,13 +295,23 @@
 
 val Suc_zero = mk_Suc zero;
 
-fun mk_nat 0 = zero
-  | mk_nat n = mk_Suc (mk_nat (IntInf.- (n, 1)));
+fun mk_nat n =
+  let
+    fun mk 0 = zero
+      | mk n = mk_Suc (mk (IntInf.- (n, 1)));
+  in if IntInf.< (n, 0)
+    then error "mk_nat: negative numeral"
+    else mk n
+  end;
 
-fun dest_nat (Const ("HOL.zero", _)) = 0
+fun dest_nat (Const ("HOL.zero_class.zero", _)) = 0
   | dest_nat (Const ("Suc", _) $ t) = IntInf.+ (dest_nat t, 1)
   | dest_nat t = raise TERM ("dest_nat", [t]);
 
+val class_size = "Nat.size";
+
+fun size_const T = Const ("Nat.size_class.size", T --> natT);
+
 
 (* bit *)
 
@@ -337,7 +349,7 @@
       2 * dest_numeral bs + IntInf.fromInt (dest_bit b)
   | dest_numeral t = raise TERM ("dest_numeral", [t]);
 
-fun number_of_const T = Const ("Numeral.number_of", intT --> T);
+fun number_of_const T = Const ("Numeral.number_class.number_of", intT --> T);
 
 fun add_numerals_of (Const _) =
       I
@@ -351,17 +363,18 @@
       add_numerals_of t
   | add_numerals_of (t as _ $ _) =
       case strip_comb t
-       of (Const ("Numeral.number_of",
+       of (Const ("Numeral.number_class.number_of",
            Type (_, [_, T])), ts) => fold (cons o rpair T) ts
         | (t', ts) => add_numerals_of t' #> fold add_numerals_of ts;
 
-fun mk_number T 0 = Const ("HOL.zero", T)
-  | mk_number T 1 = Const ("HOL.one", T)
+fun mk_number T 0 = Const ("HOL.zero_class.zero", T)
+  | mk_number T 1 = Const ("HOL.one_class.one", T)
   | mk_number T i = number_of_const T $ mk_numeral i;
 
-fun dest_number (Const ("HOL.zero", T)) = (T, 0)
-  | dest_number (Const ("HOL.one", T)) = (T, 1)
-  | dest_number (Const ("Numeral.number_of", Type ("fun", [_, T])) $ t) = (T, dest_numeral t)
+fun dest_number (Const ("HOL.zero_class.zero", T)) = (T, 0)
+  | dest_number (Const ("HOL.one_class.one", T)) = (T, 1)
+  | dest_number (Const ("Numeral.number_class.number_of", Type ("fun", [_, T])) $ t) =
+      (T, dest_numeral t)
   | dest_number t = raise TERM ("dest_number", [t]);