3 \def\isabellecontext{AB}%
5 \isamarkupsection{Case Study: A Context Free Grammar%
10 \index{grammars!defining inductively|(}%
11 Grammars are nothing but shorthands for inductive definitions of nonterminals
12 which represent sets of strings. For example, the production
13 $A \to B c$ is short for
14 \[ w \in B \Longrightarrow wc \in A \]
15 This section demonstrates this idea with an example
16 due to Hopcroft and Ullman, a grammar for generating all words with an
17 equal number of $a$'s and~$b$'s:
19 S &\to& \epsilon \mid b A \mid a B \nonumber\\
20 A &\to& a S \mid b A A \nonumber\\
21 B &\to& b S \mid a B B \nonumber
23 At the end we say a few words about the relationship between
24 the original proof \cite[p.\ts81]{HopcroftUllman} and our formal version.
26 We start by fixing the alphabet, which consists only of \isa{a}'s
29 \isacommand{datatype}\ alfa\ {\isacharequal}\ a\ {\isacharbar}\ b%
30 \begin{isamarkuptext}%
32 For convenience we include the following easy lemmas as simplification rules:%
34 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ b{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}x\ {\isasymnoteq}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ a{\isacharparenright}{\isachardoublequote}\isanewline
35 \isacommand{by}\ {\isacharparenleft}case{\isacharunderscore}tac\ x{\isacharcomma}\ auto{\isacharparenright}%
36 \begin{isamarkuptext}%
38 Words over this alphabet are of type \isa{alfa\ list}, and
39 the three nonterminals are declared as sets of such words:%
41 \isacommand{consts}\ S\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline
42 \ \ \ \ \ \ \ A\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline
43 \ \ \ \ \ \ \ B\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}%
44 \begin{isamarkuptext}%
46 The productions above are recast as a \emph{mutual} inductive
47 definition\index{inductive definition!simultaneous}
48 of \isa{S}, \isa{A} and~\isa{B}:%
50 \isacommand{inductive}\ S\ A\ B\isanewline
51 \isakeyword{intros}\isanewline
52 \ \ {\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}\ {\isasymin}\ S{\isachardoublequote}\isanewline
53 \ \ {\isachardoublequote}w\ {\isasymin}\ A\ {\isasymLongrightarrow}\ b{\isacharhash}w\ {\isasymin}\ S{\isachardoublequote}\isanewline
54 \ \ {\isachardoublequote}w\ {\isasymin}\ B\ {\isasymLongrightarrow}\ a{\isacharhash}w\ {\isasymin}\ S{\isachardoublequote}\isanewline
56 \ \ {\isachardoublequote}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ a{\isacharhash}w\ \ \ {\isasymin}\ A{\isachardoublequote}\isanewline
57 \ \ {\isachardoublequote}{\isasymlbrakk}\ v{\isasymin}A{\isacharsemicolon}\ w{\isasymin}A\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ b{\isacharhash}v{\isacharat}w\ {\isasymin}\ A{\isachardoublequote}\isanewline
59 \ \ {\isachardoublequote}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ b{\isacharhash}w\ \ \ {\isasymin}\ B{\isachardoublequote}\isanewline
60 \ \ {\isachardoublequote}{\isasymlbrakk}\ v\ {\isasymin}\ B{\isacharsemicolon}\ w\ {\isasymin}\ B\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ a{\isacharhash}v{\isacharat}w\ {\isasymin}\ B{\isachardoublequote}%
61 \begin{isamarkuptext}%
63 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
64 induction, so is the proof: we show at the same time that all words in
65 \isa{A} contain one more \isa{a} than \isa{b} and all words in \isa{B} contains one more \isa{b} than \isa{a}.%
67 \isacommand{lemma}\ correctness{\isacharcolon}\isanewline
68 \ \ {\isachardoublequote}{\isacharparenleft}w\ {\isasymin}\ S\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}{\isacharparenright}\ \ \ \ \ {\isasymand}\isanewline
69 \ \ \ {\isacharparenleft}w\ {\isasymin}\ A\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isasymand}\isanewline
70 \ \ \ {\isacharparenleft}w\ {\isasymin}\ B\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}%
73 These propositions are expressed with the help of the predefined \isa{filter} function on lists, which has the convenient syntax \isa{{\isacharbrackleft}x{\isasymin}xs{\isachardot}\ P\ x{\isacharbrackright}}, the list of all elements \isa{x} in \isa{xs} such that \isa{P\ x}
74 holds. Remember that on lists \isa{size} and \isa{length} are synonymous.
76 The proof itself is by rule induction and afterwards automatic:%
78 \isacommand{by}\ {\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharcomma}\ auto{\isacharparenright}%
79 \begin{isamarkuptext}%
81 This may seem surprising at first, and is indeed an indication of the power
82 of inductive definitions. But it is also quite straightforward. For example,
83 consider the production $A \to b A A$: if $v,w \in A$ and the elements of $A$
84 contain one more $a$ than~$b$'s, then $bvw$ must again contain one more $a$
87 As usual, the correctness of syntactic descriptions is easy, but completeness
88 is hard: does \isa{S} contain \emph{all} words with an equal number of
89 \isa{a}'s and \isa{b}'s? It turns out that this proof requires the
90 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
91 \isa{b}. This is best seen by imagining counting the difference between the
92 number of \isa{a}'s and \isa{b}'s starting at the left end of the
93 word. We start with 0 and end (at the right end) with 2. Since each move to the
94 right increases or decreases the difference by 1, we must have passed through
95 1 on our way from 0 to 2. Formally, we appeal to the following discrete
96 intermediate value theorem \isa{nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val}
98 \ \ \ \ \ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ i\ {\isacharless}\ n\ {\isasymlongrightarrow}\ {\isasymbar}f\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isasymbar}\ {\isasymle}\ {\isacharhash}{\isadigit{1}}{\isacharsemicolon}\ f\ {\isadigit{0}}\ {\isasymle}\ k{\isacharsemicolon}\ k\ {\isasymle}\ f\ n{\isasymrbrakk}\isanewline
99 \isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ i\ {\isasymle}\ n\ {\isasymand}\ f\ i\ {\isacharequal}\ k%
101 where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers,
102 \isa{{\isasymbar}{\isachardot}{\isasymbar}} is the absolute value function\footnote{See
103 Table~\ref{tab:ascii} in the Appendix for the correct \textsc{ascii}
104 syntax.}, and \isa{{\isacharhash}{\isadigit{1}}} is the integer 1 (see \S\ref{sec:numbers}).
106 First we show that our specific function, the difference between the
107 numbers of \isa{a}'s and \isa{b}'s, does indeed only change by 1 in every
108 move to the right. At this point we also start generalizing from \isa{a}'s
109 and \isa{b}'s to an arbitrary property \isa{P}. Otherwise we would have
110 to prove the desired lemma twice, once as stated above and once with the
111 roles of \isa{a}'s and \isa{b}'s interchanged.%
113 \isacommand{lemma}\ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i\ {\isacharless}\ size\ w{\isachardot}\isanewline
114 \ \ {\isasymbar}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline
115 \ \ \ {\isacharminus}\ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isasymbar}\ {\isasymle}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}%
116 \begin{isamarkuptxt}%
118 The lemma is a bit hard to read because of the coercion function
119 \isa{int\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ int}. It is required because \isa{size} returns
120 a natural number, but subtraction on type~\isa{nat} will do the wrong thing.
121 Function \isa{take} is predefined and \isa{take\ i\ xs} is the prefix of
122 length \isa{i} of \isa{xs}; below we also need \isa{drop\ i\ xs}, which
123 is what remains after that prefix has been dropped from \isa{xs}.
125 The proof is by induction on \isa{w}, with a trivial base case, and a not
126 so trivial induction step. Since it is essentially just arithmetic, we do not
129 \isacommand{apply}{\isacharparenleft}induct\ w{\isacharparenright}\isanewline
130 \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
131 \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}zabs{\isacharunderscore}def\ take{\isacharunderscore}Cons\ split{\isacharcolon}nat{\isachardot}split\ if{\isacharunderscore}splits{\isacharparenright}%
132 \begin{isamarkuptext}%
133 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:%
135 \isacommand{lemma}\ part{\isadigit{1}}{\isacharcolon}\isanewline
136 \ {\isachardoublequote}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}\ {\isasymLongrightarrow}\isanewline
137 \ \ {\isasymexists}i{\isasymle}size\ w{\isachardot}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequote}%
138 \begin{isamarkuptxt}%
140 This is proved by \isa{force} with the help of the intermediate value theorem,
141 instantiated appropriately and with its first premise disposed of by lemma
142 \isa{step{\isadigit{1}}}:%
144 \isacommand{apply}{\isacharparenleft}insert\ nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val{\isacharbrackleft}OF\ step{\isadigit{1}}{\isacharcomma}\ of\ {\isachardoublequote}P{\isachardoublequote}\ {\isachardoublequote}w{\isachardoublequote}\ {\isachardoublequote}{\isacharhash}{\isadigit{1}}{\isachardoublequote}{\isacharbrackright}{\isacharparenright}\isanewline
145 \isacommand{by}\ force%
146 \begin{isamarkuptext}%
149 Lemma \isa{part{\isadigit{1}}} tells us only about the prefix \isa{take\ i\ w}.
150 An easy lemma deals with the suffix \isa{drop\ i\ w}:%
152 \isacommand{lemma}\ part{\isadigit{2}}{\isacharcolon}\isanewline
153 \ \ {\isachardoublequote}{\isasymlbrakk}size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\isanewline
154 \ \ \ \ size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}{\isacharsemicolon}\isanewline
155 \ \ \ \ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isasymrbrakk}\isanewline
156 \ \ \ {\isasymLongrightarrow}\ size{\isacharbrackleft}x{\isasymin}drop\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}drop\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequote}\isanewline
157 \isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharparenright}%
158 \begin{isamarkuptext}%
160 In the proof we have disabled the normally useful lemma
162 \isa{take\ n\ xs\ {\isacharat}\ drop\ n\ xs\ {\isacharequal}\ xs}
163 \rulename{append_take_drop_id}
165 to allow the simplifier to apply the following lemma instead:
167 \ \ \ \ \ {\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}%
170 To dispose of trivial cases automatically, the rules of the inductive
171 definition are declared simplification rules:%
173 \isacommand{declare}\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharbrackleft}simp{\isacharbrackright}%
174 \begin{isamarkuptext}%
176 This could have been done earlier but was not necessary so far.
178 The completeness theorem tells us that if a word has the same number of
179 \isa{a}'s and \isa{b}'s, then it is in \isa{S}, and similarly
180 for \isa{A} and \isa{B}:%
182 \isacommand{theorem}\ completeness{\isacharcolon}\isanewline
183 \ \ {\isachardoublequote}{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ \ \ \ \ {\isasymlongrightarrow}\ w\ {\isasymin}\ S{\isacharparenright}\ {\isasymand}\isanewline
184 \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymlongrightarrow}\ w\ {\isasymin}\ A{\isacharparenright}\ {\isasymand}\isanewline
185 \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymlongrightarrow}\ w\ {\isasymin}\ B{\isacharparenright}{\isachardoublequote}%
186 \begin{isamarkuptxt}%
188 The proof is by induction on \isa{w}. Structural induction would fail here
189 because, as we can see from the grammar, we need to make bigger steps than
190 merely appending a single letter at the front. Hence we induct on the length
191 of \isa{w}, using the induction rule \isa{length{\isacharunderscore}induct}:%
193 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}%
194 \begin{isamarkuptxt}%
196 The \isa{rule} parameter tells \isa{induct{\isacharunderscore}tac} explicitly which induction
197 rule to use. For details see \S\ref{sec:complete-ind} below.
198 In this case the result is that we may assume the lemma already
199 holds for all words shorter than \isa{w}.
201 The proof continues with a case distinction on \isa{w},
202 on whether \isa{w} is empty or not.%
204 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ w{\isacharparenright}\isanewline
205 \ \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}%
206 \begin{isamarkuptxt}%
208 Simplification disposes of the base case and leaves only a conjunction
209 of two step cases to be proved:
210 if \isa{w\ {\isacharequal}\ a\ {\isacharhash}\ v} and \begin{isabelle}%
211 \ \ \ \ \ length\ {\isacharbrackleft}x{\isasymin}v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{2}}%
213 \isa{b\ {\isacharhash}\ v\ {\isasymin}\ A}, and similarly for \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v}.
214 We only consider the first case in detail.
216 After breaking the conjunction up into two cases, we can apply
217 \isa{part{\isadigit{1}}} to the assumption that \isa{w} contains two more \isa{a}'s than \isa{b}'s.%
219 \isacommand{apply}{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline
220 \ \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
221 \ \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
222 \ \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}%
223 \begin{isamarkuptxt}%
225 This yields an index \isa{i\ {\isasymle}\ length\ v} such that
227 \ \ \ \ \ length\ {\isacharbrackleft}x{\isasymin}take\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}take\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}%
229 With the help of \isa{part{\isadigit{2}}} it follows that
231 \ \ \ \ \ length\ {\isacharbrackleft}x{\isasymin}drop\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}drop\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}%
234 \ \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
235 \ \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}%
236 \begin{isamarkuptxt}%
238 Now it is time to decompose \isa{v} in the conclusion \isa{b\ {\isacharhash}\ v\ {\isasymin}\ A}
239 into \isa{take\ i\ v\ {\isacharat}\ drop\ i\ v},%
241 \ \isacommand{apply}{\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}%
242 \begin{isamarkuptxt}%
244 (the variables \isa{n{\isadigit{1}}} and \isa{t} are the result of composing the
245 theorems \isa{subst} and \isa{append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id})
246 after which the appropriate rule of the grammar reduces the goal
247 to the two subgoals \isa{take\ i\ v\ {\isasymin}\ A} and \isa{drop\ i\ v\ {\isasymin}\ A}:%
249 \ \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}%
250 \begin{isamarkuptxt}%
251 Both subgoals follow from the induction hypothesis because both \isa{take\ i\ v} and \isa{drop\ i\ v} are shorter than \isa{w}:%
253 \ \ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline
254 \ \isacommand{apply}{\isacharparenleft}force\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}%
255 \begin{isamarkuptxt}%
256 The case \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v} is proved analogously:%
258 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
259 \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
260 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
261 \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
262 \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline
263 \isacommand{apply}{\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
264 \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isanewline
265 \ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline
266 \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}%
267 \begin{isamarkuptext}%
268 We conclude this section with a comparison of our proof with
269 Hopcroft\index{Hopcroft, J. E.} and Ullman's\index{Ullman, J. D.}
270 \cite[p.\ts81]{HopcroftUllman}.
271 For a start, the textbook
272 grammar, for no good reason, excludes the empty word, thus complicating
273 matters just a little bit: they have 8 instead of our 7 productions.
275 More importantly, the proof itself is different: rather than
276 separating the two directions, they perform one induction on the
277 length of a word. This deprives them of the beauty of rule induction,
278 and in the easy direction (correctness) their reasoning is more
279 detailed than our \isa{auto}. For the hard part (completeness), they
280 consider just one of the cases that our \isa{simp{\isacharunderscore}all} disposes of
281 automatically. Then they conclude the proof by saying about the
282 remaining cases: ``We do this in a manner similar to our method of
283 proof for part (1); this part is left to the reader''. But this is
284 precisely the part that requires the intermediate value theorem and
285 thus is not at all similar to the other cases (which are automatic in
286 Isabelle). The authors are at least cavalier about this point and may
287 even have overlooked the slight difficulty lurking in the omitted
288 cases. Such errors are found in many pen-and-paper proofs when they
289 are scrutinized formally.%
290 \index{grammars!defining inductively|)}%
295 %%% TeX-master: "root"