# HG changeset patch # User ballarin # Date 1255638128 -7200 # Node ID 40810d98f4c916238a19ac70644c136a3d349364 # Parent 0114e04a0d64f6902d8b6279accde28b22a35f3a Changed part of the examples to int. diff -r 0114e04a0d64 -r 40810d98f4c9 doc-src/Locales/Locales/Examples1.thy --- a/doc-src/Locales/Locales/Examples1.thy Thu Oct 15 22:07:18 2009 +0200 +++ b/doc-src/Locales/Locales/Examples1.thy Thu Oct 15 22:22:08 2009 +0200 @@ -18,8 +18,8 @@ interpretations in proofs, in Section~\ref{sec:local-interpretation}. - As an example, consider the type of natural numbers @{typ nat}. The - relation @{term "op \"} is a total order over @{typ nat}, + As an example, consider the type of integers @{typ int}. The + relation @{term "op \"} is a total order over @{typ int}, divisibility @{text "op dvd"} forms a distributive lattice. We start with the interpretation that @{term "op \"} is a partial order. The facilities of the interpretation command are explored gradually in three versions. @@ -32,15 +32,15 @@ text {* The command \isakeyword{interpretation} is for the interpretation of locale in theories. In the following example, the parameter of locale - @{text partial_order} is replaced by @{term "op \ :: nat \ nat \ + @{text partial_order} is replaced by @{term "op \ :: int \ int \ bool"} and the locale instance is interpreted in the current theory. *} - interpretation %visible nat: partial_order "op \ :: nat \ nat \ bool" + interpretation %visible int: partial_order "op \ :: int \ int \ bool" txt {* \normalsize The argument of the command is a simple \emph{locale expression} consisting of the name of the interpreted locale, which is - preceded by the qualifier @{text "nat:"} and succeeded by a + preceded by the qualifier @{text "int:"} and succeeded by a white-space-separated list of terms, which provide a full instantiation of the locale parameters. The parameters are referred to by order of declaration, which is also the order in which @@ -56,9 +56,9 @@ text {* The effect of the command is that instances of all conclusions of the locale are available in the theory, where names are prefixed by the qualifier. For example, transitivity for @{typ - nat} is named @{thm [source] nat.trans} and is the following + int} is named @{thm [source] int.trans} and is the following theorem: - @{thm [display, indent=2] nat.trans} + @{thm [display, indent=2] int.trans} It is not possible to reference this theorem simply as @{text trans}, which prevents unwanted hiding of existing theorems of the theory by an interpretation. *} @@ -67,20 +67,20 @@ subsection {* Second Version: Replacement of Definitions *} text {* Not only does the above interpretation qualify theorem names. - The prefix @{text nat} is applied to all names introduced in locale + The prefix @{text int} is applied to all names introduced in locale conclusions including names introduced in definitions. The - qualified name @{text nat.less} refers to - the interpretation of the definition, which is @{term nat.less}. + qualified name @{text int.less} refers to + the interpretation of the definition, which is @{term int.less}. Qualified name and expanded form may be used almost interchangeably.% -\footnote{Since @{term "op \"} is polymorphic, for @{term nat.less} a - more general type will be inferred than for @{text nat.less} which - is over type @{typ nat}.} +\footnote{Since @{term "op \"} is polymorphic, for @{term int.less} a + more general type will be inferred than for @{text int.less} which + is over type @{typ int}.} The latter is preferred on output, as for example in the theorem - @{thm [source] nat.less_le_trans}: @{thm [display, indent=2] - nat.less_le_trans} + @{thm [source] int.less_le_trans}: @{thm [display, indent=2] + int.less_le_trans} Both notations for the strict order are not satisfactory. The - constant @{term "op <"} is the strict order for @{typ nat}. + constant @{term "op <"} is the strict order for @{typ int}. In order to allow for the desired replacement, interpretation accepts \emph{equations} in addition to the parameter instantiation. These follow the locale expression and are indicated with the diff -r 0114e04a0d64 -r 40810d98f4c9 doc-src/Locales/Locales/Examples2.thy --- a/doc-src/Locales/Locales/Examples2.thy Thu Oct 15 22:07:18 2009 +0200 +++ b/doc-src/Locales/Locales/Examples2.thy Thu Oct 15 22:22:08 2009 +0200 @@ -2,16 +2,16 @@ imports Examples begin text {* \vspace{-5ex} *} - interpretation %visible nat: partial_order "op \ :: [nat, nat] \ bool" - where "partial_order.less op \ (x::nat) y = (x < y)" + interpretation %visible int: partial_order "op \ :: [int, int] \ bool" + where "partial_order.less op \ (x::int) y = (x < y)" proof - txt {* \normalsize The goals are @{subgoals [display]} The proof that @{text \} is a partial order is as above. *} - show "partial_order (op \ :: nat \ nat \ bool)" + show "partial_order (op \ :: int \ int \ bool)" by unfold_locales auto txt {* \normalsize The second goal is shown by unfolding the definition of @{term "partial_order.less"}. *} - show "partial_order.less op \ (x::nat) y = (x < y)" + show "partial_order.less op \ (x::int) y = (x < y)" unfolding partial_order.less_def [OF `partial_order op \`] by auto qed diff -r 0114e04a0d64 -r 40810d98f4c9 doc-src/Locales/Locales/Examples3.thy --- a/doc-src/Locales/Locales/Examples3.thy Thu Oct 15 22:07:18 2009 +0200 +++ b/doc-src/Locales/Locales/Examples3.thy Thu Oct 15 22:22:08 2009 +0200 @@ -8,7 +8,7 @@ \label{sec:local-interpretation} *} text {* In the above example, the fact that @{term "op \"} is a partial - order for the natural numbers was used in the second goal to + order for the integers was used in the second goal to discharge the premise in the definition of @{text "op \"}. In general, proofs of the equations not only may involve definitions fromthe interpreted locale but arbitrarily complex arguments in the @@ -18,21 +18,21 @@ The command for local interpretations is \isakeyword{interpret}. We repeat the example from the previous section to illustrate this. *} - interpretation %visible nat: partial_order "op \ :: nat \ nat \ bool" - where "partial_order.less op \ (x::nat) y = (x < y)" + interpretation %visible int: partial_order "op \ :: int \ int \ bool" + where "partial_order.less op \ (x::int) y = (x < y)" proof - - show "partial_order (op \ :: nat \ nat \ bool)" + show "partial_order (op \ :: int \ int \ bool)" by unfold_locales auto - 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 + then interpret int: partial_order "op \ :: [int, int] \ bool" . + show "partial_order.less op \ (x::int) y = (x < y)" + unfolding int.less_def by auto qed text {* The inner interpretation is immediate from the preceding fact and proved by assumption (Isar short hand ``.''). It enriches the local proof context by the theorems also obtained in the interpretation from Section~\ref{sec:po-first}, - and @{text nat.less_def} may directly be used to unfold the + and @{text int.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 a \isakeyword{next} or \isakeyword{qed} statement. *} @@ -42,23 +42,23 @@ text {* Further interpretations are necessary for the other locales. In @{text lattice} the operations @{text \} and - @{text \} are substituted by @{term "min :: nat \ nat \ nat"} and - @{term "max :: nat \ nat \ nat"}. The entire proof for the + @{text \} are substituted by @{term "min :: int \ int \ int"} and + @{term "max :: int \ int \ int"}. The entire proof for the interpretation is reproduced to give an example of a more elaborate interpretation proof. *} - 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" + interpretation %visible int: lattice "op \ :: int \ int \ bool" + where "lattice.meet op \ (x::int) y = min x y" + and "lattice.join op \ (x::int) y = max x y" proof - - show "lattice (op \ :: nat \ nat \ bool)" + show "lattice (op \ :: int \ int \ bool)" txt {* \normalsize We have already shown that this is a partial order, *} apply unfold_locales txt {* \normalsize hence only the lattice axioms remain to be shown: @{subgoals [display]} After unfolding @{text is_inf} and @{text is_sup}, *} - apply (unfold nat.is_inf_def nat.is_sup_def) + apply (unfold int.is_inf_def int.is_sup_def) txt {* \normalsize the goals become @{subgoals [display]} This can be solved by Presburger arithmetic, which is contained in @{text arith}. *} @@ -66,40 +66,40 @@ txt {* \normalsize 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" . - 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" - by (bestsimp simp: nat.join_def nat.is_sup_def) + then interpret int: lattice "op \ :: int \ int \ bool" . + show "lattice.meet op \ (x::int) y = min x y" + by (bestsimp simp: int.meet_def int.is_inf_def) + show "lattice.join op \ (x::int) y = max x y" + by (bestsimp simp: int.join_def int.is_sup_def) qed text {* Next follows that @{text "op \"} is a total order, again for - the natural numbers. *} + the integers. *} - interpretation %visible nat: total_order "op \ :: nat \ nat \ bool" + interpretation %visible int: total_order "op \ :: int \ int \ bool" by unfold_locales arith text {* Theorems that are available in the theory at this point are shown in - Table~\ref{tab:nat-lattice}. Two points are worth noting: + Table~\ref{tab:int-lattice}. Two points are worth noting: \begin{table} \hrule \vspace{2ex} \begin{center} \begin{tabular}{l} - @{thm [source] nat.less_def} from locale @{text partial_order}: \\ - \quad @{thm nat.less_def} \\ - @{thm [source] nat.meet_left} from locale @{text lattice}: \\ - \quad @{thm nat.meet_left} \\ - @{thm [source] nat.join_distr} from locale @{text distrib_lattice}: \\ - \quad @{thm nat.join_distr} \\ - @{thm [source] nat.less_total} from locale @{text total_order}: \\ - \quad @{thm nat.less_total} + @{thm [source] int.less_def} from locale @{text partial_order}: \\ + \quad @{thm int.less_def} \\ + @{thm [source] int.meet_left} from locale @{text lattice}: \\ + \quad @{thm int.meet_left} \\ + @{thm [source] int.join_distr} from locale @{text distrib_lattice}: \\ + \quad @{thm int.join_distr} \\ + @{thm [source] int.less_total} from locale @{text total_order}: \\ + \quad @{thm int.less_total} \end{tabular} \end{center} \hrule -\caption{Interpreted theorems for @{text \} on the natural numbers.} -\label{tab:nat-lattice} +\caption{Interpreted theorems for @{text \} on the integers.} +\label{tab:int-lattice} \end{table} \begin{itemize} @@ -112,7 +112,7 @@ up in the hierarchy, regardless whether imported or proved via the \isakeyword{sublocale} command. \item - Theorem @{thm [source] nat.less_total} makes use of @{term "op <"} + Theorem @{thm [source] int.less_total} makes use of @{term "op <"} although an equation for the replacement of @{text "op \"} was only given in the interpretation of @{text partial_order}. These equations are pushed downwards the hierarchy for related @@ -229,7 +229,7 @@ For example, \isakeyword{print\_interps} @{term partial_order} outputs the following: \begin{alltt} - nat! : partial_order "op \(\le\)" + int! : partial_order "op \(\le\)" nat_dvd! : partial_order "op dvd" \end{alltt} The interpretation qualifiers on the left are decorated with an diff -r 0114e04a0d64 -r 40810d98f4c9 doc-src/Locales/Locales/document/Examples1.tex --- a/doc-src/Locales/Locales/document/Examples1.tex Thu Oct 15 22:07:18 2009 +0200 +++ b/doc-src/Locales/Locales/document/Examples1.tex Thu Oct 15 22:22:08 2009 +0200 @@ -36,8 +36,8 @@ interpretations in proofs, in Section~\ref{sec:local-interpretation}. - As an example, consider the type of natural numbers \isa{nat}. The - relation \isa{op\ {\isasymle}} is a total order over \isa{nat}, + As an example, consider the type of integers \isa{int}. The + relation \isa{op\ {\isasymle}} is a total order over \isa{int}, divisibility \isa{op\ dvd} forms a distributive lattice. We start with the interpretation that \isa{op\ {\isasymle}} is a partial order. The facilities of the interpretation command are explored gradually in three versions.% @@ -63,12 +63,12 @@ % \isatagvisible \isacommand{interpretation}\isamarkupfalse% -\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}% +\ int{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}% \begin{isamarkuptxt}% \normalsize The argument of the command is a simple \emph{locale expression} consisting of the name of the interpreted locale, which is - preceded by the qualifier \isa{nat{\isacharcolon}} and succeeded by a + preceded by the qualifier \isa{int{\isacharcolon}} and succeeded by a white-space-separated list of terms, which provide a full instantiation of the locale parameters. The parameters are referred to by order of declaration, which is also the order in which @@ -94,7 +94,7 @@ \begin{isamarkuptext}% The effect of the command is that instances of all conclusions of the locale are available in the theory, where names - are prefixed by the qualifier. For example, transitivity for \isa{nat} is named \isa{nat{\isachardot}trans} and is the following + are prefixed by the qualifier. For example, transitivity for \isa{int} is named \isa{int{\isachardot}trans} and is the following theorem: \begin{isabelle}% \ \ {\isasymlbrakk}{\isacharquery}x\ {\isasymle}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymle}\ {\isacharquery}z% @@ -110,22 +110,22 @@ % \begin{isamarkuptext}% Not only does the above interpretation qualify theorem names. - The prefix \isa{nat} is applied to all names introduced in locale + The prefix \isa{int} is applied to all names introduced in locale conclusions including names introduced in definitions. The - qualified name \isa{nat{\isachardot}less} refers to + qualified name \isa{int{\isachardot}less} refers to the interpretation of the definition, which is \isa{partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}}. Qualified name and expanded form may be used almost interchangeably.% \footnote{Since \isa{op\ {\isasymle}} is polymorphic, for \isa{partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}} a - more general type will be inferred than for \isa{nat{\isachardot}less} which - is over type \isa{nat}.} + more general type will be inferred than for \isa{int{\isachardot}less} which + is over type \isa{int}.} The latter is preferred on output, as for example in the theorem - \isa{nat{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: \begin{isabelle}% + \isa{int{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: \begin{isabelle}% \ \ {\isasymlbrakk}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharquery}x\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}z{\isasymrbrakk}\isanewline \isaindent{\ \ }{\isasymLongrightarrow}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharquery}x\ {\isacharquery}z% \end{isabelle} Both notations for the strict order are not satisfactory. The - constant \isa{op\ {\isacharless}} is the strict order for \isa{nat}. + constant \isa{op\ {\isacharless}} is the strict order for \isa{int}. In order to allow for the desired replacement, interpretation accepts \emph{equations} in addition to the parameter instantiation. These follow the locale expression and are indicated with the diff -r 0114e04a0d64 -r 40810d98f4c9 doc-src/Locales/Locales/document/Examples2.tex --- a/doc-src/Locales/Locales/document/Examples2.tex Thu Oct 15 22:07:18 2009 +0200 +++ b/doc-src/Locales/Locales/document/Examples2.tex Thu Oct 15 22:22:08 2009 +0200 @@ -29,8 +29,8 @@ % \isatagvisible \isacommand{interpretation}\isamarkupfalse% -\ 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 +\ int{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}int{\isacharcomma}\ int{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline +\ \ \ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline \ \ \isacommand{proof}\isamarkupfalse% \ {\isacharminus}% \begin{isamarkuptxt}% @@ -42,7 +42,7 @@ \end{isamarkuptxt}% \isamarkuptrue% \ \ \ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}partial{\isacharunderscore}order\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ {\isachardoublequoteopen}partial{\isacharunderscore}order\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}\isanewline \ \ \ \ \ \ \isacommand{by}\isamarkupfalse% \ unfold{\isacharunderscore}locales\ auto% \begin{isamarkuptxt}% @@ -51,7 +51,7 @@ \end{isamarkuptxt}% \isamarkuptrue% \ \ \ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\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}int{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse% \ partial{\isacharunderscore}order{\isachardot}less{\isacharunderscore}def\ {\isacharbrackleft}OF\ {\isacharbackquoteopen}partial{\isacharunderscore}order\ op\ {\isasymle}{\isacharbackquoteclose}{\isacharbrackright}\isanewline \ \ \ \ \ \ \isacommand{by}\isamarkupfalse% diff -r 0114e04a0d64 -r 40810d98f4c9 doc-src/Locales/Locales/document/Examples3.tex --- a/doc-src/Locales/Locales/document/Examples3.tex Thu Oct 15 22:07:18 2009 +0200 +++ b/doc-src/Locales/Locales/document/Examples3.tex Thu Oct 15 22:22:08 2009 +0200 @@ -45,7 +45,7 @@ % \begin{isamarkuptext}% In the above example, the fact that \isa{op\ {\isasymle}} is a partial - order for the natural numbers was used in the second goal to + order for the integers was used in the second goal to discharge the premise in the definition of \isa{op\ {\isasymsqsubset}}. In general, proofs of the equations not only may involve definitions fromthe interpreted locale but arbitrarily complex arguments in the @@ -63,22 +63,22 @@ % \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\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ int{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline +\ \ \ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline \ \ \isacommand{proof}\isamarkupfalse% \ {\isacharminus}\isanewline \ \ \ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}partial{\isacharunderscore}order\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ {\isachardoublequoteopen}partial{\isacharunderscore}order\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}\isanewline \ \ \ \ \ \ \isacommand{by}\isamarkupfalse% \ unfold{\isacharunderscore}locales\ auto\isanewline \ \ \ \ \isacommand{then}\isamarkupfalse% \ \isacommand{interpret}\isamarkupfalse% -\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}nat{\isacharcomma}\ nat{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse% +\ int{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}int{\isacharcomma}\ int{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse% \isanewline \ \ \ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\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}int{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse% -\ nat{\isachardot}less{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% +\ int{\isachardot}less{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% \ auto\isanewline \ \ \isacommand{qed}\isamarkupfalse% % @@ -94,7 +94,7 @@ and proved by assumption (Isar short hand ``.''). It enriches the local proof context by the 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 + and \isa{int{\isachardot}less{\isacharunderscore}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 a \isakeyword{next} or \isakeyword{qed} statement.% @@ -121,13 +121,13 @@ % \isatagvisible \isacommand{interpretation}\isamarkupfalse% -\ 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 +\ int{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline +\ \ \ \ \isakeyword{where}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ max\ x\ y{\isachardoublequoteclose}\isanewline \ \ \isacommand{proof}\isamarkupfalse% \ {\isacharminus}\isanewline \ \ \ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}lattice\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}% +\ {\isachardoublequoteopen}lattice\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}% \begin{isamarkuptxt}% \normalsize We have already shown that this is a partial order,% @@ -145,7 +145,7 @@ \end{isamarkuptxt}% \isamarkuptrue% \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse% -\ {\isacharparenleft}unfold\ nat{\isachardot}is{\isacharunderscore}inf{\isacharunderscore}def\ nat{\isachardot}is{\isacharunderscore}sup{\isacharunderscore}def{\isacharparenright}% +\ {\isacharparenleft}unfold\ int{\isachardot}is{\isacharunderscore}inf{\isacharunderscore}def\ int{\isachardot}is{\isacharunderscore}sup{\isacharunderscore}def{\isacharparenright}% \begin{isamarkuptxt}% \normalsize the goals become \begin{isabelle}% \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ {\isasymexists}inf{\isasymle}x{\isachardot}\ inf\ {\isasymle}\ y\ {\isasymand}\ {\isacharparenleft}{\isasymforall}z{\isachardot}\ z\ {\isasymle}\ x\ {\isasymand}\ z\ {\isasymle}\ y\ {\isasymlongrightarrow}\ z\ {\isasymle}\ inf{\isacharparenright}\isanewline @@ -165,16 +165,16 @@ \isamarkuptrue% \ \ \ \ \isacommand{then}\isamarkupfalse% \ \isacommand{interpret}\isamarkupfalse% -\ nat{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse% +\ int{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\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 +\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline \ \ \ \ \ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}bestsimp\ simp{\isacharcolon}\ nat{\isachardot}meet{\isacharunderscore}def\ nat{\isachardot}is{\isacharunderscore}inf{\isacharunderscore}def{\isacharparenright}\isanewline +\ {\isacharparenleft}bestsimp\ simp{\isacharcolon}\ int{\isachardot}meet{\isacharunderscore}def\ int{\isachardot}is{\isacharunderscore}inf{\isacharunderscore}def{\isacharparenright}\isanewline \ \ \ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ max\ x\ y{\isachardoublequoteclose}\isanewline +\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ max\ x\ y{\isachardoublequoteclose}\isanewline \ \ \ \ \ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}bestsimp\ simp{\isacharcolon}\ nat{\isachardot}join{\isacharunderscore}def\ nat{\isachardot}is{\isacharunderscore}sup{\isacharunderscore}def{\isacharparenright}\isanewline +\ {\isacharparenleft}bestsimp\ simp{\isacharcolon}\ int{\isachardot}join{\isacharunderscore}def\ int{\isachardot}is{\isacharunderscore}sup{\isacharunderscore}def{\isacharparenright}\isanewline \ \ \isacommand{qed}\isamarkupfalse% % \endisatagvisible @@ -186,7 +186,7 @@ % \begin{isamarkuptext}% Next follows that \isa{op\ {\isasymle}} is a total order, again for - the natural numbers.% + the integers.% \end{isamarkuptext}% \isamarkuptrue% % @@ -196,7 +196,7 @@ % \isatagvisible \isacommand{interpretation}\isamarkupfalse% -\ nat{\isacharcolon}\ total{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline +\ int{\isacharcolon}\ total{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline \ \ \ \ \isacommand{by}\isamarkupfalse% \ unfold{\isacharunderscore}locales\ arith% \endisatagvisible @@ -208,26 +208,26 @@ % \begin{isamarkuptext}% Theorems that are available in the theory at this point are shown in - Table~\ref{tab:nat-lattice}. Two points are worth noting: + Table~\ref{tab:int-lattice}. Two points are worth noting: \begin{table} \hrule \vspace{2ex} \begin{center} \begin{tabular}{l} - \isa{nat{\isachardot}less{\isacharunderscore}def} from locale \isa{partial{\isacharunderscore}order}: \\ + \isa{int{\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}: \\ + \isa{int{\isachardot}meet{\isacharunderscore}left} from locale \isa{lattice}: \\ \quad \isa{min\ {\isacharquery}x\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}x} \\ - \isa{nat{\isachardot}join{\isacharunderscore}distr} from locale \isa{distrib{\isacharunderscore}lattice}: \\ + \isa{int{\isachardot}join{\isacharunderscore}distr} from locale \isa{distrib{\isacharunderscore}lattice}: \\ \quad \isa{max\ {\isacharquery}x\ {\isacharparenleft}min\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ min\ {\isacharparenleft}max\ {\isacharquery}x\ {\isacharquery}y{\isacharparenright}\ {\isacharparenleft}max\ {\isacharquery}x\ {\isacharquery}z{\isacharparenright}} \\ - \isa{nat{\isachardot}less{\isacharunderscore}total} from locale \isa{total{\isacharunderscore}order}: \\ + \isa{int{\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} \end{tabular} \end{center} \hrule -\caption{Interpreted theorems for \isa{{\isasymle}} on the natural numbers.} -\label{tab:nat-lattice} +\caption{Interpreted theorems for \isa{{\isasymle}} on the integers.} +\label{tab:int-lattice} \end{table} \begin{itemize} @@ -240,7 +240,7 @@ up in the hierarchy, regardless whether imported or proved via the \isakeyword{sublocale} command. \item - Theorem \isa{nat{\isachardot}less{\isacharunderscore}total} makes use of \isa{op\ {\isacharless}} + Theorem \isa{int{\isachardot}less{\isacharunderscore}total} makes use of \isa{op\ {\isacharless}} although an equation for the replacement of \isa{op\ {\isasymsqsubset}} was only given in the interpretation of \isa{partial{\isacharunderscore}order}. These equations are pushed downwards the hierarchy for related @@ -461,7 +461,7 @@ For example, \isakeyword{print\_interps} \isa{partial{\isacharunderscore}order} outputs the following: \begin{alltt} - nat! : partial_order "op \(\le\)" + int! : partial_order "op \(\le\)" nat_dvd! : partial_order "op dvd" \end{alltt} The interpretation qualifiers on the left are decorated with an