Interpretation in proofs supports mixins.

--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Sat Jul 31 21:14:20 2010 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Sat Jul 31 21:14:20 2010 +0200
@@ -714,4 +714,25 @@
   thm local_free.lone [where ?zero = 0]
 qed
 
+lemma True
+proof
+  {
+    fix pand and pnot and por
+    assume passoc: "!!x y z. pand(pand(x, y), z) <-> pand(x, pand(y, z))"
+      and pnotnot: "!!x. pnot(pnot(x)) <-> x"
+      and por_def: "!!x y. por(x, y) <-> pnot(pand(pnot(x), pnot(y)))"
+    interpret loc: logic_o pand pnot
+      where por_eq: "!!x y. logic_o.lor_o(pand, pnot, x, y) <-> por(x, y)"  (* FIXME *)
+    proof -
+      show logic_o: "PROP logic_o(pand, pnot)" using passoc pnotnot by unfold_locales
+      fix x y
+      show "logic_o.lor_o(pand, pnot, x, y) <-> por(x, y)"
+        by (unfold logic_o.lor_o_def [OF logic_o]) (rule por_def [symmetric])
+    qed
+    print_interps logic_o  (* FIXME *)
+    thm loc.lor_o_def por_eq
+    have "!!x y. por(x, y) <-> pnot(pand(pnot(x), pnot(y)))" by (rule loc.lor_o_def)
+  }
+qed
+
 end

--- a/src/Pure/Isar/element.ML	Sat Jul 31 21:14:20 2010 +0200
+++ b/src/Pure/Isar/element.ML	Sat Jul 31 21:14:20 2010 +0200
@@ -40,6 +40,9 @@
     term list list -> term list -> Proof.context -> Proof.state
   val witness_local_proof: (witness list list -> Proof.state -> Proof.state) ->
     string -> term list list -> Proof.context -> bool -> Proof.state -> Proof.state
+  val witness_local_proof_eqs: (witness list list -> thm list -> Proof.state -> Proof.state) ->
+    string -> term list list -> term list -> Proof.context -> bool -> Proof.state ->
+    Proof.state
   val morph_witness: morphism -> witness -> witness
   val conclude_witness: witness -> thm
   val pretty_witness: Proof.context -> witness -> Pretty.T
@@ -57,6 +60,8 @@
     (Attrib.binding * (thm list * Attrib.src list) list) list
   val eq_morphism: theory -> thm list -> morphism option
   val transfer_morphism: theory -> morphism
+  val generic_note_thmss: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
+    Context.generic -> (string * thm list) list * Context.generic
   val init: context_i -> Context.generic -> Context.generic
   val activate_i: context_i -> Proof.context -> context_i * Proof.context
   val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context
@@ -280,6 +285,10 @@
       in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
   in proof after_qed' propss #> refine_witness #> Seq.hd end;
 
+fun proof_local cmd goal_ctxt int after_qed' propss =
+    Proof.map_context (K goal_ctxt)
+    #> Proof.local_goal (Proof_Display.print_results int) (K I) ProofContext.bind_propp_i
+      cmd NONE after_qed' (map (pair Thm.empty_binding) propss);
 in
 
 fun witness_proof after_qed wit_propss =
@@ -289,12 +298,11 @@
 val witness_proof_eqs = gen_witness_proof (Proof.theorem NONE);
 
 fun witness_local_proof after_qed cmd wit_propss goal_ctxt int =
