lcp@105
|
1 |
%% $Id$
|
lcp@284
|
2 |
\part{Advanced Methods}
|
lcp@105
|
3 |
Before continuing, it might be wise to try some of your own examples in
|
lcp@105
|
4 |
Isabelle, reinforcing your knowledge of the basic functions.
|
lcp@105
|
5 |
|
wenzelm@3103
|
6 |
Look through {\em Isabelle's Object-Logics\/} and try proving some
|
wenzelm@3103
|
7 |
simple theorems. You probably should begin with first-order logic
|
paulson@5205
|
8 |
(\texttt{FOL} or~\texttt{LK}). Try working some of the examples provided,
|
paulson@5205
|
9 |
and others from the literature. Set theory~(\texttt{ZF}) and
|
paulson@5205
|
10 |
Constructive Type Theory~(\texttt{CTT}) form a richer world for
|
wenzelm@3103
|
11 |
mathematical reasoning and, again, many examples are in the
|
paulson@5205
|
12 |
literature. Higher-order logic~(\texttt{HOL}) is Isabelle's most
|
paulson@3485
|
13 |
elaborate logic. Its types and functions are identified with those of
|
wenzelm@3103
|
14 |
the meta-logic.
|
lcp@105
|
15 |
|
lcp@105
|
16 |
Choose a logic that you already understand. Isabelle is a proof
|
lcp@105
|
17 |
tool, not a teaching tool; if you do not know how to do a particular proof
|
lcp@105
|
18 |
on paper, then you certainly will not be able to do it on the machine.
|
lcp@105
|
19 |
Even experienced users plan large proofs on paper.
|
lcp@105
|
20 |
|
lcp@105
|
21 |
We have covered only the bare essentials of Isabelle, but enough to perform
|
lcp@105
|
22 |
substantial proofs. By occasionally dipping into the {\em Reference
|
lcp@105
|
23 |
Manual}, you can learn additional tactics, subgoal commands and tacticals.
|
lcp@105
|
24 |
|
lcp@105
|
25 |
|
lcp@105
|
26 |
\section{Deriving rules in Isabelle}
|
lcp@105
|
27 |
\index{rules!derived}
|
lcp@105
|
28 |
A mathematical development goes through a progression of stages. Each
|
lcp@105
|
29 |
stage defines some concepts and derives rules about them. We shall see how
|
lcp@105
|
30 |
to derive rules, perhaps involving definitions, using Isabelle. The
|
lcp@310
|
31 |
following section will explain how to declare types, constants, rules and
|
lcp@105
|
32 |
definitions.
|
lcp@105
|
33 |
|
lcp@105
|
34 |
|
lcp@296
|
35 |
\subsection{Deriving a rule using tactics and meta-level assumptions}
|
lcp@296
|
36 |
\label{deriving-example}
|
lcp@310
|
37 |
\index{examples!of deriving rules}\index{assumptions!of main goal}
|
lcp@296
|
38 |
|
lcp@307
|
39 |
The subgoal module supports the derivation of rules, as discussed in
|
paulson@5205
|
40 |
\S\ref{deriving}. When the \ttindex{Goal} command is supplied a formula of
|
paulson@5205
|
41 |
the form $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, there are two
|
paulson@5205
|
42 |
possibilities:
|
paulson@5205
|
43 |
\begin{itemize}
|
paulson@5205
|
44 |
\item If all of the premises $\theta@1$, \ldots, $\theta@k$ are simple
|
paulson@5205
|
45 |
formulae{} (they do not involve the meta-connectives $\Forall$ or
|
paulson@5205
|
46 |
$\Imp$) then the command sets the goal to be
|
paulson@5205
|
47 |
$\List{\theta@1; \ldots; \theta@k} \Imp \phi$ and returns the empty list.
|
paulson@5205
|
48 |
\item If one or more premises involves the meta-connectives $\Forall$ or
|
paulson@5205
|
49 |
$\Imp$, then the command sets the goal to be $\phi$ and returns a list
|
paulson@5205
|
50 |
consisting of the theorems ${\theta@i\;[\theta@i]}$, for $i=1$, \ldots,~$k$.
|
paulson@14148
|
51 |
These meta-level assumptions are also recorded internally, allowing
|
paulson@5205
|
52 |
\texttt{result} (which is called by \texttt{qed}) to discharge them in the
|
paulson@5205
|
53 |
original order.
|
paulson@5205
|
54 |
\end{itemize}
|
paulson@5205
|
55 |
Rules that discharge assumptions or introduce eigenvariables have complex
|
paulson@14148
|
56 |
premises, and the second case applies. In this section, many of the
|
paulson@14148
|
57 |
theorems are subject to meta-level assumptions, so we make them visible by by setting the
|
paulson@14148
|
58 |
\ttindex{show_hyps} flag:
|
paulson@14148
|
59 |
\begin{ttbox}
|
paulson@14148
|
60 |
set show_hyps;
|
paulson@14148
|
61 |
{\out val it = true : bool}
|
paulson@14148
|
62 |
\end{ttbox}
|
lcp@105
|
63 |
|
paulson@14148
|
64 |
Now, we are ready to derive $\conj$ elimination. Until now, calling \texttt{Goal} has
|
paulson@5205
|
65 |
returned an empty list, which we have ignored. In this example, the list
|
paulson@5205
|
66 |
contains the two premises of the rule, since one of them involves the $\Imp$
|
paulson@5205
|
67 |
connective. We bind them to the \ML\ identifiers \texttt{major} and {\tt
|
paulson@5205
|
68 |
minor}:\footnote{Some ML compilers will print a message such as {\em binding
|
paulson@5205
|
69 |
not exhaustive}. This warns that \texttt{Goal} must return a 2-element
|
paulson@5205
|
70 |
list. Otherwise, the pattern-match will fail; ML will raise exception
|
paulson@5205
|
71 |
\xdx{Match}.}
|
lcp@105
|
72 |
\begin{ttbox}
|
paulson@5205
|
73 |
val [major,minor] = Goal
|
lcp@105
|
74 |
"[| P&Q; [| P; Q |] ==> R |] ==> R";
|
lcp@105
|
75 |
{\out Level 0}
|
lcp@105
|
76 |
{\out R}
|
lcp@105
|
77 |
{\out 1. R}
|
lcp@105
|
78 |
{\out val major = "P & Q [P & Q]" : thm}
|
lcp@105
|
79 |
{\out val minor = "[| P; Q |] ==> R [[| P; Q |] ==> R]" : thm}
|
lcp@105
|
80 |
\end{ttbox}
|
lcp@105
|
81 |
Look at the minor premise, recalling that meta-level assumptions are
|
paulson@5205
|
82 |
shown in brackets. Using \texttt{minor}, we reduce $R$ to the subgoals
|
lcp@105
|
83 |
$P$ and~$Q$:
|
lcp@105
|
84 |
\begin{ttbox}
|
lcp@105
|
85 |
by (resolve_tac [minor] 1);
|
lcp@105
|
86 |
{\out Level 1}
|
lcp@105
|
87 |
{\out R}
|
lcp@105
|
88 |
{\out 1. P}
|
lcp@105
|
89 |
{\out 2. Q}
|
lcp@105
|
90 |
\end{ttbox}
|
lcp@105
|
91 |
Deviating from~\S\ref{deriving}, we apply $({\conj}E1)$ forwards from the
|
lcp@105
|
92 |
assumption $P\conj Q$ to obtain the theorem~$P\;[P\conj Q]$.
|
lcp@105
|
93 |
\begin{ttbox}
|
lcp@105
|
94 |
major RS conjunct1;
|
lcp@105
|
95 |
{\out val it = "P [P & Q]" : thm}
|
lcp@105
|
96 |
\ttbreak
|
lcp@105
|
97 |
by (resolve_tac [major RS conjunct1] 1);
|
lcp@105
|
98 |
{\out Level 2}
|
lcp@105
|
99 |
{\out R}
|
lcp@105
|
100 |
{\out 1. Q}
|
lcp@105
|
101 |
\end{ttbox}
|
lcp@105
|
102 |
Similarly, we solve the subgoal involving~$Q$.
|
lcp@105
|
103 |
\begin{ttbox}
|
lcp@105
|
104 |
major RS conjunct2;
|
lcp@105
|
105 |
{\out val it = "Q [P & Q]" : thm}
|
lcp@105
|
106 |
by (resolve_tac [major RS conjunct2] 1);
|
lcp@105
|
107 |
{\out Level 3}
|
lcp@105
|
108 |
{\out R}
|
lcp@105
|
109 |
{\out No subgoals!}
|
lcp@105
|
110 |
\end{ttbox}
|
lcp@105
|
111 |
Calling \ttindex{topthm} returns the current proof state as a theorem.
|
wenzelm@3103
|
112 |
Note that it contains assumptions. Calling \ttindex{qed} discharges
|
wenzelm@3103
|
113 |
the assumptions --- both occurrences of $P\conj Q$ are discharged as
|
wenzelm@3103
|
114 |
one --- and makes the variables schematic.
|
lcp@105
|
115 |
\begin{ttbox}
|
lcp@105
|
116 |
topthm();
|
lcp@105
|
117 |
{\out val it = "R [P & Q, P & Q, [| P; Q |] ==> R]" : thm}
|
wenzelm@3103
|
118 |
qed "conjE";
|
lcp@105
|
119 |
{\out val conjE = "[| ?P & ?Q; [| ?P; ?Q |] ==> ?R |] ==> ?R" : thm}
|
lcp@105
|
120 |
\end{ttbox}
|
lcp@105
|
121 |
|
lcp@105
|
122 |
|
lcp@105
|
123 |
\subsection{Definitions and derived rules} \label{definitions}
|
lcp@310
|
124 |
\index{rules!derived}\index{definitions!and derived rules|(}
|
lcp@310
|
125 |
|
lcp@105
|
126 |
Definitions are expressed as meta-level equalities. Let us define negation
|
lcp@105
|
127 |
and the if-and-only-if connective:
|
lcp@105
|
128 |
\begin{eqnarray*}
|
lcp@105
|
129 |
\neg \Var{P} & \equiv & \Var{P}\imp\bot \\
|
lcp@105
|
130 |
\Var{P}\bimp \Var{Q} & \equiv &
|
lcp@105
|
131 |
(\Var{P}\imp \Var{Q}) \conj (\Var{Q}\imp \Var{P})
|
lcp@105
|
132 |
\end{eqnarray*}
|
lcp@331
|
133 |
\index{meta-rewriting}%
|
lcp@105
|
134 |
Isabelle permits {\bf meta-level rewriting} using definitions such as
|
lcp@105
|
135 |
these. {\bf Unfolding} replaces every instance
|
lcp@331
|
136 |
of $\neg \Var{P}$ by the corresponding instance of ${\Var{P}\imp\bot}$. For
|
lcp@105
|
137 |
example, $\forall x.\neg (P(x)\conj \neg R(x,0))$ unfolds to
|
lcp@105
|
138 |
\[ \forall x.(P(x)\conj R(x,0)\imp\bot)\imp\bot. \]
|
lcp@105
|
139 |
{\bf Folding} a definition replaces occurrences of the right-hand side by
|
lcp@105
|
140 |
the left. The occurrences need not be free in the entire formula.
|
lcp@105
|
141 |
|
lcp@105
|
142 |
When you define new concepts, you should derive rules asserting their
|
lcp@105
|
143 |
abstract properties, and then forget their definitions. This supports
|
lcp@331
|
144 |
modularity: if you later change the definitions without affecting their
|
lcp@105
|
145 |
abstract properties, then most of your proofs will carry through without
|
lcp@105
|
146 |
change. Indiscriminate unfolding makes a subgoal grow exponentially,
|
lcp@105
|
147 |
becoming unreadable.
|
lcp@105
|
148 |
|
lcp@105
|
149 |
Taking this point of view, Isabelle does not unfold definitions
|
lcp@105
|
150 |
automatically during proofs. Rewriting must be explicit and selective.
|
lcp@105
|
151 |
Isabelle provides tactics and meta-rules for rewriting, and a version of
|
paulson@5205
|
152 |
the \texttt{Goal} command that unfolds the conclusion and premises of the rule
|
lcp@105
|
153 |
being derived.
|
lcp@105
|
154 |
|
lcp@105
|
155 |
For example, the intuitionistic definition of negation given above may seem
|
lcp@105
|
156 |
peculiar. Using Isabelle, we shall derive pleasanter negation rules:
|
lcp@105
|
157 |
\[ \infer[({\neg}I)]{\neg P}{\infer*{\bot}{[P]}} \qquad
|
lcp@105
|
158 |
\infer[({\neg}E)]{Q}{\neg P & P} \]
|
lcp@296
|
159 |
This requires proving the following meta-formulae:
|
wenzelm@3103
|
160 |
$$ (P\Imp\bot) \Imp \neg P \eqno(\neg I) $$
|
wenzelm@3103
|
161 |
$$ \List{\neg P; P} \Imp Q. \eqno(\neg E) $$
|
lcp@105
|
162 |
|
lcp@105
|
163 |
|
lcp@296
|
164 |
\subsection{Deriving the $\neg$ introduction rule}
|
paulson@5205
|
165 |
To derive $(\neg I)$, we may call \texttt{Goal} with the appropriate formula.
|
paulson@5205
|
166 |
Again, the rule's premises involve a meta-connective, and \texttt{Goal}
|
paulson@5205
|
167 |
returns one-element list. We bind this list to the \ML\ identifier \texttt{prems}.
|
lcp@105
|
168 |
\begin{ttbox}
|
paulson@5205
|
169 |
val prems = Goal "(P ==> False) ==> ~P";
|
lcp@105
|
170 |
{\out Level 0}
|
lcp@105
|
171 |
{\out ~P}
|
lcp@105
|
172 |
{\out 1. ~P}
|
lcp@105
|
173 |
{\out val prems = ["P ==> False [P ==> False]"] : thm list}
|
lcp@105
|
174 |
\end{ttbox}
|
lcp@310
|
175 |
Calling \ttindex{rewrite_goals_tac} with \tdx{not_def}, which is the
|
lcp@105
|
176 |
definition of negation, unfolds that definition in the subgoals. It leaves
|
lcp@105
|
177 |
the main goal alone.
|
lcp@105
|
178 |
\begin{ttbox}
|
lcp@105
|
179 |
not_def;
|
lcp@105
|
180 |
{\out val it = "~?P == ?P --> False" : thm}
|
lcp@105
|
181 |
by (rewrite_goals_tac [not_def]);
|
lcp@105
|
182 |
{\out Level 1}
|
lcp@105
|
183 |
{\out ~P}
|
lcp@105
|
184 |
{\out 1. P --> False}
|
lcp@105
|
185 |
\end{ttbox}
|
lcp@310
|
186 |
Using \tdx{impI} and the premise, we reduce subgoal~1 to a triviality:
|
lcp@105
|
187 |
\begin{ttbox}
|
lcp@105
|
188 |
by (resolve_tac [impI] 1);
|
lcp@105
|
189 |
{\out Level 2}
|
lcp@105
|
190 |
{\out ~P}
|
lcp@105
|
191 |
{\out 1. P ==> False}
|
lcp@105
|
192 |
\ttbreak
|
lcp@105
|
193 |
by (resolve_tac prems 1);
|
lcp@105
|
194 |
{\out Level 3}
|
lcp@105
|
195 |
{\out ~P}
|
lcp@105
|
196 |
{\out 1. P ==> P}
|
lcp@105
|
197 |
\end{ttbox}
|
lcp@296
|
198 |
The rest of the proof is routine. Note the form of the final result.
|
lcp@105
|
199 |
\begin{ttbox}
|
lcp@105
|
200 |
by (assume_tac 1);
|
lcp@105
|
201 |
{\out Level 4}
|
lcp@105
|
202 |
{\out ~P}
|
lcp@105
|
203 |
{\out No subgoals!}
|
lcp@296
|
204 |
\ttbreak
|
wenzelm@3103
|
205 |
qed "notI";
|
lcp@105
|
206 |
{\out val notI = "(?P ==> False) ==> ~?P" : thm}
|
lcp@105
|
207 |
\end{ttbox}
|
lcp@310
|
208 |
\indexbold{*notI theorem}
|
lcp@105
|
209 |
|
paulson@5205
|
210 |
There is a simpler way of conducting this proof. The \ttindex{Goalw}
|
paulson@5205
|
211 |
command starts a backward proof, as does \texttt{Goal}, but it also
|
lcp@296
|
212 |
unfolds definitions. Thus there is no need to call
|
lcp@296
|
213 |
\ttindex{rewrite_goals_tac}:
|
lcp@105
|
214 |
\begin{ttbox}
|
paulson@5205
|
215 |
val prems = Goalw [not_def]
|
lcp@105
|
216 |
"(P ==> False) ==> ~P";
|
lcp@105
|
217 |
{\out Level 0}
|
lcp@105
|
218 |
{\out ~P}
|
lcp@105
|
219 |
{\out 1. P --> False}
|
lcp@105
|
220 |
{\out val prems = ["P ==> False [P ==> False]"] : thm list}
|
lcp@105
|
221 |
\end{ttbox}
|
lcp@105
|
222 |
|
lcp@105
|
223 |
|
lcp@296
|
224 |
\subsection{Deriving the $\neg$ elimination rule}
|
paulson@5205
|
225 |
Let us derive the rule $(\neg E)$. The proof follows that of~\texttt{conjE}
|
lcp@296
|
226 |
above, with an additional step to unfold negation in the major premise.
|
paulson@5205
|
227 |
The \texttt{Goalw} command is best for this: it unfolds definitions not only
|
paulson@5205
|
228 |
in the conclusion but the premises.
|
lcp@105
|
229 |
\begin{ttbox}
|
paulson@5205
|
230 |
Goalw [not_def] "[| ~P; P |] ==> R";
|
lcp@105
|
231 |
{\out Level 0}
|
paulson@5205
|
232 |
{\out [| ~ P; P |] ==> R}
|
paulson@5205
|
233 |
{\out 1. [| P --> False; P |] ==> R}
|
paulson@5205
|
234 |
\end{ttbox}
|
paulson@5205
|
235 |
As the first step, we apply \tdx{FalseE}:
|
paulson@5205
|
236 |
\begin{ttbox}
|
lcp@105
|
237 |
by (resolve_tac [FalseE] 1);
|
lcp@105
|
238 |
{\out Level 1}
|
paulson@5205
|
239 |
{\out [| ~ P; P |] ==> R}
|
paulson@5205
|
240 |
{\out 1. [| P --> False; P |] ==> False}
|
lcp@284
|
241 |
\end{ttbox}
|
paulson@5205
|
242 |
%
|
lcp@284
|
243 |
Everything follows from falsity. And we can prove falsity using the
|
lcp@284
|
244 |
premises and Modus Ponens:
|
lcp@284
|
245 |
\begin{ttbox}
|
paulson@5205
|
246 |
by (eresolve_tac [mp] 1);
|
lcp@105
|
247 |
{\out Level 2}
|
paulson@5205
|
248 |
{\out [| ~ P; P |] ==> R}
|
paulson@5205
|
249 |
{\out 1. P ==> P}
|
paulson@5205
|
250 |
\ttbreak
|
paulson@5205
|
251 |
by (assume_tac 1);
|
lcp@105
|
252 |
{\out Level 3}
|
paulson@5205
|
253 |
{\out [| ~ P; P |] ==> R}
|
lcp@105
|
254 |
{\out No subgoals!}
|
paulson@5205
|
255 |
\ttbreak
|
wenzelm@3103
|
256 |
qed "notE";
|
lcp@105
|
257 |
{\out val notE = "[| ~?P; ?P |] ==> ?R" : thm}
|
lcp@105
|
258 |
\end{ttbox}
|
paulson@5205
|
259 |
|
lcp@105
|
260 |
|
lcp@105
|
261 |
\medskip
|
paulson@5205
|
262 |
\texttt{Goalw} unfolds definitions in the premises even when it has to return
|
paulson@5205
|
263 |
them as a list. Another way of unfolding definitions in a theorem is by
|
paulson@5205
|
264 |
applying the function \ttindex{rewrite_rule}.
|
paulson@5205
|
265 |
|
lcp@310
|
266 |
\index{definitions!and derived rules|)}
|
lcp@105
|
267 |
|
lcp@105
|
268 |
|
lcp@284
|
269 |
\section{Defining theories}\label{sec:defining-theories}
|
lcp@105
|
270 |
\index{theories!defining|(}
|
lcp@310
|
271 |
|
wenzelm@3103
|
272 |
Isabelle makes no distinction between simple extensions of a logic ---
|
wenzelm@3103
|
273 |
like specifying a type~$bool$ with constants~$true$ and~$false$ ---
|
wenzelm@3103
|
274 |
and defining an entire logic. A theory definition has a form like
|
lcp@105
|
275 |
\begin{ttbox}
|
lcp@105
|
276 |
\(T\) = \(S@1\) + \(\cdots\) + \(S@n\) +
|
lcp@105
|
277 |
classes {\it class declarations}
|
lcp@105
|
278 |
default {\it sort}
|
lcp@331
|
279 |
types {\it type declarations and synonyms}
|
wenzelm@3103
|
280 |
arities {\it type arity declarations}
|
lcp@105
|
281 |
consts {\it constant declarations}
|
wenzelm@3103
|
282 |
syntax {\it syntactic constant declarations}
|
wenzelm@3103
|
283 |
translations {\it ast translation rules}
|
wenzelm@3103
|
284 |
defs {\it meta-logical definitions}
|
lcp@105
|
285 |
rules {\it rule declarations}
|
lcp@105
|
286 |
end
|
lcp@105
|
287 |
ML {\it ML code}
|
lcp@105
|
288 |
\end{ttbox}
|
lcp@105
|
289 |
This declares the theory $T$ to extend the existing theories
|
wenzelm@3103
|
290 |
$S@1$,~\ldots,~$S@n$. It may introduce new classes, types, arities
|
wenzelm@3103
|
291 |
(of existing types), constants and rules; it can specify the default
|
wenzelm@3103
|
292 |
sort for type variables. A constant declaration can specify an
|
wenzelm@3103
|
293 |
associated concrete syntax. The translations section specifies
|
wenzelm@3103
|
294 |
rewrite rules on abstract syntax trees, handling notations and
|
paulson@5205
|
295 |
abbreviations. \index{*ML section} The \texttt{ML} section may contain
|
wenzelm@3103
|
296 |
code to perform arbitrary syntactic transformations. The main
|
wenzelm@3212
|
297 |
declaration forms are discussed below. There are some more sections
|
wenzelm@3212
|
298 |
not presented here, the full syntax can be found in
|
wenzelm@3212
|
299 |
\iflabelundefined{app:TheorySyntax}{an appendix of the {\it Reference
|
wenzelm@3212
|
300 |
Manual}}{App.\ts\ref{app:TheorySyntax}}. Also note that
|
wenzelm@3212
|
301 |
object-logics may add further theory sections, for example
|
wenzelm@9695
|
302 |
\texttt{typedef}, \texttt{datatype} in HOL.
|
lcp@105
|
303 |
|
wenzelm@3103
|
304 |
All the declaration parts can be omitted or repeated and may appear in
|
wenzelm@3103
|
305 |
any order, except that the {\ML} section must be last (after the {\tt
|
wenzelm@3103
|
306 |
end} keyword). In the simplest case, $T$ is just the union of
|
wenzelm@3103
|
307 |
$S@1$,~\ldots,~$S@n$. New theories always extend one or more other
|
wenzelm@3103
|
308 |
theories, inheriting their types, constants, syntax, etc. The theory
|
paulson@3485
|
309 |
\thydx{Pure} contains nothing but Isabelle's meta-logic. The variant
|
wenzelm@3103
|
310 |
\thydx{CPure} offers the more usual higher-order function application
|
wenzelm@9695
|
311 |
syntax $t\,u@1\ldots\,u@n$ instead of $t(u@1,\ldots,u@n)$ in Pure.
|
lcp@105
|
312 |
|
wenzelm@3103
|
313 |
Each theory definition must reside in a separate file, whose name is
|
wenzelm@3103
|
314 |
the theory's with {\tt.thy} appended. Calling
|
wenzelm@3103
|
315 |
\ttindexbold{use_thy}~{\tt"{\it T\/}"} reads the definition from {\it
|
wenzelm@3103
|
316 |
T}{\tt.thy}, writes a corresponding file of {\ML} code {\tt.{\it
|
wenzelm@3103
|
317 |
T}.thy.ML}, reads the latter file, and deletes it if no errors
|
wenzelm@3103
|
318 |
occurred. This declares the {\ML} structure~$T$, which contains a
|
paulson@5205
|
319 |
component \texttt{thy} denoting the new theory, a component for each
|
wenzelm@3103
|
320 |
rule, and everything declared in {\it ML code}.
|
lcp@105
|
321 |
|
wenzelm@3103
|
322 |
Errors may arise during the translation to {\ML} (say, a misspelled
|
wenzelm@3103
|
323 |
keyword) or during creation of the new theory (say, a type error in a
|
paulson@5205
|
324 |
rule). But if all goes well, \texttt{use_thy} will finally read the file
|
wenzelm@3103
|
325 |
{\it T}{\tt.ML} (if it exists). This file typically contains proofs
|
paulson@3485
|
326 |
that refer to the components of~$T$. The structure is automatically
|
wenzelm@3103
|
327 |
opened, so its components may be referred to by unqualified names,
|
paulson@5205
|
328 |
e.g.\ just \texttt{thy} instead of $T$\texttt{.thy}.
|
lcp@105
|
329 |
|
wenzelm@3103
|
330 |
\ttindexbold{use_thy} automatically loads a theory's parents before
|
wenzelm@3103
|
331 |
loading the theory itself. When a theory file is modified, many
|
wenzelm@3103
|
332 |
theories may have to be reloaded. Isabelle records the modification
|
wenzelm@3103
|
333 |
times and dependencies of theory files. See
|
lcp@331
|
334 |
\iflabelundefined{sec:reloading-theories}{the {\em Reference Manual\/}}%
|
lcp@331
|
335 |
{\S\ref{sec:reloading-theories}}
|
lcp@296
|
336 |
for more details.
|
lcp@296
|
337 |
|
lcp@105
|
338 |
|
lcp@1084
|
339 |
\subsection{Declaring constants, definitions and rules}
|
lcp@310
|
340 |
\indexbold{constants!declaring}\index{rules!declaring}
|
lcp@310
|
341 |
|
lcp@1084
|
342 |
Most theories simply declare constants, definitions and rules. The {\bf
|
lcp@1084
|
343 |
constant declaration part} has the form
|
lcp@105
|
344 |
\begin{ttbox}
|
clasohm@1387
|
345 |
consts \(c@1\) :: \(\tau@1\)
|
lcp@105
|
346 |
\vdots
|
clasohm@1387
|
347 |
\(c@n\) :: \(\tau@n\)
|
lcp@105
|
348 |
\end{ttbox}
|
lcp@105
|
349 |
where $c@1$, \ldots, $c@n$ are constants and $\tau@1$, \ldots, $\tau@n$ are
|
clasohm@1387
|
350 |
types. The types must be enclosed in quotation marks if they contain
|
paulson@5205
|
351 |
user-declared infix type constructors like \texttt{*}. Each
|
lcp@105
|
352 |
constant must be enclosed in quotation marks unless it is a valid
|
lcp@105
|
353 |
identifier. To declare $c@1$, \ldots, $c@n$ as constants of type $\tau$,
|
lcp@105
|
354 |
the $n$ declarations may be abbreviated to a single line:
|
lcp@105
|
355 |
\begin{ttbox}
|
clasohm@1387
|
356 |
\(c@1\), \ldots, \(c@n\) :: \(\tau\)
|
lcp@105
|
357 |
\end{ttbox}
|
lcp@105
|
358 |
The {\bf rule declaration part} has the form
|
lcp@105
|
359 |
\begin{ttbox}
|
lcp@105
|
360 |
rules \(id@1\) "\(rule@1\)"
|
lcp@105
|
361 |
\vdots
|
lcp@105
|
362 |
\(id@n\) "\(rule@n\)"
|
lcp@105
|
363 |
\end{ttbox}
|
lcp@105
|
364 |
where $id@1$, \ldots, $id@n$ are \ML{} identifiers and $rule@1$, \ldots,
|
lcp@284
|
365 |
$rule@n$ are expressions of type~$prop$. Each rule {\em must\/} be
|
paulson@14148
|
366 |
enclosed in quotation marks. Rules are simply axioms; they are
|
paulson@14148
|
367 |
called \emph{rules} because they are mainly used to specify the inference
|
paulson@14148
|
368 |
rules when defining a new logic.
|
lcp@284
|
369 |
|
wenzelm@3103
|
370 |
\indexbold{definitions} The {\bf definition part} is similar, but with
|
paulson@5205
|
371 |
the keyword \texttt{defs} instead of \texttt{rules}. {\bf Definitions} are
|
wenzelm@3103
|
372 |
rules of the form $s \equiv t$, and should serve only as
|
paulson@3485
|
373 |
abbreviations. The simplest form of a definition is $f \equiv t$,
|
paulson@3485
|
374 |
where $f$ is a constant. Also allowed are $\eta$-equivalent forms of
|
wenzelm@3106
|
375 |
this, where the arguments of~$f$ appear applied on the left-hand side
|
wenzelm@3106
|
376 |
of the equation instead of abstracted on the right-hand side.
|
lcp@1084
|
377 |
|
wenzelm@3103
|
378 |
Isabelle checks for common errors in definitions, such as extra
|
paulson@14148
|
379 |
variables on the right-hand side and cyclic dependencies, that could
|
paulson@14148
|
380 |
least to inconsistency. It is still essential to take care:
|
paulson@14148
|
381 |
theorems proved on the basis of incorrect definitions are useless,
|
paulson@14148
|
382 |
your system can be consistent and yet still wrong.
|
wenzelm@3103
|
383 |
|
wenzelm@3103
|
384 |
\index{examples!of theories} This example theory extends first-order
|
wenzelm@3103
|
385 |
logic by declaring and defining two constants, {\em nand} and {\em
|
wenzelm@3103
|
386 |
xor}:
|
lcp@284
|
387 |
\begin{ttbox}
|
lcp@105
|
388 |
Gate = FOL +
|
clasohm@1387
|
389 |
consts nand,xor :: [o,o] => o
|
lcp@1084
|
390 |
defs nand_def "nand(P,Q) == ~(P & Q)"
|
lcp@105
|
391 |
xor_def "xor(P,Q) == P & ~Q | ~P & Q"
|
lcp@105
|
392 |
end
|
lcp@105
|
393 |
\end{ttbox}
|
lcp@105
|
394 |
|
nipkow@1649
|
395 |
Declaring and defining constants can be combined:
|
nipkow@1649
|
396 |
\begin{ttbox}
|
nipkow@1649
|
397 |
Gate = FOL +
|
nipkow@1649
|
398 |
constdefs nand :: [o,o] => o
|
nipkow@1649
|
399 |
"nand(P,Q) == ~(P & Q)"
|
nipkow@1649
|
400 |
xor :: [o,o] => o
|
nipkow@1649
|
401 |
"xor(P,Q) == P & ~Q | ~P & Q"
|
nipkow@1649
|
402 |
end
|
nipkow@1649
|
403 |
\end{ttbox}
|
paulson@5205
|
404 |
\texttt{constdefs} generates the names \texttt{nand_def} and \texttt{xor_def}
|
paulson@3485
|
405 |
automatically, which is why it is restricted to alphanumeric identifiers. In
|
nipkow@1649
|
406 |
general it has the form
|
nipkow@1649
|
407 |
\begin{ttbox}
|
nipkow@1649
|
408 |
constdefs \(id@1\) :: \(\tau@1\)
|
nipkow@1649
|
409 |
"\(id@1 \equiv \dots\)"
|
nipkow@1649
|
410 |
\vdots
|
nipkow@1649
|
411 |
\(id@n\) :: \(\tau@n\)
|
nipkow@1649
|
412 |
"\(id@n \equiv \dots\)"
|
nipkow@1649
|
413 |
\end{ttbox}
|
nipkow@1649
|
414 |
|
nipkow@1649
|
415 |
|
nipkow@1366
|
416 |
\begin{warn}
|
nipkow@1366
|
417 |
A common mistake when writing definitions is to introduce extra free variables
|
nipkow@1468
|
418 |
on the right-hand side as in the following fictitious definition:
|
nipkow@1366
|
419 |
\begin{ttbox}
|
nipkow@1366
|
420 |
defs prime_def "prime(p) == (m divides p) --> (m=1 | m=p)"
|
nipkow@1366
|
421 |
\end{ttbox}
|
paulson@5205
|
422 |
Isabelle rejects this ``definition'' because of the extra \texttt{m} on the
|
paulson@3485
|
423 |
right-hand side, which would introduce an inconsistency. What you should have
|
nipkow@1366
|
424 |
written is
|
nipkow@1366
|
425 |
\begin{ttbox}
|
nipkow@1366
|
426 |
defs prime_def "prime(p) == ALL m. (m divides p) --> (m=1 | m=p)"
|
nipkow@1366
|
427 |
\end{ttbox}
|
nipkow@1366
|
428 |
\end{warn}
|
lcp@105
|
429 |
|
lcp@105
|
430 |
\subsection{Declaring type constructors}
|
nipkow@303
|
431 |
\indexbold{types!declaring}\indexbold{arities!declaring}
|
lcp@284
|
432 |
%
|
lcp@105
|
433 |
Types are composed of type variables and {\bf type constructors}. Each
|
lcp@284
|
434 |
type constructor takes a fixed number of arguments. They are declared
|
lcp@284
|
435 |
with an \ML-like syntax. If $list$ takes one type argument, $tree$ takes
|
lcp@284
|
436 |
two arguments and $nat$ takes no arguments, then these type constructors
|
lcp@284
|
437 |
can be declared by
|
lcp@284
|
438 |
\begin{ttbox}
|
lcp@284
|
439 |
types 'a list
|
lcp@284
|
440 |
('a,'b) tree
|
lcp@284
|
441 |
nat
|
lcp@284
|
442 |
\end{ttbox}
|
lcp@105
|
443 |
|
lcp@284
|
444 |
The {\bf type declaration part} has the general form
|
lcp@105
|
445 |
\begin{ttbox}
|
lcp@284
|
446 |
types \(tids@1\) \(id@1\)
|
lcp@105
|
447 |
\vdots
|
wenzelm@841
|
448 |
\(tids@n\) \(id@n\)
|
lcp@105
|
449 |
\end{ttbox}
|
lcp@284
|
450 |
where $id@1$, \ldots, $id@n$ are identifiers and $tids@1$, \ldots, $tids@n$
|
lcp@284
|
451 |
are type argument lists as shown in the example above. It declares each
|
lcp@284
|
452 |
$id@i$ as a type constructor with the specified number of argument places.
|
lcp@105
|
453 |
|
lcp@105
|
454 |
The {\bf arity declaration part} has the form
|
lcp@105
|
455 |
\begin{ttbox}
|
lcp@105
|
456 |
arities \(tycon@1\) :: \(arity@1\)
|
lcp@105
|
457 |
\vdots
|
lcp@105
|
458 |
\(tycon@n\) :: \(arity@n\)
|
lcp@105
|
459 |
\end{ttbox}
|
lcp@105
|
460 |
where $tycon@1$, \ldots, $tycon@n$ are identifiers and $arity@1$, \ldots,
|
lcp@105
|
461 |
$arity@n$ are arities. Arity declarations add arities to existing
|
lcp@296
|
462 |
types; they do not declare the types themselves.
|
lcp@105
|
463 |
In the simplest case, for an 0-place type constructor, an arity is simply
|
lcp@105
|
464 |
the type's class. Let us declare a type~$bool$ of class $term$, with
|
lcp@284
|
465 |
constants $tt$ and~$ff$. (In first-order logic, booleans are
|
lcp@284
|
466 |
distinct from formulae, which have type $o::logic$.)
|
lcp@105
|
467 |
\index{examples!of theories}
|
lcp@284
|
468 |
\begin{ttbox}
|
lcp@105
|
469 |
Bool = FOL +
|
lcp@284
|
470 |
types bool
|
lcp@105
|
471 |
arities bool :: term
|
clasohm@1387
|
472 |
consts tt,ff :: bool
|
lcp@105
|
473 |
end
|
lcp@105
|
474 |
\end{ttbox}
|
lcp@296
|
475 |
A $k$-place type constructor may have arities of the form
|
lcp@296
|
476 |
$(s@1,\ldots,s@k)c$, where $s@1,\ldots,s@n$ are sorts and $c$ is a class.
|
lcp@296
|
477 |
Each sort specifies a type argument; it has the form $\{c@1,\ldots,c@m\}$,
|
lcp@296
|
478 |
where $c@1$, \dots,~$c@m$ are classes. Mostly we deal with singleton
|
lcp@296
|
479 |
sorts, and may abbreviate them by dropping the braces. The arity
|
lcp@296
|
480 |
$(term)term$ is short for $(\{term\})term$. Recall the discussion in
|
lcp@296
|
481 |
\S\ref{polymorphic}.
|
lcp@105
|
482 |
|
lcp@105
|
483 |
A type constructor may be overloaded (subject to certain conditions) by
|
lcp@296
|
484 |
appearing in several arity declarations. For instance, the function type
|
lcp@331
|
485 |
constructor~$fun$ has the arity $(logic,logic)logic$; in higher-order
|
lcp@105
|
486 |
logic, it is declared also to have arity $(term,term)term$.
|
lcp@105
|
487 |
|
paulson@5205
|
488 |
Theory \texttt{List} declares the 1-place type constructor $list$, gives
|
paulson@5205
|
489 |
it the arity $(term)term$, and declares constants $Nil$ and $Cons$ with
|
lcp@296
|
490 |
polymorphic types:%
|
paulson@5205
|
491 |
\footnote{In the \texttt{consts} part, type variable {\tt'a} has the default
|
paulson@5205
|
492 |
sort, which is \texttt{term}. See the {\em Reference Manual\/}
|
lcp@296
|
493 |
\iflabelundefined{sec:ref-defining-theories}{}%
|
lcp@296
|
494 |
{(\S\ref{sec:ref-defining-theories})} for more information.}
|
lcp@105
|
495 |
\index{examples!of theories}
|
lcp@284
|
496 |
\begin{ttbox}
|
lcp@105
|
497 |
List = FOL +
|
lcp@284
|
498 |
types 'a list
|
lcp@105
|
499 |
arities list :: (term)term
|
clasohm@1387
|
500 |
consts Nil :: 'a list
|
clasohm@1387
|
501 |
Cons :: ['a, 'a list] => 'a list
|
lcp@105
|
502 |
end
|
lcp@105
|
503 |
\end{ttbox}
|
lcp@284
|
504 |
Multiple arity declarations may be abbreviated to a single line:
|
lcp@105
|
505 |
\begin{ttbox}
|
lcp@105
|
506 |
arities \(tycon@1\), \ldots, \(tycon@n\) :: \(arity\)
|
lcp@105
|
507 |
\end{ttbox}
|
lcp@105
|
508 |
|
wenzelm@3103
|
509 |
%\begin{warn}
|
wenzelm@3103
|
510 |
%Arity declarations resemble constant declarations, but there are {\it no\/}
|
wenzelm@3103
|
511 |
%quotation marks! Types and rules must be quoted because the theory
|
wenzelm@3103
|
512 |
%translator passes them verbatim to the {\ML} output file.
|
wenzelm@3103
|
513 |
%\end{warn}
|
lcp@105
|
514 |
|
lcp@331
|
515 |
\subsection{Type synonyms}\indexbold{type synonyms}
|
nipkow@303
|
516 |
Isabelle supports {\bf type synonyms} ({\bf abbreviations}) which are similar
|
lcp@307
|
517 |
to those found in \ML. Such synonyms are defined in the type declaration part
|
nipkow@303
|
518 |
and are fairly self explanatory:
|
nipkow@303
|
519 |
\begin{ttbox}
|
clasohm@1387
|
520 |
types gate = [o,o] => o
|
clasohm@1387
|
521 |
'a pred = 'a => o
|
clasohm@1387
|
522 |
('a,'b)nuf = 'b => 'a
|
nipkow@303
|
523 |
\end{ttbox}
|
nipkow@303
|
524 |
Type declarations and synonyms can be mixed arbitrarily:
|
nipkow@303
|
525 |
\begin{ttbox}
|
nipkow@303
|
526 |
types nat
|
clasohm@1387
|
527 |
'a stream = nat => 'a
|
clasohm@1387
|
528 |
signal = nat stream
|
nipkow@303
|
529 |
'a list
|
nipkow@303
|
530 |
\end{ttbox}
|
wenzelm@3103
|
531 |
A synonym is merely an abbreviation for some existing type expression.
|
wenzelm@3103
|
532 |
Hence synonyms may not be recursive! Internally all synonyms are
|
wenzelm@3103
|
533 |
fully expanded. As a consequence Isabelle output never contains
|
wenzelm@3103
|
534 |
synonyms. Their main purpose is to improve the readability of theory
|
wenzelm@3103
|
535 |
definitions. Synonyms can be used just like any other type:
|
nipkow@303
|
536 |
\begin{ttbox}
|
clasohm@1387
|
537 |
consts and,or :: gate
|
clasohm@1387
|
538 |
negate :: signal => signal
|
nipkow@303
|
539 |
\end{ttbox}
|
nipkow@303
|
540 |
|
lcp@348
|
541 |
\subsection{Infix and mixfix operators}
|
lcp@310
|
542 |
\index{infixes}\index{examples!of theories}
|
lcp@310
|
543 |
|
lcp@310
|
544 |
Infix or mixfix syntax may be attached to constants. Consider the
|
lcp@310
|
545 |
following theory:
|
lcp@284
|
546 |
\begin{ttbox}
|
lcp@105
|
547 |
Gate2 = FOL +
|
clasohm@1387
|
548 |
consts "~&" :: [o,o] => o (infixl 35)
|
clasohm@1387
|
549 |
"#" :: [o,o] => o (infixl 30)
|
lcp@1084
|
550 |
defs nand_def "P ~& Q == ~(P & Q)"
|
lcp@105
|
551 |
xor_def "P # Q == P & ~Q | ~P & Q"
|
lcp@105
|
552 |
end
|
lcp@105
|
553 |
\end{ttbox}
|
lcp@310
|
554 |
The constant declaration part declares two left-associating infix operators
|
lcp@310
|
555 |
with their priorities, or precedences; they are $\nand$ of priority~35 and
|
lcp@310
|
556 |
$\xor$ of priority~30. Hence $P \xor Q \xor R$ is parsed as $(P\xor Q)
|
lcp@310
|
557 |
\xor R$ and $P \xor Q \nand R$ as $P \xor (Q \nand R)$. Note the quotation
|
lcp@310
|
558 |
marks in \verb|"~&"| and \verb|"#"|.
|
lcp@105
|
559 |
|
lcp@105
|
560 |
The constants \hbox{\verb|op ~&|} and \hbox{\verb|op #|} are declared
|
lcp@105
|
561 |
automatically, just as in \ML. Hence you may write propositions like
|
lcp@105
|
562 |
\verb|op #(True) == op ~&(True)|, which asserts that the functions $\lambda
|
lcp@105
|
563 |
Q.True \xor Q$ and $\lambda Q.True \nand Q$ are identical.
|
lcp@105
|
564 |
|
wenzelm@3212
|
565 |
\medskip Infix syntax and constant names may be also specified
|
paulson@3485
|
566 |
independently. For example, consider this version of $\nand$:
|
wenzelm@3212
|
567 |
\begin{ttbox}
|
wenzelm@3212
|
568 |
consts nand :: [o,o] => o (infixl "~&" 35)
|
wenzelm@3212
|
569 |
\end{ttbox}
|
wenzelm@3212
|
570 |
|
lcp@310
|
571 |
\bigskip\index{mixfix declarations}
|
lcp@310
|
572 |
{\bf Mixfix} operators may have arbitrary context-free syntaxes. Let us
|
lcp@310
|
573 |
add a line to the constant declaration part:
|
lcp@284
|
574 |
\begin{ttbox}
|
clasohm@1387
|
575 |
If :: [o,o,o] => o ("if _ then _ else _")
|
lcp@105
|
576 |
\end{ttbox}
|
lcp@310
|
577 |
This declares a constant $If$ of type $[o,o,o] \To o$ with concrete syntax {\tt
|
paulson@5205
|
578 |
if~$P$ then~$Q$ else~$R$} as well as \texttt{If($P$,$Q$,$R$)}. Underscores
|
lcp@310
|
579 |
denote argument positions.
|
lcp@105
|
580 |
|
paulson@5205
|
581 |
The declaration above does not allow the \texttt{if}-\texttt{then}-{\tt
|
wenzelm@3103
|
582 |
else} construct to be printed split across several lines, even if it
|
wenzelm@3103
|
583 |
is too long to fit on one line. Pretty-printing information can be
|
wenzelm@3103
|
584 |
added to specify the layout of mixfix operators. For details, see
|
lcp@310
|
585 |
\iflabelundefined{Defining-Logics}%
|
lcp@310
|
586 |
{the {\it Reference Manual}, chapter `Defining Logics'}%
|
lcp@310
|
587 |
{Chap.\ts\ref{Defining-Logics}}.
|
lcp@310
|
588 |
|
lcp@310
|
589 |
Mixfix declarations can be annotated with priorities, just like
|
lcp@105
|
590 |
infixes. The example above is just a shorthand for
|
lcp@284
|
591 |
\begin{ttbox}
|
clasohm@1387
|
592 |
If :: [o,o,o] => o ("if _ then _ else _" [0,0,0] 1000)
|
lcp@105
|
593 |
\end{ttbox}
|
lcp@310
|
594 |
The numeric components determine priorities. The list of integers
|
lcp@310
|
595 |
defines, for each argument position, the minimal priority an expression
|
lcp@310
|
596 |
at that position must have. The final integer is the priority of the
|
lcp@105
|
597 |
construct itself. In the example above, any argument expression is
|
lcp@310
|
598 |
acceptable because priorities are non-negative, and conditionals may
|
lcp@310
|
599 |
appear everywhere because 1000 is the highest priority. On the other
|
lcp@310
|
600 |
hand, the declaration
|
lcp@284
|
601 |
\begin{ttbox}
|
clasohm@1387
|
602 |
If :: [o,o,o] => o ("if _ then _ else _" [100,0,0] 99)
|
lcp@105
|
603 |
\end{ttbox}
|
lcp@284
|
604 |
defines concrete syntax for a conditional whose first argument cannot have
|
paulson@5205
|
605 |
the form \texttt{if~$P$ then~$Q$ else~$R$} because it must have a priority
|
lcp@310
|
606 |
of at least~100. We may of course write
|
lcp@284
|
607 |
\begin{quote}\tt
|
lcp@284
|
608 |
if (if $P$ then $Q$ else $R$) then $S$ else $T$
|
lcp@156
|
609 |
\end{quote}
|
lcp@310
|
610 |
because expressions in parentheses have maximal priority.
|
lcp@105
|
611 |
|
lcp@105
|
612 |
Binary type constructors, like products and sums, may also be declared as
|
lcp@105
|
613 |
infixes. The type declaration below introduces a type constructor~$*$ with
|
lcp@105
|
614 |
infix notation $\alpha*\beta$, together with the mixfix notation
|
lcp@1084
|
615 |
${<}\_,\_{>}$ for pairs. We also see a rule declaration part.
|
lcp@310
|
616 |
\index{examples!of theories}\index{mixfix declarations}
|
lcp@105
|
617 |
\begin{ttbox}
|
lcp@105
|
618 |
Prod = FOL +
|
lcp@284
|
619 |
types ('a,'b) "*" (infixl 20)
|
lcp@105
|
620 |
arities "*" :: (term,term)term
|
lcp@105
|
621 |
consts fst :: "'a * 'b => 'a"
|
lcp@105
|
622 |
snd :: "'a * 'b => 'b"
|
lcp@105
|
623 |
Pair :: "['a,'b] => 'a * 'b" ("(1<_,/_>)")
|
lcp@105
|
624 |
rules fst "fst(<a,b>) = a"
|
lcp@105
|
625 |
snd "snd(<a,b>) = b"
|
lcp@105
|
626 |
end
|
lcp@105
|
627 |
\end{ttbox}
|
lcp@105
|
628 |
|
lcp@105
|
629 |
\begin{warn}
|
paulson@5205
|
630 |
The name of the type constructor is~\texttt{*} and not \texttt{op~*}, as
|
wenzelm@3103
|
631 |
it would be in the case of an infix constant. Only infix type
|
paulson@5205
|
632 |
constructors can have symbolic names like~\texttt{*}. General mixfix
|
paulson@5205
|
633 |
syntax for types may be introduced via appropriate \texttt{syntax}
|
wenzelm@3103
|
634 |
declarations.
|
lcp@105
|
635 |
\end{warn}
|
lcp@105
|
636 |
|
lcp@105
|
637 |
|
lcp@105
|
638 |
\subsection{Overloading}
|
lcp@105
|
639 |
\index{overloading}\index{examples!of theories}
|
lcp@105
|
640 |
The {\bf class declaration part} has the form
|
lcp@105
|
641 |
\begin{ttbox}
|
lcp@105
|
642 |
classes \(id@1\) < \(c@1\)
|
lcp@105
|
643 |
\vdots
|
lcp@105
|
644 |
\(id@n\) < \(c@n\)
|
lcp@105
|
645 |
\end{ttbox}
|
lcp@105
|
646 |
where $id@1$, \ldots, $id@n$ are identifiers and $c@1$, \ldots, $c@n$ are
|
lcp@105
|
647 |
existing classes. It declares each $id@i$ as a new class, a subclass
|
lcp@105
|
648 |
of~$c@i$. In the general case, an identifier may be declared to be a
|
lcp@105
|
649 |
subclass of $k$ existing classes:
|
lcp@105
|
650 |
\begin{ttbox}
|
lcp@105
|
651 |
\(id\) < \(c@1\), \ldots, \(c@k\)
|
lcp@105
|
652 |
\end{ttbox}
|
lcp@296
|
653 |
Type classes allow constants to be overloaded. As suggested in
|
lcp@307
|
654 |
\S\ref{polymorphic}, let us define the class $arith$ of arithmetic
|
lcp@296
|
655 |
types with the constants ${+} :: [\alpha,\alpha]\To \alpha$ and $0,1 {::}
|
lcp@296
|
656 |
\alpha$, for $\alpha{::}arith$. We introduce $arith$ as a subclass of
|
lcp@296
|
657 |
$term$ and add the three polymorphic constants of this class.
|
lcp@310
|
658 |
\index{examples!of theories}\index{constants!overloaded}
|
lcp@105
|
659 |
\begin{ttbox}
|
lcp@105
|
660 |
Arith = FOL +
|
lcp@105
|
661 |
classes arith < term
|
clasohm@1387
|
662 |
consts "0" :: 'a::arith ("0")
|
clasohm@1387
|
663 |
"1" :: 'a::arith ("1")
|
clasohm@1387
|
664 |
"+" :: ['a::arith,'a] => 'a (infixl 60)
|
lcp@105
|
665 |
end
|
lcp@105
|
666 |
\end{ttbox}
|
lcp@105
|
667 |
No rules are declared for these constants: we merely introduce their
|
lcp@105
|
668 |
names without specifying properties. On the other hand, classes
|
lcp@105
|
669 |
with rules make it possible to prove {\bf generic} theorems. Such
|
lcp@105
|
670 |
theorems hold for all instances, all types in that class.
|
lcp@105
|
671 |
|
lcp@105
|
672 |
We can now obtain distinct versions of the constants of $arith$ by
|
lcp@105
|
673 |
declaring certain types to be of class $arith$. For example, let us
|
lcp@105
|
674 |
declare the 0-place type constructors $bool$ and $nat$:
|
lcp@105
|
675 |
\index{examples!of theories}
|
lcp@105
|
676 |
\begin{ttbox}
|
lcp@105
|
677 |
BoolNat = Arith +
|
lcp@348
|
678 |
types bool nat
|
lcp@348
|
679 |
arities bool, nat :: arith
|
clasohm@1387
|
680 |
consts Suc :: nat=>nat
|
lcp@284
|
681 |
\ttbreak
|
lcp@105
|
682 |
rules add0 "0 + n = n::nat"
|
lcp@105
|
683 |
addS "Suc(m)+n = Suc(m+n)"
|
lcp@105
|
684 |
nat1 "1 = Suc(0)"
|
lcp@105
|
685 |
or0l "0 + x = x::bool"
|
lcp@105
|
686 |
or0r "x + 0 = x::bool"
|
lcp@105
|
687 |
or1l "1 + x = 1::bool"
|
lcp@105
|
688 |
or1r "x + 1 = 1::bool"
|
lcp@105
|
689 |
end
|
lcp@105
|
690 |
\end{ttbox}
|
lcp@105
|
691 |
Because $nat$ and $bool$ have class $arith$, we can use $0$, $1$ and $+$ at
|
lcp@105
|
692 |
either type. The type constraints in the axioms are vital. Without
|
paulson@14148
|
693 |
constraints, the $x$ in $1+x = 1$ (axiom \texttt{or1l})
|
paulson@14148
|
694 |
would have type $\alpha{::}arith$
|
lcp@105
|
695 |
and the axiom would hold for any type of class $arith$. This would
|
lcp@284
|
696 |
collapse $nat$ to a trivial type:
|
lcp@105
|
697 |
\[ Suc(1) = Suc(0+1) = Suc(0)+1 = 1+1 = 1! \]
|
lcp@105
|
698 |
|
lcp@296
|
699 |
|
lcp@296
|
700 |
\section{Theory example: the natural numbers}
|
lcp@296
|
701 |
|
lcp@296
|
702 |
We shall now work through a small example of formalized mathematics
|
lcp@105
|
703 |
demonstrating many of the theory extension features.
|
lcp@105
|
704 |
|
lcp@105
|
705 |
|
lcp@105
|
706 |
\subsection{Extending first-order logic with the natural numbers}
|
lcp@105
|
707 |
\index{examples!of theories}
|
lcp@105
|
708 |
|
lcp@284
|
709 |
Section\ts\ref{sec:logical-syntax} has formalized a first-order logic,
|
lcp@284
|
710 |
including a type~$nat$ and the constants $0::nat$ and $Suc::nat\To nat$.
|
lcp@284
|
711 |
Let us introduce the Peano axioms for mathematical induction and the
|
lcp@310
|
712 |
freeness of $0$ and~$Suc$:\index{axioms!Peano}
|
lcp@307
|
713 |
\[ \vcenter{\infer[(induct)]{P[n/x]}{P[0/x] & \infer*{P[Suc(x)/x]}{[P]}}}
|
lcp@105
|
714 |
\qquad \parbox{4.5cm}{provided $x$ is not free in any assumption except~$P$}
|
lcp@105
|
715 |
\]
|
lcp@105
|
716 |
\[ \infer[(Suc\_inject)]{m=n}{Suc(m)=Suc(n)} \qquad
|
lcp@105
|
717 |
\infer[(Suc\_neq\_0)]{R}{Suc(m)=0}
|
lcp@105
|
718 |
\]
|
lcp@105
|
719 |
Mathematical induction asserts that $P(n)$ is true, for any $n::nat$,
|
lcp@105
|
720 |
provided $P(0)$ holds and that $P(x)$ implies $P(Suc(x))$ for all~$x$.
|
lcp@105
|
721 |
Some authors express the induction step as $\forall x. P(x)\imp P(Suc(x))$.
|
lcp@105
|
722 |
To avoid making induction require the presence of other connectives, we
|
lcp@105
|
723 |
formalize mathematical induction as
|
lcp@105
|
724 |
$$ \List{P(0); \Forall x. P(x)\Imp P(Suc(x))} \Imp P(n). \eqno(induct) $$
|
lcp@105
|
725 |
|
lcp@105
|
726 |
\noindent
|
lcp@105
|
727 |
Similarly, to avoid expressing the other rules using~$\forall$, $\imp$
|
lcp@105
|
728 |
and~$\neg$, we take advantage of the meta-logic;\footnote
|
lcp@105
|
729 |
{On the other hand, the axioms $Suc(m)=Suc(n) \bimp m=n$
|
lcp@105
|
730 |
and $\neg(Suc(m)=0)$ are logically equivalent to those given, and work
|
lcp@105
|
731 |
better with Isabelle's simplifier.}
|
lcp@105
|
732 |
$(Suc\_neq\_0)$ is
|
lcp@105
|
733 |
an elimination rule for $Suc(m)=0$:
|
lcp@105
|
734 |
$$ Suc(m)=Suc(n) \Imp m=n \eqno(Suc\_inject) $$
|
lcp@105
|
735 |
$$ Suc(m)=0 \Imp R \eqno(Suc\_neq\_0) $$
|
lcp@105
|
736 |
|
lcp@105
|
737 |
\noindent
|
lcp@105
|
738 |
We shall also define a primitive recursion operator, $rec$. Traditionally,
|
lcp@105
|
739 |
primitive recursion takes a natural number~$a$ and a 2-place function~$f$,
|
lcp@105
|
740 |
and obeys the equations
|
lcp@105
|
741 |
\begin{eqnarray*}
|
lcp@105
|
742 |
rec(0,a,f) & = & a \\
|
lcp@105
|
743 |
rec(Suc(m),a,f) & = & f(m, rec(m,a,f))
|
lcp@105
|
744 |
\end{eqnarray*}
|
lcp@105
|
745 |
Addition, defined by $m+n \equiv rec(m,n,\lambda x\,y.Suc(y))$,
|
lcp@105
|
746 |
should satisfy
|
lcp@105
|
747 |
\begin{eqnarray*}
|
lcp@105
|
748 |
0+n & = & n \\
|
lcp@105
|
749 |
Suc(m)+n & = & Suc(m+n)
|
lcp@105
|
750 |
\end{eqnarray*}
|
lcp@296
|
751 |
Primitive recursion appears to pose difficulties: first-order logic has no
|
lcp@296
|
752 |
function-valued expressions. We again take advantage of the meta-logic,
|
lcp@296
|
753 |
which does have functions. We also generalise primitive recursion to be
|
lcp@105
|
754 |
polymorphic over any type of class~$term$, and declare the addition
|
lcp@105
|
755 |
function:
|
lcp@105
|
756 |
\begin{eqnarray*}
|
lcp@105
|
757 |
rec & :: & [nat, \alpha{::}term, [nat,\alpha]\To\alpha] \To\alpha \\
|
lcp@105
|
758 |
+ & :: & [nat,nat]\To nat
|
lcp@105
|
759 |
\end{eqnarray*}
|
lcp@105
|
760 |
|
lcp@105
|
761 |
|
lcp@105
|
762 |
\subsection{Declaring the theory to Isabelle}
|
lcp@105
|
763 |
\index{examples!of theories}
|
lcp@310
|
764 |
Let us create the theory \thydx{Nat} starting from theory~\verb$FOL$,
|
lcp@105
|
765 |
which contains only classical logic with no natural numbers. We declare
|
lcp@307
|
766 |
the 0-place type constructor $nat$ and the associated constants. Note that
|
lcp@307
|
767 |
the constant~0 requires a mixfix annotation because~0 is not a legal
|
lcp@307
|
768 |
identifier, and could not otherwise be written in terms:
|
lcp@310
|
769 |
\begin{ttbox}\index{mixfix declarations}
|
lcp@105
|
770 |
Nat = FOL +
|
lcp@284
|
771 |
types nat
|
lcp@105
|
772 |
arities nat :: term
|
clasohm@1387
|
773 |
consts "0" :: nat ("0")
|
clasohm@1387
|
774 |
Suc :: nat=>nat
|
clasohm@1387
|
775 |
rec :: [nat, 'a, [nat,'a]=>'a] => 'a
|
clasohm@1387
|
776 |
"+" :: [nat, nat] => nat (infixl 60)
|
lcp@296
|
777 |
rules Suc_inject "Suc(m)=Suc(n) ==> m=n"
|
lcp@105
|
778 |
Suc_neq_0 "Suc(m)=0 ==> R"
|
lcp@296
|
779 |
induct "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)"
|
lcp@105
|
780 |
rec_0 "rec(0,a,f) = a"
|
lcp@105
|
781 |
rec_Suc "rec(Suc(m), a, f) = f(m, rec(m,a,f))"
|
lcp@296
|
782 |
add_def "m+n == rec(m, n, \%x y. Suc(y))"
|
lcp@105
|
783 |
end
|
lcp@105
|
784 |
\end{ttbox}
|
paulson@5205
|
785 |
In axiom \texttt{add_def}, recall that \verb|%| stands for~$\lambda$.
|
paulson@5205
|
786 |
Loading this theory file creates the \ML\ structure \texttt{Nat}, which
|
wenzelm@3103
|
787 |
contains the theory and axioms.
|
lcp@296
|
788 |
|
lcp@296
|
789 |
\subsection{Proving some recursion equations}
|
paulson@5205
|
790 |
Theory \texttt{FOL/ex/Nat} contains proofs involving this theory of the
|
lcp@105
|
791 |
natural numbers. As a trivial example, let us derive recursion equations
|
lcp@105
|
792 |
for \verb$+$. Here is the zero case:
|
lcp@284
|
793 |
\begin{ttbox}
|
paulson@5205
|
794 |
Goalw [add_def] "0+n = n";
|
lcp@105
|
795 |
{\out Level 0}
|
lcp@105
|
796 |
{\out 0 + n = n}
|
lcp@284
|
797 |
{\out 1. rec(0,n,\%x y. Suc(y)) = n}
|
lcp@105
|
798 |
\ttbreak
|
lcp@105
|
799 |
by (resolve_tac [rec_0] 1);
|
lcp@105
|
800 |
{\out Level 1}
|
lcp@105
|
801 |
{\out 0 + n = n}
|
lcp@105
|
802 |
{\out No subgoals!}
|
wenzelm@3103
|
803 |
qed "add_0";
|
lcp@284
|
804 |
\end{ttbox}
|
lcp@105
|
805 |
And here is the successor case:
|
lcp@284
|
806 |
\begin{ttbox}
|
paulson@5205
|
807 |
Goalw [add_def] "Suc(m)+n = Suc(m+n)";
|
lcp@105
|
808 |
{\out Level 0}
|
lcp@105
|
809 |
{\out Suc(m) + n = Suc(m + n)}
|
lcp@284
|
810 |
{\out 1. rec(Suc(m),n,\%x y. Suc(y)) = Suc(rec(m,n,\%x y. Suc(y)))}
|
lcp@105
|
811 |
\ttbreak
|
lcp@105
|
812 |
by (resolve_tac [rec_Suc] 1);
|
lcp@105
|
813 |
{\out Level 1}
|
lcp@105
|
814 |
{\out Suc(m) + n = Suc(m + n)}
|
lcp@105
|
815 |
{\out No subgoals!}
|
wenzelm@3103
|
816 |
qed "add_Suc";
|
lcp@284
|
817 |
\end{ttbox}
|
lcp@105
|
818 |
The induction rule raises some complications, which are discussed next.
|
lcp@105
|
819 |
\index{theories!defining|)}
|
lcp@105
|
820 |
|
lcp@105
|
821 |
|
lcp@105
|
822 |
\section{Refinement with explicit instantiation}
|
lcp@310
|
823 |
\index{resolution!with instantiation}
|
lcp@310
|
824 |
\index{instantiation|(}
|
lcp@310
|
825 |
|
lcp@105
|
826 |
In order to employ mathematical induction, we need to refine a subgoal by
|
lcp@105
|
827 |
the rule~$(induct)$. The conclusion of this rule is $\Var{P}(\Var{n})$,
|
lcp@105
|
828 |
which is highly ambiguous in higher-order unification. It matches every
|
lcp@105
|
829 |
way that a formula can be regarded as depending on a subterm of type~$nat$.
|
lcp@105
|
830 |
To get round this problem, we could make the induction rule conclude
|
lcp@105
|
831 |
$\forall n.\Var{P}(n)$ --- but putting a subgoal into this form requires
|
lcp@105
|
832 |
refinement by~$(\forall E)$, which is equally hard!
|
lcp@105
|
833 |
|
paulson@5205
|
834 |
The tactic \texttt{res_inst_tac}, like \texttt{resolve_tac}, refines a subgoal by
|
lcp@105
|
835 |
a rule. But it also accepts explicit instantiations for the rule's
|
lcp@105
|
836 |
schematic variables.
|
lcp@105
|
837 |
\begin{description}
|
lcp@310
|
838 |
\item[\ttindex{res_inst_tac} {\it insts} {\it thm} {\it i}]
|
lcp@105
|
839 |
instantiates the rule {\it thm} with the instantiations {\it insts}, and
|
lcp@105
|
840 |
then performs resolution on subgoal~$i$.
|
lcp@105
|
841 |
|
lcp@310
|
842 |
\item[\ttindex{eres_inst_tac}]
|
lcp@310
|
843 |
and \ttindex{dres_inst_tac} are similar, but perform elim-resolution
|
lcp@105
|
844 |
and destruct-resolution, respectively.
|
lcp@105
|
845 |
\end{description}
|
lcp@105
|
846 |
The list {\it insts} consists of pairs $[(v@1,e@1), \ldots, (v@n,e@n)]$,
|
lcp@105
|
847 |
where $v@1$, \ldots, $v@n$ are names of schematic variables in the rule ---
|
lcp@307
|
848 |
with no leading question marks! --- and $e@1$, \ldots, $e@n$ are
|
lcp@105
|
849 |
expressions giving their instantiations. The expressions are type-checked
|
lcp@105
|
850 |
in the context of a particular subgoal: free variables receive the same
|
lcp@105
|
851 |
types as they have in the subgoal, and parameters may appear. Type
|
lcp@105
|
852 |
variable instantiations may appear in~{\it insts}, but they are seldom
|
paulson@5205
|
853 |
required: \texttt{res_inst_tac} instantiates type variables automatically
|
lcp@105
|
854 |
whenever the type of~$e@i$ is an instance of the type of~$\Var{v@i}$.
|
lcp@105
|
855 |
|
lcp@105
|
856 |
\subsection{A simple proof by induction}
|
lcp@310
|
857 |
\index{examples!of induction}
|
lcp@105
|
858 |
Let us prove that no natural number~$k$ equals its own successor. To
|
lcp@105
|
859 |
use~$(induct)$, we instantiate~$\Var{n}$ to~$k$; Isabelle finds a good
|
lcp@105
|
860 |
instantiation for~$\Var{P}$.
|
lcp@284
|
861 |
\begin{ttbox}
|
paulson@5205
|
862 |
Goal "~ (Suc(k) = k)";
|
lcp@105
|
863 |
{\out Level 0}
|
lcp@459
|
864 |
{\out Suc(k) ~= k}
|
lcp@459
|
865 |
{\out 1. Suc(k) ~= k}
|
lcp@105
|
866 |
\ttbreak
|
lcp@105
|
867 |
by (res_inst_tac [("n","k")] induct 1);
|
lcp@105
|
868 |
{\out Level 1}
|
lcp@459
|
869 |
{\out Suc(k) ~= k}
|
lcp@459
|
870 |
{\out 1. Suc(0) ~= 0}
|
lcp@459
|
871 |
{\out 2. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)}
|
lcp@284
|
872 |
\end{ttbox}
|
lcp@105
|
873 |
We should check that Isabelle has correctly applied induction. Subgoal~1
|
lcp@105
|
874 |
is the base case, with $k$ replaced by~0. Subgoal~2 is the inductive step,
|
lcp@105
|
875 |
with $k$ replaced by~$Suc(x)$ and with an induction hypothesis for~$x$.
|
lcp@310
|
876 |
The rest of the proof demonstrates~\tdx{notI}, \tdx{notE} and the
|
paulson@5205
|
877 |
other rules of theory \texttt{Nat}. The base case holds by~\ttindex{Suc_neq_0}:
|
lcp@284
|
878 |
\begin{ttbox}
|
lcp@105
|
879 |
by (resolve_tac [notI] 1);
|
lcp@105
|
880 |
{\out Level 2}
|
lcp@459
|
881 |
{\out Suc(k) ~= k}
|
lcp@105
|
882 |
{\out 1. Suc(0) = 0 ==> False}
|
lcp@459
|
883 |
{\out 2. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)}
|
lcp@105
|
884 |
\ttbreak
|
lcp@105
|
885 |
by (eresolve_tac [Suc_neq_0] 1);
|
lcp@105
|
886 |
{\out Level 3}
|
lcp@459
|
887 |
{\out Suc(k) ~= k}
|
lcp@459
|
888 |
{\out 1. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)}
|
lcp@284
|
889 |
\end{ttbox}
|
lcp@105
|
890 |
The inductive step holds by the contrapositive of~\ttindex{Suc_inject}.
|
lcp@284
|
891 |
Negation rules transform the subgoal into that of proving $Suc(x)=x$ from
|
lcp@284
|
892 |
$Suc(Suc(x)) = Suc(x)$:
|
lcp@284
|
893 |
\begin{ttbox}
|
lcp@105
|
894 |
by (resolve_tac [notI] 1);
|
lcp@105
|
895 |
{\out Level 4}
|
lcp@459
|
896 |
{\out Suc(k) ~= k}
|
lcp@459
|
897 |
{\out 1. !!x. [| Suc(x) ~= x; Suc(Suc(x)) = Suc(x) |] ==> False}
|
lcp@105
|
898 |
\ttbreak
|
lcp@105
|
899 |
by (eresolve_tac [notE] 1);
|
lcp@105
|
900 |
{\out Level 5}
|
lcp@459
|
901 |
{\out Suc(k) ~= k}
|
lcp@105
|
902 |
{\out 1. !!x. Suc(Suc(x)) = Suc(x) ==> Suc(x) = x}
|
lcp@105
|
903 |
\ttbreak
|
lcp@105
|
904 |
by (eresolve_tac [Suc_inject] 1);
|
lcp@105
|
905 |
{\out Level 6}
|
lcp@459
|
906 |
{\out Suc(k) ~= k}
|
lcp@105
|
907 |
{\out No subgoals!}
|
lcp@284
|
908 |
\end{ttbox}
|
lcp@105
|
909 |
|
lcp@105
|
910 |
|
paulson@5205
|
911 |
\subsection{An example of ambiguity in \texttt{resolve_tac}}
|
lcp@105
|
912 |
\index{examples!of induction}\index{unification!higher-order}
|
paulson@5205
|
913 |
If you try the example above, you may observe that \texttt{res_inst_tac} is
|
lcp@105
|
914 |
not actually needed. Almost by chance, \ttindex{resolve_tac} finds the right
|
lcp@105
|
915 |
instantiation for~$(induct)$ to yield the desired next state. With more
|
lcp@105
|
916 |
complex formulae, our luck fails.
|
lcp@284
|
917 |
\begin{ttbox}
|
paulson@5205
|
918 |
Goal "(k+m)+n = k+(m+n)";
|
lcp@105
|
919 |
{\out Level 0}
|
lcp@105
|
920 |
{\out k + m + n = k + (m + n)}
|
lcp@105
|
921 |
{\out 1. k + m + n = k + (m + n)}
|
lcp@105
|
922 |
\ttbreak
|
lcp@105
|
923 |
by (resolve_tac [induct] 1);
|
lcp@105
|
924 |
{\out Level 1}
|
lcp@105
|
925 |
{\out k + m + n = k + (m + n)}
|
lcp@105
|
926 |
{\out 1. k + m + n = 0}
|
lcp@105
|
927 |
{\out 2. !!x. k + m + n = x ==> k + m + n = Suc(x)}
|
lcp@284
|
928 |
\end{ttbox}
|
lcp@284
|
929 |
This proof requires induction on~$k$. The occurrence of~0 in subgoal~1
|
lcp@284
|
930 |
indicates that induction has been applied to the term~$k+(m+n)$; this
|
lcp@284
|
931 |
application is sound but will not lead to a proof here. Fortunately,
|
lcp@284
|
932 |
Isabelle can (lazily!) generate all the valid applications of induction.
|
lcp@284
|
933 |
The \ttindex{back} command causes backtracking to an alternative outcome of
|
lcp@284
|
934 |
the tactic.
|
lcp@284
|
935 |
\begin{ttbox}
|
lcp@105
|
936 |
back();
|
lcp@105
|
937 |
{\out Level 1}
|
lcp@105
|
938 |
{\out k + m + n = k + (m + n)}
|
lcp@105
|
939 |
{\out 1. k + m + n = k + 0}
|
lcp@105
|
940 |
{\out 2. !!x. k + m + n = k + x ==> k + m + n = k + Suc(x)}
|
lcp@284
|
941 |
\end{ttbox}
|
lcp@284
|
942 |
Now induction has been applied to~$m+n$. This is equally useless. Let us
|
lcp@284
|
943 |
call \ttindex{back} again.
|
lcp@284
|
944 |
\begin{ttbox}
|
lcp@105
|
945 |
back();
|
lcp@105
|
946 |
{\out Level 1}
|
lcp@105
|
947 |
{\out k + m + n = k + (m + n)}
|
lcp@105
|
948 |
{\out 1. k + m + 0 = k + (m + 0)}
|
lcp@284
|
949 |
{\out 2. !!x. k + m + x = k + (m + x) ==>}
|
lcp@284
|
950 |
{\out k + m + Suc(x) = k + (m + Suc(x))}
|
lcp@284
|
951 |
\end{ttbox}
|
lcp@105
|
952 |
Now induction has been applied to~$n$. What is the next alternative?
|
lcp@284
|
953 |
\begin{ttbox}
|
lcp@105
|
954 |
back();
|
lcp@105
|
955 |
{\out Level 1}
|
lcp@105
|
956 |
{\out k + m + n = k + (m + n)}
|
lcp@105
|
957 |
{\out 1. k + m + n = k + (m + 0)}
|
lcp@105
|
958 |
{\out 2. !!x. k + m + n = k + (m + x) ==> k + m + n = k + (m + Suc(x))}
|
lcp@284
|
959 |
\end{ttbox}
|
lcp@105
|
960 |
Inspecting subgoal~1 reveals that induction has been applied to just the
|
lcp@105
|
961 |
second occurrence of~$n$. This perfectly legitimate induction is useless
|
lcp@310
|
962 |
here.
|
lcp@310
|
963 |
|
lcp@310
|
964 |
The main goal admits fourteen different applications of induction. The
|
lcp@310
|
965 |
number is exponential in the size of the formula.
|
lcp@105
|
966 |
|
lcp@105
|
967 |
\subsection{Proving that addition is associative}
|
lcp@331
|
968 |
Let us invoke the induction rule properly, using~{\tt
|
lcp@310
|
969 |
res_inst_tac}. At the same time, we shall have a glimpse at Isabelle's
|
lcp@310
|
970 |
simplification tactics, which are described in
|
lcp@310
|
971 |
\iflabelundefined{simp-chap}%
|
lcp@310
|
972 |
{the {\em Reference Manual}}{Chap.\ts\ref{simp-chap}}.
|
lcp@105
|
973 |
|
lcp@310
|
974 |
\index{simplification}\index{examples!of simplification}
|
lcp@284
|
975 |
|
wenzelm@9695
|
976 |
Isabelle's simplification tactics repeatedly apply equations to a subgoal,
|
wenzelm@9695
|
977 |
perhaps proving it. For efficiency, the rewrite rules must be packaged into a
|
wenzelm@9695
|
978 |
{\bf simplification set},\index{simplification sets} or {\bf simpset}. We
|
wenzelm@9695
|
979 |
augment the implicit simpset of FOL with the equations proved in the previous
|
wenzelm@9695
|
980 |
section, namely $0+n=n$ and $\texttt{Suc}(m)+n=\texttt{Suc}(m+n)$:
|
lcp@284
|
981 |
\begin{ttbox}
|
wenzelm@3114
|
982 |
Addsimps [add_0, add_Suc];
|
lcp@284
|
983 |
\end{ttbox}
|
lcp@105
|
984 |
We state the goal for associativity of addition, and
|
lcp@105
|
985 |
use \ttindex{res_inst_tac} to invoke induction on~$k$:
|
lcp@284
|
986 |
\begin{ttbox}
|
paulson@5205
|
987 |
Goal "(k+m)+n = k+(m+n)";
|
lcp@105
|
988 |
{\out Level 0}
|
lcp@105
|
989 |
{\out k + m + n = k + (m + n)}
|
lcp@105
|
990 |
{\out 1. k + m + n = k + (m + n)}
|
lcp@105
|
991 |
\ttbreak
|
lcp@105
|
992 |
by (res_inst_tac [("n","k")] induct 1);
|
lcp@105
|
993 |
{\out Level 1}
|
lcp@105
|
994 |
{\out k + m + n = k + (m + n)}
|
lcp@105
|
995 |
{\out 1. 0 + m + n = 0 + (m + n)}
|
lcp@284
|
996 |
{\out 2. !!x. x + m + n = x + (m + n) ==>}
|
lcp@284
|
997 |
{\out Suc(x) + m + n = Suc(x) + (m + n)}
|
lcp@284
|
998 |
\end{ttbox}
|
lcp@105
|
999 |
The base case holds easily; both sides reduce to $m+n$. The
|
wenzelm@3114
|
1000 |
tactic~\ttindex{Simp_tac} rewrites with respect to the current
|
wenzelm@3114
|
1001 |
simplification set, applying the rewrite rules for addition:
|
lcp@284
|
1002 |
\begin{ttbox}
|
wenzelm@3114
|
1003 |
by (Simp_tac 1);
|
lcp@105
|
1004 |
{\out Level 2}
|
lcp@105
|
1005 |
{\out k + m + n = k + (m + n)}
|
lcp@284
|
1006 |
{\out 1. !!x. x + m + n = x + (m + n) ==>}
|
lcp@284
|
1007 |
{\out Suc(x) + m + n = Suc(x) + (m + n)}
|
lcp@284
|
1008 |
\end{ttbox}
|
lcp@331
|
1009 |
The inductive step requires rewriting by the equations for addition
|
paulson@14148
|
1010 |
and with the induction hypothesis, which is also an equation. The
|
wenzelm@3114
|
1011 |
tactic~\ttindex{Asm_simp_tac} rewrites using the implicit
|
wenzelm@3114
|
1012 |
simplification set and any useful assumptions:
|
lcp@284
|
1013 |
\begin{ttbox}
|
wenzelm@3114
|
1014 |
by (Asm_simp_tac 1);
|
lcp@105
|
1015 |
{\out Level 3}
|
lcp@105
|
1016 |
{\out k + m + n = k + (m + n)}
|
lcp@105
|
1017 |
{\out No subgoals!}
|
lcp@284
|
1018 |
\end{ttbox}
|
lcp@310
|
1019 |
\index{instantiation|)}
|
lcp@105
|
1020 |
|
lcp@105
|
1021 |
|
lcp@284
|
1022 |
\section{A Prolog interpreter}
|
lcp@105
|
1023 |
\index{Prolog interpreter|bold}
|
lcp@284
|
1024 |
To demonstrate the power of tacticals, let us construct a Prolog
|
lcp@105
|
1025 |
interpreter and execute programs involving lists.\footnote{To run these
|
paulson@5205
|
1026 |
examples, see the file \texttt{FOL/ex/Prolog.ML}.} The Prolog program
|
lcp@105
|
1027 |
consists of a theory. We declare a type constructor for lists, with an
|
lcp@105
|
1028 |
arity declaration to say that $(\tau)list$ is of class~$term$
|
lcp@105
|
1029 |
provided~$\tau$ is:
|
lcp@105
|
1030 |
\begin{eqnarray*}
|
lcp@105
|
1031 |
list & :: & (term)term
|
lcp@105
|
1032 |
\end{eqnarray*}
|
lcp@105
|
1033 |
We declare four constants: the empty list~$Nil$; the infix list
|
lcp@105
|
1034 |
constructor~{:}; the list concatenation predicate~$app$; the list reverse
|
lcp@284
|
1035 |
predicate~$rev$. (In Prolog, functions on lists are expressed as
|
lcp@105
|
1036 |
predicates.)
|
lcp@105
|
1037 |
\begin{eqnarray*}
|
lcp@105
|
1038 |
Nil & :: & \alpha list \\
|
lcp@105
|
1039 |
{:} & :: & [\alpha,\alpha list] \To \alpha list \\
|
lcp@105
|
1040 |
app & :: & [\alpha list,\alpha list,\alpha list] \To o \\
|
lcp@105
|
1041 |
rev & :: & [\alpha list,\alpha list] \To o
|
lcp@105
|
1042 |
\end{eqnarray*}
|
lcp@284
|
1043 |
The predicate $app$ should satisfy the Prolog-style rules
|
lcp@105
|
1044 |
\[ {app(Nil,ys,ys)} \qquad
|
lcp@105
|
1045 |
{app(xs,ys,zs) \over app(x:xs, ys, x:zs)} \]
|
lcp@105
|
1046 |
We define the naive version of $rev$, which calls~$app$:
|
lcp@105
|
1047 |
\[ {rev(Nil,Nil)} \qquad
|
lcp@105
|
1048 |
{rev(xs,ys)\quad app(ys, x:Nil, zs) \over
|
lcp@105
|
1049 |
rev(x:xs, zs)}
|
lcp@105
|
1050 |
\]
|
lcp@105
|
1051 |
|
lcp@105
|
1052 |
\index{examples!of theories}
|
lcp@310
|
1053 |
Theory \thydx{Prolog} extends first-order logic in order to make use
|
lcp@105
|
1054 |
of the class~$term$ and the type~$o$. The interpreter does not use the
|
paulson@5205
|
1055 |
rules of~\texttt{FOL}.
|
lcp@105
|
1056 |
\begin{ttbox}
|
lcp@105
|
1057 |
Prolog = FOL +
|
lcp@296
|
1058 |
types 'a list
|
lcp@105
|
1059 |
arities list :: (term)term
|
clasohm@1387
|
1060 |
consts Nil :: 'a list
|
clasohm@1387
|
1061 |
":" :: ['a, 'a list]=> 'a list (infixr 60)
|
clasohm@1387
|
1062 |
app :: ['a list, 'a list, 'a list] => o
|
clasohm@1387
|
1063 |
rev :: ['a list, 'a list] => o
|
lcp@105
|
1064 |
rules appNil "app(Nil,ys,ys)"
|
lcp@105
|
1065 |
appCons "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)"
|
lcp@105
|
1066 |
revNil "rev(Nil,Nil)"
|
lcp@105
|
1067 |
revCons "[| rev(xs,ys); app(ys,x:Nil,zs) |] ==> rev(x:xs,zs)"
|
lcp@105
|
1068 |
end
|
lcp@105
|
1069 |
\end{ttbox}
|
lcp@105
|
1070 |
\subsection{Simple executions}
|
lcp@284
|
1071 |
Repeated application of the rules solves Prolog goals. Let us
|
lcp@105
|
1072 |
append the lists $[a,b,c]$ and~$[d,e]$. As the rules are applied, the
|
paulson@5205
|
1073 |
answer builds up in~\texttt{?x}.
|
lcp@105
|
1074 |
\begin{ttbox}
|
paulson@5205
|
1075 |
Goal "app(a:b:c:Nil, d:e:Nil, ?x)";
|
lcp@105
|
1076 |
{\out Level 0}
|
lcp@105
|
1077 |
{\out app(a : b : c : Nil, d : e : Nil, ?x)}
|
lcp@105
|
1078 |
{\out 1. app(a : b : c : Nil, d : e : Nil, ?x)}
|
lcp@105
|
1079 |
\ttbreak
|
lcp@105
|
1080 |
by (resolve_tac [appNil,appCons] 1);
|
lcp@105
|
1081 |
{\out Level 1}
|
lcp@105
|
1082 |
{\out app(a : b : c : Nil, d : e : Nil, a : ?zs1)}
|
lcp@105
|
1083 |
{\out 1. app(b : c : Nil, d : e : Nil, ?zs1)}
|
lcp@105
|
1084 |
\ttbreak
|
lcp@105
|
1085 |
by (resolve_tac [appNil,appCons] 1);
|
lcp@105
|
1086 |
{\out Level 2}
|
lcp@105
|
1087 |
{\out app(a : b : c : Nil, d : e : Nil, a : b : ?zs2)}
|
lcp@105
|
1088 |
{\out 1. app(c : Nil, d : e : Nil, ?zs2)}
|
lcp@105
|
1089 |
\end{ttbox}
|
lcp@105
|
1090 |
At this point, the first two elements of the result are~$a$ and~$b$.
|
lcp@105
|
1091 |
\begin{ttbox}
|
lcp@105
|
1092 |
by (resolve_tac [appNil,appCons] 1);
|
lcp@105
|
1093 |
{\out Level 3}
|
lcp@105
|
1094 |
{\out app(a : b : c : Nil, d : e : Nil, a : b : c : ?zs3)}
|
lcp@105
|
1095 |
{\out 1. app(Nil, d : e : Nil, ?zs3)}
|
lcp@105
|
1096 |
\ttbreak
|
lcp@105
|
1097 |
by (resolve_tac [appNil,appCons] 1);
|
lcp@105
|
1098 |
{\out Level 4}
|
lcp@105
|
1099 |
{\out app(a : b : c : Nil, d : e : Nil, a : b : c : d : e : Nil)}
|
lcp@105
|
1100 |
{\out No subgoals!}
|
lcp@105
|
1101 |
\end{ttbox}
|
lcp@105
|
1102 |
|
lcp@284
|
1103 |
Prolog can run functions backwards. Which list can be appended
|
lcp@105
|
1104 |
with $[c,d]$ to produce $[a,b,c,d]$?
|
lcp@105
|
1105 |
Using \ttindex{REPEAT}, we find the answer at once, $[a,b]$:
|
lcp@105
|
1106 |
\begin{ttbox}
|
paulson@5205
|
1107 |
Goal "app(?x, c:d:Nil, a:b:c:d:Nil)";
|
lcp@105
|
1108 |
{\out Level 0}
|
lcp@105
|
1109 |
{\out app(?x, c : d : Nil, a : b : c : d : Nil)}
|
lcp@105
|
1110 |
{\out 1. app(?x, c : d : Nil, a : b : c : d : Nil)}
|
lcp@105
|
1111 |
\ttbreak
|
lcp@105
|
1112 |
by (REPEAT (resolve_tac [appNil,appCons] 1));
|
lcp@105
|
1113 |
{\out Level 1}
|
lcp@105
|
1114 |
{\out app(a : b : Nil, c : d : Nil, a : b : c : d : Nil)}
|
lcp@105
|
1115 |
{\out No subgoals!}
|
lcp@105
|
1116 |
\end{ttbox}
|
lcp@105
|
1117 |
|
lcp@105
|
1118 |
|
lcp@310
|
1119 |
\subsection{Backtracking}\index{backtracking!Prolog style}
|
lcp@296
|
1120 |
Prolog backtracking can answer questions that have multiple solutions.
|
lcp@296
|
1121 |
Which lists $x$ and $y$ can be appended to form the list $[a,b,c,d]$? This
|
lcp@296
|
1122 |
question has five solutions. Using \ttindex{REPEAT} to apply the rules, we
|
lcp@296
|
1123 |
quickly find the first solution, namely $x=[]$ and $y=[a,b,c,d]$:
|
lcp@105
|
1124 |
\begin{ttbox}
|
paulson@5205
|
1125 |
Goal "app(?x, ?y, a:b:c:d:Nil)";
|
lcp@105
|
1126 |
{\out Level 0}
|
lcp@105
|
1127 |
{\out app(?x, ?y, a : b : c : d : Nil)}
|
lcp@105
|
1128 |
{\out 1. app(?x, ?y, a : b : c : d : Nil)}
|
lcp@105
|
1129 |
\ttbreak
|
lcp@105
|
1130 |
by (REPEAT (resolve_tac [appNil,appCons] 1));
|
lcp@105
|
1131 |
{\out Level 1}
|
lcp@105
|
1132 |
{\out app(Nil, a : b : c : d : Nil, a : b : c : d : Nil)}
|
lcp@105
|
1133 |
{\out No subgoals!}
|
lcp@105
|
1134 |
\end{ttbox}
|
lcp@284
|
1135 |
Isabelle can lazily generate all the possibilities. The \ttindex{back}
|
lcp@284
|
1136 |
command returns the tactic's next outcome, namely $x=[a]$ and $y=[b,c,d]$:
|
lcp@105
|
1137 |
\begin{ttbox}
|
lcp@105
|
1138 |
back();
|
lcp@105
|
1139 |
{\out Level 1}
|
lcp@105
|
1140 |
{\out app(a : Nil, b : c : d : Nil, a : b : c : d : Nil)}
|
lcp@105
|
1141 |
{\out No subgoals!}
|
lcp@105
|
1142 |
\end{ttbox}
|
lcp@105
|
1143 |
The other solutions are generated similarly.
|
lcp@105
|
1144 |
\begin{ttbox}
|
lcp@105
|
1145 |
back();
|
lcp@105
|
1146 |
{\out Level 1}
|
lcp@105
|
1147 |
{\out app(a : b : Nil, c : d : Nil, a : b : c : d : Nil)}
|
lcp@105
|
1148 |
{\out No subgoals!}
|
lcp@105
|
1149 |
\ttbreak
|
lcp@105
|
1150 |
back();
|
lcp@105
|
1151 |
{\out Level 1}
|
lcp@105
|
1152 |
{\out app(a : b : c : Nil, d : Nil, a : b : c : d : Nil)}
|
lcp@105
|
1153 |
{\out No subgoals!}
|
lcp@105
|
1154 |
\ttbreak
|
lcp@105
|
1155 |
back();
|
lcp@105
|
1156 |
{\out Level 1}
|
lcp@105
|
1157 |
{\out app(a : b : c : d : Nil, Nil, a : b : c : d : Nil)}
|
lcp@105
|
1158 |
{\out No subgoals!}
|
lcp@105
|
1159 |
\end{ttbox}
|
lcp@105
|
1160 |
|
lcp@105
|
1161 |
|
lcp@105
|
1162 |
\subsection{Depth-first search}
|
lcp@105
|
1163 |
\index{search!depth-first}
|
lcp@105
|
1164 |
Now let us try $rev$, reversing a list.
|
paulson@5205
|
1165 |
Bundle the rules together as the \ML{} identifier \texttt{rules}. Naive
|
lcp@105
|
1166 |
reverse requires 120 inferences for this 14-element list, but the tactic
|
lcp@105
|
1167 |
terminates in a few seconds.
|
lcp@105
|
1168 |
\begin{ttbox}
|
paulson@5205
|
1169 |
Goal "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)";
|
lcp@105
|
1170 |
{\out Level 0}
|
lcp@105
|
1171 |
{\out rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil, ?w)}
|
lcp@284
|
1172 |
{\out 1. rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil,}
|
lcp@284
|
1173 |
{\out ?w)}
|
lcp@284
|
1174 |
\ttbreak
|
lcp@105
|
1175 |
val rules = [appNil,appCons,revNil,revCons];
|
lcp@105
|
1176 |
\ttbreak
|
lcp@105
|
1177 |
by (REPEAT (resolve_tac rules 1));
|
lcp@105
|
1178 |
{\out Level 1}
|
lcp@105
|
1179 |
{\out rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil,}
|
lcp@105
|
1180 |
{\out n : m : l : k : j : i : h : g : f : e : d : c : b : a : Nil)}
|
lcp@105
|
1181 |
{\out No subgoals!}
|
lcp@105
|
1182 |
\end{ttbox}
|
lcp@105
|
1183 |
We may execute $rev$ backwards. This, too, should reverse a list. What
|
lcp@105
|
1184 |
is the reverse of $[a,b,c]$?
|
lcp@105
|
1185 |
\begin{ttbox}
|
paulson@5205
|
1186 |
Goal "rev(?x, a:b:c:Nil)";
|
lcp@105
|
1187 |
{\out Level 0}
|
lcp@105
|
1188 |
{\out rev(?x, a : b : c : Nil)}
|
lcp@105
|
1189 |
{\out 1. rev(?x, a : b : c : Nil)}
|
lcp@105
|
1190 |
\ttbreak
|
lcp@105
|
1191 |
by (REPEAT (resolve_tac rules 1));
|
lcp@105
|
1192 |
{\out Level 1}
|
lcp@105
|
1193 |
{\out rev(?x1 : Nil, a : b : c : Nil)}
|
lcp@105
|
1194 |
{\out 1. app(Nil, ?x1 : Nil, a : b : c : Nil)}
|
lcp@105
|
1195 |
\end{ttbox}
|
lcp@105
|
1196 |
The tactic has failed to find a solution! It reached a dead end at
|
lcp@331
|
1197 |
subgoal~1: there is no~$\Var{x@1}$ such that [] appended with~$[\Var{x@1}]$
|
lcp@105
|
1198 |
equals~$[a,b,c]$. Backtracking explores other outcomes.
|
lcp@105
|
1199 |
\begin{ttbox}
|
lcp@105
|
1200 |
back();
|
lcp@105
|
1201 |
{\out Level 1}
|
lcp@105
|
1202 |
{\out rev(?x1 : a : Nil, a : b : c : Nil)}
|
lcp@105
|
1203 |
{\out 1. app(Nil, ?x1 : Nil, b : c : Nil)}
|
lcp@105
|
1204 |
\end{ttbox}
|
lcp@105
|
1205 |
This too is a dead end, but the next outcome is successful.
|
lcp@105
|
1206 |
\begin{ttbox}
|
lcp@105
|
1207 |
back();
|
lcp@105
|
1208 |
{\out Level 1}
|
lcp@105
|
1209 |
{\out rev(c : b : a : Nil, a : b : c : Nil)}
|
lcp@105
|
1210 |
{\out No subgoals!}
|
lcp@105
|
1211 |
\end{ttbox}
|
lcp@310
|
1212 |
\ttindex{REPEAT} goes wrong because it is only a repetition tactical, not a
|
paulson@5205
|
1213 |
search tactical. \texttt{REPEAT} stops when it cannot continue, regardless of
|
lcp@310
|
1214 |
which state is reached. The tactical \ttindex{DEPTH_FIRST} searches for a
|
lcp@310
|
1215 |
satisfactory state, as specified by an \ML{} predicate. Below,
|
lcp@105
|
1216 |
\ttindex{has_fewer_prems} specifies that the proof state should have no
|
lcp@310
|
1217 |
subgoals.
|
lcp@105
|
1218 |
\begin{ttbox}
|
lcp@105
|
1219 |
val prolog_tac = DEPTH_FIRST (has_fewer_prems 1)
|
lcp@105
|
1220 |
(resolve_tac rules 1);
|
lcp@105
|
1221 |
\end{ttbox}
|
lcp@284
|
1222 |
Since Prolog uses depth-first search, this tactic is a (slow!)
|
lcp@296
|
1223 |
Prolog interpreter. We return to the start of the proof using
|
paulson@5205
|
1224 |
\ttindex{choplev}, and apply \texttt{prolog_tac}:
|
lcp@105
|
1225 |
\begin{ttbox}
|
lcp@105
|
1226 |
choplev 0;
|
lcp@105
|
1227 |
{\out Level 0}
|
lcp@105
|
1228 |
{\out rev(?x, a : b : c : Nil)}
|
lcp@105
|
1229 |
{\out 1. rev(?x, a : b : c : Nil)}
|
lcp@105
|
1230 |
\ttbreak
|
paulson@14148
|
1231 |
by prolog_tac;
|
lcp@105
|
1232 |
{\out Level 1}
|
lcp@105
|
1233 |
{\out rev(c : b : a : Nil, a : b : c : Nil)}
|
lcp@105
|
1234 |
{\out No subgoals!}
|
lcp@105
|
1235 |
\end{ttbox}
|
paulson@5205
|
1236 |
Let us try \texttt{prolog_tac} on one more example, containing four unknowns:
|
lcp@105
|
1237 |
\begin{ttbox}
|
paulson@5205
|
1238 |
Goal "rev(a:?x:c:?y:Nil, d:?z:b:?u)";
|
lcp@105
|
1239 |
{\out Level 0}
|
lcp@105
|
1240 |
{\out rev(a : ?x : c : ?y : Nil, d : ?z : b : ?u)}
|
lcp@105
|
1241 |
{\out 1. rev(a : ?x : c : ?y : Nil, d : ?z : b : ?u)}
|
lcp@105
|
1242 |
\ttbreak
|
lcp@105
|
1243 |
by prolog_tac;
|
lcp@105
|
1244 |
{\out Level 1}
|
lcp@105
|
1245 |
{\out rev(a : b : c : d : Nil, d : c : b : a : Nil)}
|
lcp@105
|
1246 |
{\out No subgoals!}
|
lcp@105
|
1247 |
\end{ttbox}
|
lcp@284
|
1248 |
Although Isabelle is much slower than a Prolog system, Isabelle
|
lcp@156
|
1249 |
tactics can exploit logic programming techniques.
|
lcp@156
|
1250 |
|