src/Pure/Isar/locale.ML

     theory -> ((string * thm list) list * (string * thm list) list) * (Proof.context * theory)
   val add_thmss: string -> string ->
     ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
     cterm list * Proof.context ->
     ((string * thm list) list * (string * thm list) list) * Proof.context
+  val add_abbrevs: string -> bool -> (bstring * term * mixfix) list ->
+    cterm list * Proof.context -> Proof.context
 
   val theorem: string -> Method.text option -> (thm list list -> theory -> theory) ->
     string * Attrib.src list -> Element.context element list -> Element.statement ->
     theory -> Proof.state
   val theorem_i: string -> Method.text option -> (thm list list -> theory -> theory) ->

        ([statement], axioms), where statement is the locale predicate applied
        to the (assumed) locale parameters.  Axioms contains the projections
        from the locale predicate to the normalised assumptions of the locale
        (cf. [1], normalisation of locale expressions.)
     *)
-  import: expr,                                       (*dynamic import*)
-  elems: (Element.context_i * stamp) list,            (*static content*)
-  params: ((string * typ) * mixfix) list * string list,
-                                                      (*all/local params*)
+  import: expr,                                                     (*dynamic import*)
+  elems: (Element.context_i * stamp) list,                          (*static content*)
+  params: ((string * typ) * mixfix) list * string list,             (*all/local params*)
+  abbrevs: ((bool * (bstring * term * mixfix) list) * stamp) list,  (*abbreviations*)
   regs: ((string * string list) * (term * thm) list) list}
     (* Registrations: indentifiers and witness theorems of locales interpreted
        in the locale.
     *)
 

 
   val empty = (NameSpace.empty, Symtab.empty, Symtab.empty);
   val copy = I;
   val extend = I;
 
-  fun join_locs _ ({predicate, import, elems, params, regs}: locale,
-      {elems = elems', regs = regs', ...}: locale) =
-    SOME {predicate = predicate, import = import,
+  fun join_locs _ ({predicate, import, elems, params, abbrevs, regs}: locale,
+      {elems = elems', abbrevs = abbrevs', regs = regs', ...}: locale) =
+    SOME
+     {predicate = predicate,
+      import = import,
       elems = gen_merge_lists (eq_snd (op =)) elems elems',
       params = params,
+      abbrevs = Library.merge (eq_snd (op =)) (abbrevs, abbrevs'),
       regs = merge_alists regs regs'};
   fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) =
     (NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2),
      Symtab.join (K (SOME o Registrations.join)) (regs1, regs2));
 

     SOME loc => loc
   | NONE => error ("Unknown locale " ^ quote name));
 
 fun change_locale name f thy =
   let
-    val {predicate, import, elems , params, regs} = the_locale thy name;
-    val (predicate', import', elems', params', regs') = f (predicate, import, elems, params, regs);
+    val {predicate, import, elems , params, abbrevs, regs} = the_locale thy name;
+    val (predicate', import', elems', params', abbrevs', regs') =
+      f (predicate, import, elems, params, abbrevs, regs);
   in
     put_locale name {predicate = predicate', import = import', elems = elems',
-      params = params', regs = regs'} thy
+      params = params', abbrevs = abbrevs', regs = regs'} thy
   end;
 
 
 (* access registrations *)
 

        GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, f regs))) I;
 val put_local_registration =
      gen_put_registration LocalLocalesData.map ProofContext.theory_of;
 
 fun put_registration_in_locale name id =
-  change_locale name (fn (predicate, import, elems, params, regs) =>
-    (predicate, import, elems, params, regs @ [(id, [])]));
+  change_locale name (fn (predicate, import, elems, params, abbrevs, regs) =>
+    (predicate, import, elems, params, abbrevs, regs @ [(id, [])]));
 
 
 (* add witness theorem to registration in theory or context,
    ignored if registration not present *)
 

   GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, add_witness id thm regs));
 
 val add_local_witness = LocalLocalesData.map oo add_witness;
 
 fun add_witness_in_locale name id thm =
