# HG changeset patch
# User ballarin
# Date 1120744351 -7200
# Node ID 1e792b32abef2daac96335723dedca15f6388f46
# Parent  008d089822e35ff6127dc45fa2ce0aebb22ef6cd
Preparations for interpretation of locales in locales.

diff -r 008d089822e3 -r 1e792b32abef src/FOL/ex/LocaleTest.thy
--- a/src/FOL/ex/LocaleTest.thy	Thu Jul 07 12:42:50 2005 +0200
+++ b/src/FOL/ex/LocaleTest.thy	Thu Jul 07 15:52:31 2005 +0200
@@ -307,4 +307,8 @@
   show ?thesis by (simp only: A.OP.AC)
 qed
 
+section {* Interpretation in Locales *}
+
+interpretation M < L .
+
 end
diff -r 008d089822e3 -r 1e792b32abef src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Jul 07 12:42:50 2005 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Jul 07 15:52:31 2005 +0200
@@ -200,7 +200,7 @@
 
 val name_facts = P.and_list1 (P.opt_thm_name "=" -- P.xthms1);
 
-fun theorems kind = P.locale_target -- name_facts
+fun theorems kind = P.opt_locale_target -- name_facts
   >> uncurry (#1 ooo IsarThy.smart_theorems kind);
 
 val theoremsP =
@@ -213,7 +213,7 @@
 
 val declareP =
   OuterSyntax.command "declare" "declare theorems (improper)" K.thy_script
-    (P.locale_target -- (P.and_list1 P.xthms1 >> List.concat)
+    (P.opt_locale_target -- (P.and_list1 P.xthms1 >> List.concat)
       >> (Toplevel.theory o uncurry IsarThy.declare_theorems));
 
 
@@ -309,19 +309,27 @@
         -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, [])
       >> (Toplevel.theory o IsarThy.add_locale o (fn ((x, y), (z, w)) => (x, y, z, w))));
 
-val view_val =
+val opt_inst =
   Scan.optional (P.$$$ "[" |-- Scan.repeat1 (P.maybe P.term) --| P.$$$ "]") [];
 
 val interpretationP =
   OuterSyntax.command "interpretation"
-    "prove and register interpretation of locale expression in theory" K.thy_goal
-    (P.opt_thm_name ":" -- P.locale_expr -- P.!!! view_val
-      >> ((Toplevel.print oo Toplevel.theory_to_proof) o IsarThy.register_globally));
+    "prove and register interpretation of locale expression in theory or locale" K.thy_goal
+    (
+      (* with target: in locale *)
+      P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") --
+        P.locale_expr >>
+        ((Toplevel.print oo Toplevel.theory_to_proof) o IsarThy.register_in_locale)
+    ||
+      (* without target: in theory *)
+      P.opt_thm_name ":" -- P.locale_expr -- P.!!! opt_inst >>
+        ((Toplevel.print oo Toplevel.theory_to_proof) o IsarThy.register_globally)
+    );
 
 val interpretP =
   OuterSyntax.command "interpret"
-    "prove and register interpretation of locale expression in context" K.prf_goal
-    (P.opt_thm_name ":" -- P.locale_expr -- P.!!! view_val
+    "prove and register interpretation of locale expression in proof context" K.prf_goal
+    (P.opt_thm_name ":" -- P.locale_expr -- P.!!! opt_inst
       >> ((Toplevel.print oo Toplevel.proof) o IsarThy.register_locally));
 
 
@@ -336,7 +344,7 @@
 
 fun gen_theorem k =
   OuterSyntax.command k ("state " ^ k) K.thy_goal
-    (P.locale_target -- Scan.optional (P.opt_thm_name ":" --|
+    (P.opt_locale_target -- Scan.optional (P.opt_thm_name ":" --|
       Scan.ahead (P.locale_keyword || P.$$$ "shows")) ("", []) --
       general_statement >> (fn ((x, y), (z, w)) =>
       (Toplevel.print o Toplevel.theory_to_proof (IsarThy.smart_multi_theorem k x y z w))));
diff -r 008d089822e3 -r 1e792b32abef src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Thu Jul 07 12:42:50 2005 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Thu Jul 07 15:52:31 2005 +0200
@@ -158,6 +158,8 @@
   val register_globally:
     ((string * Attrib.src list) * Locale.expr) * string option list ->
     bool -> theory -> ProofHistory.T
+  val register_in_locale:
+    string * Locale.expr -> bool -> theory -> ProofHistory.T
   val register_locally:
     ((string * Attrib.src list) * Locale.expr) * string option list ->
     ProofHistory.T -> ProofHistory.T
@@ -645,6 +647,14 @@
         map (fn prop => (prop, ([], []))) props)) propss) int thy'
   end;
 
