src/Pure/Isar/locale.ML
changeset 29361 764d51ab0198
child 29363 c1f024b4d76d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Isar/locale.ML	Mon Jan 05 15:55:51 2009 +0100
     1.3 @@ -0,0 +1,531 @@
     1.4 +(*  Title:      Pure/Isar/locale.ML
     1.5 +    Author:     Clemens Ballarin, TU Muenchen
     1.6 +
     1.7 +Locales -- Isar proof contexts as meta-level predicates, with local
     1.8 +syntax and implicit structures.
     1.9 +
    1.10 +Draws basic ideas from Florian Kammueller's original version of
    1.11 +locales, but uses the richer infrastructure of Isar instead of the raw
    1.12 +meta-logic.  Furthermore, structured import of contexts (with merge
    1.13 +and rename operations) are provided, as well as type-inference of the
    1.14 +signature parts, and predicate definitions of the specification text.
    1.15 +
    1.16 +Interpretation enables the reuse of theorems of locales in other
    1.17 +contexts, namely those defined by theories, structured proofs and
    1.18 +locales themselves.
    1.19 +
    1.20 +See also:
    1.21 +
    1.22 +[1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar.
    1.23 +    In Stefano Berardi et al., Types for Proofs and Programs: International
    1.24 +    Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004.
    1.25 +[2] Clemens Ballarin. Interpretation of Locales in Isabelle: Managing
    1.26 +    Dependencies between Locales. Technical Report TUM-I0607, Technische
    1.27 +    Universitaet Muenchen, 2006.
    1.28 +[3] Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and
    1.29 +    Proof Contexts. In J.M. Borwein and W.M. Farmer, MKM 2006, LNAI 4108,
    1.30 +    pages 31-43, 2006.
    1.31 +*)
    1.32 +
    1.33 +signature LOCALE =
    1.34 +sig
    1.35 +  type locale
    1.36 +
    1.37 +  val test_locale: theory -> string -> bool
    1.38 +  val register_locale: bstring ->
    1.39 +    (string * sort) list * (Binding.T * typ option * mixfix) list ->
    1.40 +    term option * term list ->
    1.41 +    (declaration * stamp) list * (declaration * stamp) list ->
    1.42 +    ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list ->
    1.43 +    ((string * Morphism.morphism) * stamp) list -> theory -> theory
    1.44 +
    1.45 +  (* Locale name space *)
    1.46 +  val intern: theory -> xstring -> string
    1.47 +  val extern: theory -> string -> xstring
    1.48 +
    1.49 +  (* Specification *)
    1.50 +  val params_of: theory -> string -> (Binding.T * typ option * mixfix) list
    1.51 +  val instance_of: theory -> string -> Morphism.morphism -> term list
    1.52 +  val specification_of: theory -> string -> term option * term list
    1.53 +  val declarations_of: theory -> string -> declaration list * declaration list
    1.54 +
    1.55 +  (* Storing results *)
    1.56 +  val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
    1.57 +    Proof.context -> Proof.context
    1.58 +  val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
    1.59 +  val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
    1.60 +  val add_declaration: string -> declaration -> Proof.context -> Proof.context
    1.61 +  val add_dependency: string -> (string * Morphism.morphism) -> theory -> theory
    1.62 +
    1.63 +  (* Activation *)
    1.64 +  val activate_declarations: theory -> string * Morphism.morphism ->
    1.65 +    Proof.context -> Proof.context
    1.66 +  val activate_global_facts: string * Morphism.morphism -> theory -> theory
    1.67 +  val activate_local_facts: string * Morphism.morphism -> Proof.context -> Proof.context
    1.68 +  val init: string -> theory -> Proof.context
    1.69 +
    1.70 +  (* Reasoning about locales *)
    1.71 +  val witness_attrib: attribute
    1.72 +  val intro_attrib: attribute
    1.73 +  val unfold_attrib: attribute
    1.74 +  val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
    1.75 +
    1.76 +  (* Registrations *)
    1.77 +  val add_global_registration: (string * (Morphism.morphism * Morphism.morphism)) ->
    1.78 +    theory -> theory
    1.79 +  val amend_global_registration: Morphism.morphism -> (string * Morphism.morphism) ->
    1.80 +    theory -> theory
    1.81 +  val get_global_registrations: theory -> (string * Morphism.morphism) list
    1.82 +
    1.83 +  (* Diagnostic *)
    1.84 +  val print_locales: theory -> unit
    1.85 +  val print_locale: theory -> bool -> bstring -> unit
    1.86 +end;
    1.87 +
    1.88 +
    1.89 +(*** Theorem list extensible via attribute --- to control intro_locales_tac ***)
    1.90 +
    1.91 +(* FIXME: consider moving named_thms.ML up in the build hierarchy and using that *)
    1.92 +functor ThmsFun() =
    1.93 +struct
    1.94 +
    1.95 +structure Data = GenericDataFun
    1.96 +(
    1.97 +  type T = thm list;
    1.98 +  val empty = [];
    1.99 +  val extend = I;
   1.100 +  fun merge _ = Thm.merge_thms;
   1.101 +);
   1.102 +
   1.103 +val get = Data.get o Context.Proof;
   1.104 +val add = Thm.declaration_attribute (Data.map o Thm.add_thm);
   1.105 +
   1.106 +end;
   1.107 +
   1.108 +
   1.109 +structure Locale: LOCALE =
   1.110 +struct
   1.111 +
   1.112 +datatype ctxt = datatype Element.ctxt;
   1.113 +
   1.114 +
   1.115 +(*** Basics ***)
   1.116 +
   1.117 +datatype locale = Loc of {
   1.118 +  (* extensible lists are in reverse order: decls, notes, dependencies *)
   1.119 +  parameters: (string * sort) list * (Binding.T * typ option * mixfix) list,
   1.120 +    (* type and term parameters *)
   1.121 +  spec: term option * term list,
   1.122 +    (* assumptions (as a single predicate expression) and defines *)
   1.123 +  decls: (declaration * stamp) list * (declaration * stamp) list,
   1.124 +    (* type and term syntax declarations *)
   1.125 +  notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list,
   1.126 +    (* theorem declarations *)
   1.127 +  dependencies: ((string * Morphism.morphism) * stamp) list
   1.128 +    (* locale dependencies (sublocale relation) *)
   1.129 +}
   1.130 +
   1.131 +
   1.132 +(*** Theory data ***)
   1.133 +
   1.134 +structure LocalesData = TheoryDataFun
   1.135 +(
   1.136 +  type T = NameSpace.T * locale Symtab.table;
   1.137 +    (* locale namespace and locales of the theory *)
   1.138 +
   1.139 +  val empty = NameSpace.empty_table;
   1.140 +  val copy = I;
   1.141 +  val extend = I;
   1.142 +
   1.143 +  fun join_locales _
   1.144 +   (Loc {parameters, spec, decls = (decls1, decls2), notes, dependencies},
   1.145 +    Loc {decls = (decls1', decls2'), notes = notes', dependencies = dependencies', ...}) =
   1.146 +      Loc {
   1.147 +        parameters = parameters,
   1.148 +        spec = spec,
   1.149 +        decls =
   1.150 +         (merge (eq_snd op =) (decls1, decls1'),
   1.151 +          merge (eq_snd op =) (decls2, decls2')),
   1.152 +        notes = merge (eq_snd op =) (notes, notes'),
   1.153 +        dependencies = merge (eq_snd op =) (dependencies, dependencies')};
   1.154 +
   1.155 +  fun merge _ = NameSpace.join_tables join_locales;
   1.156 +);
   1.157 +
   1.158 +val intern = NameSpace.intern o #1 o LocalesData.get;
   1.159 +val extern = NameSpace.extern o #1 o LocalesData.get;
   1.160 +
   1.161 +fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy)) name;
   1.162 +
   1.163 +fun the_locale thy name = case get_locale thy name
   1.164 + of SOME loc => loc
   1.165 +  | NONE => error ("Unknown locale " ^ quote name);
   1.166 +
   1.167 +fun test_locale thy name = case get_locale thy name
   1.168 + of SOME _ => true | NONE => false;
   1.169 +
   1.170 +fun register_locale bname parameters spec decls notes dependencies thy =
   1.171 +  thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy) (Binding.name bname,
   1.172 +    Loc {parameters = parameters, spec = spec, decls = decls, notes = notes,
   1.173 +      dependencies = dependencies}) #> snd);
   1.174 +
   1.175 +fun change_locale name f thy =
   1.176 +  let
   1.177 +    val Loc {parameters, spec, decls, notes, dependencies} =
   1.178 +        the_locale thy name;
   1.179 +    val (parameters', spec', decls', notes', dependencies') =
   1.180 +      f (parameters, spec, decls, notes, dependencies);
   1.181 +  in
   1.182 +    thy
   1.183 +    |> (LocalesData.map o apsnd) (Symtab.update (name, Loc {parameters = parameters',
   1.184 +      spec = spec', decls = decls', notes = notes', dependencies = dependencies'}))
   1.185 +  end;
   1.186 +
   1.187 +fun print_locales thy =
   1.188 +  let val (space, locs) = LocalesData.get thy in
   1.189 +    Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
   1.190 +    |> Pretty.writeln
   1.191 +  end;
   1.192 +
   1.193 +
   1.194 +(*** Primitive operations ***)
   1.195 +
   1.196 +fun params_of thy name =
   1.197 +  let
   1.198 +    val Loc {parameters = (_, params), ...} = the_locale thy name
   1.199 +  in params end;
   1.200 +
   1.201 +fun instance_of thy name morph =
   1.202 +  params_of thy name |>
   1.203 +    map ((fn (b, T, _) => Free (Binding.base_name b, the T)) #> Morphism.term morph);
   1.204 +
   1.205 +fun specification_of thy name =
   1.206 +  let
   1.207 +    val Loc {spec, ...} = the_locale thy name
   1.208 +  in spec end;
   1.209 +
   1.210 +fun declarations_of thy name =
   1.211 +  let
   1.212 +    val Loc {decls, ...} = the_locale thy name
   1.213 +  in
   1.214 +    decls |> apfst (map fst) |> apsnd (map fst)
   1.215 +  end;
   1.216 +
   1.217 +
   1.218 +(*** Activate context elements of locale ***)
   1.219 +
   1.220 +(** Identifiers: activated locales in theory or proof context **)
   1.221 +
   1.222 +type identifiers = (string * term list) list;
   1.223 +
   1.224 +val empty = ([] : identifiers);
   1.225 +
   1.226 +fun ident_eq thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
   1.227 +
   1.228 +local
   1.229 +
   1.230 +datatype 'a delayed = Ready of 'a | ToDo of ('a delayed * 'a delayed);
   1.231 +
   1.232 +structure IdentifiersData = GenericDataFun
   1.233 +(
   1.234 +  type T = identifiers delayed;
   1.235 +  val empty = Ready empty;
   1.236 +  val extend = I;
   1.237 +  fun merge _ = ToDo;
   1.238 +);
   1.239 +
   1.240 +in
   1.241 +
   1.242 +fun finish thy (ToDo (i1, i2)) = merge (ident_eq thy) (finish thy i1, finish thy i2)
   1.243 +  | finish _ (Ready ids) = ids;
   1.244 +
   1.245 +val _ = Context.>> (Context.map_theory (Theory.at_begin (fn thy =>
   1.246 +  (case IdentifiersData.get (Context.Theory thy) of
   1.247 +    Ready _ => NONE |
   1.248 +    ids => SOME (Context.theory_map (IdentifiersData.put (Ready (finish thy ids))) thy))
   1.249 +  )));
   1.250 +
   1.251 +fun get_global_idents thy =
   1.252 +  let val (Ready ids) = (IdentifiersData.get o Context.Theory) thy in ids end;
   1.253 +val put_global_idents = Context.theory_map o IdentifiersData.put o Ready;
   1.254 +
   1.255 +fun get_local_idents ctxt =
   1.256 +  let val (Ready ids) = (IdentifiersData.get o Context.Proof) ctxt in ids end;
   1.257 +val put_local_idents = Context.proof_map o IdentifiersData.put o Ready;
   1.258 +
   1.259 +end;
   1.260 +
   1.261 +
   1.262 +(** Resolve locale dependencies in a depth-first fashion **)
   1.263 +
   1.264 +local
   1.265 +
   1.266 +val roundup_bound = 120;
   1.267 +
   1.268 +fun add thy depth (name, morph) (deps, marked) =
   1.269 +  if depth > roundup_bound
   1.270 +  then error "Roundup bound exceeded (sublocale relation probably not terminating)."
   1.271 +  else
   1.272 +    let
   1.273 +      val Loc {parameters = (_, params), dependencies, ...} = the_locale thy name;
   1.274 +      val instance = instance_of thy name morph;
   1.275 +    in
   1.276 +      if member (ident_eq thy) marked (name, instance)
   1.277 +      then (deps, marked)
   1.278 +      else
   1.279 +        let
   1.280 +          val dependencies' =
   1.281 +            map (fn ((name, morph'), _) => (name, morph' $>  morph)) dependencies;
   1.282 +          val marked' = (name, instance) :: marked;
   1.283 +          val (deps', marked'') = fold_rev (add thy (depth + 1)) dependencies' ([], marked');
   1.284 +        in
   1.285 +          ((name, morph) :: deps' @ deps, marked'')
   1.286 +        end
   1.287 +    end;
   1.288 +
   1.289 +in
   1.290 +
   1.291 +fun roundup thy activate_dep (name, morph) (marked, input) =
   1.292 +  let
   1.293 +    (* Find all dependencies incuding new ones (which are dependencies enriching
   1.294 +      existing registrations). *)
   1.295 +    val (dependencies, marked') = add thy 0 (name, morph) ([], empty);
   1.296 +    (* Filter out exisiting fragments. *)
   1.297 +    val dependencies' = filter_out (fn (name, morph) =>
   1.298 +      member (ident_eq thy) marked (name, instance_of thy name morph)) dependencies;
   1.299 +  in
   1.300 +    (merge (ident_eq thy) (marked, marked'), input |> fold_rev (activate_dep thy) dependencies')
   1.301 +  end;
   1.302 +
   1.303 +end;
   1.304 +
   1.305 +
   1.306 +(* Declarations, facts and entire locale content *)
   1.307 +
   1.308 +fun activate_decls thy (name, morph) ctxt =
   1.309 +  let
   1.310 +    val Loc {decls = (typ_decls, term_decls), ...} = the_locale thy name;
   1.311 +  in
   1.312 +    ctxt |> fold_rev (fn (decl, _) => Context.proof_map (decl morph)) typ_decls |>
   1.313 +      fold_rev (fn (decl, _) => Context.proof_map (decl morph)) term_decls
   1.314 +  end;
   1.315 +
   1.316 +fun activate_notes activ_elem transfer thy (name, morph) input =
   1.317 +  let
   1.318 +    val Loc {notes, ...} = the_locale thy name;
   1.319 +    fun activate ((kind, facts), _) input =
   1.320 +      let
   1.321 +        val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph))
   1.322 +      in activ_elem (Notes (kind, facts')) input end;
   1.323 +  in
   1.324 +    fold_rev activate notes input
   1.325 +  end;
   1.326 +
   1.327 +fun activate_all name thy activ_elem transfer (marked, input) =
   1.328 +  let
   1.329 +    val Loc {parameters = (_, params), spec = (asm, defs), ...} =
   1.330 +      the_locale thy name;
   1.331 +  in
   1.332 +    input |>
   1.333 +      (if not (null params) then activ_elem (Fixes params) else I) |>
   1.334 +      (* FIXME type parameters *)
   1.335 +      (if is_some asm then activ_elem (Assumes [(Attrib.empty_binding, [(the asm, [])])]) else I) |>
   1.336 +      (if not (null defs)
   1.337 +        then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
   1.338 +        else I) |>
   1.339 +      pair marked |> roundup thy (activate_notes activ_elem transfer) (name, Morphism.identity)
   1.340 +  end;
   1.341 +
   1.342 +
   1.343 +(** Public activation functions **)
   1.344 +
   1.345 +local
   1.346 +
   1.347 +fun init_global_elem (Notes (kind, facts)) thy =
   1.348 +      let
   1.349 +        val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
   1.350 +      in Old_Locale.global_note_qualified kind facts' thy |> snd end
   1.351 +
   1.352 +fun init_local_elem (Fixes fixes) ctxt = ctxt |>
   1.353 +      ProofContext.add_fixes_i fixes |> snd
   1.354 +  | init_local_elem (Assumes assms) ctxt =
   1.355 +      let
   1.356 +        val assms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) assms
   1.357 +      in
   1.358 +        ctxt |> fold Variable.auto_fixes (maps (map fst o snd) assms') |>
   1.359 +          ProofContext.add_assms_i Assumption.assume_export assms' |> snd
   1.360 +     end
   1.361 +  | init_local_elem (Defines defs) ctxt =
   1.362 +      let
   1.363 +        val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs
   1.364 +      in
   1.365 +        ctxt |> fold Variable.auto_fixes (map (fst o snd) defs') |>
   1.366 +          ProofContext.add_assms_i LocalDefs.def_export (map (fn (attn, t) => (attn, [t])) defs') |>
   1.367 +          snd
   1.368 +      end
   1.369 +  | init_local_elem (Notes (kind, facts)) ctxt =
   1.370 +      let
   1.371 +        val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts
   1.372 +      in Old_Locale.local_note_qualified kind facts' ctxt |> snd end
   1.373 +
   1.374 +fun cons_elem false (Notes notes) elems = elems
   1.375 +  | cons_elem _ elem elems = elem :: elems
   1.376 +
   1.377 +in
   1.378 +
   1.379 +fun activate_declarations thy dep ctxt =
   1.380 +  roundup thy activate_decls dep (get_local_idents ctxt, ctxt) |> uncurry put_local_idents;
   1.381 +
   1.382 +fun activate_global_facts dep thy =
   1.383 +  roundup thy (activate_notes init_global_elem Element.transfer_morphism)
   1.384 +    dep (get_global_idents thy, thy) |>
   1.385 +  uncurry put_global_idents;
   1.386 +
   1.387 +fun activate_local_facts dep ctxt =
   1.388 +  roundup (ProofContext.theory_of ctxt)
   1.389 +  (activate_notes init_local_elem (Element.transfer_morphism o ProofContext.theory_of)) dep
   1.390 +    (get_local_idents ctxt, ctxt) |>
   1.391 +  uncurry put_local_idents;
   1.392 +
   1.393 +fun init name thy =
   1.394 +  activate_all name thy init_local_elem (Element.transfer_morphism o ProofContext.theory_of)
   1.395 +    (empty, ProofContext.init thy) |>
   1.396 +  uncurry put_local_idents;
   1.397 +
   1.398 +fun print_locale thy show_facts name =
   1.399 +  let
   1.400 +    val name' = intern thy name;
   1.401 +    val ctxt = init name' thy
   1.402 +  in
   1.403 +    Pretty.big_list "locale elements:"
   1.404 +      (activate_all name' thy (cons_elem show_facts) (K (Element.transfer_morphism thy))
   1.405 +        (empty, []) |> snd |> rev |>
   1.406 +        map (Element.pretty_ctxt ctxt) |> map Pretty.chunks) |> Pretty.writeln
   1.407 +  end
   1.408 +
   1.409 +end;
   1.410 +
   1.411 +
   1.412 +(*** Registrations: interpretations in theories ***)
   1.413 +
   1.414 +(* FIXME only global variant needed *)
   1.415 +structure RegistrationsData = GenericDataFun
   1.416 +(
   1.417 +  type T = ((string * (Morphism.morphism * Morphism.morphism)) * stamp) list;
   1.418 +(* FIXME mixins need to be stamped *)
   1.419 +    (* registrations, in reverse order of declaration *)
   1.420 +  val empty = [];
   1.421 +  val extend = I;
   1.422 +  fun merge _ data : T = Library.merge (eq_snd op =) data;
   1.423 +    (* FIXME consolidate with dependencies, consider one data slot only *)
   1.424 +);
   1.425 +
   1.426 +val get_global_registrations =
   1.427 +  Context.Theory #> RegistrationsData.get #> map fst #> map (apsnd op $>);
   1.428 +
   1.429 +fun add_global reg =
   1.430 +  (Context.theory_map o RegistrationsData.map) (cons (reg, stamp ()));
   1.431 +
   1.432 +fun add_global_registration (name, (base_morph, export)) thy =
   1.433 +  roundup thy (fn _ => fn (name', morph') => fn thy => add_global (name', (morph', export)) thy)
   1.434 +    (name, base_morph) (get_global_idents thy, thy) |>
   1.435 +    snd (* FIXME ?? uncurry put_global_idents *);
   1.436 +
   1.437 +fun amend_global_registration morph (name, base_morph) thy =
   1.438 +  let
   1.439 +    val regs = (Context.Theory #> RegistrationsData.get #> map fst) thy;
   1.440 +    val base = instance_of thy name base_morph;
   1.441 +    fun match (name', (morph', _)) =
   1.442 +      name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph');
   1.443 +    val i = find_index match (rev regs);
   1.444 +    val _ = if i = ~1 then error ("No interpretation of locale " ^
   1.445 +        quote (extern thy name) ^ " and parameter instantiation " ^
   1.446 +        space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available.")
   1.447 +      else ();
   1.448 +  in
   1.449 +    (Context.theory_map o RegistrationsData.map) (nth_map (length regs - 1 - i)
   1.450 +      (fn ((name, (base, export)), stamp) => ((name, (base $> morph, export)), stamp))) thy
   1.451 +  end;
   1.452 +
   1.453 +
   1.454 +(*** Storing results ***)
   1.455 +
   1.456 +(* Theorems *)
   1.457 +
   1.458 +fun add_thmss loc kind args ctxt =
   1.459 +  let
   1.460 +    val ([Notes args'], ctxt') = Element.activate_i [Notes (kind, args)] ctxt;
   1.461 +    val ctxt'' = ctxt' |> ProofContext.theory (
   1.462 +      change_locale loc
   1.463 +        (fn (parameters, spec, decls, notes, dependencies) =>
   1.464 +          (parameters, spec, decls, (args', stamp ()) :: notes, dependencies)) #>
   1.465 +      (* Registrations *)
   1.466 +      (fn thy => fold_rev (fn (name, morph) =>
   1.467 +            let
   1.468 +              val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
   1.469 +                Attrib.map_facts (Attrib.attribute_i thy)
   1.470 +            in Old_Locale.global_note_qualified kind args'' #> snd end)
   1.471 +        (get_global_registrations thy |> filter (fn (name, _) => name = loc)) thy))
   1.472 +  in ctxt'' end;
   1.473 +
   1.474 +
   1.475 +(* Declarations *)
   1.476 +
   1.477 +local
   1.478 +
   1.479 +fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
   1.480 +
   1.481 +fun add_decls add loc decl =
   1.482 +  ProofContext.theory (change_locale loc
   1.483 +    (fn (parameters, spec, decls, notes, dependencies) =>
   1.484 +      (parameters, spec, add (decl, stamp ()) decls, notes, dependencies))) #>
   1.485 +  add_thmss loc Thm.internalK
   1.486 +    [((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
   1.487 +
   1.488 +in
   1.489 +
   1.490 +val add_type_syntax = add_decls (apfst o cons);
   1.491 +val add_term_syntax = add_decls (apsnd o cons);
   1.492 +val add_declaration = add_decls (K I);
   1.493 +
   1.494 +end;
   1.495 +
   1.496 +(* Dependencies *)
   1.497 +
   1.498 +fun add_dependency loc dep =
   1.499 +  change_locale loc
   1.500 +    (fn (parameters, spec, decls, notes, dependencies) =>
   1.501 +      (parameters, spec, decls, notes, (dep, stamp ()) :: dependencies));
   1.502 +
   1.503 +
   1.504 +(*** Reasoning about locales ***)
   1.505 +
   1.506 +(** Storage for witnesses, intro and unfold rules **)
   1.507 +
   1.508 +structure Witnesses = ThmsFun();
   1.509 +structure Intros = ThmsFun();
   1.510 +structure Unfolds = ThmsFun();
   1.511 +
   1.512 +val witness_attrib = Witnesses.add;
   1.513 +val intro_attrib = Intros.add;
   1.514 +val unfold_attrib = Unfolds.add;
   1.515 +
   1.516 +(** Tactic **)
   1.517 +
   1.518 +fun intro_locales_tac eager ctxt facts st =
   1.519 +  Method.intros_tac
   1.520 +    (Witnesses.get ctxt @ Intros.get ctxt @ (if eager then Unfolds.get ctxt else [])) facts st;
   1.521 +
   1.522 +val _ = Context.>> (Context.map_theory
   1.523 +  (Method.add_methods
   1.524 +    [("intro_locales",
   1.525 +      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt ORELSE'
   1.526 +        Old_Locale.intro_locales_tac false ctxt)),
   1.527 +      "back-chain introduction rules of locales without unfolding predicates"),
   1.528 +     ("unfold_locales",
   1.529 +      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt ORELSE'
   1.530 +        Old_Locale.intro_locales_tac true ctxt)),
   1.531 +      "back-chain all introduction rules of locales")]));
   1.532 +
   1.533 +end;
   1.534 +