# HG changeset patch # User berghofe # Date 908556895 -7200 # Node ID 6ecb6ea25f190c626200288cf2134e334f5c167a # Parent f2c5354cd32f0e61bc89ffb78264383c0398d82d - Changed structure of name spaces - Proofs for datatypes with unneeded parameters are working now - added additional parameter flat_names - added quiet_mode flag diff -r f2c5354cd32f -r 6ecb6ea25f19 src/HOL/Tools/datatype_abs_proofs.ML --- 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 diff -r f2c5354cd32f -r 6ecb6ea25f19 src/HOL/Tools/datatype_aux.ML --- 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 *) diff -r f2c5354cd32f -r 6ecb6ea25f19 src/HOL/Tools/datatype_package.ML --- 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; diff -r f2c5354cd32f -r 6ecb6ea25f19 src/HOL/Tools/datatype_rep_proofs.ML --- 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;