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: