- Changed structure of name spaces
- Proofs for datatypes with unneeded parameters are working now
- added additional parameter flat_names
- added quiet_mode flag
--- a/src/HOL/Tools/datatype_abs_proofs.ML Fri Oct 16 18:52:17 1998 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Fri Oct 16 18:54:55 1998 +0200
@@ -22,21 +22,21 @@
val prove_casedist_thms : string list -> (int * (string * DatatypeAux.dtyp list *
(string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
thm -> theory -> theory * thm list
- val prove_primrec_thms : string list -> (int * (string * DatatypeAux.dtyp list *
+ val prove_primrec_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
(string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
DatatypeAux.datatype_info Symtab.table -> thm list list -> thm list list ->
thm -> theory -> theory * string list * thm list
- val prove_case_thms : string list -> (int * (string * DatatypeAux.dtyp list *
+ val prove_case_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
(string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
string list -> thm list -> theory -> theory * string list * thm list list
- val prove_distinctness_thms : string list -> (int * (string * DatatypeAux.dtyp list *
+ val prove_distinctness_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
(string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
thm list list -> thm list list -> theory -> theory * thm list list
val prove_split_thms : string list -> (int * (string * DatatypeAux.dtyp list *
(string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
thm list list -> thm list list -> thm list -> thm list list -> theory ->
theory * (thm * thm) list
- val prove_size_thms : string list -> (int * (string * DatatypeAux.dtyp list *
+ val prove_size_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
(string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
string list -> thm list -> theory -> theory * thm list
val prove_nchotomys : string list -> (int * (string * DatatypeAux.dtyp list *
@@ -60,7 +60,7 @@
fun prove_casedist_thms new_type_names descr sorts induct thy =
let
- val _ = writeln "Proving case distinction theorems...";
+ val _ = message "Proving case distinction theorems...";
val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
@@ -96,10 +96,13 @@
(*************************** primrec combinators ******************************)
-fun prove_primrec_thms new_type_names descr sorts
+fun prove_primrec_thms flat_names new_type_names descr sorts
(dt_info : datatype_info Symtab.table) constr_inject dist_rewrites induct thy =
let
- val _ = writeln "Constructing primrec combinators...";
+ val _ = message "Constructing primrec combinators...";
+
+ val big_name = space_implode "_" new_type_names;
+ val thy0 = add_path flat_names big_name thy;
val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
@@ -108,8 +111,8 @@
val induct_Ps = map head_of (dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
- val big_rec_name' = (space_implode "_" new_type_names) ^ "_rec_set";
- val rec_set_names = map (Sign.full_name (sign_of thy))
+ val big_rec_name' = big_name ^ "_rec_set";
+ val rec_set_names = map (Sign.full_name (sign_of thy0))
(if length descr' = 1 then [big_rec_name'] else
(map ((curry (op ^) (big_rec_name' ^ "_")) o string_of_int)
(1 upto (length descr'))));
@@ -165,12 +168,13 @@
(([], 0), descr' ~~ recTs ~~ rec_sets);
val (thy1, {intrs = rec_intrs, elims = rec_elims, ...}) =
- InductivePackage.add_inductive_i false true big_rec_name' false false true
- rec_sets rec_intr_ts [] [] thy;
+ setmp InductivePackage.quiet_mode (!quiet_mode)
+ (InductivePackage.add_inductive_i false true big_rec_name' false false true
+ rec_sets rec_intr_ts [] []) thy0;
(* prove uniqueness and termination of primrec combinators *)
- val _ = writeln "Proving termination and uniqueness of primrec functions...";
+ val _ = message "Proving termination and uniqueness of primrec functions...";
fun mk_unique_tac ((tac, intrs), ((((i, (tname, _, constrs)), elim), T), T')) =
let
@@ -252,13 +256,14 @@
(comb $ Free ("x", T),
Const ("Eps", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
HOLogic.mk_mem (HOLogic.mk_prod (Free ("x", T), Free ("y", T')), set)))))
- (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts));
+ (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)) |>
+ parent_path flat_names;
val reccomb_defs = map ((get_def thy2) o Sign.base_name) reccomb_names;
(* prove characteristic equations for primrec combinators *)
- val _ = writeln "Proving characteristic theorems for primrec combinators..."
+ val _ = message "Proving characteristic theorems for primrec combinators..."
val rec_thms = map (fn t => prove_goalw_cterm reccomb_defs
(cterm_of (sign_of thy2) t) (fn _ =>
@@ -269,15 +274,19 @@
(DatatypeProp.make_primrecs new_type_names descr sorts thy2)
in
- (PureThy.add_tthmss [(("recs", map Attribute.tthm_of rec_thms), [])] thy2,
+ (thy2 |> Theory.add_path (space_implode "_" new_type_names) |>
+ PureThy.add_tthmss [(("recs", map Attribute.tthm_of rec_thms), [])] |>
+ Theory.parent_path,
reccomb_names, rec_thms)
end;
(***************************** case combinators *******************************)
-fun prove_case_thms new_type_names descr sorts reccomb_names primrec_thms thy =
+fun prove_case_thms flat_names new_type_names descr sorts reccomb_names primrec_thms thy =
let
- val _ = writeln "Proving characteristic theorems for case combinators...";
+ val _ = message "Proving characteristic theorems for case combinators...";
+
+ val thy1 = add_path flat_names (space_implode "_" new_type_names) thy;
val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
@@ -293,7 +302,7 @@
end) constrs) descr';
val case_names = map (fn s =>
- Sign.full_name (sign_of thy) (s ^ "_case")) new_type_names;
+ Sign.full_name (sign_of thy1) (s ^ "_case")) new_type_names;
(* define case combinators via primrec combinators *)
@@ -325,7 +334,7 @@
Theory.add_consts_i [decl] |> Theory.add_defs_i [def];
in (defs @ [get_def thy' (Sign.base_name name)], thy')
- end) (([], thy), (hd descr) ~~ newTs ~~ case_names ~~
+ end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~
(take (length newTs, reccomb_names)));
val case_thms = map (map (fn t => prove_goalw_cterm (case_defs @
@@ -333,16 +342,20 @@
(fn _ => [rtac refl 1])))
(DatatypeProp.make_cases new_type_names descr sorts thy2);
- val thy3 = Theory.add_trrules_i
- (DatatypeProp.make_case_trrules new_type_names descr) thy2
+ val thy3 = thy2 |> Theory.add_trrules_i
+ (DatatypeProp.make_case_trrules new_type_names descr) |>
+ parent_path flat_names;
- in (store_thmss "cases" new_type_names case_thms thy3, case_names, case_thms)
+ in
+ (store_thmss "cases" new_type_names case_thms thy3, case_names, case_thms)
end;
(************************ distinctness of constructors ************************)
-fun prove_distinctness_thms new_type_names descr sorts dist_rewrites case_thms thy =
+fun prove_distinctness_thms flat_names new_type_names descr sorts dist_rewrites case_thms thy =
let
+ val thy1 = add_path flat_names (space_implode "_" new_type_names) thy;
+
val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
val newTs = take (length (hd descr), recTs);
@@ -375,7 +388,7 @@
in (thy', ord_defs @ [def]) end;
val (thy2, ord_defs) =
- foldl define_ord ((thy, []), (hd descr) ~~ newTs ~~ new_type_names);
+ foldl define_ord ((thy1, []), (hd descr) ~~ newTs ~~ new_type_names);
(**** number of constructors < dtK ****)
@@ -406,7 +419,10 @@
end) ((hd descr) ~~ (DatatypeProp.make_distincts new_type_names
descr sorts thy2) ~~ dist_rewrites ~~ case_thms)
- in (store_thmss "distinct" new_type_names distinct_thms thy2, distinct_thms)
+ in
+ (thy2 |> parent_path flat_names |>
+ store_thmss "distinct" new_type_names distinct_thms,
+ distinct_thms)
end;
(******************************* case splitting *******************************)
@@ -414,7 +430,7 @@
fun prove_split_thms new_type_names descr sorts constr_inject dist_rewrites
casedist_thms case_thms thy =
let
- val _ = writeln "Proving equations for case splitting...";
+ val _ = message "Proving equations for case splitting...";
val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
@@ -448,17 +464,20 @@
(******************************* size functions *******************************)
-fun prove_size_thms new_type_names descr sorts reccomb_names primrec_thms thy =
+fun prove_size_thms flat_names new_type_names descr sorts reccomb_names primrec_thms thy =
let
- val _ = writeln "Proving equations for size function...";
+ val _ = message "Proving equations for size function...";
+
+ val big_name = space_implode "_" new_type_names;
+ val thy1 = add_path flat_names big_name thy;
val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
val big_size_name = space_implode "_" new_type_names ^ "_size";
- val size_name = Sign.intern_const (sign_of (the (get_thy "Arith" thy))) "size";
+ val size_name = Sign.intern_const (sign_of (the (get_thy "Arith" thy1))) "size";
val size_names = replicate (length (hd descr)) size_name @
- map (Sign.full_name (sign_of thy))
+ map (Sign.full_name (sign_of thy1))
(if length (flat (tl descr)) = 1 then [big_size_name] else
map (fn i => big_size_name ^ "_" ^ string_of_int i)
(1 upto length (flat (tl descr))));
@@ -480,14 +499,15 @@
val fs = flat (map (fn (_, (_, _, constrs)) => map make_sizefun constrs) descr');
val fTs = map fastype_of fs;
- val thy' = thy |>
+ val thy' = thy1 |>
Theory.add_consts_i (map (fn (s, T) =>
(Sign.base_name s, T --> HOLogic.natT, NoSyn))
(drop (length (hd descr), size_names ~~ recTs))) |>
Theory.add_defs_i (map (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))))
- (size_names ~~ recTs ~~ def_names ~~ reccomb_names));
+ (size_names ~~ recTs ~~ def_names ~~ reccomb_names)) |>
+ parent_path flat_names;
val size_def_thms = map (get_axiom thy') def_names;
val rewrites = size_def_thms @ map mk_meta_eq primrec_thms;
@@ -497,7 +517,9 @@
(DatatypeProp.make_size new_type_names descr sorts thy')
in
- (PureThy.add_tthmss [(("size", map Attribute.tthm_of size_thms), [])] thy',
+ (thy' |> Theory.add_path big_name |>
+ PureThy.add_tthmss [(("size", map Attribute.tthm_of size_thms), [])] |>
+ Theory.parent_path,
size_thms)
end;
@@ -505,7 +527,7 @@
fun prove_nchotomys new_type_names descr sorts casedist_thms thy =
let
- val _ = writeln "Proving additional theorems for TFL...";
+ val _ = message "Proving additional theorems for TFL...";
fun prove_nchotomy (t, exhaustion) =
let
--- a/src/HOL/Tools/datatype_aux.ML Fri Oct 16 18:52:17 1998 +0200
+++ b/src/HOL/Tools/datatype_aux.ML Fri Oct 16 18:54:55 1998 +0200
@@ -8,10 +8,16 @@
signature DATATYPE_AUX =
sig
+ val quiet_mode : bool ref
+ val message : string -> unit
+
val foldl1 : ('a * 'a -> 'a) -> 'a list -> 'a
val get_thy : string -> theory -> theory option
+ val add_path : bool -> string -> theory -> theory
+ val parent_path : bool -> theory -> theory
+
val store_thmss : string -> string list -> thm list list -> theory -> theory
val store_thms : string -> string list -> thm list -> theory -> theory
@@ -55,27 +61,33 @@
structure DatatypeAux : DATATYPE_AUX =
struct
+val quiet_mode = ref false;
+fun message s = if !quiet_mode then () else writeln s;
+
(* FIXME: move to library ? *)
fun foldl1 f (x::xs) = foldl f (x, xs);
fun get_thy name thy = find_first
(equal name o Sign.name_of o sign_of) (ancestors_of thy);
+fun add_path flat_names s = if flat_names then I else Theory.add_path s;
+fun parent_path flat_names = if flat_names then I else Theory.parent_path;
+
(* store theorems in theory *)
fun store_thmss label tnames thmss thy =
foldr (fn ((tname, thms), thy') => thy' |>
- (if length tnames = 1 then I else Theory.add_path tname) |>
+ Theory.add_path tname |>
PureThy.add_tthmss [((label, map Attribute.tthm_of thms), [])] |>
- (if length tnames = 1 then I else Theory.parent_path))
- (tnames ~~ thmss, thy);
+ Theory.parent_path)
+ (tnames ~~ thmss, thy);
fun store_thms label tnames thms thy =
foldr (fn ((tname, thm), thy') => thy' |>
- (if length tnames = 1 then I else Theory.add_path tname) |>
+ Theory.add_path tname |>
PureThy.add_tthms [((label, Attribute.tthm_of thm), [])] |>
- (if length tnames = 1 then I else Theory.parent_path))
- (tnames ~~ thms, thy);
+ Theory.parent_path)
+ (tnames ~~ thms, thy);
(* split theorem thm_1 & ... & thm_n into n theorems *)
--- a/src/HOL/Tools/datatype_package.ML Fri Oct 16 18:52:17 1998 +0200
+++ b/src/HOL/Tools/datatype_package.ML Fri Oct 16 18:54:55 1998 +0200
@@ -8,8 +8,9 @@
signature DATATYPE_PACKAGE =
sig
- val add_datatype : string list -> (string list * bstring * mixfix *
- (bstring * mixfix * string list) list) list -> theory -> theory *
+ val quiet_mode : bool ref
+ val add_datatype : bool -> string list -> (string list * bstring * mixfix *
+ (bstring * string list * mixfix) list) list -> theory -> theory *
{distinct : thm list list,
inject : thm list list,
exhaustion : thm list,
@@ -19,8 +20,8 @@
induction : thm,
size : thm list,
simps : thm list}
- val add_datatype_i : string list -> (string list * bstring * mixfix *
- (bstring * mixfix * typ list) list) list -> theory -> theory *
+ val add_datatype_i : bool -> string list -> (string list * bstring * mixfix *
+ (bstring * typ list * mixfix) list) list -> theory -> theory *
{distinct : thm list list,
inject : thm list list,
exhaustion : thm list,
@@ -57,6 +58,8 @@
open DatatypeAux;
+val quiet_mode = quiet_mode;
+
(* data kind 'HOL/datatypes' *)
structure DatatypesArgs =
@@ -232,30 +235,30 @@
foldr (fn ((tname, t), (thy', axs)) =>
let
val thy'' = thy' |>
- (if length tnames = 1 then I else Theory.add_path tname) |>
+ Theory.add_path tname |>
PureThy.add_axioms_i [((label, t), [])];
val ax = get_axiom thy'' label
- in (if length tnames = 1 then thy'' else Theory.parent_path thy'', ax::axs)
+ in (Theory.parent_path thy'', ax::axs)
end) (tnames ~~ ts, (thy, []));
fun add_and_get_axiomss label tnames tss thy =
foldr (fn ((tname, ts), (thy', axss)) =>
let
val thy'' = thy' |>
- (if length tnames = 1 then I else Theory.add_path tname) |>
+ Theory.add_path tname |>
PureThy.add_axiomss_i [((label, ts), [])];
val axs = PureThy.get_thms thy'' label
- in (if length tnames = 1 then thy'' else Theory.parent_path thy'', axs::axss)
+ in (Theory.parent_path thy'', axs::axss)
end) (tnames ~~ tss, (thy, []));
-fun add_datatype_axm new_type_names descr sorts types_syntax constr_syntax dt_info thy =
+fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info thy =
let
val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
val used = foldr add_typ_tfree_names (recTs, []);
val newTs = take (length (hd descr), recTs);
- val _ = writeln ("Adding axioms for datatype(s) " ^ commas new_type_names);
+ val _ = message ("Adding axioms for datatype(s) " ^ commas new_type_names);
(**** declare new types and constants ****)
@@ -298,8 +301,6 @@
val thy2 = thy |>
- Theory.add_path (space_implode "_" new_type_names) |>
-
(** new types **)
curry (foldr (fn (((name, mx), tvs), thy') => thy' |>
@@ -309,16 +310,7 @@
replicate (length tvs) HOLogic.termS, HOLogic.termS)]))
(types_syntax ~~ tyvars) |>
- (** constructors **)
-
- curry (foldr (fn (((((_, (_, _, constrs)), T), tname),
- constr_syntax'), thy') => thy' |>
- (if length newTs = 1 then I else Theory.add_path tname) |>
- Theory.add_consts_i (map (fn ((_, cargs), (cname, mx)) =>
- (cname, map (typ_of_dtyp descr' sorts) cargs ---> T, mx))
- (constrs ~~ constr_syntax')) |>
- (if length newTs = 1 then I else Theory.parent_path)))
- (hd descr ~~ newTs ~~ new_type_names ~~ constr_syntax) |>
+ add_path flat_names (space_implode "_" new_type_names) |>
(** primrec combinators **)
@@ -345,22 +337,40 @@
Theory.add_consts_i (map (fn (s, T) =>
(Sign.base_name s, T --> HOLogic.natT, NoSyn))
- (size_names ~~ drop (length (hd descr), recTs)));
+ (size_names ~~ drop (length (hd descr), recTs))) |>
+
+ (** constructors **)
+
+ parent_path flat_names |>
+ curry (foldr (fn (((((_, (_, _, constrs)), T), tname),
+ constr_syntax'), thy') => thy' |>
+ add_path flat_names tname |>
+ Theory.add_consts_i (map (fn ((_, cargs), (cname, mx)) =>
+ (cname, map (typ_of_dtyp descr' sorts) cargs ---> T, mx))
+ (constrs ~~ constr_syntax')) |>
+ parent_path flat_names))
+ (hd descr ~~ newTs ~~ new_type_names ~~ constr_syntax);
(**** introduction of axioms ****)
+ val rec_axs = DatatypeProp.make_primrecs new_type_names descr sorts thy2;
+ val size_axs = DatatypeProp.make_size new_type_names descr sorts thy2;
+
val (thy3, inject) = thy2 |>
+ Theory.add_path (space_implode "_" new_type_names) |>
PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts), [])] |>
+ PureThy.add_axiomss_i [(("recs", rec_axs), [])] |>
+ PureThy.add_axiomss_i [(("size", size_axs), [])] |>
+ Theory.parent_path |>
add_and_get_axiomss "inject" new_type_names
(DatatypeProp.make_injs descr sorts);
+ val induct = get_axiom thy3 "induct";
+ val rec_thms = get_thms thy3 "recs";
+ val size_thms = get_thms thy3 "size";
val (thy4, distinct) = add_and_get_axiomss "distinct" new_type_names
(DatatypeProp.make_distincts new_type_names descr sorts thy3) thy3;
- val induct = get_axiom thy4 "induct";
-
val (thy5, exhaustion) = add_and_get_axioms "exhaust" new_type_names
- (DatatypeProp.make_casedists descr sorts) (PureThy.add_axiomss_i [(("recs",
- DatatypeProp.make_primrecs new_type_names descr sorts thy4), [])] thy4);
- val rec_thms = get_thms thy5 "recs";
+ (DatatypeProp.make_casedists descr sorts) thy4;
val (thy6, case_thms) = add_and_get_axiomss "cases" new_type_names
(DatatypeProp.make_cases new_type_names descr sorts thy5) thy5;
val (split_ts, split_asm_ts) = ListPair.unzip
@@ -372,9 +382,6 @@
(DatatypeProp.make_nchotomys descr sorts) thy8;
val (thy10, case_congs) = add_and_get_axioms "case_cong" new_type_names
(DatatypeProp.make_case_congs new_type_names descr sorts thy9) thy9;
- val thy11 = PureThy.add_axiomss_i [(("size",
- DatatypeProp.make_size new_type_names descr sorts thy10), [])] thy10;
- val size_thms = get_thms thy11 "size";
val dt_infos = map (make_dt_info descr' induct reccomb_names rec_thms)
((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
@@ -382,17 +389,18 @@
val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
- val thy12 = thy11 |>
+ val thy11 = thy10 |>
+ Theory.add_path (space_implode "_" new_type_names) |>
PureThy.add_tthmss [(("simps", map Attribute.tthm_of simps), [])] |>
put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
Theory.parent_path;
- val _ = store_clasimp thy12 ((claset_of thy12, simpset_of thy12)
+ val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11)
addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
addIffs flat inject addDistinct (distinct, hd descr));
in
- (thy12,
+ (thy11,
{distinct = distinct,
inject = inject,
exhaustion = exhaustion,
@@ -407,30 +415,29 @@
(******************* definitional introduction of datatypes *******************)
-fun add_datatype_def new_type_names descr sorts types_syntax constr_syntax dt_info thy =
+fun add_datatype_def flat_names new_type_names descr sorts types_syntax constr_syntax dt_info thy =
let
- val _ = writeln ("Proofs for datatype(s) " ^ commas new_type_names);
+ val _ = message ("Proofs for datatype(s) " ^ commas new_type_names);
val (thy2, inject, dist_rewrites, induct) = thy |>
- Theory.add_path (space_implode "_" new_type_names) |>
- DatatypeRepProofs.representation_proofs dt_info new_type_names descr sorts
+ DatatypeRepProofs.representation_proofs flat_names dt_info new_type_names descr sorts
types_syntax constr_syntax;
val (thy3, casedist_thms) =
DatatypeAbsProofs.prove_casedist_thms new_type_names descr sorts induct thy2;
val (thy4, reccomb_names, rec_thms) = DatatypeAbsProofs.prove_primrec_thms
- new_type_names descr sorts dt_info inject dist_rewrites induct thy3;
+ flat_names new_type_names descr sorts dt_info inject dist_rewrites induct thy3;
val (thy5, case_names, case_thms) = DatatypeAbsProofs.prove_case_thms
- new_type_names descr sorts reccomb_names rec_thms thy4;
+ flat_names new_type_names descr sorts reccomb_names rec_thms thy4;
val (thy6, distinct) = DatatypeAbsProofs.prove_distinctness_thms
- new_type_names descr sorts dist_rewrites case_thms thy5;
+ flat_names new_type_names descr sorts dist_rewrites case_thms thy5;
val (thy7, split_thms) = DatatypeAbsProofs.prove_split_thms new_type_names
descr sorts inject dist_rewrites casedist_thms case_thms thy6;
val (thy8, nchotomys) = DatatypeAbsProofs.prove_nchotomys new_type_names
descr sorts casedist_thms thy7;
val (thy9, case_congs) = DatatypeAbsProofs.prove_case_congs new_type_names
descr sorts nchotomys case_thms thy8;
- val (thy10, size_thms) = DatatypeAbsProofs.prove_size_thms new_type_names
+ val (thy10, size_thms) = DatatypeAbsProofs.prove_size_thms flat_names new_type_names
descr sorts reccomb_names rec_thms thy9;
val dt_infos = map (make_dt_info (flat descr) induct reccomb_names rec_thms)
@@ -440,9 +447,10 @@
val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
val thy11 = thy10 |>
+ Theory.add_path (space_implode "_" new_type_names) |>
PureThy.add_tthmss [(("simps", map Attribute.tthm_of simps), [])] |>
put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
- Theory.parent_path;
+ parent_path flat_names;
val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11)
addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
@@ -502,11 +510,10 @@
val _ = writeln ("Proofs for datatype(s) " ^ commas new_type_names);
val (thy2, casedist_thms) = thy |>
- Theory.add_path (space_implode "_" new_type_names) |>
DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induction;
val (thy3, reccomb_names, rec_thms) = DatatypeAbsProofs.prove_primrec_thms
- new_type_names [descr] sorts dt_info inject distinct induction thy2;
- val (thy4, case_names, case_thms) = DatatypeAbsProofs.prove_case_thms
+ false new_type_names [descr] sorts dt_info inject distinct induction thy2;
+ val (thy4, case_names, case_thms) = DatatypeAbsProofs.prove_case_thms false
new_type_names [descr] sorts reccomb_names rec_thms thy3;
val (thy5, split_thms) = DatatypeAbsProofs.prove_split_thms
new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4;
@@ -516,7 +523,7 @@
[descr] sorts nchotomys case_thms thy6;
val (thy8, size_thms) =
if exists (equal "Arith") (Sign.stamp_names_of (sign_of thy7)) then
- DatatypeAbsProofs.prove_size_thms new_type_names
+ DatatypeAbsProofs.prove_size_thms false new_type_names
[descr] sorts reccomb_names rec_thms thy7
else (thy7, []);
@@ -527,6 +534,7 @@
val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
val thy9 = thy8 |>
+ Theory.add_path (space_implode "_" new_type_names) |>
PureThy.add_tthmss [(("simps", map Attribute.tthm_of simps), [])] |>
put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
Theory.parent_path;
@@ -551,7 +559,7 @@
(******************************** add datatype ********************************)
-fun gen_add_datatype prep_typ new_type_names dts thy =
+fun gen_add_datatype prep_typ flat_names new_type_names dts thy =
let
val _ = Theory.requires thy "Datatype" "datatype definitions";
@@ -559,16 +567,17 @@
val tmp_thy = thy |>
Theory.prep_ext |>
- Theory.add_path (space_implode "_" new_type_names) |>
Theory.add_types (map (fn (tvs, tname, mx, _) =>
(tname, length tvs, mx)) dts);
val sign = sign_of tmp_thy;
+ val (tyvars, _, _, _)::_ = dts;
val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
let val full_tname = Sign.full_name sign (Syntax.type_name tname mx)
in (case duplicates tvs of
- [] => ((full_tname, tvs), (tname, mx))
+ [] => if eq_set (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
+ else error ("Mutually recursive datatypes must have same type parameters")
| dups => error ("Duplicate parameter(s) for datatype " ^ full_tname ^
" : " ^ commas dups))
end) dts);
@@ -578,15 +587,14 @@
fun prep_dt_spec ((dts', constr_syntax, sorts, i), (tvs, tname, mx, constrs)) =
let
- fun prep_constr ((constrs, constr_syntax', sorts'), (cname, mx', cargs)) =
+ fun prep_constr ((constrs, constr_syntax', sorts'), (cname, cargs, mx')) =
let
val (cargs', sorts'') = foldl (prep_typ sign) (([], sorts'), cargs);
val _ = (case foldr add_typ_tfree_names (cargs', []) \\ tvs of
[] => ()
| vs => error ("Extra type variables on rhs: " ^ commas vs))
- in (constrs @ [((if length dts = 1 then Sign.full_name sign
- else Sign.full_name_path sign (Sign.base_name tname))
- (Syntax.const_name cname mx'),
+ in (constrs @ [((if flat_names then Sign.full_name sign else
+ Sign.full_name_path sign tname) (Syntax.const_name cname mx'),
map (dtyp_of_typ new_dts) cargs')],
constr_syntax' @ [(cname, mx')], sorts'')
end handle ERROR =>
@@ -606,14 +614,15 @@
" in datatype " ^ tname)
end;
- val (dts', constr_syntax, sorts, i) = foldl prep_dt_spec (([], [], [], 0), dts);
+ val (dts', constr_syntax, sorts', i) = foldl prep_dt_spec (([], [], [], 0), dts);
val dt_info = get_datatypes thy;
val (descr, _) = unfold_datatypes dt_info dts' i;
val _ = check_nonempty descr;
+ val sorts = sorts' @ (map (rpair (Sign.defaultS sign)) (tyvars \\ map fst sorts'));
in
(if (!quick_and_dirty) then add_datatype_axm else add_datatype_def)
- new_type_names descr sorts types_syntax constr_syntax dt_info thy
+ flat_names new_type_names descr sorts types_syntax constr_syntax dt_info thy
end;
val add_datatype_i = gen_add_datatype cert_typ;
--- a/src/HOL/Tools/datatype_rep_proofs.ML Fri Oct 16 18:52:17 1998 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Fri Oct 16 18:54:55 1998 +0200
@@ -14,7 +14,7 @@
signature DATATYPE_REP_PROOFS =
sig
- val representation_proofs : DatatypeAux.datatype_info Symtab.table ->
+ val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
string list -> (int * (string * DatatypeAux.dtyp list *
(string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
(string * mixfix) list -> (string * mixfix) list list -> theory ->
@@ -41,7 +41,7 @@
(******************************************************************************)
-fun representation_proofs (dt_info : datatype_info Symtab.table)
+fun representation_proofs flat_names (dt_info : datatype_info Symtab.table)
new_type_names descr sorts types_syntax constr_syntax thy =
let
val Univ_thy = the (get_thy "Univ" thy);
@@ -56,13 +56,18 @@
val descr' = flat descr;
- val big_rec_name = (space_implode "_" new_type_names) ^ "_rep_set";
- val rep_set_names = map (Sign.full_name (sign_of thy))
+ val big_name = space_implode "_" new_type_names;
+ val thy1 = add_path flat_names big_name thy;
+ val big_rec_name = big_name ^ "_rep_set";
+ val rep_set_names = map (Sign.full_name (sign_of thy1))
(if length descr' = 1 then [big_rec_name] else
(map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int)
(1 upto (length descr'))));
- val leafTs = get_nonrec_types descr' sorts;
+ val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
+ val leafTs' = get_nonrec_types descr' sorts;
+ val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names (leafTs', []);
+ val leafTs = leafTs' @ (map (fn n => TFree (n, the (assoc (sorts, n)))) unneeded_vars);
val recTs = get_rec_types descr' sorts;
val newTs = take (length (hd descr), recTs);
val oldTs = drop (length (hd descr), recTs);
@@ -101,7 +106,7 @@
(************** generate introduction rules for representing set **********)
- val _ = writeln "Constructing representing sets...";
+ val _ = message "Constructing representing sets...";
(* make introduction rule for a single constructor *)
@@ -130,18 +135,19 @@
((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names));
val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =
- InductivePackage.add_inductive_i false true big_rec_name false true false
- consts intr_ts [] [] thy;
+ setmp InductivePackage.quiet_mode (!quiet_mode)
+ (InductivePackage.add_inductive_i false true big_rec_name false true false
+ consts intr_ts [] []) thy1;
(********************************* typedef ********************************)
- val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
+ (* FIXME: quiet_mode flag for TypedefPackage and BREADTH_FIRST *)
- val thy3 = foldl (fn (thy, ((((name, mx), tvs), c), name')) =>
+ val thy3 = add_path flat_names big_name (foldl (fn (thy, ((((name, mx), tvs), c), name')) =>
TypedefPackage.add_typedef_i_no_def name' (name, tvs, mx) c [] []
(Some (BREADTH_FIRST (has_fewer_prems 1) (resolve_tac rep_intrs 1))) thy)
- (thy2, types_syntax ~~ tyvars ~~ (take (length newTs, consts)) ~~
- new_type_names);
+ (parent_path flat_names thy2, types_syntax ~~ tyvars ~~ (take (length newTs, consts)) ~~
+ new_type_names));
(*********************** definition of constructors ***********************)
@@ -149,7 +155,8 @@
val rep_names = map (curry op ^ "Rep_") new_type_names;
val rep_names' = map (fn i => big_rep_name ^ (string_of_int i))
(1 upto (length (flat (tl descr))));
- val all_rep_names = map (Sign.full_name (sign_of thy3)) (rep_names @ rep_names');
+ val all_rep_names = map (Sign.intern_const (sign_of thy3)) rep_names @
+ map (Sign.full_name (sign_of thy3)) rep_names';
(* isomorphism declarations *)
@@ -198,20 +205,19 @@
val cong' = cterm_instantiate [(cterm_of sg cong_f, rep_const)] arg_cong;
val dist = cterm_instantiate [(cterm_of sg distinct_f, rep_const)] distinct_lemma;
val (thy', defs', eqns', _) = foldl ((make_constr_def tname T) (length constrs))
- ((if length newTs = 1 then thy else Theory.add_path tname thy, defs, [], 1),
- constrs ~~ constr_syntax)
+ ((add_path flat_names tname thy, defs, [], 1), constrs ~~ constr_syntax)
in
- (if length newTs = 1 then thy' else Theory.parent_path thy', defs', eqns @ [eqns'],
+ (parent_path flat_names thy', defs', eqns @ [eqns'],
rep_congs @ [cong'], dist_lemmas @ [dist])
end;
val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = foldl dt_constr_defs
- ((Theory.add_consts_i iso_decls thy3, [], [], [], []),
+ ((thy3 |> Theory.add_consts_i iso_decls |> parent_path flat_names, [], [], [], []),
hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax);
(*********** isomorphisms for new types (introduced by typedef) ***********)
- val _ = writeln "Proving isomorphism properties...";
+ val _ = message "Proving isomorphism properties...";
(* get axioms from theory *)
@@ -323,7 +329,8 @@
in (thy', char_thms' @ char_thms) end;
- val (thy5, iso_char_thms) = foldr make_iso_defs (tl descr, (thy4, []));
+ val (thy5, iso_char_thms) = foldr make_iso_defs
+ (tl descr, (add_path flat_names big_name thy4, []));
(* prove isomorphism properties *)
@@ -423,7 +430,7 @@
(******************* freeness theorems for constructors *******************)
- val _ = writeln "Proving freeness of constructors...";
+ val _ = message "Proving freeness of constructors...";
(* prove theorem Rep_i (Constr_j ...) = Inj_j ... *)
@@ -470,11 +477,12 @@
val constr_inject = map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts)
((DatatypeProp.make_injs descr sorts) ~~ constr_rep_thms);
- val thy6 = store_thmss "inject" new_type_names constr_inject thy5;
+ val thy6 = store_thmss "inject" new_type_names
+ constr_inject (parent_path flat_names thy5);
(*************************** induction theorem ****************************)
- val _ = writeln "Proving induction rule for datatypes...";
+ val _ = message "Proving induction rule for datatypes...";
val Rep_inverse_thms = (map (fn (_, iso, _) => iso RS subst) newT_iso_axms) @
(map (fn r => r RS inv_f_f RS subst) (drop (length newTs, iso_inj_thms)));
@@ -526,7 +534,10 @@
DEPTH_SOLVE_1 (ares_tac [prem] 1)]))
(prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
- val thy7 = PureThy.add_tthms [(("induct", Attribute.tthm_of dt_induct), [])] thy6;
+ val thy7 = thy6 |>
+ Theory.add_path big_name |>
+ PureThy.add_tthms [(("induct", Attribute.tthm_of dt_induct), [])] |>
+ Theory.parent_path;
in (thy7, constr_inject, dist_rewrites, dt_induct)
end;