author  ballarin 
Tue, 31 Mar 2009 21:25:08 +0200  
changeset 30826  a53f4872400e 
parent 30782  38e477e8524f 
child 31748  530596c997da 
permissions  rwrr 
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 15 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:pofirst}, 

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:natlattice}. 

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:natlattice} 

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 15 to locale reimplementation.
ballarin
parents:
30393
diff
changeset

140 
text {* Note that in Isabelle/HOL there is no symbol for strict 
cc5a55d7a5be
Updated chapters 15 to locale reimplementation.
ballarin
parents:
30393
diff
changeset

141 
divisibility. Instead, interpretation substitutes @{term "x dvd y \<and> 
cc5a55d7a5be
Updated chapters 15 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)" 
38e477e8524f
In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents:
30780
diff
changeset

146 
and nat_dvd_meet_eq: "lattice.meet op dvd = gcd" 
38e477e8524f
In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents:
30780
diff
changeset

147 
and nat_dvd_join_eq: "lattice.join op dvd = 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) 
27063  155 
apply (auto intro: lcm_dvd1 lcm_dvd2 lcm_least) 
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) 
27595  160 
show "lattice.meet op dvd = gcd" 
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 

27595  166 
show "lattice.join op dvd = lcm" 
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) 

171 
by (auto intro: lcm_dvd1 lcm_dvd2 lcm_least) 

172 
qed 

173 

174 
text {* Equations @{thm [source] nat_dvd_meet_eq} and @{thm [source] 

30826  175 
nat_dvd_join_eq} are used in the main part the subsequent 
176 
interpretation. *} 

27063  177 

178 
(* 

179 
definition 

180 
is_lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where 

181 
"is_lcm p m n \<longleftrightarrow> m dvd p \<and> n dvd p \<and> 

182 
(\<forall>d. m dvd d \<longrightarrow> n dvd d \<longrightarrow> p dvd d)" 

183 

184 
lemma is_gcd: "is_lcm (lcm (m, n)) m n" 

185 
by (simp add: is_lcm_def lcm_least) 

186 

187 
lemma gcd_lcm_distr_lemma: 

188 
"[ 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" 

189 
apply (unfold is_gcd_def is_lcm_def dvd_def) 

190 
apply (clarsimp simp: mult_ac) 

191 
apply (blast intro: mult_is_0) 

192 
thm mult_is_0 [THEN iffD1] 

193 
*) 

194 

195 
lemma %invisible gcd_lcm_distr: 

27595  196 
"gcd x (lcm y z) = lcm (gcd x y) (gcd x z)" sorry 
27063  197 

30780  198 
interpretation %visible nat_dvd: 
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

199 
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

200 
where "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

201 
and "lattice.meet op dvd = gcd" 
38e477e8524f
In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents:
30780
diff
changeset

202 
and "lattice.join op dvd = lcm" 
38e477e8524f
In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents:
30780
diff
changeset

203 
proof  
38e477e8524f
In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents:
30780
diff
changeset

204 
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

205 
apply unfold_locales 
38e477e8524f
In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents:
30780
diff
changeset

206 
txt {* @{subgoals [display]} *} 
38e477e8524f
In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents:
30780
diff
changeset

207 
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

208 
txt {* @{subgoals [display]} *} 
38e477e8524f
In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents:
30780
diff
changeset

209 
apply (rule gcd_lcm_distr) 
38e477e8524f
In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents:
30780
diff
changeset

210 
done 
38e477e8524f
In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents:
30780
diff
changeset

211 
qed (rule nat_dvd_less_eq nat_dvd_meet_eq nat_dvd_join_eq)+ 
27063  212 

213 

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

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

216 

217 
\begin{table} 

218 
\hrule 

219 
\vspace{2ex} 

220 
\begin{center} 

221 
\begin{tabular}{l} 

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

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

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

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

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

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

228 
\end{tabular} 

229 
\end{center} 

230 
\hrule 

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

232 
\label{tab:natdvdlattice} 

233 
\end{table} 

234 
*} 

235 

236 
text {* 

30826  237 
The syntax of the interpretation commands is shown in 
27063  238 
Table~\ref{tab:commands}. The grammar refers to 
30580
cc5a55d7a5be
Updated chapters 15 to locale reimplementation.
ballarin
parents:
30393
diff
changeset

239 
\textit{expression}, which stands for a \emph{locale} expression. 
cc5a55d7a5be
Updated chapters 15 to locale reimplementation.
ballarin
parents:
30393
diff
changeset

240 
Locale expressions are discussed in the following section. 
27063  241 
*} 
242 

243 

27077  244 
section {* Locale Expressions \label{sec:expressions} *} 
27063  245 

246 
text {* 

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

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

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

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

251 
existing locale for both. 

252 

253 
Inspecting the grammar of locale commands in 

254 
Table~\ref{tab:commands} reveals that the import of a locale can be 

255 
more than just a single locale. In general, the import is a 

30826  256 
\emph{locale expression}, which enables to combine locales 
30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

257 
and instantiate parameters. A locale expression is a sequence of 
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

258 
locale \emph{instances} followed by an optional \isakeyword{for} 
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

259 
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

260 
preceded by a qualifer and succeeded by instantiations of the 
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

261 
parameters of that locale. Instantiations may be either positional 
30826  262 
or through explicit mappings of parameters to arguments. 
30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

263 

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

264 
Using a locale expression, a locale for order 
27063  265 
preserving maps can be declared in the following way. *} 
266 

