author  nipkow 
Fri, 24 Aug 2018 16:00:41 +0200  
changeset 68800  d4bad1efa268 
parent 67613  ce654b0e6d69 
child 69505  cc2d676d5395 
permissions  rwrr 
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} & ::= & 

16 
@{text"(form)"} ~\mid~ 

17 
@{const True} ~\mid~ 

18 
@{const False} ~\mid~ 

19 
@{prop "term = term"}\\ 

55348  20 
&\mid& @{prop"\<not> form"}\index{$HOL4@\isasymnot} ~\mid~ 
21 
@{prop "form \<and> form"}\index{$HOL0@\isasymand} ~\mid~ 

22 
@{prop "form \<or> form"}\index{$HOL1@\isasymor} ~\mid~ 

23 
@{prop "form \<longrightarrow> form"}\index{$HOL2@\isasymlongrightarrow}\\ 

24 
&\mid& @{prop"\<forall>x. form"}\index{$HOL6@\isasymforall} ~\mid~ @{prop"\<exists>x. form"}\index{$HOL7@\isasymexists} 

47269  25 
\end{array} 
26 
\] 

47711  27 
Terms are the ones we have seen all along, built from constants, variables, 
47269  28 
function application and @{text"\<lambda>"}abstraction, including all the syntactic 
56989  29 
sugar like infix symbols, @{text "if"}, @{text "case"}, etc. 
47269  30 
\begin{warn} 
31 
Remember that formulas are simply terms of type @{text bool}. Hence 

32 
@{text "="} also works for formulas. Beware that @{text"="} has a higher 

33 
precedence than the other logical operators. Hence @{prop"s = t \<and> A"} means 

47711  34 
@{text"(s = t) \<and> A"}, and @{prop"A\<and>B = B\<and>A"} means @{text"A \<and> (B = B) \<and> A"}. 
47269  35 
Logical equivalence can also be written with 
36 
@{text "\<longleftrightarrow>"} instead of @{text"="}, where @{text"\<longleftrightarrow>"} has the same low 

37 
precedence as @{text"\<longrightarrow>"}. Hence @{text"A \<and> B \<longleftrightarrow> B \<and> A"} really means 

38 
@{text"(A \<and> B) \<longleftrightarrow> (B \<and> A)"}. 

39 
\end{warn} 

40 
\begin{warn} 

41 
Quantifiers need to be enclosed in parentheses if they are nested within 

42 
other constructs (just like @{text "if"}, @{text case} and @{text let}). 

43 
\end{warn} 

52404  44 
The most frequent logical symbols and their ASCII representations are shown 
45 
in Fig.~\ref{fig:logsymbols}. 

46 
\begin{figure} 

47269  47 
\begin{center} 
48 
\begin{tabular}{l@ {\qquad}l@ {\qquad}l} 

49 
@{text "\<forall>"} & \xsymbol{forall} & \texttt{ALL}\\ 

50 
@{text "\<exists>"} & \xsymbol{exists} & \texttt{EX}\\ 

51 
@{text "\<lambda>"} & \xsymbol{lambda} & \texttt{\%}\\ 

52 
@{text "\<longrightarrow>"} & \texttt{{}>}\\ 

47711  53 
@{text "\<longleftrightarrow>"} & \texttt{<>}\\ 
47269  54 
@{text "\<and>"} & \texttt{/\char`\\} & \texttt{\&}\\ 
55 
@{text "\<or>"} & \texttt{\char`\\/} & \texttt{}\\ 

56 
@{text "\<not>"} & \xsymbol{not} & \texttt{\char`~}\\ 

57 
@{text "\<noteq>"} & \xsymbol{noteq} & \texttt{\char`~=} 

58 
\end{tabular} 

59 
\end{center} 

52404  60 
\caption{Logical symbols and their ASCII forms} 
61 
\label{fig:logsymbols} 

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} 
71 
The implication @{text"\<Longrightarrow>"} is part of the Isabelle framework. It structures 

47711  72 
theorems and proof states, separating assumptions from conclusions. 
47269  73 
The implication @{text"\<longrightarrow>"} is part of the logic HOL and can occur inside the 
74 
formulas that make up the assumptions and conclusion. 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52782
diff
changeset

75 
Theorems should be of the form @{text"\<lbrakk> A\<^sub>1; \<dots>; A\<^sub>n \<rbrakk> \<Longrightarrow> A"}, 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52782
diff
changeset

76 
not @{text"A\<^sub>1 \<and> \<dots> \<and> A\<^sub>n \<longrightarrow> A"}. 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 

55348  83 
Sets of elements of type @{typ 'a} have type @{typ"'a set"}\index{set@@{text set}}. 
47711  84 
They can be finite or infinite. Sets come with the usual notation: 
47269  85 
\begin{itemize} 
55348  86 
\item \indexed{@{term"{}"}}{$IMP042},\quad @{text"{e\<^sub>1,\<dots>,e\<^sub>n}"} 
87 
\item @{prop"e \<in> A"}\index{$HOLSet0@\isasymin},\quad @{prop"A \<subseteq> B"}\index{$HOLSet2@\isasymsubseteq} 

88 
\item @{term"A \<union> B"}\index{$HOLSet4@\isasymunion},\quad @{term"A \<inter> B"}\index{$HOLSet5@\isasyminter},\quad @{term"A  B"},\quad @{term"A"} 

47269  89 
\end{itemize} 
51425  90 
(where @{term"AB"} and @{text"A"} are set difference and complement) 
47269  91 
and much more. @{const UNIV} is the set of all elements of some type. 
55348  92 
Set comprehension\index{set comprehension} is written 
93 
@{term"{x. P}"}\index{$IMP042@@{term"{x. P}"}} rather than @{text"{x  P}"}. 

47269  94 
\begin{warn} 
95 
In @{term"{x. P}"} the @{text x} must be a variable. Set comprehension 

96 
involving a proper term @{text t} must be written 

55348  97 
\noquotes{@{term[source] "{t  x y. P}"}}\index{$IMP042@@{text"{t x. P}"}}, 
49615  98 
where @{text "x y"} are those free variables in @{text t} 
99 
that occur in @{text P}. 

67613  100 
This is just a shorthand for @{term"{v. \<exists>x y. v = t \<and> P}"}, where 
49615  101 
@{text v} is a new variable. For example, @{term"{x+yx. x \<in> A}"} 
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} 

