Interpretation supports statically scoped attributes; documentation.

--- a/NEWS	Sun Apr 17 19:40:43 2005 +0200
+++ b/NEWS	Mon Apr 18 09:25:23 2005 +0200
@@ -163,6 +163,7 @@
   do not occur in proof obligations, neither are instantiated theorems stored
   in duplicate.
   Use print_interps to inspect active interpretations of a particular locale.
+  For details, see the Isar Reference manual.
 
 * Locales: proper static binding of attribute syntax -- i.e. types /
   terms / facts mentioned as arguments are always those of the locale

--- a/doc-src/IsarRef/generic.tex	Sun Apr 17 19:40:43 2005 +0200
+++ b/doc-src/IsarRef/generic.tex	Mon Apr 18 09:25:23 2005 +0200
@@ -180,7 +180,7 @@
     specifications included here, e.g.\ a local $simp$ rule.
 
   \item [$\INCLUDES{c}$] copies the specified context in a statically scoped
-    manner.
+    manner.  Only available in the long goal format of \S\ref{sec:goals}.
 
     In contrast, the initial $import$ specification of a locale expression
     maintains a dynamic relation to the locales being referenced (benefiting
@@ -224,6 +224,79 @@
 \end{descr}
 
 
+\subsubsection{Interpretation of locales}
+
+Locale expressions (more precisely, \emph{context expressions}) may be
+instantiated, and the instantiated facts added to the current context.
+This requires a proof of the instantiated specification and is called
+\emph{locale interpretation}.  Interpretation is possible in theories
+($\isarcmd{interpretation}$) and proof contexts
+($\isarcmd{interpret}$).
+
+\indexisarcmd{interpretation}\indexisarcmd{interpret}
+\indexisarcmd{print-interps}
+\begin{matharray}{rcl}
+  \isarcmd{interpretation} & : & \isartrans{theory}{proof(prove)} \\
+  \isarcmd{interpret} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
+  \isarcmd{print_interps}^* & : &  \isarkeep{theory~|~proof} \\
+\end{matharray}
+
+\indexouternonterm{interp}
+
+\railalias{printinterps}{print\_interps}
+\railterm{printinterps}
+
+\begin{rail}
+  'interpretation' interp
+  ;
+  'interpret' interp
+  ;
+  printinterps name
+  ;
+  interp: thmdecl? contextexpr ('[' (inst+) ']')?
+  ;
+\end{rail}
+
+\begin{descr}
+
+\item [$\isarcmd{interpretation}~expr~insts$]
+  interprets $expr$ in the theory.  The instantiation is positional.
+  All parameters must receive an instantiation term --- with the
+  exception of defined parameters.  These are, if omitted, derived
+  from the defining equation and other instantiations.  Use ``\_'' to
+  omit an instantiation term.  Free variables are automatically
+  generalized.
+
+  The context expression may be preceded by a name and/or attributes.
+  These take effect in the post-processing of facts.  The name is used
+  to prefix fact names, for example to avoid accidental hiding of
+  other facts.  Attributes are applied after attributes of the
+  interpreted facts.
+
+  The command is aware of interpretations already active in the
+  theory.  No proof obligations are generated for those, neither is
+  post-processing applied to their facts.  This avoids duplication of
+  interpreted facts, in particular.  Note that, in the case of a
+  locale with import, parts of the interpretation may already be
+  active.  The command will only generate proof obligations and add
+  facts for new parts.
+
+  Adding facts to locales has the
+  effect of adding interpreted facts to the theory for all active
+  interpretations also.
+  
+\item [$\isarcmd{interpret}~expr~insts$]
+  interprets $expr$ in the proof context and is otherwise similar to
+  the previous command.  Free variables in instantiations are not
+  generalized, however.
+
+\item [$\isarcmd{print_interps}~loc$]
+  prints the interpretations of a particular locale $loc$ that are
+  active in the current context, either theory or proof context.
+  
+\end{descr}
+
+
 \section{Derived proof schemes}
 
 \subsection{Generalized elimination}\label{sec:obtain}

--- a/src/FOL/ex/LocaleTest.thy	Sun Apr 17 19:40:43 2005 +0200
+++ b/src/FOL/ex/LocaleTest.thy	Mon Apr 18 09:25:23 2005 +0200
@@ -53,14 +53,12 @@
 
 
 interpretation p1: C ["X::'b" "Y::'b"] by (auto intro: A.intro C_axioms.intro)
-  (* both X and Y get type 'b since 'b is the internal type of parameter b,
-     not wanted, but put up with for now. *)
 
 print_interps A
 
 (* possible accesses *)
 thm p1.a.asm_A thm LocaleTest.p1.a.asm_A
-thm LocaleTest.asm_A thm p1.asm_A
+thm p1.asm_A thm LocaleTest.p1.asm_A
 
 
 (* without prefix *)

--- a/src/HOL/Algebra/CRing.thy	Sun Apr 17 19:40:43 2005 +0200
+++ b/src/HOL/Algebra/CRing.thy	Mon Apr 18 09:25:23 2005 +0200
@@ -574,28 +574,10 @@
 
 locale ring_hom_cring = cring R + cring S + var h +
   assumes homh [simp, intro]: "h \<in> ring_hom R S"
-(*
   notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
     and hom_mult [simp] = ring_hom_mult [OF homh]
     and hom_add [simp] = ring_hom_add [OF homh]
     and hom_one [simp] = ring_hom_one [OF homh]
-*)
-
-lemma (in ring_hom_cring) hom_closed [simp, intro]:
-  "x \<in> carrier R ==> h x \<in> carrier S"
-  by (simp add: ring_hom_closed [OF homh])
-
-lemma (in ring_hom_cring) hom_mult [simp]:
-  "[| x \<in> carrier R; y \<in> carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
-  by (simp add: ring_hom_mult [OF homh])
-
-lemma (in ring_hom_cring) hom_add [simp]:
-  "[| x \<in> carrier R; y \<in> carrier R |] ==> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
-  by (simp add: ring_hom_add [OF homh])
-
-lemma (in ring_hom_cring) hom_one [simp]:
-  "h \<one> = \<one>\<^bsub>S\<^esub>"
-  by (simp add: ring_hom_one [OF homh])
 
 lemma (in ring_hom_cring) hom_zero [simp]:
   "h \<zero> = \<zero>\<^bsub>S\<^esub>"

--- a/src/HOL/Algebra/Group.thy	Sun Apr 17 19:40:43 2005 +0200
+++ b/src/HOL/Algebra/Group.thy	Mon Apr 18 09:25:23 2005 +0200
@@ -470,8 +470,8 @@
   done
 
 text{*This alternative proof of the previous result demonstrates interpret.
-   It uses @{text Prod.inv_equality} (available after instantiation) instead of
-   @{text "group.inv_equality [OF DirProd_group]"}. *}
+   It uses @{text Prod.inv_equality} (available after @{text interpret})
+   instead of @{text "group.inv_equality [OF DirProd_group]"}. *}
 lemma
   includes group G + group H
   assumes g: "g \<in> carrier G"
