doc-src/TutorialI/Inductive/document/AB.tex
author nipkow
Sun Nov 26 10:48:38 2000 +0100 (2000-11-26)
changeset 10520 bb9dfcc87951
parent 10512 d34192966cd8
child 10589 b2d1b393b750
permissions -rw-r--r--
*** empty log message ***
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{AB}%
     4 %
     5 \isamarkupsection{Case study: A context free grammar%
     6 }
     7 %
     8 \begin{isamarkuptext}%
     9 \label{sec:CFG}
    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:
    17 \begin{eqnarray}
    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
    21 \end{eqnarray}
    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}.
    24 
    25 We start by fixing the alphabet, which consists only of \isa{a}'s
    26 and \isa{b}'s:%
    27 \end{isamarkuptext}%
    28 \isacommand{datatype}\ alfa\ {\isacharequal}\ a\ {\isacharbar}\ b%
    29 \begin{isamarkuptext}%
    30 \noindent
    31 For convenience we include the following easy lemmas as simplification rules:%
    32 \end{isamarkuptext}%
    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}%
    37 \noindent
    38 Words over this alphabet are of type \isa{alfa\ list}, and
    39 the three nonterminals are declare as sets of such words:%
    40 \end{isamarkuptext}%
    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}%
    45 \noindent
    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}:%
    49 \end{isamarkuptext}%
    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
    55 \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
    58 \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}%
    62 \noindent
    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}.%
    66 \end{isamarkuptext}%
    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}%
    71 \begin{isamarkuptxt}%
    72 \noindent
    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.
    75 
    76 The proof itself is by rule induction and afterwards automatic:%
    77 \end{isamarkuptxt}%
    78 \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharparenright}\isanewline
    79 \isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
    80 \begin{isamarkuptext}%
    81 \noindent
    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$
    86 than $b$'s.
    87 
    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}
    98 \begin{isabelle}%
    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%
   101 \end{isabelle}
   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}).
   105 
   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.%
   112 \end{isamarkuptext}%
   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}%
   120 \noindent
   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}.
   127 
   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
   130 discuss it.%
   131 \end{isamarkuptxt}%
   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:%
   138 \end{isamarkuptext}%
   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}%
   143 \noindent
   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}}}.%
   147 \end{isamarkuptxt}%
   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}%
   152 \noindent
   153 The additional lemmas are needed to mediate between \isa{nat} and \isa{int}.
   154 
   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:%
   157 \end{isamarkuptext}%
   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}%
   165 \noindent
   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.
   168 
   169 To dispose of trivial cases automatically, the rules of the inductive
   170 definition are declared simplification rules:%
   171 \end{isamarkuptext}%
   172 \isacommand{declare}\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharbrackleft}simp{\isacharbrackright}%
   173 \begin{isamarkuptext}%
   174 \noindent
   175 This could have been done earlier but was not necessary so far.
   176 
   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}:%
   180 \end{isamarkuptext}%
   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}%
   186 \noindent
   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}:%
   191 \end{isamarkuptxt}%
   192 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}%
   193 \begin{isamarkuptxt}%
   194 \noindent
   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}.
   199 
   200 The proof continues with a case distinction on \isa{w},
   201 i.e.\ if \isa{w} is empty or not.%
   202 \end{isamarkuptxt}%
   203 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ w{\isacharparenright}\isanewline
   204 \ \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}%
   205 \begin{isamarkuptxt}%
   206 \noindent
   207 Simplification disposes of the base case and leaves only two step
   208 cases to be proved:
   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.
   212 
   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.%
   215 \end{isamarkuptxt}%
   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}%
   222 \noindent
   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}}}.%
   227 \end{isamarkuptxt}%
   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}%
   231 \noindent
   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}:%
   236 \end{isamarkuptxt}%
   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}%
   240 \noindent
   241 Both subgoals follow from the induction hypothesis because both \isa{take\ i\ v} and \isa{drop\ i\ v} are shorter than \isa{w}:%
   242 \end{isamarkuptxt}%
   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}%
   246 \noindent
   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}}.
   249 
   250 The case \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v} is proved completely analogously:%
   251 \end{isamarkuptxt}%
   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.
   267 
   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.%
   280 \end{isamarkuptext}%
   281 \end{isabellebody}%
   282 %%% Local Variables:
   283 %%% mode: latex
   284 %%% TeX-master: "root"
   285 %%% End: