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