- Changed structure of name spaces
authorberghofe
Fri Oct 16 18:54:55 1998 +0200 (1998-10-16)
changeset 56616ecb6ea25f19
parent 5660 f2c5354cd32f
child 5662 72a2e33d3b9e
- Changed structure of name spaces
- Proofs for datatypes with unneeded parameters are working now
- added additional parameter flat_names
- added quiet_mode flag
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_aux.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_rep_proofs.ML
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Oct 16 18:52:17 1998 +0200
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Fri Oct 16 18:54:55 1998 +0200
     1.3 @@ -22,21 +22,21 @@
     1.4    val prove_casedist_thms : string list -> (int * (string * DatatypeAux.dtyp list *
     1.5      (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
     1.6        thm -> theory -> theory * thm list
     1.7 -  val prove_primrec_thms : string list -> (int * (string * DatatypeAux.dtyp list *
     1.8 +  val prove_primrec_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
     1.9      (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    1.10        DatatypeAux.datatype_info Symtab.table -> thm list list -> thm list list ->
    1.11          thm -> theory -> theory * string list * thm list
    1.12 -  val prove_case_thms : string list -> (int * (string * DatatypeAux.dtyp list *
    1.13 +  val prove_case_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
    1.14      (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    1.15        string list -> thm list -> theory -> theory * string list * thm list list
    1.16 -  val prove_distinctness_thms : string list -> (int * (string * DatatypeAux.dtyp list *
    1.17 +  val prove_distinctness_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
    1.18      (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    1.19        thm list list -> thm list list -> theory -> theory * thm list list
    1.20    val prove_split_thms : string list -> (int * (string * DatatypeAux.dtyp list *
    1.21      (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    1.22        thm list list -> thm list list -> thm list -> thm list list -> theory ->
    1.23          theory * (thm * thm) list
    1.24 -  val prove_size_thms : string list -> (int * (string * DatatypeAux.dtyp list *
    1.25 +  val prove_size_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
    1.26      (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    1.27        string list -> thm list -> theory -> theory * thm list
    1.28    val prove_nchotomys : string list -> (int * (string * DatatypeAux.dtyp list *
    1.29 @@ -60,7 +60,7 @@
    1.30  
    1.31  fun prove_casedist_thms new_type_names descr sorts induct thy =
    1.32    let
    1.33 -    val _ = writeln "Proving case distinction theorems...";
    1.34 +    val _ = message "Proving case distinction theorems...";
    1.35  
    1.36      val descr' = flat descr;
    1.37      val recTs = get_rec_types descr' sorts;
    1.38 @@ -96,10 +96,13 @@
    1.39  
    1.40  (*************************** primrec combinators ******************************)
    1.41  
    1.42 -fun prove_primrec_thms new_type_names descr sorts
    1.43 +fun prove_primrec_thms flat_names new_type_names descr sorts
    1.44      (dt_info : datatype_info Symtab.table) constr_inject dist_rewrites induct thy =
    1.45    let
    1.46 -    val _ = writeln "Constructing primrec combinators...";
    1.47 +    val _ = message "Constructing primrec combinators...";
    1.48 +
    1.49 +    val big_name = space_implode "_" new_type_names;
    1.50 +    val thy0 = add_path flat_names big_name thy;
    1.51  
    1.52      val descr' = flat descr;
    1.53      val recTs = get_rec_types descr' sorts;
    1.54 @@ -108,8 +111,8 @@
    1.55  
    1.56      val induct_Ps = map head_of (dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
    1.57  
    1.58 -    val big_rec_name' = (space_implode "_" new_type_names) ^ "_rec_set";
    1.59 -    val rec_set_names = map (Sign.full_name (sign_of thy))
    1.60 +    val big_rec_name' = big_name ^ "_rec_set";
    1.61 +    val rec_set_names = map (Sign.full_name (sign_of thy0))
    1.62        (if length descr' = 1 then [big_rec_name'] else
    1.63          (map ((curry (op ^) (big_rec_name' ^ "_")) o string_of_int)
    1.64            (1 upto (length descr'))));
    1.65 @@ -165,12 +168,13 @@
    1.66          (([], 0), descr' ~~ recTs ~~ rec_sets);
    1.67  
    1.68      val (thy1, {intrs = rec_intrs, elims = rec_elims, ...}) =
    1.69 -      InductivePackage.add_inductive_i false true big_rec_name' false false true
    1.70 -        rec_sets rec_intr_ts [] [] thy;
    1.71 +      setmp InductivePackage.quiet_mode (!quiet_mode)
    1.72 +        (InductivePackage.add_inductive_i false true big_rec_name' false false true
    1.73 +           rec_sets rec_intr_ts [] []) thy0;
    1.74  
    1.75      (* prove uniqueness and termination of primrec combinators *)
    1.76  
    1.77 -    val _ = writeln "Proving termination and uniqueness of primrec functions...";
    1.78 +    val _ = message "Proving termination and uniqueness of primrec functions...";
    1.79  
    1.80      fun mk_unique_tac ((tac, intrs), ((((i, (tname, _, constrs)), elim), T), T')) =
    1.81        let
    1.82 @@ -252,13 +256,14 @@
    1.83            (comb $ Free ("x", T),
    1.84             Const ("Eps", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
    1.85               HOLogic.mk_mem (HOLogic.mk_prod (Free ("x", T), Free ("y", T')), set)))))
    1.86 -               (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts));
    1.87 +               (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)) |>
    1.88 +      parent_path flat_names;
    1.89  
    1.90      val reccomb_defs = map ((get_def thy2) o Sign.base_name) reccomb_names;
    1.91  
    1.92      (* prove characteristic equations for primrec combinators *)
    1.93  
    1.94 -    val _ = writeln "Proving characteristic theorems for primrec combinators..."
    1.95 +    val _ = message "Proving characteristic theorems for primrec combinators..."
    1.96  
    1.97      val rec_thms = map (fn t => prove_goalw_cterm reccomb_defs
    1.98        (cterm_of (sign_of thy2) t) (fn _ =>
    1.99 @@ -269,15 +274,19 @@
   1.100             (DatatypeProp.make_primrecs new_type_names descr sorts thy2)
   1.101  
   1.102    in
   1.103 -    (PureThy.add_tthmss [(("recs", map Attribute.tthm_of rec_thms), [])] thy2,
   1.104 +    (thy2 |> Theory.add_path (space_implode "_" new_type_names) |>
   1.105 +             PureThy.add_tthmss [(("recs", map Attribute.tthm_of rec_thms), [])] |>
   1.106 +             Theory.parent_path,
   1.107       reccomb_names, rec_thms)
   1.108    end;
   1.109  
   1.110  (***************************** case combinators *******************************)
   1.111  
   1.112 -fun prove_case_thms new_type_names descr sorts reccomb_names primrec_thms thy =
   1.113 +fun prove_case_thms flat_names new_type_names descr sorts reccomb_names primrec_thms thy =
   1.114    let
   1.115 -    val _ = writeln "Proving characteristic theorems for case combinators...";
   1.116 +    val _ = message "Proving characteristic theorems for case combinators...";
   1.117 +
   1.118 +    val thy1 = add_path flat_names (space_implode "_" new_type_names) thy;
   1.119  
   1.120      val descr' = flat descr;
   1.121      val recTs = get_rec_types descr' sorts;
   1.122 @@ -293,7 +302,7 @@
   1.123        end) constrs) descr';
   1.124  
   1.125      val case_names = map (fn s =>
   1.126 -      Sign.full_name (sign_of thy) (s ^ "_case")) new_type_names;
   1.127 +      Sign.full_name (sign_of thy1) (s ^ "_case")) new_type_names;
   1.128  
   1.129      (* define case combinators via primrec combinators *)
   1.130  
   1.131 @@ -325,7 +334,7 @@
   1.132              Theory.add_consts_i [decl] |> Theory.add_defs_i [def];
   1.133  
   1.134          in (defs @ [get_def thy' (Sign.base_name name)], thy')
   1.135 -        end) (([], thy), (hd descr) ~~ newTs ~~ case_names ~~
   1.136 +        end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~
   1.137            (take (length newTs, reccomb_names)));
   1.138  
   1.139      val case_thms = map (map (fn t => prove_goalw_cterm (case_defs @
   1.140 @@ -333,16 +342,20 @@
   1.141          (fn _ => [rtac refl 1])))
   1.142            (DatatypeProp.make_cases new_type_names descr sorts thy2);
   1.143  
   1.144 -    val thy3 = Theory.add_trrules_i
   1.145 -      (DatatypeProp.make_case_trrules new_type_names descr) thy2
   1.146 +    val thy3 = thy2 |> Theory.add_trrules_i
   1.147 +      (DatatypeProp.make_case_trrules new_type_names descr) |>
   1.148 +      parent_path flat_names;
   1.149  
   1.150 -  in (store_thmss "cases" new_type_names case_thms thy3, case_names, case_thms)
   1.151 +  in
   1.152 +    (store_thmss "cases" new_type_names case_thms thy3, case_names, case_thms)
   1.153    end;
   1.154  
   1.155  (************************ distinctness of constructors ************************)
   1.156  
   1.157 -fun prove_distinctness_thms new_type_names descr sorts dist_rewrites case_thms thy =
   1.158 +fun prove_distinctness_thms flat_names new_type_names descr sorts dist_rewrites case_thms thy =
   1.159    let
   1.160 +    val thy1 = add_path flat_names (space_implode "_" new_type_names) thy;
   1.161 +
   1.162      val descr' = flat descr;
   1.163      val recTs = get_rec_types descr' sorts;
   1.164      val newTs = take (length (hd descr), recTs);
   1.165 @@ -375,7 +388,7 @@
   1.166          in (thy', ord_defs @ [def]) end;
   1.167  
   1.168      val (thy2, ord_defs) =
   1.169 -      foldl define_ord ((thy, []), (hd descr) ~~ newTs ~~ new_type_names);
   1.170 +      foldl define_ord ((thy1, []), (hd descr) ~~ newTs ~~ new_type_names);
   1.171  
   1.172      (**** number of constructors < dtK ****)
   1.173  
   1.174 @@ -406,7 +419,10 @@
   1.175            end) ((hd descr) ~~ (DatatypeProp.make_distincts new_type_names
   1.176              descr sorts thy2) ~~ dist_rewrites ~~ case_thms)
   1.177  
   1.178 -  in (store_thmss "distinct" new_type_names distinct_thms thy2, distinct_thms)
   1.179 +  in
   1.180 +    (thy2 |> parent_path flat_names |>
   1.181 +             store_thmss "distinct" new_type_names distinct_thms,
   1.182 +     distinct_thms)
   1.183    end;
   1.184  
   1.185  (******************************* case splitting *******************************)
   1.186 @@ -414,7 +430,7 @@
   1.187  fun prove_split_thms new_type_names descr sorts constr_inject dist_rewrites
   1.188      casedist_thms case_thms thy =
   1.189    let
   1.190 -    val _ = writeln "Proving equations for case splitting...";
   1.191 +    val _ = message "Proving equations for case splitting...";
   1.192  
   1.193      val descr' = flat descr;
   1.194      val recTs = get_rec_types descr' sorts;
   1.195 @@ -448,17 +464,20 @@
   1.196  
   1.197  (******************************* size functions *******************************)
   1.198  
   1.199 -fun prove_size_thms new_type_names descr sorts reccomb_names primrec_thms thy =
   1.200 +fun prove_size_thms flat_names new_type_names descr sorts reccomb_names primrec_thms thy =
   1.201    let
   1.202 -    val _ = writeln "Proving equations for size function...";
   1.203 +    val _ = message "Proving equations for size function...";
   1.204 +
   1.205 +    val big_name = space_implode "_" new_type_names;
   1.206 +    val thy1 = add_path flat_names big_name thy;
   1.207  
   1.208      val descr' = flat descr;
   1.209      val recTs = get_rec_types descr' sorts;
   1.210  
   1.211      val big_size_name = space_implode "_" new_type_names ^ "_size";
   1.212 -    val size_name = Sign.intern_const (sign_of (the (get_thy "Arith" thy))) "size";
   1.213 +    val size_name = Sign.intern_const (sign_of (the (get_thy "Arith" thy1))) "size";
   1.214      val size_names = replicate (length (hd descr)) size_name @
   1.215 -      map (Sign.full_name (sign_of thy))
   1.216 +      map (Sign.full_name (sign_of thy1))
   1.217          (if length (flat (tl descr)) = 1 then [big_size_name] else
   1.218            map (fn i => big_size_name ^ "_" ^ string_of_int i)
   1.219              (1 upto length (flat (tl descr))));
   1.220 @@ -480,14 +499,15 @@
   1.221      val fs = flat (map (fn (_, (_, _, constrs)) => map make_sizefun constrs) descr');
   1.222      val fTs = map fastype_of fs;
   1.223  
   1.224 -    val thy' = thy |>
   1.225 +    val thy' = thy1 |>
   1.226        Theory.add_consts_i (map (fn (s, T) =>
   1.227          (Sign.base_name s, T --> HOLogic.natT, NoSyn))
   1.228            (drop (length (hd descr), size_names ~~ recTs))) |>
   1.229        Theory.add_defs_i (map (fn (((s, T), def_name), rec_name) =>
   1.230          (def_name, Logic.mk_equals (Const (s, T --> HOLogic.natT),
   1.231            list_comb (Const (rec_name, fTs @ [T] ---> HOLogic.natT), fs))))
   1.232 -            (size_names ~~ recTs ~~ def_names ~~ reccomb_names));
   1.233 +            (size_names ~~ recTs ~~ def_names ~~ reccomb_names)) |>
   1.234 +      parent_path flat_names;
   1.235  
   1.236      val size_def_thms = map (get_axiom thy') def_names;
   1.237      val rewrites = size_def_thms @ map mk_meta_eq primrec_thms;
   1.238 @@ -497,7 +517,9 @@
   1.239          (DatatypeProp.make_size new_type_names descr sorts thy')
   1.240  
   1.241    in
   1.242 -    (PureThy.add_tthmss [(("size", map Attribute.tthm_of size_thms), [])] thy',
   1.243 +    (thy' |> Theory.add_path big_name |>
   1.244 +             PureThy.add_tthmss [(("size", map Attribute.tthm_of size_thms), [])] |>
   1.245 +             Theory.parent_path,
   1.246       size_thms)
   1.247    end;
   1.248  
   1.249 @@ -505,7 +527,7 @@
   1.250  
   1.251  fun prove_nchotomys new_type_names descr sorts casedist_thms thy =
   1.252    let
   1.253 -    val _ = writeln "Proving additional theorems for TFL...";
   1.254 +    val _ = message "Proving additional theorems for TFL...";
   1.255  
   1.256      fun prove_nchotomy (t, exhaustion) =
   1.257        let
     2.1 --- a/src/HOL/Tools/datatype_aux.ML	Fri Oct 16 18:52:17 1998 +0200
     2.2 +++ b/src/HOL/Tools/datatype_aux.ML	Fri Oct 16 18:54:55 1998 +0200
     2.3 @@ -8,10 +8,16 @@
     2.4  
     2.5  signature DATATYPE_AUX =
     2.6  sig
     2.7 +  val quiet_mode : bool ref
     2.8 +  val message : string -> unit
     2.9 +  
    2.10    val foldl1 : ('a * 'a -> 'a) -> 'a list -> 'a
    2.11  
    2.12    val get_thy : string -> theory -> theory option
    2.13  
    2.14 +  val add_path : bool -> string -> theory -> theory
    2.15 +  val parent_path : bool -> theory -> theory
    2.16 +
    2.17    val store_thmss : string -> string list -> thm list list -> theory -> theory
    2.18    val store_thms : string -> string list -> thm list -> theory -> theory
    2.19  
    2.20 @@ -55,27 +61,33 @@
    2.21  structure DatatypeAux : DATATYPE_AUX =
    2.22  struct
    2.23  
    2.24 +val quiet_mode = ref false;
    2.25 +fun message s = if !quiet_mode then () else writeln s;
    2.26 +
    2.27  (* FIXME: move to library ? *)
    2.28  fun foldl1 f (x::xs) = foldl f (x, xs);
    2.29  
    2.30  fun get_thy name thy = find_first
    2.31    (equal name o Sign.name_of o sign_of) (ancestors_of thy);
    2.32  
    2.33 +fun add_path flat_names s = if flat_names then I else Theory.add_path s;
    2.34 +fun parent_path flat_names = if flat_names then I else Theory.parent_path;
    2.35 +
    2.36  (* store theorems in theory *)
    2.37  
    2.38  fun store_thmss label tnames thmss thy =
    2.39    foldr (fn ((tname, thms), thy') => thy' |>
    2.40 -    (if length tnames = 1 then I else Theory.add_path tname) |>
    2.41 +    Theory.add_path tname |>
    2.42      PureThy.add_tthmss [((label, map Attribute.tthm_of thms), [])] |>
    2.43 -    (if length tnames = 1 then I else Theory.parent_path))
    2.44 -    (tnames ~~ thmss, thy);
    2.45 +    Theory.parent_path)
    2.46 +      (tnames ~~ thmss, thy);
    2.47  
    2.48  fun store_thms label tnames thms thy =
    2.49    foldr (fn ((tname, thm), thy') => thy' |>
    2.50 -    (if length tnames = 1 then I else Theory.add_path tname) |>
    2.51 +    Theory.add_path tname |>
    2.52      PureThy.add_tthms [((label, Attribute.tthm_of thm), [])] |>
    2.53 -    (if length tnames = 1 then I else Theory.parent_path))
    2.54 -    (tnames ~~ thms, thy);
    2.55 +    Theory.parent_path)
    2.56 +      (tnames ~~ thms, thy);
    2.57  
    2.58  (* split theorem thm_1 & ... & thm_n into n theorems *)
    2.59  
     3.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Oct 16 18:52:17 1998 +0200
     3.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Oct 16 18:54:55 1998 +0200
     3.3 @@ -8,8 +8,9 @@
     3.4  
     3.5  signature DATATYPE_PACKAGE =
     3.6  sig
     3.7 -  val add_datatype : string list -> (string list * bstring * mixfix *
     3.8 -    (bstring * mixfix * string list) list) list -> theory -> theory *
     3.9 +  val quiet_mode : bool ref
    3.10 +  val add_datatype : bool -> string list -> (string list * bstring * mixfix *
    3.11 +    (bstring * string list * mixfix) list) list -> theory -> theory *
    3.12        {distinct : thm list list,
    3.13         inject : thm list list,
    3.14         exhaustion : thm list,
    3.15 @@ -19,8 +20,8 @@
    3.16         induction : thm,
    3.17         size : thm list,
    3.18         simps : thm list}
    3.19 -  val add_datatype_i : string list -> (string list * bstring * mixfix *
    3.20 -    (bstring * mixfix * typ list) list) list -> theory -> theory *
    3.21 +  val add_datatype_i : bool -> string list -> (string list * bstring * mixfix *
    3.22 +    (bstring * typ list * mixfix) list) list -> theory -> theory *
    3.23        {distinct : thm list list,
    3.24         inject : thm list list,
    3.25         exhaustion : thm list,
    3.26 @@ -57,6 +58,8 @@
    3.27  
    3.28  open DatatypeAux;
    3.29  
    3.30 +val quiet_mode = quiet_mode;
    3.31 +
    3.32  (* data kind 'HOL/datatypes' *)
    3.33  
    3.34  structure DatatypesArgs =
    3.35 @@ -232,30 +235,30 @@
    3.36    foldr (fn ((tname, t), (thy', axs)) =>
    3.37      let
    3.38        val thy'' = thy' |>
    3.39 -        (if length tnames = 1 then I else Theory.add_path tname) |>
    3.40 +        Theory.add_path tname |>
    3.41          PureThy.add_axioms_i [((label, t), [])];
    3.42        val ax = get_axiom thy'' label
    3.43 -    in (if length tnames = 1 then thy'' else Theory.parent_path thy'', ax::axs)
    3.44 +    in (Theory.parent_path thy'', ax::axs)
    3.45      end) (tnames ~~ ts, (thy, []));
    3.46  
    3.47  fun add_and_get_axiomss label tnames tss thy =
    3.48    foldr (fn ((tname, ts), (thy', axss)) =>
    3.49      let
    3.50        val thy'' = thy' |>
    3.51 -        (if length tnames = 1 then I else Theory.add_path tname) |>
    3.52 +        Theory.add_path tname |>
    3.53          PureThy.add_axiomss_i [((label, ts), [])];
    3.54        val axs = PureThy.get_thms thy'' label
    3.55 -    in (if length tnames = 1 then thy'' else Theory.parent_path thy'', axs::axss)
    3.56 +    in (Theory.parent_path thy'', axs::axss)
    3.57      end) (tnames ~~ tss, (thy, []));
    3.58  
    3.59 -fun add_datatype_axm new_type_names descr sorts types_syntax constr_syntax dt_info thy =
    3.60 +fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info thy =
    3.61    let
    3.62      val descr' = flat descr;
    3.63      val recTs = get_rec_types descr' sorts;
    3.64      val used = foldr add_typ_tfree_names (recTs, []);
    3.65      val newTs = take (length (hd descr), recTs);
    3.66  
    3.67 -    val _ = writeln ("Adding axioms for datatype(s) " ^ commas new_type_names);
    3.68 +    val _ = message ("Adding axioms for datatype(s) " ^ commas new_type_names);
    3.69  
    3.70      (**** declare new types and constants ****)
    3.71  
    3.72 @@ -298,8 +301,6 @@
    3.73  
    3.74      val thy2 = thy |>
    3.75  
    3.76 -      Theory.add_path (space_implode "_" new_type_names) |>
    3.77 -
    3.78        (** new types **)
    3.79  
    3.80        curry (foldr (fn (((name, mx), tvs), thy') => thy' |>
    3.81 @@ -309,16 +310,7 @@
    3.82              replicate (length tvs) HOLogic.termS, HOLogic.termS)]))
    3.83                (types_syntax ~~ tyvars) |>
    3.84  
    3.85 -      (** constructors **)
    3.86 -
    3.87 -      curry (foldr (fn (((((_, (_, _, constrs)), T), tname),
    3.88 -        constr_syntax'), thy') => thy' |>
    3.89 -          (if length newTs = 1 then I else Theory.add_path tname) |>
    3.90 -            Theory.add_consts_i (map (fn ((_, cargs), (cname, mx)) =>
    3.91 -              (cname, map (typ_of_dtyp descr' sorts) cargs ---> T, mx))
    3.92 -                (constrs ~~ constr_syntax')) |>
    3.93 -          (if length newTs = 1 then I else Theory.parent_path)))
    3.94 -            (hd descr ~~ newTs ~~ new_type_names ~~ constr_syntax) |>
    3.95 +      add_path flat_names (space_implode "_" new_type_names) |>
    3.96  
    3.97        (** primrec combinators **)
    3.98  
    3.99 @@ -345,22 +337,40 @@
   3.100  
   3.101        Theory.add_consts_i (map (fn (s, T) =>
   3.102          (Sign.base_name s, T --> HOLogic.natT, NoSyn))
   3.103 -          (size_names ~~ drop (length (hd descr), recTs)));
   3.104 +          (size_names ~~ drop (length (hd descr), recTs))) |>
   3.105 +
   3.106 +      (** constructors **)
   3.107 +
   3.108 +      parent_path flat_names |>
   3.109 +      curry (foldr (fn (((((_, (_, _, constrs)), T), tname),
   3.110 +        constr_syntax'), thy') => thy' |>
   3.111 +          add_path flat_names tname |>
   3.112 +            Theory.add_consts_i (map (fn ((_, cargs), (cname, mx)) =>
   3.113 +              (cname, map (typ_of_dtyp descr' sorts) cargs ---> T, mx))
   3.114 +                (constrs ~~ constr_syntax')) |>
   3.115 +          parent_path flat_names))
   3.116 +            (hd descr ~~ newTs ~~ new_type_names ~~ constr_syntax);
   3.117  
   3.118      (**** introduction of axioms ****)
   3.119  
   3.120 +    val rec_axs = DatatypeProp.make_primrecs new_type_names descr sorts thy2;
   3.121 +    val size_axs = DatatypeProp.make_size new_type_names descr sorts thy2;
   3.122 +
   3.123      val (thy3, inject) = thy2 |>
   3.124 +      Theory.add_path (space_implode "_" new_type_names) |>
   3.125        PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts), [])] |>
   3.126 +      PureThy.add_axiomss_i [(("recs", rec_axs), [])] |>
   3.127 +      PureThy.add_axiomss_i [(("size", size_axs), [])] |>
   3.128 +      Theory.parent_path |>
   3.129        add_and_get_axiomss "inject" new_type_names
   3.130          (DatatypeProp.make_injs descr sorts);
   3.131 +    val induct = get_axiom thy3 "induct";
   3.132 +    val rec_thms = get_thms thy3 "recs";
   3.133 +    val size_thms = get_thms thy3 "size";
   3.134      val (thy4, distinct) = add_and_get_axiomss "distinct" new_type_names
   3.135        (DatatypeProp.make_distincts new_type_names descr sorts thy3) thy3;
   3.136 -    val induct = get_axiom thy4 "induct";
   3.137 -
   3.138      val (thy5, exhaustion) = add_and_get_axioms "exhaust" new_type_names
   3.139 -      (DatatypeProp.make_casedists descr sorts) (PureThy.add_axiomss_i [(("recs",
   3.140 -        DatatypeProp.make_primrecs new_type_names descr sorts thy4), [])] thy4);
   3.141 -    val rec_thms = get_thms thy5 "recs";
   3.142 +      (DatatypeProp.make_casedists descr sorts) thy4;
   3.143      val (thy6, case_thms) = add_and_get_axiomss "cases" new_type_names
   3.144        (DatatypeProp.make_cases new_type_names descr sorts thy5) thy5;
   3.145      val (split_ts, split_asm_ts) = ListPair.unzip
   3.146 @@ -372,9 +382,6 @@
   3.147        (DatatypeProp.make_nchotomys descr sorts) thy8;
   3.148      val (thy10, case_congs) = add_and_get_axioms "case_cong" new_type_names
   3.149        (DatatypeProp.make_case_congs new_type_names descr sorts thy9) thy9;
   3.150 -    val thy11 = PureThy.add_axiomss_i [(("size",
   3.151 -      DatatypeProp.make_size new_type_names descr sorts thy10), [])] thy10;
   3.152 -    val size_thms = get_thms thy11 "size";
   3.153      
   3.154      val dt_infos = map (make_dt_info descr' induct reccomb_names rec_thms)
   3.155        ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
   3.156 @@ -382,17 +389,18 @@
   3.157  
   3.158      val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   3.159  
   3.160 -    val thy12 = thy11 |>
   3.161 +    val thy11 = thy10 |>
   3.162 +      Theory.add_path (space_implode "_" new_type_names) |>
   3.163        PureThy.add_tthmss [(("simps", map Attribute.tthm_of simps), [])] |>
   3.164        put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
   3.165        Theory.parent_path;
   3.166  
   3.167 -    val _ = store_clasimp thy12 ((claset_of thy12, simpset_of thy12)
   3.168 +    val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11)
   3.169        addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
   3.170        addIffs flat inject addDistinct (distinct, hd descr));
   3.171  
   3.172    in
   3.173 -    (thy12,
   3.174 +    (thy11,
   3.175       {distinct = distinct,
   3.176        inject = inject,
   3.177        exhaustion = exhaustion,
   3.178 @@ -407,30 +415,29 @@
   3.179  
   3.180  (******************* definitional introduction of datatypes *******************)
   3.181  
   3.182 -fun add_datatype_def new_type_names descr sorts types_syntax constr_syntax dt_info thy =
   3.183 +fun add_datatype_def flat_names new_type_names descr sorts types_syntax constr_syntax dt_info thy =
   3.184    let
   3.185 -    val _ = writeln ("Proofs for datatype(s) " ^ commas new_type_names);
   3.186 +    val _ = message ("Proofs for datatype(s) " ^ commas new_type_names);
   3.187  
   3.188      val (thy2, inject, dist_rewrites, induct) = thy |>
   3.189 -      Theory.add_path (space_implode "_" new_type_names) |>
   3.190 -      DatatypeRepProofs.representation_proofs dt_info new_type_names descr sorts
   3.191 +      DatatypeRepProofs.representation_proofs flat_names dt_info new_type_names descr sorts
   3.192          types_syntax constr_syntax;
   3.193  
   3.194      val (thy3, casedist_thms) =
   3.195        DatatypeAbsProofs.prove_casedist_thms new_type_names descr sorts induct thy2;
   3.196      val (thy4, reccomb_names, rec_thms) = DatatypeAbsProofs.prove_primrec_thms
   3.197 -      new_type_names descr sorts dt_info inject dist_rewrites induct thy3;
   3.198 +      flat_names new_type_names descr sorts dt_info inject dist_rewrites induct thy3;
   3.199      val (thy5, case_names, case_thms) = DatatypeAbsProofs.prove_case_thms
   3.200 -      new_type_names descr sorts reccomb_names rec_thms thy4;
   3.201 +      flat_names new_type_names descr sorts reccomb_names rec_thms thy4;
   3.202      val (thy6, distinct) = DatatypeAbsProofs.prove_distinctness_thms
   3.203 -      new_type_names descr sorts dist_rewrites case_thms thy5;
   3.204 +      flat_names new_type_names descr sorts dist_rewrites case_thms thy5;
   3.205      val (thy7, split_thms) = DatatypeAbsProofs.prove_split_thms new_type_names
   3.206        descr sorts inject dist_rewrites casedist_thms case_thms thy6;
   3.207      val (thy8, nchotomys) = DatatypeAbsProofs.prove_nchotomys new_type_names
   3.208        descr sorts casedist_thms thy7;
   3.209      val (thy9, case_congs) = DatatypeAbsProofs.prove_case_congs new_type_names
   3.210        descr sorts nchotomys case_thms thy8;
   3.211 -    val (thy10, size_thms) = DatatypeAbsProofs.prove_size_thms new_type_names
   3.212 +    val (thy10, size_thms) = DatatypeAbsProofs.prove_size_thms flat_names new_type_names
   3.213        descr sorts reccomb_names rec_thms thy9;
   3.214  
   3.215      val dt_infos = map (make_dt_info (flat descr) induct reccomb_names rec_thms)
   3.216 @@ -440,9 +447,10 @@
   3.217      val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   3.218  
   3.219      val thy11 = thy10 |>
   3.220 +      Theory.add_path (space_implode "_" new_type_names) |>
   3.221        PureThy.add_tthmss [(("simps", map Attribute.tthm_of simps), [])] |>
   3.222        put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
   3.223 -      Theory.parent_path;
   3.224 +      parent_path flat_names;
   3.225  
   3.226      val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11)
   3.227        addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
   3.228 @@ -502,11 +510,10 @@
   3.229      val _ = writeln ("Proofs for datatype(s) " ^ commas new_type_names);
   3.230  
   3.231      val (thy2, casedist_thms) = thy |>
   3.232 -      Theory.add_path (space_implode "_" new_type_names) |>
   3.233        DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induction;
   3.234      val (thy3, reccomb_names, rec_thms) = DatatypeAbsProofs.prove_primrec_thms
   3.235 -      new_type_names [descr] sorts dt_info inject distinct induction thy2;
   3.236 -    val (thy4, case_names, case_thms) = DatatypeAbsProofs.prove_case_thms
   3.237 +      false new_type_names [descr] sorts dt_info inject distinct induction thy2;
   3.238 +    val (thy4, case_names, case_thms) = DatatypeAbsProofs.prove_case_thms false
   3.239        new_type_names [descr] sorts reccomb_names rec_thms thy3;
   3.240      val (thy5, split_thms) = DatatypeAbsProofs.prove_split_thms
   3.241        new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4;
   3.242 @@ -516,7 +523,7 @@
   3.243        [descr] sorts nchotomys case_thms thy6;
   3.244      val (thy8, size_thms) =
   3.245        if exists (equal "Arith") (Sign.stamp_names_of (sign_of thy7)) then
   3.246 -        DatatypeAbsProofs.prove_size_thms new_type_names
   3.247 +        DatatypeAbsProofs.prove_size_thms false new_type_names
   3.248            [descr] sorts reccomb_names rec_thms thy7
   3.249        else (thy7, []);
   3.250  
   3.251 @@ -527,6 +534,7 @@
   3.252      val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   3.253  
   3.254      val thy9 = thy8 |>
   3.255 +      Theory.add_path (space_implode "_" new_type_names) |>
   3.256        PureThy.add_tthmss [(("simps", map Attribute.tthm_of simps), [])] |>
   3.257        put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
   3.258        Theory.parent_path;
   3.259 @@ -551,7 +559,7 @@
   3.260  
   3.261  (******************************** add datatype ********************************)
   3.262  
   3.263 -fun gen_add_datatype prep_typ new_type_names dts thy =
   3.264 +fun gen_add_datatype prep_typ flat_names new_type_names dts thy =
   3.265    let
   3.266      val _ = Theory.requires thy "Datatype" "datatype definitions";
   3.267  
   3.268 @@ -559,16 +567,17 @@
   3.269  
   3.270      val tmp_thy = thy |>
   3.271        Theory.prep_ext |>
   3.272 -      Theory.add_path (space_implode "_" new_type_names) |>
   3.273        Theory.add_types (map (fn (tvs, tname, mx, _) =>
   3.274          (tname, length tvs, mx)) dts);
   3.275  
   3.276      val sign = sign_of tmp_thy;
   3.277  
   3.278 +    val (tyvars, _, _, _)::_ = dts;
   3.279      val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
   3.280        let val full_tname = Sign.full_name sign (Syntax.type_name tname mx)
   3.281        in (case duplicates tvs of
   3.282 -            [] => ((full_tname, tvs), (tname, mx))
   3.283 +            [] => if eq_set (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
   3.284 +                  else error ("Mutually recursive datatypes must have same type parameters")
   3.285            | dups => error ("Duplicate parameter(s) for datatype " ^ full_tname ^
   3.286                " : " ^ commas dups))
   3.287        end) dts);
   3.288 @@ -578,15 +587,14 @@
   3.289  
   3.290      fun prep_dt_spec ((dts', constr_syntax, sorts, i), (tvs, tname, mx, constrs)) =
   3.291        let
   3.292 -        fun prep_constr ((constrs, constr_syntax', sorts'), (cname, mx', cargs)) =
   3.293 +        fun prep_constr ((constrs, constr_syntax', sorts'), (cname, cargs, mx')) =
   3.294            let
   3.295              val (cargs', sorts'') = foldl (prep_typ sign) (([], sorts'), cargs);
   3.296              val _ = (case foldr add_typ_tfree_names (cargs', []) \\ tvs of
   3.297                  [] => ()
   3.298                | vs => error ("Extra type variables on rhs: " ^ commas vs))
   3.299 -          in (constrs @ [((if length dts = 1 then Sign.full_name sign
   3.300 -               else Sign.full_name_path sign (Sign.base_name tname))
   3.301 -                 (Syntax.const_name cname mx'),
   3.302 +          in (constrs @ [((if flat_names then Sign.full_name sign else
   3.303 +                Sign.full_name_path sign tname) (Syntax.const_name cname mx'),
   3.304                     map (dtyp_of_typ new_dts) cargs')],
   3.305                constr_syntax' @ [(cname, mx')], sorts'')
   3.306            end handle ERROR =>
   3.307 @@ -606,14 +614,15 @@
   3.308               " in datatype " ^ tname)
   3.309        end;
   3.310  
   3.311 -    val (dts', constr_syntax, sorts, i) = foldl prep_dt_spec (([], [], [], 0), dts);
   3.312 +    val (dts', constr_syntax, sorts', i) = foldl prep_dt_spec (([], [], [], 0), dts);
   3.313      val dt_info = get_datatypes thy;
   3.314      val (descr, _) = unfold_datatypes dt_info dts' i;
   3.315      val _ = check_nonempty descr;
   3.316 +    val sorts = sorts' @ (map (rpair (Sign.defaultS sign)) (tyvars \\ map fst sorts'));
   3.317  
   3.318    in
   3.319      (if (!quick_and_dirty) then add_datatype_axm else add_datatype_def)
   3.320 -      new_type_names descr sorts types_syntax constr_syntax dt_info thy
   3.321 +      flat_names new_type_names descr sorts types_syntax constr_syntax dt_info thy
   3.322    end;
   3.323  
   3.324  val add_datatype_i = gen_add_datatype cert_typ;
     4.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Fri Oct 16 18:52:17 1998 +0200
     4.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri Oct 16 18:54:55 1998 +0200
     4.3 @@ -14,7 +14,7 @@
     4.4  
     4.5  signature DATATYPE_REP_PROOFS =
     4.6  sig
     4.7 -  val representation_proofs : DatatypeAux.datatype_info Symtab.table ->
     4.8 +  val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
     4.9      string list -> (int * (string * DatatypeAux.dtyp list *
    4.10        (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    4.11          (string * mixfix) list -> (string * mixfix) list list -> theory ->
    4.12 @@ -41,7 +41,7 @@
    4.13  
    4.14  (******************************************************************************)
    4.15  
    4.16 -fun representation_proofs (dt_info : datatype_info Symtab.table)
    4.17 +fun representation_proofs flat_names (dt_info : datatype_info Symtab.table)
    4.18        new_type_names descr sorts types_syntax constr_syntax thy =
    4.19    let
    4.20      val Univ_thy = the (get_thy "Univ" thy);
    4.21 @@ -56,13 +56,18 @@
    4.22  
    4.23      val descr' = flat descr;
    4.24  
    4.25 -    val big_rec_name = (space_implode "_" new_type_names) ^ "_rep_set";
    4.26 -    val rep_set_names = map (Sign.full_name (sign_of thy))
    4.27 +    val big_name = space_implode "_" new_type_names;
    4.28 +    val thy1 = add_path flat_names big_name thy;
    4.29 +    val big_rec_name = big_name ^ "_rep_set";
    4.30 +    val rep_set_names = map (Sign.full_name (sign_of thy1))
    4.31        (if length descr' = 1 then [big_rec_name] else
    4.32          (map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int)
    4.33            (1 upto (length descr'))));
    4.34  
    4.35 -    val leafTs = get_nonrec_types descr' sorts;
    4.36 +    val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
    4.37 +    val leafTs' = get_nonrec_types descr' sorts;
    4.38 +    val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names (leafTs', []);
    4.39 +    val leafTs = leafTs' @ (map (fn n => TFree (n, the (assoc (sorts, n)))) unneeded_vars);
    4.40      val recTs = get_rec_types descr' sorts;
    4.41      val newTs = take (length (hd descr), recTs);
    4.42      val oldTs = drop (length (hd descr), recTs);
    4.43 @@ -101,7 +106,7 @@
    4.44  
    4.45      (************** generate introduction rules for representing set **********)
    4.46  
    4.47 -    val _ = writeln "Constructing representing sets...";
    4.48 +    val _ = message "Constructing representing sets...";
    4.49  
    4.50      (* make introduction rule for a single constructor *)
    4.51  
    4.52 @@ -130,18 +135,19 @@
    4.53          ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names));
    4.54  
    4.55      val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =
    4.56 -      InductivePackage.add_inductive_i false true big_rec_name false true false
    4.57 -        consts intr_ts [] [] thy;
    4.58 +      setmp InductivePackage.quiet_mode (!quiet_mode)
    4.59 +        (InductivePackage.add_inductive_i false true big_rec_name false true false
    4.60 +           consts intr_ts [] []) thy1;
    4.61  
    4.62      (********************************* typedef ********************************)
    4.63  
    4.64 -    val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
    4.65 +    (* FIXME: quiet_mode flag for TypedefPackage and BREADTH_FIRST *)
    4.66  
    4.67 -    val thy3 = foldl (fn (thy, ((((name, mx), tvs), c), name')) =>
    4.68 +    val thy3 = add_path flat_names big_name (foldl (fn (thy, ((((name, mx), tvs), c), name')) =>
    4.69        TypedefPackage.add_typedef_i_no_def name' (name, tvs, mx) c [] []
    4.70          (Some (BREADTH_FIRST (has_fewer_prems 1) (resolve_tac rep_intrs 1))) thy)
    4.71 -          (thy2, types_syntax ~~ tyvars ~~ (take (length newTs, consts)) ~~
    4.72 -            new_type_names);
    4.73 +          (parent_path flat_names thy2, types_syntax ~~ tyvars ~~ (take (length newTs, consts)) ~~
    4.74 +            new_type_names));
    4.75  
    4.76      (*********************** definition of constructors ***********************)
    4.77  
    4.78 @@ -149,7 +155,8 @@
    4.79      val rep_names = map (curry op ^ "Rep_") new_type_names;
    4.80      val rep_names' = map (fn i => big_rep_name ^ (string_of_int i))
    4.81        (1 upto (length (flat (tl descr))));
    4.82 -    val all_rep_names = map (Sign.full_name (sign_of thy3)) (rep_names @ rep_names');
    4.83 +    val all_rep_names = map (Sign.intern_const (sign_of thy3)) rep_names @
    4.84 +      map (Sign.full_name (sign_of thy3)) rep_names';
    4.85  
    4.86      (* isomorphism declarations *)
    4.87  
    4.88 @@ -198,20 +205,19 @@
    4.89          val cong' = cterm_instantiate [(cterm_of sg cong_f, rep_const)] arg_cong;
    4.90          val dist = cterm_instantiate [(cterm_of sg distinct_f, rep_const)] distinct_lemma;
    4.91          val (thy', defs', eqns', _) = foldl ((make_constr_def tname T) (length constrs))
    4.92 -          ((if length newTs = 1 then thy else Theory.add_path tname thy, defs, [], 1),
    4.93 -            constrs ~~ constr_syntax)
    4.94 +          ((add_path flat_names tname thy, defs, [], 1), constrs ~~ constr_syntax)
    4.95        in
    4.96 -        (if length newTs = 1 then thy' else Theory.parent_path thy', defs', eqns @ [eqns'],
    4.97 +        (parent_path flat_names thy', defs', eqns @ [eqns'],
    4.98            rep_congs @ [cong'], dist_lemmas @ [dist])
    4.99        end;
   4.100  
   4.101      val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = foldl dt_constr_defs
   4.102 -      ((Theory.add_consts_i iso_decls thy3, [], [], [], []),
   4.103 +      ((thy3 |> Theory.add_consts_i iso_decls |> parent_path flat_names, [], [], [], []),
   4.104          hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax);
   4.105  
   4.106      (*********** isomorphisms for new types (introduced by typedef) ***********)
   4.107  
   4.108 -    val _ = writeln "Proving isomorphism properties...";
   4.109 +    val _ = message "Proving isomorphism properties...";
   4.110  
   4.111      (* get axioms from theory *)
   4.112  
   4.113 @@ -323,7 +329,8 @@
   4.114  
   4.115        in (thy', char_thms' @ char_thms) end;
   4.116  
   4.117 -    val (thy5, iso_char_thms) = foldr make_iso_defs (tl descr, (thy4, []));
   4.118 +    val (thy5, iso_char_thms) = foldr make_iso_defs
   4.119 +      (tl descr, (add_path flat_names big_name thy4, []));
   4.120  
   4.121      (* prove isomorphism properties *)
   4.122  
   4.123 @@ -423,7 +430,7 @@
   4.124  
   4.125      (******************* freeness theorems for constructors *******************)
   4.126  
   4.127 -    val _ = writeln "Proving freeness of constructors...";
   4.128 +    val _ = message "Proving freeness of constructors...";
   4.129  
   4.130      (* prove theorem  Rep_i (Constr_j ...) = Inj_j ...  *)
   4.131      
   4.132 @@ -470,11 +477,12 @@
   4.133      val constr_inject = map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts)
   4.134        ((DatatypeProp.make_injs descr sorts) ~~ constr_rep_thms);
   4.135  
   4.136 -    val thy6 = store_thmss "inject" new_type_names constr_inject thy5;
   4.137 +    val thy6 = store_thmss "inject" new_type_names
   4.138 +      constr_inject (parent_path flat_names thy5);
   4.139  
   4.140      (*************************** induction theorem ****************************)
   4.141  
   4.142 -    val _ = writeln "Proving induction rule for datatypes...";
   4.143 +    val _ = message "Proving induction rule for datatypes...";
   4.144  
   4.145      val Rep_inverse_thms = (map (fn (_, iso, _) => iso RS subst) newT_iso_axms) @
   4.146        (map (fn r => r RS inv_f_f RS subst) (drop (length newTs, iso_inj_thms)));
   4.147 @@ -526,7 +534,10 @@
   4.148              DEPTH_SOLVE_1 (ares_tac [prem] 1)]))
   4.149                (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
   4.150  
   4.151 -    val thy7 = PureThy.add_tthms [(("induct", Attribute.tthm_of dt_induct), [])] thy6;
   4.152 +    val thy7 = thy6 |>
   4.153 +      Theory.add_path big_name |>
   4.154 +      PureThy.add_tthms [(("induct", Attribute.tthm_of dt_induct), [])] |>
   4.155 +      Theory.parent_path;
   4.156  
   4.157    in (thy7, constr_inject, dist_rewrites, dt_induct)
   4.158    end;