# HG changeset patch
# User ballarin
# Date 1126874791 -7200
# Node ID 9deaf32c83bec13f3b147bd011c5e984b10faa36
# Parent  4e603046e53979829d84593681021d96abc40646
interpretation uses primitive goal interface

diff -r 4e603046e539 -r 9deaf32c83be src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Sep 16 14:44:52 2005 +0200
+++ b/src/Pure/Isar/locale.ML	Fri Sep 16 14:46:31 2005 +0200
@@ -11,6 +11,10 @@
 (with merge and rename operations), as well as type-inference of the
 signature parts, and predicate definitions of the specification text.
 
+Interpretation enables the reuse of theorems of locales in other
+contexts, namely those defined by theories, structured proofs and
+locales themselves.
+
 See also:
 
 [1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar.
@@ -24,7 +28,6 @@
 - 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 =
@@ -1617,13 +1620,10 @@
 
 in
 
-(* CB: processing of locales for add_locale(_i) and print_locale *)
-  (* 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 (map Elem y) [] z);
 fun cert_context x y z = #1 (gen_context_i true [] x (map Elem y) [] z);
 
-(* CB: processing of locales for note_thmss(_i),
-   Proof.multi_theorem(_i) and antiquotations with option "locale" *)
 val read_context_statement = gen_statement intern gen_context;
 val cert_context_statement = gen_statement (K I) gen_context_i;
 
@@ -2002,7 +2002,7 @@
     val extraTs = foldr Term.add_term_tfrees [] exts' \\
       foldr Term.add_typ_tfrees [] (map #2 parms);
     val _ = if null extraTs then ()
-      else warning ("Additional type variables in locale specification: " ^ quote bname);
+      else warning ("Additional type variable(s) in locale specification " ^ quote bname);
 
     val (pred_thy, (elemss', predicate as (predicate_statement, predicate_axioms))) =
       if do_pred then thy |> define_preds bname text elemss
@@ -2410,7 +2410,15 @@
   in (propss, activate) end;
 
 fun prep_propp propss = propss |> map (fn ((name, _), props) =>
-  ((NameSpace.base name, []), map (rpair ([], [])) props));
+  map (rpair ([], [])) props);
+
+fun prop_name thy propss =
+    propss |> map (fn ((name, _), _) => extern thy name);
+fun goal_name thy kind NONE propss =
+    kind ^ (Proof.goal_names NONE "" (prop_name thy propss))
+  | goal_name thy kind (SOME target) propss =
+    kind ^ (Proof.goal_names (SOME (extern thy target)) ""
+      (prop_name thy propss));
 
 in
 
@@ -2420,24 +2428,40 @@
     val (propss, activate) = prep_global_registration (prfx, atts) expr insts thy;
     fun after_qed (goal_ctxt, raw_results) _ =
       activate (map (ProofContext.export_plain goal_ctxt thy_ctxt) raw_results);
-  in Proof.theorem_i Drule.internalK after_qed NONE ("", []) (prep_propp propss) thy_ctxt end;
+  in
+    Proof.generic_goal
+      (ProofContext.bind_propp_schematic_i #> Proof.auto_fix)
+      (goal_name thy "interpretation" NONE propss)
+      (K (K Seq.single), after_qed) (prep_propp propss) (Proof.init thy_ctxt)
+  end;
 
 fun interpretation_in_locale (raw_target, expr) thy =
   let
+    val thy_ctxt = ProofContext.init thy;
     val target = intern thy raw_target;
     val (propss, activate) = prep_registration_in_locale target expr thy;
-    fun after_qed ((goal_ctxt, locale_ctxt), raw_results) _ =
-      activate (map (ProofContext.export_plain goal_ctxt locale_ctxt) raw_results);
+    val (_, (target_view, _), target_ctxt, _, propp) =
+      cert_context_statement (SOME target) [] (prep_propp propss) thy_ctxt;
+    val target_ctxt' = target_ctxt |> ProofContext.add_view thy_ctxt target_view;
+    fun after_qed (goal_ctxt, raw_results) _ =
+      activate (map (ProofContext.export_plain goal_ctxt target_ctxt') raw_results);
   in
-    theorem_in_locale_i Drule.internalK after_qed target ("", []) [] (prep_propp propss) thy
+    Proof.generic_goal 
+      (ProofContext.bind_propp_schematic_i #> Proof.auto_fix)
+      (goal_name thy "interpretation" (SOME target) propss)
+      (K (K Seq.single), after_qed) propp (Proof.init target_ctxt')
   end;
 
-fun interpret (prfx, atts) expr insts int state =
+fun interpret (prfx, atts) expr insts _ state =
   let
     val (propss, activate) =
       prep_local_registration (prfx, atts) expr insts (Proof.context_of state);
     fun after_qed (_, raw_results) _ = Seq.single o Proof.map_context (activate raw_results);
-  in Proof.have_i after_qed (prep_propp propss) int state end;
+  in
+    Proof.generic_goal ProofContext.bind_propp_i
+      (goal_name (Proof.theory_of state) "interpret" NONE propss)
+      (after_qed, K (K I)) (prep_propp propss) state
+  end;
 
 end;
 
diff -r 4e603046e539 -r 9deaf32c83be src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Sep 16 14:44:52 2005 +0200
+++ b/src/Pure/Isar/proof.ML	Fri Sep 16 14:46:31 2005 +0200
@@ -83,12 +83,20 @@
   val apply: Method.text -> state -> state Seq.seq
   val apply_end: Method.text -> state -> state Seq.seq
   val goal_names: string option -> string -> string list -> string
+  val generic_goal:
+   (context * 'a -> context * (term list list * (context -> context))) ->
+   string ->
+   (context * thm list -> thm list list -> state -> state Seq.seq) *
+   (context * thm list -> thm list list -> theory -> theory) ->
+   'a -> state -> state
   val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
     (theory -> 'a -> context attribute) ->
     (context * 'b list -> context * (term list list * (context -> context))) ->
     string -> (context * thm list -> thm list list -> state -> state Seq.seq) ->
     ((string * 'a list) * 'b) list -> state -> state
   val local_qed: Method.text option * bool -> state -> state Seq.seq
+  val auto_fix: context * (term list list * 'a) ->
+    context * (term list list * 'a)
   val global_goal: (context -> (string * string) * (string * thm list) list -> unit) ->
    (theory -> 'a -> theory attribute) ->
    (context * 'b list -> context * (term list list * (context -> context))) ->
@@ -832,6 +840,9 @@
 
 (* global goals *)
 
+fun auto_fix (ctxt, (propss, after_ctxt)) =
+  (ctxt |> ProofContext.fix_frees (List.concat propss), (propss, after_ctxt));
+
 fun global_goal print_results prep_att prepp
     kind after_qed target (name, raw_atts) stmt ctxt =
   let
@@ -850,8 +861,7 @@
           #2 o global_results kind [((name, atts), List.concat (map #2 res'))]))
       #> after_qed raw_results results;
 
-    val prepp' = prepp #> (fn (ctxt, (propss, after_ctxt)) =>
-      (ctxt |> ProofContext.fix_frees (List.concat propss), (propss, after_ctxt)));
+    val prepp' = prepp #> auto_fix;
   in
     init ctxt
     |> generic_goal prepp' (kind ^ goal_names target name names)