@@ -542,19 +542,8 @@
   @{term H}, with a homomorphism @{term h} between them*}
 locale group_hom = group G + group H + var h +
   assumes homh: "h \<in> hom G H"
-(*
   notes hom_mult [simp] = hom_mult [OF homh]
     and hom_closed [simp] = hom_closed [OF homh]
-CB: late binding problem?
-*)
-
-lemma (in group_hom) hom_mult [simp]:
-  "[| x \<in> carrier G; y \<in> carrier G |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
-  by (simp add: hom_mult [OF homh])
-
-lemma (in group_hom) hom_closed [simp]:
-  "x \<in> carrier G ==> h x \<in> carrier H"
-  by (simp add: hom_closed [OF homh])
 
 lemma (in group_hom) one_closed [simp]:
   "h \<one> \<in> carrier H"

--- a/src/HOL/Algebra/UnivPoly.thy	Sun Apr 17 19:40:43 2005 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Mon Apr 18 09:25:23 2005 +0200
@@ -1474,7 +1474,6 @@
     by (simp del: monom_mult (* eval.hom_mult eval.hom_pow, delayed inst! *)
       add: monom_mult [THEN sym] monom_pow)
   also
-  (*  from ring_hom_cring_P_S [OF S] instantiate eval: ring_hom_cring *)
   from R S eval_monom1 have "... = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n"
     by (simp add: eval_const)
   finally show ?thesis .
