author  ballarin 
Thu, 15 Oct 2009 22:22:08 +0200  
changeset 32982  40810d98f4c9 
parent 32981  0114e04a0d64 
child 32983  a6914429005b 
permissions  rwrr 
27063  1 
theory Examples3 
32981  2 
imports Examples "~~/src/HOL/Number_Theory/UniqueFactorization" 
27063  3 
begin 
32981  4 
hide %invisible const Lattices.lattice 
5 
(* imported again through Number_Theory *) 

6 
text {* \vspace{5ex} *} 

7 
subsection {* Third Version: Local Interpretation 

8 
\label{sec:localinterpretation} *} 

27063  9 

32981  10 
text {* In the above example, the fact that @{term "op \<le>"} is a partial 
32982  11 
order for the integers was used in the second goal to 
32981  12 
discharge the premise in the definition of @{text "op \<sqsubset>"}. In 
13 
general, proofs of the equations not only may involve definitions 

14 
fromthe interpreted locale but arbitrarily complex arguments in the 

15 
context of the locale. Therefore is would be convenient to have the 

16 
interpreted locale conclusions temporary available in the proof. 

17 
This can be achieved by a locale interpretation in the proof body. 

18 
The command for local interpretations is \isakeyword{interpret}. We 

19 
repeat the example from the previous section to illustrate this. *} 

27063  20 

32982  21 
interpretation %visible int: partial_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool" 
22 
where "partial_order.less op \<le> (x::int) y = (x < y)" 

32981  23 
proof  
32982  24 
show "partial_order (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)" 
32981  25 
by unfold_locales auto 
32982  26 
then interpret int: partial_order "op \<le> :: [int, int] \<Rightarrow> bool" . 
27 
show "partial_order.less op \<le> (x::int) y = (x < y)" 

28 
unfolding int.less_def by auto 

32981  29 
qed 
27063  30 

32981  31 
text {* The inner interpretation is immediate from the preceding fact 
32 
and proved by assumption (Isar short hand ``.''). It enriches the 

33 
local proof context by the theorems 

30826  34 
also obtained in the interpretation from Section~\ref{sec:pofirst}, 
32982  35 
and @{text int.less_def} may directly be used to unfold the 
30826  36 
definition. Theorems from the local interpretation disappear after 
32981  37 
leaving the proof context  that is, after the closing a 
38 
\isakeyword{next} or \isakeyword{qed} statement. *} 

27063  39 

40 

41 
subsection {* Further Interpretations *} 

42 

32981  43 
text {* Further interpretations are necessary for 
27063  44 
the other locales. In @{text lattice} the operations @{text \<sqinter>} and 
32982  45 
@{text \<squnion>} are substituted by @{term "min :: int \<Rightarrow> int \<Rightarrow> int"} and 
46 
@{term "max :: int \<Rightarrow> int \<Rightarrow> int"}. The entire proof for the 

32981  47 
interpretation is reproduced to give an example of a more 
27063  48 
elaborate interpretation proof. *} 
49 

32982  50 
interpretation %visible int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool" 
51 
where "lattice.meet op \<le> (x::int) y = min x y" 

52 
and "lattice.join op \<le> (x::int) y = max x y" 

32981  53 
proof  
32982  54 
show "lattice (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)" 
32981  55 
txt {* \normalsize We have already shown that this is a partial 
56 
order, *} 

57 
apply unfold_locales 

58 
txt {* \normalsize hence only the lattice axioms remain to be 

59 
shown: @{subgoals [display]} After unfolding @{text is_inf} and 

60 
@{text is_sup}, *} 

32982  61 
apply (unfold int.is_inf_def int.is_sup_def) 
32981  62 
txt {* \normalsize the goals become @{subgoals [display]} 
63 
This can be solved by Presburger arithmetic, which is contained 

64 
in @{text arith}. *} 

65 
by arith+ 

66 
txt {* \normalsize In order to show the equations, we put ourselves 

67 
in a situation where the lattice theorems can be used in a 

68 
convenient way. *} 

32982  69 
then interpret int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool" . 
70 
show "lattice.meet op \<le> (x::int) y = min x y" 

71 
by (bestsimp simp: int.meet_def int.is_inf_def) 

72 
show "lattice.join op \<le> (x::int) y = max x y" 

73 
by (bestsimp simp: int.join_def int.is_sup_def) 

32981  74 
qed 
27063  75 

