--- 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 *}
--- 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>
--- 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}}