interpretation: unfolding of equations;
authorballarin
Mon, 23 Jul 2007 13:50:31 +0200
changeset 23920 4288dc7dc248
parent 23919 af871d13e320
child 23921 947152add153
interpretation: unfolding of equations;
NEWS
doc-src/IsarRef/generic.tex
--- a/NEWS	Mon Jul 23 13:48:30 2007 +0200
+++ b/NEWS	Mon Jul 23 13:50:31 2007 +0200
@@ -364,6 +364,18 @@
 has changed.  This enables to override declarations from fragments due
 to interpretations -- for example, unwanted simp rules.
 
+* Isar/locales: interpretation in theories and proof contexts has been
+extended.  One may now specify (and prove) equations, which are
+unfolded in interpreted theorems.  This is useful for replacing
+defined concepts (constants depending on locale parameters) by
+concepts already existing in the target context.  Example:
+
+  interpretation partial_order ["op <= :: [int, int] => bool"]
+    where "partial_order.less (op <=) (x::int) y = (x < y)"
+
+Typically, the constant `partial_order.less' is created by the
+specification element definition in the context of locale partial_order.
+
 * Provers/induct: improved internal context management to support
 local fixes and defines on-the-fly.  Thus explicit meta-level
 connectives !! and ==> are rarely required anymore in inductive goals
--- a/doc-src/IsarRef/generic.tex	Mon Jul 23 13:48:30 2007 +0200
+++ b/doc-src/IsarRef/generic.tex	Mon Jul 23 13:50:31 2007 +0200
@@ -341,41 +341,48 @@
 \railterm{printinterps}
 
 \begin{rail}
-  'interpretation' (interp | name ('<' | subseteq) contextexp)
+  'interpretation' (interp | name ('<' | subseteq) contextexpr)
   ;
   'interpret' interp
   ;
   printinterps '!'? name
   ;
-  interp: thmdecl? contextexpr ('[' (inst+) ']')?
+  interp: thmdecl? \\ (contextexpr ('[' (inst+) ']')? |
+    name ('[' (inst+) ']')? 'where' (prop + 'and'))
   ;
 \end{rail}
 
 
 \begin{descr}
 
-\item [$\isarcmd{interpretation}~expr~insts$]
+\item [$\isarcmd{interpretation}~expr~insts~\isarkeyword{where}~eqns$]
 
-  The first form of $\isarcmd{interpretation}$ interprets $expr$
-  in the theory.  The instantiation is given as a list of
-  terms $insts$ and 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 first form of $\isarcmd{interpretation}$ interprets $expr$ in
+  the theory.  The instantiation is given as a list of terms $insts$
+  and 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 command generates proof obligations for the instantiated
   specifications (assumes and defines elements).  Once these are
   discharged by the user, instantiated facts are added to the theory in
   a post-processing phase.
 
+  Additional equations, which are unfolded in facts during
+  post-processing, may be given after the keyword
+  $\isarkeyword{where}$.  This is useful for interpreting concepts
+  introduced through definition specification elements.  The equations
+  must be proved.  Note that if equations are present, the context
+  expression is restricted to a locale name.
+
   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
+  active.  The command will only generate proof obligations and process
   facts for new parts.
 
   The context expression may be preceded by a name and/or attributes.
@@ -420,7 +427,7 @@
   prefix and attributes, although only for fragments of $expr$ that
   are not interpreted in the theory already.
 
-\item [$\isarcmd{interpret}~expr~insts$]
+\item [$\isarcmd{interpret}~expr~insts~\isarkeyword{where}~eqns$]
   interprets $expr$ in the proof context and is otherwise similar to
   interpretation in theories.  Free variables in instantiations are not
   generalized, however.