32981  76 
text {* Next follows that @{text "op \<le>"} is a total order, again for 
32982  77 
the integers. *} 
27063  78 

32982  79 
interpretation %visible int: total_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool" 
32981  80 
by unfold_locales arith 
27063  81 

82 
text {* Theorems that are available in the theory at this point are shown in 

32982  83 
Table~\ref{tab:intlattice}. Two points are worth noting: 
27063  84 

85 
\begin{table} 

86 
\hrule 

87 
\vspace{2ex} 

88 
\begin{center} 

89 
\begin{tabular}{l} 

32982  90 
@{thm [source] int.less_def} from locale @{text partial_order}: \\ 
91 
\quad @{thm int.less_def} \\ 

92 
@{thm [source] int.meet_left} from locale @{text lattice}: \\ 

93 
\quad @{thm int.meet_left} \\ 

94 
@{thm [source] int.join_distr} from locale @{text distrib_lattice}: \\ 

95 
\quad @{thm int.join_distr} \\ 

96 
@{thm [source] int.less_total} from locale @{text total_order}: \\ 

97 
\quad @{thm int.less_total} 

27063  98 
\end{tabular} 
99 
\end{center} 

100 
\hrule 

32982  101 
\caption{Interpreted theorems for @{text \<le>} on the integers.} 
102 
\label{tab:intlattice} 

27063  103 
\end{table} 
32804
ca430e6aee1c
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents:
31960
diff
changeset

104 

ca430e6aee1c
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents:
31960
diff
changeset

105 
\begin{itemize} 
ca430e6aee1c
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents:
31960
diff
changeset

106 
\item 
32981  107 
Locale @{text distrib_lattice} was also interpreted. Since the 
108 
locale hierarcy reflects that total orders are distributive 

109 
lattices, the interpretation of the latter was inserted 

110 
automatically with the interpretation of the former. In general, 

111 
interpretation of a locale will also interpret all locales further 

112 
up in the hierarchy, regardless whether imported or proved via the 

113 
\isakeyword{sublocale} command. 

32804
ca430e6aee1c
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents:
31960
diff
changeset

114 
\item 
32982  115 
Theorem @{thm [source] int.less_total} makes use of @{term "op <"} 
32981  116 
although an equation for the replacement of @{text "op \<sqsubset>"} was only 
117 
given in the interpretation of @{text partial_order}. These 

118 
equations are pushed downwards the hierarchy for related 

119 
interpretations  that is, for interpretations that share the 

120 
instance for parameters they have in common. 

32804
ca430e6aee1c
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents:
31960
diff
changeset

121 
\end{itemize} 
32981  122 
In the next section, the divisibility relation on the natural 
123 
numbers will be explored. 

27063  124 
*} 
125 

126 

32981  127 
subsection {* Interpretations for Divisibility *} 
128 

129 
text {* In this section, further examples of interpretations are 

130 
presented. Impatient readers may skip this section at first 

131 
reading. 

132 

133 
Divisibility on the natural numbers is a distributive lattice 

134 
but not a total order. Interpretation again proceeds 

135 
incrementally. In order to distinguish divisibility from the order 

136 
relation $\le$, we use the qualifier @{text nat_dvd} for 

137 
divisibility. *} 

27063  138 

32981  139 
interpretation nat_dvd: partial_order "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" 
140 
where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)" 

141 
proof  

142 
show "partial_order (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)" 

143 
by unfold_locales (auto simp: dvd_def) 

144 
then interpret nat_dvd: partial_order "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" . 

145 
show "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)" 

146 
apply (unfold nat_dvd.less_def) 

147 
apply auto 

148 
done 

149 
qed 

150 

151 
text {* Note that in Isabelle/HOL there is no operator for strict 

152 
divisibility. Instead, we substitute @{term "x dvd y \<and> x \<noteq> y"}. *} 

27063  153 

32981  154 
interpretation nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" 
155 
where nat_dvd_meet_eq: 

156 
"lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd" 

157 
and nat_dvd_join_eq: 

158 
"lattice.join (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = lcm" 

159 
proof  

160 
show "lattice (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)" 

161 
apply unfold_locales 

162 
apply (unfold nat_dvd.is_inf_def nat_dvd.is_sup_def) 

163 
apply (rule_tac x = "gcd x y" in exI) 

164 
apply auto [1] 

