10225
|
1 |
(*<*)theory AB = Main:(*>*)
|
|
2 |
|
10884
|
3 |
section{*Case Study: A Context Free Grammar*}
|
10217
|
4 |
|
10242
|
5 |
text{*\label{sec:CFG}
|
11494
|
6 |
\index{grammars!defining inductively|(}%
|
10236
|
7 |
Grammars are nothing but shorthands for inductive definitions of nonterminals
|
|
8 |
which represent sets of strings. For example, the production
|
|
9 |
$A \to B c$ is short for
|
|
10 |
\[ w \in B \Longrightarrow wc \in A \]
|
10884
|
11 |
This section demonstrates this idea with an example
|
|
12 |
due to Hopcroft and Ullman, a grammar for generating all words with an
|
|
13 |
equal number of $a$'s and~$b$'s:
|
10236
|
14 |
\begin{eqnarray}
|
|
15 |
S &\to& \epsilon \mid b A \mid a B \nonumber\\
|
|
16 |
A &\to& a S \mid b A A \nonumber\\
|
|
17 |
B &\to& b S \mid a B B \nonumber
|
|
18 |
\end{eqnarray}
|
10884
|
19 |
At the end we say a few words about the relationship between
|
|
20 |
the original proof \cite[p.\ts81]{HopcroftUllman} and our formal version.
|
10236
|
21 |
|
10287
|
22 |
We start by fixing the alphabet, which consists only of @{term a}'s
|
10884
|
23 |
and~@{term b}'s:
|
10236
|
24 |
*}
|
|
25 |
|
10217
|
26 |
datatype alfa = a | b;
|
|
27 |
|
10236
|
28 |
text{*\noindent
|
10287
|
29 |
For convenience we include the following easy lemmas as simplification rules:
|
10236
|
30 |
*}
|
|
31 |
|
|
32 |
lemma [simp]: "(x \<noteq> a) = (x = b) \<and> (x \<noteq> b) = (x = a)";
|
10884
|
33 |
by (case_tac x, auto)
|
10217
|
34 |
|
10236
|
35 |
text{*\noindent
|
|
36 |
Words over this alphabet are of type @{typ"alfa list"}, and
|
10884
|
37 |
the three nonterminals are declared as sets of such words:
|
10236
|
38 |
*}
|
|
39 |
|
10217
|
40 |
consts S :: "alfa list set"
|
|
41 |
A :: "alfa list set"
|
|
42 |
B :: "alfa list set";
|
|
43 |
|
10236
|
44 |
text{*\noindent
|
10884
|
45 |
The productions above are recast as a \emph{mutual} inductive
|
10242
|
46 |
definition\index{inductive definition!simultaneous}
|
10884
|
47 |
of @{term S}, @{term A} and~@{term B}:
|
10236
|
48 |
*}
|
|
49 |
|
10217
|
50 |
inductive S A B
|
|
51 |
intros
|
10236
|
52 |
"[] \<in> S"
|
|
53 |
"w \<in> A \<Longrightarrow> b#w \<in> S"
|
|
54 |
"w \<in> B \<Longrightarrow> a#w \<in> S"
|
10217
|
55 |
|
10236
|
56 |
"w \<in> S \<Longrightarrow> a#w \<in> A"
|
|
57 |
"\<lbrakk> v\<in>A; w\<in>A \<rbrakk> \<Longrightarrow> b#v@w \<in> A"
|
|
58 |
|
|
59 |
"w \<in> S \<Longrightarrow> b#w \<in> B"
|
|
60 |
"\<lbrakk> v \<in> B; w \<in> B \<rbrakk> \<Longrightarrow> a#v@w \<in> B";
|
10217
|
61 |
|
10236
|
62 |
text{*\noindent
|
|
63 |
First we show that all words in @{term S} contain the same number of @{term
|
10884
|
64 |
a}'s and @{term b}'s. Since the definition of @{term S} is by mutual
|
|
65 |
induction, so is the proof: we show at the same time that all words in
|
10236
|
66 |
@{term A} contain one more @{term a} than @{term b} and all words in @{term
|
|
67 |
B} contains one more @{term b} than @{term a}.
|
|
68 |
*}
|
10217
|
69 |
|
10236
|
70 |
lemma correctness:
|
|
71 |
"(w \<in> S \<longrightarrow> size[x\<in>w. x=a] = size[x\<in>w. x=b]) \<and>
|
10237
|
72 |
(w \<in> A \<longrightarrow> size[x\<in>w. x=a] = size[x\<in>w. x=b] + 1) \<and>
|
|
73 |
(w \<in> B \<longrightarrow> size[x\<in>w. x=b] = size[x\<in>w. x=a] + 1)"
|
10217
|
74 |
|
10236
|
75 |
txt{*\noindent
|
|
76 |
These propositions are expressed with the help of the predefined @{term
|
10283
|
77 |
filter} function on lists, which has the convenient syntax @{text"[x\<in>xs. P
|
10236
|
78 |
x]"}, the list of all elements @{term x} in @{term xs} such that @{prop"P x"}
|
10884
|
79 |
holds. Remember that on lists @{text size} and @{text length} are synonymous.
|
10236
|
80 |
|
|
81 |
The proof itself is by rule induction and afterwards automatic:
|
|
82 |
*}
|
|
83 |
|
10884
|
84 |
by (rule S_A_B.induct, auto)
|
10217
|
85 |
|
10236
|
86 |
text{*\noindent
|
|
87 |
This may seem surprising at first, and is indeed an indication of the power
|
|
88 |
of inductive definitions. But it is also quite straightforward. For example,
|
|
89 |
consider the production $A \to b A A$: if $v,w \in A$ and the elements of $A$
|
10884
|
90 |
contain one more $a$ than~$b$'s, then $bvw$ must again contain one more $a$
|
|
91 |
than~$b$'s.
|
10236
|
92 |
|
|
93 |
As usual, the correctness of syntactic descriptions is easy, but completeness
|
|
94 |
is hard: does @{term S} contain \emph{all} words with an equal number of
|
|
95 |
@{term a}'s and @{term b}'s? It turns out that this proof requires the
|
10884
|
96 |
following lemma: every string with two more @{term a}'s than @{term
|
|
97 |
b}'s can be cut somewhere such that each half has one more @{term a} than
|
10236
|
98 |
@{term b}. This is best seen by imagining counting the difference between the
|
10283
|
99 |
number of @{term a}'s and @{term b}'s starting at the left end of the
|
|
100 |
word. We start with 0 and end (at the right end) with 2. Since each move to the
|
10236
|
101 |
right increases or decreases the difference by 1, we must have passed through
|
|
102 |
1 on our way from 0 to 2. Formally, we appeal to the following discrete
|
|
103 |
intermediate value theorem @{thm[source]nat0_intermed_int_val}
|
|
104 |
@{thm[display]nat0_intermed_int_val[no_vars]}
|
|
105 |
where @{term f} is of type @{typ"nat \<Rightarrow> int"}, @{typ int} are the integers,
|
11308
|
106 |
@{text"\<bar>.\<bar>"} is the absolute value function\footnote{See
|
|
107 |
Table~\ref{tab:ascii} in the Appendix for the correct \textsc{ascii}
|
|
108 |
syntax.}, and @{term"#1::int"} is the integer 1 (see \S\ref{sec:numbers}).
|
10217
|
109 |
|
11147
|
110 |
First we show that our specific function, the difference between the
|
10236
|
111 |
numbers of @{term a}'s and @{term b}'s, does indeed only change by 1 in every
|
|
112 |
move to the right. At this point we also start generalizing from @{term a}'s
|
|
113 |
and @{term b}'s to an arbitrary property @{term P}. Otherwise we would have
|
|
114 |
to prove the desired lemma twice, once as stated above and once with the
|
|
115 |
roles of @{term a}'s and @{term b}'s interchanged.
|
|
116 |
*}
|
|
117 |
|
|
118 |
lemma step1: "\<forall>i < size w.
|
10608
|
119 |
\<bar>(int(size[x\<in>take (i+1) w. P x])-int(size[x\<in>take (i+1) w. \<not>P x]))
|
|
120 |
- (int(size[x\<in>take i w. P x])-int(size[x\<in>take i w. \<not>P x]))\<bar> \<le> #1"
|
10236
|
121 |
|
|
122 |
txt{*\noindent
|
|
123 |
The lemma is a bit hard to read because of the coercion function
|
11147
|
124 |
@{text"int :: nat \<Rightarrow> int"}. It is required because @{term size} returns
|
10884
|
125 |
a natural number, but subtraction on type~@{typ nat} will do the wrong thing.
|
10236
|
126 |
Function @{term take} is predefined and @{term"take i xs"} is the prefix of
|
10884
|
127 |
length @{term i} of @{term xs}; below we also need @{term"drop i xs"}, which
|
10236
|
128 |
is what remains after that prefix has been dropped from @{term xs}.
|
|
129 |
|
|
130 |
The proof is by induction on @{term w}, with a trivial base case, and a not
|
|
131 |
so trivial induction step. Since it is essentially just arithmetic, we do not
|
|
132 |
discuss it.
|
|
133 |
*}
|
|
134 |
|
10217
|
135 |
apply(induct w);
|
|
136 |
apply(simp);
|
10236
|
137 |
by(force simp add:zabs_def take_Cons split:nat.split if_splits);
|
10217
|
138 |
|
10236
|
139 |
text{*
|
11494
|
140 |
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
|
141 |
*}
|
10217
|
142 |
|
|
143 |
lemma part1:
|
10236
|
144 |
"size[x\<in>w. P x] = size[x\<in>w. \<not>P x]+2 \<Longrightarrow>
|
|
145 |
\<exists>i\<le>size w. size[x\<in>take i w. P x] = size[x\<in>take i w. \<not>P x]+1";
|
|
146 |
|
|
147 |
txt{*\noindent
|
10884
|
148 |
This is proved by @{text force} with the help of the intermediate value theorem,
|
10608
|
149 |
instantiated appropriately and with its first premise disposed of by lemma
|
|
150 |
@{thm[source]step1}:
|
10236
|
151 |
*}
|
|
152 |
|
|
153 |
apply(insert nat0_intermed_int_val[OF step1, of "P" "w" "#1"]);
|
10608
|
154 |
by force;
|
10236
|
155 |
|
|
156 |
text{*\noindent
|
|
157 |
|
|
158 |
Lemma @{thm[source]part1} tells us only about the prefix @{term"take i w"}.
|
10884
|
159 |
An easy lemma deals with the suffix @{term"drop i w"}:
|
10236
|
160 |
*}
|
|
161 |
|
10217
|
162 |
|
|
163 |
lemma part2:
|
10236
|
164 |
"\<lbrakk>size[x\<in>take i w @ drop i w. P x] =
|
|
165 |
size[x\<in>take i w @ drop i w. \<not>P x]+2;
|
|
166 |
size[x\<in>take i w. P x] = size[x\<in>take i w. \<not>P x]+1\<rbrakk>
|
|
167 |
\<Longrightarrow> size[x\<in>drop i w. P x] = size[x\<in>drop i w. \<not>P x]+1";
|
10217
|
168 |
by(simp del:append_take_drop_id);
|
|
169 |
|
10236
|
170 |
text{*\noindent
|
11257
|
171 |
In the proof we have disabled the normally useful lemma
|
10884
|
172 |
\begin{isabelle}
|
|
173 |
@{thm append_take_drop_id[no_vars]}
|
|
174 |
\rulename{append_take_drop_id}
|
|
175 |
\end{isabelle}
|
11257
|
176 |
to allow the simplifier to apply the following lemma instead:
|
|
177 |
@{text[display]"[x\<in>xs@ys. P x] = [x\<in>xs. P x] @ [x\<in>ys. P x]"}
|
10236
|
178 |
|
|
179 |
To dispose of trivial cases automatically, the rules of the inductive
|
|
180 |
definition are declared simplification rules:
|
|
181 |
*}
|
|
182 |
|
|
183 |
declare S_A_B.intros[simp];
|
|
184 |
|
|
185 |
text{*\noindent
|
|
186 |
This could have been done earlier but was not necessary so far.
|
|
187 |
|
|
188 |
The completeness theorem tells us that if a word has the same number of
|
10884
|
189 |
@{term a}'s and @{term b}'s, then it is in @{term S}, and similarly
|
|
190 |
for @{term A} and @{term B}:
|
10236
|
191 |
*}
|
|
192 |
|
|
193 |
theorem completeness:
|
|
194 |
"(size[x\<in>w. x=a] = size[x\<in>w. x=b] \<longrightarrow> w \<in> S) \<and>
|
10237
|
195 |
(size[x\<in>w. x=a] = size[x\<in>w. x=b] + 1 \<longrightarrow> w \<in> A) \<and>
|
|
196 |
(size[x\<in>w. x=b] = size[x\<in>w. x=a] + 1 \<longrightarrow> w \<in> B)";
|
10236
|
197 |
|
|
198 |
txt{*\noindent
|
|
199 |
The proof is by induction on @{term w}. Structural induction would fail here
|
|
200 |
because, as we can see from the grammar, we need to make bigger steps than
|
|
201 |
merely appending a single letter at the front. Hence we induct on the length
|
|
202 |
of @{term w}, using the induction rule @{thm[source]length_induct}:
|
|
203 |
*}
|
10217
|
204 |
|
|
205 |
apply(induct_tac w rule: length_induct);
|
10236
|
206 |
(*<*)apply(rename_tac w)(*>*)
|
|
207 |
|
|
208 |
txt{*\noindent
|
|
209 |
The @{text rule} parameter tells @{text induct_tac} explicitly which induction
|
|
210 |
rule to use. For details see \S\ref{sec:complete-ind} below.
|
|
211 |
In this case the result is that we may assume the lemma already
|
|
212 |
holds for all words shorter than @{term w}.
|
|
213 |
|
|
214 |
The proof continues with a case distinction on @{term w},
|
11494
|
215 |
on whether @{term w} is empty or not.
|
10236
|
216 |
*}
|
|
217 |
|
|
218 |
apply(case_tac w);
|
|
219 |
apply(simp_all);
|
|
220 |
(*<*)apply(rename_tac x v)(*>*)
|
|
221 |
|
|
222 |
txt{*\noindent
|
11257
|
223 |
Simplification disposes of the base case and leaves only a conjunction
|
|
224 |
of two step cases to be proved:
|
10884
|
225 |
if @{prop"w = a#v"} and @{prop[display]"size[x\<in>v. x=a] = size[x\<in>v. x=b]+2"} then
|
10236
|
226 |
@{prop"b#v \<in> A"}, and similarly for @{prop"w = b#v"}.
|
|
227 |
We only consider the first case in detail.
|
|
228 |
|
11257
|
229 |
After breaking the conjunction up into two cases, we can apply
|
10236
|
230 |
@{thm[source]part1} to the assumption that @{term w} contains two more @{term
|
|
231 |
a}'s than @{term b}'s.
|
|
232 |
*}
|
|
233 |
|
11257
|
234 |
apply(rule conjI)
|
|
235 |
apply(clarify)
|
|
236 |
apply(frule part1[of "\<lambda>x. x=a", simplified])
|
|
237 |
apply(clarify)
|
10236
|
238 |
txt{*\noindent
|
|
239 |
This yields an index @{prop"i \<le> length v"} such that
|
10884
|
240 |
@{prop[display]"length [x\<in>take i v . x = a] = length [x\<in>take i v . x = b] + 1"}
|
11147
|
241 |
With the help of @{thm[source]part2} it follows that
|
10884
|
242 |
@{prop[display]"length [x\<in>drop i v . x = a] = length [x\<in>drop i v . x = b] + 1"}
|
10236
|
243 |
*}
|
|
244 |
|
11257
|
245 |
apply(drule part2[of "\<lambda>x. x=a", simplified])
|
|
246 |
apply(assumption)
|
10236
|
247 |
|
|
248 |
txt{*\noindent
|
|
249 |
Now it is time to decompose @{term v} in the conclusion @{prop"b#v \<in> A"}
|
|
250 |
into @{term"take i v @ drop i v"},
|
11257
|
251 |
*}
|
|
252 |
|
|
253 |
apply(rule_tac n1=i and t=v in subst[OF append_take_drop_id])
|
|
254 |
|
|
255 |
txt{*\noindent
|
|
256 |
(the variables @{term n1} and @{term t} are the result of composing the
|
|
257 |
theorems @{thm[source]subst} and @{thm[source]append_take_drop_id})
|
10236
|
258 |
after which the appropriate rule of the grammar reduces the goal
|
|
259 |
to the two subgoals @{prop"take i v \<in> A"} and @{prop"drop i v \<in> A"}:
|
|
260 |
*}
|
|
261 |
|
11257
|
262 |
apply(rule S_A_B.intros)
|
10236
|
263 |
|
11257
|
264 |
txt{*
|
10236
|
265 |
Both subgoals follow from the induction hypothesis because both @{term"take i
|
|
266 |
v"} and @{term"drop i v"} are shorter than @{term w}:
|
|
267 |
*}
|
|
268 |
|
11257
|
269 |
apply(force simp add: min_less_iff_disj)
|
|
270 |
apply(force split add: nat_diff_split)
|
10236
|
271 |
|
11257
|
272 |
txt{*
|
10884
|
273 |
The case @{prop"w = b#v"} is proved analogously:
|
10236
|
274 |
*}
|
|
275 |
|
11257
|
276 |
apply(clarify)
|
|
277 |
apply(frule part1[of "\<lambda>x. x=b", simplified])
|
|
278 |
apply(clarify)
|
|
279 |
apply(drule part2[of "\<lambda>x. x=b", simplified])
|
|
280 |
apply(assumption)
|
|
281 |
apply(rule_tac n1=i and t=v in subst[OF append_take_drop_id])
|
|
282 |
apply(rule S_A_B.intros)
|
|
283 |
apply(force simp add:min_less_iff_disj)
|
|
284 |
by(force simp add:min_less_iff_disj split add: nat_diff_split)
|
10217
|
285 |
|
10236
|
286 |
text{*
|
10884
|
287 |
We conclude this section with a comparison of our proof with
|
11494
|
288 |
Hopcroft\index{Hopcroft, J. E.} and Ullman's\index{Ullman, J. D.}
|
|
289 |
\cite[p.\ts81]{HopcroftUllman}.
|
|
290 |
For a start, the textbook
|
11257
|
291 |
grammar, for no good reason, excludes the empty word, thus complicating
|
|
292 |
matters just a little bit: they have 8 instead of our 7 productions.
|
10236
|
293 |
|
11147
|
294 |
More importantly, the proof itself is different: rather than
|
|
295 |
separating the two directions, they perform one induction on the
|
|
296 |
length of a word. This deprives them of the beauty of rule induction,
|
|
297 |
and in the easy direction (correctness) their reasoning is more
|
|
298 |
detailed than our @{text auto}. For the hard part (completeness), they
|
|
299 |
consider just one of the cases that our @{text simp_all} disposes of
|
|
300 |
automatically. Then they conclude the proof by saying about the
|
|
301 |
remaining cases: ``We do this in a manner similar to our method of
|
|
302 |
proof for part (1); this part is left to the reader''. But this is
|
|
303 |
precisely the part that requires the intermediate value theorem and
|
|
304 |
thus is not at all similar to the other cases (which are automatic in
|
|
305 |
Isabelle). The authors are at least cavalier about this point and may
|
|
306 |
even have overlooked the slight difficulty lurking in the omitted
|
11494
|
307 |
cases. Such errors are found in many pen-and-paper proofs when they
|
|
308 |
are scrutinized formally.%
|
|
309 |
\index{grammars!defining inductively|)}
|
|
310 |
*}
|
10236
|
311 |
|
10225
|
312 |
(*<*)end(*>*)
|