267 
locale order_preserving = 

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

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

269 
for le (infixl "\<sqsubseteq>" 50) and le' (infixl "\<preceq>" 50) + 
27063  270 
fixes \<phi> :: "'a \<Rightarrow> 'b" 
271 
assumes hom_le: "x \<sqsubseteq> y \<Longrightarrow> \<phi> x \<preceq> \<phi> y" 

272 

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

273 
text {* The second and third line contain the expression  two 
30826  274 
instances of the partial order locale where the parameter is 
275 
instantiated to @{text le} 

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

276 
and @{text le'}, respectively. The \isakeyword{for} clause consists 
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

277 
of parameter declarations and is similar to the context element 
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

278 
\isakeyword{fixes}. The notable difference is that the 
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

279 
\isakeyword{for} clause is part of the expression, and only 
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

280 
parameters defined in the expression may occur in its instances. 
27063  281 

30826  282 
Instances define \emph{morphisms} on locales. Their effect on the 
283 
parameters is lifted to terms, propositions and theorems in the 

284 
canonical way, 

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

285 
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

286 
assumption of a locale expression is the conjunction of the 
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

287 
assumptions of the instances. The conclusions of a sequence of 
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

288 
instances are obtained by appending the conclusions of the 
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

289 
instances in the order of the sequence. 
27063  290 

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

291 
The qualifiers in the expression are already a familiar concept from 
30780  292 
the \isakeyword{interpretation} command 
293 
(Section~\ref{sec:pofirst}). Here, they serve to distinguish names 

294 
(in particular theorem names) for the two partial orders within the 

295 
locale. Qualifiers in the \isakeyword{locale} command (and in 

296 
\isakeyword{sublocale}) default to optional  that is, they need 

297 
not occur in references to the qualified names. Here are examples 

298 
of theorems in locale @{text order_preserving}: *} 

27063  299 

300 
context %invisible order_preserving begin 

301 

302 
text {* 

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

304 

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

305 
@{thm [source] hom_le}: @{thm hom_le} 
27063  306 
*} 
307 

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

308 
text {* The theorems for the partial order @{text \<preceq>} 
27063  309 
are qualified by @{text le'}. For example, @{thm [source] 
310 
le'.less_le_trans}: @{thm [display, indent=2] le'.less_le_trans} *} 

311 

312 
end %invisible 

313 

30826  314 
text {* This example reveals that there is no infix syntax for the 
315 
strict operation associated with @{text \<preceq>}. This can be declared 

316 
through an abbreviation. *} 

27063  317 

318 
abbreviation (in order_preserving) 

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

320 

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

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

27063  324 

30826  325 
text (in order_preserving) {* Qualifiers not only apply to theorem names, but also to names 
326 
introduced by definitions and abbreviations. For example, in @{text 

327 
partial_order} the name @{text less} abbreviates @{term 

328 
"partial_order.less le"}. Therefore, in @{text order_preserving} 

329 
the qualified name @{text le.less} abbreviates @{term 

330 
"partial_order.less le"} and @{text le'.less} abbreviates @{term 

331 
"partial_order.less le'"}. Hence, the equation in the abbreviation 

332 
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

333 
le'.less"}. *} 
27063  334 

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

335 
text {* Readers may find the declaration of locale @{text 
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

336 
order_preserving} a little awkward, because the declaration and 
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

337 
concrete syntax for @{text le} from @{text partial_order} are 
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

338 
repeated in the declaration of @{text order_preserving}. Locale 
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

339 
expressions provide a convenient short hand for this. A parameter 
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

340 
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

341 
provided for it. In positional instantiations, a parameter position 
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

342 
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

343 
instantiation terms than the instantiated locale's number of 
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

344 
parameters. In named instantiations, instantiation pairs for 
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

345 
certain parameters may simply be omitted. Untouched parameters are 
30826  346 
implicitly declared by the locale expression and with their concrete 
347 
syntax. In the sequence of parameters, they appear before the 

348 
parameters from the \isakeyword{for} clause. 

27063  349 

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

350 
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

351 
lattice homomorphism if it preserves meet and join. *} 
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

352 

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

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

354 
le: lattice + le': lattice le' for le' (infixl "\<preceq>" 50) + 
27063  355 
fixes \<phi> 
30826  356 
assumes hom_meet: "\<phi> (x \<sqinter> y) = le'.meet (\<phi> x) (\<phi> y)" 
357 
and hom_join: "\<phi> (x \<squnion> y) = le'.join (\<phi> x) (\<phi> y)" 

27063  358 

359 
abbreviation (in lattice_hom) 

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

361 
abbreviation (in lattice_hom) 

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

363 

364 
text {* A homomorphism is an endomorphism if both orders coincide. *} 

365 

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

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

367 

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

368 
text {* In this declaration, the first parameter of @{text 
30826  369 
lattice_hom}, @{text le}, is untouched and is then used to instantiate 
30780  370 
the second parameter. Its concrete syntax is preserved. *} 
30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

371 

27063  372 

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

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

375 
interpretation which is introduced below. Renamings are 

376 
indicated by $\sqsubseteq \mapsto \preceq$ etc. The expression 

377 
imported by @{text lattice_end} identifies the first and second 

378 
parameter of @{text lattice_hom}. By looking at the inheritance diagram it would seem 

379 
that two identical copies of each of the locales @{text 

380 
partial_order} and @{text lattice} are imported. This is not the 

381 
case! Inheritance paths with identical morphisms are detected and 

27503  382 
the conclusions of the respective locales appear only once. 
27063  383 

384 
\begin{figure} 

385 
\hrule \vspace{2ex} 

386 
\begin{center} 

387 
\begin{tikzpicture} 

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

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

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

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

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

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

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

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

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

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

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

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

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

401 
\draw (o)  (l); 

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

403 
\draw (lh)  (le); 

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

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

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

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

408 
\end{tikzpicture} 

409 
\end{center} 

410 
\hrule 

411 
\caption{Hierarchy of Homomorphism Locales.} 

412 
\label{fig:hom} 

413 
\end{figure} 

414 
*} 

415 

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

417 
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

418 
interpretation is used to assert this: *} 
27063  419 

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

