1.1 --- a/src/HOL/Tools/inductive_package.ML	Sat Jan 26 17:08:35 2008 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat Jan 26 17:08:36 2008 +0100
     1.3 @@ -39,7 +39,8 @@
     1.4    val inductive_cases_i: ((bstring * Attrib.src list) * term list) list ->
     1.5      Proof.context -> thm list list * local_theory
     1.6    val add_inductive_i:
     1.7 -    {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} ->
     1.8 +    {verbose: bool, kind: string, group: string, alt_name: bstring,
     1.9 +      coind: bool, no_elim: bool, no_ind: bool} ->
    1.10      ((string * typ) * mixfix) list ->
    1.11      (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
    1.12        local_theory -> inductive_result * local_theory
    1.13 @@ -48,7 +49,8 @@
    1.14      ((bstring * Attrib.src list) * string) list -> (thmref * Attrib.src list) list ->
    1.15      local_theory -> inductive_result * local_theory
    1.16    val add_inductive_global:
    1.17 -    {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} ->
    1.18 +    {verbose: bool, kind: string, group: string, alt_name: bstring,
    1.19 +      coind: bool, no_elim: bool, no_ind: bool} ->
    1.20      ((string * typ) * mixfix) list -> (string * typ) list ->
    1.21      ((bstring * Attrib.src list) * term) list -> thm list -> theory -> inductive_result * theory
    1.22    val arities_of: thm -> (string * int) list
    1.23 @@ -64,12 +66,13 @@
    1.24  sig
    1.25    include BASIC_INDUCTIVE_PACKAGE
    1.26    type add_ind_def
    1.27 -  val declare_rules: string -> bstring -> bool -> bool -> string list ->
    1.28 +  val declare_rules: string -> string -> bstring -> bool -> bool -> string list ->
    1.29      thm list -> bstring list -> Attrib.src list list -> (thm * string list) list ->
    1.30      thm -> local_theory -> thm list * thm list * thm * local_theory
    1.31    val add_ind_def: add_ind_def
    1.32    val gen_add_inductive_i: add_ind_def ->
    1.33 -    {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} ->
    1.34 +    {verbose: bool, kind: string, group: string, alt_name: bstring,
    1.35 +      coind: bool, no_elim: bool, no_ind: bool} ->
    1.36      ((string * typ) * mixfix) list ->
    1.37      (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
    1.38        local_theory -> inductive_result * local_theory
    1.39 @@ -585,7 +588,7 @@
    1.40  
    1.41  (** specification of (co)inductive predicates **)
    1.42  
    1.43 -fun mk_ind_def alt_name coind cs intr_ts monos
    1.44 +fun mk_ind_def group alt_name coind cs intr_ts monos
    1.45        params cnames_syn ctxt =
    1.46    let
    1.47      val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp};
    1.48 @@ -644,7 +647,7 @@
    1.49        space_implode "_" (map fst cnames_syn) else alt_name;
    1.50  
    1.51      val ((rec_const, (_, fp_def)), ctxt') = ctxt |>
    1.52 -      LocalTheory.define Thm.internalK
    1.53 +      LocalTheory.define_grouped Thm.internalK group
    1.54          ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
    1.55           (("", []), fold_rev lambda params
    1.56             (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)));
    1.57 @@ -661,7 +664,7 @@
    1.58              (list_comb (rec_const, params @ make_bool_args' bs i @
    1.59                make_args argTs (xs ~~ Ts)))))
    1.60          end) (cnames_syn ~~ cs);
    1.61 -    val (consts_defs, ctxt'') = fold_map (LocalTheory.define Thm.internalK) specs ctxt';
    1.62 +    val (consts_defs, ctxt'') = fold_map (LocalTheory.define_grouped Thm.internalK group) specs ctxt';
    1.63      val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
    1.64  
    1.65      val mono = prove_mono predT fp_fun monos ctxt''
    1.66 @@ -670,7 +673,7 @@
    1.67      list_comb (rec_const, params), preds, argTs, bs, xs)
    1.68    end;
    1.69  
    1.70 -fun declare_rules kind rec_name coind no_ind cnames intrs intr_names intr_atts
    1.71 +fun declare_rules kind group rec_name coind no_ind cnames intrs intr_names intr_atts
    1.72        elims raw_induct ctxt =
    1.73    let
    1.74      val ind_case_names = RuleCases.case_names intr_names;
    1.75 @@ -685,29 +688,29 @@
    1.76  
    1.77      val (intrs', ctxt1) =
    1.78        ctxt |>
    1.79 -      LocalTheory.notes kind
    1.80 +      LocalTheory.notes_grouped kind group
    1.81          (map (NameSpace.qualified rec_name) intr_names ~~
    1.82           intr_atts ~~ map (fn th => [([th],
    1.83             [Attrib.internal (K (ContextRules.intro_query NONE))])]) intrs) |>>
    1.84        map (hd o snd);
    1.85      val (((_, elims'), (_, [induct'])), ctxt2) =
    1.86        ctxt1 |>
    1.87 -      LocalTheory.note kind ((NameSpace.qualified rec_name "intros", []), intrs') ||>>
    1.88 +      LocalTheory.note_grouped kind group ((NameSpace.qualified rec_name "intros", []), intrs') ||>>
    1.89        fold_map (fn (name, (elim, cases)) =>
    1.90 -        LocalTheory.note kind ((NameSpace.qualified (Sign.base_name name) "cases",
    1.91 +        LocalTheory.note_grouped kind group ((NameSpace.qualified (Sign.base_name name) "cases",
    1.92            [Attrib.internal (K (RuleCases.case_names cases)),
    1.93             Attrib.internal (K (RuleCases.consumes 1)),
    1.94             Attrib.internal (K (Induct.cases_pred name)),
    1.95             Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #>
    1.96          apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
    1.97 -      LocalTheory.note kind ((NameSpace.qualified rec_name (coind_prefix coind ^ "induct"),
    1.98 +      LocalTheory.note_grouped kind group ((NameSpace.qualified rec_name (coind_prefix coind ^ "induct"),
    1.99          map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
   1.100  
   1.101      val ctxt3 = if no_ind orelse coind then ctxt2 else
   1.102        let val inducts = cnames ~~ ProjectRule.projects ctxt2 (1 upto length cnames) induct'
   1.103        in
   1.104          ctxt2 |>
   1.105 -        LocalTheory.notes kind [((NameSpace.qualified rec_name "inducts", []),
   1.106 +        LocalTheory.notes_grouped kind group [((NameSpace.qualified rec_name "inducts", []),
   1.107            inducts |> map (fn (name, th) => ([th],
   1.108              [Attrib.internal (K ind_case_names),
   1.109               Attrib.internal (K (RuleCases.consumes 1)),
   1.110 @@ -716,12 +719,13 @@
   1.111    in (intrs', elims', induct', ctxt3) end;
   1.112  
   1.113  type add_ind_def =
   1.114 -  {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} ->
   1.115 +  {verbose: bool, kind: string, group: string, alt_name: bstring,
   1.116 +    coind: bool, no_elim: bool, no_ind: bool} ->
   1.117    term list -> ((string * Attrib.src list) * term) list -> thm list ->
   1.118    term list -> (string * mixfix) list ->
   1.119    local_theory -> inductive_result * local_theory
   1.120  
   1.121 -fun add_ind_def {verbose, kind, alt_name, coind, no_elim, no_ind}
   1.122 +fun add_ind_def {verbose, kind, group, alt_name, coind, no_elim, no_ind}
   1.123      cs intros monos params cnames_syn ctxt =
   1.124    let
   1.125      val _ = null cnames_syn andalso error "No inductive predicates given";
   1.126 @@ -734,7 +738,7 @@
   1.127        apfst split_list (split_list (map (check_rule ctxt cs params) intros));
   1.128  
   1.129      val (ctxt1, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
   1.130 -      argTs, bs, xs) = mk_ind_def alt_name coind cs intr_ts
   1.131 +      argTs, bs, xs) = mk_ind_def group alt_name coind cs intr_ts
   1.132          monos params cnames_syn ctxt;
   1.133  
   1.134      val (intrs, unfold) = prove_intrs coind mono fp_def (length bs + length xs)
   1.135 @@ -753,7 +757,7 @@
   1.136           prove_indrule cs argTs bs xs rec_const params intr_ts mono fp_def
   1.137             rec_preds_defs ctxt1);
   1.138  
   1.139 -    val (intrs', elims', induct, ctxt2) = declare_rules kind rec_name coind no_ind
   1.140 +    val (intrs', elims', induct, ctxt2) = declare_rules kind group rec_name coind no_ind
   1.141        cnames intrs intr_names intr_atts elims raw_induct ctxt1;
   1.142  
   1.143      val names = map #1 cnames_syn;
   1.144 @@ -773,7 +777,7 @@
   1.145  
   1.146  (* external interfaces *)
   1.147  
   1.148 -fun gen_add_inductive_i mk_def (flags as {verbose, kind, alt_name, coind, no_elim, no_ind})
   1.149 +fun gen_add_inductive_i mk_def (flags as {verbose, kind, group, alt_name, coind, no_elim, no_ind})
   1.150      cnames_syn pnames spec monos lthy =
   1.151    let
   1.152      val thy = ProofContext.theory_of lthy;
   1.153 @@ -837,7 +841,7 @@
   1.154      val (cs, ps) = chop (length cnames_syn) vars;
   1.155      val intrs = map (apsnd the_single) specs;
   1.156      val monos = Attrib.eval_thms lthy raw_monos;
   1.157 -    val flags = {verbose = verbose, kind = Thm.theoremK, alt_name = "",
   1.158 +    val flags = {verbose = verbose, kind = Thm.theoremK, group = serial_string (), alt_name = "",
   1.159        coind = coind, no_elim = false, no_ind = false};
   1.160    in gen_add_inductive_i mk_def flags cs (map fst ps) intrs monos lthy end;
   1.161  
   1.162 @@ -911,6 +915,7 @@
   1.163    end;
   1.164  
   1.165  
   1.166 +
   1.167  (** package setup **)
   1.168  
   1.169  (* setup theory *)

     2.1 --- a/src/HOL/Tools/inductive_set_package.ML	Sat Jan 26 17:08:35 2008 +0100
     2.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Sat Jan 26 17:08:36 2008 +0100
     2.3 @@ -12,7 +12,8 @@
     2.4    val to_pred_att: thm list -> attribute
     2.5    val pred_set_conv_att: attribute
     2.6    val add_inductive_i:
     2.7 -    {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} ->
     2.8 +    {verbose: bool, kind: string, group: string, alt_name: bstring,
     2.9 +      coind: bool, no_elim: bool, no_ind: bool} ->
    2.10      ((string * typ) * mixfix) list ->
    2.11      (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
    2.12        local_theory -> InductivePackage.inductive_result * local_theory
    2.13 @@ -402,7 +403,7 @@
    2.14  
    2.15  (**** definition of inductive sets ****)
    2.16  
    2.17 -fun add_ind_set_def {verbose, kind, alt_name, coind, no_elim, no_ind}
    2.18 +fun add_ind_set_def {verbose, kind, group, alt_name, coind, no_elim, no_ind}
    2.19      cs intros monos params cnames_syn ctxt =
    2.20    let
    2.21      val thy = ProofContext.theory_of ctxt;
    2.22 @@ -465,7 +466,7 @@
    2.23      val cnames_syn' = map (fn (s, _) => (s ^ "p", NoSyn)) cnames_syn;
    2.24      val monos' = map (to_pred [] (Context.Proof ctxt)) monos;
    2.25      val ({preds, intrs, elims, raw_induct, ...}, ctxt1) =
    2.26 -      InductivePackage.add_ind_def {verbose = verbose, kind = kind,
    2.27 +      InductivePackage.add_ind_def {verbose = verbose, kind = kind, group = group,
    2.28            alt_name = "",  (* FIXME pass alt_name (!?) *)
    2.29            coind = coind, no_elim = no_elim, no_ind = no_ind}
    2.30          cs' intros' monos' params1 cnames_syn' ctxt;
    2.31 @@ -502,7 +503,7 @@
    2.32      val (intr_names, intr_atts) = split_list (map fst intros);
    2.33      val raw_induct' = to_set [] (Context.Proof ctxt3) raw_induct;
    2.34      val (intrs', elims', induct, ctxt4) =
    2.35 -      InductivePackage.declare_rules kind rec_name coind no_ind cnames
    2.36 +      InductivePackage.declare_rules kind group rec_name coind no_ind cnames
    2.37        (map (to_set [] (Context.Proof ctxt3)) intrs) intr_names intr_atts
    2.38        (map (fn th => (to_set [] (Context.Proof ctxt3) th,
    2.39           map fst (fst (RuleCases.get th)))) elims)