+fun register_in_locale (target, expr) int thy =
+  let
+    val target = Locale.intern thy target;
+  in
+    locale_multi_theorem_i Drule.internalK target ("",[]) []
+      [] (*concl*) int thy
+  end;
+
 fun register_locally (((prfx, atts), expr), insts) =
   ProofHistory.apply (fn state =>
     let
diff -r 008d089822e3 -r 1e792b32abef src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Jul 07 12:42:50 2005 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Jul 07 15:52:31 2005 +0200
@@ -88,6 +88,10 @@
   val prep_global_registration:
     string * Attrib.src list -> expr -> string option list -> theory ->
     theory * ((string * term list) * term list) list * (theory -> theory)
+(*
+  val prep_registration_in_locale:
+    string -> expr -> string option list -> theory ->
+*)
   val prep_local_registration:
     string * Attrib.src list -> expr -> string option list -> context ->
     context * ((string * term list) * term list) list * (context -> context)
@@ -126,7 +130,7 @@
 
 type locale =
  {predicate: cterm list * thm list,
-    (* CB: For old-style locales with "(open)" this entry is ([], []).
+    (* CB: For locales with "(open)" this entry is ([], []).
        For new-style locales, which declare predicates, if the locale declares
        no predicates, this is also ([], []).
        If the locale declares predicates, the record field is
@@ -137,8 +141,12 @@
     *)
   import: expr,                                       (*dynamic import*)
   elems: (element_i * stamp) list,                    (*static content*)
-  params: ((string * typ) * mixfix option) list * string list}
+  params: ((string * typ) * mixfix option) list * string list,
                                                       (*all/local params*)
+  regs: ((string * string list) * thm list) list}
+    (* Registrations: indentifiers and witness theorems of locales interpreted
+       in the locale.
+    *)
 
 
 (* CB: an internal (Int) locale element was either imported or included,
@@ -235,7 +243,7 @@
         end;
 
 
-(** registration management **)
+(** management of registrations in theories and proof contexts **)
 
 structure Registrations :
   sig
@@ -323,6 +331,7 @@
     end;
 end;
 
+
 (** theory data **)
 
 structure GlobalLocalesData = TheoryDataFun
@@ -337,11 +346,12 @@
   val copy = I;
   val extend = I;
 
-  fun join_locs _ ({predicate, import, elems, params}: locale,
-      {elems = elems', ...}: locale) =
+  fun join_locs _ ({predicate, import, elems, params, regs}: locale,
+      {elems = elems', regs = regs', ...}: locale) =
     SOME {predicate = predicate, import = import,
       elems = gen_merge_lists eq_snd elems elems',
-      params = params};
+      params = params,
+      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));
@@ -452,17 +462,6 @@
 val put_local_registration =
      gen_put_registration LocalLocalesData.map ProofContext.theory_of;
 
-(* TODO: needed? *)
-(*
-fun smart_put_registration id attn ctxt =
-  (* ignore registration if already present in theory *)
-     let
-       val thy = ProofContext.theory_of ctxt;
-     in case get_global_registration thy id of
-          NONE => put_local_registration id attn ctxt
-        | SOME _ => ctxt
-     end;
-*)
 
 (* add witness theorem to registration in theory or context,
    ignored if registration not present *)
@@ -813,8 +812,8 @@
             map (inst_thm ctxt env) axs), map (inst_elem ctxt env) elems);
       in map inst (elemss ~~ envs) end;
 
