2
|
1 |
theory FirstSteps
|
25
|
2 |
imports Base
|
2
|
3 |
begin
|
|
4 |
|
|
5 |
|
|
6 |
chapter {* First Steps *}
|
|
7 |
|
42
|
8 |
text {*
|
|
9 |
|
54
|
10 |
Isabelle programming is done in ML. Just like lemmas and proofs, ML-code
|
50
|
11 |
in Isabelle is part of a theory. If you want to follow the code written in
|
54
|
12 |
this chapter, we assume you are working inside the theory starting with
|
2
|
13 |
|
6
|
14 |
\begin{center}
|
5
|
15 |
\begin{tabular}{@ {}l}
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
16 |
\isacommand{theory} FirstSteps\\
|
5
|
17 |
\isacommand{imports} Main\\
|
|
18 |
\isacommand{begin}\\
|
6
|
19 |
\ldots
|
5
|
20 |
\end{tabular}
|
6
|
21 |
\end{center}
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
22 |
*}
|
5
|
23 |
|
20
|
24 |
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
|
25 |
|
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
26 |
|
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
27 |
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
28 |
text {*
|
5
|
29 |
The easiest and quickest way to include code in a theory is
|
49
|
30 |
by using the \isacommand{ML}-command. For example\smallskip
|
2
|
31 |
|
42
|
32 |
\isa{\isacommand{ML}
|
|
33 |
\isacharverbatimopen\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
|
42
|
35 |
\isacharverbatimclose\isanewline
|
|
36 |
@{ML_text "> 7"}\smallskip}
|
2
|
37 |
|
49
|
38 |
Expressions inside \isacommand{ML}-commands are immediately evaluated,
|
6
|
39 |
like ``normal'' Isabelle proof scripts, by using the advance and undo buttons of
|
49
|
40 |
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
|
41 |
can also contain value and function bindings, and even those can be
|
49
|
42 |
undone when the proof script is retracted. In what follows we will drop the
|
42
|
43 |
\isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} whenever
|
40
|
44 |
we show code and its response.
|
10
|
45 |
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
46 |
Once a portion of code is relatively stable, one usually wants to
|
15
|
47 |
export it to a separate ML-file. Such files can then be included in a
|
|
48 |
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
|
49 |
|
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
50 |
\begin{center}
|
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
51 |
\begin{tabular}{@ {}l}
|
54
|
52 |
\isacommand{theory} FirstSteps\\
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
53 |
\isacommand{imports} Main\\
|
15
|
54 |
\isacommand{uses} @{ML_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
|
55 |
\isacommand{begin}\\
|
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
56 |
\ldots
|
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
57 |
\end{tabular}
|
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
58 |
\end{center}
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
59 |
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
60 |
*}
|
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
61 |
|
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
62 |
section {* Debugging and Printing *}
|
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 |
text {*
|
13
|
65 |
|
50
|
66 |
During development you might find it necessary to inspect some data
|
10
|
67 |
in your code. This can be done in a ``quick-and-dirty'' fashion using
|
12
|
68 |
the function @{ML "warning"}. For example
|
10
|
69 |
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
70 |
@{ML [display] "warning \"any string\""}
|
10
|
71 |
|
50
|
72 |
will print out @{ML_text [quotes] "any string"} inside the response buffer
|
|
73 |
of Isabelle. This function expects a string. If you develop under PolyML,
|
|
74 |
then there is a convenient, though again ``quick-and-dirty'', method for
|
|
75 |
converting values into strings, for example:
|
10
|
76 |
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
77 |
@{ML [display] "warning (makestring 1)"}
|
12
|
78 |
|
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
79 |
However this only works if the type of what is converted is monomorphic and is not
|
12
|
80 |
a function.
|
|
81 |
|
52
|
82 |
The function @{ML "warning"} should only be used for testing purposes, because any
|
|
83 |
output this function generates will be overwritten as soon as an error is
|
50
|
84 |
raised. For printing anything more serious and elaborate, the
|
54
|
85 |
function @{ML tracing} is more appropriate. This function writes all output into
|
49
|
86 |
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
|
87 |
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
88 |
@{ML [display] "tracing \"foo\""}
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
89 |
|
54
|
90 |
It is also possible to redirect the ``channel'' where the string @{ML_text "foo"} is
|
15
|
91 |
printed to a separate file, e.g. to prevent Proof General from choking on massive
|
52
|
92 |
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
|
93 |
*}
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
94 |
|
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
95 |
ML{*
|
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 |
val strip_specials =
|
42
|
97 |
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
|
98 |
fun strip ("\^A" :: _ :: cs) = strip cs
|
42
|
99 |
| strip (c :: cs) = c :: strip cs
|
|
100 |
| strip [] = [];
|
|
101 |
in implode o strip o explode end;
|
|
102 |
|
|
103 |
fun redirect_tracing stream =
|
|
104 |
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
|
105 |
(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
|
106 |
TextIO.output (stream, "\n");
|
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
107 |
TextIO.flushOut stream));
|
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 |
*}
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
109 |
|
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
110 |
text {*
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
111 |
|
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\")"}
|
15
|
113 |
will cause that all tracing information is printed into the file @{ML_text "foo.bar"}.
|
|
114 |
|
|
115 |
*}
|
|
116 |
|
10
|
117 |
|
2
|
118 |
section {* Antiquotations *}
|
|
119 |
|
|
120 |
text {*
|
49
|
121 |
The main advantage of embedding all code in a theory is that the code can
|
|
122 |
contain references to entities defined on the logical level of Isabelle (by
|
|
123 |
this we mean definitions, theorems, terms and so on). This is done using
|
|
124 |
antiquotations. For example, one can print out the name of the current
|
|
125 |
theory by typing
|
|
126 |
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
127 |
|
41
b11653b11bd3
further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
128 |
@{ML_response [display] "Context.theory_name @{theory}" "FirstSteps"}
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
129 |
|
5
|
130 |
where @{text "@{theory}"} is an antiquotation that is substituted with the
|
49
|
131 |
current theory (remember that we assumed we are inside the theory
|
|
132 |
@{ML_text FirstSteps}). The name of this theory can be extracted using
|
|
133 |
the function @{ML "Context.theory_name"}.
|
5
|
134 |
|
10
|
135 |
Note, however, that antiquotations are statically scoped, that is the value is
|
12
|
136 |
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
|
137 |
*}
|
5
|
138 |
|
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
139 |
ML {*
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
140 |
fun not_current_thyname () = Context.theory_name @{theory}
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
141 |
*}
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
142 |
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
143 |
text {*
|
2
|
144 |
|
5
|
145 |
does \emph{not} return the name of the current theory, if it is run in a
|
|
146 |
different theory. Instead, the code above defines the constant function
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
147 |
that always returns the string @{ML_text "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
|
148 |
function is called. Operationally speaking, the antiquotation @{text "@{theory}"} is
|
5
|
149 |
\emph{not} replaced with code that will look up the current theory in
|
|
150 |
some data structure and return it. Instead, it is literally
|
|
151 |
replaced with the value representing the theory name.
|
2
|
152 |
|
21
|
153 |
In a similar way you can use antiquotations to refer to theorems or simpsets:
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
154 |
|
54
|
155 |
@{ML_response_fake [display] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
|
|
156 |
@{ML_response_fake [display] "@{simpset}" "\<dots>"}
|
|
157 |
|
|
158 |
(FIXME: what does a simpset look like? It seems to be the same problem
|
|
159 |
like tokens.)
|
10
|
160 |
|
50
|
161 |
While antiquotations have many applications, they were originally introduced to
|
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
162 |
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
|
163 |
*}
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
164 |
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
165 |
ML {*
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
166 |
val allI = thm "allI"
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
167 |
*}
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
168 |
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
169 |
text {*
|
49
|
170 |
These bindings were difficult to maintain and also could be accidentally
|
|
171 |
overwritten by the user. This usually broke definitional
|
|
172 |
packages. Antiquotations solve this problem, since they are ``linked''
|
50
|
173 |
statically at compile-time. However, that also sometimes limits their
|
49
|
174 |
applicability. In the course of this introduction, we will learn more about
|
|
175 |
these antiquotations: they greatly simplify Isabelle programming since one
|
|
176 |
can directly access all kinds of logical elements from ML.
|
|
177 |
|
2
|
178 |
*}
|
|
179 |
|
15
|
180 |
section {* Terms and Types *}
|
2
|
181 |
|
|
182 |
text {*
|
49
|
183 |
One way to construct terms of Isabelle on the ML-level is by using the antiquotation
|
|
184 |
\mbox{@{text "@{term \<dots>}"}}. For example
|
2
|
185 |
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
186 |
@{ML_response [display] "@{term \"(a::nat) + b = c\"}"
|
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
187 |
"Const (\"op =\", \<dots>) $ (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
|
2
|
188 |
|
50
|
189 |
This will show the term @{term "(a::nat) + b = c"}, but printed using the internal
|
13
|
190 |
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
|
191 |
datatype @{ML_type "term"}.
|
2
|
192 |
|
34
|
193 |
The internal representation of terms uses the usual de Bruijn index mechanism where bound
|
11
|
194 |
variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to
|
10
|
195 |
the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that
|
12
|
196 |
binds the corresponding variable. However, in Isabelle the names of bound variables are
|
11
|
197 |
kept at abstractions for printing purposes, and so should be treated only as comments.
|
10
|
198 |
|
2
|
199 |
\begin{readmore}
|
13
|
200 |
Terms are described in detail in \isccite{sec:terms}. Their
|
2
|
201 |
definition and many useful operations can be found in @{ML_file "Pure/term.ML"}.
|
|
202 |
\end{readmore}
|
|
203 |
|
13
|
204 |
Sometimes the internal representation of terms can be surprisingly different
|
12
|
205 |
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
|
206 |
parsing/type-checking/pretty printing can be quite elaborate.
|
2
|
207 |
|
10
|
208 |
\begin{exercise}
|
2
|
209 |
Look at the internal term representation of the following terms, and
|
|
210 |
find out why they are represented like this.
|
|
211 |
|
|
212 |
\begin{itemize}
|
|
213 |
\item @{term "case x of 0 \<Rightarrow> 0 | Suc y \<Rightarrow> y"}
|
|
214 |
\item @{term "\<lambda>(x,y). P y x"}
|
|
215 |
\item @{term "{ [x::int] | x. x \<le> -2 }"}
|
|
216 |
\end{itemize}
|
|
217 |
|
|
218 |
Hint: The third term is already quite big, and the pretty printer
|
|
219 |
may omit parts of it by default. If you want to see all of it, you
|
52
|
220 |
can use the following ML function to set the limit to a value high
|
13
|
221 |
enough:
|
10
|
222 |
\end{exercise}
|
12
|
223 |
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
224 |
@{ML [display] "print_depth 50"}
|
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
225 |
|
13
|
226 |
The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type,
|
50
|
227 |
inserting the invisible @{text "Trueprop"}-coercions whenever necessary.
|
12
|
228 |
Consider for example
|
|
229 |
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
230 |
@{ML_response [display] "@{term \"P x\"}" "Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)"}
|
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
231 |
@{ML_response [display] "@{prop \"P x\"}"
|
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
232 |
"Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>))"}
|
12
|
233 |
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
234 |
which inserts the coercion in the latter case and
|
12
|
235 |
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
236 |
@{ML_response [display] "@{term \"P x \<Longrightarrow> Q x\"}" "Const (\"==>\", \<dots>) $ \<dots> $ \<dots>"}
|
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
237 |
@{ML_response [display] "@{prop \"P x \<Longrightarrow> Q x\"}" "Const (\"==>\", \<dots>) $ \<dots> $ \<dots>"}
|
12
|
238 |
|
50
|
239 |
which does not (since it is already constructed using the meta-implication).
|
19
|
240 |
|
|
241 |
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
|
242 |
|
42
|
243 |
@{ML_response_fake [display] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
244 |
|
19
|
245 |
\begin{readmore}
|
|
246 |
Types are described in detail in \isccite{sec:types}. Their
|
54
|
247 |
definition and many useful operations can also be found in @{ML_file "Pure/type.ML"}.
|
19
|
248 |
\end{readmore}
|
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
249 |
*}
|
19
|
250 |
|
|
251 |
|
15
|
252 |
section {* Constructing Terms and Types Manually *}
|
12
|
253 |
|
|
254 |
text {*
|
|
255 |
|
19
|
256 |
While antiquotations are very convenient for constructing terms and types,
|
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
257 |
they can only construct fixed terms. Unfortunately, one often needs to construct terms
|
13
|
258 |
dynamically. For example, a function that returns the implication
|
52
|
259 |
@{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the type @{term "\<tau>"}
|
19
|
260 |
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
|
261 |
*}
|
12
|
262 |
|
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
263 |
ML {*
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
264 |
fun make_imp P Q tau =
|
12
|
265 |
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
|
266 |
val x = Free ("x",tau)
|
12
|
267 |
in Logic.all x (Logic.mk_implies (HOLogic.mk_Trueprop (P $ x),
|
|
268 |
HOLogic.mk_Trueprop (Q $ x)))
|
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
269 |
end
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
270 |
*}
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
271 |
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
272 |
text {*
|
12
|
273 |
|
19
|
274 |
The reason is that one cannot pass the arguments @{term P}, @{term Q} and
|
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
275 |
@{term "tau"} into an antiquotation. For example the following does not work as
|
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
276 |
expected.
|
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
277 |
*}
|
13
|
278 |
|
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
279 |
ML {*
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
280 |
fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"}
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
281 |
*}
|
12
|
282 |
|
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 |
text {*
|
19
|
284 |
To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"}
|
|
285 |
to both functions.
|
|
286 |
|
|
287 |
One tricky point in constructing terms by hand is to obtain the
|
50
|
288 |
fully qualified name for constants. For example the names for @{text "zero"} and
|
19
|
289 |
@{text "+"} are more complex than one first expects, namely
|
15
|
290 |
|
|
291 |
\begin{center}
|
|
292 |
@{ML_text "HOL.zero_class.zero"} and @{ML_text "HOL.plus_class.plus"}.
|
|
293 |
\end{center}
|
|
294 |
|
|
295 |
The extra prefixes @{ML_text zero_class} and @{ML_text plus_class} are present because
|
|
296 |
these constants are defined within type classes; the prefix @{text "HOL"} indicates in
|
|
297 |
which theory they are defined. Guessing such internal names can sometimes be quite hard.
|
52
|
298 |
Therefore Isabelle provides the antiquotation @{text "@{const_name \<dots>}"} which does the
|
15
|
299 |
expansion automatically, for example:
|
49
|
300 |
|
|
301 |
@{ML_response_fake [display] "@{const_name \"Nil\"}" "List.list.Nil"}
|
10
|
302 |
|
19
|
303 |
(FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
|
11
|
304 |
|
50
|
305 |
Similarly, types can be constructed manually, for example as follows:
|
49
|
306 |
|
|
307 |
*}
|
|
308 |
|
|
309 |
ML {*
|
|
310 |
fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2])
|
|
311 |
*}
|
|
312 |
|
|
313 |
text {*
|
|
314 |
which can be equally written as
|
|
315 |
*}
|
|
316 |
|
|
317 |
ML {*
|
|
318 |
fun make_fun_type tau1 tau2 = tau1 --> tau2
|
|
319 |
*}
|
|
320 |
|
|
321 |
text {*
|
20
|
322 |
|
13
|
323 |
\begin{readmore}
|
|
324 |
There are many functions in @{ML_file "Pure/logic.ML"} and
|
12
|
325 |
@{ML_file "HOL/hologic.ML"} that make such manual constructions of terms
|
49
|
326 |
and types easier.\end{readmore}
|
13
|
327 |
|
|
328 |
Have a look at these files and try to solve the following two exercises:
|
11
|
329 |
|
|
330 |
*}
|
|
331 |
|
|
332 |
text {*
|
|
333 |
|
13
|
334 |
\begin{exercise}\label{fun:revsum}
|
11
|
335 |
Write a function @{ML_text "rev_sum : term -> term"} that takes a
|
|
336 |
term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "i"} might be zero)
|
|
337 |
and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume
|
|
338 |
the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"}
|
13
|
339 |
associates to the left. Try your function on some examples.
|
11
|
340 |
\end{exercise}
|
|
341 |
|
15
|
342 |
\begin{exercise}\label{fun:makesum}
|
11
|
343 |
Write a function which takes two terms representing natural numbers
|
|
344 |
in unary (like @{term "Suc (Suc (Suc 0))"}), and produce the unary
|
|
345 |
number representing their sum.
|
|
346 |
\end{exercise}
|
|
347 |
|
|
348 |
*}
|
|
349 |
|
49
|
350 |
section {* Type-Checking *}
|
10
|
351 |
|
|
352 |
text {*
|
13
|
353 |
|
10
|
354 |
We can freely construct and manipulate terms, since they are just
|
|
355 |
arbitrary unchecked trees. However, we eventually want to see if a
|
54
|
356 |
term is well-formed, or type-checks, relative to a theory.
|
50
|
357 |
Type-checking is done via the function @{ML cterm_of}, which converts
|
10
|
358 |
a @{ML_type term} into a @{ML_type cterm}, a \emph{certified} term.
|
|
359 |
Unlike @{ML_type term}s, which are just trees, @{ML_type
|
|
360 |
"cterm"}s are abstract objects that are guaranteed to be
|
50
|
361 |
type-correct, and that can only be constructed via the ``official
|
|
362 |
interfaces''.
|
2
|
363 |
|
54
|
364 |
Type-checking is always relative to a theory context. For now we use
|
10
|
365 |
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
|
366 |
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
|
367 |
|
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
368 |
@{ML_response_fake [display] "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}
|
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
369 |
|
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
370 |
or use the antiquotation
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
371 |
|
41
b11653b11bd3
further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
372 |
@{ML_response_fake [display] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"}
|
10
|
373 |
|
54
|
374 |
Attempting
|
|
375 |
|
|
376 |
@{ML_response_fake_both [display] "@{cterm \"1 + True\"}" "Type unification failed \<dots>"}
|
|
377 |
|
|
378 |
yields an error. A slightly more elaborate example is
|
20
|
379 |
|
41
b11653b11bd3
further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
380 |
@{ML_response_fake [display]
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
381 |
"let
|
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
382 |
val natT = @{typ \"nat\"}
|
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
383 |
val zero = @{term \"0::nat\"}
|
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
384 |
in
|
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
385 |
cterm_of @{theory}
|
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
386 |
(Const (@{const_name plus}, natT --> natT --> natT)
|
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
387 |
$ zero $ zero)
|
41
b11653b11bd3
further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
388 |
end" "0 + 0"}
|
12
|
389 |
|
13
|
390 |
\begin{exercise}
|
|
391 |
Check that the function defined in Exercise~\ref{fun:revsum} returns a
|
50
|
392 |
result that type-checks.
|
13
|
393 |
\end{exercise}
|
|
394 |
|
|
395 |
*}
|
|
396 |
|
2
|
397 |
section {* Theorems *}
|
|
398 |
|
|
399 |
text {*
|
50
|
400 |
Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm}
|
54
|
401 |
that can only be built by going through interfaces. In effect all proofs
|
|
402 |
are checked.
|
2
|
403 |
|
13
|
404 |
To see theorems in ``action'', let us give a proof for the following statement
|
10
|
405 |
*}
|
|
406 |
|
|
407 |
lemma
|
|
408 |
assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x"
|
|
409 |
and assm\<^isub>2: "P t"
|
13
|
410 |
shows "Q t" (*<*)oops(*>*)
|
10
|
411 |
|
|
412 |
text {*
|
49
|
413 |
on the ML-level:\footnote{Note that @{text "|>"} is reverse
|
2
|
414 |
application. This combinator, and several variants are defined in
|
13
|
415 |
@{ML_file "Pure/General/basics.ML"}.}
|
10
|
416 |
|
42
|
417 |
@{ML_response_fake [display]
|
|
418 |
"let
|
10
|
419 |
val thy = @{theory}
|
|
420 |
|
42
|
421 |
val assm1 = cterm_of thy @{prop \"\<And>(x::nat). P x \<Longrightarrow> Q x\"}
|
49
|
422 |
val assm2 = cterm_of thy @{prop \"(P::nat\<Rightarrow>bool) t\"}
|
10
|
423 |
|
|
424 |
val Pt_implies_Qt =
|
|
425 |
assume assm1
|
42
|
426 |
|> forall_elim (cterm_of thy @{term \"t::nat\"});
|
10
|
427 |
|
|
428 |
val Qt = implies_elim Pt_implies_Qt (assume assm2);
|
|
429 |
in
|
|
430 |
|
|
431 |
Qt
|
|
432 |
|> implies_intr assm2
|
|
433 |
|> implies_intr assm1
|
48
|
434 |
end" "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
|
12
|
435 |
|
21
|
436 |
This code-snippet constructs the following proof:
|
|
437 |
|
|
438 |
\[
|
|
439 |
\infer[(@{text "\<Longrightarrow>"}$-$intro)]{\vdash @{prop "(\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> P t \<Longrightarrow> Q t"}}
|
|
440 |
{\infer[(@{text "\<Longrightarrow>"}$-$intro)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}
|
|
441 |
{\infer[(@{text "\<Longrightarrow>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"}, @{prop "P t"} \vdash @{prop "Q t"}}
|
|
442 |
{\infer[(@{text "\<And>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}
|
|
443 |
{\infer[(assume)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "\<And>x. P x \<Longrightarrow> Q x"}}{}}
|
|
444 |
&
|
|
445 |
\infer[(assume)]{@{prop "P t"} \vdash @{prop "P t"}}{}
|
|
446 |
}
|
|
447 |
}
|
|
448 |
}
|
|
449 |
\]
|
|
450 |
|
|
451 |
|
13
|
452 |
\begin{readmore}
|
50
|
453 |
For the functions @{text "assume"}, @{text "forall_elim"} etc
|
13
|
454 |
see \isccite{sec:thms}. The basic functions for theorems are defined in
|
|
455 |
@{ML_file "Pure/thm.ML"}.
|
|
456 |
\end{readmore}
|
12
|
457 |
|
10
|
458 |
*}
|
|
459 |
|
|
460 |
|
12
|
461 |
section {* Tactical Reasoning *}
|
2
|
462 |
|
|
463 |
text {*
|
13
|
464 |
The goal-oriented tactical style reasoning of the ML level is similar
|
|
465 |
to the @{text apply}-style at the user level, i.e.~the reasoning is centred
|
|
466 |
around a \emph{goal}, which is modified in a sequence of proof steps
|
|
467 |
until it is solved.
|
2
|
468 |
|
|
469 |
A goal (or goal state) is a special @{ML_type thm}, which by
|
12
|
470 |
convention is an implication of the form:
|
|
471 |
|
2
|
472 |
@{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> #(C)"}
|
12
|
473 |
|
49
|
474 |
where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the open
|
|
475 |
subgoals.
|
13
|
476 |
Since the goal @{term C} can potentially be an implication, there is a
|
12
|
477 |
@{text "#"} wrapped around it, which prevents that premises are
|
50
|
478 |
misinterpreted as open subgoals. The wrapper @{text "# :: prop \<Rightarrow>
|
12
|
479 |
prop"} is just the identity function and used as a syntactic marker.
|
13
|
480 |
|
|
481 |
\begin{readmore}
|
54
|
482 |
For more on goals see \isccite{sec:tactical-goals}. (FIXME: in which
|
|
483 |
file is most code for dealing with goals?)
|
13
|
484 |
\end{readmore}
|
2
|
485 |
|
12
|
486 |
Tactics are functions that map a goal state to a (lazy)
|
2
|
487 |
sequence of successor states, hence the type of a tactic is
|
|
488 |
@{ML_type[display] "thm -> thm Seq.seq"}
|
12
|
489 |
|
|
490 |
\begin{readmore}
|
2
|
491 |
See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy
|
13
|
492 |
sequences. However in day-to-day Isabelle programming, one rarely
|
|
493 |
constructs sequences explicitly, but uses the predefined tactic
|
50
|
494 |
combinators (tacticals) instead. See @{ML_file "Pure/tctical.ML"}
|
|
495 |
for the code; see Chapters 3 and 4 in the old Isabelle Reference Manual.
|
12
|
496 |
\end{readmore}
|
2
|
497 |
|
34
|
498 |
While tactics can operate on the subgoals (the @{text "A\<^isub>i"} above), they
|
13
|
499 |
are expected to leave the conclusion @{term C} intact, with the
|
|
500 |
exception of possibly instantiating schematic variables.
|
12
|
501 |
|
13
|
502 |
To see how tactics work, let us transcribe a simple @{text apply}-style
|
50
|
503 |
proof into ML:
|
2
|
504 |
*}
|
|
505 |
|
|
506 |
lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
|
|
507 |
apply (erule disjE)
|
|
508 |
apply (rule disjI2)
|
|
509 |
apply assumption
|
|
510 |
apply (rule disjI1)
|
|
511 |
apply assumption
|
|
512 |
done
|
|
513 |
|
12
|
514 |
text {*
|
21
|
515 |
To start the proof, the function @{ML "Goal.prove"}~@{text "ctxt xs As C tac"} sets
|
|
516 |
up a goal state for proving the goal @{text C} under the assumptions @{text As}
|
|
517 |
(empty in the proof at hand)
|
|
518 |
with the variables @{text xs} that will be generalised once the
|
|
519 |
goal is proved. The @{text "tac"} is the tactic which proves the goal and which
|
50
|
520 |
can make use of the local assumptions (there are none in this example).
|
12
|
521 |
|
42
|
522 |
@{ML_response_fake [display]
|
|
523 |
"let
|
2
|
524 |
val ctxt = @{context}
|
42
|
525 |
val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}
|
2
|
526 |
in
|
42
|
527 |
Goal.prove ctxt [\"P\", \"Q\"] [] goal (fn _ =>
|
2
|
528 |
eresolve_tac [disjE] 1
|
|
529 |
THEN resolve_tac [disjI2] 1
|
|
530 |
THEN assume_tac 1
|
|
531 |
THEN resolve_tac [disjI1] 1
|
|
532 |
THEN assume_tac 1)
|
48
|
533 |
end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}
|
21
|
534 |
|
|
535 |
\begin{readmore}
|
54
|
536 |
To learn more about the function @{ML Goal.prove} see \isccite{sec:results} and
|
|
537 |
the file @{ML_file "Pure/goal.ML"}.
|
21
|
538 |
\end{readmore}
|
|
539 |
|
|
540 |
|
42
|
541 |
An alternative way to transcribe this proof is as follows
|
2
|
542 |
|
42
|
543 |
@{ML_response_fake [display]
|
|
544 |
"let
|
12
|
545 |
val ctxt = @{context}
|
42
|
546 |
val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}
|
12
|
547 |
in
|
42
|
548 |
Goal.prove ctxt [\"P\", \"Q\"] [] goal (fn _ =>
|
12
|
549 |
(eresolve_tac [disjE]
|
|
550 |
THEN' resolve_tac [disjI2]
|
|
551 |
THEN' assume_tac
|
|
552 |
THEN' resolve_tac [disjI1]
|
|
553 |
THEN' assume_tac) 1)
|
48
|
554 |
end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}
|
42
|
555 |
|
|
556 |
(FIXME: are there any advantages/disadvantages about this way?)
|
2
|
557 |
*}
|
|
558 |
|
20
|
559 |
section {* Storing Theorems *}
|
|
560 |
|
|
561 |
section {* Theorem Attributes *}
|
|
562 |
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
563 |
|
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
564 |
|
2
|
565 |
|
|
566 |
end |