108 
@{text "\<in>"} & \texttt{\char`\\\char`\<in>} & \texttt{:}\\ 

109 
@{text "\<subseteq>"} & \texttt{\char`\\\char`\<subseteq>} & \texttt{<=}\\ 

110 
@{text "\<union>"} & \texttt{\char`\\\char`\<union>} & \texttt{Un}\\ 

111 
@{text "\<inter>"} & \texttt{\char`\\\char`\<inter>} & \texttt{Int} 

112 
\end{tabular} 

113 
\end{center} 

67613  114 
Sets also allow bounded quantifications @{prop"\<forall>x \<in> A. P"} and 
115 
@{prop"\<exists>x \<in> A. P"}. 

47269  116 

55348  117 
For the more ambitious, there are also @{text"\<Union>"}\index{$HOLSet6@\isasymUnion} 
118 
and @{text"\<Inter>"}\index{$HOLSet7@\isasymInter}: 

52404  119 
\begin{center} 
120 
@{thm Union_eq} \qquad @{thm Inter_eq} 

121 
\end{center} 

122 
The ASCII forms of @{text"\<Union>"} are \texttt{\char`\\\char`\<Union>} and \texttt{Union}, 

123 
those of @{text"\<Inter>"} are \texttt{\char`\\\char`\<Inter>} and \texttt{Inter}. 

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} 

55348  135 
@{const_typ set}\index{set@@{const set}} & converts a list to the set of its elements\\ 
136 
@{const_typ finite}\index{finite@@{const finite}} & is true iff its argument is finite\\ 

62223  137 
\noquotes{@{term[source] "card :: 'a set \<Rightarrow> nat"}}\index{card@@{const card}} & is the cardinality of a finite set\\ 
51784  138 
& and is @{text 0} for all infinite sets\\ 
55348  139 
@{thm image_def}\index{$IMP042@@{term"f ` A"}} & is the image of a function over a set 
51784  140 
\end{tabular} 
141 
\end{center} 

58620  142 
See @{cite "NipkowMain"} for the wealth of further predefined functions in theory 
51784  143 
@{theory Main}. 
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> 
54214  155 
Define a function @{text "set ::"} @{typ "'a tree \<Rightarrow> 'a set"} 
156 
that returns the elements in a tree and a function 

157 
@{text "ord ::"} @{typ "int tree \<Rightarrow> bool"} 

56989  158 
that tests if an @{typ "int tree"} is ordered. 
54214  159 

160 
Define a function @{text ins} that inserts an element into an ordered @{typ "int tree"} 

161 
while maintaining the order of the tree. If the element is already in the tree, the 

162 
same tree should be returned. Prove correctness of @{text ins}: 

163 
@{prop "set(ins x t) = {x} \<union> set t"} and @{prop "ord t \<Longrightarrow> ord(ins i t)"}. 

164 
\endexercise 

165 

166 

52361  167 
\section{Proof Automation} 
47269  168 

55348  169 
So far we have only seen @{text simp} and \indexed{@{text auto}}{auto}: Both perform 
47269  170 
rewriting, both can also prove linear arithmetic facts (no multiplication), 
171 
and @{text auto} is also able to prove simple logical or settheoretic 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{proofmethod} 

183 
\end{quote} 

184 
is short for 

185 
\begin{quote} 

186 
\isacom{apply} \textit{proofmethod}\\ 

187 
\isacom{done} 

188 
\end{quote} 

189 
The key characteristics of both @{text simp} and @{text auto} are 

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 

198 
A proof method that is still incomplete but tries harder than @{text auto} is 

55348  199 
\indexed{@{text fastforce}}{fastforce}. It either succeeds or fails, it acts on the first 
58605  200 
subgoal only, and it can be modified like @{text auto}, e.g., 
47269  201 
with @{text "simp add"}. Here is a typical example of what @{text fastforce} 
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 

67406  209 
text\<open>This lemma is out of reach for @{text auto} because of the 
47269  210 
quantifiers. Even @{text fastforce} fails when the quantifier structure 
211 
becomes more complicated. In a few cases, its slow version @{text force} 

212 
succeeds where @{text fastforce} fails. 

213 

55348  214 
The method of choice for complex logical goals is \indexed{@{text blast}}{blast}. In the 
47711  215 
following example, @{text T} and @{text A} are two binary predicates. It 
216 
is shown that if @{text T} is total, @{text A} is antisymmetric and @{text T} is 

47269  217 
a subset of @{text A}, then @{text A} is a subset of @{text T}: 
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. 
229 
Method @{text blast} 

230 
\begin{itemize} 

231 
\item is (in principle) a complete proof procedure for firstorder 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!) 

55348  260 
and insists on a proof that it can check. This is what \indexed{@{text metis}}{metis} does. 
58605  261 
It is given a list of lemmas and tries to find a proof using just those lemmas 
56989  262 
(and pure logic). In contrast to using @{text simp} and friends who know a lot of 
47269  263 
lemmas already, using @{text metis} manually is tedious because one has 
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 

269 
the above lemma, even without any knowledge of what the functions @{const take} 

270 
and @{const drop} do. Keep in mind that the variables in the two lemmas 

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 

277 
incomparable. Therefore it is recommended to apply @{text simp} or @{text 

278 
auto} before invoking \isacom{sledgehammer} on what is left. 

279 

51436  280 
\subsection{Arithmetic} 
47269  281 

282 
By arithmetic formulas we mean formulas involving variables, numbers, @{text 

283 
"+"}, @{text""}, @{text "="}, @{text "<"}, @{text "\<le>"} and the usual logical 

284 
connectives @{text"\<not>"}, @{text"\<and>"}, @{text"\<or>"}, @{text"\<longrightarrow>"}, 

285 
@{text"\<longleftrightarrow>"}. Strictly speaking, this is known as \concept{linear arithmetic} 

286 
because it does not involve multiplication, although multiplication with 

