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 |
theory Examples1 |
2 |
imports Examples |
|
3 |
begin |
|
4 |
||
5 |
section {* Use of Locales in Theories and Proofs *} |
|
6 |
||
7 |
text {* Locales enable to prove theorems abstractly, relative to |
|
8 |
sets of assumptions. These theorems can then be used in other |
|
9 |
contexts where the assumptions themselves, or |
|
10 |
instances of the assumptions, are theorems. This form of theorem |
|
11 |
reuse is called \emph{interpretation}. |
|
12 |
||
13 |
The changes of the locale |
|
14 |
hierarchy from the previous sections are examples of |
|
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
29293
diff
changeset
|
15 |
interpretations. The command \isakeyword{sublocale} $l_1 |
27063 | 16 |
\subseteq l_2$ is said to \emph{interpret} locale $l_2$ in the |
17 |
context of $l_1$. It causes all theorems of $l_2$ to be made |
|
18 |
available in $l_1$. The interpretation is \emph{dynamic}: not only |
|
19 |
theorems already present in $l_2$ are available in $l_1$. Theorems |
|
20 |
that will be added to $l_2$ in future will automatically be |
|
21 |
propagated to $l_1$. |
|
22 |
||
23 |
Locales can also be interpreted in the contexts of theories and |
|
24 |
structured proofs. These interpretations are dynamic, too. |
|
25 |
Theorems added to locales will be propagated to theories. |
|
26 |
In this section the interpretation in |
|
27 |
theories is illustrated; interpretation in proofs is analogous. |
|
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
29293
diff
changeset
|
28 |
|
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
29293
diff
changeset
|
29 |
As an example, consider the type of natural numbers @{typ nat}. The |
27063 | 30 |
order relation @{text \<le>} is a total order over @{typ nat}, |
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
29293
diff
changeset
|
31 |
divisibility @{text dvd} is a distributive lattice. We start with the |
27063 | 32 |
interpretation that @{text \<le>} is a partial order. The facilities of |
33 |
the interpretation command are explored in three versions. |
|
34 |
*} |
|
35 |
||
36 |
||
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
29293
diff
changeset
|
37 |
subsection {* First Version: Replacement of Parameters Only |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
29293
diff
changeset
|
38 |
\label{sec:po-first} *} |
27063 | 39 |
|
40 |
text {* |
|
41 |
In the most basic form, interpretation just replaces the locale |
|
42 |
parameters by terms. The following command interprets the locale |
|
43 |
@{text partial_order} in the global context of the theory. The |
|
44 |
parameter @{term le} is replaced by @{term "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"}. *} |
|
45 |
||
30780 | 46 |
interpretation %visible nat: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool" |
27063 | 47 |
txt {* The locale name is succeeded by a \emph{parameter |
30780 | 48 |
instantiation}. This is a list of terms, which refer to |
27063 | 49 |
the parameters in the order of declaration in the locale. The |
30780 | 50 |
locale name is preceded by an optional \emph{interpretation |
51 |
qualifier}. |
|
27063 | 52 |
|
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
29293
diff
changeset
|
53 |
The command creates the goal% |
27063 | 54 |
\footnote{Note that @{text op} binds tighter than functions |
55 |
application: parentheses around @{text "op \<le>"} are not necessary.} |
|
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
29293
diff
changeset
|
56 |
@{subgoals [display]} which can be shown easily: |
27063 | 57 |
*} |
58 |
by unfold_locales auto |
|
59 |
||
60 |
text {* Now theorems from the locale are available in the theory, |
|
61 |
interpreted for natural numbers, for example @{thm [source] |
|
62 |
nat.trans}: @{thm [display, indent=2] nat.trans} |
|
63 |
||
30780 | 64 |
The interpretation qualifier, @{text nat} in the example, is applied |
65 |
to all names processed by the interpretation. If a qualifer is |
|
66 |
given in the \isakeyword{interpretation} command, its use is |
|
67 |
mandatory when referencing the name. For example, the above theorem |
|
68 |
cannot be referred to simply by @{text trans}. This prevents |
|
69 |
unwanted hiding of theorems. *} |
|
27063 | 70 |
|
71 |
||
72 |
subsection {* Second Version: Replacement of Definitions *} |
|
73 |
||
74 |
text {* The above interpretation also creates the theorem |
|
75 |
@{thm [source] nat.less_le_trans}: @{thm [display, indent=2] |
|
76 |
nat.less_le_trans} |
|
77 |
Here, @{term "partial_order.less (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"} |
|
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
29293
diff
changeset
|
78 |
represents the strict order, although @{text "<"} is the natural |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
29293
diff
changeset
|
79 |
strict order for @{typ nat}. Interpretation allows to map concepts |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
29293
diff
changeset
|
80 |
introduced through definitions in locales to the corresponding |
27063 | 81 |
concepts of the theory.% |
82 |
\footnote{This applies not only to \isakeyword{definition} but also to |
|
83 |
\isakeyword{inductive}, \isakeyword{fun} and \isakeyword{function}.} |
|
84 |
*} |
|
85 |
||
86 |
end |