# HG changeset patch
# User ballarin
# Date 1229081460 -3600
# Node ID ab99da3854afecfb122b4a3e085383f6f05070e3
# Parent  4025459e3f83fcabe2c4cf42ab7e141a353fef01
Equations in interpretation as goals.

diff -r 4025459e3f83 -r ab99da3854af src/FOL/ex/NewLocaleSetup.thy
--- a/src/FOL/ex/NewLocaleSetup.thy	Thu Dec 11 17:56:34 2008 +0100
+++ b/src/FOL/ex/NewLocaleSetup.thy	Fri Dec 12 12:31:00 2008 +0100
@@ -45,8 +45,7 @@
   OuterSyntax.command "interpretation"
     "prove interpretation of locale expression in theory" K.thy_goal
     (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)) []
+      Scan.optional (P.$$$ "where" |-- P.and_list1 (SpecParse.opt_thm_name ":" -- P.prop)) []
         >> (fn (expr, mixin) => Toplevel.print o
             Toplevel.theory_to_proof (Expression.interpretation_cmd expr mixin)));
 
diff -r 4025459e3f83 -r ab99da3854af src/FOL/ex/NewLocaleTest.thy
--- a/src/FOL/ex/NewLocaleTest.thy	Thu Dec 11 17:56:34 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy	Fri Dec 12 12:31:00 2008 +0100
@@ -421,16 +421,15 @@
 
 end
 
-lemma bool_logic_o: "PROP logic_o(op &, Not)"
-  by unfold_locales fast+
+interpretation x: logic_o "op &" "Not"
+  where bool_logic_o: "logic_o.lor_o(op &, Not, x, y) <-> x | y"
+proof -
+  show bool_logic_o: "PROP logic_o(op &, Not)" by unfold_locales fast+
+  show "logic_o.lor_o(op &, Not, x, y) <-> x | y"
+    by (unfold logic_o.lor_o_def [OF bool_logic_o]) fast
+qed
 
-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
+thm x.lor_o_def bool_logic_o
 
 lemma (in logic_o) lor_triv: "x || y <-> x || y" by fast
 
diff -r 4025459e3f83 -r ab99da3854af src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Thu Dec 11 17:56:34 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Fri Dec 12 12:31:00 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 -> Facts.ref list -> theory -> Proof.state;
-  val interpretation: expression_i -> thm list -> theory -> Proof.state;
+  val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state;
+  val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state;
   val interpret_cmd: expression -> bool -> Proof.state -> Proof.state;
   val interpret: expression_i -> bool -> Proof.state -> Proof.state;
 end;
@@ -786,41 +786,63 @@
 
 local
 
-fun gen_interpretation prep_expr prep_thms
+datatype goal = Reg of string * Morphism.morphism | Eqns of Attrib.binding list;
+
+fun gen_interpretation prep_expr parse_prop prep_attr
     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;
+    val ((propss, regs, export), expr_ctxt) = prep_expr expression ctxt;
+    
+    val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
+    val eq_attns = map ((apsnd o map) (prep_attr thy) o fst) equations;
+    val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
+    val export' = Variable.export_morphism goal_ctxt expr_ctxt;
 
-    fun store_reg ((name, morph), thms) =
-      let
-        val morph' = morph $> Element.satisfy_morphism thms;
-      in
-        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 store (Reg (name, morph), thms) (regs, thy) =
+        let
+          val thms' = map (Element.morph_witness export') thms;
+          val morph' = morph $> Element.satisfy_morphism thms';
+          val add = NewLocale.add_global_registration (name, (morph', export));
+        in ((name, morph') :: regs, add thy) end
+      | store (Eqns [], []) (regs, thy) =
+        let val add = fold_rev (fn (name, morph) =>
+              NewLocale.activate_global_facts (name, morph $> export)) regs;
+        in (regs, add thy) end
+      | store (Eqns attns, thms) (regs, thy) =
+        let
+          val thms' = thms |> map (Element.conclude_witness #>
+            Morphism.thm (export' $> export) #>
+            LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
+            Drule.abs_def);
+          val eq_morph =
+            Morphism.term_morphism (MetaSimplifier.rewrite_term thy thms' []) $>
+            Morphism.thm_morphism (MetaSimplifier.rewrite_rule thms');
+          val attns' = map ((apsnd o map) (Attrib.attribute_i thy)) attns;
+          val add =
+            fold_rev (fn (name, morph) =>
+              NewLocale.amend_global_registration eq_morph (name, morph) #>
+              NewLocale.activate_global_facts (name, morph $> eq_morph $> export)) regs #>
+            PureThy.note_thmss Thm.lemmaK (attns' ~~ map (fn th => [([th], [])]) thms') #>
+            snd
+        in (regs, add thy) end;
 
     fun after_qed results =
-      ProofContext.theory (fold store_reg (regs ~~ prep_result propss results));
+      ProofContext.theory (fn thy =>
+        fold store (map Reg regs @ [Eqns eq_attns] ~~
+          prep_result (propss @ [eqns]) results) ([], thy) |> snd);
   in
     goal_ctxt |>
-      Proof.theorem_i NONE after_qed (prep_propp propss) |>
+      Proof.theorem_i NONE after_qed (prep_propp (propss @ [eqns])) |>
       Element.refine_witness |> Seq.hd
   end;
 
 in
 
 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;
+  Syntax.parse_prop Attrib.intern_src x;
+fun interpretation x = gen_interpretation cert_goal_expression (K I) (K I) x;
 
 end;
 
diff -r 4025459e3f83 -r ab99da3854af src/Pure/Isar/new_locale.ML
--- a/src/Pure/Isar/new_locale.ML	Thu Dec 11 17:56:34 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML	Fri Dec 12 12:31:00 2008 +0100
@@ -50,7 +50,7 @@
   (* Registrations *)
   val add_global_registration: (string * (Morphism.morphism * Morphism.morphism)) ->
     theory -> theory
-  val amend_global_registration: (string * Morphism.morphism) -> Morphism.morphism ->
+  val amend_global_registration: Morphism.morphism -> (string * Morphism.morphism) ->
     theory -> theory
   val get_global_registrations: theory -> (string * Morphism.morphism) list
 
@@ -471,7 +471,7 @@
 fun add_global_registration reg =
   (Context.theory_map o RegistrationsData.map) (cons (reg, stamp ()));
 
-fun amend_global_registration (name, base_morph) morph thy =
+fun amend_global_registration morph (name, base_morph) thy =
   let
     val regs = (Context.Theory #> RegistrationsData.get #> map fst) thy;
     val base = instance_of thy name base_morph;