inductive: no collective atts;
authorwenzelm
Fri Sep 28 19:19:26 2001 +0200 (2001-09-28)
changeset 11628e57a6e51715e
parent 11627 abf9cda4a4d2
child 11629 481148b273b5
inductive: no collective atts;
src/HOL/Isar_examples/W_correct.thy
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_package.ML
src/HOL/thy_syntax.ML
     1.1 --- a/src/HOL/Isar_examples/W_correct.thy	Fri Sep 28 19:18:46 2001 +0200
     1.2 +++ b/src/HOL/Isar_examples/W_correct.thy	Fri Sep 28 19:19:26 2001 +0200
     1.3 @@ -33,10 +33,10 @@
     1.4    "a |- e :: t" == "(a, e, t) : has_type"
     1.5  
     1.6  inductive has_type
     1.7 -  intros [simp]
     1.8 -    Var: "n < length a ==> a |- Var n :: a ! n"
     1.9 -    Abs: "t1#a |- e :: t2 ==> a |- Abs e :: t1 -> t2"
    1.10 -    App: "a |- e1 :: t2 -> t1 ==> a |- e2 :: t2
    1.11 +  intros
    1.12 +    Var [simp]: "n < length a ==> a |- Var n :: a ! n"
    1.13 +    Abs [simp]: "t1#a |- e :: t2 ==> a |- Abs e :: t1 -> t2"
    1.14 +    App [simp]: "a |- e1 :: t2 -> t1 ==> a |- e2 :: t2
    1.15        ==> a |- App e1 e2 :: t1"
    1.16  
    1.17  
     2.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Sep 28 19:18:46 2001 +0200
     2.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Fri Sep 28 19:19:26 2001 +0200
     2.3 @@ -182,7 +182,7 @@
     2.4      val (thy1, {intrs = rec_intrs, elims = rec_elims, ...}) =
     2.5        setmp InductivePackage.quiet_mode (!quiet_mode)
     2.6          (InductivePackage.add_inductive_i false true big_rec_name' false false true
     2.7 -           rec_sets [] (map (fn x => (("", x), [])) rec_intr_ts) [fun_rel_comp_mono] []) thy0;
     2.8 +           rec_sets (map (fn x => (("", x), [])) rec_intr_ts) [fun_rel_comp_mono] []) thy0;
     2.9  
    2.10      (* prove uniqueness and termination of primrec combinators *)
    2.11  
     3.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Fri Sep 28 19:18:46 2001 +0200
     3.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri Sep 28 19:19:26 2001 +0200
     3.3 @@ -175,7 +175,7 @@
     3.4      val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =
     3.5        setmp InductivePackage.quiet_mode (!quiet_mode)
     3.6          (InductivePackage.add_inductive_i false true big_rec_name false true false
     3.7 -           consts [] (map (fn x => (("", x), [])) intr_ts) [Funs_mono] []) thy1;
     3.8 +           consts (map (fn x => (("", x), [])) intr_ts) [Funs_mono] []) thy1;
     3.9  
    3.10      (********************************* typedef ********************************)
    3.11  
     4.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Sep 28 19:18:46 2001 +0200
     4.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Sep 28 19:19:26 2001 +0200
     4.3 @@ -49,11 +49,11 @@
     4.4    val inductive_cases_i: ((bstring * theory attribute list) * term list) * Comment.text
     4.5      -> theory -> theory
     4.6    val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
     4.7 -    theory attribute list -> ((bstring * term) * theory attribute list) list ->
     4.8 +    ((bstring * term) * theory attribute list) list ->
     4.9        thm list -> thm list -> theory -> theory *
    4.10        {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    4.11         intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    4.12 -  val add_inductive: bool -> bool -> string list -> Args.src list ->
    4.13 +  val add_inductive: bool -> bool -> string list ->
    4.14      ((bstring * string) * Args.src list) list -> (xstring * Args.src list) list ->
    4.15        (xstring * Args.src list) list -> theory -> theory *
    4.16        {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    4.17 @@ -741,7 +741,7 @@
    4.18    in (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) end;
    4.19  
    4.20  fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
    4.21 -    atts intros monos con_defs thy params paramTs cTs cnames induct_cases =
    4.22 +    intros monos con_defs thy params paramTs cTs cnames induct_cases =
    4.23    let
    4.24      val _ =
    4.25        if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
    4.26 @@ -772,7 +772,7 @@
    4.27      val (thy3, ([intrs'', elims'], [induct'])) =
    4.28        thy2
    4.29        |> PureThy.add_thmss
    4.30 -        [(("intros", intrs'), atts),
    4.31 +        [(("intros", intrs'), []),
    4.32            (("elims", elims), [RuleCases.consumes 1])]
    4.33        |>>> PureThy.add_thms
    4.34          [((coind_prefix coind ^ "induct", rulify induct),
    4.35 @@ -799,7 +799,7 @@
    4.36    | None => error (msg ^ Sign.string_of_term sign t));
    4.37  
    4.38  fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
    4.39 -    atts pre_intros monos con_defs thy =
    4.40 +    pre_intros monos con_defs thy =
    4.41    let
    4.42      val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
    4.43      val sign = Theory.sign_of thy;
    4.44 @@ -822,19 +822,18 @@
    4.45      val induct_cases = map (#1 o #1) intros;
    4.46  
    4.47      val (thy1, result as {elims, induct, ...}) =
    4.48 -      add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos
    4.49 +      add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs intros monos
    4.50          con_defs thy params paramTs cTs cnames induct_cases;
    4.51      val thy2 = thy1
    4.52        |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
    4.53        |> add_cases_induct no_elim (no_ind orelse coind) full_cnames elims induct;
    4.54    in (thy2, result) end;
    4.55  
    4.56 -fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy =
    4.57 +fun add_inductive verbose coind c_strings intro_srcs raw_monos raw_con_defs thy =
    4.58    let
    4.59      val sign = Theory.sign_of thy;
    4.60      val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings;
    4.61  
    4.62 -    val atts = map (Attrib.global_attribute thy) srcs;
    4.63      val intr_names = map (fst o fst) intro_srcs;
    4.64      fun read_rule s = Thm.read_cterm sign (s, propT)
    4.65        handle ERROR => error ("The error(s) above occurred for " ^ s);
    4.66 @@ -847,7 +846,7 @@
    4.67        |> apfst (IsarThy.apply_theorems raw_con_defs);
    4.68    in
    4.69      add_inductive_i verbose false "" coind false false cs'
    4.70 -      atts ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy'
    4.71 +      ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy'
    4.72    end;
    4.73  
    4.74  
    4.75 @@ -867,13 +866,13 @@
    4.76  
    4.77  local structure P = OuterParse and K = OuterSyntax.Keyword in
    4.78  
    4.79 -fun mk_ind coind (((sets, (atts, intrs)), monos), con_defs) =
    4.80 -  #1 o add_inductive true coind sets atts (map P.triple_swap intrs) monos con_defs;
    4.81 +fun mk_ind coind (((sets, intrs), monos), con_defs) =
    4.82 +  #1 o add_inductive true coind sets (map P.triple_swap intrs) monos con_defs;
    4.83  
    4.84  fun ind_decl coind =
    4.85    (Scan.repeat1 P.term --| P.marg_comment) --
    4.86    (P.$$$ "intros" |--
    4.87 -    P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
    4.88 +    P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
    4.89    Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
    4.90    Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) []
    4.91    >> (Toplevel.theory o mk_ind coind);
     5.1 --- a/src/HOL/thy_syntax.ML	Fri Sep 28 19:18:46 2001 +0200
     5.2 +++ b/src/HOL/thy_syntax.ML	Fri Sep 28 19:19:26 2001 +0200
     5.3 @@ -63,7 +63,7 @@
     5.4          \local\n\
     5.5          \val (thy, {defs, mono, unfold, intrs, elims, mk_cases, induct, ...}) =\n\
     5.6          \  InductivePackage.add_inductive true " ^
     5.7 -        (if coind then "true " else "false ") ^ srec_tms ^ " [] " ^
     5.8 +        (if coind then "true " else "false ") ^ srec_tms ^
     5.9           sintrs ^ " " ^ mk_list (no_atts monos) ^ " " ^ mk_list (no_atts con_defs) ^ " thy;\n\
    5.10          \in\n\
    5.11          \structure " ^ big_rec_name ^ " =\n\