src/Doc/Locales/Examples1.thy
 author haftmann Mon Feb 06 20:56:34 2017 +0100 (2017-02-06) changeset 64990 c6a7de505796 parent 61701 e89cfc004f18 child 67399 eab6ce8368fa permissions -rw-r--r--
more explicit errors in pathological cases
 ballarin@27063  1 theory Examples1  ballarin@27063  2 imports Examples  ballarin@27063  3 begin  wenzelm@57607  4 wenzelm@61419  5 section \Use of Locales in Theories and Proofs  wenzelm@61419  6  \label{sec:interpretation}\  ballarin@27063  7 wenzelm@61419  8 text \  ballarin@32983  9  Locales can be interpreted in the contexts of theories and  ballarin@27063  10  structured proofs. These interpretations are dynamic, too.  ballarin@32981  11  Conclusions of locales will be propagated to the current theory or  ballarin@32981  12  the current proof context.%  ballarin@32981  13 \footnote{Strictly speaking, only interpretation in theories is  ballarin@32981  14  dynamic since it is not possible to change locales or the locale  ballarin@32981  15  hierarchy from within a proof.}  ballarin@32981  16  The focus of this section is on  ballarin@32981  17  interpretation in theories, but we will also encounter  ballarin@32981  18  interpretations in proofs, in  ballarin@32981  19  Section~\ref{sec:local-interpretation}.  ballarin@30580  20 ballarin@32982  21  As an example, consider the type of integers @{typ int}. The  ballarin@32983  22  relation @{term "op \"} is a total order over @{typ int}. We start  ballarin@32983  23  with the interpretation that @{term "op \"} is a partial order. The  ballarin@32983  24  facilities of the interpretation command are explored gradually in  ballarin@32983  25  three versions.  wenzelm@61419  26 \  ballarin@27063  27 ballarin@27063  28 wenzelm@61419  29 subsection \First Version: Replacement of Parameters Only  wenzelm@61419  30  \label{sec:po-first}\  ballarin@27063  31 wenzelm@61419  32 text \  ballarin@32981  33  The command \isakeyword{interpretation} is for the interpretation of  ballarin@32981  34  locale in theories. In the following example, the parameter of locale  ballarin@32982  35  @{text partial_order} is replaced by @{term "op \ :: int \ int \  ballarin@32981  36  bool"} and the locale instance is interpreted in the current  wenzelm@61419  37  theory.\  ballarin@27063  38 ballarin@32982  39  interpretation %visible int: partial_order "op \ :: int \ int \ bool"  wenzelm@61419  40 txt \\normalsize  ballarin@32981  41  The argument of the command is a simple \emph{locale expression}  ballarin@32981  42  consisting of the name of the interpreted locale, which is  ballarin@32982  43  preceded by the qualifier @{text "int:"} and succeeded by a  ballarin@32981  44  white-space-separated list of terms, which provide a full  ballarin@32981  45  instantiation of the locale parameters. The parameters are referred  ballarin@32981  46  to by order of declaration, which is also the order in which  ballarin@32983  47  \isakeyword{print\_locale} outputs them. The locale has only a  ballarin@32983  48  single parameter, hence the list of instantiation terms is a  ballarin@32983  49  singleton.  ballarin@32981  50 ballarin@32981  51  The command creates the goal  ballarin@30580  52  @{subgoals [display]} which can be shown easily:  wenzelm@61419  53 \  ballarin@27063  54  by unfold_locales auto  ballarin@27063  55 wenzelm@61419  56 text \The effect of the command is that instances of all  ballarin@32981  57  conclusions of the locale are available in the theory, where names  ballarin@32981  58  are prefixed by the qualifier. For example, transitivity for @{typ  ballarin@32982  59  int} is named @{thm [source] int.trans} and is the following  ballarin@32981  60  theorem:  ballarin@32982  61  @{thm [display, indent=2] int.trans}  ballarin@32981  62  It is not possible to reference this theorem simply as @{text  ballarin@32983  63  trans}. This prevents unwanted hiding of existing theorems of the  wenzelm@61419  64  theory by an interpretation.\  ballarin@27063  65 ballarin@27063  66 wenzelm@61419  67 subsection \Second Version: Replacement of Definitions\  ballarin@27063  68 wenzelm@61419  69 text \Not only does the above interpretation qualify theorem names.  ballarin@32982  70  The prefix @{text int} is applied to all names introduced in locale  ballarin@32981  71  conclusions including names introduced in definitions. The  ballarin@32983  72  qualified name @{text int.less} is short for  ballarin@61701  73  the interpretation of the definition, which is @{text "partial_order.less op \"}.  ballarin@32981  74  Qualified name and expanded form may be used almost  ballarin@32981  75  interchangeably.%  ballarin@61701  76 \footnote{Since @{term "op \"} is polymorphic, for @{text "partial_order.less op \"} a  ballarin@32982  77  more general type will be inferred than for @{text int.less} which  ballarin@32982  78  is over type @{typ int}.}  ballarin@61701  79  The former is preferred on output, as for example in the theorem  ballarin@32982  80  @{thm [source] int.less_le_trans}: @{thm [display, indent=2]  ballarin@32982  81  int.less_le_trans}  ballarin@32981  82  Both notations for the strict order are not satisfactory. The  ballarin@32982  83  constant @{term "op <"} is the strict order for @{typ int}.  ballarin@32981  84  In order to allow for the desired replacement, interpretation  ballarin@32981  85  accepts \emph{equations} in addition to the parameter instantiation.  ballarin@32981  86  These follow the locale expression and are indicated with the  ballarin@61566  87  keyword \isakeyword{rewrites}. This is the revised interpretation:  wenzelm@61419  88 \  ballarin@27063  89 end