58504  287 
numbers, e.g., @{text"2*n"}, is allowed. Such formulas can be proved by 
55348  288 
\indexed{@{text arith}}{arith}: 
67406  289 
\<close> 
47269  290 

291 
lemma "\<lbrakk> (a::nat) \<le> x + b; 2*x < c \<rbrakk> \<Longrightarrow> 2*a + 1 \<le> 2*b + c" 

292 
by arith 

293 

67406  294 
text\<open>In fact, @{text auto} and @{text simp} can prove many linear 
47269  295 
arithmetic formulas already, like the one above, by calling a weak but fast 
296 
version of @{text arith}. Hence it is usually not necessary to invoke 

297 
@{text arith} explicitly. 

298 

299 
The above example involves natural numbers, but integers (type @{typ int}) 

300 
and real numbers (type @{text real}) are supported as well. As are a number 

301 
of further operators like @{const min} and @{const max}. On @{typ nat} and 

302 
@{typ int}, @{text arith} can even prove theorems with quantifiers in them, 

303 
but we will not enlarge on that here. 

304 

305 

52361  306 
\subsection{Trying Them All} 
47727  307 

308 
If you want to try all of the above automatic proof methods you simply type 

309 
\begin{isabelle} 

310 
\isacom{try} 

311 
\end{isabelle} 

63414  312 
There is also a lightweight variant \isacom{try0} that does not call 
313 
sledgehammer. If desired, specific simplification and introduction rules 

314 
can be added: 

47727  315 
\begin{isabelle} 
63414  316 
\isacom{try0} @{text"simp: \<dots> intro: \<dots>"} 
47727  317 
\end{isabelle} 
318 

52361  319 
\section{Single Step Proofs} 
47269  320 

321 
Although automation is nice, it often fails, at least initially, and you need 

322 
to find out why. When @{text fastforce} or @{text blast} simply fail, you have 

323 
no clue why. At this point, the stepwise 

324 
application of proof rules may be necessary. For example, if @{text blast} 

325 
fails on @{prop"A \<and> B"}, you want to attack the two 

326 
conjuncts @{text A} and @{text B} separately. This can 

327 
be achieved by applying \emph{conjunction introduction} 

328 
\[ @{thm[mode=Rule,show_question_marks]conjI}\ @{text conjI} 

329 
\] 

330 
to the proof state. We will now examine the details of this process. 

331 

52361  332 
\subsection{Instantiating Unknowns} 
47269  333 

334 
We had briefly mentioned earlier that after proving some theorem, 

55317  335 
Isabelle replaces all free variables @{text x} by so called \conceptidx{unknowns}{unknown} 
47269  336 
@{text "?x"}. We can see this clearly in rule @{thm[source] conjI}. 
337 
These unknowns can later be instantiated explicitly or implicitly: 

338 
\begin{itemize} 

55317  339 
\item By hand, using \indexed{@{text of}}{of}. 
47269  340 
The expression @{text"conjI[of \"a=b\" \"False\"]"} 
341 
instantiates the unknowns in @{thm[source] conjI} from left to right with the 

342 
two formulas @{text"a=b"} and @{text False}, yielding the rule 

63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63414
diff
changeset

343 
@{thm[display,mode=Rule,margin=100]conjI[of "a=b" False]} 
47269  344 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52782
diff
changeset

345 
In general, @{text"th[of string\<^sub>1 \<dots> string\<^sub>n]"} instantiates 
47269  346 
the unknowns in the theorem @{text th} from left to right with the terms 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52782
diff
changeset

347 
@{text string\<^sub>1} to @{text string\<^sub>n}. 
47269  348 

55317  349 
\item By unification. \conceptidx{Unification}{unification} is the process of making two 
47269  350 
terms syntactically equal by suitable instantiations of unknowns. For example, 
351 
unifying @{text"?P \<and> ?Q"} with \mbox{@{prop"a=b \<and> False"}} instantiates 

352 
@{text "?P"} with @{prop "a=b"} and @{text "?Q"} with @{prop False}. 

353 
\end{itemize} 

354 
We need not instantiate all unknowns. If we want to skip a particular one we 

58605  355 
can write @{text"_"} instead, for example @{text "conjI[of _ \"False\"]"}. 
55317  356 
Unknowns can also be instantiated by name using \indexed{@{text "where"}}{where}, for example 
54839  357 
@{text "conjI[where ?P = \"a=b\""} \isacom{and} @{text"?Q = \"False\"]"}. 
47269  358 

359 

52361  360 
\subsection{Rule Application} 
47269  361 

55317  362 
\conceptidx{Rule application}{rule application} means applying a rule backwards to a proof state. 
47269  363 
For example, applying rule @{thm[source]conjI} to a proof state 
364 
\begin{quote} 

365 
@{text"1. \<dots> \<Longrightarrow> A \<and> B"} 

366 
\end{quote} 

367 
results in two subgoals, one for each premise of @{thm[source]conjI}: 

368 
\begin{quote} 

369 
@{text"1. \<dots> \<Longrightarrow> A"}\\ 

370 
@{text"2. \<dots> \<Longrightarrow> B"} 

371 
\end{quote} 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52782
diff
changeset

372 
In general, the application of a rule @{text"\<lbrakk> A\<^sub>1; \<dots>; A\<^sub>n \<rbrakk> \<Longrightarrow> A"} 
47269  373 
to a subgoal \mbox{@{text"\<dots> \<Longrightarrow> C"}} proceeds in two steps: 
374 
\begin{enumerate} 

375 
\item 

376 
Unify @{text A} and @{text C}, thus instantiating the unknowns in the rule. 

377 
\item 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52782
diff
changeset

378 
Replace the subgoal @{text C} with @{text n} new subgoals @{text"A\<^sub>1"} to @{text"A\<^sub>n"}. 
47269  379 
\end{enumerate} 
380 
This is the command to apply rule @{text xyz}: 

381 
\begin{quote} 

55348  382 
\isacom{apply}@{text"(rule xyz)"}\index{rule@@{text rule}} 
47269  383 
\end{quote} 
384 
This is also called \concept{backchaining} with rule @{text xyz}. 

385 

52361  386 
\subsection{Introduction Rules} 
47269  387 

