src/HOL/Tools/inductive_package.ML
changeset 18728 6790126ab5f6
parent 18708 4b3dadb4fe33
child 18787 5784fe1b5657
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -38,16 +38,16 @@
     1.4       intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}) option
     1.5    val the_mk_cases: theory -> string -> string -> thm
     1.6    val print_inductives: theory -> unit
     1.7 -  val mono_add_global: theory attribute
     1.8 -  val mono_del_global: theory attribute
     1.9 +  val mono_add: attribute
    1.10 +  val mono_del: attribute
    1.11    val get_monos: theory -> thm list
    1.12    val inductive_forall_name: string
    1.13    val inductive_forall_def: thm
    1.14    val rulify: thm -> thm
    1.15    val inductive_cases: ((bstring * Attrib.src list) * string list) list -> theory -> theory
    1.16 -  val inductive_cases_i: ((bstring * theory attribute list) * term list) list -> theory -> theory
    1.17 +  val inductive_cases_i: ((bstring * attribute list) * term list) list -> theory -> theory
    1.18    val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
    1.19 -    ((bstring * term) * theory attribute list) list -> thm list -> theory -> theory *
    1.20 +    ((bstring * term) * attribute list) list -> thm list -> theory -> theory *
    1.21        {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    1.22         intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    1.23    val add_inductive: bool -> bool -> string list ->
    1.24 @@ -128,7 +128,7 @@
    1.25  (** monotonicity rules **)
    1.26  
    1.27  val get_monos = #2 o InductiveData.get;
    1.28 -fun map_monos f = InductiveData.map (Library.apsnd f);
    1.29 +val map_monos = Context.map_theory o InductiveData.map o Library.apsnd;
    1.30  
    1.31  fun mk_mono thm =
    1.32    let
    1.33 @@ -148,12 +148,8 @@
    1.34  
    1.35  (* attributes *)
    1.36  
    1.37 -fun mono_add_global (thy, thm) = (map_monos (Drule.add_rules (mk_mono thm)) thy, thm);
    1.38 -fun mono_del_global (thy, thm) = (map_monos (Drule.del_rules (mk_mono thm)) thy, thm);
    1.39 -
    1.40 -val mono_attr =
    1.41 - (Attrib.add_del_args mono_add_global mono_del_global,
    1.42 -  Attrib.add_del_args Attrib.undef_local_attribute Attrib.undef_local_attribute);
    1.43 +val mono_add = Thm.declaration_attribute (map_monos o Drule.add_rules o mk_mono);
    1.44 +val mono_del = Thm.declaration_attribute (map_monos o Drule.del_rules o mk_mono);
    1.45  
    1.46  
    1.47  
    1.48 @@ -435,12 +431,11 @@
    1.49        thy
    1.50        |> Theory.parent_path
    1.51        |> Theory.add_path (Sign.base_name name)
    1.52 -      |> PureThy.add_thms [(("cases", elim), [Attrib.theory (InductAttrib.cases_set name)])] |> snd
    1.53 +      |> PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set name])] |> snd
    1.54        |> Theory.restore_naming thy;
    1.55      val cases_specs = if no_elim then [] else map2 cases_spec names elims;
    1.56  
    1.57 -    val induct_att =
    1.58 -      Attrib.theory o (if coind then InductAttrib.coinduct_set else InductAttrib.induct_set);
    1.59 +    val induct_att = if coind then InductAttrib.coinduct_set else InductAttrib.induct_set;
    1.60      val induct_specs =
    1.61        if no_induct then I
    1.62        else
    1.63 @@ -577,7 +572,7 @@
    1.64       ((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props));
    1.65    in thy |> IsarThy.theorems_i Drule.lemmaK facts |> snd end;
    1.66  
    1.67 -val inductive_cases = gen_inductive_cases Attrib.global_attribute ProofContext.read_prop;
    1.68 +val inductive_cases = gen_inductive_cases Attrib.attribute ProofContext.read_prop;
    1.69  val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop;
    1.70  
    1.71  
    1.72 @@ -852,7 +847,7 @@
    1.73      fun read_rule s = Thm.read_cterm thy (s, propT)
    1.74        handle ERROR msg => cat_error msg ("The error(s) above occurred for " ^ s);
    1.75      val intr_ts = map (Thm.term_of o read_rule o snd o fst) intro_srcs;
    1.76 -    val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
    1.77 +    val intr_atts = map (map (Attrib.attribute thy) o snd) intro_srcs;
    1.78      val (cs', intr_ts') = unify_consts thy cs intr_ts;
    1.79  
    1.80      val (monos, thy') = thy |> IsarThy.apply_theorems raw_monos;
    1.81 @@ -871,7 +866,8 @@
    1.82    InductiveData.init #>
    1.83    Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
    1.84      "dynamic case analysis on sets")] #>
    1.85 -  Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")];
    1.86 +  Attrib.add_attributes [("mono", Attrib.add_del_args mono_add mono_del,
    1.87 +    "declaration of monotonicity rule")];
    1.88  
    1.89  
    1.90  (* outer syntax *)