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
|
50
|
10 |
in Isabelle is part of a theory. If you want to follow the code written 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
|
49
|
29 |
by using the \isacommand{ML}-command. For example\smallskip
|
2
|
30 |
|
75
|
31 |
\begin{isabelle}
|
|
32 |
\begin{graybox}
|
42
|
33 |
\isa{\isacommand{ML}
|
|
34 |
\isacharverbatimopen\isanewline
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
35 |
\hspace{5mm}@{ML "3 + 4"}\isanewline
|
42
|
36 |
\isacharverbatimclose\isanewline
|
58
|
37 |
@{text "> 7"}\smallskip}
|
75
|
38 |
\end{graybox}
|
|
39 |
\end{isabelle}
|
2
|
40 |
|
75
|
41 |
Like ``normal'' Isabelle proof scripts,
|
58
|
42 |
\isacommand{ML}-commands can be evaluated by using the advance and undo buttons of
|
49
|
43 |
your Isabelle environment. The code inside the \isacommand{ML}-command
|
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
44 |
can also contain value and function bindings, and even those can be
|
75
|
45 |
undone when the proof script is retracted. As mentioned earlier, we will
|
|
46 |
drop the \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose}
|
58
|
47 |
whenever we show code and its response.
|
10
|
48 |
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
49 |
Once a portion of code is relatively stable, one usually wants to
|
15
|
50 |
export it to a separate ML-file. Such files can then be included in a
|
|
51 |
theory by using \isacommand{uses} 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
|
75
|
78 |
converting values into strings, namely using 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
|
|
83 |
and is 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
|
49
|
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
|
65
|
94 |
printed to a separate file, e.g. to prevent ProofGeneral from choking on massive
|
52
|
95 |
amounts of trace output. This redirection can be achieved using 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 |
|
|
115 |
Error messages can be printed using the function @{ML error} as in
|
|
116 |
|
|
117 |
@{ML_response_fake [display,gray] "if 0=1 then 1 else (error \"foo\")" "\"foo\""}
|
|
118 |
|
15
|
119 |
*}
|
|
120 |
|
10
|
121 |
|
75
|
122 |
|
|
123 |
|
2
|
124 |
section {* Antiquotations *}
|
|
125 |
|
|
126 |
text {*
|
49
|
127 |
The main advantage of embedding all code in a theory is that the code can
|
58
|
128 |
contain references to entities defined on the logical level of Isabelle. By
|
|
129 |
this we mean definitions, theorems, terms and so on. This kind of reference is
|
|
130 |
realised with antiquotations. For example, one can print out the name of the current
|
49
|
131 |
theory by typing
|
|
132 |
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
133 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
134 |
@{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
|
135 |
|
5
|
136 |
where @{text "@{theory}"} is an antiquotation that is substituted with the
|
49
|
137 |
current theory (remember that we assumed we are inside the theory
|
58
|
138 |
@{text FirstSteps}). The name of this theory can be extracted with
|
49
|
139 |
the function @{ML "Context.theory_name"}.
|
5
|
140 |
|
10
|
141 |
Note, however, that antiquotations are statically scoped, that is the value is
|
12
|
142 |
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
|
143 |
*}
|
5
|
144 |
|
69
|
145 |
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
|
146 |
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
147 |
text {*
|
2
|
148 |
|
58
|
149 |
does, as its name suggest, \emph{not} return the name of the current theory, if it is run in a
|
5
|
150 |
different theory. Instead, the code above defines the constant function
|
58
|
151 |
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
|
152 |
function is called. Operationally speaking, the antiquotation @{text "@{theory}"} is
|
5
|
153 |
\emph{not} replaced with code that will look up the current theory in
|
|
154 |
some data structure and return it. Instead, it is literally
|
|
155 |
replaced with the value representing the theory name.
|
2
|
156 |
|
75
|
157 |
In a similar way you can use antiquotations to refer to theorems:
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
158 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
159 |
@{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
|
75
|
160 |
|
|
161 |
or simpsets:
|
|
162 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
163 |
@{ML_response_fake [display,gray]
|
70
|
164 |
"let
|
|
165 |
val ({rules,...},_) = MetaSimplifier.rep_ss @{simpset}
|
|
166 |
in
|
|
167 |
map #name (Net.entries rules)
|
|
168 |
end" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
|
54
|
169 |
|
75
|
170 |
The code above extracts the theorem names that are stored in a simpset.
|
|
171 |
We refer to the current simpset with the antiquotation @{text "@{simpset}"}.
|
|
172 |
The function @{ML rep_ss in MetaSimplifier} returns a record
|
|
173 |
containing all information about the simpset. The rules of a simpset are stored
|
71
|
174 |
in a discrimination net (a datastructure for fast indexing). From this net
|
|
175 |
we can extract the entries using the function @{ML Net.entries}.
|
10
|
176 |
|
75
|
177 |
\begin{readmore}
|
|
178 |
The infrastructure for simpsets is implemented in @{ML_file "Pure/meta_simplifier.ML"}
|
|
179 |
and @{ML_file "Pure/simplifier.ML"}.
|
|
180 |
\end{readmore}
|
|
181 |
|
|
182 |
While antiquotations have many applications, they were originally introduced in order
|
|
183 |
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
|
184 |
*}
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
185 |
|
69
|
186 |
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
|
187 |
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
188 |
text {*
|
75
|
189 |
These bindings were difficult to maintain and also could be accidentally
|
|
190 |
overwritten by the user. This usually broke definitional
|
49
|
191 |
packages. Antiquotations solve this problem, since they are ``linked''
|
75
|
192 |
statically at compile-time. However, this static linkage also limits their
|
|
193 |
usefulness in cases where data needs to be build up dynamically. In the course of
|
|
194 |
this introduction, we will learn more about
|
49
|
195 |
these antiquotations: they greatly simplify Isabelle programming since one
|
|
196 |
can directly access all kinds of logical elements from ML.
|
|
197 |
|
2
|
198 |
*}
|
|
199 |
|
15
|
200 |
section {* Terms and Types *}
|
2
|
201 |
|
|
202 |
text {*
|
49
|
203 |
One way to construct terms of Isabelle on the ML-level is by using the antiquotation
|
|
204 |
\mbox{@{text "@{term \<dots>}"}}. For example
|
2
|
205 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
206 |
@{ML_response [display,gray]
|
75
|
207 |
"@{term \"(a::nat) + b = c\"}"
|
|
208 |
"Const (\"op =\", \<dots>) $
|
|
209 |
(Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
|
2
|
210 |
|
50
|
211 |
This will show the term @{term "(a::nat) + b = c"}, but printed using the internal
|
13
|
212 |
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
|
213 |
datatype @{ML_type "term"}.
|
2
|
214 |
|
34
|
215 |
The internal representation of terms uses the usual de Bruijn index mechanism where bound
|
11
|
216 |
variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to
|
10
|
217 |
the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that
|
12
|
218 |
binds the corresponding variable. However, in Isabelle the names of bound variables are
|
11
|
219 |
kept at abstractions for printing purposes, and so should be treated only as comments.
|
10
|
220 |
|
2
|
221 |
\begin{readmore}
|
13
|
222 |
Terms are described in detail in \isccite{sec:terms}. Their
|
2
|
223 |
definition and many useful operations can be found in @{ML_file "Pure/term.ML"}.
|
|
224 |
\end{readmore}
|
|
225 |
|
13
|
226 |
Sometimes the internal representation of terms can be surprisingly different
|
12
|
227 |
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
|
228 |
parsing/type-checking/pretty printing can be quite elaborate.
|
2
|
229 |
|
10
|
230 |
\begin{exercise}
|
2
|
231 |
Look at the internal term representation of the following terms, and
|
|
232 |
find out why they are represented like this.
|
|
233 |
|
|
234 |
\begin{itemize}
|
|
235 |
\item @{term "case x of 0 \<Rightarrow> 0 | Suc y \<Rightarrow> y"}
|
|
236 |
\item @{term "\<lambda>(x,y). P y x"}
|
|
237 |
\item @{term "{ [x::int] | x. x \<le> -2 }"}
|
|
238 |
\end{itemize}
|
|
239 |
|
|
240 |
Hint: The third term is already quite big, and the pretty printer
|
|
241 |
may omit parts of it by default. If you want to see all of it, you
|
52
|
242 |
can use the following ML function to set the limit to a value high
|
13
|
243 |
enough:
|
12
|
244 |
|
75
|
245 |
@{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
|
246 |
\end{exercise}
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
247 |
|
13
|
248 |
The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type,
|
50
|
249 |
inserting the invisible @{text "Trueprop"}-coercions whenever necessary.
|
68
|
250 |
Consider for example the pairs
|
12
|
251 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
252 |
@{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),
|
65
|
253 |
Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
|
|
254 |
|
68
|
255 |
where an coercion is inserted in the second component and
|
12
|
256 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
257 |
@{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})"
|
65
|
258 |
"(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}
|
12
|
259 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
260 |
where it is not (since it is already constructed by a meta-implication).
|
19
|
261 |
|
|
262 |
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
|
263 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
264 |
@{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
|
265 |
|
19
|
266 |
\begin{readmore}
|
|
267 |
Types are described in detail in \isccite{sec:types}. Their
|
54
|
268 |
definition and many useful operations can also be found in @{ML_file "Pure/type.ML"}.
|
19
|
269 |
\end{readmore}
|
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
270 |
*}
|
19
|
271 |
|
|
272 |
|
15
|
273 |
section {* Constructing Terms and Types Manually *}
|
12
|
274 |
|
|
275 |
text {*
|
|
276 |
|
19
|
277 |
While antiquotations are very convenient for constructing terms and types,
|
65
|
278 |
they can only construct fixed terms (remember they are ``linked'' at compile-time).
|
|
279 |
However, one often needs to construct terms
|
13
|
280 |
dynamically. For example, a function that returns the implication
|
52
|
281 |
@{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the type @{term "\<tau>"}
|
19
|
282 |
as arguments can only be written 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
|
283 |
*}
|
12
|
284 |
|
69
|
285 |
ML{*fun make_imp P Q tau =
|
12
|
286 |
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
|
287 |
val x = Free ("x",tau)
|
75
|
288 |
in
|
|
289 |
Logic.all x (Logic.mk_implies (P $ x, Q $ x))
|
69
|
290 |
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
|
291 |
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
292 |
text {*
|
12
|
293 |
|
19
|
294 |
The reason is that one cannot pass the arguments @{term P}, @{term Q} and
|
65
|
295 |
@{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
|
296 |
*}
|
13
|
297 |
|
69
|
298 |
ML{*fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} *}
|
12
|
299 |
|
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
300 |
text {*
|
19
|
301 |
To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"}
|
75
|
302 |
to both functions. With @{ML make_imp} we obtain the intended term involving
|
68
|
303 |
@{term "S"}, @{text "T"} and @{text "@{typ nat}"}
|
65
|
304 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
305 |
@{ML_response [display,gray] "make_imp @{term S} @{term T} @{typ nat}"
|
65
|
306 |
"Const \<dots> $
|
|
307 |
Abs (\"x\", Type (\"nat\",[]),
|
|
308 |
Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $
|
|
309 |
(Free (\"T\",\<dots>) $ \<dots>))"}
|
68
|
310 |
|
75
|
311 |
With @{ML make_wrong_imp} we obtain a term involving the @{term "P"}
|
68
|
312 |
and @{text "Q"} from the antiquotation.
|
|
313 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
314 |
@{ML_response [display,gray] "make_wrong_imp @{term S} @{term T} @{typ nat}"
|
65
|
315 |
"Const \<dots> $
|
|
316 |
Abs (\"x\", \<dots>,
|
|
317 |
Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $
|
|
318 |
(Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
|
|
319 |
|
68
|
320 |
One tricky point in constructing terms by hand is to obtain the fully
|
|
321 |
qualified name for constants. For example the names for @{text "zero"} and
|
|
322 |
@{text "+"} are more complex than one first expects, namely
|
19
|
323 |
|
15
|
324 |
|
|
325 |
\begin{center}
|
58
|
326 |
@{text "HOL.zero_class.zero"} and @{text "HOL.plus_class.plus"}.
|
15
|
327 |
\end{center}
|
|
328 |
|
68
|
329 |
The extra prefixes @{text zero_class} and @{text plus_class} are present
|
|
330 |
because these constants are defined within type classes; the prefix @{text
|
|
331 |
"HOL"} indicates in which theory they are defined. Guessing such internal
|
|
332 |
names can sometimes be quite hard. Therefore Isabelle provides the
|
|
333 |
antiquotation @{text "@{const_name \<dots>}"} which does the expansion
|
|
334 |
automatically, for example:
|
49
|
335 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
336 |
@{ML_response_fake [display,gray] "@{const_name \"Nil\"}" "List.list.Nil"}
|
10
|
337 |
|
19
|
338 |
(FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
|
11
|
339 |
|
75
|
340 |
Similarly, types can be constructed manually. For example a function type
|
|
341 |
can be constructed as follows:
|
49
|
342 |
|
|
343 |
*}
|
|
344 |
|
69
|
345 |
ML{*fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2]) *}
|
49
|
346 |
|
75
|
347 |
text {* This can be equally written as *}
|
49
|
348 |
|
69
|
349 |
ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *}
|
49
|
350 |
|
|
351 |
text {*
|
20
|
352 |
|
13
|
353 |
\begin{readmore}
|
|
354 |
There are many functions in @{ML_file "Pure/logic.ML"} and
|
12
|
355 |
@{ML_file "HOL/hologic.ML"} that make such manual constructions of terms
|
49
|
356 |
and types easier.\end{readmore}
|
13
|
357 |
|
|
358 |
Have a look at these files and try to solve the following two exercises:
|
11
|
359 |
|
|
360 |
*}
|
|
361 |
|
|
362 |
text {*
|
|
363 |
|
13
|
364 |
\begin{exercise}\label{fun:revsum}
|
58
|
365 |
Write a function @{text "rev_sum : term -> term"} that takes a
|
11
|
366 |
term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "i"} might be zero)
|
|
367 |
and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume
|
|
368 |
the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"}
|
13
|
369 |
associates to the left. Try your function on some examples.
|
11
|
370 |
\end{exercise}
|
|
371 |
|
15
|
372 |
\begin{exercise}\label{fun:makesum}
|
11
|
373 |
Write a function which takes two terms representing natural numbers
|
75
|
374 |
in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produce the
|
11
|
375 |
number representing their sum.
|
|
376 |
\end{exercise}
|
|
377 |
|
|
378 |
*}
|
|
379 |
|
49
|
380 |
section {* Type-Checking *}
|
10
|
381 |
|
|
382 |
text {*
|
13
|
383 |
|
10
|
384 |
We can freely construct and manipulate terms, since they are just
|
|
385 |
arbitrary unchecked trees. However, we eventually want to see if a
|
54
|
386 |
term is well-formed, or type-checks, relative to a theory.
|
50
|
387 |
Type-checking is done via the function @{ML cterm_of}, which converts
|
10
|
388 |
a @{ML_type term} into a @{ML_type cterm}, a \emph{certified} term.
|
|
389 |
Unlike @{ML_type term}s, which are just trees, @{ML_type
|
|
390 |
"cterm"}s are abstract objects that are guaranteed to be
|
50
|
391 |
type-correct, and that can only be constructed via the ``official
|
|
392 |
interfaces''.
|
2
|
393 |
|
54
|
394 |
Type-checking is always relative to a theory context. For now we use
|
10
|
395 |
the @{ML "@{theory}"} antiquotation to get hold of the current theory.
|
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
396 |
For example we can write
|
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
397 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
398 |
@{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
|
399 |
|
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
400 |
or use the antiquotation
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
401 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
402 |
@{ML_response_fake [display,gray] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"}
|
10
|
403 |
|
54
|
404 |
Attempting
|
|
405 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
406 |
@{ML_response_fake_both [display,gray] "@{cterm \"1 + True\"}" "Type unification failed \<dots>"}
|
54
|
407 |
|
|
408 |
yields an error. A slightly more elaborate example is
|
20
|
409 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
410 |
@{ML_response_fake [display,gray]
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
411 |
"let
|
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
412 |
val natT = @{typ \"nat\"}
|
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
413 |
val zero = @{term \"0::nat\"}
|
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
414 |
in
|
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
415 |
cterm_of @{theory}
|
75
|
416 |
(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
|
417 |
end" "0 + 0"}
|
12
|
418 |
|
13
|
419 |
\begin{exercise}
|
|
420 |
Check that the function defined in Exercise~\ref{fun:revsum} returns a
|
50
|
421 |
result that type-checks.
|
13
|
422 |
\end{exercise}
|
|
423 |
|
|
424 |
*}
|
|
425 |
|
2
|
426 |
section {* Theorems *}
|
|
427 |
|
|
428 |
text {*
|
50
|
429 |
Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm}
|
75
|
430 |
that can only be built by going through interfaces. As a consequence of this is that
|
|
431 |
every proof is correct by construction (FIXME reference LCF-philosophy)
|
2
|
432 |
|
13
|
433 |
To see theorems in ``action'', let us give a proof for the following statement
|
10
|
434 |
*}
|
|
435 |
|
|
436 |
lemma
|
|
437 |
assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x"
|
|
438 |
and assm\<^isub>2: "P t"
|
13
|
439 |
shows "Q t" (*<*)oops(*>*)
|
10
|
440 |
|
|
441 |
text {*
|
49
|
442 |
on the ML-level:\footnote{Note that @{text "|>"} is reverse
|
75
|
443 |
application. See Section~\ref{sec:combinators}.}
|
10
|
444 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
445 |
@{ML_response_fake [display,gray]
|
42
|
446 |
"let
|
10
|
447 |
val thy = @{theory}
|
|
448 |
|
42
|
449 |
val assm1 = cterm_of thy @{prop \"\<And>(x::nat). P x \<Longrightarrow> Q x\"}
|
49
|
450 |
val assm2 = cterm_of thy @{prop \"(P::nat\<Rightarrow>bool) t\"}
|
10
|
451 |
|
|
452 |
val Pt_implies_Qt =
|
|
453 |
assume assm1
|
42
|
454 |
|> forall_elim (cterm_of thy @{term \"t::nat\"});
|
10
|
455 |
|
|
456 |
val Qt = implies_elim Pt_implies_Qt (assume assm2);
|
|
457 |
in
|
|
458 |
|
|
459 |
Qt
|
|
460 |
|> implies_intr assm2
|
|
461 |
|> implies_intr assm1
|
48
|
462 |
end" "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
|
12
|
463 |
|
21
|
464 |
This code-snippet constructs the following proof:
|
|
465 |
|
|
466 |
\[
|
|
467 |
\infer[(@{text "\<Longrightarrow>"}$-$intro)]{\vdash @{prop "(\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> P t \<Longrightarrow> Q t"}}
|
|
468 |
{\infer[(@{text "\<Longrightarrow>"}$-$intro)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}
|
|
469 |
{\infer[(@{text "\<Longrightarrow>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"}, @{prop "P t"} \vdash @{prop "Q t"}}
|
|
470 |
{\infer[(@{text "\<And>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}
|
|
471 |
{\infer[(assume)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "\<And>x. P x \<Longrightarrow> Q x"}}{}}
|
|
472 |
&
|
|
473 |
\infer[(assume)]{@{prop "P t"} \vdash @{prop "P t"}}{}
|
|
474 |
}
|
|
475 |
}
|
|
476 |
}
|
|
477 |
\]
|
|
478 |
|
|
479 |
|
13
|
480 |
\begin{readmore}
|
50
|
481 |
For the functions @{text "assume"}, @{text "forall_elim"} etc
|
13
|
482 |
see \isccite{sec:thms}. The basic functions for theorems are defined in
|
|
483 |
@{ML_file "Pure/thm.ML"}.
|
|
484 |
\end{readmore}
|
12
|
485 |
|
10
|
486 |
*}
|
|
487 |
|
20
|
488 |
section {* Storing Theorems *}
|
|
489 |
|
|
490 |
section {* Theorem Attributes *}
|
|
491 |
|
75
|
492 |
section {* Operations on Constants (Names) *}
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
493 |
|
68
|
494 |
text {*
|
75
|
495 |
(FIXME how can I extract the constant name without the theory name etc)
|
|
496 |
*}
|
|
497 |
|
|
498 |
section {* Combinators\label{sec:combinators} *}
|
|
499 |
|
|
500 |
text {*
|
|
501 |
Perhaps one of the most puzzling aspects for a beginner when reading at
|
73
bcbcf5c839ae
used newly exported break reference in ThyOutput for writing separate output_list function
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
502 |
existing Isabelle code is the liberal use of combinators. At first they
|
75
|
503 |
seem to obstruct the comprehension of the code, but after getting familiar
|
|
504 |
with them they actually ease the reading 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
|
505 |
|
bcbcf5c839ae
used newly exported break reference in ThyOutput for writing separate output_list function
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
506 |
\begin{readmore}
|
75
|
507 |
The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}
|
73
bcbcf5c839ae
used newly exported break reference in ThyOutput for writing separate output_list function
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
508 |
and @{ML_file "Pure/General/basics.ML"}.
|
bcbcf5c839ae
used newly exported break reference in ThyOutput for writing separate output_list function
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
509 |
\end{readmore}
|
bcbcf5c839ae
used newly exported break reference in ThyOutput for writing separate output_list function
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
510 |
|
bcbcf5c839ae
used newly exported break reference in ThyOutput for writing separate output_list function
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
511 |
The simplest combinator is @{ML I} which is just the identidy function.
|
bcbcf5c839ae
used newly exported break reference in ThyOutput for writing separate output_list function
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
512 |
*}
|
bcbcf5c839ae
used newly exported break reference in ThyOutput for writing separate output_list function
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
513 |
|
bcbcf5c839ae
used newly exported break reference in ThyOutput for writing separate output_list function
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
514 |
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
|
515 |
|
75
|
516 |
text {* Another frequently used combinator is @{ML K} *}
|
|
517 |
|
|
518 |
ML{*fun K x = fn _ => x*}
|
|
519 |
|
73
bcbcf5c839ae
used newly exported break reference in ThyOutput for writing separate output_list function
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
520 |
text {*
|
75
|
521 |
which ``wraps'' a function around the argument @{text "x"}. This function
|
|
522 |
ignores its argument.
|
73
bcbcf5c839ae
used newly exported break reference in ThyOutput for writing separate output_list function
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
523 |
|
75
|
524 |
@{ML "(op |>)"}
|
68
|
525 |
*}
|
2
|
526 |
|
75
|
527 |
ML{*fun x |> f = f x*}
|
|
528 |
|
2
|
529 |
end |