420 
sublocale lattice_hom \<subseteq> order_preserving proof unfold_locales 
27063  421 
fix x y 
422 
assume "x \<sqsubseteq> y" 

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

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

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

426 
qed 

427 

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

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

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

430 
the locale @{text order_preserving} are now active in @{text 
27063  431 
lattice_hom}, for example 
30826  432 
@{thm [source] hom_le}: 
433 
@{thm [display, indent=2] hom_le} 

27063  434 
*} 
435 

436 

437 

438 
section {* Further Reading *} 

439 

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

441 
available. For the locale hierarchy of import and interpretation 

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

443 
and proofs are covered in \cite{Ballarin2006b}. In the latter, we 

444 
show how interpretation in proofs enables to reason about families 

445 
of algebraic structures, which cannot be expressed with locales 

446 
directly. 

447 

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

449 
of axiomatic type classes through a combination with locale 

450 
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

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

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

455 
on the other hand, do not. 

456 

457 
The original work of Kamm\"uller on locales \cite{KammullerEtAl1999} 

458 
may be of interest from a historical perspective. The mathematical 

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

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

461 
*} 

462 

463 
text {* 

464 
\begin{table} 

465 
\hrule 

466 
\vspace{2ex} 

467 
\begin{center} 

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

469 
\multicolumn{3}{l}{Miscellaneous} \\ 

470 

471 
\textit{attrname} & ::= 

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

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

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

474 
\textit{qualifier} & ::= 
30751  475 
& \textit{name} [``\textbf{?}'' $$ ``\textbf{!}''] \\[2ex] 
27063  476 

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

478 

479 
\textit{fixes} & ::= 

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

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

482 
\textit{mixfix} ] \\ 

483 
\begin{comment} 

484 
\textit{constrains} & ::= 

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

486 
\end{comment} 

487 
\textit{assumes} & ::= 

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

489 
\begin{comment} 

490 
\textit{defines} & ::= 

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

492 
\textit{notes} & ::= 

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

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

495 
\end{comment} 

496 

497 
\textit{element} & ::= 

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

499 
\begin{comment} 

500 
&  

501 
& \textbf{constrains} \textit{constrains} 

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

503 
\end{comment} 

504 
&  

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

506 
%\begin{comment} 

507 
% &  

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

509 
% &  

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

511 
%\end{comment} 

512 

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

514 

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

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

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

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

518 
& \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

519 
( \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

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

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

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

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

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

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

528 

529 
\textit{locale} & ::= 

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

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

531 
&  & \textit{expression} [ ``\textbf{+}'' \textit{element}$^+$ ] \\ 
27063  532 
\textit{toplevel} & ::= 
533 
& \textbf{locale} \textit{name} [ ``\textbf{=}'' 

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

535 

536 
\multicolumn{3}{l}{Interpretation} \\ 

537 

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

539 
\textit{prop} \\ 

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

540 
\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

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

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

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

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

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

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

550 
\textit{expression} \textit{proof} \\[2ex] 
27063  551 

552 
\multicolumn{3}{l}{Diagnostics} \\ 

553 

554 
\textit{toplevel} & ::= 

555 
& \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\ 

556 
&  & \textbf{print\_locales} 

557 
\end{tabular} 

558 
\end{center} 

559 
\hrule 

30826  560 
\caption{Syntax of Locale Commands.} 
27063  561 
\label{tab:commands} 
562 
\end{table} 

563 
*} 

564 

565 
text {* \textbf{Acknowledgements.} Alexander Krauss, Tobias Nipkow, 

566 
Christian Sternagel and Makarius Wenzel have made useful comments on 

567 
a draft of this document. *} 

568 

569 
end 