src/HOL/Tools/datatype_package.ML
changeset 21419 809e7520234a
parent 21350 6e58289b6685
child 21459 20c2ddee8bc5
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Sat Nov 18 00:20:27 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Sat Nov 18 00:20:28 2006 +0100
     1.3 @@ -640,11 +640,22 @@
     1.4  
     1.5      val case_names = map (fn s => (s ^ "_case")) new_type_names;
     1.6  
     1.7 +    fun instance_size_class tyco thy =
     1.8 +      let
     1.9 +        val size_sort = ["Nat.size"];
    1.10 +        val n = Sign.arity_number thy tyco;
    1.11 +      in
    1.12 +        thy
    1.13 +        |> AxClass.prove_arity (tyco, replicate n HOLogic.typeS, size_sort)
    1.14 +             (ClassPackage.intro_classes_tac [])
    1.15 +      end
    1.16 +
    1.17      val thy2' = thy
    1.18  
    1.19        (** new types **)
    1.20 -      |> fold (fn ((name, mx), tvs) => TypedefPackage.add_typedecls [(name, tvs, mx)])
    1.21 -           (types_syntax ~~ tyvars)
    1.22 +      |> fold2 (fn (name, mx) => fn tvs => TypedefPackage.add_typedecls [(name, tvs, mx)])
    1.23 +           types_syntax tyvars
    1.24 +      |> fold (fn (_, (name, _, _)) => instance_size_class name) descr'
    1.25        |> add_path flat_names (space_implode "_" new_type_names)
    1.26  
    1.27        (** primrec combinators **)
    1.28 @@ -813,8 +824,6 @@
    1.29  
    1.30  fun gen_rep_datatype apply_theorems alt_names raw_distinct raw_inject raw_induction thy0 =
    1.31    let
    1.32 -    val _ = Theory.requires thy0 "Inductive" "datatype representations";
    1.33 -
    1.34      val (((distinct, inject), [induction]), thy1) =
    1.35        thy0
    1.36        |> fold_map apply_theorems raw_distinct
    1.37 @@ -852,13 +861,8 @@
    1.38      val sorts = add_term_tfrees (concl_of induction', []);
    1.39      val dt_info = get_datatypes thy1;
    1.40  
    1.41 -    val (case_names_induct, case_names_exhausts) = case RuleCases.get induction
    1.42 -     of (("1", _) :: _, _) => (mk_case_names_induct descr, mk_case_names_exhausts descr (map #1 dtnames))
    1.43 -      | (cases, _) => (RuleCases.case_names (map fst cases),
    1.44 -          replicate (length ((filter (fn ((_, (name, _, _))) => member (op =)
    1.45 -            (map #1 dtnames) name) descr)))
    1.46 -            (RuleCases.case_names (map fst cases)));
    1.47 -    
    1.48 +    val (case_names_induct, case_names_exhausts) =
    1.49 +      (mk_case_names_induct descr, mk_case_names_exhausts descr (map #1 dtnames));
    1.50  
    1.51      val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
    1.52