# HG changeset patch # User wenzelm # Date 1254166557 -7200 # Node ID d5de73f4bcb80f2e6709cc2851f6d1efe3cca10b # Parent f7ed14d60818256362ea24b26828c5bd4a7c1d25# Parent a900d3cd47ccb68753b576b9ffa7b74d065ca9a2 merged diff -r a900d3cd47cc -r d5de73f4bcb8 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Mon Sep 28 20:52:05 2009 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Mon Sep 28 21:35:57 2009 +0200 @@ -245,7 +245,7 @@ val (full_new_type_names',thy1) = Datatype.add_datatype config new_type_names' dts'' thy; - val {descr, inducts = (_, induct), ...} = + val {descr, induct, ...} = Datatype.the_info thy1 (hd full_new_type_names'); fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); diff -r a900d3cd47cc -r d5de73f4bcb8 src/HOL/Tools/Datatype/datatype.ML --- 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; diff -r a900d3cd47cc -r d5de73f4bcb8 src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Mon Sep 28 20:52:05 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Mon Sep 28 21:35:57 2009 +0200 @@ -20,7 +20,7 @@ attribute list -> theory -> thm list * theory val prove_primrec_thms : config -> string list -> descr list -> (string * sort) list -> - info Symtab.table -> thm list list -> thm list list -> + (string -> thm list) -> thm list list -> thm list list -> simpset -> thm -> theory -> (string list * thm list) * theory val prove_case_thms : config -> string list -> descr list -> (string * sort) list -> @@ -88,7 +88,7 @@ (*************************** primrec combinators ******************************) fun prove_primrec_thms (config : config) new_type_names descr sorts - (dt_info : info Symtab.table) constr_inject dist_rewrites dist_ss induct thy = + injects_of constr_inject dist_rewrites dist_ss induct thy = let val _ = message config "Constructing primrec combinators ..."; @@ -174,11 +174,11 @@ val inject = map (fn r => r RS iffD1) (if i < length newTs then List.nth (constr_inject, i) - else #inject (the (Symtab.lookup dt_info tname))); + else injects_of tname); fun mk_unique_constr_tac n ((tac, intr::intrs, j), (cname, cargs)) = let - val k = length (List.filter is_rec_type cargs) + val k = length (filter is_rec_type cargs) in (EVERY [DETERM tac, REPEAT (etac ex1E 1), rtac ex1I 1, diff -r a900d3cd47cc -r d5de73f4bcb8 src/HOL/Tools/Datatype/datatype_aux.ML --- a/src/HOL/Tools/Datatype/datatype_aux.ML Mon Sep 28 20:52:05 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Mon Sep 28 21:35:57 2009 +0200 @@ -193,7 +193,8 @@ sorts : (string * sort) list, inject : thm list, distinct : simproc_dist, - inducts : thm list * thm, + induct : thm, + inducts : thm list, exhaust : thm, nchotomy : thm, rec_names : string list, @@ -202,7 +203,8 @@ case_rewrites : thm list, case_cong : thm, weak_case_cong : thm, - splits : thm * thm}; + split : thm, + split_asm: thm}; fun mk_Free s T i = Free (s ^ (string_of_int i), T); diff -r a900d3cd47cc -r d5de73f4bcb8 src/HOL/Tools/Datatype/datatype_realizer.ML --- a/src/HOL/Tools/Datatype/datatype_realizer.ML Mon Sep 28 20:52:05 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Mon Sep 28 21:35:57 2009 +0200 @@ -38,7 +38,7 @@ fun mk_realizes T = Const ("realizes", T --> HOLogic.boolT --> HOLogic.boolT); -fun make_ind sorts ({descr, rec_names, rec_rewrites, inducts = (_, induct), ...} : info) is thy = +fun make_ind sorts ({descr, rec_names, rec_rewrites, induct, ...} : info) is thy = let val recTs = get_rec_types descr sorts; val pnames = if length descr = 1 then ["P"] diff -r a900d3cd47cc -r d5de73f4bcb8 src/HOL/Tools/Datatype/datatype_rep_proofs.ML --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Mon Sep 28 20:52:05 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Mon Sep 28 21:35:57 2009 +0200 @@ -389,7 +389,7 @@ fun prove_iso_thms (ds, (inj_thms, elem_thms)) = let val (_, (tname, _, _)) = hd ds; - val induct = (snd o #inducts o the o Symtab.lookup dt_info) tname; + val induct = (#induct o the o Symtab.lookup dt_info) tname; fun mk_ind_concl (i, _) = let diff -r a900d3cd47cc -r d5de73f4bcb8 src/HOL/Tools/Function/size.ML --- a/src/HOL/Tools/Function/size.ML Mon Sep 28 20:52:05 2009 +0200 +++ b/src/HOL/Tools/Function/size.ML Mon Sep 28 21:35:57 2009 +0200 @@ -59,7 +59,7 @@ fun prove_size_thms (info : info) new_type_names thy = let - val {descr, alt_names, sorts, rec_names, rec_rewrites, inducts = (_, induct), ...} = info; + val {descr, alt_names, sorts, rec_names, rec_rewrites, induct, ...} = info; val l = length new_type_names; val alt_names' = (case alt_names of NONE => replicate l NONE | SOME names => map SOME names); diff -r a900d3cd47cc -r d5de73f4bcb8 src/HOL/Tools/TFL/casesplit.ML --- a/src/HOL/Tools/TFL/casesplit.ML Mon Sep 28 20:52:05 2009 +0200 +++ b/src/HOL/Tools/TFL/casesplit.ML Mon Sep 28 21:35:57 2009 +0200 @@ -96,7 +96,7 @@ | TVar((s,i),_) => error ("Free variable: " ^ s) val dt = Datatype.the_info thy ty_str in - cases_thm_of_induct_thm (snd (#inducts dt)) + cases_thm_of_induct_thm (#induct dt) end; (* diff -r a900d3cd47cc -r d5de73f4bcb8 src/HOL/Tools/old_primrec.ML --- a/src/HOL/Tools/old_primrec.ML Mon Sep 28 20:52:05 2009 +0200 +++ b/src/HOL/Tools/old_primrec.ML Mon Sep 28 21:35:57 2009 +0200 @@ -230,7 +230,7 @@ (tname, dt)::(find_dts dt_info tnames' tnames) else find_dts dt_info tnames' tnames); -fun prepare_induct ({descr, inducts = (_, induct), ...}: info) rec_eqns = +fun prepare_induct ({descr, induct, ...}: info) rec_eqns = let fun constrs_of (_, (_, _, cs)) = map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs;