intrs attributes;
authorwenzelm
Tue Apr 27 10:50:31 1999 +0200 (1999-04-27)
changeset 652116c425fc00cb
parent 6520 08637598f7ec
child 6522 2f6cec5c046f
intrs attributes;
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Apr 27 10:50:08 1999 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Apr 27 10:50:31 1999 +0200
     1.3 @@ -36,11 +36,13 @@
     1.4        induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
     1.5    val print_inductives: theory -> unit
     1.6    val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
     1.7 -    ((bstring * term) * theory attribute list) list -> thm list -> thm list -> theory -> theory *
     1.8 +    theory attribute list -> ((bstring * term) * theory attribute list) list ->
     1.9 +      thm list -> thm list -> theory -> theory *
    1.10        {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    1.11         intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    1.12 -  val add_inductive: bool -> bool -> string list -> ((bstring * string) * Args.src list) list ->
    1.13 -    (xstring * Args.src list) list -> (xstring * Args.src list) list -> theory -> theory *
    1.14 +  val add_inductive: bool -> bool -> string list -> Args.src list ->
    1.15 +    ((bstring * string) * Args.src list) list -> (xstring * Args.src list) list ->
    1.16 +      (xstring * Args.src list) list -> theory -> theory *
    1.17        {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    1.18         intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    1.19    val setup: (theory -> theory) list
    1.20 @@ -452,7 +454,7 @@
    1.21  (** definitional introduction of (co)inductive sets **)
    1.22  
    1.23  fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
    1.24 -    intros monos con_defs thy params paramTs cTs cnames =
    1.25 +    atts intros monos con_defs thy params paramTs cTs cnames =
    1.26    let
    1.27      val _ = if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
    1.28        commas_quote cnames) else ();
    1.29 @@ -539,7 +541,7 @@
    1.30        else standard (raw_induct RSN (2, rev_mp));
    1.31  
    1.32      val thy'' = thy'
    1.33 -      |> PureThy.add_thmss [(("intrs", intrs), [])]
    1.34 +      |> PureThy.add_thmss [(("intrs", intrs), atts)]
    1.35        |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)
    1.36        |> (if no_elim then I else PureThy.add_thmss [(("elims", elims), [])])
    1.37        |> (if no_ind then I else PureThy.add_thms
    1.38 @@ -562,7 +564,7 @@
    1.39  (** axiomatic introduction of (co)inductive sets **)
    1.40  
    1.41  fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs
    1.42 -    intros monos con_defs thy params paramTs cTs cnames =
    1.43 +    atts intros monos con_defs thy params paramTs cTs cnames =
    1.44    let
    1.45      val _ = if verbose then message ("Adding axioms for " ^ coind_prefix coind ^
    1.46        "inductive set(s) " ^ commas_quote cnames) else ();
    1.47 @@ -581,7 +583,7 @@
    1.48                (map (fn (c, n) => (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
    1.49           else I)
    1.50        |> Theory.add_path rec_name
    1.51 -      |> PureThy.add_axiomss_i [(("intrs", intr_ts), []), (("elims", elim_ts), [])]
    1.52 +      |> PureThy.add_axiomss_i [(("intrs", intr_ts), atts), (("elims", elim_ts), [])]
    1.53        |> (if coind then I else PureThy.add_axioms_i [(("internal_induct", ind_t), [])]);
    1.54  
    1.55      val intrs = PureThy.get_thms thy' "intrs";
    1.56 @@ -612,7 +614,7 @@
    1.57  (** introduction of (co)inductive sets **)
    1.58  
    1.59  fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
    1.60 -    intros monos con_defs thy =
    1.61 +    atts intros monos con_defs thy =
    1.62    let
    1.63      val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
    1.64      val sign = Theory.sign_of thy;
    1.65 @@ -635,7 +637,7 @@
    1.66  
    1.67      val (thy1, result) =
    1.68        (if ! quick_and_dirty then add_ind_axm else add_ind_def)
    1.69 -        verbose declare_consts alt_name coind no_elim no_ind cs intros monos
    1.70 +        verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos
    1.71          con_defs thy params paramTs cTs cnames;
    1.72      val thy2 = thy1 |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result);
    1.73    in (thy2, result) end;
    1.74 @@ -644,11 +646,12 @@
    1.75  
    1.76  (** external interface **)
    1.77  
    1.78 -fun add_inductive verbose coind c_strings intro_srcs raw_monos raw_con_defs thy =
    1.79 +fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy =
    1.80    let
    1.81      val sign = Theory.sign_of thy;
    1.82      val cs = map (readtm (Theory.sign_of thy) HOLogic.termTVar) c_strings;
    1.83  
    1.84 +    val atts = map (Attrib.global_attribute thy) srcs;
    1.85      val intr_names = map (fst o fst) intro_srcs;
    1.86      val intr_ts = map (readtm (Theory.sign_of thy) propT o snd o fst) intro_srcs;
    1.87      val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
    1.88 @@ -686,7 +689,7 @@
    1.89        |> apfst (IsarThy.apply_theorems raw_con_defs);
    1.90    in
    1.91      add_inductive_i verbose false "" coind false false cs''
    1.92 -      ((intr_names ~~ intr_ts'') ~~ intr_atts) monos con_defs thy'
    1.93 +      atts ((intr_names ~~ intr_ts'') ~~ intr_atts) monos con_defs thy'
    1.94    end;
    1.95  
    1.96  
    1.97 @@ -702,12 +705,12 @@
    1.98  
    1.99  local open OuterParse in
   1.100  
   1.101 -fun mk_ind coind (((sets, intrs), monos), con_defs) =
   1.102 -  #1 o add_inductive true coind sets (map triple_swap intrs) monos con_defs;
   1.103 +fun mk_ind coind (((sets, (atts, intrs)), monos), con_defs) =
   1.104 +  #1 o add_inductive true coind sets atts (map triple_swap intrs) monos con_defs;
   1.105  
   1.106  fun ind_decl coind =
   1.107    Scan.repeat1 term --
   1.108 -  ($$$ "intrs" |-- !!! (Scan.repeat1 (opt_thm_name ":" -- term))) --
   1.109 +  ($$$ "intrs" |-- !!! (opt_attribs -- Scan.repeat1 (opt_thm_name ":" -- term))) --
   1.110    Scan.optional ($$$ "monos" |-- !!! xthms1) [] --
   1.111    Scan.optional ($$$ "con_defs" |-- !!! xthms1) []
   1.112    >> (Toplevel.theory o mk_ind coind);