1.1 --- a/doc-src/Codegen/Thy/Further.thy Mon Jun 14 12:01:30 2010 +0200
1.2 +++ b/doc-src/Codegen/Thy/Further.thy Mon Jun 14 15:27:08 2010 +0200
1.3 @@ -12,6 +12,92 @@
1.4 contains exhaustive syntax diagrams.
1.5 *}
1.6
1.7 +subsection {* Locales and interpretation *}
1.8 +
1.9 +lemma funpow_mult: -- FIXME
1.10 + fixes f :: "'a \<Rightarrow> 'a"
1.11 + shows "(f ^^ m) ^^ n = f ^^ (m * n)"
1.12 + by (induct n) (simp_all add: funpow_add)
1.13 +
1.14 +text {*
1.15 + A technical issue comes to surface when generating code from
1.16 + specifications stemming from locale interpretation.
1.17 +
1.18 + Let us assume a locale specifying a power operation
1.19 + on arbitrary types:
1.20 +*}
1.21 +
1.22 +locale %quote power =
1.23 + fixes power :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
1.24 + assumes power_commute: "power x \<circ> power y = power y \<circ> power x"
1.25 +begin
1.26 +
1.27 +text {*
1.28 + \noindent Inside that locale we can lift @{text power} to exponent lists
1.29 + by means of specification relative to that locale:
1.30 +*}
1.31 +
1.32 +primrec %quote powers :: "'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
1.33 + "powers [] = id"
1.34 +| "powers (x # xs) = power x \<circ> powers xs"
1.35 +
1.36 +lemma %quote powers_append:
1.37 + "powers (xs @ ys) = powers xs \<circ> powers ys"
1.38 + by (induct xs) simp_all
1.39 +
1.40 +lemma %quote powers_power:
1.41 + "powers xs \<circ> power x = power x \<circ> powers xs"
1.42 + by (induct xs)
1.43 + (simp_all del: o_apply id_apply add: o_assoc [symmetric],
1.44 + simp del: o_apply add: o_assoc power_commute)
1.45 +
1.46 +lemma %quote powers_rev:
1.47 + "powers (rev xs) = powers xs"
1.48 + by (induct xs) (simp_all add: powers_append powers_power)
1.49 +
1.50 +end %quote
1.51 +
1.52 +text {*
1.53 + After an interpretation of this locale (say, @{command
1.54 + interpretation} @{text "fun_power:"} @{term [source] "power (\<lambda>n (f ::
1.55 + 'a \<Rightarrow> 'a). f ^^ n)"}), one would expect to have a constant @{text
1.56 + "fun_power.powers :: nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"} for which code
1.57 + can be generated. But this not the case: internally, the term
1.58 + @{text "fun_power.powers"} is an abbreviation for the foundational
1.59 + term @{term [source] "power.powers (\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)"}
1.60 + (see \cite{isabelle-locale} for the details behind).
1.61 +
1.62 + Furtunately, with minor effort the desired behaviour can be achieved.
1.63 + First, a dedicated definition of the constant on which the local @{text "powers"}
1.64 + after interpretation is supposed to be mapped on:
1.65 +*}
1.66 +
1.67 +definition %quote funpows :: "nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
1.68 + [code del]: "funpows = power.powers (\<lambda>n f. f ^^ n)"
1.69 +
1.70 +text {*
1.71 + \noindent In general, the pattern is @{text "c = t"} where @{text c} is
1.72 + the name of the future constant and @{text t} the foundational term
1.73 + corresponding to the local constant after interpretation.
1.74 +
1.75 + The interpretation itself is enriched with an equation @{text "t = c"}:
1.76 +*}
1.77 +
1.78 +interpretation %quote fun_power: power "\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n" where
1.79 + "power.powers (\<lambda>n f. f ^^ n) = funpows"
1.80 + by unfold_locales
1.81 + (simp_all add: expand_fun_eq funpow_mult mult_commute funpows_def)
1.82 +
1.83 +text {*
1.84 + \noindent This additional equation is trivially proved by the definition
1.85 + itself.
1.86 +
1.87 + After this setup procedure, code generation can continue as usual:
1.88 +*}
1.89 +
1.90 +text %quote {*@{code_stmts funpows (consts) Nat.funpow funpows (Haskell)}*}
1.91 +
1.92 +
1.93 subsection {* Modules *}
1.94
1.95 text {*
2.1 --- a/doc-src/Codegen/Thy/document/Further.tex Mon Jun 14 12:01:30 2010 +0200
2.2 +++ b/doc-src/Codegen/Thy/document/Further.tex Mon Jun 14 15:27:08 2010 +0200
2.3 @@ -33,6 +33,191 @@
2.4 \end{isamarkuptext}%
2.5 \isamarkuptrue%
2.6 %
2.7 +\isamarkupsubsection{Locales and interpretation%
2.8 +}
2.9 +\isamarkuptrue%
2.10 +\isacommand{lemma}\isamarkupfalse%
2.11 +\ funpow{\isacharunderscore}mult{\isacharcolon}\ %
2.12 +\isamarkupcmt{FIXME%
2.13 +}
2.14 +\isanewline
2.15 +\ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline
2.16 +\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}f\ {\isacharcircum}{\isacharcircum}\ m{\isacharparenright}\ {\isacharcircum}{\isacharcircum}\ n\ {\isacharequal}\ f\ {\isacharcircum}{\isacharcircum}\ {\isacharparenleft}m\ {\isacharasterisk}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
2.17 +%
2.18 +\isadelimproof
2.19 +\ \ %
2.20 +\endisadelimproof
2.21 +%
2.22 +\isatagproof
2.23 +\isacommand{by}\isamarkupfalse%
2.24 +\ {\isacharparenleft}induct\ n{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ funpow{\isacharunderscore}add{\isacharparenright}%
2.25 +\endisatagproof
2.26 +{\isafoldproof}%
2.27 +%
2.28 +\isadelimproof
2.29 +%
2.30 +\endisadelimproof
2.31 +%
2.32 +\begin{isamarkuptext}%
2.33 +A technical issue comes to surface when generating code from
2.34 + specifications stemming from locale interpretation.
2.35 +
2.36 + Let us assume a locale specifying a power operation
2.37 + on arbitrary types:%
2.38 +\end{isamarkuptext}%
2.39 +\isamarkuptrue%
2.40 +%
2.41 +\isadelimquote
2.42 +%
2.43 +\endisadelimquote
2.44 +%
2.45 +\isatagquote
2.46 +\isacommand{locale}\isamarkupfalse%
2.47 +\ power\ {\isacharequal}\isanewline
2.48 +\ \ \isakeyword{fixes}\ power\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b{\isachardoublequoteclose}\isanewline
2.49 +\ \ \isakeyword{assumes}\ power{\isacharunderscore}commute{\isacharcolon}\ {\isachardoublequoteopen}power\ x\ {\isasymcirc}\ power\ y\ {\isacharequal}\ power\ y\ {\isasymcirc}\ power\ x{\isachardoublequoteclose}\isanewline
2.50 +\isakeyword{begin}%
2.51 +\endisatagquote
2.52 +{\isafoldquote}%
2.53 +%
2.54 +\isadelimquote
2.55 +%
2.56 +\endisadelimquote
2.57 +%
2.58 +\begin{isamarkuptext}%
2.59 +\noindent Inside that locale we can lift \isa{power} to exponent lists
2.60 + by means of specification relative to that locale:%
2.61 +\end{isamarkuptext}%
2.62 +\isamarkuptrue%
2.63 +%
2.64 +\isadelimquote
2.65 +%
2.66 +\endisadelimquote
2.67 +%
2.68 +\isatagquote
2.69 +\isacommand{primrec}\isamarkupfalse%
2.70 +\ powers\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
2.71 +\ \ {\isachardoublequoteopen}powers\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ id{\isachardoublequoteclose}\isanewline
2.72 +{\isacharbar}\ {\isachardoublequoteopen}powers\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharequal}\ power\ x\ {\isasymcirc}\ powers\ xs{\isachardoublequoteclose}\isanewline
2.73 +\isanewline
2.74 +\isacommand{lemma}\isamarkupfalse%
2.75 +\ powers{\isacharunderscore}append{\isacharcolon}\isanewline
2.76 +\ \ {\isachardoublequoteopen}powers\ {\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ powers\ xs\ {\isasymcirc}\ powers\ ys{\isachardoublequoteclose}\isanewline
2.77 +\ \ \isacommand{by}\isamarkupfalse%
2.78 +\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
2.79 +\isanewline
2.80 +\isacommand{lemma}\isamarkupfalse%
2.81 +\ powers{\isacharunderscore}power{\isacharcolon}\isanewline
2.82 +\ \ {\isachardoublequoteopen}powers\ xs\ {\isasymcirc}\ power\ x\ {\isacharequal}\ power\ x\ {\isasymcirc}\ powers\ xs{\isachardoublequoteclose}\isanewline
2.83 +\ \ \isacommand{by}\isamarkupfalse%
2.84 +\ {\isacharparenleft}induct\ xs{\isacharparenright}\isanewline
2.85 +\ \ \ \ {\isacharparenleft}simp{\isacharunderscore}all\ del{\isacharcolon}\ o{\isacharunderscore}apply\ id{\isacharunderscore}apply\ add{\isacharcolon}\ o{\isacharunderscore}assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharcomma}\isanewline
2.86 +\ \ \ \ \ \ simp\ del{\isacharcolon}\ o{\isacharunderscore}apply\ add{\isacharcolon}\ o{\isacharunderscore}assoc\ power{\isacharunderscore}commute{\isacharparenright}\isanewline
2.87 +\isanewline
2.88 +\isacommand{lemma}\isamarkupfalse%
2.89 +\ powers{\isacharunderscore}rev{\isacharcolon}\isanewline
2.90 +\ \ {\isachardoublequoteopen}powers\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ powers\ xs{\isachardoublequoteclose}\isanewline
2.91 +\ \ \ \ \isacommand{by}\isamarkupfalse%
2.92 +\ {\isacharparenleft}induct\ xs{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ powers{\isacharunderscore}append\ powers{\isacharunderscore}power{\isacharparenright}\isanewline
2.93 +\isanewline
2.94 +\isacommand{end}\isamarkupfalse%
2.95 +%
2.96 +\endisatagquote
2.97 +{\isafoldquote}%
2.98 +%
2.99 +\isadelimquote
2.100 +%
2.101 +\endisadelimquote
2.102 +%
2.103 +\begin{isamarkuptext}%
2.104 +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
2.105 + can be generated. But this not the case: internally, the term
2.106 + \isa{fun{\isacharunderscore}power{\isachardot}powers} is an abbreviation for the foundational
2.107 + 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}}
2.108 + (see \cite{isabelle-locale} for the details behind).
2.109 +
2.110 + Furtunately, with minor effort the desired behaviour can be achieved.
2.111 + First, a dedicated definition of the constant on which the local \isa{powers}
2.112 + after interpretation is supposed to be mapped on:%
2.113 +\end{isamarkuptext}%
2.114 +\isamarkuptrue%
2.115 +%
2.116 +\isadelimquote
2.117 +%
2.118 +\endisadelimquote
2.119 +%
2.120 +\isatagquote
2.121 +\isacommand{definition}\isamarkupfalse%
2.122 +\ funpows\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
2.123 +\ \ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}funpows\ {\isacharequal}\ power{\isachardot}powers\ {\isacharparenleft}{\isasymlambda}n\ f{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isacharparenright}{\isachardoublequoteclose}%
2.124 +\endisatagquote
2.125 +{\isafoldquote}%
2.126 +%
2.127 +\isadelimquote
2.128 +%
2.129 +\endisadelimquote
2.130 +%
2.131 +\begin{isamarkuptext}%
2.132 +\noindent In general, the pattern is \isa{c\ {\isacharequal}\ t} where \isa{c} is
2.133 + the name of the future constant and \isa{t} the foundational term
2.134 + corresponding to the local constant after interpretation.
2.135 +
2.136 + The interpretation itself is enriched with an equation \isa{t\ {\isacharequal}\ c}:%
2.137 +\end{isamarkuptext}%
2.138 +\isamarkuptrue%
2.139 +%
2.140 +\isadelimquote
2.141 +%
2.142 +\endisadelimquote
2.143 +%
2.144 +\isatagquote
2.145 +\isacommand{interpretation}\isamarkupfalse%
2.146 +\ 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
2.147 +\ \ {\isachardoublequoteopen}power{\isachardot}powers\ {\isacharparenleft}{\isasymlambda}n\ f{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isacharparenright}\ {\isacharequal}\ funpows{\isachardoublequoteclose}\isanewline
2.148 +\ \ \isacommand{by}\isamarkupfalse%
2.149 +\ unfold{\isacharunderscore}locales\isanewline
2.150 +\ \ \ \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ expand{\isacharunderscore}fun{\isacharunderscore}eq\ funpow{\isacharunderscore}mult\ mult{\isacharunderscore}commute\ funpows{\isacharunderscore}def{\isacharparenright}%
2.151 +\endisatagquote
2.152 +{\isafoldquote}%
2.153 +%
2.154 +\isadelimquote
2.155 +%
2.156 +\endisadelimquote
2.157 +%
2.158 +\begin{isamarkuptext}%
2.159 +\noindent This additional equation is trivially proved by the definition
2.160 + itself.
2.161 +
2.162 + After this setup procedure, code generation can continue as usual:%
2.163 +\end{isamarkuptext}%
2.164 +\isamarkuptrue%
2.165 +%
2.166 +\isadelimquote
2.167 +%
2.168 +\endisadelimquote
2.169 +%
2.170 +\isatagquote
2.171 +%
2.172 +\begin{isamarkuptext}%
2.173 +\isatypewriter%
2.174 +\noindent%
2.175 +\hspace*{0pt}funpow ::~forall a.~Nat -> (a -> a) -> a -> a;\\
2.176 +\hspace*{0pt}funpow (Suc n) f = f .~funpow n f;\\
2.177 +\hspace*{0pt}funpow Zero{\char95}nat f = id;\\
2.178 +\hspace*{0pt}\\
2.179 +\hspace*{0pt}funpows ::~forall a.~[Nat] -> (a -> a) -> a -> a;\\
2.180 +\hspace*{0pt}funpows [] = id;\\
2.181 +\hspace*{0pt}funpows (x :~xs) = funpow x .~funpows xs;%
2.182 +\end{isamarkuptext}%
2.183 +\isamarkuptrue%
2.184 +%
2.185 +\endisatagquote
2.186 +{\isafoldquote}%
2.187 +%
2.188 +\isadelimquote
2.189 +%
2.190 +\endisadelimquote
2.191 +%
2.192 \isamarkupsubsection{Modules%
2.193 }
2.194 \isamarkuptrue%