39 Isabelle. They contain definitions, syntax declarations, axioms, |
39 Isabelle. They contain definitions, syntax declarations, axioms, |
40 theorems and much more. For example, if a definition is made, it |
40 theorems and much more. For example, if a definition is made, it |
41 must be stored in a theory in order to be usable later on. Similar |
41 must be stored in a theory in order to be usable later on. Similar |
42 with proofs: once a proof is finished, the proved theorem needs to |
42 with proofs: once a proof is finished, the proved theorem needs to |
43 be stored in the theorem database of the theory in order to be |
43 be stored in the theorem database of the theory in order to be |
44 usable. All relevant data of a theory can be queried as follows. |
44 usable. All relevant data of a theory can be queried with the |
|
45 Isabelle command \isacommand{print\_theory}. |
45 |
46 |
46 \begin{isabelle} |
47 \begin{isabelle} |
47 \isacommand{print\_theory}\\ |
48 \isacommand{print\_theory}\\ |
48 @{text "> names: Pure Code_Generator HOL \<dots>"}\\ |
49 @{text "> names: Pure Code_Generator HOL \<dots>"}\\ |
49 @{text "> classes: Inf < type \<dots>"}\\ |
50 @{text "> classes: Inf < type \<dots>"}\\ |
60 \end{isabelle} |
61 \end{isabelle} |
61 |
62 |
62 Functions acting on theories often end with the suffix @{text "_global"}, |
63 Functions acting on theories often end with the suffix @{text "_global"}, |
63 for example the function @{ML read_term_global in Syntax} in the structure |
64 for example the function @{ML read_term_global in Syntax} in the structure |
64 @{ML_struct Syntax}. The reason is to set them syntactically apart from |
65 @{ML_struct Syntax}. The reason is to set them syntactically apart from |
65 functions acting on contexts or local theories (which will be discussed in |
66 functions acting on contexts or local theories, which will be discussed in |
66 the next sections). There is a tendency in the Isabelle development to prefer |
67 the next sections. There is a tendency amongst Isabelle developers to prefer |
67 ``non-global'' operations, because they have some advantages, as we will also |
68 ``non-global'' operations, because they have some advantages, as we will also |
68 discuss later. However, some basic understanding of theories is still necessary |
69 discuss later. However, some basic understanding of theories is still necessary |
69 for effective Isabelle programming. |
70 for effective Isabelle programming. |
70 |
71 |
71 An important command with theories is \isacommand{setup}. In the |
72 An important Isabelle command with theories is \isacommand{setup}. In the |
72 previous chapters we used it to make, for example, a theorem attribute known |
73 previous chapters we used it to make, for example, a theorem attribute known |
73 to Isabelle or to register a theorem under a name. What happens behind the |
74 to Isabelle or to register a theorem under a name. What happens behind the |
74 scenes is that \isacommand{setup} expects a function of type @{ML_type |
75 scenes is that \isacommand{setup} expects a function of type @{ML_type |
75 "theory -> theory"}: the input theory is the current theory and the output |
76 "theory -> theory"}: the input theory is the current theory and the output |
76 the theory where the attribute has been registered or the theorem has been |
77 the theory where the attribute has been registered or the theorem has been |
77 stored. This is a fundamental principle in Isabelle. A similar situation |
78 stored. This is a fundamental principle in Isabelle. A similar situation |
78 arises with declaring constants. The function that declares a constant on |
79 arises with declaring a constant, which can be done on the ML-level with |
79 the ML-level is @{ML_ind declare_const in Sign} in the structure @{ML_struct |
80 function @{ML_ind declare_const in Sign} from the structure @{ML_struct |
80 Sign}. To see how \isacommand{setup} works, consider the following code: |
81 Sign}. To see how \isacommand{setup} works, consider the following code: |
81 |
82 |
82 *} |
83 *} |
83 |
84 |
84 ML{*let |
85 ML{*let |
89 end*} |
90 end*} |
90 |
91 |
91 text {* |
92 text {* |
92 If you simply run this code\footnote{Recall that ML-code needs to be enclosed in |
93 If you simply run this code\footnote{Recall that ML-code needs to be enclosed in |
93 \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.} with the |
94 \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.} with the |
94 intention of declaring a constant @{text "BAR"} with type @{typ nat}, then |
95 intention of declaring a constant @{text "BAR"} having type @{typ nat}, then |
95 indeed you obtain a theory as result. But if you query the |
96 indeed you obtain a theory as result. But if you query the |
96 constant on the Isabelle level using the command \isacommand{term} |
97 constant on the Isabelle level using the command \isacommand{term} |
97 |
98 |
98 \begin{isabelle} |
99 \begin{isabelle} |
99 \isacommand{term}~@{text BAR}\\ |
100 \isacommand{term}~@{text BAR}\\ |
123 @{text "> \"BAR\" :: \"nat\""} |
124 @{text "> \"BAR\" :: \"nat\""} |
124 \end{isabelle} |
125 \end{isabelle} |
125 |
126 |
126 returns now a (black) constant with the type @{typ nat}, as expected. |
127 returns now a (black) constant with the type @{typ nat}, as expected. |
127 |
128 |
128 In a sense, \isacommand{setup} can be seen as a transaction that takes the |
129 In a sense, \isacommand{setup} can be seen as a transaction that |
129 current theory, applies an operation, and produces a new current theory. This |
130 takes the current theory @{text thy}, applies an operation, and |
130 means that we have to be careful to apply operations always to the most current |
131 produces a new current theory @{text thy'}. This means that we have |
131 theory, not to a \emph{stale} one. Consider again the function inside the |
132 to be careful to apply operations always to the most current theory, |
|
133 not to a \emph{stale} one. Consider again the function inside the |
132 \isacommand{setup}-command: |
134 \isacommand{setup}-command: |
133 |
135 |
134 \begin{isabelle} |
136 \begin{isabelle} |
135 \begin{graybox} |
137 \begin{graybox} |
136 \isacommand{setup}~@{text "\<verbopen>"} @{ML |
138 \isacommand{setup}~@{text "\<verbopen>"} @{ML |
199 contain ``short-term memory data''. The reason is that a vast number of |
201 contain ``short-term memory data''. The reason is that a vast number of |
200 functions in Isabelle depend in one way or another on contexts. Even such |
202 functions in Isabelle depend in one way or another on contexts. Even such |
201 mundane operations like printing out a term make essential use of contexts. |
203 mundane operations like printing out a term make essential use of contexts. |
202 For this consider the following contrived proof whose only purpose is to |
204 For this consider the following contrived proof whose only purpose is to |
203 fix two variables: |
205 fix two variables: |
|
206 |
|
207 \def\shadecolor{gray} |
|
208 \begin{shaded} |
|
209 aaa |
|
210 \end{shaded} |
|
211 |
|
212 \mbox{}\hspace{10mm}\begin{graybox}aa\end{graybox} |
204 *} |
213 *} |
205 |
214 |
206 lemma "True" |
215 lemma "True" |
207 proof - |
216 proof - |
208 txt {*\mbox{}\\[-7mm]*} ML_prf {* Variable.dest_fixes @{context} *} txt {*\mbox{}\\[-7mm]*} |
217 txt_raw {*\mbox{}\\[-7mm]*} |
|
218 ML_prf{*Variable.dest_fixes @{context}*} |
|
219 txt_raw {*\mbox{}\\[-7mm]\mbox{}*} |
209 fix x y |
220 fix x y |
210 txt {*\mbox{}\\[-7mm]*} |
221 txt_raw {*\mbox{}\\[-7mm]*} |
211 ML_prf {* Variable.dest_fixes @{context} *} |
222 ML_prf {* Variable.dest_fixes @{context} *} |
212 txt {*\mbox{}\\[-7mm]*} |
223 txt_raw {*\mbox{}\\[-7mm] \ldots*}(*<*)oops(*>*) |
213 oops |
|
214 |
224 |
215 text {* |
225 text {* |
216 The interesting point in this proof is that we injected ML-code before and after |
226 The interesting point in this proof is that we injected ML-code before and after |
217 the variables are fixed. For this remember that ML-code inside a proof |
227 the variables are fixed. For this remember that ML-code inside a proof |
218 needs to be enclosed in \isacommand{ML\_prf}~@{text "\<verbopen> \<dots> \<verbclose>"}, |
228 needs to be enclosed in \isacommand{ML\_prf}~@{text "\<verbopen> \<dots> \<verbclose>"}, |
229 |
239 |
230 lemma "True" |
240 lemma "True" |
231 proof - |
241 proof - |
232 fix x y |
242 fix x y |
233 { fix z w |
243 { fix z w |
234 txt {*\mbox{}\\[-7mm]*} |
244 txt_raw {*\mbox{}\\[-7mm]*} |
235 ML_prf {* Variable.dest_fixes @{context} *} |
245 ML_prf {* Variable.dest_fixes @{context} *} |
236 txt {*\mbox{}\\[-7mm]*} |
246 txt_raw {*\mbox{}\\[-7mm]*} |
237 } |
247 txt_raw {* \mbox{}\hspace{4mm}\mbox{} *} } |
238 txt {*\mbox{}\\[-7mm]*} |
248 txt_raw {*\mbox{}\\[-7mm]*} |
239 ML_prf {* Variable.dest_fixes @{context} *} |
249 ML_prf {* Variable.dest_fixes @{context} *} |
240 txt {*\mbox{}\\[-7mm]*} |
250 txt_raw {*\mbox{}\\[-7mm] \ldots*}(*<*)oops(*>*) |
241 oops |
251 |
|
252 text {* |
|
253 The above proof corresoponds roughly to the following ML-code. |
|
254 *} |
242 |
255 |
243 (* |
256 (* |
244 ML{*Proof_Context.debug := true*} |
257 ML{*Proof_Context.debug := true*} |
245 ML{*Proof_Context.verbose := true*} |
258 ML{*Proof_Context.verbose := true*} |
246 *) |
259 *) |