165 
apply (rule_tac x = "lcm x y" in exI) 

166 
apply (auto intro: lcm_least_nat) 

167 
done 

168 
then interpret nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" . 

169 
show "lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd" 

170 
apply (auto simp add: expand_fun_eq) 

171 
apply (unfold nat_dvd.meet_def) 

172 
apply (rule the_equality) 

173 
apply (unfold nat_dvd.is_inf_def) 

174 
by auto 

175 
show "lattice.join (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = lcm" 

176 
apply (auto simp add: expand_fun_eq) 

177 
apply (unfold nat_dvd.join_def) 

178 
apply (rule the_equality) 

179 
apply (unfold nat_dvd.is_sup_def) 

180 
apply (auto intro: lcm_least_nat iff: lcm_unique_nat) 

181 
done 

182 
qed 

27063  183 

32981  184 
text {* The replacement equations @{thm [source] nat_dvd_meet_eq} and 
185 
@{thm [source] nat_dvd_join_eq} are theorems of current theories. 

186 
They are named so that they can be used in the main part of the 

187 
subsequent interpretation. *} 

27063  188 

32981  189 
interpretation %visible nat_dvd: 
190 
distrib_lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" 

27063  191 
apply unfold_locales 
32981  192 
txt {* \normalsize @{subgoals [display]} 
193 
Distributivity of lattice meet and join needs to be shown. This is 

194 
distributivity of gcd and lcm, as becomes apparent when unfolding 

195 
the replacement equations from the previous interpretation: *} 

196 
unfolding nat_dvd_meet_eq nat_dvd_join_eq 

197 
txt {* \normalsize @{subgoals [display]} 

198 
This is a result of number theory: *} 

199 
by (rule UniqueFactorization.gcd_lcm_distrib_nat) 

27063  200 

201 
text {* Theorems that are available in the theory after these 

202 
interpretations are shown in Table~\ref{tab:natdvdlattice}. 

203 

204 
\begin{table} 

205 
\hrule 

206 
\vspace{2ex} 

207 
\begin{center} 

208 
\begin{tabular}{l} 

209 
@{thm [source] nat_dvd.less_def} from locale @{text partial_order}: \\ 

210 
\quad @{thm nat_dvd.less_def} \\ 

211 
@{thm [source] nat_dvd.meet_left} from locale @{text lattice}: \\ 

212 
\quad @{thm nat_dvd.meet_left} \\ 

213 
@{thm [source] nat_dvd.join_distr} from locale @{text distrib_lattice}: \\ 

214 
\quad @{thm nat_dvd.join_distr} \\ 

215 
\end{tabular} 

216 
\end{center} 

217 
\hrule 

218 
\caption{Interpreted theorems for @{text dvd} on the natural numbers.} 

219 
\label{tab:natdvdlattice} 

220 
\end{table} 

221 
*} 

222 

32981  223 

224 
subsection {* Inspecting Interpretations of a Locale *} 

225 

226 
text {* The interpretations for a locale $n$ within the current 

227 
theory may be inspected with \isakeyword{print\_interps}~$n$. This 

228 
prints the list of instances of $n$, for which interpretations exist. 

229 
For example, \isakeyword{print\_interps} @{term partial_order} 

230 
outputs the following: 

231 
\begin{alltt} 

32982  232 
int! : partial_order "op \(\le\)" 
32981  233 
nat_dvd! : partial_order "op dvd" 
234 
\end{alltt} 

235 
The interpretation qualifiers on the left are decorated with an 

236 
exclamation point, which means that they are mandatory. Qualifiers 

237 
can either be \emph{mandatory} or \emph{optional}, designated by 

238 
``!'' or ``?'' respectively. Mandatory qualifiers must occur in a 

239 
name reference while optional ones need not. Mandatory qualifiers 

240 
prevent accidental hiding of names, while optional qualifers can be 

241 
more convenient to use. For \isakeyword{interpretation}, the 

242 
default for qualifiers without an explicit designator is ``!''. 

243 
*} 

27063  244 

245 

27077  246 
section {* Locale Expressions \label{sec:expressions} *} 
27063  247 

