hierarchically inclusive named theorem collections
authorhaftmann
Tue Apr 16 19:50:30 2019 +0000 (7 days ago)
changeset 70177b67bab2b132c
parent 70176 330382e284a4
child 70178 4900351361b0
child 70180 5beca7396282
hierarchically inclusive named theorem collections
src/HOL/Eisbach/method_closure.ML
src/Pure/Pure.thy
src/Pure/Tools/named_theorems.ML
src/Tools/atomize_elim.ML
     1.1 --- a/src/HOL/Eisbach/method_closure.ML	Tue Apr 16 19:50:21 2019 +0000
     1.2 +++ b/src/HOL/Eisbach/method_closure.ML	Tue Apr 16 19:50:30 2019 +0000
     1.3 @@ -182,7 +182,7 @@
     1.4        |> Local_Theory.map_background_naming (Name_Space.add_path (Binding.name_of name))
     1.5        |> Config.put Method.old_section_parser true
     1.6        |> fold setup_local_method methods
     1.7 -      |> fold_map (fn b => Named_Theorems.declare b "") uses;
     1.8 +      |> fold_map (fn b => Named_Theorems.declare b [] "") uses;
     1.9  
    1.10      val (term_args, lthy2) = lthy1
    1.11        |> add_fixes vars |-> fold_map Proof_Context.inferred_param |>> map Free;
     2.1 --- a/src/Pure/Pure.thy	Tue Apr 16 19:50:21 2019 +0000
     2.2 +++ b/src/Pure/Pure.thy	Tue Apr 16 19:50:30 2019 +0000
     2.3 @@ -545,8 +545,9 @@
     2.4  val _ =
     2.5    Outer_Syntax.local_theory \<^command_keyword>\<open>named_theorems\<close>
     2.6      "declare named collection of theorems"
     2.7 -    (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >>
     2.8 -      fold (fn (b, descr) => snd o Named_Theorems.declare b descr));
     2.9 +    (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text ""
    2.10 +      -- Scan.optional (\<^keyword>\<open>includes\<close> |-- Scan.repeat1 Parse.text) []) >>
    2.11 +      fold (fn ((b, descr), extends) => snd o Named_Theorems.declare b extends descr));
    2.12  
    2.13  in end\<close>
    2.14  
     3.1 --- a/src/Pure/Tools/named_theorems.ML	Tue Apr 16 19:50:21 2019 +0000
     3.2 +++ b/src/Pure/Tools/named_theorems.ML	Tue Apr 16 19:50:30 2019 +0000
     3.3 @@ -14,7 +14,8 @@
     3.4    val add: string -> attribute
     3.5    val del: string -> attribute
     3.6    val check: Proof.context -> string * Position.T -> string
     3.7 -  val declare: binding -> string -> local_theory -> string * local_theory
     3.8 +  val declare: binding -> string list -> string ->
     3.9 +    local_theory -> string * local_theory
    3.10  end;
    3.11  
    3.12  structure Named_Theorems: NAMED_THEOREMS =
    3.13 @@ -87,15 +88,17 @@
    3.14  
    3.15  (* declaration *)
    3.16  
    3.17 -fun declare binding descr lthy =
    3.18 +fun declare binding raw_extends descr lthy =
    3.19    let
    3.20      val name = Local_Theory.full_name lthy binding;
    3.21 +    val extends = map (fn s => check lthy (s, Position.none)) raw_extends;
    3.22      val description =
    3.23        "declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr);
    3.24      val lthy' = lthy
    3.25        |> Local_Theory.background_theory (Context.theory_map (new_entry name))
    3.26        |> Local_Theory.map_contexts (K (Context.proof_map (new_entry name)))
    3.27 -      |> Local_Theory.add_thms_dynamic (binding, fn context => content context name)
    3.28 +      |> Local_Theory.add_thms_dynamic (binding,
    3.29 +           fn context => maps (content context) (extends @ [name]))
    3.30        |> Attrib.local_setup binding (Attrib.add_del (add name) (del name)) description
    3.31    in (name, lthy') end;
    3.32  
     4.1 --- a/src/Tools/atomize_elim.ML	Tue Apr 16 19:50:21 2019 +0000
     4.2 +++ b/src/Tools/atomize_elim.ML	Tue Apr 16 19:50:30 2019 +0000
     4.3 @@ -19,7 +19,7 @@
     4.4  val named_theorems =
     4.5    Context.>>> (Context.map_theory_result
     4.6     (Named_Target.theory_init #>
     4.7 -    Named_Theorems.declare \<^binding>\<open>atomize_elim\<close> "atomize_elim rewrite rule" ##>
     4.8 +    Named_Theorems.declare \<^binding>\<open>atomize_elim\<close> [] "atomize_elim rewrite rule" ##>
     4.9      Local_Theory.exit_global));
    4.10  
    4.11