-(* like unify_elemss, but does not touch axioms,
-   additional parameter for enforcing further constraints (eg. syntax) *)
+(* like unify_elemss, but does not touch axioms, additional
+   parameter c_parms for enforcing further constraints (eg. syntax) *)
 
 fun unify_elemss' _ _ [] [] = []
   | unify_elemss' _ [] [elems] [] = [elems]
@@ -906,7 +905,7 @@
       | identify top (Merge es) =
           Library.foldl (fn ((ids, parms, syn), e) => let
                      val (ids', parms', syn') = identify top e
-                   in (gen_merge_lists eq_fst ids ids',
+                   in (merge_alists ids ids',
                        merge_lists parms parms',
                        merge_syntax ctxt ids' (syn, syn')) end)
             (([], [], Symtab.empty), es);
@@ -1288,7 +1287,14 @@
 
 end;
 
-(* CB: type inference and consistency checks for locales *)
+
+(* CB: type inference and consistency checks for locales.
+
+   Works by building a context (through declare_elemss), extracting the
+   required information and adjusting the context elements (finish_elemss).
+   Can also universally close free vars in assms and defs.  This is only
+   needed for Ext elements and controlled by parameter do_close.  
+*)
 
 fun prep_elemss prep_parms prepp do_close context fixed_params raw_elemss raw_concl =
   let
@@ -1617,12 +1623,12 @@
 
 fun put_facts loc args thy =
   let
-    val {predicate, import, elems, params} = the_locale thy loc;
+    val {predicate, import, elems, params, regs} = the_locale thy loc;
     val note = Notes (map (fn ((a, atts), bs) =>
       ((a, atts), map (apfst (map (curry Thm.name_thm a))) bs)) args);
   in
     thy |> put_locale loc {predicate = predicate, import = import,
-      elems = elems @ [(note, stamp ())], params = params}
+      elems = elems @ [(note, stamp ())], params = params, regs = regs}
   end;
 
 (* add theorem to locale and theory,
@@ -1838,7 +1844,8 @@
     |> put_locale name {predicate = predicate, import = import,
         elems = map (fn e => (e, stamp ())) (List.concat (map #2 (List.filter (equal "" o #1 o #1) elemss'))),
         params = (params_of elemss' |>
-          map (fn (x, SOME T) => ((x, T), valOf (Symtab.lookup (syn, x)))), map #1 (params_of body_elemss))}
+          map (fn (x, SOME T) => ((x, T), valOf (Symtab.lookup (syn, x)))), map #1 (params_of body_elemss)),
+        regs = []}
   end;
 
 in
@@ -1937,9 +1944,8 @@
     val ctxt' = ctxt |> ProofContext.theory_of |> ProofContext.init;
     val ((ids, _), raw_elemss) = flatten (ctxt', intern_expr thy)
           (([], Symtab.empty), Expr expr);
-    val do_close = false;  (* effect unknown *)
     val ((parms, all_elemss, _), (spec, (xs, defs, _))) =
-          read_elemss do_close ctxt' [] raw_elemss [];
+          read_elemss false ctxt' [] raw_elemss [];
 
 
     (** compute instantiation **)
diff -r 008d089822e3 -r 1e792b32abef src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Thu Jul 07 12:42:50 2005 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Thu Jul 07 15:52:31 2005 +0200
@@ -71,7 +71,8 @@
   val spec_opt_name: token list -> ((bstring * string) * Attrib.src list) * token list
   val xthm: token list -> (thmref * Attrib.src list) * token list
   val xthms1: token list -> (thmref * Attrib.src list) list * token list
-  val locale_target: token list -> xstring option * token list
+  val locale_target: token list -> xstring * token list
+  val opt_locale_target: token list -> xstring option * token list
   val locale_expr: token list -> Locale.expr * token list
   val locale_keyword: token list -> string * token list
   val locale_element: token list -> Locale.element * token list
@@ -340,7 +341,8 @@
 
 in
 
-val locale_target = Scan.option (($$$ "(" -- $$$ "in") |-- !!! (xname --| $$$ ")"));
+val locale_target = ($$$ "(" -- $$$ "in") |-- !!! (xname --| $$$ ")");
+val opt_locale_target = Scan.option locale_target;
 val locale_expr = expr0;
 val locale_keyword = loc_keyword;