author | wenzelm |
Mon, 25 Mar 2019 17:21:26 +0100 | |
changeset 69981 | 3dced198b9ec |
parent 69597 | ff784d5a5bfb |
child 72315 | 8162ca81ea8a |
permissions | -rw-r--r-- |
47269 | 1 |
(*<*) |
2 |
theory Logic |
|
3 |
imports LaTeXsugar |
|
4 |
begin |
|
5 |
(*>*) |
|
67406 | 6 |
text\<open> |
47269 | 7 |
\vspace{-5ex} |
51436 | 8 |
\section{Formulas} |
47269 | 9 |
|
47711 | 10 |
The core syntax of formulas (\textit{form} below) |
47720 | 11 |
provides the standard logical constructs, in decreasing order of precedence: |
47269 | 12 |
\[ |
13 |
\begin{array}{rcl} |
|
14 |
||
15 |
\mathit{form} & ::= & |
|
69505 | 16 |
\<open>(form)\<close> ~\mid~ |
69597 | 17 |
\<^const>\<open>True\<close> ~\mid~ |
18 |
\<^const>\<open>False\<close> ~\mid~ |
|
19 |
\<^prop>\<open>term = term\<close>\\ |
|
20 |
&\mid& \<^prop>\<open>\<not> form\<close>\index{$HOL4@\isasymnot} ~\mid~ |
|
21 |
\<^prop>\<open>form \<and> form\<close>\index{$HOL0@\isasymand} ~\mid~ |
|
22 |
\<^prop>\<open>form \<or> form\<close>\index{$HOL1@\isasymor} ~\mid~ |
|
23 |
\<^prop>\<open>form \<longrightarrow> form\<close>\index{$HOL2@\isasymlongrightarrow}\\ |
|
24 |
&\mid& \<^prop>\<open>\<forall>x. form\<close>\index{$HOL6@\isasymforall} ~\mid~ \<^prop>\<open>\<exists>x. form\<close>\index{$HOL7@\isasymexists} |
|
47269 | 25 |
\end{array} |
26 |
\] |
|
47711 | 27 |
Terms are the ones we have seen all along, built from constants, variables, |
69505 | 28 |
function application and \<open>\<lambda>\<close>-abstraction, including all the syntactic |
29 |
sugar like infix symbols, \<open>if\<close>, \<open>case\<close>, etc. |
|
47269 | 30 |
\begin{warn} |
69505 | 31 |
Remember that formulas are simply terms of type \<open>bool\<close>. Hence |
32 |
\<open>=\<close> also works for formulas. Beware that \<open>=\<close> has a higher |
|
69597 | 33 |
precedence than the other logical operators. Hence \<^prop>\<open>s = t \<and> A\<close> means |
34 |
\<open>(s = t) \<and> A\<close>, and \<^prop>\<open>A\<and>B = B\<and>A\<close> means \<open>A \<and> (B = B) \<and> A\<close>. |
|
47269 | 35 |
Logical equivalence can also be written with |
69505 | 36 |
\<open>\<longleftrightarrow>\<close> instead of \<open>=\<close>, where \<open>\<longleftrightarrow>\<close> has the same low |
37 |
precedence as \<open>\<longrightarrow>\<close>. Hence \<open>A \<and> B \<longleftrightarrow> B \<and> A\<close> really means |
|
38 |
\<open>(A \<and> B) \<longleftrightarrow> (B \<and> A)\<close>. |
|
47269 | 39 |
\end{warn} |
40 |
\begin{warn} |
|
41 |
Quantifiers need to be enclosed in parentheses if they are nested within |
|
69505 | 42 |
other constructs (just like \<open>if\<close>, \<open>case\<close> and \<open>let\<close>). |
47269 | 43 |
\end{warn} |
52404 | 44 |
The most frequent logical symbols and their ASCII representations are shown |
45 |
in Fig.~\ref{fig:log-symbols}. |
|
46 |
\begin{figure} |
|
47269 | 47 |
\begin{center} |
48 |
\begin{tabular}{l@ {\qquad}l@ {\qquad}l} |
|
69505 | 49 |
\<open>\<forall>\<close> & \xsymbol{forall} & \texttt{ALL}\\ |
50 |
\<open>\<exists>\<close> & \xsymbol{exists} & \texttt{EX}\\ |
|
51 |
\<open>\<lambda>\<close> & \xsymbol{lambda} & \texttt{\%}\\ |
|
52 |
\<open>\<longrightarrow>\<close> & \texttt{-{}->}\\ |
|
53 |
\<open>\<longleftrightarrow>\<close> & \texttt{<->}\\ |
|
54 |
\<open>\<and>\<close> & \texttt{/\char`\\} & \texttt{\&}\\ |
|
55 |
\<open>\<or>\<close> & \texttt{\char`\\/} & \texttt{|}\\ |
|
56 |
\<open>\<not>\<close> & \xsymbol{not} & \texttt{\char`~}\\ |
|
57 |
\<open>\<noteq>\<close> & \xsymbol{noteq} & \texttt{\char`~=} |
|
47269 | 58 |
\end{tabular} |
59 |
\end{center} |
|
52404 | 60 |
\caption{Logical symbols and their ASCII forms} |
61 |
\label{fig:log-symbols} |
|
62 |
\end{figure} |
|
63 |
The first column shows the symbols, the other columns ASCII representations. |
|
64 |
The \texttt{\char`\\}\texttt{<...>} form is always converted into the symbolic form |
|
65 |
by the Isabelle interfaces, the treatment of the other ASCII forms |
|
66 |
depends on the interface. The ASCII forms \texttt{/\char`\\} and |
|
67 |
\texttt{\char`\\/} |
|
68 |
are special in that they are merely keyboard shortcuts for the interface and |
|
69 |
not logical symbols by themselves. |
|
47269 | 70 |
\begin{warn} |
69505 | 71 |
The implication \<open>\<Longrightarrow>\<close> is part of the Isabelle framework. It structures |
47711 | 72 |
theorems and proof states, separating assumptions from conclusions. |
69505 | 73 |
The implication \<open>\<longrightarrow>\<close> is part of the logic HOL and can occur inside the |
47269 | 74 |
formulas that make up the assumptions and conclusion. |
69505 | 75 |
Theorems should be of the form \<open>\<lbrakk> A\<^sub>1; \<dots>; A\<^sub>n \<rbrakk> \<Longrightarrow> A\<close>, |
76 |
not \<open>A\<^sub>1 \<and> \<dots> \<and> A\<^sub>n \<longrightarrow> A\<close>. Both are logically equivalent |
|
47269 | 77 |
but the first one works better when using the theorem in further proofs. |
78 |
\end{warn} |
|
79 |
||
51436 | 80 |
\section{Sets} |
51038 | 81 |
\label{sec:Sets} |
47269 | 82 |
|
69597 | 83 |
Sets of elements of type \<^typ>\<open>'a\<close> have type \<^typ>\<open>'a set\<close>\index{set@\<open>set\<close>}. |
47711 | 84 |
They can be finite or infinite. Sets come with the usual notation: |
47269 | 85 |
\begin{itemize} |
69597 | 86 |
\item \indexed{\<^term>\<open>{}\<close>}{$IMP042},\quad \<open>{e\<^sub>1,\<dots>,e\<^sub>n}\<close> |
87 |
\item \<^prop>\<open>e \<in> A\<close>\index{$HOLSet0@\isasymin},\quad \<^prop>\<open>A \<subseteq> B\<close>\index{$HOLSet2@\isasymsubseteq} |
|
88 |
\item \<^term>\<open>A \<union> B\<close>\index{$HOLSet4@\isasymunion},\quad \<^term>\<open>A \<inter> B\<close>\index{$HOLSet5@\isasyminter},\quad \<^term>\<open>A - B\<close>,\quad \<^term>\<open>-A\<close> |
|
47269 | 89 |
\end{itemize} |
69597 | 90 |
(where \<^term>\<open>A-B\<close> and \<open>-A\<close> are set difference and complement) |
91 |
and much more. \<^const>\<open>UNIV\<close> is the set of all elements of some type. |
|
55348 | 92 |
Set comprehension\index{set comprehension} is written |
69597 | 93 |
\<^term>\<open>{x. P}\<close>\index{$IMP042@\<^term>\<open>{x. P}\<close>} rather than \<open>{x | P}\<close>. |
47269 | 94 |
\begin{warn} |
69597 | 95 |
In \<^term>\<open>{x. P}\<close> the \<open>x\<close> must be a variable. Set comprehension |
69505 | 96 |
involving a proper term \<open>t\<close> must be written |
97 |
\noquotes{@{term[source] "{t | x y. P}"}}\index{$IMP042@\<open>{t |x. P}\<close>}, |
|
98 |
where \<open>x y\<close> are those free variables in \<open>t\<close> |
|
99 |
that occur in \<open>P\<close>. |
|
69597 | 100 |
This is just a shorthand for \<^term>\<open>{v. \<exists>x y. v = t \<and> P}\<close>, where |
101 |
\<open>v\<close> is a new variable. For example, \<^term>\<open>{x+y|x. x \<in> A}\<close> |
|
49615 | 102 |
is short for \noquotes{@{term[source]"{v. \<exists>x. v = x+y \<and> x \<in> A}"}}. |
47269 | 103 |
\end{warn} |
104 |
||
105 |
Here are the ASCII representations of the mathematical symbols: |
|
106 |
\begin{center} |
|
107 |
\begin{tabular}{l@ {\quad}l@ {\quad}l} |
|
69505 | 108 |
\<open>\<in>\<close> & \texttt{\char`\\\char`\<in>} & \texttt{:}\\ |
109 |
\<open>\<subseteq>\<close> & \texttt{\char`\\\char`\<subseteq>} & \texttt{<=}\\ |
|
110 |
\<open>\<union>\<close> & \texttt{\char`\\\char`\<union>} & \texttt{Un}\\ |
|
111 |
\<open>\<inter>\<close> & \texttt{\char`\\\char`\<inter>} & \texttt{Int} |
|
47269 | 112 |
\end{tabular} |
113 |
\end{center} |
|
69597 | 114 |
Sets also allow bounded quantifications \<^prop>\<open>\<forall>x \<in> A. P\<close> and |
115 |
\<^prop>\<open>\<exists>x \<in> A. P\<close>. |
|
47269 | 116 |
|
69505 | 117 |
For the more ambitious, there are also \<open>\<Union>\<close>\index{$HOLSet6@\isasymUnion} |
118 |
and \<open>\<Inter>\<close>\index{$HOLSet7@\isasymInter}: |
|
52404 | 119 |
\begin{center} |
120 |
@{thm Union_eq} \qquad @{thm Inter_eq} |
|
121 |
\end{center} |
|
69505 | 122 |
The ASCII forms of \<open>\<Union>\<close> are \texttt{\char`\\\char`\<Union>} and \texttt{Union}, |
123 |
those of \<open>\<Inter>\<close> are \texttt{\char`\\\char`\<Inter>} and \texttt{Inter}. |
|
52404 | 124 |
There are also indexed unions and intersections: |
51784 | 125 |
\begin{center} |
68800 | 126 |
@{thm[eta_contract=false] UNION_eq} \\ @{thm[eta_contract=false] INTER_eq} |
52404 | 127 |
\end{center} |
128 |
The ASCII forms are \ \texttt{UN x:A.~B} \ and \ \texttt{INT x:A. B} \ |
|
129 |
where \texttt{x} may occur in \texttt{B}. |
|
58605 | 130 |
If \texttt{A} is \texttt{UNIV} you can write \ \texttt{UN x.~B} \ and \ \texttt{INT x. B}. |
52404 | 131 |
|
132 |
Some other frequently useful functions on sets are the following: |
|
133 |
\begin{center} |
|
134 |
\begin{tabular}{l@ {\quad}l} |
|
69597 | 135 |
@{const_typ set}\index{set@\<^const>\<open>set\<close>} & converts a list to the set of its elements\\ |
136 |
@{const_typ finite}\index{finite@\<^const>\<open>finite\<close>} & is true iff its argument is finite\\ |
|
137 |
\noquotes{@{term[source] "card :: 'a set \<Rightarrow> nat"}}\index{card@\<^const>\<open>card\<close>} & is the cardinality of a finite set\\ |
|
69505 | 138 |
& and is \<open>0\<close> for all infinite sets\\ |
69597 | 139 |
@{thm image_def}\index{$IMP042@\<^term>\<open>f ` A\<close>} & is the image of a function over a set |
51784 | 140 |
\end{tabular} |
141 |
\end{center} |
|
58620 | 142 |
See @{cite "Nipkow-Main"} for the wealth of further predefined functions in theory |
69597 | 143 |
\<^theory>\<open>Main\<close>. |
51784 | 144 |
|
54214 | 145 |
|
54436 | 146 |
\subsection*{Exercises} |
54214 | 147 |
|
148 |
\exercise |
|
149 |
Start from the data type of binary trees defined earlier: |
|
67406 | 150 |
\<close> |
54214 | 151 |
|
152 |
datatype 'a tree = Tip | Node "'a tree" 'a "'a tree" |
|
153 |
||
67406 | 154 |
text\<open> |
69597 | 155 |
Define a function \<open>set ::\<close> \<^typ>\<open>'a tree \<Rightarrow> 'a set\<close> |
54214 | 156 |
that returns the elements in a tree and a function |
69597 | 157 |
\<open>ord ::\<close> \<^typ>\<open>int tree \<Rightarrow> bool\<close> |
158 |
that tests if an \<^typ>\<open>int tree\<close> is ordered. |
|
54214 | 159 |
|
69597 | 160 |
Define a function \<open>ins\<close> that inserts an element into an ordered \<^typ>\<open>int tree\<close> |
54214 | 161 |
while maintaining the order of the tree. If the element is already in the tree, the |
69505 | 162 |
same tree should be returned. Prove correctness of \<open>ins\<close>: |
69597 | 163 |
\<^prop>\<open>set(ins x t) = {x} \<union> set t\<close> and \<^prop>\<open>ord t \<Longrightarrow> ord(ins i t)\<close>. |
54214 | 164 |
\endexercise |
165 |
||
166 |
||
52361 | 167 |
\section{Proof Automation} |
47269 | 168 |
|
69505 | 169 |
So far we have only seen \<open>simp\<close> and \indexed{\<open>auto\<close>}{auto}: Both perform |
47269 | 170 |
rewriting, both can also prove linear arithmetic facts (no multiplication), |
69505 | 171 |
and \<open>auto\<close> is also able to prove simple logical or set-theoretic goals: |
67406 | 172 |
\<close> |
47269 | 173 |
|
174 |
lemma "\<forall>x. \<exists>y. x = y" |
|
175 |
by auto |
|
176 |
||
177 |
lemma "A \<subseteq> B \<inter> C \<Longrightarrow> A \<subseteq> B \<union> C" |
|
178 |
by auto |
|
179 |
||
67406 | 180 |
text\<open>where |
47269 | 181 |
\begin{quote} |
182 |
\isacom{by} \textit{proof-method} |
|
183 |
\end{quote} |
|
184 |
is short for |
|
185 |
\begin{quote} |
|
186 |
\isacom{apply} \textit{proof-method}\\ |
|
187 |
\isacom{done} |
|
188 |
\end{quote} |
|
69505 | 189 |
The key characteristics of both \<open>simp\<close> and \<open>auto\<close> are |
47269 | 190 |
\begin{itemize} |
59568 | 191 |
\item They show you where they got stuck, giving you an idea how to continue. |
47269 | 192 |
\item They perform the obvious steps but are highly incomplete. |
193 |
\end{itemize} |
|
55317 | 194 |
A proof method is \conceptnoidx{complete} if it can prove all true formulas. |
47269 | 195 |
There is no complete proof method for HOL, not even in theory. |
196 |
Hence all our proof methods only differ in how incomplete they are. |
|
197 |
||
69505 | 198 |
A proof method that is still incomplete but tries harder than \<open>auto\<close> is |
199 |
\indexed{\<open>fastforce\<close>}{fastforce}. It either succeeds or fails, it acts on the first |
|
200 |
subgoal only, and it can be modified like \<open>auto\<close>, e.g., |
|
201 |
with \<open>simp add\<close>. Here is a typical example of what \<open>fastforce\<close> |
|
47269 | 202 |
can do: |
67406 | 203 |
\<close> |
47269 | 204 |
|
205 |
lemma "\<lbrakk> \<forall>xs \<in> A. \<exists>ys. xs = ys @ ys; us \<in> A \<rbrakk> |
|
206 |
\<Longrightarrow> \<exists>n. length us = n+n" |
|
207 |
by fastforce |
|
208 |
||
69505 | 209 |
text\<open>This lemma is out of reach for \<open>auto\<close> because of the |
210 |
quantifiers. Even \<open>fastforce\<close> fails when the quantifier structure |
|
211 |
becomes more complicated. In a few cases, its slow version \<open>force\<close> |
|
212 |
succeeds where \<open>fastforce\<close> fails. |
|
47269 | 213 |
|
69505 | 214 |
The method of choice for complex logical goals is \indexed{\<open>blast\<close>}{blast}. In the |
215 |
following example, \<open>T\<close> and \<open>A\<close> are two binary predicates. It |
|
216 |
is shown that if \<open>T\<close> is total, \<open>A\<close> is antisymmetric and \<open>T\<close> is |
|
217 |
a subset of \<open>A\<close>, then \<open>A\<close> is a subset of \<open>T\<close>: |
|
67406 | 218 |
\<close> |
47269 | 219 |
|
220 |
lemma |
|
221 |
"\<lbrakk> \<forall>x y. T x y \<or> T y x; |
|
222 |
\<forall>x y. A x y \<and> A y x \<longrightarrow> x = y; |
|
223 |
\<forall>x y. T x y \<longrightarrow> A x y \<rbrakk> |
|
224 |
\<Longrightarrow> \<forall>x y. A x y \<longrightarrow> T x y" |
|
225 |
by blast |
|
226 |
||
67406 | 227 |
text\<open> |
47269 | 228 |
We leave it to the reader to figure out why this lemma is true. |
69505 | 229 |
Method \<open>blast\<close> |
47269 | 230 |
\begin{itemize} |
231 |
\item is (in principle) a complete proof procedure for first-order formulas, |
|
232 |
a fragment of HOL. In practice there is a search bound. |
|
233 |
\item does no rewriting and knows very little about equality. |
|
234 |
\item covers logic, sets and relations. |
|
235 |
\item either succeeds or fails. |
|
236 |
\end{itemize} |
|
237 |
Because of its strength in logic and sets and its weakness in equality reasoning, it complements the earlier proof methods. |
|
238 |
||
239 |
||
55348 | 240 |
\subsection{\concept{Sledgehammer}} |
47269 | 241 |
|
242 |
Command \isacom{sledgehammer} calls a number of external automatic |
|
243 |
theorem provers (ATPs) that run for up to 30 seconds searching for a |
|
244 |
proof. Some of these ATPs are part of the Isabelle installation, others are |
|
245 |
queried over the internet. If successful, a proof command is generated and can |
|
246 |
be inserted into your proof. The biggest win of \isacom{sledgehammer} is |
|
247 |
that it will take into account the whole lemma library and you do not need to |
|
67406 | 248 |
feed in any lemma explicitly. For example,\<close> |
47269 | 249 |
|
250 |
lemma "\<lbrakk> xs @ ys = ys @ xs; length xs = length ys \<rbrakk> \<Longrightarrow> xs = ys" |
|
251 |
||
67406 | 252 |
txt\<open>cannot be solved by any of the standard proof methods, but |
253 |
\isacom{sledgehammer} finds the following proof:\<close> |
|
47269 | 254 |
|
255 |
by (metis append_eq_conv_conj) |
|
256 |
||
67406 | 257 |
text\<open>We do not explain how the proof was found but what this command |
47269 | 258 |
means. For a start, Isabelle does not trust external tools (and in particular |
259 |
not the translations from Isabelle's logic to those tools!) |
|
69505 | 260 |
and insists on a proof that it can check. This is what \indexed{\<open>metis\<close>}{metis} does. |
58605 | 261 |
It is given a list of lemmas and tries to find a proof using just those lemmas |
69505 | 262 |
(and pure logic). In contrast to using \<open>simp\<close> and friends who know a lot of |
263 |
lemmas already, using \<open>metis\<close> manually is tedious because one has |
|
47269 | 264 |
to find all the relevant lemmas first. But that is precisely what |
265 |
\isacom{sledgehammer} does for us. |
|
266 |
In this case lemma @{thm[source]append_eq_conv_conj} alone suffices: |
|
267 |
@{thm[display] append_eq_conv_conj} |
|
268 |
We leave it to the reader to figure out why this lemma suffices to prove |
|
69597 | 269 |
the above lemma, even without any knowledge of what the functions \<^const>\<open>take\<close> |
270 |
and \<^const>\<open>drop\<close> do. Keep in mind that the variables in the two lemmas |
|
47269 | 271 |
are independent of each other, despite the same names, and that you can |
272 |
substitute arbitrary values for the free variables in a lemma. |
|
273 |
||
274 |
Just as for the other proof methods we have seen, there is no guarantee that |
|
275 |
\isacom{sledgehammer} will find a proof if it exists. Nor is |
|
276 |
\isacom{sledgehammer} superior to the other proof methods. They are |
|
69505 | 277 |
incomparable. Therefore it is recommended to apply \<open>simp\<close> or \<open>auto\<close> before invoking \isacom{sledgehammer} on what is left. |
47269 | 278 |
|
51436 | 279 |
\subsection{Arithmetic} |
47269 | 280 |
|
69505 | 281 |
By arithmetic formulas we mean formulas involving variables, numbers, \<open>+\<close>, \<open>-\<close>, \<open>=\<close>, \<open><\<close>, \<open>\<le>\<close> and the usual logical |
282 |
connectives \<open>\<not>\<close>, \<open>\<and>\<close>, \<open>\<or>\<close>, \<open>\<longrightarrow>\<close>, |
|
283 |
\<open>\<longleftrightarrow>\<close>. Strictly speaking, this is known as \concept{linear arithmetic} |
|
47269 | 284 |
because it does not involve multiplication, although multiplication with |
69505 | 285 |
numbers, e.g., \<open>2*n\<close>, is allowed. Such formulas can be proved by |
286 |
\indexed{\<open>arith\<close>}{arith}: |
|
67406 | 287 |
\<close> |
47269 | 288 |
|
289 |
lemma "\<lbrakk> (a::nat) \<le> x + b; 2*x < c \<rbrakk> \<Longrightarrow> 2*a + 1 \<le> 2*b + c" |
|
290 |
by arith |
|
291 |
||
69505 | 292 |
text\<open>In fact, \<open>auto\<close> and \<open>simp\<close> can prove many linear |
47269 | 293 |
arithmetic formulas already, like the one above, by calling a weak but fast |
69505 | 294 |
version of \<open>arith\<close>. Hence it is usually not necessary to invoke |
295 |
\<open>arith\<close> explicitly. |
|
47269 | 296 |
|
69597 | 297 |
The above example involves natural numbers, but integers (type \<^typ>\<open>int\<close>) |
69505 | 298 |
and real numbers (type \<open>real\<close>) are supported as well. As are a number |
69597 | 299 |
of further operators like \<^const>\<open>min\<close> and \<^const>\<open>max\<close>. On \<^typ>\<open>nat\<close> and |
300 |
\<^typ>\<open>int\<close>, \<open>arith\<close> can even prove theorems with quantifiers in them, |
|
47269 | 301 |
but we will not enlarge on that here. |
302 |
||
303 |
||
52361 | 304 |
\subsection{Trying Them All} |
47727 | 305 |
|
306 |
If you want to try all of the above automatic proof methods you simply type |
|
307 |
\begin{isabelle} |
|
308 |
\isacom{try} |
|
309 |
\end{isabelle} |
|
63414 | 310 |
There is also a lightweight variant \isacom{try0} that does not call |
311 |
sledgehammer. If desired, specific simplification and introduction rules |
|
312 |
can be added: |
|
47727 | 313 |
\begin{isabelle} |
69505 | 314 |
\isacom{try0} \<open>simp: \<dots> intro: \<dots>\<close> |
47727 | 315 |
\end{isabelle} |
316 |
||
52361 | 317 |
\section{Single Step Proofs} |
47269 | 318 |
|
319 |
Although automation is nice, it often fails, at least initially, and you need |
|
69505 | 320 |
to find out why. When \<open>fastforce\<close> or \<open>blast\<close> simply fail, you have |
47269 | 321 |
no clue why. At this point, the stepwise |
69505 | 322 |
application of proof rules may be necessary. For example, if \<open>blast\<close> |
69597 | 323 |
fails on \<^prop>\<open>A \<and> B\<close>, you want to attack the two |
69505 | 324 |
conjuncts \<open>A\<close> and \<open>B\<close> separately. This can |
47269 | 325 |
be achieved by applying \emph{conjunction introduction} |
69505 | 326 |
\[ @{thm[mode=Rule,show_question_marks]conjI}\ \<open>conjI\<close> |
47269 | 327 |
\] |
328 |
to the proof state. We will now examine the details of this process. |
|
329 |
||
52361 | 330 |
\subsection{Instantiating Unknowns} |
47269 | 331 |
|
332 |
We had briefly mentioned earlier that after proving some theorem, |
|
69505 | 333 |
Isabelle replaces all free variables \<open>x\<close> by so called \conceptidx{unknowns}{unknown} |
334 |
\<open>?x\<close>. We can see this clearly in rule @{thm[source] conjI}. |
|
47269 | 335 |
These unknowns can later be instantiated explicitly or implicitly: |
336 |
\begin{itemize} |
|
69505 | 337 |
\item By hand, using \indexed{\<open>of\<close>}{of}. |
338 |
The expression \<open>conjI[of "a=b" "False"]\<close> |
|
47269 | 339 |
instantiates the unknowns in @{thm[source] conjI} from left to right with the |
69505 | 340 |
two formulas \<open>a=b\<close> and \<open>False\<close>, yielding the rule |
63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63414
diff
changeset
|
341 |
@{thm[display,mode=Rule,margin=100]conjI[of "a=b" False]} |
47269 | 342 |
|
69505 | 343 |
In general, \<open>th[of string\<^sub>1 \<dots> string\<^sub>n]\<close> instantiates |
344 |
the unknowns in the theorem \<open>th\<close> from left to right with the terms |
|
345 |
\<open>string\<^sub>1\<close> to \<open>string\<^sub>n\<close>. |
|
47269 | 346 |
|
55317 | 347 |
\item By unification. \conceptidx{Unification}{unification} is the process of making two |
47269 | 348 |
terms syntactically equal by suitable instantiations of unknowns. For example, |
69597 | 349 |
unifying \<open>?P \<and> ?Q\<close> with \mbox{\<^prop>\<open>a=b \<and> False\<close>} instantiates |
350 |
\<open>?P\<close> with \<^prop>\<open>a=b\<close> and \<open>?Q\<close> with \<^prop>\<open>False\<close>. |
|
47269 | 351 |
\end{itemize} |
352 |
We need not instantiate all unknowns. If we want to skip a particular one we |
|
69505 | 353 |
can write \<open>_\<close> instead, for example \<open>conjI[of _ "False"]\<close>. |
354 |
Unknowns can also be instantiated by name using \indexed{\<open>where\<close>}{where}, for example |
|
355 |
\<open>conjI[where ?P = "a=b"\<close> \isacom{and} \<open>?Q = "False"]\<close>. |
|
47269 | 356 |
|
357 |
||
52361 | 358 |
\subsection{Rule Application} |
47269 | 359 |
|
55317 | 360 |
\conceptidx{Rule application}{rule application} means applying a rule backwards to a proof state. |
47269 | 361 |
For example, applying rule @{thm[source]conjI} to a proof state |
362 |
\begin{quote} |
|
69505 | 363 |
\<open>1. \<dots> \<Longrightarrow> A \<and> B\<close> |
47269 | 364 |
\end{quote} |
365 |
results in two subgoals, one for each premise of @{thm[source]conjI}: |
|
366 |
\begin{quote} |
|
69505 | 367 |
\<open>1. \<dots> \<Longrightarrow> A\<close>\\ |
368 |
\<open>2. \<dots> \<Longrightarrow> B\<close> |
|
47269 | 369 |
\end{quote} |
69505 | 370 |
In general, the application of a rule \<open>\<lbrakk> A\<^sub>1; \<dots>; A\<^sub>n \<rbrakk> \<Longrightarrow> A\<close> |
371 |
to a subgoal \mbox{\<open>\<dots> \<Longrightarrow> C\<close>} proceeds in two steps: |
|
47269 | 372 |
\begin{enumerate} |
373 |
\item |
|
69505 | 374 |
Unify \<open>A\<close> and \<open>C\<close>, thus instantiating the unknowns in the rule. |
47269 | 375 |
\item |
69505 | 376 |
Replace the subgoal \<open>C\<close> with \<open>n\<close> new subgoals \<open>A\<^sub>1\<close> to \<open>A\<^sub>n\<close>. |
47269 | 377 |
\end{enumerate} |
69505 | 378 |
This is the command to apply rule \<open>xyz\<close>: |
47269 | 379 |
\begin{quote} |
69505 | 380 |
\isacom{apply}\<open>(rule xyz)\<close>\index{rule@\<open>rule\<close>} |
47269 | 381 |
\end{quote} |
69505 | 382 |
This is also called \concept{backchaining} with rule \<open>xyz\<close>. |
47269 | 383 |
|
52361 | 384 |
\subsection{Introduction Rules} |
47269 | 385 |
|
386 |
Conjunction introduction (@{thm[source] conjI}) is one example of a whole |
|
55317 | 387 |
class of rules known as \conceptidx{introduction rules}{introduction rule}. They explain under which |
47269 | 388 |
premises some logical construct can be introduced. Here are some further |
389 |
useful introduction rules: |
|
390 |
\[ |
|
69505 | 391 |
\inferrule*[right=\mbox{\<open>impI\<close>}]{\mbox{\<open>?P \<Longrightarrow> ?Q\<close>}}{\mbox{\<open>?P \<longrightarrow> ?Q\<close>}} |
47269 | 392 |
\qquad |
69505 | 393 |
\inferrule*[right=\mbox{\<open>allI\<close>}]{\mbox{\<open>\<And>x. ?P x\<close>}}{\mbox{\<open>\<forall>x. ?P x\<close>}} |
47269 | 394 |
\] |
395 |
\[ |
|
69505 | 396 |
\inferrule*[right=\mbox{\<open>iffI\<close>}]{\mbox{\<open>?P \<Longrightarrow> ?Q\<close>} \\ \mbox{\<open>?Q \<Longrightarrow> ?P\<close>}} |
397 |
{\mbox{\<open>?P = ?Q\<close>}} |
|
47269 | 398 |
\] |
399 |
These rules are part of the logical system of \concept{natural deduction} |
|
58620 | 400 |
(e.g., @{cite HuthRyan}). Although we intentionally de-emphasize the basic rules |
47269 | 401 |
of logic in favour of automatic proof methods that allow you to take bigger |
402 |
steps, these rules are helpful in locating where and why automation fails. |
|
403 |
When applied backwards, these rules decompose the goal: |
|
404 |
\begin{itemize} |
|
405 |
\item @{thm[source] conjI} and @{thm[source]iffI} split the goal into two subgoals, |
|
406 |
\item @{thm[source] impI} moves the left-hand side of a HOL implication into the list of assumptions, |
|
69505 | 407 |
\item and @{thm[source] allI} removes a \<open>\<forall>\<close> by turning the quantified variable into a fixed local variable of the subgoal. |
47269 | 408 |
\end{itemize} |
409 |
Isabelle knows about these and a number of other introduction rules. |
|
410 |
The command |
|
411 |
\begin{quote} |
|
69505 | 412 |
\isacom{apply} \<open>rule\<close>\index{rule@\<open>rule\<close>} |
47269 | 413 |
\end{quote} |
414 |
automatically selects the appropriate rule for the current subgoal. |
|
415 |
||
416 |
You can also turn your own theorems into introduction rules by giving them |
|
69505 | 417 |
the \indexed{\<open>intro\<close>}{intro} attribute, analogous to the \<open>simp\<close> attribute. In |
418 |
that case \<open>blast\<close>, \<open>fastforce\<close> and (to a limited extent) \<open>auto\<close> will automatically backchain with those theorems. The \<open>intro\<close> |
|
47269 | 419 |
attribute should be used with care because it increases the search space and |
47711 | 420 |
can lead to nontermination. Sometimes it is better to use it only in |
69505 | 421 |
specific calls of \<open>blast\<close> and friends. For example, |
69597 | 422 |
@{thm[source] le_trans}, transitivity of \<open>\<le>\<close> on type \<^typ>\<open>nat\<close>, |
47269 | 423 |
is not an introduction rule by default because of the disastrous effect |
424 |
on the search space, but can be useful in specific situations: |
|
67406 | 425 |
\<close> |
47269 | 426 |
|
427 |
lemma "\<lbrakk> (a::nat) \<le> b; b \<le> c; c \<le> d; d \<le> e \<rbrakk> \<Longrightarrow> a \<le> e" |
|
428 |
by(blast intro: le_trans) |
|
429 |
||
67406 | 430 |
text\<open> |
69505 | 431 |
Of course this is just an example and could be proved by \<open>arith\<close>, too. |
47269 | 432 |
|
52361 | 433 |
\subsection{Forward Proof} |
47269 | 434 |
\label{sec:forward-proof} |
435 |
||
436 |
Forward proof means deriving new theorems from old theorems. We have already |
|
69505 | 437 |
seen a very simple form of forward proof: the \<open>of\<close> operator for |
438 |
instantiating unknowns in a theorem. The big brother of \<open>of\<close> is |
|
69597 | 439 |
\indexed{\<open>OF\<close>}{OF} for applying one theorem to others. Given a theorem \<^prop>\<open>A \<Longrightarrow> B\<close> called |
69505 | 440 |
\<open>r\<close> and a theorem \<open>A'\<close> called \<open>r'\<close>, the theorem \<open>r[OF r']\<close> is the result of applying \<open>r\<close> to \<open>r'\<close>, where \<open>r\<close> should be viewed as a function taking a theorem \<open>A\<close> and returning |
441 |
\<open>B\<close>. More precisely, \<open>A\<close> and \<open>A'\<close> are unified, thus |
|
442 |
instantiating the unknowns in \<open>B\<close>, and the result is the instantiated |
|
443 |
\<open>B\<close>. Of course, unification may also fail. |
|
47269 | 444 |
\begin{warn} |
445 |
Application of rules to other rules operates in the forward direction: from |
|
446 |
the premises to the conclusion of the rule; application of rules to proof |
|
447 |
states operates in the backward direction, from the conclusion to the |
|
448 |
premises. |
|
449 |
\end{warn} |
|
450 |
||
69505 | 451 |
In general \<open>r\<close> can be of the form \<open>\<lbrakk> A\<^sub>1; \<dots>; A\<^sub>n \<rbrakk> \<Longrightarrow> A\<close> |
452 |
and there can be multiple argument theorems \<open>r\<^sub>1\<close> to \<open>r\<^sub>m\<close> |
|
453 |
(with \<open>m \<le> n\<close>), in which case \<open>r[OF r\<^sub>1 \<dots> r\<^sub>m]\<close> is obtained |
|
454 |
by unifying and thus proving \<open>A\<^sub>i\<close> with \<open>r\<^sub>i\<close>, \<open>i = 1\<dots>m\<close>. |
|
47269 | 455 |
Here is an example, where @{thm[source]refl} is the theorem |
456 |
@{thm[show_question_marks] refl}: |
|
67406 | 457 |
\<close> |
47269 | 458 |
|
459 |
thm conjI[OF refl[of "a"] refl[of "b"]] |
|
460 |
||
67406 | 461 |
text\<open>yields the theorem @{thm conjI[OF refl[of "a"] refl[of "b"]]}. |
47269 | 462 |
The command \isacom{thm} merely displays the result. |
463 |
||
464 |
Forward reasoning also makes sense in connection with proof states. |
|
69505 | 465 |
Therefore \<open>blast\<close>, \<open>fastforce\<close> and \<open>auto\<close> support a modifier |
466 |
\<open>dest\<close> which instructs the proof method to use certain rules in a |
|
467 |
forward fashion. If \<open>r\<close> is of the form \mbox{\<open>A \<Longrightarrow> B\<close>}, the modifier |
|
468 |
\mbox{\<open>dest: r\<close>}\index{dest@\<open>dest:\<close>} |
|
469 |
allows proof search to reason forward with \<open>r\<close>, i.e., |
|
470 |
to replace an assumption \<open>A'\<close>, where \<open>A'\<close> unifies with \<open>A\<close>, |
|
471 |
with the correspondingly instantiated \<open>B\<close>. For example, @{thm[source,show_question_marks] Suc_leD} is the theorem \mbox{@{thm Suc_leD}}, which works well for forward reasoning: |
|
67406 | 472 |
\<close> |
47269 | 473 |
|
474 |
lemma "Suc(Suc(Suc a)) \<le> b \<Longrightarrow> a \<le> b" |
|
475 |
by(blast dest: Suc_leD) |
|
476 |
||
67406 | 477 |
text\<open>In this particular example we could have backchained with |
47269 | 478 |
@{thm[source] Suc_leD}, too, but because the premise is more complicated than the conclusion this can easily lead to nontermination. |
479 |
||
54212 | 480 |
%\subsection{Finding Theorems} |
481 |
% |
|
482 |
%Command \isacom{find{\isacharunderscorekeyword}theorems} searches for specific theorems in the current |
|
483 |
%theory. Search criteria include pattern matching on terms and on names. |
|
58620 | 484 |
%For details see the Isabelle/Isar Reference Manual~@{cite IsarRef}. |
54212 | 485 |
%\bigskip |
47727 | 486 |
|
47269 | 487 |
\begin{warn} |
488 |
To ease readability we will drop the question marks |
|
489 |
in front of unknowns from now on. |
|
490 |
\end{warn} |
|
491 |
||
47727 | 492 |
|
52361 | 493 |
\section{Inductive Definitions} |
55361 | 494 |
\label{sec:inductive-defs}\index{inductive definition|(} |
47269 | 495 |
|
496 |
Inductive definitions are the third important definition facility, after |
|
47711 | 497 |
datatypes and recursive function. |
52782 | 498 |
\ifsem |
47711 | 499 |
In fact, they are the key construct in the |
47269 | 500 |
definition of operational semantics in the second part of the book. |
52782 | 501 |
\fi |
47269 | 502 |
|
52361 | 503 |
\subsection{An Example: Even Numbers} |
47269 | 504 |
\label{sec:Logic:even} |
505 |
||
506 |
Here is a simple example of an inductively defined predicate: |
|
507 |
\begin{itemize} |
|
508 |
\item 0 is even |
|
509 |
\item If $n$ is even, so is $n+2$. |
|
510 |
\end{itemize} |
|
511 |
The operative word ``inductive'' means that these are the only even numbers. |
|
69505 | 512 |
In Isabelle we give the two rules the names \<open>ev0\<close> and \<open>evSS\<close> |
47269 | 513 |
and write |
67406 | 514 |
\<close> |
47269 | 515 |
|
516 |
inductive ev :: "nat \<Rightarrow> bool" where |
|
517 |
ev0: "ev 0" | |
|
518 |
evSS: (*<*)"ev n \<Longrightarrow> ev (Suc(Suc n))"(*>*) |
|
67406 | 519 |
text_raw\<open>@{prop[source]"ev n \<Longrightarrow> ev (n + 2)"}\<close> |
47269 | 520 |
|
67406 | 521 |
text\<open>To get used to inductive definitions, we will first prove a few |
69597 | 522 |
properties of \<^const>\<open>ev\<close> informally before we descend to the Isabelle level. |
47269 | 523 |
|
69597 | 524 |
How do we prove that some number is even, e.g., \<^prop>\<open>ev 4\<close>? Simply by combining the defining rules for \<^const>\<open>ev\<close>: |
47269 | 525 |
\begin{quote} |
69505 | 526 |
\<open>ev 0 \<Longrightarrow> ev (0 + 2) \<Longrightarrow> ev((0 + 2) + 2) = ev 4\<close> |
47269 | 527 |
\end{quote} |
528 |
||
55361 | 529 |
\subsubsection{Rule Induction}\index{rule induction|(} |
47269 | 530 |
|
531 |
Showing that all even numbers have some property is more complicated. For |
|
532 |
example, let us prove that the inductive definition of even numbers agrees |
|
67406 | 533 |
with the following recursive one:\<close> |
47269 | 534 |
|
58962 | 535 |
fun evn :: "nat \<Rightarrow> bool" where |
536 |
"evn 0 = True" | |
|
537 |
"evn (Suc 0) = False" | |
|
538 |
"evn (Suc(Suc n)) = evn n" |
|
47269 | 539 |
|
69597 | 540 |
text\<open>We prove \<^prop>\<open>ev m \<Longrightarrow> evn m\<close>. That is, we |
541 |
assume \<^prop>\<open>ev m\<close> and by induction on the form of its derivation |
|
542 |
prove \<^prop>\<open>evn m\<close>. There are two cases corresponding to the two rules |
|
543 |
for \<^const>\<open>ev\<close>: |
|
47269 | 544 |
\begin{description} |
545 |
\item[Case @{thm[source]ev0}:] |
|
69597 | 546 |
\<^prop>\<open>ev m\<close> was derived by rule \<^prop>\<open>ev 0\<close>: \\ |
547 |
\<open>\<Longrightarrow>\<close> \<^prop>\<open>m=(0::nat)\<close> \<open>\<Longrightarrow>\<close> \<open>evn m = evn 0 = True\<close> |
|
47269 | 548 |
\item[Case @{thm[source]evSS}:] |
69597 | 549 |
\<^prop>\<open>ev m\<close> was derived by rule \<^prop>\<open>ev n \<Longrightarrow> ev(n+2)\<close>: \\ |
550 |
\<open>\<Longrightarrow>\<close> \<^prop>\<open>m=n+(2::nat)\<close> and by induction hypothesis \<^prop>\<open>evn n\<close>\\ |
|
69505 | 551 |
\<open>\<Longrightarrow>\<close> \<open>evn m = evn(n + 2) = evn n = True\<close> |
47269 | 552 |
\end{description} |
553 |
||
554 |
What we have just seen is a special case of \concept{rule induction}. |
|
555 |
Rule induction applies to propositions of this form |
|
556 |
\begin{quote} |
|
69597 | 557 |
\<^prop>\<open>ev n \<Longrightarrow> P n\<close> |
47269 | 558 |
\end{quote} |
69597 | 559 |
That is, we want to prove a property \<^prop>\<open>P n\<close> |
560 |
for all even \<open>n\<close>. But if we assume \<^prop>\<open>ev n\<close>, then there must be |
|
47269 | 561 |
some derivation of this assumption using the two defining rules for |
69597 | 562 |
\<^const>\<open>ev\<close>. That is, we must prove |
47269 | 563 |
\begin{description} |
69597 | 564 |
\item[Case @{thm[source]ev0}:] \<^prop>\<open>P(0::nat)\<close> |
565 |
\item[Case @{thm[source]evSS}:] \<^prop>\<open>\<lbrakk> ev n; P n \<rbrakk> \<Longrightarrow> P(n + 2::nat)\<close> |
|
47269 | 566 |
\end{description} |
567 |
The corresponding rule is called @{thm[source] ev.induct} and looks like this: |
|
568 |
\[ |
|
569 |
\inferrule{ |
|
570 |
\mbox{@{thm (prem 1) ev.induct[of "n"]}}\\ |
|
571 |
\mbox{@{thm (prem 2) ev.induct}}\\ |
|
69597 | 572 |
\mbox{\<^prop>\<open>!!n. \<lbrakk> ev n; P n \<rbrakk> \<Longrightarrow> P(n+2)\<close>}} |
47269 | 573 |
{\mbox{@{thm (concl) ev.induct[of "n"]}}} |
574 |
\] |
|
69597 | 575 |
The first premise \<^prop>\<open>ev n\<close> enforces that this rule can only be applied |
69505 | 576 |
in situations where we know that \<open>n\<close> is even. |
47269 | 577 |
|
69597 | 578 |
Note that in the induction step we may not just assume \<^prop>\<open>P n\<close> but also |
579 |
\mbox{\<^prop>\<open>ev n\<close>}, which is simply the premise of rule @{thm[source] |
|
580 |
evSS}. Here is an example where the local assumption \<^prop>\<open>ev n\<close> comes in |
|
581 |
handy: we prove \<^prop>\<open>ev m \<Longrightarrow> ev(m - 2)\<close> by induction on \<^prop>\<open>ev m\<close>. |
|
582 |
Case @{thm[source]ev0} requires us to prove \<^prop>\<open>ev(0 - 2)\<close>, which follows |
|
583 |
from \<^prop>\<open>ev 0\<close> because \<^prop>\<open>0 - 2 = (0::nat)\<close> on type \<^typ>\<open>nat\<close>. In |
|
584 |
case @{thm[source]evSS} we have \mbox{\<^prop>\<open>m = n+(2::nat)\<close>} and may assume |
|
585 |
\<^prop>\<open>ev n\<close>, which implies \<^prop>\<open>ev (m - 2)\<close> because \<open>m - 2 = (n + |
|
69505 | 586 |
2) - 2 = n\<close>. We did not need the induction hypothesis at all for this proof (it |
69597 | 587 |
is just a case analysis of which rule was used) but having \<^prop>\<open>ev n\<close> |
56989 | 588 |
at our disposal in case @{thm[source]evSS} was essential. |
47711 | 589 |
This case analysis of rules is also called ``rule inversion'' |
47269 | 590 |
and is discussed in more detail in \autoref{ch:Isar}. |
591 |
||
592 |
\subsubsection{In Isabelle} |
|
593 |
||
594 |
Let us now recast the above informal proofs in Isabelle. For a start, |
|
69597 | 595 |
we use \<^const>\<open>Suc\<close> terms instead of numerals in rule @{thm[source]evSS}: |
47269 | 596 |
@{thm[display] evSS} |
69505 | 597 |
This avoids the difficulty of unifying \<open>n+2\<close> with some numeral, |
47269 | 598 |
which is not automatic. |
599 |
||
69597 | 600 |
The simplest way to prove \<^prop>\<open>ev(Suc(Suc(Suc(Suc 0))))\<close> is in a forward |
69505 | 601 |
direction: \<open>evSS[OF evSS[OF ev0]]\<close> yields the theorem @{thm evSS[OF |
47269 | 602 |
evSS[OF ev0]]}. Alternatively, you can also prove it as a lemma in backwards |
603 |
fashion. Although this is more verbose, it allows us to demonstrate how each |
|
67406 | 604 |
rule application changes the proof state:\<close> |
47269 | 605 |
|
606 |
lemma "ev(Suc(Suc(Suc(Suc 0))))" |
|
67406 | 607 |
txt\<open> |
47269 | 608 |
@{subgoals[display,indent=0,goals_limit=1]} |
67406 | 609 |
\<close> |
47269 | 610 |
apply(rule evSS) |
67406 | 611 |
txt\<open> |
47269 | 612 |
@{subgoals[display,indent=0,goals_limit=1]} |
67406 | 613 |
\<close> |
47269 | 614 |
apply(rule evSS) |
67406 | 615 |
txt\<open> |
47269 | 616 |
@{subgoals[display,indent=0,goals_limit=1]} |
67406 | 617 |
\<close> |
47269 | 618 |
apply(rule ev0) |
619 |
done |
|
620 |
||
67406 | 621 |
text\<open>\indent |
47269 | 622 |
Rule induction is applied by giving the induction rule explicitly via the |
69505 | 623 |
\<open>rule:\<close> modifier:\index{inductionrule@\<open>induction ... rule:\<close>}\<close> |
47269 | 624 |
|
58962 | 625 |
lemma "ev m \<Longrightarrow> evn m" |
47269 | 626 |
apply(induction rule: ev.induct) |
627 |
by(simp_all) |
|
628 |
||
67406 | 629 |
text\<open>Both cases are automatic. Note that if there are multiple assumptions |
69597 | 630 |
of the form \<^prop>\<open>ev t\<close>, method \<open>induction\<close> will induct on the leftmost |
47269 | 631 |
one. |
632 |
||
633 |
As a bonus, we also prove the remaining direction of the equivalence of |
|
69597 | 634 |
\<^const>\<open>ev\<close> and \<^const>\<open>evn\<close>: |
67406 | 635 |
\<close> |
47269 | 636 |
|
58962 | 637 |
lemma "evn n \<Longrightarrow> ev n" |
638 |
apply(induction n rule: evn.induct) |
|
47269 | 639 |
|
69505 | 640 |
txt\<open>This is a proof by computation induction on \<open>n\<close> (see |
47269 | 641 |
\autoref{sec:recursive-funs}) that sets up three subgoals corresponding to |
69597 | 642 |
the three equations for \<^const>\<open>evn\<close>: |
47269 | 643 |
@{subgoals[display,indent=0]} |
69597 | 644 |
The first and third subgoals follow with @{thm[source]ev0} and @{thm[source]evSS}, and the second subgoal is trivially true because \<^prop>\<open>evn(Suc 0)\<close> is \<^const>\<open>False\<close>: |
67406 | 645 |
\<close> |
47269 | 646 |
|
647 |
by (simp_all add: ev0 evSS) |
|
648 |
||
69597 | 649 |
text\<open>The rules for \<^const>\<open>ev\<close> make perfect simplification and introduction |
47269 | 650 |
rules because their premises are always smaller than the conclusion. It |
651 |
makes sense to turn them into simplification and introduction rules |
|
55348 | 652 |
permanently, to enhance proof automation. They are named @{thm[source] ev.intros} |
69505 | 653 |
\index{intros@\<open>.intros\<close>} by Isabelle:\<close> |
47269 | 654 |
|
655 |
declare ev.intros[simp,intro] |
|
656 |
||
67406 | 657 |
text\<open>The rules of an inductive definition are not simplification rules by |
47269 | 658 |
default because, in contrast to recursive functions, there is no termination |
659 |
requirement for inductive definitions. |
|
660 |
||
52361 | 661 |
\subsubsection{Inductive Versus Recursive} |
47269 | 662 |
|
663 |
We have seen two definitions of the notion of evenness, an inductive and a |
|
664 |
recursive one. Which one is better? Much of the time, the recursive one is |
|
665 |
more convenient: it allows us to do rewriting in the middle of terms, and it |
|
666 |
expresses both the positive information (which numbers are even) and the |
|
667 |
negative information (which numbers are not even) directly. An inductive |
|
668 |
definition only expresses the positive information directly. The negative |
|
69505 | 669 |
information, for example, that \<open>1\<close> is not even, has to be proved from |
47269 | 670 |
it (by induction or rule inversion). On the other hand, rule induction is |
69597 | 671 |
tailor-made for proving \mbox{\<^prop>\<open>ev n \<Longrightarrow> P n\<close>} because it only asks you |
672 |
to prove the positive cases. In the proof of \<^prop>\<open>evn n \<Longrightarrow> P n\<close> by |
|
58962 | 673 |
computation induction via @{thm[source]evn.induct}, we are also presented |
47269 | 674 |
with the trivial negative cases. If you want the convenience of both |
675 |
rewriting and rule induction, you can make two definitions and show their |
|
676 |
equivalence (as above) or make one definition and prove additional properties |
|
677 |
from it, for example rule induction from computation induction. |
|
678 |
||
679 |
But many concepts do not admit a recursive definition at all because there is |
|
680 |
no datatype for the recursion (for example, the transitive closure of a |
|
47711 | 681 |
relation), or the recursion would not terminate (for example, |
682 |
an interpreter for a programming language). Even if there is a recursive |
|
47269 | 683 |
definition, if we are only interested in the positive information, the |
684 |
inductive definition may be much simpler. |
|
685 |
||
52361 | 686 |
\subsection{The Reflexive Transitive Closure} |
47269 | 687 |
\label{sec:star} |
688 |
||
689 |
Evenness is really more conveniently expressed recursively than inductively. |
|
690 |
As a second and very typical example of an inductive definition we define the |
|
47711 | 691 |
reflexive transitive closure. |
52782 | 692 |
\ifsem |
47711 | 693 |
It will also be an important building block for |
47269 | 694 |
some of the semantics considered in the second part of the book. |
52782 | 695 |
\fi |
47269 | 696 |
|
69505 | 697 |
The reflexive transitive closure, called \<open>star\<close> below, is a function |
698 |
that maps a binary predicate to another binary predicate: if \<open>r\<close> is of |
|
69597 | 699 |
type \<open>\<tau> \<Rightarrow> \<tau> \<Rightarrow> bool\<close> then \<^term>\<open>star r\<close> is again of type \<open>\<tau> \<Rightarrow> |
700 |
\<tau> \<Rightarrow> bool\<close>, and \<^prop>\<open>star r x y\<close> means that \<open>x\<close> and \<open>y\<close> are in |
|
701 |
the relation \<^term>\<open>star r\<close>. Think \<^term>\<open>r\<^sup>*\<close> when you see \<^term>\<open>star |
|
702 |
r\<close>, because \<open>star r\<close> is meant to be the reflexive transitive closure. |
|
703 |
That is, \<^prop>\<open>star r x y\<close> is meant to be true if from \<open>x\<close> we can |
|
69505 | 704 |
reach \<open>y\<close> in finitely many \<open>r\<close> steps. This concept is naturally |
67406 | 705 |
defined inductively:\<close> |
47269 | 706 |
|
707 |
inductive star :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" for r where |
|
708 |
refl: "star r x x" | |
|
709 |
step: "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z" |
|
710 |
||
69597 | 711 |
text\<open>The base case @{thm[source] refl} is reflexivity: \<^term>\<open>x=y\<close>. The |
69505 | 712 |
step case @{thm[source]step} combines an \<open>r\<close> step (from \<open>x\<close> to |
69597 | 713 |
\<open>y\<close>) and a \<^term>\<open>star r\<close> step (from \<open>y\<close> to \<open>z\<close>) into a |
714 |
\<^term>\<open>star r\<close> step (from \<open>x\<close> to \<open>z\<close>). |
|
69505 | 715 |
The ``\isacom{for}~\<open>r\<close>'' in the header is merely a hint to Isabelle |
69597 | 716 |
that \<open>r\<close> is a fixed parameter of \<^const>\<open>star\<close>, in contrast to the |
717 |
further parameters of \<^const>\<open>star\<close>, which change. As a result, Isabelle |
|
47269 | 718 |
generates a simpler induction rule. |
719 |
||
69597 | 720 |
By definition \<^term>\<open>star r\<close> is reflexive. It is also transitive, but we |
67406 | 721 |
need rule induction to prove that:\<close> |
47269 | 722 |
|
723 |
lemma star_trans: "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z" |
|
724 |
apply(induction rule: star.induct) |
|
725 |
(*<*) |
|
726 |
defer |
|
727 |
apply(rename_tac u x y) |
|
728 |
defer |
|
729 |
(*>*) |
|
69597 | 730 |
txt\<open>The induction is over \<^prop>\<open>star r x y\<close> (the first matching assumption) |
731 |
and we try to prove \mbox{\<^prop>\<open>star r y z \<Longrightarrow> star r x z\<close>}, |
|
732 |
which we abbreviate by \<^prop>\<open>P x y\<close>. These are our two subgoals: |
|
47269 | 733 |
@{subgoals[display,indent=0]} |
69597 | 734 |
The first one is \<^prop>\<open>P x x\<close>, the result of case @{thm[source]refl}, |
69505 | 735 |
and it is trivial:\index{assumption@\<open>assumption\<close>} |
67406 | 736 |
\<close> |
47269 | 737 |
apply(assumption) |
69505 | 738 |
txt\<open>Let us examine subgoal \<open>2\<close>, case @{thm[source] step}. |
69597 | 739 |
Assumptions \<^prop>\<open>r u x\<close> and \mbox{\<^prop>\<open>star r x y\<close>} |
47269 | 740 |
are the premises of rule @{thm[source]step}. |
69597 | 741 |
Assumption \<^prop>\<open>star r y z \<Longrightarrow> star r x z\<close> is \mbox{\<^prop>\<open>P x y\<close>}, |
742 |
the IH coming from \<^prop>\<open>star r x y\<close>. We have to prove \<^prop>\<open>P u y\<close>, |
|
743 |
which we do by assuming \<^prop>\<open>star r y z\<close> and proving \<^prop>\<open>star r u z\<close>. |
|
744 |
The proof itself is straightforward: from \mbox{\<^prop>\<open>star r y z\<close>} the IH |
|
745 |
leads to \<^prop>\<open>star r x z\<close> which, together with \<^prop>\<open>r u x\<close>, |
|
746 |
leads to \mbox{\<^prop>\<open>star r u z\<close>} via rule @{thm[source]step}: |
|
67406 | 747 |
\<close> |
47269 | 748 |
apply(metis step) |
749 |
done |
|
750 |
||
67406 | 751 |
text\<open>\index{rule induction|)} |
47269 | 752 |
|
52361 | 753 |
\subsection{The General Case} |
47269 | 754 |
|
755 |
Inductive definitions have approximately the following general form: |
|
756 |
\begin{quote} |
|
69505 | 757 |
\isacom{inductive} \<open>I :: "\<tau> \<Rightarrow> bool"\<close> \isacom{where} |
47269 | 758 |
\end{quote} |
759 |
followed by a sequence of (possibly named) rules of the form |
|
760 |
\begin{quote} |
|
69505 | 761 |
\<open>\<lbrakk> I a\<^sub>1; \<dots>; I a\<^sub>n \<rbrakk> \<Longrightarrow> I a\<close> |
47269 | 762 |
\end{quote} |
69505 | 763 |
separated by \<open>|\<close>. As usual, \<open>n\<close> can be 0. |
47269 | 764 |
The corresponding rule induction principle |
69505 | 765 |
\<open>I.induct\<close> applies to propositions of the form |
47269 | 766 |
\begin{quote} |
69597 | 767 |
\<^prop>\<open>I x \<Longrightarrow> P x\<close> |
47269 | 768 |
\end{quote} |
69505 | 769 |
where \<open>P\<close> may itself be a chain of implications. |
47269 | 770 |
\begin{warn} |
771 |
Rule induction is always on the leftmost premise of the goal. |
|
69505 | 772 |
Hence \<open>I x\<close> must be the first premise. |
47269 | 773 |
\end{warn} |
69597 | 774 |
Proving \<^prop>\<open>I x \<Longrightarrow> P x\<close> by rule induction means proving |
69505 | 775 |
for every rule of \<open>I\<close> that \<open>P\<close> is invariant: |
47269 | 776 |
\begin{quote} |
69505 | 777 |
\<open>\<lbrakk> I a\<^sub>1; P a\<^sub>1; \<dots>; I a\<^sub>n; P a\<^sub>n \<rbrakk> \<Longrightarrow> P a\<close> |
47269 | 778 |
\end{quote} |
779 |
||
780 |
The above format for inductive definitions is simplified in a number of |
|
69505 | 781 |
respects. \<open>I\<close> can have any number of arguments and each rule can have |
782 |
additional premises not involving \<open>I\<close>, so-called \conceptidx{side |
|
55317 | 783 |
conditions}{side condition}. In rule inductions, these side conditions appear as additional |
47269 | 784 |
assumptions. The \isacom{for} clause seen in the definition of the reflexive |
55361 | 785 |
transitive closure simplifies the induction rule. |
786 |
\index{inductive definition|)} |
|
54231 | 787 |
|
54436 | 788 |
\subsection*{Exercises} |
54186 | 789 |
|
54231 | 790 |
\begin{exercise} |
58502 | 791 |
Formalize the following definition of palindromes |
54231 | 792 |
\begin{itemize} |
793 |
\item The empty list and a singleton list are palindromes. |
|
69597 | 794 |
\item If \<open>xs\<close> is a palindrome, so is \<^term>\<open>a # xs @ [a]\<close>. |
54231 | 795 |
\end{itemize} |
69597 | 796 |
as an inductive predicate \<open>palindrome ::\<close> \<^typ>\<open>'a list \<Rightarrow> bool\<close> |
797 |
and prove that \<^prop>\<open>rev xs = xs\<close> if \<open>xs\<close> is a palindrome. |
|
54231 | 798 |
\end{exercise} |
799 |
||
54212 | 800 |
\exercise |
69597 | 801 |
We could also have defined \<^const>\<open>star\<close> as follows: |
67406 | 802 |
\<close> |
54212 | 803 |
|
804 |
inductive star' :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" for r where |
|
805 |
refl': "star' r x x" | |
|
806 |
step': "star' r x y \<Longrightarrow> r y z \<Longrightarrow> star' r x z" |
|
807 |
||
67406 | 808 |
text\<open> |
69505 | 809 |
The single \<open>r\<close> step is performed after rather than before the \<open>star'\<close> |
69597 | 810 |
steps. Prove \<^prop>\<open>star' r x y \<Longrightarrow> star r x y\<close> and |
811 |
\<^prop>\<open>star r x y \<Longrightarrow> star' r x y\<close>. You may need lemmas. |
|
54217 | 812 |
Note that rule induction fails |
813 |
if the assumption about the inductive predicate is not the first assumption. |
|
54212 | 814 |
\endexercise |
815 |
||
54292 | 816 |
\begin{exercise}\label{exe:iter} |
69597 | 817 |
Analogous to \<^const>\<open>star\<close>, give an inductive definition of the \<open>n\<close>-fold iteration |
818 |
of a relation \<open>r\<close>: \<^term>\<open>iter r n x y\<close> should hold if there are \<open>x\<^sub>0\<close>, \dots, \<open>x\<^sub>n\<close> |
|
819 |
such that \<^prop>\<open>x = x\<^sub>0\<close>, \<^prop>\<open>x\<^sub>n = y\<close> and \<open>r x\<^bsub>i\<^esub> x\<^bsub>i+1\<^esub>\<close> for |
|
820 |
all \<^prop>\<open>i < n\<close>. Correct and prove the following claim: |
|
821 |
\<^prop>\<open>star r x y \<Longrightarrow> iter r n x y\<close>. |
|
54290 | 822 |
\end{exercise} |
823 |
||
61012 | 824 |
\begin{exercise}\label{exe:cfg} |
54218 | 825 |
A context-free grammar can be seen as an inductive definition where each |
826 |
nonterminal $A$ is an inductively defined predicate on lists of terminal |
|
56116 | 827 |
symbols: $A(w)$ means that $w$ is in the language generated by $A$. |
54218 | 828 |
For example, the production $S \to a S b$ can be viewed as the implication |
69597 | 829 |
\<^prop>\<open>S w \<Longrightarrow> S (a # w @ [b])\<close> where \<open>a\<close> and \<open>b\<close> are terminal symbols, |
54218 | 830 |
i.e., elements of some alphabet. The alphabet can be defined like this: |
69505 | 831 |
\isacom{datatype} \<open>alpha = a | b | \<dots>\<close> |
54218 | 832 |
|
833 |
Define the two grammars (where $\varepsilon$ is the empty word) |
|
834 |
\[ |
|
835 |
\begin{array}{r@ {\quad}c@ {\quad}l} |
|
836 |
S &\to& \varepsilon \quad\mid\quad aSb \quad\mid\quad SS \\ |
|
837 |
T &\to& \varepsilon \quad\mid\quad TaTb |
|
838 |
\end{array} |
|
839 |
\] |
|
840 |
as two inductive predicates. |
|
69505 | 841 |
If you think of \<open>a\<close> and \<open>b\<close> as ``\<open>(\<close>'' and ``\<open>)\<close>'', |
56989 | 842 |
the grammar defines strings of balanced parentheses. |
69597 | 843 |
Prove \<^prop>\<open>T w \<Longrightarrow> S w\<close> and \mbox{\<^prop>\<open>S w \<Longrightarrow> T w\<close>} separately and conclude |
844 |
\<^prop>\<open>S w = T w\<close>. |
|
54218 | 845 |
\end{exercise} |
846 |
||
54212 | 847 |
\ifsem |
54186 | 848 |
\begin{exercise} |
54203 | 849 |
In \autoref{sec:AExp} we defined a recursive evaluation function |
69505 | 850 |
\<open>aval :: aexp \<Rightarrow> state \<Rightarrow> val\<close>. |
54203 | 851 |
Define an inductive evaluation predicate |
69505 | 852 |
\<open>aval_rel :: aexp \<Rightarrow> state \<Rightarrow> val \<Rightarrow> bool\<close> |
54203 | 853 |
and prove that it agrees with the recursive function: |
69597 | 854 |
\<^prop>\<open>aval_rel a s v \<Longrightarrow> aval a s = v\<close>, |
855 |
\<^prop>\<open>aval a s = v \<Longrightarrow> aval_rel a s v\<close> and thus |
|
54203 | 856 |
\noquotes{@{prop [source] "aval_rel a s v \<longleftrightarrow> aval a s = v"}}. |
857 |
\end{exercise} |
|
858 |
||
859 |
\begin{exercise} |
|
54210 | 860 |
Consider the stack machine from Chapter~3 |
861 |
and recall the concept of \concept{stack underflow} |
|
862 |
from Exercise~\ref{exe:stack-underflow}. |
|
863 |
Define an inductive predicate |
|
69505 | 864 |
\<open>ok :: nat \<Rightarrow> instr list \<Rightarrow> nat \<Rightarrow> bool\<close> |
865 |
such that \<open>ok n is n'\<close> means that with any initial stack of length |
|
866 |
\<open>n\<close> the instructions \<open>is\<close> can be executed |
|
867 |
without stack underflow and that the final stack has length \<open>n'\<close>. |
|
868 |
Prove that \<open>ok\<close> correctly computes the final stack size |
|
54186 | 869 |
@{prop[display] "\<lbrakk>ok n is n'; length stk = n\<rbrakk> \<Longrightarrow> length (exec is s stk) = n'"} |
69505 | 870 |
and that instruction sequences generated by \<open>comp\<close> |
871 |
cannot cause stack underflow: \ \<open>ok n (comp a) ?\<close> \ for |
|
872 |
some suitable value of \<open>?\<close>. |
|
54186 | 873 |
\end{exercise} |
874 |
\fi |
|
67406 | 875 |
\<close> |
47269 | 876 |
(*<*) |
877 |
end |
|
878 |
(*>*) |