Save current state of locales tutorial.
--- a/doc-src/Locales/Locales/Examples.thy Thu Oct 15 22:06:43 2009 +0200
+++ b/doc-src/Locales/Locales/Examples.thy Thu Oct 15 22:07:18 2009 +0200
@@ -1,5 +1,5 @@
theory Examples
-imports Main GCD
+imports Main
begin
hide %invisible const Lattices.lattice
@@ -57,16 +57,56 @@
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 {* The parameter of this locale is @{term le}, with infix syntax
- @{text \<sqsubseteq>}. There is an implicit type parameter @{typ "'a"}. It
- is not necessary to declare parameter types: most general types will
- be inferred from the context elements for all parameters.
+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.
+
+ Isabelle recognises undbound 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"}.
+
+ 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
+ by issuing \isakeyword{print\_locale!} @{term partial_order}. The output
+ is the following list of context elements.
- The above declaration not only introduces the locale, it also
- defines the \emph{locale predicate} @{term partial_order} with
- definition @{thm [source] partial_order_def}:
+\begin{alltt}
+ \isakeyword{fixes} le :: "'a \(\Rightarrow\) 'a \(\Rightarrow\) bool" (\isakeyword{infixl} "\(\sqsubseteq\)" 50)
+ \isakeyword{assumes} "partial_order op \(\sqsubseteq\)"
+ \isakeyword{notes} assumption
+ refl [intro, simp] = `?x \(\sqsubseteq\) ?x`
+ \isakeyword{and}
+ anti_sym [intro] = `\(\isasymlbrakk\)?x \(\sqsubseteq\) ?y; ?y \(\sqsubseteq\) ?x\(\isasymrbrakk\) \(\Longrightarrow\) ?x = ?y`
+ \isakeyword{and}
+ trans [trans] = `\(\isasymlbrakk\)?x \(\sqsubseteq\) ?y; ?y \(\sqsubseteq\) ?z\(\isasymrbrakk\) \(\Longrightarrow\) ?x \(\sqsubseteq\) ?z`
+\end{alltt}
+
+ 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}:
@{thm [display, indent=2] partial_order_def}
+ The original assumptions 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}:
+ @{thm [display, indent=2] partial_order_def}
+*}
+
+subsection {* Extending the Locale *}
+
+text {*
The specification of a locale is fixed, but its list of conclusions
may be extended through Isar commands that take a \emph{target} argument.
In the following, \isakeyword{definition} and
@@ -101,23 +141,25 @@
less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubset>" 50)
where "(x \<sqsubset> y) = (x \<sqsubseteq> y \<and> x \<noteq> y)"
-text {* A definition in a locale depends on the locale parameters.
- Here, a global constant @{term partial_order.less} is declared, which is lifted over the
- locale parameter @{term le}. Its definition is the global theorem
- @{thm [source] partial_order.less_def}:
+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}
+ @{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. That is,
- @{term "partial_order.less le"} is printed and parsed as infix
- @{text \<sqsubset>}. *}
+ hiding this construction in the context of the locale. In the
+ context of the locale, 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]
+ less_def} is added to the locale:
+ @{thm [display, indent=2] less_def}
+*}
-text (in partial_order) {* Finally, the conclusion of the definition
- is added to the locale, @{thm [source] less_def}:
- @{thm [display, indent=2] less_def}
- *}
-
-text {* As an example of a theorem statement in the locale, here is the
- derivation of a transitivity law. *}
+text {* The treatment of theorem statements is more straightforward.
+ As an example, here is the derivation of a transitivity law for the
+ strict order relation. *}
lemma (in partial_order) less_le_trans [trans]:
"\<lbrakk> x \<sqsubset> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubset> z"
@@ -128,6 +170,8 @@
declared as introduction rule, hence it is in the context's set of
rules used by the classical reasoner by default. *}
+subsection {* Context Blocks *}
+
text {* When working with locales, sequences of commands with the same
target are frequent. A block of commands, delimited by
\isakeyword{begin} and \isakeyword{end}, makes a theory-like style
@@ -139,7 +183,7 @@
This style of working is illustrated in the block below, where
notions of infimum and supremum for partial orders are introduced,
- together with theorems. *}
+ together with theorems about their uniqueness. *}
context partial_order begin
@@ -238,13 +282,7 @@
end
-text {* 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.
-
- The syntax of the locale commands discussed in this tutorial is
+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}
@@ -257,11 +295,13 @@
Algebraic structures are commonly defined by adding operations and
properties to existing structures. For example, partial orders
are extended to lattices and total orders. Lattices are extended to
- distributive lattices.
+ distributive lattices. *}
- With locales, this inheritance is achieved through \emph{import} of a
- locale. Import is a separate entity in the locale declaration. If
- present, it precedes the context elements.
+text {*
+ With locales, this kind of inheritance is achieved through
+ \emph{import} of locales. The import part of a locale declaration,
+ if present, precedes the context elements. Here is an example,
+ where partial orders are extended to lattices.
*}
locale lattice = partial_order +
@@ -270,8 +310,8 @@
begin
text {* These assumptions refer to the predicates for infimum
- and supremum defined in @{text partial_order}. We may now introduce
- the notions of meet and join. *}
+ and supremum defined for @{text partial_order} in the previous
+ section. We now introduce the notions of meet and join. *}
definition
meet (infixl "\<sqinter>" 70) where "x \<sqinter> y = (THE inf. is_inf x y inf)"
@@ -518,8 +558,9 @@
end
-text {* Locales for total orders and distributive lattices follow.
- Each comes with an example theorem. *}
+text {* Locales for total orders and distributive lattices follow for
+ further examples in this tutorial. Each comes with an example
+ theorem. *}
locale total_order = partial_order +
assumes total: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
@@ -543,7 +584,8 @@
qed
text {*
- The locale hierachy obtained through these declarations is shown in Figure~\ref{fig:lattices}(a).
+ The locale hierachy obtained through these declarations is shown in
+ Figure~\ref{fig:lattices}(a).
\begin{figure}
\hrule \vspace{2ex}
@@ -594,21 +636,50 @@
\label{sec:changing-the-hierarchy} *}
text {*
- Total orders are lattices. Hence, by deriving the lattice
- axioms for total orders, the hierarchy may be changed
- and @{text lattice} be placed between @{text partial_order}
- and @{text total_order}, as shown in Figure~\ref{fig:lattices}(b).
- Changes to the locale hierarchy may be declared
- with the \isakeyword{sublocale} command. *}
+ Locales enable to prove theorems abstractly, relative to
+ sets of assumptions. These theorems can then be used in other
+ contexts where the assumptions themselves, or
+ instances of the assumptions, are theorems. This form of theorem
+ reuse is called \emph{interpretation}. Locales generalise
+ interpretation from theorems to conclusions, enabling the reuse of
+ definitions and other constructs that are not part of the
+ 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
+ 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
+ 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
+ available in $l_1$.
+
+ Of course, the change of hierarchy must be supported by a theorem
+ that reflects, in our example, that total orders are indeed
+ lattices. Therefore the \isakeyword{sublocale} command generates a
+ goal, which must be discharged by the user. This is illustrated in
+ the following paragraphs. First the sublocale relation is stated.
+*}
sublocale %visible total_order \<subseteq> lattice
-txt {* This enters the context of locale @{text total_order}, in
- which the goal @{subgoals [display]} must be shown. First, the
- locale predicate needs to be unfolded --- for example using its
+txt {* \normalsize
+ This enters the context of locale @{text total_order}, in
+ which the goal @{subgoals [display]} must be shown.
+ Now the
+ locale predicate needs to be unfolded --- for example, using its
definition or by introduction rules
- provided by the locale package. The methods @{text intro_locales}
- and @{text unfold_locales} automate this. They are aware of the
+ 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
current context and dependencies between locales and automatically
discharge goals implied by these. While @{text unfold_locales}
always unfolds locale predicates to assumptions, @{text
@@ -618,22 +689,26 @@
is smaller.
For the current goal, we would like to get hold of
- the assumptions of @{text lattice}, hence @{text unfold_locales}
- is appropriate. *}
+ the assumptions of @{text lattice}, which need to be shown, hence
+ @{text unfold_locales} is appropriate. *}
proof unfold_locales
-txt {* Since both @{text lattice} and @{text total_order}
- inherit @{text partial_order}, the assumptions of the latter are
- discharged, and the only subgoals that remain are the assumptions
- introduced in @{text lattice} @{subgoals [display]}
- The proof for the first subgoal is *}
+txt {* \normalsize
+ Since the fact that both lattices and total orders are partial
+ orders is already reflected in the locale hierarchy, the assumptions
+ of @{text partial_order} are discharged automatically, and only the
+ assumptions introduced in @{text lattice} remain as subgoals
+ @{subgoals [display]}
+ The proof for the first subgoal is obtained by constructing an
+ infimum, whose existence is implied by totality. *}
fix x y
from total have "is_inf x y (if x \<sqsubseteq> y then x else y)"
by (auto simp: is_inf_def)
then show "\<exists>inf. is_inf x y inf" ..
-txt {* The proof for the second subgoal is analogous and not
+txt {* \normalsize
+ The proof for the second subgoal is analogous and not
reproduced here. *}
next %invisible
fix x y
@@ -641,7 +716,8 @@
by (auto simp: is_sup_def)
then show "\<exists>sup. is_sup x y sup" .. qed %visible
-text {* Similarly, total orders are distributive lattices. *}
+text {* Similarly, we may establsih that total orders are distributive
+ lattices with a second \isakeyword{sublocale} statement. *}
sublocale total_order \<subseteq> distrib_lattice
proof unfold_locales
@@ -666,6 +742,18 @@
qed
qed
-text {* The locale hierarchy is now as shown in Figure~\ref{fig:lattices}(c). *}
+text {* The locale hierarchy is now as shown in
+ Figure~\ref{fig:lattices}(c). *}
+
+text {*
+ Locale interpretation is \emph{dynamic}. The statement
+ \isakeyword{sublocale} $l_1 \subseteq l_2$ will not just add the
+ current conclusions of $l_2$ to $l_1$. Rather the dependency is
+ stored, and conclusions that will be
+ added to $l_2$ in future are automatically propagated to $l_1$.
+ 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}. *}
end
--- a/doc-src/Locales/Locales/Examples1.thy Thu Oct 15 22:06:43 2009 +0200
+++ b/doc-src/Locales/Locales/Examples1.thy Thu Oct 15 22:07:18 2009 +0200
@@ -2,35 +2,27 @@
imports Examples
begin
-section {* Use of Locales in Theories and Proofs *}
-
-text {* Locales enable to prove theorems abstractly, relative to
- sets of assumptions. These theorems can then be used in other
- contexts where the assumptions themselves, or
- instances of the assumptions, are theorems. This form of theorem
- reuse is called \emph{interpretation}.
+section {* Use of Locales in Theories and Proofs
+ \label{sec:interpretation} *}
- The changes of the locale
- hierarchy from the previous sections are examples of
- interpretations. The command \isakeyword{sublocale} $l_1
- \subseteq l_2$ is said to \emph{interpret} locale $l_2$ in the
- context of $l_1$. It causes all theorems of $l_2$ to be made
- available in $l_1$. The interpretation is \emph{dynamic}: not only
- theorems already present in $l_2$ are available in $l_1$. Theorems
- that will be added to $l_2$ in future will automatically be
- propagated to $l_1$.
-
+text {*
Locales can also be interpreted in the contexts of theories and
structured proofs. These interpretations are dynamic, too.
- Theorems added to locales will be propagated to theories.
- In this section the interpretation in
- theories is illustrated; interpretation in proofs is analogous.
+ Conclusions of locales will be propagated to the current theory or
+ the current proof context.%
+\footnote{Strictly speaking, only interpretation in theories is
+ dynamic since it is not possible to change locales or the locale
+ hierarchy from within a proof.}
+ The focus of this section is on
+ interpretation in theories, but we will also encounter
+ interpretations in proofs, in
+ Section~\ref{sec:local-interpretation}.
As an example, consider the type of natural numbers @{typ nat}. The
- relation @{text \<le>} is a total order over @{typ nat},
- divisibility @{text dvd} is a distributive lattice. We start with the
- interpretation that @{text \<le>} is a partial order. The facilities of
- the interpretation command are explored in three versions.
+ relation @{term "op \<le>"} is a total order over @{typ nat},
+ 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.
*}
@@ -38,45 +30,60 @@
\label{sec:po-first} *}
text {*
- In the most basic form, interpretation just replaces the locale
- parameters by terms. The following command interprets the locale
- @{text partial_order} in the global context of the theory. The
- parameter @{term le} is replaced by @{term "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"}. *}
+ The command \isakeyword{interpretation} is for the interpretation of
+ locale in theories. In the following example, the parameter of locale
+ @{text partial_order} is replaced by @{term "op \<le> :: nat \<Rightarrow> nat \<Rightarrow>
+ bool"} and the locale instance is interpreted in the current
+ theory. *}
interpretation %visible nat: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
-txt {* The locale name is succeeded by a \emph{parameter
- instantiation}. This is a list of terms, which refer to
- the parameters in the order of declaration in the locale. The
- locale name is preceded by an optional \emph{interpretation
- qualifier}, here @{text nat}.
+txt {* \normalsize
+ The argument of the command is a simple \emph{locale expression}
+ consisting of the name of the interpreted locale, which is
+ preceded by the qualifier @{text "nat:"} and succeeded by a
+ 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.
- The command creates the goal%
-\footnote{Note that @{text op} binds tighter than functions
- application: parentheses around @{text "op \<le>"} are not necessary.}
+[TODO: Introduce morphisms. Reference to \ref{sec:locale-expressions}.]
+
+ The command creates the goal
@{subgoals [display]} which can be shown easily:
*}
by unfold_locales auto
-text {* Now theorems from the locale are available in the theory,
- interpreted for natural numbers, for example @{thm [source]
- nat.trans}: @{thm [display, indent=2] nat.trans}
-
- The interpretation qualifier, @{text nat} in the example, is applied
- to all names processed by the interpretation. If a qualifer is
- given in the \isakeyword{interpretation} command, its use is
- mandatory when referencing the name. For example, the above theorem
- cannot be referred to simply by @{text trans}. This prevents
- unwanted hiding of theorems. *}
+text {* The effect of the command is that instances of all
+ conclusions of the locale are available in the theory, where names
+ are prefixed by the qualifier. For example, transitivity for @{typ
+ nat} is named @{thm [source] nat.trans} and is the following
+ theorem:
+ @{thm [display, indent=2] nat.trans}
+ It is not possible to reference this theorem simply as @{text
+ trans}, which prevents unwanted hiding of existing theorems of the
+ theory by an interpretation. *}
subsection {* Second Version: Replacement of Definitions *}
-text {* The above interpretation also creates the theorem
+text {* Not only does the above interpretation qualify theorem names.
+ The prefix @{text nat} is applied to all names introduced in locale
+ conclusions including names introduced in definitions. The
+ qualified name @{text nat.less} refers to
+ the interpretation of the definition, which is @{term nat.less}.
+ Qualified name and expanded form may be used almost
+ interchangeably.%
+\footnote{Since @{term "op \<le>"} is polymorphic, for @{term nat.less} a
+ more general type will be inferred than for @{text nat.less} which
+ is over type @{typ nat}.}
+ The latter is preferred on output, as for example in the theorem
@{thm [source] nat.less_le_trans}: @{thm [display, indent=2]
nat.less_le_trans}
- Here, @{term "partial_order.less (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"}
- represents the strict order, although @{text "<"} is the natural
- strict order for @{typ nat}. Interpretation allows to map concepts
- introduced by definitions in locales to the corresponding
- concepts of the theory. *}
+ Both notations for the strict order are not satisfactory. The
+ constant @{term "op <"} is the strict order for @{typ nat}.
+ 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.
+ *}
end
--- a/doc-src/Locales/Locales/Examples2.thy Thu Oct 15 22:06:43 2009 +0200
+++ b/doc-src/Locales/Locales/Examples2.thy Thu Oct 15 22:07:18 2009 +0200
@@ -1,27 +1,23 @@
theory Examples2
imports Examples
begin
-text {* This is achieved by unfolding suitable equations during
- interpretation. These equations are given after the keyword
- \isakeyword{where} and require proofs. The revised command
- that replaces @{text "\<sqsubset>"} by @{text "<"} is: *}
+text {* \vspace{-5ex} *}
+ interpretation %visible nat: partial_order "op \<le> :: [nat, nat] \<Rightarrow> bool"
+ where "partial_order.less op \<le> (x::nat) y = (x < y)"
+ proof -
+ txt {* \normalsize The goals are @{subgoals [display]}
+ The proof that @{text \<le>} is a partial order is as above. *}
+ show "partial_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
+ by unfold_locales auto
+ txt {* \normalsize The second goal is shown by unfolding the
+ definition of @{term "partial_order.less"}. *}
+ show "partial_order.less op \<le> (x::nat) y = (x < y)"
+ unfolding partial_order.less_def [OF `partial_order op \<le>`]
+ by auto
+ qed
-interpretation %visible nat: partial_order "op \<le> :: [nat, nat] \<Rightarrow> bool"
- where "partial_order.less op \<le> (x::nat) y = (x < y)"
-proof -
- txt {* The goals are @{subgoals [display]}
- The proof that @{text \<le>} is a partial order is as above. *}
- show "partial_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
- by unfold_locales auto
- txt {* The second goal is shown by unfolding the
- definition of @{term "partial_order.less"}. *}
- show "partial_order.less op \<le> (x::nat) y = (x < y)"
- unfolding partial_order.less_def [OF `partial_order op \<le>`]
- by auto
-qed
-
-text {* Note that the above proof is not in the context of a locale.
- Hence, the correct interpretation of @{text
+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}.
*}
end
--- a/doc-src/Locales/Locales/Examples3.thy Thu Oct 15 22:06:43 2009 +0200
+++ b/doc-src/Locales/Locales/Examples3.thy Thu Oct 15 22:07:18 2009 +0200
@@ -1,77 +1,86 @@
theory Examples3
-imports Examples
+imports Examples "~~/src/HOL/Number_Theory/UniqueFactorization"
begin
-subsection {* Third Version: Local Interpretation *}
+hide %invisible const Lattices.lattice
+ (* imported again through Number_Theory *)
+text {* \vspace{-5ex} *}
+subsection {* Third Version: Local Interpretation
+ \label{sec:local-interpretation} *}
-text {* In the above example, the fact that @{text \<le>} is a partial
- order for the natural numbers was used in the proof of the
- second goal. In general, proofs of the equations may involve
- theorems implied by the fact the assumptions of the instantiated
- locale hold for the instantiating structure. If these theorems have
- been shown abstractly in the locale they can be made available
- conveniently in the context through an auxiliary local interpretation (keyword
- \isakeyword{interpret}). This interpretation is inside the proof of the global
- interpretation. The third revision of the example illustrates this. *}
+text {* In the above example, the fact that @{term "op \<le>"} is a partial
+ order for the natural numbers 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
+ 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.
+ The command for local interpretations is \isakeyword{interpret}. We
+ repeat the example from the previous section to illustrate this. *}
-interpretation %visible nat: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
- where "partial_order.less op \<le> (x::nat) y = (x < y)"
-proof -
- show "partial_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
- by unfold_locales auto
- then interpret nat: partial_order "op \<le> :: [nat, nat] \<Rightarrow> bool" .
- show "partial_order.less op \<le> (x::nat) y = (x < y)"
- unfolding nat.less_def by auto
-qed
+ interpretation %visible nat: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
+ where "partial_order.less op \<le> (x::nat) y = (x < y)"
+ proof -
+ show "partial_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
+ by unfold_locales auto
+ then interpret nat: partial_order "op \<le> :: [nat, nat] \<Rightarrow> bool" .
+ show "partial_order.less op \<le> (x::nat) y = (x < y)"
+ unfolding nat.less_def by auto
+ qed
-text {* The inner interpretation does not require an elaborate new
- proof, it is immediate from the preceding fact and proved with
- ``.''. It enriches the local proof context by the very theorems
+text {* The inner interpretation is immediate from the preceding fact
+ and proved by assumption (Isar short hand ``.''). It enriches the
+ local proof context by the theorems
also obtained in the interpretation from Section~\ref{sec:po-first},
and @{text nat.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
- \isakeyword{qed} --- and are then replaced by those with the desired
- substitutions of the strict order. *}
+ leaving the proof context --- that is, after the closing a
+ \isakeyword{next} or \isakeyword{qed} statement. *}
subsection {* Further Interpretations *}
-text {* Further interpretations are necessary to reuse theorems from
+text {* Further interpretations are necessary for
the other locales. In @{text lattice} the operations @{text \<sqinter>} and
@{text \<squnion>} are substituted by @{term "min :: nat \<Rightarrow> nat \<Rightarrow> nat"} and
@{term "max :: nat \<Rightarrow> nat \<Rightarrow> nat"}. The entire proof for the
- interpretation is reproduced in order to give an example of a more
+ interpretation is reproduced to give an example of a more
elaborate interpretation proof. *}
-interpretation %visible nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
- where "lattice.meet op \<le> (x::nat) y = min x y"
- and "lattice.join op \<le> (x::nat) y = max x y"
-proof -
- show "lattice (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
- txt {* We have already shown that this is a partial order, *}
- apply unfold_locales
- txt {* hence only the lattice axioms remain to be shown: @{subgoals
- [display]} After unfolding @{text is_inf} and @{text is_sup}, *}
- apply (unfold nat.is_inf_def nat.is_sup_def)
- txt {* the goals become @{subgoals [display]} which can be solved
- by Presburger arithmetic. *}
- by arith+
- txt {* In order to show the equations, we put ourselves in a
- situation where the lattice theorems can be used in a convenient way. *}
- then interpret nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool" .
- show "lattice.meet op \<le> (x::nat) y = min x y"
- by (bestsimp simp: nat.meet_def nat.is_inf_def)
- show "lattice.join op \<le> (x::nat) y = max x y"
- by (bestsimp simp: nat.join_def nat.is_sup_def)
-qed
+ interpretation %visible nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
+ where "lattice.meet op \<le> (x::nat) y = min x y"
+ and "lattice.join op \<le> (x::nat) y = max x y"
+ proof -
+ show "lattice (op \<le> :: nat \<Rightarrow> nat \<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}, *}
+ apply (unfold nat.is_inf_def nat.is_sup_def)
+ txt {* \normalsize the goals become @{subgoals [display]}
+ This can be solved by Presburger arithmetic, which is contained
+ in @{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
+ convenient way. *}
+ then interpret nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool" .
+ show "lattice.meet op \<le> (x::nat) y = min x y"
+ by (bestsimp simp: nat.meet_def nat.is_inf_def)
+ show "lattice.join op \<le> (x::nat) y = max x y"
+ by (bestsimp simp: nat.join_def nat.is_sup_def)
+ qed
-text {* Next follows that @{text \<le>} is a total order. *}
+text {* Next follows that @{text "op \<le>"} is a total order, again for
+ the natural numbers. *}
-interpretation %visible nat: total_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
- by unfold_locales arith
+ interpretation %visible nat: total_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
+ by unfold_locales arith
text {* Theorems that are available in the theory at this point are shown in
- Table~\ref{tab:nat-lattice}.
+ Table~\ref{tab:nat-lattice}. Two points are worth noting:
\begin{table}
\hrule
@@ -93,113 +102,101 @@
\label{tab:nat-lattice}
\end{table}
- Note that since the locale hierarchy reflects that total orders are
- distributive lattices, an explicit interpretation of distributive
- lattices for the order relation on natural numbers is not neccessary.
-
- Why not push this idea further and just give the last interpretation
- as a single interpretation instead of the sequence of three? The
- reasons for this are twofold:
\begin{itemize}
\item
- Often it is easier to work in an incremental fashion, because later
- interpretations require theorems provided by earlier
- interpretations.
+ Locale @{text distrib_lattice} was also interpreted. Since the
+ locale hierarcy 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.
\item
- Assume that a definition is made in some locale $l_1$, and that $l_2$
- imports $l_1$. Let an equation for the definition be
- proved in an interpretation of $l_2$. The equation will be unfolded
- in interpretations of theorems added to $l_2$ or below in the import
- hierarchy, but not for theorems added above $l_2$.
- Hence, an equation interpreting a definition should always be given in
- an interpretation of the locale where the definition is made, not in
- an interpretation of a locale further down the hierarchy.
+ Theorem @{thm [source] nat.less_total} makes use of @{term "op <"}
+ 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.
\end{itemize}
+ In the next section, the divisibility relation on the natural
+ numbers will be explored.
*}
-subsection {* Lattice @{text "dvd"} on @{typ nat} *}
+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. *}
-text {* Divisibility on the natural numbers is a distributive lattice
- but not a total order. Interpretation again proceeds
- incrementally. *}
+ 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: 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
+ 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 {* Note that in Isabelle/HOL there is no symbol for strict
- divisibility. Instead, interpretation substitutes @{term "x dvd y \<and>
- x \<noteq> y"}. *}
+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 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)"
+ interpretation %visible nat_dvd:
+ distrib_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 {* Equations @{thm [source] nat_dvd_meet_eq} and @{thm [source]
- nat_dvd_join_eq} are used in the main part the subsequent
- interpretation. *}
-
-(*
-definition
- is_lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
- "is_lcm p m n \<longleftrightarrow> m dvd p \<and> n dvd p \<and>
- (\<forall>d. m dvd d \<longrightarrow> n dvd d \<longrightarrow> p dvd d)"
-
-lemma is_gcd: "is_lcm (lcm (m, n)) m n"
- by (simp add: is_lcm_def lcm_least)
-
-lemma gcd_lcm_distr_lemma:
- "[| is_gcd g1 x l1; is_lcm l1 y z; is_gcd g2 x y; is_gcd g3 x z |] ==> is_lcm g1 g2 g3"
-apply (unfold is_gcd_def is_lcm_def dvd_def)
-apply (clarsimp simp: mult_ac)
-apply (blast intro: mult_is_0)
-thm mult_is_0 [THEN iffD1]
-*)
-
-lemma %invisible gcd_lcm_distr:
- "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)" sorry
-
-interpretation %visible nat_dvd:
- distrib_lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
- apply unfold_locales
- txt {* @{subgoals [display]} *}
- apply (unfold nat_dvd_meet_eq nat_dvd_join_eq)
- txt {* @{subgoals [display]} *}
- apply (rule gcd_lcm_distr) done
-
+ 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}.
@@ -223,12 +220,27 @@
\end{table}
*}
-text {*
- The syntax of the interpretation commands is shown in
- Table~\ref{tab:commands}. The grammar refers to
- \textit{expression}, which stands for a \emph{locale} expression.
- Locale expressions are discussed in the following section.
- *}
+
+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{alltt}
+ nat! : 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
+ 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
+ more convenient to use. For \isakeyword{interpretation}, the
+ default for qualifiers without an explicit designator is ``!''.
+*}
section {* Locale Expressions \label{sec:expressions} *}
@@ -240,70 +252,81 @@
far: it involves two partial orders, and it is desirable to use the
existing locale for both.
- Inspecting the grammar of locale commands in
- Table~\ref{tab:commands} reveals that the import of a locale can be
- more than just a single locale. In general, the import is a
- \emph{locale expression}, which enables to combine locales
- and instantiate parameters. A locale expression is a sequence of
- locale \emph{instances} followed by an optional \isakeyword{for}
- clause. Each instance consists of a locale reference, which may be
- preceded by a qualifer and succeeded by instantiations of the
- parameters of that locale. Instantiations may be either positional
- or through explicit mappings of parameters to arguments.
+ 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.
+
+ 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
+ expression.
+
+ A \emph{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:
+\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.
- Using a locale expression, a locale for order
- preserving maps can be declared in the following way. *}
+ 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{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
+ 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
+ parameters is declared.
+
+ Two context elements for the map parameter @{text \<phi>} and the
+ assumptions that it is order perserving complete the locale
+ declaration. *}
locale order_preserving =
le: partial_order le + le': partial_order le'
for le (infixl "\<sqsubseteq>" 50) and le' (infixl "\<preceq>" 50) +
- fixes \<phi> :: "'a \<Rightarrow> 'b"
+ fixes \<phi>
assumes hom_le: "x \<sqsubseteq> y \<Longrightarrow> \<phi> x \<preceq> \<phi> y"
-text {* The second and third line contain the expression --- two
- instances of the partial order locale where the parameter is
- instantiated to @{text le}
- and @{text le'}, respectively. The \isakeyword{for} clause consists
- of parameter declarations and is similar to the context element
- \isakeyword{fixes}. The notable difference is that the
- \isakeyword{for} clause is part of the expression, and only
- parameters defined in the expression may occur in its instances.
+text (in order_preserving) {* Here are examples of theorems that are
+ available in the locale:
- Instances define \emph{morphisms} on locales. Their effect on the
- parameters is lifted to terms, propositions and theorems in the
- canonical way,
- and thus to the assumptions and conclusions of a locale. The
- assumption of a locale expression is the conjunction of the
- assumptions of the instances. The conclusions of a sequence of
- instances are obtained by appending the conclusions of the
- instances in the order of the sequence.
+ @{thm [source] hom_le}: @{thm hom_le}
- The qualifiers in the expression are already a familiar concept from
- the \isakeyword{interpretation} command
- (Section~\ref{sec:po-first}). Here, they serve to distinguish names
- (in particular theorem names) for the two partial orders within the
- locale. Qualifiers in the \isakeyword{locale} command (and in
- \isakeyword{sublocale}) default to optional --- that is, they need
- not occur in references to the qualified names. Here are examples
- of theorems in locale @{text order_preserving}: *}
-
-context %invisible order_preserving begin
-
-text {*
@{thm [source] le.less_le_trans}: @{thm le.less_le_trans}
- @{thm [source] hom_le}: @{thm hom_le}
- *}
+ @{thm [source] le'.less_le_trans}:
+ @{thm [display, indent=2] le'.less_le_trans}
-text {* The theorems for the partial order @{text \<preceq>}
- are qualified by @{text le'}. For example, @{thm [source]
- le'.less_le_trans}: @{thm [display, indent=2] le'.less_le_trans} *}
-
-end %invisible
-
-text {* This example reveals that there is no infix syntax for the
- strict operation associated with @{text \<preceq>}. This can be declared
- through an abbreviation. *}
+ 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: *}
abbreviation (in order_preserving)
less' (infixl "\<prec>" 50) where "less' \<equiv> partial_order.less le'"
@@ -312,33 +335,48 @@
@{thm [source] le'.less_le_trans}:
@{thm [display, indent=2] le'.less_le_trans} *}
-text (in order_preserving) {* Qualifiers not only apply to theorem names, but also to names
- introduced by definitions and abbreviations. For example, in @{text
- partial_order} the name @{text less} abbreviates @{term
- "partial_order.less le"}. Therefore, in @{text order_preserving}
- the qualified name @{text le.less} abbreviates @{term
- "partial_order.less le"} and @{text le'.less} abbreviates @{term
- "partial_order.less le'"}. Hence, the equation in the abbreviation
- above could have been written more concisely as @{text "less' \<equiv>
- le'.less"}. *}
+
+subsection {* Default Instantiations and Implicit Parameters *}
+
+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
+ 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
+ Section~\ref{sec:changing-the-hierarchy}. *}
+
+
+text {* In a locale expression that occurs within a locale
+ declaration, omitted parameters additionally extend the (possibly
+ empty) \isakeyword{for} clause.
-text {* Readers may find the declaration of locale @{text
- order_preserving} a little awkward, because the declaration and
- concrete syntax for @{text le} from @{text partial_order} are
- repeated in the declaration of @{text order_preserving}. Locale
- expressions provide a convenient short hand for this. A parameter
- in an instance is \emph{untouched} if no instantiation term is
- provided for it. In positional instantiations, a parameter position
- may be skipped with an underscore, and it is allowed to give fewer
- instantiation terms than the instantiated locale's number of
- parameters. In named instantiations, instantiation pairs for
- certain parameters may simply be omitted. Untouched parameters are
- implicitly declared by the locale expression and with their concrete
- syntax. In the sequence of parameters, they appear before the
- parameters from the \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 following locales illustrate this. A map @{text \<phi>} is a
- lattice homomorphism if it preserves meet and join. *}
+ There is an exception to this rule in locale declarations, where the
+ \isakeyword{for} clause servers 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{alltt}
+ partial_order le \isakeyword{for} le (\isakeyword{infixl} "\(\sqsubseteq\)" 50)\textrm{.}
+\end{alltt}
+ This short hand was used in the locale declarations of
+ 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
+ join. *}
locale lattice_hom =
le: lattice + le': lattice le' for le' (infixl "\<preceq>" 50) +
@@ -346,29 +384,42 @@
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)"
- abbreviation (in lattice_hom)
- meet' (infixl "\<sqinter>''" 50) where "meet' \<equiv> le'.meet"
- abbreviation (in lattice_hom)
- join' (infixl "\<squnion>''" 50) where "join' \<equiv> le'.join"
+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 {* A homomorphism is an endomorphism if both orders coincide. *}
+ Before turning to the second example, we complete the locale by
+ provinding infix syntax for the meet and join operations of the
+ second lattice.
+*}
+
+ context lattice_hom begin
+ abbreviation meet' (infixl "\<sqinter>''" 50) where "meet' \<equiv> le'.meet"
+ 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. *}
locale lattice_end = lattice_hom _ le
-text {* In this declaration, the first parameter of @{text
- lattice_hom}, @{text le}, is untouched and is then used to instantiate
- the second parameter. Its concrete syntax is preserved. *}
-
+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
+ 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. The expression
- imported by @{text lattice_end} identifies the first and second
- parameter of @{text lattice_hom}. By looking at the inheritance diagram it would seem
+ 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. This is not the
- case! Inheritance paths with identical morphisms are detected and
+ partial_order} and @{text lattice} are imported by @{text
+ lattice_end}. This is not the case! Inheritance paths with
+ identical morphisms are automatically detected and
the conclusions of the respective locales appear only once.
\begin{figure}
@@ -423,14 +474,50 @@
@{thm [display, indent=2] hom_le}
*}
+(*
+section {* Conditional Interpretation *}
+ locale non_negative =
+ fixes n :: int
+ assumes non_negative: "0 \<le> n"
+
+ 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"
+ apply unfold_locales using non_negative apply - by (rule mult_left_mono)
+
+ 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
+
+ apply unfold_locales unfolding is_inf_def is_sup_def by arith+
+
+
+ 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
+
+ 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
+
+*)
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, we
+ 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.
@@ -444,10 +531,18 @@
category. Order preserving maps, homomorphisms and vector spaces,
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}.
+
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 sources of this tutorial, which include all proofs, are
+ available with the Isabelle distribution at
+ \url{http://isabelle.in.tum.de}.
*}
text {*
@@ -542,8 +637,9 @@
\multicolumn{3}{l}{Diagnostics} \\
\textit{toplevel} & ::=
- & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\
- & | & \textbf{print\_locales}
+ & \textbf{print\_locales} \\
+ & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\
+ & | & \textbf{print\_interps} \textit{locale}
\end{tabular}
\end{center}
\hrule
@@ -552,8 +648,18 @@
\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{Acknowledgements.} Alexander Krauss, Tobias Nipkow,
- Christian Sternagel and Makarius Wenzel have made useful comments on
- a draft of this document. *}
+ Randy Pollack, Christian Sternagel and Makarius Wenzel have made
+ useful comments on earlier versions of this document. *}
end
--- a/doc-src/Locales/Locales/ROOT.ML Thu Oct 15 22:06:43 2009 +0200
+++ b/doc-src/Locales/Locales/ROOT.ML Thu Oct 15 22:07:18 2009 +0200
@@ -1,4 +1,4 @@
-no_document use_thy "GCD";
+no_document use_thy "~~/src/HOL/Number_Theory/UniqueFactorization";
use_thy "Examples1";
use_thy "Examples2";
-setmp_noncritical quick_and_dirty true use_thy "Examples3";
+use_thy "Examples3";
--- a/doc-src/Locales/Locales/document/Examples.tex Thu Oct 15 22:06:43 2009 +0200
+++ b/doc-src/Locales/Locales/document/Examples.tex Thu Oct 15 22:07:18 2009 +0200
@@ -9,7 +9,7 @@
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Examples\isanewline
-\isakeyword{imports}\ Main\ GCD\isanewline
+\isakeyword{imports}\ Main\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
@@ -81,22 +81,68 @@
\ \ \ \ \ \ \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}, with infix syntax
- \isa{{\isasymsqsubseteq}}. There is an implicit type parameter \isa{{\isacharprime}a}. It
- is not necessary to declare parameter types: most general types will
- be inferred from the context elements for all parameters.
+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.
+
+ Isabelle recognises undbound 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}.
- The above declaration not only introduces the locale, it also
- defines the \emph{locale predicate} \isa{partial{\isacharunderscore}order} with
- definition \isa{partial{\isacharunderscore}order{\isacharunderscore}def}:
+ 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
+ by issuing \isakeyword{print\_locale!} \isa{partial{\isacharunderscore}order}. The output
+ is the following list of context elements.
+
+\begin{alltt}
+ \isakeyword{fixes} le :: "'a \(\Rightarrow\) 'a \(\Rightarrow\) bool" (\isakeyword{infixl} "\(\sqsubseteq\)" 50)
+ \isakeyword{assumes} "partial_order op \(\sqsubseteq\)"
+ \isakeyword{notes} assumption
+ refl [intro, simp] = `?x \(\sqsubseteq\) ?x`
+ \isakeyword{and}
+ anti_sym [intro] = `\(\isasymlbrakk\)?x \(\sqsubseteq\) ?y; ?y \(\sqsubseteq\) ?x\(\isasymrbrakk\) \(\Longrightarrow\) ?x = ?y`
+ \isakeyword{and}
+ trans [trans] = `\(\isasymlbrakk\)?x \(\sqsubseteq\) ?y; ?y \(\sqsubseteq\) ?z\(\isasymrbrakk\) \(\Longrightarrow\) ?x \(\sqsubseteq\) ?z`
+\end{alltt}
+
+ 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}:
\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
+ 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.
- The specification of a locale is fixed, but its list of conclusions
+ 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}:
+ \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}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Extending the Locale%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The specification of a locale is fixed, but its list of conclusions
may be extended through Isar commands that take a \emph{target} argument.
In the following, \isakeyword{definition} and
\isakeyword{theorem} are illustrated.
@@ -131,24 +177,20 @@
\ \ \ \ less\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqsubset}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline
\ \ \ \ \isakeyword{where}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymsqsubset}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymsqsubseteq}\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
-A definition in a locale depends on the locale parameters.
- Here, a global constant \isa{partial{\isacharunderscore}order{\isachardot}less} is declared, which is lifted over the
- locale parameter \isa{le}. Its definition is the global theorem
- \isa{partial{\isacharunderscore}order{\isachardot}less{\isacharunderscore}def}:
+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}
+ \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. That is,
- \isa{partial{\isacharunderscore}order{\isachardot}less\ le} is printed and parsed as infix
- \isa{{\isasymsqsubset}}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Finally, the conclusion of the definition
- is added to the locale, \isa{less{\isacharunderscore}def}:
+ hiding this construction in the context of the locale. In the
+ context of the locale, 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:
\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}%
@@ -156,8 +198,9 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-As an example of a theorem statement in the locale, here is the
- derivation of a transitivity law.%
+The treatment of theorem statements is more straightforward.
+ As an example, here is the derivation of a transitivity law for the
+ strict order relation.%
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{lemma}\isamarkupfalse%
@@ -187,6 +230,10 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsubsection{Context Blocks%
+}
+\isamarkuptrue%
+%
\begin{isamarkuptext}%
When working with locales, sequences of commands with the same
target are frequent. A block of commands, delimited by
@@ -199,7 +246,7 @@
This style of working is illustrated in the block below, where
notions of infimum and supremum for partial orders are introduced,
- together with theorems.%
+ together with theorems about their uniqueness.%
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{context}\isamarkupfalse%
@@ -466,13 +513,7 @@
\ \ \isacommand{end}\isamarkupfalse%
%
\begin{isamarkuptext}%
-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.
-
- The syntax of the locale commands discussed in this tutorial is
+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}
@@ -488,11 +529,15 @@
Algebraic structures are commonly defined by adding operations and
properties to existing structures. For example, partial orders
are extended to lattices and total orders. Lattices are extended to
- distributive lattices.
-
- With locales, this inheritance is achieved through \emph{import} of a
- locale. Import is a separate entity in the locale declaration. If
- present, it precedes the context elements.%
+ distributive lattices.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+With locales, this kind of inheritance is achieved through
+ \emph{import} of locales. The import part of a locale declaration,
+ if present, precedes the context elements. Here is an example,
+ where partial orders are extended to lattices.%
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{locale}\isamarkupfalse%
@@ -502,8 +547,8 @@
\ \ \isakeyword{begin}%
\begin{isamarkuptext}%
These assumptions refer to the predicates for infimum
- and supremum defined in \isa{partial{\isacharunderscore}order}. We may now introduce
- the notions of meet and join.%
+ and supremum defined for \isa{partial{\isacharunderscore}order} in the previous
+ section. We now introduce the notions of meet and join.%
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{definition}\isamarkupfalse%
@@ -1071,8 +1116,9 @@
\ \ \isacommand{end}\isamarkupfalse%
%
\begin{isamarkuptext}%
-Locales for total orders and distributive lattices follow.
- Each comes with an example theorem.%
+Locales for total orders and distributive lattices follow for
+ further examples in this tutorial. Each comes with an example
+ theorem.%
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{locale}\isamarkupfalse%
@@ -1147,7 +1193,8 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-The locale hierachy obtained through these declarations is shown in Figure~\ref{fig:lattices}(a).
+The locale hierachy obtained through these declarations is shown in
+ Figure~\ref{fig:lattices}(a).
\begin{figure}
\hrule \vspace{2ex}
@@ -1201,12 +1248,37 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Total orders are lattices. Hence, by deriving the lattice
- axioms for total orders, the hierarchy may be changed
- and \isa{lattice} be placed between \isa{partial{\isacharunderscore}order}
- and \isa{total{\isacharunderscore}order}, as shown in Figure~\ref{fig:lattices}(b).
- Changes to the locale hierarchy may be declared
- with the \isakeyword{sublocale} command.%
+Locales enable to prove theorems abstractly, relative to
+ sets of assumptions. These theorems can then be used in other
+ contexts where the assumptions themselves, or
+ instances of the assumptions, are theorems. This form of theorem
+ reuse is called \emph{interpretation}. Locales generalise
+ interpretation from theorems to conclusions, enabling the reuse of
+ definitions and other constructs that are not part of the
+ 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
+ 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
+ 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
+ available in $l_1$.
+
+ Of course, the change of hierarchy must be supported by a theorem
+ that reflects, in our example, that total orders are indeed
+ lattices. Therefore the \isakeyword{sublocale} command generates a
+ goal, which must be discharged by the user. This is illustrated in
+ the following paragraphs. First the sublocale relation is stated.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1218,14 +1290,17 @@
\isacommand{sublocale}\isamarkupfalse%
\ total{\isacharunderscore}order\ {\isasymsubseteq}\ lattice%
\begin{isamarkuptxt}%
-This enters the context of locale \isa{total{\isacharunderscore}order}, in
+\normalsize
+ This enters the context of locale \isa{total{\isacharunderscore}order}, in
which the goal \begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ lattice\ op\ {\isasymsqsubseteq}%
-\end{isabelle} must be shown. First, the
- locale predicate needs to be unfolded --- for example using its
+\end{isabelle} must be shown.
+ Now the
+ locale predicate needs to be unfolded --- for example, using its
definition or by introduction rules
- provided by the locale package. The methods \isa{intro{\isacharunderscore}locales}
- and \isa{unfold{\isacharunderscore}locales} automate this. They are aware of the
+ 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
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
@@ -1234,21 +1309,24 @@
is smaller.
For the current goal, we would like to get hold of
- the assumptions of \isa{lattice}, hence \isa{unfold{\isacharunderscore}locales}
- is appropriate.%
+ the assumptions of \isa{lattice}, which need to be shown, hence
+ \isa{unfold{\isacharunderscore}locales} is appropriate.%
\end{isamarkuptxt}%
\isamarkuptrue%
\ \ \isacommand{proof}\isamarkupfalse%
\ unfold{\isacharunderscore}locales%
\begin{isamarkuptxt}%
-Since both \isa{lattice} and \isa{total{\isacharunderscore}order}
- inherit \isa{partial{\isacharunderscore}order}, the assumptions of the latter are
- discharged, and the only subgoals that remain are the assumptions
- introduced in \isa{lattice} \begin{isabelle}%
+\normalsize
+ Since the fact that both lattices and total orders are partial
+ orders is already reflected in the locale hierarchy, the assumptions
+ of \isa{partial{\isacharunderscore}order} are discharged automatically, and only the
+ assumptions introduced in \isa{lattice} remain as subgoals
+ \begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ {\isasymexists}inf{\isachardot}\ is{\isacharunderscore}inf\ x\ y\ inf\isanewline
\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ {\isasymexists}sup{\isachardot}\ is{\isacharunderscore}sup\ x\ y\ sup%
\end{isabelle}
- The proof for the first subgoal is%
+ The proof for the first subgoal is obtained by constructing an
+ infimum, whose existence is implied by totality.%
\end{isamarkuptxt}%
\isamarkuptrue%
\ \ \ \ \isacommand{fix}\isamarkupfalse%
@@ -1263,7 +1341,8 @@
\ {\isachardoublequoteopen}{\isasymexists}inf{\isachardot}\ is{\isacharunderscore}inf\ x\ y\ inf{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
%
\begin{isamarkuptxt}%
-The proof for the second subgoal is analogous and not
+\normalsize
+ The proof for the second subgoal is analogous and not
reproduced here.%
\end{isamarkuptxt}%
\isamarkuptrue%
@@ -1315,7 +1394,8 @@
\endisadelimvisible
%
\begin{isamarkuptext}%
-Similarly, total orders are distributive lattices.%
+Similarly, we may establsih that total orders are distributive
+ lattices with a second \isakeyword{sublocale} statement.%
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{sublocale}\isamarkupfalse%
@@ -1396,7 +1476,21 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-The locale hierarchy is now as shown in Figure~\ref{fig:lattices}(c).%
+The locale hierarchy is now as shown in
+ Figure~\ref{fig:lattices}(c).%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Locale interpretation is \emph{dynamic}. The statement
+ \isakeyword{sublocale} $l_1 \subseteq l_2$ will not just add the
+ current conclusions of $l_2$ to $l_1$. Rather the dependency is
+ stored, and conclusions that will be
+ added to $l_2$ in future are automatically propagated to $l_1$.
+ 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}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Locales/Locales/document/Examples1.tex Thu Oct 15 22:06:43 2009 +0200
+++ b/doc-src/Locales/Locales/document/Examples1.tex Thu Oct 15 22:07:18 2009 +0200
@@ -18,38 +18,29 @@
%
\endisadelimtheory
%
-\isamarkupsection{Use of Locales in Theories and Proofs%
+\isamarkupsection{Use of Locales in Theories and Proofs
+ \label{sec:interpretation}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Locales enable to prove theorems abstractly, relative to
- sets of assumptions. These theorems can then be used in other
- contexts where the assumptions themselves, or
- instances of the assumptions, are theorems. This form of theorem
- reuse is called \emph{interpretation}.
-
- The changes of the locale
- hierarchy from the previous sections are examples of
- interpretations. The command \isakeyword{sublocale} $l_1
- \subseteq l_2$ is said to \emph{interpret} locale $l_2$ in the
- context of $l_1$. It causes all theorems of $l_2$ to be made
- available in $l_1$. The interpretation is \emph{dynamic}: not only
- theorems already present in $l_2$ are available in $l_1$. Theorems
- that will be added to $l_2$ in future will automatically be
- propagated to $l_1$.
-
- Locales can also be interpreted in the contexts of theories and
+Locales can also be interpreted in the contexts of theories and
structured proofs. These interpretations are dynamic, too.
- Theorems added to locales will be propagated to theories.
- In this section the interpretation in
- theories is illustrated; interpretation in proofs is analogous.
+ Conclusions of locales will be propagated to the current theory or
+ the current proof context.%
+\footnote{Strictly speaking, only interpretation in theories is
+ dynamic since it is not possible to change locales or the locale
+ hierarchy from within a proof.}
+ The focus of this section is on
+ interpretation in theories, but we will also encounter
+ interpretations in proofs, in
+ Section~\ref{sec:local-interpretation}.
As an example, consider the type of natural numbers \isa{nat}. The
- relation \isa{{\isasymle}} is a total order over \isa{nat},
- divisibility \isa{dvd} is a distributive lattice. We start with the
- interpretation that \isa{{\isasymle}} is a partial order. The facilities of
- the interpretation command are explored in three versions.%
+ relation \isa{op\ {\isasymle}} is a total order over \isa{nat},
+ 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.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -59,10 +50,10 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-In the most basic form, interpretation just replaces the locale
- parameters by terms. The following command interprets the locale
- \isa{partial{\isacharunderscore}order} in the global context of the theory. The
- parameter \isa{le} is replaced by \isa{op\ {\isasymle}}.%
+The command \isakeyword{interpretation} is for the interpretation of
+ locale in theories. In the following example, the parameter of locale
+ \isa{partial{\isacharunderscore}order} is replaced by \isa{op\ {\isasymle}} and the locale instance is interpreted in the current
+ theory.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -74,15 +65,18 @@
\isacommand{interpretation}\isamarkupfalse%
\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}%
\begin{isamarkuptxt}%
-The locale name is succeeded by a \emph{parameter
- instantiation}. This is a list of terms, which refer to
- the parameters in the order of declaration in the locale. The
- locale name is preceded by an optional \emph{interpretation
- qualifier}, here \isa{nat}.
+\normalsize
+ The argument of the command is a simple \emph{locale expression}
+ consisting of the name of the interpreted locale, which is
+ preceded by the qualifier \isa{nat{\isacharcolon}} and succeeded by a
+ 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.
- The command creates the goal%
-\footnote{Note that \isa{op} binds tighter than functions
- application: parentheses around \isa{op\ {\isasymle}} are not necessary.}
+[TODO: Introduce morphisms. Reference to \ref{sec:locale-expressions}.]
+
+ The command creates the goal
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ partial{\isacharunderscore}order\ op\ {\isasymle}%
\end{isabelle} which can be shown easily:%
@@ -98,17 +92,15 @@
\endisadelimvisible
%
\begin{isamarkuptext}%
-Now theorems from the locale are available in the theory,
- interpreted for natural numbers, for example \isa{nat{\isachardot}trans}: \begin{isabelle}%
+The effect of the command is that instances of all
+ conclusions of the locale are available in the theory, where names
+ are prefixed by the qualifier. For example, transitivity for \isa{nat} is named \isa{nat{\isachardot}trans} and is the following
+ theorem:
+ \begin{isabelle}%
\ \ {\isasymlbrakk}{\isacharquery}x\ {\isasymle}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymle}\ {\isacharquery}z%
\end{isabelle}
-
- The interpretation qualifier, \isa{nat} in the example, is applied
- to all names processed by the interpretation. If a qualifer is
- given in the \isakeyword{interpretation} command, its use is
- mandatory when referencing the name. For example, the above theorem
- cannot be referred to simply by \isa{trans}. This prevents
- unwanted hiding of theorems.%
+ It is not possible to reference this theorem simply as \isa{trans}, which prevents unwanted hiding of existing theorems of the
+ theory by an interpretation.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -117,16 +109,27 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The above interpretation also creates the theorem
+Not only does the above interpretation qualify theorem names.
+ The prefix \isa{nat} is applied to all names introduced in locale
+ conclusions including names introduced in definitions. The
+ qualified name \isa{nat{\isachardot}less} refers to
+ 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.%
+\footnote{Since \isa{op\ {\isasymle}} is polymorphic, for \isa{partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}} a
+ more general type will be inferred than for \isa{nat{\isachardot}less} which
+ is over type \isa{nat}.}
+ The latter is preferred on output, as for example in the theorem
\isa{nat{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: \begin{isabelle}%
\ \ {\isasymlbrakk}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharquery}x\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}z{\isasymrbrakk}\isanewline
\isaindent{\ \ }{\isasymLongrightarrow}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharquery}x\ {\isacharquery}z%
\end{isabelle}
- Here, \isa{partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}}
- represents the strict order, although \isa{{\isacharless}} is the natural
- strict order for \isa{nat}. Interpretation allows to map concepts
- introduced by definitions in locales to the corresponding
- concepts of the theory.%
+ Both notations for the strict order are not satisfactory. The
+ constant \isa{op\ {\isacharless}} is the strict order for \isa{nat}.
+ 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.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Locales/Locales/document/Examples2.tex Thu Oct 15 22:06:43 2009 +0200
+++ b/doc-src/Locales/Locales/document/Examples2.tex Thu Oct 15 22:07:18 2009 +0200
@@ -19,47 +19,44 @@
\endisadelimtheory
%
\begin{isamarkuptext}%
-This is achieved by unfolding suitable equations during
- interpretation. These equations are given after the keyword
- \isakeyword{where} and require proofs. The revised command
- that replaces \isa{{\isasymsqsubset}} by \isa{{\isacharless}} is:%
+\vspace{-5ex}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimvisible
-%
+\ \ %
\endisadelimvisible
%
\isatagvisible
\isacommand{interpretation}\isamarkupfalse%
\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}nat{\isacharcomma}\ nat{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isacommand{proof}\isamarkupfalse%
+\ \ \ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharminus}%
\begin{isamarkuptxt}%
-The goals are \begin{isabelle}%
+\normalsize The goals are \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%
+\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}partial{\isacharunderscore}order\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ unfold{\isacharunderscore}locales\ auto%
\begin{isamarkuptxt}%
-The second goal is shown by unfolding the
- definition of \isa{partial{\isacharunderscore}order{\isachardot}less}.%
+\normalsize The second goal is shown by unfolding the
+ definition of \isa{partial{\isacharunderscore}order{\isachardot}less}.%
\end{isamarkuptxt}%
\isamarkuptrue%
-\ \ \isacommand{show}\isamarkupfalse%
+\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ partial{\isacharunderscore}order{\isachardot}less{\isacharunderscore}def\ {\isacharbrackleft}OF\ {\isacharbackquoteopen}partial{\isacharunderscore}order\ op\ {\isasymle}{\isacharbackquoteclose}{\isacharbrackright}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
-\isacommand{qed}\isamarkupfalse%
+\ \ \isacommand{qed}\isamarkupfalse%
%
\endisatagvisible
{\isafoldvisible}%
@@ -69,8 +66,8 @@
\endisadelimvisible
%
\begin{isamarkuptext}%
-Note that the above proof is not in the context of a locale.
- Hence, the correct interpretation of \isa{partial{\isacharunderscore}order{\isachardot}less{\isacharunderscore}def} is obtained manually with \isa{OF}.%
+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}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Locales/Locales/document/Examples3.tex Thu Oct 15 22:06:43 2009 +0200
+++ b/doc-src/Locales/Locales/document/Examples3.tex Thu Oct 15 22:07:18 2009 +0200
@@ -9,56 +9,78 @@
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Examples{\isadigit{3}}\isanewline
-\isakeyword{imports}\ Examples\isanewline
+\isakeyword{imports}\ Examples\ {\isachardoublequoteopen}{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}HOL{\isacharslash}Number{\isacharunderscore}Theory{\isacharslash}UniqueFactorization{\isachardoublequoteclose}\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
+\isanewline
%
\endisadelimtheory
%
-\isamarkupsubsection{Third Version: Local Interpretation%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\isataginvisible
+\isacommand{hide}\isamarkupfalse%
+\ const\ Lattices{\isachardot}lattice%
+\endisataginvisible
+{\isafoldinvisible}%
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\begin{isamarkuptext}%
+\vspace{-5ex}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Third Version: Local Interpretation
+ \label{sec:local-interpretation}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-In the above example, the fact that \isa{{\isasymle}} is a partial
- order for the natural numbers was used in the proof of the
- second goal. In general, proofs of the equations may involve
- theorems implied by the fact the assumptions of the instantiated
- locale hold for the instantiating structure. If these theorems have
- been shown abstractly in the locale they can be made available
- conveniently in the context through an auxiliary local interpretation (keyword
- \isakeyword{interpret}). This interpretation is inside the proof of the global
- interpretation. The third revision of the example illustrates this.%
+In the above example, the fact that \isa{op\ {\isasymle}} is a partial
+ order for the natural numbers 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
+ 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.
+ The command for local interpretations is \isakeyword{interpret}. We
+ repeat the example from the previous section to illustrate this.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimvisible
-%
+\ \ %
\endisadelimvisible
%
\isatagvisible
\isacommand{interpretation}\isamarkupfalse%
\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isacommand{proof}\isamarkupfalse%
+\ \ \ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharminus}\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
+\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}partial{\isacharunderscore}order\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ unfold{\isacharunderscore}locales\ auto\isanewline
-\ \ \isacommand{then}\isamarkupfalse%
+\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{interpret}\isamarkupfalse%
\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}nat{\isacharcomma}\ nat{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
+\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ nat{\isachardot}less{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
-\isacommand{qed}\isamarkupfalse%
+\ \ \isacommand{qed}\isamarkupfalse%
%
\endisatagvisible
{\isafoldvisible}%
@@ -68,15 +90,14 @@
\endisadelimvisible
%
\begin{isamarkuptext}%
-The inner interpretation does not require an elaborate new
- proof, it is immediate from the preceding fact and proved with
- ``.''. It enriches the local proof context by the very theorems
+The inner interpretation is immediate from the preceding fact
+ and proved by assumption (Isar short hand ``.''). It enriches the
+ local proof context by the theorems
also obtained in the interpretation from Section~\ref{sec:po-first},
and \isa{nat{\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
- \isakeyword{qed} --- and are then replaced by those with the desired
- substitutions of the strict order.%
+ leaving the proof context --- that is, after the closing a
+ \isakeyword{next} or \isakeyword{qed} statement.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -85,71 +106,76 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Further interpretations are necessary to reuse theorems from
+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
- interpretation is reproduced in order to give an example of a more
+ interpretation is reproduced to give an example of a more
elaborate interpretation proof.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimvisible
-%
+\ \ %
\endisadelimvisible
%
\isatagvisible
\isacommand{interpretation}\isamarkupfalse%
\ nat{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{where}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ max\ x\ y{\isachardoublequoteclose}\isanewline
-\isacommand{proof}\isamarkupfalse%
+\ \ \ \ \isakeyword{where}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ max\ x\ y{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharminus}\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
+\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}lattice\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptxt}%
-We have already shown that this is a partial order,%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ unfold{\isacharunderscore}locales%
-\begin{isamarkuptxt}%
-hence only the lattice axioms remain to be 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},%
+\normalsize We have already shown that this is a partial
+ order,%
\end{isamarkuptxt}%
\isamarkuptrue%
-\ \ \ \ \isacommand{apply}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
+\ unfold{\isacharunderscore}locales%
+\begin{isamarkuptxt}%
+\normalsize hence only the lattice axioms remain to be
+ 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{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}unfold\ nat{\isachardot}is{\isacharunderscore}inf{\isacharunderscore}def\ nat{\isachardot}is{\isacharunderscore}sup{\isacharunderscore}def{\isacharparenright}%
\begin{isamarkuptxt}%
-the goals become \begin{isabelle}%
+\normalsize the goals become \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} which can be solved
- by Presburger arithmetic.%
+\end{isabelle}
+ This can be solved by Presburger arithmetic, which is contained
+ in \isa{arith}.%
\end{isamarkuptxt}%
\isamarkuptrue%
-\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ arith{\isacharplus}%
\begin{isamarkuptxt}%
-In order to show the equations, we put ourselves in a
- situation where the lattice theorems can be used in a convenient way.%
+\normalsize In order to show the equations, we put ourselves
+ in a situation where the lattice theorems can be used in a
+ convenient way.%
\end{isamarkuptxt}%
\isamarkuptrue%
-\ \ \isacommand{then}\isamarkupfalse%
+\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{interpret}\isamarkupfalse%
\ nat{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
+\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}bestsimp\ simp{\isacharcolon}\ nat{\isachardot}meet{\isacharunderscore}def\ nat{\isachardot}is{\isacharunderscore}inf{\isacharunderscore}def{\isacharparenright}\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
+\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ max\ x\ y{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}bestsimp\ simp{\isacharcolon}\ nat{\isachardot}join{\isacharunderscore}def\ nat{\isachardot}is{\isacharunderscore}sup{\isacharunderscore}def{\isacharparenright}\isanewline
-\isacommand{qed}\isamarkupfalse%
+\ \ \isacommand{qed}\isamarkupfalse%
%
\endisatagvisible
{\isafoldvisible}%
@@ -159,18 +185,19 @@
\endisadelimvisible
%
\begin{isamarkuptext}%
-Next follows that \isa{{\isasymle}} is a total order.%
+Next follows that \isa{op\ {\isasymle}} is a total order, again for
+ the natural numbers.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimvisible
-%
+\ \ %
\endisadelimvisible
%
\isatagvisible
\isacommand{interpretation}\isamarkupfalse%
\ nat{\isacharcolon}\ total{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{by}\isamarkupfalse%
+\ \ \ \ \isacommand{by}\isamarkupfalse%
\ unfold{\isacharunderscore}locales\ arith%
\endisatagvisible
{\isafoldvisible}%
@@ -181,7 +208,7 @@
%
\begin{isamarkuptext}%
Theorems that are available in the theory at this point are shown in
- Table~\ref{tab:nat-lattice}.
+ Table~\ref{tab:nat-lattice}. Two points are worth noting:
\begin{table}
\hrule
@@ -203,69 +230,72 @@
\label{tab:nat-lattice}
\end{table}
- Note that since the locale hierarchy reflects that total orders are
- distributive lattices, an explicit interpretation of distributive
- lattices for the order relation on natural numbers is not neccessary.
-
- Why not push this idea further and just give the last interpretation
- as a single interpretation instead of the sequence of three? The
- reasons for this are twofold:
\begin{itemize}
\item
- Often it is easier to work in an incremental fashion, because later
- interpretations require theorems provided by earlier
- interpretations.
+ Locale \isa{distrib{\isacharunderscore}lattice} was also interpreted. Since the
+ locale hierarcy 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.
\item
- Assume that a definition is made in some locale $l_1$, and that $l_2$
- imports $l_1$. Let an equation for the definition be
- proved in an interpretation of $l_2$. The equation will be unfolded
- in interpretations of theorems added to $l_2$ or below in the import
- hierarchy, but not for theorems added above $l_2$.
- Hence, an equation interpreting a definition should always be given in
- an interpretation of the locale where the definition is made, not in
- an interpretation of a locale further down the hierarchy.
-\end{itemize}%
+ Theorem \isa{nat{\isachardot}less{\isacharunderscore}total} makes use of \isa{op\ {\isacharless}}
+ 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{Lattice \isa{dvd} on \isa{nat}%
+\isamarkupsubsection{Interpretations for Divisibility%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Divisibility on the natural numbers is a distributive lattice
+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.%
+ 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%
+\ \ \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
+\ \ \ \ \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%
+\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}partial{\isacharunderscore}order\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ unfold{\isacharunderscore}locales\ {\isacharparenleft}auto\ simp{\isacharcolon}\ dvd{\isacharunderscore}def{\isacharparenright}\isanewline
-\ \ \isacommand{then}\isamarkupfalse%
+\ \ \ \ \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%
+\ \ \ \ \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%
+\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isachardot}less{\isacharunderscore}def{\isacharparenright}\isanewline
-\ \ \ \ \isacommand{apply}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ auto\isanewline
-\ \ \ \ \isacommand{done}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{done}\isamarkupfalse%
\isanewline
-\isacommand{qed}\isamarkupfalse%
+\ \ \isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
@@ -275,69 +305,71 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-Note that in Isabelle/HOL there is no symbol for strict
- divisibility. Instead, interpretation substitutes \isa{x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y}.%
+Note that in Isabelle/HOL there is no operator for strict
+ divisibility. Instead, we substitute \isa{x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y}.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{interpretation}\isamarkupfalse%
+\ \ \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}\ {\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}\ {\isachardoublequoteopen}lattice{\isachardot}join\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ lcm{\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%
+\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}lattice\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{apply}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ unfold{\isacharunderscore}locales\isanewline
-\ \ \ \ \isacommand{apply}\isamarkupfalse%
+\ \ \ \ \ \ \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%
+\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequoteopen}gcd\ x\ y{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
-\ \ \ \ \isacommand{apply}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ auto\ {\isacharbrackleft}{\isadigit{1}}{\isacharbrackright}\isanewline
-\ \ \ \ \isacommand{apply}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequoteopen}lcm\ x\ y{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
-\ \ \ \ \isacommand{apply}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}auto\ intro{\isacharcolon}\ lcm{\isacharunderscore}least{\isacharunderscore}nat{\isacharparenright}\isanewline
-\ \ \ \ \isacommand{done}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{done}\isamarkupfalse%
\isanewline
-\ \ \isacommand{then}\isamarkupfalse%
+\ \ \ \ \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%
+\ \ \ \ \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%
+\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ expand{\isacharunderscore}fun{\isacharunderscore}eq{\isacharparenright}\isanewline
-\ \ \ \ \isacommand{apply}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isachardot}meet{\isacharunderscore}def{\isacharparenright}\isanewline
-\ \ \ \ \isacommand{apply}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ the{\isacharunderscore}equality{\isacharparenright}\isanewline
-\ \ \ \ \isacommand{apply}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isachardot}is{\isacharunderscore}inf{\isacharunderscore}def{\isacharparenright}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
+\ \ \ \ \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%
+\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ expand{\isacharunderscore}fun{\isacharunderscore}eq{\isacharparenright}\isanewline
-\ \ \ \ \isacommand{apply}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isachardot}join{\isacharunderscore}def{\isacharparenright}\isanewline
-\ \ \ \ \isacommand{apply}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ the{\isacharunderscore}equality{\isacharparenright}\isanewline
-\ \ \ \ \isacommand{apply}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isachardot}is{\isacharunderscore}sup{\isacharunderscore}def{\isacharparenright}\isanewline
-\ \ \ \ \isacommand{apply}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}auto\ intro{\isacharcolon}\ lcm{\isacharunderscore}least{\isacharunderscore}nat\ iff{\isacharcolon}\ lcm{\isacharunderscore}unique{\isacharunderscore}nat{\isacharparenright}\isanewline
-\ \ \ \ \isacommand{done}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{done}\isamarkupfalse%
\isanewline
-\isacommand{qed}\isamarkupfalse%
+\ \ \isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
@@ -347,59 +379,46 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-Equations \isa{nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq} and \isa{nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq} are used in the main part the subsequent
- interpretation.%
+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%
%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isataginvisible
-\isacommand{lemma}\isamarkupfalse%
-\ gcd{\isacharunderscore}lcm{\isacharunderscore}distr{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}gcd\ x\ {\isacharparenleft}lcm\ y\ z{\isacharparenright}\ {\isacharequal}\ lcm\ {\isacharparenleft}gcd\ x\ y{\isacharparenright}\ {\isacharparenleft}gcd\ x\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{sorry}\isamarkupfalse%
-%
-\endisataginvisible
-{\isafoldinvisible}%
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-\isanewline
-%
\isadelimvisible
-\isanewline
-%
+\ \ %
\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%
+\ \ \ \ distrib{\isacharunderscore}lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ unfold{\isacharunderscore}locales%
\begin{isamarkuptxt}%
-\begin{isabelle}%
+\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}%
+\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{apply}\isamarkupfalse%
-\ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq\ nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq{\isacharparenright}%
+\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
+\ nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq\ nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq%
\begin{isamarkuptxt}%
-\begin{isabelle}%
+\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}%
+\end{isabelle}
+ This is a result of number theory:%
\end{isamarkuptxt}%
\isamarkuptrue%
-\ \ \isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}rule\ gcd{\isacharunderscore}lcm{\isacharunderscore}distr{\isacharparenright}\ \isacommand{done}\isamarkupfalse%
-%
+\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}rule\ UniqueFactorization{\isachardot}gcd{\isacharunderscore}lcm{\isacharunderscore}distrib{\isacharunderscore}nat{\isacharparenright}%
\endisatagvisible
{\isafoldvisible}%
%
@@ -431,11 +450,28 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsubsection{Inspecting Interpretations of a Locale%
+}
+\isamarkuptrue%
+%
\begin{isamarkuptext}%
-The syntax of the interpretation commands is shown in
- Table~\ref{tab:commands}. The grammar refers to
- \textit{expression}, which stands for a \emph{locale} expression.
- Locale expressions are discussed in the following section.%
+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} \isa{partial{\isacharunderscore}order}
+ outputs the following:
+\begin{alltt}
+ nat! : 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
+ 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
+ more convenient to use. For \isakeyword{interpretation}, the
+ default for qualifiers without an explicit designator is ``!''.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -449,105 +485,84 @@
far: it involves two partial orders, and it is desirable to use the
existing locale for both.
- Inspecting the grammar of locale commands in
- Table~\ref{tab:commands} reveals that the import of a locale can be
- more than just a single locale. In general, the import is a
- \emph{locale expression}, which enables to combine locales
- and instantiate parameters. A locale expression is a sequence of
- locale \emph{instances} followed by an optional \isakeyword{for}
- clause. Each instance consists of a locale reference, which may be
- preceded by a qualifer and succeeded by instantiations of the
- parameters of that locale. Instantiations may be either positional
- or through explicit mappings of parameters to arguments.
+ 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.
+
+ 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
+ expression.
+
+ A \emph{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:
+\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.
- Using a locale expression, a locale for order
- preserving maps can be declared in the following way.%
+ 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{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
+ 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
+ parameters is declared.
+
+ Two context elements for the map parameter \isa{{\isasymphi}} and the
+ assumptions that it is order perserving complete the locale
+ declaration.%
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{locale}\isamarkupfalse%
\ order{\isacharunderscore}preserving\ {\isacharequal}\isanewline
\ \ \ \ le{\isacharcolon}\ partial{\isacharunderscore}order\ le\ {\isacharplus}\ le{\isacharprime}{\isacharcolon}\ partial{\isacharunderscore}order\ le{\isacharprime}\isanewline
\ \ \ \ \ \ \isakeyword{for}\ le\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqsubseteq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{and}\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline
-\ \ \ \ \isakeyword{fixes}\ {\isasymphi}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{fixes}\ {\isasymphi}\isanewline
\ \ \ \ \isakeyword{assumes}\ hom{\isacharunderscore}le{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymsqsubseteq}\ y\ {\isasymLongrightarrow}\ {\isasymphi}\ x\ {\isasympreceq}\ {\isasymphi}\ y{\isachardoublequoteclose}%
\begin{isamarkuptext}%
-The second and third line contain the expression --- two
- instances of the partial order locale where the parameter is
- instantiated to \isa{le}
- and \isa{le{\isacharprime}}, respectively. The \isakeyword{for} clause consists
- of parameter declarations and is similar to the context element
- \isakeyword{fixes}. The notable difference is that the
- \isakeyword{for} clause is part of the expression, and only
- parameters defined in the expression may occur in its instances.
+Here are examples of theorems that are
+ available in the locale:
- Instances define \emph{morphisms} on locales. Their effect on the
- parameters is lifted to terms, propositions and theorems in the
- canonical way,
- and thus to the assumptions and conclusions of a locale. The
- assumption of a locale expression is the conjunction of the
- assumptions of the instances. The conclusions of a sequence of
- instances are obtained by appending the conclusions of the
- instances in the order of the sequence.
+ \isa{hom{\isacharunderscore}le}: \isa{{\isacharquery}x\ {\isasymsqsubseteq}\ {\isacharquery}y\ {\isasymLongrightarrow}\ {\isasymphi}\ {\isacharquery}x\ {\isasympreceq}\ {\isasymphi}\ {\isacharquery}y}
- The qualifiers in the expression are already a familiar concept from
- the \isakeyword{interpretation} command
- (Section~\ref{sec:po-first}). Here, they serve to distinguish names
- (in particular theorem names) for the two partial orders within the
- locale. Qualifiers in the \isakeyword{locale} command (and in
- \isakeyword{sublocale}) default to optional --- that is, they need
- not occur in references to the qualified names. Here are examples
- of theorems in locale \isa{order{\isacharunderscore}preserving}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isataginvisible
-\isacommand{context}\isamarkupfalse%
-\ order{\isacharunderscore}preserving\ \isakeyword{begin}%
-\endisataginvisible
-{\isafoldinvisible}%
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\begin{isamarkuptext}%
-\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{\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{hom{\isacharunderscore}le}: \isa{{\isacharquery}x\ {\isasymsqsubseteq}\ {\isacharquery}y\ {\isasymLongrightarrow}\ {\isasymphi}\ {\isacharquery}x\ {\isasympreceq}\ {\isasymphi}\ {\isacharquery}y}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The theorems for the partial order \isa{{\isasympreceq}}
- are qualified by \isa{le{\isacharprime}}. For example, \isa{le{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: \begin{isabelle}%
+ \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%
-\end{isabelle}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isataginvisible
-\isacommand{end}\isamarkupfalse%
-%
-\endisataginvisible
-{\isafoldinvisible}%
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\begin{isamarkuptext}%
-This example reveals that there is no infix syntax for the
- strict operation associated with \isa{{\isasympreceq}}. This can be declared
- through an abbreviation.%
+\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:%
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{abbreviation}\isamarkupfalse%
@@ -562,31 +577,52 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsubsection{Default Instantiations and Implicit Parameters%
+}
+\isamarkuptrue%
+%
\begin{isamarkuptext}%
-Qualifiers not only apply to theorem names, but also to names
- introduced by definitions and abbreviations. For example, in \isa{partial{\isacharunderscore}order} the name \isa{less} abbreviates \isa{op\ {\isasymsqsubset}}. Therefore, in \isa{order{\isacharunderscore}preserving}
- the qualified name \isa{le{\isachardot}less} abbreviates \isa{op\ {\isasymsqsubset}} and \isa{le{\isacharprime}{\isachardot}less} abbreviates \isa{op\ {\isasymprec}}. Hence, the equation in the abbreviation
- above could have been written more concisely as \isa{less{\isacharprime}\ {\isasymequiv}\ le{\isacharprime}{\isachardot}less}.%
+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
+ Section~\ref{sec:changing-the-hierarchy}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Readers may find the declaration of locale \isa{order{\isacharunderscore}preserving} a little awkward, because the declaration and
- concrete syntax for \isa{le} from \isa{partial{\isacharunderscore}order} are
- repeated in the declaration of \isa{order{\isacharunderscore}preserving}. Locale
- expressions provide a convenient short hand for this. A parameter
- in an instance is \emph{untouched} if no instantiation term is
- provided for it. In positional instantiations, a parameter position
- may be skipped with an underscore, and it is allowed to give fewer
- instantiation terms than the instantiated locale's number of
- parameters. In named instantiations, instantiation pairs for
- certain parameters may simply be omitted. Untouched parameters are
- implicitly declared by the locale expression and with their concrete
- syntax. In the sequence of parameters, they appear before the
- parameters from the \isakeyword{for} clause.
+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 following locales illustrate this. A map \isa{{\isasymphi}} is a
- lattice homomorphism if it preserves meet and join.%
+ There is an exception to this rule in locale declarations, where the
+ \isakeyword{for} clause servers 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{alltt}
+ partial_order le \isakeyword{for} le (\isakeyword{infixl} "\(\sqsubseteq\)" 50)\textrm{.}
+\end{alltt}
+ This short hand was used in the locale declarations of
+ 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
+ join.%
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{locale}\isamarkupfalse%
@@ -594,23 +630,39 @@
\ \ \ \ le{\isacharcolon}\ lattice\ {\isacharplus}\ le{\isacharprime}{\isacharcolon}\ lattice\ le{\isacharprime}\ \isakeyword{for}\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline
\ \ \ \ \isakeyword{fixes}\ {\isasymphi}\isanewline
\ \ \ \ \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}\isanewline
-\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}}.
+
+ Before turning to the second example, we complete the locale by
+ provinding infix syntax for the meet and join operations of the
+ second lattice.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ \isacommand{context}\isamarkupfalse%
+\ lattice{\isacharunderscore}hom\ \isakeyword{begin}\isanewline
\ \ \isacommand{abbreviation}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{in}\ lattice{\isacharunderscore}hom{\isacharparenright}\isanewline
-\ \ \ \ meet{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqinter}{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}meet{\isacharprime}\ {\isasymequiv}\ le{\isacharprime}{\isachardot}meet{\isachardoublequoteclose}\isanewline
+\ meet{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqinter}{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}meet{\isacharprime}\ {\isasymequiv}\ le{\isacharprime}{\isachardot}meet{\isachardoublequoteclose}\isanewline
\ \ \isacommand{abbreviation}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{in}\ lattice{\isacharunderscore}hom{\isacharparenright}\isanewline
-\ \ \ \ join{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqunion}{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}join{\isacharprime}\ {\isasymequiv}\ le{\isacharprime}{\isachardot}join{\isachardoublequoteclose}%
+\ join{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqunion}{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}join{\isacharprime}\ {\isasymequiv}\ le{\isacharprime}{\isachardot}join{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{end}\isamarkupfalse%
+%
\begin{isamarkuptext}%
-A homomorphism is an endomorphism if both orders coincide.%
+The next example pushes 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}%
-In this declaration, the first parameter of \isa{lattice{\isacharunderscore}hom}, \isa{le}, is untouched and is then used to instantiate
- the second parameter. Its concrete syntax is preserved.%
+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
+ parameter of the homomorphism locale.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -618,11 +670,10 @@
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. The expression
- imported by \isa{lattice{\isacharunderscore}end} identifies the first and second
- parameter of \isa{lattice{\isacharunderscore}hom}. 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. This is not the
- case! Inheritance paths with identical morphisms are detected and
+ 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.
\begin{figure}
@@ -716,7 +767,7 @@
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, we
+ 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.
@@ -730,10 +781,18 @@
category. Order preserving maps, homomorphisms and vector spaces,
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}.
+
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}.%
+ on algebra \cite[Chapter~8]{Jacobson1985}.
+
+ The sources of this tutorial, which include all proofs, are
+ available with the Isabelle distribution at
+ \url{http://isabelle.in.tum.de}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -829,8 +888,9 @@
\multicolumn{3}{l}{Diagnostics} \\
\textit{toplevel} & ::=
- & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\
- & | & \textbf{print\_locales}
+ & \textbf{print\_locales} \\
+ & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\
+ & | & \textbf{print\_interps} \textit{locale}
\end{tabular}
\end{center}
\hrule
@@ -841,9 +901,22 @@
\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.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
\textbf{Acknowledgements.} Alexander Krauss, Tobias Nipkow,
- Christian Sternagel and Makarius Wenzel have made useful comments on
- a draft of this document.%
+ Randy Pollack, Christian Sternagel and Makarius Wenzel have made
+ useful comments on earlier versions of this document.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Locales/Locales/document/root.bib Thu Oct 15 22:06:43 2009 +0200
+++ b/doc-src/Locales/Locales/document/root.bib Thu Oct 15 22:07:18 2009 +0200
@@ -42,6 +42,24 @@
year = 2006
}
+% TYPES 2008
+
+@inproceedings{HaftmannWenzel2009,
+ author = "Florian Haftmann and Makarius Wenzel",
+ title = "Local theory specifications in {Isabelle}/{Isar}",
+ pages = "153--168",
+ crossref = "BerardiEtAl2009"
+}
+
+@proceedings{BerardiEtAl2009,
+ editor = "Stefano Berardi and Ferruccio Damiani and Ugo de Liguoro",
+ title = "Types for Proofs and Programs, TYPES 2008, Torino, Italy",
+ booktitle = "Types for Proofs and Programs, TYPES 2008, Torino, Italy",
+ series = "LNCS 5497",
+ publisher = "Springer",
+ year = 2009
+}
+
% MKM 2006
@inproceedings{Ballarin2006b,
--- a/doc-src/Locales/Locales/document/root.tex Thu Oct 15 22:06:43 2009 +0200
+++ b/doc-src/Locales/Locales/document/root.tex Thu Oct 15 22:07:18 2009 +0200
@@ -6,6 +6,7 @@
\usepackage{subfigure}
\usepackage{../../../isabelle,../../../isabellesym}
\usepackage{verbatim}
+\usepackage{alltt}
\usepackage{array}
\usepackage{amssymb}
--- a/doc-src/Locales/Locales/document/session.tex Thu Oct 15 22:06:43 2009 +0200
+++ b/doc-src/Locales/Locales/document/session.tex Thu Oct 15 22:07:18 2009 +0200
@@ -1,3 +1,11 @@
+\input{Primes.tex}
+
+\input{Cong.tex}
+
+\input{Multiset.tex}
+
+\input{UniqueFactorization.tex}
+
\input{Examples.tex}
\input{Examples1.tex}