author | ballarin |
Sat, 28 Mar 2009 22:14:21 +0100 | |
changeset 30780 | c3f1e8a9e0b5 |
parent 30751 | 36a255c2e428 |
child 30782 | 38e477e8524f |
permissions | -rw-r--r-- |
27063 | 1 |
theory Examples3 |
2 |
imports Examples |
|
3 |
begin |
|
4 |
||
5 |
subsection {* Third Version: Local Interpretation *} |
|
6 |
||
7 |
text {* In the above example, the fact that @{text \<le>} is a partial |
|
8 |
order for the natural numbers was used in the proof of the |
|
9 |
second goal. In general, proofs of the equations may involve |
|
10 |
theorems implied by the fact the assumptions of the instantiated |
|
11 |
locale hold for the instantiating structure. If these theorems have |
|
12 |
been shown abstractly in the locale they can be made available |
|
13 |
conveniently in the context through an auxiliary local interpretation (keyword |
|
14 |
\isakeyword{interpret}). This interpretation is inside the proof of the global |
|
15 |
interpretation. The third revision of the example illustrates this. *} |
|
16 |
||
30780 | 17 |
interpretation %visible nat: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool" |
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
18 |
where "partial_order.less op \<le> (x::nat) y = (x < y)" |
27063 | 19 |
proof - |
20 |
show "partial_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)" |
|
21 |
by unfold_locales auto |
|
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset
|
22 |
then interpret nat: partial_order "op \<le> :: [nat, nat] \<Rightarrow> bool" . |
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
23 |
show "partial_order.less op \<le> (x::nat) y = (x < y)" |
27063 | 24 |
unfolding nat.less_def by auto |
25 |
qed |
|
26 |
||
27 |
text {* The inner interpretation does not require an |
|
28 |
elaborate new proof, it is immediate from the preceeding fact and |
|
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
29 |
proved with ``.''. Strict qualifiers are normally not necessary for |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
30 |
interpretations inside proofs, since these have only limited scope. |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
31 |
|
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
32 |
The above interpretation enriches the local proof context by |
27063 | 33 |
the very theorems also obtained in the interpretation from |
34 |
Section~\ref{sec:po-first}, and @{text nat.less_def} may directly be |
|
35 |
used to unfold the definition. Theorems from the local |
|
36 |
interpretation disappear after leaving the proof context --- that |
|
37 |
is, after the closing \isakeyword{qed} --- and are |
|
38 |
then replaced by those with the desired substitutions of the strict |
|
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
39 |
order. *} |
27063 | 40 |
|
41 |
||
42 |
subsection {* Further Interpretations *} |
|
43 |
||
44 |
text {* Further interpretations are necessary to reuse theorems from |
|
45 |
the other locales. In @{text lattice} the operations @{text \<sqinter>} and |
|
46 |
@{text \<squnion>} are substituted by @{term "min :: nat \<Rightarrow> nat \<Rightarrow> nat"} and |
|
47 |
@{term "max :: nat \<Rightarrow> nat \<Rightarrow> nat"}. The entire proof for the |
|
48 |
interpretation is reproduced in order to give an example of a more |
|
49 |
elaborate interpretation proof. *} |
|
50 |
||
30780 | 51 |
interpretation %visible nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool" |
27063 | 52 |
where "lattice.meet op \<le> (x::nat) y = min x y" |
53 |
and "lattice.join op \<le> (x::nat) y = max x y" |
|
54 |
proof - |
|
55 |
show "lattice (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)" |
|
56 |
txt {* We have already shown that this is a partial order, *} |
|
57 |
apply unfold_locales |
|
58 |
txt {* hence only the lattice axioms remain to be shown: @{subgoals |
|
59 |
[display]} After unfolding @{text is_inf} and @{text is_sup}, *} |
|
60 |
apply (unfold nat.is_inf_def nat.is_sup_def) |
|
61 |
txt {* the goals become @{subgoals [display]} which can be solved |
|
62 |
by Presburger arithmetic. *} |
|
63 |
by arith+ |
|
64 |
txt {* In order to show the equations, we put ourselves in a |
|
65 |
situation where the lattice theorems can be used in a convenient way. *} |
|
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset
|
66 |
then interpret nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool" . |
27063 | 67 |
show "lattice.meet op \<le> (x::nat) y = min x y" |
68 |
by (bestsimp simp: nat.meet_def nat.is_inf_def) |
|
69 |
show "lattice.join op \<le> (x::nat) y = max x y" |
|
70 |
by (bestsimp simp: nat.join_def nat.is_sup_def) |
|
71 |
qed |
|
72 |
||
73 |
text {* That the relation @{text \<le>} is a total order completes this |
|
74 |
sequence of interpretations. *} |
|
75 |
||
30780 | 76 |
interpretation %visible nat: total_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool" |
27063 | 77 |
by unfold_locales arith |
78 |
||
79 |
text {* Theorems that are available in the theory at this point are shown in |
|
80 |
Table~\ref{tab:nat-lattice}. |
|
81 |
||
82 |
\begin{table} |
|
83 |
\hrule |
|
84 |
\vspace{2ex} |
|
85 |
\begin{center} |
|
86 |
\begin{tabular}{l} |
|
87 |
@{thm [source] nat.less_def} from locale @{text partial_order}: \\ |
|
88 |
\quad @{thm nat.less_def} \\ |
|
89 |
@{thm [source] nat.meet_left} from locale @{text lattice}: \\ |
|
90 |
\quad @{thm nat.meet_left} \\ |
|
91 |
@{thm [source] nat.join_distr} from locale @{text distrib_lattice}: \\ |
|
92 |
\quad @{thm nat.join_distr} \\ |
|
93 |
@{thm [source] nat.less_total} from locale @{text total_order}: \\ |
|
94 |
\quad @{thm nat.less_total} |
|
95 |
\end{tabular} |
|
96 |
\end{center} |
|
97 |
\hrule |
|
98 |
\caption{Interpreted theorems for @{text \<le>} on the natural numbers.} |
|
99 |
\label{tab:nat-lattice} |
|
100 |
\end{table} |
|
101 |
||
102 |
Note that since the locale hierarchy reflects that total orders are |
|
103 |
distributive lattices, an explicit interpretation of distributive |
|
104 |
lattices for the order relation on natural numbers is not neccessary. |
|
105 |
||
106 |
Why not push this idea further and just give the last interpretation |
|
107 |
as a single interpretation instead of the sequence of three? The |
|
108 |
reasons for this are twofold: |
|
109 |
\begin{itemize} |
|
110 |
\item |
|
111 |
Often it is easier to work in an incremental fashion, because later |
|
112 |
interpretations require theorems provided by earlier |
|
113 |
interpretations. |
|
114 |
\item |
|
115 |
Assume that a definition is made in some locale $l_1$, and that $l_2$ |
|
116 |
imports $l_1$. Let an equation for the definition be |
|
117 |
proved in an interpretation of $l_2$. The equation will be unfolded |
|
118 |
in interpretations of theorems added to $l_2$ or below in the import |
|
119 |
hierarchy, but not for theorems added above $l_2$. |
|
120 |
Hence, an equation interpreting a definition should always be given in |
|
121 |
an interpretation of the locale where the definition is made, not in |
|
122 |
an interpretation of a locale further down the hierarchy. |
|
123 |
\end{itemize} |
|
124 |
*} |
|
125 |
||
126 |
||
127 |
subsection {* Lattice @{text "dvd"} on @{typ nat} *} |
|
128 |
||
129 |
text {* Divisibility on the natural numbers is a distributive lattice |
|
130 |
but not a total order. Interpretation again proceeds |
|
131 |
incrementally. *} |
|
132 |
||
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset
|
133 |
interpretation nat_dvd: partial_order "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" |
27063 | 134 |
where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)" |
135 |
proof - |
|
136 |
show "partial_order (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)" |
|
137 |
by unfold_locales (auto simp: dvd_def) |
|
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset
|
138 |
then interpret nat_dvd: partial_order "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" . |
27063 | 139 |
show "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)" |
140 |
apply (unfold nat_dvd.less_def) |
|
141 |
apply auto |
|
142 |
done |
|
143 |
qed |
|
144 |
||
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
145 |
text {* Note that in Isabelle/HOL there is no symbol for strict |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
146 |
divisibility. Instead, interpretation substitutes @{term "x dvd y \<and> |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
147 |
x \<noteq> y"}. *} |
27063 | 148 |
|
30780 | 149 |
interpretation nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" |
27063 | 150 |
where nat_dvd_meet_eq: |
27595 | 151 |
"lattice.meet op dvd = gcd" |
27063 | 152 |
and nat_dvd_join_eq: |
27595 | 153 |
"lattice.join op dvd = lcm" |
27063 | 154 |
proof - |
155 |
show "lattice (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)" |
|
156 |
apply unfold_locales |
|
157 |
apply (unfold nat_dvd.is_inf_def nat_dvd.is_sup_def) |
|
27595 | 158 |
apply (rule_tac x = "gcd x y" in exI) |
27063 | 159 |
apply auto [1] |
27595 | 160 |
apply (rule_tac x = "lcm x y" in exI) |
27063 | 161 |
apply (auto intro: lcm_dvd1 lcm_dvd2 lcm_least) |
162 |
done |
|
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset
|
163 |
then interpret nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" . |
27595 | 164 |
show "lattice.meet op dvd = gcd" |
165 |
apply (auto simp add: expand_fun_eq) |
|
27063 | 166 |
apply (unfold nat_dvd.meet_def) |
167 |
apply (rule the_equality) |
|
168 |
apply (unfold nat_dvd.is_inf_def) |
|
169 |
by auto |
|
27595 | 170 |
show "lattice.join op dvd = lcm" |
171 |
apply (auto simp add: expand_fun_eq) |
|
27063 | 172 |
apply (unfold nat_dvd.join_def) |
173 |
apply (rule the_equality) |
|
174 |
apply (unfold nat_dvd.is_sup_def) |
|
175 |
by (auto intro: lcm_dvd1 lcm_dvd2 lcm_least) |
|
176 |
qed |
|
177 |
||
178 |
text {* Equations @{thm [source] nat_dvd_meet_eq} and @{thm [source] |
|
179 |
nat_dvd_join_eq} are named since they are handy in the proof of |
|
180 |
the subsequent interpretation. *} |
|
181 |
||
182 |
(* |
|
183 |
definition |
|
184 |
is_lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where |
|
185 |
"is_lcm p m n \<longleftrightarrow> m dvd p \<and> n dvd p \<and> |
|
186 |
(\<forall>d. m dvd d \<longrightarrow> n dvd d \<longrightarrow> p dvd d)" |
|
187 |
||
188 |
lemma is_gcd: "is_lcm (lcm (m, n)) m n" |
|
189 |
by (simp add: is_lcm_def lcm_least) |
|
190 |
||
191 |
lemma gcd_lcm_distr_lemma: |
|
192 |
"[| is_gcd g1 x l1; is_lcm l1 y z; is_gcd g2 x y; is_gcd g3 x z |] ==> is_lcm g1 g2 g3" |
|
193 |
apply (unfold is_gcd_def is_lcm_def dvd_def) |
|
194 |
apply (clarsimp simp: mult_ac) |
|
195 |
apply (blast intro: mult_is_0) |
|
196 |
thm mult_is_0 [THEN iffD1] |
|
197 |
*) |
|
198 |
||
199 |
lemma %invisible gcd_lcm_distr: |
|
27595 | 200 |
"gcd x (lcm y z) = lcm (gcd x y) (gcd x z)" sorry |
27063 | 201 |
|
30780 | 202 |
interpretation %visible nat_dvd: |
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset
|
203 |
distrib_lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" |
27063 | 204 |
apply unfold_locales |
205 |
txt {* @{subgoals [display]} *} |
|
206 |
apply (unfold nat_dvd_meet_eq nat_dvd_join_eq) |
|
207 |
txt {* @{subgoals [display]} *} |
|
208 |
apply (rule gcd_lcm_distr) done |
|
209 |
||
210 |
||
211 |
text {* Theorems that are available in the theory after these |
|
212 |
interpretations are shown in Table~\ref{tab:nat-dvd-lattice}. |
|
213 |
||
214 |
\begin{table} |
|
215 |
\hrule |
|
216 |
\vspace{2ex} |
|
217 |
\begin{center} |
|
218 |
\begin{tabular}{l} |
|
219 |
@{thm [source] nat_dvd.less_def} from locale @{text partial_order}: \\ |
|
220 |
\quad @{thm nat_dvd.less_def} \\ |
|
221 |
@{thm [source] nat_dvd.meet_left} from locale @{text lattice}: \\ |
|
222 |
\quad @{thm nat_dvd.meet_left} \\ |
|
223 |
@{thm [source] nat_dvd.join_distr} from locale @{text distrib_lattice}: \\ |
|
224 |
\quad @{thm nat_dvd.join_distr} \\ |
|
225 |
\end{tabular} |
|
226 |
\end{center} |
|
227 |
\hrule |
|
228 |
\caption{Interpreted theorems for @{text dvd} on the natural numbers.} |
|
229 |
\label{tab:nat-dvd-lattice} |
|
230 |
\end{table} |
|
231 |
*} |
|
232 |
||
233 |
text {* |
|
234 |
The full syntax of the interpretation commands is shown in |
|
235 |
Table~\ref{tab:commands}. The grammar refers to |
|
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
236 |
\textit{expression}, which stands for a \emph{locale} expression. |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
237 |
Locale expressions are discussed in the following section. |
27063 | 238 |
*} |
239 |
||
240 |
||
27077 | 241 |
section {* Locale Expressions \label{sec:expressions} *} |
27063 | 242 |
|
243 |
text {* |
|
244 |
A map @{term \<phi>} between partial orders @{text \<sqsubseteq>} and @{text \<preceq>} |
|
245 |
is called order preserving if @{text "x \<sqsubseteq> y"} implies @{text "\<phi> x \<preceq> |
|
246 |
\<phi> y"}. This situation is more complex than those encountered so |
|
247 |
far: it involves two partial orders, and it is desirable to use the |
|
248 |
existing locale for both. |
|
249 |
||
250 |
Inspecting the grammar of locale commands in |
|
251 |
Table~\ref{tab:commands} reveals that the import of a locale can be |
|
252 |
more than just a single locale. In general, the import is a |
|
30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
253 |
\emph{locale expression}. These enable to combine locales |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
254 |
and instantiate parameters. A locale expression is a sequence of |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
255 |
locale \emph{instances} followed by an optional \isakeyword{for} |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
256 |
clause. Each instance consists of a locale reference, which may be |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
257 |
preceded by a qualifer and succeeded by instantiations of the |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
258 |
parameters of that locale. Instantiations may be either positional |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
259 |
or through explicit parameter argument pairs. |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
260 |
|
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
261 |
Using a locale expression, a locale for order |
27063 | 262 |
preserving maps can be declared in the following way. *} |
263 |
||
264 |
locale order_preserving = |
|
30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
265 |
le: partial_order le + le': partial_order le' |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
266 |
for le (infixl "\<sqsubseteq>" 50) and le' (infixl "\<preceq>" 50) + |
27063 | 267 |
fixes \<phi> :: "'a \<Rightarrow> 'b" |
268 |
assumes hom_le: "x \<sqsubseteq> y \<Longrightarrow> \<phi> x \<preceq> \<phi> y" |
|
269 |
||
30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
270 |
text {* The second and third line contain the expression --- two |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
271 |
instances of the partial order locale with instantiations @{text le} |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
272 |
and @{text le'}, respectively. The \isakeyword{for} clause consists |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
273 |
of parameter declarations and is similar to the context element |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
274 |
\isakeyword{fixes}. The notable difference is that the |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
275 |
\isakeyword{for} clause is part of the expression, and only |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
276 |
parameters defined in the expression may occur in its instances. |
27063 | 277 |
|
30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
278 |
Instances are \emph{morphisms} on locales. Their effect on the |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
279 |
parameters is naturally lifted to terms, propositions and theorems, |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
280 |
and thus to the assumptions and conclusions of a locale. The |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
281 |
assumption of a locale expression is the conjunction of the |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
282 |
assumptions of the instances. The conclusions of a sequence of |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
283 |
instances are obtained by appending the conclusions of the |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
284 |
instances in the order of the sequence. |
27063 | 285 |
|
30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
286 |
The qualifiers in the expression are already a familiar concept from |
30780 | 287 |
the \isakeyword{interpretation} command |
288 |
(Section~\ref{sec:po-first}). Here, they serve to distinguish names |
|
289 |
(in particular theorem names) for the two partial orders within the |
|
290 |
locale. Qualifiers in the \isakeyword{locale} command (and in |
|
291 |
\isakeyword{sublocale}) default to optional --- that is, they need |
|
292 |
not occur in references to the qualified names. Here are examples |
|
293 |
of theorems in locale @{text order_preserving}: *} |
|
27063 | 294 |
|
295 |
context %invisible order_preserving begin |
|
296 |
||
297 |
text {* |
|
298 |
@{thm [source] le.less_le_trans}: @{thm le.less_le_trans} |
|
299 |
||
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset
|
300 |
@{thm [source] hom_le}: @{thm hom_le} |
27063 | 301 |
*} |
302 |
||
30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
303 |
text {* The theorems for the partial order @{text \<preceq>} |
27063 | 304 |
are qualified by @{text le'}. For example, @{thm [source] |
305 |
le'.less_le_trans}: @{thm [display, indent=2] le'.less_le_trans} *} |
|
306 |
||
307 |
end %invisible |
|
308 |
||
309 |
text {* This example reveals that there is no infix syntax for the strict |
|
30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
310 |
version of @{text \<preceq>}! This can be declared through an abbreviation. |
27063 | 311 |
*} |
312 |
||
313 |
abbreviation (in order_preserving) |
|
314 |
less' (infixl "\<prec>" 50) where "less' \<equiv> partial_order.less le'" |
|
315 |
||
30393
aa6f42252bf6
replaced old locale option by proper "text (in locale)";
wenzelm
parents:
29568
diff
changeset
|
316 |
text (in order_preserving) {* Now the theorem is displayed nicely as |
aa6f42252bf6
replaced old locale option by proper "text (in locale)";
wenzelm
parents:
29568
diff
changeset
|
317 |
@{thm le'.less_le_trans}. *} |
27063 | 318 |
|
30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
319 |
text {* Qualifiers not only apply to theorem names, but also to names |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
320 |
introduced by definitions and abbreviations. In locale |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
321 |
@{text partial_order} the full name of the strict order of @{text \<sqsubseteq>} is |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
322 |
@{text le.less} and therefore @{text le'.less} is the full name of |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
323 |
the strict order of @{text \<preceq>}. Hence, the equation in the |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
324 |
abbreviation above could have been also written as @{text "less' \<equiv> |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
325 |
le'.less"}. *} |
27063 | 326 |
|
30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
327 |
text {* Readers may find the declaration of locale @{text |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
328 |
order_preserving} a little awkward, because the declaration and |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
329 |
concrete syntax for @{text le} from @{text partial_order} are |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
330 |
repeated in the declaration of @{text order_preserving}. Locale |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
331 |
expressions provide a convenient short hand for this. A parameter |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
332 |
in an instance is \emph{untouched} if no instantiation term is |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
333 |
provided for it. In positional instantiations, a parameter position |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
334 |
may be skipped with an underscore, and it is allowed to give fewer |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
335 |
instantiation terms than the instantiated locale's number of |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
336 |
parameters. In named instantiations, instantiation pairs for |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
337 |
certain parameters may simply be omitted. Untouched parameters are |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
338 |
declared by the locale expression and with their concrete syntax by |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
339 |
implicitly adding them to the beginning of the \isakeyword{for} |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
340 |
clause. |
27063 | 341 |
|
30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
342 |
The following locales illustrate this. A map @{text \<phi>} is a |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
343 |
lattice homomorphism if it preserves meet and join. *} |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
344 |
|
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
345 |
locale lattice_hom = |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
346 |
le: lattice + le': lattice le' for le' (infixl "\<preceq>" 50) + |
27063 | 347 |
fixes \<phi> |
348 |
assumes hom_meet: |
|
30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
349 |
"\<phi> (x \<sqinter> y) = le'.meet (\<phi> x) (\<phi> y)" |
27063 | 350 |
and hom_join: |
30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
351 |
"\<phi> (x \<squnion> y) = le'.join (\<phi> x) (\<phi> y)" |
27063 | 352 |
|
353 |
abbreviation (in lattice_hom) |
|
354 |
meet' (infixl "\<sqinter>''" 50) where "meet' \<equiv> le'.meet" |
|
355 |
abbreviation (in lattice_hom) |
|
356 |
join' (infixl "\<squnion>''" 50) where "join' \<equiv> le'.join" |
|
357 |
||
358 |
text {* A homomorphism is an endomorphism if both orders coincide. *} |
|
359 |
||
30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
360 |
locale lattice_end = lattice_hom _ le |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
361 |
|
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
362 |
text {* In this declaration, the first parameter of @{text |
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
363 |
lattice_hom}, @{text le}, is untouched and then used to instantiate |
30780 | 364 |
the second parameter. Its concrete syntax is preserved. *} |
30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
365 |
|
27063 | 366 |
|
367 |
text {* The inheritance diagram of the situation we have now is shown |
|
368 |
in Figure~\ref{fig:hom}, where the dashed line depicts an |
|
369 |
interpretation which is introduced below. Renamings are |
|
370 |
indicated by $\sqsubseteq \mapsto \preceq$ etc. The expression |
|
371 |
imported by @{text lattice_end} identifies the first and second |
|
372 |
parameter of @{text lattice_hom}. By looking at the inheritance diagram it would seem |
|
373 |
that two identical copies of each of the locales @{text |
|
374 |
partial_order} and @{text lattice} are imported. This is not the |
|
375 |
case! Inheritance paths with identical morphisms are detected and |
|
27503 | 376 |
the conclusions of the respective locales appear only once. |
27063 | 377 |
|
378 |
\begin{figure} |
|
379 |
\hrule \vspace{2ex} |
|
380 |
\begin{center} |
|
381 |
\begin{tikzpicture} |
|
382 |
\node (o) at (0,0) {@{text partial_order}}; |
|
383 |
\node (oh) at (1.5,-2) {@{text order_preserving}}; |
|
384 |
\node (oh1) at (1.5,-0.7) {$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$}; |
|
385 |
\node (oh2) at (0,-1.3) {$\scriptscriptstyle \sqsubseteq \mapsto \preceq$}; |
|
386 |
\node (l) at (-1.5,-2) {@{text lattice}}; |
|
387 |
\node (lh) at (0,-4) {@{text lattice_hom}}; |
|
388 |
\node (lh1) at (0,-2.7) {$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$}; |
|
389 |
\node (lh2) at (-1.5,-3.3) {$\scriptscriptstyle \sqsubseteq \mapsto \preceq$}; |
|
390 |
\node (le) at (0,-6) {@{text lattice_end}}; |
|
391 |
\node (le1) at (0,-4.8) |
|
392 |
[anchor=west]{$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$}; |
|
393 |
\node (le2) at (0,-5.2) |
|
394 |
[anchor=west]{$\scriptscriptstyle \preceq \mapsto \sqsubseteq$}; |
|
395 |
\draw (o) -- (l); |
|
396 |
\draw[dashed] (oh) -- (lh); |
|
397 |
\draw (lh) -- (le); |
|
398 |
\draw (o) .. controls (oh1.south west) .. (oh); |
|
399 |
\draw (o) .. controls (oh2.north east) .. (oh); |
|
400 |
\draw (l) .. controls (lh1.south west) .. (lh); |
|
401 |
\draw (l) .. controls (lh2.north east) .. (lh); |
|
402 |
\end{tikzpicture} |
|
403 |
\end{center} |
|
404 |
\hrule |
|
405 |
\caption{Hierarchy of Homomorphism Locales.} |
|
406 |
\label{fig:hom} |
|
407 |
\end{figure} |
|
408 |
*} |
|
409 |
||
410 |
text {* It can be shown easily that a lattice homomorphism is order |
|
411 |
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
|
412 |
interpretation is used to assert this: *} |
27063 | 413 |
|
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset
|
414 |
sublocale lattice_hom \<subseteq> order_preserving proof unfold_locales |
27063 | 415 |
fix x y |
416 |
assume "x \<sqsubseteq> y" |
|
417 |
then have "y = (x \<squnion> y)" by (simp add: le.join_connection) |
|
418 |
then have "\<phi> y = (\<phi> x \<squnion>' \<phi> y)" by (simp add: hom_join [symmetric]) |
|
419 |
then show "\<phi> x \<preceq> \<phi> y" by (simp add: le'.join_connection) |
|
420 |
qed |
|
421 |
||
30393
aa6f42252bf6
replaced old locale option by proper "text (in locale)";
wenzelm
parents:
29568
diff
changeset
|
422 |
text (in lattice_hom) {* |
aa6f42252bf6
replaced old locale option by proper "text (in locale)";
wenzelm
parents:
29568
diff
changeset
|
423 |
Theorems and other declarations --- syntax, in particular --- from |
aa6f42252bf6
replaced old locale option by proper "text (in locale)";
wenzelm
parents:
29568
diff
changeset
|
424 |
the locale @{text order_preserving} are now active in @{text |
27063 | 425 |
lattice_hom}, for example |
30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
426 |
|
30393
aa6f42252bf6
replaced old locale option by proper "text (in locale)";
wenzelm
parents:
29568
diff
changeset
|
427 |
@{thm [source] le'.less_le_trans}: |
aa6f42252bf6
replaced old locale option by proper "text (in locale)";
wenzelm
parents:
29568
diff
changeset
|
428 |
@{thm le'.less_le_trans} |
27063 | 429 |
*} |
430 |
||
431 |
||
432 |
||
433 |
section {* Further Reading *} |
|
434 |
||
435 |
text {* More information on locales and their interpretation is |
|
436 |
available. For the locale hierarchy of import and interpretation |
|
437 |
dependencies see \cite{Ballarin2006a}; interpretations in theories |
|
438 |
and proofs are covered in \cite{Ballarin2006b}. In the latter, we |
|
439 |
show how interpretation in proofs enables to reason about families |
|
440 |
of algebraic structures, which cannot be expressed with locales |
|
441 |
directly. |
|
442 |
||
443 |
Haftmann and Wenzel \cite{HaftmannWenzel2007} overcome a restriction |
|
444 |
of axiomatic type classes through a combination with locale |
|
445 |
interpretation. The result is a Haskell-style class system with a |
|
30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset
|
446 |
facility to generate ML and Haskell code. Classes are sufficient for |
27063 | 447 |
simple specifications with a single type parameter. The locales for |
448 |
orders and lattices presented in this tutorial fall into this |
|
449 |
category. Order preserving maps, homomorphisms and vector spaces, |
|
450 |
on the other hand, do not. |
|
451 |
||
452 |
The original work of Kamm\"uller on locales \cite{KammullerEtAl1999} |
|
453 |
may be of interest from a historical perspective. The mathematical |
|
454 |
background on orders and lattices is taken from Jacobson's textbook |
|
455 |
on algebra \cite[Chapter~8]{Jacobson1985}. |
|
456 |
*} |
|
457 |
||
458 |
text {* |
|
459 |
\begin{table} |
|
460 |
\hrule |
|
461 |
\vspace{2ex} |
|
462 |
\begin{center} |
|
463 |
\begin{tabular}{l>$c<$l} |
|
464 |
\multicolumn{3}{l}{Miscellaneous} \\ |
|
465 |
||
466 |
\textit{attr-name} & ::= |
|
467 |
& \textit{name} $|$ \textit{attribute} $|$ |
|
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset
|
468 |
\textit{name} \textit{attribute} \\ |
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset
|
469 |
\textit{qualifier} & ::= |
30751 | 470 |
& \textit{name} [``\textbf{?}'' $|$ ``\textbf{!}''] \\[2ex] |
27063 | 471 |
|
472 |
\multicolumn{3}{l}{Context Elements} \\ |
|
473 |
||
474 |
\textit{fixes} & ::= |
|
475 |
& \textit{name} [ ``\textbf{::}'' \textit{type} ] |
|
476 |
[ ``\textbf{(}'' \textbf{structure} ``\textbf{)}'' $|$ |
|
477 |
\textit{mixfix} ] \\ |
|
478 |
\begin{comment} |
|
479 |
\textit{constrains} & ::= |
|
480 |
& \textit{name} ``\textbf{::}'' \textit{type} \\ |
|
481 |
\end{comment} |
|
482 |
\textit{assumes} & ::= |
|
483 |
& [ \textit{attr-name} ``\textbf{:}'' ] \textit{proposition} \\ |
|
484 |
\begin{comment} |
|
485 |
\textit{defines} & ::= |
|
486 |
& [ \textit{attr-name} ``\textbf{:}'' ] \textit{proposition} \\ |
|
487 |
\textit{notes} & ::= |
|
488 |
& [ \textit{attr-name} ``\textbf{=}'' ] |
|
489 |
( \textit{qualified-name} [ \textit{attribute} ] )$^+$ \\ |
|
490 |
\end{comment} |
|
491 |
||
492 |
\textit{element} & ::= |
|
493 |
& \textbf{fixes} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ \\ |
|
494 |
\begin{comment} |
|
495 |
& | |
|
496 |
& \textbf{constrains} \textit{constrains} |
|
497 |
( \textbf{and} \textit{constrains} )$^*$ \\ |
|
498 |
\end{comment} |
|
499 |
& | |
|
500 |
& \textbf{assumes} \textit{assumes} ( \textbf{and} \textit{assumes} )$^*$ \\[2ex] |
|
501 |
%\begin{comment} |
|
502 |
% & | |
|
503 |
% & \textbf{defines} \textit{defines} ( \textbf{and} \textit{defines} )$^*$ \\ |
|
504 |
% & | |
|
505 |
% & \textbf{notes} \textit{notes} ( \textbf{and} \textit{notes} )$^*$ \\ |
|
506 |
%\end{comment} |
|
507 |
||
508 |
\multicolumn{3}{l}{Locale Expressions} \\ |
|
509 |
||
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset
|
510 |
\textit{pos-insts} & ::= |
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset
|
511 |
& ( \textit{term} $|$ ``\textbf{\_}'' )$^*$ \\ |
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset
|
512 |
\textit{named-insts} & ::= |
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset
|
513 |
& \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
|
514 |
( \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
|
515 |
\textit{instance} & ::= |
30751 | 516 |
& [ \textit{qualifier} ``\textbf{:}'' ] |
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset
|
517 |
\textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\ |
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset
|
518 |
\textit{expression} & ::= |
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset
|
519 |
& \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$ |
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset
|
520 |
[ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex] |
27063 | 521 |
|
522 |
\multicolumn{3}{l}{Declaration of Locales} \\ |
|
523 |
||
524 |
\textit{locale} & ::= |
|
525 |
& \textit{element}$^+$ \\ |
|
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset
|
526 |
& | & \textit{expression} [ ``\textbf{+}'' \textit{element}$^+$ ] \\ |
27063 | 527 |
\textit{toplevel} & ::= |
528 |
& \textbf{locale} \textit{name} [ ``\textbf{=}'' |
|
529 |
\textit{locale} ] \\[2ex] |
|
530 |
||
531 |
\multicolumn{3}{l}{Interpretation} \\ |
|
532 |
||
533 |
\textit{equation} & ::= & [ \textit{attr-name} ``\textbf{:}'' ] |
|
534 |
\textit{prop} \\ |
|
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset
|
535 |
\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
|
536 |
\textit{equation} )$^*$ \\ |
27063 | 537 |
\textit{toplevel} & ::= |
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset
|
538 |
& \textbf{sublocale} \textit{name} ( ``$<$'' $|$ |
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset
|
539 |
``$\subseteq$'' ) \textit{expression} \textit{proof} \\ |
27063 | 540 |
& | |
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset
|
541 |
& \textbf{interpretation} |
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset
|
542 |
\textit{expression} [ \textit{equations} ] \textit{proof} \\ |
27063 | 543 |
& | |
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset
|
544 |
& \textbf{interpret} |
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset
|
545 |
\textit{expression} \textit{proof} \\[2ex] |
27063 | 546 |
|
547 |
\multicolumn{3}{l}{Diagnostics} \\ |
|
548 |
||
549 |
\textit{toplevel} & ::= |
|
550 |
& \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\ |
|
551 |
& | & \textbf{print\_locales} |
|
552 |
\end{tabular} |
|
553 |
\end{center} |
|
554 |
\hrule |
|
29567 | 555 |
\caption{Syntax of Locale Commands (abridged).} |
27063 | 556 |
\label{tab:commands} |
557 |
\end{table} |
|
558 |
*} |
|
559 |
||
560 |
text {* \textbf{Acknowledgements.} Alexander Krauss, Tobias Nipkow, |
|
561 |
Christian Sternagel and Makarius Wenzel have made useful comments on |
|
562 |
a draft of this document. *} |
|
563 |
||
564 |
end |