# HG changeset patch
# User haftmann
# Date 1415986782 -3600
# Node ID 16d92d37a8a1de2ed130aeac2e3b85f016758189
# Parent  2c8b2fb54b8806a9e05905316cf329f8c4a813a1
documentation stubs about permanent_interpretation

diff -r 2c8b2fb54b88 -r 16d92d37a8a1 src/Doc/Codegen/Further.thy
--- a/src/Doc/Codegen/Further.thy	Fri Nov 14 13:18:33 2014 +0100
+++ b/src/Doc/Codegen/Further.thy	Fri Nov 14 18:39:42 2014 +0100
@@ -1,5 +1,5 @@
 theory Further
-imports Setup
+imports Setup "~~/src/Tools/Permanent_Interpretation"
 begin
 
 section {* Further issues \label{sec:further} *}
@@ -202,7 +202,7 @@
   The interpretation itself is enriched with an equation @{text "t = c"}:
 *}
 
-interpretation %quote fun_power: power "\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n" where
+interpretation %quote fun_power: power "(\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)" where
   "power.powers (\<lambda>n f. f ^^ n) = funpows"
   by unfold_locales
     (simp_all add: fun_eq_iff funpow_mult mult.commute funpows_def)
@@ -216,7 +216,27 @@
 
 text %quotetypewriter {*
   @{code_stmts funpows (consts) Nat.funpow funpows (Haskell)}
-*}
+*} (*<*)
+
+(*>*) text {*
+  Fortunately, an even more succint approach is available using command
+  @{command permanent_interpretation}.  This is available
+  by importing theory @{file "~~/src/Tools/Permanent_Interpretation.thy"}.
+  Then the pattern above collapses to
+*} (*<*)
+
+setup {* Sign.add_path "funpows" *}
+hide_const (open) funpows
+
+(*>*)
+permanent_interpretation %quote fun_power: power "(\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)"
+  defining funpows = "fun_power.powers :: nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
+  by unfold_locales
+    (simp_all add: fun_eq_iff funpow_mult mult.commute) (*<*)
+
+setup {* Sign.parent_path *}
+
+(*>*)
 
 
 subsection {* Parallel computation *}
diff -r 2c8b2fb54b88 -r 16d92d37a8a1 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Fri Nov 14 13:18:33 2014 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Fri Nov 14 18:39:42 2014 +0100
@@ -1,5 +1,5 @@
 theory Spec
-imports Base Main
+imports Base Main "~~/src/Tools/Permanent_Interpretation"
 begin
 
 chapter \<open>Specifications\<close>
@@ -796,6 +796,81 @@
 \<close>
 
 
+subsubsection \<open>Permanent locale interpretation\<close>
+
+text \<open>
+  Permanent locale interpretation is a library extension on top
+  of @{command "interpretation"} and @{command "sublocale"}.  It is
+  available by importing theory @{file "~~/src/Tools/Permanent_Interpretation.thy"}
+  and provides
+  \begin{enumerate}
+    \item a unified view on arbitrary suitable local theories as interpretation target; 
+    \item rewrite morphisms by means of \emph{mixin definitions}. 
+  \end{enumerate}
+  
+  \begin{matharray}{rcl}
+    @{command_def "permanent_interpretation"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
+  \end{matharray}
+
+  @{rail \<open>
+    @@{command permanent_interpretation} @{syntax locale_expr} \<newline>
+      definitions? equations?
+    ;
+
+    definitions: @'defining' (@{syntax thmdecl}? @{syntax name} \<newline>
+      @{syntax mixfix}? @'=' @{syntax term} + @'and');
+    equations: @'where' (@{syntax thmdecl}? @{syntax prop} + @'and')
+  \<close>}
+
+  \begin{description}
+
+  \item @{command "permanent_interpretation"}~@{text "expr \<DEFINING> defs \<WHERE> eqns"}
+  interprets @{text expr} in the current local theory.  The command
+  generates proof obligations for the instantiated specifications.
+  Instantiated declarations (in particular, facts) are added to the
+  local theory's underlying target in a post-processing phase.  When
+  adding declarations to locales, interpreted versions of these
+  declarations are added to any target for all interpretations
+  in that target as well. That is, permanent interpretations
+  dynamically participate in any declarations added to
+  locales.
+  
+  The local theory's underlying target must explicitly support
+  permanent interpretations.  Prominent examples are global theories
+  (where @{command "permanent_interpretation"} is technically
+  corresponding to @{command "interpretation"}) and locales
+  (where @{command "permanent_interpretation"} is technically
+  corresponding to @{command "sublocale"}).  Unnamed contexts
+  \secref{sec:target} are not admissible since they are
+  non-permanent due to their very nature.  
+
+  In additions to \emph{rewrite morphisms} specified by @{text eqns},
+  also \emph{mixin definitions} may be specified.  Semantically, a
+  mixin definition results in a corresponding definition in
+  the local theory's underlying target \emph{and} a mixin equation
+  in the resulting rewrite morphisms which is symmetric to the
+  original definition equation.
+  
+  The technical difference to a conventional definition plus
+  an explicit mixin equation is that
+  
+  \begin{enumerate}
+  
+    \item definitions are parsed in the syntactic interpretation
+      context, just like equations;
+  
+    \item the proof needs not consider the equations stemming from
+      definitions -- they are proved implicitly by construction.
+      
+  \end{enumerate}
+  
+  Mixin definitions yield a pattern for introducing new explicit
+  operations for existing terms after interpretation.
+  
+  \end{description}
+\<close>
+
+
 section \<open>Classes \label{sec:class}\<close>
 
 text \<open>
diff -r 2c8b2fb54b88 -r 16d92d37a8a1 src/Doc/isar.sty
--- a/src/Doc/isar.sty	Fri Nov 14 13:18:33 2014 +0100
+++ b/src/Doc/isar.sty	Fri Nov 14 18:39:42 2014 +0100
@@ -15,6 +15,7 @@
 \newcommand{\isasymAND}{\isakeyword{and}}
 \newcommand{\isasymIS}{\isakeyword{is}}
 \newcommand{\isasymWHERE}{\isakeyword{where}}
+\newcommand{\isasymDEFINING}{\isakeyword{defining}}
 \newcommand{\isasymBEGIN}{\isakeyword{begin}}
 \newcommand{\isasymIMPORTS}{\isakeyword{imports}}
 \newcommand{\isasymIN}{\isakeyword{in}}