6 |
6 |
7 |
7 |
8 chapter {* First Steps *} |
8 chapter {* First Steps *} |
9 |
9 |
10 text {* |
10 text {* |
11 Isabelle programming is done in ML. Just like lemmas and proofs, ML-code |
11 Isabelle programming is done in ML. Just like lemmas and proofs, ML-code for |
12 for Isabelle must be part of a theory. If you want to follow the code given in |
12 Isabelle must be part of a theory. If you want to follow the code given in |
13 this chapter, we assume you are working inside the theory starting with |
13 this chapter, we assume you are working inside the theory starting with |
14 |
14 |
15 \begin{quote} |
15 \begin{quote} |
16 \begin{tabular}{@ {}l} |
16 \begin{tabular}{@ {}l} |
17 \isacommand{theory} FirstSteps\\ |
17 \isacommand{theory} FirstSteps\\ |
26 *} |
26 *} |
27 |
27 |
28 section {* Including ML-Code *} |
28 section {* Including ML-Code *} |
29 |
29 |
30 text {* |
30 text {* |
31 The easiest and quickest way to include code in a theory is |
31 The easiest and quickest way to include code in a theory is by using the |
32 by using the \isacommand{ML}-command. For example: |
32 \isacommand{ML}-command. For example: |
33 |
33 |
34 \begin{isabelle} |
34 \begin{isabelle} |
35 \begin{graybox} |
35 \begin{graybox} |
36 \isacommand{ML}~@{text "\<verbopen>"}\isanewline |
36 \isacommand{ML}~@{text "\<verbopen>"}\isanewline |
37 \hspace{5mm}@{ML "3 + 4"}\isanewline |
37 \hspace{5mm}@{ML "3 + 4"}\isanewline |
38 @{text "\<verbclose>"}\isanewline |
38 @{text "\<verbclose>"}\isanewline |
39 @{text "> 7"}\smallskip |
39 @{text "> 7"}\smallskip |
40 \end{graybox} |
40 \end{graybox} |
41 \end{isabelle} |
41 \end{isabelle} |
42 |
42 |
43 Like normal Isabelle scripts, \isacommand{ML}-commands can be |
43 Like normal Isabelle scripts, \isacommand{ML}-commands can be evaluated by |
44 evaluated by using the advance and undo buttons of your Isabelle |
44 using the advance and undo buttons of your Isabelle environment. The code |
45 environment. The code inside the \isacommand{ML}-command can also contain |
45 inside the \isacommand{ML}-command can also contain value and function |
46 value and function bindings, for example |
46 bindings, for example |
47 *} |
47 *} |
48 |
48 |
49 ML %gray {* |
49 ML %gray {* |
50 val r = ref 0 |
50 val r = ref 0 |
51 fun f n = n + 1 |
51 fun f n = n + 1 |
52 *} |
52 *} |
53 |
53 |
54 text {* |
54 text {* |
55 and even those can be undone when the proof |
55 and even those can be undone when the proof script is retracted. As |
56 script is retracted. As mentioned in the Introduction, we will drop the |
56 mentioned in the Introduction, we will drop the \isacommand{ML}~@{text |
57 \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we |
57 "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we show code. The lines |
58 show code. The lines prefixed with @{text [quotes] ">"} are not part of the |
58 prefixed with @{text [quotes] ">"} are not part of the code, rather they |
59 code, rather they indicate what the response is when the code is evaluated. |
59 indicate what the response is when the code is evaluated. There are also |
60 There are also the commands \isacommand{ML\_val} and \isacommand{ML\_prf} for |
60 the commands \isacommand{ML\_val} and \isacommand{ML\_prf} for including |
61 including ML-code. The first evaluates the given code, but any effect on the |
61 ML-code. The first evaluates the given code, but any effect on the theory, |
62 theory, in which the code is embedded, is suppressed. The second needs to |
62 in which the code is embedded, is suppressed. The second needs to be used if |
63 be used if ML-code is defined |
63 ML-code is defined inside a proof. For example |
64 inside a proof. For example |
|
65 |
64 |
66 \begin{quote} |
65 \begin{quote} |
67 \begin{isabelle} |
66 \begin{isabelle} |
68 \isacommand{lemma}~@{text "test:"}\isanewline |
67 \isacommand{lemma}~@{text "test:"}\isanewline |
69 \isacommand{shows}~@{text [quotes] "True"}\isanewline |
68 \isacommand{shows}~@{text [quotes] "True"}\isanewline |
70 \isacommand{ML\_prf}~@{text "\<verbopen>"}~@{ML "writeln \"Trivial!\""}~@{text "\<verbclose>"}\isanewline |
69 \isacommand{ML\_prf}~@{text "\<verbopen>"}~@{ML "writeln \"Trivial!\""}~@{text "\<verbclose>"}\isanewline |
71 \isacommand{oops} |
70 \isacommand{oops} |
72 \end{isabelle} |
71 \end{isabelle} |
73 \end{quote} |
72 \end{quote} |
74 |
73 |
75 However, both commands will only play minor roles in this tutorial (we will always |
74 However, both commands will only play minor roles in this tutorial (we will |
76 arrange that the ML-code is defined outside of proofs, for example). |
75 always arrange that the ML-code is defined outside of proofs, for example). |
77 |
76 |
78 Once a portion of code is relatively stable, you usually want to export it |
77 Once a portion of code is relatively stable, you usually want to export it |
79 to a separate ML-file. Such files can then be included somewhere inside a |
78 to a separate ML-file. Such files can then be included somewhere inside a |
80 theory by using the command \isacommand{use}. For example |
79 theory by using the command \isacommand{use}. For example |
81 |
80 |
103 \isacommand{begin}\\ |
102 \isacommand{begin}\\ |
104 \ldots |
103 \ldots |
105 \end{tabular} |
104 \end{tabular} |
106 \end{quote} |
105 \end{quote} |
107 |
106 |
108 Note that no parentheses are given this time. Note also that the |
107 Note that no parentheses are given this time. Note also that the included |
109 included ML-file should not contain any |
108 ML-file should not contain any \isacommand{use} itself. Otherwise Isabelle |
110 \isacommand{use} itself. Otherwise Isabelle is unable to record all |
109 is unable to record all file dependencies, which is a nuisance if you have |
111 file dependencies, which is a nuisance if you have to track down |
110 to track down errors. |
112 errors. |
|
113 *} |
111 *} |
114 |
112 |
115 section {* Debugging and Printing\label{sec:printing} *} |
113 section {* Debugging and Printing\label{sec:printing} *} |
116 |
114 |
117 text {* |
115 text {* |
118 |
116 During development you might find it necessary to inspect some data in your |
119 During development you might find it necessary to inspect some data |
117 code. This can be done in a ``quick-and-dirty'' fashion using the function |
120 in your code. This can be done in a ``quick-and-dirty'' fashion using |
118 @{ML [index] "writeln"}. For example |
121 the function @{ML [index] "writeln"}. For example |
|
122 |
119 |
123 @{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""} |
120 @{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""} |
124 |
121 |
125 will print out @{text [quotes] "any string"} inside the response buffer |
122 will print out @{text [quotes] "any string"} inside the response buffer of |
126 of Isabelle. This function expects a string as argument. If you develop under PolyML, |
123 Isabelle. This function expects a string as argument. If you develop under |
127 then there is a convenient, though again ``quick-and-dirty'', method for |
124 PolyML, then there is a convenient, though again ``quick-and-dirty'', method |
128 converting values into strings, namely the function @{ML PolyML.makestring}: |
125 for converting values into strings, namely the function |
|
126 @{ML [index] makestring in PolyML}: |
129 |
127 |
130 @{ML_response_fake [display,gray] "writeln (PolyML.makestring 1)" "\"1\""} |
128 @{ML_response_fake [display,gray] "writeln (PolyML.makestring 1)" "\"1\""} |
131 |
129 |
132 However, @{ML [index] makestring in PolyML} only works if the type of what is converted is monomorphic |
130 However, @{ML makestring in PolyML} only works if the type of what |
133 and not a function. |
131 is converted is monomorphic and not a function. |
134 |
132 |
135 The function @{ML "writeln"} should only be used for testing purposes, because any |
133 The function @{ML "writeln"} should only be used for testing purposes, |
136 output this function generates will be overwritten as soon as an error is |
134 because any output this function generates will be overwritten as soon as an |
137 raised. For printing anything more serious and elaborate, the |
135 error is raised. For printing anything more serious and elaborate, the |
138 function @{ML [index] tracing} is more appropriate. This function writes all output into |
136 function @{ML [index] tracing} is more appropriate. This function writes all |
139 a separate tracing buffer. For example: |
137 output into a separate tracing buffer. For example: |
140 |
138 |
141 @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""} |
139 @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""} |
142 |
140 |
143 It is also possible to redirect the ``channel'' where the string @{text "foo"} is |
141 It is also possible to redirect the ``channel'' where the string @{text |
144 printed to a separate file, e.g., to prevent ProofGeneral from choking on massive |
142 "foo"} is printed to a separate file, e.g., to prevent ProofGeneral from |
145 amounts of trace output. This redirection can be achieved with the code: |
143 choking on massive amounts of trace output. This redirection can be achieved |
|
144 with the code: |
146 *} |
145 *} |
147 |
146 |
148 ML{*val strip_specials = |
147 ML{*val strip_specials = |
149 let |
148 let |
150 fun strip ("\^A" :: _ :: cs) = strip cs |
149 fun strip ("\^A" :: _ :: cs) = strip cs |
196 ML {* Toplevel.program (fn () => innocent ()) *} |
195 ML {* Toplevel.program (fn () => innocent ()) *} |
197 *) |
196 *) |
198 |
197 |
199 text {* |
198 text {* |
200 Most often you want to inspect data of Isabelle's most basic data |
199 Most often you want to inspect data of Isabelle's most basic data |
201 structures, namely @{ML_type term}, @{ML_type cterm} or @{ML_type |
200 structures, namely @{ML_type term}, @{ML_type cterm} and @{ML_type |
202 thm}. Isabelle contains elaborate pretty-printing functions for printing |
201 thm}. Isabelle contains elaborate pretty-printing functions for printing |
203 them (see Section \ref{sec:pretty}), but for quick-and-dirty solutions they |
202 them (see Section \ref{sec:pretty}), but for quick-and-dirty solutions they |
204 are a bit unwieldy. One way to transform a term into a string is to use the |
203 are a bit unwieldy. One way to transform a term into a string is to use the |
205 function @{ML [index] string_of_term in Syntax} in structure @{ML_struct |
204 function @{ML [index] string_of_term in Syntax} in structure @{ML_struct |
206 Syntax}, which we bind for more convenience to the toplevel. |
205 Syntax}, which we bind for more convenience to the toplevel. |
268 "tracing (string_of_thm @{context} @{thm conjI})" |
267 "tracing (string_of_thm @{context} @{thm conjI})" |
269 "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"} |
268 "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"} |
270 |
269 |
271 In order to improve the readability of theorems we convert these schematic |
270 In order to improve the readability of theorems we convert these schematic |
272 variables into free variables using the function @{ML [index] import in |
271 variables into free variables using the function @{ML [index] import in |
273 Variable}. This is similar to the theorem attribute @{text "[no_vars]"} from |
272 Variable}. This is similar to statements like @{text "conjI[no_vars]"} |
274 Isabelle's user-level. |
273 from Isabelle's user-level. |
275 *} |
274 *} |
276 |
275 |
277 ML{*fun no_vars ctxt thm = |
276 ML{*fun no_vars ctxt thm = |
278 let |
277 let |
279 val ((_, [thm']), _) = Variable.import true [thm] ctxt |
278 val ((_, [thm']), _) = Variable.import true [thm] ctxt |
522 |
521 |
523 text {* |
522 text {* |
524 These two functions can be used to avoid explicit @{text "lets"} for |
523 These two functions can be used to avoid explicit @{text "lets"} for |
525 intermediate values in functions that return pairs. Suppose for example you |
524 intermediate values in functions that return pairs. Suppose for example you |
526 want to separate a list of integers into two lists according to a |
525 want to separate a list of integers into two lists according to a |
527 treshold. For example if the treshold is @{ML "5"}, the list @{ML |
526 treshold. If the treshold is @{ML "5"}, the list @{ML "[1,6,2,5,3,4]"} |
528 "[1,6,2,5,3,4]"} should be separated to @{ML "([1,2,3,4], [6,5])"}. This |
527 should be separated to @{ML "([1,2,3,4], [6,5])"}. This function can be |
529 function can be implemented as |
528 implemented as |
530 *} |
529 *} |
531 |
530 |
532 ML{*fun separate i [] = ([], []) |
531 ML{*fun separate i [] = ([], []) |
533 | separate i (x::xs) = |
532 | separate i (x::xs) = |
534 let |
533 let |
617 #-> (fn x => fn y => x + y)*} |
616 #-> (fn x => fn y => x + y)*} |
618 |
617 |
619 |
618 |
620 text {* |
619 text {* |
621 When using combinators for writing function in waterfall fashion, it is |
620 When using combinators for writing function in waterfall fashion, it is |
622 sometimes necessary to do some ``plumbing'' for fitting functions |
621 sometimes necessary to do some ``plumbing'' in order to fit functions |
623 together. We have already seen such plumbing in the function @{ML |
622 together. We have already seen such plumbing in the function @{ML |
624 apply_fresh_args}, where @{ML curry} is needed for making the function @{ML |
623 apply_fresh_args}, where @{ML curry} is needed for making the function @{ML |
625 list_comb} that works over pairs to fit with the combinator @{ML "|>"}. Such |
624 list_comb} that works over pairs to fit with the combinator @{ML "|>"}. Such |
626 plumbing is also needed in situations where a functions operate over lists, |
625 plumbing is also needed in situations where a functions operate over lists, |
627 but one calculates only with a single entity. An example is the function |
626 but one calculates only with a single entity. An example is the function |