-  gen_witness_proof (fn after_qed' => fn propss =>
-    Proof.map_context (K goal_ctxt)
-    #> Proof.local_goal (Proof_Display.print_results int) (K I) ProofContext.bind_propp_i
-      cmd NONE after_qed' (map (pair Thm.empty_binding) propss))
+  gen_witness_proof (proof_local cmd goal_ctxt int)
     (fn wits => fn _ => after_qed wits) wit_propss [];
 
+fun witness_local_proof_eqs after_qed cmd wit_propss eq_props goal_ctxt int =
+  gen_witness_proof (proof_local cmd goal_ctxt int) after_qed wit_propss eq_props;
 end;
 
 
@@ -467,6 +475,15 @@
 
 (* init *)
 
+fun generic_note_thmss kind facts context =
+  let
+    val facts' = Attrib.map_facts (Attrib.attribute_i (Context.theory_of context)) facts;
+  in
+    context |> Context.mapping_result
+      (PureThy.note_thmss kind facts')
+      (ProofContext.note_thmss kind facts')
+  end;
+
 fun init (Fixes fixes) = Context.map_proof (ProofContext.add_fixes fixes #> #2)
   | init (Constrains _) = I
   | init (Assumes asms) = Context.map_proof (fn ctxt =>
@@ -486,13 +503,7 @@
           |> fold Variable.auto_fixes (map #1 asms)
           |> ProofContext.add_assms_i Local_Defs.def_export (map #2 asms);
       in ctxt' end)
-  | init (Notes (kind, facts)) = (fn context =>
-      let
-        val facts' = Attrib.map_facts (Attrib.attribute_i (Context.theory_of context)) facts;
-        val context' = context |> Context.mapping
-          (PureThy.note_thmss kind facts' #> #2)
-          (ProofContext.note_thmss kind facts' #> #2);
-      in context' end);
+  | init (Notes (kind, facts)) = generic_note_thmss kind facts #> #2;
 
 
 (* activate *)

--- a/src/Pure/Isar/expression.ML	Sat Jul 31 21:14:20 2010 +0200
+++ b/src/Pure/Isar/expression.ML	Sat Jul 31 21:14:20 2010 +0200
@@ -43,8 +43,8 @@
   val sublocale_cmd: string -> expression -> theory -> Proof.state
   val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state
   val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state
-  val interpret: expression_i -> bool -> Proof.state -> Proof.state
-  val interpret_cmd: expression -> bool -> Proof.state -> Proof.state
+  val interpret: expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state
+  val interpret_cmd: expression -> (Attrib.binding * string) list -> bool -> Proof.state -> Proof.state
 end;
 
 structure Expression : EXPRESSION =
@@ -790,10 +790,29 @@
 
 (*** Interpretation ***)
 
-(** Interpretation in theories **)
+(** Interpretation in theories and proof contexts **)
 
 local
 
+fun note_eqns_register deps witss attrss eqns export export' context =
+  let
+    fun meta_rewrite context =
+      map (Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def) o
+        maps snd;
+  in
+    context
+    |> Element.generic_note_thmss Thm.lemmaK
+      (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn],[])]) eqns)
+    |-> (fn facts => `(fn context => meta_rewrite context facts))
+    |-> (fn eqns => fold (fn ((dep, morph), wits) =>
+      fn context =>
+        Locale.add_registration (dep, morph $> Element.satisfy_morphism
+            (map (Element.morph_witness export') wits))
+          (Element.eq_morphism (Context.theory_of context) eqns |>
+            Option.map (rpair true))
+          export context) (deps ~~ witss))
+  end;
+
 fun gen_interpretation prep_expr parse_prop prep_attr
     expression equations theory =
   let
@@ -805,36 +824,42 @@
     val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
     val export' = Variable.export_morphism goal_ctxt expr_ctxt;
 
-    fun note_eqns raw_eqns thy =
-      let
-        val eqns = map (Morphism.thm (export' $> export)) raw_eqns;
-        val eqn_attrss = map2 (fn attrs => fn eqn =>
-          ((apsnd o map) (Attrib.attribute_i thy) attrs, [([eqn], [])])) attrss eqns;
-        fun meta_rewrite thy =
-          map (Local_Defs.meta_rewrite_rule (ProofContext.init_global thy) #> Drule.abs_def) o
-            maps snd;
-      in
-        thy
-        |> PureThy.note_thmss Thm.lemmaK eqn_attrss
-        |-> (fn facts => `(fn thy => meta_rewrite thy facts))
-      end;
-
-    fun after_qed witss eqns = ProofContext.theory (note_eqns eqns
-      #-> (fn eqns => fold (fn ((dep, morph), wits) =>
-        fn thy => Context.theory_map
-          (Locale.add_registration (dep, morph $> Element.satisfy_morphism
-              (map (Element.morph_witness export') wits))
-            (Element.eq_morphism thy eqns |> Option.map (rpair true))
-            export) thy) (deps ~~ witss)));
+    fun after_qed witss eqns = (ProofContext.theory o Context.theory_map)
+      (note_eqns_register deps witss attrss eqns export export');
 
   in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
 
+fun gen_interpret prep_expr parse_prop prep_attr
+    expression equations int state =
+  let
+    val _ = Proof.assert_forward_or_chain state;
+    val ctxt = Proof.context_of state;
+    val theory = ProofContext.theory_of ctxt;
+
+    val ((propss, deps, export), expr_ctxt) = prep_expr expression ctxt;
+
+    val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
+    val attrss = map ((apsnd o map) (prep_attr theory) o fst) equations;
+    val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
+    val export' = Variable.export_morphism goal_ctxt expr_ctxt;
+
+    fun after_qed witss eqns = (Proof.map_context o Context.proof_map)
+      (note_eqns_register deps witss attrss eqns export export');
+  in
+    state
+    |> Element.witness_local_proof_eqs after_qed "interpret" propss eqns goal_ctxt int
+  end;
+
 in
 
 fun interpretation x = gen_interpretation cert_goal_expression (K I) (K I) x;
 fun interpretation_cmd x = gen_interpretation read_goal_expression
   Syntax.parse_prop Attrib.intern_src x;
 
+fun interpret x = gen_interpret cert_goal_expression (K I) (K I) x;
+fun interpret_cmd x = gen_interpret read_goal_expression
+  Syntax.parse_prop Attrib.intern_src x;
+
 end;
 
 
@@ -859,36 +884,5 @@
 
 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 Context.proof_map (Locale.activate_facts (name, morph')) end;
-
-    fun after_qed wits =
-      Proof.map_context (fold2 store_reg regs wits);
-  in
-    state
-    |> Element.witness_local_proof after_qed "interpret" propss goal_ctxt int
-  end;
-
-in
-
-fun interpret x = gen_interpret cert_goal_expression x;
-fun interpret_cmd x = gen_interpret read_goal_expression x;
-
 end;
 
-end;
-

--- a/src/Pure/Isar/isar_syn.ML	Sat Jul 31 21:14:20 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat Jul 31 21:14:20 2010 +0200
@@ -444,8 +444,10 @@
   Outer_Syntax.command "interpret"
     "prove interpretation of locale expression in proof context"
     (Keyword.tag_proof Keyword.prf_goal)
-    (Parse.!!! (Parse_Spec.locale_expression true)
-      >> (fn expr => Toplevel.print o Toplevel.proof' (Expression.interpret_cmd expr)));
+    (Parse.!!! (Parse_Spec.locale_expression true) --
+      Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
+      >> (fn (expr, equations) => Toplevel.print o
+          Toplevel.proof' (Expression.interpret_cmd expr equations)));
 
 
 (* classes *)