author | wenzelm |
Sat, 05 Jan 2019 17:24:33 +0100 | |
changeset 69597 | ff784d5a5bfb |
parent 69505 | cc2d676d5395 |
child 76987 | 4c275405faae |
permissions | -rw-r--r-- |
27063 | 1 |
theory Examples |
32981 | 2 |
imports Main |
27063 | 3 |
begin |
4 |
||
5 |
(* |
|
6 |
text {* The following presentation will use notation of |
|
7 |
Isabelle's meta logic, hence a few sentences to explain this. |
|
8 |
The logical |
|
9 |
primitives are universal quantification (@{text "\<And>"}), entailment |
|
10 |
(@{text "\<Longrightarrow>"}) and equality (@{text "\<equiv>"}). Variables (not bound |
|
11 |
variables) are sometimes preceded by a question mark. The logic is |
|
32983 | 12 |
typed. Type variables are denoted by~@{text "'a"},~@{text "'b"} |
13 |
etc., and~@{text "\<Rightarrow>"} is the function type. Double brackets~@{text |
|
14 |
"\<lbrakk>"} and~@{text "\<rbrakk>"} are used to abbreviate nested entailment. |
|
27063 | 15 |
*} |
16 |
*) |
|
17 |
||
61419 | 18 |
section \<open>Introduction\<close> |
27063 | 19 |
|
61419 | 20 |
text \<open> |
27063 | 21 |
Locales are based on contexts. A \emph{context} can be seen as a |
22 |
formula schema |
|
23 |
\[ |
|
69505 | 24 |
\<open>\<And>x\<^sub>1\<dots>x\<^sub>n. \<lbrakk> A\<^sub>1; \<dots> ;A\<^sub>m \<rbrakk> \<Longrightarrow> \<dots>\<close> |
27063 | 25 |
\] |
69505 | 26 |
where the variables~\<open>x\<^sub>1\<close>, \ldots,~\<open>x\<^sub>n\<close> are called |
27 |
\emph{parameters} and the premises $\<open>A\<^sub>1\<close>, \ldots,~\<open>A\<^sub>m\<close>$ \emph{assumptions}. A formula~\<open>C\<close> |
|
27063 | 28 |
is a \emph{theorem} in the context if it is a conclusion |
29 |
\[ |
|
69505 | 30 |
\<open>\<And>x\<^sub>1\<dots>x\<^sub>n. \<lbrakk> A\<^sub>1; \<dots> ;A\<^sub>m \<rbrakk> \<Longrightarrow> C\<close>. |
27063 | 31 |
\] |
32 |
Isabelle/Isar's notion of context goes beyond this logical view. |
|
33 |
Its contexts record, in a consecutive order, proved |
|
32983 | 34 |
conclusions along with \emph{attributes}, which can provide context |
35 |
specific configuration information for proof procedures and concrete |
|
36 |
syntax. From a logical perspective, locales are just contexts that |
|
37 |
have been made persistent. To the user, though, they provide |
|
38 |
powerful means for declaring and combining contexts, and for the |
|
39 |
reuse of theorems proved in these contexts. |
|
61419 | 40 |
\<close> |
27063 | 41 |
|
61419 | 42 |
section \<open>Simple Locales\<close> |
27063 | 43 |
|
61419 | 44 |
text \<open> |
32983 | 45 |
In its simplest form, a |
27063 | 46 |
\emph{locale declaration} consists of a sequence of context elements |
47 |
declaring parameters (keyword \isakeyword{fixes}) and assumptions |
|
48 |
(keyword \isakeyword{assumes}). The following is the specification of |
|
69505 | 49 |
partial orders, as locale \<open>partial_order\<close>. |
61419 | 50 |
\<close> |
27063 | 51 |
|
52 |
locale partial_order = |
|
53 |
fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50) |
|
54 |
assumes refl [intro, simp]: "x \<sqsubseteq> x" |
|
55 |
and anti_sym [intro]: "\<lbrakk> x \<sqsubseteq> y; y \<sqsubseteq> x \<rbrakk> \<Longrightarrow> x = y" |
|
56 |
and trans [trans]: "\<lbrakk> x \<sqsubseteq> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z" |
|
57 |
||
69505 | 58 |
text (in partial_order) \<open>The parameter of this locale is~\<open>le\<close>, |
59 |
which is a binary predicate with infix syntax~\<open>\<sqsubseteq>\<close>. The |
|
32983 | 60 |
parameter syntax is available in the subsequent |
61 |
assumptions, which are the familiar partial order axioms. |
|
32981 | 62 |
|
32983 | 63 |
Isabelle recognises unbound names as free variables. In locale |
32981 | 64 |
assumptions, these are implicitly universally quantified. That is, |
69597 | 65 |
\<^term>\<open>\<lbrakk> x \<sqsubseteq> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z\<close> in fact means |
66 |
\<^term>\<open>\<And>x y z. \<lbrakk> x \<sqsubseteq> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z\<close>. |
|
27063 | 67 |
|
32981 | 68 |
Two commands are provided to inspect locales: |
69 |
\isakeyword{print\_locales} lists the names of all locales of the |
|
70 |
current theory; \isakeyword{print\_locale}~$n$ prints the parameters |
|
32983 | 71 |
and assumptions of locale $n$; the variation \isakeyword{print\_locale!}~$n$ |
72 |
additionally outputs the conclusions that are stored in the locale. |
|
73 |
We may inspect the new locale |
|
69597 | 74 |
by issuing \isakeyword{print\_locale!} \<^term>\<open>partial_order\<close>. The output |
32981 | 75 |
is the following list of context elements. |
32983 | 76 |
\begin{small} |
32981 | 77 |
\begin{alltt} |
78 |
\isakeyword{fixes} le :: "'a \(\Rightarrow\) 'a \(\Rightarrow\) bool" (\isakeyword{infixl} "\(\sqsubseteq\)" 50) |
|
67398 | 79 |
\isakeyword{assumes} "partial_order (\(\sqsubseteq\))" |
32981 | 80 |
\isakeyword{notes} assumption |
81 |
refl [intro, simp] = `?x \(\sqsubseteq\) ?x` |
|
82 |
\isakeyword{and} |
|
83 |
anti_sym [intro] = `\(\isasymlbrakk\)?x \(\sqsubseteq\) ?y; ?y \(\sqsubseteq\) ?x\(\isasymrbrakk\) \(\Longrightarrow\) ?x = ?y` |
|
84 |
\isakeyword{and} |
|
85 |
trans [trans] = `\(\isasymlbrakk\)?x \(\sqsubseteq\) ?y; ?y \(\sqsubseteq\) ?z\(\isasymrbrakk\) \(\Longrightarrow\) ?x \(\sqsubseteq\) ?z` |
|
86 |
\end{alltt} |
|
32983 | 87 |
\end{small} |
51799
8fcf6e32544e
Clarified confusing sentence in locales tutorial.
ballarin
parents:
48985
diff
changeset
|
88 |
|
8fcf6e32544e
Clarified confusing sentence in locales tutorial.
ballarin
parents:
48985
diff
changeset
|
89 |
This differs from the declaration. The assumptions have turned into |
8fcf6e32544e
Clarified confusing sentence in locales tutorial.
ballarin
parents:
48985
diff
changeset
|
90 |
conclusions, denoted by the keyword \isakeyword{notes}. Also, |
69597 | 91 |
there is only one assumption, namely \<^term>\<open>partial_order le\<close>. |
92 |
The locale declaration has introduced the predicate \<^term>\<open>partial_order\<close> to the theory. This predicate is the |
|
32983 | 93 |
\emph{locale predicate}. Its definition may be inspected by |
94 |
issuing \isakeyword{thm} @{thm [source] partial_order_def}. |
|
27063 | 95 |
@{thm [display, indent=2] partial_order_def} |
32983 | 96 |
In our example, this is a unary predicate over the parameter of the |
97 |
locale. It is equivalent to the original assumptions, which have |
|
98 |
been turned into conclusions and are |
|
32981 | 99 |
available as theorems in the context of the locale. The names and |
100 |
attributes from the locale declaration are associated to these |
|
101 |
theorems and are effective in the context of the locale. |
|
27063 | 102 |
|
32983 | 103 |
Each conclusion has a \emph{foundational theorem} as counterpart |
104 |
in the theory. Technically, this is simply the theorem composed |
|
105 |
of context and conclusion. For the transitivity theorem, this is |
|
106 |
@{thm [source] partial_order.trans}: |
|
37206 | 107 |
@{thm [display, indent=2] partial_order.trans} |
61419 | 108 |
\<close> |
32981 | 109 |
|
61419 | 110 |
subsection \<open>Targets: Extending Locales\<close> |
32981 | 111 |
|
61419 | 112 |
text \<open> |
27063 | 113 |
The specification of a locale is fixed, but its list of conclusions |
114 |
may be extended through Isar commands that take a \emph{target} argument. |
|
115 |
In the following, \isakeyword{definition} and |
|
116 |
\isakeyword{theorem} are illustrated. |
|
117 |
Table~\ref{tab:commands-with-target} lists Isar commands that accept |
|
32983 | 118 |
a target. Isar provides various ways of specifying the target. A |
27063 | 119 |
target for a single command may be indicated with keyword |
120 |
\isakeyword{in} in the following way: |
|
121 |
||
122 |
\begin{table} |
|
123 |
\hrule |
|
124 |
\vspace{2ex} |
|
125 |
\begin{center} |
|
126 |
\begin{tabular}{ll} |
|
127 |
\isakeyword{definition} & definition through an equation \\ |
|
128 |
\isakeyword{inductive} & inductive definition \\ |
|
30826 | 129 |
\isakeyword{primrec} & primitive recursion \\ |
130 |
\isakeyword{fun}, \isakeyword{function} & general recursion \\ |
|
27063 | 131 |
\isakeyword{abbreviation} & syntactic abbreviation \\ |
132 |
\isakeyword{theorem}, etc.\ & theorem statement with proof \\ |
|
30826 | 133 |
\isakeyword{theorems}, etc.\ & redeclaration of theorems \\ |
134 |
\isakeyword{text}, etc.\ & document markup |
|
27063 | 135 |
\end{tabular} |
136 |
\end{center} |
|
137 |
\hrule |
|
138 |
\caption{Isar commands that accept a target.} |
|
139 |
\label{tab:commands-with-target} |
|
140 |
\end{table} |
|
61419 | 141 |
\<close> |
27063 | 142 |
|
143 |
definition (in partial_order) |
|
144 |
less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubset>" 50) |
|
145 |
where "(x \<sqsubset> y) = (x \<sqsubseteq> y \<and> x \<noteq> y)" |
|
146 |
||
69505 | 147 |
text (in partial_order) \<open>The strict order \<open>less\<close> with infix |
148 |
syntax~\<open>\<sqsubset>\<close> is |
|
149 |
defined in terms of the locale parameter~\<open>le\<close> and the general |
|
32983 | 150 |
equality of the object logic we work in. The definition generates a |
151 |
\emph{foundational constant} |
|
69597 | 152 |
\<^term>\<open>partial_order.less\<close> with definition @{thm [source] |
32981 | 153 |
partial_order.less_def}: |
27063 | 154 |
@{thm [display, indent=2] partial_order.less_def} |
30826 | 155 |
At the same time, the locale is extended by syntax transformations |
32983 | 156 |
hiding this construction in the context of the locale. Here, the |
69505 | 157 |
abbreviation \<open>less\<close> is available for |
158 |
\<open>partial_order.less le\<close>, and it is printed |
|
159 |
and parsed as infix~\<open>\<sqsubset>\<close>. Finally, the conclusion @{thm [source] |
|
32981 | 160 |
less_def} is added to the locale: |
161 |
@{thm [display, indent=2] less_def} |
|
61419 | 162 |
\<close> |
30393
aa6f42252bf6
replaced old locale option by proper "text (in locale)";
wenzelm
parents:
29567
diff
changeset
|
163 |
|
61419 | 164 |
text \<open>The treatment of theorem statements is more straightforward. |
32981 | 165 |
As an example, here is the derivation of a transitivity law for the |
61419 | 166 |
strict order relation.\<close> |
27063 | 167 |
|
168 |
lemma (in partial_order) less_le_trans [trans]: |
|
169 |
"\<lbrakk> x \<sqsubset> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubset> z" |
|
170 |
unfolding %visible less_def by %visible (blast intro: trans) |
|
171 |
||
61419 | 172 |
text \<open>In the context of the proof, conclusions of the |
69505 | 173 |
locale may be used like theorems. Attributes are effective: \<open>anti_sym\<close> was |
27063 | 174 |
declared as introduction rule, hence it is in the context's set of |
61419 | 175 |
rules used by the classical reasoner by default.\<close> |
27063 | 176 |
|
61419 | 177 |
subsection \<open>Context Blocks\<close> |
32981 | 178 |
|
61419 | 179 |
text \<open>When working with locales, sequences of commands with the same |
27063 | 180 |
target are frequent. A block of commands, delimited by |
181 |
\isakeyword{begin} and \isakeyword{end}, makes a theory-like style |
|
182 |
of working possible. All commands inside the block refer to the |
|
183 |
same target. A block may immediately follow a locale |
|
184 |
declaration, which makes that locale the target. Alternatively the |
|
185 |
target for a block may be given with the \isakeyword{context} |
|
186 |
command. |
|
187 |
||
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
188 |
This style of working is illustrated in the block below, where |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
189 |
notions of infimum and supremum for partial orders are introduced, |
61419 | 190 |
together with theorems about their uniqueness.\<close> |
27063 | 191 |
|
46855 | 192 |
context partial_order |
193 |
begin |
|
27063 | 194 |
|
195 |
definition |
|
196 |
is_inf where "is_inf x y i = |
|
197 |
(i \<sqsubseteq> x \<and> i \<sqsubseteq> y \<and> (\<forall>z. z \<sqsubseteq> x \<and> z \<sqsubseteq> y \<longrightarrow> z \<sqsubseteq> i))" |
|
198 |
||
199 |
definition |
|
200 |
is_sup where "is_sup x y s = |
|
201 |
(x \<sqsubseteq> s \<and> y \<sqsubseteq> s \<and> (\<forall>z. x \<sqsubseteq> z \<and> y \<sqsubseteq> z \<longrightarrow> s \<sqsubseteq> z))" |
|
202 |
||
203 |
lemma %invisible is_infI [intro?]: "i \<sqsubseteq> x \<Longrightarrow> i \<sqsubseteq> y \<Longrightarrow> |
|
204 |
(\<And>z. z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> i) \<Longrightarrow> is_inf x y i" |
|
205 |
by (unfold is_inf_def) blast |
|
206 |
||
207 |
lemma %invisible is_inf_lower [elim?]: |
|
208 |
"is_inf x y i \<Longrightarrow> (i \<sqsubseteq> x \<Longrightarrow> i \<sqsubseteq> y \<Longrightarrow> C) \<Longrightarrow> C" |
|
209 |
by (unfold is_inf_def) blast |
|
210 |
||
211 |
lemma %invisible is_inf_greatest [elim?]: |
|
212 |
"is_inf x y i \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> i" |
|
213 |
by (unfold is_inf_def) blast |
|
214 |
||
215 |
theorem is_inf_uniq: "\<lbrakk>is_inf x y i; is_inf x y i'\<rbrakk> \<Longrightarrow> i = i'" |
|
32983 | 216 |
proof - |
27063 | 217 |
assume inf: "is_inf x y i" |
218 |
assume inf': "is_inf x y i'" |
|
219 |
show ?thesis |
|
220 |
proof (rule anti_sym) |
|
221 |
from inf' show "i \<sqsubseteq> i'" |
|
222 |
proof (rule is_inf_greatest) |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
223 |
from inf show "i \<sqsubseteq> x" .. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
224 |
from inf show "i \<sqsubseteq> y" .. |
27063 | 225 |
qed |
226 |
from inf show "i' \<sqsubseteq> i" |
|
227 |
proof (rule is_inf_greatest) |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
228 |
from inf' show "i' \<sqsubseteq> x" .. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
229 |
from inf' show "i' \<sqsubseteq> y" .. |
27063 | 230 |
qed |
231 |
qed |
|
232 |
qed |
|
233 |
||
234 |
theorem %invisible is_inf_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_inf x y x" |
|
235 |
proof - |
|
236 |
assume "x \<sqsubseteq> y" |
|
237 |
show ?thesis |
|
238 |
proof |
|
239 |
show "x \<sqsubseteq> x" .. |
|
240 |
show "x \<sqsubseteq> y" by fact |
|
241 |
fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" by fact |
|
242 |
qed |
|
243 |
qed |
|
244 |
||
245 |
lemma %invisible is_supI [intro?]: "x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow> |
|
246 |
(\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z) \<Longrightarrow> is_sup x y s" |
|
247 |
by (unfold is_sup_def) blast |
|
248 |
||
249 |
lemma %invisible is_sup_least [elim?]: |
|
250 |
"is_sup x y s \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z" |
|
251 |
by (unfold is_sup_def) blast |
|
252 |
||
253 |
lemma %invisible is_sup_upper [elim?]: |
|
254 |
"is_sup x y s \<Longrightarrow> (x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow> C) \<Longrightarrow> C" |
|
255 |
by (unfold is_sup_def) blast |
|
256 |
||
257 |
theorem is_sup_uniq: "\<lbrakk>is_sup x y s; is_sup x y s'\<rbrakk> \<Longrightarrow> s = s'" |
|
32983 | 258 |
proof - |
27063 | 259 |
assume sup: "is_sup x y s" |
260 |
assume sup': "is_sup x y s'" |
|
261 |
show ?thesis |
|
262 |
proof (rule anti_sym) |
|
263 |
from sup show "s \<sqsubseteq> s'" |
|
264 |
proof (rule is_sup_least) |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
265 |
from sup' show "x \<sqsubseteq> s'" .. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
266 |
from sup' show "y \<sqsubseteq> s'" .. |
27063 | 267 |
qed |
268 |
from sup' show "s' \<sqsubseteq> s" |
|
269 |
proof (rule is_sup_least) |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
270 |
from sup show "x \<sqsubseteq> s" .. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
271 |
from sup show "y \<sqsubseteq> s" .. |
27063 | 272 |
qed |
273 |
qed |
|
274 |
qed |
|
275 |
||
276 |
theorem %invisible is_sup_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_sup x y y" |
|
277 |
proof - |
|
278 |
assume "x \<sqsubseteq> y" |
|
279 |
show ?thesis |
|
280 |
proof |
|
281 |
show "x \<sqsubseteq> y" by fact |
|
282 |
show "y \<sqsubseteq> y" .. |
|
283 |
fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z" |
|
284 |
show "y \<sqsubseteq> z" by fact |
|
285 |
qed |
|
286 |
qed |
|
287 |
||
288 |
end |
|
289 |
||
61419 | 290 |
text \<open>The syntax of the locale commands discussed in this tutorial is |
32983 | 291 |
shown in Table~\ref{tab:commands}. The grammar is complete with the |
292 |
exception of the context elements \isakeyword{constrains} and |
|
293 |
\isakeyword{defines}, which are provided for backward |
|
294 |
compatibility. See the Isabelle/Isar Reference |
|
61419 | 295 |
Manual @{cite IsarRef} for full documentation.\<close> |
27063 | 296 |
|
297 |
||
61419 | 298 |
section \<open>Import \label{sec:import}\<close> |
27063 | 299 |
|
61419 | 300 |
text \<open> |
27063 | 301 |
Algebraic structures are commonly defined by adding operations and |
302 |
properties to existing structures. For example, partial orders |
|
303 |
are extended to lattices and total orders. Lattices are extended to |
|
61419 | 304 |
distributive lattices.\<close> |
27063 | 305 |
|
61419 | 306 |
text \<open> |
32981 | 307 |
With locales, this kind of inheritance is achieved through |
308 |
\emph{import} of locales. The import part of a locale declaration, |
|
309 |
if present, precedes the context elements. Here is an example, |
|
310 |
where partial orders are extended to lattices. |
|
61419 | 311 |
\<close> |
27063 | 312 |
|
313 |
locale lattice = partial_order + |
|
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
314 |
assumes ex_inf: "\<exists>inf. is_inf x y inf" |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
315 |
and ex_sup: "\<exists>sup. is_sup x y sup" |
27063 | 316 |
begin |
317 |
||
61419 | 318 |
text \<open>These assumptions refer to the predicates for infimum |
69505 | 319 |
and supremum defined for \<open>partial_order\<close> in the previous |
63724 | 320 |
section. We now introduce the notions of meet and join, |
321 |
together with an example theorem.\<close> |
|
27063 | 322 |
|
323 |
definition |
|
324 |
meet (infixl "\<sqinter>" 70) where "x \<sqinter> y = (THE inf. is_inf x y inf)" |
|
325 |
definition |
|
326 |
join (infixl "\<squnion>" 65) where "x \<squnion> y = (THE sup. is_sup x y sup)" |
|
327 |
||
328 |
lemma %invisible meet_equality [elim?]: "is_inf x y i \<Longrightarrow> x \<sqinter> y = i" |
|
329 |
proof (unfold meet_def) |
|
330 |
assume "is_inf x y i" |
|
331 |
then show "(THE i. is_inf x y i) = i" |
|
61419 | 332 |
by (rule the_equality) (rule is_inf_uniq [OF _ \<open>is_inf x y i\<close>]) |
27063 | 333 |
qed |
334 |
||
335 |
lemma %invisible meetI [intro?]: |
|
336 |
"i \<sqsubseteq> x \<Longrightarrow> i \<sqsubseteq> y \<Longrightarrow> (\<And>z. z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> i) \<Longrightarrow> x \<sqinter> y = i" |
|
337 |
by (rule meet_equality, rule is_infI) blast+ |
|
338 |
||
339 |
lemma %invisible is_inf_meet [intro?]: "is_inf x y (x \<sqinter> y)" |
|
340 |
proof (unfold meet_def) |
|
341 |
from ex_inf obtain i where "is_inf x y i" .. |
|
342 |
then show "is_inf x y (THE i. is_inf x y i)" |
|
61419 | 343 |
by (rule theI) (rule is_inf_uniq [OF _ \<open>is_inf x y i\<close>]) |
27063 | 344 |
qed |
345 |
||
63724 | 346 |
lemma meet_left(*<*)[intro?](*>*): "x \<sqinter> y \<sqsubseteq> x" |
27063 | 347 |
by (rule is_inf_lower) (rule is_inf_meet) |
348 |
||
349 |
lemma %invisible meet_right [intro?]: |
|
350 |
"x \<sqinter> y \<sqsubseteq> y" |
|
351 |
by (rule is_inf_lower) (rule is_inf_meet) |
|
352 |
||
353 |
lemma %invisible meet_le [intro?]: |
|
354 |
"\<lbrakk> z \<sqsubseteq> x; z \<sqsubseteq> y \<rbrakk> \<Longrightarrow> z \<sqsubseteq> x \<sqinter> y" |
|
355 |
by (rule is_inf_greatest) (rule is_inf_meet) |
|
356 |
||
357 |
lemma %invisible join_equality [elim?]: "is_sup x y s \<Longrightarrow> x \<squnion> y = s" |
|
358 |
proof (unfold join_def) |
|
359 |
assume "is_sup x y s" |
|
360 |
then show "(THE s. is_sup x y s) = s" |
|
61419 | 361 |
by (rule the_equality) (rule is_sup_uniq [OF _ \<open>is_sup x y s\<close>]) |
27063 | 362 |
qed |
363 |
||
364 |
lemma %invisible joinI [intro?]: "x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow> |
|
365 |
(\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z) \<Longrightarrow> x \<squnion> y = s" |
|
366 |
by (rule join_equality, rule is_supI) blast+ |
|
367 |
||
368 |
lemma %invisible is_sup_join [intro?]: "is_sup x y (x \<squnion> y)" |
|
369 |
proof (unfold join_def) |
|
370 |
from ex_sup obtain s where "is_sup x y s" .. |
|
371 |
then show "is_sup x y (THE s. is_sup x y s)" |
|
61419 | 372 |
by (rule theI) (rule is_sup_uniq [OF _ \<open>is_sup x y s\<close>]) |
27063 | 373 |
qed |
374 |
||
375 |
lemma %invisible join_left [intro?]: |
|
376 |
"x \<sqsubseteq> x \<squnion> y" |
|
377 |
by (rule is_sup_upper) (rule is_sup_join) |
|
378 |
||
379 |
lemma %invisible join_right [intro?]: |
|
380 |
"y \<sqsubseteq> x \<squnion> y" |
|
381 |
by (rule is_sup_upper) (rule is_sup_join) |
|
382 |
||
383 |
lemma %invisible join_le [intro?]: |
|
384 |
"\<lbrakk> x \<sqsubseteq> z; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<squnion> y \<sqsubseteq> z" |
|
385 |
by (rule is_sup_least) (rule is_sup_join) |
|
386 |
||
387 |
theorem %invisible meet_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)" |
|
388 |
proof (rule meetI) |
|
389 |
show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x \<sqinter> y" |
|
390 |
proof |
|
391 |
show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x" .. |
|
392 |
show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y" |
|
393 |
proof - |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
394 |
have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" .. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
395 |
also have "\<dots> \<sqsubseteq> y" .. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
396 |
finally show ?thesis . |
27063 | 397 |
qed |
398 |
qed |
|
399 |
show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> z" |
|
400 |
proof - |
|
401 |
have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" .. |
|
402 |
also have "\<dots> \<sqsubseteq> z" .. |
|
403 |
finally show ?thesis . |
|
404 |
qed |
|
405 |
fix w assume "w \<sqsubseteq> x \<sqinter> y" and "w \<sqsubseteq> z" |
|
406 |
show "w \<sqsubseteq> x \<sqinter> (y \<sqinter> z)" |
|
407 |
proof |
|
408 |
show "w \<sqsubseteq> x" |
|
409 |
proof - |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
410 |
have "w \<sqsubseteq> x \<sqinter> y" by fact |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
411 |
also have "\<dots> \<sqsubseteq> x" .. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
412 |
finally show ?thesis . |
27063 | 413 |
qed |
414 |
show "w \<sqsubseteq> y \<sqinter> z" |
|
415 |
proof |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
416 |
show "w \<sqsubseteq> y" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
417 |
proof - |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
418 |
have "w \<sqsubseteq> x \<sqinter> y" by fact |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
419 |
also have "\<dots> \<sqsubseteq> y" .. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
420 |
finally show ?thesis . |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
421 |
qed |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
422 |
show "w \<sqsubseteq> z" by fact |
27063 | 423 |
qed |
424 |
qed |
|
425 |
qed |
|
426 |
||
427 |
theorem %invisible meet_commute: "x \<sqinter> y = y \<sqinter> x" |
|
428 |
proof (rule meetI) |
|
429 |
show "y \<sqinter> x \<sqsubseteq> x" .. |
|
430 |
show "y \<sqinter> x \<sqsubseteq> y" .. |
|
431 |
fix z assume "z \<sqsubseteq> y" and "z \<sqsubseteq> x" |
|
432 |
then show "z \<sqsubseteq> y \<sqinter> x" .. |
|
433 |
qed |
|
434 |
||
435 |
theorem %invisible meet_join_absorb: "x \<sqinter> (x \<squnion> y) = x" |
|
436 |
proof (rule meetI) |
|
437 |
show "x \<sqsubseteq> x" .. |
|
438 |
show "x \<sqsubseteq> x \<squnion> y" .. |
|
439 |
fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> x \<squnion> y" |
|
440 |
show "z \<sqsubseteq> x" by fact |
|
441 |
qed |
|
442 |
||
443 |
theorem %invisible join_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" |
|
444 |
proof (rule joinI) |
|
445 |
show "x \<squnion> y \<sqsubseteq> x \<squnion> (y \<squnion> z)" |
|
446 |
proof |
|
447 |
show "x \<sqsubseteq> x \<squnion> (y \<squnion> z)" .. |
|
448 |
show "y \<sqsubseteq> x \<squnion> (y \<squnion> z)" |
|
449 |
proof - |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
450 |
have "y \<sqsubseteq> y \<squnion> z" .. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
451 |
also have "... \<sqsubseteq> x \<squnion> (y \<squnion> z)" .. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
452 |
finally show ?thesis . |
27063 | 453 |
qed |
454 |
qed |
|
455 |
show "z \<sqsubseteq> x \<squnion> (y \<squnion> z)" |
|
456 |
proof - |
|
457 |
have "z \<sqsubseteq> y \<squnion> z" .. |
|
458 |
also have "... \<sqsubseteq> x \<squnion> (y \<squnion> z)" .. |
|
459 |
finally show ?thesis . |
|
460 |
qed |
|
461 |
fix w assume "x \<squnion> y \<sqsubseteq> w" and "z \<sqsubseteq> w" |
|
462 |
show "x \<squnion> (y \<squnion> z) \<sqsubseteq> w" |
|
463 |
proof |
|
464 |
show "x \<sqsubseteq> w" |
|
465 |
proof - |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
466 |
have "x \<sqsubseteq> x \<squnion> y" .. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
467 |
also have "\<dots> \<sqsubseteq> w" by fact |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
468 |
finally show ?thesis . |
27063 | 469 |
qed |
470 |
show "y \<squnion> z \<sqsubseteq> w" |
|
471 |
proof |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
472 |
show "y \<sqsubseteq> w" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
473 |
proof - |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
474 |
have "y \<sqsubseteq> x \<squnion> y" .. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
475 |
also have "... \<sqsubseteq> w" by fact |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
476 |
finally show ?thesis . |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
477 |
qed |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
478 |
show "z \<sqsubseteq> w" by fact |
27063 | 479 |
qed |
480 |
qed |
|
481 |
qed |
|
482 |
||
483 |
theorem %invisible join_commute: "x \<squnion> y = y \<squnion> x" |
|
484 |
proof (rule joinI) |
|
485 |
show "x \<sqsubseteq> y \<squnion> x" .. |
|
486 |
show "y \<sqsubseteq> y \<squnion> x" .. |
|
487 |
fix z assume "y \<sqsubseteq> z" and "x \<sqsubseteq> z" |
|
488 |
then show "y \<squnion> x \<sqsubseteq> z" .. |
|
489 |
qed |
|
490 |
||
491 |
theorem %invisible join_meet_absorb: "x \<squnion> (x \<sqinter> y) = x" |
|
492 |
proof (rule joinI) |
|
493 |
show "x \<sqsubseteq> x" .. |
|
494 |
show "x \<sqinter> y \<sqsubseteq> x" .. |
|
495 |
fix z assume "x \<sqsubseteq> z" and "x \<sqinter> y \<sqsubseteq> z" |
|
496 |
show "x \<sqsubseteq> z" by fact |
|
497 |
qed |
|
498 |
||
499 |
theorem %invisible meet_idem: "x \<sqinter> x = x" |
|
500 |
proof - |
|
501 |
have "x \<sqinter> (x \<squnion> (x \<sqinter> x)) = x" by (rule meet_join_absorb) |
|
502 |
also have "x \<squnion> (x \<sqinter> x) = x" by (rule join_meet_absorb) |
|
503 |
finally show ?thesis . |
|
504 |
qed |
|
505 |
||
506 |
theorem %invisible meet_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x" |
|
507 |
proof (rule meetI) |
|
508 |
assume "x \<sqsubseteq> y" |
|
509 |
show "x \<sqsubseteq> x" .. |
|
510 |
show "x \<sqsubseteq> y" by fact |
|
511 |
fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" |
|
512 |
show "z \<sqsubseteq> x" by fact |
|
513 |
qed |
|
514 |
||
515 |
theorem %invisible meet_related2 [elim?]: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y" |
|
516 |
by (drule meet_related) (simp add: meet_commute) |
|
517 |
||
518 |
theorem %invisible join_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y" |
|
519 |
proof (rule joinI) |
|
520 |
assume "x \<sqsubseteq> y" |
|
521 |
show "y \<sqsubseteq> y" .. |
|
522 |
show "x \<sqsubseteq> y" by fact |
|
523 |
fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z" |
|
524 |
show "y \<sqsubseteq> z" by fact |
|
525 |
qed |
|
526 |
||
527 |
theorem %invisible join_related2 [elim?]: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x" |
|
528 |
by (drule join_related) (simp add: join_commute) |
|
529 |
||
530 |
theorem %invisible meet_connection: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)" |
|
531 |
proof |
|
532 |
assume "x \<sqsubseteq> y" |
|
533 |
then have "is_inf x y x" .. |
|
534 |
then show "x \<sqinter> y = x" .. |
|
535 |
next |
|
536 |
have "x \<sqinter> y \<sqsubseteq> y" .. |
|
537 |
also assume "x \<sqinter> y = x" |
|
538 |
finally show "x \<sqsubseteq> y" . |
|
539 |
qed |
|
540 |
||
541 |
theorem %invisible join_connection: "(x \<sqsubseteq> y) = (x \<squnion> y = y)" |
|
542 |
proof |
|
543 |
assume "x \<sqsubseteq> y" |
|
544 |
then have "is_sup x y y" .. |
|
545 |
then show "x \<squnion> y = y" .. |
|
546 |
next |
|
547 |
have "x \<sqsubseteq> x \<squnion> y" .. |
|
548 |
also assume "x \<squnion> y = y" |
|
549 |
finally show "x \<sqsubseteq> y" . |
|
550 |
qed |
|
551 |
||
552 |
theorem %invisible meet_connection2: "(x \<sqsubseteq> y) = (y \<sqinter> x = x)" |
|
553 |
using meet_commute meet_connection by simp |
|
554 |
||
555 |
theorem %invisible join_connection2: "(x \<sqsubseteq> y) = (x \<squnion> y = y)" |
|
556 |
using join_commute join_connection by simp |
|
557 |
||
61419 | 558 |
text %invisible \<open>Naming according to Jacobson I, p.\ 459.\<close> |
27063 | 559 |
lemmas %invisible L1 = join_commute meet_commute |
560 |
lemmas %invisible L2 = join_assoc meet_assoc |
|
561 |
(* lemmas L3 = join_idem meet_idem *) |
|
562 |
lemmas %invisible L4 = join_meet_absorb meet_join_absorb |
|
563 |
||
564 |
end |
|
565 |
||
61419 | 566 |
text \<open>Locales for total orders and distributive lattices follow to |
32983 | 567 |
establish a sufficiently rich landscape of locales for |
63724 | 568 |
further examples in this tutorial.\<close> |
27063 | 569 |
|
570 |
locale total_order = partial_order + |
|
571 |
assumes total: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x" |
|
572 |
||
573 |
lemma (in total_order) less_total: "x \<sqsubset> y \<or> x = y \<or> y \<sqsubset> x" |
|
574 |
using total |
|
575 |
by (unfold less_def) blast |
|
576 |
||
577 |
locale distrib_lattice = lattice + |
|
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
578 |
assumes meet_distr: "x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z" |
27063 | 579 |
|
580 |
lemma (in distrib_lattice) join_distr: |
|
581 |
"x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" (* txt {* Jacobson I, p.\ 462 *} *) |
|
582 |
proof - |
|
583 |
have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by (simp add: L4) |
|
584 |
also have "... = x \<squnion> ((x \<sqinter> z) \<squnion> (y \<sqinter> z))" by (simp add: L2) |
|
585 |
also have "... = x \<squnion> ((x \<squnion> y) \<sqinter> z)" by (simp add: L1 meet_distr) |
|
586 |
also have "... = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)" by (simp add: L1 L4) |
|
587 |
also have "... = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by (simp add: meet_distr) |
|
588 |
finally show ?thesis . |
|
589 |
qed |
|
590 |
||
61419 | 591 |
text \<open> |
32983 | 592 |
The locale hierarchy obtained through these declarations is shown in |
32981 | 593 |
Figure~\ref{fig:lattices}(a). |
27063 | 594 |
|
595 |
\begin{figure} |
|
596 |
\hrule \vspace{2ex} |
|
597 |
\begin{center} |
|
32983 | 598 |
\subfigure[Declared hierarchy]{ |
27063 | 599 |
\begin{tikzpicture} |
69505 | 600 |
\node (po) at (0,0) {\<open>partial_order\<close>}; |
601 |
\node (lat) at (-1.5,-1) {\<open>lattice\<close>}; |
|
602 |
\node (dlat) at (-1.5,-2) {\<open>distrib_lattice\<close>}; |
|
603 |
\node (to) at (1.5,-1) {\<open>total_order\<close>}; |
|
27063 | 604 |
\draw (po) -- (lat); |
605 |
\draw (lat) -- (dlat); |
|
606 |
\draw (po) -- (to); |
|
607 |
% \draw[->, dashed] (lat) -- (to); |
|
608 |
\end{tikzpicture} |
|
609 |
} \\ |
|
610 |
\subfigure[Total orders are lattices]{ |
|
611 |
\begin{tikzpicture} |
|
69505 | 612 |
\node (po) at (0,0) {\<open>partial_order\<close>}; |
613 |
\node (lat) at (0,-1) {\<open>lattice\<close>}; |
|
614 |
\node (dlat) at (-1.5,-2) {\<open>distrib_lattice\<close>}; |
|
615 |
\node (to) at (1.5,-2) {\<open>total_order\<close>}; |
|
27063 | 616 |
\draw (po) -- (lat); |
617 |
\draw (lat) -- (dlat); |
|
618 |
\draw (lat) -- (to); |
|
619 |
% \draw[->, dashed] (dlat) -- (to); |
|
620 |
\end{tikzpicture} |
|
621 |
} \quad |
|
622 |
\subfigure[Total orders are distributive lattices]{ |
|
623 |
\begin{tikzpicture} |
|
69505 | 624 |
\node (po) at (0,0) {\<open>partial_order\<close>}; |
625 |
\node (lat) at (0,-1) {\<open>lattice\<close>}; |
|
626 |
\node (dlat) at (0,-2) {\<open>distrib_lattice\<close>}; |
|
627 |
\node (to) at (0,-3) {\<open>total_order\<close>}; |
|
27063 | 628 |
\draw (po) -- (lat); |
629 |
\draw (lat) -- (dlat); |
|
630 |
\draw (dlat) -- (to); |
|
631 |
\end{tikzpicture} |
|
632 |
} |
|
633 |
\end{center} |
|
634 |
\hrule |
|
635 |
\caption{Hierarchy of Lattice Locales.} |
|
636 |
\label{fig:lattices} |
|
637 |
\end{figure} |
|
61419 | 638 |
\<close> |
27063 | 639 |
|
61419 | 640 |
section \<open>Changing the Locale Hierarchy |
641 |
\label{sec:changing-the-hierarchy}\<close> |
|
27063 | 642 |
|
61419 | 643 |
text \<open> |
32981 | 644 |
Locales enable to prove theorems abstractly, relative to |
645 |
sets of assumptions. These theorems can then be used in other |
|
646 |
contexts where the assumptions themselves, or |
|
647 |
instances of the assumptions, are theorems. This form of theorem |
|
648 |
reuse is called \emph{interpretation}. Locales generalise |
|
649 |
interpretation from theorems to conclusions, enabling the reuse of |
|
650 |
definitions and other constructs that are not part of the |
|
651 |
specifications of the locales. |
|
652 |
||
37094 | 653 |
The first form of interpretation we will consider in this tutorial |
32983 | 654 |
is provided by the \isakeyword{sublocale} command. It enables to |
32981 | 655 |
modify the import hierarchy to reflect the \emph{logical} relation |
656 |
between locales. |
|
657 |
||
658 |
Consider the locale hierarchy from Figure~\ref{fig:lattices}(a). |
|
32983 | 659 |
Total orders are lattices, although this is not reflected here, and |
660 |
definitions, theorems and other conclusions |
|
69597 | 661 |
from \<^term>\<open>lattice\<close> are not available in \<^term>\<open>total_order\<close>. To |
32981 | 662 |
obtain the situation in Figure~\ref{fig:lattices}(b), it is |
663 |
sufficient to add the conclusions of the latter locale to the former. |
|
664 |
The \isakeyword{sublocale} command does exactly this. |
|
665 |
The declaration \isakeyword{sublocale} $l_1 |
|
666 |
\subseteq l_2$ causes locale $l_2$ to be \emph{interpreted} in the |
|
32983 | 667 |
context of $l_1$. This means that all conclusions of $l_2$ are made |
32981 | 668 |
available in $l_1$. |
669 |
||
670 |
Of course, the change of hierarchy must be supported by a theorem |
|
671 |
that reflects, in our example, that total orders are indeed |
|
672 |
lattices. Therefore the \isakeyword{sublocale} command generates a |
|
673 |
goal, which must be discharged by the user. This is illustrated in |
|
674 |
the following paragraphs. First the sublocale relation is stated. |
|
61419 | 675 |
\<close> |
27063 | 676 |
|
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27375
diff
changeset
|
677 |
sublocale %visible total_order \<subseteq> lattice |
27063 | 678 |
|
61419 | 679 |
txt \<open>\normalsize |
69505 | 680 |
This enters the context of locale \<open>total_order\<close>, in |
32981 | 681 |
which the goal @{subgoals [display]} must be shown. |
682 |
Now the |
|
683 |
locale predicate needs to be unfolded --- for example, using its |
|
27063 | 684 |
definition or by introduction rules |
32983 | 685 |
provided by the locale package. For automation, the locale package |
69505 | 686 |
provides the methods \<open>intro_locales\<close> and \<open>unfold_locales\<close>. They are aware of the |
27063 | 687 |
current context and dependencies between locales and automatically |
69505 | 688 |
discharge goals implied by these. While \<open>unfold_locales\<close> |
689 |
always unfolds locale predicates to assumptions, \<open>intro_locales\<close> only unfolds definitions along the locale |
|
27063 | 690 |
hierarchy, leaving a goal consisting of predicates defined by the |
691 |
locale package. Occasionally the latter is of advantage since the goal |
|
692 |
is smaller. |
|
693 |
||
694 |
For the current goal, we would like to get hold of |
|
69505 | 695 |
the assumptions of \<open>lattice\<close>, which need to be shown, hence |
696 |
\<open>unfold_locales\<close> is appropriate.\<close> |
|
27063 | 697 |
|
698 |
proof unfold_locales |
|
699 |
||
61419 | 700 |
txt \<open>\normalsize |
32981 | 701 |
Since the fact that both lattices and total orders are partial |
702 |
orders is already reflected in the locale hierarchy, the assumptions |
|
69505 | 703 |
of \<open>partial_order\<close> are discharged automatically, and only the |
704 |
assumptions introduced in \<open>lattice\<close> remain as subgoals |
|
32981 | 705 |
@{subgoals [display]} |
706 |
The proof for the first subgoal is obtained by constructing an |
|
61419 | 707 |
infimum, whose existence is implied by totality.\<close> |
27063 | 708 |
|
709 |
fix x y |
|
710 |
from total have "is_inf x y (if x \<sqsubseteq> y then x else y)" |
|
711 |
by (auto simp: is_inf_def) |
|
712 |
then show "\<exists>inf. is_inf x y inf" .. |
|
61419 | 713 |
txt \<open>\normalsize |
32981 | 714 |
The proof for the second subgoal is analogous and not |
61419 | 715 |
reproduced here.\<close> |
27063 | 716 |
next %invisible |
717 |
fix x y |
|
718 |
from total have "is_sup x y (if x \<sqsubseteq> y then y else x)" |
|
719 |
by (auto simp: is_sup_def) |
|
720 |
then show "\<exists>sup. is_sup x y sup" .. qed %visible |
|
721 |
||
61419 | 722 |
text \<open>Similarly, we may establish that total orders are distributive |
723 |
lattices with a second \isakeyword{sublocale} statement.\<close> |
|
27063 | 724 |
|
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27375
diff
changeset
|
725 |
sublocale total_order \<subseteq> distrib_lattice |
32983 | 726 |
proof unfold_locales |
27063 | 727 |
fix %"proof" x y z |
728 |
show "x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z" (is "?l = ?r") |
|
61419 | 729 |
txt \<open>Jacobson I, p.\ 462\<close> |
27063 | 730 |
proof - |
731 |
{ assume c: "y \<sqsubseteq> x" "z \<sqsubseteq> x" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
732 |
from c have "?l = y \<squnion> z" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
733 |
by (metis c join_connection2 join_related2 meet_related2 total) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
734 |
also from c have "... = ?r" by (metis meet_related2) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
735 |
finally have "?l = ?r" . } |
27063 | 736 |
moreover |
737 |
{ assume c: "x \<sqsubseteq> y \<or> x \<sqsubseteq> z" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
738 |
from c have "?l = x" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
739 |
by (metis join_connection2 join_related2 meet_connection total trans) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
740 |
also from c have "... = ?r" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
741 |
by (metis join_commute join_related2 meet_connection meet_related2 total) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30826
diff
changeset
|
742 |
finally have "?l = ?r" . } |
27063 | 743 |
moreover note total |
744 |
ultimately show ?thesis by blast |
|
745 |
qed |
|
746 |
qed |
|
747 |
||
61419 | 748 |
text \<open>The locale hierarchy is now as shown in |
749 |
Figure~\ref{fig:lattices}(c).\<close> |
|
32981 | 750 |
|
61419 | 751 |
text \<open> |
32981 | 752 |
Locale interpretation is \emph{dynamic}. The statement |
753 |
\isakeyword{sublocale} $l_1 \subseteq l_2$ will not just add the |
|
754 |
current conclusions of $l_2$ to $l_1$. Rather the dependency is |
|
755 |
stored, and conclusions that will be |
|
756 |
added to $l_2$ in future are automatically propagated to $l_1$. |
|
757 |
The sublocale relation is transitive --- that is, propagation takes |
|
758 |
effect along chains of sublocales. Even cycles in the sublocale relation are |
|
759 |
supported, as long as these cycles do not lead to infinite chains. |
|
58620 | 760 |
Details are discussed in the technical report @{cite Ballarin2006a}. |
61419 | 761 |
See also Section~\ref{sec:infinite-chains} of this tutorial.\<close> |
27063 | 762 |
|
763 |
end |