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: