src/Pure/Isar/locale.ML

 
 (* TODO:
 - beta-eta normalisation of interpretation parameters
 - dangling type frees in locales
 - test subsumption of interpretations when merging theories
+- var vs. fixes in locale to be interpreted (interpretation in locale)
+  (implicit locale expressions generated by multiple registrations)
+- current finish_global adds unwanted lemmas to theory/locale
 *)
 
 signature LOCALE =
 sig
   type context

       (term * (term list * term list)) list list
 
   (* Diagnostic functions *)
   val print_locales: theory -> unit
   val print_locale: theory -> expr -> element list -> unit
-  val print_global_registrations: string -> theory -> unit
-  val print_local_registrations': string -> context -> unit
-  val print_local_registrations: string -> context -> unit
+  val print_global_registrations: bool -> string -> theory -> unit
+  val print_local_registrations': bool -> string -> context -> unit
+  val print_local_registrations: bool -> string -> context -> unit
 
   (* Storing results *)
   val add_locale_context: bool -> bstring -> expr -> element list -> theory
     -> theory * ProofContext.context
   val add_locale_context_i: bool -> bstring -> expr -> element_i list -> theory

     string * Attrib.src list -> expr -> string option list -> context ->
     ((string * term list) * term list) list * (thm list -> context -> context)
   val prep_registration_in_locale:
     string -> expr -> theory ->
     ((string * string list) * term list) list * (thm list -> theory -> theory)
-
-  (* Diagnostic *)
-  val show_wits: bool ref;
 end;
 
 structure Locale: LOCALE =
 struct
-
-(** Diagnostic: whether to show witness theorems of registrations **)
-
-val show_wits = ref false;
 
 (** locale elements and expressions **)
 
 type context = ProofContext.context;
 

                 ((map (fn (a, T) => (certT (TVar (valOf (assoc (al, a)))), certT T)) tinst'),
                   []))
             |> (fn th => Drule.implies_elim_list th
                  (map (Thm.assume o cert o tinst_tab_term tinst) hyps))
         end;
-
 
 (* instantiate TFrees and Frees *)
 
 fun inst_tab_term (inst, tinst) = if Symtab.is_empty inst
       then tinst_tab_term tinst

             |> (fn th => Drule.implies_elim_list th
                  (map (Thm.assume o cert o inst_tab_term (inst, tinst)) hyps))
         end;
 
 
+fun inst_tab_att thy (inst as (_, tinst)) =
+    Args.map_values I (tinst_tab_type tinst)
+    (inst_tab_term inst) (inst_tab_thm thy inst);
+
+fun inst_tab_atts thy inst = map (inst_tab_att thy inst);
+
+
 (** management of registrations in theories and proof contexts **)
 
 structure Registrations :
   sig
     type T

   end;
 
 
 (* printing of registrations *)
 
-fun gen_print_registrations get_regs mk_ctxt msg loc thy_ctxt =
+fun gen_print_registrations get_regs mk_ctxt msg show_wits loc thy_ctxt =
   let
     val ctxt = mk_ctxt thy_ctxt;
     val thy = ProofContext.theory_of ctxt;
 
     val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;

         Pretty.breaks (Pretty.str prfx :: Args.pretty_attribs ctxt atts);
     val prt_thm = Pretty.quote o ProofContext.pretty_thm ctxt;
     fun prt_thms thms =
         Pretty.enclose "[" "]" (Pretty.breaks (map prt_thm thms));
     fun prt_reg (ts, (("", []), thms)) =
-        if ! show_wits
+        if show_wits
           then Pretty.block [prt_inst ts, Pretty.fbrk, prt_thms thms]
           else prt_inst ts
       | prt_reg (ts, (attn, thms)) =
