Finished revisions of locales tutorial.
--- a/NEWS Thu Oct 15 22:22:08 2009 +0200
+++ b/NEWS Sat Oct 17 22:58:18 2009 +0200
@@ -23,6 +23,9 @@
to print all interpretations of locale l in the theory. Interpretations
in proofs are not shown.
+* Thoroughly revised locales tutorial. New section on conditional
+interpretation.
+
*** HOL ***
--- a/doc-src/Locales/Locales/Examples.thy Thu Oct 15 22:22:08 2009 +0200
+++ b/doc-src/Locales/Locales/Examples.thy Sat Oct 17 22:58:18 2009 +0200
@@ -12,9 +12,9 @@
primitives are universal quantification (@{text "\<And>"}), entailment
(@{text "\<Longrightarrow>"}) and equality (@{text "\<equiv>"}). Variables (not bound
variables) are sometimes preceded by a question mark. The logic is
- typed. Type variables are denoted by @{text "'a"}, @{text "'b"}
- etc., and @{text "\<Rightarrow>"} is the function type. Double brackets @{text
- "\<lbrakk>"} and @{text "\<rbrakk>"} are used to abbreviate nested entailment.
+ typed. Type variables are denoted by~@{text "'a"},~@{text "'b"}
+ etc., and~@{text "\<Rightarrow>"} is the function type. Double brackets~@{text
+ "\<lbrakk>"} and~@{text "\<rbrakk>"} are used to abbreviate nested entailment.
*}
*)
@@ -26,25 +26,27 @@
\[
@{text "\<And>x\<^sub>1\<dots>x\<^sub>n. \<lbrakk> A\<^sub>1; \<dots> ;A\<^sub>m \<rbrakk> \<Longrightarrow> \<dots>"}
\]
- where variables @{text "x\<^sub>1"}, \ldots, @{text "x\<^sub>n"} are called
- \emph{parameters} and the premises $@{text "A\<^sub>1"}, \ldots,
- @{text "A\<^sub>m"}$ \emph{assumptions}. A formula @{text "C"}
+ where variables~@{text "x\<^sub>1"}, \ldots,~@{text "x\<^sub>n"} are called
+ \emph{parameters} and the premises $@{text "A\<^sub>1"}, \ldots,~@{text
+ "A\<^sub>m"}$ \emph{assumptions}. A formula~@{text "C"}
is a \emph{theorem} in the context if it is a conclusion
\[
-%\label{eq-fact-in-context}
@{text "\<And>x\<^sub>1\<dots>x\<^sub>n. \<lbrakk> A\<^sub>1; \<dots> ;A\<^sub>m \<rbrakk> \<Longrightarrow> C"}.
\]
Isabelle/Isar's notion of context goes beyond this logical view.
Its contexts record, in a consecutive order, proved
- conclusions along with attributes, which
- may control proof procedures. Contexts also contain syntax information
- for parameters and for terms depending on them.
+ conclusions along with \emph{attributes}, which can provide context
+ specific configuration information for proof procedures and concrete
+ syntax. From a logical perspective, locales are just contexts that
+ have been made persistent. To the user, though, they provide
+ powerful means for declaring and combining contexts, and for the
+ reuse of theorems proved in these contexts.
*}
section {* Simple Locales *}
text {*
- Locales can be seen as persistent contexts. In its simplest form, a
+ In its simplest form, a
\emph{locale declaration} consists of a sequence of context elements
declaring parameters (keyword \isakeyword{fixes}) and assumptions
(keyword \isakeyword{assumes}). The following is the specification of
@@ -57,24 +59,25 @@
and anti_sym [intro]: "\<lbrakk> x \<sqsubseteq> y; y \<sqsubseteq> x \<rbrakk> \<Longrightarrow> x = y"
and trans [trans]: "\<lbrakk> x \<sqsubseteq> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
-text (in partial_order) {* The parameter of this locale is @{text le},
- which is a binary predicate with infix syntax
- @{text \<sqsubseteq>}. The parameter syntax is available in the subsequent
- assumptions, which ar the normal partial order axioms.
+text (in partial_order) {* The parameter of this locale is~@{text le},
+ which is a binary predicate with infix syntax~@{text \<sqsubseteq>}. The
+ parameter syntax is available in the subsequent
+ assumptions, which are the familiar partial order axioms.
- Isabelle recognises undbound names as free variables. In locale
+ Isabelle recognises unbound names as free variables. In locale
assumptions, these are implicitly universally quantified. That is,
- it is sufficient to write @{term "\<lbrakk> x \<sqsubseteq> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"} rather
- than @{term "\<And>x y z. \<lbrakk> x \<sqsubseteq> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"}.
+ @{term "\<lbrakk> x \<sqsubseteq> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"} in fact means
+ @{term "\<And>x y z. \<lbrakk> x \<sqsubseteq> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"}.
Two commands are provided to inspect locales:
\isakeyword{print\_locales} lists the names of all locales of the
current theory; \isakeyword{print\_locale}~$n$ prints the parameters
- and assumptions of locale $n$; \isakeyword{print\_locale!}~$n$
- additionally outputs the conclusions. We may inspect the new locale
+ and assumptions of locale $n$; the variation \isakeyword{print\_locale!}~$n$
+ additionally outputs the conclusions that are stored in the locale.
+ We may inspect the new locale
by issuing \isakeyword{print\_locale!} @{term partial_order}. The output
is the following list of context elements.
-
+\begin{small}
\begin{alltt}
\isakeyword{fixes} le :: "'a \(\Rightarrow\) 'a \(\Rightarrow\) bool" (\isakeyword{infixl} "\(\sqsubseteq\)" 50)
\isakeyword{assumes} "partial_order op \(\sqsubseteq\)"
@@ -85,26 +88,30 @@
\isakeyword{and}
trans [trans] = `\(\isasymlbrakk\)?x \(\sqsubseteq\) ?y; ?y \(\sqsubseteq\) ?z\(\isasymrbrakk\) \(\Longrightarrow\) ?x \(\sqsubseteq\) ?z`
\end{alltt}
-
+\end{small}
The keyword \isakeyword{notes} denotes a conclusion element. There
- is only a single assumption @{term "partial_order le"} in the
- output. The locale declaration has introduced the predicate @{term
- partial_order} to the theory. The predicate is called \emph{locale
- predicate} of the locale. Its definition may be inspected by
- issuing \isakeyword{thm} @{thm [source] partial_order_def}:
+ is one conclusion, which was added automatically. Instead, there is
+ only one assumption, namely @{term "partial_order le"}. The locale
+ declaration has introduced the predicate @{term
+ partial_order} to the theory. This predicate is the
+ \emph{locale predicate}. Its definition may be inspected by
+ issuing \isakeyword{thm} @{thm [source] partial_order_def}.
@{thm [display, indent=2] partial_order_def}
- The original assumptions have been turned into conclusions and are
+ In our example, this is a unary predicate over the parameter of the
+ locale. It is equivalent to the original assumptions, which have
+ been turned into conclusions and are
available as theorems in the context of the locale. The names and
attributes from the locale declaration are associated to these
theorems and are effective in the context of the locale.
- Each locale theorem has a \emph{foundational theorem} as counterpart
- in the theory. For the transitivity theorem, this is @{thm [source]
- partial_order.trans}:
+ Each conclusion has a \emph{foundational theorem} as counterpart
+ in the theory. Technically, this is simply the theorem composed
+ of context and conclusion. For the transitivity theorem, this is
+ @{thm [source] partial_order.trans}:
@{thm [display, indent=2] partial_order_def}
*}
-subsection {* Extending the Locale *}
+subsection {* Targets: Extending Locales *}
text {*
The specification of a locale is fixed, but its list of conclusions
@@ -112,7 +119,7 @@
In the following, \isakeyword{definition} and
\isakeyword{theorem} are illustrated.
Table~\ref{tab:commands-with-target} lists Isar commands that accept
- a target. There are various ways of specifying the target. A
+ a target. Isar provides various ways of specifying the target. A
target for a single command may be indicated with keyword
\isakeyword{in} in the following way:
@@ -142,17 +149,18 @@
where "(x \<sqsubset> y) = (x \<sqsubseteq> y \<and> x \<noteq> y)"
text (in partial_order) {* The strict order @{text less} with infix
- syntax @{text \<sqsubset>} is
- defined in terms of the locale parameter @{text le} and the general
- equality. The definition generates a \emph{foundational constant}
+ syntax~@{text \<sqsubset>} is
+ defined in terms of the locale parameter~@{text le} and the general
+ equality of the object logic we work in. The definition generates a
+ \emph{foundational constant}
@{term partial_order.less} with definition @{thm [source]
partial_order.less_def}:
@{thm [display, indent=2] partial_order.less_def}
At the same time, the locale is extended by syntax transformations
- hiding this construction in the context of the locale. In the
- context of the locale, the abbreviation @{text less} is available for
+ hiding this construction in the context of the locale. Here, the
+ abbreviation @{text less} is available for
@{text "partial_order.less le"}, and it is printed
- and parsed as infix @{text \<sqsubset>}. Finally, the theorem @{thm [source]
+ and parsed as infix~@{text \<sqsubset>}. Finally, the conclusion @{thm [source]
less_def} is added to the locale:
@{thm [display, indent=2] less_def}
*}
@@ -165,8 +173,9 @@
"\<lbrakk> x \<sqsubset> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubset> z"
unfolding %visible less_def by %visible (blast intro: trans)
-text {* In the context of the proof, assumptions and theorems of the
- locale may be used. Attributes are effective: @{text anti_sym} was
+text {* In the context of the proof, conclusions of the
+ locale may be used like theorems. Attributes are effective: @{text
+ anti_sym} was
declared as introduction rule, hence it is in the context's set of
rules used by the classical reasoner by default. *}
@@ -208,7 +217,7 @@
by (unfold is_inf_def) blast
theorem is_inf_uniq: "\<lbrakk>is_inf x y i; is_inf x y i'\<rbrakk> \<Longrightarrow> i = i'"
- proof -
+ proof -
assume inf: "is_inf x y i"
assume inf': "is_inf x y i'"
show ?thesis
@@ -250,7 +259,7 @@
by (unfold is_sup_def) blast
theorem is_sup_uniq: "\<lbrakk>is_sup x y s; is_sup x y s'\<rbrakk> \<Longrightarrow> s = s'"
- proof -
+ proof -
assume sup: "is_sup x y s"
assume sup': "is_sup x y s'"
show ?thesis
@@ -283,10 +292,11 @@
end
text {* The syntax of the locale commands discussed in this tutorial is
- shown in Table~\ref{tab:commands}. The grammer is complete with the
- exception of additional context elements not discussed here. See the
- Isabelle/Isar Reference Manual~\cite{IsarRef}
- for full documentation. *}
+ shown in Table~\ref{tab:commands}. The grammar is complete with the
+ exception of the context elements \isakeyword{constrains} and
+ \isakeyword{defines}, which are provided for backward
+ compatibility. See the Isabelle/Isar Reference
+ Manual~\cite{IsarRef} for full documentation. *}
section {* Import \label{sec:import} *}
@@ -315,7 +325,6 @@
definition
meet (infixl "\<sqinter>" 70) where "x \<sqinter> y = (THE inf. is_inf x y inf)"
-
definition
join (infixl "\<squnion>" 65) where "x \<squnion> y = (THE sup. is_sup x y sup)"
@@ -558,7 +567,8 @@
end
-text {* Locales for total orders and distributive lattices follow for
+text {* Locales for total orders and distributive lattices follow to
+ establish a sufficiently rich landscape of locales for
further examples in this tutorial. Each comes with an example
theorem. *}
@@ -584,13 +594,13 @@
qed
text {*
- The locale hierachy obtained through these declarations is shown in
+ The locale hierarchy obtained through these declarations is shown in
Figure~\ref{fig:lattices}(a).
\begin{figure}
\hrule \vspace{2ex}
\begin{center}
-\subfigure[Declared hierachy]{
+\subfigure[Declared hierarchy]{
\begin{tikzpicture}
\node (po) at (0,0) {@{text partial_order}};
\node (lat) at (-1.5,-1) {@{text lattice}};
@@ -646,20 +656,20 @@
specifications of the locales.
The first from of interpretation we will consider in this tutorial
- is provided by the \isakeyword{sublocale} command, which enables to
+ is provided by the \isakeyword{sublocale} command. It enables to
modify the import hierarchy to reflect the \emph{logical} relation
between locales.
Consider the locale hierarchy from Figure~\ref{fig:lattices}(a).
- Total orders are lattices, although this is not reflected in the
- import hierarchy, and definitions, theorems and other conclusions
+ Total orders are lattices, although this is not reflected here, and
+ definitions, theorems and other conclusions
from @{term lattice} are not available in @{term total_order}. To
obtain the situation in Figure~\ref{fig:lattices}(b), it is
sufficient to add the conclusions of the latter locale to the former.
The \isakeyword{sublocale} command does exactly this.
The declaration \isakeyword{sublocale} $l_1
\subseteq l_2$ causes locale $l_2$ to be \emph{interpreted} in the
- context of $l_1$. All conclusions of $l_2$ are made
+ context of $l_1$. This means that all conclusions of $l_2$ are made
available in $l_1$.
Of course, the change of hierarchy must be supported by a theorem
@@ -677,9 +687,9 @@
Now the
locale predicate needs to be unfolded --- for example, using its
definition or by introduction rules
- provided by the locale package. The locale package provides the
- methods @{text intro_locales} and @{text unfold_locales} to automate
- this. They are aware of the
+ provided by the locale package. For automation, the locale package
+ provides the methods @{text intro_locales} and @{text
+ unfold_locales}. They are aware of the
current context and dependencies between locales and automatically
discharge goals implied by these. While @{text unfold_locales}
always unfolds locale predicates to assumptions, @{text
@@ -716,11 +726,11 @@
by (auto simp: is_sup_def)
then show "\<exists>sup. is_sup x y sup" .. qed %visible
-text {* Similarly, we may establsih that total orders are distributive
+text {* Similarly, we may establish that total orders are distributive
lattices with a second \isakeyword{sublocale} statement. *}
sublocale total_order \<subseteq> distrib_lattice
- proof unfold_locales
+ proof unfold_locales
fix %"proof" x y z
show "x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z" (is "?l = ?r")
txt {* Jacobson I, p.\ 462 *}
@@ -754,6 +764,7 @@
The sublocale relation is transitive --- that is, propagation takes
effect along chains of sublocales. Even cycles in the sublocale relation are
supported, as long as these cycles do not lead to infinite chains.
- For details, see \cite{Ballarin2006a}. *}
+ Details are discussed in the technical report \cite{Ballarin2006a}.
+ See also Section~\ref{sec:infinite-chains} of this tutorial. *}
end
--- a/doc-src/Locales/Locales/Examples1.thy Thu Oct 15 22:22:08 2009 +0200
+++ b/doc-src/Locales/Locales/Examples1.thy Sat Oct 17 22:58:18 2009 +0200
@@ -1,12 +1,12 @@
theory Examples1
imports Examples
begin
-
+text {* \vspace{-5ex} *}
section {* Use of Locales in Theories and Proofs
\label{sec:interpretation} *}
text {*
- Locales can also be interpreted in the contexts of theories and
+ Locales can be interpreted in the contexts of theories and
structured proofs. These interpretations are dynamic, too.
Conclusions of locales will be propagated to the current theory or
the current proof context.%
@@ -19,10 +19,10 @@
Section~\ref{sec:local-interpretation}.
As an example, consider the type of integers @{typ int}. The
- relation @{term "op \<le>"} is a total order over @{typ int},
- divisibility @{text "op dvd"} forms a distributive lattice. We start with the
- interpretation that @{term "op \<le>"} is a partial order. The facilities of
- the interpretation command are explored gradually in three versions.
+ relation @{term "op \<le>"} is a total order over @{typ int}. We start
+ with the interpretation that @{term "op \<le>"} is a partial order. The
+ facilities of the interpretation command are explored gradually in
+ three versions.
*}
@@ -44,9 +44,9 @@
white-space-separated list of terms, which provide a full
instantiation of the locale parameters. The parameters are referred
to by order of declaration, which is also the order in which
- \isakeyword{print\_locale} outputs them.
-
-[TODO: Introduce morphisms. Reference to \ref{sec:locale-expressions}.]
+ \isakeyword{print\_locale} outputs them. The locale has only a
+ single parameter, hence the list of instantiation terms is a
+ singleton.
The command creates the goal
@{subgoals [display]} which can be shown easily:
@@ -60,7 +60,7 @@
theorem:
@{thm [display, indent=2] int.trans}
It is not possible to reference this theorem simply as @{text
- trans}, which prevents unwanted hiding of existing theorems of the
+ trans}. This prevents unwanted hiding of existing theorems of the
theory by an interpretation. *}
@@ -69,7 +69,7 @@
text {* Not only does the above interpretation qualify theorem names.
The prefix @{text int} is applied to all names introduced in locale
conclusions including names introduced in definitions. The
- qualified name @{text int.less} refers to
+ qualified name @{text int.less} is short for
the interpretation of the definition, which is @{term int.less}.
Qualified name and expanded form may be used almost
interchangeably.%
@@ -84,6 +84,6 @@
In order to allow for the desired replacement, interpretation
accepts \emph{equations} in addition to the parameter instantiation.
These follow the locale expression and are indicated with the
- keyword \isakeyword{where}. The revised interpretation follows.
+ keyword \isakeyword{where}. This is the revised interpretation:
*}
end
--- a/doc-src/Locales/Locales/Examples2.thy Thu Oct 15 22:22:08 2009 +0200
+++ b/doc-src/Locales/Locales/Examples2.thy Sat Oct 17 22:58:18 2009 +0200
@@ -5,8 +5,9 @@
interpretation %visible int: partial_order "op \<le> :: [int, int] \<Rightarrow> bool"
where "partial_order.less op \<le> (x::int) y = (x < y)"
proof -
- txt {* \normalsize The goals are @{subgoals [display]}
- The proof that @{text \<le>} is a partial order is as above. *}
+ txt {* \normalsize The goals are now:
+ @{subgoals [display]}
+ The proof that~@{text \<le>} is a partial order is as above. *}
show "partial_order (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)"
by unfold_locales auto
txt {* \normalsize The second goal is shown by unfolding the
@@ -17,7 +18,7 @@
qed
text {* Note that the above proof is not in the context of the
- interpreted locale. Hence, the correct interpretation of @{text
- "partial_order.less_def"} is obtained manually with @{text OF}.
+ interpreted locale. Hence, the premise of @{text
+ "partial_order.less_def"} is discharged manually with @{text OF}.
*}
end
--- a/doc-src/Locales/Locales/Examples3.thy Thu Oct 15 22:22:08 2009 +0200
+++ b/doc-src/Locales/Locales/Examples3.thy Sat Oct 17 22:58:18 2009 +0200
@@ -1,8 +1,6 @@
theory Examples3
-imports Examples "~~/src/HOL/Number_Theory/UniqueFactorization"
+imports Examples
begin
-hide %invisible const Lattices.lattice
- (* imported again through Number_Theory *)
text {* \vspace{-5ex} *}
subsection {* Third Version: Local Interpretation
\label{sec:local-interpretation} *}
@@ -11,7 +9,7 @@
order for the integers was used in the second goal to
discharge the premise in the definition of @{text "op \<sqsubset>"}. In
general, proofs of the equations not only may involve definitions
- fromthe interpreted locale but arbitrarily complex arguments in the
+ from the interpreted locale but arbitrarily complex arguments in the
context of the locale. Therefore is would be convenient to have the
interpreted locale conclusions temporary available in the proof.
This can be achieved by a locale interpretation in the proof body.
@@ -34,34 +32,38 @@
also obtained in the interpretation from Section~\ref{sec:po-first},
and @{text int.less_def} may directly be used to unfold the
definition. Theorems from the local interpretation disappear after
- leaving the proof context --- that is, after the closing a
+ leaving the proof context --- that is, after the succeeding
\isakeyword{next} or \isakeyword{qed} statement. *}
subsection {* Further Interpretations *}
text {* Further interpretations are necessary for
- the other locales. In @{text lattice} the operations @{text \<sqinter>} and
- @{text \<squnion>} are substituted by @{term "min :: int \<Rightarrow> int \<Rightarrow> int"} and
- @{term "max :: int \<Rightarrow> int \<Rightarrow> int"}. The entire proof for the
+ the other locales. In @{text lattice} the operations~@{text \<sqinter>}
+ and~@{text \<squnion>} are substituted by @{term "min :: int \<Rightarrow> int \<Rightarrow> int"}
+ and @{term "max :: int \<Rightarrow> int \<Rightarrow> int"}. The entire proof for the
interpretation is reproduced to give an example of a more
- elaborate interpretation proof. *}
+ elaborate interpretation proof. Note that the equations are named
+ so they can be used in a later example. *}
interpretation %visible int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
- where "lattice.meet op \<le> (x::int) y = min x y"
- and "lattice.join op \<le> (x::int) y = max x y"
+ where int_min_eq: "lattice.meet op \<le> (x::int) y = min x y"
+ and int_max_eq: "lattice.join op \<le> (x::int) y = max x y"
proof -
show "lattice (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)"
txt {* \normalsize We have already shown that this is a partial
order, *}
apply unfold_locales
txt {* \normalsize hence only the lattice axioms remain to be
- shown: @{subgoals [display]} After unfolding @{text is_inf} and
- @{text is_sup}, *}
+ shown.
+ @{subgoals [display]}
+ By @{text is_inf} and @{text is_sup}, *}
apply (unfold int.is_inf_def int.is_sup_def)
- txt {* \normalsize the goals become @{subgoals [display]}
- This can be solved by Presburger arithmetic, which is contained
- in @{text arith}. *}
+ txt {* \normalsize the goals are transformed to these
+ statements:
+ @{subgoals [display]}
+ This is Presburger arithmetic, which can be solved by the
+ method @{text arith}. *}
by arith+
txt {* \normalsize In order to show the equations, we put ourselves
in a situation where the lattice theorems can be used in a
@@ -98,211 +100,112 @@
\end{tabular}
\end{center}
\hrule
-\caption{Interpreted theorems for @{text \<le>} on the integers.}
+\caption{Interpreted theorems for~@{text \<le>} on the integers.}
\label{tab:int-lattice}
\end{table}
\begin{itemize}
\item
Locale @{text distrib_lattice} was also interpreted. Since the
- locale hierarcy reflects that total orders are distributive
+ locale hierarchy reflects that total orders are distributive
lattices, the interpretation of the latter was inserted
automatically with the interpretation of the former. In general,
- interpretation of a locale will also interpret all locales further
- up in the hierarchy, regardless whether imported or proved via the
- \isakeyword{sublocale} command.
+ interpretation traverses the locale hierarchy upwards and interprets
+ all encountered locales, regardless whether imported or proved via
+ the \isakeyword{sublocale} command. Existing interpretations are
+ skipped avoiding duplicate work.
\item
- Theorem @{thm [source] int.less_total} makes use of @{term "op <"}
+ The predicate @{term "op <"} appears in theorem @{thm [source]
+ int.less_total}
although an equation for the replacement of @{text "op \<sqsubset>"} was only
- given in the interpretation of @{text partial_order}. These
- equations are pushed downwards the hierarchy for related
- interpretations --- that is, for interpretations that share the
- instance for parameters they have in common.
+ given in the interpretation of @{text partial_order}. The
+ interpretation equations are pushed downwards the hierarchy for
+ related interpretations --- that is, for interpretations that share
+ the instances of parameters they have in common.
\end{itemize}
- In the next section, the divisibility relation on the natural
- numbers will be explored.
*}
-
-subsection {* Interpretations for Divisibility *}
-
-text {* In this section, further examples of interpretations are
- presented. Impatient readers may skip this section at first
- reading.
-
- Divisibility on the natural numbers is a distributive lattice
- but not a total order. Interpretation again proceeds
- incrementally. In order to distinguish divisibility from the order
- relation $\le$, we use the qualifier @{text nat_dvd} for
- divisibility. *}
-
- interpretation nat_dvd: partial_order "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
- where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
- proof -
- show "partial_order (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
- by unfold_locales (auto simp: dvd_def)
- then interpret nat_dvd: partial_order "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" .
- show "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
- apply (unfold nat_dvd.less_def)
- apply auto
- done
- qed
-
-text {* Note that in Isabelle/HOL there is no operator for strict
- divisibility. Instead, we substitute @{term "x dvd y \<and> x \<noteq> y"}. *}
-
- interpretation nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
- where nat_dvd_meet_eq:
- "lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd"
- and nat_dvd_join_eq:
- "lattice.join (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = lcm"
- proof -
- show "lattice (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
- apply unfold_locales
- apply (unfold nat_dvd.is_inf_def nat_dvd.is_sup_def)
- apply (rule_tac x = "gcd x y" in exI)
- apply auto [1]
- apply (rule_tac x = "lcm x y" in exI)
- apply (auto intro: lcm_least_nat)
- done
- then interpret nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" .
- show "lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd"
- apply (auto simp add: expand_fun_eq)
- apply (unfold nat_dvd.meet_def)
- apply (rule the_equality)
- apply (unfold nat_dvd.is_inf_def)
- by auto
- show "lattice.join (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = lcm"
- apply (auto simp add: expand_fun_eq)
- apply (unfold nat_dvd.join_def)
- apply (rule the_equality)
- apply (unfold nat_dvd.is_sup_def)
- apply (auto intro: lcm_least_nat iff: lcm_unique_nat)
- done
- qed
-
-text {* The replacement equations @{thm [source] nat_dvd_meet_eq} and
- @{thm [source] nat_dvd_join_eq} are theorems of current theories.
- They are named so that they can be used in the main part of the
- subsequent interpretation. *}
-
- interpretation %visible nat_dvd:
- distrib_lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
- apply unfold_locales
- txt {* \normalsize @{subgoals [display]}
- Distributivity of lattice meet and join needs to be shown. This is
- distributivity of gcd and lcm, as becomes apparent when unfolding
- the replacement equations from the previous interpretation: *}
- unfolding nat_dvd_meet_eq nat_dvd_join_eq
- txt {* \normalsize @{subgoals [display]}
- This is a result of number theory: *}
- by (rule UniqueFactorization.gcd_lcm_distrib_nat)
-
-text {* Theorems that are available in the theory after these
- interpretations are shown in Table~\ref{tab:nat-dvd-lattice}.
-
-\begin{table}
-\hrule
-\vspace{2ex}
-\begin{center}
-\begin{tabular}{l}
- @{thm [source] nat_dvd.less_def} from locale @{text partial_order}: \\
- \quad @{thm nat_dvd.less_def} \\
- @{thm [source] nat_dvd.meet_left} from locale @{text lattice}: \\
- \quad @{thm nat_dvd.meet_left} \\
- @{thm [source] nat_dvd.join_distr} from locale @{text distrib_lattice}: \\
- \quad @{thm nat_dvd.join_distr} \\
-\end{tabular}
-\end{center}
-\hrule
-\caption{Interpreted theorems for @{text dvd} on the natural numbers.}
-\label{tab:nat-dvd-lattice}
-\end{table}
- *}
-
-
-subsection {* Inspecting Interpretations of a Locale *}
-
text {* The interpretations for a locale $n$ within the current
theory may be inspected with \isakeyword{print\_interps}~$n$. This
prints the list of instances of $n$, for which interpretations exist.
For example, \isakeyword{print\_interps} @{term partial_order}
outputs the following:
+\begin{small}
\begin{alltt}
int! : partial_order "op \(\le\)"
- nat_dvd! : partial_order "op dvd"
\end{alltt}
- The interpretation qualifiers on the left are decorated with an
- exclamation point, which means that they are mandatory. Qualifiers
+\end{small}
+ Of course, there is only one interpretation.
+ The interpretation qualifier on the left is decorated with an
+ exclamation point. This means that it is mandatory. Qualifiers
can either be \emph{mandatory} or \emph{optional}, designated by
``!'' or ``?'' respectively. Mandatory qualifiers must occur in a
name reference while optional ones need not. Mandatory qualifiers
- prevent accidental hiding of names, while optional qualifers can be
+ prevent accidental hiding of names, while optional qualifiers can be
more convenient to use. For \isakeyword{interpretation}, the
- default for qualifiers without an explicit designator is ``!''.
+ default is ``!''.
*}
section {* Locale Expressions \label{sec:expressions} *}
text {*
- A map @{term \<phi>} between partial orders @{text \<sqsubseteq>} and @{text \<preceq>}
+ A map~@{term \<phi>} between partial orders~@{text \<sqsubseteq>} and~@{text \<preceq>}
is called order preserving if @{text "x \<sqsubseteq> y"} implies @{text "\<phi> x \<preceq>
\<phi> y"}. This situation is more complex than those encountered so
far: it involves two partial orders, and it is desirable to use the
existing locale for both.
A locale for order preserving maps requires three parameters: @{text
- le} (\isakeyword{infixl}~@{text \<sqsubseteq>}), @{text le'}
- (\isakeyword{infixl}~@{text \<preceq>}) for the orders and @{text \<phi>} for the
- map.
+ le}~(\isakeyword{infixl}~@{text \<sqsubseteq>}) and @{text
+ le'}~(\isakeyword{infixl}~@{text \<preceq>}) for the orders and~@{text \<phi>}
+ for the map.
In order to reuse the existing locale for partial orders, which has
- the single parameter @{text le}, it must be imported twice, once
- mapping its parameter to @{text le} (\isakeyword{infixl}~@{text \<sqsubseteq>})
- from the new locale and once to @{text le'}
- (\isakeyword{infixl}~@{text \<preceq>}). This can be achieved with a locale
+ the single parameter~@{text le}, it must be imported twice, once
+ mapping its parameter to~@{text le} from the new locale and once
+ to~@{text le'}. This can be achieved with a compound locale
expression.
- A \emph{locale expression} is a sequence of \emph{locale instances}
- separated by ``$\textbf{+}$'' and followed by a \isakeyword{for}
+ In general, a locale expression is a sequence of \emph{locale instances}
+ separated by~``$\textbf{+}$'' and followed by a \isakeyword{for}
clause.
-An instance has the following format:
+ An instance has the following format:
\begin{quote}
\textit{qualifier} \textbf{:} \textit{locale-name}
\textit{parameter-instantiation}
\end{quote}
We have already seen locale instances as arguments to
\isakeyword{interpretation} in Section~\ref{sec:interpretation}.
- The qualifier serves to disambiguate the names from different
- instances of the same locale.
+ As before, the qualifier serves to disambiguate names from
+ different instances of the same locale. While in
+ \isakeyword{interpretation} qualifiers default to mandatory, in
+ import and in the \isakeyword{sublocale} command, they default to
+ optional.
- Since the parameters @{text le} and @{text le'} are to be partial
+ Since the parameters~@{text le} and~@{text le'} are to be partial
orders, our locale for order preserving maps will import the these
instances:
+\begin{small}
\begin{alltt}
le: partial_order le
le': partial_order le'
\end{alltt}
- For matter of convenience we choose the parameter names also as
- qualifiers. This is an arbitrary decision. Technically, qualifiers
+\end{small}
+ For matter of convenience we choose to name parameter names and
+ qualifiers alike. This is an arbitrary decision. Technically, qualifiers
and parameters are unrelated.
Having determined the instances, let us turn to the \isakeyword{for}
clause. It serves to declare locale parameters in the same way as
the context element \isakeyword{fixes} does. Context elements can
only occur after the import section, and therefore the parameters
- referred to inthe instances must be declared in the \isakeyword{for}
- clause.%
-\footnote{Since all parameters can be declared in the \isakeyword{for}
- clause, the context element \isakeyword{fixes} is not needed in
- locales. It is provided for compatibility with the long goals
- format, where the context element also occurs.}
- The \isakeyword{for} clause is also where the syntax of these
+ referred to in the instances must be declared in the \isakeyword{for}
+ clause. The \isakeyword{for} clause is also where the syntax of these
parameters is declared.
- Two context elements for the map parameter @{text \<phi>} and the
- assumptions that it is order perserving complete the locale
+ Two context elements for the map parameter~@{text \<phi>} and the
+ assumptions that it is order preserving complete the locale
declaration. *}
locale order_preserving =
@@ -314,19 +217,18 @@
text (in order_preserving) {* Here are examples of theorems that are
available in the locale:
- @{thm [source] hom_le}: @{thm hom_le}
-
- @{thm [source] le.less_le_trans}: @{thm le.less_le_trans}
+ \hspace*{1em}@{thm [source] hom_le}: @{thm hom_le}
- @{thm [source] le'.less_le_trans}:
- @{thm [display, indent=2] le'.less_le_trans}
+ \hspace*{1em}@{thm [source] le.less_le_trans}: @{thm le.less_le_trans}
+ \hspace*{1em}@{thm [source] le'.less_le_trans}:
+ @{thm [display, indent=4] le'.less_le_trans}
While there is infix syntax for the strict operation associated to
@{term "op \<sqsubseteq>"}, there is none for the strict version of @{term
"op \<preceq>"}. The abbreviation @{text less} with its infix syntax is only
available for the original instance it was declared for. We may
- introduce the abbreviation @{text less'} with infix syntax @{text \<prec>}
- with this declaration: *}
+ introduce the abbreviation @{text less'} with infix syntax~@{text \<prec>}
+ with the following declaration: *}
abbreviation (in order_preserving)
less' (infixl "\<prec>" 50) where "less' \<equiv> partial_order.less le'"
@@ -335,47 +237,55 @@
@{thm [source] le'.less_le_trans}:
@{thm [display, indent=2] le'.less_le_trans} *}
+text {* There are short notations for locale expressions. These are
+ discussed in the following. *}
-subsection {* Default Instantiations and Implicit Parameters *}
+
+subsection {* Default Instantiations *}
-text {* It is possible to omit parameter instantiations in a locale
- expression. In that case, the instantiation defaults to the name of
- the parameter itself. That is, the locale expression @{text
+text {*
+ It is possible to omit parameter instantiations. The
+ instantiation then defaults to the name of
+ the parameter itself. For example, the locale expression @{text
partial_order} is short for @{text "partial_order le"}, since the
- locale's single parameter is @{text le}. We took advantage of this
- short hand in the \isakeyword{sublocale} declarations of
+ locale's single parameter is~@{text le}. We took advantage of this
+ in the \isakeyword{sublocale} declarations of
Section~\ref{sec:changing-the-hierarchy}. *}
+subsection {* Implicit Parameters \label{sec:implicit-parameters} *}
+
text {* In a locale expression that occurs within a locale
declaration, omitted parameters additionally extend the (possibly
empty) \isakeyword{for} clause.
- The \isakeyword{for} clause is a
- general construct of Isabelle/Isar to mark names from the preceding
- declaration as ``arbitrary but fixed''. This is necessary for
- example, if the name is already bound in a surrounding context. In
- a locale expression, names occurring in parameter instantiations
- should be bound by a \isakeyword{for} clause whenever these names
- are not introduced elsewhere in the context --- for example, on the
- left hand side of a \isakeyword{sublocale} declaration.
+ The \isakeyword{for} clause is a general construct of Isabelle/Isar
+ to mark names occurring in the preceding declaration as ``arbitrary
+ but fixed''. This is necessary for example, if the name is already
+ bound in a surrounding context. In a locale expression, names
+ occurring in parameter instantiations should be bound by a
+ \isakeyword{for} clause whenever these names are not introduced
+ elsewhere in the context --- for example, on the left hand side of a
+ \isakeyword{sublocale} declaration.
There is an exception to this rule in locale declarations, where the
- \isakeyword{for} clause servers to declare locale parameters. Here,
+ \isakeyword{for} clause serves to declare locale parameters. Here,
locale parameters for which no parameter instantiation is given are
implicitly added, with their mixfix syntax, at the beginning of the
\isakeyword{for} clause. For example, in a locale declaration, the
expression @{text partial_order} is short for
+\begin{small}
\begin{alltt}
partial_order le \isakeyword{for} le (\isakeyword{infixl} "\(\sqsubseteq\)" 50)\textrm{.}
\end{alltt}
- This short hand was used in the locale declarations of
+\end{small}
+ This short hand was used in the locale declarations throughout
Section~\ref{sec:import}.
*}
text{*
- The following locale declarations provide more examples. A map
- @{text \<phi>} is a lattice homomorphism if it preserves meet and
+ The following locale declarations provide more examples. A
+ map~@{text \<phi>} is a lattice homomorphism if it preserves meet and
join. *}
locale lattice_hom =
@@ -384,13 +294,13 @@
assumes hom_meet: "\<phi> (x \<sqinter> y) = le'.meet (\<phi> x) (\<phi> y)"
and hom_join: "\<phi> (x \<squnion> y) = le'.join (\<phi> x) (\<phi> y)"
-text {* We omit the parameter instantiation in the first instance of
- @{term lattice}. This causes the parameter @{text le} to be added
- to the \isakeyword{for} clause, and the locale has parameters
- @{text le} and @{text le'}.
+text {* The parameter instantiation in the first instance of @{term
+ lattice} is omitted. This causes the parameter~@{text le} to be
+ added to the \isakeyword{for} clause, and the locale has
+ parameters~@{text le},~@{text le'} and, of course,~@{text \<phi>}.
Before turning to the second example, we complete the locale by
- provinding infix syntax for the meet and join operations of the
+ providing infix syntax for the meet and join operations of the
second lattice.
*}
@@ -399,23 +309,24 @@
abbreviation join' (infixl "\<squnion>''" 50) where "join' \<equiv> le'.join"
end
-text {* The next example pushes the short hand facilities. A
- homomorphism is an endomorphism if both orders coincide. *}
+text {* The next example makes radical use of the short hand
+ facilities. A homomorphism is an endomorphism if both orders
+ coincide. *}
locale lattice_end = lattice_hom _ le
-text {* The notation @{text _} enables to omit a parameter in a
- positional instantiation. The omitted parameter, @{text le} becomes
+text {* The notation~@{text _} enables to omit a parameter in a
+ positional instantiation. The omitted parameter,~@{text le} becomes
the parameter of the declared locale and is, in the following
- position used to instantiate the second parameter of @{text
+ position, used to instantiate the second parameter of @{text
lattice_hom}. The effect is that of identifying the first in second
parameter of the homomorphism locale. *}
text {* The inheritance diagram of the situation we have now is shown
in Figure~\ref{fig:hom}, where the dashed line depicts an
- interpretation which is introduced below. Renamings are
- indicated by $\sqsubseteq \mapsto \preceq$ etc. By looking at the
- inheritance diagram it would seem
+ interpretation which is introduced below. Parameter instantiations
+ are indicated by $\sqsubseteq \mapsto \preceq$ etc. By looking at
+ the inheritance diagram it would seem
that two identical copies of each of the locales @{text
partial_order} and @{text lattice} are imported by @{text
lattice_end}. This is not the case! Inheritance paths with
@@ -472,57 +383,130 @@
lattice_hom}, for example
@{thm [source] hom_le}:
@{thm [display, indent=2] hom_le}
+ This theorem will be useful in the following section.
*}
-(*
+
section {* Conditional Interpretation *}
+text {* There are situations where an interpretation is not possible
+ in the general case since the desired property is only valid if
+ certain conditions are fulfilled. Take, for example, the function
+ @{text "\<lambda>i. n * i"} that scales its argument by a constant factor.
+ This function is order preserving (and even a lattice endomorphism)
+ with respect to @{term "op \<le>"} provided @{text "n \<ge> 0"}.
+
+ It is not possible to express this using a global interpretation,
+ because it is in general unspecified whether~@{term n} is
+ non-negative, but one may make an interpretation in an inner context
+ of a proof where full information is available.
+ This is not fully satisfactory either, since potentially
+ interpretations may be required to make interpretations in many
+ contexts. What is
+ required is an interpretation that depends on the condition --- and
+ this can be done with the \isakeyword{sublocale} command. For this
+ purpose, we introduce a locale for the condition. *}
+
locale non_negative =
fixes n :: int
- assumes non_negative: "0 \<le> n"
+ assumes non_neg: "0 \<le> n"
+
+text {* It is again convenient to make the interpretation in an
+ incremental fashion, first for order preserving maps, the for
+ lattice endomorphisms. *}
- interpretation partial_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
- where "partial_order.less op \<le> (x::int) y = (x < y)"
- sorry
+ sublocale non_negative \<subseteq>
+ order_preserving "op \<le>" "op \<le>" "\<lambda>i. n * i"
+ using non_neg by unfold_locales (rule mult_left_mono)
+
+text {* While the proof of the previous interpretation
+ is straightforward from monotonicity lemmas for~@{term "op *"}, the
+ second proof follows a useful pattern. *}
- sublocale non_negative \<subseteq> order_preserving "op \<le>" "op \<le>" "\<lambda>i. n * i"
- apply unfold_locales using non_negative apply - by (rule mult_left_mono)
+ sublocale %visible non_negative \<subseteq> lattice_end "op \<le>" "\<lambda>i. n * i"
+ proof (unfold_locales, unfold int_min_eq int_max_eq)
+ txt {* \normalsize Unfolding the locale predicates \emph{and} the
+ interpretation equations immediately yields two subgoals that
+ reflect the core conjecture.
+ @{subgoals [display]}
+ It is now necessary to show, in the context of @{term
+ non_negative}, that multiplication by~@{term n} commutes with
+ @{term min} and @{term max}. *}
+ qed (auto simp: hom_le)
- interpretation lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
- where min_eq: "lattice.meet op \<le> (x::int) y = min x y"
- and max_eq: "lattice.join op \<le> (x::int) y = max x y"
- sorry
+text (in order_preserving) {* The lemma @{thm [source] hom_le}
+ simplifies a proof that would have otherwise been lengthy and we may
+ consider making it a default rule for the simplifier: *}
- apply unfold_locales unfolding is_inf_def is_sup_def by arith+
+ lemmas (in order_preserving) hom_le [simp]
- sublocale non_negative \<subseteq> lattice_end "op \<le>" "\<lambda>i. n * i"
- apply unfold_locales unfolding min_eq max_eq apply (case_tac "x \<le> y")
- unfolding min_def apply auto apply arith
- apply (rule sym)
- apply (rule the_equality)
- proof
+subsection {* Avoiding Infinite Chains of Interpretations
+ \label{sec:infinite-chains} *}
+
+text {* Similar situations arise frequently in formalisations of
+ abstract algebra where it is desirable to express that certain
+ constructions preserve certain properties. For example, polynomials
+ over rings are rings, or --- an example from the domain where the
+ illustrations of this tutorial are taken from --- a partial order
+ may be obtained for a function space by point-wise lifting of the
+ partial order of the co-domain. This corresponds to the following
+ interpretation: *}
+
+ sublocale %visible partial_order \<subseteq> f: partial_order "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x"
+ oops
+
+text {* Unfortunately this is a cyclic interpretation that leads to an
+ infinite chain, namely
+ @{text [display, indent=2] "partial_order \<subseteq> partial_order (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) \<subseteq>
+ partial_order (\<lambda>f g. \<forall>x y. f x y \<sqsubseteq> g x y) \<subseteq> \<dots>"}
+ and the interpretation is rejected.
+
+ Instead it is necessary to declare a locale that is logically
+ equivalent to @{term partial_order} but serves to collect facts
+ about functions spaces where the co-domain is a partial order, and
+ to make the interpretation in its context: *}
- locale fspace_po = partial_order
- sublocale fspace_po \<subseteq> fspace: partial_order "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x"
-(* fspace needed to disambiguate less etc *)
-apply unfold_locales
-apply auto
-apply (rule) apply auto apply (blast intro: trans) done
+ locale fun_partial_order = partial_order
+
+ sublocale fun_partial_order \<subseteq>
+ f: partial_order "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x"
+ by unfold_locales (fast,rule,fast,blast intro: trans)
+
+text {* It is quite common in abstract algebra that such a construction
+ maps a hierarchy of algebraic structures (or specifications) to a
+ related hierarchy. By means of the same lifting, a function space
+ is a lattice if its co-domain is a lattice: *}
+
+ locale fun_lattice = fun_partial_order + lattice
-*)
+ sublocale fun_lattice \<subseteq> f: lattice "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x"
+ proof unfold_locales
+ fix f g
+ have "partial_order.is_inf (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g (\<lambda>x. f x \<sqinter> g x)"
+ apply (rule is_infI) apply rule+ apply (drule spec, assumption)+ done
+ then show "\<exists>inf. partial_order.is_inf (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g inf"
+ by fast
+ next
+ fix f g
+ have "partial_order.is_sup (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g (\<lambda>x. f x \<squnion> g x)"
+ apply (rule is_supI) apply rule+ apply (drule spec, assumption)+ done
+ then show "\<exists>sup. partial_order.is_sup (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g sup"
+ by fast
+ qed
+
section {* Further Reading *}
text {* More information on locales and their interpretation is
available. For the locale hierarchy of import and interpretation
- dependencies see \cite{Ballarin2006a}; interpretations in theories
- and proofs are covered in \cite{Ballarin2006b}. In the latter, I
+ dependencies see~\cite{Ballarin2006a}; interpretations in theories
+ and proofs are covered in~\cite{Ballarin2006b}. In the latter, I
show how interpretation in proofs enables to reason about families
of algebraic structures, which cannot be expressed with locales
directly.
- Haftmann and Wenzel \cite{HaftmannWenzel2007} overcome a restriction
+ Haftmann and Wenzel~\cite{HaftmannWenzel2007} overcome a restriction
of axiomatic type classes through a combination with locale
interpretation. The result is a Haskell-style class system with a
facility to generate ML and Haskell code. Classes are sufficient for
@@ -532,13 +516,16 @@
on the other hand, do not.
The locales reimplementation for Isabelle 2009 provides, among other
- improvements, a clean intergration with Isabelle/Isar's local theory
- mechnisms, which are described in \cite{HaftmannWenzel2009}.
+ improvements, a clean integration with Isabelle/Isar's local theory
+ mechanisms, which are described in another paper by Haftmann and
+ Wenzel~\cite{HaftmannWenzel2009}.
- The original work of Kamm\"uller on locales \cite{KammullerEtAl1999}
- may be of interest from a historical perspective. The mathematical
- background on orders and lattices is taken from Jacobson's textbook
- on algebra \cite[Chapter~8]{Jacobson1985}.
+ The original work of Kamm\"uller on locales~\cite{KammullerEtAl1999}
+ may be of interest from a historical perspective. My previous
+ report on locales and locale expressions~\cite{Ballarin2004a}
+ describes a simpler form of expressions than available now and is
+ outdated. The mathematical background on orders and lattices is
+ taken from Jacobson's textbook on algebra~\cite[Chapter~8]{Jacobson1985}.
The sources of this tutorial, which include all proofs, are
available with the Isabelle distribution at
@@ -648,18 +635,22 @@
\end{table}
*}
-text {* \textbf{Revision History.} For the present third revision,
- which was completed in October 2009, much of the explanatory text
- has been rewritten. In addition, inheritance of interpretation
- equations, which was not available for Isabelle 2009, but in the
- meantime has been implemented, is illustrated. The second revision
- accommodates changes introduced by the locales reimplementation for
- Isabelle 2009. Most notably, in complex specifications
- (\emph{locale expressions}) renaming has been generalised to
- instantiation. *}
+text {* \textbf{Revision History.} For the present third revision of
+ the tutorial, much of the explanatory text
+ was rewritten. Inheritance of interpretation equations is
+ available with the forthcoming release of Isabelle, which at the
+ time of editing these notes is expected for the end of 2009.
+ The second revision accommodates changes introduced by the locales
+ reimplementation for Isabelle 2009. Most notably locale expressions
+ have been generalised from renaming to instantiation. *}
text {* \textbf{Acknowledgements.} Alexander Krauss, Tobias Nipkow,
Randy Pollack, Christian Sternagel and Makarius Wenzel have made
- useful comments on earlier versions of this document. *}
+ useful comments on earlier versions of this document. The section
+ on conditional interpretation was inspired by a number of e-mail
+ enquiries the author received from locale users, and which suggested
+ that this use case is important enough to deserve explicit
+ explanation. The term \emph{conditional interpretation} is due to
+ Larry Paulson. *}
end
--- a/doc-src/Locales/Locales/ROOT.ML Thu Oct 15 22:22:08 2009 +0200
+++ b/doc-src/Locales/Locales/ROOT.ML Sat Oct 17 22:58:18 2009 +0200
@@ -1,4 +1,3 @@
-no_document use_thy "~~/src/HOL/Number_Theory/UniqueFactorization";
use_thy "Examples1";
use_thy "Examples2";
use_thy "Examples3";
--- a/doc-src/Locales/Locales/document/Examples.tex Thu Oct 15 22:22:08 2009 +0200
+++ b/doc-src/Locales/Locales/document/Examples.tex Sat Oct 17 22:58:18 2009 +0200
@@ -46,19 +46,20 @@
\[
\isa{{\isasymAnd}x\isactrlsub {\isadigit{1}}{\isasymdots}x\isactrlsub n{\isachardot}\ {\isasymlbrakk}\ A\isactrlsub {\isadigit{1}}{\isacharsemicolon}\ {\isasymdots}\ {\isacharsemicolon}A\isactrlsub m\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymdots}}
\]
- where variables \isa{x\isactrlsub {\isadigit{1}}}, \ldots, \isa{x\isactrlsub n} are called
- \emph{parameters} and the premises $\isa{A\isactrlsub {\isadigit{1}}}, \ldots,
- \isa{A\isactrlsub m}$ \emph{assumptions}. A formula \isa{C}
+ where variables~\isa{x\isactrlsub {\isadigit{1}}}, \ldots,~\isa{x\isactrlsub n} are called
+ \emph{parameters} and the premises $\isa{A\isactrlsub {\isadigit{1}}}, \ldots,~\isa{A\isactrlsub m}$ \emph{assumptions}. A formula~\isa{C}
is a \emph{theorem} in the context if it is a conclusion
\[
-%\label{eq-fact-in-context}
\isa{{\isasymAnd}x\isactrlsub {\isadigit{1}}{\isasymdots}x\isactrlsub n{\isachardot}\ {\isasymlbrakk}\ A\isactrlsub {\isadigit{1}}{\isacharsemicolon}\ {\isasymdots}\ {\isacharsemicolon}A\isactrlsub m\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ C}.
\]
Isabelle/Isar's notion of context goes beyond this logical view.
Its contexts record, in a consecutive order, proved
- conclusions along with attributes, which
- may control proof procedures. Contexts also contain syntax information
- for parameters and for terms depending on them.%
+ conclusions along with \emph{attributes}, which can provide context
+ specific configuration information for proof procedures and concrete
+ syntax. From a logical perspective, locales are just contexts that
+ have been made persistent. To the user, though, they provide
+ powerful means for declaring and combining contexts, and for the
+ reuse of theorems proved in these contexts.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -67,7 +68,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Locales can be seen as persistent contexts. In its simplest form, a
+In its simplest form, a
\emph{locale declaration} consists of a sequence of context elements
declaring parameters (keyword \isakeyword{fixes}) and assumptions
(keyword \isakeyword{assumes}). The following is the specification of
@@ -81,24 +82,25 @@
\ \ \ \ \ \ \isakeyword{and}\ anti{\isacharunderscore}sym\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}\ x\ {\isasymsqsubseteq}\ y{\isacharsemicolon}\ y\ {\isasymsqsubseteq}\ x\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isakeyword{and}\ trans\ {\isacharbrackleft}trans{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}\ x\ {\isasymsqsubseteq}\ y{\isacharsemicolon}\ y\ {\isasymsqsubseteq}\ z\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isasymsqsubseteq}\ z{\isachardoublequoteclose}%
\begin{isamarkuptext}%
-The parameter of this locale is \isa{le},
- which is a binary predicate with infix syntax
- \isa{{\isasymsqsubseteq}}. The parameter syntax is available in the subsequent
- assumptions, which ar the normal partial order axioms.
+The parameter of this locale is~\isa{le},
+ which is a binary predicate with infix syntax~\isa{{\isasymsqsubseteq}}. The
+ parameter syntax is available in the subsequent
+ assumptions, which are the familiar partial order axioms.
- Isabelle recognises undbound names as free variables. In locale
+ Isabelle recognises unbound names as free variables. In locale
assumptions, these are implicitly universally quantified. That is,
- it is sufficient to write \isa{{\isasymlbrakk}x\ {\isasymsqsubseteq}\ y{\isacharsemicolon}\ y\ {\isasymsqsubseteq}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isasymsqsubseteq}\ z} rather
- than \isa{{\isasymAnd}x\ y\ z{\isachardot}\ {\isasymlbrakk}x\ {\isasymsqsubseteq}\ y{\isacharsemicolon}\ y\ {\isasymsqsubseteq}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isasymsqsubseteq}\ z}.
+ \isa{{\isasymlbrakk}x\ {\isasymsqsubseteq}\ y{\isacharsemicolon}\ y\ {\isasymsqsubseteq}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isasymsqsubseteq}\ z} in fact means
+ \isa{{\isasymAnd}x\ y\ z{\isachardot}\ {\isasymlbrakk}x\ {\isasymsqsubseteq}\ y{\isacharsemicolon}\ y\ {\isasymsqsubseteq}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isasymsqsubseteq}\ z}.
Two commands are provided to inspect locales:
\isakeyword{print\_locales} lists the names of all locales of the
current theory; \isakeyword{print\_locale}~$n$ prints the parameters
- and assumptions of locale $n$; \isakeyword{print\_locale!}~$n$
- additionally outputs the conclusions. We may inspect the new locale
+ and assumptions of locale $n$; the variation \isakeyword{print\_locale!}~$n$
+ additionally outputs the conclusions that are stored in the locale.
+ We may inspect the new locale
by issuing \isakeyword{print\_locale!} \isa{partial{\isacharunderscore}order}. The output
is the following list of context elements.
-
+\begin{small}
\begin{alltt}
\isakeyword{fixes} le :: "'a \(\Rightarrow\) 'a \(\Rightarrow\) bool" (\isakeyword{infixl} "\(\sqsubseteq\)" 50)
\isakeyword{assumes} "partial_order op \(\sqsubseteq\)"
@@ -109,25 +111,30 @@
\isakeyword{and}
trans [trans] = `\(\isasymlbrakk\)?x \(\sqsubseteq\) ?y; ?y \(\sqsubseteq\) ?z\(\isasymrbrakk\) \(\Longrightarrow\) ?x \(\sqsubseteq\) ?z`
\end{alltt}
-
+\end{small}
The keyword \isakeyword{notes} denotes a conclusion element. There
- is only a single assumption \isa{partial{\isacharunderscore}order\ op\ {\isasymsqsubseteq}} in the
- output. The locale declaration has introduced the predicate \isa{partial{\isacharunderscore}order} to the theory. The predicate is called \emph{locale
- predicate} of the locale. Its definition may be inspected by
- issuing \isakeyword{thm} \isa{partial{\isacharunderscore}order{\isacharunderscore}def}:
+ is one conclusion, which was added automatically. Instead, there is
+ only one assumption, namely \isa{partial{\isacharunderscore}order\ op\ {\isasymsqsubseteq}}. The locale
+ declaration has introduced the predicate \isa{partial{\isacharunderscore}order} to the theory. This predicate is the
+ \emph{locale predicate}. Its definition may be inspected by
+ issuing \isakeyword{thm} \isa{partial{\isacharunderscore}order{\isacharunderscore}def}.
\begin{isabelle}%
\ \ partial{\isacharunderscore}order\ {\isacharquery}le\ {\isasymequiv}\isanewline
\isaindent{\ \ }{\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}le\ x\ x{\isacharparenright}\ {\isasymand}\isanewline
\isaindent{\ \ }{\isacharparenleft}{\isasymforall}x\ y{\isachardot}\ {\isacharquery}le\ x\ y\ {\isasymlongrightarrow}\ {\isacharquery}le\ y\ x\ {\isasymlongrightarrow}\ x\ {\isacharequal}\ y{\isacharparenright}\ {\isasymand}\isanewline
\isaindent{\ \ }{\isacharparenleft}{\isasymforall}x\ y\ z{\isachardot}\ {\isacharquery}le\ x\ y\ {\isasymlongrightarrow}\ {\isacharquery}le\ y\ z\ {\isasymlongrightarrow}\ {\isacharquery}le\ x\ z{\isacharparenright}%
\end{isabelle}
- The original assumptions have been turned into conclusions and are
+ In our example, this is a unary predicate over the parameter of the
+ locale. It is equivalent to the original assumptions, which have
+ been turned into conclusions and are
available as theorems in the context of the locale. The names and
attributes from the locale declaration are associated to these
theorems and are effective in the context of the locale.
- Each locale theorem has a \emph{foundational theorem} as counterpart
- in the theory. For the transitivity theorem, this is \isa{partial{\isacharunderscore}order{\isachardot}trans}:
+ Each conclusion has a \emph{foundational theorem} as counterpart
+ in the theory. Technically, this is simply the theorem composed
+ of context and conclusion. For the transitivity theorem, this is
+ \isa{partial{\isacharunderscore}order{\isachardot}trans}:
\begin{isabelle}%
\ \ partial{\isacharunderscore}order\ {\isacharquery}le\ {\isasymequiv}\isanewline
\isaindent{\ \ }{\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}le\ x\ x{\isacharparenright}\ {\isasymand}\isanewline
@@ -137,7 +144,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Extending the Locale%
+\isamarkupsubsection{Targets: Extending Locales%
}
\isamarkuptrue%
%
@@ -147,7 +154,7 @@
In the following, \isakeyword{definition} and
\isakeyword{theorem} are illustrated.
Table~\ref{tab:commands-with-target} lists Isar commands that accept
- a target. There are various ways of specifying the target. A
+ a target. Isar provides various ways of specifying the target. A
target for a single command may be indicated with keyword
\isakeyword{in} in the following way:
@@ -178,19 +185,20 @@
\ \ \ \ \isakeyword{where}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymsqsubset}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymsqsubseteq}\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
The strict order \isa{less} with infix
- syntax \isa{{\isasymsqsubset}} is
- defined in terms of the locale parameter \isa{le} and the general
- equality. The definition generates a \emph{foundational constant}
+ syntax~\isa{{\isasymsqsubset}} is
+ defined in terms of the locale parameter~\isa{le} and the general
+ equality of the object logic we work in. The definition generates a
+ \emph{foundational constant}
\isa{partial{\isacharunderscore}order{\isachardot}less} with definition \isa{partial{\isacharunderscore}order{\isachardot}less{\isacharunderscore}def}:
\begin{isabelle}%
\ \ partial{\isacharunderscore}order\ {\isacharquery}le\ {\isasymLongrightarrow}\isanewline
\isaindent{\ \ }partial{\isacharunderscore}order{\isachardot}less\ {\isacharquery}le\ {\isacharquery}x\ {\isacharquery}y\ {\isacharequal}\ {\isacharparenleft}{\isacharquery}le\ {\isacharquery}x\ {\isacharquery}y\ {\isasymand}\ {\isacharquery}x\ {\isasymnoteq}\ {\isacharquery}y{\isacharparenright}%
\end{isabelle}
At the same time, the locale is extended by syntax transformations
- hiding this construction in the context of the locale. In the
- context of the locale, the abbreviation \isa{less} is available for
+ hiding this construction in the context of the locale. Here, the
+ abbreviation \isa{less} is available for
\isa{partial{\isacharunderscore}order{\isachardot}less\ le}, and it is printed
- and parsed as infix \isa{{\isasymsqsubset}}. Finally, the theorem \isa{less{\isacharunderscore}def} is added to the locale:
+ and parsed as infix~\isa{{\isasymsqsubset}}. Finally, the conclusion \isa{less{\isacharunderscore}def} is added to the locale:
\begin{isabelle}%
\ \ {\isacharparenleft}{\isacharquery}x\ {\isasymsqsubset}\ {\isacharquery}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharquery}x\ {\isasymsqsubseteq}\ {\isacharquery}y\ {\isasymand}\ {\isacharquery}x\ {\isasymnoteq}\ {\isacharquery}y{\isacharparenright}%
\end{isabelle}%
@@ -223,8 +231,8 @@
\endisadelimvisible
%
\begin{isamarkuptext}%
-In the context of the proof, assumptions and theorems of the
- locale may be used. Attributes are effective: \isa{anti{\isacharunderscore}sym} was
+In the context of the proof, conclusions of the
+ locale may be used like theorems. Attributes are effective: \isa{anti{\isacharunderscore}sym} was
declared as introduction rule, hence it is in the context's set of
rules used by the classical reasoner by default.%
\end{isamarkuptext}%
@@ -297,7 +305,7 @@
\ is{\isacharunderscore}inf{\isacharunderscore}uniq{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}is{\isacharunderscore}inf\ x\ y\ i{\isacharsemicolon}\ is{\isacharunderscore}inf\ x\ y\ i{\isacharprime}{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharequal}\ i{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
-\ \ %
+\ \ \ \ %
\endisadelimproof
%
\isatagproof
@@ -414,7 +422,7 @@
\ is{\isacharunderscore}sup{\isacharunderscore}uniq{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}is{\isacharunderscore}sup\ x\ y\ s{\isacharsemicolon}\ is{\isacharunderscore}sup\ x\ y\ s{\isacharprime}{\isasymrbrakk}\ {\isasymLongrightarrow}\ s\ {\isacharequal}\ s{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
-\ \ %
+\ \ \ \ %
\endisadelimproof
%
\isatagproof
@@ -514,10 +522,11 @@
%
\begin{isamarkuptext}%
The syntax of the locale commands discussed in this tutorial is
- shown in Table~\ref{tab:commands}. The grammer is complete with the
- exception of additional context elements not discussed here. See the
- Isabelle/Isar Reference Manual~\cite{IsarRef}
- for full documentation.%
+ shown in Table~\ref{tab:commands}. The grammar is complete with the
+ exception of the context elements \isakeyword{constrains} and
+ \isakeyword{defines}, which are provided for backward
+ compatibility. See the Isabelle/Isar Reference
+ Manual~\cite{IsarRef} for full documentation.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -554,7 +563,6 @@
\ \ \isacommand{definition}\isamarkupfalse%
\isanewline
\ \ \ \ meet\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqinter}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}x\ {\isasymsqinter}\ y\ {\isacharequal}\ {\isacharparenleft}THE\ inf{\isachardot}\ is{\isacharunderscore}inf\ x\ y\ inf{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
\ \ \isacommand{definition}\isamarkupfalse%
\isanewline
\ \ \ \ join\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqunion}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{5}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}x\ {\isasymsqunion}\ y\ {\isacharequal}\ {\isacharparenleft}THE\ sup{\isachardot}\ is{\isacharunderscore}sup\ x\ y\ sup{\isacharparenright}{\isachardoublequoteclose}\isanewline
@@ -1116,7 +1124,8 @@
\ \ \isacommand{end}\isamarkupfalse%
%
\begin{isamarkuptext}%
-Locales for total orders and distributive lattices follow for
+Locales for total orders and distributive lattices follow to
+ establish a sufficiently rich landscape of locales for
further examples in this tutorial. Each comes with an example
theorem.%
\end{isamarkuptext}%
@@ -1193,13 +1202,13 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-The locale hierachy obtained through these declarations is shown in
+The locale hierarchy obtained through these declarations is shown in
Figure~\ref{fig:lattices}(a).
\begin{figure}
\hrule \vspace{2ex}
\begin{center}
-\subfigure[Declared hierachy]{
+\subfigure[Declared hierarchy]{
\begin{tikzpicture}
\node (po) at (0,0) {\isa{partial{\isacharunderscore}order}};
\node (lat) at (-1.5,-1) {\isa{lattice}};
@@ -1258,20 +1267,20 @@
specifications of the locales.
The first from of interpretation we will consider in this tutorial
- is provided by the \isakeyword{sublocale} command, which enables to
+ is provided by the \isakeyword{sublocale} command. It enables to
modify the import hierarchy to reflect the \emph{logical} relation
between locales.
Consider the locale hierarchy from Figure~\ref{fig:lattices}(a).
- Total orders are lattices, although this is not reflected in the
- import hierarchy, and definitions, theorems and other conclusions
+ Total orders are lattices, although this is not reflected here, and
+ definitions, theorems and other conclusions
from \isa{lattice} are not available in \isa{total{\isacharunderscore}order}. To
obtain the situation in Figure~\ref{fig:lattices}(b), it is
sufficient to add the conclusions of the latter locale to the former.
The \isakeyword{sublocale} command does exactly this.
The declaration \isakeyword{sublocale} $l_1
\subseteq l_2$ causes locale $l_2$ to be \emph{interpreted} in the
- context of $l_1$. All conclusions of $l_2$ are made
+ context of $l_1$. This means that all conclusions of $l_2$ are made
available in $l_1$.
Of course, the change of hierarchy must be supported by a theorem
@@ -1298,9 +1307,8 @@
Now the
locale predicate needs to be unfolded --- for example, using its
definition or by introduction rules
- provided by the locale package. The locale package provides the
- methods \isa{intro{\isacharunderscore}locales} and \isa{unfold{\isacharunderscore}locales} to automate
- this. They are aware of the
+ provided by the locale package. For automation, the locale package
+ provides the methods \isa{intro{\isacharunderscore}locales} and \isa{unfold{\isacharunderscore}locales}. They are aware of the
current context and dependencies between locales and automatically
discharge goals implied by these. While \isa{unfold{\isacharunderscore}locales}
always unfolds locale predicates to assumptions, \isa{intro{\isacharunderscore}locales} only unfolds definitions along the locale
@@ -1394,7 +1402,7 @@
\endisadelimvisible
%
\begin{isamarkuptext}%
-Similarly, we may establsih that total orders are distributive
+Similarly, we may establish that total orders are distributive
lattices with a second \isakeyword{sublocale} statement.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -1402,7 +1410,7 @@
\ total{\isacharunderscore}order\ {\isasymsubseteq}\ distrib{\isacharunderscore}lattice\isanewline
%
\isadelimproof
-\ \ %
+\ \ \ \ %
\endisadelimproof
%
\isatagproof
@@ -1490,7 +1498,8 @@
The sublocale relation is transitive --- that is, propagation takes
effect along chains of sublocales. Even cycles in the sublocale relation are
supported, as long as these cycles do not lead to infinite chains.
- For details, see \cite{Ballarin2006a}.%
+ Details are discussed in the technical report \cite{Ballarin2006a}.
+ See also Section~\ref{sec:infinite-chains} of this tutorial.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Locales/Locales/document/Examples1.tex Thu Oct 15 22:22:08 2009 +0200
+++ b/doc-src/Locales/Locales/document/Examples1.tex Sat Oct 17 22:58:18 2009 +0200
@@ -18,13 +18,18 @@
%
\endisadelimtheory
%
+\begin{isamarkuptext}%
+\vspace{-5ex}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsection{Use of Locales in Theories and Proofs
\label{sec:interpretation}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Locales can also be interpreted in the contexts of theories and
+Locales can be interpreted in the contexts of theories and
structured proofs. These interpretations are dynamic, too.
Conclusions of locales will be propagated to the current theory or
the current proof context.%
@@ -37,10 +42,10 @@
Section~\ref{sec:local-interpretation}.
As an example, consider the type of integers \isa{int}. The
- relation \isa{op\ {\isasymle}} is a total order over \isa{int},
- divisibility \isa{op\ dvd} forms a distributive lattice. We start with the
- interpretation that \isa{op\ {\isasymle}} is a partial order. The facilities of
- the interpretation command are explored gradually in three versions.%
+ relation \isa{op\ {\isasymle}} is a total order over \isa{int}. We start
+ with the interpretation that \isa{op\ {\isasymle}} is a partial order. The
+ facilities of the interpretation command are explored gradually in
+ three versions.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -72,9 +77,9 @@
white-space-separated list of terms, which provide a full
instantiation of the locale parameters. The parameters are referred
to by order of declaration, which is also the order in which
- \isakeyword{print\_locale} outputs them.
-
-[TODO: Introduce morphisms. Reference to \ref{sec:locale-expressions}.]
+ \isakeyword{print\_locale} outputs them. The locale has only a
+ single parameter, hence the list of instantiation terms is a
+ singleton.
The command creates the goal
\begin{isabelle}%
@@ -99,7 +104,7 @@
\begin{isabelle}%
\ \ {\isasymlbrakk}{\isacharquery}x\ {\isasymle}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymle}\ {\isacharquery}z%
\end{isabelle}
- It is not possible to reference this theorem simply as \isa{trans}, which prevents unwanted hiding of existing theorems of the
+ It is not possible to reference this theorem simply as \isa{trans}. This prevents unwanted hiding of existing theorems of the
theory by an interpretation.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -112,7 +117,7 @@
Not only does the above interpretation qualify theorem names.
The prefix \isa{int} is applied to all names introduced in locale
conclusions including names introduced in definitions. The
- qualified name \isa{int{\isachardot}less} refers to
+ qualified name \isa{int{\isachardot}less} is short for
the interpretation of the definition, which is \isa{partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}}.
Qualified name and expanded form may be used almost
interchangeably.%
@@ -129,7 +134,7 @@
In order to allow for the desired replacement, interpretation
accepts \emph{equations} in addition to the parameter instantiation.
These follow the locale expression and are indicated with the
- keyword \isakeyword{where}. The revised interpretation follows.%
+ keyword \isakeyword{where}. This is the revised interpretation:%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Locales/Locales/document/Examples2.tex Thu Oct 15 22:22:08 2009 +0200
+++ b/doc-src/Locales/Locales/document/Examples2.tex Sat Oct 17 22:58:18 2009 +0200
@@ -34,11 +34,12 @@
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharminus}%
\begin{isamarkuptxt}%
-\normalsize The goals are \begin{isabelle}%
+\normalsize The goals are now:
+ \begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ partial{\isacharunderscore}order\ op\ {\isasymle}\isanewline
\ {\isadigit{2}}{\isachardot}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ x\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}%
\end{isabelle}
- The proof that \isa{{\isasymle}} is a partial order is as above.%
+ The proof that~\isa{{\isasymle}} is a partial order is as above.%
\end{isamarkuptxt}%
\isamarkuptrue%
\ \ \ \ \isacommand{show}\isamarkupfalse%
@@ -67,7 +68,7 @@
%
\begin{isamarkuptext}%
Note that the above proof is not in the context of the
- interpreted locale. Hence, the correct interpretation of \isa{partial{\isacharunderscore}order{\isachardot}less{\isacharunderscore}def} is obtained manually with \isa{OF}.%
+ interpreted locale. Hence, the premise of \isa{partial{\isacharunderscore}order{\isachardot}less{\isacharunderscore}def} is discharged manually with \isa{OF}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Locales/Locales/document/Examples3.tex Thu Oct 15 22:22:08 2009 +0200
+++ b/doc-src/Locales/Locales/document/Examples3.tex Sat Oct 17 22:58:18 2009 +0200
@@ -9,30 +9,15 @@
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Examples{\isadigit{3}}\isanewline
-\isakeyword{imports}\ Examples\ {\isachardoublequoteopen}{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}HOL{\isacharslash}Number{\isacharunderscore}Theory{\isacharslash}UniqueFactorization{\isachardoublequoteclose}\isanewline
+\isakeyword{imports}\ Examples\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
-\isanewline
%
\endisadelimtheory
%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isataginvisible
-\isacommand{hide}\isamarkupfalse%
-\ const\ Lattices{\isachardot}lattice%
-\endisataginvisible
-{\isafoldinvisible}%
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
\begin{isamarkuptext}%
\vspace{-5ex}%
\end{isamarkuptext}%
@@ -48,7 +33,7 @@
order for the integers was used in the second goal to
discharge the premise in the definition of \isa{op\ {\isasymsqsubset}}. In
general, proofs of the equations not only may involve definitions
- fromthe interpreted locale but arbitrarily complex arguments in the
+ from the interpreted locale but arbitrarily complex arguments in the
context of the locale. Therefore is would be convenient to have the
interpreted locale conclusions temporary available in the proof.
This can be achieved by a locale interpretation in the proof body.
@@ -96,7 +81,7 @@
also obtained in the interpretation from Section~\ref{sec:po-first},
and \isa{int{\isachardot}less{\isacharunderscore}def} may directly be used to unfold the
definition. Theorems from the local interpretation disappear after
- leaving the proof context --- that is, after the closing a
+ leaving the proof context --- that is, after the succeeding
\isakeyword{next} or \isakeyword{qed} statement.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -107,11 +92,12 @@
%
\begin{isamarkuptext}%
Further interpretations are necessary for
- the other locales. In \isa{lattice} the operations \isa{{\isasymsqinter}} and
- \isa{{\isasymsqunion}} are substituted by \isa{min} and
- \isa{max}. The entire proof for the
+ the other locales. In \isa{lattice} the operations~\isa{{\isasymsqinter}}
+ and~\isa{{\isasymsqunion}} are substituted by \isa{min}
+ and \isa{max}. The entire proof for the
interpretation is reproduced to give an example of a more
- elaborate interpretation proof.%
+ elaborate interpretation proof. Note that the equations are named
+ so they can be used in a later example.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -122,8 +108,8 @@
\isatagvisible
\isacommand{interpretation}\isamarkupfalse%
\ int{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{where}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ max\ x\ y{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{where}\ int{\isacharunderscore}min{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \isakeyword{and}\ int{\isacharunderscore}max{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ max\ x\ y{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharminus}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
@@ -137,22 +123,25 @@
\ unfold{\isacharunderscore}locales%
\begin{isamarkuptxt}%
\normalsize hence only the lattice axioms remain to be
- shown: \begin{isabelle}%
+ shown.
+ \begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ {\isasymexists}inf{\isachardot}\ partial{\isacharunderscore}order{\isachardot}is{\isacharunderscore}inf\ op\ {\isasymle}\ x\ y\ inf\isanewline
\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ {\isasymexists}sup{\isachardot}\ partial{\isacharunderscore}order{\isachardot}is{\isacharunderscore}sup\ op\ {\isasymle}\ x\ y\ sup%
-\end{isabelle} After unfolding \isa{is{\isacharunderscore}inf} and
- \isa{is{\isacharunderscore}sup},%
+\end{isabelle}
+ By \isa{is{\isacharunderscore}inf} and \isa{is{\isacharunderscore}sup},%
\end{isamarkuptxt}%
\isamarkuptrue%
\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}unfold\ int{\isachardot}is{\isacharunderscore}inf{\isacharunderscore}def\ int{\isachardot}is{\isacharunderscore}sup{\isacharunderscore}def{\isacharparenright}%
\begin{isamarkuptxt}%
-\normalsize the goals become \begin{isabelle}%
+\normalsize the goals are transformed to these
+ statements:
+ \begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ {\isasymexists}inf{\isasymle}x{\isachardot}\ inf\ {\isasymle}\ y\ {\isasymand}\ {\isacharparenleft}{\isasymforall}z{\isachardot}\ z\ {\isasymle}\ x\ {\isasymand}\ z\ {\isasymle}\ y\ {\isasymlongrightarrow}\ z\ {\isasymle}\ inf{\isacharparenright}\isanewline
\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ {\isasymexists}sup{\isasymge}x{\isachardot}\ y\ {\isasymle}\ sup\ {\isasymand}\ {\isacharparenleft}{\isasymforall}z{\isachardot}\ x\ {\isasymle}\ z\ {\isasymand}\ y\ {\isasymle}\ z\ {\isasymlongrightarrow}\ sup\ {\isasymle}\ z{\isacharparenright}%
\end{isabelle}
- This can be solved by Presburger arithmetic, which is contained
- in \isa{arith}.%
+ This is Presburger arithmetic, which can be solved by the
+ method \isa{arith}.%
\end{isamarkuptxt}%
\isamarkuptrue%
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
@@ -226,233 +215,30 @@
\end{tabular}
\end{center}
\hrule
-\caption{Interpreted theorems for \isa{{\isasymle}} on the integers.}
+\caption{Interpreted theorems for~\isa{{\isasymle}} on the integers.}
\label{tab:int-lattice}
\end{table}
\begin{itemize}
\item
Locale \isa{distrib{\isacharunderscore}lattice} was also interpreted. Since the
- locale hierarcy reflects that total orders are distributive
+ locale hierarchy reflects that total orders are distributive
lattices, the interpretation of the latter was inserted
automatically with the interpretation of the former. In general,
- interpretation of a locale will also interpret all locales further
- up in the hierarchy, regardless whether imported or proved via the
- \isakeyword{sublocale} command.
+ interpretation traverses the locale hierarchy upwards and interprets
+ all encountered locales, regardless whether imported or proved via
+ the \isakeyword{sublocale} command. Existing interpretations are
+ skipped avoiding duplicate work.
\item
- Theorem \isa{int{\isachardot}less{\isacharunderscore}total} makes use of \isa{op\ {\isacharless}}
+ The predicate \isa{op\ {\isacharless}} appears in theorem \isa{int{\isachardot}less{\isacharunderscore}total}
although an equation for the replacement of \isa{op\ {\isasymsqsubset}} was only
- given in the interpretation of \isa{partial{\isacharunderscore}order}. These
- equations are pushed downwards the hierarchy for related
- interpretations --- that is, for interpretations that share the
- instance for parameters they have in common.
-\end{itemize}
- In the next section, the divisibility relation on the natural
- numbers will be explored.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Interpretations for Divisibility%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-In this section, further examples of interpretations are
- presented. Impatient readers may skip this section at first
- reading.
-
- Divisibility on the natural numbers is a distributive lattice
- but not a total order. Interpretation again proceeds
- incrementally. In order to distinguish divisibility from the order
- relation $\le$, we use the qualifier \isa{nat{\isacharunderscore}dvd} for
- divisibility.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\ \ \isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharunderscore}dvd{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
-%
-\isadelimproof
-\ \ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\ {\isacharminus}\isanewline
-\ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}partial{\isacharunderscore}order\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
-\ unfold{\isacharunderscore}locales\ {\isacharparenleft}auto\ simp{\isacharcolon}\ dvd{\isacharunderscore}def{\isacharparenright}\isanewline
-\ \ \ \ \isacommand{then}\isamarkupfalse%
-\ \isacommand{interpret}\isamarkupfalse%
-\ nat{\isacharunderscore}dvd{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
-\isanewline
-\ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isachardot}less{\isacharunderscore}def{\isacharparenright}\isanewline
-\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ auto\isanewline
-\ \ \ \ \ \ \isacommand{done}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-Note that in Isabelle/HOL there is no operator for strict
- divisibility. Instead, we substitute \isa{x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y}.%
+ given in the interpretation of \isa{partial{\isacharunderscore}order}. The
+ interpretation equations are pushed downwards the hierarchy for
+ related interpretations --- that is, for interpretations that share
+ the instances of parameters they have in common.
+\end{itemize}%
\end{isamarkuptext}%
\isamarkuptrue%
-\ \ \isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharunderscore}dvd{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{where}\ nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq{\isacharcolon}\isanewline
-\ \ \ \ \ \ \ \ {\isachardoublequoteopen}lattice{\isachardot}meet\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq{\isacharcolon}\isanewline
-\ \ \ \ \ \ \ \ {\isachardoublequoteopen}lattice{\isachardot}join\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline
-%
-\isadelimproof
-\ \ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\ {\isacharminus}\isanewline
-\ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}lattice\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ unfold{\isacharunderscore}locales\isanewline
-\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isachardot}is{\isacharunderscore}inf{\isacharunderscore}def\ nat{\isacharunderscore}dvd{\isachardot}is{\isacharunderscore}sup{\isacharunderscore}def{\isacharparenright}\isanewline
-\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequoteopen}gcd\ x\ y{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
-\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ auto\ {\isacharbrackleft}{\isadigit{1}}{\isacharbrackright}\isanewline
-\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequoteopen}lcm\ x\ y{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
-\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}auto\ intro{\isacharcolon}\ lcm{\isacharunderscore}least{\isacharunderscore}nat{\isacharparenright}\isanewline
-\ \ \ \ \ \ \isacommand{done}\isamarkupfalse%
-\isanewline
-\ \ \ \ \isacommand{then}\isamarkupfalse%
-\ \isacommand{interpret}\isamarkupfalse%
-\ nat{\isacharunderscore}dvd{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
-\isanewline
-\ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}lattice{\isachardot}meet\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ expand{\isacharunderscore}fun{\isacharunderscore}eq{\isacharparenright}\isanewline
-\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isachardot}meet{\isacharunderscore}def{\isacharparenright}\isanewline
-\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}rule\ the{\isacharunderscore}equality{\isacharparenright}\isanewline
-\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isachardot}is{\isacharunderscore}inf{\isacharunderscore}def{\isacharparenright}\isanewline
-\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
-\ auto\isanewline
-\ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}lattice{\isachardot}join\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ expand{\isacharunderscore}fun{\isacharunderscore}eq{\isacharparenright}\isanewline
-\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isachardot}join{\isacharunderscore}def{\isacharparenright}\isanewline
-\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}rule\ the{\isacharunderscore}equality{\isacharparenright}\isanewline
-\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isachardot}is{\isacharunderscore}sup{\isacharunderscore}def{\isacharparenright}\isanewline
-\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}auto\ intro{\isacharcolon}\ lcm{\isacharunderscore}least{\isacharunderscore}nat\ iff{\isacharcolon}\ lcm{\isacharunderscore}unique{\isacharunderscore}nat{\isacharparenright}\isanewline
-\ \ \ \ \ \ \isacommand{done}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-The replacement equations \isa{nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq} and
- \isa{nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq} are theorems of current theories.
- They are named so that they can be used in the main part of the
- subsequent interpretation.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimvisible
-\ \ %
-\endisadelimvisible
-%
-\isatagvisible
-\isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharunderscore}dvd{\isacharcolon}\isanewline
-\ \ \ \ distrib{\isacharunderscore}lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ unfold{\isacharunderscore}locales%
-\begin{isamarkuptxt}%
-\normalsize \begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ y\ z{\isachardot}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }lattice{\isachardot}meet\ op\ dvd\ x\ {\isacharparenleft}lattice{\isachardot}join\ op\ dvd\ y\ z{\isacharparenright}\ {\isacharequal}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }lattice{\isachardot}join\ op\ dvd\ {\isacharparenleft}lattice{\isachardot}meet\ op\ dvd\ x\ y{\isacharparenright}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }{\isacharparenleft}lattice{\isachardot}meet\ op\ dvd\ x\ z{\isacharparenright}%
-\end{isabelle}
- Distributivity of lattice meet and join needs to be shown. This is
- distributivity of gcd and lcm, as becomes apparent when unfolding
- the replacement equations from the previous interpretation:%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
-\ nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq\ nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq%
-\begin{isamarkuptxt}%
-\normalsize \begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ y\ z{\isachardot}\ gcd\ x\ {\isacharparenleft}lcm\ y\ z{\isacharparenright}\ {\isacharequal}\ lcm\ {\isacharparenleft}gcd\ x\ y{\isacharparenright}\ {\isacharparenleft}gcd\ x\ z{\isacharparenright}%
-\end{isabelle}
- This is a result of number theory:%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}rule\ UniqueFactorization{\isachardot}gcd{\isacharunderscore}lcm{\isacharunderscore}distrib{\isacharunderscore}nat{\isacharparenright}%
-\endisatagvisible
-{\isafoldvisible}%
-%
-\isadelimvisible
-%
-\endisadelimvisible
-%
-\begin{isamarkuptext}%
-Theorems that are available in the theory after these
- interpretations are shown in Table~\ref{tab:nat-dvd-lattice}.
-
-\begin{table}
-\hrule
-\vspace{2ex}
-\begin{center}
-\begin{tabular}{l}
- \isa{nat{\isacharunderscore}dvd{\isachardot}less{\isacharunderscore}def} from locale \isa{partial{\isacharunderscore}order}: \\
- \quad \isa{{\isacharparenleft}{\isacharquery}x\ dvd\ {\isacharquery}y\ {\isasymand}\ {\isacharquery}x\ {\isasymnoteq}\ {\isacharquery}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharquery}x\ dvd\ {\isacharquery}y\ {\isasymand}\ {\isacharquery}x\ {\isasymnoteq}\ {\isacharquery}y{\isacharparenright}} \\
- \isa{nat{\isacharunderscore}dvd{\isachardot}meet{\isacharunderscore}left} from locale \isa{lattice}: \\
- \quad \isa{gcd\ {\isacharquery}x\ {\isacharquery}y\ dvd\ {\isacharquery}x} \\
- \isa{nat{\isacharunderscore}dvd{\isachardot}join{\isacharunderscore}distr} from locale \isa{distrib{\isacharunderscore}lattice}: \\
- \quad \isa{lcm\ {\isacharquery}x\ {\isacharparenleft}gcd\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ gcd\ {\isacharparenleft}lcm\ {\isacharquery}x\ {\isacharquery}y{\isacharparenright}\ {\isacharparenleft}lcm\ {\isacharquery}x\ {\isacharquery}z{\isacharparenright}} \\
-\end{tabular}
-\end{center}
-\hrule
-\caption{Interpreted theorems for \isa{dvd} on the natural numbers.}
-\label{tab:nat-dvd-lattice}
-\end{table}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Inspecting Interpretations of a Locale%
-}
-\isamarkuptrue%
%
\begin{isamarkuptext}%
The interpretations for a locale $n$ within the current
@@ -460,18 +246,20 @@
prints the list of instances of $n$, for which interpretations exist.
For example, \isakeyword{print\_interps} \isa{partial{\isacharunderscore}order}
outputs the following:
+\begin{small}
\begin{alltt}
int! : partial_order "op \(\le\)"
- nat_dvd! : partial_order "op dvd"
\end{alltt}
- The interpretation qualifiers on the left are decorated with an
- exclamation point, which means that they are mandatory. Qualifiers
+\end{small}
+ Of course, there is only one interpretation.
+ The interpretation qualifier on the left is decorated with an
+ exclamation point. This means that it is mandatory. Qualifiers
can either be \emph{mandatory} or \emph{optional}, designated by
``!'' or ``?'' respectively. Mandatory qualifiers must occur in a
name reference while optional ones need not. Mandatory qualifiers
- prevent accidental hiding of names, while optional qualifers can be
+ prevent accidental hiding of names, while optional qualifiers can be
more convenient to use. For \isakeyword{interpretation}, the
- default for qualifiers without an explicit designator is ``!''.%
+ default is ``!''.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -480,61 +268,59 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-A map \isa{{\isasymphi}} between partial orders \isa{{\isasymsqsubseteq}} and \isa{{\isasympreceq}}
+A map~\isa{{\isasymphi}} between partial orders~\isa{{\isasymsqsubseteq}} and~\isa{{\isasympreceq}}
is called order preserving if \isa{x\ {\isasymsqsubseteq}\ y} implies \isa{{\isasymphi}\ x\ {\isasympreceq}\ {\isasymphi}\ y}. This situation is more complex than those encountered so
far: it involves two partial orders, and it is desirable to use the
existing locale for both.
- A locale for order preserving maps requires three parameters: \isa{le} (\isakeyword{infixl}~\isa{{\isasymsqsubseteq}}), \isa{le{\isacharprime}}
- (\isakeyword{infixl}~\isa{{\isasympreceq}}) for the orders and \isa{{\isasymphi}} for the
- map.
+ A locale for order preserving maps requires three parameters: \isa{le}~(\isakeyword{infixl}~\isa{{\isasymsqsubseteq}}) and \isa{le{\isacharprime}}~(\isakeyword{infixl}~\isa{{\isasympreceq}}) for the orders and~\isa{{\isasymphi}}
+ for the map.
In order to reuse the existing locale for partial orders, which has
- the single parameter \isa{le}, it must be imported twice, once
- mapping its parameter to \isa{le} (\isakeyword{infixl}~\isa{{\isasymsqsubseteq}})
- from the new locale and once to \isa{le{\isacharprime}}
- (\isakeyword{infixl}~\isa{{\isasympreceq}}). This can be achieved with a locale
+ the single parameter~\isa{le}, it must be imported twice, once
+ mapping its parameter to~\isa{le} from the new locale and once
+ to~\isa{le{\isacharprime}}. This can be achieved with a compound locale
expression.
- A \emph{locale expression} is a sequence of \emph{locale instances}
- separated by ``$\textbf{+}$'' and followed by a \isakeyword{for}
+ In general, a locale expression is a sequence of \emph{locale instances}
+ separated by~``$\textbf{+}$'' and followed by a \isakeyword{for}
clause.
-An instance has the following format:
+ An instance has the following format:
\begin{quote}
\textit{qualifier} \textbf{:} \textit{locale-name}
\textit{parameter-instantiation}
\end{quote}
We have already seen locale instances as arguments to
\isakeyword{interpretation} in Section~\ref{sec:interpretation}.
- The qualifier serves to disambiguate the names from different
- instances of the same locale.
+ As before, the qualifier serves to disambiguate names from
+ different instances of the same locale. While in
+ \isakeyword{interpretation} qualifiers default to mandatory, in
+ import and in the \isakeyword{sublocale} command, they default to
+ optional.
- Since the parameters \isa{le} and \isa{le{\isacharprime}} are to be partial
+ Since the parameters~\isa{le} and~\isa{le{\isacharprime}} are to be partial
orders, our locale for order preserving maps will import the these
instances:
+\begin{small}
\begin{alltt}
le: partial_order le
le': partial_order le'
\end{alltt}
- For matter of convenience we choose the parameter names also as
- qualifiers. This is an arbitrary decision. Technically, qualifiers
+\end{small}
+ For matter of convenience we choose to name parameter names and
+ qualifiers alike. This is an arbitrary decision. Technically, qualifiers
and parameters are unrelated.
Having determined the instances, let us turn to the \isakeyword{for}
clause. It serves to declare locale parameters in the same way as
the context element \isakeyword{fixes} does. Context elements can
only occur after the import section, and therefore the parameters
- referred to inthe instances must be declared in the \isakeyword{for}
- clause.%
-\footnote{Since all parameters can be declared in the \isakeyword{for}
- clause, the context element \isakeyword{fixes} is not needed in
- locales. It is provided for compatibility with the long goals
- format, where the context element also occurs.}
- The \isakeyword{for} clause is also where the syntax of these
+ referred to in the instances must be declared in the \isakeyword{for}
+ clause. The \isakeyword{for} clause is also where the syntax of these
parameters is declared.
- Two context elements for the map parameter \isa{{\isasymphi}} and the
- assumptions that it is order perserving complete the locale
+ Two context elements for the map parameter~\isa{{\isasymphi}} and the
+ assumptions that it is order preserving complete the locale
declaration.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -548,21 +334,20 @@
Here are examples of theorems that are
available in the locale:
- \isa{hom{\isacharunderscore}le}: \isa{{\isacharquery}x\ {\isasymsqsubseteq}\ {\isacharquery}y\ {\isasymLongrightarrow}\ {\isasymphi}\ {\isacharquery}x\ {\isasympreceq}\ {\isasymphi}\ {\isacharquery}y}
+ \hspace*{1em}\isa{hom{\isacharunderscore}le}: \isa{{\isacharquery}x\ {\isasymsqsubseteq}\ {\isacharquery}y\ {\isasymLongrightarrow}\ {\isasymphi}\ {\isacharquery}x\ {\isasympreceq}\ {\isasymphi}\ {\isacharquery}y}
- \isa{le{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: \isa{{\isasymlbrakk}{\isacharquery}x\ {\isasymsqsubset}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasymsqsubseteq}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymsqsubset}\ {\isacharquery}z}
+ \hspace*{1em}\isa{le{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: \isa{{\isasymlbrakk}{\isacharquery}x\ {\isasymsqsubset}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasymsqsubseteq}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymsqsubset}\ {\isacharquery}z}
- \isa{le{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}:
+ \hspace*{1em}\isa{le{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}:
\begin{isabelle}%
-\ \ {\isasymlbrakk}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasympreceq}\ {\isacharquery}x\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\isanewline
-\isaindent{\ \ }{\isasymLongrightarrow}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasympreceq}\ {\isacharquery}x\ {\isacharquery}z%
+\ \ \ \ {\isasymlbrakk}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasympreceq}\ {\isacharquery}x\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\isanewline
+\isaindent{\ \ \ \ }{\isasymLongrightarrow}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasympreceq}\ {\isacharquery}x\ {\isacharquery}z%
\end{isabelle}
-
While there is infix syntax for the strict operation associated to
\isa{op\ {\isasymsqsubseteq}}, there is none for the strict version of \isa{op\ {\isasympreceq}}. The abbreviation \isa{less} with its infix syntax is only
available for the original instance it was declared for. We may
- introduce the abbreviation \isa{less{\isacharprime}} with infix syntax \isa{{\isasymprec}}
- with this declaration:%
+ introduce the abbreviation \isa{less{\isacharprime}} with infix syntax~\isa{{\isasymprec}}
+ with the following declaration:%
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{abbreviation}\isamarkupfalse%
@@ -577,51 +362,63 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Default Instantiations and Implicit Parameters%
+\begin{isamarkuptext}%
+There are short notations for locale expressions. These are
+ discussed in the following.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Default Instantiations%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-It is possible to omit parameter instantiations in a locale
- expression. In that case, the instantiation defaults to the name of
- the parameter itself. That is, the locale expression \isa{partial{\isacharunderscore}order} is short for \isa{partial{\isacharunderscore}order\ le}, since the
- locale's single parameter is \isa{le}. We took advantage of this
- short hand in the \isakeyword{sublocale} declarations of
+It is possible to omit parameter instantiations. The
+ instantiation then defaults to the name of
+ the parameter itself. For example, the locale expression \isa{partial{\isacharunderscore}order} is short for \isa{partial{\isacharunderscore}order\ le}, since the
+ locale's single parameter is~\isa{le}. We took advantage of this
+ in the \isakeyword{sublocale} declarations of
Section~\ref{sec:changing-the-hierarchy}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsubsection{Implicit Parameters \label{sec:implicit-parameters}%
+}
+\isamarkuptrue%
+%
\begin{isamarkuptext}%
In a locale expression that occurs within a locale
declaration, omitted parameters additionally extend the (possibly
empty) \isakeyword{for} clause.
- The \isakeyword{for} clause is a
- general construct of Isabelle/Isar to mark names from the preceding
- declaration as ``arbitrary but fixed''. This is necessary for
- example, if the name is already bound in a surrounding context. In
- a locale expression, names occurring in parameter instantiations
- should be bound by a \isakeyword{for} clause whenever these names
- are not introduced elsewhere in the context --- for example, on the
- left hand side of a \isakeyword{sublocale} declaration.
+ The \isakeyword{for} clause is a general construct of Isabelle/Isar
+ to mark names occurring in the preceding declaration as ``arbitrary
+ but fixed''. This is necessary for example, if the name is already
+ bound in a surrounding context. In a locale expression, names
+ occurring in parameter instantiations should be bound by a
+ \isakeyword{for} clause whenever these names are not introduced
+ elsewhere in the context --- for example, on the left hand side of a
+ \isakeyword{sublocale} declaration.
There is an exception to this rule in locale declarations, where the
- \isakeyword{for} clause servers to declare locale parameters. Here,
+ \isakeyword{for} clause serves to declare locale parameters. Here,
locale parameters for which no parameter instantiation is given are
implicitly added, with their mixfix syntax, at the beginning of the
\isakeyword{for} clause. For example, in a locale declaration, the
expression \isa{partial{\isacharunderscore}order} is short for
+\begin{small}
\begin{alltt}
partial_order le \isakeyword{for} le (\isakeyword{infixl} "\(\sqsubseteq\)" 50)\textrm{.}
\end{alltt}
- This short hand was used in the locale declarations of
+\end{small}
+ This short hand was used in the locale declarations throughout
Section~\ref{sec:import}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The following locale declarations provide more examples. A map
- \isa{{\isasymphi}} is a lattice homomorphism if it preserves meet and
+The following locale declarations provide more examples. A
+ map~\isa{{\isasymphi}} is a lattice homomorphism if it preserves meet and
join.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -632,13 +429,12 @@
\ \ \ \ \isakeyword{assumes}\ hom{\isacharunderscore}meet{\isacharcolon}\ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}x\ {\isasymsqinter}\ y{\isacharparenright}\ {\isacharequal}\ le{\isacharprime}{\isachardot}meet\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isakeyword{and}\ hom{\isacharunderscore}join{\isacharcolon}\ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}x\ {\isasymsqunion}\ y{\isacharparenright}\ {\isacharequal}\ le{\isacharprime}{\isachardot}join\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
-We omit the parameter instantiation in the first instance of
- \isa{lattice}. This causes the parameter \isa{le} to be added
- to the \isakeyword{for} clause, and the locale has parameters
- \isa{le} and \isa{le{\isacharprime}}.
+The parameter instantiation in the first instance of \isa{lattice} is omitted. This causes the parameter~\isa{le} to be
+ added to the \isakeyword{for} clause, and the locale has
+ parameters~\isa{le},~\isa{le{\isacharprime}} and, of course,~\isa{{\isasymphi}}.
Before turning to the second example, we complete the locale by
- provinding infix syntax for the meet and join operations of the
+ providing infix syntax for the meet and join operations of the
second lattice.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -651,17 +447,18 @@
\ \ \isacommand{end}\isamarkupfalse%
%
\begin{isamarkuptext}%
-The next example pushes the short hand facilities. A
- homomorphism is an endomorphism if both orders coincide.%
+The next example makes radical use of the short hand
+ facilities. A homomorphism is an endomorphism if both orders
+ coincide.%
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{locale}\isamarkupfalse%
\ lattice{\isacharunderscore}end\ {\isacharequal}\ lattice{\isacharunderscore}hom\ {\isacharunderscore}\ le%
\begin{isamarkuptext}%
-The notation \isa{{\isacharunderscore}} enables to omit a parameter in a
- positional instantiation. The omitted parameter, \isa{le} becomes
+The notation~\isa{{\isacharunderscore}} enables to omit a parameter in a
+ positional instantiation. The omitted parameter,~\isa{le} becomes
the parameter of the declared locale and is, in the following
- position used to instantiate the second parameter of \isa{lattice{\isacharunderscore}hom}. The effect is that of identifying the first in second
+ position, used to instantiate the second parameter of \isa{lattice{\isacharunderscore}hom}. The effect is that of identifying the first in second
parameter of the homomorphism locale.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -669,9 +466,9 @@
\begin{isamarkuptext}%
The inheritance diagram of the situation we have now is shown
in Figure~\ref{fig:hom}, where the dashed line depicts an
- interpretation which is introduced below. Renamings are
- indicated by $\sqsubseteq \mapsto \preceq$ etc. By looking at the
- inheritance diagram it would seem
+ interpretation which is introduced below. Parameter instantiations
+ are indicated by $\sqsubseteq \mapsto \preceq$ etc. By looking at
+ the inheritance diagram it would seem
that two identical copies of each of the locales \isa{partial{\isacharunderscore}order} and \isa{lattice} are imported by \isa{lattice{\isacharunderscore}end}. This is not the case! Inheritance paths with
identical morphisms are automatically detected and
the conclusions of the respective locales appear only once.
@@ -755,9 +552,236 @@
\isa{hom{\isacharunderscore}le}:
\begin{isabelle}%
\ \ {\isacharquery}x\ {\isasymsqsubseteq}\ {\isacharquery}y\ {\isasymLongrightarrow}\ {\isasymphi}\ {\isacharquery}x\ {\isasympreceq}\ {\isasymphi}\ {\isacharquery}y%
-\end{isabelle}%
+\end{isabelle}
+ This theorem will be useful in the following section.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Conditional Interpretation%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+There are situations where an interpretation is not possible
+ in the general case since the desired property is only valid if
+ certain conditions are fulfilled. Take, for example, the function
+ \isa{{\isasymlambda}i{\isachardot}\ n\ {\isacharasterisk}\ i} that scales its argument by a constant factor.
+ This function is order preserving (and even a lattice endomorphism)
+ with respect to \isa{op\ {\isasymle}} provided \isa{n\ {\isasymge}\ {\isadigit{0}}}.
+
+ It is not possible to express this using a global interpretation,
+ because it is in general unspecified whether~\isa{n} is
+ non-negative, but one may make an interpretation in an inner context
+ of a proof where full information is available.
+ This is not fully satisfactory either, since potentially
+ interpretations may be required to make interpretations in many
+ contexts. What is
+ required is an interpretation that depends on the condition --- and
+ this can be done with the \isakeyword{sublocale} command. For this
+ purpose, we introduce a locale for the condition.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ \isacommand{locale}\isamarkupfalse%
+\ non{\isacharunderscore}negative\ {\isacharequal}\isanewline
+\ \ \ \ \isakeyword{fixes}\ n\ {\isacharcolon}{\isacharcolon}\ int\isanewline
+\ \ \ \ \isakeyword{assumes}\ non{\isacharunderscore}neg{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymle}\ n{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+It is again convenient to make the interpretation in an
+ incremental fashion, first for order preserving maps, the for
+ lattice endomorphisms.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ \isacommand{sublocale}\isamarkupfalse%
+\ non{\isacharunderscore}negative\ {\isasymsubseteq}\isanewline
+\ \ \ \ \ \ order{\isacharunderscore}preserving\ {\isachardoublequoteopen}op\ {\isasymle}{\isachardoublequoteclose}\ {\isachardoublequoteopen}op\ {\isasymle}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymlambda}i{\isachardot}\ n\ {\isacharasterisk}\ i{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ \ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{using}\isamarkupfalse%
+\ non{\isacharunderscore}neg\ \isacommand{by}\isamarkupfalse%
+\ unfold{\isacharunderscore}locales\ {\isacharparenleft}rule\ mult{\isacharunderscore}left{\isacharunderscore}mono{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+While the proof of the previous interpretation
+ is straightforward from monotonicity lemmas for~\isa{op\ {\isacharasterisk}}, the
+ second proof follows a useful pattern.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimvisible
+\ \ %
+\endisadelimvisible
+%
+\isatagvisible
+\isacommand{sublocale}\isamarkupfalse%
+\ non{\isacharunderscore}negative\ {\isasymsubseteq}\ lattice{\isacharunderscore}end\ {\isachardoublequoteopen}op\ {\isasymle}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymlambda}i{\isachardot}\ n\ {\isacharasterisk}\ i{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{proof}\isamarkupfalse%
+\ {\isacharparenleft}unfold{\isacharunderscore}locales{\isacharcomma}\ unfold\ int{\isacharunderscore}min{\isacharunderscore}eq\ int{\isacharunderscore}max{\isacharunderscore}eq{\isacharparenright}%
+\begin{isamarkuptxt}%
+\normalsize Unfolding the locale predicates \emph{and} the
+ interpretation equations immediately yields two subgoals that
+ reflect the core conjecture.
+ \begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ n\ {\isacharasterisk}\ min\ x\ y\ {\isacharequal}\ min\ {\isacharparenleft}n\ {\isacharasterisk}\ x{\isacharparenright}\ {\isacharparenleft}n\ {\isacharasterisk}\ y{\isacharparenright}\isanewline
+\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ n\ {\isacharasterisk}\ max\ x\ y\ {\isacharequal}\ max\ {\isacharparenleft}n\ {\isacharasterisk}\ x{\isacharparenright}\ {\isacharparenleft}n\ {\isacharasterisk}\ y{\isacharparenright}%
+\end{isabelle}
+ It is now necessary to show, in the context of \isa{non{\isacharunderscore}negative}, that multiplication by~\isa{n} commutes with
+ \isa{min} and \isa{max}.%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{qed}\isamarkupfalse%
+\ {\isacharparenleft}auto\ simp{\isacharcolon}\ hom{\isacharunderscore}le{\isacharparenright}%
+\endisatagvisible
+{\isafoldvisible}%
+%
+\isadelimvisible
+%
+\endisadelimvisible
+%
+\begin{isamarkuptext}%
+The lemma \isa{hom{\isacharunderscore}le}
+ simplifies a proof that would have otherwise been lengthy and we may
+ consider making it a default rule for the simplifier:%
\end{isamarkuptext}%
\isamarkuptrue%
+\ \ \isacommand{lemmas}\isamarkupfalse%
+\ {\isacharparenleft}\isakeyword{in}\ order{\isacharunderscore}preserving{\isacharparenright}\ hom{\isacharunderscore}le\ {\isacharbrackleft}simp{\isacharbrackright}%
+\isamarkupsubsection{Avoiding Infinite Chains of Interpretations
+ \label{sec:infinite-chains}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Similar situations arise frequently in formalisations of
+ abstract algebra where it is desirable to express that certain
+ constructions preserve certain properties. For example, polynomials
+ over rings are rings, or --- an example from the domain where the
+ illustrations of this tutorial are taken from --- a partial order
+ may be obtained for a function space by point-wise lifting of the
+ partial order of the co-domain. This corresponds to the following
+ interpretation:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimvisible
+\ \ %
+\endisadelimvisible
+%
+\isatagvisible
+\isacommand{sublocale}\isamarkupfalse%
+\ partial{\isacharunderscore}order\ {\isasymsubseteq}\ f{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}{\isasymlambda}f\ g{\isachardot}\ {\isasymforall}x{\isachardot}\ f\ x\ {\isasymsqsubseteq}\ g\ x{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{oops}\isamarkupfalse%
+%
+\endisatagvisible
+{\isafoldvisible}%
+%
+\isadelimvisible
+%
+\endisadelimvisible
+%
+\begin{isamarkuptext}%
+Unfortunately this is a cyclic interpretation that leads to an
+ infinite chain, namely
+ \begin{isabelle}%
+\ \ partial{\isacharunderscore}order\ {\isasymsubseteq}\ partial{\isacharunderscore}order\ {\isacharparenleft}{\isasymlambda}f\ g{\isachardot}\ {\isasymforall}x{\isachardot}\ f\ x\ {\isasymsqsubseteq}\ g\ x{\isacharparenright}\ {\isasymsubseteq}\isanewline
+\isaindent{\ \ }\ \ partial{\isacharunderscore}order\ {\isacharparenleft}{\isasymlambda}f\ g{\isachardot}\ {\isasymforall}x\ y{\isachardot}\ f\ x\ y\ {\isasymsqsubseteq}\ g\ x\ y{\isacharparenright}\ {\isasymsubseteq}\ \ {\isasymdots}%
+\end{isabelle}
+ and the interpretation is rejected.
+
+ Instead it is necessary to declare a locale that is logically
+ equivalent to \isa{partial{\isacharunderscore}order} but serves to collect facts
+ about functions spaces where the co-domain is a partial order, and
+ to make the interpretation in its context:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ \isacommand{locale}\isamarkupfalse%
+\ fun{\isacharunderscore}partial{\isacharunderscore}order\ {\isacharequal}\ partial{\isacharunderscore}order\isanewline
+\isanewline
+\ \ \isacommand{sublocale}\isamarkupfalse%
+\ fun{\isacharunderscore}partial{\isacharunderscore}order\ {\isasymsubseteq}\isanewline
+\ \ \ \ \ \ f{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}{\isasymlambda}f\ g{\isachardot}\ {\isasymforall}x{\isachardot}\ f\ x\ {\isasymsqsubseteq}\ g\ x{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ \ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ unfold{\isacharunderscore}locales\ {\isacharparenleft}fast{\isacharcomma}rule{\isacharcomma}fast{\isacharcomma}blast\ intro{\isacharcolon}\ trans{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+It is quite common in abstract algebra that such a construction
+ maps a hierarchy of algebraic structures (or specifications) to a
+ related hierarchy. By means of the same lifting, a function space
+ is a lattice if its co-domain is a lattice:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ \isacommand{locale}\isamarkupfalse%
+\ fun{\isacharunderscore}lattice\ {\isacharequal}\ fun{\isacharunderscore}partial{\isacharunderscore}order\ {\isacharplus}\ lattice\isanewline
+\isanewline
+\ \ \isacommand{sublocale}\isamarkupfalse%
+\ fun{\isacharunderscore}lattice\ {\isasymsubseteq}\ f{\isacharcolon}\ lattice\ {\isachardoublequoteopen}{\isasymlambda}f\ g{\isachardot}\ {\isasymforall}x{\isachardot}\ f\ x\ {\isasymsqsubseteq}\ g\ x{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ \ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{proof}\isamarkupfalse%
+\ unfold{\isacharunderscore}locales\isanewline
+\ \ \ \ \isacommand{fix}\isamarkupfalse%
+\ f\ g\isanewline
+\ \ \ \ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}is{\isacharunderscore}inf\ {\isacharparenleft}{\isasymlambda}f\ g{\isachardot}\ {\isasymforall}x{\isachardot}\ f\ x\ {\isasymsqsubseteq}\ g\ x{\isacharparenright}\ f\ g\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ f\ x\ {\isasymsqinter}\ g\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
+\ {\isacharparenleft}rule\ is{\isacharunderscore}infI{\isacharparenright}\ \isacommand{apply}\isamarkupfalse%
+\ rule{\isacharplus}\ \isacommand{apply}\isamarkupfalse%
+\ {\isacharparenleft}drule\ spec{\isacharcomma}\ assumption{\isacharparenright}{\isacharplus}\ \isacommand{done}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymexists}inf{\isachardot}\ partial{\isacharunderscore}order{\isachardot}is{\isacharunderscore}inf\ {\isacharparenleft}{\isasymlambda}f\ g{\isachardot}\ {\isasymforall}x{\isachardot}\ f\ x\ {\isasymsqsubseteq}\ g\ x{\isacharparenright}\ f\ g\ inf{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
+\ fast\isanewline
+\ \ \isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{fix}\isamarkupfalse%
+\ f\ g\isanewline
+\ \ \ \ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}is{\isacharunderscore}sup\ {\isacharparenleft}{\isasymlambda}f\ g{\isachardot}\ {\isasymforall}x{\isachardot}\ f\ x\ {\isasymsqsubseteq}\ g\ x{\isacharparenright}\ f\ g\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ f\ x\ {\isasymsqunion}\ g\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
+\ {\isacharparenleft}rule\ is{\isacharunderscore}supI{\isacharparenright}\ \isacommand{apply}\isamarkupfalse%
+\ rule{\isacharplus}\ \isacommand{apply}\isamarkupfalse%
+\ {\isacharparenleft}drule\ spec{\isacharcomma}\ assumption{\isacharparenright}{\isacharplus}\ \isacommand{done}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymexists}sup{\isachardot}\ partial{\isacharunderscore}order{\isachardot}is{\isacharunderscore}sup\ {\isacharparenleft}{\isasymlambda}f\ g{\isachardot}\ {\isasymforall}x{\isachardot}\ f\ x\ {\isasymsqsubseteq}\ g\ x{\isacharparenright}\ f\ g\ sup{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
+\ fast\isanewline
+\ \ \isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
%
\isamarkupsection{Further Reading%
}
@@ -766,13 +790,13 @@
\begin{isamarkuptext}%
More information on locales and their interpretation is
available. For the locale hierarchy of import and interpretation
- dependencies see \cite{Ballarin2006a}; interpretations in theories
- and proofs are covered in \cite{Ballarin2006b}. In the latter, I
+ dependencies see~\cite{Ballarin2006a}; interpretations in theories
+ and proofs are covered in~\cite{Ballarin2006b}. In the latter, I
show how interpretation in proofs enables to reason about families
of algebraic structures, which cannot be expressed with locales
directly.
- Haftmann and Wenzel \cite{HaftmannWenzel2007} overcome a restriction
+ Haftmann and Wenzel~\cite{HaftmannWenzel2007} overcome a restriction
of axiomatic type classes through a combination with locale
interpretation. The result is a Haskell-style class system with a
facility to generate ML and Haskell code. Classes are sufficient for
@@ -782,13 +806,16 @@
on the other hand, do not.
The locales reimplementation for Isabelle 2009 provides, among other
- improvements, a clean intergration with Isabelle/Isar's local theory
- mechnisms, which are described in \cite{HaftmannWenzel2009}.
+ improvements, a clean integration with Isabelle/Isar's local theory
+ mechanisms, which are described in another paper by Haftmann and
+ Wenzel~\cite{HaftmannWenzel2009}.
- The original work of Kamm\"uller on locales \cite{KammullerEtAl1999}
- may be of interest from a historical perspective. The mathematical
- background on orders and lattices is taken from Jacobson's textbook
- on algebra \cite[Chapter~8]{Jacobson1985}.
+ The original work of Kamm\"uller on locales~\cite{KammullerEtAl1999}
+ may be of interest from a historical perspective. My previous
+ report on locales and locale expressions~\cite{Ballarin2004a}
+ describes a simpler form of expressions than available now and is
+ outdated. The mathematical background on orders and lattices is
+ taken from Jacobson's textbook on algebra~\cite[Chapter~8]{Jacobson1985}.
The sources of this tutorial, which include all proofs, are
available with the Isabelle distribution at
@@ -901,22 +928,26 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-\textbf{Revision History.} For the present third revision,
- which was completed in October 2009, much of the explanatory text
- has been rewritten. In addition, inheritance of interpretation
- equations, which was not available for Isabelle 2009, but in the
- meantime has been implemented, is illustrated. The second revision
- accommodates changes introduced by the locales reimplementation for
- Isabelle 2009. Most notably, in complex specifications
- (\emph{locale expressions}) renaming has been generalised to
- instantiation.%
+\textbf{Revision History.} For the present third revision of
+ the tutorial, much of the explanatory text
+ was rewritten. Inheritance of interpretation equations is
+ available with the forthcoming release of Isabelle, which at the
+ time of editing these notes is expected for the end of 2009.
+ The second revision accommodates changes introduced by the locales
+ reimplementation for Isabelle 2009. Most notably locale expressions
+ have been generalised from renaming to instantiation.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\begin{isamarkuptext}%
\textbf{Acknowledgements.} Alexander Krauss, Tobias Nipkow,
Randy Pollack, Christian Sternagel and Makarius Wenzel have made
- useful comments on earlier versions of this document.%
+ useful comments on earlier versions of this document. The section
+ on conditional interpretation was inspired by a number of e-mail
+ enquiries the author received from locale users, and which suggested
+ that this use case is important enough to deserve explicit
+ explanation. The term \emph{conditional interpretation} is due to
+ Larry Paulson.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Locales/Locales/document/root.bib Thu Oct 15 22:22:08 2009 +0200
+++ b/doc-src/Locales/Locales/document/root.bib Sat Oct 17 22:58:18 2009 +0200
@@ -42,6 +42,24 @@
year = 2006
}
+% TYPES 2003
+
+@inproceedings{Ballarin2004a,
+ author = "Clemens Ballarin",
+ title = "Locales and Locale Expressions in {Isabelle/Isar}",
+ pages = "34--50",
+ crossref = "BerardiEtAl2004"
+}
+
+@proceedings{BerardiEtAl2004,
+ editor = "Stefano Berardi and Mario Coppo and Ferruccio Damiani",
+ title = "Types for Proofs and Programs, TYPES 2003, Torino, Italy",
+ booktitle = "Types for Proofs and Programs, TYPES 2003, Torino, Italy",
+ publisher = "Springer",
+ series = "LNCS 3085",
+ year = 2004
+}
+
% TYPES 2008
@inproceedings{HaftmannWenzel2009,
--- a/doc-src/Locales/Locales/document/root.tex Thu Oct 15 22:22:08 2009 +0200
+++ b/doc-src/Locales/Locales/document/root.tex Sat Oct 17 22:58:18 2009 +0200
@@ -23,26 +23,26 @@
\begin{document}
-\title{Tutorial to Locales and Locale Interpretation \\[1ex]
- \large 2nd revision, for Isabelle 2009}
+\title{Tutorial to Locales and Locale Interpretation}
\author{Clemens Ballarin}
\date{}
\maketitle
\begin{abstract}
- Locales are Isabelle's mechanism for dealing with parametric theories.
- We present typical examples of locale specifications,
- along with interpretations between locales to change their
- hierarchic dependencies and interpretations to reuse locales in
- theory contexts and proofs.
+ Locales are Isabelle's approach for dealing with parametric
+ theories. They have been designed as a module system for a
+ theorem prover that can adequately represent the complex
+ inter-dependencies between structures found in abstract algebra, but
+ have proven fruitful also in other applications --- for example,
+ software verification.
- This tutorial is intended for locale novices; familiarity with
- Isabelle and Isar is presumed.
- The second revision accommodates changes introduced by the locales
- reimplementation for Isabelle 2009. Most notably, in complex
- specifications (\emph{locale expressions}) renaming has been
- generalised to instantiation.
+ Both design and implementation of locales have evolved considerably
+ since Kamm\"uller did his initial experiments. Today, locales
+ are a simple yet powerful extension of the Isar proof language.
+ The present tutorial covers all major facilities of locales. It is
+ intended for locale novices; familiarity with Isabelle and Isar is
+ presumed.
\end{abstract}
\parindent 0pt\parskip 0.5ex
--- a/doc-src/Locales/Locales/document/session.tex Thu Oct 15 22:22:08 2009 +0200
+++ b/doc-src/Locales/Locales/document/session.tex Sat Oct 17 22:58:18 2009 +0200
@@ -1,11 +1,3 @@
-\input{Primes.tex}
-
-\input{Cong.tex}
-
-\input{Multiset.tex}
-
-\input{UniqueFactorization.tex}
-
\input{Examples.tex}
\input{Examples1.tex}