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