# HG changeset patch # User ballarin # Date 1237410898 -3600 # Node ID cc5a55d7a5be58cb64cda1fc62bc4215870795cd # Parent c12484a273678a840bf5c09447c87a034cfa8dc2 Updated chapters 1-5 to locale reimplementation. diff -r c12484a27367 -r cc5a55d7a5be doc-src/Locales/Locales/Examples.thy --- a/doc-src/Locales/Locales/Examples.thy Wed Mar 18 19:11:26 2009 +0100 +++ b/doc-src/Locales/Locales/Examples.thy Wed Mar 18 22:14:58 2009 +0100 @@ -1,5 +1,3 @@ -(* $Id$ *) - theory Examples imports Main GCD begin @@ -137,9 +135,9 @@ target for a block may be given with the \isakeyword{context} command. - In the block below, notions of infimum and supremum together with - theorems are introduced for partial orders. - *} + This style of working is illustrated in the block below, where + notions of infimum and supremum for partial orders are introduced, + together with theorems. *} context partial_order begin @@ -238,15 +236,19 @@ end -text {* In fact, many more theorems need to be shown for a usable - theory of partial orders. The - above two serve as illustrative examples. *} +text {* The definitions of @{text is_inf} and @{text is_sup} look + like ordinary definitions in theories. Despite, what is going on + behind the scenes is more complex. The definition of @{text + is_inf}, say, creates a constant @{const partial_order.is_inf} where + the locale parameters that occur in the definition of @{text is_inf} + are additional arguments. Writing @{text "is_inf x y inf"} is just + a notational convenience for @{text "partial_order.is_inf op \ x y + inf"}. *} -text {* - Two commands are provided to inspect locales: +text {* Two commands are provided to inspect locales: \isakeyword{print\_locales} lists the names of all locales of the - theory; \isakeyword{print\_locale}~$n$ prints the parameters and - assumptions of locale $n$; \isakeyword{print\_locale!}~$n$ + current theory; \isakeyword{print\_locale}~$n$ prints the parameters + and assumptions of locale $n$; \isakeyword{print\_locale!}~$n$ additionally outputs the conclusions. The syntax of the locale commands discussed in this tutorial is @@ -255,11 +257,9 @@ for full documentation. *} -section {* Import *} +section {* Import \label{sec:import} *} text {* -\label{sec:import} - Algebraic structures are commonly defined by adding operations and properties to existing structures. For example, partial orders are extended to lattices and total orders. Lattices are extended to @@ -270,11 +270,11 @@ *} locale lattice = partial_order + - assumes ex_inf: "\inf. partial_order.is_inf le x y inf" - and ex_sup: "\sup. partial_order.is_sup le x y sup" + assumes ex_inf: "\inf. is_inf x y inf" + and ex_sup: "\sup. is_sup x y sup" begin -text {* Note that the assumptions above refer to the predicates for infimum +text {* These assumptions refer to the predicates for infimum and supremum defined in @{text partial_order}. In the current implementation of locales, syntax from definitions of the imported locale is unavailable in the locale declaration, neither are their @@ -537,9 +537,7 @@ by (unfold less_def) blast locale distrib_lattice = lattice + - assumes meet_distr: - "lattice.meet le x (lattice.join le y z) = - lattice.join le (lattice.meet le x y) (lattice.meet le x z)" + assumes meet_distr: "x \ (y \ z) = x \ y \ x \ z" lemma (in distrib_lattice) join_distr: "x \ (y \ z) = (x \ y) \ (x \ z)" (* txt {* Jacobson I, p.\ 462 *} *) @@ -600,11 +598,10 @@ \end{figure} *} -section {* Changing the Locale Hierarchy *} +section {* Changing the Locale Hierarchy + \label{sec:changing-the-hierarchy} *} text {* -\label{sec:changing-the-hierarchy} - Total orders are lattices. Hence, by deriving the lattice axioms for total orders, the hierarchy may be changed and @{text lattice} be placed between @{text partial_order} diff -r c12484a27367 -r cc5a55d7a5be doc-src/Locales/Locales/Examples1.thy --- a/doc-src/Locales/Locales/Examples1.thy Wed Mar 18 19:11:26 2009 +0100 +++ b/doc-src/Locales/Locales/Examples1.thy Wed Mar 18 22:14:58 2009 +0100 @@ -1,5 +1,3 @@ -(* $Id$ *) - theory Examples1 imports Examples begin @@ -14,7 +12,7 @@ The changes of the locale hierarchy from the previous sections are examples of - interpretations. The command \isakeyword{interpretation} $l_1 + interpretations. The command \isakeyword{sublocale} $l_1 \subseteq l_2$ is said to \emph{interpret} locale $l_2$ in the context of $l_1$. It causes all theorems of $l_2$ to be made available in $l_1$. The interpretation is \emph{dynamic}: not only @@ -27,17 +25,17 @@ Theorems added to locales will be propagated to theories. In this section the interpretation in theories is illustrated; interpretation in proofs is analogous. - As an example consider, the type of natural numbers @{typ nat}. The + + As an example, consider the type of natural numbers @{typ nat}. The order relation @{text \} is a total order over @{typ nat}, - divisibility @{text dvd} is a distributive lattice. - - We start with the + divisibility @{text dvd} is a distributive lattice. We start with the interpretation that @{text \} is a partial order. The facilities of the interpretation command are explored in three versions. *} -subsection {* First Version: Replacement of Parameters Only \label{sec:po-first} *} +subsection {* First Version: Replacement of Parameters Only + \label{sec:po-first} *} text {* In the most basic form, interpretation just replaces the locale @@ -45,7 +43,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 @@ -53,10 +51,10 @@ which is used to qualify names from the locale in the global context. - The command creates the goal @{subgoals [display]} which can be shown - easily:% + The command creates the goal% \footnote{Note that @{text op} binds tighter than functions application: parentheses around @{text "op \"} are not necessary.} + @{subgoals [display]} which can be shown easily: *} by unfold_locales auto @@ -64,12 +62,14 @@ interpreted for natural numbers, for example @{thm [source] nat.trans}: @{thm [display, indent=2] nat.trans} - In order to avoid unwanted hiding of theorems, interpretation - accepts a qualifier, @{text nat} in the example, which is applied to - all names processed by the - interpretation. If present the qualifier is mandatory --- that is, - the above theorem cannot be referred to simply as @{text 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. *} subsection {* Second Version: Replacement of Definitions *} @@ -78,9 +78,9 @@ @{thm [source] nat.less_le_trans}: @{thm [display, indent=2] nat.less_le_trans} Here, @{term "partial_order.less (op \ :: nat \ nat \ bool)"} - represents the strict order, although @{text "<"} is defined on - @{typ nat}. Interpretation enables to map concepts - introduced in locales through definitions to the corresponding + represents the strict order, although @{text "<"} is the natural + strict order for @{typ nat}. Interpretation allows to map concepts + introduced through definitions in locales to the corresponding concepts of the theory.% \footnote{This applies not only to \isakeyword{definition} but also to \isakeyword{inductive}, \isakeyword{fun} and \isakeyword{function}.} diff -r c12484a27367 -r cc5a55d7a5be doc-src/Locales/Locales/Examples2.thy --- a/doc-src/Locales/Locales/Examples2.thy Wed Mar 18 19:11:26 2009 +0100 +++ b/doc-src/Locales/Locales/Examples2.thy Wed Mar 18 22:14:58 2009 +0100 @@ -1,19 +1,17 @@ -(* $Id$ *) - theory Examples2 imports Examples begin text {* This is achieved by unfolding suitable equations during interpretation. These equations are given after the keyword - \isakeyword{where} and require proofs. The revised command, - replacing @{text "\"} by @{text "<"}, is: *} + \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]} - The proof that @{text \} is a partial order is a above. *} + The proof that @{text \} is a partial order is as above. *} show "partial_order (op \ :: nat \ nat \ bool)" by unfold_locales auto txt {* The second goal is shown by unfolding the diff -r c12484a27367 -r cc5a55d7a5be doc-src/Locales/Locales/Examples3.thy --- a/doc-src/Locales/Locales/Examples3.thy Wed Mar 18 19:11:26 2009 +0100 +++ b/doc-src/Locales/Locales/Examples3.thy Wed Mar 18 22:14:58 2009 +0100 @@ -1,5 +1,3 @@ -(* $Id$ *) - theory Examples3 imports Examples begin @@ -16,27 +14,29 @@ \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" - where "partial_order.less (op \) (x::nat) y = (x < y)" +interpretation %visible nat!: partial_order "op \ :: nat \ nat \ bool" + where "partial_order.less op \ (x::nat) y = (x < y)" proof - show "partial_order (op \ :: nat \ nat \ bool)" by unfold_locales auto then interpret nat: partial_order "op \ :: [nat, nat] \ bool" . - show "partial_order.less (op \) (x::nat) y = (x < y)" + show "partial_order.less op \ (x::nat) y = (x < y)" unfolding nat.less_def by auto qed text {* The inner interpretation does not require an elaborate new proof, it is immediate from the preceeding fact and - proved with ``.''. - This interpretation enriches the local proof context by + proved with ``.''. Strict qualifiers are normally not necessary for + interpretations inside proofs, since these have only limited scope. + + The above interpretation enriches the local proof context by the very theorems also obtained in the interpretation from Section~\ref{sec:po-first}, and @{text nat.less_def} may directly be used to unfold the definition. Theorems from the local interpretation disappear after leaving the proof context --- that is, after the closing \isakeyword{qed} --- and are then replaced by those with the desired substitutions of the strict - order. *} + order. *} subsection {* Further Interpretations *} @@ -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 @@ -142,10 +142,11 @@ done qed -text {* Note that there is no symbol for strict divisibility. Instead, - interpretation substitutes @{term "x dvd y \ x \ y"}. *} +text {* Note that in Isabelle/HOL 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: @@ -198,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]} *} @@ -232,8 +233,8 @@ text {* The full syntax of the interpretation commands is shown in Table~\ref{tab:commands}. The grammar refers to - \textit{expr}, which stands for a \emph{locale} expression. Locale - expressions are discussed in Section~\ref{sec:expressions}. + \textit{expression}, which stands for a \emph{locale} expression. + Locale expressions are discussed in the following section. *} diff -r c12484a27367 -r cc5a55d7a5be doc-src/Locales/Locales/document/Examples.tex --- a/doc-src/Locales/Locales/document/Examples.tex Wed Mar 18 19:11:26 2009 +0100 +++ b/doc-src/Locales/Locales/document/Examples.tex Wed Mar 18 22:14:58 2009 +0100 @@ -3,8 +3,6 @@ \def\isabellecontext{Examples}% % \isadelimtheory -\isanewline -\isanewline % \endisadelimtheory % @@ -197,8 +195,9 @@ target for a block may be given with the \isakeyword{context} command. - In the block below, notions of infimum and supremum together with - theorems are introduced for partial orders.% + This style of working is illustrated in the block below, where + notions of infimum and supremum for partial orders are introduced, + together with theorems.% \end{isamarkuptext}% \isamarkuptrue% \ \ \isacommand{context}\isamarkupfalse% @@ -465,17 +464,20 @@ \ \ \isacommand{end}\isamarkupfalse% % \begin{isamarkuptext}% -In fact, many more theorems need to be shown for a usable - theory of partial orders. The - above two serve as illustrative examples.% +The definitions of \isa{is{\isacharunderscore}inf} and \isa{is{\isacharunderscore}sup} look + like ordinary definitions in theories. Despite, what is going on + behind the scenes is more complex. The definition of \isa{is{\isacharunderscore}inf}, say, creates a constant \isa{partial{\isacharunderscore}order{\isachardot}is{\isacharunderscore}inf} where + the locale parameters that occur in the definition of \isa{is{\isacharunderscore}inf} + are additional arguments. Writing \isa{is{\isacharunderscore}inf\ x\ y\ inf} is just + a notational convenience for \isa{partial{\isacharunderscore}order{\isachardot}is{\isacharunderscore}inf\ op\ {\isasymsqsubseteq}\ x\ y\ inf}.% \end{isamarkuptext}% \isamarkuptrue% % \begin{isamarkuptext}% Two commands are provided to inspect locales: \isakeyword{print\_locales} lists the names of all locales of the - theory; \isakeyword{print\_locale}~$n$ prints the parameters and - assumptions of locale $n$; \isakeyword{print\_locale!}~$n$ + current theory; \isakeyword{print\_locale}~$n$ prints the parameters + and assumptions of locale $n$; \isakeyword{print\_locale!}~$n$ additionally outputs the conclusions. The syntax of the locale commands discussed in this tutorial is @@ -485,14 +487,12 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsection{Import% +\isamarkupsection{Import \label{sec:import}% } \isamarkuptrue% % \begin{isamarkuptext}% -\label{sec:import} - - Algebraic structures are commonly defined by adding operations and +Algebraic structures are commonly defined by adding operations and properties to existing structures. For example, partial orders are extended to lattices and total orders. Lattices are extended to distributive lattices. @@ -503,11 +503,11 @@ \isamarkuptrue% \ \ \isacommand{locale}\isamarkupfalse% \ lattice\ {\isacharequal}\ partial{\isacharunderscore}order\ {\isacharplus}\isanewline -\ \ \ \ \isakeyword{assumes}\ ex{\isacharunderscore}inf{\isacharcolon}\ {\isachardoublequoteopen}{\isasymexists}inf{\isachardot}\ partial{\isacharunderscore}order{\isachardot}is{\isacharunderscore}inf\ le\ x\ y\ inf{\isachardoublequoteclose}\isanewline -\ \ \ \ \ \ \isakeyword{and}\ ex{\isacharunderscore}sup{\isacharcolon}\ {\isachardoublequoteopen}{\isasymexists}sup{\isachardot}\ partial{\isacharunderscore}order{\isachardot}is{\isacharunderscore}sup\ le\ x\ y\ sup{\isachardoublequoteclose}\isanewline +\ \ \ \ \isakeyword{assumes}\ ex{\isacharunderscore}inf{\isacharcolon}\ {\isachardoublequoteopen}{\isasymexists}inf{\isachardot}\ is{\isacharunderscore}inf\ x\ y\ inf{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ \isakeyword{and}\ ex{\isacharunderscore}sup{\isacharcolon}\ {\isachardoublequoteopen}{\isasymexists}sup{\isachardot}\ is{\isacharunderscore}sup\ x\ y\ sup{\isachardoublequoteclose}\isanewline \ \ \isakeyword{begin}% \begin{isamarkuptext}% -Note that the assumptions above refer to the predicates for infimum +These assumptions refer to the predicates for infimum and supremum defined in \isa{partial{\isacharunderscore}order}. In the current implementation of locales, syntax from definitions of the imported locale is unavailable in the locale declaration, neither are their @@ -1110,9 +1110,7 @@ \isanewline \ \ \isacommand{locale}\isamarkupfalse% \ distrib{\isacharunderscore}lattice\ {\isacharequal}\ lattice\ {\isacharplus}\isanewline -\ \ \ \ \isakeyword{assumes}\ meet{\isacharunderscore}distr{\isacharcolon}\isanewline -\ \ \ \ \ \ {\isachardoublequoteopen}lattice{\isachardot}meet\ le\ x\ {\isacharparenleft}lattice{\isachardot}join\ le\ y\ z{\isacharparenright}\ {\isacharequal}\isanewline -\ \ \ \ \ \ lattice{\isachardot}join\ le\ {\isacharparenleft}lattice{\isachardot}meet\ le\ x\ y{\isacharparenright}\ {\isacharparenleft}lattice{\isachardot}meet\ le\ x\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \ \ \isakeyword{assumes}\ meet{\isacharunderscore}distr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymsqinter}\ {\isacharparenleft}y\ {\isasymsqunion}\ z{\isacharparenright}\ {\isacharequal}\ x\ {\isasymsqinter}\ y\ {\isasymsqunion}\ x\ {\isasymsqinter}\ z{\isachardoublequoteclose}\isanewline \isanewline \ \ \isacommand{lemma}\isamarkupfalse% \ {\isacharparenleft}\isakeyword{in}\ distrib{\isacharunderscore}lattice{\isacharparenright}\ join{\isacharunderscore}distr{\isacharcolon}\isanewline @@ -1206,14 +1204,13 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsection{Changing the Locale Hierarchy% +\isamarkupsection{Changing the Locale Hierarchy + \label{sec:changing-the-hierarchy}% } \isamarkuptrue% % \begin{isamarkuptext}% -\label{sec:changing-the-hierarchy} - - Total orders are lattices. Hence, by deriving the lattice +Total orders are lattices. Hence, by deriving the lattice axioms for total orders, the hierarchy may be changed and \isa{lattice} be placed between \isa{partial{\isacharunderscore}order} and \isa{total{\isacharunderscore}order}, as shown in Figure~\ref{fig:lattices}(b). diff -r c12484a27367 -r cc5a55d7a5be doc-src/Locales/Locales/document/Examples1.tex --- a/doc-src/Locales/Locales/document/Examples1.tex Wed Mar 18 19:11:26 2009 +0100 +++ b/doc-src/Locales/Locales/document/Examples1.tex Wed Mar 18 22:14:58 2009 +0100 @@ -3,8 +3,6 @@ \def\isabellecontext{Examples{\isadigit{1}}}% % \isadelimtheory -\isanewline -\isanewline % \endisadelimtheory % @@ -33,7 +31,7 @@ The changes of the locale hierarchy from the previous sections are examples of - interpretations. The command \isakeyword{interpretation} $l_1 + interpretations. The command \isakeyword{sublocale} $l_1 \subseteq l_2$ is said to \emph{interpret} locale $l_2$ in the context of $l_1$. It causes all theorems of $l_2$ to be made available in $l_1$. The interpretation is \emph{dynamic}: not only @@ -46,17 +44,17 @@ Theorems added to locales will be propagated to theories. In this section the interpretation in theories is illustrated; interpretation in proofs is analogous. - As an example consider, the type of natural numbers \isa{nat}. The + + As an example, consider the type of natural numbers \isa{nat}. The order relation \isa{{\isasymle}} is a total order over \isa{nat}, - divisibility \isa{dvd} is a distributive lattice. - - We start with the + divisibility \isa{dvd} is a distributive lattice. We start with the interpretation that \isa{{\isasymle}} is a partial order. The facilities of the interpretation command are explored in three versions.% \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsection{First Version: Replacement of Parameters Only \label{sec:po-first}% +\isamarkupsubsection{First Version: Replacement of Parameters Only + \label{sec:po-first}% } \isamarkuptrue% % @@ -74,7 +72,7 @@ % \isatagvisible \isacommand{interpretation}\isamarkupfalse% -\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}% +\ nat{\isacharbang}{\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 @@ -83,12 +81,12 @@ which is used to qualify names from the locale in the global context. - The command creates the goal \begin{isabelle}% + The command creates the goal% +\footnote{Note that \isa{op} binds tighter than functions + application: parentheses around \isa{op\ {\isasymle}} are not necessary.} + \begin{isabelle}% \ {\isadigit{1}}{\isachardot}\ partial{\isacharunderscore}order\ op\ {\isasymle}% -\end{isabelle} which can be shown - easily:% -\footnote{Note that \isa{op} binds tighter than functions - application: parentheses around \isa{op\ {\isasymle}} are not necessary.}% +\end{isabelle} which can be shown easily:% \end{isamarkuptxt}% \isamarkuptrue% \ \ \ \ \isacommand{by}\isamarkupfalse% @@ -106,11 +104,14 @@ \ \ {\isasymlbrakk}{\isacharquery}x\ {\isasymle}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymle}\ {\isacharquery}z% \end{isabelle} - In order to avoid unwanted hiding of theorems, interpretation - accepts a qualifier, \isa{nat} in the example, which is applied to - all names processed by the - interpretation. If present the qualifier is mandatory --- that is, - the above theorem cannot be referred to simply as \isa{trans}.% + 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.% \end{isamarkuptext}% \isamarkuptrue% % @@ -125,9 +126,9 @@ \isaindent{\ \ }{\isasymLongrightarrow}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharquery}x\ {\isacharquery}z% \end{isabelle} Here, \isa{partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}} - represents the strict order, although \isa{{\isacharless}} is defined on - \isa{nat}. Interpretation enables to map concepts - introduced in locales through definitions to the corresponding + represents the strict order, although \isa{{\isacharless}} is the natural + strict order for \isa{nat}. Interpretation allows to map concepts + introduced through definitions in locales to the corresponding concepts of the theory.% \footnote{This applies not only to \isakeyword{definition} but also to \isakeyword{inductive}, \isakeyword{fun} and \isakeyword{function}.}% diff -r c12484a27367 -r cc5a55d7a5be doc-src/Locales/Locales/document/Examples2.tex --- a/doc-src/Locales/Locales/document/Examples2.tex Wed Mar 18 19:11:26 2009 +0100 +++ b/doc-src/Locales/Locales/document/Examples2.tex Wed Mar 18 22:14:58 2009 +0100 @@ -3,8 +3,6 @@ \def\isabellecontext{Examples{\isadigit{2}}}% % \isadelimtheory -\isanewline -\isanewline % \endisadelimtheory % @@ -23,8 +21,8 @@ \begin{isamarkuptext}% This is achieved by unfolding suitable equations during interpretation. These equations are given after the keyword - \isakeyword{where} and require proofs. The revised command, - replacing \isa{{\isasymsqsubset}} by \isa{{\isacharless}}, is:% + \isakeyword{where} and require proofs. The revised command + that replaces \isa{{\isasymsqsubset}} by \isa{{\isacharless}}, is:% \end{isamarkuptext}% \isamarkuptrue% % @@ -34,7 +32,7 @@ % \isatagvisible \isacommand{interpretation}\isamarkupfalse% -\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}nat{\isacharcomma}\ nat{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline +\ nat{\isacharbang}{\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}% @@ -43,7 +41,7 @@ \ {\isadigit{1}}{\isachardot}\ partial{\isacharunderscore}order\ op\ {\isasymle}\isanewline \ {\isadigit{2}}{\isachardot}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ x\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}% \end{isabelle} - The proof that \isa{{\isasymle}} is a partial order is a above.% + The proof that \isa{{\isasymle}} is a partial order is as above.% \end{isamarkuptxt}% \isamarkuptrue% \ \ \isacommand{show}\isamarkupfalse% diff -r c12484a27367 -r cc5a55d7a5be doc-src/Locales/Locales/document/Examples3.tex --- a/doc-src/Locales/Locales/document/Examples3.tex Wed Mar 18 19:11:26 2009 +0100 +++ b/doc-src/Locales/Locales/document/Examples3.tex Wed Mar 18 22:14:58 2009 +0100 @@ -3,8 +3,6 @@ \def\isabellecontext{Examples{\isadigit{3}}}% % \isadelimtheory -\isanewline -\isanewline % \endisadelimtheory % @@ -43,8 +41,8 @@ % \isatagvisible \isacommand{interpretation}\isamarkupfalse% -\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline -\ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ {\isacharparenleft}op\ {\isasymle}{\isacharparenright}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ nat{\isacharbang}{\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 \ \ \isacommand{show}\isamarkupfalse% @@ -56,7 +54,7 @@ \ 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 +\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline \ \ \ \ \isacommand{unfolding}\isamarkupfalse% \ nat{\isachardot}less{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% \ auto\isanewline @@ -72,8 +70,10 @@ \begin{isamarkuptext}% The inner interpretation does not require an elaborate new proof, it is immediate from the preceeding fact and - proved with ``.''. - This interpretation enriches the local proof context by + proved with ``.''. Strict qualifiers are normally not necessary for + interpretations inside proofs, since these have only limited scope. + + The above interpretation enriches the local proof context by the very theorems also obtained in the interpretation from Section~\ref{sec:po-first}, and \isa{nat{\isachardot}less{\isacharunderscore}def} may directly be used to unfold the definition. Theorems from the local @@ -104,7 +104,7 @@ % \isatagvisible \isacommand{interpretation}\isamarkupfalse% -\ nat{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline +\ nat{\isacharbang}{\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{\isacharcolon}\ total{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline +\ nat{\isacharbang}{\isacharcolon}\ total{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline \ \ \isacommand{by}\isamarkupfalse% \ unfold{\isacharunderscore}locales\ arith% \endisatagvisible @@ -280,12 +280,12 @@ \endisadelimproof % \begin{isamarkuptext}% -Note that there is no symbol for strict divisibility. Instead, - interpretation substitutes \isa{x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y}.% +Note that in Isabelle/HOL there is no symbol for strict + divisibility. Instead, interpretation substitutes \isa{x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y}.% \end{isamarkuptext}% \isamarkuptrue% \isacommand{interpretation}\isamarkupfalse% -\ nat{\isacharunderscore}dvd{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline +\ nat{\isacharunderscore}dvd{\isacharbang}{\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{\isacharcolon}\isanewline +\ nat{\isacharunderscore}dvd{\isacharbang}{\isacharcolon}\isanewline \ \ distrib{\isacharunderscore}lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline \ \ \isacommand{apply}\isamarkupfalse% \ unfold{\isacharunderscore}locales% @@ -439,8 +439,8 @@ \begin{isamarkuptext}% The full syntax of the interpretation commands is shown in Table~\ref{tab:commands}. The grammar refers to - \textit{expr}, which stands for a \emph{locale} expression. Locale - expressions are discussed in Section~\ref{sec:expressions}.% + \textit{expression}, which stands for a \emph{locale} expression. + Locale expressions are discussed in the following section.% \end{isamarkuptext}% \isamarkuptrue% %