3 \def\isabellecontext{AB}%
6 \isamarkupsection{Case Study: A Context Free Grammar%
10 \begin{isamarkuptext}%
12 \index{grammars!defining inductively|(}%
13 Grammars are nothing but shorthands for inductive definitions of nonterminals
14 which represent sets of strings. For example, the production
15 $A \to B c$ is short for
16 \[ w \in B \Longrightarrow wc \in A \]
17 This section demonstrates this idea with an example
18 due to Hopcroft and Ullman, a grammar for generating all words with an
19 equal number of $a$'s and~$b$'s:
21 S &\to& \epsilon \mid b A \mid a B \nonumber\\
22 A &\to& a S \mid b A A \nonumber\\
23 B &\to& b S \mid a B B \nonumber
25 At the end we say a few words about the relationship between
26 the original proof \cite[p.\ts81]{HopcroftUllman} and our formal version.
28 We start by fixing the alphabet, which consists only of \isa{a}'s
32 \isacommand{datatype}\ alfa\ {\isacharequal}\ a\ {\isacharbar}\ b\isamarkupfalse%
34 \begin{isamarkuptext}%
36 For convenience we include the following easy lemmas as simplification rules:%
39 \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
41 \isacommand{by}\ {\isacharparenleft}case{\isacharunderscore}tac\ x{\isacharcomma}\ auto{\isacharparenright}\isamarkupfalse%
43 \begin{isamarkuptext}%
45 Words over this alphabet are of type \isa{alfa\ list}, and
46 the three nonterminals are declared as sets of such words:%
49 \isacommand{consts}\ S\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline
50 \ \ \ \ \ \ \ A\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline
51 \ \ \ \ \ \ \ B\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isamarkupfalse%
53 \begin{isamarkuptext}%
55 The productions above are recast as a \emph{mutual} inductive
56 definition\index{inductive definition!simultaneous}
57 of \isa{S}, \isa{A} and~\isa{B}:%
60 \isacommand{inductive}\ S\ A\ B\isanewline
61 \isakeyword{intros}\isanewline
62 \ \ {\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}\ {\isasymin}\ S{\isachardoublequote}\isanewline
63 \ \ {\isachardoublequote}w\ {\isasymin}\ A\ {\isasymLongrightarrow}\ b{\isacharhash}w\ {\isasymin}\ S{\isachardoublequote}\isanewline
64 \ \ {\isachardoublequote}w\ {\isasymin}\ B\ {\isasymLongrightarrow}\ a{\isacharhash}w\ {\isasymin}\ S{\isachardoublequote}\isanewline
66 \ \ {\isachardoublequote}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ a{\isacharhash}w\ \ \ {\isasymin}\ A{\isachardoublequote}\isanewline
67 \ \ {\isachardoublequote}{\isasymlbrakk}\ v{\isasymin}A{\isacharsemicolon}\ w{\isasymin}A\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ b{\isacharhash}v{\isacharat}w\ {\isasymin}\ A{\isachardoublequote}\isanewline
69 \ \ {\isachardoublequote}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ b{\isacharhash}w\ \ \ {\isasymin}\ B{\isachardoublequote}\isanewline
70 \ \ {\isachardoublequote}{\isasymlbrakk}\ v\ {\isasymin}\ B{\isacharsemicolon}\ w\ {\isasymin}\ B\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ a{\isacharhash}v{\isacharat}w\ {\isasymin}\ B{\isachardoublequote}\isamarkupfalse%
72 \begin{isamarkuptext}%
74 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
75 induction, so is the proof: we show at the same time that all words in
76 \isa{A} contain one more \isa{a} than \isa{b} and all words in \isa{B} contains one more \isa{b} than \isa{a}.%
79 \isacommand{lemma}\ correctness{\isacharcolon}\isanewline
80 \ \ {\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
81 \ \ \ {\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
82 \ \ \ {\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}\isamarkupfalse%
86 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}
87 holds. Remember that on lists \isa{size} and \isa{length} are synonymous.
89 The proof itself is by rule induction and afterwards automatic:%
92 \isacommand{by}\ {\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharcomma}\ auto{\isacharparenright}\isamarkupfalse%
94 \begin{isamarkuptext}%
96 This may seem surprising at first, and is indeed an indication of the power
97 of inductive definitions. But it is also quite straightforward. For example,
98 consider the production $A \to b A A$: if $v,w \in A$ and the elements of $A$
99 contain one more $a$ than~$b$'s, then $bvw$ must again contain one more $a$
102 As usual, the correctness of syntactic descriptions is easy, but completeness
103 is hard: does \isa{S} contain \emph{all} words with an equal number of
104 \isa{a}'s and \isa{b}'s? It turns out that this proof requires the
105 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
106 \isa{b}. This is best seen by imagining counting the difference between the
107 number of \isa{a}'s and \isa{b}'s starting at the left end of the
108 word. We start with 0 and end (at the right end) with 2. Since each move to the
109 right increases or decreases the difference by 1, we must have passed through
110 1 on our way from 0 to 2. Formally, we appeal to the following discrete
111 intermediate value theorem \isa{nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val}
113 \ \ \ \ \ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ i\ {\isacharless}\ n\ {\isasymlongrightarrow}\ {\isasymbar}f\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isasymbar}\ {\isasymle}\ Numeral{\isadigit{1}}{\isacharsemicolon}\ f\ {\isadigit{0}}\ {\isasymle}\ k{\isacharsemicolon}\ k\ {\isasymle}\ f\ n{\isasymrbrakk}\isanewline
114 \isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ i\ {\isasymle}\ n\ {\isasymand}\ f\ i\ {\isacharequal}\ k%
116 where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers,
117 \isa{{\isasymbar}{\isachardot}{\isasymbar}} is the absolute value function\footnote{See
118 Table~\ref{tab:ascii} in the Appendix for the correct \textsc{ascii}
119 syntax.}, and \isa{{\isadigit{1}}} is the integer 1 (see \S\ref{sec:numbers}).
121 First we show that our specific function, the difference between the
122 numbers of \isa{a}'s and \isa{b}'s, does indeed only change by 1 in every
123 move to the right. At this point we also start generalizing from \isa{a}'s
124 and \isa{b}'s to an arbitrary property \isa{P}. Otherwise we would have
125 to prove the desired lemma twice, once as stated above and once with the
126 roles of \isa{a}'s and \isa{b}'s interchanged.%
129 \isacommand{lemma}\ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i\ {\isacharless}\ size\ w{\isachardot}\isanewline
130 \ \ {\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
131 \ \ \ {\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}\ Numeral{\isadigit{1}}{\isachardoublequote}\isamarkupfalse%
133 \begin{isamarkuptxt}%
135 The lemma is a bit hard to read because of the coercion function
136 \isa{int\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ int}. It is required because \isa{size} returns
137 a natural number, but subtraction on type~\isa{nat} will do the wrong thing.
138 Function \isa{take} is predefined and \isa{take\ i\ xs} is the prefix of
139 length \isa{i} of \isa{xs}; below we also need \isa{drop\ i\ xs}, which
140 is what remains after that prefix has been dropped from \isa{xs}.
142 The proof is by induction on \isa{w}, with a trivial base case, and a not
143 so trivial induction step. Since it is essentially just arithmetic, we do not
147 \isacommand{apply}{\isacharparenleft}induct\ w{\isacharparenright}\isanewline
149 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
151 \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ zabs{\isacharunderscore}def\ take{\isacharunderscore}Cons\ split{\isacharcolon}\ nat{\isachardot}split\ if{\isacharunderscore}splits{\isacharparenright}\isamarkupfalse%
153 \begin{isamarkuptext}%
154 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:%
157 \isacommand{lemma}\ part{\isadigit{1}}{\isacharcolon}\isanewline
158 \ {\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
159 \ \ {\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}\isamarkupfalse%
161 \begin{isamarkuptxt}%
163 This is proved by \isa{force} with the help of the intermediate value theorem,
164 instantiated appropriately and with its first premise disposed of by lemma
165 \isa{step{\isadigit{1}}}:%
168 \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}Numeral{\isadigit{1}}{\isachardoublequote}{\isacharbrackright}{\isacharparenright}\isanewline
170 \isacommand{by}\ force\isamarkupfalse%
172 \begin{isamarkuptext}%
175 Lemma \isa{part{\isadigit{1}}} tells us only about the prefix \isa{take\ i\ w}.
176 An easy lemma deals with the suffix \isa{drop\ i\ w}:%
179 \isacommand{lemma}\ part{\isadigit{2}}{\isacharcolon}\isanewline
180 \ \ {\isachardoublequote}{\isasymlbrakk}size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\isanewline
181 \ \ \ \ size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}{\isacharsemicolon}\isanewline
182 \ \ \ \ 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
183 \ \ \ {\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
185 \isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharparenright}\isamarkupfalse%
187 \begin{isamarkuptext}%
189 In the proof we have disabled the normally useful lemma
191 \isa{take\ n\ xs\ {\isacharat}\ drop\ n\ xs\ {\isacharequal}\ xs}
192 \rulename{append_take_drop_id}
194 to allow the simplifier to apply the following lemma instead:
196 \ \ \ \ \ {\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}%
199 To dispose of trivial cases automatically, the rules of the inductive
200 definition are declared simplification rules:%
203 \isacommand{declare}\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharbrackleft}simp{\isacharbrackright}\isamarkupfalse%
205 \begin{isamarkuptext}%
207 This could have been done earlier but was not necessary so far.
209 The completeness theorem tells us that if a word has the same number of
210 \isa{a}'s and \isa{b}'s, then it is in \isa{S}, and similarly
211 for \isa{A} and \isa{B}:%
214 \isacommand{theorem}\ completeness{\isacharcolon}\isanewline
215 \ \ {\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
216 \ \ \ {\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
217 \ \ \ {\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}\isamarkupfalse%
219 \begin{isamarkuptxt}%
221 The proof is by induction on \isa{w}. Structural induction would fail here
222 because, as we can see from the grammar, we need to make bigger steps than
223 merely appending a single letter at the front. Hence we induct on the length
224 of \isa{w}, using the induction rule \isa{length{\isacharunderscore}induct}:%
227 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}\isamarkupfalse%
230 \begin{isamarkuptxt}%
232 The \isa{rule} parameter tells \isa{induct{\isacharunderscore}tac} explicitly which induction
233 rule to use. For details see \S\ref{sec:complete-ind} below.
234 In this case the result is that we may assume the lemma already
235 holds for all words shorter than \isa{w}.
237 The proof continues with a case distinction on \isa{w},
238 on whether \isa{w} is empty or not.%
241 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ w{\isacharparenright}\isanewline
243 \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
246 \begin{isamarkuptxt}%
248 Simplification disposes of the base case and leaves only a conjunction
249 of two step cases to be proved:
250 if \isa{w\ {\isacharequal}\ a\ {\isacharhash}\ v} and \begin{isabelle}%
251 \ \ \ \ \ length\ {\isacharbrackleft}x{\isasymin}v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{2}}%
253 \isa{b\ {\isacharhash}\ v\ {\isasymin}\ A}, and similarly for \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v}.
254 We only consider the first case in detail.
256 After breaking the conjunction up into two cases, we can apply
257 \isa{part{\isadigit{1}}} to the assumption that \isa{w} contains two more \isa{a}'s than \isa{b}'s.%
260 \isacommand{apply}{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline
262 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
264 \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
266 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isamarkupfalse%
268 \begin{isamarkuptxt}%
270 This yields an index \isa{i\ {\isasymle}\ length\ v} such that
272 \ \ \ \ \ 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}}%
274 With the help of \isa{part{\isadigit{2}}} it follows that
276 \ \ \ \ \ 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}}%
280 \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
282 \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isamarkupfalse%
284 \begin{isamarkuptxt}%
286 Now it is time to decompose \isa{v} in the conclusion \isa{b\ {\isacharhash}\ v\ {\isasymin}\ A}
287 into \isa{take\ i\ v\ {\isacharat}\ drop\ i\ v},%
290 \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}\isamarkupfalse%
292 \begin{isamarkuptxt}%
294 (the variables \isa{n{\isadigit{1}}} and \isa{t} are the result of composing the
295 theorems \isa{subst} and \isa{append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id})
296 after which the appropriate rule of the grammar reduces the goal
297 to the two subgoals \isa{take\ i\ v\ {\isasymin}\ A} and \isa{drop\ i\ v\ {\isasymin}\ A}:%
300 \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isamarkupfalse%
302 \begin{isamarkuptxt}%
303 Both subgoals follow from the induction hypothesis because both \isa{take\ i\ v} and \isa{drop\ i\ v} are shorter than \isa{w}:%
306 \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline
308 \isacommand{apply}{\isacharparenleft}force\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isamarkupfalse%
310 \begin{isamarkuptxt}%
311 The case \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v} is proved analogously:%
314 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
316 \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
318 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
320 \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
322 \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline
324 \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
326 \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isanewline
328 \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline
330 \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isamarkupfalse%
332 \begin{isamarkuptext}%
333 We conclude this section with a comparison of our proof with
334 Hopcroft\index{Hopcroft, J. E.} and Ullman's\index{Ullman, J. D.}
335 \cite[p.\ts81]{HopcroftUllman}.
336 For a start, the textbook
337 grammar, for no good reason, excludes the empty word, thus complicating
338 matters just a little bit: they have 8 instead of our 7 productions.
340 More importantly, the proof itself is different: rather than
341 separating the two directions, they perform one induction on the
342 length of a word. This deprives them of the beauty of rule induction,
343 and in the easy direction (correctness) their reasoning is more
344 detailed than our \isa{auto}. For the hard part (completeness), they
345 consider just one of the cases that our \isa{simp{\isacharunderscore}all} disposes of
346 automatically. Then they conclude the proof by saying about the
347 remaining cases: ``We do this in a manner similar to our method of
348 proof for part (1); this part is left to the reader''. But this is
349 precisely the part that requires the intermediate value theorem and
350 thus is not at all similar to the other cases (which are automatic in
351 Isabelle). The authors are at least cavalier about this point and may
352 even have overlooked the slight difficulty lurking in the omitted
353 cases. Such errors are found in many pen-and-paper proofs when they
354 are scrutinized formally.%
355 \index{grammars!defining inductively|)}%
362 %%% TeX-master: "root"