-        if ! show_wits
+        if show_wits
           then Pretty.block ((prt_attn attn @
             [Pretty.str ":", Pretty.brk 1, prt_inst ts, Pretty.fbrk,
               prt_thms thms]))
           else Pretty.block ((prt_attn attn @
             [Pretty.str ":", Pretty.brk 1, prt_inst ts]));

      gen_print_registrations (#3 o GlobalLocalesData.get)
        ProofContext.init "theory";
 val print_local_registrations' =
      gen_print_registrations LocalLocalesData.get
        I "context";
-fun print_local_registrations loc ctxt =
-  (print_global_registrations loc (ProofContext.theory_of ctxt);
-   print_local_registrations' loc ctxt);
+fun print_local_registrations show_wits loc ctxt =
+  (print_global_registrations show_wits loc (ProofContext.theory_of ctxt);
+   print_local_registrations' show_wits loc ctxt);
 
 
 (* diagnostics *)
 
 fun err_in_locale ctxt msg ids =

    specification fragment to assumptions of other (assumed) specification
    fragments. *)
 
 datatype 'a mode = Assumed of 'a | Derived of 'a;
 
-fun map_mode2 f _ (Assumed x) = Assumed (f x)
-  | map_mode2 _ g (Derived x) = Derived (g x);
-
 fun map_mode f (Assumed x) = Assumed (f x)
   | map_mode f (Derived x) = Derived (f x);
 
 (* flatten expressions *)
 

     fun identify top (Locale name) =
     (* CB: ids_ax is a list of tuples of the form ((name, ps), axs),
        where name is a locale name, ps a list of parameter names and axs
        a list of axioms relating to the identifier, axs is empty unless
        identify at top level (top = true);
-       ty is the parameter typing (empty if at top level);
        parms is accumulated list of parameters *)
           let
             val {predicate = (_, axioms), import, params, ...} =
               the_locale thy name;
             val ps = map (#1 o #1) (#1 params);

   |>> 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 *)
+
+fun collect_global_witnesses thy parms ids vts = let
+    val ts = map Logic.unvarify vts;
+    val (parms, parmTs) = split_list parms;
+    val parmvTs = map Type.varifyT parmTs;
+    val vtinst = fold (Sign.typ_match thy) (parmvTs ~~ map Term.fastype_of ts) Vartab.empty;
+    val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T))
+        |> Symtab.make;            
+    (* replace parameter names in ids by instantiations *)
+    val vinst = Symtab.make (parms ~~ vts);
+    fun vinst_names ps = map (fn p => Symtab.lookup (vinst, p) |> valOf) ps;
+    val inst = Symtab.make (parms ~~ ts);
+    val ids' = map (apsnd vinst_names) ids;
+    val wits = List.concat (map (snd o valOf o get_global_registration thy) ids');
+  in ((inst, tinst), wits) end;
+
+
 (* store instantiations of args for all registered interpretations
    of the theory *)
 
 fun note_thmss_registrations kind target args thy =
   let
-    val (parms, parmTs) =
-          the_locale thy target |> #params |> fst |> map fst |> split_list;
-    val parmvTs = map Type.varifyT parmTs;
+    val parms = the_locale thy target |> #params |> fst |> map fst;
     val ids = flatten (ProofContext.init thy, intern_expr thy)
       (([], Symtab.empty), Expr (Locale target)) |> fst |> fst
       |> List.mapPartial (fn (id, (_, Assumed _)) => SOME id | _ => NONE)
 
     val regs = get_global_registrations thy target;
 
     (* add args to thy for all registrations *)
 
     fun activate (thy, (vts, ((prfx, atts2), _))) =
       let
-        val ts = map Logic.unvarify vts;
-        (* type instantiation *)
-        val vtinst = fold (Sign.typ_match thy) (parmvTs ~~ map Term.fastype_of ts) Vartab.empty;
-        val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T))
-             |> Symtab.make;            
-        (* replace parameter names in ids by instantiations *)
-        val vinst = Symtab.make (parms ~~ vts);
-        fun vinst_names ps = map (fn p => Symtab.lookup (vinst, p) |> valOf) ps;
-        val inst = Symtab.make (parms ~~ ts);
-        val ids' = map (apsnd vinst_names) ids;
-        val prems = List.concat (map (snd o valOf o get_global_registration thy) ids');
+        val ((inst, tinst), prems) = collect_global_witnesses thy parms ids vts;
         val args' = map (fn ((n, atts), [(ths, [])]) =>
             ((NameSpace.qualified prfx n,
-              map (Attrib.global_attribute_i thy) (atts @ atts2)),
-             [(map (Drule.standard o Drule.satisfy_hyps prems o inst_tab_thm thy (inst, tinst)) ths, [])]))
+              map (Attrib.global_attribute_i thy)
+                  (inst_tab_atts thy (inst, tinst) atts @ atts2)),
+             [(map (Drule.standard o Drule.satisfy_hyps prems o
+                inst_tab_thm thy (inst, tinst)) ths, [])]))
           args;
       in global_note_accesses_i (Drule.kind kind) prfx args' thy |> fst end;
   in Library.foldl activate (thy, regs) end;
 
 

 
 local
 
 (* extract proof obligations (assms and defs) from elements *)
 
