# HG changeset patch
# User nipkow
# Date 864371846 -7200
# Node ID da002cef70901c5cd513fa351207812e992c7585
# Parent  a106a557d704b9eecee1f1664fde42e64bd5eb62
Added overloaded function `size' for all datatypes.

diff -r a106a557d704 -r da002cef7090 src/HOL/Arith.thy
--- a/src/HOL/Arith.thy	Thu May 22 18:29:17 1997 +0200
+++ b/src/HOL/Arith.thy	Fri May 23 09:17:26 1997 +0200
@@ -14,6 +14,8 @@
 consts
   pred      :: nat => nat
   div, mod  :: [nat, nat] => nat  (infixl 70)
+  (* size of a datatype value; overloaded *)
+  size      :: 'a => nat
 
 defs
   pred_def  "pred(m) == case m of 0 => 0 | Suc n => n"
diff -r a106a557d704 -r da002cef7090 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Thu May 22 18:29:17 1997 +0200
+++ b/src/HOL/NatDef.ML	Fri May 23 09:17:26 1997 +0200
@@ -701,6 +701,8 @@
 
 
 (* add function nat_add_primrec *) 
-val (_, nat_add_primrec) = Datatype.add_datatype
-([], "nat", [("0", [], Mixfix ("0", [], max_pri)), ("Suc", [dtTyp ([], "nat")], NoSyn)]) HOL.thy;
+val (_, nat_add_primrec, _) = Datatype.add_datatype
+([], "nat", [("0", [], Mixfix ("0", [], max_pri)), ("Suc", [dtTyp ([],
+"nat")], NoSyn)]) (add_thyname "Arith" HOL.thy);
+(* pretend Arith is part of the basic theory to fool package *)
 
diff -r a106a557d704 -r da002cef7090 src/HOL/datatype.ML
--- a/src/HOL/datatype.ML	Thu May 22 18:29:17 1997 +0200
+++ b/src/HOL/datatype.ML	Fri May 23 09:17:26 1997 +0200
@@ -143,8 +143,7 @@
 in
   fun add_datatype (typevars, tname, cons_list') thy = 
     let
-      val dummy = if length cons_list' < dtK then ()
-                  else require_thy thy "Nat" "datatype definitions";
+      val dummy = require_thy thy "Arith" "datatype definitions";
       
       fun typid(dtRek(_,id)) = id
         | typid(dtVar s) = implode (tl (explode s))
@@ -344,6 +343,19 @@
       val rules_rec = rec_rules 1 cons_list
 
 (* -------------------------------------------------------------------- *)
+(* The size function                                                    *) 
+
+      fun size_eqn(_,name,types,vns,_) =
+        let fun sum((T,vn)::args) =
+                  if is_dtRek T then "size(" ^ vn ^ ") + " ^ sum(args)
+                  else sum args
+              | sum [] = "1"
+            val rhs = if exists is_dtRek types then sum(types~~vns) else "0"
+        in ("", "size(" ^ C_exp name vns ^ ") = " ^ rhs) end;
+
+      val size_eqns  = map size_eqn cons_list;
+
+(* -------------------------------------------------------------------- *)
       val consts = 
         map const_type cons_list
         @ (if num_of_cons < dtK then []
@@ -413,7 +425,7 @@
            |> add_arities arities
            |> add_consts consts
            |> add_trrules xrules
-           |> add_axioms rules, add_primrec)
+           |> add_axioms rules, add_primrec, size_eqns)
     end
 
 (*Check if the (induction) variable occurs among the premises, which
diff -r a106a557d704 -r da002cef7090 src/HOL/thy_syntax.ML
--- a/src/HOL/thy_syntax.ML	Thu May 22 18:29:17 1997 +0200
+++ b/src/HOL/thy_syntax.ML	Fri May 23 09:17:26 1997 +0200
@@ -118,9 +118,9 @@
 
   (*generate string for calling add_datatype and build_record*)
   fun mk_params ((ts, tname), cons) =
-   ("val (thy, " ^ tname ^ "_add_primrec) = Datatype.add_datatype\n"
+   ("val (thy," ^ tname ^ "_add_primrec," ^ tname ^ "_size_eqns) = Datatype.add_datatype\n"
     ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
-    \val thy = thy"
+    \val thy = ("^tname^"_add_primrec "^tname^"_size_eqns thy)"
     ,
     "structure " ^ tname ^ " =\n\
     \struct\n\
@@ -147,7 +147,12 @@
     \val dummy = AddIffs " ^ tname ^ ".inject;\n\
     \val dummy = " ^
       (if length cons < dtK then "AddIffs " else "Addsimps ") ^
-      tname ^ ".distinct;");
+      tname ^ ".distinct;\n\
+    \val dummy = Addsimps(map (fn (_,eqn) =>\n\
+    \ prove_goalw thy [get_def thy " ^ quote("size_"^tname) ^
+                     "] eqn (fn _ => [Simp_tac 1]))\n" ^
+    tname^"_size_eqns)\n"
+   );
 
   (*parsers*)
   val tvars = type_args >> map (cat "dtVar");