Improved names for size function.
authorberghofe
Wed Aug 30 13:54:57 2000 +0200 (2000-08-30)
changeset 97398470c4662685
parent 9738 2e1dca5af2d4
child 9740 1c5b0f27de56
Improved names for size function.
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_prop.ML
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Wed Aug 30 13:54:53 2000 +0200
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Wed Aug 30 13:54:57 2000 +0200
     1.3 @@ -417,15 +417,12 @@
     1.4      val descr' = flat descr;
     1.5      val recTs = get_rec_types descr' sorts;
     1.6  
     1.7 -    val big_size_name = space_implode "_" new_type_names ^ "_size";
     1.8      val size_name = Sign.intern_const (Theory.sign_of (theory "Arith")) "size";
     1.9      val size_names = replicate (length (hd descr)) size_name @
    1.10 -      map (Sign.full_name (Theory.sign_of thy1))
    1.11 -        (if length (flat (tl descr)) = 1 then [big_size_name] else
    1.12 -          map (fn i => big_size_name ^ "_" ^ string_of_int i)
    1.13 -            (1 upto length (flat (tl descr))));
    1.14 -    val def_names = map (fn i => big_size_name ^ "_def_" ^ string_of_int i)
    1.15 -      (1 upto length recTs);
    1.16 +      map (Sign.full_name (Theory.sign_of thy1)) (DatatypeProp.indexify_names
    1.17 +        (map (fn T => name_of_typ T ^ "_size") (drop (length (hd descr), recTs))));
    1.18 +    val def_names = map (fn s => s ^ "_def") (DatatypeProp.indexify_names
    1.19 +      (map (fn T => name_of_typ T ^ "_size") recTs));
    1.20  
    1.21      fun plus (t1, t2) = Const ("op +", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2;
    1.22  
    1.23 @@ -456,7 +453,7 @@
    1.24  
    1.25      val size_thms = map (fn t => prove_goalw_cterm rewrites
    1.26        (cterm_of (Theory.sign_of thy') t) (fn _ => [rtac refl 1]))
    1.27 -        (DatatypeProp.make_size new_type_names descr sorts thy')
    1.28 +        (DatatypeProp.make_size descr sorts thy')
    1.29  
    1.30    in
    1.31      thy' |> Theory.add_path big_name |>
     2.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Aug 30 13:54:53 2000 +0200
     2.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Aug 30 13:54:57 2000 +0200
     2.3 @@ -456,10 +456,8 @@
     2.4        (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
     2.5          (1 upto (length descr')));
     2.6  
     2.7 -    val big_size_name = space_implode "_" new_type_names ^ "_size";
     2.8 -    val size_names = if length (flat (tl descr)) = 1 then [big_size_name] else
     2.9 -      map (fn i => big_size_name ^ "_" ^ string_of_int i)
    2.10 -        (1 upto length (flat (tl descr)));
    2.11 +    val size_names = DatatypeProp.indexify_names
    2.12 +      (map (fn T => name_of_typ T ^ "_size") (drop (length (hd descr), recTs)));
    2.13  
    2.14      val freeT = TFree (variant used "'t", HOLogic.termS);
    2.15      val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
    2.16 @@ -517,7 +515,7 @@
    2.17      (**** introduction of axioms ****)
    2.18  
    2.19      val rec_axs = DatatypeProp.make_primrecs new_type_names descr sorts thy2;
    2.20 -    val size_axs = if no_size then [] else DatatypeProp.make_size new_type_names descr sorts thy2;
    2.21 +    val size_axs = if no_size then [] else DatatypeProp.make_size descr sorts thy2;
    2.22  
    2.23      val (thy3, (([induct], [rec_thms]), inject)) =
    2.24        thy2 |>
     3.1 --- a/src/HOL/Tools/datatype_prop.ML	Wed Aug 30 13:54:53 2000 +0200
     3.2 +++ b/src/HOL/Tools/datatype_prop.ML	Wed Aug 30 13:54:57 2000 +0200
     3.3 @@ -31,7 +31,7 @@
     3.4        theory -> (term * term) list
     3.5    val make_case_trrules : string list -> (int * (string * DatatypeAux.dtyp list *
     3.6      (string * DatatypeAux.dtyp list) list)) list list -> ast Syntax.trrule list
     3.7 -  val make_size : string list -> (int * (string * DatatypeAux.dtyp list *
     3.8 +  val make_size : (int * (string * DatatypeAux.dtyp list *
     3.9      (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    3.10        theory -> term list
    3.11    val make_weak_case_congs : string list -> (int * (string * DatatypeAux.dtyp list *
    3.12 @@ -393,18 +393,15 @@
    3.13  
    3.14  (******************************* size functions *******************************)
    3.15  
    3.16 -fun make_size new_type_names descr sorts thy =
    3.17 +fun make_size descr sorts thy =
    3.18    let
    3.19      val descr' = flat descr;
    3.20      val recTs = get_rec_types descr' sorts;
    3.21  
    3.22 -    val big_size_name = space_implode "_" new_type_names ^ "_size";
    3.23      val size_name = Sign.intern_const (Theory.sign_of (theory "Arith")) "size";
    3.24      val size_names = replicate (length (hd descr)) size_name @
    3.25 -      map (Sign.intern_const (Theory.sign_of thy))
    3.26 -        (if length (flat (tl descr)) = 1 then [big_size_name] else
    3.27 -          map (fn i => big_size_name ^ "_" ^ string_of_int i)
    3.28 -            (1 upto length (flat (tl descr))));
    3.29 +      map (Sign.intern_const (Theory.sign_of thy)) (indexify_names
    3.30 +        (map (fn T => name_of_typ T ^ "_size") (drop (length (hd descr), recTs))));
    3.31      val size_consts = map (fn (s, T) =>
    3.32        Const (s, T --> HOLogic.natT)) (size_names ~~ recTs);
    3.33