@@ -1487,9 +1486,6 @@
   assume S: "s \<in> carrier S" and R: "r \<in> carrier R" and P: "p \<in> carrier P"
   from ring_hom_cring_P_S [OF S] interpret ring_hom_cring [P S "eval R S h s"]
     by - (rule ring_hom_cring.axioms, assumption)+
-(*
-  from ring_hom_cring_P_S [OF S] instantiate eval: ring_hom_cring
-*)
   from S R P show ?thesis
     by (simp add: monom_mult_is_smult [THEN sym] eval_const)
 qed
@@ -1571,11 +1567,15 @@
   by (fast intro: UP_univ_propI INTEG_cring id_ring_hom)
 
 text {*
-  An instantiation mechanism would now import all theorems and lemmas
+  Interpretation allows now to import all theorems and lemmas
   valid in the context of homomorphisms between @{term INTEG} and @{term
   "UP INTEG"} globally.
 *}
 
+interpretation INTEG: UP_univ_prop [INTEG INTEG id]
+  using INTEG_id_eval
+  by - (rule UP_univ_prop.axioms, assumption)+
+
 lemma INTEG_closed [intro, simp]:
   "z \<in> carrier INTEG"
   by (unfold INTEG_def) simp
@@ -1589,6 +1589,6 @@
   by (induct n) (simp_all add: INTEG_def nat_pow_def)
 
 lemma "eval INTEG INTEG id 10 (monom (UP INTEG) 5 2) = 500"
-  by (simp add: UP_univ_prop.eval_monom [OF INTEG_id_eval])
+  by (simp add: INTEG.eval_monom)
 
 end

--- a/src/Pure/Isar/locale.ML	Sun Apr 17 19:40:43 2005 +0200
+++ b/src/Pure/Isar/locale.ML	Mon Apr 18 09:25:23 2005 +0200
@@ -351,8 +351,12 @@
   in
     (case loc_regs of
         NONE => Pretty.str ("No interpretations in " ^ msg ^ ".")
-      | SOME r => Pretty.big_list ("Interpretations in " ^ msg ^ ":")
-          (map prt_inst (Termlisttab.dest r)))
+      | SOME r => let
+            val r' = Termlisttab.dest r;
+            val r'' = Library.sort_wrt (fn (_, ((prfx, _), _)) => prfx) r';
+          in Pretty.big_list ("Interpretations in " ^ msg ^ ":")
+            (map prt_inst r'')
+          end)
     |> Pretty.writeln
   end;
 
@@ -540,7 +544,6 @@
 fun tinst_tab_elem sg tinst =
   map_values (tinst_tab_type tinst) (tinst_tab_term tinst) (tinst_tab_thm sg tinst);
 
-
 (* instantiate TFrees and Frees *)
 
 fun inst_tab_term (inst, tinst) = if Symtab.is_empty inst
@@ -589,8 +592,8 @@
                  (map (Thm.assume o cert o inst_tab_term (inst, tinst)) hyps))
         end;
 
-fun inst_tab_elem sg inst =
-  map_values (tinst_tab_type (#2 inst)) (inst_tab_term inst) (inst_tab_thm sg inst);
+fun inst_tab_elem sg (inst as (_, tinst)) =
+  map_values (tinst_tab_type tinst) (inst_tab_term inst) (inst_tab_thm sg inst);
 
 fun inst_tab_elems sign inst ((n, ps), elems) =
       ((n, map (inst_tab_term inst) ps), map (inst_tab_elem sign inst) elems);
@@ -1923,7 +1926,8 @@
         disch (prfx, atts) (thy_ctxt, Notes facts) =
       let
         val reg_atts = map (attrib thy_ctxt) atts;
-        val facts = map_attrib_facts (attrib thy_ctxt) facts;
+        (* discharge hyps in attributes *)
+        val facts = map_attrib_facts (attrib thy_ctxt o Args.map_values I I I disch) facts;
         val facts' = map (apfst (apsnd (fn a => a @ reg_atts))) facts;
         (* discharge hyps *)
         val facts'' = map (apsnd (map (apfst (map disch)))) facts';