-fun extract_asms_elem (ts, Fixes _) = ts
-  | extract_asms_elem (ts, Constrains _) = ts
-  | extract_asms_elem (ts, Assumes asms) =
+fun extract_asms_elem (Fixes _) ts = ts
+  | extract_asms_elem (Constrains _) ts = ts
+  | extract_asms_elem (Assumes asms) ts =
       ts @ List.concat (map (fn (_, ams) => map (fn (t, _) => t) ams) asms)
-  | extract_asms_elem (ts, Defines defs) =
+  | extract_asms_elem (Defines defs) ts =
       ts @ map (fn (_, (def, _)) => def) defs
-  | extract_asms_elem (ts, Notes _) = ts;
+  | extract_asms_elem (Notes _) ts = ts;
 
 fun extract_asms_elems ((id, Assumed _), elems) =
-      SOME (id, Library.foldl extract_asms_elem ([], elems))
-  | extract_asms_elems ((_, Derived _), _) = NONE;
-
-fun extract_asms_elemss elemss =
-      List.mapPartial extract_asms_elems elemss;
+      (id, fold extract_asms_elem elems [])
+  | extract_asms_elems ((id, Derived _), _) = (id, []);
+
+fun extract_asms_elemss elemss = map extract_asms_elems elemss;
 
 (* activate instantiated facts in theory or context *)
 
-fun gen_activate_facts_elemss get_reg note_thmss attrib std put_reg add_wit
+fun gen_activate_facts_elemss get_reg note attrib std put_reg add_wit
         attn all_elemss new_elemss propss result thy_ctxt =
     let
       fun activate_elem disch (prfx, atts) (Notes facts) thy_ctxt =
           let
             val facts' = facts

               |> map (apfst (apsnd (fn a => a @ map (attrib thy_ctxt) atts)))
               (* discharge hyps *)
               |> map (apsnd (map (apfst (map disch))))
               (* prefix names *)
               |> map (apfst (apfst (NameSpace.qualified prfx)))
-          in fst (note_thmss prfx facts' thy_ctxt) end
+          in fst (note prfx facts' thy_ctxt) end
         | activate_elem _ _ _ thy_ctxt = thy_ctxt;
 
-      fun activate_elems disch ((id, mode), elems) thy_ctxt =
+      fun activate_elems disch ((id, _), elems) thy_ctxt =
           let
             val ((prfx, atts2), _) = valOf (get_reg thy_ctxt id)
                 handle Option => sys_error ("Unknown registration of " ^
                   quote (fst id) ^ " while activating facts.");
           in

 
 fun prep_registration_in_locale target expr thy =
   (* target already in internal form *)
   let
     val ctxt = ProofContext.init thy;
-    val ((target_ids, target_syn), target_elemss) = flatten (ctxt, I)
+    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)
-        ((target_ids, target_syn), Expr expr);
-    val ids = Library.drop (length target_ids, all_ids);
-    val ((parms, elemss, _), _) =
-        read_elemss false ctxt fixed raw_elemss [];
+        ((raw_target_ids, target_syn), Expr expr);
+    val (target_ids, ids) = splitAt (length raw_target_ids, all_ids);
+    val ((parms, elemss, _), _) = read_elemss false ctxt fixed raw_elemss [];
 
     (** compute proof obligations **)
 
     (* restore "small" ids, with mode *)
     val ids' = map (apsnd snd) ids;
     (* remove Int markers *)
     val elemss' = map (fn (_, es) =>
         map (fn Int e => e) es) elemss
     (* extract assumptions and defs *)
