# HG changeset patch # User ballarin # Date 1238193828 -3600 # Node ID 3779e2158dad321e12b69eef4cd21a9ca3f45640 # Parent 44a16c6956f9e205d984ea7bcd9d77822c4ca760 Update explanation of locale expressions to locale reimplementation. diff -r 44a16c6956f9 -r 3779e2158dad doc-src/Locales/Locales/Examples3.thy --- a/doc-src/Locales/Locales/Examples3.thy Fri Mar 27 20:25:07 2009 +0100 +++ b/doc-src/Locales/Locales/Examples3.thy Fri Mar 27 23:43:48 2009 +0100 @@ -250,47 +250,45 @@ 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}. Locale expressions enable to combine locales - and rename parameters. A locale name is a locale expression. If - $e_1$ and $e_2$ are locale expressions then $e_1 + e_2$ is their - \emph{merge}. If $e$ is an expression, then $e~q_1 \ldots q_n$ is - a \emph{renamed expression} where the parameters in $e$ are renamed - to $q_1 \ldots q_n$. Using a locale expression, a locale for order + \emph{locale expression}. These enable 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 parameter argument pairs. + + Using a locale expression, a locale for order preserving maps can be declared in the following way. *} locale order_preserving = - le: partial_order + le': partial_order le' for le' (infixl "\" 50) + + le: partial_order le + le': partial_order le' + for le (infixl "\" 50) and le' (infixl "\" 50) + fixes \ :: "'a \ 'b" assumes hom_le: "x \ y \ \ x \ \ y" -text {* The second line contains the expression, which is the - merge of two partial order locales. The parameter of the second one - is @{text le'} with new infix syntax @{text \}. The - parameters of the entire locale are @{text le}, @{text le'} and - @{text \}. This is their \emph{canonical order}, - which is obtained by a left-to-right traversal of the expression, - where only the new parameters are appended to the end of the list. The - parameters introduced in the locale elements of the declaration - follow. +text {* The second and third line contain the expression --- two + instances of the partial order locale with instantiations @{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. - In renamings parameters are referred to by position in the canonical - order; an underscore is used to skip a parameter position, which is - then not renamed. Renaming deletes the syntax of a parameter unless - a new mixfix annotation is given. + Instances are \emph{morphisms} on locales. Their effect on the + parameters is naturally lifted to terms, propositions and theorems, + 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. - Parameter renamings are morphisms between locales. These can be - lifted to terms and theorems and thus be applied to assumptions and - conclusions. The assumption of a merge is the conjunction of the - assumptions of the merged locale. The conclusions of a merge are - obtained by appending the conclusions of the left locale and of the - right locale. *} - -text {* The locale @{text order_preserving} contains theorems for both - orders @{text \} and @{text \}. How can one refer to a theorem for - a particular order, @{text \} or @{text \}? Names in locales are - qualified by the locale parameters. More precisely, a name is - qualified by the parameters of the locale in which its declaration - occurs. Here are examples: *} + The qualifiers in the expression are already a familiar concept from + the \isakeyword{interpretation} command. They serve to distinguish + names (in particular theorem names) for the two partial orders + within the locale. Qualifiers in the \isakeyword{locale} command + default to optional. Here are examples of theorems in locale @{text + order_preserving}: *} context %invisible order_preserving begin @@ -300,16 +298,14 @@ @{thm [source] hom_le}: @{thm hom_le} *} -text {* When renaming a locale, the morphism is also applied - to the qualifiers. Hence theorems for the partial order @{text \} +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 - version of @{text \}! This can, of course, not be introduced - automatically, but it can be declared manually through an abbreviation. + version of @{text \}! This can be declared through an abbreviation. *} abbreviation (in order_preserving) @@ -318,22 +314,39 @@ text (in order_preserving) {* Now the theorem is displayed nicely as @{thm le'.less_le_trans}. *} -text {* Not only names of theorems are qualified. In fact, all names - are qualified, in particular names introduced by definitions and - abbreviations. The name of the strict order of @{text \} is @{text - le.less} and therefore @{text le'.less} is the name of the strict - order of @{text \}. Hence, the equation in the above abbreviation - could have been written as @{text "less' \ le'.less"}. *} +text {* Qualifiers not only apply to theorem names, but also to names + introduced by definitions and abbreviations. In locale + @{text partial_order} the full name of the strict order of @{text \} is + @{text le.less} and therefore @{text le'.less} is the full name of + the strict order of @{text \}. Hence, the equation in the + abbreviation above could have been also written as @{text "less' \ + le'.less"}. *} -text {* Two more locales illustrate working with locale expressions. - A map @{text \} is a lattice homomorphism if it preserves meet and join. *} +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 + declared by the locale expression and with their concrete syntax by + implicitly adding them to the beginning of the \isakeyword{for} + clause. - locale lattice_hom = le: lattice + le': lattice le' for le' (infixl "\" 50) + + The following locales illustrate this. 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) + fixes \ assumes hom_meet: - "\ (lattice.meet le x y) = lattice.meet le' (\ x) (\ y)" + "\ (x \ y) = le'.meet (\ x) (\ y)" and hom_join: - "\ (lattice.join le x y) = lattice.join le' (\ x) (\ y)" + "\ (x \ y) = le'.join (\ x) (\ y)" abbreviation (in lattice_hom) meet' (infixl "\''" 50) where "meet' \ le'.meet" @@ -342,8 +355,12 @@ text {* A homomorphism is an endomorphism if both orders coincide. *} - locale lattice_end = - lattice_hom le le for le (infixl "\" 50) + locale lattice_end = lattice_hom _ le + +text {* In this declaration, the first parameter of @{text + lattice_hom}, @{text le}, is untouched and then used to instantiate + the second parameter. Its concrete syntax is preseverd. *} + text {* The inheritance diagram of the situation we have now is shown in Figure~\ref{fig:hom}, where the dashed line depicts an @@ -390,7 +407,7 @@ text {* It can be shown easily that a lattice homomorphism is order preserving. As the final example of this section, a locale - interpretation is used to assert this. *} + interpretation is used to assert this: *} sublocale lattice_hom \ order_preserving proof unfold_locales fix x y @@ -404,6 +421,7 @@ Theorems and other declarations --- syntax, in particular --- from the locale @{text order_preserving} are now active in @{text lattice_hom}, for example + @{thm [source] le'.less_le_trans}: @{thm le'.less_le_trans} *} @@ -423,7 +441,7 @@ Haftmann and Wenzel \cite{HaftmannWenzel2007} overcome a restriction of axiomatic type classes through a combination with locale interpretation. The result is a Haskell-style class system with a - facility to generate Haskell code. Classes are sufficient for + facility to generate ML and Haskell code. Classes are sufficient for simple specifications with a single type parameter. The locales for orders and lattices presented in this tutorial fall into this category. Order preserving maps, homomorphisms and vector spaces, diff -r 44a16c6956f9 -r 3779e2158dad doc-src/Locales/Locales/document/Examples3.tex --- a/doc-src/Locales/Locales/document/Examples3.tex Fri Mar 27 20:25:07 2009 +0100 +++ b/doc-src/Locales/Locales/document/Examples3.tex Fri Mar 27 23:43:48 2009 +0100 @@ -457,52 +457,46 @@ 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}. Locale expressions enable to combine locales - and rename parameters. A locale name is a locale expression. If - $e_1$ and $e_2$ are locale expressions then $e_1 + e_2$ is their - \emph{merge}. If $e$ is an expression, then $e~q_1 \ldots q_n$ is - a \emph{renamed expression} where the parameters in $e$ are renamed - to $q_1 \ldots q_n$. Using a locale expression, a locale for order + \emph{locale expression}. These enable 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 parameter argument pairs. + + Using a locale expression, a locale for order preserving maps can be declared in the following way.% \end{isamarkuptext}% \isamarkuptrue% \ \ \isacommand{locale}\isamarkupfalse% \ order{\isacharunderscore}preserving\ {\isacharequal}\isanewline -\ \ \ \ le{\isacharcolon}\ partial{\isacharunderscore}order\ {\isacharplus}\ le{\isacharprime}{\isacharcolon}\ partial{\isacharunderscore}order\ le{\isacharprime}\ \isakeyword{for}\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\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{assumes}\ hom{\isacharunderscore}le{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymsqsubseteq}\ y\ {\isasymLongrightarrow}\ {\isasymphi}\ x\ {\isasympreceq}\ {\isasymphi}\ y{\isachardoublequoteclose}% \begin{isamarkuptext}% -The second line contains the expression, which is the - merge of two partial order locales. The parameter of the second one - is \isa{le{\isacharprime}} with new infix syntax \isa{{\isasympreceq}}. The - parameters of the entire locale are \isa{le}, \isa{le{\isacharprime}} and - \isa{{\isasymphi}}. This is their \emph{canonical order}, - which is obtained by a left-to-right traversal of the expression, - where only the new parameters are appended to the end of the list. The - parameters introduced in the locale elements of the declaration - follow. - - In renamings parameters are referred to by position in the canonical - order; an underscore is used to skip a parameter position, which is - then not renamed. Renaming deletes the syntax of a parameter unless - a new mixfix annotation is given. +The second and third line contain the expression --- two + instances of the partial order locale with instantiations \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. - Parameter renamings are morphisms between locales. These can be - lifted to terms and theorems and thus be applied to assumptions and - conclusions. The assumption of a merge is the conjunction of the - assumptions of the merged locale. The conclusions of a merge are - obtained by appending the conclusions of the left locale and of the - right locale.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\begin{isamarkuptext}% -The locale \isa{order{\isacharunderscore}preserving} contains theorems for both - orders \isa{{\isasymsqsubseteq}} and \isa{{\isasympreceq}}. How can one refer to a theorem for - a particular order, \isa{{\isasymsqsubseteq}} or \isa{{\isasympreceq}}? Names in locales are - qualified by the locale parameters. More precisely, a name is - qualified by the parameters of the locale in which its declaration - occurs. Here are examples:% + Instances are \emph{morphisms} on locales. Their effect on the + parameters is naturally lifted to terms, propositions and theorems, + 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. + + The qualifiers in the expression are already a familiar concept from + the \isakeyword{interpretation} command. They serve to distinguish + names (in particular theorem names) for the two partial orders + within the locale. Qualifiers in the \isakeyword{locale} command + default to optional. Here are examples of theorems in locale \isa{order{\isacharunderscore}preserving}:% \end{isamarkuptext}% \isamarkuptrue% % @@ -528,8 +522,7 @@ \isamarkuptrue% % \begin{isamarkuptext}% -When renaming a locale, the morphism is also applied - to the qualifiers. Hence theorems for the partial order \isa{{\isasympreceq}} +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}% \ \ {\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% @@ -553,8 +546,7 @@ % \begin{isamarkuptext}% This example reveals that there is no infix syntax for the strict - version of \isa{{\isasympreceq}}! This can, of course, not be introduced - automatically, but it can be declared manually through an abbreviation.% + version of \isa{{\isasympreceq}}! This can be declared through an abbreviation.% \end{isamarkuptext}% \isamarkuptrue% \ \ \isacommand{abbreviation}\isamarkupfalse% @@ -567,26 +559,42 @@ \isamarkuptrue% % \begin{isamarkuptext}% -Not only names of theorems are qualified. In fact, all names - are qualified, in particular names introduced by definitions and - abbreviations. The name of the strict order of \isa{{\isasymsqsubseteq}} is \isa{le{\isachardot}less} and therefore \isa{le{\isacharprime}{\isachardot}less} is the name of the strict - order of \isa{{\isasympreceq}}. Hence, the equation in the above abbreviation - could have been written as \isa{less{\isacharprime}\ {\isasymequiv}\ le{\isacharprime}{\isachardot}less}.% +Qualifiers not only apply to theorem names, but also to names + introduced by definitions and abbreviations. In locale + \isa{partial{\isacharunderscore}order} the full name of the strict order of \isa{{\isasymsqsubseteq}} is + \isa{le{\isachardot}less} and therefore \isa{le{\isacharprime}{\isachardot}less} is the full name of + the strict order of \isa{{\isasympreceq}}. Hence, the equation in the + abbreviation above could have been also written as \isa{less{\isacharprime}\ {\isasymequiv}\ le{\isacharprime}{\isachardot}less}.% \end{isamarkuptext}% \isamarkuptrue% % \begin{isamarkuptext}% -Two more locales illustrate working with locale expressions. - A map \isa{{\isasymphi}} is a lattice homomorphism if it preserves meet and join.% +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 + declared by the locale expression and with their concrete syntax by + implicitly adding them to the beginning of the \isakeyword{for} + clause. + + The following locales illustrate this. A map \isa{{\isasymphi}} is a + lattice homomorphism if it preserves meet and join.% \end{isamarkuptext}% \isamarkuptrue% \ \ \isacommand{locale}\isamarkupfalse% -\ lattice{\isacharunderscore}hom\ {\isacharequal}\ 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 +\ lattice{\isacharunderscore}hom\ {\isacharequal}\isanewline +\ \ \ \ 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}\isanewline -\ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}lattice{\isachardot}meet\ le\ x\ y{\isacharparenright}\ {\isacharequal}\ lattice{\isachardot}meet\ le{\isacharprime}\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ \ \ {\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}\isanewline -\ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}lattice{\isachardot}join\ le\ x\ y{\isacharparenright}\ {\isacharequal}\ lattice{\isachardot}join\ le{\isacharprime}\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}x\ {\isasymsqunion}\ y{\isacharparenright}\ {\isacharequal}\ le{\isacharprime}{\isachardot}join\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline \isanewline \ \ \isacommand{abbreviation}\isamarkupfalse% \ {\isacharparenleft}\isakeyword{in}\ lattice{\isacharunderscore}hom{\isacharparenright}\isanewline @@ -599,8 +607,13 @@ \end{isamarkuptext}% \isamarkuptrue% \ \ \isacommand{locale}\isamarkupfalse% -\ lattice{\isacharunderscore}end\ {\isacharequal}\isanewline -\ \ \ \ lattice{\isacharunderscore}hom\ le\ le\ \isakeyword{for}\ le\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqsubseteq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}% +\ 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 then used to instantiate + the second parameter. Its concrete syntax is preseverd.% +\end{isamarkuptext}% +\isamarkuptrue% +% \begin{isamarkuptext}% The inheritance diagram of the situation we have now is shown in Figure~\ref{fig:hom}, where the dashed line depicts an @@ -648,7 +661,7 @@ \begin{isamarkuptext}% It can be shown easily that a lattice homomorphism is order preserving. As the final example of this section, a locale - interpretation is used to assert this.% + interpretation is used to assert this:% \end{isamarkuptext}% \isamarkuptrue% \ \ \isacommand{sublocale}\isamarkupfalse% @@ -688,6 +701,7 @@ \begin{isamarkuptext}% Theorems and other declarations --- syntax, in particular --- from the locale \isa{order{\isacharunderscore}preserving} are now active in \isa{lattice{\isacharunderscore}hom}, for example + \isa{le{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: \isa{{\isasymlbrakk}{\isacharquery}x\ {\isasymprec}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymprec}\ {\isacharquery}z}% \end{isamarkuptext}% @@ -709,7 +723,7 @@ Haftmann and Wenzel \cite{HaftmannWenzel2007} overcome a restriction of axiomatic type classes through a combination with locale interpretation. The result is a Haskell-style class system with a - facility to generate Haskell code. Classes are sufficient for + facility to generate ML and Haskell code. Classes are sufficient for simple specifications with a single type parameter. The locales for orders and lattices presented in this tutorial fall into this category. Order preserving maps, homomorphisms and vector spaces,