3 \def\isabellecontext{AB}%
5 \isamarkupsection{Case Study: A Context Free Grammar%
10 Grammars are nothing but shorthands for inductive definitions of nonterminals
11 which represent sets of strings. For example, the production
12 $A \to B c$ is short for
13 \[ w \in B \Longrightarrow wc \in A \]
14 This section demonstrates this idea with an example
15 due to Hopcroft and Ullman, a grammar for generating all words with an
16 equal number of $a$'s and~$b$'s:
18 S &\to& \epsilon \mid b A \mid a B \nonumber\\
19 A &\to& a S \mid b A A \nonumber\\
20 B &\to& b S \mid a B B \nonumber
22 At the end we say a few words about the relationship between
23 the original proof \cite[p.\ts81]{HopcroftUllman} and our formal version.
25 We start by fixing the alphabet, which consists only of \isa{a}'s
28 \isacommand{datatype}\ alfa\ {\isacharequal}\ a\ {\isacharbar}\ b%
29 \begin{isamarkuptext}%
31 For convenience we include the following easy lemmas as simplification rules:%
33 \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
34 \isacommand{by}\ {\isacharparenleft}case{\isacharunderscore}tac\ x{\isacharcomma}\ auto{\isacharparenright}%
35 \begin{isamarkuptext}%
37 Words over this alphabet are of type \isa{alfa\ list}, and
38 the three nonterminals are declared as sets of such words:%
40 \isacommand{consts}\ S\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline
41 \ \ \ \ \ \ \ A\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline
42 \ \ \ \ \ \ \ B\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}%
43 \begin{isamarkuptext}%
45 The productions above are recast as a \emph{mutual} inductive
46 definition\index{inductive definition!simultaneous}
47 of \isa{S}, \isa{A} and~\isa{B}:%
49 \isacommand{inductive}\ S\ A\ B\isanewline
50 \isakeyword{intros}\isanewline
51 \ \ {\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}\ {\isasymin}\ S{\isachardoublequote}\isanewline
52 \ \ {\isachardoublequote}w\ {\isasymin}\ A\ {\isasymLongrightarrow}\ b{\isacharhash}w\ {\isasymin}\ S{\isachardoublequote}\isanewline
53 \ \ {\isachardoublequote}w\ {\isasymin}\ B\ {\isasymLongrightarrow}\ a{\isacharhash}w\ {\isasymin}\ S{\isachardoublequote}\isanewline
55 \ \ {\isachardoublequote}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ a{\isacharhash}w\ \ \ {\isasymin}\ A{\isachardoublequote}\isanewline
56 \ \ {\isachardoublequote}{\isasymlbrakk}\ v{\isasymin}A{\isacharsemicolon}\ w{\isasymin}A\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ b{\isacharhash}v{\isacharat}w\ {\isasymin}\ A{\isachardoublequote}\isanewline
58 \ \ {\isachardoublequote}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ b{\isacharhash}w\ \ \ {\isasymin}\ B{\isachardoublequote}\isanewline
59 \ \ {\isachardoublequote}{\isasymlbrakk}\ v\ {\isasymin}\ B{\isacharsemicolon}\ w\ {\isasymin}\ B\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ a{\isacharhash}v{\isacharat}w\ {\isasymin}\ B{\isachardoublequote}%
60 \begin{isamarkuptext}%
62 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
63 induction, so is the proof: we show at the same time that all words in
64 \isa{A} contain one more \isa{a} than \isa{b} and all words in \isa{B} contains one more \isa{b} than \isa{a}.%
66 \isacommand{lemma}\ correctness{\isacharcolon}\isanewline
67 \ \ {\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
68 \ \ \ {\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
69 \ \ \ {\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}%
72 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}
73 holds. Remember that on lists \isa{size} and \isa{length} are synonymous.
75 The proof itself is by rule induction and afterwards automatic:%
77 \isacommand{by}\ {\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharcomma}\ auto{\isacharparenright}%
78 \begin{isamarkuptext}%
80 This may seem surprising at first, and is indeed an indication of the power
81 of inductive definitions. But it is also quite straightforward. For example,
82 consider the production $A \to b A A$: if $v,w \in A$ and the elements of $A$
83 contain one more $a$ than~$b$'s, then $bvw$ must again contain one more $a$
86 As usual, the correctness of syntactic descriptions is easy, but completeness
87 is hard: does \isa{S} contain \emph{all} words with an equal number of
88 \isa{a}'s and \isa{b}'s? It turns out that this proof requires the
89 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
90 \isa{b}. This is best seen by imagining counting the difference between the
91 number of \isa{a}'s and \isa{b}'s starting at the left end of the
92 word. We start with 0 and end (at the right end) with 2. Since each move to the
93 right increases or decreases the difference by 1, we must have passed through
94 1 on our way from 0 to 2. Formally, we appeal to the following discrete
95 intermediate value theorem \isa{nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val}
97 \ \ \ \ \ {\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
98 \isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ i\ {\isasymle}\ n\ {\isasymand}\ f\ i\ {\isacharequal}\ k%
100 where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers,
101 \isa{{\isasymbar}{\isachardot}{\isasymbar}} is the absolute value function, and \isa{{\isacharhash}{\isadigit{1}}} is the
102 integer 1 (see \S\ref{sec:numbers}).
104 First we show that our specific function, the difference between the
105 numbers of \isa{a}'s and \isa{b}'s, does indeed only change by 1 in every
106 move to the right. At this point we also start generalizing from \isa{a}'s
107 and \isa{b}'s to an arbitrary property \isa{P}. Otherwise we would have
108 to prove the desired lemma twice, once as stated above and once with the
109 roles of \isa{a}'s and \isa{b}'s interchanged.%
111 \isacommand{lemma}\ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i\ {\isacharless}\ size\ w{\isachardot}\isanewline
112 \ \ {\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
113 \ \ \ {\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}%
114 \begin{isamarkuptxt}%
116 The lemma is a bit hard to read because of the coercion function
117 \isa{int\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ int}. It is required because \isa{size} returns
118 a natural number, but subtraction on type~\isa{nat} will do the wrong thing.
119 Function \isa{take} is predefined and \isa{take\ i\ xs} is the prefix of
120 length \isa{i} of \isa{xs}; below we also need \isa{drop\ i\ xs}, which
121 is what remains after that prefix has been dropped from \isa{xs}.
123 The proof is by induction on \isa{w}, with a trivial base case, and a not
124 so trivial induction step. Since it is essentially just arithmetic, we do not
127 \isacommand{apply}{\isacharparenleft}induct\ w{\isacharparenright}\isanewline
128 \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
129 \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}zabs{\isacharunderscore}def\ take{\isacharunderscore}Cons\ split{\isacharcolon}nat{\isachardot}split\ if{\isacharunderscore}splits{\isacharparenright}%
130 \begin{isamarkuptext}%
131 Finally we come to the above mentioned lemma about cutting in half a word with two
132 more elements of one sort than of the other sort:%
134 \isacommand{lemma}\ part{\isadigit{1}}{\isacharcolon}\isanewline
135 \ {\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
136 \ \ {\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}%
137 \begin{isamarkuptxt}%
139 This is proved by \isa{force} with the help of the intermediate value theorem,
140 instantiated appropriately and with its first premise disposed of by lemma
141 \isa{step{\isadigit{1}}}:%
143 \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
144 \isacommand{by}\ force%
145 \begin{isamarkuptext}%
148 Lemma \isa{part{\isadigit{1}}} tells us only about the prefix \isa{take\ i\ w}.
149 An easy lemma deals with the suffix \isa{drop\ i\ w}:%
151 \isacommand{lemma}\ part{\isadigit{2}}{\isacharcolon}\isanewline
152 \ \ {\isachardoublequote}{\isasymlbrakk}size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\isanewline
153 \ \ \ \ size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}{\isacharsemicolon}\isanewline
154 \ \ \ \ 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
155 \ \ \ {\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
156 \isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharparenright}%
157 \begin{isamarkuptext}%
159 In the proof, we have had to disable a normally useful lemma:
161 \isa{take\ n\ xs\ {\isacharat}\ drop\ n\ xs\ {\isacharequal}\ xs}
162 \rulename{append_take_drop_id}
165 To dispose of trivial cases automatically, the rules of the inductive
166 definition are declared simplification rules:%
168 \isacommand{declare}\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharbrackleft}simp{\isacharbrackright}%
169 \begin{isamarkuptext}%
171 This could have been done earlier but was not necessary so far.
173 The completeness theorem tells us that if a word has the same number of
174 \isa{a}'s and \isa{b}'s, then it is in \isa{S}, and similarly
175 for \isa{A} and \isa{B}:%
177 \isacommand{theorem}\ completeness{\isacharcolon}\isanewline
178 \ \ {\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
179 \ \ \ {\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
180 \ \ \ {\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}%
181 \begin{isamarkuptxt}%
183 The proof is by induction on \isa{w}. Structural induction would fail here
184 because, as we can see from the grammar, we need to make bigger steps than
185 merely appending a single letter at the front. Hence we induct on the length
186 of \isa{w}, using the induction rule \isa{length{\isacharunderscore}induct}:%
188 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}%
189 \begin{isamarkuptxt}%
191 The \isa{rule} parameter tells \isa{induct{\isacharunderscore}tac} explicitly which induction
192 rule to use. For details see \S\ref{sec:complete-ind} below.
193 In this case the result is that we may assume the lemma already
194 holds for all words shorter than \isa{w}.
196 The proof continues with a case distinction on \isa{w},
197 i.e.\ if \isa{w} is empty or not.%
199 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ w{\isacharparenright}\isanewline
200 \ \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}%
201 \begin{isamarkuptxt}%
203 Simplification disposes of the base case and leaves only two step
205 if \isa{w\ {\isacharequal}\ a\ {\isacharhash}\ v} and \begin{isabelle}%
206 \ \ \ \ \ length\ {\isacharbrackleft}x{\isasymin}v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{2}}%
208 \isa{b\ {\isacharhash}\ v\ {\isasymin}\ A}, and similarly for \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v}.
209 We only consider the first case in detail.
211 After breaking the conjuction up into two cases, we can apply
212 \isa{part{\isadigit{1}}} to the assumption that \isa{w} contains two more \isa{a}'s than \isa{b}'s.%
214 \isacommand{apply}{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline
215 \ \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
216 \ \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
217 \ \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
218 \ \isacommand{apply}{\isacharparenleft}erule\ conjE{\isacharparenright}%
219 \begin{isamarkuptxt}%
221 This yields an index \isa{i\ {\isasymle}\ length\ v} such that
223 \ \ \ \ \ 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}}%
225 With the help of \isa{part{\isadigit{2}}} it follows that
227 \ \ \ \ \ 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}}%
230 \ \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
231 \ \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}%
232 \begin{isamarkuptxt}%
234 Now it is time to decompose \isa{v} in the conclusion \isa{b\ {\isacharhash}\ v\ {\isasymin}\ A}
235 into \isa{take\ i\ v\ {\isacharat}\ drop\ i\ v},
236 after which the appropriate rule of the grammar reduces the goal
237 to the two subgoals \isa{take\ i\ v\ {\isasymin}\ A} and \isa{drop\ i\ v\ {\isasymin}\ A}:%
239 \ \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
240 \ \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}%
241 \begin{isamarkuptxt}%
243 Both subgoals follow from the induction hypothesis because both \isa{take\ i\ v} and \isa{drop\ i\ v} are shorter than \isa{w}:%
245 \ \ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline
246 \ \isacommand{apply}{\isacharparenleft}force\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}%
247 \begin{isamarkuptxt}%
249 Note that the variables \isa{n{\isadigit{1}}} and \isa{t} referred to in the
250 substitution step above come from the derived theorem \isa{subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}}.
252 The case \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v} is proved analogously:%
254 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
255 \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
256 \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
257 \isacommand{apply}{\isacharparenleft}erule\ conjE{\isacharparenright}\isanewline
258 \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
259 \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline
260 \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
261 \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isanewline
262 \ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline
263 \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}%
264 \begin{isamarkuptext}%
265 We conclude this section with a comparison of our proof with
266 Hopcroft and Ullman's \cite[p.\ts81]{HopcroftUllman}. For a start, the texbook
267 grammar, for no good reason, excludes the empty word. That complicates
268 matters just a little bit because we now have 8 instead of our 7 productions.
270 More importantly, the proof itself is different: rather than
271 separating the two directions, they perform one induction on the
272 length of a word. This deprives them of the beauty of rule induction,
273 and in the easy direction (correctness) their reasoning is more
274 detailed than our \isa{auto}. For the hard part (completeness), they
275 consider just one of the cases that our \isa{simp{\isacharunderscore}all} disposes of
276 automatically. Then they conclude the proof by saying about the
277 remaining cases: ``We do this in a manner similar to our method of
278 proof for part (1); this part is left to the reader''. But this is
279 precisely the part that requires the intermediate value theorem and
280 thus is not at all similar to the other cases (which are automatic in
281 Isabelle). The authors are at least cavalier about this point and may
282 even have overlooked the slight difficulty lurking in the omitted
283 cases. This is not atypical for pen-and-paper proofs, once analysed in
289 %%% TeX-master: "root"