# HG changeset patch
# User ballarin
# Date 1080907710 -7200
# Node ID 859b11514537c3f9e37e5080349ebff26312fa04
# Parent  0af3da3beae83525b01e05ac08e8d614802ae608
Experimental command for instantiation of locales in proof contexts:
        instantiate <label>: <loc>

diff -r 0af3da3beae8 -r 859b11514537 NEWS
--- a/NEWS	Fri Apr 02 12:25:48 2004 +0200
+++ b/NEWS	Fri Apr 02 14:08:30 2004 +0200
@@ -52,7 +52,8 @@
 
 *** Isar ***
 
-* Tactic emulation methods ?rule_tac, cut_tac, subgoal_tac and thin_tac:
+* Tactic emulation methods rule_tac, erule_tac, drule_tac, frule_tac,
+  cut_tac, subgoal_tac and thin_tac:
   - Now understand static (Isar) contexts.  As a consequence, users of Isar
     locales are no longer forced to write Isar proof scripts.
     For details see Isar Reference Manual, paragraph 4.3.2: Further tactic
@@ -79,6 +80,14 @@
     specification and "includes" elements in goal statement.
   - Rule sets <locale>.intro and <locale>.axioms no longer declared as
     [intro?] and [elim?] (respectively) by default.
+  - Experimental command for instantiation of locales in proof contexts:
+        instantiate <label>: <loc>
+    Instantiates locale <loc> and adds all its theorems to the current context
+    taking into account their attributes, and qualifying their names with
+    <label>.  If the locale has assumptions, a chained fact of the form
+    "<loc> t1 ... tn" is expected from which instantiations of the parameters
+    are derived.
+    A few (very simple) examples can be found in FOL/ex/LocaleInst.thy.
 
 * HOL: Tactic emulation methods induct_tac and case_tac understand static
   (Isar) contexts.
diff -r 0af3da3beae8 -r 859b11514537 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Fri Apr 02 12:25:48 2004 +0200
+++ b/etc/isar-keywords-ZF.el	Fri Apr 02 14:08:30 2004 +0200
@@ -55,6 +55,7 @@
     "exit"
     "extract"
     "extract_type"
+    "finalconsts"
     "finally"
     "fix"
     "from"
@@ -69,6 +70,7 @@
     "inductive_cases"
     "init_toplevel"
     "instance"
+    "instantiate"
     "judgment"
     "kill"
     "kill_thy"
@@ -308,6 +310,7 @@
     "defs"
     "extract"
     "extract_type"
+    "finalconsts"
     "generate_code"
     "global"
     "hide"