248 
text {* 

249 
A map @{term \<phi>} between partial orders @{text \<sqsubseteq>} and @{text \<preceq>} 

250 
is called order preserving if @{text "x \<sqsubseteq> y"} implies @{text "\<phi> x \<preceq> 

251 
\<phi> y"}. This situation is more complex than those encountered so 

252 
far: it involves two partial orders, and it is desirable to use the 

253 
existing locale for both. 

254 

32981  255 
A locale for order preserving maps requires three parameters: @{text 
256 
le} (\isakeyword{infixl}~@{text \<sqsubseteq>}), @{text le'} 

257 
(\isakeyword{infixl}~@{text \<preceq>}) for the orders and @{text \<phi>} for the 

258 
map. 

259 

260 
In order to reuse the existing locale for partial orders, which has 

261 
the single parameter @{text le}, it must be imported twice, once 

262 
mapping its parameter to @{text le} (\isakeyword{infixl}~@{text \<sqsubseteq>}) 

263 
from the new locale and once to @{text le'} 

264 
(\isakeyword{infixl}~@{text \<preceq>}). This can be achieved with a locale 

265 
expression. 

266 

267 
A \emph{locale expression} is a sequence of \emph{locale instances} 

268 
separated by ``$\textbf{+}$'' and followed by a \isakeyword{for} 

269 
clause. 

270 
An instance has the following format: 

271 
\begin{quote} 

272 
\textit{qualifier} \textbf{:} \textit{localename} 

273 
\textit{parameterinstantiation} 

274 
\end{quote} 

275 
We have already seen locale instances as arguments to 

276 
\isakeyword{interpretation} in Section~\ref{sec:interpretation}. 

277 
The qualifier serves to disambiguate the names from different 

278 
instances of the same locale. 

30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

279 

32981  280 
Since the parameters @{text le} and @{text le'} are to be partial 
281 
orders, our locale for order preserving maps will import the these 

282 
instances: 

283 
\begin{alltt} 

284 
le: partial_order le 

285 
le': partial_order le' 

286 
\end{alltt} 

287 
For matter of convenience we choose the parameter names also as 

288 
qualifiers. This is an arbitrary decision. Technically, qualifiers 

289 
and parameters are unrelated. 

290 

291 
Having determined the instances, let us turn to the \isakeyword{for} 

292 
clause. It serves to declare locale parameters in the same way as 

293 
the context element \isakeyword{fixes} does. Context elements can 

294 
only occur after the import section, and therefore the parameters 

295 
referred to inthe instances must be declared in the \isakeyword{for} 

296 
clause.% 

297 
\footnote{Since all parameters can be declared in the \isakeyword{for} 

298 
clause, the context element \isakeyword{fixes} is not needed in 

299 
locales. It is provided for compatibility with the long goals 

300 
format, where the context element also occurs.} 

301 
The \isakeyword{for} clause is also where the syntax of these 

302 
parameters is declared. 

303 

304 
Two context elements for the map parameter @{text \<phi>} and the 

305 
assumptions that it is order perserving complete the locale 

306 
declaration. *} 

27063  307 

308 
locale order_preserving = 

30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

309 
le: partial_order le + le': partial_order le' 
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

310 
for le (infixl "\<sqsubseteq>" 50) and le' (infixl "\<preceq>" 50) + 
32981  311 
fixes \<phi> 
27063  312 
assumes hom_le: "x \<sqsubseteq> y \<Longrightarrow> \<phi> x \<preceq> \<phi> y" 
313 

32981  314 
text (in order_preserving) {* Here are examples of theorems that are 
315 
available in the locale: 

27063  316 

32981  317 
@{thm [source] hom_le}: @{thm hom_le} 
27063  318 

319 
@{thm [source] le.less_le_trans}: @{thm le.less_le_trans} 

320 

32981  321 
@{thm [source] le'.less_le_trans}: 
322 
@{thm [display, indent=2] le'.less_le_trans} 

27063  323 

32981  324 
While there is infix syntax for the strict operation associated to 
325 
@{term "op \<sqsubseteq>"}, there is none for the strict version of @{term 

326 
"op \<preceq>"}. The abbreviation @{text less} with its infix syntax is only 

327 
available for the original instance it was declared for. We may 

328 
introduce the abbreviation @{text less'} with infix syntax @{text \<prec>} 

329 
with this declaration: *} 

27063  330 

331 
abbreviation (in order_preserving) 

332 
less' (infixl "\<prec>" 50) where "less' \<equiv> partial_order.less le'" 

333 

30393
aa6f42252bf6
replaced old locale option by proper "text (in locale)";
wenzelm
parents:
29568
diff
changeset

334 
text (in order_preserving) {* Now the theorem is displayed nicely as 
30826  335 
@{thm [source] le'.less_le_trans}: 
336 
@{thm [display, indent=2] le'.less_le_trans} *} 

27063  337 

32981  338 

339 
subsection {* Default Instantiations and Implicit Parameters *} 

340 

341 
text {* It is possible to omit parameter instantiations in a locale 

342 
expression. In that case, the instantiation defaults to the name of 

343 
the parameter itself. That is, the locale expression @{text 

344 
partial_order} is short for @{text "partial_order le"}, since the 

345 
locale's single parameter is @{text le}. We took advantage of this 

346 
short hand in the \isakeyword{sublocale} declarations of 

347 
Section~\ref{sec:changingthehierarchy}. *} 

348 

349 

350 
text {* In a locale expression that occurs within a locale 

351 
declaration, omitted parameters additionally extend the (possibly 

352 
empty) \isakeyword{for} clause. 

27063  353 

32981  354 
The \isakeyword{for} clause is a 
355 
general construct of Isabelle/Isar to mark names from the preceding 

356 
declaration as ``arbitrary but fixed''. This is necessary for 

357 
example, if the name is already bound in a surrounding context. In 

358 
a locale expression, names occurring in parameter instantiations 

359 
should be bound by a \isakeyword{for} clause whenever these names 

360 
are not introduced elsewhere in the context  for example, on the 

361 
left hand side of a \isakeyword{sublocale} declaration. 

27063  362 

32981  363 
There is an exception to this rule in locale declarations, where the 
364 
\isakeyword{for} clause servers to declare locale parameters. Here, 

365 
locale parameters for which no parameter instantiation is given are 

366 
implicitly added, with their mixfix syntax, at the beginning of the 

367 
\isakeyword{for} clause. For example, in a locale declaration, the 

368 
expression @{text partial_order} is short for 

369 
\begin{alltt} 

370 
partial_order le \isakeyword{for} le (\isakeyword{infixl} "\(\sqsubseteq\)" 50)\textrm{.} 

371 
\end{alltt} 

372 
This short hand was used in the locale declarations of 

373 
Section~\ref{sec:import}. 

374 
*} 

375 

376 
text{* 

377 
The following locale declarations provide more examples. A map 

378 
@{text \<phi>} is a lattice homomorphism if it preserves meet and 

379 
join. *} 

30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

380 

3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

381 
locale lattice_hom = 
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

382 
le: lattice + le': lattice le' for le' (infixl "\<preceq>" 50) + 
27063  383 
fixes \<phi> 
30826  384 
assumes hom_meet: "\<phi> (x \<sqinter> y) = le'.meet (\<phi> x) (\<phi> y)" 
385 
and hom_join: "\<phi> (x \<squnion> y) = le'.join (\<phi> x) (\<phi> y)" 

27063  386 

32981  387 
text {* We omit the parameter instantiation in the first instance of 
388 
@{term lattice}. This causes the parameter @{text le} to be added 

389 
to the \isakeyword{for} clause, and the locale has parameters 

390 
@{text le} and @{text le'}. 

27063  391 

32981  392 
Before turning to the second example, we complete the locale by 
393 
provinding infix syntax for the meet and join operations of the 

394 
second lattice. 

395 
*} 

396 

397 
context lattice_hom begin 

398 
abbreviation meet' (infixl "\<sqinter>''" 50) where "meet' \<equiv> le'.meet" 

399 
abbreviation join' (infixl "\<squnion>''" 50) where "join' \<equiv> le'.join" 

400 
end 

401 

402 
text {* The next example pushes the short hand facilities. A 

403 
homomorphism is an endomorphism if both orders coincide. *} 

27063  404 

30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

405 
locale lattice_end = lattice_hom _ le 
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

406 

32981  407 
text {* The notation @{text _} enables to omit a parameter in a 
408 
positional instantiation. The omitted parameter, @{text le} becomes 

409 
the parameter of the declared locale and is, in the following 

410 
position used to instantiate the second parameter of @{text 

411 
lattice_hom}. The effect is that of identifying the first in second 

412 
parameter of the homomorphism locale. *} 

27063  413 

414 
text {* The inheritance diagram of the situation we have now is shown 

415 
in Figure~\ref{fig:hom}, where the dashed line depicts an 

416 
interpretation which is introduced below. Renamings are 

32981  417 
indicated by $\sqsubseteq \mapsto \preceq$ etc. By looking at the 
418 
inheritance diagram it would seem 

27063  419 
that two identical copies of each of the locales @{text 
32981  420 
partial_order} and @{text lattice} are imported by @{text 
421 
lattice_end}. This is not the case! Inheritance paths with 

422 
identical morphisms are automatically detected and 

27503  423 
the conclusions of the respective locales appear only once. 
27063  424 

425 
\begin{figure} 

426 
\hrule \vspace{2ex} 

427 
\begin{center} 

428 
\begin{tikzpicture} 

429 
\node (o) at (0,0) {@{text partial_order}}; 

430 
\node (oh) at (1.5,2) {@{text order_preserving}}; 

431 
\node (oh1) at (1.5,0.7) {$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$}; 

432 
\node (oh2) at (0,1.3) {$\scriptscriptstyle \sqsubseteq \mapsto \preceq$}; 

433 
\node (l) at (1.5,2) {@{text lattice}}; 

434 
\node (lh) at (0,4) {@{text lattice_hom}}; 

435 
\node (lh1) at (0,2.7) {$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$}; 

436 
\node (lh2) at (1.5,3.3) {$\scriptscriptstyle \sqsubseteq \mapsto \preceq$}; 

437 
\node (le) at (0,6) {@{text lattice_end}}; 

438 
\node (le1) at (0,4.8) 

439 
[anchor=west]{$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$}; 

440 
\node (le2) at (0,5.2) 

441 
[anchor=west]{$\scriptscriptstyle \preceq \mapsto \sqsubseteq$}; 

442 
\draw (o)  (l); 

443 
\draw[dashed] (oh)  (lh); 

444 
\draw (lh)  (le); 

445 
\draw (o) .. controls (oh1.south west) .. (oh); 

446 
\draw (o) .. controls (oh2.north east) .. (oh); 

447 
\draw (l) .. controls (lh1.south west) .. (lh); 

448 
\draw (l) .. controls (lh2.north east) .. (lh); 

449 
\end{tikzpicture} 

450 
\end{center} 

451 
\hrule 

452 
\caption{Hierarchy of Homomorphism Locales.} 

453 
\label{fig:hom} 

454 
\end{figure} 

455 
*} 

456 

457 
text {* It can be shown easily that a lattice homomorphism is order 

458 
preserving. As the final example of this section, a locale 

30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

459 
interpretation is used to assert this: *} 
27063  460 

29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

461 
sublocale lattice_hom \<subseteq> order_preserving proof unfold_locales 
27063  462 
fix x y 
463 
assume "x \<sqsubseteq> y" 

464 
then have "y = (x \<squnion> y)" by (simp add: le.join_connection) 

465 
then have "\<phi> y = (\<phi> x \<squnion>' \<phi> y)" by (simp add: hom_join [symmetric]) 

466 
then show "\<phi> x \<preceq> \<phi> y" by (simp add: le'.join_connection) 

467 
qed 

468 

30393
aa6f42252bf6
replaced old locale option by proper "text (in locale)";
wenzelm
parents:
29568
diff
changeset

469 
text (in lattice_hom) {* 
aa6f42252bf6
replaced old locale option by proper "text (in locale)";
wenzelm
parents:
29568
diff
changeset

470 
Theorems and other declarations  syntax, in particular  from 
aa6f42252bf6
replaced old locale option by proper "text (in locale)";
wenzelm
parents:
29568
diff
changeset

471 
the locale @{text order_preserving} are now active in @{text 
27063  472 
lattice_hom}, for example 
30826  473 
@{thm [source] hom_le}: 
474 
@{thm [display, indent=2] hom_le} 

27063  475 
*} 
476 

32981  477 
(* 
478 
section {* Conditional Interpretation *} 

27063  479 

32981  480 
locale non_negative = 
481 
fixes n :: int 

482 
assumes non_negative: "0 \<le> n" 

483 

484 
interpretation partial_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool" 

485 
where "partial_order.less op \<le> (x::int) y = (x < y)" 

486 
sorry 

487 

488 
sublocale non_negative \<subseteq> order_preserving "op \<le>" "op \<le>" "\<lambda>i. n * i" 

489 
apply unfold_locales using non_negative apply  by (rule mult_left_mono) 

490 

491 
interpretation lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool" 

492 
where min_eq: "lattice.meet op \<le> (x::int) y = min x y" 

493 
and max_eq: "lattice.join op \<le> (x::int) y = max x y" 

494 
sorry 

495 

496 
apply unfold_locales unfolding is_inf_def is_sup_def by arith+ 

497 

498 

499 
sublocale non_negative \<subseteq> lattice_end "op \<le>" "\<lambda>i. n * i" 

500 
apply unfold_locales unfolding min_eq max_eq apply (case_tac "x \<le> y") 

501 
unfolding min_def apply auto apply arith 

502 
apply (rule sym) 

503 
apply (rule the_equality) 

504 
proof 

505 

506 
locale fspace_po = partial_order 

507 
sublocale fspace_po \<subseteq> fspace: partial_order "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x" 

508 
(* fspace needed to disambiguate less etc *) 

509 
apply unfold_locales 

510 
apply auto 

511 
apply (rule) apply auto apply (blast intro: trans) done 

512 

513 
*) 

27063  514 

515 
section {* Further Reading *} 

516 

517 
text {* More information on locales and their interpretation is 

518 
available. For the locale hierarchy of import and interpretation 

519 
dependencies see \cite{Ballarin2006a}; interpretations in theories 

32981  520 
and proofs are covered in \cite{Ballarin2006b}. In the latter, I 
27063  521 
show how interpretation in proofs enables to reason about families 
522 
of algebraic structures, which cannot be expressed with locales 

523 
directly. 

524 

525 
Haftmann and Wenzel \cite{HaftmannWenzel2007} overcome a restriction 

526 
of axiomatic type classes through a combination with locale 

527 
interpretation. The result is a Haskellstyle class system with a 

30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

528 
facility to generate ML and Haskell code. Classes are sufficient for 
27063  529 
simple specifications with a single type parameter. The locales for 
530 
orders and lattices presented in this tutorial fall into this 

531 
category. Order preserving maps, homomorphisms and vector spaces, 

532 
on the other hand, do not. 

533 

32981  534 
The locales reimplementation for Isabelle 2009 provides, among other 
535 
improvements, a clean intergration with Isabelle/Isar's local theory 

536 
mechnisms, which are described in \cite{HaftmannWenzel2009}. 

537 

27063  538 
The original work of Kamm\"uller on locales \cite{KammullerEtAl1999} 
539 
may be of interest from a historical perspective. The mathematical 

540 
background on orders and lattices is taken from Jacobson's textbook 

541 
on algebra \cite[Chapter~8]{Jacobson1985}. 

32981  542 

543 
The sources of this tutorial, which include all proofs, are 

544 
available with the Isabelle distribution at 

545 
\url{http://isabelle.in.tum.de}. 

27063  546 
*} 
547 

548 
text {* 

549 
\begin{table} 

550 
\hrule 

551 
\vspace{2ex} 

552 
\begin{center} 

553 
\begin{tabular}{l>$c<$l} 

554 
\multicolumn{3}{l}{Miscellaneous} \\ 

555 

556 
\textit{attrname} & ::= 

557 
& \textit{name} $$ \textit{attribute} $$ 

29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

558 
\textit{name} \textit{attribute} \\ 
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

559 
\textit{qualifier} & ::= 
30751  560 
& \textit{name} [``\textbf{?}'' $$ ``\textbf{!}''] \\[2ex] 
27063  561 

562 
\multicolumn{3}{l}{Context Elements} \\ 

563 

564 
\textit{fixes} & ::= 

565 
& \textit{name} [ ``\textbf{::}'' \textit{type} ] 

566 
[ ``\textbf{(}'' \textbf{structure} ``\textbf{)}'' $$ 

567 
\textit{mixfix} ] \\ 

568 
\begin{comment} 

569 
\textit{constrains} & ::= 

570 
& \textit{name} ``\textbf{::}'' \textit{type} \\ 

571 
\end{comment} 

572 
\textit{assumes} & ::= 

573 
& [ \textit{attrname} ``\textbf{:}'' ] \textit{proposition} \\ 

574 
\begin{comment} 

575 
\textit{defines} & ::= 

576 
& [ \textit{attrname} ``\textbf{:}'' ] \textit{proposition} \\ 

577 
\textit{notes} & ::= 

578 
& [ \textit{attrname} ``\textbf{=}'' ] 

579 
( \textit{qualifiedname} [ \textit{attribute} ] )$^+$ \\ 

580 
\end{comment} 

581 

582 
\textit{element} & ::= 

583 
& \textbf{fixes} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ \\ 

584 
\begin{comment} 

585 
&  

586 
& \textbf{constrains} \textit{constrains} 

587 
( \textbf{and} \textit{constrains} )$^*$ \\ 

588 
\end{comment} 

589 
&  

590 
& \textbf{assumes} \textit{assumes} ( \textbf{and} \textit{assumes} )$^*$ \\[2ex] 

591 
%\begin{comment} 

592 
% &  

593 
% & \textbf{defines} \textit{defines} ( \textbf{and} \textit{defines} )$^*$ \\ 

594 
% &  

595 
% & \textbf{notes} \textit{notes} ( \textbf{and} \textit{notes} )$^*$ \\ 

596 
%\end{comment} 

597 

598 
\multicolumn{3}{l}{Locale Expressions} \\ 

599 

29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

600 
\textit{posinsts} & ::= 
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

601 
& ( \textit{term} $$ ``\textbf{\_}'' )$^*$ \\ 
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

602 
\textit{namedinsts} & ::= 
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

603 
& \textbf{where} \textit{name} ``\textbf{=}'' \textit{term} 
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

604 
( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\ 
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

605 
\textit{instance} & ::= 
30751  606 
& [ \textit{qualifier} ``\textbf{:}'' ] 
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

607 
\textit{qualifiedname} ( \textit{posinsts} $$ \textit{namedinst} ) \\ 
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

608 
\textit{expression} & ::= 
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

609 
& \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$ 
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

610 
[ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex] 
27063  611 

612 
\multicolumn{3}{l}{Declaration of Locales} \\ 

613 

614 
\textit{locale} & ::= 

615 
& \textit{element}$^+$ \\ 

29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

616 
&  & \textit{expression} [ ``\textbf{+}'' \textit{element}$^+$ ] \\ 
27063  617 
\textit{toplevel} & ::= 
618 
& \textbf{locale} \textit{name} [ ``\textbf{=}'' 

619 
\textit{locale} ] \\[2ex] 

620 

621 
\multicolumn{3}{l}{Interpretation} \\ 

622 

623 
\textit{equation} & ::= & [ \textit{attrname} ``\textbf{:}'' ] 

624 
\textit{prop} \\ 

29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

625 
\textit{equations} & ::= & \textbf{where} \textit{equation} ( \textbf{and} 
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

626 
\textit{equation} )$^*$ \\ 
27063  627 
\textit{toplevel} & ::= 
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

628 
& \textbf{sublocale} \textit{name} ( ``$<$'' $$ 
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

629 
``$\subseteq$'' ) \textit{expression} \textit{proof} \\ 
27063  630 
&  
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

631 
& \textbf{interpretation} 
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

632 
\textit{expression} [ \textit{equations} ] \textit{proof} \\ 
27063  633 
&  
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

634 
& \textbf{interpret} 
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

635 
\textit{expression} \textit{proof} \\[2ex] 
27063  636 

637 
\multicolumn{3}{l}{Diagnostics} \\ 

638 

639 
\textit{toplevel} & ::= 

32981  640 
& \textbf{print\_locales} \\ 
641 
&  & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\ 

642 
&  & \textbf{print\_interps} \textit{locale} 

27063  643 
\end{tabular} 
644 
\end{center} 

645 
\hrule 

30826  646 
\caption{Syntax of Locale Commands.} 
27063  647 
\label{tab:commands} 
648 
\end{table} 

649 
*} 

650 

32981  651 
text {* \textbf{Revision History.} For the present third revision, 
652 
which was completed in October 2009, much of the explanatory text 

653 
has been rewritten. In addition, inheritance of interpretation 

654 
equations, which was not available for Isabelle 2009, but in the 

655 
meantime has been implemented, is illustrated. The second revision 

656 
accommodates changes introduced by the locales reimplementation for 

657 
Isabelle 2009. Most notably, in complex specifications 

658 
(\emph{locale expressions}) renaming has been generalised to 

659 
instantiation. *} 

660 

27063  661 
text {* \textbf{Acknowledgements.} Alexander Krauss, Tobias Nipkow, 
32981  662 
Randy Pollack, Christian Sternagel and Makarius Wenzel have made 
663 
useful comments on earlier versions of this document. *} 

27063  664 

665 
end 