12 |
12 |
13 |
13 |
14 chapter {* Advanced Isabelle *} |
14 chapter {* Advanced Isabelle *} |
15 |
15 |
16 text {* |
16 text {* |
17 TBD |
17 While terms, types and theorems are the most basic data structures in |
|
18 Isabelle, there are a number of layers built on top of them. Most of these |
|
19 layers are concerned with storing and manipulating data. Handling |
|
20 them properly is an essential skill for Isabelle programming. The most basic |
|
21 layer are theories. They contain global data and can be seen as the |
|
22 ``long-term memory'' of Isabelle. There is usually only one theory |
|
23 active at each moment. Proof contexts and local theories, on the |
|
24 other hand, store local data for a task at hand. They act like the |
|
25 ``short-term memory'' and there can be many of them that are active |
|
26 in parallel. |
18 *} |
27 *} |
19 |
28 |
20 section {* Theories\label{sec:theories} (TBD) *} |
29 section {* Theories\label{sec:theories} (TBD) *} |
21 |
30 |
22 text {* |
31 text {* |
23 Theories are the most fundamental building blocks in Isabelle. They |
32 As said above, theories are the most basic layer in Isabelle. They contain |
24 contain definitions, syntax declarations, axioms, proofs etc. If a definition |
33 definitions, syntax declarations, axioms, proofs etc. If a definition is |
25 is stated, it must be stored in a theory in order to be usable later |
34 stated, it must be stored in a theory in order to be usable later |
26 on. Similar with proofs: once a proof is finished, the proved theorem |
35 on. Similar with proofs: once a proof is finished, the proved theorem needs |
27 needs to be stored in the theorem database of the theory in order to |
36 to be stored in the theorem database of the theory in order to be |
28 be usable. All relevant data of a theort can be querried as follows. |
37 usable. All relevant data of a theory can be queried as follows. |
29 |
38 |
30 \begin{isabelle} |
39 \begin{isabelle} |
31 \isacommand{print\_theory}\\ |
40 \isacommand{print\_theory}\\ |
32 @{text "> names: Pure Code_Generator HOL \<dots>"}\\ |
41 @{text "> names: Pure Code_Generator HOL \<dots>"}\\ |
33 @{text "> classes: Inf < type \<dots>"}\\ |
42 @{text "> classes: Inf < type \<dots>"}\\ |
41 @{text "> oracles: \<dots>"}\\ |
50 @{text "> oracles: \<dots>"}\\ |
42 @{text "> definitions: \<dots>"}\\ |
51 @{text "> definitions: \<dots>"}\\ |
43 @{text "> theorems: \<dots>"} |
52 @{text "> theorems: \<dots>"} |
44 \end{isabelle} |
53 \end{isabelle} |
45 |
54 |
|
55 |
|
56 |
46 \begin{center} |
57 \begin{center} |
47 \begin{tikzpicture} |
58 \begin{tikzpicture} |
48 \node[top color=white, bottom color=gray!30, draw=black!100, drop shadow] {A}; |
59 \node[top color=white, bottom color=gray!30, draw=black!100, drop shadow] {A}; |
49 \end{tikzpicture} |
60 \end{tikzpicture} |
50 \end{center} |
61 \end{center} |
51 |
|
52 |
|
53 In contrast to an ordinary theory, which simply consists of a type |
|
54 signature, as well as tables for constants, axioms and theorems, a local |
|
55 theory contains additional context information, such as locally fixed |
|
56 variables and local assumptions that may be used by the package. The type |
|
57 @{ML_type local_theory} is identical to the type of \emph{proof contexts} |
|
58 @{ML_type "Proof.context"}, although not every proof context constitutes a |
|
59 valid local theory. |
|
60 |
|
61 @{ML "Context.>> o Context.map_theory"} |
|
62 |
62 |
63 \footnote{\bf FIXME: list append in merge operations can cause |
63 \footnote{\bf FIXME: list append in merge operations can cause |
64 exponential blowups.} |
64 exponential blowups.} |
65 *} |
65 *} |
66 |
66 |
122 section {* Contexts (TBD) *} |
122 section {* Contexts (TBD) *} |
123 |
123 |
124 section {* Local Theories (TBD) *} |
124 section {* Local Theories (TBD) *} |
125 |
125 |
126 text {* |
126 text {* |
|
127 In contrast to an ordinary theory, which simply consists of a type |
|
128 signature, as well as tables for constants, axioms and theorems, a local |
|
129 theory contains additional context information, such as locally fixed |
|
130 variables and local assumptions that may be used by the package. The type |
|
131 @{ML_type local_theory} is identical to the type of \emph{proof contexts} |
|
132 @{ML_type "Proof.context"}, although not every proof context constitutes a |
|
133 valid local theory. |
|
134 |
|
135 @{ML "Context.>> o Context.map_theory"} |
127 @{ML_ind "Local_Theory.declaration"} |
136 @{ML_ind "Local_Theory.declaration"} |
128 *} |
137 *} |
129 |
138 |
130 (* |
139 (* |
131 setup {* |
140 setup {* |