# HG changeset patch # User wenzelm # Date 1203953475 -3600 # Node ID fe2d24c26e0c9dc6b2613f535c668a9641979d67 # Parent 70ef56eb650a0bf6fdccbb40c7f28e638bf92541 inductive package: simplified group handling; diff -r 70ef56eb650a -r fe2d24c26e0c src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Mon Feb 25 12:05:58 2008 +0100 +++ b/src/HOL/Nominal/nominal_package.ML Mon Feb 25 16:31:15 2008 +0100 @@ -563,12 +563,12 @@ val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) = setmp InductivePackage.quiet_mode false - (InductivePackage.add_inductive_global {verbose = false, kind = Thm.internalK, - group = serial_string (), (* FIXME pass proper group (!?) *) + (InductivePackage.add_inductive_global (serial_string ()) + {verbose = false, kind = Thm.internalK, alt_name = big_rep_name, coind = false, no_elim = true, no_ind = false} - (map (fn (s, T) => ((s, T --> HOLogic.boolT), NoSyn)) - (rep_set_names' ~~ recTs')) - [] (map (fn x => (("", []), x)) intr_ts) []) thy3; + (map (fn (s, T) => ((s, T --> HOLogic.boolT), NoSyn)) + (rep_set_names' ~~ recTs')) + [] (map (fn x => (("", []), x)) intr_ts) []) thy3; (**** Prove that representing set is closed under permutation ****) @@ -1488,12 +1488,12 @@ val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) = thy10 |> setmp InductivePackage.quiet_mode (!quiet_mode) - (InductivePackage.add_inductive_global {verbose = false, kind = Thm.internalK, - group = serial_string (), (* FIXME pass proper group (!?) *) + (InductivePackage.add_inductive_global (serial_string ()) + {verbose = false, kind = Thm.internalK, alt_name = big_rec_name, coind = false, no_elim = false, no_ind = false} - (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts)) - (map dest_Free rec_fns) - (map (fn x => (("", []), x)) rec_intr_ts) []) ||> + (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts)) + (map dest_Free rec_fns) + (map (fn x => (("", []), x)) rec_intr_ts) []) ||> PureThy.hide_thms true [NameSpace.append (Sign.full_name thy10 big_rec_name) "induct"]; diff -r 70ef56eb650a -r fe2d24c26e0c src/HOL/Tools/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_abs_proofs.ML Mon Feb 25 12:05:58 2008 +0100 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Mon Feb 25 16:31:15 2008 +0100 @@ -155,12 +155,12 @@ val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) = setmp InductivePackage.quiet_mode (!quiet_mode) - (InductivePackage.add_inductive_global {verbose = false, kind = Thm.internalK, - group = serial_string (), (* FIXME pass proper group (!?) *) - alt_name = big_rec_name', coind = false, no_elim = false, no_ind = true} - (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts)) - (map dest_Free rec_fns) - (map (fn x => (("", []), x)) rec_intr_ts) []) thy0; + (InductivePackage.add_inductive_global (serial_string ()) + {verbose = false, kind = Thm.internalK, alt_name = big_rec_name', + coind = false, no_elim = false, no_ind = true} + (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts)) + (map dest_Free rec_fns) + (map (fn x => (("", []), x)) rec_intr_ts) []) thy0; (* prove uniqueness and termination of primrec combinators *) diff -r 70ef56eb650a -r fe2d24c26e0c src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Mon Feb 25 12:05:58 2008 +0100 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Mon Feb 25 16:31:15 2008 +0100 @@ -177,11 +177,11 @@ val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) = setmp InductivePackage.quiet_mode (! quiet_mode) - (InductivePackage.add_inductive_global {verbose = false, kind = Thm.internalK, - group = serial_string (), (* FIXME pass proper group (!?) *) - alt_name = big_rec_name, coind = false, no_elim = true, no_ind = false} - (map (fn s => ((s, UnivT'), NoSyn)) rep_set_names') [] - (map (fn x => (("", []), x)) intr_ts) []) thy1; + (InductivePackage.add_inductive_global (serial_string ()) + {verbose = false, kind = Thm.internalK, alt_name = big_rec_name, + coind = false, no_elim = true, no_ind = false} + (map (fn s => ((s, UnivT'), NoSyn)) rep_set_names') [] + (map (fn x => (("", []), x)) intr_ts) []) thy1; (********************************* typedef ********************************) diff -r 70ef56eb650a -r fe2d24c26e0c src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Mon Feb 25 12:05:58 2008 +0100 +++ b/src/HOL/Tools/inductive_package.ML Mon Feb 25 16:31:15 2008 +0100 @@ -39,8 +39,7 @@ val inductive_cases_i: ((bstring * Attrib.src list) * term list) list -> Proof.context -> thm list list * local_theory val add_inductive_i: - {verbose: bool, kind: string, group: string, alt_name: bstring, - coind: bool, no_elim: bool, no_ind: bool} -> + {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} -> ((string * typ) * mixfix) list -> (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list -> local_theory -> inductive_result * local_theory @@ -48,9 +47,8 @@ (string * string option * mixfix) list -> ((bstring * Attrib.src list) * string) list -> (thmref * Attrib.src list) list -> local_theory -> inductive_result * local_theory - val add_inductive_global: - {verbose: bool, kind: string, group: string, alt_name: bstring, - coind: bool, no_elim: bool, no_ind: bool} -> + val add_inductive_global: string -> + {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} -> ((string * typ) * mixfix) list -> (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list -> theory -> inductive_result * theory val arities_of: thm -> (string * int) list @@ -66,13 +64,12 @@ sig include BASIC_INDUCTIVE_PACKAGE type add_ind_def - val declare_rules: string -> string -> bstring -> bool -> bool -> string list -> + val declare_rules: string -> bstring -> bool -> bool -> string list -> thm list -> bstring list -> Attrib.src list list -> (thm * string list) list -> thm -> local_theory -> thm list * thm list * thm * local_theory val add_ind_def: add_ind_def val gen_add_inductive_i: add_ind_def -> - {verbose: bool, kind: string, group: string, alt_name: bstring, - coind: bool, no_elim: bool, no_ind: bool} -> + {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} -> ((string * typ) * mixfix) list -> (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list -> local_theory -> inductive_result * local_theory @@ -588,8 +585,7 @@ (** specification of (co)inductive predicates **) -fun mk_ind_def group alt_name coind cs intr_ts monos - params cnames_syn ctxt = +fun mk_ind_def alt_name coind cs intr_ts monos params cnames_syn ctxt = let val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp}; @@ -647,7 +643,7 @@ space_implode "_" (map fst cnames_syn) else alt_name; val ((rec_const, (_, fp_def)), ctxt') = ctxt |> - LocalTheory.define_grouped Thm.internalK group + LocalTheory.define Thm.internalK ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn), (("", []), fold_rev lambda params (Const (fp_name, (predT --> predT) --> predT) $ fp_fun))); @@ -664,7 +660,7 @@ (list_comb (rec_const, params @ make_bool_args' bs i @ make_args argTs (xs ~~ Ts))))) end) (cnames_syn ~~ cs); - val (consts_defs, ctxt'') = fold_map (LocalTheory.define_grouped Thm.internalK group) specs ctxt'; + val (consts_defs, ctxt'') = fold_map (LocalTheory.define Thm.internalK) specs ctxt'; val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs); val mono = prove_mono predT fp_fun monos ctxt'' @@ -673,7 +669,7 @@ list_comb (rec_const, params), preds, argTs, bs, xs) end; -fun declare_rules kind group rec_name coind no_ind cnames intrs intr_names intr_atts +fun declare_rules kind rec_name coind no_ind cnames intrs intr_names intr_atts elims raw_induct ctxt = let val ind_case_names = RuleCases.case_names intr_names; @@ -688,29 +684,29 @@ val (intrs', ctxt1) = ctxt |> - LocalTheory.notes_grouped kind group + LocalTheory.notes kind (map (NameSpace.qualified rec_name) intr_names ~~ intr_atts ~~ map (fn th => [([th], [Attrib.internal (K (ContextRules.intro_query NONE))])]) intrs) |>> map (hd o snd); val (((_, elims'), (_, [induct'])), ctxt2) = ctxt1 |> - LocalTheory.note_grouped kind group ((NameSpace.qualified rec_name "intros", []), intrs') ||>> + LocalTheory.note kind ((NameSpace.qualified rec_name "intros", []), intrs') ||>> fold_map (fn (name, (elim, cases)) => - LocalTheory.note_grouped kind group ((NameSpace.qualified (Sign.base_name name) "cases", + LocalTheory.note kind ((NameSpace.qualified (Sign.base_name name) "cases", [Attrib.internal (K (RuleCases.case_names cases)), Attrib.internal (K (RuleCases.consumes 1)), Attrib.internal (K (Induct.cases_pred name)), Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #> apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>> - LocalTheory.note_grouped kind group ((NameSpace.qualified rec_name (coind_prefix coind ^ "induct"), + LocalTheory.note kind ((NameSpace.qualified rec_name (coind_prefix coind ^ "induct"), map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]); val ctxt3 = if no_ind orelse coind then ctxt2 else let val inducts = cnames ~~ ProjectRule.projects ctxt2 (1 upto length cnames) induct' in ctxt2 |> - LocalTheory.notes_grouped kind group [((NameSpace.qualified rec_name "inducts", []), + LocalTheory.notes kind [((NameSpace.qualified rec_name "inducts", []), inducts |> map (fn (name, th) => ([th], [Attrib.internal (K ind_case_names), Attrib.internal (K (RuleCases.consumes 1)), @@ -719,13 +715,12 @@ in (intrs', elims', induct', ctxt3) end; type add_ind_def = - {verbose: bool, kind: string, group: string, alt_name: bstring, - coind: bool, no_elim: bool, no_ind: bool} -> + {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} -> term list -> ((string * Attrib.src list) * term) list -> thm list -> term list -> (string * mixfix) list -> local_theory -> inductive_result * local_theory -fun add_ind_def {verbose, kind, group, alt_name, coind, no_elim, no_ind} +fun add_ind_def {verbose, kind, alt_name, coind, no_elim, no_ind} cs intros monos params cnames_syn ctxt = let val _ = null cnames_syn andalso error "No inductive predicates given"; @@ -738,8 +733,7 @@ apfst split_list (split_list (map (check_rule ctxt cs params) intros)); val (ctxt1, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds, - argTs, bs, xs) = mk_ind_def group alt_name coind cs intr_ts - monos params cnames_syn ctxt; + argTs, bs, xs) = mk_ind_def alt_name coind cs intr_ts monos params cnames_syn ctxt; val (intrs, unfold) = prove_intrs coind mono fp_def (length bs + length xs) params intr_ts rec_preds_defs ctxt1; @@ -757,7 +751,7 @@ prove_indrule cs argTs bs xs rec_const params intr_ts mono fp_def rec_preds_defs ctxt1); - val (intrs', elims', induct, ctxt2) = declare_rules kind group rec_name coind no_ind + val (intrs', elims', induct, ctxt2) = declare_rules kind rec_name coind no_ind cnames intrs intr_names intr_atts elims raw_induct ctxt1; val names = map #1 cnames_syn; @@ -777,7 +771,7 @@ (* external interfaces *) -fun gen_add_inductive_i mk_def (flags as {verbose, kind, group, alt_name, coind, no_elim, no_ind}) +fun gen_add_inductive_i mk_def (flags as {verbose, kind, alt_name, coind, no_elim, no_ind}) cnames_syn pnames spec monos lthy = let val thy = ProofContext.theory_of lthy; @@ -841,18 +835,23 @@ val (cs, ps) = chop (length cnames_syn) vars; val intrs = map (apsnd the_single) specs; val monos = Attrib.eval_thms lthy raw_monos; - val flags = {verbose = verbose, kind = Thm.theoremK, group = serial_string (), alt_name = "", + val flags = {verbose = verbose, kind = Thm.theoremK, alt_name = "", coind = coind, no_elim = false, no_ind = false}; - in gen_add_inductive_i mk_def flags cs (map fst ps) intrs monos lthy end; + in + lthy + |> LocalTheory.set_group (serial_string ()) + |> gen_add_inductive_i mk_def flags cs (map fst ps) intrs monos + end; val add_inductive_i = gen_add_inductive_i add_ind_def; val add_inductive = gen_add_inductive add_ind_def; -fun add_inductive_global flags cnames_syn pnames pre_intros monos thy = +fun add_inductive_global group flags cnames_syn pnames pre_intros monos thy = let val name = Sign.full_name thy (fst (fst (hd cnames_syn))); val ctxt' = thy |> TheoryTarget.init NONE + |> LocalTheory.set_group group |> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd |> LocalTheory.exit; val info = #2 (the_inductive ctxt' name); diff -r 70ef56eb650a -r fe2d24c26e0c src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Mon Feb 25 12:05:58 2008 +0100 +++ b/src/HOL/Tools/inductive_realizer.ML Mon Feb 25 16:31:15 2008 +0100 @@ -350,9 +350,9 @@ (** realizability predicate **) val (ind_info, thy3') = thy2 |> - InductivePackage.add_inductive_global {verbose = false, kind = Thm.theoremK, - group = serial_string (), (* FIXME pass proper group (!?) *) - alt_name = "", coind = false, no_elim = false, no_ind = false} + InductivePackage.add_inductive_global (serial_string ()) + {verbose = false, kind = Thm.theoremK, alt_name = "", + coind = false, no_elim = false, no_ind = false} rlzpreds rlzparams (map (fn (rintr, intr) => ((Sign.base_name (name_of_thm intr), []), subst_atomic rlzpreds' (Logic.unvarify rintr))) diff -r 70ef56eb650a -r fe2d24c26e0c src/HOL/Tools/inductive_set_package.ML --- a/src/HOL/Tools/inductive_set_package.ML Mon Feb 25 12:05:58 2008 +0100 +++ b/src/HOL/Tools/inductive_set_package.ML Mon Feb 25 16:31:15 2008 +0100 @@ -12,8 +12,7 @@ val to_pred_att: thm list -> attribute val pred_set_conv_att: attribute val add_inductive_i: - {verbose: bool, kind: string, group: string, alt_name: bstring, - coind: bool, no_elim: bool, no_ind: bool} -> + {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} -> ((string * typ) * mixfix) list -> (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list -> local_theory -> InductivePackage.inductive_result * local_theory @@ -402,7 +401,7 @@ (**** definition of inductive sets ****) -fun add_ind_set_def {verbose, kind, group, alt_name, coind, no_elim, no_ind} +fun add_ind_set_def {verbose, kind, alt_name, coind, no_elim, no_ind} cs intros monos params cnames_syn ctxt = let val thy = ProofContext.theory_of ctxt; @@ -465,8 +464,7 @@ val cnames_syn' = map (fn (s, _) => (s ^ "p", NoSyn)) cnames_syn; val monos' = map (to_pred [] (Context.Proof ctxt)) monos; val ({preds, intrs, elims, raw_induct, ...}, ctxt1) = - InductivePackage.add_ind_def {verbose = verbose, kind = kind, group = group, - alt_name = "", (* FIXME pass alt_name (!?) *) + InductivePackage.add_ind_def {verbose = verbose, kind = kind, alt_name = "", coind = coind, no_elim = no_elim, no_ind = no_ind} cs' intros' monos' params1 cnames_syn' ctxt; @@ -502,7 +500,7 @@ val (intr_names, intr_atts) = split_list (map fst intros); val raw_induct' = to_set [] (Context.Proof ctxt3) raw_induct; val (intrs', elims', induct, ctxt4) = - InductivePackage.declare_rules kind group rec_name coind no_ind cnames + InductivePackage.declare_rules kind rec_name coind no_ind cnames (map (to_set [] (Context.Proof ctxt3)) intrs) intr_names intr_atts (map (fn th => (to_set [] (Context.Proof ctxt3) th, map fst (fst (RuleCases.get th)))) elims)