--- 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 =
--- 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);