# HG changeset patch # User ballarin # Date 1232393828 -3600 # Node ID 937baa077df272183d8ec081001e9f0873e31fde # Parent 3c6cd80a48541e152c03aee9f82d7a39eaf3b3b4 Fixed tutorial to compile with new locales; grammar of new locale commands. diff -r 3c6cd80a4854 -r 937baa077df2 doc-src/Locales/Locales/Examples.thy --- a/doc-src/Locales/Locales/Examples.thy Tue Dec 30 16:50:46 2008 +0100 +++ b/doc-src/Locales/Locales/Examples.thy Mon Jan 19 20:37:08 2009 +0100 @@ -608,9 +608,9 @@ 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{interpretation} command. *} + with the \isakeyword{sublocale} command. *} - interpretation %visible total_order \ lattice + 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 @@ -652,7 +652,7 @@ text {* Similarly, total orders are distributive lattices. *} - interpretation total_order \ distrib_lattice + sublocale total_order \ distrib_lattice proof unfold_locales fix %"proof" x y z show "x \ (y \ z) = x \ y \ x \ z" (is "?l = ?r") diff -r 3c6cd80a4854 -r 937baa077df2 doc-src/Locales/Locales/Examples1.thy --- a/doc-src/Locales/Locales/Examples1.thy Tue Dec 30 16:50:46 2008 +0100 +++ b/doc-src/Locales/Locales/Examples1.thy Mon Jan 19 20:37:08 2009 +0100 @@ -45,7 +45,7 @@ @{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 the parameters in the order of declaration in the locale. The diff -r 3c6cd80a4854 -r 937baa077df2 doc-src/Locales/Locales/Examples2.thy --- a/doc-src/Locales/Locales/Examples2.thy Tue Dec 30 16:50:46 2008 +0100 +++ b/doc-src/Locales/Locales/Examples2.thy Mon Jan 19 20:37:08 2009 +0100 @@ -9,7 +9,7 @@ \isakeyword{where} and require proofs. The revised command, replacing @{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 3c6cd80a4854 -r 937baa077df2 doc-src/Locales/Locales/Examples3.thy --- a/doc-src/Locales/Locales/Examples3.thy Tue Dec 30 16:50:46 2008 +0100 +++ b/doc-src/Locales/Locales/Examples3.thy Mon Jan 19 20:37:08 2009 +0100 @@ -16,12 +16,12 @@ \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)" by unfold_locales auto - then interpret nat: partial_order ["op \ :: [nat, nat] \ bool"] . + 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 @@ -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 - @@ -63,7 +63,7 @@ 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"] . + 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" @@ -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 @@ -130,12 +130,12 @@ but not a total order. Interpretation again proceeds incrementally. *} -interpretation nat_dvd: partial_order ["op dvd :: nat \ nat \ bool"] +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"] . + 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 @@ -145,7 +145,7 @@ text {* Note that there is no symbol for strict 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: @@ -159,7 +159,7 @@ apply (rule_tac x = "lcm x y" in exI) apply (auto intro: lcm_dvd1 lcm_dvd2 lcm_least) done - then interpret nat_dvd: lattice ["op dvd :: nat \ nat \ bool"] . + then interpret nat_dvd: lattice "op dvd :: nat \ nat \ bool" . show "lattice.meet op dvd = gcd" apply (auto simp add: expand_fun_eq) apply (unfold nat_dvd.meet_def) @@ -203,7 +203,7 @@ ML %invisible {* reset quick_and_dirty *} interpretation %visible nat_dvd: - distrib_lattice ["op dvd :: nat \ nat \ bool"] + distrib_lattice "op dvd :: nat \ nat \ bool" apply unfold_locales txt {* @{subgoals [display]} *} apply (unfold nat_dvd_meet_eq nat_dvd_join_eq) @@ -262,7 +262,7 @@ preserving maps can be declared in the following way. *} locale order_preserving = - partial_order + partial_order le' (infixl "\" 50) + + le: partial_order + le': partial_order le' for le' (infixl "\" 50) + fixes \ :: "'a \ 'b" assumes hom_le: "x \ y \ \ x \ \ y" @@ -300,7 +300,7 @@ text {* @{thm [source] le.less_le_trans}: @{thm le.less_le_trans} - @{thm [source] le_le'_\.hom_le}: @{thm le_le'_\.hom_le} + @{thm [source] hom_le}: @{thm hom_le} *} text {* When renaming a locale, the morphism is also applied @@ -331,7 +331,7 @@ text {* Two more locales illustrate working with locale expressions. A map @{text \} is a lattice homomorphism if it preserves meet and join. *} - locale lattice_hom = lattice + lattice le' (infixl "\" 50) + + 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)" @@ -346,7 +346,7 @@ text {* A homomorphism is an endomorphism if both orders coincide. *} locale lattice_end = - lattice_hom le (infixl "\" 50) le (infixl "\" 50) + lattice_hom le le for le (infixl "\" 50) text {* The inheritance diagram of the situation we have now is shown in Figure~\ref{fig:hom}, where the dashed line depicts an @@ -395,7 +395,7 @@ preserving. As the final example of this section, a locale interpretation is used to assert this. *} - interpretation lattice_hom \ order_preserving proof unfold_locales + sublocale lattice_hom \ order_preserving proof unfold_locales fix x y assume "x \ y" then have "y = (x \ y)" by (simp add: le.join_connection) @@ -448,7 +448,9 @@ \textit{attr-name} & ::= & \textit{name} $|$ \textit{attribute} $|$ - \textit{name} \textit{attribute} \\[2ex] + \textit{name} \textit{attribute} \\ + \textit{qualifier} & ::= + & \textit{name} [``\textbf{!}''] \\[2ex] \multicolumn{3}{l}{Context Elements} \\ @@ -488,19 +490,23 @@ \multicolumn{3}{l}{Locale Expressions} \\ - \textit{rename} & ::= - & \textit{name} [ \textit{mixfix} ] $|$ ``\textbf{\_}'' \\ - \textit{expr} & ::= - & \textit{renamed-expr} ( ``\textbf{+}'' \textit{renamed-expr} )$^*$ \\ - \textit{renamed-expr} & ::= - & ( \textit{qualified-name} $|$ - ``\textbf{(}'' \textit{expr} ``\textbf{)}'' ) \textit{rename}$^*$ \\[2ex] + \textit{pos-insts} & ::= + & ( \textit{term} $|$ ``\textbf{\_}'' )$^*$ \\ + \textit{named-insts} & ::= + & \textbf{where} \textit{name} ``\textbf{=}'' \textit{term} + ( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\ + \textit{instance} & ::= + & [ \textit{qualifier} \textbf{:} ] + \textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\ + \textit{expression} & ::= + & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$ + [ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex] \multicolumn{3}{l}{Declaration of Locales} \\ \textit{locale} & ::= & \textit{element}$^+$ \\ - & | & \textit{locale-expr} [ ``\textbf{+}'' \textit{element}$^+$ ] \\ + & | & \textit{expression} [ ``\textbf{+}'' \textit{element}$^+$ ] \\ \textit{toplevel} & ::= & \textbf{locale} \textit{name} [ ``\textbf{=}'' \textit{locale} ] \\[2ex] @@ -509,19 +515,17 @@ \textit{equation} & ::= & [ \textit{attr-name} ``\textbf{:}'' ] \textit{prop} \\ - \textit{insts} & ::= & [ ``\textbf{[}'' \textit{term}$^+$ - ``\textbf{]}'' ] \\ - & & [ \textbf{where} \textit{equation} ( \textbf{and} - \textit{equation} )$^*$ ] \\ + \textit{equations} & ::= & \textbf{where} \textit{equation} ( \textbf{and} + \textit{equation} )$^*$ \\ \textit{toplevel} & ::= - & \textbf{interpretation} \textit{name} ( ``$<$'' $|$ - ``$\subseteq$'' ) \textit{expr} \textit{proof} \\ + & \textbf{sublocale} \textit{name} ( ``$<$'' $|$ + ``$\subseteq$'' ) \textit{expression} \textit{proof} \\ & | - & \textbf{interpretation} [ \textit{attr-name} ``\textbf{:}'' ] - \textit{expr} \textit{insts} \textit{proof} \\ + & \textbf{interpretation} + \textit{expression} [ \textit{equations} ] \textit{proof} \\ & | - & \textbf{interpret} [ \textit{attr-name} ``\textbf{:}'' ] - \textit{expr} \textit{insts} \textit{proof} \\[2ex] + & \textbf{interpret} + \textit{expression} \textit{proof} \\[2ex] \multicolumn{3}{l}{Diagnostics} \\ @@ -531,7 +535,7 @@ \end{tabular} \end{center} \hrule -\caption{Syntax of Locale Commands.} +\caption{Syntax of Locale Commands (abrigded).} \label{tab:commands} \end{table} *} diff -r 3c6cd80a4854 -r 937baa077df2 doc-src/Locales/Locales/document/Examples.tex --- a/doc-src/Locales/Locales/document/Examples.tex Tue Dec 30 16:50:46 2008 +0100 +++ b/doc-src/Locales/Locales/document/Examples.tex Mon Jan 19 20:37:08 2009 +0100 @@ -1213,7 +1213,7 @@ 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{interpretation} command.% + with the \isakeyword{sublocale} command.% \end{isamarkuptext}% \isamarkuptrue% % @@ -1222,7 +1222,7 @@ \endisadelimvisible % \isatagvisible -\isacommand{interpretation}\isamarkupfalse% +\isacommand{sublocale}\isamarkupfalse% \ total{\isacharunderscore}order\ {\isasymsubseteq}\ lattice% \begin{isamarkuptxt}% This enters the context of locale \isa{total{\isacharunderscore}order}, in @@ -1325,7 +1325,7 @@ Similarly, total orders are distributive lattices.% \end{isamarkuptext}% \isamarkuptrue% -\ \ \isacommand{interpretation}\isamarkupfalse% +\ \ \isacommand{sublocale}\isamarkupfalse% \ total{\isacharunderscore}order\ {\isasymsubseteq}\ distrib{\isacharunderscore}lattice\isanewline % \isadelimproof diff -r 3c6cd80a4854 -r 937baa077df2 doc-src/Locales/Locales/document/Examples1.tex --- a/doc-src/Locales/Locales/document/Examples1.tex Tue Dec 30 16:50:46 2008 +0100 +++ b/doc-src/Locales/Locales/document/Examples1.tex Mon Jan 19 20:37:08 2009 +0100 @@ -74,7 +74,7 @@ % \isatagvisible \isacommand{interpretation}\isamarkupfalse% -\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}% +\ 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 diff -r 3c6cd80a4854 -r 937baa077df2 doc-src/Locales/Locales/document/Examples2.tex --- a/doc-src/Locales/Locales/document/Examples2.tex Tue Dec 30 16:50:46 2008 +0100 +++ b/doc-src/Locales/Locales/document/Examples2.tex Mon Jan 19 20:37:08 2009 +0100 @@ -34,7 +34,7 @@ % \isatagvisible \isacommand{interpretation}\isamarkupfalse% -\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}nat{\isacharcomma}\ nat{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\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 3c6cd80a4854 -r 937baa077df2 doc-src/Locales/Locales/document/Examples3.tex --- a/doc-src/Locales/Locales/document/Examples3.tex Tue Dec 30 16:50:46 2008 +0100 +++ b/doc-src/Locales/Locales/document/Examples3.tex Mon Jan 19 20:37:08 2009 +0100 @@ -43,7 +43,7 @@ % \isatagvisible \isacommand{interpretation}\isamarkupfalse% -\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\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\ {\isacharparenleft}op\ {\isasymle}{\isacharparenright}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline \isacommand{proof}\isamarkupfalse% \ {\isacharminus}\isanewline @@ -53,7 +53,7 @@ \ unfold{\isacharunderscore}locales\ auto\isanewline \ \ \isacommand{then}\isamarkupfalse% \ \isacommand{interpret}\isamarkupfalse% -\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}nat{\isacharcomma}\ nat{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}}\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% \ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ {\isacharparenleft}op\ {\isasymle}{\isacharparenright}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline @@ -91,8 +91,8 @@ \begin{isamarkuptext}% Further interpretations are necessary to reuse theorems from the other locales. In \isa{lattice} the operations \isa{{\isasymsqinter}} and - \isa{{\isasymsqunion}} are substituted by \isa{ord{\isacharunderscore}class{\isachardot}min} and - \isa{ord{\isacharunderscore}class{\isachardot}max}. The entire proof for the + \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 elaborate interpretation proof.% \end{isamarkuptext}% @@ -104,7 +104,7 @@ % \isatagvisible \isacommand{interpretation}\isamarkupfalse% -\ nat{\isacharcolon}\ lattice\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\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% @@ -143,7 +143,7 @@ \isamarkuptrue% \ \ \isacommand{then}\isamarkupfalse% \ \isacommand{interpret}\isamarkupfalse% -\ nat{\isacharcolon}\ lattice\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}}\isamarkupfalse% +\ nat{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse% \isanewline \ \ \isacommand{show}\isamarkupfalse% \ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline @@ -174,7 +174,7 @@ % \isatagvisible \isacommand{interpretation}\isamarkupfalse% -\ nat{\isacharcolon}\ total{\isacharunderscore}order\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\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 @@ -196,11 +196,11 @@ \isa{nat{\isachardot}less{\isacharunderscore}def} from locale \isa{partial{\isacharunderscore}order}: \\ \quad \isa{{\isacharparenleft}{\isacharquery}x\ {\isacharless}\ {\isacharquery}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharquery}x\ {\isasymle}\ {\isacharquery}y\ {\isasymand}\ {\isacharquery}x\ {\isasymnoteq}\ {\isacharquery}y{\isacharparenright}} \\ \isa{nat{\isachardot}meet{\isacharunderscore}left} from locale \isa{lattice}: \\ - \quad \isa{ord{\isacharunderscore}class{\isachardot}min\ {\isacharquery}x\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}x} \\ + \quad \isa{min\ {\isacharquery}x\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}x} \\ \isa{nat{\isachardot}join{\isacharunderscore}distr} from locale \isa{distrib{\isacharunderscore}lattice}: \\ - \quad \isa{ord{\isacharunderscore}class{\isachardot}max\ {\isacharquery}x\ {\isacharparenleft}ord{\isacharunderscore}class{\isachardot}min\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ ord{\isacharunderscore}class{\isachardot}min\ {\isacharparenleft}ord{\isacharunderscore}class{\isachardot}max\ {\isacharquery}x\ {\isacharquery}y{\isacharparenright}\ {\isacharparenleft}ord{\isacharunderscore}class{\isachardot}max\ {\isacharquery}x\ {\isacharquery}z{\isacharparenright}} \\ + \quad \isa{lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharquery}x\ {\isacharparenleft}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharquery}x\ {\isacharquery}y{\isacharparenright}\ {\isacharparenleft}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharquery}x\ {\isacharquery}z{\isacharparenright}} \\ \isa{nat{\isachardot}less{\isacharunderscore}total} from locale \isa{total{\isacharunderscore}order}: \\ - \quad \isa{{\isacharquery}x\ {\isacharless}\ {\isacharquery}y\ {\isasymor}\ {\isacharquery}x\ {\isacharequal}\ {\isacharquery}y\ {\isasymor}\ {\isacharquery}y\ {\isacharless}\ {\isacharquery}x} + \quad \isa{partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharquery}x\ {\isacharquery}y\ {\isasymor}\ {\isacharquery}x\ {\isacharequal}\ {\isacharquery}y\ {\isasymor}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharquery}y\ {\isacharquery}x} \end{tabular} \end{center} \hrule @@ -244,7 +244,7 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{interpretation}\isamarkupfalse% -\ nat{\isacharunderscore}dvd{\isacharcolon}\ partial{\isacharunderscore}order\ {\isacharbrackleft}{\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\isanewline +\ 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 % \isadelimproof @@ -260,7 +260,7 @@ \ unfold{\isacharunderscore}locales\ {\isacharparenleft}auto\ simp{\isacharcolon}\ dvd{\isacharunderscore}def{\isacharparenright}\isanewline \ \ \isacommand{then}\isamarkupfalse% \ \isacommand{interpret}\isamarkupfalse% -\ nat{\isacharunderscore}dvd{\isacharcolon}\ partial{\isacharunderscore}order\ {\isacharbrackleft}{\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}}\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% \ {\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 @@ -285,7 +285,7 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{interpretation}\isamarkupfalse% -\ nat{\isacharunderscore}dvd{\isacharcolon}\ lattice\ {\isacharbrackleft}{\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\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 @@ -316,7 +316,7 @@ \isanewline \ \ \isacommand{then}\isamarkupfalse% \ \isacommand{interpret}\isamarkupfalse% -\ nat{\isacharunderscore}dvd{\isacharcolon}\ lattice\ {\isacharbrackleft}{\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}}\isamarkupfalse% +\ nat{\isacharunderscore}dvd{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse% \isanewline \ \ \isacommand{show}\isamarkupfalse% \ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ dvd\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline @@ -390,7 +390,7 @@ \isatagvisible \isacommand{interpretation}\isamarkupfalse% \ nat{\isacharunderscore}dvd{\isacharcolon}\isanewline -\ \ distrib{\isacharunderscore}lattice\ {\isacharbrackleft}{\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\isanewline +\ \ distrib{\isacharunderscore}lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline \ \ \isacommand{apply}\isamarkupfalse% \ unfold{\isacharunderscore}locales% \begin{isamarkuptxt}% @@ -434,7 +434,7 @@ \isa{nat{\isacharunderscore}dvd{\isachardot}meet{\isacharunderscore}left} from locale \isa{lattice}: \\ \quad \isa{gcd\ {\isacharquery}x\ {\isacharquery}y\ dvd\ {\isacharquery}x} \\ \isa{nat{\isacharunderscore}dvd{\isachardot}join{\isacharunderscore}distr} from locale \isa{distrib{\isacharunderscore}lattice}: \\ - \quad \isa{lcm\ {\isacharquery}x\ {\isacharparenleft}gcd\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ gcd\ {\isacharparenleft}lcm\ {\isacharquery}x\ {\isacharquery}y{\isacharparenright}\ {\isacharparenleft}lcm\ {\isacharquery}x\ {\isacharquery}z{\isacharparenright}} \\ + \quad \isa{lattice{\isachardot}join\ op\ dvd\ {\isacharquery}x\ {\isacharparenleft}lattice{\isachardot}meet\ op\ dvd\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ lattice{\isachardot}meet\ op\ dvd\ {\isacharparenleft}lattice{\isachardot}join\ op\ dvd\ {\isacharquery}x\ {\isacharquery}y{\isacharparenright}\ {\isacharparenleft}lattice{\isachardot}join\ op\ dvd\ {\isacharquery}x\ {\isacharquery}z{\isacharparenright}} \\ \end{tabular} \end{center} \hrule @@ -476,7 +476,7 @@ \isamarkuptrue% \ \ \isacommand{locale}\isamarkupfalse% \ order{\isacharunderscore}preserving\ {\isacharequal}\isanewline -\ \ \ \ partial{\isacharunderscore}order\ {\isacharplus}\ partial{\isacharunderscore}order\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\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 \ \ \ \ \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}% @@ -531,7 +531,7 @@ \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{\isacharunderscore}le{\isacharprime}{\isacharunderscore}{\isasymphi}{\isachardot}hom{\isacharunderscore}le}: \isa{{\isacharquery}x\ {\isasymsqsubseteq}\ {\isacharquery}y\ {\isasymLongrightarrow}\ {\isasymphi}\ {\isacharquery}x\ {\isasympreceq}\ {\isasymphi}\ {\isacharquery}y}% + \isa{hom{\isacharunderscore}le}: \isa{{\isacharquery}x\ {\isasymsqsubseteq}\ {\isacharquery}y\ {\isasymLongrightarrow}\ {\isasymphi}\ {\isacharquery}x\ {\isasympreceq}\ {\isasymphi}\ {\isacharquery}y}% \end{isamarkuptext}% \isamarkuptrue% % @@ -589,7 +589,7 @@ \end{isamarkuptext}% \isamarkuptrue% \ \ \isacommand{locale}\isamarkupfalse% -\ lattice{\isacharunderscore}hom\ {\isacharequal}\ lattice\ {\isacharplus}\ lattice\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline +\ 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 \ \ \ \ \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 @@ -608,7 +608,7 @@ \isamarkuptrue% \ \ \isacommand{locale}\isamarkupfalse% \ lattice{\isacharunderscore}end\ {\isacharequal}\isanewline -\ \ \ \ lattice{\isacharunderscore}hom\ le\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqsubseteq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ le\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqsubseteq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}% +\ \ \ \ lattice{\isacharunderscore}hom\ le\ le\ \isakeyword{for}\ le\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqsubseteq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}% \begin{isamarkuptext}% The inheritance diagram of the situation we have now is shown in Figure~\ref{fig:hom}, where the dashed line depicts an @@ -659,7 +659,7 @@ interpretation is used to assert this.% \end{isamarkuptext}% \isamarkuptrue% -\ \ \isacommand{interpretation}\isamarkupfalse% +\ \ \isacommand{sublocale}\isamarkupfalse% \ lattice{\isacharunderscore}hom\ {\isasymsubseteq}\ order{\isacharunderscore}preserving% \isadelimproof \ % @@ -741,7 +741,9 @@ \textit{attr-name} & ::= & \textit{name} $|$ \textit{attribute} $|$ - \textit{name} \textit{attribute} \\[2ex] + \textit{name} \textit{attribute} \\ + \textit{qualifier} & ::= + & \textit{name} [``\textbf{!}''] \\[2ex] \multicolumn{3}{l}{Context Elements} \\ @@ -781,19 +783,23 @@ \multicolumn{3}{l}{Locale Expressions} \\ - \textit{rename} & ::= - & \textit{name} [ \textit{mixfix} ] $|$ ``\textbf{\_}'' \\ - \textit{expr} & ::= - & \textit{renamed-expr} ( ``\textbf{+}'' \textit{renamed-expr} )$^*$ \\ - \textit{renamed-expr} & ::= - & ( \textit{qualified-name} $|$ - ``\textbf{(}'' \textit{expr} ``\textbf{)}'' ) \textit{rename}$^*$ \\[2ex] + \textit{pos-insts} & ::= + & ( \textit{term} $|$ ``\textbf{\_}'' )$^*$ \\ + \textit{named-insts} & ::= + & \textbf{where} \textit{name} ``\textbf{=}'' \textit{term} + ( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\ + \textit{instance} & ::= + & [ \textit{qualifier} \textbf{:} ] + \textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\ + \textit{expression} & ::= + & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$ + [ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex] \multicolumn{3}{l}{Declaration of Locales} \\ \textit{locale} & ::= & \textit{element}$^+$ \\ - & | & \textit{locale-expr} [ ``\textbf{+}'' \textit{element}$^+$ ] \\ + & | & \textit{expression} [ ``\textbf{+}'' \textit{element}$^+$ ] \\ \textit{toplevel} & ::= & \textbf{locale} \textit{name} [ ``\textbf{=}'' \textit{locale} ] \\[2ex] @@ -802,19 +808,17 @@ \textit{equation} & ::= & [ \textit{attr-name} ``\textbf{:}'' ] \textit{prop} \\ - \textit{insts} & ::= & [ ``\textbf{[}'' \textit{term}$^+$ - ``\textbf{]}'' ] \\ - & & [ \textbf{where} \textit{equation} ( \textbf{and} - \textit{equation} )$^*$ ] \\ + \textit{equations} & ::= & \textbf{where} \textit{equation} ( \textbf{and} + \textit{equation} )$^*$ \\ \textit{toplevel} & ::= - & \textbf{interpretation} \textit{name} ( ``$<$'' $|$ - ``$\subseteq$'' ) \textit{expr} \textit{proof} \\ + & \textbf{sublocale} \textit{name} ( ``$<$'' $|$ + ``$\subseteq$'' ) \textit{expression} \textit{proof} \\ & | - & \textbf{interpretation} [ \textit{attr-name} ``\textbf{:}'' ] - \textit{expr} \textit{insts} \textit{proof} \\ + & \textbf{interpretation} + \textit{expression} [ \textit{equations} ] \textit{proof} \\ & | - & \textbf{interpret} [ \textit{attr-name} ``\textbf{:}'' ] - \textit{expr} \textit{insts} \textit{proof} \\[2ex] + & \textbf{interpret} + \textit{expression} \textit{proof} \\[2ex] \multicolumn{3}{l}{Diagnostics} \\ @@ -824,7 +828,7 @@ \end{tabular} \end{center} \hrule -\caption{Syntax of Locale Commands.} +\caption{Syntax of Locale Commands (abrigded).} \label{tab:commands} \end{table}% \end{isamarkuptext}% diff -r 3c6cd80a4854 -r 937baa077df2 doc-src/Locales/Locales/document/root.tex --- a/doc-src/Locales/Locales/document/root.tex Tue Dec 30 16:50:46 2008 +0100 +++ b/doc-src/Locales/Locales/document/root.tex Mon Jan 19 20:37:08 2009 +0100 @@ -22,14 +22,17 @@ \begin{document} -\title{Tutorial to Locales and Locale Interpretation} +\title{Tutorial to Locales and Locale Interpretation \\[1ex] + \large 2nd revision, for Isabelle 2009} \author{Clemens Ballarin} \date{} \maketitle +%\thispagestyle{myheadings} +%\markright{Technical Report TUM-I0723, Technische Universit\"at M\"unchen, 2007} \thispagestyle{myheadings} -\markright{Technical Report TUM-I0723, Technische Universit\"at M\"unchen, 2007} +\markright{This tutorial is currently not consistent.} \begin{abstract} Locales are Isabelle's mechanism to deal with parametric theories. @@ -40,6 +43,10 @@ This tutorial is intended for locale novices; familiarity with Isabelle and Isar is presumed. + The 2nd 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{abstract} \parindent 0pt\parskip 0.5ex