-  change_locale name (fn (predicate, import, elems, params, regs) =>
+  change_locale name (fn (predicate, import, elems, params, abbrevs, regs) =>
     let
       fun add (id', thms) =
         if id = id' then (id', thm :: thms) else (id', thms);
-    in (predicate, import, elems, params, map add regs) end);
+    in (predicate, import, elems, params, abbrevs, map add regs) end);
 
 
 (* printing of registrations *)
 
 fun gen_print_registrations get_regs mk_ctxt msg show_wits loc thy_ctxt =

           val {elems, ...} = the_locale thy name;
           val ts = List.concat (map
             (fn (Assumes asms, _) => List.concat (map (map #1 o #2) asms)
               | _ => [])
             elems);
-          val (axs1, axs2) = splitAt (length ts, axioms);
+          val (axs1, axs2) = chop (length ts) axioms;
         in (((name, parms), (all_ps, Assumed axs1)), axs2) end
       | axiomify all_ps (id, (_, Derived ths)) axioms =
           ((id, (all_ps, Derived ths)), axioms);
 
     (* identifiers of an expression *)

       ((ctxt, mode), [])
   | activate_elem _ ((ctxt, Assumed axs), Assumes asms) =
       let
         val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
         val ts = List.concat (map (map #1 o #2) asms');
-        val (ps, qs) = splitAt (length ts, axs);
+        val (ps, qs) = chop (length ts) axs;
         val (_, ctxt') =
           ctxt |> fold ProofContext.fix_frees ts
           |> ProofContext.add_assms_i (axioms_export ps) asms';
       in ((ctxt', Assumed qs), []) end
   | activate_elem _ ((ctxt, Derived ths), Assumes asms) =

         (* CB: add type information from conclusion and external elements to context *)
         val ctxt = fold ProofContext.declare_term (List.concat (map (map fst) all_propp)) ctxt;
         (* CB: resolve schematic variables (patterns) in conclusion and external elements. *)
         val all_propp' = map2 (curry (op ~~))
           (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp);
-        val (concl, propp) = splitAt (length raw_concl, all_propp')
+        val (concl, propp) = chop (length raw_concl) all_propp';
       in (propp, (ctxt, concl)) end
 
     val (proppss, (ctxt, concl)) =
       (fold_burrow o fold_burrow) prep_prop raw_proppss (raw_ctxt, raw_concl);
 

     val all_elemss' = map (fn (((_, ps), _), (((n, ps'), mode), elems)) =>
         (((n, map (fn p => (p, (the o AList.lookup (op =) ps') p)) ps), mode), elems))
       (ids ~~ all_elemss);
 
     (* CB: all_elemss and parms contain the correct parameter types *)
-    val (ps,qs) = splitAt(length raw_import_elemss, all_elemss')
+    val (ps, qs) = chop (length raw_import_elemss) all_elemss';
     val (import_ctxt, (import_elemss, _)) =
       activate_facts prep_facts (context, ps);
 
     val (ctxt, (elemss, _)) =
       activate_facts prep_facts (import_ctxt, qs);

 fun cert_context import body ctxt = #1 (cert_ctxt true [] import (map Elem body) [] ctxt);
 
 val read_context_statement = prep_statement intern read_ctxt;
 val cert_context_statement = prep_statement (K I) cert_ctxt;
 
-fun init loc thy = #2 (cert_context_statement (SOME loc) [] [] (ProofContext.init thy));
-
 end;
 
 
 (* print locale *)
 

 
 
 
 (** store results **)
 
-(* accesses of interpreted theorems *)
-
-local
-
-(*fully qualified name in theory is T.p.r.n where
-  T: theory name, p: interpretation prefix, r: renaming prefix, n: name*)  (* FIXME not necessarily so *)
-fun global_accesses _ [] = []
-  | global_accesses "" [T, n] = [[T, n], [n]]
-  | global_accesses "" [T, r, n] = [[T, r, n], [T, n], [r, n], [n]]
-  | global_accesses _ [T, p, n] = [[T, p, n], [p, n]]
-  | global_accesses _ [T, p, r, n] = [[T, p, r, n], [T, p, n], [p, r, n], [p, n]]
-  | global_accesses _ names = error ("Bad name declaration " ^ quote (NameSpace.pack names));
-
-(*fully qualified name in context is p.r.n where
-  p: interpretation prefix, r: renaming prefix, n: name*)  (* FIXME not necessarily so *)
-fun local_accesses _ [] = []
-  | local_accesses "" [n] = [[n]]
-  | local_accesses "" [r, n] = [[r, n], [n]]
-  | local_accesses _ [p, n] = [[p, n]]
-  | local_accesses _ [p, r, n] = [[p, r, n], [p, n]]
-  | local_accesses _ names = error ("Bad name declaration " ^ quote (NameSpace.pack names));
-
-in
-
-fun global_note_accesses_i kind prfx args thy =
+(* naming of interpreted theorems *)
+
+fun global_note_prefix_i kind prfx args thy =
   thy
-  |> Theory.qualified_names
-  |> Theory.custom_accesses (global_accesses prfx)
+  |> Theory.qualified_force_prefix prfx
   |> PureThy.note_thmss_i kind args
   ||> Theory.restore_naming thy;
 
-fun local_note_accesses_i prfx args ctxt =
+fun local_note_prefix_i prfx args ctxt =
   ctxt
-  |> ProofContext.qualified_names
-  |> ProofContext.custom_accesses (local_accesses prfx)
+  |> ProofContext.qualified_force_prefix prfx
   |> ProofContext.note_thmss_i args |> swap
   |>> ProofContext.restore_naming ctxt;
-
-end;
 
 
 (* collect witness theorems for global registration;
    requires parameters and flattened list of (assumed!) identifiers
    instead of recomputing it from the target *)

         val args' = args |> map (fn ((n, atts), [(ths, [])]) =>
             ((NameSpace.qualified prfx n,
               map (Attrib.attribute_i thy) (map inst_atts atts @ atts2)),
              [(map (Drule.standard o satisfy_protected prems o
             Element.inst_thm thy insts) ths, [])]));
-      in global_note_accesses_i kind prfx args' thy |> snd end;
+      in global_note_prefix_i kind prfx args' thy |> snd end;
   in fold activate regs thy end;
+
+
+(* abbreviations *)
+
+fun add_abbrevs loc revert decls =
+  snd #> ProofContext.add_abbrevs_i revert decls #>
+  ProofContext.map_theory (change_locale loc
+    (fn (predicate, import, elems, params, abbrevs, regs) =>
+      (predicate, import, elems, params, ((revert, decls), stamp ()) :: abbrevs, regs)));
+
+fun init_abbrevs loc ctxt =
+  fold_rev (uncurry ProofContext.add_abbrevs_i o fst)
+    (#abbrevs (the_locale (ProofContext.theory_of ctxt) loc)) ctxt;
+
+fun init loc =
+  ProofContext.init
+  #> init_abbrevs loc
+  #> (#2 o cert_context_statement (SOME loc) [] []);
 
 
 (* theory/locale results *)
 
 fun theory_results kind prefix results (view, ctxt) thy =

   let
     val (ctxt', ([(_, [Notes args'])], facts)) =
       activate_facts prep_facts (ctxt, [((("", []), Assumed []), [Ext (Notes args)])]);
     val (facts', thy') =
       thy
-      |> change_locale loc (fn (predicate, import, elems, params, regs) =>
-        (predicate, import, elems @ [(Notes args', stamp ())], params, regs))
+      |> change_locale loc (fn (predicate, import, elems, params, abbrevs, regs) =>
+        (predicate, import, elems @ [(Notes args', stamp ())], params, abbrevs, regs))
       |> note_thmss_registrations kind loc args'
       |> global_results (map (#1 o #1) args' ~~ map #2 facts) (view, ctxt);
   in ((facts, facts'), (ProofContext.transfer thy' ctxt', thy')) end;
 
 fun gen_note prep_locale prep_facts kind raw_loc args thy =

   in ((statement, intro, axioms), defs_thy) end;
 
 fun assumes_to_notes (Assumes asms) axms =
        axms
        |> fold_map (fn (a, spec) => fn axs =>
-            let val (ps, qs) = splitAt (length spec, axs)
-            in ((a, [(ps, [])]), qs) end
-          ) asms
-       |-> (fn asms' => pair (Notes asms'))
+            let val (ps, qs) = chop (length spec) axs
+            in ((a, [(ps, [])]), qs) end) asms
+       |-> (pair o Notes)
   | assumes_to_notes e axms = (e, axms);
 
 (* CB: changes only "new" elems, these have identifier ("", _). *)
 
 fun change_elemss axioms elemss =

 
     fun axiomify axioms elemss =
       (axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let
                    val ts = List.concat (List.mapPartial (fn (Assumes asms) =>
                      SOME (List.concat (map (map #1 o #2) asms)) | _ => NONE) elems);
-                   val (axs1, axs2) = splitAt (length ts, axs);
+                   val (axs1, axs2) = chop (length ts) axs;
                  in (axs2, ((id, Assumed axs1), elems)) end)
         |> snd;
     val pred_ctxt = ProofContext.init pred_thy;
     val (ctxt, (_, facts)) = activate_facts (K I)
       (pred_ctxt, axiomify predicate_axioms elemss');

     pred_thy
     |> PureThy.note_thmss_qualified "" bname facts' |> snd
     |> declare_locale name
     |> put_locale name {predicate = predicate, import = import,
         elems = map (fn e => (e, stamp ())) elems',
-        params = (params_of elemss' |>
-          map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))), map #1 (params_of body_elemss)),
+        params = (params_of elemss' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),
+          map #1 (params_of body_elemss)),
+        abbrevs = [],
         regs = []}
     |> pair (body_ctxt)
   end;
 
 in

 val add_locale = gen_add_locale read_context intern_expr;
 val add_locale_i = gen_add_locale cert_context (K I);
 
 end;
 
-val _ = Context.add_setup (
-  add_locale_i true "var" empty [Fixes [(Syntax.internal "x", NONE, NoSyn)]]
-  #> snd
-  #> add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", NONE, Structure)]]
-  #> snd
-)
+val _ = Context.add_setup
+ (add_locale_i true "var" empty [Fixes [(Syntax.internal "x", NONE, NoSyn)]] #> snd #>
+  add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", NONE, Structure)]] #> snd);
 
 
 
 (** locale goals **)
 

     val loc_attss = map (map (prep_src thy) o snd o fst) concl;
     val target = if no_target then NONE else SOME (extern thy loc);
     val elems = map (prep_elem thy) (raw_elems @ concl_elems);
     val names = map (fst o fst) concl;
 
-    val thy_ctxt = ProofContext.init thy;
+    val thy_ctxt = init_abbrevs loc (ProofContext.init thy);
     val (_, (loc_view, loc_ctxt), (elems_view, elems_ctxt), propp) =
       prep_stmt (SOME raw_loc) elems (map snd concl) thy_ctxt;
     val elems_ctxt' = elems_ctxt
       |> ProofContext.add_view loc_ctxt elems_view
       |> ProofContext.add_view thy_ctxt loc_view;

     end;
 
 fun global_activate_facts_elemss x = gen_activate_facts_elemss
       (fn thy => fn (name, ps) =>
         get_global_registration thy (name, map Logic.varify ps))
-      (swap ooo global_note_accesses_i "")
+      (swap ooo global_note_prefix_i "")
       Attrib.attribute_i Drule.standard
       (fn (name, ps) => put_global_registration (name, map Logic.varify ps))
       (fn (n, ps) => fn (t, th) =>
          add_global_witness (n, map Logic.varify ps)
          (Logic.unvarify t, Drule.freeze_all th)) x;
 
 fun local_activate_facts_elemss x = gen_activate_facts_elemss
       get_local_registration
-      local_note_accesses_i
+      local_note_prefix_i
       (Attrib.attribute_i o ProofContext.theory_of) I
       put_local_registration
       add_local_witness x;
 
 fun gen_prep_registration mk_ctxt is_local read_terms test_reg activate

     val ((raw_target_ids, target_syn), _) = flatten (ctxt, I)
         (([], Symtab.empty), Expr (Locale target));
     val fixed = the_locale thy target |> #params |> #1 |> map #1;
     val ((all_ids, syn), raw_elemss) = flatten (ctxt, intern_expr thy)
         ((raw_target_ids, target_syn), Expr expr);
-    val (target_ids, ids) = splitAt (length raw_target_ids, all_ids);
+    val (target_ids, ids) = chop (length raw_target_ids) all_ids;
     val ((parms, elemss, _), _) = read_elemss false ctxt fixed raw_elemss [];
 
     (** compute proof obligations **)
 
     (* restore "small" ids, with mode *)

                       |> map (apfst (apsnd (fn a => a @ map (Attrib.attribute thy) atts2)))
                       |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy)))))
                       |> map (apfst (apfst (NameSpace.qualified prfx)))
                 in
                   thy
-                  |> global_note_accesses_i "" prfx facts'
+                  |> global_note_prefix_i "" prfx facts'
                   |> snd
                 end
               | activate_elem _ thy = thy;
 
             fun activate_elems (_, elems) thy = fold activate_elem elems thy;