inductive package: simplified group handling;
authorwenzelm
Mon Feb 25 16:31:15 2008 +0100 (2008-02-25)
changeset 26128fe2d24c26e0c
parent 26127 70ef56eb650a
child 26129 14f6dbb195c4
inductive package: simplified group handling;
src/HOL/Nominal/nominal_package.ML
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/inductive_set_package.ML
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Mon Feb 25 12:05:58 2008 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Mon Feb 25 16:31:15 2008 +0100
     1.3 @@ -563,12 +563,12 @@
     1.4  
     1.5      val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
     1.6        setmp InductivePackage.quiet_mode false
     1.7 -        (InductivePackage.add_inductive_global {verbose = false, kind = Thm.internalK,
     1.8 -            group = serial_string (),  (* FIXME pass proper group (!?) *)
     1.9 +        (InductivePackage.add_inductive_global (serial_string ())
    1.10 +          {verbose = false, kind = Thm.internalK,
    1.11              alt_name = big_rep_name, coind = false, no_elim = true, no_ind = false}
    1.12 -           (map (fn (s, T) => ((s, T --> HOLogic.boolT), NoSyn))
    1.13 -              (rep_set_names' ~~ recTs'))
    1.14 -           [] (map (fn x => (("", []), x)) intr_ts) []) thy3;
    1.15 +          (map (fn (s, T) => ((s, T --> HOLogic.boolT), NoSyn))
    1.16 +             (rep_set_names' ~~ recTs'))
    1.17 +          [] (map (fn x => (("", []), x)) intr_ts) []) thy3;
    1.18  
    1.19      (**** Prove that representing set is closed under permutation ****)
    1.20  
    1.21 @@ -1488,12 +1488,12 @@
    1.22      val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
    1.23        thy10 |>
    1.24        setmp InductivePackage.quiet_mode (!quiet_mode)
    1.25 -        (InductivePackage.add_inductive_global {verbose = false, kind = Thm.internalK,
    1.26 -            group = serial_string (),  (* FIXME pass proper group (!?) *)
    1.27 +        (InductivePackage.add_inductive_global (serial_string ())
    1.28 +          {verbose = false, kind = Thm.internalK,
    1.29              alt_name = big_rec_name, coind = false, no_elim = false, no_ind = false}
    1.30 -           (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
    1.31 -           (map dest_Free rec_fns)
    1.32 -           (map (fn x => (("", []), x)) rec_intr_ts) []) ||>
    1.33 +          (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
    1.34 +          (map dest_Free rec_fns)
    1.35 +          (map (fn x => (("", []), x)) rec_intr_ts) []) ||>
    1.36        PureThy.hide_thms true [NameSpace.append
    1.37          (Sign.full_name thy10 big_rec_name) "induct"];
    1.38  
     2.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Mon Feb 25 12:05:58 2008 +0100
     2.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Mon Feb 25 16:31:15 2008 +0100
     2.3 @@ -155,12 +155,12 @@
     2.4  
     2.5      val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
     2.6        setmp InductivePackage.quiet_mode (!quiet_mode)
     2.7 -        (InductivePackage.add_inductive_global {verbose = false, kind = Thm.internalK,
     2.8 -            group = serial_string (),  (* FIXME pass proper group (!?) *)
     2.9 -            alt_name = big_rec_name', coind = false, no_elim = false, no_ind = true}
    2.10 -           (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
    2.11 -           (map dest_Free rec_fns)
    2.12 -           (map (fn x => (("", []), x)) rec_intr_ts) []) thy0;
    2.13 +        (InductivePackage.add_inductive_global (serial_string ())
    2.14 +          {verbose = false, kind = Thm.internalK, alt_name = big_rec_name',
    2.15 +            coind = false, no_elim = false, no_ind = true}
    2.16 +          (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
    2.17 +          (map dest_Free rec_fns)
    2.18 +          (map (fn x => (("", []), x)) rec_intr_ts) []) thy0;
    2.19  
    2.20      (* prove uniqueness and termination of primrec combinators *)
    2.21  
     3.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Mon Feb 25 12:05:58 2008 +0100
     3.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Mon Feb 25 16:31:15 2008 +0100
     3.3 @@ -177,11 +177,11 @@
     3.4  
     3.5      val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
     3.6        setmp InductivePackage.quiet_mode (! quiet_mode)
     3.7 -        (InductivePackage.add_inductive_global {verbose = false, kind = Thm.internalK,
     3.8 -            group = serial_string (),  (* FIXME pass proper group (!?) *)
     3.9 -            alt_name = big_rec_name, coind = false, no_elim = true, no_ind = false}
    3.10 -           (map (fn s => ((s, UnivT'), NoSyn)) rep_set_names') []
    3.11 -           (map (fn x => (("", []), x)) intr_ts) []) thy1;
    3.12 +        (InductivePackage.add_inductive_global (serial_string ())
    3.13 +          {verbose = false, kind = Thm.internalK, alt_name = big_rec_name,
    3.14 +            coind = false, no_elim = true, no_ind = false}
    3.15 +          (map (fn s => ((s, UnivT'), NoSyn)) rep_set_names') []
    3.16 +          (map (fn x => (("", []), x)) intr_ts) []) thy1;
    3.17  
    3.18      (********************************* typedef ********************************)
    3.19  
     4.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Feb 25 12:05:58 2008 +0100
     4.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Feb 25 16:31:15 2008 +0100
     4.3 @@ -39,8 +39,7 @@
     4.4    val inductive_cases_i: ((bstring * Attrib.src list) * term list) list ->
     4.5      Proof.context -> thm list list * local_theory
     4.6    val add_inductive_i:
     4.7 -    {verbose: bool, kind: string, group: string, alt_name: bstring,
     4.8 -      coind: bool, no_elim: bool, no_ind: bool} ->
     4.9 +    {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} ->
    4.10      ((string * typ) * mixfix) list ->
    4.11      (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
    4.12        local_theory -> inductive_result * local_theory
    4.13 @@ -48,9 +47,8 @@
    4.14      (string * string option * mixfix) list ->
    4.15      ((bstring * Attrib.src list) * string) list -> (thmref * Attrib.src list) list ->
    4.16      local_theory -> inductive_result * local_theory
    4.17 -  val add_inductive_global:
    4.18 -    {verbose: bool, kind: string, group: string, alt_name: bstring,
    4.19 -      coind: bool, no_elim: bool, no_ind: bool} ->
    4.20 +  val add_inductive_global: string ->
    4.21 +    {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} ->
    4.22      ((string * typ) * mixfix) list -> (string * typ) list ->
    4.23      ((bstring * Attrib.src list) * term) list -> thm list -> theory -> inductive_result * theory
    4.24    val arities_of: thm -> (string * int) list
    4.25 @@ -66,13 +64,12 @@
    4.26  sig
    4.27    include BASIC_INDUCTIVE_PACKAGE
    4.28    type add_ind_def
    4.29 -  val declare_rules: string -> string -> bstring -> bool -> bool -> string list ->
    4.30 +  val declare_rules: string -> bstring -> bool -> bool -> string list ->
    4.31      thm list -> bstring list -> Attrib.src list list -> (thm * string list) list ->
    4.32      thm -> local_theory -> thm list * thm list * thm * local_theory
    4.33    val add_ind_def: add_ind_def
    4.34    val gen_add_inductive_i: add_ind_def ->
    4.35 -    {verbose: bool, kind: string, group: string, alt_name: bstring,
    4.36 -      coind: bool, no_elim: bool, no_ind: bool} ->
    4.37 +    {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} ->
    4.38      ((string * typ) * mixfix) list ->
    4.39      (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
    4.40        local_theory -> inductive_result * local_theory
    4.41 @@ -588,8 +585,7 @@
    4.42  
    4.43  (** specification of (co)inductive predicates **)
    4.44  
    4.45 -fun mk_ind_def group alt_name coind cs intr_ts monos
    4.46 -      params cnames_syn ctxt =
    4.47 +fun mk_ind_def alt_name coind cs intr_ts monos params cnames_syn ctxt =
    4.48    let
    4.49      val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp};
    4.50  
    4.51 @@ -647,7 +643,7 @@
    4.52        space_implode "_" (map fst cnames_syn) else alt_name;
    4.53  
    4.54      val ((rec_const, (_, fp_def)), ctxt') = ctxt |>
    4.55 -      LocalTheory.define_grouped Thm.internalK group
    4.56 +      LocalTheory.define Thm.internalK
    4.57          ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
    4.58           (("", []), fold_rev lambda params
    4.59             (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)));
    4.60 @@ -664,7 +660,7 @@
    4.61              (list_comb (rec_const, params @ make_bool_args' bs i @
    4.62                make_args argTs (xs ~~ Ts)))))
    4.63          end) (cnames_syn ~~ cs);
    4.64 -    val (consts_defs, ctxt'') = fold_map (LocalTheory.define_grouped Thm.internalK group) specs ctxt';
    4.65 +    val (consts_defs, ctxt'') = fold_map (LocalTheory.define Thm.internalK) specs ctxt';
    4.66      val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
    4.67  
    4.68      val mono = prove_mono predT fp_fun monos ctxt''
    4.69 @@ -673,7 +669,7 @@
    4.70      list_comb (rec_const, params), preds, argTs, bs, xs)
    4.71    end;
    4.72  
    4.73 -fun declare_rules kind group rec_name coind no_ind cnames intrs intr_names intr_atts
    4.74 +fun declare_rules kind rec_name coind no_ind cnames intrs intr_names intr_atts
    4.75        elims raw_induct ctxt =
    4.76    let
    4.77      val ind_case_names = RuleCases.case_names intr_names;
    4.78 @@ -688,29 +684,29 @@
    4.79  
    4.80      val (intrs', ctxt1) =
    4.81        ctxt |>
    4.82 -      LocalTheory.notes_grouped kind group
    4.83 +      LocalTheory.notes kind
    4.84          (map (NameSpace.qualified rec_name) intr_names ~~
    4.85           intr_atts ~~ map (fn th => [([th],
    4.86             [Attrib.internal (K (ContextRules.intro_query NONE))])]) intrs) |>>
    4.87        map (hd o snd);
    4.88      val (((_, elims'), (_, [induct'])), ctxt2) =
    4.89        ctxt1 |>
    4.90 -      LocalTheory.note_grouped kind group ((NameSpace.qualified rec_name "intros", []), intrs') ||>>
    4.91 +      LocalTheory.note kind ((NameSpace.qualified rec_name "intros", []), intrs') ||>>
    4.92        fold_map (fn (name, (elim, cases)) =>
    4.93 -        LocalTheory.note_grouped kind group ((NameSpace.qualified (Sign.base_name name) "cases",
    4.94 +        LocalTheory.note kind ((NameSpace.qualified (Sign.base_name name) "cases",
    4.95            [Attrib.internal (K (RuleCases.case_names cases)),
    4.96             Attrib.internal (K (RuleCases.consumes 1)),
    4.97             Attrib.internal (K (Induct.cases_pred name)),
    4.98             Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #>
    4.99          apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
   4.100 -      LocalTheory.note_grouped kind group ((NameSpace.qualified rec_name (coind_prefix coind ^ "induct"),
   4.101 +      LocalTheory.note kind ((NameSpace.qualified rec_name (coind_prefix coind ^ "induct"),
   4.102          map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
   4.103  
   4.104      val ctxt3 = if no_ind orelse coind then ctxt2 else
   4.105        let val inducts = cnames ~~ ProjectRule.projects ctxt2 (1 upto length cnames) induct'
   4.106        in
   4.107          ctxt2 |>
   4.108 -        LocalTheory.notes_grouped kind group [((NameSpace.qualified rec_name "inducts", []),
   4.109 +        LocalTheory.notes kind [((NameSpace.qualified rec_name "inducts", []),
   4.110            inducts |> map (fn (name, th) => ([th],
   4.111              [Attrib.internal (K ind_case_names),
   4.112               Attrib.internal (K (RuleCases.consumes 1)),
   4.113 @@ -719,13 +715,12 @@
   4.114    in (intrs', elims', induct', ctxt3) end;
   4.115  
   4.116  type add_ind_def =
   4.117 -  {verbose: bool, kind: string, group: string, alt_name: bstring,
   4.118 -    coind: bool, no_elim: bool, no_ind: bool} ->
   4.119 +  {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} ->
   4.120    term list -> ((string * Attrib.src list) * term) list -> thm list ->
   4.121    term list -> (string * mixfix) list ->
   4.122    local_theory -> inductive_result * local_theory
   4.123  
   4.124 -fun add_ind_def {verbose, kind, group, alt_name, coind, no_elim, no_ind}
   4.125 +fun add_ind_def {verbose, kind, alt_name, coind, no_elim, no_ind}
   4.126      cs intros monos params cnames_syn ctxt =
   4.127    let
   4.128      val _ = null cnames_syn andalso error "No inductive predicates given";
   4.129 @@ -738,8 +733,7 @@
   4.130        apfst split_list (split_list (map (check_rule ctxt cs params) intros));
   4.131  
   4.132      val (ctxt1, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
   4.133 -      argTs, bs, xs) = mk_ind_def group alt_name coind cs intr_ts
   4.134 -        monos params cnames_syn ctxt;
   4.135 +      argTs, bs, xs) = mk_ind_def alt_name coind cs intr_ts monos params cnames_syn ctxt;
   4.136  
   4.137      val (intrs, unfold) = prove_intrs coind mono fp_def (length bs + length xs)
   4.138        params intr_ts rec_preds_defs ctxt1;
   4.139 @@ -757,7 +751,7 @@
   4.140           prove_indrule cs argTs bs xs rec_const params intr_ts mono fp_def
   4.141             rec_preds_defs ctxt1);
   4.142  
   4.143 -    val (intrs', elims', induct, ctxt2) = declare_rules kind group rec_name coind no_ind
   4.144 +    val (intrs', elims', induct, ctxt2) = declare_rules kind rec_name coind no_ind
   4.145        cnames intrs intr_names intr_atts elims raw_induct ctxt1;
   4.146  
   4.147      val names = map #1 cnames_syn;
   4.148 @@ -777,7 +771,7 @@
   4.149  
   4.150  (* external interfaces *)
   4.151  
   4.152 -fun gen_add_inductive_i mk_def (flags as {verbose, kind, group, alt_name, coind, no_elim, no_ind})
   4.153 +fun gen_add_inductive_i mk_def (flags as {verbose, kind, alt_name, coind, no_elim, no_ind})
   4.154      cnames_syn pnames spec monos lthy =
   4.155    let
   4.156      val thy = ProofContext.theory_of lthy;
   4.157 @@ -841,18 +835,23 @@
   4.158      val (cs, ps) = chop (length cnames_syn) vars;
   4.159      val intrs = map (apsnd the_single) specs;
   4.160      val monos = Attrib.eval_thms lthy raw_monos;
   4.161 -    val flags = {verbose = verbose, kind = Thm.theoremK, group = serial_string (), alt_name = "",
   4.162 +    val flags = {verbose = verbose, kind = Thm.theoremK, alt_name = "",
   4.163        coind = coind, no_elim = false, no_ind = false};
   4.164 -  in gen_add_inductive_i mk_def flags cs (map fst ps) intrs monos lthy end;
   4.165 +  in
   4.166 +    lthy
   4.167 +    |> LocalTheory.set_group (serial_string ())
   4.168 +    |> gen_add_inductive_i mk_def flags cs (map fst ps) intrs monos
   4.169 +  end;
   4.170  
   4.171  val add_inductive_i = gen_add_inductive_i add_ind_def;
   4.172  val add_inductive = gen_add_inductive add_ind_def;
   4.173  
   4.174 -fun add_inductive_global flags cnames_syn pnames pre_intros monos thy =
   4.175 +fun add_inductive_global group flags cnames_syn pnames pre_intros monos thy =
   4.176    let
   4.177      val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
   4.178      val ctxt' = thy
   4.179        |> TheoryTarget.init NONE
   4.180 +      |> LocalTheory.set_group group
   4.181        |> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd
   4.182        |> LocalTheory.exit;
   4.183      val info = #2 (the_inductive ctxt' name);
     5.1 --- a/src/HOL/Tools/inductive_realizer.ML	Mon Feb 25 12:05:58 2008 +0100
     5.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Mon Feb 25 16:31:15 2008 +0100
     5.3 @@ -350,9 +350,9 @@
     5.4      (** realizability predicate **)
     5.5  
     5.6      val (ind_info, thy3') = thy2 |>
     5.7 -      InductivePackage.add_inductive_global {verbose = false, kind = Thm.theoremK,
     5.8 -          group = serial_string (),  (* FIXME pass proper group (!?) *)
     5.9 -          alt_name = "", coind = false, no_elim = false, no_ind = false}
    5.10 +      InductivePackage.add_inductive_global (serial_string ())
    5.11 +        {verbose = false, kind = Thm.theoremK, alt_name = "",
    5.12 +          coind = false, no_elim = false, no_ind = false}
    5.13          rlzpreds rlzparams (map (fn (rintr, intr) =>
    5.14            ((Sign.base_name (name_of_thm intr), []),
    5.15             subst_atomic rlzpreds' (Logic.unvarify rintr)))
     6.1 --- a/src/HOL/Tools/inductive_set_package.ML	Mon Feb 25 12:05:58 2008 +0100
     6.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Mon Feb 25 16:31:15 2008 +0100
     6.3 @@ -12,8 +12,7 @@
     6.4    val to_pred_att: thm list -> attribute
     6.5    val pred_set_conv_att: attribute
     6.6    val add_inductive_i:
     6.7 -    {verbose: bool, kind: string, group: string, alt_name: bstring,
     6.8 -      coind: bool, no_elim: bool, no_ind: bool} ->
     6.9 +    {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} ->
    6.10      ((string * typ) * mixfix) list ->
    6.11      (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
    6.12        local_theory -> InductivePackage.inductive_result * local_theory
    6.13 @@ -402,7 +401,7 @@
    6.14  
    6.15  (**** definition of inductive sets ****)
    6.16  
    6.17 -fun add_ind_set_def {verbose, kind, group, alt_name, coind, no_elim, no_ind}
    6.18 +fun add_ind_set_def {verbose, kind, alt_name, coind, no_elim, no_ind}
    6.19      cs intros monos params cnames_syn ctxt =
    6.20    let
    6.21      val thy = ProofContext.theory_of ctxt;
    6.22 @@ -465,8 +464,7 @@
    6.23      val cnames_syn' = map (fn (s, _) => (s ^ "p", NoSyn)) cnames_syn;
    6.24      val monos' = map (to_pred [] (Context.Proof ctxt)) monos;
    6.25      val ({preds, intrs, elims, raw_induct, ...}, ctxt1) =
    6.26 -      InductivePackage.add_ind_def {verbose = verbose, kind = kind, group = group,
    6.27 -          alt_name = "",  (* FIXME pass alt_name (!?) *)
    6.28 +      InductivePackage.add_ind_def {verbose = verbose, kind = kind, alt_name = "",
    6.29            coind = coind, no_elim = no_elim, no_ind = no_ind}
    6.30          cs' intros' monos' params1 cnames_syn' ctxt;
    6.31  
    6.32 @@ -502,7 +500,7 @@
    6.33      val (intr_names, intr_atts) = split_list (map fst intros);
    6.34      val raw_induct' = to_set [] (Context.Proof ctxt3) raw_induct;
    6.35      val (intrs', elims', induct, ctxt4) =
    6.36 -      InductivePackage.declare_rules kind group rec_name coind no_ind cnames
    6.37 +      InductivePackage.declare_rules kind rec_name coind no_ind cnames
    6.38        (map (to_set [] (Context.Proof ctxt3)) intrs) intr_names intr_atts
    6.39        (map (fn th => (to_set [] (Context.Proof ctxt3) th,
    6.40           map fst (fst (RuleCases.get th)))) elims)