generic attributes;
authorwenzelm
Tue Jan 10 19:34:04 2006 +0100 (2006-01-10)
changeset 1864389a7978f90e1
parent 18642 6954633b6a76
child 18644 b59766bc66c9
generic attributes;
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/typedef_package.ML
src/Provers/classical.ML
src/Pure/Isar/obtain.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Jan 10 19:33:42 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Jan 10 19:34:04 2006 +0100
     1.3 @@ -365,10 +365,10 @@
     1.4      fun proj i = ProjectRule.project induction (i + 1);
     1.5  
     1.6      fun named_rules (name, {index, exhaustion, ...}: datatype_info) =
     1.7 -      [(("", proj index), [InductAttrib.induct_type_global name]),
     1.8 -       (("", exhaustion), [InductAttrib.cases_type_global name])];
     1.9 +      [(("", proj index), [Attrib.theory (InductAttrib.induct_type name)]),
    1.10 +       (("", exhaustion), [Attrib.theory (InductAttrib.cases_type name)])];
    1.11      fun unnamed_rule i =
    1.12 -      (("", proj i), [Drule.kind_internal, InductAttrib.induct_type_global ""]);
    1.13 +      (("", proj i), [Drule.kind_internal, Attrib.theory (InductAttrib.induct_type "")]);
    1.14    in
    1.15      PureThy.add_thms
    1.16        (List.concat (map named_rules infos) @
     2.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Jan 10 19:33:42 2006 +0100
     2.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Jan 10 19:34:04 2006 +0100
     2.3 @@ -435,12 +435,12 @@
     2.4        thy
     2.5        |> Theory.parent_path
     2.6        |> Theory.add_path (Sign.base_name name)
     2.7 -      |> PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set_global name])] |> snd
     2.8 +      |> PureThy.add_thms [(("cases", elim), [Attrib.theory (InductAttrib.cases_set name)])] |> snd
     2.9        |> Theory.restore_naming thy;
    2.10      val cases_specs = if no_elim then [] else map2 cases_spec names elims;
    2.11  
    2.12      val induct_att =
    2.13 -      if coind then InductAttrib.coinduct_set_global else InductAttrib.induct_set_global;
    2.14 +      Attrib.theory o (if coind then InductAttrib.coinduct_set else InductAttrib.induct_set);
    2.15      val induct_specs =
    2.16        if no_induct then I
    2.17        else
     3.1 --- a/src/HOL/Tools/record_package.ML	Tue Jan 10 19:33:42 2006 +0100
     3.2 +++ b/src/HOL/Tools/record_package.ML	Tue Jan 10 19:34:04 2006 +0100
     3.3 @@ -1215,8 +1215,8 @@
     3.4  (* attributes *)
     3.5  
     3.6  fun case_names_fields x = RuleCases.case_names ["fields"] x;
     3.7 -fun induct_type_global name = [case_names_fields, InductAttrib.induct_type_global name];
     3.8 -fun cases_type_global name = [case_names_fields, InductAttrib.cases_type_global name];
     3.9 +fun induct_type_global name = [case_names_fields, Attrib.theory (InductAttrib.induct_type name)];
    3.10 +fun cases_type_global name = [case_names_fields, Attrib.theory (InductAttrib.cases_type name)];
    3.11  
    3.12  (* tactics *)
    3.13  
     4.1 --- a/src/HOL/Tools/typedef_package.ML	Tue Jan 10 19:33:42 2006 +0100
     4.2 +++ b/src/HOL/Tools/typedef_package.ML	Tue Jan 10 19:34:04 2006 +0100
     4.3 @@ -176,13 +176,17 @@
     4.4                  ((Rep_name ^ "_inject", make Rep_inject), []),
     4.5                  ((Abs_name ^ "_inject", make Abs_inject), []),
     4.6                  ((Rep_name ^ "_cases", make Rep_cases),
     4.7 -                  [RuleCases.case_names [Rep_name], InductAttrib.cases_set_global full_name]),
     4.8 +                  [RuleCases.case_names [Rep_name],
     4.9 +                    Attrib.theory (InductAttrib.cases_set full_name)]),
    4.10                  ((Abs_name ^ "_cases", make Abs_cases),
    4.11 -                  [RuleCases.case_names [Abs_name], InductAttrib.cases_type_global full_tname]),
    4.12 +                  [RuleCases.case_names [Abs_name],
    4.13 +                    Attrib.theory (InductAttrib.cases_type full_tname)]),
    4.14                  ((Rep_name ^ "_induct", make Rep_induct),
    4.15 -                  [RuleCases.case_names [Rep_name], InductAttrib.induct_set_global full_name]),
    4.16 +                  [RuleCases.case_names [Rep_name],
    4.17 +                    Attrib.theory (InductAttrib.induct_set full_name)]),
    4.18                  ((Abs_name ^ "_induct", make Abs_induct),
    4.19 -                  [RuleCases.case_names [Abs_name], InductAttrib.induct_type_global full_tname])])
    4.20 +                  [RuleCases.case_names [Abs_name],
    4.21 +                    Attrib.theory (InductAttrib.induct_type full_tname)])])
    4.22              ||> Theory.parent_path;
    4.23            val result = {type_definition = type_definition, set_def = set_def,
    4.24              Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
     5.1 --- a/src/Provers/classical.ML	Tue Jan 10 19:33:42 2006 +0100
     5.2 +++ b/src/Provers/classical.ML	Tue Jan 10 19:34:04 2006 +0100
     5.3 @@ -968,7 +968,7 @@
     5.4  val haz_dest_global = change_global_cs (op addDs);
     5.5  val haz_elim_global = change_global_cs (op addEs);
     5.6  val haz_intro_global = change_global_cs (op addIs);
     5.7 -val rule_del_global = change_global_cs (op delrules) o ContextRules.rule_del_global;
     5.8 +val rule_del_global = change_global_cs (op delrules) o Attrib.theory ContextRules.rule_del;
     5.9  
    5.10  val safe_dest_local = change_local_cs (op addSDs);
    5.11  val safe_elim_local = change_local_cs (op addSEs);
    5.12 @@ -976,7 +976,7 @@
    5.13  val haz_dest_local = change_local_cs (op addDs);
    5.14  val haz_elim_local = change_local_cs (op addEs);
    5.15  val haz_intro_local = change_local_cs (op addIs);
    5.16 -val rule_del_local = change_local_cs (op delrules) o ContextRules.rule_del_local;
    5.17 +val rule_del_local = change_local_cs (op delrules) o Attrib.context ContextRules.rule_del;
    5.18  
    5.19  
    5.20  (* tactics referring to the implicit claset *)
    5.21 @@ -1019,16 +1019,16 @@
    5.22  val setup_attrs = Attrib.add_attributes
    5.23   [("swapped", (swapped, swapped), "classical swap of introduction rule"),
    5.24    (destN,
    5.25 -   (add_rule ContextRules.dest_query_global haz_dest_global safe_dest_global,
    5.26 -    add_rule ContextRules.dest_query_local haz_dest_local safe_dest_local),
    5.27 +   (add_rule (Attrib.theory o ContextRules.dest_query) haz_dest_global safe_dest_global,
    5.28 +    add_rule (Attrib.context o ContextRules.dest_query) haz_dest_local safe_dest_local),
    5.29      "declaration of destruction rule"),
    5.30    (elimN,
    5.31 -   (add_rule ContextRules.elim_query_global haz_elim_global safe_elim_global,
    5.32 -    add_rule ContextRules.elim_query_local haz_elim_local safe_elim_local),
    5.33 +   (add_rule (Attrib.theory o ContextRules.elim_query) haz_elim_global safe_elim_global,
    5.34 +    add_rule (Attrib.context o ContextRules.elim_query) haz_elim_local safe_elim_local),
    5.35      "declaration of elimination rule"),
    5.36    (introN,
    5.37 -   (add_rule ContextRules.intro_query_global haz_intro_global safe_intro_global,
    5.38 -    add_rule ContextRules.intro_query_local haz_intro_local safe_intro_local),
    5.39 +   (add_rule (Attrib.theory o ContextRules.intro_query) haz_intro_global safe_intro_global,
    5.40 +    add_rule (Attrib.context o ContextRules.intro_query) haz_intro_local safe_intro_local),
    5.41      "declaration of introduction rule"),
    5.42    (ruleN, (del_rule rule_del_global, del_rule rule_del_local),
    5.43      "remove declaration of intro/elim/dest rule")];
     6.1 --- a/src/Pure/Isar/obtain.ML	Tue Jan 10 19:33:42 2006 +0100
     6.2 +++ b/src/Pure/Isar/obtain.ML	Tue Jan 10 19:34:04 2006 +0100
     6.3 @@ -134,7 +134,8 @@
     6.4      |> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, ([], []))])] int
     6.5      |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
     6.6      |> Proof.fix_i [([thesisN], NONE)]
     6.7 -    |> Proof.assume_i [((thatN, [ContextRules.intro_query_local NONE]), [(that_prop, ([], []))])]
     6.8 +    |> Proof.assume_i
     6.9 +      [((thatN, [Attrib.context (ContextRules.intro_query NONE)]), [(that_prop, ([], []))])]
    6.10      |> `Proof.the_facts
    6.11      ||> Proof.chain_facts chain_facts
    6.12      ||> Proof.show_i NONE after_qed [(("", []), [(thesis, ([], []))])] false
     7.1 --- a/src/ZF/Tools/inductive_package.ML	Tue Jan 10 19:33:42 2006 +0100
     7.2 +++ b/src/ZF/Tools/inductive_package.ML	Tue Jan 10 19:34:04 2006 +0100
     7.3 @@ -514,8 +514,9 @@
     7.4  
     7.5       val ([induct', mutual_induct'], thy') =
     7.6         thy
     7.7 -       |> PureThy.add_thms [((co_prefix ^ "induct", induct), [case_names, InductAttrib.induct_set_global big_rec_name]),
     7.8 -            (("mutual_induct", mutual_induct), [case_names])];
     7.9 +       |> PureThy.add_thms [((co_prefix ^ "induct", induct),
    7.10 +             [case_names, Attrib.theory (InductAttrib.induct_set big_rec_name)]),
    7.11 +           (("mutual_induct", mutual_induct), [case_names])];
    7.12      in ((thy', induct'), mutual_induct')
    7.13      end;  (*of induction_rules*)
    7.14  
    7.15 @@ -536,7 +537,7 @@
    7.16      |> PureThy.add_thms
    7.17        [(("bnd_mono", bnd_mono), []),
    7.18         (("dom_subset", dom_subset), []),
    7.19 -       (("cases", elim), [case_names, InductAttrib.cases_set_global big_rec_name])]
    7.20 +       (("cases", elim), [case_names, Attrib.theory (InductAttrib.cases_set big_rec_name)])]
    7.21      ||>> (PureThy.add_thmss o map Thm.no_attributes)
    7.22          [("defs", defs),
    7.23           ("intros", intrs)];