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 a standard example
15 \cite[p.\ 81]{HopcroftUllman}, 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 of the formalization
23 and the text in the book~\cite[p.\ 81]{HopcroftUllman}.
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{apply}{\isacharparenleft}case{\isacharunderscore}tac\ x{\isacharparenright}\isanewline
35 \isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
36 \begin{isamarkuptext}%
38 Words over this alphabet are of type \isa{alfa\ list}, and
39 the three nonterminals are declare 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 above productions are recast as a \emph{simultaneous} 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 simultaneous
64 induction, so is this 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{size} are synonymous.
76 The proof itself is by rule induction and afterwards automatic:%
78 \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharparenright}\isanewline
79 \isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
80 \begin{isamarkuptext}%
82 This may seem surprising at first, and is indeed an indication of the power
83 of inductive definitions. But it is also quite straightforward. For example,
84 consider the production $A \to b A A$: if $v,w \in A$ and the elements of $A$
85 contain one more $a$ than $b$'s, then $bvw$ must again contain one more $a$
88 As usual, the correctness of syntactic descriptions is easy, but completeness
89 is hard: does \isa{S} contain \emph{all} words with an equal number of
90 \isa{a}'s and \isa{b}'s? It turns out that this proof requires the
91 following little lemma: every string with two more \isa{a}'s than \isa{b}'s can be cut somehwere such that each half has one more \isa{a} than
92 \isa{b}. This is best seen by imagining counting the difference between the
93 number of \isa{a}'s and \isa{b}'s starting at the left end of the
94 word. We start with 0 and end (at the right end) with 2. Since each move to the
95 right increases or decreases the difference by 1, we must have passed through
96 1 on our way from 0 to 2. Formally, we appeal to the following discrete
97 intermediate value theorem \isa{nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val}
99 \ \ \ \ \ {\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
100 \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ i\ {\isasymle}\ n\ {\isasymand}\ f\ i\ {\isacharequal}\ k%
102 where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers,
103 \isa{abs} is the absolute value function, and \isa{{\isacharhash}{\isadigit{1}}} is the
104 integer 1 (see \S\ref{sec:numbers}).
106 First we show that the 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 \ \ abs{\isacharparenleft}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ \ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\isanewline
115 \ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline
116 \ \ \ \ \ \ {\isacharminus}\isanewline
117 \ \ \ \ \ \ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ \ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\isanewline
118 \ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymle}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}%
119 \begin{isamarkuptxt}%
121 The lemma is a bit hard to read because of the coercion function
122 \isa{{\isachardoublequote}int{\isacharcolon}{\isacharcolon}nat\ {\isasymRightarrow}\ int{\isachardoublequote}}. It is required because \isa{size} returns
123 a natural number, but \isa{{\isacharminus}} on \isa{nat} will do the wrong thing.
124 Function \isa{take} is predefined and \isa{take\ i\ xs} is the prefix of
125 length \isa{i} of \isa{xs}; below we als need \isa{drop\ i\ xs}, which
126 is what remains after that prefix has been dropped from \isa{xs}.
128 The proof is by induction on \isa{w}, with a trivial base case, and a not
129 so trivial induction step. Since it is essentially just arithmetic, we do not
132 \isacommand{apply}{\isacharparenleft}induct\ w{\isacharparenright}\isanewline
133 \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
134 \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}zabs{\isacharunderscore}def\ take{\isacharunderscore}Cons\ split{\isacharcolon}nat{\isachardot}split\ if{\isacharunderscore}splits{\isacharparenright}%
135 \begin{isamarkuptext}%
136 Finally we come to the above mentioned lemma about cutting a word with two
137 more elements of one sort than of the other sort into two halves:%
139 \isacommand{lemma}\ part{\isadigit{1}}{\isacharcolon}\isanewline
140 \ {\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
141 \ \ {\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}%
142 \begin{isamarkuptxt}%
144 This is proved with the help of the intermediate value theorem, instantiated
145 appropriately and with its first premise disposed of by lemma
146 \isa{step{\isadigit{1}}}.%
148 \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
149 \isacommand{apply}\ simp\isanewline
150 \isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}int{\isacharunderscore}Suc\ add{\isacharcolon}zdiff{\isacharunderscore}eq{\isacharunderscore}eq\ sym{\isacharbrackleft}OF\ int{\isacharunderscore}Suc{\isacharbrackright}{\isacharparenright}%
151 \begin{isamarkuptext}%
153 The additional lemmas are needed to mediate between \isa{nat} and \isa{int}.
155 Lemma \isa{part{\isadigit{1}}} tells us only about the prefix \isa{take\ i\ w}.
156 The suffix \isa{drop\ i\ w} is dealt with in the following easy lemma:%
158 \isacommand{lemma}\ part{\isadigit{2}}{\isacharcolon}\isanewline
159 \ \ {\isachardoublequote}{\isasymlbrakk}size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\isanewline
160 \ \ \ \ size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}{\isacharsemicolon}\isanewline
161 \ \ \ \ 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
162 \ \ \ {\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
163 \isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharparenright}%
164 \begin{isamarkuptext}%
166 Lemma \isa{append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id}, \isa{take\ n\ xs\ {\isacharat}\ drop\ n\ xs\ {\isacharequal}\ xs},
167 which is generally useful, needs to be disabled for once.
169 To dispose of trivial cases automatically, the rules of the inductive
170 definition are declared simplification rules:%
172 \isacommand{declare}\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharbrackleft}simp{\isacharbrackright}%
173 \begin{isamarkuptext}%
175 This could have been done earlier but was not necessary so far.
177 The completeness theorem tells us that if a word has the same number of
178 \isa{a}'s and \isa{b}'s, then it is in \isa{S}, and similarly and
179 simultaneously for \isa{A} and \isa{B}:%
181 \isacommand{theorem}\ completeness{\isacharcolon}\isanewline
182 \ \ {\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
183 \ \ \ {\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
184 \ \ \ {\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}%
185 \begin{isamarkuptxt}%
187 The proof is by induction on \isa{w}. Structural induction would fail here
188 because, as we can see from the grammar, we need to make bigger steps than
189 merely appending a single letter at the front. Hence we induct on the length
190 of \isa{w}, using the induction rule \isa{length{\isacharunderscore}induct}:%
192 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}%
193 \begin{isamarkuptxt}%
195 The \isa{rule} parameter tells \isa{induct{\isacharunderscore}tac} explicitly which induction
196 rule to use. For details see \S\ref{sec:complete-ind} below.
197 In this case the result is that we may assume the lemma already
198 holds for all words shorter than \isa{w}.
200 The proof continues with a case distinction on \isa{w},
201 i.e.\ if \isa{w} is empty or not.%
203 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ w{\isacharparenright}\isanewline
204 \ \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}%
205 \begin{isamarkuptxt}%
207 Simplification disposes of the base case and leaves only two step
209 if \isa{w\ {\isacharequal}\ a\ {\isacharhash}\ v} and \isa{length\ {\isacharbrackleft}x{\isasymin}v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{2}}} then
210 \isa{b\ {\isacharhash}\ v\ {\isasymin}\ A}, and similarly for \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v}.
211 We only consider the first case in detail.
213 After breaking the conjuction up into two cases, we can apply
214 \isa{part{\isadigit{1}}} to the assumption that \isa{w} contains two more \isa{a}'s than \isa{b}'s.%
216 \isacommand{apply}{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline
217 \ \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
218 \ \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
219 \ \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
220 \ \isacommand{apply}{\isacharparenleft}erule\ conjE{\isacharparenright}%
221 \begin{isamarkuptxt}%
223 This yields an index \isa{i\ {\isasymle}\ length\ v} such that
224 \isa{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{1}}} it follows that
226 \isa{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}}}.%
228 \ \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
229 \ \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}%
230 \begin{isamarkuptxt}%
232 Now it is time to decompose \isa{v} in the conclusion \isa{b\ {\isacharhash}\ v\ {\isasymin}\ A}
233 into \isa{take\ i\ v\ {\isacharat}\ drop\ i\ v},
234 after which the appropriate rule of the grammar reduces the goal
235 to the two subgoals \isa{take\ i\ v\ {\isasymin}\ A} and \isa{drop\ i\ v\ {\isasymin}\ A}:%
237 \ \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
238 \ \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}%
239 \begin{isamarkuptxt}%
241 Both subgoals follow from the induction hypothesis because both \isa{take\ i\ v} and \isa{drop\ i\ v} are shorter than \isa{w}:%
243 \ \ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline
244 \ \isacommand{apply}{\isacharparenleft}force\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}%
245 \begin{isamarkuptxt}%
247 Note that the variables \isa{n{\isadigit{1}}} and \isa{t} referred to in the
248 substitution step above come from the derived theorem \isa{subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}}.
250 The case \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v} is proved completely analogously:%
252 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
253 \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
254 \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
255 \isacommand{apply}{\isacharparenleft}erule\ conjE{\isacharparenright}\isanewline
256 \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
257 \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline
258 \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
259 \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isanewline
260 \ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline
261 \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}%
262 \begin{isamarkuptext}%
263 We conclude this section with a comparison of the above proof and the one
264 in the textbook \cite[p.\ 81]{HopcroftUllman}. For a start, the texbook
265 grammar, for no good reason, excludes the empty word, which complicates
266 matters just a little bit because we now have 8 instead of our 7 productions.
268 More importantly, the proof itself is different: rather than separating the
269 two directions, they perform one induction on the length of a word. This
270 deprives them of the beauty of rule induction and in the easy direction
271 (correctness) their reasoning is more detailed than our \isa{auto}. For the
272 hard part (completeness), they consider just one of the cases that our \isa{simp{\isacharunderscore}all} disposes of automatically. Then they conclude the proof by saying
273 about the remaining cases: ``We do this in a manner similar to our method of
274 proof for part (1); this part is left to the reader''. But this is precisely
275 the part that requires the intermediate value theorem and thus is not at all
276 similar to the other cases (which are automatic in Isabelle). We conclude
277 that the authors are at least cavalier about this point and may even have
278 overlooked the slight difficulty lurking in the omitted cases. This is not
279 atypical for pen-and-paper proofs, once analysed in detail.%
284 %%% TeX-master: "root"