21 |
21 |
22 \medskip |
22 \medskip |
23 While terms, types and theorems are the most basic data structures in |
23 While terms, types and theorems are the most basic data structures in |
24 Isabelle, there are a number of layers built on top of them. Most of these |
24 Isabelle, there are a number of layers built on top of them. Most of these |
25 layers are concerned with storing and manipulating data. Handling them |
25 layers are concerned with storing and manipulating data. Handling them |
26 properly is an essential skill for programming on the ML-level of Isabelle |
26 properly is an essential skill for programming on the ML-level of Isabelle. |
27 programming. The most basic layer are theories. They contain global data and |
27 The most basic layer are theories. They contain global data and |
28 can be seen as the ``long-term memory'' of Isabelle. There is usually only |
28 can be seen as the ``long-term memory'' of Isabelle. There is usually only |
29 one theory active at each moment. Proof contexts and local theories, on the |
29 one theory active at each moment. Proof contexts and local theories, on the |
30 other hand, store local data for a task at hand. They act like the |
30 other hand, store local data for a task at hand. They act like the |
31 ``short-term memory'' and there can be many of them that are active in |
31 ``short-term memory'' and there can be many of them that are active in |
32 parallel. |
32 parallel. |
33 *} |
33 *} |
34 |
34 |
35 section {* Theories and Setups\label{sec:theories} *} |
35 section {* Theories and Setups\label{sec:theories} *} |
36 |
36 |
37 text {* |
37 text {* |
38 Theories, as said above, are the most basic layer of abstraction in |
38 Theories, as said above, are a basic layer of abstraction in Isabelle. They |
39 Isabelle. They contain definitions, syntax declarations, axioms, proofs |
39 contain definitions, syntax declarations, axioms, theorems and much more. If a |
40 and much more. If a definition is made, it must be stored in a theory in order to be |
40 definition is made, it must be stored in a theory in order to be usable |
41 usable later on. Similar with proofs: once a proof is finished, the proved |
41 later on. Similar with proofs: once a proof is finished, the proved theorem |
42 theorem needs to be stored in the theorem database of the theory in order to |
42 needs to be stored in the theorem database of the theory in order to be |
43 be usable. All relevant data of a theory can be queried as follows. |
43 usable. All relevant data of a theory can be queried as follows. |
44 |
44 |
45 \begin{isabelle} |
45 \begin{isabelle} |
46 \isacommand{print\_theory}\\ |
46 \isacommand{print\_theory}\\ |
47 @{text "> names: Pure Code_Generator HOL \<dots>"}\\ |
47 @{text "> names: Pure Code_Generator HOL \<dots>"}\\ |
48 @{text "> classes: Inf < type \<dots>"}\\ |
48 @{text "> classes: Inf < type \<dots>"}\\ |
56 @{text "> oracles: \<dots>"}\\ |
56 @{text "> oracles: \<dots>"}\\ |
57 @{text "> definitions: \<dots>"}\\ |
57 @{text "> definitions: \<dots>"}\\ |
58 @{text "> theorems: \<dots>"} |
58 @{text "> theorems: \<dots>"} |
59 \end{isabelle} |
59 \end{isabelle} |
60 |
60 |
|
61 Functions acting on theories often end with the suffix @{text "_global"}, |
|
62 for example the function @{ML read_term_global in Syntax} in the structure |
|
63 @{ML_struct Syntax}. The reason is to set them syntactically apart from |
|
64 functions acting on contexts or local theories (which will be discussed in |
|
65 next sections). There is a tendency in the Isabelle development to prefer |
|
66 ``non-global'' operations, because they have some advantages, as we will also |
|
67 discuss later. However, some basic management of theories will very likely |
|
68 never go away. |
|
69 |
61 In the context ML-programming, the most important command with theories |
70 In the context ML-programming, the most important command with theories |
62 is \isacommand{setup}. In the previous chapters we used it, for |
71 is \isacommand{setup}. In the previous chapters we used it, for |
63 example, to make a theorem attribute known to Isabelle or to register a theorem |
72 example, to make a theorem attribute known to Isabelle or to register a theorem |
64 under a name. What happens behind the scenes is that \isacommand{setup} |
73 under a name. What happens behind the scenes is that \isacommand{setup} |
65 expects a function of type @{ML_type "theory -> theory"}: the input theory |
74 expects a function of type @{ML_type "theory -> theory"}: the input theory |