-    val propss = extract_asms_elemss (ids' ~~ elemss');
-
-    (** activation function: add registrations **)
+    val ids_elemss = ids' ~~ elemss';
+    val propss = extract_asms_elemss ids_elemss;
+
+    (** activation function:
+        - add registrations to the target locale
+        - add induced registrations for all global registrations of
+          the target, unless already present
+        - add facts of induced registrations to theory **)
+
+    val t_ids = List.mapPartial
+        (fn (id, (_, Assumed _)) => SOME id | _ => NONE) target_ids;
+
     fun activate locale_results thy = let
-        val thmss = unflat (map snd propss) locale_results;
-        fun activate_id (id, thms) thy =
+        val ids_elemss_thmss = ids_elemss ~~
+	    unflat (map snd propss) locale_results;
+        val regs = get_global_registrations thy target;
+
+        fun activate_id (((id, Assumed _), _), thms) thy =
             thy |> put_registration_in_locale target id
-                |> fold (add_witness_in_locale target id) thms;
+                |> fold (add_witness_in_locale target id) thms
+          | activate_id _ thy = thy;
+
+        fun activate_reg (vts, ((prfx, atts2), _)) thy = let
+            val ((inst, tinst), wits) =
+                collect_global_witnesses thy fixed t_ids vts;
+            fun inst_parms ps = map (fn p =>
+                  valOf (assoc (map #1 fixed ~~ vts, p))) ps;
+            val disch = Drule.fconv_rule (Thm.beta_conversion true) o
+                Drule.satisfy_hyps wits;
+            val new_elemss = List.filter (fn (((name, ps), _), _) =>
+                not (test_global_registration thy (name, inst_parms ps))) (ids_elemss);
+            fun activate_assumed_id (((_, Derived _), _), _) thy = thy
+              | activate_assumed_id ((((name, ps), Assumed _), _), thms) thy = let
+                val ps' = inst_parms ps;
+              in
+                if test_global_registration thy (name, ps')
+                then thy
+                else thy
+                  |> put_global_registration (name, ps') (prfx, atts2)
+                  |> fold (fn thm => fn thy => add_global_witness (name, ps')
+                       ((disch o inst_tab_thm thy (inst, tinst)) thm) thy) thms
+              end;
+
+            fun activate_derived_id ((_, Assumed _), _) thy = thy
+              | activate_derived_id (((name, ps), Derived ths), _) thy = let
+                val ps' = inst_parms ps;
+              in
+                if test_global_registration thy (name, ps')
+                then thy
+                else thy
+                  |> put_global_registration (name, ps') (prfx, atts2)
+                  |> fold (fn thm => fn thy => add_global_witness (name, ps')
+                       ((disch o inst_tab_thm thy (inst, tinst) o Drule.satisfy_hyps locale_results) thm) thy) ths
+              end;
+
+            fun activate_elem (Notes facts) thy =
+                let
+                  val facts' = facts
+                      |> Attrib.map_facts (Attrib.global_attribute_i thy o
+                         Args.map_values I (tinst_tab_type tinst)
+                           (inst_tab_term (inst, tinst))
+                           (disch o inst_tab_thm thy (inst, tinst) o
+                            Drule.satisfy_hyps locale_results))
+                      |> map (apfst (apsnd (fn a => a @ map (Attrib.global_attribute thy) atts2)))
+                      |> map (apsnd (map (apfst (map (disch o inst_tab_thm thy (inst, tinst) o Drule.satisfy_hyps locale_results)))))
+                      |> map (apfst (apfst (NameSpace.qualified prfx)))
+                in
+                  fst (global_note_accesses_i (Drule.kind "") prfx facts' thy)
+                end
+              | activate_elem _ thy = thy;
+
+            fun activate_elems (_, elems) thy = fold activate_elem elems thy;
+
+          in thy |> fold activate_assumed_id ids_elemss_thmss
+                 |> fold activate_derived_id ids_elemss
+                 |> fold activate_elems new_elemss end;
       in
-        fold activate_id (map fst propss ~~ thmss) thy
+        thy |> fold activate_id ids_elemss_thmss
+            |> fold activate_reg regs
       end;
 
   in (propss, activate) end;
 
 end;  (* local *)