# HG changeset patch # User ballarin # Date 1238274861 -3600 # Node ID c3f1e8a9e0b56545fbef4c5afdc70a5ba0637773 # Parent 492ca5d4f2353f1844f12120f8d9e03fd049f0d2 Default mode of qualifiers in locale commands. diff -r 492ca5d4f235 -r c3f1e8a9e0b5 doc-src/Locales/Locales/Examples.thy --- a/doc-src/Locales/Locales/Examples.thy Sat Mar 28 21:07:04 2009 +0100 +++ b/doc-src/Locales/Locales/Examples.thy Sat Mar 28 22:14:21 2009 +0100 @@ -252,7 +252,8 @@ additionally outputs the conclusions. The syntax of the locale commands discussed in this tutorial is - shown in Table~\ref{tab:commands}. See the + 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} for full documentation. *} diff -r 492ca5d4f235 -r c3f1e8a9e0b5 doc-src/Locales/Locales/Examples1.thy --- a/doc-src/Locales/Locales/Examples1.thy Sat Mar 28 21:07:04 2009 +0100 +++ b/doc-src/Locales/Locales/Examples1.thy Sat Mar 28 22:14:21 2009 +0100 @@ -43,13 +43,12 @@ @{text partial_order} in the global context of the theory. The parameter @{term le} is replaced by @{term "op \ :: nat \ nat \ bool"}. *} - interpretation %visible nat!: partial_order "op \ :: nat \ nat \ bool" + interpretation %visible nat: partial_order "op \ :: nat \ nat \ bool" txt {* The locale name is succeeded by a \emph{parameter - instantiation}. In general, this is a list of terms, which refer to + 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 prefix}, - which is used to qualify names from the locale in the global - context. + locale name is preceded by an optional \emph{interpretation + qualifier}. The command creates the goal% \footnote{Note that @{text op} binds tighter than functions @@ -62,14 +61,12 @@ interpreted for natural numbers, for example @{thm [source] nat.trans}: @{thm [display, indent=2] nat.trans} - Interpretation accepts a qualifier, @{text nat} in the example, - which is applied to all names processed by the interpretation. If - followed by an exclamation point the qualifier is mandatory --- that - is, the above theorem cannot be referred to simply by @{text trans}. - A qualifier succeeded by an exclamation point is called - \emph{strict}. It prevents unwanted hiding of theorems. It is - advisable to use strict qualifiers for all interpretations in - theories. *} + 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. *} subsection {* Second Version: Replacement of Definitions *} diff -r 492ca5d4f235 -r c3f1e8a9e0b5 doc-src/Locales/Locales/Examples2.thy --- a/doc-src/Locales/Locales/Examples2.thy Sat Mar 28 21:07:04 2009 +0100 +++ b/doc-src/Locales/Locales/Examples2.thy Sat Mar 28 22:14:21 2009 +0100 @@ -7,7 +7,7 @@ \isakeyword{where} and require proofs. The revised command that replaces @{text "\"} by @{text "<"}, is: *} -interpretation %visible nat!: partial_order "op \ :: [nat, nat] \ bool" +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]} diff -r 492ca5d4f235 -r c3f1e8a9e0b5 doc-src/Locales/Locales/Examples3.thy --- a/doc-src/Locales/Locales/Examples3.thy Sat Mar 28 21:07:04 2009 +0100 +++ b/doc-src/Locales/Locales/Examples3.thy Sat Mar 28 22:14:21 2009 +0100 @@ -14,7 +14,7 @@ \isakeyword{interpret}). This interpretation is inside the proof of the global interpretation. The third revision of the example illustrates this. *} -interpretation %visible nat!: partial_order "op \ :: nat \ nat \ bool" +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)" @@ -48,7 +48,7 @@ interpretation is reproduced in order to give an example of a more elaborate interpretation proof. *} -interpretation %visible nat!: lattice "op \ :: nat \ nat \ bool" +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 - @@ -73,7 +73,7 @@ text {* That the relation @{text \} is a total order completes this sequence of interpretations. *} -interpretation %visible nat!: total_order "op \ :: nat \ nat \ bool" +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 @@ -146,7 +146,7 @@ divisibility. Instead, interpretation substitutes @{term "x dvd y \ x \ y"}. *} -interpretation nat_dvd!: lattice "op dvd :: nat \ nat \ bool" +interpretation nat_dvd: lattice "op dvd :: nat \ nat \ bool" where nat_dvd_meet_eq: "lattice.meet op dvd = gcd" and nat_dvd_join_eq: @@ -199,7 +199,7 @@ lemma %invisible gcd_lcm_distr: "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)" sorry -interpretation %visible nat_dvd!: +interpretation %visible nat_dvd: distrib_lattice "op dvd :: nat \ nat \ bool" apply unfold_locales txt {* @{subgoals [display]} *} @@ -284,11 +284,13 @@ 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 @{text - order_preserving}: *} + 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 @@ -359,7 +361,7 @@ 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. *} + the second parameter. Its concrete syntax is preserved. *} text {* The inheritance diagram of the situation we have now is shown diff -r 492ca5d4f235 -r c3f1e8a9e0b5 doc-src/Locales/Locales/document/Examples.tex --- a/doc-src/Locales/Locales/document/Examples.tex Sat Mar 28 21:07:04 2009 +0100 +++ b/doc-src/Locales/Locales/document/Examples.tex Sat Mar 28 22:14:21 2009 +0100 @@ -481,7 +481,8 @@ additionally outputs the conclusions. The syntax of the locale commands discussed in this tutorial is - shown in Table~\ref{tab:commands}. See the + 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} for full documentation.% \end{isamarkuptext}% diff -r 492ca5d4f235 -r c3f1e8a9e0b5 doc-src/Locales/Locales/document/Examples1.tex --- a/doc-src/Locales/Locales/document/Examples1.tex Sat Mar 28 21:07:04 2009 +0100 +++ b/doc-src/Locales/Locales/document/Examples1.tex Sat Mar 28 22:14:21 2009 +0100 @@ -72,14 +72,13 @@ % \isatagvisible \isacommand{interpretation}\isamarkupfalse% -\ nat{\isacharbang}{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}% +\ 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}. In general, this is a list of terms, which refer to + 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 prefix}, - which is used to qualify names from the locale in the global - context. + locale name is preceded by an optional \emph{interpretation + qualifier}. The command creates the goal% \footnote{Note that \isa{op} binds tighter than functions @@ -104,14 +103,12 @@ \ \ {\isasymlbrakk}{\isacharquery}x\ {\isasymle}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymle}\ {\isacharquery}z% \end{isabelle} - Interpretation accepts a qualifier, \isa{nat} in the example, - which is applied to all names processed by the interpretation. If - followed by an exclamation point the qualifier is mandatory --- that - is, the above theorem cannot be referred to simply by \isa{trans}. - A qualifier succeeded by an exclamation point is called - \emph{strict}. It prevents unwanted hiding of theorems. It is - advisable to use strict qualifiers for all interpretations in - theories.% + 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.% \end{isamarkuptext}% \isamarkuptrue% % diff -r 492ca5d4f235 -r c3f1e8a9e0b5 doc-src/Locales/Locales/document/Examples2.tex --- a/doc-src/Locales/Locales/document/Examples2.tex Sat Mar 28 21:07:04 2009 +0100 +++ b/doc-src/Locales/Locales/document/Examples2.tex Sat Mar 28 22:14:21 2009 +0100 @@ -32,7 +32,7 @@ % \isatagvisible \isacommand{interpretation}\isamarkupfalse% -\ nat{\isacharbang}{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}nat{\isacharcomma}\ nat{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline +\ 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% \ {\isacharminus}% diff -r 492ca5d4f235 -r c3f1e8a9e0b5 doc-src/Locales/Locales/document/Examples3.tex --- a/doc-src/Locales/Locales/document/Examples3.tex Sat Mar 28 21:07:04 2009 +0100 +++ b/doc-src/Locales/Locales/document/Examples3.tex Sat Mar 28 22:14:21 2009 +0100 @@ -41,7 +41,7 @@ % \isatagvisible \isacommand{interpretation}\isamarkupfalse% -\ nat{\isacharbang}{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline +\ 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% \ {\isacharminus}\isanewline @@ -104,7 +104,7 @@ % \isatagvisible \isacommand{interpretation}\isamarkupfalse% -\ nat{\isacharbang}{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline +\ 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% @@ -174,7 +174,7 @@ % \isatagvisible \isacommand{interpretation}\isamarkupfalse% -\ nat{\isacharbang}{\isacharcolon}\ total{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline +\ nat{\isacharcolon}\ total{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline \ \ \isacommand{by}\isamarkupfalse% \ unfold{\isacharunderscore}locales\ arith% \endisatagvisible @@ -285,7 +285,7 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{interpretation}\isamarkupfalse% -\ nat{\isacharunderscore}dvd{\isacharbang}{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline +\ 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}\isanewline \ \ \ \ \ \ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ dvd\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline \ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq{\isacharcolon}\isanewline @@ -381,7 +381,7 @@ % \isatagvisible \isacommand{interpretation}\isamarkupfalse% -\ nat{\isacharunderscore}dvd{\isacharbang}{\isacharcolon}\isanewline +\ nat{\isacharunderscore}dvd{\isacharcolon}\isanewline \ \ distrib{\isacharunderscore}lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline \ \ \isacommand{apply}\isamarkupfalse% \ unfold{\isacharunderscore}locales% @@ -493,10 +493,13 @@ 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}:% + 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% % @@ -610,7 +613,7 @@ \ 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.% + the second parameter. Its concrete syntax is preserved.% \end{isamarkuptext}% \isamarkuptrue% %