src/Pure/Isar/locale.ML

     ((bstring * context attribute list) * (thm list * context attribute list) list) list ->
     theory -> theory * (bstring * thm list) list
   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;
 
 structure Locale: LOCALE =
 struct

 type 'att element = (string, string, string, 'att) elem_expr;
 type 'att element_i = (typ, term, thm list, 'att) elem_expr;
 
 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
        assumptions of the body.
        The context generated when entering "loc" contains not (necessarily) a
        single assumption "loc", but a list of assumptions of all locale
        predicates of locales without import and all delta predicates of
        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*)
   params: (string * typ option) list * string list};                  (*all/local params*)
 

 
 (** Prune premises:
    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. **)
 
 (* Note: reconstruction of the correct premises fails for subspace_normed_vs
    in HOL/Real/HahnBanach/NormedSpace.thy.  This cannot be fixed since in the

 
 (** structured contexts: rename + merge + implicit type instantiation **)
 
 (* 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));
     val tfrees = map TFree
       (Term.invent_type_names (ProofContext.used_types ctxt) (length tvars) ~~ map #2 tvars);

     val Vs = map (apsome (Envir.norm_type unifier)) Us';
     val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (mapfilter I Vs));
   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;
 
 
 (* flatten expressions *)
 
 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 =
       flat (map (fn ((name, (ps, qs)), _) => map (rpair (name, ps)) qs) elemss)

     (case find_first (fn (_, ids) => length ids > 1) param_decls of
       Some (q, ids) => err_in_locale ctxt ("Multiple declaration of parameter " ^ quote q)
           (map (apsnd (map fst)) ids)
     | 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);
     val maxidx = length raw_parmss;

     val ((ctxt', axs'), res) = apsnd flat (activate_elems ((name, ps), elems) (ctxt, axs));
   in ((ctxt', axs'), (((name, ps), elems), res)) end);
 
 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 *)

 
 (* attributes *)
 
 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. *)
 
 

 
 
 (* propositions and bindings *)
 
 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
 

 
 end;
 
 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*)
   let
     val body = Term.strip_all_body eq;

 
 end;
 
 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);
     val (concl, propp) = splitAt(length raw_concl, all_propp');
     val propps = unflat raw_propps propp;

     val xs = map #1 (params_of raw_elemss);
     val typing = unify_frozen ctxt 0
       (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
 
 fun read_elemss x = prep_elemss read_fixes ProofContext.read_propp_schematic x;

 (* facts *)
 
 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);
 
 fun prep_facts _ _ (Int elem) = elem

 fun prep_context_statement prep_expr prep_elemss prep_facts
     do_close axioms fixed_params import elements raw_concl context =
   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)
     val ((import_ctxt, axioms'), (import_elemss, _)) =
       activate_facts prep_facts ((context, axioms), ps);

 fun gen_statement prep_locale prep_ctxt raw_locale elems concl ctxt =
   let
     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
           in (view, param_types ps, Locale name) end);
     val ((((locale_ctxt, _), (elems_ctxt, _)), _), concl') =
       prep_ctxt false view_axioms fixed_params import elems concl ctxt;
   in (locale, view_statement, locale_ctxt, elems_ctxt, concl') end;
 
 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);
 
 val read_context_statement = gen_statement intern gen_context;
 val cert_context_statement = gen_statement (K I) gen_context_i;
 
 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 **)
 
 (* print locale *)

   |>> hide_bound_names (map (#1 o #1) args)
   |>> Theory.parent_path;
 
 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;
 
 local
 

 
 in
 
 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
     val args' = map (fn ((a, ths), atts) => ((a, atts), [(ths, [])])) args;
     val thy' = put_facts loc args' thy;
     val {view = (_, view_axioms), ...} = the_locale thy loc;
     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;
 
 
 (* predicate text *)