10217
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{AB}%
|
17056
|
4 |
%
|
|
5 |
\isadelimtheory
|
|
6 |
%
|
|
7 |
\endisadelimtheory
|
|
8 |
%
|
|
9 |
\isatagtheory
|
|
10 |
%
|
|
11 |
\endisatagtheory
|
|
12 |
{\isafoldtheory}%
|
|
13 |
%
|
|
14 |
\isadelimtheory
|
|
15 |
%
|
|
16 |
\endisadelimtheory
|
10225
|
17 |
%
|
10878
|
18 |
\isamarkupsection{Case Study: A Context Free Grammar%
|
10395
|
19 |
}
|
11866
|
20 |
\isamarkuptrue%
|
10236
|
21 |
%
|
|
22 |
\begin{isamarkuptext}%
|
10242
|
23 |
\label{sec:CFG}
|
11494
|
24 |
\index{grammars!defining inductively|(}%
|
10236
|
25 |
Grammars are nothing but shorthands for inductive definitions of nonterminals
|
|
26 |
which represent sets of strings. For example, the production
|
|
27 |
$A \to B c$ is short for
|
|
28 |
\[ w \in B \Longrightarrow wc \in A \]
|
10878
|
29 |
This section demonstrates this idea with an example
|
|
30 |
due to Hopcroft and Ullman, a grammar for generating all words with an
|
|
31 |
equal number of $a$'s and~$b$'s:
|
10236
|
32 |
\begin{eqnarray}
|
|
33 |
S &\to& \epsilon \mid b A \mid a B \nonumber\\
|
|
34 |
A &\to& a S \mid b A A \nonumber\\
|
|
35 |
B &\to& b S \mid a B B \nonumber
|
|
36 |
\end{eqnarray}
|
10878
|
37 |
At the end we say a few words about the relationship between
|
|
38 |
the original proof \cite[p.\ts81]{HopcroftUllman} and our formal version.
|
10236
|
39 |
|
10299
|
40 |
We start by fixing the alphabet, which consists only of \isa{a}'s
|
10878
|
41 |
and~\isa{b}'s:%
|
10236
|
42 |
\end{isamarkuptext}%
|
17175
|
43 |
\isamarkuptrue%
|
|
44 |
\isacommand{datatype}\isamarkupfalse%
|
|
45 |
\ alfa\ {\isacharequal}\ a\ {\isacharbar}\ b%
|
10236
|
46 |
\begin{isamarkuptext}%
|
|
47 |
\noindent
|
10299
|
48 |
For convenience we include the following easy lemmas as simplification rules:%
|
10236
|
49 |
\end{isamarkuptext}%
|
17175
|
50 |
\isamarkuptrue%
|
|
51 |
\isacommand{lemma}\isamarkupfalse%
|
|
52 |
\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymnoteq}\ a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ b{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}x\ {\isasymnoteq}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ a{\isacharparenright}{\isachardoublequoteclose}\isanewline
|
17056
|
53 |
%
|
|
54 |
\isadelimproof
|
|
55 |
%
|
|
56 |
\endisadelimproof
|
|
57 |
%
|
|
58 |
\isatagproof
|
17175
|
59 |
\isacommand{by}\isamarkupfalse%
|
|
60 |
\ {\isacharparenleft}case{\isacharunderscore}tac\ x{\isacharcomma}\ auto{\isacharparenright}%
|
17056
|
61 |
\endisatagproof
|
|
62 |
{\isafoldproof}%
|
|
63 |
%
|
|
64 |
\isadelimproof
|
|
65 |
%
|
|
66 |
\endisadelimproof
|
11866
|
67 |
%
|
10236
|
68 |
\begin{isamarkuptext}%
|
|
69 |
\noindent
|
|
70 |
Words over this alphabet are of type \isa{alfa\ list}, and
|
10878
|
71 |
the three nonterminals are declared as sets of such words:%
|
10236
|
72 |
\end{isamarkuptext}%
|
17175
|
73 |
\isamarkuptrue%
|
|
74 |
\isacommand{consts}\isamarkupfalse%
|
|
75 |
\ S\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}alfa\ list\ set{\isachardoublequoteclose}\isanewline
|
|
76 |
\ \ \ \ \ \ \ A\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}alfa\ list\ set{\isachardoublequoteclose}\isanewline
|
|
77 |
\ \ \ \ \ \ \ B\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}alfa\ list\ set{\isachardoublequoteclose}%
|
10236
|
78 |
\begin{isamarkuptext}%
|
|
79 |
\noindent
|
10878
|
80 |
The productions above are recast as a \emph{mutual} inductive
|
10242
|
81 |
definition\index{inductive definition!simultaneous}
|
10878
|
82 |
of \isa{S}, \isa{A} and~\isa{B}:%
|
10236
|
83 |
\end{isamarkuptext}%
|
17175
|
84 |
\isamarkuptrue%
|
|
85 |
\isacommand{inductive}\isamarkupfalse%
|
|
86 |
\ S\ A\ B\isanewline
|
10217
|
87 |
\isakeyword{intros}\isanewline
|
17175
|
88 |
\ \ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}\ {\isasymin}\ S{\isachardoublequoteclose}\isanewline
|
|
89 |
\ \ {\isachardoublequoteopen}w\ {\isasymin}\ A\ {\isasymLongrightarrow}\ b{\isacharhash}w\ {\isasymin}\ S{\isachardoublequoteclose}\isanewline
|
|
90 |
\ \ {\isachardoublequoteopen}w\ {\isasymin}\ B\ {\isasymLongrightarrow}\ a{\isacharhash}w\ {\isasymin}\ S{\isachardoublequoteclose}\isanewline
|
10217
|
91 |
\isanewline
|
17175
|
92 |
\ \ {\isachardoublequoteopen}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ a{\isacharhash}w\ \ \ {\isasymin}\ A{\isachardoublequoteclose}\isanewline
|
|
93 |
\ \ {\isachardoublequoteopen}{\isasymlbrakk}\ v{\isasymin}A{\isacharsemicolon}\ w{\isasymin}A\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ b{\isacharhash}v{\isacharat}w\ {\isasymin}\ A{\isachardoublequoteclose}\isanewline
|
10217
|
94 |
\isanewline
|
17175
|
95 |
\ \ {\isachardoublequoteopen}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ b{\isacharhash}w\ \ \ {\isasymin}\ B{\isachardoublequoteclose}\isanewline
|
|
96 |
\ \ {\isachardoublequoteopen}{\isasymlbrakk}\ v\ {\isasymin}\ B{\isacharsemicolon}\ w\ {\isasymin}\ B\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ a{\isacharhash}v{\isacharat}w\ {\isasymin}\ B{\isachardoublequoteclose}%
|
10236
|
97 |
\begin{isamarkuptext}%
|
|
98 |
\noindent
|
10878
|
99 |
First we show that all words in \isa{S} contain the same number of \isa{a}'s and \isa{b}'s. Since the definition of \isa{S} is by mutual
|
|
100 |
induction, so is the proof: we show at the same time that all words in
|
10236
|
101 |
\isa{A} contain one more \isa{a} than \isa{b} and all words in \isa{B} contains one more \isa{b} than \isa{a}.%
|
|
102 |
\end{isamarkuptext}%
|
17175
|
103 |
\isamarkuptrue%
|
|
104 |
\isacommand{lemma}\isamarkupfalse%
|
|
105 |
\ correctness{\isacharcolon}\isanewline
|
23380
|
106 |
\ \ {\isachardoublequoteopen}{\isacharparenleft}w\ {\isasymin}\ S\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymleftarrow}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymleftarrow}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}{\isacharparenright}\ \ \ \ \ {\isasymand}\isanewline
|
|
107 |
\ \ \ {\isacharparenleft}w\ {\isasymin}\ A\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymleftarrow}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymleftarrow}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isasymand}\isanewline
|
|
108 |
\ \ \ {\isacharparenleft}w\ {\isasymin}\ B\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymleftarrow}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymleftarrow}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}%
|
17056
|
109 |
\isadelimproof
|
|
110 |
%
|
|
111 |
\endisadelimproof
|
|
112 |
%
|
|
113 |
\isatagproof
|
16069
|
114 |
%
|
|
115 |
\begin{isamarkuptxt}%
|
|
116 |
\noindent
|
23380
|
117 |
These propositions are expressed with the help of the predefined \isa{filter} function on lists, which has the convenient syntax \isa{{\isacharbrackleft}x{\isasymleftarrow}xs{\isachardot}\ P\ x{\isacharbrackright}}, the list of all elements \isa{x} in \isa{xs} such that \isa{P\ x}
|
16069
|
118 |
holds. Remember that on lists \isa{size} and \isa{length} are synonymous.
|
|
119 |
|
|
120 |
The proof itself is by rule induction and afterwards automatic:%
|
|
121 |
\end{isamarkuptxt}%
|
17175
|
122 |
\isamarkuptrue%
|
|
123 |
\isacommand{by}\isamarkupfalse%
|
|
124 |
\ {\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharcomma}\ auto{\isacharparenright}%
|
17056
|
125 |
\endisatagproof
|
|
126 |
{\isafoldproof}%
|
|
127 |
%
|
|
128 |
\isadelimproof
|
|
129 |
%
|
|
130 |
\endisadelimproof
|
11866
|
131 |
%
|
10236
|
132 |
\begin{isamarkuptext}%
|
|
133 |
\noindent
|
|
134 |
This may seem surprising at first, and is indeed an indication of the power
|
|
135 |
of inductive definitions. But it is also quite straightforward. For example,
|
|
136 |
consider the production $A \to b A A$: if $v,w \in A$ and the elements of $A$
|
10878
|
137 |
contain one more $a$ than~$b$'s, then $bvw$ must again contain one more $a$
|
|
138 |
than~$b$'s.
|
10236
|
139 |
|
|
140 |
As usual, the correctness of syntactic descriptions is easy, but completeness
|
|
141 |
is hard: does \isa{S} contain \emph{all} words with an equal number of
|
|
142 |
\isa{a}'s and \isa{b}'s? It turns out that this proof requires the
|
10878
|
143 |
following lemma: every string with two more \isa{a}'s than \isa{b}'s can be cut somewhere such that each half has one more \isa{a} than
|
10236
|
144 |
\isa{b}. This is best seen by imagining counting the difference between the
|
10283
|
145 |
number of \isa{a}'s and \isa{b}'s starting at the left end of the
|
|
146 |
word. We start with 0 and end (at the right end) with 2. Since each move to the
|
10236
|
147 |
right increases or decreases the difference by 1, we must have passed through
|
|
148 |
1 on our way from 0 to 2. Formally, we appeal to the following discrete
|
|
149 |
intermediate value theorem \isa{nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val}
|
|
150 |
\begin{isabelle}%
|
19654
|
151 |
\ \ \ \ \ {\isasymlbrakk}{\isasymforall}i{\isacharless}n{\isachardot}\ {\isasymbar}f\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isasymbar}\ {\isasymle}\ {\isadigit{1}}{\isacharsemicolon}\ f\ {\isadigit{0}}\ {\isasymle}\ k{\isacharsemicolon}\ k\ {\isasymle}\ f\ n{\isasymrbrakk}\isanewline
|
|
152 |
\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isasymexists}i{\isasymle}n{\isachardot}\ f\ i\ {\isacharequal}\ k%
|
10236
|
153 |
\end{isabelle}
|
|
154 |
where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers,
|
11308
|
155 |
\isa{{\isasymbar}{\isachardot}{\isasymbar}} is the absolute value function\footnote{See
|
|
156 |
Table~\ref{tab:ascii} in the Appendix for the correct \textsc{ascii}
|
11708
|
157 |
syntax.}, and \isa{{\isadigit{1}}} is the integer 1 (see \S\ref{sec:numbers}).
|
10236
|
158 |
|
11147
|
159 |
First we show that our specific function, the difference between the
|
10236
|
160 |
numbers of \isa{a}'s and \isa{b}'s, does indeed only change by 1 in every
|
|
161 |
move to the right. At this point we also start generalizing from \isa{a}'s
|
|
162 |
and \isa{b}'s to an arbitrary property \isa{P}. Otherwise we would have
|
|
163 |
to prove the desired lemma twice, once as stated above and once with the
|
|
164 |
roles of \isa{a}'s and \isa{b}'s interchanged.%
|
|
165 |
\end{isamarkuptext}%
|
17175
|
166 |
\isamarkuptrue%
|
|
167 |
\isacommand{lemma}\isamarkupfalse%
|
|
168 |
\ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}i\ {\isacharless}\ size\ w{\isachardot}\isanewline
|
23380
|
169 |
\ \ {\isasymbar}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymleftarrow}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymleftarrow}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline
|
|
170 |
\ \ \ {\isacharminus}\ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymleftarrow}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymleftarrow}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isasymbar}\ {\isasymle}\ {\isadigit{1}}{\isachardoublequoteclose}%
|
17056
|
171 |
\isadelimproof
|
|
172 |
%
|
|
173 |
\endisadelimproof
|
|
174 |
%
|
|
175 |
\isatagproof
|
16069
|
176 |
%
|
|
177 |
\begin{isamarkuptxt}%
|
|
178 |
\noindent
|
|
179 |
The lemma is a bit hard to read because of the coercion function
|
|
180 |
\isa{int\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ int}. It is required because \isa{size} returns
|
|
181 |
a natural number, but subtraction on type~\isa{nat} will do the wrong thing.
|
|
182 |
Function \isa{take} is predefined and \isa{take\ i\ xs} is the prefix of
|
|
183 |
length \isa{i} of \isa{xs}; below we also need \isa{drop\ i\ xs}, which
|
|
184 |
is what remains after that prefix has been dropped from \isa{xs}.
|
|
185 |
|
|
186 |
The proof is by induction on \isa{w}, with a trivial base case, and a not
|
|
187 |
so trivial induction step. Since it is essentially just arithmetic, we do not
|
|
188 |
discuss it.%
|
|
189 |
\end{isamarkuptxt}%
|
17175
|
190 |
\isamarkuptrue%
|
|
191 |
\isacommand{apply}\isamarkupfalse%
|
|
192 |
{\isacharparenleft}induct{\isacharunderscore}tac\ w{\isacharparenright}\isanewline
|
|
193 |
\isacommand{apply}\isamarkupfalse%
|
|
194 |
{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ abs{\isacharunderscore}if\ take{\isacharunderscore}Cons\ split{\isacharcolon}\ nat{\isachardot}split{\isacharparenright}\isanewline
|
|
195 |
\isacommand{done}\isamarkupfalse%
|
|
196 |
%
|
17056
|
197 |
\endisatagproof
|
|
198 |
{\isafoldproof}%
|
|
199 |
%
|
|
200 |
\isadelimproof
|
|
201 |
%
|
|
202 |
\endisadelimproof
|
11866
|
203 |
%
|
10236
|
204 |
\begin{isamarkuptext}%
|
11494
|
205 |
Finally we come to the above-mentioned lemma about cutting in half a word with two more elements of one sort than of the other sort:%
|
10236
|
206 |
\end{isamarkuptext}%
|
17175
|
207 |
\isamarkuptrue%
|
|
208 |
\isacommand{lemma}\isamarkupfalse%
|
|
209 |
\ part{\isadigit{1}}{\isacharcolon}\isanewline
|
23380
|
210 |
\ {\isachardoublequoteopen}size{\isacharbrackleft}x{\isasymleftarrow}w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymleftarrow}w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}\ {\isasymLongrightarrow}\isanewline
|
|
211 |
\ \ {\isasymexists}i{\isasymle}size\ w{\isachardot}\ size{\isacharbrackleft}x{\isasymleftarrow}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymleftarrow}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequoteclose}%
|
17056
|
212 |
\isadelimproof
|
|
213 |
%
|
|
214 |
\endisadelimproof
|
|
215 |
%
|
|
216 |
\isatagproof
|
16069
|
217 |
%
|
|
218 |
\begin{isamarkuptxt}%
|
|
219 |
\noindent
|
|
220 |
This is proved by \isa{force} with the help of the intermediate value theorem,
|
|
221 |
instantiated appropriately and with its first premise disposed of by lemma
|
|
222 |
\isa{step{\isadigit{1}}}:%
|
|
223 |
\end{isamarkuptxt}%
|
17175
|
224 |
\isamarkuptrue%
|
|
225 |
\isacommand{apply}\isamarkupfalse%
|
|
226 |
{\isacharparenleft}insert\ nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val{\isacharbrackleft}OF\ step{\isadigit{1}}{\isacharcomma}\ of\ {\isachardoublequoteopen}P{\isachardoublequoteclose}\ {\isachardoublequoteopen}w{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isadigit{1}}{\isachardoublequoteclose}{\isacharbrackright}{\isacharparenright}\isanewline
|
|
227 |
\isacommand{by}\isamarkupfalse%
|
|
228 |
\ force%
|
17056
|
229 |
\endisatagproof
|
|
230 |
{\isafoldproof}%
|
|
231 |
%
|
|
232 |
\isadelimproof
|
|
233 |
%
|
|
234 |
\endisadelimproof
|
11866
|
235 |
%
|
10236
|
236 |
\begin{isamarkuptext}%
|
|
237 |
\noindent
|
|
238 |
|
|
239 |
Lemma \isa{part{\isadigit{1}}} tells us only about the prefix \isa{take\ i\ w}.
|
10878
|
240 |
An easy lemma deals with the suffix \isa{drop\ i\ w}:%
|
10236
|
241 |
\end{isamarkuptext}%
|
17175
|
242 |
\isamarkuptrue%
|
|
243 |
\isacommand{lemma}\isamarkupfalse%
|
|
244 |
\ part{\isadigit{2}}{\isacharcolon}\isanewline
|
23380
|
245 |
\ \ {\isachardoublequoteopen}{\isasymlbrakk}size{\isacharbrackleft}x{\isasymleftarrow}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\isanewline
|
|
246 |
\ \ \ \ size{\isacharbrackleft}x{\isasymleftarrow}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}{\isacharsemicolon}\isanewline
|
|
247 |
\ \ \ \ size{\isacharbrackleft}x{\isasymleftarrow}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymleftarrow}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isasymrbrakk}\isanewline
|
|
248 |
\ \ \ {\isasymLongrightarrow}\ size{\isacharbrackleft}x{\isasymleftarrow}drop\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymleftarrow}drop\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequoteclose}\isanewline
|
17056
|
249 |
%
|
|
250 |
\isadelimproof
|
|
251 |
%
|
|
252 |
\endisadelimproof
|
|
253 |
%
|
|
254 |
\isatagproof
|
17175
|
255 |
\isacommand{by}\isamarkupfalse%
|
|
256 |
{\isacharparenleft}simp\ del{\isacharcolon}\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharparenright}%
|
17056
|
257 |
\endisatagproof
|
|
258 |
{\isafoldproof}%
|
|
259 |
%
|
|
260 |
\isadelimproof
|
|
261 |
%
|
|
262 |
\endisadelimproof
|
11866
|
263 |
%
|
10236
|
264 |
\begin{isamarkuptext}%
|
|
265 |
\noindent
|
11257
|
266 |
In the proof we have disabled the normally useful lemma
|
10878
|
267 |
\begin{isabelle}
|
|
268 |
\isa{take\ n\ xs\ {\isacharat}\ drop\ n\ xs\ {\isacharequal}\ xs}
|
|
269 |
\rulename{append_take_drop_id}
|
|
270 |
\end{isabelle}
|
11257
|
271 |
to allow the simplifier to apply the following lemma instead:
|
|
272 |
\begin{isabelle}%
|
|
273 |
\ \ \ \ \ {\isacharbrackleft}x{\isasymin}xs{\isacharat}ys{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}x{\isasymin}xs{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharat}\ {\isacharbrackleft}x{\isasymin}ys{\isachardot}\ P\ x{\isacharbrackright}%
|
|
274 |
\end{isabelle}
|
10236
|
275 |
|
|
276 |
To dispose of trivial cases automatically, the rules of the inductive
|
|
277 |
definition are declared simplification rules:%
|
|
278 |
\end{isamarkuptext}%
|
17175
|
279 |
\isamarkuptrue%
|
|
280 |
\isacommand{declare}\isamarkupfalse%
|
|
281 |
\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharbrackleft}simp{\isacharbrackright}%
|
10236
|
282 |
\begin{isamarkuptext}%
|
|
283 |
\noindent
|
|
284 |
This could have been done earlier but was not necessary so far.
|
|
285 |
|
|
286 |
The completeness theorem tells us that if a word has the same number of
|
10878
|
287 |
\isa{a}'s and \isa{b}'s, then it is in \isa{S}, and similarly
|
|
288 |
for \isa{A} and \isa{B}:%
|
10236
|
289 |
\end{isamarkuptext}%
|
17175
|
290 |
\isamarkuptrue%
|
|
291 |
\isacommand{theorem}\isamarkupfalse%
|
|
292 |
\ completeness{\isacharcolon}\isanewline
|
23380
|
293 |
\ \ {\isachardoublequoteopen}{\isacharparenleft}size{\isacharbrackleft}x{\isasymleftarrow}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymleftarrow}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ \ \ \ \ {\isasymlongrightarrow}\ w\ {\isasymin}\ S{\isacharparenright}\ {\isasymand}\isanewline
|
|
294 |
\ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isasymleftarrow}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymleftarrow}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymlongrightarrow}\ w\ {\isasymin}\ A{\isacharparenright}\ {\isasymand}\isanewline
|
|
295 |
\ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isasymleftarrow}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymleftarrow}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymlongrightarrow}\ w\ {\isasymin}\ B{\isacharparenright}{\isachardoublequoteclose}%
|
17056
|
296 |
\isadelimproof
|
|
297 |
%
|
|
298 |
\endisadelimproof
|
|
299 |
%
|
|
300 |
\isatagproof
|
16069
|
301 |
%
|
|
302 |
\begin{isamarkuptxt}%
|
|
303 |
\noindent
|
|
304 |
The proof is by induction on \isa{w}. Structural induction would fail here
|
|
305 |
because, as we can see from the grammar, we need to make bigger steps than
|
|
306 |
merely appending a single letter at the front. Hence we induct on the length
|
|
307 |
of \isa{w}, using the induction rule \isa{length{\isacharunderscore}induct}:%
|
|
308 |
\end{isamarkuptxt}%
|
17175
|
309 |
\isamarkuptrue%
|
|
310 |
\isacommand{apply}\isamarkupfalse%
|
17181
|
311 |
{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}%
|
16069
|
312 |
\begin{isamarkuptxt}%
|
|
313 |
\noindent
|
|
314 |
The \isa{rule} parameter tells \isa{induct{\isacharunderscore}tac} explicitly which induction
|
|
315 |
rule to use. For details see \S\ref{sec:complete-ind} below.
|
|
316 |
In this case the result is that we may assume the lemma already
|
|
317 |
holds for all words shorter than \isa{w}.
|
|
318 |
|
|
319 |
The proof continues with a case distinction on \isa{w},
|
|
320 |
on whether \isa{w} is empty or not.%
|
|
321 |
\end{isamarkuptxt}%
|
17175
|
322 |
\isamarkuptrue%
|
|
323 |
\isacommand{apply}\isamarkupfalse%
|
|
324 |
{\isacharparenleft}case{\isacharunderscore}tac\ w{\isacharparenright}\isanewline
|
|
325 |
\ \isacommand{apply}\isamarkupfalse%
|
17181
|
326 |
{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}%
|
16069
|
327 |
\begin{isamarkuptxt}%
|
|
328 |
\noindent
|
|
329 |
Simplification disposes of the base case and leaves only a conjunction
|
|
330 |
of two step cases to be proved:
|
|
331 |
if \isa{w\ {\isacharequal}\ a\ {\isacharhash}\ v} and \begin{isabelle}%
|
23380
|
332 |
\ \ \ \ \ length\ {\isacharparenleft}if\ x\ {\isacharequal}\ a\ then\ {\isacharbrackleft}x\ {\isasymin}\ v{\isacharbrackright}\ else\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
|
|
333 |
\isaindent{\ \ \ \ \ }length\ {\isacharparenleft}if\ x\ {\isacharequal}\ b\ then\ {\isacharbrackleft}x\ {\isasymin}\ v{\isacharbrackright}\ else\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharplus}\ {\isadigit{2}}%
|
16069
|
334 |
\end{isabelle} then
|
|
335 |
\isa{b\ {\isacharhash}\ v\ {\isasymin}\ A}, and similarly for \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v}.
|
|
336 |
We only consider the first case in detail.
|
|
337 |
|
|
338 |
After breaking the conjunction up into two cases, we can apply
|
|
339 |
\isa{part{\isadigit{1}}} to the assumption that \isa{w} contains two more \isa{a}'s than \isa{b}'s.%
|
|
340 |
\end{isamarkuptxt}%
|
17175
|
341 |
\isamarkuptrue%
|
|
342 |
\isacommand{apply}\isamarkupfalse%
|
|
343 |
{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline
|
|
344 |
\ \isacommand{apply}\isamarkupfalse%
|
|
345 |
{\isacharparenleft}clarify{\isacharparenright}\isanewline
|
|
346 |
\ \isacommand{apply}\isamarkupfalse%
|
|
347 |
{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequoteclose}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
|
|
348 |
\ \isacommand{apply}\isamarkupfalse%
|
|
349 |
{\isacharparenleft}clarify{\isacharparenright}%
|
16069
|
350 |
\begin{isamarkuptxt}%
|
|
351 |
\noindent
|
|
352 |
This yields an index \isa{i\ {\isasymle}\ length\ v} such that
|
|
353 |
\begin{isabelle}%
|
23380
|
354 |
\ \ \ \ \ length\ {\isacharbrackleft}x{\isasymleftarrow}take\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymleftarrow}take\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}%
|
16069
|
355 |
\end{isabelle}
|
|
356 |
With the help of \isa{part{\isadigit{2}}} it follows that
|
|
357 |
\begin{isabelle}%
|
23380
|
358 |
\ \ \ \ \ length\ {\isacharbrackleft}x{\isasymleftarrow}drop\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymleftarrow}drop\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}%
|
16069
|
359 |
\end{isabelle}%
|
|
360 |
\end{isamarkuptxt}%
|
17175
|
361 |
\isamarkuptrue%
|
|
362 |
\ \isacommand{apply}\isamarkupfalse%
|
|
363 |
{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequoteclose}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
|
|
364 |
\ \ \isacommand{apply}\isamarkupfalse%
|
|
365 |
{\isacharparenleft}assumption{\isacharparenright}%
|
16069
|
366 |
\begin{isamarkuptxt}%
|
|
367 |
\noindent
|
|
368 |
Now it is time to decompose \isa{v} in the conclusion \isa{b\ {\isacharhash}\ v\ {\isasymin}\ A}
|
|
369 |
into \isa{take\ i\ v\ {\isacharat}\ drop\ i\ v},%
|
|
370 |
\end{isamarkuptxt}%
|
17175
|
371 |
\isamarkuptrue%
|
|
372 |
\ \isacommand{apply}\isamarkupfalse%
|
|
373 |
{\isacharparenleft}rule{\isacharunderscore}tac\ n{\isadigit{1}}{\isacharequal}i\ \isakeyword{and}\ t{\isacharequal}v\ \isakeyword{in}\ subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}{\isacharparenright}%
|
16069
|
374 |
\begin{isamarkuptxt}%
|
|
375 |
\noindent
|
|
376 |
(the variables \isa{n{\isadigit{1}}} and \isa{t} are the result of composing the
|
|
377 |
theorems \isa{subst} and \isa{append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id})
|
|
378 |
after which the appropriate rule of the grammar reduces the goal
|
|
379 |
to the two subgoals \isa{take\ i\ v\ {\isasymin}\ A} and \isa{drop\ i\ v\ {\isasymin}\ A}:%
|
|
380 |
\end{isamarkuptxt}%
|
17175
|
381 |
\isamarkuptrue%
|
|
382 |
\ \isacommand{apply}\isamarkupfalse%
|
|
383 |
{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}%
|
16069
|
384 |
\begin{isamarkuptxt}%
|
|
385 |
Both subgoals follow from the induction hypothesis because both \isa{take\ i\ v} and \isa{drop\ i\ v} are shorter than \isa{w}:%
|
|
386 |
\end{isamarkuptxt}%
|
17175
|
387 |
\isamarkuptrue%
|
|
388 |
\ \ \isacommand{apply}\isamarkupfalse%
|
|
389 |
{\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline
|
|
390 |
\ \isacommand{apply}\isamarkupfalse%
|
|
391 |
{\isacharparenleft}force\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}%
|
16069
|
392 |
\begin{isamarkuptxt}%
|
|
393 |
The case \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v} is proved analogously:%
|
|
394 |
\end{isamarkuptxt}%
|
17175
|
395 |
\isamarkuptrue%
|
|
396 |
\isacommand{apply}\isamarkupfalse%
|
|
397 |
{\isacharparenleft}clarify{\isacharparenright}\isanewline
|
|
398 |
\isacommand{apply}\isamarkupfalse%
|
|
399 |
{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequoteclose}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
|
|
400 |
\isacommand{apply}\isamarkupfalse%
|
|
401 |
{\isacharparenleft}clarify{\isacharparenright}\isanewline
|
|
402 |
\isacommand{apply}\isamarkupfalse%
|
|
403 |
{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequoteclose}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
|
|
404 |
\ \isacommand{apply}\isamarkupfalse%
|
|
405 |
{\isacharparenleft}assumption{\isacharparenright}\isanewline
|
|
406 |
\isacommand{apply}\isamarkupfalse%
|
|
407 |
{\isacharparenleft}rule{\isacharunderscore}tac\ n{\isadigit{1}}{\isacharequal}i\ \isakeyword{and}\ t{\isacharequal}v\ \isakeyword{in}\ subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}{\isacharparenright}\isanewline
|
|
408 |
\isacommand{apply}\isamarkupfalse%
|
|
409 |
{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isanewline
|
|
410 |
\ \isacommand{apply}\isamarkupfalse%
|
|
411 |
{\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline
|
|
412 |
\isacommand{by}\isamarkupfalse%
|
|
413 |
{\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}%
|
17056
|
414 |
\endisatagproof
|
|
415 |
{\isafoldproof}%
|
|
416 |
%
|
|
417 |
\isadelimproof
|
|
418 |
%
|
|
419 |
\endisadelimproof
|
11866
|
420 |
%
|
10236
|
421 |
\begin{isamarkuptext}%
|
10878
|
422 |
We conclude this section with a comparison of our proof with
|
11494
|
423 |
Hopcroft\index{Hopcroft, J. E.} and Ullman's\index{Ullman, J. D.}
|
|
424 |
\cite[p.\ts81]{HopcroftUllman}.
|
|
425 |
For a start, the textbook
|
11257
|
426 |
grammar, for no good reason, excludes the empty word, thus complicating
|
|
427 |
matters just a little bit: they have 8 instead of our 7 productions.
|
10236
|
428 |
|
11158
|
429 |
More importantly, the proof itself is different: rather than
|
|
430 |
separating the two directions, they perform one induction on the
|
|
431 |
length of a word. This deprives them of the beauty of rule induction,
|
|
432 |
and in the easy direction (correctness) their reasoning is more
|
|
433 |
detailed than our \isa{auto}. For the hard part (completeness), they
|
|
434 |
consider just one of the cases that our \isa{simp{\isacharunderscore}all} disposes of
|
|
435 |
automatically. Then they conclude the proof by saying about the
|
|
436 |
remaining cases: ``We do this in a manner similar to our method of
|
|
437 |
proof for part (1); this part is left to the reader''. But this is
|
|
438 |
precisely the part that requires the intermediate value theorem and
|
|
439 |
thus is not at all similar to the other cases (which are automatic in
|
|
440 |
Isabelle). The authors are at least cavalier about this point and may
|
|
441 |
even have overlooked the slight difficulty lurking in the omitted
|
11494
|
442 |
cases. Such errors are found in many pen-and-paper proofs when they
|
|
443 |
are scrutinized formally.%
|
|
444 |
\index{grammars!defining inductively|)}%
|
10236
|
445 |
\end{isamarkuptext}%
|
17175
|
446 |
\isamarkuptrue%
|
17056
|
447 |
%
|
|
448 |
\isadelimtheory
|
|
449 |
%
|
|
450 |
\endisadelimtheory
|
|
451 |
%
|
|
452 |
\isatagtheory
|
|
453 |
%
|
|
454 |
\endisatagtheory
|
|
455 |
{\isafoldtheory}%
|
|
456 |
%
|
|
457 |
\isadelimtheory
|
|
458 |
%
|
|
459 |
\endisadelimtheory
|
10217
|
460 |
\end{isabellebody}%
|
|
461 |
%%% Local Variables:
|
|
462 |
%%% mode: latex
|
|
463 |
%%% TeX-master: "root"
|
|
464 |
%%% End:
|