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