
nipkow@10217: %
nipkow@10217: \begin{isabellebody}%
nipkow@10217: \def\isabellecontext{AB}%
nipkow@10225: %
wenzelm@10395: \isamarkupsection{Case study: A context free grammar%
wenzelm@10395: }
nipkow@10236: %
nipkow@10236: \begin{isamarkuptext}%
nipkow@10242: \label{sec:CFG}
nipkow@10236: Grammars are nothing but shorthands for inductive definitions of nonterminals
nipkow@10236: which represent sets of strings. For example, the production
nipkow@10236: $A \to B c$ is short for
nipkow@10236: \[ w \in B \Longrightarrow wc \in A \]
nipkow@10236: This section demonstrates this idea with a standard example
nipkow@10236: \cite[p.\ 81]{HopcroftUllman}, a grammar for generating all words with an
nipkow@10236: equal number of $a$'s and $b$'s:
nipkow@10236: \begin{eqnarray}
nipkow@10236: S &\to& \epsilon \mid b A \mid a B \nonumber\\
nipkow@10236: A &\to& a S \mid b A A \nonumber\\
nipkow@10236: B &\to& b S \mid a B B \nonumber
nipkow@10236: \end{eqnarray}
nipkow@10236: At the end we say a few words about the relationship of the formalization
nipkow@10236: and the text in the book~\cite[p.\ 81]{HopcroftUllman}.
nipkow@10236: 
paulson@10299: We start by fixing the alphabet, which consists only of \isa{a}'s
nipkow@10236: and \isa{b}'s:%
nipkow@10236: \end{isamarkuptext}%
nipkow@10236: \isacommand{datatype}\ alfa\ {\isacharequal}\ a\ {\isacharbar}\ b%
nipkow@10236: \begin{isamarkuptext}%
nipkow@10236: \noindent
paulson@10299: For convenience we include the following easy lemmas as simplification rules:%
nipkow@10236: \end{isamarkuptext}%
nipkow@10236: \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: \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ x{\isacharparenright}\isanewline
nipkow@10236: \isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
nipkow@10236: \begin{isamarkuptext}%
nipkow@10236: \noindent
nipkow@10236: Words over this alphabet are of type \isa{alfa\ list}, and
nipkow@10236: the three nonterminals are declare as sets of such words:%
nipkow@10236: \end{isamarkuptext}%
nipkow@10217: \isacommand{consts}\ S\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline
nipkow@10217: \ \ \ \ \ \ \ A\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline
nipkow@10236: \ \ \ \ \ \ \ B\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}%
nipkow@10236: \begin{isamarkuptext}%
nipkow@10236: \noindent
nipkow@10236: The above productions are recast as a \emph{simultaneous} inductive
nipkow@10242: definition\index{inductive definition!simultaneous}
nipkow@10242: of \isa{S}, \isa{A} and \isa{B}:%
nipkow@10236: \end{isamarkuptext}%
nipkow@10217: \isacommand{inductive}\ S\ A\ B\isanewline
nipkow@10217: \isakeyword{intros}\isanewline
nipkow@10236: \ \ {\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}\ {\isasymin}\ S{\isachardoublequote}\isanewline
nipkow@10236: \ \ {\isachardoublequote}w\ {\isasymin}\ A\ {\isasymLongrightarrow}\ b{\isacharhash}w\ {\isasymin}\ S{\isachardoublequote}\isanewline
nipkow@10236: \ \ {\isachardoublequote}w\ {\isasymin}\ B\ {\isasymLongrightarrow}\ a{\isacharhash}w\ {\isasymin}\ S{\isachardoublequote}\isanewline
nipkow@10217: \isanewline
nipkow@10236: \ \ {\isachardoublequote}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ a{\isacharhash}w\ \ \ {\isasymin}\ A{\isachardoublequote}\isanewline
nipkow@10236: \ \ {\isachardoublequote}{\isasymlbrakk}\ v{\isasymin}A{\isacharsemicolon}\ w{\isasymin}A\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ b{\isacharhash}v{\isacharat}w\ {\isasymin}\ A{\isachardoublequote}\isanewline
nipkow@10217: \isanewline
nipkow@10236: \ \ {\isachardoublequote}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ b{\isacharhash}w\ \ \ {\isasymin}\ B{\isachardoublequote}\isanewline
nipkow@10236: \ \ {\isachardoublequote}{\isasymlbrakk}\ v\ {\isasymin}\ B{\isacharsemicolon}\ w\ {\isasymin}\ B\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ a{\isacharhash}v{\isacharat}w\ {\isasymin}\ B{\isachardoublequote}%
nipkow@10236: \begin{isamarkuptext}%
nipkow@10236: \noindent
nipkow@10236: 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: induction, so is this proof: we show at the same time that all words in
nipkow@10236: \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: \end{isamarkuptext}%
nipkow@10236: \isacommand{lemma}\ correctness{\isacharcolon}\isanewline
nipkow@10236: \ \ {\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: \ \ \ {\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: \ \ \ {\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: \begin{isamarkuptxt}%
nipkow@10236: \noindent
nipkow@10283: 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: holds. Remember that on lists \isa{size} and \isa{size} are synonymous.
nipkow@10236: 
nipkow@10236: The proof itself is by rule induction and afterwards automatic:%
nipkow@10236: \end{isamarkuptxt}%
nipkow@10217: \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharparenright}\isanewline
nipkow@10236: \isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
nipkow@10236: \begin{isamarkuptext}%
nipkow@10236: \noindent
nipkow@10236: This may seem surprising at first, and is indeed an indication of the power
nipkow@10236: of inductive definitions. But it is also quite straightforward. For example,
nipkow@10236: consider the production $A \to b A A$: if $v,w \in A$ and the elements of $A$
nipkow@10236: contain one more $a$ than $b$'s, then $bvw$ must again contain one more $a$
nipkow@10236: than $b$'s.
nipkow@10236: 
nipkow@10236: As usual, the correctness of syntactic descriptions is easy, but completeness
nipkow@10236: is hard: does \isa{S} contain \emph{all} words with an equal number of
nipkow@10236: \isa{a}'s and \isa{b}'s? It turns out that this proof requires the
nipkow@10236: 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: \isa{b}. This is best seen by imagining counting the difference between the
nipkow@10283: number of \isa{a}'s and \isa{b}'s starting at the left end of the
nipkow@10283: word. We start with 0 and end (at the right end) with 2. Since each move to the
nipkow@10236: right increases or decreases the difference by 1, we must have passed through
nipkow@10236: 1 on our way from 0 to 2. Formally, we appeal to the following discrete
nipkow@10236: intermediate value theorem \isa{nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val}
nipkow@10236: \begin{isabelle}%
nipkow@10236: \ \ \ \ \ {\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
nipkow@10236: \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ i\ {\isasymle}\ n\ {\isasymand}\ f\ i\ {\isacharequal}\ k%
nipkow@10236: \end{isabelle}
nipkow@10236: where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers,
nipkow@10236: \isa{abs} is the absolute value function, and \isa{{\isacharhash}{\isadigit{1}}} is the
nipkow@10420: integer 1 (see \S\ref{sec:numbers}).
nipkow@10236: 
nipkow@10236: First we show that the our specific function, the difference between the
nipkow@10236: numbers of \isa{a}'s and \isa{b}'s, does indeed only change by 1 in every
nipkow@10236: move to the right. At this point we also start generalizing from \isa{a}'s
nipkow@10236: and \isa{b}'s to an arbitrary property \isa{P}. Otherwise we would have
nipkow@10236: to prove the desired lemma twice, once as stated above and once with the
nipkow@10236: roles of \isa{a}'s and \isa{b}'s interchanged.%
nipkow@10236: \end{isamarkuptext}%
nipkow@10236: \isacommand{lemma}\ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i\ {\isacharless}\ size\ w{\isachardot}\isanewline
nipkow@10236: \ \ abs{\isacharparenleft}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ \ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\isanewline
nipkow@10236: \ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline
nipkow@10236: \ \ \ \ \ \ {\isacharminus}\isanewline
nipkow@10236: \ \ \ \ \ \ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ \ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\isanewline
nipkow@10420: \ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymle}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}%
nipkow@10236: \begin{isamarkuptxt}%
nipkow@10236: \noindent
nipkow@10236: The lemma is a bit hard to read because of the coercion function
nipkow@10236: \isa{{\isachardoublequote}int{\isacharcolon}{\isacharcolon}nat\ {\isasymRightarrow}\ int{\isachardoublequote}}. It is required because \isa{size} returns
nipkow@10236: a natural number, but \isa{{\isacharminus}} on \isa{nat} will do the wrong thing.
nipkow@10236: Function \isa{take} is predefined and \isa{take\ i\ xs} is the prefix of
nipkow@10236: length \isa{i} of \isa{xs}; below we als need \isa{drop\ i\ xs}, which
nipkow@10236: is what remains after that prefix has been dropped from \isa{xs}.
nipkow@10236: 
nipkow@10236: The proof is by induction on \isa{w}, with a trivial base case, and a not
nipkow@10236: so trivial induction step. Since it is essentially just arithmetic, we do not
nipkow@10236: discuss it.%
nipkow@10236: \end{isamarkuptxt}%
nipkow@10217: \isacommand{apply}{\isacharparenleft}induct\ w{\isacharparenright}\isanewline
nipkow@10217: \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
nipkow@10236: \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}zabs{\isacharunderscore}def\ take{\isacharunderscore}Cons\ split{\isacharcolon}nat{\isachardot}split\ if{\isacharunderscore}splits{\isacharparenright}%
nipkow@10236: \begin{isamarkuptext}%
nipkow@10236: Finally we come to the above mentioned lemma about cutting a word with two
nipkow@10283: more elements of one sort than of the other sort into two halves:%
nipkow@10236: \end{isamarkuptext}%
nipkow@10236: \isacommand{lemma}\ part{\isadigit{1}}{\isacharcolon}\isanewline
nipkow@10236: \ {\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: \ \ {\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: \begin{isamarkuptxt}%
nipkow@10236: \noindent
nipkow@10236: This is proved with the help of the intermediate value theorem, instantiated
nipkow@10236: appropriately and with its first premise disposed of by lemma
nipkow@10236: \isa{step{\isadigit{1}}}.%
nipkow@10236: \end{isamarkuptxt}%
nipkow@10236: \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@10236: \isacommand{apply}\ simp\isanewline
nipkow@10236: \isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}int{\isacharunderscore}Suc\ add{\isacharcolon}zdiff{\isacharunderscore}eq{\isacharunderscore}eq\ sym{\isacharbrackleft}OF\ int{\isacharunderscore}Suc{\isacharbrackright}{\isacharparenright}%
nipkow@10236: \begin{isamarkuptext}%
nipkow@10236: \noindent
nipkow@10236: The additional lemmas are needed to mediate between \isa{nat} and \isa{int}.
nipkow@10236: 
nipkow@10236: Lemma \isa{part{\isadigit{1}}} tells us only about the prefix \isa{take\ i\ w}.
nipkow@10236: The suffix \isa{drop\ i\ w} is dealt with in the following easy lemma:%
nipkow@10236: \end{isamarkuptext}%
nipkow@10236: \isacommand{lemma}\ part{\isadigit{2}}{\isacharcolon}\isanewline
nipkow@10236: \ \ {\isachardoublequote}{\isasymlbrakk}size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\isanewline
nipkow@10236: \ \ \ \ size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}{\isacharsemicolon}\isanewline
nipkow@10236: \ \ \ \ 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: \ \ \ {\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: \isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharparenright}%
nipkow@10236: \begin{isamarkuptext}%
nipkow@10236: \noindent
nipkow@10236: Lemma \isa{append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id}, \isa{take\ n\ xs\ {\isacharat}\ drop\ n\ xs\ {\isacharequal}\ xs},
nipkow@10236: which is generally useful, needs to be disabled for once.
nipkow@10236: 
nipkow@10236: To dispose of trivial cases automatically, the rules of the inductive
nipkow@10236: definition are declared simplification rules:%
nipkow@10236: \end{isamarkuptext}%
nipkow@10236: \isacommand{declare}\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharbrackleft}simp{\isacharbrackright}%
nipkow@10236: \begin{isamarkuptext}%
nipkow@10236: \noindent
nipkow@10236: This could have been done earlier but was not necessary so far.
nipkow@10236: 
nipkow@10236: The completeness theorem tells us that if a word has the same number of
nipkow@10236: \isa{a}'s and \isa{b}'s, then it is in \isa{S}, and similarly and
nipkow@10236: simultaneously for \isa{A} and \isa{B}:%
nipkow@10236: \end{isamarkuptext}%
nipkow@10236: \isacommand{theorem}\ completeness{\isacharcolon}\isanewline
nipkow@10236: \ \ {\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: \ \ \ {\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: \ \ \ {\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: \begin{isamarkuptxt}%
nipkow@10236: \noindent
nipkow@10236: The proof is by induction on \isa{w}. Structural induction would fail here
nipkow@10236: because, as we can see from the grammar, we need to make bigger steps than
nipkow@10236: merely appending a single letter at the front. Hence we induct on the length
nipkow@10236: of \isa{w}, using the induction rule \isa{length{\isacharunderscore}induct}:%
nipkow@10236: \end{isamarkuptxt}%
nipkow@10236: \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}%
nipkow@10236: \begin{isamarkuptxt}%
nipkow@10236: \noindent
nipkow@10236: The \isa{rule} parameter tells \isa{induct{\isacharunderscore}tac} explicitly which induction
nipkow@10236: rule to use. For details see \S\ref{sec:complete-ind} below.
nipkow@10236: In this case the result is that we may assume the lemma already
nipkow@10236: holds for all words shorter than \isa{w}.
nipkow@10236: 
nipkow@10236: The proof continues with a case distinction on \isa{w},
nipkow@10236: i.e.\ if \isa{w} is empty or not.%
nipkow@10236: \end{isamarkuptxt}%
nipkow@10236: \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ w{\isacharparenright}\isanewline
nipkow@10236: \ \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}%
nipkow@10236: \begin{isamarkuptxt}%
nipkow@10236: \noindent
nipkow@10236: Simplification disposes of the base case and leaves only two step
nipkow@10236: cases to be proved:
nipkow@10236: 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: \isa{b\ {\isacharhash}\ v\ {\isasymin}\ A}, and similarly for \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v}.
nipkow@10236: We only consider the first case in detail.
nipkow@10236: 
nipkow@10236: After breaking the conjuction up into two cases, we can apply
nipkow@10236: \isa{part{\isadigit{1}}} to the assumption that \isa{w} contains two more \isa{a}'s than \isa{b}'s.%
nipkow@10236: \end{isamarkuptxt}%
nipkow@10217: \isacommand{apply}{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline
nipkow@10217: \ \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
nipkow@10236: \ \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
nipkow@10236: \ \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
nipkow@10236: \ \isacommand{apply}{\isacharparenleft}erule\ conjE{\isacharparenright}%
nipkow@10236: \begin{isamarkuptxt}%
nipkow@10236: \noindent
nipkow@10236: This yields an index \isa{i\ {\isasymle}\ length\ v} such that
nipkow@10236: \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: With the help of \isa{part{\isadigit{1}}} it follows that
nipkow@10236: \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: \end{isamarkuptxt}%
nipkow@10236: \ \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
nipkow@10236: \ \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}%
nipkow@10236: \begin{isamarkuptxt}%
nipkow@10236: \noindent
nipkow@10236: Now it is time to decompose \isa{v} in the conclusion \isa{b\ {\isacharhash}\ v\ {\isasymin}\ A}
nipkow@10236: into \isa{take\ i\ v\ {\isacharat}\ drop\ i\ v},
nipkow@10236: after which the appropriate rule of the grammar reduces the goal
nipkow@10236: to the two subgoals \isa{take\ i\ v\ {\isasymin}\ A} and \isa{drop\ i\ v\ {\isasymin}\ A}:%
nipkow@10236: \end{isamarkuptxt}%
nipkow@10236: \ \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: \ \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}%
nipkow@10236: \begin{isamarkuptxt}%
nipkow@10236: \noindent
nipkow@10236: 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: \end{isamarkuptxt}%
nipkow@10236: \ \ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline
nipkow@10236: \ \isacommand{apply}{\isacharparenleft}force\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}%
nipkow@10236: \begin{isamarkuptxt}%
nipkow@10236: \noindent
nipkow@10236: Note that the variables \isa{n{\isadigit{1}}} and \isa{t} referred to in the
nipkow@10236: substitution step above come from the derived theorem \isa{subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}}.
nipkow@10236: 
nipkow@10236: The case \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v} is proved completely analogously:%
nipkow@10236: \end{isamarkuptxt}%
nipkow@10217: \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
nipkow@10236: \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
nipkow@10217: \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
nipkow@10217: \isacommand{apply}{\isacharparenleft}erule\ conjE{\isacharparenright}\isanewline
nipkow@10236: \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
nipkow@10217: \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline
nipkow@10236: \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: \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isanewline
nipkow@10217: \ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline
nipkow@10236: \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: \begin{isamarkuptext}%
nipkow@10236: We conclude this section with a comparison of the above proof and the one
nipkow@10236: in the textbook \cite[p.\ 81]{HopcroftUllman}. For a start, the texbook
nipkow@10236: grammar, for no good reason, excludes the empty word, which complicates
nipkow@10236: matters just a little bit because we now have 8 instead of our 7 productions.
nipkow@10236: 
nipkow@10236: More importantly, the proof itself is different: rather than separating the
nipkow@10236: two directions, they perform one induction on the length of a word. This
nipkow@10236: deprives them of the beauty of rule induction and in the easy direction
nipkow@10236: (correctness) their reasoning is more detailed than our \isa{auto}. For the
nipkow@10236: 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: about the remaining cases: ``We do this in a manner similar to our method of
nipkow@10236: proof for part (1); this part is left to the reader''. But this is precisely
nipkow@10236: the part that requires the intermediate value theorem and thus is not at all
nipkow@10236: similar to the other cases (which are automatic in Isabelle). We conclude
nipkow@10236: that the authors are at least cavalier about this point and may even have
nipkow@10236: overlooked the slight difficulty lurking in the omitted cases. This is not
nipkow@10396: atypical for pencil-and-paper proofs, once analysed in detail.%
nipkow@10236: \end{isamarkuptext}%
nipkow@10217: \end{isabellebody}%
nipkow@10217: %%% Local Variables:
nipkow@10217: %%% mode: latex
nipkow@10217: %%% TeX-master: "root"
nipkow@10217: %%% End:




