# HG changeset patch # User ballarin # Date 1255637238 -7200 # Node ID 0114e04a0d64f6902d8b6279accde28b22a35f3a # Parent d556a0e04e33eb5cf1b8b9cf201ce9036a4bad23 Save current state of locales tutorial. diff -r d556a0e04e33 -r 0114e04a0d64 doc-src/Locales/Locales/Examples.thy --- 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]: "\ x \ y; y \ x \ \ x = y" and trans [trans]: "\ x \ y; y \ z \ \ x \ z" -text {* The parameter of this locale is @{term le}, with infix syntax - @{text \}. 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 \}. 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 "\ x \ y; y \ z \ \ x \ z"} rather + than @{term "\x y z. \ x \ y; y \ z \ \ x \ 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 \ 'a \ bool" (infixl "\" 50) where "(x \ y) = (x \ y \ x \ 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 \} 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 \}. *} + 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 \}. 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]: "\ x \ y; y \ z \ \ x \ 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 "\" 70) where "x \ 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 \ y \ y \ 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 \ 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 \ y then x else y)" by (auto simp: is_inf_def) then show "\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 "\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 \ 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 diff -r d556a0e04e33 -r 0114e04a0d64 doc-src/Locales/Locales/Examples1.thy --- 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 \} is a total order over @{typ nat}, - divisibility @{text dvd} is a distributive lattice. We start with the - interpretation that @{text \} is a partial order. The facilities of - the interpretation command are explored in three versions. + relation @{term "op \"} is a total order over @{typ nat}, + divisibility @{text "op dvd"} forms a distributive lattice. We start with the + interpretation that @{term "op \"} 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 \ :: nat \ nat \ 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 \ :: nat \ nat \ + bool"} and the locale instance is interpreted in the current + theory. *} interpretation %visible nat: partial_order "op \ :: nat \ nat \ 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 \"} 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 \"} 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 \ :: nat \ nat \ 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 diff -r d556a0e04e33 -r 0114e04a0d64 doc-src/Locales/Locales/Examples2.thy --- 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 "\"} by @{text "<"} is: *} +text {* \vspace{-5ex} *} + interpretation %visible nat: partial_order "op \ :: [nat, nat] \ bool" + where "partial_order.less op \ (x::nat) y = (x < y)" + proof - + txt {* \normalsize The goals are @{subgoals [display]} + The proof that @{text \} is a partial order is as above. *} + show "partial_order (op \ :: nat \ nat \ 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 \ (x::nat) y = (x < y)" + unfolding partial_order.less_def [OF `partial_order op \`] + by auto + qed -interpretation %visible nat: partial_order "op \ :: [nat, nat] \ bool" - where "partial_order.less op \ (x::nat) y = (x < y)" -proof - - txt {* The goals are @{subgoals [display]} - The proof that @{text \} is a partial order is as above. *} - show "partial_order (op \ :: nat \ nat \ 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 \ (x::nat) y = (x < y)" - unfolding partial_order.less_def [OF `partial_order op \`] - 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 diff -r d556a0e04e33 -r 0114e04a0d64 doc-src/Locales/Locales/Examples3.thy --- 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 \} 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 \"} is a partial + order for the natural numbers was used in the second goal to + discharge the premise in the definition of @{text "op \"}. 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 \ :: nat \ nat \ bool" - where "partial_order.less op \ (x::nat) y = (x < y)" -proof - - show "partial_order (op \ :: nat \ nat \ bool)" - by unfold_locales auto - then interpret nat: partial_order "op \ :: [nat, nat] \ bool" . - show "partial_order.less op \ (x::nat) y = (x < y)" - unfolding nat.less_def by auto -qed + interpretation %visible nat: partial_order "op \ :: nat \ nat \ bool" + where "partial_order.less op \ (x::nat) y = (x < y)" + proof - + show "partial_order (op \ :: nat \ nat \ bool)" + by unfold_locales auto + then interpret nat: partial_order "op \ :: [nat, nat] \ bool" . + show "partial_order.less op \ (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 \} and @{text \} are substituted by @{term "min :: nat \ nat \ nat"} and @{term "max :: nat \ nat \ 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 \ :: nat \ nat \ bool" - where "lattice.meet op \ (x::nat) y = min x y" - and "lattice.join op \ (x::nat) y = max x y" -proof - - show "lattice (op \ :: nat \ nat \ 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 \ :: nat \ nat \ bool" . - show "lattice.meet op \ (x::nat) y = min x y" - by (bestsimp simp: nat.meet_def nat.is_inf_def) - show "lattice.join op \ (x::nat) y = max x y" - by (bestsimp simp: nat.join_def nat.is_sup_def) -qed + interpretation %visible nat: lattice "op \ :: nat \ nat \ bool" + where "lattice.meet op \ (x::nat) y = min x y" + and "lattice.join op \ (x::nat) y = max x y" + proof - + show "lattice (op \ :: nat \ nat \ 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 \ :: nat \ nat \ bool" . + show "lattice.meet op \ (x::nat) y = min x y" + by (bestsimp simp: nat.meet_def nat.is_inf_def) + show "lattice.join op \ (x::nat) y = max x y" + by (bestsimp simp: nat.join_def nat.is_sup_def) + qed -text {* Next follows that @{text \} is a total order. *} +text {* Next follows that @{text "op \"} is a total order, again for + the natural numbers. *} -interpretation %visible nat: total_order "op \ :: nat \ nat \ bool" - by unfold_locales arith + interpretation %visible nat: total_order "op \ :: nat \ nat \ 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 \"} 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 \ nat \ bool" + where "partial_order.less op dvd (x::nat) y = (x dvd y \ x \ y)" + proof - + show "partial_order (op dvd :: nat \ nat \ bool)" + by unfold_locales (auto simp: dvd_def) + then interpret nat_dvd: partial_order "op dvd :: nat \ nat \ bool" . + show "partial_order.less op dvd (x::nat) y = (x dvd y \ x \ 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 \ x \ y"}. *} -interpretation nat_dvd: partial_order "op dvd :: nat \ nat \ bool" - where "partial_order.less op dvd (x::nat) y = (x dvd y \ x \ y)" -proof - - show "partial_order (op dvd :: nat \ nat \ bool)" - by unfold_locales (auto simp: dvd_def) - then interpret nat_dvd: partial_order "op dvd :: nat \ nat \ bool" . - show "partial_order.less op dvd (x::nat) y = (x dvd y \ x \ y)" - apply (unfold nat_dvd.less_def) - apply auto - done -qed + interpretation nat_dvd: lattice "op dvd :: nat \ nat \ bool" + where nat_dvd_meet_eq: + "lattice.meet (op dvd :: nat \ nat \ bool) = gcd" + and nat_dvd_join_eq: + "lattice.join (op dvd :: nat \ nat \ bool) = lcm" + proof - + show "lattice (op dvd :: nat \ nat \ 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 \ nat \ bool" . + show "lattice.meet (op dvd :: nat \ nat \ 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 \ nat \ 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 \ - x \ 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 \ nat \ bool" - where nat_dvd_meet_eq: "lattice.meet (op dvd :: nat \ nat \ bool) = gcd" - and nat_dvd_join_eq: "lattice.join (op dvd :: nat \ nat \ bool) = lcm" -proof - - show "lattice (op dvd :: nat \ nat \ bool)" + interpretation %visible nat_dvd: + distrib_lattice "op dvd :: nat \ nat \ 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 \ nat \ bool" . - show "lattice.meet (op dvd :: nat \ nat \ 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 \ nat \ 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 \ nat \ nat \ bool" where - "is_lcm p m n \ m dvd p \ n dvd p \ - (\d. m dvd d \ n dvd d \ 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 \ nat \ 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 \}), @{text le'} + (\isakeyword{infixl}~@{text \}) for the orders and @{text \} 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 \}) + from the new locale and once to @{text le'} + (\isakeyword{infixl}~@{text \}). 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 \} 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 "\" 50) and le' (infixl "\" 50) + - fixes \ :: "'a \ 'b" + fixes \ assumes hom_le: "x \ y \ \ x \ \ 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 \} - 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 \}. This can be declared - through an abbreviation. *} + While there is infix syntax for the strict operation associated to + @{term "op \"}, there is none for the strict version of @{term + "op \"}. 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 \} + with this declaration: *} abbreviation (in order_preserving) less' (infixl "\" 50) where "less' \ 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' \ - 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 \} 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 \} is a lattice homomorphism if it preserves meet and + join. *} locale lattice_hom = le: lattice + le': lattice le' for le' (infixl "\" 50) + @@ -346,29 +384,42 @@ assumes hom_meet: "\ (x \ y) = le'.meet (\ x) (\ y)" and hom_join: "\ (x \ y) = le'.join (\ x) (\ y)" - abbreviation (in lattice_hom) - meet' (infixl "\''" 50) where "meet' \ le'.meet" - abbreviation (in lattice_hom) - join' (infixl "\''" 50) where "join' \ 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 "\''" 50) where "meet' \ le'.meet" + abbreviation join' (infixl "\''" 50) where "join' \ 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 \ n" + + interpretation partial_order "op \ :: int \ int \ bool" + where "partial_order.less op \ (x::int) y = (x < y)" + sorry + + sublocale non_negative \ order_preserving "op \" "op \" "\i. n * i" + apply unfold_locales using non_negative apply - by (rule mult_left_mono) + + interpretation lattice "op \ :: int \ int \ bool" + where min_eq: "lattice.meet op \ (x::int) y = min x y" + and max_eq: "lattice.join op \ (x::int) y = max x y" + sorry + + apply unfold_locales unfolding is_inf_def is_sup_def by arith+ + + + sublocale non_negative \ lattice_end "op \" "\i. n * i" + apply unfold_locales unfolding min_eq max_eq apply (case_tac "x \ y") + unfolding min_def apply auto apply arith + apply (rule sym) + apply (rule the_equality) + proof + + locale fspace_po = partial_order + sublocale fspace_po \ fspace: partial_order "\f g. \x. f x \ 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 diff -r d556a0e04e33 -r 0114e04a0d64 doc-src/Locales/Locales/ROOT.ML --- 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"; diff -r d556a0e04e33 -r 0114e04a0d64 doc-src/Locales/Locales/document/Examples.tex --- 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% % diff -r d556a0e04e33 -r 0114e04a0d64 doc-src/Locales/Locales/document/Examples1.tex --- 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% % diff -r d556a0e04e33 -r 0114e04a0d64 doc-src/Locales/Locales/document/Examples2.tex --- 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% % diff -r d556a0e04e33 -r 0114e04a0d64 doc-src/Locales/Locales/document/Examples3.tex --- 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% % diff -r d556a0e04e33 -r 0114e04a0d64 doc-src/Locales/Locales/document/root.bib --- 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, diff -r d556a0e04e33 -r 0114e04a0d64 doc-src/Locales/Locales/document/root.tex --- 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} diff -r d556a0e04e33 -r 0114e04a0d64 doc-src/Locales/Locales/document/session.tex --- 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}