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 a basic layer of abstraction in |
38 Theories, as said above, are the most basic layer of abstraction in |
39 Isabelle. They contain definitions, syntax declarations, axioms, |
39 Isabelle. They record information about 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 with the |
44 usable. All relevant data of a theory can be queried with the |
68 ``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 |
69 discuss later. However, some basic understanding of theories is still necessary |
69 discuss later. However, some basic understanding of theories is still necessary |
70 for effective Isabelle programming. |
70 for effective Isabelle programming. |
71 |
71 |
72 An important Isabelle command with theories is \isacommand{setup}. In the |
72 An important Isabelle command with theories is \isacommand{setup}. In the |
73 previous chapters we used it to make, for example, a theorem attribute known |
73 previous chapters we used it already to make a theorem attribute known |
74 to Isabelle or to register a theorem under a name. What happens behind the |
74 to Isabelle and to register a theorem under a name. What happens behind the |
75 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 |
76 "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 |
77 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 |
78 stored. This is a fundamental principle in Isabelle. A similar situation |
78 stored. This is a fundamental principle in Isabelle. A similar situation |
79 arises with declaring a constant, which can be done on the ML-level with |
79 arises with declaring a constant, which can be done on the ML-level with |
122 \begin{isabelle} |
122 \begin{isabelle} |
123 \isacommand{term}~@{text [quotes] "BAR"}\\ |
123 \isacommand{term}~@{text [quotes] "BAR"}\\ |
124 @{text "> \"BAR\" :: \"nat\""} |
124 @{text "> \"BAR\" :: \"nat\""} |
125 \end{isabelle} |
125 \end{isabelle} |
126 |
126 |
127 returns now a (black) constant with the type @{typ nat}, as expected. |
127 now returns a (black) constant with the type @{typ nat}, as expected. |
128 |
128 |
129 In a sense, \isacommand{setup} can be seen as a transaction that |
129 In a sense, \isacommand{setup} can be seen as a transaction that |
130 takes the current theory @{text thy}, applies an operation, and |
130 takes the current theory @{text thy}, applies an operation, and |
131 produces a new current theory @{text thy'}. This means that we have |
131 produces a new current theory @{text thy'}. This means that we have |
132 to be careful to apply operations always to the most current theory, |
132 to be careful to apply operations always to the most current theory, |
199 text {* |
199 text {* |
200 Contexts are arguably more important than theories, even though they only |
200 Contexts are arguably more important than theories, even though they only |
201 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 |
202 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 |
203 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. |
204 For this consider the following contrived proof whose only purpose is to |
204 For this consider the following contrived proof-snippet whose only purpose is to |
205 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} |
|
213 *} |
206 *} |
214 |
207 |
215 lemma "True" |
208 lemma "True" |
216 proof - |
209 proof - |
217 txt_raw {*\mbox{}\\[-7mm]*} |
210 txt_raw {*\mbox{}\\[-7mm]*} |
218 ML_prf{*Variable.dest_fixes @{context}*} |
211 ML_prf {* Variable.dest_fixes @{context} *} |
219 txt_raw {*\mbox{}\\[-7mm]\mbox{}*} |
212 txt_raw {*\mbox{}\\[-7mm]\mbox{}*} |
220 fix x y |
213 fix x y |
221 txt_raw {*\mbox{}\\[-7mm]*} |
214 txt_raw {*\mbox{}\\[-7mm]*} |
222 ML_prf {* Variable.dest_fixes @{context} *} |
215 ML_prf {* Variable.dest_fixes @{context} *} |
223 txt_raw {*\mbox{}\\[-7mm] \ldots*}(*<*)oops(*>*) |
216 txt_raw {*\mbox{}\\[-7mm] \ldots*}(*<*)oops(*>*) |
224 |
217 |
225 text {* |
218 text {* |
232 means a context has a dataslot containing information about fixed variables. |
225 means a context has a dataslot containing information about fixed variables. |
233 The ML-antiquotation @{text "@{context}"} points to the context that is |
226 The ML-antiquotation @{text "@{context}"} points to the context that is |
234 active at that point of the theory. Consequently, in the first call to |
227 active at that point of the theory. Consequently, in the first call to |
235 @{ML dest_fixes in Variable} this dataslot is empty; in the second it is |
228 @{ML dest_fixes in Variable} this dataslot is empty; in the second it is |
236 filled with @{text x} and @{text y}. What is interesting is that contexts |
229 filled with @{text x} and @{text y}. What is interesting is that contexts |
237 can be stacked. For this consider the following proof fraqument |
230 can be stacked. For this consider the following proof fragment |
238 *} |
231 *} |
239 |
232 |
240 lemma "True" |
233 lemma "True" |
241 proof - |
234 proof - |
242 fix x y |
235 fix x y |
243 { fix z w |
236 { fix z w |
244 txt_raw {*\mbox{}\\[-7mm]*} |
237 txt_raw {*\mbox{}\\[-7mm]*} |
245 ML_prf {* Variable.dest_fixes @{context} *} |
238 ML_prf {* Variable.dest_fixes @{context} *} |
246 txt_raw {*\mbox{}\\[-7mm]*} |
239 txt_raw {*\mbox{}\\[-7mm]\mbox{}*} |
247 txt_raw {* \mbox{}\hspace{4mm}\mbox{} *} } |
240 } |
248 txt_raw {*\mbox{}\\[-7mm]*} |
241 txt_raw {*\mbox{}\\[-7mm]*} |
249 ML_prf {* Variable.dest_fixes @{context} *} |
242 ML_prf {* Variable.dest_fixes @{context} *} |
250 txt_raw {*\mbox{}\\[-7mm] \ldots*}(*<*)oops(*>*) |
243 txt_raw {*\mbox{}\\[-7mm] \ldots*}(*<*)oops(*>*) |
251 |
244 |
252 text {* |
245 text {* |
|
246 The first time we call @{ML dest_fixes in Variable} we have four fixes variables; |
|
247 the second time we get only the fixes variables @{text x} and @{text y} as answer. |
|
248 This means the curly-braces act as opening and closing statements for a context. |
253 The above proof corresoponds roughly to the following ML-code. |
249 The above proof corresoponds roughly to the following ML-code. |
254 *} |
250 *} |
|
251 |
|
252 ML{*val ctxt0 = @{context}; |
|
253 val ([x, y], ctxt1) = Variable.add_fixes ["x", "y"] ctxt0; |
|
254 val ([z, w], ctxt2) = Variable.add_fixes ["z", "w"] ctxt1*} |
|
255 |
|
256 text {* |
|
257 Now let us come back to the point about printing terms. |
|
258 *} |
|
259 |
255 |
260 |
256 (* |
261 (* |
257 ML{*Proof_Context.debug := true*} |
262 ML{*Proof_Context.debug := true*} |
258 ML{*Proof_Context.verbose := true*} |
263 ML{*Proof_Context.verbose := true*} |
259 *) |
264 *) |