388 
Conjunction introduction (@{thm[source] conjI}) is one example of a whole 

55317  389 
class of rules known as \conceptidx{introduction rules}{introduction rule}. They explain under which 
47269  390 
premises some logical construct can be introduced. Here are some further 
391 
useful introduction rules: 

392 
\[ 

393 
\inferrule*[right=\mbox{@{text impI}}]{\mbox{@{text"?P \<Longrightarrow> ?Q"}}}{\mbox{@{text"?P \<longrightarrow> ?Q"}}} 

394 
\qquad 

395 
\inferrule*[right=\mbox{@{text allI}}]{\mbox{@{text"\<And>x. ?P x"}}}{\mbox{@{text"\<forall>x. ?P x"}}} 

396 
\] 

397 
\[ 

398 
\inferrule*[right=\mbox{@{text iffI}}]{\mbox{@{text"?P \<Longrightarrow> ?Q"}} \\ \mbox{@{text"?Q \<Longrightarrow> ?P"}}} 

399 
{\mbox{@{text"?P = ?Q"}}} 

400 
\] 

401 
These rules are part of the logical system of \concept{natural deduction} 

58620  402 
(e.g., @{cite HuthRyan}). Although we intentionally deemphasize the basic rules 
47269  403 
of logic in favour of automatic proof methods that allow you to take bigger 
404 
steps, these rules are helpful in locating where and why automation fails. 

405 
When applied backwards, these rules decompose the goal: 

406 
\begin{itemize} 

407 
\item @{thm[source] conjI} and @{thm[source]iffI} split the goal into two subgoals, 

408 
\item @{thm[source] impI} moves the lefthand side of a HOL implication into the list of assumptions, 

409 
\item and @{thm[source] allI} removes a @{text "\<forall>"} by turning the quantified variable into a fixed local variable of the subgoal. 

410 
\end{itemize} 

411 
Isabelle knows about these and a number of other introduction rules. 

412 
The command 

413 
\begin{quote} 

55348  414 
\isacom{apply} @{text rule}\index{rule@@{text rule}} 
47269  415 
\end{quote} 
416 
automatically selects the appropriate rule for the current subgoal. 

417 

418 
You can also turn your own theorems into introduction rules by giving them 

55348  419 
the \indexed{@{text"intro"}}{intro} attribute, analogous to the @{text simp} attribute. In 
47269  420 
that case @{text blast}, @{text fastforce} and (to a limited extent) @{text 
421 
auto} will automatically backchain with those theorems. The @{text intro} 

422 
attribute should be used with care because it increases the search space and 

47711  423 
can lead to nontermination. Sometimes it is better to use it only in 
424 
specific calls of @{text blast} and friends. For example, 

47269  425 
@{thm[source] le_trans}, transitivity of @{text"\<le>"} on type @{typ nat}, 
426 
is not an introduction rule by default because of the disastrous effect 

427 
on the search space, but can be useful in specific situations: 

67406  428 
\<close> 
47269  429 

430 
lemma "\<lbrakk> (a::nat) \<le> b; b \<le> c; c \<le> d; d \<le> e \<rbrakk> \<Longrightarrow> a \<le> e" 

431 
by(blast intro: le_trans) 

432 

67406  433 
text\<open> 
47269  434 
Of course this is just an example and could be proved by @{text arith}, too. 
435 

52361  436 
\subsection{Forward Proof} 
47269  437 
\label{sec:forwardproof} 
438 

439 
Forward proof means deriving new theorems from old theorems. We have already 

440 
seen a very simple form of forward proof: the @{text of} operator for 

54839  441 
instantiating unknowns in a theorem. The big brother of @{text of} is 
55317  442 
\indexed{@{text OF}}{OF} for applying one theorem to others. Given a theorem @{prop"A \<Longrightarrow> B"} called 
47269  443 
@{text r} and a theorem @{text A'} called @{text r'}, the theorem @{text 
444 
"r[OF r']"} is the result of applying @{text r} to @{text r'}, where @{text 

445 
r} should be viewed as a function taking a theorem @{text A} and returning 

