Interpretation in theories: first version with equations.

--- a/src/FOL/ex/NewLocaleSetup.thy	Thu Dec 11 17:55:51 2008 +0100
+++ b/src/FOL/ex/NewLocaleSetup.thy	Thu Dec 11 17:56:34 2008 +0100
@@ -44,9 +44,11 @@
 val _ =
   OuterSyntax.command "interpretation"
     "prove interpretation of locale expression in theory" K.thy_goal
-    (P.!!! SpecParse.locale_expression
-        >> (fn expr => Toplevel.print o
-            Toplevel.theory_to_proof (Expression.interpretation_cmd expr)));
+    (P.!!! SpecParse.locale_expression --
+      Scan.optional (P.$$$ "where" |-- P.and_list1 (P.alt_string >> Facts.Fact ||
+    P.position P.xname -- Scan.option Attrib.thm_sel >> Facts.Named)) []
+        >> (fn (expr, mixin) => Toplevel.print o
+            Toplevel.theory_to_proof (Expression.interpretation_cmd expr mixin)));
 
 val _ =
   OuterSyntax.command "interpret"

--- a/src/FOL/ex/NewLocaleTest.thy	Thu Dec 11 17:55:51 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy	Thu Dec 11 17:56:34 2008 +0100
@@ -304,8 +304,7 @@
   done
 
 print_locale! order_with_def
-(* Note that decls come after theorems that make use of them.
-  Appears to be harmless at least in this example. *)
+(* Note that decls come after theorems that make use of them. *)
 
 
 (* locale with many parameters ---
@@ -408,7 +407,37 @@
   by unfold_locales
 
 
-section {* Interpretation in proofs *}
+subsection {* Equations *}
+
+locale logic_o =
+  fixes land (infixl "&&" 55)
+    and lnot ("-- _" [60] 60)
+  assumes assoc_o: "(x && y) && z <-> x && (y && z)"
+    and notnot_o: "-- (-- x) <-> x"
+begin
+
+definition lor_o (infixl "||" 50) where
+  "x || y <-> --(-- x && -- y)"
+
+end
+
+lemma bool_logic_o: "PROP logic_o(op &, Not)"
+  by unfold_locales fast+
+
+lemma bool_lor_eq: "logic_o.lor_o(op &, Not, x, y) <-> x | y"
+  by (unfold logic_o.lor_o_def [OF bool_logic_o]) fast
+
+interpretation x: logic_o "op &" "Not" where bool_lor_eq
+  by (rule bool_logic_o)
+
+thm x.lor_o_def
+
+lemma (in logic_o) lor_triv: "x || y <-> x || y" by fast
+
+(* thm x.lor_triv *)
+
+
+subsection {* Interpretation in proofs *}
 
 lemma True
 proof

--- a/src/Pure/Isar/expression.ML	Thu Dec 11 17:55:51 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Thu Dec 11 17:56:34 2008 +0100
@@ -28,8 +28,8 @@
   (* Interpretation *)
   val sublocale_cmd: string -> expression -> theory -> Proof.state;
   val sublocale: string -> expression_i -> theory -> Proof.state;
-  val interpretation_cmd: expression -> theory -> Proof.state;
-  val interpretation: expression_i -> theory -> Proof.state;
+  val interpretation_cmd: expression -> Facts.ref list -> theory -> Proof.state;
+  val interpretation: expression_i -> thm list -> theory -> Proof.state;
   val interpret_cmd: expression -> bool -> Proof.state -> Proof.state;
   val interpret: expression_i -> bool -> Proof.state -> Proof.state;
 end;
@@ -786,19 +786,26 @@
 
 local
 
-fun gen_interpretation prep_expr
-    expression thy =
+fun gen_interpretation prep_expr prep_thms
+    expression equations thy =
   let
     val ctxt = ProofContext.init thy;
 
+    val eqns = equations |> prep_thms ctxt |>
+      map (Drule.abs_def o LocalDefs.meta_rewrite_rule ctxt);
+    val eq_morph =
+      Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
+      Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns);
+
     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;
+        val morph' = morph $> Element.satisfy_morphism thms;
       in
-        NewLocale.add_global_registration (name, morph') #>
-        NewLocale.activate_global_facts (name, morph')
+        NewLocale.add_global_registration (name, (morph', export)) #>
+        NewLocale.amend_global_registration (name, morph') eq_morph #>
+        NewLocale.activate_global_facts (name, morph' $> eq_morph $> export)
       end;
 
     fun after_qed results =
@@ -811,8 +818,9 @@
 
 in
 
-fun interpretation_cmd x = gen_interpretation read_goal_expression x;
-fun interpretation x = gen_interpretation cert_goal_expression x;
+fun interpretation_cmd x = gen_interpretation read_goal_expression
+  (fn ctxt => map (ProofContext.get_fact ctxt) #> flat) x;
+fun interpretation x = gen_interpretation cert_goal_expression (K I) x;
 
 end;
 

--- a/src/Pure/Isar/new_locale.ML	Thu Dec 11 17:55:51 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML	Thu Dec 11 17:56:34 2008 +0100
@@ -48,7 +48,10 @@
   val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
 
   (* Registrations *)
-  val add_global_registration: (string * Morphism.morphism) -> theory -> theory
+  val add_global_registration: (string * (Morphism.morphism * Morphism.morphism)) ->
+    theory -> theory
+  val amend_global_registration: (string * Morphism.morphism) -> Morphism.morphism ->
+    theory -> theory
   val get_global_registrations: theory -> (string * Morphism.morphism) list
 
   (* Diagnostic *)
@@ -454,7 +457,8 @@
 (* FIXME only global variant needed *)
 structure RegistrationsData = GenericDataFun
 (
-  type T = ((string * Morphism.morphism) * stamp) list;
+  type T = ((string * (Morphism.morphism * Morphism.morphism)) * stamp) list;
+(* FIXME mixins need to be stamped *)
     (* registrations, in reverse order of declaration *)
   val empty = [];
   val extend = I;
@@ -462,9 +466,26 @@
     (* FIXME consolidate with dependencies, consider one data slot only *)
 );
 
-val get_global_registrations = map fst o RegistrationsData.get o Context.Theory;
+val get_global_registrations =
+  Context.Theory #> RegistrationsData.get #> map fst #> map (apsnd op $>);
 fun add_global_registration reg =
   (Context.theory_map o RegistrationsData.map) (cons (reg, stamp ()));
 
+fun amend_global_registration (name, base_morph) morph thy =
+  let
+    val regs = (Context.Theory #> RegistrationsData.get #> map fst) thy;
+    val base = instance_of thy name base_morph;
+    fun match (name', (morph', _)) =
+      name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph');
+    val i = find_index match (rev regs);
+    val _ = if i = ~1 then error ("No interpretation of locale " ^
+        quote (extern thy name) ^ " and parameter instantiation " ^
+        space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available.")
+      else ();
+  in
+    (Context.theory_map o RegistrationsData.map) (nth_map (length regs - 1 - i)
+      (fn ((name, (base, export)), stamp) => ((name, (base $> morph, export)), stamp))) thy
+  end;
+
 end;