1(* Title: Pure/Tools/named_theorems.ML 2 Author: Makarius 3 4Named collections of theorems in canonical order. 5*) 6 7signature NAMED_THEOREMS = 8sig 9 val member: Proof.context -> string -> thm -> bool 10 val get: Proof.context -> string -> thm list 11 val clear: string -> Context.generic -> Context.generic 12 val add_thm: string -> thm -> Context.generic -> Context.generic 13 val del_thm: string -> thm -> Context.generic -> Context.generic 14 val add: string -> attribute 15 val del: string -> attribute 16 val check: Proof.context -> string * Position.T -> string 17 val declare: binding -> string -> local_theory -> string * local_theory 18end; 19 20structure Named_Theorems: NAMED_THEOREMS = 21struct 22 23(* context data *) 24 25structure Data = Generic_Data 26( 27 type T = thm Item_Net.T Symtab.table; 28 val empty: T = Symtab.empty; 29 val extend = I; 30 val merge : T * T -> T = Symtab.join (K Item_Net.merge); 31); 32 33fun new_entry name = 34 Data.map (fn data => 35 if Symtab.defined data name 36 then error ("Duplicate declaration of named theorems: " ^ quote name) 37 else Symtab.update (name, Thm.full_rules) data); 38 39fun undeclared name = "Undeclared named theorems " ^ quote name; 40 41val defined_entry = Symtab.defined o Data.get; 42 43fun the_entry context name = 44 (case Symtab.lookup (Data.get context) name of 45 NONE => error (undeclared name) 46 | SOME entry => entry); 47 48fun map_entry name f context = 49 (the_entry context name; Data.map (Symtab.map_entry name f) context); 50 51 52(* maintain content *) 53 54fun member ctxt = Item_Net.member o the_entry (Context.Proof ctxt); 55 56fun content context = 57 rev o map (Thm.transfer'' context) o Item_Net.content o the_entry context; 58 59val get = content o Context.Proof; 60 61fun clear name = map_entry name (K Thm.full_rules); 62 63fun add_thm name th = map_entry name (Item_Net.update (Thm.trim_context th)); 64fun del_thm name = map_entry name o Item_Net.remove; 65 66val add = Thm.declaration_attribute o add_thm; 67val del = Thm.declaration_attribute o del_thm; 68 69 70(* check *) 71 72fun check ctxt (xname, pos) = 73 let 74 val context = Context.Proof ctxt; 75 val fact_ref = Facts.Named ((xname, Position.none), NONE); 76 fun err () = 77 let 78 val space = Facts.space_of (Proof_Context.facts_of ctxt); 79 val completion = Name_Space.completion context space (defined_entry context) (xname, pos); 80 in error (undeclared xname ^ Position.here pos ^ Completion.markup_report [completion]) end; 81 in 82 (case try (Proof_Context.get_fact_generic context) fact_ref of 83 SOME (SOME name, _) => if defined_entry context name then name else err () 84 | _ => err ()) 85 end; 86 87 88(* declaration *) 89 90fun declare binding descr lthy = 91 let 92 val name = Local_Theory.full_name lthy binding; 93 val description = 94 "declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr); 95 val lthy' = lthy 96 |> Local_Theory.background_theory (Context.theory_map (new_entry name)) 97 |> Local_Theory.map_contexts (K (Context.proof_map (new_entry name))) 98 |> Local_Theory.add_thms_dynamic (binding, fn context => content context name) 99 |> Attrib.local_setup binding (Attrib.add_del (add name) (del name)) description 100 in (name, lthy') end; 101 102 103(* ML antiquotation *) 104 105val _ = Theory.setup 106 (ML_Antiquotation.inline_embedded \<^binding>\<open>named_theorems\<close> 107 (Args.context -- Scan.lift Args.embedded_position >> 108 (fn (ctxt, name) => ML_Syntax.print_string (check ctxt name)))); 109 110end; 111