446 
@{text B}. More precisely, @{text A} and @{text A'} are unified, thus 

447 
instantiating the unknowns in @{text B}, and the result is the instantiated 

448 
@{text B}. Of course, unification may also fail. 

449 
\begin{warn} 

450 
Application of rules to other rules operates in the forward direction: from 

451 
the premises to the conclusion of the rule; application of rules to proof 

452 
states operates in the backward direction, from the conclusion to the 

453 
premises. 

454 
\end{warn} 

455 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52782
diff
changeset

456 
In general @{text r} can be of the form @{text"\<lbrakk> A\<^sub>1; \<dots>; A\<^sub>n \<rbrakk> \<Longrightarrow> A"} 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52782
diff
changeset

457 
and there can be multiple argument theorems @{text r\<^sub>1} to @{text r\<^sub>m} 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52782
diff
changeset

458 
(with @{text"m \<le> n"}), in which case @{text "r[OF r\<^sub>1 \<dots> r\<^sub>m]"} is obtained 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52782
diff
changeset

459 
by unifying and thus proving @{text "A\<^sub>i"} with @{text "r\<^sub>i"}, @{text"i = 1\<dots>m"}. 
47269  460 
Here is an example, where @{thm[source]refl} is the theorem 
461 
@{thm[show_question_marks] refl}: 

67406  462 
\<close> 
47269  463 

464 
thm conjI[OF refl[of "a"] refl[of "b"]] 

465 

67406  466 
text\<open>yields the theorem @{thm conjI[OF refl[of "a"] refl[of "b"]]}. 
47269  467 
The command \isacom{thm} merely displays the result. 
468 

469 
Forward reasoning also makes sense in connection with proof states. 

470 
Therefore @{text blast}, @{text fastforce} and @{text auto} support a modifier 

471 
@{text dest} which instructs the proof method to use certain rules in a 

472 
forward fashion. If @{text r} is of the form \mbox{@{text "A \<Longrightarrow> B"}}, the modifier 

55348  473 
\mbox{@{text"dest: r"}}\index{dest@@{text"dest:"}} 
58504  474 
allows proof search to reason forward with @{text r}, i.e., 
47269  475 
to replace an assumption @{text A'}, where @{text A'} unifies with @{text A}, 
476 
with the correspondingly instantiated @{text B}. For example, @{thm[source,show_question_marks] Suc_leD} is the theorem \mbox{@{thm Suc_leD}}, which works well for forward reasoning: 

67406  477 
\<close> 
47269  478 

479 
lemma "Suc(Suc(Suc a)) \<le> b \<Longrightarrow> a \<le> b" 

480 
by(blast dest: Suc_leD) 

481 

67406  482 
text\<open>In this particular example we could have backchained with 
47269  483 
@{thm[source] Suc_leD}, too, but because the premise is more complicated than the conclusion this can easily lead to nontermination. 
484 

54212  485 
%\subsection{Finding Theorems} 
486 
% 

487 
%Command \isacom{find{\isacharunderscorekeyword}theorems} searches for specific theorems in the current 

488 
%theory. Search criteria include pattern matching on terms and on names. 

58620  489 
%For details see the Isabelle/Isar Reference Manual~@{cite IsarRef}. 
54212  490 
%\bigskip 
47727  491 

47269  492 
\begin{warn} 
493 
To ease readability we will drop the question marks 

494 
in front of unknowns from now on. 

495 
\end{warn} 

496 

47727  497 

52361  498 
\section{Inductive Definitions} 
55361  499 
\label{sec:inductivedefs}\index{inductive definition(} 
47269  500 

501 
Inductive definitions are the third important definition facility, after 

47711  502 
datatypes and recursive function. 
52782  503 
\ifsem 
47711  504 
In fact, they are the key construct in the 
47269  505 
definition of operational semantics in the second part of the book. 
52782  506 
\fi 
47269  507 

52361  508 
\subsection{An Example: Even Numbers} 
47269  509 
\label{sec:Logic:even} 
510 

511 
Here is a simple example of an inductively defined predicate: 

512 
\begin{itemize} 

513 
\item 0 is even 

514 
\item If $n$ is even, so is $n+2$. 

515 
\end{itemize} 

516 
The operative word ``inductive'' means that these are the only even numbers. 

517 
In Isabelle we give the two rules the names @{text ev0} and @{text evSS} 

518 
and write 

67406  519 
\<close> 
47269  520 

521 
inductive ev :: "nat \<Rightarrow> bool" where 

522 
ev0: "ev 0"  

523 
evSS: (*<*)"ev n \<Longrightarrow> ev (Suc(Suc n))"(*>*) 

67406  524 
text_raw\<open>@{prop[source]"ev n \<Longrightarrow> ev (n + 2)"}\<close> 
47269  525 

67406  526 
text\<open>To get used to inductive definitions, we will first prove a few 
47269  527 
properties of @{const ev} informally before we descend to the Isabelle level. 
528 

58504  529 
How do we prove that some number is even, e.g., @{prop "ev 4"}? Simply by combining the defining rules for @{const ev}: 
47269  530 
\begin{quote} 
531 
@{text "ev 0 \<Longrightarrow> ev (0 + 2) \<Longrightarrow> ev((0 + 2) + 2) = ev 4"} 

532 
\end{quote} 

533 

55361  534 
\subsubsection{Rule Induction}\index{rule induction(} 
47269  535 

536 
Showing that all even numbers have some property is more complicated. For 

537 
example, let us prove that the inductive definition of even numbers agrees 

67406  538 
with the following recursive one:\<close> 
47269  539 

58962  540 
fun evn :: "nat \<Rightarrow> bool" where 
541 
"evn 0 = True"  

542 
"evn (Suc 0) = False"  

543 
"evn (Suc(Suc n)) = evn n" 

47269  544 

67406  545 
text\<open>We prove @{prop"ev m \<Longrightarrow> evn m"}. That is, we 
47269  546 
assume @{prop"ev m"} and by induction on the form of its derivation 
58962  547 
prove @{prop"evn m"}. There are two cases corresponding to the two rules 
47269  548 
for @{const ev}: 
549 
\begin{description} 

550 
\item[Case @{thm[source]ev0}:] 

551 
@{prop"ev m"} was derived by rule @{prop "ev 0"}: \\ 

58962  552 
@{text"\<Longrightarrow>"} @{prop"m=(0::nat)"} @{text"\<Longrightarrow>"} @{text "evn m = evn 0 = True"} 
47269  553 
\item[Case @{thm[source]evSS}:] 
554 
@{prop"ev m"} was derived by rule @{prop "ev n \<Longrightarrow> ev(n+2)"}: \\ 

58962  555 
@{text"\<Longrightarrow>"} @{prop"m=n+(2::nat)"} and by induction hypothesis @{prop"evn n"}\\ 
556 
@{text"\<Longrightarrow>"} @{text"evn m = evn(n + 2) = evn n = True"} 

47269  557 
\end{description} 
558 

559 
What we have just seen is a special case of \concept{rule induction}. 

560 
Rule induction applies to propositions of this form 

561 
\begin{quote} 

562 
@{prop "ev n \<Longrightarrow> P n"} 

563 
\end{quote} 

564 
That is, we want to prove a property @{prop"P n"} 

565 
for all even @{text n}. But if we assume @{prop"ev n"}, then there must be 

566 
some derivation of this assumption using the two defining rules for 

567 
@{const ev}. That is, we must prove 

568 
\begin{description} 

569 
\item[Case @{thm[source]ev0}:] @{prop"P(0::nat)"} 

570 
\item[Case @{thm[source]evSS}:] @{prop"\<lbrakk> ev n; P n \<rbrakk> \<Longrightarrow> P(n + 2::nat)"} 

571 
\end{description} 

572 
The corresponding rule is called @{thm[source] ev.induct} and looks like this: 

573 
\[ 

574 
\inferrule{ 

575 
\mbox{@{thm (prem 1) ev.induct[of "n"]}}\\ 

576 
\mbox{@{thm (prem 2) ev.induct}}\\ 

577 
\mbox{@{prop"!!n. \<lbrakk> ev n; P n \<rbrakk> \<Longrightarrow> P(n+2)"}}} 

578 
{\mbox{@{thm (concl) ev.induct[of "n"]}}} 

579 
\] 

580 
The first premise @{prop"ev n"} enforces that this rule can only be applied 

581 
in situations where we know that @{text n} is even. 

582 

583 
Note that in the induction step we may not just assume @{prop"P n"} but also 

584 
\mbox{@{prop"ev n"}}, which is simply the premise of rule @{thm[source] 

585 
evSS}. Here is an example where the local assumption @{prop"ev n"} comes in 

586 
handy: we prove @{prop"ev m \<Longrightarrow> ev(m  2)"} by induction on @{prop"ev m"}. 

587 
Case @{thm[source]ev0} requires us to prove @{prop"ev(0  2)"}, which follows 

588 
from @{prop"ev 0"} because @{prop"0  2 = (0::nat)"} on type @{typ nat}. In 

589 
case @{thm[source]evSS} we have \mbox{@{prop"m = n+(2::nat)"}} and may assume 

590 
@{prop"ev n"}, which implies @{prop"ev (m  2)"} because @{text"m  2 = (n + 

56989  591 
2)  2 = n"}. We did not need the induction hypothesis at all for this proof (it 
592 
is just a case analysis of which rule was used) but having @{prop"ev n"} 

593 
at our disposal in case @{thm[source]evSS} was essential. 

47711  594 
This case analysis of rules is also called ``rule inversion'' 
47269  595 
and is discussed in more detail in \autoref{ch:Isar}. 
596 

597 
\subsubsection{In Isabelle} 

598 

599 
Let us now recast the above informal proofs in Isabelle. For a start, 

600 
we use @{const Suc} terms instead of numerals in rule @{thm[source]evSS}: 

601 
@{thm[display] evSS} 

602 
This avoids the difficulty of unifying @{text"n+2"} with some numeral, 

603 
which is not automatic. 

604 

605 
The simplest way to prove @{prop"ev(Suc(Suc(Suc(Suc 0))))"} is in a forward 

606 
direction: @{text "evSS[OF evSS[OF ev0]]"} yields the theorem @{thm evSS[OF 

607 
evSS[OF ev0]]}. Alternatively, you can also prove it as a lemma in backwards 

608 
fashion. Although this is more verbose, it allows us to demonstrate how each 

67406  609 
rule application changes the proof state:\<close> 
47269  610 

611 
lemma "ev(Suc(Suc(Suc(Suc 0))))" 

67406  612 
txt\<open> 
47269  613 
@{subgoals[display,indent=0,goals_limit=1]} 
67406  614 
\<close> 
47269  615 
apply(rule evSS) 
67406  616 
txt\<open> 
47269  617 
@{subgoals[display,indent=0,goals_limit=1]} 
67406  618 
\<close> 
47269  619 
apply(rule evSS) 
67406  620 
txt\<open> 
47269  621 
@{subgoals[display,indent=0,goals_limit=1]} 
67406  622 
\<close> 
47269  623 
apply(rule ev0) 
624 
done 

625 

67406  626 
text\<open>\indent 
47269  627 
Rule induction is applied by giving the induction rule explicitly via the 
67406  628 
@{text"rule:"} modifier:\index{inductionrule@@{text"induction ... rule:"}}\<close> 
47269  629 

58962  630 
lemma "ev m \<Longrightarrow> evn m" 
47269  631 
apply(induction rule: ev.induct) 
632 
by(simp_all) 

633 

67406  634 
text\<open>Both cases are automatic. Note that if there are multiple assumptions 
47269  635 
of the form @{prop"ev t"}, method @{text induction} will induct on the leftmost 
636 
one. 

637 

638 
As a bonus, we also prove the remaining direction of the equivalence of 

58962  639 
@{const ev} and @{const evn}: 
67406  640 
\<close> 
47269  641 

58962  642 
lemma "evn n \<Longrightarrow> ev n" 
643 
apply(induction n rule: evn.induct) 

47269  644 

67406  645 
txt\<open>This is a proof by computation induction on @{text n} (see 
47269  646 
\autoref{sec:recursivefuns}) that sets up three subgoals corresponding to 
58962  647 
the three equations for @{const evn}: 
47269  648 
@{subgoals[display,indent=0]} 
58962  649 
The first and third subgoals follow with @{thm[source]ev0} and @{thm[source]evSS}, and the second subgoal is trivially true because @{prop"evn(Suc 0)"} is @{const False}: 
67406  650 
\<close> 
47269  651 

652 
by (simp_all add: ev0 evSS) 

653 

67406  654 
text\<open>The rules for @{const ev} make perfect simplification and introduction 
47269  655 
rules because their premises are always smaller than the conclusion. It 
656 
makes sense to turn them into simplification and introduction rules 

55348  657 
permanently, to enhance proof automation. They are named @{thm[source] ev.intros} 
67406  658 
\index{intros@@{text".intros"}} by Isabelle:\<close> 
47269  659 

660 
declare ev.intros[simp,intro] 

661 

67406  662 
text\<open>The rules of an inductive definition are not simplification rules by 
47269  663 
default because, in contrast to recursive functions, there is no termination 
664 
requirement for inductive definitions. 

665 

52361  666 
\subsubsection{Inductive Versus Recursive} 
47269  667 

668 
We have seen two definitions of the notion of evenness, an inductive and a 

669 
recursive one. Which one is better? Much of the time, the recursive one is 

670 
more convenient: it allows us to do rewriting in the middle of terms, and it 

671 
expresses both the positive information (which numbers are even) and the 

672 
negative information (which numbers are not even) directly. An inductive 

673 
definition only expresses the positive information directly. The negative 

674 
information, for example, that @{text 1} is not even, has to be proved from 

675 
it (by induction or rule inversion). On the other hand, rule induction is 

47711  676 
tailormade for proving \mbox{@{prop"ev n \<Longrightarrow> P n"}} because it only asks you 
58962  677 
to prove the positive cases. In the proof of @{prop"evn n \<Longrightarrow> P n"} by 
678 
computation induction via @{thm[source]evn.induct}, we are also presented 

47269  679 
with the trivial negative cases. If you want the convenience of both 
680 
rewriting and rule induction, you can make two definitions and show their 

681 
equivalence (as above) or make one definition and prove additional properties 

682 
from it, for example rule induction from computation induction. 

683 

684 
But many concepts do not admit a recursive definition at all because there is 

685 
no datatype for the recursion (for example, the transitive closure of a 

47711  686 
relation), or the recursion would not terminate (for example, 
687 
an interpreter for a programming language). Even if there is a recursive 

47269  688 
definition, if we are only interested in the positive information, the 
689 
inductive definition may be much simpler. 

690 

52361  691 
\subsection{The Reflexive Transitive Closure} 
47269  692 
\label{sec:star} 
693 

694 
Evenness is really more conveniently expressed recursively than inductively. 

695 
As a second and very typical example of an inductive definition we define the 

47711  696 
reflexive transitive closure. 
52782  697 
\ifsem 
47711  698 
It will also be an important building block for 
47269  699 
some of the semantics considered in the second part of the book. 
52782  700 
\fi 
47269  701 

702 
The reflexive transitive closure, called @{text star} below, is a function 

703 
that maps a binary predicate to another binary predicate: if @{text r} is of 

704 
type @{text"\<tau> \<Rightarrow> \<tau> \<Rightarrow> bool"} then @{term "star r"} is again of type @{text"\<tau> \<Rightarrow> 

705 
\<tau> \<Rightarrow> bool"}, and @{prop"star r x y"} means that @{text x} and @{text y} are in 

67613  706 
the relation @{term"star r"}. Think @{term"r\<^sup>*"} when you see @{term"star 
47269  707 
r"}, because @{text"star r"} is meant to be the reflexive transitive closure. 
708 
That is, @{prop"star r x y"} is meant to be true if from @{text x} we can 

709 
reach @{text y} in finitely many @{text r} steps. This concept is naturally 

67406  710 
defined inductively:\<close> 
47269  711 

712 
inductive star :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" for r where 

713 
refl: "star r x x"  

714 
step: "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z" 

715 

67406  716 
text\<open>The base case @{thm[source] refl} is reflexivity: @{term "x=y"}. The 
47269  717 
step case @{thm[source]step} combines an @{text r} step (from @{text x} to 
47711  718 
@{text y}) and a @{term"star r"} step (from @{text y} to @{text z}) into a 
719 
@{term"star r"} step (from @{text x} to @{text z}). 

47269  720 
The ``\isacom{for}~@{text r}'' in the header is merely a hint to Isabelle 
721 
that @{text r} is a fixed parameter of @{const star}, in contrast to the 

722 
further parameters of @{const star}, which change. As a result, Isabelle 

723 
generates a simpler induction rule. 

724 

725 
By definition @{term"star r"} is reflexive. It is also transitive, but we 

67406  726 
need rule induction to prove that:\<close> 
47269  727 

728 
lemma star_trans: "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z" 

729 
apply(induction rule: star.induct) 

730 
(*<*) 

731 
defer 

732 
apply(rename_tac u x y) 

733 
defer 

734 
(*>*) 

67406  735 
txt\<open>The induction is over @{prop"star r x y"} (the first matching assumption) 
54212  736 
and we try to prove \mbox{@{prop"star r y z \<Longrightarrow> star r x z"}}, 
47269  737 
which we abbreviate by @{prop"P x y"}. These are our two subgoals: 
738 
@{subgoals[display,indent=0]} 

739 
The first one is @{prop"P x x"}, the result of case @{thm[source]refl}, 

55348  740 
and it is trivial:\index{assumption@@{text assumption}} 
67406  741 
\<close> 
47269  742 
apply(assumption) 
67406  743 
txt\<open>Let us examine subgoal @{text 2}, case @{thm[source] step}. 
47269  744 
Assumptions @{prop"r u x"} and \mbox{@{prop"star r x y"}} 
745 
are the premises of rule @{thm[source]step}. 

746 
Assumption @{prop"star r y z \<Longrightarrow> star r x z"} is \mbox{@{prop"P x y"}}, 

747 
the IH coming from @{prop"star r x y"}. We have to prove @{prop"P u y"}, 

748 
which we do by assuming @{prop"star r y z"} and proving @{prop"star r u z"}. 

749 
The proof itself is straightforward: from \mbox{@{prop"star r y z"}} the IH 

750 
leads to @{prop"star r x z"} which, together with @{prop"r u x"}, 

751 
leads to \mbox{@{prop"star r u z"}} via rule @{thm[source]step}: 

67406  752 
\<close> 
47269  753 
apply(metis step) 
754 
done 

755 

67406  756 
text\<open>\index{rule induction)} 
47269  757 

52361  758 
\subsection{The General Case} 
47269  759 

760 
Inductive definitions have approximately the following general form: 

761 
\begin{quote} 

762 
\isacom{inductive} @{text"I :: \"\<tau> \<Rightarrow> bool\""} \isacom{where} 

763 
\end{quote} 

764 
followed by a sequence of (possibly named) rules of the form 

765 
\begin{quote} 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52782
diff
changeset

766 
@{text "\<lbrakk> I a\<^sub>1; \<dots>; I a\<^sub>n \<rbrakk> \<Longrightarrow> I a"} 
47269  767 
\end{quote} 
768 
separated by @{text""}. As usual, @{text n} can be 0. 

769 
The corresponding rule induction principle 

770 
@{text I.induct} applies to propositions of the form 

771 
\begin{quote} 

772 
@{prop "I x \<Longrightarrow> P x"} 

773 
\end{quote} 

774 
where @{text P} may itself be a chain of implications. 

775 
\begin{warn} 

776 
Rule induction is always on the leftmost premise of the goal. 

777 
Hence @{text "I x"} must be the first premise. 

778 
\end{warn} 

779 
Proving @{prop "I x \<Longrightarrow> P x"} by rule induction means proving 

780 
for every rule of @{text I} that @{text P} is invariant: 

781 
\begin{quote} 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52782
diff
changeset

782 
@{text "\<lbrakk> I a\<^sub>1; P a\<^sub>1; \<dots>; I a\<^sub>n; P a\<^sub>n \<rbrakk> \<Longrightarrow> P a"} 
47269  783 
\end{quote} 
784 

785 
The above format for inductive definitions is simplified in a number of 

786 
respects. @{text I} can have any number of arguments and each rule can have 

55317  787 
additional premises not involving @{text I}, socalled \conceptidx{side 
788 
conditions}{side condition}. In rule inductions, these side conditions appear as additional 

47269  789 
assumptions. The \isacom{for} clause seen in the definition of the reflexive 
55361  790 
transitive closure simplifies the induction rule. 
791 
\index{inductive definition)} 

54231  792 

54436  793 
\subsection*{Exercises} 
54186  794 

54231  795 
\begin{exercise} 
58502  796 
Formalize the following definition of palindromes 
54231  797 
\begin{itemize} 
798 
\item The empty list and a singleton list are palindromes. 

799 
\item If @{text xs} is a palindrome, so is @{term "a # xs @ [a]"}. 

800 
\end{itemize} 

801 
as an inductive predicate @{text "palindrome ::"} @{typ "'a list \<Rightarrow> bool"} 

802 
and prove that @{prop "rev xs = xs"} if @{text xs} is a palindrome. 

803 
\end{exercise} 

804 

54212  805 
\exercise 
54231  806 
We could also have defined @{const star} as follows: 
67406  807 
\<close> 
54212  808 

809 
inductive star' :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" for r where 

810 
refl': "star' r x x"  

811 
step': "star' r x y \<Longrightarrow> r y z \<Longrightarrow> star' r x z" 

812 

67406  813 
text\<open> 
56116  814 
The single @{text r} step is performed after rather than before the @{text star'} 
54217  815 
steps. Prove @{prop "star' r x y \<Longrightarrow> star r x y"} and 
60605  816 
@{prop "star r x y \<Longrightarrow> star' r x y"}. You may need lemmas. 
54217  817 
Note that rule induction fails 
818 
if the assumption about the inductive predicate is not the first assumption. 

54212  819 
\endexercise 
820 

54292  821 
\begin{exercise}\label{exe:iter} 
54290  822 
Analogous to @{const star}, give an inductive definition of the @{text n}fold iteration 
823 
of a relation @{text r}: @{term "iter r n x y"} should hold if there are @{text x\<^sub>0}, \dots, @{text x\<^sub>n} 

824 
such that @{prop"x = x\<^sub>0"}, @{prop"x\<^sub>n = y"} and @{text"r x\<^bsub>i\<^esub> x\<^bsub>i+1\<^esub>"} for 

825 
all @{prop"i < n"}. Correct and prove the following claim: 

826 
@{prop"star r x y \<Longrightarrow> iter r n x y"}. 

827 
\end{exercise} 

828 

61012  829 
\begin{exercise}\label{exe:cfg} 
54218  830 
A contextfree grammar can be seen as an inductive definition where each 
831 
nonterminal $A$ is an inductively defined predicate on lists of terminal 

56116  832 
symbols: $A(w)$ means that $w$ is in the language generated by $A$. 
54218  833 
For example, the production $S \to a S b$ can be viewed as the implication 
834 
@{prop"S w \<Longrightarrow> S (a # w @ [b])"} where @{text a} and @{text b} are terminal symbols, 

835 
i.e., elements of some alphabet. The alphabet can be defined like this: 

836 
\isacom{datatype} @{text"alpha = a  b  \<dots>"} 

837 

838 
Define the two grammars (where $\varepsilon$ is the empty word) 

839 
\[ 

840 
\begin{array}{r@ {\quad}c@ {\quad}l} 

841 
S &\to& \varepsilon \quad\mid\quad aSb \quad\mid\quad SS \\ 

842 
T &\to& \varepsilon \quad\mid\quad TaTb 

843 
\end{array} 

844 
\] 

845 
as two inductive predicates. 

846 
If you think of @{text a} and @{text b} as ``@{text "("}'' and ``@{text ")"}'', 

56989  847 
the grammar defines strings of balanced parentheses. 
848 
Prove @{prop"T w \<Longrightarrow> S w"} and \mbox{@{prop "S w \<Longrightarrow> T w"}} separately and conclude 

54218  849 
@{prop "S w = T w"}. 
850 
\end{exercise} 

851 

54212  852 
\ifsem 
54186  853 
\begin{exercise} 
54203  854 
In \autoref{sec:AExp} we defined a recursive evaluation function 
855 
@{text "aval :: aexp \<Rightarrow> state \<Rightarrow> val"}. 

856 
Define an inductive evaluation predicate 

857 
@{text "aval_rel :: aexp \<Rightarrow> state \<Rightarrow> val \<Rightarrow> bool"} 

858 
and prove that it agrees with the recursive function: 

859 
@{prop "aval_rel a s v \<Longrightarrow> aval a s = v"}, 

860 
@{prop "aval a s = v \<Longrightarrow> aval_rel a s v"} and thus 

861 
\noquotes{@{prop [source] "aval_rel a s v \<longleftrightarrow> aval a s = v"}}. 

862 
\end{exercise} 

863 

864 
\begin{exercise} 

54210  865 
Consider the stack machine from Chapter~3 
866 
and recall the concept of \concept{stack underflow} 

867 
from Exercise~\ref{exe:stackunderflow}. 

868 
Define an inductive predicate 

54186  869 
@{text "ok :: nat \<Rightarrow> instr list \<Rightarrow> nat \<Rightarrow> bool"} 
870 
such that @{text "ok n is n'"} means that with any initial stack of length 

871 
@{text n} the instructions @{text "is"} can be executed 

872 
without stack underflow and that the final stack has length @{text n'}. 

873 
Prove that @{text ok} correctly computes the final stack size 

874 
@{prop[display] "\<lbrakk>ok n is n'; length stk = n\<rbrakk> \<Longrightarrow> length (exec is s stk) = n'"} 

875 
and that instruction sequences generated by @{text comp} 

876 
cannot cause stack underflow: \ @{text "ok n (comp a) ?"} \ for 

877 
some suitable value of @{text "?"}. 

878 
\end{exercise} 

879 
\fi 

67406  880 
\<close> 
47269  881 
(*<*) 
882 
end 

883 
(*>*) 