author | ballarin |
Sat, 28 Mar 2009 22:14:21 +0100 | |
changeset 30780 | c3f1e8a9e0b5 |
parent 30580 | cc5a55d7a5be |
child 30826 | a53f4872400e |
permissions | -rw-r--r-- |
27063 | 1 |
% |
2 |
\begin{isabellebody}% |
|
3 |
\def\isabellecontext{Examples{\isadigit{1}}}% |
|
4 |
% |
|
5 |
\isadelimtheory |
|
6 |
% |
|
7 |
\endisadelimtheory |
|
8 |
% |
|
9 |
\isatagtheory |
|
27080 | 10 |
\isacommand{theory}\isamarkupfalse% |
11 |
\ Examples{\isadigit{1}}\isanewline |
|
12 |
\isakeyword{imports}\ Examples\isanewline |
|
13 |
\isakeyword{begin}% |
|
27063 | 14 |
\endisatagtheory |
15 |
{\isafoldtheory}% |
|
16 |
% |
|
17 |
\isadelimtheory |
|
18 |
% |
|
19 |
\endisadelimtheory |
|
20 |
% |
|
21 |
\isamarkupsection{Use of Locales in Theories and Proofs% |
|
22 |
} |
|
23 |
\isamarkuptrue% |
|
24 |
% |
|
25 |
\begin{isamarkuptext}% |
|
26 |
Locales enable to prove theorems abstractly, relative to |
|
27 |
sets of assumptions. These theorems can then be used in other |
|
28 |
contexts where the assumptions themselves, or |
|
29 |
instances of the assumptions, are theorems. This form of theorem |
|
30 |
reuse is called \emph{interpretation}. |
|
31 |
||
32 |
The changes of the locale |
|
33 |
hierarchy from the previous sections are examples of |
|
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
29297
diff
changeset
|
34 |
interpretations. The command \isakeyword{sublocale} $l_1 |
27063 | 35 |
\subseteq l_2$ is said to \emph{interpret} locale $l_2$ in the |
36 |
context of $l_1$. It causes all theorems of $l_2$ to be made |
|
37 |
available in $l_1$. The interpretation is \emph{dynamic}: not only |
|
38 |
theorems already present in $l_2$ are available in $l_1$. Theorems |
|
39 |
that will be added to $l_2$ in future will automatically be |
|
40 |
propagated to $l_1$. |
|
41 |
||
42 |
Locales can also be interpreted in the contexts of theories and |
|
43 |
structured proofs. These interpretations are dynamic, too. |
|
44 |
Theorems added to locales will be propagated to theories. |
|
45 |
In this section the interpretation in |
|
46 |
theories is illustrated; interpretation in proofs is analogous. |
|
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
29297
diff
changeset
|
47 |
|
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
29297
diff
changeset
|
48 |
As an example, consider the type of natural numbers \isa{nat}. The |
27063 | 49 |
order relation \isa{{\isasymle}} is a total order over \isa{nat}, |
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
29297
diff
changeset
|
50 |
divisibility \isa{dvd} is a distributive lattice. We start with the |
27063 | 51 |
interpretation that \isa{{\isasymle}} is a partial order. The facilities of |
52 |
the interpretation command are explored in three versions.% |
|
53 |
\end{isamarkuptext}% |
|
54 |
\isamarkuptrue% |
|
55 |
% |
|
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
29297
diff
changeset
|
56 |
\isamarkupsubsection{First Version: Replacement of Parameters Only |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
29297
diff
changeset
|
57 |
\label{sec:po-first}% |
27063 | 58 |
} |
59 |
\isamarkuptrue% |
|
60 |
% |
|
61 |
\begin{isamarkuptext}% |
|
27079 | 62 |
In the most basic form, interpretation just replaces the locale |
27063 | 63 |
parameters by terms. The following command interprets the locale |
64 |
\isa{partial{\isacharunderscore}order} in the global context of the theory. The |
|
65 |
parameter \isa{le} is replaced by \isa{op\ {\isasymle}}.% |
|
66 |
\end{isamarkuptext}% |
|
67 |
\isamarkuptrue% |
|
68 |
% |
|
69 |
\isadelimvisible |
|
70 |
\ \ % |
|
71 |
\endisadelimvisible |
|
72 |
% |
|
73 |
\isatagvisible |
|
74 |
\isacommand{interpretation}\isamarkupfalse% |
|
30780 | 75 |
\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}% |
27063 | 76 |
\begin{isamarkuptxt}% |
77 |
The locale name is succeeded by a \emph{parameter |
|
30780 | 78 |
instantiation}. This is a list of terms, which refer to |
27063 | 79 |
the parameters in the order of declaration in the locale. The |
30780 | 80 |
locale name is preceded by an optional \emph{interpretation |
81 |
qualifier}. |
|
27063 | 82 |
|
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
29297
diff
changeset
|
83 |
The command creates the goal% |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
29297
diff
changeset
|
84 |
\footnote{Note that \isa{op} binds tighter than functions |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
29297
diff
changeset
|
85 |
application: parentheses around \isa{op\ {\isasymle}} are not necessary.} |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
29297
diff
changeset
|
86 |
\begin{isabelle}% |
27063 | 87 |
\ {\isadigit{1}}{\isachardot}\ partial{\isacharunderscore}order\ op\ {\isasymle}% |
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
29297
diff
changeset
|
88 |
\end{isabelle} which can be shown easily:% |
27063 | 89 |
\end{isamarkuptxt}% |
90 |
\isamarkuptrue% |
|
91 |
\ \ \ \ \isacommand{by}\isamarkupfalse% |
|
92 |
\ unfold{\isacharunderscore}locales\ auto% |
|
93 |
\endisatagvisible |
|
94 |
{\isafoldvisible}% |
|
95 |
% |
|
96 |
\isadelimvisible |
|
97 |
% |
|
98 |
\endisadelimvisible |
|
99 |
% |
|
100 |
\begin{isamarkuptext}% |
|
101 |
Now theorems from the locale are available in the theory, |
|
102 |
interpreted for natural numbers, for example \isa{nat{\isachardot}trans}: \begin{isabelle}% |
|
103 |
\ \ {\isasymlbrakk}{\isacharquery}x\ {\isasymle}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymle}\ {\isacharquery}z% |
|
104 |
\end{isabelle} |
|
105 |
||
30780 | 106 |
The interpretation qualifier, \isa{nat} in the example, is applied |
107 |
to all names processed by the interpretation. If a qualifer is |
|
108 |
given in the \isakeyword{interpretation} command, its use is |
|
109 |
mandatory when referencing the name. For example, the above theorem |
|
110 |
cannot be referred to simply by \isa{trans}. This prevents |
|
111 |
unwanted hiding of theorems.% |
|
27063 | 112 |
\end{isamarkuptext}% |
113 |
\isamarkuptrue% |
|
114 |
% |
|
115 |
\isamarkupsubsection{Second Version: Replacement of Definitions% |
|
116 |
} |
|
117 |
\isamarkuptrue% |
|
118 |
% |
|
119 |
\begin{isamarkuptext}% |
|
120 |
The above interpretation also creates the theorem |
|
121 |
\isa{nat{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: \begin{isabelle}% |
|
122 |
\ \ {\isasymlbrakk}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharquery}x\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}z{\isasymrbrakk}\isanewline |
|
123 |
\isaindent{\ \ }{\isasymLongrightarrow}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharquery}x\ {\isacharquery}z% |
|
124 |
\end{isabelle} |
|
125 |
Here, \isa{partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}} |
|
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
29297
diff
changeset
|
126 |
represents the strict order, although \isa{{\isacharless}} is the natural |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
29297
diff
changeset
|
127 |
strict order for \isa{nat}. Interpretation allows to map concepts |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
29297
diff
changeset
|
128 |
introduced through definitions in locales to the corresponding |
27063 | 129 |
concepts of the theory.% |
130 |
\footnote{This applies not only to \isakeyword{definition} but also to |
|
131 |
\isakeyword{inductive}, \isakeyword{fun} and \isakeyword{function}.}% |
|
132 |
\end{isamarkuptext}% |
|
133 |
\isamarkuptrue% |
|
134 |
% |
|
135 |
\isadelimtheory |
|
136 |
% |
|
137 |
\endisadelimtheory |
|
138 |
% |
|
139 |
\isatagtheory |
|
27080 | 140 |
\isacommand{end}\isamarkupfalse% |
27063 | 141 |
% |
142 |
\endisatagtheory |
|
143 |
{\isafoldtheory}% |
|
144 |
% |
|
145 |
\isadelimtheory |
|
146 |
% |
|
147 |
\endisadelimtheory |
|
27080 | 148 |
\isanewline |
27063 | 149 |
\end{isabellebody}% |
150 |
%%% Local Variables: |
|
151 |
%%% mode: latex |
|
152 |
%%% TeX-master: "root" |
|
153 |
%%% End: |