22 *} |
22 *} |
23 (*>*) |
23 (*>*) |
24 |
24 |
25 chapter {* First Steps *} |
25 chapter {* First Steps *} |
26 |
26 |
|
27 |
27 text {* |
28 text {* |
28 Isabelle programming happens in an enhanced dialect of Standard ML, |
29 Isabelle programming is done Standard ML, however it often uses an |
29 which adds antiquotations containing references to the logical |
30 antiquotation mehanism to refer to the logical context of Isabelle. |
30 context. |
31 The ML-code that one writes is, just like lemmas and proofs in Isabelle, |
31 |
32 part of a theory. If you want to follow the code written in this |
32 Just like all lemmas or proofs, all ML code that you write lives in |
33 chapter, we assume you are working inside the theory defined as |
33 a theory, where it is embedded using the \isacommand{ML} command: |
34 |
|
35 \begin{tabular}{@ {}l} |
|
36 \isacommand{theory} CookBook\\ |
|
37 \isacommand{imports} Main\\ |
|
38 \isacommand{begin}\\ |
|
39 \end{tabular} |
|
40 |
|
41 |
|
42 The easiest and quickest way to include code in a theory is |
|
43 by using the \isacommand{ML} command. For example |
34 *} |
44 *} |
35 |
45 |
36 ML {* |
46 ML {* |
37 3 + 4 |
47 3 + 4 |
38 *} |
48 *} |
39 |
49 |
40 text {* |
50 text {* |
41 The \isacommand{ML} command takes an arbitrary ML expression, which |
51 The expression inside \isacommand{ML} commands is emmediately evaluated |
42 is evaluated. It can also contain value or function bindings. |
52 like ``normal'' proof scripts by using the advance and retreat buttons of |
|
53 your Isabelle environment. The code inside the \isacommand{ML} command |
|
54 can also contain value- and function bindings. \marginpar{\tiny FIXME can one undo them like |
|
55 Isabelle lemmas/proofs - probably not} |
43 *} |
56 *} |
44 |
57 |
45 section {* Antiquotations *} |
58 section {* Antiquotations *} |
46 |
59 |
47 text {* |
60 text {* |
48 The main advantage of embedding all code in a theory is that the |
61 The main advantage of embedding all code in a theory is that the |
49 code can contain references to entities that are defined in the |
62 code can contain references to entities that are defined on the |
50 theory. Let us for example, print out the name of the current |
63 logical level of Isabelle. This is done using antiquotations. |
51 theory: |
64 For example, one can print out the name of |
|
65 the current theory by typing |
52 *} |
66 *} |
53 |
67 |
54 ML {* Context.theory_name @{theory} *} |
68 ML {* Context.theory_name @{theory} *} |
55 |
69 |
56 text {* The @{text "@{theory}"} antiquotation is substituted with the |
70 text {* |
57 current theory, whose name can then be extracted using a the |
71 where @{text "@{theory}"} is an antiquotation that is substituted with the |
58 function @{ML "Context.theory_name"}. Note that antiquotations are |
72 current theory (remember that we assumed we are inside the theory CookBook). |
59 statically scoped. The function |
73 The name of this theory can be extrated using a the function @{ML "Context.theory_name"}. |
|
74 So the code above returns the string @{ML "\"CookBook\""}. |
|
75 |
|
76 Note that antiquotations are statically scoped, that is the value is |
|
77 determined at ``compile-time'' not ``run-time''. For example the function |
|
78 |
60 *} |
79 *} |
61 |
80 |
62 ML {* |
81 ML {* |
63 fun current_thyname () = Context.theory_name @{theory} |
82 fun current_thyname () = Context.theory_name @{theory} |
64 *} |
83 *} |
65 |
84 |
66 text {* |
85 text {* |
67 does \emph{not} return the name of the current theory. Instead, we have |
86 does \emph{not} return the name of the current theory, if it is run in a |
68 defined the constant function that always returns the string @{ML "\"CookBook\""}, which is |
87 different theory. Instead, the code above defines the constant function |
69 the name of @{text "@{theory}"} at the point where the code |
88 that always returns the string @{ML "\"CookBook\""}, no matter where the |
70 is embedded. Operationally speaking, @{text "@{theory}"} is \emph{not} |
89 function is called. Operationally speaking, @{text "@{theory}"} is |
71 replaced with code that will look up the current theory in some |
90 \emph{not} replaced with code that will look up the current theory in |
72 (destructive) data structure and return it. Instead, it is really |
91 some data structure and return it. Instead, it is literally |
73 replaced with the theory value. |
92 replaced with the value representing the theory name. |
74 |
93 |
75 In the course of this introduction, we will learn about more of |
94 In the course of this introduction, we will learn more about |
76 these antoquotations, which greatly simplify programming, since you |
95 these antoquotations: they greatly simplify Isabelle programming since one |
77 can directly access all kinds of logical elements from ML. |
96 can directly access all kinds of logical elements from ML. |
78 *} |
97 *} |
79 |
98 |
80 section {* Terms *} |
99 section {* Terms *} |
81 |
100 |
86 |
105 |
87 ML {* @{term "(a::nat) + b = c"} *} |
106 ML {* @{term "(a::nat) + b = c"} *} |
88 |
107 |
89 text {* |
108 text {* |
90 This shows the term @{term "(a::nat) + b = c"} in the internal |
109 This shows the term @{term "(a::nat) + b = c"} in the internal |
91 representation, with all gory details. Terms are just an ML |
110 representation with all gory details. Terms are just an ML |
92 datatype, and they are defined in @{ML_file "Pure/term.ML"}. |
111 datatype, and they are defined in @{ML_file "Pure/term.ML"}. |
93 |
112 |
94 The representation of terms uses deBruin indices: Bound variables |
113 The representation of terms uses deBruin indices: bound variables |
95 are represented by the constructor @{ML Bound}, and the index refers to |
114 are represented by the constructor @{ML Bound}, and the index refers to |
96 the number of lambdas we have to skip until we hit the lambda that |
115 the number of lambdas we have to skip until we hit the lambda that |
97 binds the variable. The names of bound variables are kept at the |
116 binds the variable. The names of bound variables are kept at the |
98 abstractions, but they are just comments. |
117 abstractions, but they should be treated just as comments. |
99 See \ichcite{ch:logic} for more details. |
118 See \ichcite{ch:logic} for more details. |
100 |
119 |
101 \begin{readmore} |
120 \begin{readmore} |
102 Terms are described in detail in \ichcite{ch:logic}. Their |
121 Terms are described in detail in \ichcite{ch:logic}. Their |
103 definition and many useful operations can be found in @{ML_file "Pure/term.ML"}. |
122 definition and many useful operations can be found in @{ML_file "Pure/term.ML"}. |