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 \<open>Use of Locales in Theories and Proofs
wenzelm@61419
     6
  \label{sec:interpretation}\<close>
ballarin@27063
     7
wenzelm@61419
     8
text \<open>
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 \<le>"} is a total order over @{typ int}.  We start
ballarin@32983
    23
  with the interpretation that @{term "op \<le>"} 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
\<close>
ballarin@27063
    27
ballarin@27063
    28
wenzelm@61419
    29
subsection \<open>First Version: Replacement of Parameters Only
wenzelm@61419
    30
  \label{sec:po-first}\<close>
ballarin@27063
    31
wenzelm@61419
    32
text \<open>
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 \<le> :: int \<Rightarrow> int \<Rightarrow>
ballarin@32981
    36
  bool"} and the locale instance is interpreted in the current
wenzelm@61419
    37
  theory.\<close>
ballarin@27063
    38
ballarin@32982
    39
  interpretation %visible int: partial_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
wenzelm@61419
    40
txt \<open>\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
\<close>
ballarin@27063
    54
    by unfold_locales auto
ballarin@27063
    55
wenzelm@61419
    56
text \<open>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.\<close>
ballarin@27063
    65
ballarin@27063
    66
wenzelm@61419
    67
subsection \<open>Second Version: Replacement of Definitions\<close>
ballarin@27063
    68
wenzelm@61419
    69
text \<open>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 \<le>"}.
ballarin@32981
    74
  Qualified name and expanded form may be used almost
ballarin@32981
    75
  interchangeably.%
ballarin@61701
    76
\footnote{Since @{term "op \<le>"} is polymorphic, for @{text "partial_order.less op \<le>"} 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
\<close>
ballarin@27063
    89
end