src/Doc/Locales/Examples3.thy
 author haftmann Mon Feb 06 20:56:34 2017 +0100 (2017-02-06) changeset 64990 c6a7de505796 parent 63724 e7df93d4d9b8 child 67398 5eb932e604a2 permissions -rw-r--r--
more explicit errors in pathological cases
 ballarin@27063  1 theory Examples3  ballarin@32983  2 imports Examples  ballarin@27063  3 begin  wenzelm@57607  4 wenzelm@61419  5 subsection \Third Version: Local Interpretation  wenzelm@61419  6  \label{sec:local-interpretation}\  ballarin@27063  7 wenzelm@61419  8 text \In the above example, the fact that @{term "op \"} is a partial  ballarin@32982  9  order for the integers was used in the second goal to  ballarin@32981  10  discharge the premise in the definition of @{text "op \"}. In  ballarin@32981  11  general, proofs of the equations not only may involve definitions  ballarin@32983  12  from the interpreted locale but arbitrarily complex arguments in the  wenzelm@46855  13  context of the locale. Therefore it would be convenient to have the  wenzelm@46855  14  interpreted locale conclusions temporarily available in the proof.  ballarin@32981  15  This can be achieved by a locale interpretation in the proof body.  ballarin@32981  16  The command for local interpretations is \isakeyword{interpret}. We  wenzelm@61419  17  repeat the example from the previous section to illustrate this.\  ballarin@27063  18 ballarin@32982  19  interpretation %visible int: partial_order "op \ :: int \ int \ bool"  ballarin@61566  20  rewrites "int.less x y = (x < y)"  ballarin@32981  21  proof -  ballarin@32982  22  show "partial_order (op \ :: int \ int \ bool)"  ballarin@32981  23  by unfold_locales auto  ballarin@32982  24  then interpret int: partial_order "op \ :: [int, int] \ bool" .  ballarin@43543  25  show "int.less x y = (x < y)"  ballarin@32982  26  unfolding int.less_def by auto  ballarin@32981  27  qed  ballarin@27063  28 wenzelm@61419  29 text \The inner interpretation is immediate from the preceding fact  ballarin@32981  30  and proved by assumption (Isar short hand .''). It enriches the  ballarin@32981  31  local proof context by the theorems  ballarin@30826  32  also obtained in the interpretation from Section~\ref{sec:po-first},  ballarin@32982  33  and @{text int.less_def} may directly be used to unfold the  ballarin@30826  34  definition. Theorems from the local interpretation disappear after  ballarin@32983  35  leaving the proof context --- that is, after the succeeding  wenzelm@61419  36  \isakeyword{next} or \isakeyword{qed} statement.\  ballarin@27063  37 ballarin@27063  38 wenzelm@61419  39 subsection \Further Interpretations\  ballarin@27063  40 wenzelm@61419  41 text \Further interpretations are necessary for  ballarin@32983  42  the other locales. In @{text lattice} the operations~@{text \}  ballarin@32983  43  and~@{text \} are substituted by @{term "min :: int \ int \ int"}  ballarin@32983  44  and @{term "max :: int \ int \ int"}. The entire proof for the  ballarin@32981  45  interpretation is reproduced to give an example of a more  ballarin@32983  46  elaborate interpretation proof. Note that the equations are named  wenzelm@61419  47  so they can be used in a later example.\  ballarin@27063  48 ballarin@32982  49  interpretation %visible int: lattice "op \ :: int \ int \ bool"  ballarin@61566  50  rewrites int_min_eq: "int.meet x y = min x y"  ballarin@43543  51  and int_max_eq: "int.join x y = max x y"  ballarin@32981  52  proof -  ballarin@32982  53  show "lattice (op \ :: int \ int \ bool)"  wenzelm@61419  54  txt \\normalsize We have already shown that this is a partial  wenzelm@61419  55  order,\  ballarin@32981  56  apply unfold_locales  wenzelm@61419  57  txt \\normalsize hence only the lattice axioms remain to be  wenzelm@43708  58  shown.  ballarin@32983  59  @{subgoals [display]}  wenzelm@61419  60  By @{text is_inf} and @{text is_sup},\  ballarin@32982  61  apply (unfold int.is_inf_def int.is_sup_def)  wenzelm@61419  62  txt \\normalsize the goals are transformed to these  wenzelm@43708  63  statements:  wenzelm@43708  64  @{subgoals [display]}  wenzelm@43708  65  This is Presburger arithmetic, which can be solved by the  wenzelm@61419  66  method @{text arith}.\  ballarin@32981  67  by arith+  wenzelm@61419  68  txt \\normalsize In order to show the equations, we put ourselves  ballarin@32981  69  in a situation where the lattice theorems can be used in a  wenzelm@61419  70  convenient way.\  ballarin@32982  71  then interpret int: lattice "op \ :: int \ int \ bool" .  ballarin@43543  72  show "int.meet x y = min x y"  ballarin@32982  73  by (bestsimp simp: int.meet_def int.is_inf_def)  ballarin@43543  74  show "int.join x y = max x y"  ballarin@32982  75  by (bestsimp simp: int.join_def int.is_sup_def)  ballarin@32981  76  qed  ballarin@27063  77 wenzelm@61419  78 text \Next follows that @{text "op \"} is a total order, again for  wenzelm@61419  79  the integers.\  ballarin@27063  80 ballarin@32982  81  interpretation %visible int: total_order "op \ :: int \ int \ bool"  ballarin@32981  82  by unfold_locales arith  ballarin@27063  83 wenzelm@61419  84 text \Theorems that are available in the theory at this point are shown in  ballarin@32982  85  Table~\ref{tab:int-lattice}. Two points are worth noting:  ballarin@27063  86 ballarin@27063  87 \begin{table}  ballarin@27063  88 \hrule  ballarin@27063  89 \vspace{2ex}  ballarin@27063  90 \begin{center}  ballarin@27063  91 \begin{tabular}{l}  ballarin@32982  92  @{thm [source] int.less_def} from locale @{text partial_order}: \\  ballarin@32982  93  \quad @{thm int.less_def} \\  ballarin@63724  94  @{thm [source] int.meet_left} from locale @{text lattice}: \\  ballarin@63724  95  \quad @{thm int.meet_left} \\  ballarin@32982  96  @{thm [source] int.join_distr} from locale @{text distrib_lattice}: \\  ballarin@32982  97  \quad @{thm int.join_distr} \\  ballarin@32982  98  @{thm [source] int.less_total} from locale @{text total_order}: \\  ballarin@32982  99  \quad @{thm int.less_total}  ballarin@27063  100 \end{tabular}  ballarin@27063  101 \end{center}  ballarin@27063  102 \hrule  ballarin@32983  103 \caption{Interpreted theorems for~@{text \} on the integers.}  ballarin@32982  104 \label{tab:int-lattice}  ballarin@27063  105 \end{table}  ballarin@32804  106 ballarin@32804  107 \begin{itemize}  ballarin@32804  108 \item  ballarin@32981  109  Locale @{text distrib_lattice} was also interpreted. Since the  ballarin@32983  110  locale hierarchy reflects that total orders are distributive  ballarin@32981  111  lattices, the interpretation of the latter was inserted  ballarin@32981  112  automatically with the interpretation of the former. In general,  ballarin@32983  113  interpretation traverses the locale hierarchy upwards and interprets  ballarin@32983  114  all encountered locales, regardless whether imported or proved via  ballarin@32983  115  the \isakeyword{sublocale} command. Existing interpretations are  ballarin@32983  116  skipped avoiding duplicate work.  ballarin@32804  117 \item  ballarin@32983  118  The predicate @{term "op <"} appears in theorem @{thm [source]  ballarin@32983  119  int.less_total}  ballarin@32981  120  although an equation for the replacement of @{text "op \"} was only  ballarin@32983  121  given in the interpretation of @{text partial_order}. The  ballarin@32983  122  interpretation equations are pushed downwards the hierarchy for  ballarin@32983  123  related interpretations --- that is, for interpretations that share  ballarin@32983  124  the instances of parameters they have in common.  ballarin@32804  125 \end{itemize}  wenzelm@61419  126 \  ballarin@27063  127 wenzelm@61419  128 text \The interpretations for a locale $n$ within the current  ballarin@32981  129  theory may be inspected with \isakeyword{print\_interps}~$n$. This  ballarin@32981  130  prints the list of instances of $n$, for which interpretations exist.  ballarin@32981  131  For example, \isakeyword{print\_interps} @{term partial_order}  ballarin@32981  132  outputs the following:  ballarin@32983  133 \begin{small}  ballarin@32981  134 \begin{alltt}  ballarin@61731  135  int : partial_order "op $$\le$$"  ballarin@32981  136 \end{alltt}  ballarin@32983  137 \end{small}  ballarin@32983  138  Of course, there is only one interpretation.  ballarin@61731  139  The interpretation qualifier on the left is mandatory. Qualifiers  ballarin@61731  140  can either be \emph{mandatory} or \emph{optional}. Optional qualifiers  ballarin@61731  141  are designated by ?''. Mandatory qualifiers must occur in  ballarin@61731  142  name references while optional ones need not. Mandatory qualifiers  ballarin@32983  143  prevent accidental hiding of names, while optional qualifiers can be  ballarin@61731  144  more convenient to use. The default is mandatory.  wenzelm@61419  145 \  ballarin@27063  146 ballarin@27063  147 wenzelm@61419  148 section \Locale Expressions \label{sec:expressions}\  ballarin@27063  149 wenzelm@61419  150 text \  ballarin@32983  151  A map~@{term \} between partial orders~@{text \} and~@{text \}  ballarin@27063  152  is called order preserving if @{text "x \ y"} implies @{text "\ x \  ballarin@27063  153  \ y"}. This situation is more complex than those encountered so  ballarin@27063  154  far: it involves two partial orders, and it is desirable to use the  ballarin@27063  155  existing locale for both.  ballarin@27063  156 ballarin@32981  157  A locale for order preserving maps requires three parameters: @{text  ballarin@32983  158  le}~(\isakeyword{infixl}~@{text \}) and @{text  ballarin@32983  159  le'}~(\isakeyword{infixl}~@{text \}) for the orders and~@{text \}  ballarin@32983  160  for the map.  ballarin@32981  161 ballarin@32981  162  In order to reuse the existing locale for partial orders, which has  ballarin@32983  163  the single parameter~@{text le}, it must be imported twice, once  ballarin@32983  164  mapping its parameter to~@{text le} from the new locale and once  ballarin@32983  165  to~@{text le'}. This can be achieved with a compound locale  ballarin@32981  166  expression.  ballarin@32981  167 ballarin@32983  168  In general, a locale expression is a sequence of \emph{locale instances}  ballarin@32983  169  separated by~$\textbf{+}$'' and followed by a \isakeyword{for}  ballarin@32981  170  clause.  ballarin@32983  171  An instance has the following format:  ballarin@32981  172 \begin{quote}  ballarin@32981  173  \textit{qualifier} \textbf{:} \textit{locale-name}  ballarin@32981  174  \textit{parameter-instantiation}  ballarin@32981  175 \end{quote}  ballarin@32981  176  We have already seen locale instances as arguments to  ballarin@32981  177  \isakeyword{interpretation} in Section~\ref{sec:interpretation}.  ballarin@32983  178  As before, the qualifier serves to disambiguate names from  ballarin@61731  179  different instances of the same locale, and unless designated with a  ballarin@61731  180  ?'' it must occur in name references.  ballarin@30750  181 ballarin@32983  182  Since the parameters~@{text le} and~@{text le'} are to be partial  ballarin@32981  183  orders, our locale for order preserving maps will import the these  ballarin@32981  184  instances:  ballarin@32983  185 \begin{small}  ballarin@32981  186 \begin{alltt}  ballarin@32981  187  le: partial_order le  ballarin@32981  188  le': partial_order le'  ballarin@32981  189 \end{alltt}  ballarin@32983  190 \end{small}  ballarin@32983  191  For matter of convenience we choose to name parameter names and  ballarin@32983  192  qualifiers alike. This is an arbitrary decision. Technically, qualifiers  ballarin@32981  193  and parameters are unrelated.  ballarin@32981  194 ballarin@32981  195  Having determined the instances, let us turn to the \isakeyword{for}  ballarin@32981  196  clause. It serves to declare locale parameters in the same way as  ballarin@32981  197  the context element \isakeyword{fixes} does. Context elements can  ballarin@32981  198  only occur after the import section, and therefore the parameters  ballarin@32983  199  referred to in the instances must be declared in the \isakeyword{for}  ballarin@32983  200  clause. The \isakeyword{for} clause is also where the syntax of these  ballarin@32981  201  parameters is declared.  ballarin@32981  202 ballarin@32983  203  Two context elements for the map parameter~@{text \} and the  ballarin@32983  204  assumptions that it is order preserving complete the locale  wenzelm@61419  205  declaration.\  ballarin@27063  206 ballarin@27063  207  locale order_preserving =  ballarin@30750  208  le: partial_order le + le': partial_order le'  ballarin@30750  209  for le (infixl "\" 50) and le' (infixl "\" 50) +  ballarin@32981  210  fixes \  ballarin@27063  211  assumes hom_le: "x \ y \ \ x \ \ y"  ballarin@27063  212 wenzelm@61419  213 text (in order_preserving) \Here are examples of theorems that are  ballarin@32981  214  available in the locale:  ballarin@27063  215 ballarin@32983  216  \hspace*{1em}@{thm [source] hom_le}: @{thm hom_le}  ballarin@27063  217 ballarin@32983  218  \hspace*{1em}@{thm [source] le.less_le_trans}: @{thm le.less_le_trans}  ballarin@27063  219 ballarin@32983  220  \hspace*{1em}@{thm [source] le'.less_le_trans}:  ballarin@32983  221  @{thm [display, indent=4] le'.less_le_trans}  ballarin@61701  222  While there is infix syntax for the strict operation associated with  ballarin@32981  223  @{term "op \"}, there is none for the strict version of @{term  ballarin@61701  224  "op \"}. The syntax @{text "\"} for @{text less} is only  ballarin@32981  225  available for the original instance it was declared for. We may  ballarin@61701  226  introduce infix syntax for @{text le'.less} with the following declaration:\  ballarin@27063  227 ballarin@61701  228  notation (in order_preserving) le'.less (infixl "\" 50)  ballarin@27063  229 wenzelm@61419  230 text (in order_preserving) \Now the theorem is displayed nicely as  ballarin@30826  231  @{thm [source] le'.less_le_trans}:  wenzelm@61419  232  @{thm [display, indent=2] le'.less_le_trans}\  ballarin@27063  233 wenzelm@61419  234 text \There are short notations for locale expressions. These are  wenzelm@61419  235  discussed in the following.\  ballarin@32981  236 ballarin@32983  237 wenzelm@61419  238 subsection \Default Instantiations\  ballarin@32981  239 wenzelm@61419  240 text \  ballarin@32983  241  It is possible to omit parameter instantiations. The  ballarin@32983  242  instantiation then defaults to the name of  ballarin@32983  243  the parameter itself. For example, the locale expression @{text  ballarin@32981  244  partial_order} is short for @{text "partial_order le"}, since the  ballarin@32983  245  locale's single parameter is~@{text le}. We took advantage of this  ballarin@32983  246  in the \isakeyword{sublocale} declarations of  wenzelm@61419  247  Section~\ref{sec:changing-the-hierarchy}.\  ballarin@32981  248 ballarin@32981  249 wenzelm@61419  250 subsection \Implicit Parameters \label{sec:implicit-parameters}\  ballarin@32983  251 wenzelm@61419  252 text \In a locale expression that occurs within a locale  ballarin@32981  253  declaration, omitted parameters additionally extend the (possibly  ballarin@32981  254  empty) \isakeyword{for} clause.  ballarin@27063  255 ballarin@32983  256  The \isakeyword{for} clause is a general construct of Isabelle/Isar  ballarin@32983  257  to mark names occurring in the preceding declaration as arbitrary  ballarin@32983  258  but fixed''. This is necessary for example, if the name is already  ballarin@32983  259  bound in a surrounding context. In a locale expression, names  ballarin@32983  260  occurring in parameter instantiations should be bound by a  ballarin@32983  261  \isakeyword{for} clause whenever these names are not introduced  ballarin@32983  262  elsewhere in the context --- for example, on the left hand side of a  ballarin@32983  263  \isakeyword{sublocale} declaration.  ballarin@27063  264 ballarin@32981  265  There is an exception to this rule in locale declarations, where the  ballarin@32983  266  \isakeyword{for} clause serves to declare locale parameters. Here,  ballarin@32981  267  locale parameters for which no parameter instantiation is given are  ballarin@32981  268  implicitly added, with their mixfix syntax, at the beginning of the  ballarin@32981  269  \isakeyword{for} clause. For example, in a locale declaration, the  ballarin@32981  270  expression @{text partial_order} is short for  ballarin@32983  271 \begin{small}  ballarin@32981  272 \begin{alltt}  ballarin@32981  273  partial_order le \isakeyword{for} le (\isakeyword{infixl} "$$\sqsubseteq$$" 50)\textrm{.}  ballarin@32981  274 \end{alltt}  ballarin@32983  275 \end{small}  ballarin@32983  276  This short hand was used in the locale declarations throughout  ballarin@32981  277  Section~\ref{sec:import}.  wenzelm@61419  278 \  ballarin@32981  279 wenzelm@61419  280 text\  ballarin@32983  281  The following locale declarations provide more examples. A  ballarin@32983  282  map~@{text \} is a lattice homomorphism if it preserves meet and  wenzelm@61419  283  join.\  ballarin@30750  284 ballarin@30750  285  locale lattice_hom =  ballarin@30750  286  le: lattice + le': lattice le' for le' (infixl "\" 50) +  ballarin@27063  287  fixes \  ballarin@30826  288  assumes hom_meet: "\ (x \ y) = le'.meet (\ x) (\ y)"  ballarin@30826  289  and hom_join: "\ (x \ y) = le'.join (\ x) (\ y)"  ballarin@27063  290 wenzelm@61419  291 text \The parameter instantiation in the first instance of @{term  ballarin@32983  292  lattice} is omitted. This causes the parameter~@{text le} to be  ballarin@32983  293  added to the \isakeyword{for} clause, and the locale has  ballarin@32983  294  parameters~@{text le},~@{text le'} and, of course,~@{text \}.  ballarin@27063  295 ballarin@32981  296  Before turning to the second example, we complete the locale by  ballarin@32983  297  providing infix syntax for the meet and join operations of the  ballarin@32981  298  second lattice.  wenzelm@61419  299 \  ballarin@32981  300 wenzelm@46855  301  context lattice_hom  wenzelm@46855  302  begin  ballarin@61701  303  notation le'.meet (infixl "\''" 50)  ballarin@61701  304  notation le'.join (infixl "\''" 50)  ballarin@32981  305  end  ballarin@32981  306 wenzelm@61419  307 text \The next example makes radical use of the short hand  ballarin@32983  308  facilities. A homomorphism is an endomorphism if both orders  wenzelm@61419  309  coincide.\  ballarin@27063  310 ballarin@30750  311  locale lattice_end = lattice_hom _ le  ballarin@30750  312 wenzelm@61419  313 text \The notation~@{text _} enables to omit a parameter in a  ballarin@32983  314  positional instantiation. The omitted parameter,~@{text le} becomes  ballarin@32981  315  the parameter of the declared locale and is, in the following  ballarin@32983  316  position, used to instantiate the second parameter of @{text  ballarin@32981  317  lattice_hom}. The effect is that of identifying the first in second  wenzelm@61419  318  parameter of the homomorphism locale.\  ballarin@27063  319 wenzelm@61419  320 text \The inheritance diagram of the situation we have now is shown  ballarin@27063  321  in Figure~\ref{fig:hom}, where the dashed line depicts an  ballarin@32983  322  interpretation which is introduced below. Parameter instantiations  ballarin@32983  323  are indicated by $\sqsubseteq \mapsto \preceq$ etc. By looking at  ballarin@32983  324  the inheritance diagram it would seem  ballarin@27063  325  that two identical copies of each of the locales @{text  ballarin@32981  326  partial_order} and @{text lattice} are imported by @{text  ballarin@32981  327  lattice_end}. This is not the case! Inheritance paths with  ballarin@32981  328  identical morphisms are automatically detected and  huffman@27503  329  the conclusions of the respective locales appear only once.  ballarin@27063  330 ballarin@27063  331 \begin{figure}  ballarin@27063  332 \hrule \vspace{2ex}  ballarin@27063  333 \begin{center}  ballarin@27063  334 \begin{tikzpicture}  ballarin@27063  335  \node (o) at (0,0) {@{text partial_order}};  ballarin@27063  336  \node (oh) at (1.5,-2) {@{text order_preserving}};  ballarin@27063  337  \node (oh1) at (1.5,-0.7) {$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$};  ballarin@27063  338  \node (oh2) at (0,-1.3) {$\scriptscriptstyle \sqsubseteq \mapsto \preceq$};  ballarin@27063  339  \node (l) at (-1.5,-2) {@{text lattice}};  ballarin@27063  340  \node (lh) at (0,-4) {@{text lattice_hom}};  ballarin@27063  341  \node (lh1) at (0,-2.7) {$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$};  ballarin@27063  342  \node (lh2) at (-1.5,-3.3) {$\scriptscriptstyle \sqsubseteq \mapsto \preceq$};  ballarin@27063  343  \node (le) at (0,-6) {@{text lattice_end}};  ballarin@27063  344  \node (le1) at (0,-4.8)  ballarin@27063  345  [anchor=west]{$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$};  ballarin@27063  346  \node (le2) at (0,-5.2)  ballarin@27063  347  [anchor=west]{$\scriptscriptstyle \preceq \mapsto \sqsubseteq$};  ballarin@27063  348  \draw (o) -- (l);  ballarin@27063  349  \draw[dashed] (oh) -- (lh);  ballarin@27063  350  \draw (lh) -- (le);  ballarin@27063  351  \draw (o) .. controls (oh1.south west) .. (oh);  ballarin@27063  352  \draw (o) .. controls (oh2.north east) .. (oh);  ballarin@27063  353  \draw (l) .. controls (lh1.south west) .. (lh);  ballarin@27063  354  \draw (l) .. controls (lh2.north east) .. (lh);  ballarin@27063  355 \end{tikzpicture}  ballarin@27063  356 \end{center}  ballarin@27063  357 \hrule  ballarin@27063  358 \caption{Hierarchy of Homomorphism Locales.}  ballarin@27063  359 \label{fig:hom}  ballarin@27063  360 \end{figure}  wenzelm@61419  361 \  ballarin@27063  362 wenzelm@61419  363 text \It can be shown easily that a lattice homomorphism is order  ballarin@27063  364  preserving. As the final example of this section, a locale  wenzelm@61419  365  interpretation is used to assert this:\  ballarin@27063  366 wenzelm@46855  367  sublocale lattice_hom \ order_preserving  wenzelm@46855  368  proof unfold_locales  ballarin@27063  369  fix x y  ballarin@27063  370  assume "x \ y"  ballarin@27063  371  then have "y = (x \ y)" by (simp add: le.join_connection)  ballarin@27063  372  then have "\ y = (\ x \' \ y)" by (simp add: hom_join [symmetric])  ballarin@27063  373  then show "\ x \ \ y" by (simp add: le'.join_connection)  ballarin@27063  374  qed  ballarin@27063  375 wenzelm@61419  376 text (in lattice_hom) \  wenzelm@30393  377  Theorems and other declarations --- syntax, in particular --- from  wenzelm@30393  378  the locale @{text order_preserving} are now active in @{text  ballarin@27063  379  lattice_hom}, for example  ballarin@30826  380  @{thm [source] hom_le}:  ballarin@30826  381  @{thm [display, indent=2] hom_le}  ballarin@32983  382  This theorem will be useful in the following section.  wenzelm@61419  383 \  ballarin@27063  384 ballarin@32983  385 wenzelm@61419  386 section \Conditional Interpretation\  ballarin@27063  387 wenzelm@61419  388 text \There are situations where an interpretation is not possible  ballarin@32983  389  in the general case since the desired property is only valid if  ballarin@32983  390  certain conditions are fulfilled. Take, for example, the function  ballarin@32983  391  @{text "\i. n * i"} that scales its argument by a constant factor.  ballarin@32983  392  This function is order preserving (and even a lattice endomorphism)  ballarin@32983  393  with respect to @{term "op \"} provided @{text "n \ 0"}.  ballarin@32983  394 ballarin@32983  395  It is not possible to express this using a global interpretation,  ballarin@32983  396  because it is in general unspecified whether~@{term n} is  ballarin@32983  397  non-negative, but one may make an interpretation in an inner context  ballarin@32983  398  of a proof where full information is available.  ballarin@32983  399  This is not fully satisfactory either, since potentially  ballarin@32983  400  interpretations may be required to make interpretations in many  ballarin@32983  401  contexts. What is  ballarin@32983  402  required is an interpretation that depends on the condition --- and  ballarin@32983  403  this can be done with the \isakeyword{sublocale} command. For this  wenzelm@61419  404  purpose, we introduce a locale for the condition.\  ballarin@32983  405 ballarin@32981  406  locale non_negative =  ballarin@32981  407  fixes n :: int  ballarin@32983  408  assumes non_neg: "0 \ n"  ballarin@32983  409 wenzelm@61419  410 text \It is again convenient to make the interpretation in an  blanchet@63390  411  incremental fashion, first for order preserving maps, then for  wenzelm@61419  412  lattice endomorphisms.\  ballarin@32981  413 ballarin@32983  414  sublocale non_negative \  ballarin@32983  415  order_preserving "op \" "op \" "\i. n * i"  ballarin@32983  416  using non_neg by unfold_locales (rule mult_left_mono)  ballarin@32983  417 wenzelm@61419  418 text \While the proof of the previous interpretation  ballarin@32983  419  is straightforward from monotonicity lemmas for~@{term "op *"}, the  wenzelm@61419  420  second proof follows a useful pattern.\  ballarin@32981  421 ballarin@32983  422  sublocale %visible non_negative \ lattice_end "op \" "\i. n * i"  ballarin@32983  423  proof (unfold_locales, unfold int_min_eq int_max_eq)  wenzelm@61419  424  txt \\normalsize Unfolding the locale predicates \emph{and} the  ballarin@32983  425  interpretation equations immediately yields two subgoals that  ballarin@32983  426  reflect the core conjecture.  ballarin@32983  427  @{subgoals [display]}  ballarin@32983  428  It is now necessary to show, in the context of @{term  ballarin@32983  429  non_negative}, that multiplication by~@{term n} commutes with  wenzelm@61419  430  @{term min} and @{term max}.\  ballarin@32983  431  qed (auto simp: hom_le)  ballarin@32981  432 wenzelm@61419  433 text (in order_preserving) \The lemma @{thm [source] hom_le}  ballarin@32983  434  simplifies a proof that would have otherwise been lengthy and we may  wenzelm@61419  435  consider making it a default rule for the simplifier:\  ballarin@32981  436 ballarin@32983  437  lemmas (in order_preserving) hom_le [simp]  ballarin@32981  438 ballarin@32981  439 wenzelm@61419  440 subsection \Avoiding Infinite Chains of Interpretations  wenzelm@61419  441  \label{sec:infinite-chains}\  ballarin@32983  442 wenzelm@61419  443 text \Similar situations arise frequently in formalisations of  ballarin@32983  444  abstract algebra where it is desirable to express that certain  ballarin@32983  445  constructions preserve certain properties. For example, polynomials  ballarin@32983  446  over rings are rings, or --- an example from the domain where the  ballarin@32983  447  illustrations of this tutorial are taken from --- a partial order  ballarin@32983  448  may be obtained for a function space by point-wise lifting of the  ballarin@32983  449  partial order of the co-domain. This corresponds to the following  wenzelm@61419  450  interpretation:\  ballarin@32983  451 ballarin@32983  452  sublocale %visible partial_order \ f: partial_order "\f g. \x. f x \ g x"  ballarin@32983  453  oops  ballarin@32983  454 wenzelm@61419  455 text \Unfortunately this is a cyclic interpretation that leads to an  ballarin@32983  456  infinite chain, namely  ballarin@32983  457  @{text [display, indent=2] "partial_order \ partial_order (\f g. \x. f x \ g x) \  ballarin@32983  458  partial_order (\f g. \x y. f x y \ g x y) \ \"}  ballarin@32983  459  and the interpretation is rejected.  ballarin@32983  460 ballarin@32983  461  Instead it is necessary to declare a locale that is logically  ballarin@32983  462  equivalent to @{term partial_order} but serves to collect facts  ballarin@32983  463  about functions spaces where the co-domain is a partial order, and  wenzelm@61419  464  to make the interpretation in its context:\  ballarin@32981  465 ballarin@32983  466  locale fun_partial_order = partial_order  ballarin@32983  467 ballarin@32983  468  sublocale fun_partial_order \  ballarin@32983  469  f: partial_order "\f g. \x. f x \ g x"  ballarin@32983  470  by unfold_locales (fast,rule,fast,blast intro: trans)  ballarin@32983  471 wenzelm@61419  472 text \It is quite common in abstract algebra that such a construction  ballarin@32983  473  maps a hierarchy of algebraic structures (or specifications) to a  ballarin@32983  474  related hierarchy. By means of the same lifting, a function space  wenzelm@61419  475  is a lattice if its co-domain is a lattice:\  ballarin@32983  476 ballarin@32983  477  locale fun_lattice = fun_partial_order + lattice  ballarin@32981  478 ballarin@32983  479  sublocale fun_lattice \ f: lattice "\f g. \x. f x \ g x"  wenzelm@46855  480  proof unfold_locales  ballarin@32983  481  fix f g  ballarin@32983  482  have "partial_order.is_inf (\f g. \x. f x \ g x) f g (\x. f x \ g x)"  ballarin@61565  483  apply (rule f.is_infI) apply rule+ apply (drule spec, assumption)+ done  ballarin@32983  484  then show "\inf. partial_order.is_inf (\f g. \x. f x \ g x) f g inf"  ballarin@32983  485  by fast  ballarin@32983  486  next  ballarin@32983  487  fix f g  ballarin@32983  488  have "partial_order.is_sup (\f g. \x. f x \ g x) f g (\x. f x \ g x)"  ballarin@61565  489  apply (rule f.is_supI) apply rule+ apply (drule spec, assumption)+ done  ballarin@32983  490  then show "\sup. partial_order.is_sup (\f g. \x. f x \ g x) f g sup"  ballarin@32983  491  by fast  ballarin@32983  492  qed  ballarin@32983  493 ballarin@27063  494 wenzelm@61419  495 section \Further Reading\  ballarin@27063  496 wenzelm@61419  497 text \More information on locales and their interpretation is  ballarin@27063  498  available. For the locale hierarchy of import and interpretation  wenzelm@58620  499  dependencies see~@{cite Ballarin2006a}; interpretations in theories  wenzelm@58620  500  and proofs are covered in~@{cite Ballarin2006b}. In the latter, I  ballarin@27063  501  show how interpretation in proofs enables to reason about families  ballarin@27063  502  of algebraic structures, which cannot be expressed with locales  ballarin@27063  503  directly.  ballarin@27063  504 wenzelm@58620  505  Haftmann and Wenzel~@{cite HaftmannWenzel2007} overcome a restriction  ballarin@27063  506  of axiomatic type classes through a combination with locale  ballarin@27063  507  interpretation. The result is a Haskell-style class system with a  ballarin@30750  508  facility to generate ML and Haskell code. Classes are sufficient for  ballarin@27063  509  simple specifications with a single type parameter. The locales for  ballarin@27063  510  orders and lattices presented in this tutorial fall into this  ballarin@27063  511  category. Order preserving maps, homomorphisms and vector spaces,  ballarin@27063  512  on the other hand, do not.  ballarin@27063  513 ballarin@32981  514  The locales reimplementation for Isabelle 2009 provides, among other  ballarin@32983  515  improvements, a clean integration with Isabelle/Isar's local theory  ballarin@32983  516  mechanisms, which are described in another paper by Haftmann and  wenzelm@58620  517  Wenzel~@{cite HaftmannWenzel2009}.  ballarin@32981  518 wenzelm@58620  519  The original work of Kamm\"uller on locales~@{cite KammullerEtAl1999}  ballarin@32983  520  may be of interest from a historical perspective. My previous  wenzelm@58620  521  report on locales and locale expressions~@{cite Ballarin2004a}  ballarin@32983  522  describes a simpler form of expressions than available now and is  ballarin@32983  523  outdated. The mathematical background on orders and lattices is  wenzelm@58620  524  taken from Jacobson's textbook on algebra~@{cite \Chapter~8\ Jacobson1985}.  ballarin@32981  525 ballarin@32981  526  The sources of this tutorial, which include all proofs, are  ballarin@32981  527  available with the Isabelle distribution at  wenzelm@63680  528  \<^url>\http://isabelle.in.tum.de\.  wenzelm@61419  529 \  ballarin@27063  530 wenzelm@61419  531 text \  ballarin@27063  532 \begin{table}  ballarin@27063  533 \hrule  ballarin@27063  534 \vspace{2ex}  ballarin@27063  535 \begin{center}  ballarin@27063  536 \begin{tabular}{l>$c<$l}  ballarin@27063  537  \multicolumn{3}{l}{Miscellaneous} \\  ballarin@27063  538 ballarin@27063  539  \textit{attr-name} & ::=  ballarin@27063  540  & \textit{name} $|$ \textit{attribute} $|$  ballarin@29566  541  \textit{name} \textit{attribute} \\  ballarin@29566  542  \textit{qualifier} & ::=  ballarin@61731  543  & \textit{name} [\textbf{?}''] \\[2ex]  ballarin@27063  544 ballarin@27063  545  \multicolumn{3}{l}{Context Elements} \\  ballarin@27063  546 ballarin@27063  547  \textit{fixes} & ::=  ballarin@27063  548  & \textit{name} [ \textbf{::}'' \textit{type} ]  ballarin@27063  549  [ \textbf{(}'' \textbf{structure} \textbf{)}'' $|$  ballarin@27063  550  \textit{mixfix} ] \\  ballarin@27063  551 \begin{comment}  ballarin@27063  552  \textit{constrains} & ::=  ballarin@27063  553  & \textit{name} \textbf{::}'' \textit{type} \\  ballarin@27063  554 \end{comment}  ballarin@27063  555  \textit{assumes} & ::=  ballarin@27063  556  & [ \textit{attr-name} \textbf{:}'' ] \textit{proposition} \\  ballarin@27063  557 \begin{comment}  ballarin@27063  558  \textit{defines} & ::=  ballarin@27063  559  & [ \textit{attr-name} \textbf{:}'' ] \textit{proposition} \\  ballarin@27063  560  \textit{notes} & ::=  ballarin@27063  561  & [ \textit{attr-name} \textbf{=}'' ]  ballarin@27063  562  ( \textit{qualified-name} [ \textit{attribute} ] )$^+$ \\  ballarin@27063  563 \end{comment}  ballarin@27063  564 ballarin@27063  565  \textit{element} & ::=  ballarin@27063  566  & \textbf{fixes} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ \\  ballarin@27063  567 \begin{comment}  ballarin@27063  568  & |  ballarin@27063  569  & \textbf{constrains} \textit{constrains}  ballarin@27063  570  ( \textbf{and} \textit{constrains} )$^*$ \\  ballarin@27063  571 \end{comment}  ballarin@27063  572  & |  ballarin@27063  573  & \textbf{assumes} \textit{assumes} ( \textbf{and} \textit{assumes} )$^*$ \\[2ex]  ballarin@27063  574 %\begin{comment}  ballarin@27063  575 % & |  ballarin@27063  576 % & \textbf{defines} \textit{defines} ( \textbf{and} \textit{defines} )$^*$ \\  ballarin@27063  577 % & |  ballarin@27063  578 % & \textbf{notes} \textit{notes} ( \textbf{and} \textit{notes} )$^*$ \\  ballarin@27063  579 %\end{comment}  ballarin@27063  580 ballarin@27063  581  \multicolumn{3}{l}{Locale Expressions} \\  ballarin@27063  582 ballarin@29566  583  \textit{pos-insts} & ::=  ballarin@29566  584  & ( \textit{term} $|$ \textbf{\_}'' )$^*$ \\  ballarin@29566  585  \textit{named-insts} & ::=  ballarin@29566  586  & \textbf{where} \textit{name} \textbf{=}'' \textit{term}  ballarin@29566  587  ( \textbf{and} \textit{name} \textbf{=}'' \textit{term} )$^*$ \\  ballarin@29566  588  \textit{instance} & ::=  ballarin@30751  589  & [ \textit{qualifier} \textbf{:}'' ]  ballarin@33867  590  \textit{name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\  ballarin@29566  591  \textit{expression} & ::=  ballarin@29566  592  & \textit{instance} ( \textbf{+}'' \textit{instance} )$^*$  ballarin@29566  593  [ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex]  ballarin@27063  594 ballarin@27063  595  \multicolumn{3}{l}{Declaration of Locales} \\  ballarin@27063  596 ballarin@27063  597  \textit{locale} & ::=  ballarin@27063  598  & \textit{element}$^+$ \\  ballarin@29566  599  & | & \textit{expression} [ \textbf{+}'' \textit{element}$^+$ ] \\  ballarin@27063  600  \textit{toplevel} & ::=  ballarin@27063  601  & \textbf{locale} \textit{name} [ \textbf{=}''  ballarin@27063  602  \textit{locale} ] \\[2ex]  ballarin@27063  603 ballarin@27063  604  \multicolumn{3}{l}{Interpretation} \\  ballarin@27063  605 ballarin@27063  606  \textit{equation} & ::= & [ \textit{attr-name} \textbf{:}'' ]  ballarin@27063  607  \textit{prop} \\  ballarin@61566  608  \textit{equations} & ::= & \textbf{rewrites} \textit{equation} ( \textbf{and}  ballarin@29566  609  \textit{equation} )$^*$ \\  ballarin@27063  610  \textit{toplevel} & ::=  ballarin@29566  611  & \textbf{sublocale} \textit{name} ( $<$'' $|$  ballarin@29566  612  $\subseteq$'' ) \textit{expression} \textit{proof} \\  ballarin@27063  613  & |  ballarin@29566  614  & \textbf{interpretation}  ballarin@29566  615  \textit{expression} [ \textit{equations} ] \textit{proof} \\  ballarin@27063  616  & |  ballarin@29566  617  & \textbf{interpret}  ballarin@29566  618  \textit{expression} \textit{proof} \\[2ex]  ballarin@27063  619 ballarin@27063  620  \multicolumn{3}{l}{Diagnostics} \\  ballarin@27063  621 ballarin@27063  622  \textit{toplevel} & ::=  ballarin@32981  623  & \textbf{print\_locales} \\  ballarin@33867  624  & | & \textbf{print\_locale} [ \textbf{!}'' ] \textit{name} \\  ballarin@33867  625  & | & \textbf{print\_interps} \textit{name}  ballarin@27063  626 \end{tabular}  ballarin@27063  627 \end{center}  ballarin@27063  628 \hrule  ballarin@30826  629 \caption{Syntax of Locale Commands.}  ballarin@27063  630 \label{tab:commands}  ballarin@27063  631 \end{table}  wenzelm@61419  632 \  ballarin@27063  633 ballarin@61732  634 text \\textbf{Revision History.} The present fourth revision of the  ballarin@61732  635  tutorial accommodates minor updates to the syntax of the locale commands  ballarin@61732  636  and the handling of notation under morphisms introduced with Isabelle 2016.  ballarin@61732  637  For the third revision of the tutorial, which corresponds to the published  ballarin@61732  638  version, much of the explanatory text was rewritten. Inheritance of  ballarin@61732  639  interpretation equations was made available with Isabelle 2009-1.  ballarin@32983  640  The second revision accommodates changes introduced by the locales  ballarin@32983  641  reimplementation for Isabelle 2009. Most notably locale expressions  ballarin@61732  642  were generalised from renaming to instantiation.\  ballarin@32981  643 wenzelm@61419  644 text \\textbf{Acknowledgements.} Alexander Krauss, Tobias Nipkow,  ballarin@37206  645  Randy Pollack, Andreas Schropp, Christian Sternagel and Makarius Wenzel  ballarin@37206  646  have made  ballarin@32983  647  useful comments on earlier versions of this document. The section  ballarin@32983  648  on conditional interpretation was inspired by a number of e-mail  ballarin@32983  649  enquiries the author received from locale users, and which suggested  ballarin@32983  650  that this use case is important enough to deserve explicit  ballarin@32983  651  explanation. The term \emph{conditional interpretation} is due to  wenzelm@61419  652  Larry Paulson.\  ballarin@27063  653 ballarin@27063  654 end