--- a/doc-src/Codegen/Thy/Further.thy Mon Jun 14 12:01:30 2010 +0200
+++ b/doc-src/Codegen/Thy/Further.thy Mon Jun 14 15:27:08 2010 +0200
@@ -12,6 +12,92 @@
contains exhaustive syntax diagrams.
*}
+subsection {* Locales and interpretation *}
+
+lemma funpow_mult: -- FIXME
+ fixes f :: "'a \<Rightarrow> 'a"
+ shows "(f ^^ m) ^^ n = f ^^ (m * n)"
+ by (induct n) (simp_all add: funpow_add)
+
+text {*
+ A technical issue comes to surface when generating code from
+ specifications stemming from locale interpretation.
+
+ Let us assume a locale specifying a power operation
+ on arbitrary types:
+*}
+
+locale %quote power =
+ fixes power :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
+ assumes power_commute: "power x \<circ> power y = power y \<circ> power x"
+begin
+
+text {*
+ \noindent Inside that locale we can lift @{text power} to exponent lists
+ by means of specification relative to that locale:
+*}
+
+primrec %quote powers :: "'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
+ "powers [] = id"
+| "powers (x # xs) = power x \<circ> powers xs"
+
+lemma %quote powers_append:
+ "powers (xs @ ys) = powers xs \<circ> powers ys"
+ by (induct xs) simp_all
+
+lemma %quote powers_power:
+ "powers xs \<circ> power x = power x \<circ> powers xs"
+ by (induct xs)
+ (simp_all del: o_apply id_apply add: o_assoc [symmetric],
+ simp del: o_apply add: o_assoc power_commute)
+
+lemma %quote powers_rev:
+ "powers (rev xs) = powers xs"
+ by (induct xs) (simp_all add: powers_append powers_power)
+
+end %quote
+
+text {*
+ After an interpretation of this locale (say, @{command
+ interpretation} @{text "fun_power:"} @{term [source] "power (\<lambda>n (f ::
+ 'a \<Rightarrow> 'a). f ^^ n)"}), one would expect to have a constant @{text
+ "fun_power.powers :: nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"} for which code
+ can be generated. But this not the case: internally, the term
+ @{text "fun_power.powers"} is an abbreviation for the foundational
+ term @{term [source] "power.powers (\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)"}
+ (see \cite{isabelle-locale} for the details behind).
+
+ Furtunately, with minor effort the desired behaviour can be achieved.
+ First, a dedicated definition of the constant on which the local @{text "powers"}
+ after interpretation is supposed to be mapped on:
+*}
+
+definition %quote funpows :: "nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
+ [code del]: "funpows = power.powers (\<lambda>n f. f ^^ n)"
+
+text {*
+ \noindent In general, the pattern is @{text "c = t"} where @{text c} is
+ the name of the future constant and @{text t} the foundational term
+ corresponding to the local constant after interpretation.
+
+ 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
+ "power.powers (\<lambda>n f. f ^^ n) = funpows"
+ by unfold_locales
+ (simp_all add: expand_fun_eq funpow_mult mult_commute funpows_def)
+
+text {*
+ \noindent This additional equation is trivially proved by the definition
+ itself.
+
+ After this setup procedure, code generation can continue as usual:
+*}
+
+text %quote {*@{code_stmts funpows (consts) Nat.funpow funpows (Haskell)}*}
+
+
subsection {* Modules *}
text {*
--- a/doc-src/Codegen/Thy/document/Further.tex Mon Jun 14 12:01:30 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Further.tex Mon Jun 14 15:27:08 2010 +0200
@@ -33,6 +33,191 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsubsection{Locales and interpretation%
+}
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ funpow{\isacharunderscore}mult{\isacharcolon}\ %
+\isamarkupcmt{FIXME%
+}
+\isanewline
+\ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}f\ {\isacharcircum}{\isacharcircum}\ m{\isacharparenright}\ {\isacharcircum}{\isacharcircum}\ n\ {\isacharequal}\ f\ {\isacharcircum}{\isacharcircum}\ {\isacharparenleft}m\ {\isacharasterisk}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ n{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ funpow{\isacharunderscore}add{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+A technical issue comes to surface when generating code from
+ specifications stemming from locale interpretation.
+
+ Let us assume a locale specifying a power operation
+ on arbitrary types:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{locale}\isamarkupfalse%
+\ power\ {\isacharequal}\isanewline
+\ \ \isakeyword{fixes}\ power\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{assumes}\ power{\isacharunderscore}commute{\isacharcolon}\ {\isachardoublequoteopen}power\ x\ {\isasymcirc}\ power\ y\ {\isacharequal}\ power\ y\ {\isasymcirc}\ power\ x{\isachardoublequoteclose}\isanewline
+\isakeyword{begin}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent Inside that locale we can lift \isa{power} to exponent lists
+ by means of specification relative to that locale:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{primrec}\isamarkupfalse%
+\ powers\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}powers\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ id{\isachardoublequoteclose}\isanewline
+{\isacharbar}\ {\isachardoublequoteopen}powers\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharequal}\ power\ x\ {\isasymcirc}\ powers\ xs{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ powers{\isacharunderscore}append{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}powers\ {\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ powers\ xs\ {\isasymcirc}\ powers\ ys{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ powers{\isacharunderscore}power{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}powers\ xs\ {\isasymcirc}\ power\ x\ {\isacharequal}\ power\ x\ {\isasymcirc}\ powers\ xs{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ xs{\isacharparenright}\isanewline
+\ \ \ \ {\isacharparenleft}simp{\isacharunderscore}all\ del{\isacharcolon}\ o{\isacharunderscore}apply\ id{\isacharunderscore}apply\ add{\isacharcolon}\ o{\isacharunderscore}assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharcomma}\isanewline
+\ \ \ \ \ \ simp\ del{\isacharcolon}\ o{\isacharunderscore}apply\ add{\isacharcolon}\ o{\isacharunderscore}assoc\ power{\isacharunderscore}commute{\isacharparenright}\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ powers{\isacharunderscore}rev{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}powers\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ powers\ xs{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ xs{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ powers{\isacharunderscore}append\ powers{\isacharunderscore}power{\isacharparenright}\isanewline
+\isanewline
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+After an interpretation of this locale (say, \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} \isa{fun{\isacharunderscore}power{\isacharcolon}} \isa{{\isachardoublequote}power\ {\isacharparenleft}{\isasymlambda}n\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isacharparenright}{\isachardoublequote}}), one would expect to have a constant \isa{fun{\isacharunderscore}power{\isachardot}powers\ {\isacharcolon}{\isacharcolon}\ nat\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} for which code
+ can be generated. But this not the case: internally, the term
+ \isa{fun{\isacharunderscore}power{\isachardot}powers} is an abbreviation for the foundational
+ term \isa{{\isachardoublequote}power{\isachardot}powers\ {\isacharparenleft}{\isasymlambda}n\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isacharparenright}{\isachardoublequote}}
+ (see \cite{isabelle-locale} for the details behind).
+
+ Furtunately, with minor effort the desired behaviour can be achieved.
+ First, a dedicated definition of the constant on which the local \isa{powers}
+ after interpretation is supposed to be mapped on:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{definition}\isamarkupfalse%
+\ funpows\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}funpows\ {\isacharequal}\ power{\isachardot}powers\ {\isacharparenleft}{\isasymlambda}n\ f{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isacharparenright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent In general, the pattern is \isa{c\ {\isacharequal}\ t} where \isa{c} is
+ the name of the future constant and \isa{t} the foundational term
+ corresponding to the local constant after interpretation.
+
+ The interpretation itself is enriched with an equation \isa{t\ {\isacharequal}\ c}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{interpretation}\isamarkupfalse%
+\ fun{\isacharunderscore}power{\isacharcolon}\ power\ {\isachardoublequoteopen}{\isasymlambda}n\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}power{\isachardot}powers\ {\isacharparenleft}{\isasymlambda}n\ f{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isacharparenright}\ {\isacharequal}\ funpows{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ unfold{\isacharunderscore}locales\isanewline
+\ \ \ \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ expand{\isacharunderscore}fun{\isacharunderscore}eq\ funpow{\isacharunderscore}mult\ mult{\isacharunderscore}commute\ funpows{\isacharunderscore}def{\isacharparenright}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent This additional equation is trivially proved by the definition
+ itself.
+
+ After this setup procedure, code generation can continue as usual:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isatypewriter%
+\noindent%
+\hspace*{0pt}funpow ::~forall a.~Nat -> (a -> a) -> a -> a;\\
+\hspace*{0pt}funpow (Suc n) f = f .~funpow n f;\\
+\hspace*{0pt}funpow Zero{\char95}nat f = id;\\
+\hspace*{0pt}\\
+\hspace*{0pt}funpows ::~forall a.~[Nat] -> (a -> a) -> a -> a;\\
+\hspace*{0pt}funpows [] = id;\\
+\hspace*{0pt}funpows (x :~xs) = funpow x .~funpows xs;%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
\isamarkupsubsection{Modules%
}
\isamarkuptrue%