# HG changeset patch # User haftmann # Date 1238254412 -3600 # Node ID b3c851b0ea39526fc6872a680b2a14fc2fc7b2e9 # Parent 78d12065c638f3696537120695c7e3839dcf6450# Parent 16c689643a7a3f0e001acbc47b2b9bb6c46cbf14 merged diff -r 16c689643a7a -r b3c851b0ea39 doc-src/Locales/Locales/Examples3.thy --- a/doc-src/Locales/Locales/Examples3.thy Sat Mar 28 16:29:39 2009 +0100 +++ b/doc-src/Locales/Locales/Examples3.thy Sat Mar 28 16:33:32 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, @@ -447,7 +465,7 @@ & \textit{name} $|$ \textit{attribute} $|$ \textit{name} \textit{attribute} \\ \textit{qualifier} & ::= - & \textit{name} [``\textbf{!}''] \\[2ex] + & \textit{name} [``\textbf{?}'' $|$ ``\textbf{!}''] \\[2ex] \multicolumn{3}{l}{Context Elements} \\ @@ -493,7 +511,7 @@ & \textbf{where} \textit{name} ``\textbf{=}'' \textit{term} ( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\ \textit{instance} & ::= - & [ \textit{qualifier} \textbf{:} ] + & [ \textit{qualifier} ``\textbf{:}'' ] \textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\ \textit{expression} & ::= & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$ diff -r 16c689643a7a -r b3c851b0ea39 doc-src/Locales/Locales/document/Examples3.tex --- a/doc-src/Locales/Locales/document/Examples3.tex Sat Mar 28 16:29:39 2009 +0100 +++ b/doc-src/Locales/Locales/document/Examples3.tex Sat Mar 28 16:33:32 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, @@ -734,7 +748,7 @@ & \textit{name} $|$ \textit{attribute} $|$ \textit{name} \textit{attribute} \\ \textit{qualifier} & ::= - & \textit{name} [``\textbf{!}''] \\[2ex] + & \textit{name} [``\textbf{?}'' $|$ ``\textbf{!}''] \\[2ex] \multicolumn{3}{l}{Context Elements} \\ @@ -780,7 +794,7 @@ & \textbf{where} \textit{name} ``\textbf{=}'' \textit{term} ( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\ \textit{instance} & ::= - & [ \textit{qualifier} \textbf{:} ] + & [ \textit{qualifier} ``\textbf{:}'' ] \textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\ \textit{expression} & ::= & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$ diff -r 16c689643a7a -r b3c851b0ea39 etc/isar-keywords-ZF.el --- a/etc/isar-keywords-ZF.el Sat Mar 28 16:29:39 2009 +0100 +++ b/etc/isar-keywords-ZF.el Sat Mar 28 16:33:32 2009 +0100 @@ -18,6 +18,7 @@ "ML" "ML_command" "ML_prf" + "ML_test" "ML_val" "ProofGeneral\\.inform_file_processed" "ProofGeneral\\.inform_file_retracted" @@ -348,6 +349,7 @@ (defconst isar-keywords-theory-decl '("ML" + "ML_test" "abbreviation" "arities" "attribute_setup" diff -r 16c689643a7a -r b3c851b0ea39 etc/isar-keywords.el --- a/etc/isar-keywords.el Sat Mar 28 16:29:39 2009 +0100 +++ b/etc/isar-keywords.el Sat Mar 28 16:33:32 2009 +0100 @@ -18,6 +18,7 @@ "ML" "ML_command" "ML_prf" + "ML_test" "ML_val" "ProofGeneral\\.inform_file_processed" "ProofGeneral\\.inform_file_retracted" @@ -419,6 +420,7 @@ (defconst isar-keywords-theory-decl '("ML" + "ML_test" "abbreviation" "arities" "atom_decl" diff -r 16c689643a7a -r b3c851b0ea39 lib/jedit/isabelle.xml --- a/lib/jedit/isabelle.xml Sat Mar 28 16:29:39 2009 +0100 +++ b/lib/jedit/isabelle.xml Sat Mar 28 16:33:32 2009 +0100 @@ -45,6 +45,7 @@ ML ML_prf + ML_test abbreviation actions diff -r 16c689643a7a -r b3c851b0ea39 src/FOL/ex/LocaleTest.thy --- a/src/FOL/ex/LocaleTest.thy Sat Mar 28 16:29:39 2009 +0100 +++ b/src/FOL/ex/LocaleTest.thy Sat Mar 28 16:33:32 2009 +0100 @@ -1,7 +1,7 @@ -(* Title: FOL/ex/NewLocaleTest.thy +(* Title: FOL/ex/LocaleTest.thy Author: Clemens Ballarin, TU Muenchen -Testing environment for locale expressions. +Test environment for the locale implementation. *) theory LocaleTest diff -r 16c689643a7a -r b3c851b0ea39 src/HOL/ex/Formal_Power_Series_Examples.thy --- a/src/HOL/ex/Formal_Power_Series_Examples.thy Sat Mar 28 16:29:39 2009 +0100 +++ b/src/HOL/ex/Formal_Power_Series_Examples.thy Sat Mar 28 16:33:32 2009 +0100 @@ -191,31 +191,39 @@ lemma E_minus_ii_sin_cos: "E (- (ii * c)) = fps_cos c - fps_const ii * fps_sin c " unfolding minus_mult_right Eii_sin_cos by simp +lemma fps_const_minus: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d) "by (simp add: fps_eq_iff fps_const_def) + +lemma fps_number_of_fps_const: "number_of i = fps_const (number_of i :: 'a:: {comm_ring_1, number_ring})" + apply (subst (2) number_of_eq) +apply(rule int_induct[of _ 0]) +apply (simp_all add: number_of_fps_def) +by (simp_all add: fps_const_add[symmetric] fps_const_minus[symmetric]) + lemma fps_cos_Eii: "fps_cos c = (E (ii * c) + E (- ii * c)) / fps_const 2" proof- have th: "fps_cos c + fps_cos c = fps_cos c * fps_const 2" - by (simp add: fps_eq_iff) + by (simp add: fps_eq_iff fps_number_of_fps_const complex_number_of_def[symmetric]) show ?thesis unfolding Eii_sin_cos minus_mult_commute - by (simp add: fps_divide_def fps_const_inverse th) + by (simp add: fps_number_of_fps_const fps_divide_def fps_const_inverse th complex_number_of_def[symmetric]) qed lemma fps_sin_Eii: "fps_sin c = (E (ii * c) - E (- ii * c)) / fps_const (2*ii)" proof- have th: "fps_const \ * fps_sin c + fps_const \ * fps_sin c = fps_sin c * fps_const (2 * ii)" - by (simp add: fps_eq_iff) + by (simp add: fps_eq_iff fps_number_of_fps_const complex_number_of_def[symmetric]) show ?thesis unfolding Eii_sin_cos minus_mult_commute by (simp add: fps_divide_def fps_const_inverse th) qed lemma fps_const_mult_2: "fps_const (2::'a::number_ring) * a = a +a" - by (simp add: fps_eq_iff) + by (simp add: fps_eq_iff fps_number_of_fps_const) lemma fps_const_mult_2_right: "a * fps_const (2::'a::number_ring) = a +a" - by (simp add: fps_eq_iff) + by (simp add: fps_eq_iff fps_number_of_fps_const) lemma fps_tan_Eii: "fps_tan c = (E (ii * c) - E (- ii * c)) / (fps_const ii * (E (ii * c) + E (- ii * c)))"