2
|
1 |
theory FirstSteps
|
25
|
2 |
imports Base
|
2
|
3 |
begin
|
|
4 |
|
|
5 |
chapter {* First Steps *}
|
|
6 |
|
42
|
7 |
text {*
|
|
8 |
|
54
|
9 |
Isabelle programming is done in ML. Just like lemmas and proofs, ML-code
|
89
|
10 |
in Isabelle is part of a theory. If you want to follow the code given in
|
54
|
11 |
this chapter, we assume you are working inside the theory starting with
|
2
|
12 |
|
6
|
13 |
\begin{center}
|
5
|
14 |
\begin{tabular}{@ {}l}
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
15 |
\isacommand{theory} FirstSteps\\
|
5
|
16 |
\isacommand{imports} Main\\
|
|
17 |
\isacommand{begin}\\
|
6
|
18 |
\ldots
|
5
|
19 |
\end{tabular}
|
6
|
20 |
\end{center}
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
21 |
*}
|
5
|
22 |
|
20
|
23 |
section {* Including ML-Code *}
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
24 |
|
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
25 |
|
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
26 |
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
27 |
text {*
|
5
|
28 |
The easiest and quickest way to include code in a theory is
|
89
|
29 |
by using the \isacommand{ML}-command. For example:
|
2
|
30 |
|
75
|
31 |
\begin{isabelle}
|
|
32 |
\begin{graybox}
|
85
|
33 |
\isacommand{ML}~@{text "\<verbopen>"}\isanewline
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
34 |
\hspace{5mm}@{ML "3 + 4"}\isanewline
|
85
|
35 |
@{text "\<verbclose>"}\isanewline
|
|
36 |
@{text "> 7"}\smallskip
|
75
|
37 |
\end{graybox}
|
|
38 |
\end{isabelle}
|
2
|
39 |
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
40 |
Like normal Isabelle proof scripts, \isacommand{ML}-commands can be
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
41 |
evaluated by using the advance and undo buttons of your Isabelle
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
42 |
environment. The code inside the \isacommand{ML}-command can also contain
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
43 |
value and function bindings, and even those can be undone when the proof
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
44 |
script is retracted. As mentioned earlier, we will drop the
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
45 |
\isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we
|
107
|
46 |
show code. The lines prefixed with @{text [quotes] ">"} are not part of the
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
47 |
code, rather they indicate what the response is when the code is evaluated.
|
10
|
48 |
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
49 |
Once a portion of code is relatively stable, you usually want to export it
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
50 |
to a separate ML-file. Such files can then be included in a theory by using
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
51 |
the \isacommand{uses}-command in the header of the theory, like:
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
52 |
|
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
53 |
\begin{center}
|
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
54 |
\begin{tabular}{@ {}l}
|
54
|
55 |
\isacommand{theory} FirstSteps\\
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
56 |
\isacommand{imports} Main\\
|
58
|
57 |
\isacommand{uses} @{text "\"file_to_be_included.ML\""} @{text "\<dots>"}\\
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
58 |
\isacommand{begin}\\
|
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
59 |
\ldots
|
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
60 |
\end{tabular}
|
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
61 |
\end{center}
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
62 |
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
63 |
*}
|
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
64 |
|
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
65 |
section {* Debugging and Printing *}
|
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
66 |
|
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
67 |
text {*
|
13
|
68 |
|
50
|
69 |
During development you might find it necessary to inspect some data
|
10
|
70 |
in your code. This can be done in a ``quick-and-dirty'' fashion using
|
12
|
71 |
the function @{ML "warning"}. For example
|
10
|
72 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
73 |
@{ML_response_fake [display,gray] "warning \"any string\"" "\"any string\""}
|
10
|
74 |
|
58
|
75 |
will print out @{text [quotes] "any string"} inside the response buffer
|
|
76 |
of Isabelle. This function expects a string as argument. If you develop under PolyML,
|
50
|
77 |
then there is a convenient, though again ``quick-and-dirty'', method for
|
107
|
78 |
converting values into strings, namely the function @{ML makestring}:
|
10
|
79 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
80 |
@{ML_response_fake [display,gray] "warning (makestring 1)" "\"1\""}
|
12
|
81 |
|
65
|
82 |
However @{ML makestring} only works if the type of what is converted is monomorphic
|
78
|
83 |
and not a function.
|
12
|
84 |
|
52
|
85 |
The function @{ML "warning"} should only be used for testing purposes, because any
|
|
86 |
output this function generates will be overwritten as soon as an error is
|
50
|
87 |
raised. For printing anything more serious and elaborate, the
|
54
|
88 |
function @{ML tracing} is more appropriate. This function writes all output into
|
89
|
89 |
a separate tracing buffer. For example:
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
90 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
91 |
@{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
92 |
|
58
|
93 |
It is also possible to redirect the ``channel'' where the string @{text "foo"} is
|
78
|
94 |
printed to a separate file, e.g.~to prevent ProofGeneral from choking on massive
|
107
|
95 |
amounts of trace output. This redirection can be achieved with the code:
|
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
96 |
*}
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
97 |
|
69
|
98 |
ML{*val strip_specials =
|
42
|
99 |
let
|
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
100 |
fun strip ("\^A" :: _ :: cs) = strip cs
|
42
|
101 |
| strip (c :: cs) = c :: strip cs
|
|
102 |
| strip [] = [];
|
|
103 |
in implode o strip o explode end;
|
|
104 |
|
|
105 |
fun redirect_tracing stream =
|
|
106 |
Output.tracing_fn := (fn s =>
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
107 |
(TextIO.output (stream, (strip_specials s));
|
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
108 |
TextIO.output (stream, "\n");
|
69
|
109 |
TextIO.flushOut stream)) *}
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
110 |
|
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
111 |
text {*
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
112 |
Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"}
|
58
|
113 |
will cause that all tracing information is printed into the file @{text "foo.bar"}.
|
75
|
114 |
|
107
|
115 |
You can print out error messages with the function @{ML error}; for example:
|
75
|
116 |
|
|
117 |
@{ML_response_fake [display,gray] "if 0=1 then 1 else (error \"foo\")" "\"foo\""}
|
|
118 |
|
104
|
119 |
Section~\ref{sec:printing} will give more information about printing
|
107
|
120 |
the main data structures of Isabelle, namely @{ML_type term}, @{ML_type cterm}
|
104
|
121 |
and @{ML_type thm}.
|
15
|
122 |
*}
|
|
123 |
|
10
|
124 |
|
75
|
125 |
|
|
126 |
|
2
|
127 |
section {* Antiquotations *}
|
|
128 |
|
|
129 |
text {*
|
49
|
130 |
The main advantage of embedding all code in a theory is that the code can
|
58
|
131 |
contain references to entities defined on the logical level of Isabelle. By
|
|
132 |
this we mean definitions, theorems, terms and so on. This kind of reference is
|
|
133 |
realised with antiquotations. For example, one can print out the name of the current
|
49
|
134 |
theory by typing
|
|
135 |
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
136 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
137 |
@{ML_response [display,gray] "Context.theory_name @{theory}" "\"FirstSteps\""}
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
138 |
|
5
|
139 |
where @{text "@{theory}"} is an antiquotation that is substituted with the
|
49
|
140 |
current theory (remember that we assumed we are inside the theory
|
89
|
141 |
@{text FirstSteps}). The name of this theory can be extracted using
|
49
|
142 |
the function @{ML "Context.theory_name"}.
|
5
|
143 |
|
89
|
144 |
Note, however, that antiquotations are statically linked, that is their value is
|
12
|
145 |
determined at ``compile-time'', not ``run-time''. For example the function
|
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
146 |
*}
|
5
|
147 |
|
69
|
148 |
ML{*fun not_current_thyname () = Context.theory_name @{theory} *}
|
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
149 |
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
150 |
text {*
|
2
|
151 |
|
89
|
152 |
does \emph{not} return the name of the current theory, if it is run in a
|
5
|
153 |
different theory. Instead, the code above defines the constant function
|
58
|
154 |
that always returns the string @{text [quotes] "FirstSteps"}, no matter where the
|
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
155 |
function is called. Operationally speaking, the antiquotation @{text "@{theory}"} is
|
5
|
156 |
\emph{not} replaced with code that will look up the current theory in
|
|
157 |
some data structure and return it. Instead, it is literally
|
|
158 |
replaced with the value representing the theory name.
|
2
|
159 |
|
81
|
160 |
In a similar way you can use antiquotations to refer to proved theorems:
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
161 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
162 |
@{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
|
75
|
163 |
|
107
|
164 |
and simpsets:
|
75
|
165 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
166 |
@{ML_response_fake [display,gray]
|
70
|
167 |
"let
|
89
|
168 |
val ({rules,...}, _) = MetaSimplifier.rep_ss @{simpset}
|
70
|
169 |
in
|
|
170 |
map #name (Net.entries rules)
|
|
171 |
end" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
|
54
|
172 |
|
89
|
173 |
The code about simpsets extracts the theorem names stored in the
|
81
|
174 |
current simpset. We get hold of the current simpset with the antiquotation
|
|
175 |
@{text "@{simpset}"}. The function @{ML rep_ss in MetaSimplifier} returns a record
|
|
176 |
containing all information about the simpset. The rules of a simpset are
|
104
|
177 |
stored in a \emph{discrimination net} (a data structure for fast
|
81
|
178 |
indexing). From this net we can extract the entries using the function @{ML
|
|
179 |
Net.entries}.
|
|
180 |
|
10
|
181 |
|
75
|
182 |
\begin{readmore}
|
81
|
183 |
The infrastructure for simpsets is implemented in @{ML_file "Pure/meta_simplifier.ML"}
|
78
|
184 |
and @{ML_file "Pure/simplifier.ML"}. Discrimination nets are implemented
|
|
185 |
in @{ML_file "Pure/net.ML"}.
|
75
|
186 |
\end{readmore}
|
|
187 |
|
|
188 |
While antiquotations have many applications, they were originally introduced in order
|
89
|
189 |
to avoid explicit bindings for theorems such as:
|
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
190 |
*}
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
191 |
|
69
|
192 |
ML{*val allI = thm "allI" *}
|
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
193 |
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
194 |
text {*
|
78
|
195 |
These bindings are difficult to maintain and also can be accidentally
|
89
|
196 |
overwritten by the user. This often breakes Isabelle
|
49
|
197 |
packages. Antiquotations solve this problem, since they are ``linked''
|
89
|
198 |
statically at compile-time. However, this static linkage also limits their
|
|
199 |
usefulness in cases where data needs to be build up dynamically. In the
|
|
200 |
course of this introduction, we will learn more about these antiquotations:
|
|
201 |
they greatly simplify Isabelle programming since one can directly access all
|
|
202 |
kinds of logical elements from th ML-level.
|
49
|
203 |
|
2
|
204 |
*}
|
|
205 |
|
15
|
206 |
section {* Terms and Types *}
|
2
|
207 |
|
|
208 |
text {*
|
49
|
209 |
One way to construct terms of Isabelle on the ML-level is by using the antiquotation
|
89
|
210 |
\mbox{@{text "@{term \<dots>}"}}. For example:
|
2
|
211 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
212 |
@{ML_response [display,gray]
|
75
|
213 |
"@{term \"(a::nat) + b = c\"}"
|
|
214 |
"Const (\"op =\", \<dots>) $
|
|
215 |
(Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
|
2
|
216 |
|
50
|
217 |
This will show the term @{term "(a::nat) + b = c"}, but printed using the internal
|
13
|
218 |
representation of this term. This internal representation corresponds to the
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
219 |
datatype @{ML_type "term"}.
|
2
|
220 |
|
34
|
221 |
The internal representation of terms uses the usual de Bruijn index mechanism where bound
|
11
|
222 |
variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to
|
10
|
223 |
the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that
|
12
|
224 |
binds the corresponding variable. However, in Isabelle the names of bound variables are
|
11
|
225 |
kept at abstractions for printing purposes, and so should be treated only as comments.
|
10
|
226 |
|
2
|
227 |
\begin{readmore}
|
13
|
228 |
Terms are described in detail in \isccite{sec:terms}. Their
|
78
|
229 |
definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}.
|
2
|
230 |
\end{readmore}
|
|
231 |
|
13
|
232 |
Sometimes the internal representation of terms can be surprisingly different
|
12
|
233 |
from what you see at the user level, because the layers of
|
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
234 |
parsing/type-checking/pretty printing can be quite elaborate.
|
2
|
235 |
|
10
|
236 |
\begin{exercise}
|
2
|
237 |
Look at the internal term representation of the following terms, and
|
89
|
238 |
find out why they are represented like this:
|
2
|
239 |
|
|
240 |
\begin{itemize}
|
|
241 |
\item @{term "case x of 0 \<Rightarrow> 0 | Suc y \<Rightarrow> y"}
|
|
242 |
\item @{term "\<lambda>(x,y). P y x"}
|
|
243 |
\item @{term "{ [x::int] | x. x \<le> -2 }"}
|
|
244 |
\end{itemize}
|
|
245 |
|
|
246 |
Hint: The third term is already quite big, and the pretty printer
|
|
247 |
may omit parts of it by default. If you want to see all of it, you
|
104
|
248 |
can use the following ML-function to set the limit to a value high
|
13
|
249 |
enough:
|
12
|
250 |
|
75
|
251 |
@{ML [display,gray] "print_depth 50"}
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
252 |
\end{exercise}
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
253 |
|
13
|
254 |
The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type,
|
50
|
255 |
inserting the invisible @{text "Trueprop"}-coercions whenever necessary.
|
68
|
256 |
Consider for example the pairs
|
12
|
257 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
258 |
@{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),
|
65
|
259 |
Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
|
|
260 |
|
68
|
261 |
where an coercion is inserted in the second component and
|
12
|
262 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
263 |
@{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})"
|
65
|
264 |
"(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}
|
12
|
265 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
266 |
where it is not (since it is already constructed by a meta-implication).
|
19
|
267 |
|
89
|
268 |
Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example:
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
269 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
270 |
@{ML_response_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
271 |
|
19
|
272 |
\begin{readmore}
|
|
273 |
Types are described in detail in \isccite{sec:types}. Their
|
78
|
274 |
definition and many useful operations are implemented
|
|
275 |
in @{ML_file "Pure/type.ML"}.
|
19
|
276 |
\end{readmore}
|
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
277 |
*}
|
19
|
278 |
|
|
279 |
|
15
|
280 |
section {* Constructing Terms and Types Manually *}
|
12
|
281 |
|
|
282 |
text {*
|
81
|
283 |
While antiquotations are very convenient for constructing terms, they can
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
284 |
only construct fixed terms (remember they are ``linked'' at compile-time).
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
285 |
However, you often need to construct terms dynamically. For example, a
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
286 |
function that returns the implication @{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
287 |
@{term P}, @{term Q} and the type @{term "\<tau>"} as arguments can only be
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
288 |
written as:
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
289 |
|
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
290 |
*}
|
12
|
291 |
|
69
|
292 |
ML{*fun make_imp P Q tau =
|
12
|
293 |
let
|
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
294 |
val x = Free ("x",tau)
|
75
|
295 |
in
|
|
296 |
Logic.all x (Logic.mk_implies (P $ x, Q $ x))
|
69
|
297 |
end *}
|
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
298 |
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
299 |
text {*
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
300 |
The reason is that you cannot pass the arguments @{term P}, @{term Q} and
|
104
|
301 |
@{term "tau"} into an antiquotation. For example the following does \emph{not} work.
|
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
302 |
*}
|
13
|
303 |
|
69
|
304 |
ML{*fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} *}
|
12
|
305 |
|
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
306 |
text {*
|
19
|
307 |
To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"}
|
75
|
308 |
to both functions. With @{ML make_imp} we obtain the intended term involving
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
309 |
the given arguments
|
65
|
310 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
311 |
@{ML_response [display,gray] "make_imp @{term S} @{term T} @{typ nat}"
|
65
|
312 |
"Const \<dots> $
|
|
313 |
Abs (\"x\", Type (\"nat\",[]),
|
|
314 |
Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $
|
|
315 |
(Free (\"T\",\<dots>) $ \<dots>))"}
|
68
|
316 |
|
81
|
317 |
whereas with @{ML make_wrong_imp} we obtain a term involving the @{term "P"}
|
68
|
318 |
and @{text "Q"} from the antiquotation.
|
|
319 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
320 |
@{ML_response [display,gray] "make_wrong_imp @{term S} @{term T} @{typ nat}"
|
65
|
321 |
"Const \<dots> $
|
|
322 |
Abs (\"x\", \<dots>,
|
|
323 |
Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $
|
|
324 |
(Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
|
|
325 |
|
81
|
326 |
(FIXME: expand the following point)
|
|
327 |
|
68
|
328 |
One tricky point in constructing terms by hand is to obtain the fully
|
|
329 |
qualified name for constants. For example the names for @{text "zero"} and
|
|
330 |
@{text "+"} are more complex than one first expects, namely
|
19
|
331 |
|
15
|
332 |
|
|
333 |
\begin{center}
|
58
|
334 |
@{text "HOL.zero_class.zero"} and @{text "HOL.plus_class.plus"}.
|
15
|
335 |
\end{center}
|
|
336 |
|
68
|
337 |
The extra prefixes @{text zero_class} and @{text plus_class} are present
|
|
338 |
because these constants are defined within type classes; the prefix @{text
|
|
339 |
"HOL"} indicates in which theory they are defined. Guessing such internal
|
|
340 |
names can sometimes be quite hard. Therefore Isabelle provides the
|
|
341 |
antiquotation @{text "@{const_name \<dots>}"} which does the expansion
|
|
342 |
automatically, for example:
|
49
|
343 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
344 |
@{ML_response_fake [display,gray] "@{const_name \"Nil\"}" "List.list.Nil"}
|
10
|
345 |
|
19
|
346 |
(FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
|
11
|
347 |
|
104
|
348 |
Although to some extend types of terms can be inferred, there are many
|
|
349 |
situations where you need to construct types manually, especially
|
|
350 |
when defining constants. For example the function returning a function
|
|
351 |
type is as follows:
|
49
|
352 |
|
|
353 |
*}
|
|
354 |
|
69
|
355 |
ML{*fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2]) *}
|
49
|
356 |
|
104
|
357 |
text {* This can be equally written as: *}
|
49
|
358 |
|
69
|
359 |
ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *}
|
49
|
360 |
|
|
361 |
text {*
|
20
|
362 |
|
13
|
363 |
\begin{readmore}
|
89
|
364 |
There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
365 |
@{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms
|
49
|
366 |
and types easier.\end{readmore}
|
13
|
367 |
|
|
368 |
Have a look at these files and try to solve the following two exercises:
|
11
|
369 |
|
|
370 |
*}
|
|
371 |
|
|
372 |
text {*
|
|
373 |
|
13
|
374 |
\begin{exercise}\label{fun:revsum}
|
58
|
375 |
Write a function @{text "rev_sum : term -> term"} that takes a
|
11
|
376 |
term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "i"} might be zero)
|
|
377 |
and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume
|
|
378 |
the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"}
|
13
|
379 |
associates to the left. Try your function on some examples.
|
11
|
380 |
\end{exercise}
|
|
381 |
|
15
|
382 |
\begin{exercise}\label{fun:makesum}
|
11
|
383 |
Write a function which takes two terms representing natural numbers
|
75
|
384 |
in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produce the
|
11
|
385 |
number representing their sum.
|
|
386 |
\end{exercise}
|
|
387 |
|
107
|
388 |
A handy function for manipulating terms is @{ML map_types}: it takes a
|
|
389 |
function and applies it to every type in the term. You can, for example,
|
|
390 |
change every @{typ nat} into an @{typ int} using the function
|
89
|
391 |
*}
|
|
392 |
|
|
393 |
ML{*fun nat_to_int t =
|
|
394 |
(case t of
|
|
395 |
@{typ nat} => @{typ int}
|
|
396 |
| Type (s, ts) => Type (s, map nat_to_int ts)
|
|
397 |
| _ => t)*}
|
|
398 |
|
|
399 |
text {*
|
107
|
400 |
an then apply it as follows:
|
|
401 |
|
89
|
402 |
|
|
403 |
@{ML_response_fake [display,gray]
|
|
404 |
"map_types nat_to_int @{term \"a = (1::nat)\"}"
|
|
405 |
"Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\")
|
|
406 |
$ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}
|
|
407 |
|
11
|
408 |
*}
|
|
409 |
|
49
|
410 |
section {* Type-Checking *}
|
10
|
411 |
|
|
412 |
text {*
|
13
|
413 |
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
414 |
You can freely construct and manipulate terms, since they are just
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
415 |
arbitrary unchecked trees. However, you eventually want to see if a
|
54
|
416 |
term is well-formed, or type-checks, relative to a theory.
|
50
|
417 |
Type-checking is done via the function @{ML cterm_of}, which converts
|
10
|
418 |
a @{ML_type term} into a @{ML_type cterm}, a \emph{certified} term.
|
|
419 |
Unlike @{ML_type term}s, which are just trees, @{ML_type
|
|
420 |
"cterm"}s are abstract objects that are guaranteed to be
|
81
|
421 |
type-correct, and they can only be constructed via ``official
|
50
|
422 |
interfaces''.
|
2
|
423 |
|
54
|
424 |
Type-checking is always relative to a theory context. For now we use
|
10
|
425 |
the @{ML "@{theory}"} antiquotation to get hold of the current theory.
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
426 |
For example you can write:
|
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
427 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
428 |
@{ML_response_fake [display,gray] "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}
|
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
429 |
|
107
|
430 |
This can also be written with an antiquotation:
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
431 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
432 |
@{ML_response_fake [display,gray] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"}
|
10
|
433 |
|
78
|
434 |
Attempting to obtain the certified term for
|
54
|
435 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
436 |
@{ML_response_fake_both [display,gray] "@{cterm \"1 + True\"}" "Type unification failed \<dots>"}
|
54
|
437 |
|
78
|
438 |
yields an error (since the term is not typable). A slightly more elaborate
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
439 |
example that type-checks is:
|
20
|
440 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
441 |
@{ML_response_fake [display,gray]
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
442 |
"let
|
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
443 |
val natT = @{typ \"nat\"}
|
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
444 |
val zero = @{term \"0::nat\"}
|
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
445 |
in
|
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
446 |
cterm_of @{theory}
|
75
|
447 |
(Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero)
|
41
b11653b11bd3
further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
448 |
end" "0 + 0"}
|
12
|
449 |
|
13
|
450 |
\begin{exercise}
|
|
451 |
Check that the function defined in Exercise~\ref{fun:revsum} returns a
|
50
|
452 |
result that type-checks.
|
13
|
453 |
\end{exercise}
|
|
454 |
|
89
|
455 |
(FIXME: @{text "ctyp_of"}, @{ML fastype_of}, @{text dummyT})
|
86
|
456 |
|
13
|
457 |
*}
|
|
458 |
|
2
|
459 |
section {* Theorems *}
|
|
460 |
|
|
461 |
text {*
|
50
|
462 |
Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm}
|
78
|
463 |
that can only be built by going through interfaces. As a consequence, every proof
|
107
|
464 |
in Isabelle is correct by construction.
|
|
465 |
|
|
466 |
(FIXME reference LCF-philosophy)
|
2
|
467 |
|
78
|
468 |
To see theorems in ``action'', let us give a proof on the ML-level for the following
|
|
469 |
statement:
|
10
|
470 |
*}
|
|
471 |
|
|
472 |
lemma
|
|
473 |
assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x"
|
|
474 |
and assm\<^isub>2: "P t"
|
13
|
475 |
shows "Q t" (*<*)oops(*>*)
|
10
|
476 |
|
|
477 |
text {*
|
78
|
478 |
The corresponding ML-code is as follows:\footnote{Note that @{text "|>"} is reverse
|
75
|
479 |
application. See Section~\ref{sec:combinators}.}
|
10
|
480 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
481 |
@{ML_response_fake [display,gray]
|
42
|
482 |
"let
|
10
|
483 |
val thy = @{theory}
|
|
484 |
|
42
|
485 |
val assm1 = cterm_of thy @{prop \"\<And>(x::nat). P x \<Longrightarrow> Q x\"}
|
49
|
486 |
val assm2 = cterm_of thy @{prop \"(P::nat\<Rightarrow>bool) t\"}
|
10
|
487 |
|
|
488 |
val Pt_implies_Qt =
|
|
489 |
assume assm1
|
42
|
490 |
|> forall_elim (cterm_of thy @{term \"t::nat\"});
|
10
|
491 |
|
|
492 |
val Qt = implies_elim Pt_implies_Qt (assume assm2);
|
|
493 |
in
|
|
494 |
Qt
|
|
495 |
|> implies_intr assm2
|
|
496 |
|> implies_intr assm1
|
48
|
497 |
end" "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
|
12
|
498 |
|
21
|
499 |
This code-snippet constructs the following proof:
|
|
500 |
|
|
501 |
\[
|
|
502 |
\infer[(@{text "\<Longrightarrow>"}$-$intro)]{\vdash @{prop "(\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> P t \<Longrightarrow> Q t"}}
|
|
503 |
{\infer[(@{text "\<Longrightarrow>"}$-$intro)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}
|
|
504 |
{\infer[(@{text "\<Longrightarrow>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"}, @{prop "P t"} \vdash @{prop "Q t"}}
|
|
505 |
{\infer[(@{text "\<And>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}
|
|
506 |
{\infer[(assume)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "\<And>x. P x \<Longrightarrow> Q x"}}{}}
|
|
507 |
&
|
|
508 |
\infer[(assume)]{@{prop "P t"} \vdash @{prop "P t"}}{}
|
|
509 |
}
|
|
510 |
}
|
|
511 |
}
|
|
512 |
\]
|
|
513 |
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
514 |
However, while we obtained a theorem as result, this theorem is not
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
515 |
yet stored in Isabelle's theorem database. So it cannot be referenced later
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
516 |
on. How to store theorems will be explained in the next section.
|
21
|
517 |
|
13
|
518 |
\begin{readmore}
|
50
|
519 |
For the functions @{text "assume"}, @{text "forall_elim"} etc
|
13
|
520 |
see \isccite{sec:thms}. The basic functions for theorems are defined in
|
|
521 |
@{ML_file "Pure/thm.ML"}.
|
|
522 |
\end{readmore}
|
12
|
523 |
|
10
|
524 |
*}
|
|
525 |
|
20
|
526 |
section {* Storing Theorems *}
|
|
527 |
|
|
528 |
section {* Theorem Attributes *}
|
|
529 |
|
104
|
530 |
section {* Printing Terms and Theorems\label{sec:printing} *}
|
100
|
531 |
|
|
532 |
text {*
|
107
|
533 |
During development, you often want to inspect date of type @{ML_type term}, @{ML_type cterm}
|
|
534 |
or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing them,
|
104
|
535 |
but for quick-and-dirty solutions they are far too unwieldy. A simple way to transform
|
101
|
536 |
a term into a string is to use the function @{ML Syntax.string_of_term}.
|
100
|
537 |
|
|
538 |
@{ML_response_fake [display,gray]
|
|
539 |
"Syntax.string_of_term @{context} @{term \"1::nat\"}"
|
|
540 |
"\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}
|
|
541 |
|
104
|
542 |
This produces a string with some printing directions encoded in it. The string
|
107
|
543 |
can be properly printed by using the function @{ML warning}.
|
100
|
544 |
|
|
545 |
@{ML_response_fake [display,gray]
|
|
546 |
"warning (Syntax.string_of_term @{context} @{term \"1::nat\"})"
|
|
547 |
"\"1\""}
|
|
548 |
|
101
|
549 |
A @{ML_type cterm} can be transformed into a string by the following function.
|
100
|
550 |
*}
|
|
551 |
|
|
552 |
ML{*fun str_of_cterm ctxt t =
|
|
553 |
Syntax.string_of_term ctxt (term_of t)*}
|
|
554 |
|
|
555 |
text {*
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
556 |
If there are more than one @{ML_type cterm}s to be printed, you can use the
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
557 |
function @{ML commas} to separate them.
|
100
|
558 |
*}
|
|
559 |
|
|
560 |
ML{*fun str_of_cterms ctxt ts =
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
561 |
commas (map (str_of_cterm ctxt) ts)*}
|
100
|
562 |
|
|
563 |
text {*
|
101
|
564 |
The easiest way to get the string of a theorem is to transform it
|
100
|
565 |
into a @{ML_type cterm} using the function @{ML crep_thm}.
|
|
566 |
*}
|
|
567 |
|
|
568 |
ML{*fun str_of_thm ctxt thm =
|
|
569 |
let
|
|
570 |
val {prop, ...} = crep_thm thm
|
|
571 |
in
|
|
572 |
str_of_cterm ctxt prop
|
|
573 |
end*}
|
|
574 |
|
|
575 |
text {*
|
101
|
576 |
Again the function @{ML commas} helps with printing more than one theorem.
|
100
|
577 |
*}
|
|
578 |
|
|
579 |
ML{*fun str_of_thms ctxt thms =
|
|
580 |
commas (map (str_of_thm ctxt) thms)*}
|
|
581 |
|
|
582 |
|
75
|
583 |
section {* Operations on Constants (Names) *}
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
584 |
|
68
|
585 |
text {*
|
78
|
586 |
|
|
587 |
@{ML_response [display] "Sign.base_name \"List.list.Nil\"" "\"Nil\""}
|
86
|
588 |
|
92
|
589 |
authentic syntax?
|
|
590 |
|
|
591 |
*}
|
|
592 |
|
|
593 |
ML {* @{const_name lfp} *}
|
|
594 |
|
|
595 |
text {*
|
|
596 |
constants in case-patterns?
|
|
597 |
|
|
598 |
In the meantime, lfp has been moved to the Inductive theory, so it is
|
|
599 |
no longer called Lfp.lfp. If a @{text "@{const_name}"} antiquotation had been
|
|
600 |
used, we would have gotten an error for this. Another advantage of the
|
|
601 |
antiquotation is that we can then just write @{text "@{const_name lfp}"} rather
|
|
602 |
than @{text "@{const_name Lfp.lfp}"} or whatever, and it expands to the correct
|
|
603 |
name.
|
78
|
604 |
|
75
|
605 |
*}
|
|
606 |
|
|
607 |
section {* Combinators\label{sec:combinators} *}
|
|
608 |
|
|
609 |
text {*
|
82
|
610 |
For beginners, perhaps the most puzzling parts in the existing code of Isabelle are
|
|
611 |
the combinators. At first they seem to greatly obstruct the
|
|
612 |
comprehension of the code, but after getting familiar with them, they
|
|
613 |
actually ease the understanding and also the programming.
|
73
bcbcf5c839ae
used newly exported break reference in ThyOutput for writing separate output_list function
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
614 |
|
bcbcf5c839ae
used newly exported break reference in ThyOutput for writing separate output_list function
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
615 |
\begin{readmore}
|
75
|
616 |
The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}
|
87
|
617 |
and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans}
|
104
|
618 |
contains further information about combinators.
|
73
bcbcf5c839ae
used newly exported break reference in ThyOutput for writing separate output_list function
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
619 |
\end{readmore}
|
bcbcf5c839ae
used newly exported break reference in ThyOutput for writing separate output_list function
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
620 |
|
104
|
621 |
The simplest combinator is @{ML I}, which is just the identity function defined as
|
73
bcbcf5c839ae
used newly exported break reference in ThyOutput for writing separate output_list function
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
622 |
*}
|
bcbcf5c839ae
used newly exported break reference in ThyOutput for writing separate output_list function
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
623 |
|
bcbcf5c839ae
used newly exported break reference in ThyOutput for writing separate output_list function
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
624 |
ML{*fun I x = x*}
|
bcbcf5c839ae
used newly exported break reference in ThyOutput for writing separate output_list function
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
625 |
|
82
|
626 |
text {* Another simple combinator is @{ML K}, defined as *}
|
75
|
627 |
|
|
628 |
ML{*fun K x = fn _ => x*}
|
|
629 |
|
73
bcbcf5c839ae
used newly exported break reference in ThyOutput for writing separate output_list function
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
630 |
text {*
|
84
|
631 |
@{ML K} ``wraps'' a function around the argument @{text "x"}. However, this
|
101
|
632 |
function ignores its argument. As a result, @{ML K} defines a constant function
|
104
|
633 |
always returning @{text x}.
|
73
bcbcf5c839ae
used newly exported break reference in ThyOutput for writing separate output_list function
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
634 |
|
101
|
635 |
The next combinator is reverse application, @{ML "|>"}, defined as:
|
68
|
636 |
*}
|
2
|
637 |
|
75
|
638 |
ML{*fun x |> f = f x*}
|
|
639 |
|
81
|
640 |
text {* While just syntactic sugar for the usual function application,
|
|
641 |
the purpose of this combinator is to implement functions in a
|
78
|
642 |
``waterfall fashion''. Consider for example the function *}
|
|
643 |
|
|
644 |
ML %linenumbers{*fun inc_by_five x =
|
|
645 |
x |> (fn x => x + 1)
|
|
646 |
|> (fn x => (x, x))
|
|
647 |
|> fst
|
|
648 |
|> (fn x => x + 4)*}
|
|
649 |
|
|
650 |
text {*
|
104
|
651 |
which increments its argument @{text x} by 5. It does this by first incrementing
|
78
|
652 |
the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking
|
|
653 |
the first component of the pair (Line 4) and finally incrementing the first
|
|
654 |
component by 4 (Line 5). This kind of cascading manipulations of values is quite
|
81
|
655 |
common when dealing with theories (for example by adding a definition, followed by
|
101
|
656 |
lemmas and so on). The reverse application allows you to read what happens in
|
|
657 |
a top-down manner. This kind of coding should also be familiar,
|
100
|
658 |
if you used Haskell's do-notation. Writing the function @{ML inc_by_five} using
|
|
659 |
the reverse application is much clearer than writing
|
78
|
660 |
*}
|
|
661 |
|
|
662 |
ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*}
|
|
663 |
|
|
664 |
text {* or *}
|
|
665 |
|
|
666 |
ML{*fun inc_by_five x =
|
|
667 |
((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x*}
|
|
668 |
|
81
|
669 |
text {* and typographically more economical than *}
|
78
|
670 |
|
|
671 |
ML{*fun inc_by_five x =
|
|
672 |
let val y1 = x + 1
|
|
673 |
val y2 = (y1, y1)
|
|
674 |
val y3 = fst y2
|
|
675 |
val y4 = y3 + 4
|
|
676 |
in y4 end*}
|
|
677 |
|
|
678 |
text {*
|
82
|
679 |
Another reason why the let-bindings in the code above are better to be
|
84
|
680 |
avoided: it is more than easy to get the intermediate values wrong, not to
|
|
681 |
mention the nightmares the maintenance of this code causes!
|
82
|
682 |
|
|
683 |
|
81
|
684 |
(FIXME: give a real world example involving theories)
|
|
685 |
|
82
|
686 |
Similarly, the combinator @{ML "#>"} is the reverse function
|
86
|
687 |
composition. It can be used to define the following function
|
78
|
688 |
*}
|
|
689 |
|
|
690 |
ML{*val inc_by_six =
|
|
691 |
(fn x => x + 1)
|
|
692 |
#> (fn x => x + 2)
|
|
693 |
#> (fn x => x + 3)*}
|
|
694 |
|
|
695 |
text {*
|
|
696 |
which is the function composed of first the increment-by-one function and then
|
84
|
697 |
increment-by-two, followed by increment-by-three. Again, the reverse function
|
|
698 |
composition allows one to read the code top-down.
|
78
|
699 |
|
82
|
700 |
The remaining combinators described in this section add convenience for the
|
|
701 |
``waterfall method'' of writing functions. The combinator @{ML tap} allows
|
|
702 |
one to get hold of an intermediate result (to do some side-calculations for
|
|
703 |
instance). The function
|
78
|
704 |
|
82
|
705 |
*}
|
|
706 |
|
|
707 |
ML %linenumbers{*fun inc_by_three x =
|
78
|
708 |
x |> (fn x => x + 1)
|
|
709 |
|> tap (fn x => tracing (makestring x))
|
|
710 |
|> (fn x => x + 2)*}
|
|
711 |
|
84
|
712 |
text {* increments the argument first by one and then by two. In the middle (Line 3),
|
81
|
713 |
however, it uses @{ML tap} for printing the ``plus-one'' intermediate
|
84
|
714 |
result inside the tracing buffer. The function @{ML tap} can only
|
82
|
715 |
be used for side-calculations, because any value that is computed cannot
|
100
|
716 |
be merged back into the ``main waterfall''. To do this, you can use the next
|
|
717 |
combinator.
|
78
|
718 |
|
82
|
719 |
The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value
|
|
720 |
and returns the result together with the value (as a pair). For example
|
|
721 |
the function
|
78
|
722 |
*}
|
|
723 |
|
|
724 |
ML{*fun inc_as_pair x =
|
|
725 |
x |> `(fn x => x + 1)
|
|
726 |
|> (fn (x, y) => (x, y + 1))*}
|
|
727 |
|
|
728 |
text {*
|
100
|
729 |
takes @{text x} as argument, and then increments @{text x}, but also keeps
|
|
730 |
@{text x}. The intermediate result is therefore the pair @{ML "(x + 1, x)"
|
|
731 |
for x}. After that, the function increments the right-hand component of the
|
|
732 |
pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}.
|
82
|
733 |
|
|
734 |
The combinators @{ML "|>>"} and @{ML "||>"} are defined for
|
78
|
735 |
functions manipulating pairs. The first applies the function to
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
736 |
the first component of the pair, defined as
|
78
|
737 |
*}
|
|
738 |
|
|
739 |
ML{*fun (x, y) |>> f = (f x, y)*}
|
|
740 |
|
|
741 |
text {*
|
81
|
742 |
and the second combinator to the second component, defined as
|
78
|
743 |
*}
|
|
744 |
|
|
745 |
ML{*fun (x, y) ||> f = (x, f y)*}
|
|
746 |
|
81
|
747 |
text {*
|
82
|
748 |
With the combinator @{ML "|->"} you can re-combine the elements from a pair.
|
|
749 |
This combinator is defined as
|
|
750 |
*}
|
|
751 |
|
|
752 |
ML{*fun (x, y) |-> f = f x y*}
|
|
753 |
|
107
|
754 |
text {* and can be used to write the following roundabout version
|
|
755 |
of the @{text double} function
|
|
756 |
*}
|
82
|
757 |
|
|
758 |
ML{*fun double x =
|
|
759 |
x |> (fn x => (x, x))
|
|
760 |
|-> (fn x => fn y => x + y)*}
|
|
761 |
|
|
762 |
text {*
|
86
|
763 |
Recall that @{ML "|>"} is the reverse function applications. Recall also that the related
|
|
764 |
reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"},
|
82
|
765 |
@{ML "|>>"} and @{ML "||>"} described above have related combinators for function
|
86
|
766 |
composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "#->"},
|
|
767 |
for example, the function @{text double} can also be written as
|
82
|
768 |
*}
|
|
769 |
|
|
770 |
ML{*val double =
|
|
771 |
(fn x => (x, x))
|
|
772 |
#-> (fn x => fn y => x + y)*}
|
|
773 |
|
|
774 |
text {*
|
|
775 |
|
81
|
776 |
(FIXME: find a good exercise for combinators)
|
|
777 |
*}
|
78
|
778 |
|
89
|
779 |
|
|
780 |
(*<*)
|
|
781 |
setup {*
|
|
782 |
Sign.add_consts_i [("bar", @{typ "nat"},NoSyn)]
|
|
783 |
*}
|
|
784 |
|
|
785 |
lemma "bar = (1::nat)"
|
|
786 |
oops
|
|
787 |
|
|
788 |
setup {*
|
|
789 |
Sign.add_consts_i [("foo", @{typ "nat"},NoSyn)]
|
|
790 |
#> PureThy.add_defs false [((Binding.name "foo_def",
|
|
791 |
Logic.mk_equals (Const ("FirstSteps.foo", @{typ "nat"}), @{term "1::nat"})), [])]
|
|
792 |
#> snd
|
|
793 |
*}
|
|
794 |
|
|
795 |
lemma "foo = (1::nat)"
|
|
796 |
apply(simp add: foo_def)
|
|
797 |
done
|
|
798 |
|
|
799 |
thm foo_def
|
|
800 |
(*>*)
|
|
801 |
|
92
|
802 |
section {* Misc *}
|
|
803 |
|
|
804 |
ML {*DatatypePackage.get_datatype @{theory} "List.list"*}
|
|
805 |
|
2
|
806 |
end |