13999
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{Induction}%
|
17125
|
4 |
%
|
|
5 |
\isadelimtheory
|
|
6 |
%
|
|
7 |
\endisadelimtheory
|
|
8 |
%
|
|
9 |
\isatagtheory
|
|
10 |
%
|
|
11 |
\endisatagtheory
|
|
12 |
{\isafoldtheory}%
|
|
13 |
%
|
|
14 |
\isadelimtheory
|
|
15 |
%
|
|
16 |
\endisadelimtheory
|
13999
|
17 |
%
|
|
18 |
\isamarkupsection{Case distinction and induction \label{sec:Induct}%
|
|
19 |
}
|
|
20 |
\isamarkuptrue%
|
|
21 |
%
|
|
22 |
\begin{isamarkuptext}%
|
|
23 |
Computer science applications abound with inductively defined
|
|
24 |
structures, which is why we treat them in more detail. HOL already
|
|
25 |
comes with a datatype of lists with the two constructors \isa{Nil}
|
|
26 |
and \isa{Cons}. \isa{Nil} is written \isa{{\isacharbrackleft}{\isacharbrackright}} and \isa{Cons\ x\ xs} is written \isa{x\ {\isacharhash}\ xs}.%
|
|
27 |
\end{isamarkuptext}%
|
|
28 |
\isamarkuptrue%
|
|
29 |
%
|
|
30 |
\isamarkupsubsection{Case distinction\label{sec:CaseDistinction}%
|
|
31 |
}
|
|
32 |
\isamarkuptrue%
|
|
33 |
%
|
|
34 |
\begin{isamarkuptext}%
|
|
35 |
We have already met the \isa{cases} method for performing
|
|
36 |
binary case splits. Here is another example:%
|
|
37 |
\end{isamarkuptext}%
|
17175
|
38 |
\isamarkuptrue%
|
|
39 |
\isacommand{lemma}\isamarkupfalse%
|
|
40 |
\ {\isachardoublequoteopen}{\isasymnot}\ A\ {\isasymor}\ A{\isachardoublequoteclose}\isanewline
|
17125
|
41 |
%
|
|
42 |
\isadelimproof
|
|
43 |
%
|
|
44 |
\endisadelimproof
|
|
45 |
%
|
|
46 |
\isatagproof
|
17175
|
47 |
\isacommand{proof}\isamarkupfalse%
|
|
48 |
\ cases\isanewline
|
|
49 |
\ \ \isacommand{assume}\isamarkupfalse%
|
|
50 |
\ {\isachardoublequoteopen}A{\isachardoublequoteclose}\ \isacommand{thus}\isamarkupfalse%
|
|
51 |
\ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
|
|
52 |
\isanewline
|
|
53 |
\isacommand{next}\isamarkupfalse%
|
|
54 |
\isanewline
|
|
55 |
\ \ \isacommand{assume}\isamarkupfalse%
|
|
56 |
\ {\isachardoublequoteopen}{\isasymnot}\ A{\isachardoublequoteclose}\ \isacommand{thus}\isamarkupfalse%
|
|
57 |
\ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
|
|
58 |
\isanewline
|
|
59 |
\isacommand{qed}\isamarkupfalse%
|
|
60 |
%
|
17125
|
61 |
\endisatagproof
|
|
62 |
{\isafoldproof}%
|
|
63 |
%
|
|
64 |
\isadelimproof
|
|
65 |
%
|
|
66 |
\endisadelimproof
|
13999
|
67 |
%
|
|
68 |
\begin{isamarkuptext}%
|
|
69 |
\noindent The two cases must come in this order because \isa{cases} merely abbreviates \isa{{\isacharparenleft}rule\ case{\isacharunderscore}split{\isacharunderscore}thm{\isacharparenright}} where
|
|
70 |
\isa{case{\isacharunderscore}split{\isacharunderscore}thm} is \isa{{\isasymlbrakk}{\isacharquery}P\ {\isasymLongrightarrow}\ {\isacharquery}Q{\isacharsemicolon}\ {\isasymnot}\ {\isacharquery}P\ {\isasymLongrightarrow}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q}. If we reverse
|
|
71 |
the order of the two cases in the proof, the first case would prove
|
|
72 |
\isa{{\isasymnot}\ A\ {\isasymLongrightarrow}\ {\isasymnot}\ A\ {\isasymor}\ A} which would solve the first premise of
|
|
73 |
\isa{case{\isacharunderscore}split{\isacharunderscore}thm}, instantiating \isa{{\isacharquery}P} with \isa{{\isasymnot}\ A}, thus making the second premise \isa{{\isasymnot}\ {\isasymnot}\ A\ {\isasymLongrightarrow}\ {\isasymnot}\ A\ {\isasymor}\ A}.
|
|
74 |
Therefore the order of subgoals is not always completely arbitrary.
|
|
75 |
|
|
76 |
The above proof is appropriate if \isa{A} is textually small.
|
|
77 |
However, if \isa{A} is large, we do not want to repeat it. This can
|
|
78 |
be avoided by the following idiom%
|
|
79 |
\end{isamarkuptext}%
|
17175
|
80 |
\isamarkuptrue%
|
|
81 |
\isacommand{lemma}\isamarkupfalse%
|
|
82 |
\ {\isachardoublequoteopen}{\isasymnot}\ A\ {\isasymor}\ A{\isachardoublequoteclose}\isanewline
|
17125
|
83 |
%
|
|
84 |
\isadelimproof
|
|
85 |
%
|
|
86 |
\endisadelimproof
|
|
87 |
%
|
|
88 |
\isatagproof
|
17175
|
89 |
\isacommand{proof}\isamarkupfalse%
|
|
90 |
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}A{\isachardoublequoteclose}{\isacharparenright}\isanewline
|
|
91 |
\ \ \isacommand{case}\isamarkupfalse%
|
|
92 |
\ True\ \isacommand{thus}\isamarkupfalse%
|
|
93 |
\ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
|
|
94 |
\isanewline
|
|
95 |
\isacommand{next}\isamarkupfalse%
|
|
96 |
\isanewline
|
|
97 |
\ \ \isacommand{case}\isamarkupfalse%
|
|
98 |
\ False\ \isacommand{thus}\isamarkupfalse%
|
|
99 |
\ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
|
|
100 |
\isanewline
|
|
101 |
\isacommand{qed}\isamarkupfalse%
|
|
102 |
%
|
17125
|
103 |
\endisatagproof
|
|
104 |
{\isafoldproof}%
|
|
105 |
%
|
|
106 |
\isadelimproof
|
|
107 |
%
|
|
108 |
\endisadelimproof
|
13999
|
109 |
%
|
|
110 |
\begin{isamarkuptext}%
|
|
111 |
\noindent which is like the previous proof but instantiates
|
|
112 |
\isa{{\isacharquery}P} right away with \isa{A}. Thus we could prove the two
|
25412
|
113 |
cases in any order. The phrase \isakeyword{case}~\isa{True}
|
|
114 |
abbreviates \isakeyword{assume}~\isa{True{\isacharcolon}\ A} and analogously for
|
13999
|
115 |
\isa{False} and \isa{{\isasymnot}\ A}.
|
|
116 |
|
|
117 |
The same game can be played with other datatypes, for example lists,
|
|
118 |
where \isa{tl} is the tail of a list, and \isa{length} returns a
|
|
119 |
natural number (remember: $0-1=0$):%
|
|
120 |
\end{isamarkuptext}%
|
17175
|
121 |
\isamarkuptrue%
|
|
122 |
\isacommand{lemma}\isamarkupfalse%
|
|
123 |
\ {\isachardoublequoteopen}length{\isacharparenleft}tl\ xs{\isacharparenright}\ {\isacharequal}\ length\ xs\ {\isacharminus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
|
17125
|
124 |
%
|
|
125 |
\isadelimproof
|
|
126 |
%
|
|
127 |
\endisadelimproof
|
|
128 |
%
|
|
129 |
\isatagproof
|
17175
|
130 |
\isacommand{proof}\isamarkupfalse%
|
|
131 |
\ {\isacharparenleft}cases\ xs{\isacharparenright}\isanewline
|
|
132 |
\ \ \isacommand{case}\isamarkupfalse%
|
|
133 |
\ Nil\ \isacommand{thus}\isamarkupfalse%
|
|
134 |
\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
|
|
135 |
\ simp\isanewline
|
|
136 |
\isacommand{next}\isamarkupfalse%
|
|
137 |
\isanewline
|
|
138 |
\ \ \isacommand{case}\isamarkupfalse%
|
|
139 |
\ Cons\ \isacommand{thus}\isamarkupfalse%
|
|
140 |
\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
|
|
141 |
\ simp\isanewline
|
|
142 |
\isacommand{qed}\isamarkupfalse%
|
|
143 |
%
|
17125
|
144 |
\endisatagproof
|
|
145 |
{\isafoldproof}%
|
|
146 |
%
|
|
147 |
\isadelimproof
|
|
148 |
%
|
|
149 |
\endisadelimproof
|
13999
|
150 |
%
|
|
151 |
\begin{isamarkuptext}%
|
25412
|
152 |
\noindent Here \isakeyword{case}~\isa{Nil} abbreviates
|
|
153 |
\isakeyword{assume}~\isa{Nil{\isacharcolon}}~\isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} and
|
|
154 |
\isakeyword{case}~\isa{Cons} abbreviates \isakeyword{fix}~\isa{{\isacharquery}\ {\isacharquery}{\isacharquery}}
|
|
155 |
\isakeyword{assume}~\isa{Cons{\isacharcolon}}~\isa{xs\ {\isacharequal}\ {\isacharquery}\ {\isacharhash}\ {\isacharquery}{\isacharquery}},
|
13999
|
156 |
where \isa{{\isacharquery}} and \isa{{\isacharquery}{\isacharquery}}
|
|
157 |
stand for variable names that have been chosen by the system.
|
|
158 |
Therefore we cannot refer to them.
|
|
159 |
Luckily, this proof is simple enough we do not need to refer to them.
|
|
160 |
However, sometimes one may have to. Hence Isar offers a simple scheme for
|
|
161 |
naming those variables: replace the anonymous \isa{Cons} by
|
25412
|
162 |
\isa{{\isacharparenleft}Cons\ y\ ys{\isacharparenright}}, which abbreviates \isakeyword{fix}~\isa{y\ ys}
|
|
163 |
\isakeyword{assume}~\isa{Cons{\isacharcolon}}~\isa{xs\ {\isacharequal}\ y\ {\isacharhash}\ ys}.
|
13999
|
164 |
In each \isakeyword{case} the assumption can be
|
|
165 |
referred to inside the proof by the name of the constructor. In
|
|
166 |
Section~\ref{sec:full-Ind} below we will come across an example
|
25403
|
167 |
of this.
|
|
168 |
|
|
169 |
\subsection{Structural induction}
|
|
170 |
|
13999
|
171 |
We start with an inductive proof where both cases are proved automatically:%
|
|
172 |
\end{isamarkuptext}%
|
17175
|
173 |
\isamarkuptrue%
|
|
174 |
\isacommand{lemma}\isamarkupfalse%
|
|
175 |
\ {\isachardoublequoteopen}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat{\isasymle}n{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
|
17125
|
176 |
%
|
|
177 |
\isadelimproof
|
|
178 |
%
|
|
179 |
\endisadelimproof
|
|
180 |
%
|
|
181 |
\isatagproof
|
17175
|
182 |
\isacommand{by}\isamarkupfalse%
|
25427
|
183 |
\ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all%
|
17125
|
184 |
\endisatagproof
|
|
185 |
{\isafoldproof}%
|
|
186 |
%
|
|
187 |
\isadelimproof
|
|
188 |
%
|
|
189 |
\endisadelimproof
|
13999
|
190 |
%
|
|
191 |
\begin{isamarkuptext}%
|
15909
|
192 |
\noindent The constraint \isa{{\isacharcolon}{\isacharcolon}nat} is needed because all of
|
|
193 |
the operations involved are overloaded.
|
25427
|
194 |
This proof also demonstrates that \isakeyword{by} can take two arguments,
|
|
195 |
one to start and one to finish the proof --- the latter is optional.
|
15909
|
196 |
|
|
197 |
If we want to expose more of the structure of the
|
13999
|
198 |
proof, we can use pattern matching to avoid having to repeat the goal
|
|
199 |
statement:%
|
|
200 |
\end{isamarkuptext}%
|
17175
|
201 |
\isamarkuptrue%
|
|
202 |
\isacommand{lemma}\isamarkupfalse%
|
|
203 |
\ {\isachardoublequoteopen}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat{\isasymle}n{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequoteopen}{\isacharquery}P\ n{\isachardoublequoteclose}{\isacharparenright}\isanewline
|
17125
|
204 |
%
|
|
205 |
\isadelimproof
|
|
206 |
%
|
|
207 |
\endisadelimproof
|
|
208 |
%
|
|
209 |
\isatagproof
|
17175
|
210 |
\isacommand{proof}\isamarkupfalse%
|
|
211 |
\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
|
|
212 |
\ \ \isacommand{show}\isamarkupfalse%
|
|
213 |
\ {\isachardoublequoteopen}{\isacharquery}P\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
|
|
214 |
\ simp\isanewline
|
|
215 |
\isacommand{next}\isamarkupfalse%
|
|
216 |
\isanewline
|
|
217 |
\ \ \isacommand{fix}\isamarkupfalse%
|
|
218 |
\ n\ \isacommand{assume}\isamarkupfalse%
|
|
219 |
\ {\isachardoublequoteopen}{\isacharquery}P\ n{\isachardoublequoteclose}\isanewline
|
|
220 |
\ \ \isacommand{thus}\isamarkupfalse%
|
|
221 |
\ {\isachardoublequoteopen}{\isacharquery}P{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
|
|
222 |
\ simp\isanewline
|
|
223 |
\isacommand{qed}\isamarkupfalse%
|
|
224 |
%
|
17125
|
225 |
\endisatagproof
|
|
226 |
{\isafoldproof}%
|
|
227 |
%
|
|
228 |
\isadelimproof
|
|
229 |
%
|
|
230 |
\endisadelimproof
|
13999
|
231 |
%
|
|
232 |
\begin{isamarkuptext}%
|
|
233 |
\noindent We could refine this further to show more of the equational
|
|
234 |
proof. Instead we explore the same avenue as for case distinctions:
|
|
235 |
introducing context via the \isakeyword{case} command:%
|
|
236 |
\end{isamarkuptext}%
|
17175
|
237 |
\isamarkuptrue%
|
|
238 |
\isacommand{lemma}\isamarkupfalse%
|
|
239 |
\ {\isachardoublequoteopen}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isasymle}\ n{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
|
17125
|
240 |
%
|
|
241 |
\isadelimproof
|
|
242 |
%
|
|
243 |
\endisadelimproof
|
|
244 |
%
|
|
245 |
\isatagproof
|
17175
|
246 |
\isacommand{proof}\isamarkupfalse%
|
|
247 |
\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
|
|
248 |
\ \ \isacommand{case}\isamarkupfalse%
|
|
249 |
\ {\isadigit{0}}\ \isacommand{show}\isamarkupfalse%
|
|
250 |
\ {\isacharquery}case\ \isacommand{by}\isamarkupfalse%
|
|
251 |
\ simp\isanewline
|
|
252 |
\isacommand{next}\isamarkupfalse%
|
|
253 |
\isanewline
|
|
254 |
\ \ \isacommand{case}\isamarkupfalse%
|
|
255 |
\ Suc\ \isacommand{thus}\isamarkupfalse%
|
|
256 |
\ {\isacharquery}case\ \isacommand{by}\isamarkupfalse%
|
|
257 |
\ simp\isanewline
|
|
258 |
\isacommand{qed}\isamarkupfalse%
|
|
259 |
%
|
17125
|
260 |
\endisatagproof
|
|
261 |
{\isafoldproof}%
|
|
262 |
%
|
|
263 |
\isadelimproof
|
|
264 |
%
|
|
265 |
\endisadelimproof
|
13999
|
266 |
%
|
|
267 |
\begin{isamarkuptext}%
|
|
268 |
\noindent The implicitly defined \isa{{\isacharquery}case} refers to the
|
|
269 |
corresponding case to be proved, i.e.\ \isa{{\isacharquery}P\ {\isadigit{0}}} in the first case and
|
|
270 |
\isa{{\isacharquery}P{\isacharparenleft}Suc\ n{\isacharparenright}} in the second case. Context \isakeyword{case}~\isa{{\isadigit{0}}} is
|
|
271 |
empty whereas \isakeyword{case}~\isa{Suc} assumes \isa{{\isacharquery}P\ n}. Again we
|
|
272 |
have the same problem as with case distinctions: we cannot refer to an anonymous \isa{n}
|
|
273 |
in the induction step because it has not been introduced via \isakeyword{fix}
|
|
274 |
(in contrast to the previous proof). The solution is the one outlined for
|
|
275 |
\isa{Cons} above: replace \isa{Suc} by \isa{{\isacharparenleft}Suc\ i{\isacharparenright}}:%
|
|
276 |
\end{isamarkuptext}%
|
17175
|
277 |
\isamarkuptrue%
|
|
278 |
\isacommand{lemma}\isamarkupfalse%
|
|
279 |
\ \isakeyword{fixes}\ n{\isacharcolon}{\isacharcolon}nat\ \isakeyword{shows}\ {\isachardoublequoteopen}n\ {\isacharless}\ n{\isacharasterisk}n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
|
17125
|
280 |
%
|
|
281 |
\isadelimproof
|
|
282 |
%
|
|
283 |
\endisadelimproof
|
|
284 |
%
|
|
285 |
\isatagproof
|
17175
|
286 |
\isacommand{proof}\isamarkupfalse%
|
|
287 |
\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
|
|
288 |
\ \ \isacommand{case}\isamarkupfalse%
|
|
289 |
\ {\isadigit{0}}\ \isacommand{show}\isamarkupfalse%
|
|
290 |
\ {\isacharquery}case\ \isacommand{by}\isamarkupfalse%
|
|
291 |
\ simp\isanewline
|
|
292 |
\isacommand{next}\isamarkupfalse%
|
|
293 |
\isanewline
|
|
294 |
\ \ \isacommand{case}\isamarkupfalse%
|
|
295 |
\ {\isacharparenleft}Suc\ i{\isacharparenright}\ \isacommand{thus}\isamarkupfalse%
|
|
296 |
\ {\isachardoublequoteopen}Suc\ i\ {\isacharless}\ Suc\ i\ {\isacharasterisk}\ Suc\ i\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
|
|
297 |
\ simp\isanewline
|
|
298 |
\isacommand{qed}\isamarkupfalse%
|
|
299 |
%
|
17125
|
300 |
\endisatagproof
|
|
301 |
{\isafoldproof}%
|
|
302 |
%
|
|
303 |
\isadelimproof
|
|
304 |
%
|
|
305 |
\endisadelimproof
|
13999
|
306 |
%
|
|
307 |
\begin{isamarkuptext}%
|
|
308 |
\noindent Of course we could again have written
|
|
309 |
\isakeyword{thus}~\isa{{\isacharquery}case} instead of giving the term explicitly
|
25403
|
310 |
but we wanted to use \isa{i} somewhere.
|
|
311 |
|
|
312 |
\subsection{Generalization via \isa{arbitrary}}
|
13999
|
313 |
|
25403
|
314 |
It is frequently necessary to generalize a claim before it becomes
|
|
315 |
provable by induction. The tutorial~\cite{LNCS2283} demonstrates this
|
|
316 |
with \isa{itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys}, where \isa{ys}
|
|
317 |
needs to be universally quantified before induction succeeds.\footnote{\isa{rev\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}},\quad \isa{rev\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharequal}\ rev\ xs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}},\\ \isa{itrev\ {\isacharbrackleft}{\isacharbrackright}\ ys\ {\isacharequal}\ ys},\quad \isa{itrev\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys\ {\isacharequal}\ itrev\ xs\ {\isacharparenleft}x\ {\isacharhash}\ ys{\isacharparenright}}} But
|
|
318 |
strictly speaking, this quantification step is already part of the
|
|
319 |
proof and the quantifiers should not clutter the original claim. This
|
|
320 |
is how the quantification step can be combined with induction:%
|
13999
|
321 |
\end{isamarkuptext}%
|
17175
|
322 |
\isamarkuptrue%
|
|
323 |
\isacommand{lemma}\isamarkupfalse%
|
25403
|
324 |
\ {\isachardoublequoteopen}itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\isanewline
|
|
325 |
%
|
|
326 |
\isadelimproof
|
|
327 |
%
|
|
328 |
\endisadelimproof
|
|
329 |
%
|
|
330 |
\isatagproof
|
|
331 |
\isacommand{by}\isamarkupfalse%
|
25427
|
332 |
\ {\isacharparenleft}induct\ xs\ arbitrary{\isacharcolon}\ ys{\isacharparenright}\ simp{\isacharunderscore}all%
|
25403
|
333 |
\endisatagproof
|
|
334 |
{\isafoldproof}%
|
|
335 |
%
|
|
336 |
\isadelimproof
|
|
337 |
%
|
|
338 |
\endisadelimproof
|
|
339 |
%
|
|
340 |
\begin{isamarkuptext}%
|
|
341 |
\noindent The annotation \isa{arbitrary{\isacharcolon}}~\emph{vars}
|
|
342 |
universally quantifies all \emph{vars} before the induction. Hence
|
|
343 |
they can be replaced by \emph{arbitrary} values in the proof.
|
|
344 |
|
|
345 |
The nice thing about generalization via \isa{arbitrary{\isacharcolon}} is that in
|
|
346 |
the induction step the claim is available in unquantified form but
|
|
347 |
with the generalized variables replaced by \isa{{\isacharquery}}-variables, ready
|
|
348 |
for instantiation. In the above example the
|
|
349 |
induction hypothesis is \isa{itrev\ xs\ {\isacharquery}ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ {\isacharquery}ys}.
|
|
350 |
|
|
351 |
For the curious: \isa{arbitrary{\isacharcolon}} introduces \isa{{\isasymAnd}}
|
|
352 |
behind the scenes.
|
|
353 |
|
|
354 |
\subsection{Inductive proofs of conditional formulae}
|
25412
|
355 |
\label{sec:full-Ind}
|
25403
|
356 |
|
|
357 |
Induction also copes well with formulae involving \isa{{\isasymLongrightarrow}}, for example%
|
|
358 |
\end{isamarkuptext}%
|
|
359 |
\isamarkuptrue%
|
|
360 |
\isacommand{lemma}\isamarkupfalse%
|
|
361 |
\ {\isachardoublequoteopen}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequoteclose}\isanewline
|
|
362 |
%
|
|
363 |
\isadelimproof
|
|
364 |
%
|
|
365 |
\endisadelimproof
|
|
366 |
%
|
|
367 |
\isatagproof
|
|
368 |
\isacommand{by}\isamarkupfalse%
|
25427
|
369 |
\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
|
25403
|
370 |
\endisatagproof
|
|
371 |
{\isafoldproof}%
|
|
372 |
%
|
|
373 |
\isadelimproof
|
|
374 |
%
|
|
375 |
\endisadelimproof
|
|
376 |
%
|
|
377 |
\begin{isamarkuptext}%
|
|
378 |
\noindent This is an improvement over that style the
|
|
379 |
tutorial~\cite{LNCS2283} advises, which requires \isa{{\isasymlongrightarrow}}.
|
|
380 |
A further improvement is shown in the following proof:%
|
|
381 |
\end{isamarkuptext}%
|
|
382 |
\isamarkuptrue%
|
|
383 |
\isacommand{lemma}\isamarkupfalse%
|
|
384 |
\ \ {\isachardoublequoteopen}map\ f\ xs\ {\isacharequal}\ map\ f\ ys\ {\isasymLongrightarrow}\ length\ xs\ {\isacharequal}\ length\ ys{\isachardoublequoteclose}\isanewline
|
17125
|
385 |
%
|
|
386 |
\isadelimproof
|
|
387 |
%
|
|
388 |
\endisadelimproof
|
|
389 |
%
|
|
390 |
\isatagproof
|
17175
|
391 |
\isacommand{proof}\isamarkupfalse%
|
25403
|
392 |
\ {\isacharparenleft}induct\ ys\ arbitrary{\isacharcolon}\ xs{\isacharparenright}\isanewline
|
|
393 |
\ \ \isacommand{case}\isamarkupfalse%
|
|
394 |
\ Nil\ \isacommand{thus}\isamarkupfalse%
|
17175
|
395 |
\ {\isacharquery}case\ \isacommand{by}\isamarkupfalse%
|
|
396 |
\ simp\isanewline
|
25403
|
397 |
\isacommand{next}\isamarkupfalse%
|
|
398 |
\isanewline
|
|
399 |
\ \ \isacommand{case}\isamarkupfalse%
|
|
400 |
\ {\isacharparenleft}Cons\ y\ ys{\isacharparenright}\ \ \isacommand{note}\isamarkupfalse%
|
|
401 |
\ Asm\ {\isacharequal}\ Cons\isanewline
|
|
402 |
\ \ \isacommand{show}\isamarkupfalse%
|
|
403 |
\ {\isacharquery}case\isanewline
|
|
404 |
\ \ \isacommand{proof}\isamarkupfalse%
|
|
405 |
\ {\isacharparenleft}cases\ xs{\isacharparenright}\isanewline
|
|
406 |
\ \ \ \ \isacommand{case}\isamarkupfalse%
|
|
407 |
\ Nil\isanewline
|
|
408 |
\ \ \ \ \isacommand{hence}\isamarkupfalse%
|
|
409 |
\ False\ \isacommand{using}\isamarkupfalse%
|
|
410 |
\ Asm{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ \isacommand{by}\isamarkupfalse%
|
|
411 |
\ simp\isanewline
|
|
412 |
\ \ \ \ \isacommand{thus}\isamarkupfalse%
|
|
413 |
\ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
|
|
414 |
\isanewline
|
17175
|
415 |
\ \ \isacommand{next}\isamarkupfalse%
|
|
416 |
\isanewline
|
|
417 |
\ \ \ \ \isacommand{case}\isamarkupfalse%
|
25403
|
418 |
\ {\isacharparenleft}Cons\ x\ xs{\isacharprime}{\isacharparenright}\isanewline
|
|
419 |
\ \ \ \ \isacommand{with}\isamarkupfalse%
|
|
420 |
\ Asm{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ \isacommand{have}\isamarkupfalse%
|
|
421 |
\ {\isachardoublequoteopen}map\ f\ xs{\isacharprime}\ {\isacharequal}\ map\ f\ ys{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
|
25427
|
422 |
\ simp\isanewline
|
25403
|
423 |
\ \ \ \ \isacommand{from}\isamarkupfalse%
|
|
424 |
\ Asm{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}OF\ this{\isacharbrackright}\ {\isacharbackquoteopen}xs\ {\isacharequal}\ x{\isacharhash}xs{\isacharprime}{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%
|
|
425 |
\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
|
17175
|
426 |
\ simp\isanewline
|
|
427 |
\ \ \isacommand{qed}\isamarkupfalse%
|
|
428 |
\isanewline
|
|
429 |
\isacommand{qed}\isamarkupfalse%
|
|
430 |
%
|
17125
|
431 |
\endisatagproof
|
|
432 |
{\isafoldproof}%
|
|
433 |
%
|
|
434 |
\isadelimproof
|
|
435 |
%
|
|
436 |
\endisadelimproof
|
13999
|
437 |
%
|
|
438 |
\begin{isamarkuptext}%
|
25403
|
439 |
\noindent
|
|
440 |
The base case is trivial. In the step case Isar assumes
|
|
441 |
(under the name \isa{Cons}) two propositions:
|
|
442 |
\begin{center}
|
|
443 |
\begin{tabular}{l}
|
|
444 |
\isa{map\ f\ {\isacharquery}xs\ {\isacharequal}\ map\ f\ ys\ {\isasymLongrightarrow}\ length\ {\isacharquery}xs\ {\isacharequal}\ length\ ys}\\
|
|
445 |
\isa{map\ f\ xs\ {\isacharequal}\ map\ f\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}}
|
|
446 |
\end{tabular}
|
|
447 |
\end{center}
|
|
448 |
The first is the induction hypothesis, the second, and this is new,
|
|
449 |
is the premise of the induction step. The actual goal at this point is merely
|
|
450 |
\isa{length\ xs\ {\isacharequal}\ length\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}}. The assumptions are given the new name
|
|
451 |
\isa{Asm} to avoid a name clash further down. The proof procedes with a case distinction on \isa{xs}. In the case \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}, the second of our two
|
|
452 |
assumptions (\isa{Asm{\isacharparenleft}{\isadigit{2}}{\isacharparenright}}) implies the contradiction \isa{{\isadigit{0}}\ {\isacharequal}\ Suc{\isacharparenleft}{\isasymdots}{\isacharparenright}}.
|
|
453 |
In the case \isa{xs\ {\isacharequal}\ x\ {\isacharhash}\ xs{\isacharprime}}, we first obtain
|
|
454 |
\isa{map\ f\ xs{\isacharprime}\ {\isacharequal}\ map\ f\ ys}, from which a forward step with the first assumption (\isa{Asm{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}OF\ this{\isacharbrackright}}) yields \isa{length\ xs{\isacharprime}\ {\isacharequal}\ length\ ys}. Together
|
|
455 |
with \isa{xs\ {\isacharequal}\ x\ {\isacharhash}\ xs} this yields the goal
|
|
456 |
\isa{length\ xs\ {\isacharequal}\ length\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}}.
|
13999
|
457 |
|
25403
|
458 |
|
|
459 |
\subsection{Induction formulae involving \isa{{\isasymAnd}} or \isa{{\isasymLongrightarrow}}}
|
|
460 |
|
|
461 |
Let us now consider abstractly the situation where the goal to be proved
|
|
462 |
contains both \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}}, say \isa{{\isasymAnd}x{\isachardot}\ P\ x\ {\isasymLongrightarrow}\ Q\ x}.
|
|
463 |
This means that in each case of the induction,
|
|
464 |
\isa{{\isacharquery}case} would be of the form \isa{{\isasymAnd}x{\isachardot}\ P{\isacharprime}\ x\ {\isasymLongrightarrow}\ Q{\isacharprime}\ x}. Thus the
|
|
465 |
first proof steps will be the canonical ones, fixing \isa{x} and assuming
|
|
466 |
\isa{P{\isacharprime}\ x}. To avoid this tedium, induction performs the canonical steps
|
|
467 |
automatically: in each step case, the assumptions contain both the
|
|
468 |
usual induction hypothesis and \isa{P{\isacharprime}\ x}, whereas \isa{{\isacharquery}case} is only
|
|
469 |
\isa{Q{\isacharprime}\ x}.
|
|
470 |
|
|
471 |
\subsection{Rule induction}
|
|
472 |
|
13999
|
473 |
HOL also supports inductively defined sets. See \cite{LNCS2283}
|
|
474 |
for details. As an example we define our own version of the reflexive
|
|
475 |
transitive closure of a relation --- HOL provides a predefined one as well.%
|
|
476 |
\end{isamarkuptext}%
|
17175
|
477 |
\isamarkuptrue%
|
25056
|
478 |
\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse%
|
|
479 |
\isanewline
|
|
480 |
\ \ rtc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequoteclose}\ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharunderscore}{\isacharasterisk}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
|
|
481 |
\ \ \isakeyword{for}\ r\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequoteclose}\isanewline
|
|
482 |
\isakeyword{where}\isanewline
|
|
483 |
\ \ refl{\isacharcolon}\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\isanewline
|
|
484 |
{\isacharbar}\ step{\isacharcolon}\ \ {\isachardoublequoteopen}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}%
|
13999
|
485 |
\begin{isamarkuptext}%
|
|
486 |
\noindent
|
|
487 |
First the constant is declared as a function on binary
|
|
488 |
relations (with concrete syntax \isa{r{\isacharasterisk}} instead of \isa{rtc\ r}), then the defining clauses are given. We will now prove that
|
|
489 |
\isa{r{\isacharasterisk}} is indeed transitive:%
|
|
490 |
\end{isamarkuptext}%
|
17175
|
491 |
\isamarkuptrue%
|
|
492 |
\isacommand{lemma}\isamarkupfalse%
|
|
493 |
\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\isanewline
|
17125
|
494 |
%
|
|
495 |
\isadelimproof
|
|
496 |
%
|
|
497 |
\endisadelimproof
|
|
498 |
%
|
|
499 |
\isatagproof
|
17175
|
500 |
\isacommand{using}\isamarkupfalse%
|
|
501 |
\ A\isanewline
|
|
502 |
\isacommand{proof}\isamarkupfalse%
|
|
503 |
\ induct\isanewline
|
|
504 |
\ \ \isacommand{case}\isamarkupfalse%
|
|
505 |
\ refl\ \isacommand{thus}\isamarkupfalse%
|
|
506 |
\ {\isacharquery}case\ \isacommand{{\isachardot}}\isamarkupfalse%
|
|
507 |
\isanewline
|
|
508 |
\isacommand{next}\isamarkupfalse%
|
|
509 |
\isanewline
|
|
510 |
\ \ \isacommand{case}\isamarkupfalse%
|
|
511 |
\ step\ \isacommand{thus}\isamarkupfalse%
|
|
512 |
\ {\isacharquery}case\ \isacommand{by}\isamarkupfalse%
|
|
513 |
{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isachardot}step{\isacharparenright}\isanewline
|
|
514 |
\isacommand{qed}\isamarkupfalse%
|
|
515 |
%
|
17125
|
516 |
\endisatagproof
|
|
517 |
{\isafoldproof}%
|
|
518 |
%
|
|
519 |
\isadelimproof
|
|
520 |
%
|
|
521 |
\endisadelimproof
|
13999
|
522 |
%
|
|
523 |
\begin{isamarkuptext}%
|
|
524 |
\noindent Rule induction is triggered by a fact $(x_1,\dots,x_n)
|
|
525 |
\in R$ piped into the proof, here \isakeyword{using}~\isa{A}. The
|
|
526 |
proof itself follows the inductive definition very
|
|
527 |
closely: there is one case for each rule, and it has the same name as
|
|
528 |
the rule, analogous to structural induction.
|
|
529 |
|
|
530 |
However, this proof is rather terse. Here is a more readable version:%
|
|
531 |
\end{isamarkuptext}%
|
17175
|
532 |
\isamarkuptrue%
|
|
533 |
\isacommand{lemma}\isamarkupfalse%
|
25403
|
534 |
\ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\isanewline
|
17125
|
535 |
%
|
|
536 |
\isadelimproof
|
|
537 |
%
|
|
538 |
\endisadelimproof
|
|
539 |
%
|
|
540 |
\isatagproof
|
25403
|
541 |
\isacommand{using}\isamarkupfalse%
|
|
542 |
\ assms\isanewline
|
17175
|
543 |
\isacommand{proof}\isamarkupfalse%
|
|
544 |
\ induct\isanewline
|
25403
|
545 |
\ \ \isacommand{fix}\isamarkupfalse%
|
17175
|
546 |
\ x\ \isacommand{assume}\isamarkupfalse%
|
|
547 |
\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\ \ %
|
16459
|
548 |
\isamarkupcmt{\isa{B}[\isa{y} := \isa{x}]%
|
|
549 |
}
|
|
550 |
\isanewline
|
25403
|
551 |
\ \ \isacommand{thus}\isamarkupfalse%
|
17175
|
552 |
\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
|
|
553 |
\isanewline
|
25403
|
554 |
\isacommand{next}\isamarkupfalse%
|
17175
|
555 |
\isanewline
|
25403
|
556 |
\ \ \isacommand{fix}\isamarkupfalse%
|
17175
|
557 |
\ x{\isacharprime}\ x\ y\isanewline
|
25403
|
558 |
\ \ \isacommand{assume}\isamarkupfalse%
|
17175
|
559 |
\ {\isadigit{1}}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharprime}{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
|
25403
|
560 |
\ \ \ \ \ \ \ \ \ IH{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
|
|
561 |
\ \ \ \ \ \ \ \ \ B{\isacharcolon}\ \ {\isachardoublequoteopen}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\isanewline
|
|
562 |
\ \ \isacommand{from}\isamarkupfalse%
|
17175
|
563 |
\ {\isadigit{1}}\ IH{\isacharbrackleft}OF\ B{\isacharbrackright}\ \isacommand{show}\isamarkupfalse%
|
|
564 |
\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharprime}{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
|
|
565 |
{\isacharparenleft}rule\ rtc{\isachardot}step{\isacharparenright}\isanewline
|
|
566 |
\isacommand{qed}\isamarkupfalse%
|
|
567 |
%
|
17125
|
568 |
\endisatagproof
|
|
569 |
{\isafoldproof}%
|
|
570 |
%
|
|
571 |
\isadelimproof
|
|
572 |
%
|
|
573 |
\endisadelimproof
|
13999
|
574 |
%
|
|
575 |
\begin{isamarkuptext}%
|
25403
|
576 |
\noindent
|
|
577 |
This time, merely for a change, we start the proof with by feeding both
|
|
578 |
assumptions into the inductive proof. Only the first assumption is
|
|
579 |
``consumed'' by the induction.
|
|
580 |
Since the second one is left over we don't just prove \isa{{\isacharquery}thesis} but
|
|
581 |
\isa{{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharquery}thesis}, just as in the previous proof.
|
|
582 |
The base case is trivial. In the assumptions for the induction step we can
|
13999
|
583 |
see very clearly how things fit together and permit ourselves the
|
|
584 |
obvious forward step \isa{IH{\isacharbrackleft}OF\ B{\isacharbrackright}}.
|
|
585 |
|
25403
|
586 |
The notation \isakeyword{case}~\isa{(}\emph{constructor} \emph{vars}\isa{)}
|
|
587 |
is also supported for inductive definitions. The \emph{constructor} is the
|
|
588 |
name of the rule and the \emph{vars} fix the free variables in the
|
13999
|
589 |
rule; the order of the \emph{vars} must correspond to the
|
25403
|
590 |
left-to-right order of the variables as they appear in the rule.
|
13999
|
591 |
For example, we could start the above detailed proof of the induction
|
25403
|
592 |
with \isakeyword{case}~\isa{(step x' x y)}. In that case we don't need
|
|
593 |
to spell out the assumptions but can refer to them by \isa{step{\isacharparenleft}{\isachardot}{\isacharparenright}},
|
|
594 |
although the resulting text will be quite cryptic.
|
|
595 |
|
|
596 |
\subsection{More induction}
|
|
597 |
|
13999
|
598 |
We close the section by demonstrating how arbitrary induction
|
|
599 |
rules are applied. As a simple example we have chosen recursion
|
|
600 |
induction, i.e.\ induction based on a recursive function
|
|
601 |
definition. However, most of what we show works for induction in
|
|
602 |
general.
|
|
603 |
|
|
604 |
The example is an unusual definition of rotation:%
|
|
605 |
\end{isamarkuptext}%
|
17175
|
606 |
\isamarkuptrue%
|
25403
|
607 |
\isacommand{fun}\isamarkupfalse%
|
|
608 |
\ rot\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
|
|
609 |
{\isachardoublequoteopen}rot\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
|
|
610 |
{\isachardoublequoteopen}rot\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}x{\isacharbrackright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
|
17175
|
611 |
{\isachardoublequoteopen}rot\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ y\ {\isacharhash}\ rot{\isacharparenleft}x{\isacharhash}zs{\isacharparenright}{\isachardoublequoteclose}%
|
13999
|
612 |
\begin{isamarkuptext}%
|
|
613 |
\noindent This yields, among other things, the induction rule
|
|
614 |
\isa{rot{\isachardot}induct}: \begin{isabelle}%
|
25403
|
615 |
{\isasymlbrakk}P\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ P\ {\isacharbrackleft}x{\isacharbrackright}{\isacharsemicolon}\ {\isasymAnd}x\ y\ zs{\isachardot}\ P\ {\isacharparenleft}x\ {\isacharhash}\ zs{\isacharparenright}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}x\ {\isacharhash}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ a{\isadigit{0}}%
|
13999
|
616 |
\end{isabelle}
|
25403
|
617 |
The following proof relies on a default naming scheme for cases: they are
|
13999
|
618 |
called 1, 2, etc, unless they have been named explicitly. The latter happens
|
25403
|
619 |
only with datatypes and inductively defined sets, but (usually)
|
|
620 |
not with recursive functions.%
|
13999
|
621 |
\end{isamarkuptext}%
|
17175
|
622 |
\isamarkuptrue%
|
|
623 |
\isacommand{lemma}\isamarkupfalse%
|
|
624 |
\ {\isachardoublequoteopen}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ rot\ xs\ {\isacharequal}\ tl\ xs\ {\isacharat}\ {\isacharbrackleft}hd\ xs{\isacharbrackright}{\isachardoublequoteclose}\isanewline
|
17125
|
625 |
%
|
|
626 |
\isadelimproof
|
|
627 |
%
|
|
628 |
\endisadelimproof
|
|
629 |
%
|
|
630 |
\isatagproof
|
17175
|
631 |
\isacommand{proof}\isamarkupfalse%
|
|
632 |
\ {\isacharparenleft}induct\ xs\ rule{\isacharcolon}\ rot{\isachardot}induct{\isacharparenright}\isanewline
|
|
633 |
\ \ \isacommand{case}\isamarkupfalse%
|
|
634 |
\ {\isadigit{1}}\ \isacommand{thus}\isamarkupfalse%
|
|
635 |
\ {\isacharquery}case\ \isacommand{by}\isamarkupfalse%
|
|
636 |
\ simp\isanewline
|
|
637 |
\isacommand{next}\isamarkupfalse%
|
|
638 |
\isanewline
|
|
639 |
\ \ \isacommand{case}\isamarkupfalse%
|
|
640 |
\ {\isadigit{2}}\ \isacommand{show}\isamarkupfalse%
|
|
641 |
\ {\isacharquery}case\ \isacommand{by}\isamarkupfalse%
|
|
642 |
\ simp\isanewline
|
|
643 |
\isacommand{next}\isamarkupfalse%
|
|
644 |
\isanewline
|
|
645 |
\ \ \isacommand{case}\isamarkupfalse%
|
|
646 |
\ {\isacharparenleft}{\isadigit{3}}\ a\ b\ cs{\isacharparenright}\isanewline
|
|
647 |
\ \ \isacommand{have}\isamarkupfalse%
|
|
648 |
\ {\isachardoublequoteopen}rot\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ cs{\isacharparenright}\ {\isacharequal}\ b\ {\isacharhash}\ rot{\isacharparenleft}a\ {\isacharhash}\ cs{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
|
|
649 |
\ simp\isanewline
|
|
650 |
\ \ \isacommand{also}\isamarkupfalse%
|
|
651 |
\ \isacommand{have}\isamarkupfalse%
|
|
652 |
\ {\isachardoublequoteopen}{\isasymdots}\ {\isacharequal}\ b\ {\isacharhash}\ tl{\isacharparenleft}a\ {\isacharhash}\ cs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}hd{\isacharparenleft}a\ {\isacharhash}\ cs{\isacharparenright}{\isacharbrackright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
|
|
653 |
{\isacharparenleft}simp\ add{\isacharcolon}{\isadigit{3}}{\isacharparenright}\isanewline
|
|
654 |
\ \ \isacommand{also}\isamarkupfalse%
|
|
655 |
\ \isacommand{have}\isamarkupfalse%
|
|
656 |
\ {\isachardoublequoteopen}{\isasymdots}\ {\isacharequal}\ tl\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ cs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}hd\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ cs{\isacharparenright}{\isacharbrackright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
|
|
657 |
\ simp\isanewline
|
|
658 |
\ \ \isacommand{finally}\isamarkupfalse%
|
|
659 |
\ \isacommand{show}\isamarkupfalse%
|
|
660 |
\ {\isacharquery}case\ \isacommand{{\isachardot}}\isamarkupfalse%
|
|
661 |
\isanewline
|
|
662 |
\isacommand{qed}\isamarkupfalse%
|
|
663 |
%
|
17125
|
664 |
\endisatagproof
|
|
665 |
{\isafoldproof}%
|
|
666 |
%
|
|
667 |
\isadelimproof
|
|
668 |
%
|
|
669 |
\endisadelimproof
|
13999
|
670 |
%
|
|
671 |
\begin{isamarkuptext}%
|
|
672 |
\noindent
|
|
673 |
The third case is only shown in gory detail (see \cite{BauerW-TPHOLs01}
|
|
674 |
for how to reason with chains of equations) to demonstrate that the
|
25403
|
675 |
\isakeyword{case}~\isa{(}\emph{constructor} \emph{vars}\isa{)} notation also
|
13999
|
676 |
works for arbitrary induction theorems with numbered cases. The order
|
|
677 |
of the \emph{vars} corresponds to the order of the
|
|
678 |
\isa{{\isasymAnd}}-quantified variables in each case of the induction
|
25403
|
679 |
theorem. For induction theorems produced by \isakeyword{fun} it is
|
13999
|
680 |
the order in which the variables appear on the left-hand side of the
|
|
681 |
equation.
|
|
682 |
|
|
683 |
The proof is so simple that it can be condensed to%
|
|
684 |
\end{isamarkuptext}%
|
17175
|
685 |
\isamarkuptrue%
|
17125
|
686 |
%
|
|
687 |
\isadelimproof
|
|
688 |
%
|
|
689 |
\endisadelimproof
|
|
690 |
%
|
|
691 |
\isatagproof
|
17175
|
692 |
\isacommand{by}\isamarkupfalse%
|
25412
|
693 |
\ {\isacharparenleft}induct\ xs\ rule{\isacharcolon}\ rot{\isachardot}induct{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
|
17125
|
694 |
%
|
|
695 |
\endisatagproof
|
|
696 |
{\isafoldproof}%
|
|
697 |
%
|
|
698 |
\isadelimproof
|
|
699 |
%
|
|
700 |
\endisadelimproof
|
|
701 |
%
|
|
702 |
\isadelimtheory
|
|
703 |
%
|
|
704 |
\endisadelimtheory
|
|
705 |
%
|
|
706 |
\isatagtheory
|
|
707 |
%
|
|
708 |
\endisatagtheory
|
|
709 |
{\isafoldtheory}%
|
|
710 |
%
|
|
711 |
\isadelimtheory
|
|
712 |
%
|
|
713 |
\endisadelimtheory
|
13999
|
714 |
\end{isabellebody}%
|
|
715 |
%%% Local Variables:
|
|
716 |
%%% mode: latex
|
|
717 |
%%% TeX-master: "root"
|
|
718 |
%%% End:
|