added instance for class size
authorhaftmann
Sat Nov 18 00:20:28 2006 +0100 (2006-11-18)
changeset 21419809e7520234a
parent 21418 4bc2882f80af
child 21420 8b15e5e66813
added instance for class size
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_package.ML
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Sat Nov 18 00:20:27 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Sat Nov 18 00:20:28 2006 +0100
     1.3 @@ -399,7 +399,7 @@
     1.4      val big_name = space_implode "_" new_type_names;
     1.5      val thy1 = add_path flat_names big_name thy;
     1.6  
     1.7 -    val descr' = List.concat descr;
     1.8 +    val descr' = flat descr;
     1.9      val recTs = get_rec_types descr' sorts;
    1.10  
    1.11      val size_name = "Nat.size";
    1.12 @@ -414,24 +414,35 @@
    1.13      fun make_sizefun (_, cargs) =
    1.14        let
    1.15          val Ts = map (typ_of_dtyp descr' sorts) cargs;
    1.16 -        val k = length (List.filter is_rec_type cargs);
    1.17 +        val k = length (filter is_rec_type cargs);
    1.18          val t = if k = 0 then HOLogic.zero else
    1.19            foldl1 plus (map Bound (k - 1 downto 0) @ [HOLogic.mk_nat 1])
    1.20        in
    1.21          foldr (fn (T, t') => Abs ("x", T, t')) t (Ts @ replicate k HOLogic.natT)
    1.22        end;
    1.23  
    1.24 -    val fs = List.concat (map (fn (_, (_, _, constrs)) => map make_sizefun constrs) descr');
    1.25 +    val fs = maps (fn (_, (_, _, constrs)) => map make_sizefun constrs) descr';
    1.26      val fTs = map fastype_of fs;
    1.27  
    1.28 +    fun instance_size_class tyco thy =
    1.29 +      let
    1.30 +        val size_sort = ["Nat.size"];
    1.31 +        val n = Sign.arity_number thy tyco;
    1.32 +      in
    1.33 +        thy
    1.34 +        |> AxClass.prove_arity (tyco, replicate n HOLogic.typeS, size_sort)
    1.35 +             (ClassPackage.intro_classes_tac [])
    1.36 +      end
    1.37 +
    1.38      val (size_def_thms, thy') =
    1.39        thy1
    1.40        |> Theory.add_consts_i (map (fn (s, T) =>
    1.41             (Sign.base_name s, T --> HOLogic.natT, NoSyn))
    1.42             (Library.drop (length (hd descr), size_names ~~ recTs)))
    1.43 -      |> (PureThy.add_defs_i true o map Thm.no_attributes) (map (fn (((s, T), def_name), rec_name) =>
    1.44 +      |> fold (fn (_, (name, _, _)) => instance_size_class name) descr'
    1.45 +      |> PureThy.add_defs_i true (map (Thm.no_attributes o (fn (((s, T), def_name), rec_name) =>
    1.46             (def_name, Logic.mk_equals (Const (s, T --> HOLogic.natT),
    1.47 -            list_comb (Const (rec_name, fTs @ [T] ---> HOLogic.natT), fs))))
    1.48 +            list_comb (Const (rec_name, fTs @ [T] ---> HOLogic.natT), fs)))))
    1.49              (size_names ~~ recTs ~~ def_names ~~ reccomb_names))
    1.50        ||> parent_path flat_names;
    1.51  
    1.52 @@ -446,7 +457,7 @@
    1.53      |> Theory.add_path big_name
    1.54      |> PureThy.add_thmss [(("size", size_thms), [])]
    1.55      ||> Theory.parent_path
    1.56 -    |-> (fn thmss => pair (Library.flat thmss))
    1.57 +    |-> (fn thmss => pair (flat thmss))
    1.58    end;
    1.59  
    1.60  fun prove_weak_case_congs new_type_names descr sorts thy =
     2.1 --- a/src/HOL/Tools/datatype_package.ML	Sat Nov 18 00:20:27 2006 +0100
     2.2 +++ b/src/HOL/Tools/datatype_package.ML	Sat Nov 18 00:20:28 2006 +0100
     2.3 @@ -640,11 +640,22 @@
     2.4  
     2.5      val case_names = map (fn s => (s ^ "_case")) new_type_names;
     2.6  
     2.7 +    fun instance_size_class tyco thy =
     2.8 +      let
     2.9 +        val size_sort = ["Nat.size"];
    2.10 +        val n = Sign.arity_number thy tyco;
    2.11 +      in
    2.12 +        thy
    2.13 +        |> AxClass.prove_arity (tyco, replicate n HOLogic.typeS, size_sort)
    2.14 +             (ClassPackage.intro_classes_tac [])
    2.15 +      end
    2.16 +
    2.17      val thy2' = thy
    2.18  
    2.19        (** new types **)
    2.20 -      |> fold (fn ((name, mx), tvs) => TypedefPackage.add_typedecls [(name, tvs, mx)])
    2.21 -           (types_syntax ~~ tyvars)
    2.22 +      |> fold2 (fn (name, mx) => fn tvs => TypedefPackage.add_typedecls [(name, tvs, mx)])
    2.23 +           types_syntax tyvars
    2.24 +      |> fold (fn (_, (name, _, _)) => instance_size_class name) descr'
    2.25        |> add_path flat_names (space_implode "_" new_type_names)
    2.26  
    2.27        (** primrec combinators **)
    2.28 @@ -813,8 +824,6 @@
    2.29  
    2.30  fun gen_rep_datatype apply_theorems alt_names raw_distinct raw_inject raw_induction thy0 =
    2.31    let
    2.32 -    val _ = Theory.requires thy0 "Inductive" "datatype representations";
    2.33 -
    2.34      val (((distinct, inject), [induction]), thy1) =
    2.35        thy0
    2.36        |> fold_map apply_theorems raw_distinct
    2.37 @@ -852,13 +861,8 @@
    2.38      val sorts = add_term_tfrees (concl_of induction', []);
    2.39      val dt_info = get_datatypes thy1;
    2.40  
    2.41 -    val (case_names_induct, case_names_exhausts) = case RuleCases.get induction
    2.42 -     of (("1", _) :: _, _) => (mk_case_names_induct descr, mk_case_names_exhausts descr (map #1 dtnames))
    2.43 -      | (cases, _) => (RuleCases.case_names (map fst cases),
    2.44 -          replicate (length ((filter (fn ((_, (name, _, _))) => member (op =)
    2.45 -            (map #1 dtnames) name) descr)))
    2.46 -            (RuleCases.case_names (map fst cases)));
    2.47 -    
    2.48 +    val (case_names_induct, case_names_exhausts) =
    2.49 +      (mk_case_names_induct descr, mk_case_names_exhausts descr (map #1 dtnames));
    2.50  
    2.51      val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
    2.52