@@ -393,6 +396,7 @@
 
 (defconst isar-keywords-proof-decl
   '("also"
+    "instantiate"
     "let"
     "moreover"
     "note"
diff -r 0af3da3beae8 -r 859b11514537 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Fri Apr 02 12:25:48 2004 +0200
+++ b/etc/isar-keywords.el	Fri Apr 02 14:08:30 2004 +0200
@@ -73,6 +73,7 @@
     "inductive_cases"
     "init_toplevel"
     "instance"
+    "instantiate"
     "judgment"
     "kill"
     "kill_thy"
@@ -429,6 +430,7 @@
 
 (defconst isar-keywords-proof-decl
   '("also"
+    "instantiate"
     "let"
     "moreover"
     "note"
diff -r 0af3da3beae8 -r 859b11514537 src/FOL/IsaMakefile
--- a/src/FOL/IsaMakefile	Fri Apr 02 12:25:48 2004 +0200
+++ b/src/FOL/IsaMakefile	Fri Apr 02 14:08:30 2004 +0200
@@ -44,6 +44,7 @@
 
 $(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy \
   ex/If.thy ex/IffOracle.ML ex/IffOracle.thy ex/List.ML ex/List.thy	\
+  ex/LocaleInst.thy \
   ex/Nat.ML ex/Nat.thy ex/Nat2.ML ex/Nat2.thy ex/Natural_Numbers.thy	\
   ex/Prolog.ML ex/Prolog.thy ex/ROOT.ML ex/Classical.thy ex/document/root.tex\
   ex/foundn.ML ex/Intuitionistic.thy ex/intro.ML ex/prop.ML ex/quant.ML
diff -r 0af3da3beae8 -r 859b11514537 src/FOL/ex/LocaleInst.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/LocaleInst.thy	Fri Apr 02 14:08:30 2004 +0200
@@ -0,0 +1,114 @@
+(*  Title:      FOL/ex/LocaleInst.thy
+    ID:         $Id$
+    Author:     Clemens Ballarin
+    Copyright (c) 2004 by Clemens Ballarin
+
+Test of locale instantiation mechanism, also provides a few examples.
+*)
+
+header {* Test of Locale instantiation *}
+
+theory LocaleInst = FOL:
+
+ML {* set show_hyps *}
+
+section {* Locale without assumptions *}
+
+locale L1 = notes rev_conjI [intro] = conjI [THEN iffD1 [OF conj_commute]]
+
+lemma "[| A; B |] ==> A & B"
+proof -
+  instantiate my: L1   txt {* No chained fact required. *}
+  assume B and A  txt {* order reversed *}
+  then show "A & B" ..
+  txt {* Applies @{thm my.rev_conjI}. *}
+qed
+
+section {* Simple locale with assumptions *}
+
+typedecl i
+arities  i :: "term"
+
+consts bin :: "[i, i] => i" (infixl "#" 60)
+
+axioms i_assoc: "(x # y) # z = x # (y # z)"
+  i_comm: "x # y = y # x"
+
+locale L2 =
+  fixes OP (infixl "+" 60)
+  assumes assoc: "(x + y) + z = x + (y + z)"
+    and comm: "x + y = y + x"
+
+lemma (in L2) lcomm: "x + (y + z) = y + (x + z)"
+proof -
+  have "x + (y + z) = (x + y) + z" by (simp add: assoc)
+  also have "... = (y + x) + z" by (simp add: comm)
+  also have "... = y + (x + z)" by (simp add: assoc)
+  finally show ?thesis .
+qed
+
+lemmas (in L2) AC = comm assoc lcomm
+
+lemma "(x::i) # y # z # w = y # x # w # z"
+proof -
+  have "L2 (op #)" by (rule L2.intro [of "op #", OF i_assoc i_comm])
+  then instantiate my: L2
+    txt {* Chained fact required to discharge assumptions of @{text L2}
+      and instantiate parameters. *}
+  show ?thesis by (simp only: my.OP.AC)  (* or simply AC *)
+qed
+
+section {* Nested locale with assumptions *}
+
+locale L3 =
+  fixes OP (infixl "+" 60)
+  assumes assoc: "(x + y) + z = x + (y + z)"
+
+locale L4 = L3 +
+  assumes comm: "x + y = y + x"
+
+lemma (in L4) lcomm: "x + (y + z) = y + (x + z)"
+proof -
+  have "x + (y + z) = (x + y) + z" by (simp add: assoc)
+  also have "... = (y + x) + z" by (simp add: comm)
+  also have "... = y + (x + z)" by (simp add: assoc)
+  finally show ?thesis .
+qed
+
+lemmas (in L4) AC = comm assoc lcomm
+
+text {* Conceptually difficult locale:
+   2nd context fragment contains facts with differing metahyps. *}
+
+lemma L4_intro:
+  fixes OP (infixl "+" 60)
+  assumes assoc: "!!x y z. (x + y) + z = x + (y + z)"
+    and comm: "!!x y. x + y = y + x"
+  shows "L4 (op+)"
+    by (blast intro: L4.intro L3.intro assoc L4_axioms.intro comm)
+
+lemma "(x::i) # y # z # w = y # x # w # z"
+proof -
+  have "L4 (op #)" by (rule L4_intro [of "op #", OF i_assoc i_comm])
+  then instantiate my: L4
+  show ?thesis by (simp only: my.OP.AC)  (* or simply AC *)
+qed
+
+section {* Locale with definition *}
+
+text {* This example is admittedly not very creative :-) *}
+
+locale L5 = L4 + var A +
+  defines A_def: "A == True"
+
+lemma (in L5) lem: A
+  by (unfold A_def) rule
+
+lemma "L5(op #) ==> True"
+proof -
+  assume "L5(op #)"
+  then instantiate my: L5
+  show ?thesis by (rule lem)  (* lem instantiated to True *)
+qed
+
+end
diff -r 0af3da3beae8 -r 859b11514537 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Apr 02 12:25:48 2004 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Apr 02 14:08:30 2004 +0200
@@ -357,6 +357,12 @@
   OuterSyntax.command "using" "augment goal facts" K.prf_decl
     (facts >> (Toplevel.print oo (Toplevel.proof o IsarThy.using_facts)));
 
+val instantiateP =
+  OuterSyntax.command "instantiate" "instantiate locale" K.prf_decl
+    (P.name --| P.$$$ ":" -- P.xname
+(*    (P.xname -- (P.$$$ "[" |-- P.name --| P.$$$ "]") *)
+      >> (Toplevel.print oo (Toplevel.proof o IsarThy.instantiate_locale)));
+
 
 (* proof context *)
 
@@ -756,7 +762,7 @@
   default_proofP, immediate_proofP, done_proofP, skip_proofP,
   forget_proofP, deferP, preferP, applyP, apply_endP, proofP, alsoP,
   finallyP, moreoverP, ultimatelyP, backP, cannot_undoP, clear_undosP,
-  redoP, undos_proofP, undoP, killP,
+  redoP, undos_proofP, undoP, killP, instantiateP,
   (*diagnostic commands*)
   pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
   print_syntaxP, print_theoremsP, print_localesP, print_localeP,
diff -r 0af3da3beae8 -r 859b11514537 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Fri Apr 02 12:25:48 2004 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Fri Apr 02 14:08:30 2004 +0200
@@ -48,6 +48,7 @@
   val using_facts_i: (thm * Proof.context attribute list) list list
     -> ProofHistory.T -> ProofHistory.T
   val chain: ProofHistory.T -> ProofHistory.T
+  val instantiate_locale: string * string -> ProofHistory.T -> ProofHistory.T
   val fix: (string list * string option) list -> ProofHistory.T -> ProofHistory.T
   val fix_i: (string list * typ option) list -> ProofHistory.T -> ProofHistory.T
   val let_bind: (string list * string) list -> ProofHistory.T -> ProofHistory.T
@@ -290,6 +291,10 @@
 
 val chain = ProofHistory.apply Proof.chain;
 
+(* locale instantiation *)
+
+fun instantiate_locale (prfx, loc) =
+  ProofHistory.apply (Proof.instantiate_locale (loc, prfx));
 
 (* context *)
 
diff -r 0af3da3beae8 -r 859b11514537 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Apr 02 12:25:48 2004 +0200
+++ b/src/Pure/Isar/locale.ML	Fri Apr 02 14:08:30 2004 +0200
@@ -65,6 +65,7 @@
   val add_thmss: string -> ((string * thm list) * context attribute list) list ->
     theory * context -> (theory * context) * (string * thm list) list
   val prune_prems: theory -> thm -> thm
+  val instantiate: string -> string -> thm list option -> context -> context
   val setup: (theory -> theory) list
 end;
 
@@ -96,7 +97,7 @@
 
 type locale =
  {view: cterm list * thm list,
-    (* If locale "loc" contains assumptions, either via import or in the
+    (* CB: If locale "loc" contains assumptions, either via import or in the
        locale body, a locale predicate "loc" is defined capturing all the
        assumptions.  If both import and body contain assumptions, additionally
        a delta predicate "loc_axioms" is defined that abbreviates the
@@ -107,10 +108,11 @@
        locales with import from the import hierarchy (duplicates removed,
        cf. [1], normalisation of locale expressions).
 
-       The first part of view in the above definition (also called statement)
-       represents this list of assumptions.  The second part (also called
-       axioms) contains projections from the predicate "loc" to these
-       assumptions.
+       The record entry view is either ([], []) or ([statement], axioms)
+       where statement is the predicate "loc" applied to the parameters,
+       and axioms contains projections from "loc" to the list of assumptions
+       generated when entering the locale.
+       It appears that an axiom of the form A [A] is never generated.
      *)
   import: expr,                                                         (*dynamic import*)
   elems: ((typ, term, thm list, context attribute) elem * stamp) list,  (*static content*)
@@ -229,7 +231,7 @@
    Remove internal delta predicates (generated by "includes") from the
    premises of a theorem.
 
-   Assumes no outer quanfifiers and no flex-flex pairs.
+   Assumes no outer quantifiers and no flex-flex pairs.
    May change names of TVars.
    Performs compress and close_derivation on result, if modified. **)
 
@@ -466,6 +468,9 @@
 
 (* parameter types *)
 
+(* CB: frozen_tvars has the following type:
+  ProofContext.context -> Term.typ list -> (Term.indexname * Term.typ) list *)
+
 fun frozen_tvars ctxt Ts =
   let
     val tvars = rev (foldl Term.add_tvarsT ([], Ts));
@@ -492,6 +497,9 @@
   in map (apsome (Envir.norm_type unifier')) Vs end;
 
 fun params_of elemss = gen_distinct eq_fst (flat (map (snd o fst) elemss));
+
+(* CB: param_types has the following type:
+  ('a * 'b Library.option) list -> ('a * 'b) list *)
 fun param_types ps = mapfilter (fn (_, None) => None | (x, Some T) => Some (x, T)) ps;
 
 
@@ -499,6 +507,11 @@
 
 local
 
+(* CB: unique_parms has the following type:
+     'a ->
+     (('b * (('c * 'd) list * Symtab.key list)) * 'e) list ->
+     (('b * ('c * 'd) list) * 'e) list  *)
+
 fun unique_parms ctxt elemss =
   let
     val param_decls =
@@ -511,6 +524,12 @@
     | None => map (apfst (apsnd #1)) elemss)
   end;
 
+(* CB: unify_parms has the following type:
+     ProofContext.context ->
+     (string * Term.typ) list ->
+     (string * Term.typ Library.option) list list ->
+     ((string * Term.sort) * Term.typ) list list *)
+
 fun unify_parms ctxt fixed_parms raw_parmss =
   let
     val tsig = Sign.tsig_of (ProofContext.sign_of ctxt);
@@ -649,13 +668,22 @@
 
 in
 
+(* CB: activate_facts prep_facts ((ctxt, axioms), elemss),
+   where elemss is a list of pairs consisting of identifiers and context
+   elements, extends ctxt by the context elements yielding ctxt' and returns
+   ((ctxt', axioms'), (elemss', facts)).
+   Assumptions use entries from axioms to set up exporters in ctxt'.  Unused
+   axioms are returned as axioms'; elemss' is obtained from elemss (without
+   identifier) and the intermediate context with prep_facts.
+   If get_facts or get_facts_i is used for prep_facts, these also remove
+   the internal/external markers from elemss. *)
+
 fun activate_facts prep_facts arg =
   apsnd (apsnd flat o Library.split_list) (activate_elemss prep_facts arg);
 
 end;
 
 
-
 (** prepare context elements **)
 
 (* expressions *)
@@ -669,7 +697,7 @@
 
 local fun read_att attrib (x, srcs) = (x, map attrib srcs) in
 
-(* Map attrib over
+(* CB: Map attrib over
    * A context element: add attrib to attribute lists of assumptions,
      definitions and facts (on both sides for facts).
    * Locale expression: no effect. *)
@@ -705,6 +733,22 @@
 
 datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;
 
+(* CB: flatten (ids, expr) normalises expr (which is either a locale
+   expression or a single context element) wrt.
+   to the list ids of already accumulated identifiers.
+   It returns (ids', elemss) where ids' is an extension of ids
+   with identifiers generated for expr, and elemss is the list of
+   context elements generated from expr, decorated with additional
+   information (the identifiers?), including parameter names.
+   It appears that the identifier name is empty for external elements
+   (this is suggested by the implementation of activate_facts). *)
+
+fun flatten _ (ids, Elem (Fixes fixes)) =
+      (ids, [(("", map (rpair None o #1) fixes), Ext (Fixes fixes))])
+  | flatten _ (ids, Elem elem) = (ids, [(("", []), Ext elem)])
+  | flatten (ctxt, prep_expr) (ids, Expr expr) =
+      apsnd (map (apsnd Int)) (flatten_expr ctxt (ids, prep_expr expr));
+
 local
 
 local
@@ -752,6 +796,9 @@
 
 local
 
+(* CB: following code (norm_term, abstract_term, abstract_thm, bind_def)
+   used in eval_text for defines elements. *)
+
 val norm_term = Envir.beta_norm oo Term.subst_atomic;
 
 fun abstract_term eq =    (*assumes well-formedness according to ProofContext.cert_def*)
@@ -845,12 +892,22 @@
 
 fun prep_elemss prep_fixes prepp do_close context fixed_params raw_elemss raw_concl =
   let
+    (* CB: raw_elemss are list of pairs consisting of identifiers and
+       context elements, the latter marked as internal or external. *)
     val (raw_ctxt, raw_proppss) = declare_elemss prep_fixes fixed_params raw_elemss context;
+    (* CB: raw_ctxt is context with additional fixed variables derived from
+       the fixes elements in raw_elemss,
+       raw_proppss contains assumptions and definitions from the
+       (external?) elements in raw_elemss. *)
     val raw_propps = map flat raw_proppss;
     val raw_propp = flat raw_propps;
     val (ctxt, all_propp) =
       prepp (ProofContext.declare_terms (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
+    (* CB: read/cert entire proposition (conclusion and premises from
+       the context elements). *)
     val ctxt = ProofContext.declare_terms (flat (map (map fst) all_propp)) ctxt;
+    (* CB: it appears that terms declared in the propositions are added
+       to the context here. *)
 
     val all_propp' = map2 (op ~~)
       (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp))), map (map snd) all_propp);
@@ -863,9 +920,33 @@
       (map (ProofContext.default_type raw_ctxt) xs)
       (map (ProofContext.default_type ctxt) xs);
     val parms = param_types (xs ~~ typing);
+    (* CB: parms are the parameters from raw_elemss, with correct typing. *)
 
+    (* CB: extract information from assumes and defines elements
+       (fixes and notes in raw_elemss don't have an effect on text and elemss),
+       compute final form of context elements. *)
     val (text, elemss) = finish_elemss ctxt parms do_close
       (((([], []), ([], [])), ([], [], [])), raw_elemss ~~ proppss);
+    (* CB: text has the following structure:
+           (((exts, exts'), (ints, ints')), (xs, env, defs))
+       where
+         exts: external assumptions (terms in external assumes elements)
+         exts': dito, normalised wrt. env
+         ints: internal assumptions (terms in internal assumes elements)
+         ints': dito, normalised wrt. env
+         xs: the free variables in exts' and ints' and rhss of definitions,
+           this includes parameters except defined parameters
+         env: list of term pairs encoding substitutions, where the first term
+           is a free variable; substitutions represent defines elements and
+           the rhs is normalised wrt. the previous env
+         defs: theorems representing the substitutions from defines elements
+           (thms are normalised wrt. env).
+       elemss is an updated version of raw_elemss:
+         - type info added to Fixes
+         - axiom and definition statement replaced by corresponding one
+           from proppss in Assumes and Defines
+         - Facts unchanged
+       *)
   in ((parms, elemss, concl), text) end;
 
 in
@@ -881,6 +962,7 @@
 local
 
 fun prep_name ctxt (name, atts) =
+  (* CB: reject qualified names in locale declarations *)
   if NameSpace.is_qualified name then
     raise ProofContext.CONTEXT ("Illegal qualified name: " ^ quote name, ctxt)
   else (name, atts);
@@ -909,15 +991,12 @@
   let
     val sign = ProofContext.sign_of context;
 
-    fun flatten (ids, Elem (Fixes fixes)) =
-          (ids, [(("", map (rpair None o #1) fixes), Ext (Fixes fixes))])
-      | flatten (ids, Elem elem) = (ids, [(("", []), Ext elem)])
-      | flatten (ids, Expr expr) =
-          apsnd (map (apsnd Int)) (flatten_expr context (ids, prep_expr sign expr));
-
-    val (import_ids, raw_import_elemss) = flatten ([], Expr import);
+    val (import_ids, raw_import_elemss) = flatten (context, prep_expr sign) ([], Expr import);
     (* CB: normalise "includes" among elements *)
-    val raw_elemss = flat (#2 ((foldl_map flatten (import_ids, elements))));
+    val raw_elemss = flat (#2 ((foldl_map (flatten (context, prep_expr sign))
+      (import_ids, elements))));
+    (* CB: raw_import_elemss @ raw_elemss is the normalised list of
+       context elements obtained from import and elements. *)
     val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close
       context fixed_params (raw_import_elemss @ raw_elemss) raw_concl;
     val (ps,qs) = splitAt(length raw_import_elemss, all_elemss)
@@ -938,7 +1017,7 @@
     val thy = ProofContext.theory_of ctxt;
     val locale = apsome (prep_locale (Theory.sign_of thy)) raw_locale;
     val ((view_statement, view_axioms), fixed_params, import) =
-(* view_axioms are xxx.axioms of locale xxx *)
+(* CB: view_axioms are xxx.axioms of locale xxx *)
       (case locale of None => (([], []), [], empty)
       | Some name =>
           let val {view, params = (ps, _), ...} = the_locale thy name
@@ -949,7 +1028,7 @@
 
 in
 
-(* CB: arguments are: x->import, y->body (elements?), z->context *)
+(* CB: arguments are: x->import, y->body (elements), z->context *)
 fun read_context x y z = #1 (gen_context true [] [] x y [] z);
 fun cert_context x y z = #1 (gen_context_i true [] [] x y [] z);
 
@@ -959,6 +1038,157 @@
 end;
 
 
+(** CB: experimental instantiation mechanism **)
+
+fun instantiate loc_name prfx raw_inst ctxt =
+  let
+    val thy = ProofContext.theory_of ctxt;
+    val sign = Theory.sign_of thy;
+    val tsig = Sign.tsig_of sign;
+    val cert = cterm_of sign;
+
+    (** process the locale **)
+
+    val {view = (_, axioms), params = (ps, _), ...} =
+      the_locale thy (intern sign loc_name);
+    val fixed_params = param_types ps;
+    val (ids, raw_elemss) =
+          flatten (ctxt, intern_expr sign) ([], Expr (Locale loc_name));
+    val ((parms, all_elemss, concl),
+         (spec as (_, (ints, _)), (xs, env, defs))) =
+      read_elemss false (* do_close *) ctxt
+        fixed_params (* could also put [] here??? *) raw_elemss
+        [] (* concl *);
+
+    (** analyse the instantiation theorem inst **)
+
+    val inst = case raw_inst of
+        None => if null ints
+	  then None
+	  else error "Locale has assumptions but no chained fact was found"
+      | Some [] => if null ints
+	  then None
+	  else error "Locale has assumptions but no chained fact was found"
+      | Some [thm] => if null ints
+	  then (warning "Locale has no assumptions: fact ignored"; None)
+	  else Some thm
+      | Some _ => error "Multiple facts are not allowed";
+
+    val args = case inst of
+            None => []
+          | Some thm => thm |> prop_of |> ObjectLogic.drop_judgment sign
+              |> Term.strip_comb |> snd;
+    val cargs = map cert args;
+
+    (* process parameters: match their types with those of arguments *)
+
+    val def_names = map (fn (Free (s, _), _) => s) env;
+    val (defined, assumed) = partition
+          (fn (s, _) => s mem def_names) fixed_params;
+    val cassumed = map (cert o Free) assumed;
+    val cdefined = map (cert o Free) defined;
+
+    val param_types = map snd assumed;
+    val v_param_types = map Type.varifyT param_types;
+    val arg_types = map Term.fastype_of args;
+    val Tenv = foldl (Type.typ_match tsig)
+          (Vartab.empty, v_param_types ~~ arg_types)
+          handle Library.LIST "~~" => error "Number of parameters does not match number of arguments of chained fact";
+    (* get their sorts *)
+    val tfrees = foldr Term.add_typ_tfrees (param_types, []);
+    val Tenv' = map
+          (fn ((a, i), T) => ((a, the (assoc_string (tfrees, a))), T))
+          (Vartab.dest Tenv);
+
+    (* process (internal) elements *)
+
+    fun inst_type [] T = T
+      | inst_type env T =
+          Term.map_type_tfree (fn v => if_none (assoc (env, v)) (TFree v)) T;
+
+    fun inst_term [] t = t
+      | inst_term env t = Term.map_term_types (inst_type env) t;
+
+    (* parameters with argument types *)
+
+    val cparams' = map (cterm_of sign o inst_term Tenv' o term_of) cassumed;
+    val cdefined' = map (cert o inst_term Tenv' o term_of) cdefined;
+    val cdefining = map (cert o inst_term Tenv' o snd) env;
+
+    fun inst_thm _ [] th = th
+      | inst_thm ctxt Tenv th =
+	  let
+	    val sign = ProofContext.sign_of ctxt;
+	    val cert = Thm.cterm_of sign;
+	    val certT = Thm.ctyp_of sign;
+	    val {hyps, prop, maxidx, ...} = Thm.rep_thm th;
+	    val tfrees = foldr Term.add_term_tfree_names (prop :: hyps, []);
+	    val Tenv' = filter (fn ((a, _), _) => a mem_string tfrees) Tenv;
+	  in
+	    if null Tenv' then th
+	    else
+	      th
+	      |> Drule.implies_intr_list (map cert hyps)
+	      |> Drule.tvars_intr_list (map (#1 o #1) Tenv')
+	      |> (fn (th', al) => th' |>
+		Thm.instantiate ((map (fn ((a, _), T) =>
+                  (the (assoc (al, a)), certT T)) Tenv'), []))
+	      |> (fn th'' => Drule.implies_elim_list th''
+		  (map (Thm.assume o cert o inst_term Tenv') hyps))
+	  end;
+
+    fun inst_thm' thm =
+      let
+        (* not all axs are normally applicable *)
+        val hyps = #hyps (rep_thm thm);
+        val ass = map (fn ax => (prop_of ax, ax)) axioms;
+        val axs' = foldl (fn (axs, hyp) => 
+              (case assoc (ass, hyp) of None => axs
+                 | Some ax => axs @ [ax])) ([], hyps);
+        val thm' = Drule.satisfy_hyps axs' thm;
+        (* instantiate types *)
+        val thm'' = inst_thm ctxt Tenv' thm';
+        (* substitute arguments and discharge hypotheses *)
+        val thm''' = case inst of
+                None => thm''
+              | Some inst_thm => let
+		    val hyps = #hyps (rep_thm thm'');
+		    val th = thm'' |> implies_intr_hyps
+		      |> forall_intr_list (cparams' @ cdefined')
+		      |> forall_elim_list (cargs @ cdefining)
+		    (* th has premises of the form either inst_thm or x==x *)
+		    fun mk hyp = if Logic.is_equals hyp
+			  then hyp |> Logic.dest_equals |> snd |> cert
+				 |> reflexive
+			  else inst_thm
+                  in implies_elim_list th (map mk hyps)
+                  end;
+      in thm''' end;
+
+    fun inst_elem (ctxt, (Ext _)) = ctxt
+      | inst_elem (ctxt, (Int (Notes facts))) =
+              (* instantiate fact *)
+          let val facts' =
+              map (apsnd (map (apfst (map inst_thm')))) facts
+              (* rename fact *)
+              val facts'' =
+              map (apfst (apfst (fn "" => ""
+                                  | s => NameSpace.append prfx s)))
+                  facts'
+          in fst (ProofContext.have_thmss_i facts'' ctxt)
+          end
+      | inst_elem (ctxt, (Int _)) = ctxt;
+
+    fun inst_elems (ctxt, (id, elems)) = foldl inst_elem (ctxt, elems);
+
+    fun inst_elemss ctxt elemss = foldl inst_elems (ctxt, elemss);
+
+    (* main part *)
+
+    val ctxt' = ProofContext.qualified true ctxt;
+  in ProofContext.restore_qualified ctxt (inst_elemss ctxt' all_elemss)
+  end;
+
 
 (** define locales **)
 
@@ -1019,6 +1249,7 @@
 
 fun smart_have_thmss kind None = PureThy.have_thmss_i (Drule.kind kind)
   | smart_have_thmss kind (Some (loc, _)) = have_thmss_qualified kind loc;
+  (* CB: only used in Proof.finish_global. *)
 
 end;
 
@@ -1050,6 +1281,8 @@
 
 val have_thmss = gen_have_thmss intern ProofContext.get_thms;
 val have_thmss_i = gen_have_thmss (K I) (K I);
+  (* CB: have_thmss(_i) is the base for the Isar commands
+     "theorems (in loc)" and "declare (in loc)". *)
 
 fun add_thmss loc args (thy, ctxt) =
   let
@@ -1059,6 +1292,7 @@
     val ((ctxt', _), (_, facts')) =
       activate_facts (K I) ((ctxt, view_axioms), [(("", []), [Notes args'])]);
   in ((thy', ctxt'), facts') end;
+  (* CB: only used in Proof.finish_global. *)
 
 end;
 
diff -r 0af3da3beae8 -r 859b11514537 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Fri Apr 02 12:25:48 2004 +0200
+++ b/src/Pure/Isar/method.ML	Fri Apr 02 14:08:30 2004 +0200
@@ -368,7 +368,8 @@
 	val params = Logic.strip_params Bi
 			     (* params of subgoal i as string typ pairs *)
 	val params = rev(Term.rename_wrt_term Bi params)
-						 (* as they are printed *)
+			   (* as they are printed: bound variables with *)
+                           (* the same name are renamed during printing *)
         fun types' (a, ~1) = (case assoc (params, a) of
                 None => types (a, ~1)
               | some => some)
diff -r 0af3da3beae8 -r 859b11514537 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Fri Apr 02 12:25:48 2004 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Fri Apr 02 14:08:30 2004 +0200
@@ -174,7 +174,8 @@
 val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
 
 val uname = underscore >> K None || name >> Some;
-
+  (* CB: underscore yields None, any other name Some with that string.
+     Used, for example, in the renaming of locale parameters.  *)
 
 (* sorts and arities *)
 
diff -r 0af3da3beae8 -r 859b11514537 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Apr 02 12:25:48 2004 +0200
+++ b/src/Pure/Isar/proof.ML	Fri Apr 02 14:08:30 2004 +0200
@@ -65,6 +65,7 @@
     (thm list * context attribute list) list) list -> state -> state
   val using_thmss: ((xstring * context attribute list) list) list -> state -> state
   val using_thmss_i: ((thm list * context attribute list) list) list -> state -> state
+  val instantiate_locale: string * string -> state -> state
   val fix: (string list * string option) list -> state -> state
   val fix_i: (string list * typ option) list -> state -> state
   val assm: ProofContext.exporter
@@ -510,6 +511,7 @@
 
 
 (* have_thmss *)
+(* CB: this implements "note" of the Isar/VM *)
 
 local
 
@@ -565,6 +567,19 @@
 end;
 
 
+(* locale instantiation *)
+
+fun instantiate_locale (loc_name, prfx) state = let
+    val ctxt = context_of state;
+    val facts = if is_chain state then get_facts state else None;
+  in
+    state
+    |> assert_forward_or_chain
+    |> enter_forward
+    |> reset_facts
+    |> map_context (Locale.instantiate loc_name prfx facts)
+  end;
+
 (* fix *)
 
 fun gen_fix f xs state =
diff -r 0af3da3beae8 -r 859b11514537 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Apr 02 12:25:48 2004 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Apr 02 14:08:30 2004 +0200
@@ -160,9 +160,17 @@
       ((cterm list * exporter) list *                         (*assumes: A ==> _*)
         (string * thm list) list) *
       (string * string) list,                                 (*fixes: !!x. _*)
+    (* CB: asms is of the form ((asms, prems), fixed) *)
     binds: (term * typ) option Vartab.table,                  (*term bindings*)
     thms: bool * NameSpace.T * thm list option Symtab.table
       * FactIndex.T,                                          (*local thms*)
+    (* CB: thms is of the form (q, n, t, i) where
+       q: indicates whether theorems with qualified names may be stored;
+          this is initially forbidden (false); flag may be changed with
+          qualified and restore_qualified;
+       n: theorem namespace;
+       t: table of theorems;
+       i: index for theorem lookup (find theorem command) *) 
     cases: (string * RuleCases.T) list,                       (*local contexts*)
     defs:
       typ Vartab.table *                                      (*type constraints*)
@@ -1215,6 +1223,8 @@
 
 end;
 
+(* CB: fix free variables occuring in ts, unless already fixed. *)
+
 fun fix_frees ts ctxt =
   let
     val frees = foldl Term.add_frees ([], ts);