doc-src/TutorialI/Inductive/document/AB.tex
author nipkow
Tue Oct 17 13:28:57 2000 +0200 (2000-10-17)
changeset 10236 7626cb4e1407
parent 10225 b9fd52525b69
child 10237 875bf54b5d74
permissions -rw-r--r--
*** empty log message ***
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{AB}%
     4 %
     5 \isamarkupsection{A context free grammar}
     6 %
     7 \begin{isamarkuptext}%
     8 Grammars are nothing but shorthands for inductive definitions of nonterminals
     9 which represent sets of strings. For example, the production
    10 $A \to B c$ is short for
    11 \[ w \in B \Longrightarrow wc \in A \]
    12 This section demonstrates this idea with a standard example
    13 \cite[p.\ 81]{HopcroftUllman}, a grammar for generating all words with an
    14 equal number of $a$'s and $b$'s:
    15 \begin{eqnarray}
    16 S &\to& \epsilon \mid b A \mid a B \nonumber\\
    17 A &\to& a S \mid b A A \nonumber\\
    18 B &\to& b S \mid a B B \nonumber
    19 \end{eqnarray}
    20 At the end we say a few words about the relationship of the formalization
    21 and the text in the book~\cite[p.\ 81]{HopcroftUllman}.
    22 
    23 We start by fixing the alpgabet, which consists only of \isa{a}'s
    24 and \isa{b}'s:%
    25 \end{isamarkuptext}%
    26 \isacommand{datatype}\ alfa\ {\isacharequal}\ a\ {\isacharbar}\ b%
    27 \begin{isamarkuptext}%
    28 \noindent
    29 For convenience we includ the following easy lemmas as simplification rules:%
    30 \end{isamarkuptext}%
    31 \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
    32 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ x{\isacharparenright}\isanewline
    33 \isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
    34 \begin{isamarkuptext}%
    35 \noindent
    36 Words over this alphabet are of type \isa{alfa\ list}, and
    37 the three nonterminals are declare as sets of such words:%
    38 \end{isamarkuptext}%
    39 \isacommand{consts}\ S\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline
    40 \ \ \ \ \ \ \ A\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline
    41 \ \ \ \ \ \ \ B\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}%
    42 \begin{isamarkuptext}%
    43 \noindent
    44 The above productions are recast as a \emph{simultaneous} inductive
    45 definition of \isa{S}, \isa{A} and \isa{B}:%
    46 \end{isamarkuptext}%
    47 \isacommand{inductive}\ S\ A\ B\isanewline
    48 \isakeyword{intros}\isanewline
    49 \ \ {\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}\ {\isasymin}\ S{\isachardoublequote}\isanewline
    50 \ \ {\isachardoublequote}w\ {\isasymin}\ A\ {\isasymLongrightarrow}\ b{\isacharhash}w\ {\isasymin}\ S{\isachardoublequote}\isanewline
    51 \ \ {\isachardoublequote}w\ {\isasymin}\ B\ {\isasymLongrightarrow}\ a{\isacharhash}w\ {\isasymin}\ S{\isachardoublequote}\isanewline
    52 \isanewline
    53 \ \ {\isachardoublequote}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ a{\isacharhash}w\ \ \ {\isasymin}\ A{\isachardoublequote}\isanewline
    54 \ \ {\isachardoublequote}{\isasymlbrakk}\ v{\isasymin}A{\isacharsemicolon}\ w{\isasymin}A\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ b{\isacharhash}v{\isacharat}w\ {\isasymin}\ A{\isachardoublequote}\isanewline
    55 \isanewline
    56 \ \ {\isachardoublequote}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ b{\isacharhash}w\ \ \ {\isasymin}\ B{\isachardoublequote}\isanewline
    57 \ \ {\isachardoublequote}{\isasymlbrakk}\ v\ {\isasymin}\ B{\isacharsemicolon}\ w\ {\isasymin}\ B\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ a{\isacharhash}v{\isacharat}w\ {\isasymin}\ B{\isachardoublequote}%
    58 \begin{isamarkuptext}%
    59 \noindent
    60 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
    61 induction, so is this proof: we show at the same time that all words in
    62 \isa{A} contain one more \isa{a} than \isa{b} and all words in \isa{B} contains one more \isa{b} than \isa{a}.%
    63 \end{isamarkuptext}%
    64 \isacommand{lemma}\ correctness{\isacharcolon}\isanewline
    65 \ \ {\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
    66 \ \ \ \ {\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
    67 \ \ \ \ {\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}%
    68 \begin{isamarkuptxt}%
    69 \noindent
    70 These propositions are expressed with the help of the predefined \isa{filter} function on lists, which has the convenient syntax \isa{filter\ P\ xs}, the list of all elements \isa{x} in \isa{xs} such that \isa{P\ x}
    71 holds. The length of a list is usually written \isa{size}, and \isa{size} is merely a shorthand.
    72 
    73 The proof itself is by rule induction and afterwards automatic:%
    74 \end{isamarkuptxt}%
    75 \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharparenright}\isanewline
    76 \isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
    77 \begin{isamarkuptext}%
    78 \noindent
    79 This may seem surprising at first, and is indeed an indication of the power
    80 of inductive definitions. But it is also quite straightforward. For example,
    81 consider the production $A \to b A A$: if $v,w \in A$ and the elements of $A$
    82 contain one more $a$ than $b$'s, then $bvw$ must again contain one more $a$
    83 than $b$'s.
    84 
    85 As usual, the correctness of syntactic descriptions is easy, but completeness
    86 is hard: does \isa{S} contain \emph{all} words with an equal number of
    87 \isa{a}'s and \isa{b}'s? It turns out that this proof requires the
    88 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
    89 \isa{b}. This is best seen by imagining counting the difference between the
    90 number of \isa{a}'s than \isa{b}'s starting at the left end of the
    91 word. We start at 0 and end (at the right end) with 2. Since each move to the
    92 right increases or decreases the difference by 1, we must have passed through
    93 1 on our way from 0 to 2. Formally, we appeal to the following discrete
    94 intermediate value theorem \isa{nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val}
    95 \begin{isabelle}%
    96 \ \ \ \ \ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ i\ {\isacharless}\ n\ {\isasymlongrightarrow}\ abs\ {\isacharparenleft}f\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isacharparenright}\ {\isasymle}\ {\isacharhash}{\isadigit{1}}{\isacharsemicolon}\ f\ {\isadigit{0}}\ {\isasymle}\ k{\isacharsemicolon}\ k\ {\isasymle}\ f\ n{\isasymrbrakk}\isanewline
    97 \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ i\ {\isasymle}\ n\ {\isasymand}\ f\ i\ {\isacharequal}\ k%
    98 \end{isabelle}
    99 where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers,
   100 \isa{abs} is the absolute value function, and \isa{{\isacharhash}{\isadigit{1}}} is the
   101 integer 1 (see \S\ref{sec:int}).
   102 
   103 First we show that the our specific function, the difference between the
   104 numbers of \isa{a}'s and \isa{b}'s, does indeed only change by 1 in every
   105 move to the right. At this point we also start generalizing from \isa{a}'s
   106 and \isa{b}'s to an arbitrary property \isa{P}. Otherwise we would have
   107 to prove the desired lemma twice, once as stated above and once with the
   108 roles of \isa{a}'s and \isa{b}'s interchanged.%
   109 \end{isamarkuptext}%
   110 \isacommand{lemma}\ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i\ {\isacharless}\ size\ w{\isachardot}\isanewline
   111 \ \ abs{\isacharparenleft}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ \ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\isanewline
   112 \ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline
   113 \ \ \ \ \ \ {\isacharminus}\isanewline
   114 \ \ \ \ \ \ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ \ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\isanewline
   115 \ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharless}{\isacharequal}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}%
   116 \begin{isamarkuptxt}%
   117 \noindent
   118 The lemma is a bit hard to read because of the coercion function
   119 \isa{{\isachardoublequote}int{\isacharcolon}{\isacharcolon}nat\ {\isasymRightarrow}\ int{\isachardoublequote}}. It is required because \isa{size} returns
   120 a natural number, but \isa{{\isacharminus}} on \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 als need \isa{drop\ i\ xs}, which
   123 is what remains after that prefix has been dropped from \isa{xs}.
   124 
   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
   127 discuss it.%
   128 \end{isamarkuptxt}%
   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 a word with two
   134 more elements of one sort than of the other sort into two halfs:%
   135 \end{isamarkuptext}%
   136 \isacommand{lemma}\ part{\isadigit{1}}{\isacharcolon}\isanewline
   137 \ {\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
   138 \ \ {\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}%
   139 \begin{isamarkuptxt}%
   140 \noindent
   141 This is proved with the help of the intermediate value theorem, instantiated
   142 appropriately and with its first premise disposed of by lemma
   143 \isa{step{\isadigit{1}}}.%
   144 \end{isamarkuptxt}%
   145 \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
   146 \isacommand{apply}\ simp\isanewline
   147 \isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}int{\isacharunderscore}Suc\ add{\isacharcolon}zdiff{\isacharunderscore}eq{\isacharunderscore}eq\ sym{\isacharbrackleft}OF\ int{\isacharunderscore}Suc{\isacharbrackright}{\isacharparenright}%
   148 \begin{isamarkuptext}%
   149 \noindent
   150 The additional lemmas are needed to mediate between \isa{nat} and \isa{int}.
   151 
   152 Lemma \isa{part{\isadigit{1}}} tells us only about the prefix \isa{take\ i\ w}.
   153 The suffix \isa{drop\ i\ w} is dealt with in the following easy lemma:%
   154 \end{isamarkuptext}%
   155 \isacommand{lemma}\ part{\isadigit{2}}{\isacharcolon}\isanewline
   156 \ \ {\isachardoublequote}{\isasymlbrakk}size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\isanewline
   157 \ \ \ \ size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}{\isacharsemicolon}\isanewline
   158 \ \ \ \ 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
   159 \ \ \ {\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
   160 \isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharparenright}%
   161 \begin{isamarkuptext}%
   162 \noindent
   163 Lemma \isa{append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id}, \isa{take\ n\ xs\ {\isacharat}\ drop\ n\ xs\ {\isacharequal}\ xs},
   164 which is generally useful, needs to be disabled for once.
   165 
   166 To dispose of trivial cases automatically, the rules of the inductive
   167 definition are declared simplification rules:%
   168 \end{isamarkuptext}%
   169 \isacommand{declare}\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharbrackleft}simp{\isacharbrackright}%
   170 \begin{isamarkuptext}%
   171 \noindent
   172 This could have been done earlier but was not necessary so far.
   173 
   174 The completeness theorem tells us that if a word has the same number of
   175 \isa{a}'s and \isa{b}'s, then it is in \isa{S}, and similarly and
   176 simultaneously for \isa{A} and \isa{B}:%
   177 \end{isamarkuptext}%
   178 \isacommand{theorem}\ completeness{\isacharcolon}\isanewline
   179 \ \ {\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
   180 \ \ \ \ {\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
   181 \ \ \ \ {\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}%
   182 \begin{isamarkuptxt}%
   183 \noindent
   184 The proof is by induction on \isa{w}. Structural induction would fail here
   185 because, as we can see from the grammar, we need to make bigger steps than
   186 merely appending a single letter at the front. Hence we induct on the length
   187 of \isa{w}, using the induction rule \isa{length{\isacharunderscore}induct}:%
   188 \end{isamarkuptxt}%
   189 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}%
   190 \begin{isamarkuptxt}%
   191 \noindent
   192 The \isa{rule} parameter tells \isa{induct{\isacharunderscore}tac} explicitly which induction
   193 rule to use. For details see \S\ref{sec:complete-ind} below.
   194 In this case the result is that we may assume the lemma already
   195 holds for all words shorter than \isa{w}.
   196 
   197 The proof continues with a case distinction on \isa{w},
   198 i.e.\ if \isa{w} is empty or not.%
   199 \end{isamarkuptxt}%
   200 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ w{\isacharparenright}\isanewline
   201 \ \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}%
   202 \begin{isamarkuptxt}%
   203 \noindent
   204 Simplification disposes of the base case and leaves only two step
   205 cases to be proved:
   206 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
   207 \isa{b\ {\isacharhash}\ v\ {\isasymin}\ A}, and similarly for \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v}.
   208 We only consider the first case in detail.
   209 
   210 After breaking the conjuction up into two cases, we can apply
   211 \isa{part{\isadigit{1}}} to the assumption that \isa{w} contains two more \isa{a}'s than \isa{b}'s.%
   212 \end{isamarkuptxt}%
   213 \isacommand{apply}{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline
   214 \ \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
   215 \ \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
   216 \ \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
   217 \ \isacommand{apply}{\isacharparenleft}erule\ conjE{\isacharparenright}%
   218 \begin{isamarkuptxt}%
   219 \noindent
   220 This yields an index \isa{i\ {\isasymle}\ length\ v} such that
   221 \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}}}.
   222 With the help of \isa{part{\isadigit{1}}} it follows that
   223 \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}}}.%
   224 \end{isamarkuptxt}%
   225 \ \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
   226 \ \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}%
   227 \begin{isamarkuptxt}%
   228 \noindent
   229 Now it is time to decompose \isa{v} in the conclusion \isa{b\ {\isacharhash}\ v\ {\isasymin}\ A}
   230 into \isa{take\ i\ v\ {\isacharat}\ drop\ i\ v},
   231 after which the appropriate rule of the grammar reduces the goal
   232 to the two subgoals \isa{take\ i\ v\ {\isasymin}\ A} and \isa{drop\ i\ v\ {\isasymin}\ A}:%
   233 \end{isamarkuptxt}%
   234 \ \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
   235 \ \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}%
   236 \begin{isamarkuptxt}%
   237 \noindent
   238 Both subgoals follow from the induction hypothesis because both \isa{take\ i\ v} and \isa{drop\ i\ v} are shorter than \isa{w}:%
   239 \end{isamarkuptxt}%
   240 \ \ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline
   241 \ \isacommand{apply}{\isacharparenleft}force\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}%
   242 \begin{isamarkuptxt}%
   243 \noindent
   244 Note that the variables \isa{n{\isadigit{1}}} and \isa{t} referred to in the
   245 substitution step above come from the derived theorem \isa{subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}}.
   246 
   247 The case \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v} is proved completely analogously:%
   248 \end{isamarkuptxt}%
   249 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
   250 \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
   251 \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
   252 \isacommand{apply}{\isacharparenleft}erule\ conjE{\isacharparenright}\isanewline
   253 \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
   254 \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline
   255 \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
   256 \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isanewline
   257 \ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline
   258 \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}%
   259 \begin{isamarkuptext}%
   260 We conclude this section with a comparison of the above proof and the one
   261 in the textbook \cite[p.\ 81]{HopcroftUllman}. For a start, the texbook
   262 grammar, for no good reason, excludes the empty word, which complicates
   263 matters just a little bit because we now have 8 instead of our 7 productions.
   264 
   265 More importantly, the proof itself is different: rather than separating the
   266 two directions, they perform one induction on the length of a word. This
   267 deprives them of the beauty of rule induction and in the easy direction
   268 (correctness) their reasoning is more detailed than our \isa{auto}. For the
   269 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
   270 about the remaining cases: ``We do this in a manner similar to our method of
   271 proof for part (1); this part is left to the reader''. But this is precisely
   272 the part that requires the intermediate value theorem and thus is not at all
   273 similar to the other cases (which are automatic in Isabelle). We conclude
   274 that the authors are at least cavalier about this point and may even have
   275 overlooked the slight difficulty lurking in the omitted cases. This is not
   276 atypical for pen-and-paper proofs, once analysed in detail.%
   277 \end{isamarkuptext}%
   278 \end{isabellebody}%
   279 %%% Local Variables:
   280 %%% mode: latex
   281 %%% TeX-master: "root"
   282 %%% End: