src/Doc/Locales/Examples1.thy
author wenzelm
Sat, 05 Apr 2014 15:03:40 +0200
changeset 56421 1ffd7eaa778b
parent 48985 5386df44a037
child 57607 5ff0cf3f5f6f
permissions -rw-r--r--
updated to jedit_build-20140405: Code2HTML.jar, CommonControls.jar, Console.jar, kappalayout.jar, Navigator.jar, SideKick.jar, doc with jEdit manuals (ant dist-manuals);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     1
theory Examples1
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     2
imports Examples
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     3
begin
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
     4
text {* \vspace{-5ex} *}
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
     5
section {* Use of Locales in Theories and Proofs
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
     6
  \label{sec:interpretation} *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     7
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
     8
text {*
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
     9
  Locales can be interpreted in the contexts of theories and
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    10
  structured proofs.  These interpretations are dynamic, too.
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    11
  Conclusions of locales will be propagated to the current theory or
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    12
  the current proof context.%
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    13
\footnote{Strictly speaking, only interpretation in theories is
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    14
  dynamic since it is not possible to change locales or the locale
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    15
  hierarchy from within a proof.}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    16
  The focus of this section is on
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    17
  interpretation in theories, but we will also encounter
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    18
  interpretations in proofs, in
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    19
  Section~\ref{sec:local-interpretation}.
30580
cc5a55d7a5be Updated chapters 1-5 to locale reimplementation.
ballarin
parents: 29293
diff changeset
    20
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    21
  As an example, consider the type of integers @{typ int}.  The
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
    22
  relation @{term "op \<le>"} is a total order over @{typ int}.  We start
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
    23
  with the interpretation that @{term "op \<le>"} is a partial order.  The
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
    24
  facilities of the interpretation command are explored gradually in
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
    25
  three versions.
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    26
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    27
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    28
30580
cc5a55d7a5be Updated chapters 1-5 to locale reimplementation.
ballarin
parents: 29293
diff changeset
    29
subsection {* First Version: Replacement of Parameters Only
cc5a55d7a5be Updated chapters 1-5 to locale reimplementation.
ballarin
parents: 29293
diff changeset
    30
  \label{sec:po-first} *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    31
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    32
text {*
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    33
  The command \isakeyword{interpretation} is for the interpretation of
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    34
  locale in theories.  In the following example, the parameter of locale
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    35
  @{text partial_order} is replaced by @{term "op \<le> :: int \<Rightarrow> int \<Rightarrow>
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    36
  bool"} and the locale instance is interpreted in the current
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    37
  theory. *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    38
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    39
  interpretation %visible int: partial_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    40
txt {* \normalsize
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    41
  The argument of the command is a simple \emph{locale expression}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    42
  consisting of the name of the interpreted locale, which is
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    43
  preceded by the qualifier @{text "int:"} and succeeded by a
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    44
  white-space-separated list of terms, which provide a full
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    45
  instantiation of the locale parameters.  The parameters are referred
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    46
  to by order of declaration, which is also the order in which
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
    47
  \isakeyword{print\_locale} outputs them.  The locale has only a
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
    48
  single parameter, hence the list of instantiation terms is a
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
    49
  singleton.
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    50
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    51
  The command creates the goal
30580
cc5a55d7a5be Updated chapters 1-5 to locale reimplementation.
ballarin
parents: 29293
diff changeset
    52
  @{subgoals [display]} which can be shown easily:
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    53
 *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    54
    by unfold_locales auto
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    55
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    56
text {*  The effect of the command is that instances of all
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    57
  conclusions of the locale are available in the theory, where names
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    58
  are prefixed by the qualifier.  For example, transitivity for @{typ
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    59
  int} is named @{thm [source] int.trans} and is the following
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    60
  theorem:
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    61
  @{thm [display, indent=2] int.trans}
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    62
  It is not possible to reference this theorem simply as @{text
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
    63
  trans}.  This prevents unwanted hiding of existing theorems of the
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    64
  theory by an interpretation. *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    65
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    66
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    67
subsection {* Second Version: Replacement of Definitions *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    68
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    69
text {* Not only does the above interpretation qualify theorem names.
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    70
  The prefix @{text int} is applied to all names introduced in locale
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    71
  conclusions including names introduced in definitions.  The
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
    72
  qualified name @{text int.less} is short for
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    73
  the interpretation of the definition, which is @{term int.less}.
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    74
  Qualified name and expanded form may be used almost
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    75
  interchangeably.%
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    76
\footnote{Since @{term "op \<le>"} is polymorphic, for @{term int.less} a
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    77
  more general type will be inferred than for @{text int.less} which
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    78
  is over type @{typ int}.}
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    79
  The latter is preferred on output, as for example in the theorem
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    80
  @{thm [source] int.less_le_trans}: @{thm [display, indent=2]
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    81
  int.less_le_trans}
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    82
  Both notations for the strict order are not satisfactory.  The
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    83
  constant @{term "op <"} is the strict order for @{typ int}.
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    84
  In order to allow for the desired replacement, interpretation
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    85
  accepts \emph{equations} in addition to the parameter instantiation.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    86
  These follow the locale expression and are indicated with the
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
    87
  keyword \isakeyword{where}.  This is the revised interpretation:
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30826
diff changeset
    88
  *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    89
end