--- a/src/HOL/Tools/Datatype/datatype.ML Mon Sep 28 20:52:05 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML Mon Sep 28 21:35:57 2009 +0200
@@ -216,29 +216,6 @@
| dups => error ("Inconsistent sort constraints for " ^ commas dups))
end;
-(* arrange data entries *)
-
-fun make_dt_info alt_names descr sorts inducts reccomb_names rec_thms
- ((((((((((i, (_, (tname, _, _))), case_name), case_thms),
- exhaust_thm), distinct_thm), inject), splits), nchotomy), case_cong), weak_case_cong) =
- (tname,
- {index = i,
- alt_names = alt_names,
- descr = descr,
- sorts = sorts,
- inject = inject,
- distinct = distinct_thm,
- inducts = inducts,
- exhaust = exhaust_thm,
- nchotomy = nchotomy,
- rec_names = reccomb_names,
- rec_rewrites = rec_thms,
- case_name = case_name,
- case_rewrites = case_thms,
- case_cong = case_cong,
- weak_case_cong = weak_case_cong,
- splits = splits});
-
(* case names *)
local
@@ -320,71 +297,82 @@
(type T = config * string list val eq: T * T -> bool = eq_snd op =);
fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
-fun add_rules simps case_thms rec_thms inject distinct
- weak_case_congs cong_att =
- PureThy.add_thmss [((Binding.name "simps", simps), []),
- ((Binding.empty, flat case_thms @
- flat distinct @ rec_thms), [Simplifier.simp_add]),
- ((Binding.empty, rec_thms), [Code.add_default_eqn_attribute]),
- ((Binding.empty, flat inject), [iff_add]),
- ((Binding.empty, map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
- ((Binding.empty, weak_case_congs), [cong_att])]
- #> snd;
+fun make_dt_info alt_names descr sorts induct inducts rec_names rec_rewrites
+ (index, (((((((((((_, (tname, _, _))), inject), distinct),
+ exhaust), nchotomy), case_name), case_rewrites), case_cong), weak_case_cong), (split, split_asm))) =
+ (tname,
+ {index = index,
+ alt_names = alt_names,
+ descr = descr,
+ sorts = sorts,
+ inject = inject,
+ distinct = distinct,
+ induct = induct,
+ inducts = inducts,
+ exhaust = exhaust,
+ nchotomy = nchotomy,
+ rec_names = rec_names,
+ rec_rewrites = rec_rewrites,
+ case_name = case_name,
+ case_rewrites = case_rewrites,
+ case_cong = case_cong,
+ weak_case_cong = weak_case_cong,
+ split = split,
+ split_asm = split_asm});
-fun add_cases_induct infos inducts thy =
- let
- fun named_rules (name, {index, exhaust, ...}: info) =
- [((Binding.empty, nth inducts index), [Induct.induct_type name]),
- ((Binding.empty, exhaust), [Induct.cases_type name])];
- fun unnamed_rule i =
- ((Binding.empty, nth inducts i), [Thm.kind_internal, Induct.induct_type ""]);
- in
- thy |> PureThy.add_thms
- (maps named_rules infos @
- map unnamed_rule (length infos upto length inducts - 1)) |> snd
- |> PureThy.add_thmss [((Binding.name "inducts", inducts), [])] |> snd
- end;
-
-fun derive_datatype_props config dt_names alt_names descr sorts induct inject distinct thy1 =
+fun derive_datatype_props config dt_names alt_names descr sorts
+ induct inject (distinct_rules, distinct_rewrites, distinct_entry) thy1 =
let
- val thy2 = thy1 |> Theory.checkpoint
+ val thy2 = thy1 |> Theory.checkpoint;
+ val flat_descr = flat descr;
val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
- val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
- val (case_names_induct, case_names_exhausts) =
- (mk_case_names_induct descr, mk_case_names_exhausts descr dt_names);
- val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
+ val _ = message config ("Deriving properties for datatype(s) " ^ commas_quote new_type_names);
- val (casedist_thms, thy3) = thy2 |>
- DatatypeAbsProofs.prove_casedist_thms config new_type_names [descr] sorts induct
- case_names_exhausts;
- val ((reccomb_names, rec_thms), thy4) = DatatypeAbsProofs.prove_primrec_thms
- config new_type_names [descr] sorts (get_all thy3) inject distinct
- (Simplifier.theory_context thy3 dist_ss) induct thy3;
- val ((case_thms, case_names), thy5) = DatatypeAbsProofs.prove_case_thms
- config new_type_names [descr] sorts reccomb_names rec_thms thy4;
- val (split_thms, thy6) = DatatypeAbsProofs.prove_split_thms
- config new_type_names [descr] sorts inject distinct casedist_thms case_thms thy5;
- val (nchotomys, thy7) = DatatypeAbsProofs.prove_nchotomys config new_type_names
- [descr] sorts casedist_thms thy6;
- val (case_congs, thy8) = DatatypeAbsProofs.prove_case_congs new_type_names
- [descr] sorts nchotomys case_thms thy7;
- val (weak_case_congs, thy9) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
- [descr] sorts thy8;
+ val (exhaust, thy3) = DatatypeAbsProofs.prove_casedist_thms config new_type_names
+ descr sorts induct (mk_case_names_exhausts flat_descr dt_names) thy2;
+ val (nchotomys, thy4) = DatatypeAbsProofs.prove_nchotomys config new_type_names
+ descr sorts exhaust thy3;
+ val ((rec_names, rec_rewrites), thy5) = DatatypeAbsProofs.prove_primrec_thms
+ config new_type_names descr sorts (#inject o the o Symtab.lookup (get_all thy4))
+ inject distinct_rewrites (Simplifier.theory_context thy4 dist_ss) induct thy4;
+ val ((case_rewrites, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
+ config new_type_names descr sorts rec_names rec_rewrites thy5;
+ val (case_congs, thy7) = DatatypeAbsProofs.prove_case_congs new_type_names
+ descr sorts nchotomys case_rewrites thy6;
+ val (weak_case_congs, thy8) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
+ descr sorts thy7;
+ val (splits, thy9) = DatatypeAbsProofs.prove_split_thms
+ config new_type_names descr sorts inject distinct_rewrites exhaust case_rewrites thy8;
- val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
- val dt_infos = map (make_dt_info alt_names descr sorts (inducts, induct) reccomb_names rec_thms)
- ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
- map FewConstrs distinct ~~ inject ~~ split_thms ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
+ val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
+ val dt_infos = map_index (make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites)
+ (hd descr ~~ inject ~~ distinct_entry ~~ exhaust ~~ nchotomys ~~
+ case_names ~~ case_rewrites ~~ case_congs ~~ weak_case_congs ~~ splits);
val dt_names = map fst dt_infos;
+ val prfx = Binding.qualify true (space_implode "_" new_type_names);
+ val simps = flat (inject @ distinct_rules @ case_rewrites) @ rec_rewrites;
+ val named_rules = flat (map_index (fn (index, tname) =>
+ [((Binding.empty, [nth inducts index]), [Induct.induct_type tname]),
+ ((Binding.empty, [nth exhaust index]), [Induct.cases_type tname])]) dt_names);
+ val unnamed_rules = map (fn induct =>
+ ((Binding.empty, [induct]), [Thm.kind_internal, Induct.induct_type ""]))
+ (Library.drop (length dt_names, inducts));
in
thy9
+ |> PureThy.add_thmss ([((prfx (Binding.name "simps"), simps), []),
+ ((prfx (Binding.name "inducts"), inducts), []),
+ ((prfx (Binding.name "splits"), maps (fn (x, y) => [x, y]) splits), []),
+ ((Binding.empty, flat case_rewrites @ flat distinct_rules @ rec_rewrites),
+ [Simplifier.simp_add]),
+ ((Binding.empty, rec_rewrites), [Code.add_default_eqn_attribute]),
+ ((Binding.empty, flat inject), [iff_add]),
+ ((Binding.empty, map (fn th => th RS notE) (flat distinct_rules)),
+ [Classical.safe_elim NONE]),
+ ((Binding.empty, weak_case_congs), [Simplifier.attrib (op addcongs)])]
+ @ named_rules @ unnamed_rules)
+ |> snd
|> add_case_tr' case_names
- |> add_rules simps case_thms rec_thms inject distinct weak_case_congs (Simplifier.attrib (op addcongs))
|> register dt_infos
- |> add_cases_induct dt_infos inducts
- |> Sign.parent_path
- |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
- |> snd
|> DatatypeInterpretation.data (config, dt_names)
|> pair dt_names
end;
@@ -392,21 +380,21 @@
(** declare existing type as datatype **)
-fun prove_rep_datatype config dt_names alt_names descr sorts raw_induct raw_inject half_distinct thy1 =
+fun prove_rep_datatype config dt_names alt_names descr sorts raw_inject half_distinct raw_induct thy1 =
let
val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
- val (case_names_induct, case_names_exhausts) =
- (mk_case_names_induct descr, mk_case_names_exhausts descr dt_names);
val (((inject, distinct), [induct]), thy2) =
thy1
|> store_thmss "inject" new_type_names raw_inject
||>> store_thmss "distinct" new_type_names raw_distinct
||> Sign.add_path (space_implode "_" new_type_names)
- ||>> PureThy.add_thms [((Binding.name "induct", raw_induct), [case_names_induct])];
+ ||>> PureThy.add_thms [((Binding.name "induct", raw_induct), [mk_case_names_induct descr])]
+ ||> Sign.restore_naming thy1;
in
thy2
- |> derive_datatype_props config dt_names alt_names descr sorts induct inject distinct
+ |> derive_datatype_props config dt_names alt_names [descr] sorts
+ induct inject (distinct, distinct, map FewConstrs distinct)
end;
fun gen_rep_datatype prep_term config after_qed alt_names raw_ts thy =
@@ -460,12 +448,12 @@
fun after_qed' raw_thms =
let
- val [[[induct]], injs, half_distincts] =
+ val [[[raw_induct]], raw_inject, half_distinct] =
unflat rules (map Drule.zero_var_indexes_list raw_thms);
(*FIXME somehow dubious*)
in
ProofContext.theory_result
- (prove_rep_datatype config dt_names alt_names descr vs induct injs half_distincts)
+ (prove_rep_datatype config dt_names alt_names descr vs raw_inject half_distinct raw_induct)
#-> after_qed
end;
in
@@ -480,59 +468,11 @@
(** definitional introduction of datatypes **)
-fun add_datatype_def config new_type_names descr sorts types_syntax constr_syntax dt_info
- case_names_induct case_names_exhausts thy =
- let
- val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
-
- val ((inject, distinct, dist_rewrites, simproc_dists, induct), thy2) = thy |>
- DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts
- types_syntax constr_syntax case_names_induct;
- val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
-
- val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms config new_type_names descr
- sorts induct case_names_exhausts thy2;
- val ((reccomb_names, rec_thms), thy4) = DatatypeAbsProofs.prove_primrec_thms
- config new_type_names descr sorts dt_info inject dist_rewrites
- (Simplifier.theory_context thy3 dist_ss) induct thy3;
- val ((case_thms, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
- config new_type_names descr sorts reccomb_names rec_thms thy4;
- val (split_thms, thy7) = DatatypeAbsProofs.prove_split_thms config new_type_names
- descr sorts inject dist_rewrites casedist_thms case_thms thy6;
- val (nchotomys, thy8) = DatatypeAbsProofs.prove_nchotomys config new_type_names
- descr sorts casedist_thms thy7;
- val (case_congs, thy9) = DatatypeAbsProofs.prove_case_congs new_type_names
- descr sorts nchotomys case_thms thy8;
- val (weak_case_congs, thy10) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
- descr sorts thy9;
-
- val dt_infos = map
- (make_dt_info (SOME new_type_names) (flat descr) sorts (inducts, induct) reccomb_names rec_thms)
- ((0 upto length (hd descr) - 1) ~~ hd descr ~~ case_names ~~ case_thms ~~
- casedist_thms ~~ simproc_dists ~~ inject ~~ split_thms ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
-
- val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
- val dt_names = map fst dt_infos;
-
- val thy12 =
- thy10
- |> add_case_tr' case_names
- |> Sign.add_path (space_implode "_" new_type_names)
- |> add_rules simps case_thms rec_thms inject distinct
- weak_case_congs (Simplifier.attrib (op addcongs))
- |> register dt_infos
- |> add_cases_induct dt_infos inducts
- |> Sign.parent_path
- |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
- |> DatatypeInterpretation.data (config, map fst dt_infos);
- in (dt_names, thy12) end;
-
fun gen_add_datatype prep_typ config new_type_names dts thy =
let
val _ = Theory.requires thy "Datatype" "datatype definitions";
(* this theory is used just for parsing *)
-
val tmp_thy = thy |>
Theory.copy |>
Sign.add_types (map (fn (tvs, tname, mx, _) =>
@@ -547,6 +487,7 @@
| dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
" : " ^ commas dups))
end) dts);
+ val dt_names = map fst new_dts;
val _ = (case duplicates (op =) (map fst new_dts) @ duplicates (op =) new_type_names of
[] => () | dups => error ("Duplicate datatypes: " ^ commas dups));
@@ -589,13 +530,13 @@
if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
else raise exn;
- val descr' = flat descr;
- val case_names_induct = mk_case_names_induct descr';
- val case_names_exhausts = mk_case_names_exhausts descr' (map #1 new_dts);
+ val _ = message config ("Constructing datatype(s) " ^ commas_quote new_type_names);
+ val ((inject, distinct_rules, distinct_rewrites, distinct_entry, induct), thy') = thy |>
+ DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts
+ types_syntax constr_syntax (mk_case_names_induct (flat descr));
in
- add_datatype_def
- config new_type_names descr sorts types_syntax constr_syntax dt_info
- case_names_induct case_names_exhausts thy
+ derive_datatype_props config dt_names (SOME new_type_names) descr sorts
+ induct inject (distinct_rules, distinct_rewrites, distinct_entry) thy'
end;
val add_datatype = gen_add_datatype cert_typ;