# HG changeset patch
# User haftmann
# Date 1163805628 -3600
# Node ID 809e7520234ac268e72127d8e4081ee695d3117a
# Parent  4bc2882f80af42b80afab03f83c5896e24c36137
added instance for class size

diff -r 4bc2882f80af -r 809e7520234a src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Sat Nov 18 00:20:27 2006 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Sat Nov 18 00:20:28 2006 +0100
@@ -399,7 +399,7 @@
     val big_name = space_implode "_" new_type_names;
     val thy1 = add_path flat_names big_name thy;
 
-    val descr' = List.concat descr;
+    val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
 
     val size_name = "Nat.size";
@@ -414,24 +414,35 @@
     fun make_sizefun (_, cargs) =
       let
         val Ts = map (typ_of_dtyp descr' sorts) cargs;
-        val k = length (List.filter is_rec_type 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])
       in
         foldr (fn (T, t') => Abs ("x", T, t')) t (Ts @ replicate k HOLogic.natT)
       end;
 
-    val fs = List.concat (map (fn (_, (_, _, constrs)) => map make_sizefun constrs) descr');
+    val fs = maps (fn (_, (_, _, constrs)) => map make_sizefun constrs) descr';
     val fTs = map fastype_of fs;
 
+    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)
+             (ClassPackage.intro_classes_tac [])
+      end
+
     val (size_def_thms, thy') =
       thy1
       |> Theory.add_consts_i (map (fn (s, T) =>
            (Sign.base_name s, T --> HOLogic.natT, NoSyn))
            (Library.drop (length (hd descr), size_names ~~ recTs)))
-      |> (PureThy.add_defs_i true o map Thm.no_attributes) (map (fn (((s, T), def_name), rec_name) =>
+      |> fold (fn (_, (name, _, _)) => instance_size_class name) descr'
+      |> PureThy.add_defs_i true (map (Thm.no_attributes o (fn (((s, T), def_name), rec_name) =>
            (def_name, Logic.mk_equals (Const (s, T --> HOLogic.natT),
-            list_comb (Const (rec_name, fTs @ [T] ---> HOLogic.natT), fs))))
+            list_comb (Const (rec_name, fTs @ [T] ---> HOLogic.natT), fs)))))
             (size_names ~~ recTs ~~ def_names ~~ reccomb_names))
       ||> parent_path flat_names;
 
@@ -446,7 +457,7 @@
     |> Theory.add_path big_name
     |> PureThy.add_thmss [(("size", size_thms), [])]
     ||> Theory.parent_path
-    |-> (fn thmss => pair (Library.flat thmss))
+    |-> (fn thmss => pair (flat thmss))
   end;
 
 fun prove_weak_case_congs new_type_names descr sorts thy =
diff -r 4bc2882f80af -r 809e7520234a src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Sat Nov 18 00:20:27 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Sat Nov 18 00:20:28 2006 +0100
@@ -640,11 +640,22 @@
 
     val case_names = map (fn s => (s ^ "_case")) new_type_names;
 
+    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)
+             (ClassPackage.intro_classes_tac [])
+      end
+
     val thy2' = thy
 
       (** new types **)
-      |> fold (fn ((name, mx), tvs) => TypedefPackage.add_typedecls [(name, tvs, mx)])
-           (types_syntax ~~ tyvars)
+      |> fold2 (fn (name, mx) => fn tvs => TypedefPackage.add_typedecls [(name, tvs, mx)])
+           types_syntax tyvars
+      |> fold (fn (_, (name, _, _)) => instance_size_class name) descr'
       |> add_path flat_names (space_implode "_" new_type_names)
 
       (** primrec combinators **)
@@ -813,8 +824,6 @@
 
 fun gen_rep_datatype apply_theorems alt_names raw_distinct raw_inject raw_induction thy0 =
   let
-    val _ = Theory.requires thy0 "Inductive" "datatype representations";
-
     val (((distinct, inject), [induction]), thy1) =
       thy0
       |> fold_map apply_theorems raw_distinct
@@ -852,13 +861,8 @@
     val sorts = add_term_tfrees (concl_of induction', []);
     val dt_info = get_datatypes thy1;
 
-    val (case_names_induct, case_names_exhausts) = case RuleCases.get induction
-     of (("1", _) :: _, _) => (mk_case_names_induct descr, mk_case_names_exhausts descr (map #1 dtnames))
-      | (cases, _) => (RuleCases.case_names (map fst cases),
-          replicate (length ((filter (fn ((_, (name, _, _))) => member (op =)
-            (map #1 dtnames) name) descr)))
-            (RuleCases.case_names (map fst cases)));
-    
+    val (case_names_induct, case_names_exhausts) =
+      (mk_case_names_induct descr, mk_case_names_exhausts descr (map #1 dtnames));
 
     val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);