Interpretation in proof contexts.

--- a/src/FOL/ex/NewLocaleSetup.thy	Fri Dec 05 11:42:27 2008 +0100
+++ b/src/FOL/ex/NewLocaleSetup.thy	Fri Dec 05 16:41:36 2008 +0100
@@ -41,11 +41,19 @@
 
 val _ =
   OuterSyntax.command "interpretation"
-    "prove and register interpretation of locale expression in theory" K.thy_goal
+    "prove interpretation of locale expression in theory" K.thy_goal
     (P.!!! Expression.parse_expression
         >> (fn expr => Toplevel.print o
             Toplevel.theory_to_proof (Expression.interpretation_cmd expr)));
 
+val _ =
+  OuterSyntax.command "interpret"
+    "prove interpretation of locale expression in proof context"
+    (K.tag_proof K.prf_goal)
+    (P.!!! Expression.parse_expression
+        >> (fn expr => Toplevel.print o
+            Toplevel.proof' (fn int => Expression.interpret_cmd expr int)));
+
 end
 
 *}

--- a/src/FOL/ex/NewLocaleTest.thy	Fri Dec 05 11:42:27 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy	Fri Dec 05 16:41:36 2008 +0100
@@ -341,4 +341,24 @@
 
 thm two.assoc
 
+
+text {* Interpretation in proofs *}
+
+lemma True
+proof
+  interpret "local": lgrp "op +" "0" "minus"
+    by unfold_locales  (* subsumed *)
+  {
+    fix zero :: int
+    assume "!!x. zero + x = x" "!!x. (-x) + x = zero"
+    then interpret local_fixed: lgrp "op +" zero "minus"
+      by unfold_locales
+    thm local_fixed.lone
+  }
+  assume "!!x zero. zero + x = x" "!!x zero. (-x) + x = zero"
+  then interpret local_free: lgrp "op +" zero "minus" for zero
+    by unfold_locales
+  thm local_free.lone [where ?zero = 0]
+qed
+
 end

--- a/src/Pure/Isar/expression.ML	Fri Dec 05 11:42:27 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Fri Dec 05 16:41:36 2008 +0100
@@ -28,10 +28,8 @@
   val sublocale: string -> expression_i -> theory -> Proof.state;
   val interpretation_cmd: expression -> theory -> Proof.state;
   val interpretation: expression_i -> theory -> Proof.state;
-(*
-  val interpret_cmd: Morphism.morphism -> expression -> bool -> Proof.state -> Proof.state;
-  val interpret: Morphism.morphism -> expression_i -> bool -> Proof.state -> Proof.state;
-*)
+  val interpret_cmd: expression -> bool -> Proof.state -> Proof.state;
+  val interpret: expression_i -> bool -> Proof.state -> Proof.state;
 
   (* Debugging and development *)
   val parse_expression: OuterParse.token list -> expression * OuterParse.token list
@@ -538,14 +536,12 @@
 
 fun prep_declaration prep activate raw_import raw_elems context =
   let
-    val thy = ProofContext.theory_of context;
-
     val ((fixed, deps, elems, _), (parms, (spec, (_, _, defs)))) =
       prep false true context raw_import raw_elems [];
     (* Declare parameters and imported facts *)
     val context' = context |>
       ProofContext.add_fixes_i fixed |> snd |>
-      NewLocale.clear_local_idents |> fold (NewLocale.activate_local_facts thy) deps;
+      NewLocale.clear_local_idents |> fold NewLocale.activate_local_facts deps;
     val ((elems', _), _) = activate elems (ProofContext.set_stmt true context');
   in ((fixed, deps, elems'), (parms, spec, defs)) end;
 
@@ -837,6 +833,7 @@
 
 end;
 
+
 (** Interpretation in theories **)
 
 local
@@ -846,7 +843,7 @@
   let
     val ctxt = ProofContext.init thy;
 
-    val ((propss, deps, export), goal_ctxt) = prep_expr expression ctxt;
+    val ((propss, regs, export), goal_ctxt) = prep_expr expression ctxt;
     
     fun store_reg ((name, morph), thms) =
       let
@@ -857,7 +854,7 @@
       end;
 
     fun after_qed results =
-      ProofContext.theory (fold store_reg (deps ~~ prep_result propss results));
+      ProofContext.theory (fold store_reg (regs ~~ prep_result propss results));
   in
     goal_ctxt |>
       Proof.theorem_i NONE after_qed (prep_propp propss) |>
@@ -871,5 +868,41 @@
 
 end;
 
+
+(** Interpretation in proof contexts **)
+
+local
+
+fun gen_interpret prep_expr
+    expression int state =
+  let
+    val _ = Proof.assert_forward_or_chain state;
+    val ctxt = Proof.context_of state;
+
+    val ((propss, regs, export), goal_ctxt) = prep_expr expression ctxt;
+    
+    fun store_reg ((name, morph), thms) =
+      let
+        val morph' = morph $> Element.satisfy_morphism thms $> export;
+      in
+        NewLocale.activate_local_facts (name, morph')
+      end;
+
+    fun after_qed results =
+      Proof.map_context (fold store_reg (regs ~~ prep_result propss results)) #> Seq.single;
+  in
+    state |> Proof.map_context (K goal_ctxt) |>
+      Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
+      "interpret" NONE after_qed (map (pair (Binding.empty, [])) (prep_propp propss)) |>
+      Element.refine_witness |> Seq.hd
+  end;
+
+in
+
+fun interpret_cmd x = gen_interpret read_goal_expression x;
+fun interpret x = gen_interpret cert_goal_expression x;
+
 end;
 
+end;
+

--- a/src/Pure/Isar/new_locale.ML	Fri Dec 05 11:42:27 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML	Fri Dec 05 16:41:36 2008 +0100
@@ -37,10 +37,8 @@
   (* Activation *)
   val activate_declarations: theory -> string * Morphism.morphism ->
     Proof.context -> Proof.context
-  val activate_global_facts: string * Morphism.morphism ->
-    theory -> theory
-  val activate_local_facts: theory -> string * Morphism.morphism ->
-    Proof.context -> Proof.context
+  val activate_global_facts: string * Morphism.morphism -> theory -> theory
+  val activate_local_facts: string * Morphism.morphism -> Proof.context -> Proof.context
 (*  val activate: string -> theory -> (Element.context_i -> 'a -> 'a) -> 'a -> 'a *)
   val init: string -> theory -> Proof.context
 
@@ -360,8 +358,9 @@
   roundup thy (activate_notes init_global_elem) dep (get_global_idents thy, thy) |>
   uncurry put_global_idents;
 
-fun activate_local_facts thy dep ctxt =
-  roundup thy (activate_notes init_local_elem) dep (get_local_idents ctxt, ctxt) |>
+fun activate_local_facts dep ctxt =
+  roundup (ProofContext.theory_of ctxt) (activate_notes init_local_elem) dep
+    (get_local_idents ctxt, ctxt) |>
   uncurry put_local_idents;
 
 fun init name thy = activate_all name thy init_local_elem (empty, ProofContext.init thy) |>
@@ -454,8 +453,9 @@
       "back-chain all introduction rules of locales")]));
 
 
-(*** Registrations: interpretations in theories and proof contexts ***)
+(*** Registrations: interpretations in theories ***)
 
+(* FIXME only global variant needed *)
 structure RegistrationsData = GenericDataFun
 (
   type T = ((string * Morphism.morphism) * stamp) list;
@@ -470,6 +470,5 @@
 fun add_global_registration reg =
   (Context.theory_map o RegistrationsData.map) (cons (reg, stamp ()));
 
-
 end;