--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/document/AB.tex Thu Jul 26 17:16:02 2012 +0200
@@ -0,0 +1,462 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{AB}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupsection{Case Study: A Context Free Grammar%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\label{sec:CFG}
+\index{grammars!defining inductively|(}%
+Grammars are nothing but shorthands for inductive definitions of nonterminals
+which represent sets of strings. For example, the production
+$A \to B c$ is short for
+\[ w \in B \Longrightarrow wc \in A \]
+This section demonstrates this idea with an example
+due to Hopcroft and Ullman, a grammar for generating all words with an
+equal number of $a$'s and~$b$'s:
+\begin{eqnarray}
+S &\to& \epsilon \mid b A \mid a B \nonumber\\
+A &\to& a S \mid b A A \nonumber\\
+B &\to& b S \mid a B B \nonumber
+\end{eqnarray}
+At the end we say a few words about the relationship between
+the original proof \cite[p.\ts81]{HopcroftUllman} and our formal version.
+
+We start by fixing the alphabet, which consists only of \isa{a}'s
+and~\isa{b}'s:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{datatype}\isamarkupfalse%
+\ alfa\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{7C}{\isacharbar}}\ b%
+\begin{isamarkuptext}%
+\noindent
+For convenience we include the following easy lemmas as simplification rules:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}case{\isaliteral{5F}{\isacharunderscore}}tac\ x{\isaliteral{2C}{\isacharcomma}}\ auto{\isaliteral{29}{\isacharparenright}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent
+Words over this alphabet are of type \isa{alfa\ list}, and
+the three nonterminals are declared as sets of such words.
+The productions above are recast as a \emph{mutual} inductive
+definition\index{inductive definition!simultaneous}
+of \isa{S}, \isa{A} and~\isa{B}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse%
+\isanewline
+\ \ S\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}alfa\ list\ set{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline
+\ \ A\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}alfa\ list\ set{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline
+\ \ B\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}alfa\ list\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isakeyword{where}\isanewline
+\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ S{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ b{\isaliteral{23}{\isacharhash}}w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ S{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a{\isaliteral{23}{\isacharhash}}w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ S{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isanewline
+{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ S\ \ \ \ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a{\isaliteral{23}{\isacharhash}}w\ \ \ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ v{\isaliteral{5C3C696E3E}{\isasymin}}A{\isaliteral{3B}{\isacharsemicolon}}\ w{\isaliteral{5C3C696E3E}{\isasymin}}A\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ b{\isaliteral{23}{\isacharhash}}v{\isaliteral{40}{\isacharat}}w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isanewline
+{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ S\ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ b{\isaliteral{23}{\isacharhash}}w\ \ \ {\isaliteral{5C3C696E3E}{\isasymin}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ v\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B{\isaliteral{3B}{\isacharsemicolon}}\ w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a{\isaliteral{23}{\isacharhash}}v{\isaliteral{40}{\isacharat}}w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+\noindent
+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 mutual
+induction, so is the proof: we show at the same time that all words in
+\isa{A} contain one more \isa{a} than \isa{b} and all words in \isa{B} contain one more \isa{b} than \isa{a}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ correctness{\isaliteral{3A}{\isacharcolon}}\isanewline
+\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ S\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}w{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}a{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}w{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}b{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ \ \ \ \ {\isaliteral{5C3C616E643E}{\isasymand}}\isanewline
+\ \ \ {\isaliteral{28}{\isacharparenleft}}w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}w{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}a{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}w{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}b{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\isanewline
+\ \ \ {\isaliteral{28}{\isacharparenleft}}w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}w{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}b{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}w{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}a{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+\noindent
+These propositions are expressed with the help of the predefined \isa{filter} function on lists, which has the convenient syntax \isa{{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}xs{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{5D}{\isacharbrackright}}}, the list of all elements \isa{x} in \isa{xs} such that \isa{P\ x}
+holds. Remember that on lists \isa{size} and \isa{length} are synonymous.
+
+The proof itself is by rule induction and afterwards automatic:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}rule\ S{\isaliteral{5F}{\isacharunderscore}}A{\isaliteral{5F}{\isacharunderscore}}B{\isaliteral{2E}{\isachardot}}induct{\isaliteral{2C}{\isacharcomma}}\ auto{\isaliteral{29}{\isacharparenright}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent
+This may seem surprising at first, and is indeed an indication of the power
+of inductive definitions. But it is also quite straightforward. For example,
+consider the production $A \to b A A$: if $v,w \in A$ and the elements of $A$
+contain one more $a$ than~$b$'s, then $bvw$ must again contain one more $a$
+than~$b$'s.
+
+As usual, the correctness of syntactic descriptions is easy, but completeness
+is hard: does \isa{S} contain \emph{all} words with an equal number of
+\isa{a}'s and \isa{b}'s? It turns out that this proof requires the
+following lemma: every string with two more \isa{a}'s than \isa{b}'s can be cut somewhere such that each half has one more \isa{a} than
+\isa{b}. This is best seen by imagining counting the difference between the
+number of \isa{a}'s and \isa{b}'s starting at the left end of the
+word. We start with 0 and end (at the right end) with 2. Since each move to the
+right increases or decreases the difference by 1, we must have passed through
+1 on our way from 0 to 2. Formally, we appeal to the following discrete
+intermediate value theorem \isa{nat{\isadigit{0}}{\isaliteral{5F}{\isacharunderscore}}intermed{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}val}
+\begin{isabelle}%
+\ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{3C}{\isacharless}}n{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6261723E}{\isasymbar}}f\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}\ f\ i{\isaliteral{5C3C6261723E}{\isasymbar}}\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\ f\ {\isadigit{0}}\ {\isaliteral{5C3C6C653E}{\isasymle}}\ k{\isaliteral{3B}{\isacharsemicolon}}\ k\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ n{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline
+\isaindent{\ \ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}i{\isaliteral{5C3C6C653E}{\isasymle}}n{\isaliteral{2E}{\isachardot}}\ f\ i\ {\isaliteral{3D}{\isacharequal}}\ k%
+\end{isabelle}
+where \isa{f} is of type \isa{nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ int}, \isa{int} are the integers,
+\isa{{\isaliteral{5C3C6261723E}{\isasymbar}}{\isaliteral{2E}{\isachardot}}{\isaliteral{5C3C6261723E}{\isasymbar}}} is the absolute value function\footnote{See
+Table~\ref{tab:ascii} in the Appendix for the correct \textsc{ascii}
+syntax.}, and \isa{{\isadigit{1}}} is the integer 1 (see \S\ref{sec:numbers}).
+
+First we show that our specific function, the difference between the
+numbers of \isa{a}'s and \isa{b}'s, does indeed only change by 1 in every
+move to the right. At this point we also start generalizing from \isa{a}'s
+and \isa{b}'s to an arbitrary property \isa{P}. Otherwise we would have
+to prove the desired lemma twice, once as stated above and once with the
+roles of \isa{a}'s and \isa{b}'s interchanged.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ step{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i\ {\isaliteral{3C}{\isacharless}}\ size\ w{\isaliteral{2E}{\isachardot}}\isanewline
+\ \ {\isaliteral{5C3C6261723E}{\isasymbar}}{\isaliteral{28}{\isacharparenleft}}int{\isaliteral{28}{\isacharparenleft}}size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}take\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ w{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2D}{\isacharminus}}int{\isaliteral{28}{\isacharparenleft}}size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}take\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ w{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}P\ x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}int{\isaliteral{28}{\isacharparenleft}}size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}take\ i\ w{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2D}{\isacharminus}}int{\isaliteral{28}{\isacharparenleft}}size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}take\ i\ w{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}P\ x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6261723E}{\isasymbar}}\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+\noindent
+The lemma is a bit hard to read because of the coercion function
+\isa{int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ int}. It is required because \isa{size} returns
+a natural number, but subtraction on type~\isa{nat} will do the wrong thing.
+Function \isa{take} is predefined and \isa{take\ i\ xs} is the prefix of
+length \isa{i} of \isa{xs}; below we also need \isa{drop\ i\ xs}, which
+is what remains after that prefix has been dropped from \isa{xs}.
+
+The proof is by induction on \isa{w}, with a trivial base case, and a not
+so trivial induction step. Since it is essentially just arithmetic, we do not
+discuss it.%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ w{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}auto\ simp\ add{\isaliteral{3A}{\isacharcolon}}\ abs{\isaliteral{5F}{\isacharunderscore}}if\ take{\isaliteral{5F}{\isacharunderscore}}Cons\ split{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{2E}{\isachardot}}split{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{done}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+Finally we come to the above-mentioned lemma about cutting in half a word with two more elements of one sort than of the other sort:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ part{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}w{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}w{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}P\ x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2B}{\isacharplus}}{\isadigit{2}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\isanewline
+\ \ {\isaliteral{5C3C6578697374733E}{\isasymexists}}i{\isaliteral{5C3C6C653E}{\isasymle}}size\ w{\isaliteral{2E}{\isachardot}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}take\ i\ w{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}take\ i\ w{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}P\ x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+\noindent
+This is proved by \isa{force} with the help of the intermediate value theorem,
+instantiated appropriately and with its first premise disposed of by lemma
+\isa{step{\isadigit{1}}}:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}insert\ nat{\isadigit{0}}{\isaliteral{5F}{\isacharunderscore}}intermed{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}val{\isaliteral{5B}{\isacharbrackleft}}OF\ step{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ of\ {\isaliteral{22}{\isachardoublequoteopen}}P{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}w{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{by}\isamarkupfalse%
+\ force%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent
+
+Lemma \isa{part{\isadigit{1}}} tells us only about the prefix \isa{take\ i\ w}.
+An easy lemma deals with the suffix \isa{drop\ i\ w}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ part{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\isanewline
+\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}take\ i\ w\ {\isaliteral{40}{\isacharat}}\ drop\ i\ w{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ \ \ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}take\ i\ w\ {\isaliteral{40}{\isacharat}}\ drop\ i\ w{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}P\ x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2B}{\isacharplus}}{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\ \ \ \ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}take\ i\ w{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}take\ i\ w{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}P\ x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline
+\ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}drop\ i\ w{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}drop\ i\ w{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}P\ x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}simp\ del{\isaliteral{3A}{\isacharcolon}}\ append{\isaliteral{5F}{\isacharunderscore}}take{\isaliteral{5F}{\isacharunderscore}}drop{\isaliteral{5F}{\isacharunderscore}}id{\isaliteral{29}{\isacharparenright}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent
+In the proof we have disabled the normally useful lemma
+\begin{isabelle}
+\isa{take\ n\ xs\ {\isaliteral{40}{\isacharat}}\ drop\ n\ xs\ {\isaliteral{3D}{\isacharequal}}\ xs}
+\rulename{append_take_drop_id}
+\end{isabelle}
+to allow the simplifier to apply the following lemma instead:
+\begin{isabelle}%
+\ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C696E3E}{\isasymin}}xs{\isaliteral{40}{\isacharat}}ys{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C696E3E}{\isasymin}}xs{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{40}{\isacharat}}\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C696E3E}{\isasymin}}ys{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{5D}{\isacharbrackright}}%
+\end{isabelle}
+
+To dispose of trivial cases automatically, the rules of the inductive
+definition are declared simplification rules:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{declare}\isamarkupfalse%
+\ S{\isaliteral{5F}{\isacharunderscore}}A{\isaliteral{5F}{\isacharunderscore}}B{\isaliteral{2E}{\isachardot}}intros{\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}%
+\begin{isamarkuptext}%
+\noindent
+This could have been done earlier but was not necessary so far.
+
+The completeness theorem tells us that if a word has the same number of
+\isa{a}'s and \isa{b}'s, then it is in \isa{S}, and similarly
+for \isa{A} and \isa{B}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{theorem}\isamarkupfalse%
+\ completeness{\isaliteral{3A}{\isacharcolon}}\isanewline
+\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}w{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}a{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}w{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}b{\isaliteral{5D}{\isacharbrackright}}\ \ \ \ \ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ S{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\isanewline
+\ \ \ {\isaliteral{28}{\isacharparenleft}}size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}w{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}a{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}w{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}b{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\isanewline
+\ \ \ {\isaliteral{28}{\isacharparenleft}}size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}w{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}b{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}w{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}a{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+\noindent
+The proof is by induction on \isa{w}. Structural induction would fail here
+because, as we can see from the grammar, we need to make bigger steps than
+merely appending a single letter at the front. Hence we induct on the length
+of \isa{w}, using the induction rule \isa{length{\isaliteral{5F}{\isacharunderscore}}induct}:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ w\ rule{\isaliteral{3A}{\isacharcolon}}\ length{\isaliteral{5F}{\isacharunderscore}}induct{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}rename{\isaliteral{5F}{\isacharunderscore}}tac\ w{\isaliteral{29}{\isacharparenright}}%
+\begin{isamarkuptxt}%
+\noindent
+The \isa{rule} parameter tells \isa{induct{\isaliteral{5F}{\isacharunderscore}}tac} explicitly which induction
+rule to use. For details see \S\ref{sec:complete-ind} below.
+In this case the result is that we may assume the lemma already
+holds for all words shorter than \isa{w}. Because the induction step renames
+the induction variable we rename it back to \isa{w}.
+
+The proof continues with a case distinction on \isa{w},
+on whether \isa{w} is empty or not.%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}case{\isaliteral{5F}{\isacharunderscore}}tac\ w{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{29}{\isacharparenright}}%
+\begin{isamarkuptxt}%
+\noindent
+Simplification disposes of the base case and leaves only a conjunction
+of two step cases to be proved:
+if \isa{w\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{23}{\isacharhash}}\ v} and \begin{isabelle}%
+\ \ \ \ \ length\ {\isaliteral{28}{\isacharparenleft}}if\ x\ {\isaliteral{3D}{\isacharequal}}\ a\ then\ {\isaliteral{5B}{\isacharbrackleft}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ v{\isaliteral{5D}{\isacharbrackright}}\ else\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\isaindent{\ \ \ \ \ }length\ {\isaliteral{28}{\isacharparenleft}}if\ x\ {\isaliteral{3D}{\isacharequal}}\ b\ then\ {\isaliteral{5B}{\isacharbrackleft}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ v{\isaliteral{5D}{\isacharbrackright}}\ else\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}%
+\end{isabelle} then
+\isa{b\ {\isaliteral{23}{\isacharhash}}\ v\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A}, and similarly for \isa{w\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{23}{\isacharhash}}\ v}.
+We only consider the first case in detail.
+
+After breaking the conjunction up into two cases, we can apply
+\isa{part{\isadigit{1}}} to the assumption that \isa{w} contains two more \isa{a}'s than \isa{b}'s.%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}rule\ conjI{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}clarify{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}frule\ part{\isadigit{1}}{\isaliteral{5B}{\isacharbrackleft}}of\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}a{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{2C}{\isacharcomma}}\ simplified{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}clarify{\isaliteral{29}{\isacharparenright}}%
+\begin{isamarkuptxt}%
+\noindent
+This yields an index \isa{i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ length\ v} such that
+\begin{isabelle}%
+\ \ \ \ \ length\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}take\ i\ v\ {\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ length\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}take\ i\ v\ {\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}%
+\end{isabelle}
+With the help of \isa{part{\isadigit{2}}} it follows that
+\begin{isabelle}%
+\ \ \ \ \ length\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}drop\ i\ v\ {\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ length\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}drop\ i\ v\ {\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}%
+\end{isabelle}%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}drule\ part{\isadigit{2}}{\isaliteral{5B}{\isacharbrackleft}}of\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}a{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{2C}{\isacharcomma}}\ simplified{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}assumption{\isaliteral{29}{\isacharparenright}}%
+\begin{isamarkuptxt}%
+\noindent
+Now it is time to decompose \isa{v} in the conclusion \isa{b\ {\isaliteral{23}{\isacharhash}}\ v\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A}
+into \isa{take\ i\ v\ {\isaliteral{40}{\isacharat}}\ drop\ i\ v},%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}rule{\isaliteral{5F}{\isacharunderscore}}tac\ n{\isadigit{1}}{\isaliteral{3D}{\isacharequal}}i\ \isakeyword{and}\ t{\isaliteral{3D}{\isacharequal}}v\ \isakeyword{in}\ subst{\isaliteral{5B}{\isacharbrackleft}}OF\ append{\isaliteral{5F}{\isacharunderscore}}take{\isaliteral{5F}{\isacharunderscore}}drop{\isaliteral{5F}{\isacharunderscore}}id{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}%
+\begin{isamarkuptxt}%
+\noindent
+(the variables \isa{n{\isadigit{1}}} and \isa{t} are the result of composing the
+theorems \isa{subst} and \isa{append{\isaliteral{5F}{\isacharunderscore}}take{\isaliteral{5F}{\isacharunderscore}}drop{\isaliteral{5F}{\isacharunderscore}}id})
+after which the appropriate rule of the grammar reduces the goal
+to the two subgoals \isa{take\ i\ v\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A} and \isa{drop\ i\ v\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A}:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}rule\ S{\isaliteral{5F}{\isacharunderscore}}A{\isaliteral{5F}{\isacharunderscore}}B{\isaliteral{2E}{\isachardot}}intros{\isaliteral{29}{\isacharparenright}}%
+\begin{isamarkuptxt}%
+Both subgoals follow from the induction hypothesis because both \isa{take\ i\ v} and \isa{drop\ i\ v} are shorter than \isa{w}:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}force\ simp\ add{\isaliteral{3A}{\isacharcolon}}\ min{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}iff{\isaliteral{5F}{\isacharunderscore}}disj{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}force\ split\ add{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{5F}{\isacharunderscore}}diff{\isaliteral{5F}{\isacharunderscore}}split{\isaliteral{29}{\isacharparenright}}%
+\begin{isamarkuptxt}%
+The case \isa{w\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{23}{\isacharhash}}\ v} is proved analogously:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}clarify{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}frule\ part{\isadigit{1}}{\isaliteral{5B}{\isacharbrackleft}}of\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}b{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{2C}{\isacharcomma}}\ simplified{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}clarify{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}drule\ part{\isadigit{2}}{\isaliteral{5B}{\isacharbrackleft}}of\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}b{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{2C}{\isacharcomma}}\ simplified{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}assumption{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}rule{\isaliteral{5F}{\isacharunderscore}}tac\ n{\isadigit{1}}{\isaliteral{3D}{\isacharequal}}i\ \isakeyword{and}\ t{\isaliteral{3D}{\isacharequal}}v\ \isakeyword{in}\ subst{\isaliteral{5B}{\isacharbrackleft}}OF\ append{\isaliteral{5F}{\isacharunderscore}}take{\isaliteral{5F}{\isacharunderscore}}drop{\isaliteral{5F}{\isacharunderscore}}id{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}rule\ S{\isaliteral{5F}{\isacharunderscore}}A{\isaliteral{5F}{\isacharunderscore}}B{\isaliteral{2E}{\isachardot}}intros{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}force\ simp\ add{\isaliteral{3A}{\isacharcolon}}\ min{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}iff{\isaliteral{5F}{\isacharunderscore}}disj{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{by}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}force\ simp\ add{\isaliteral{3A}{\isacharcolon}}\ min{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}iff{\isaliteral{5F}{\isacharunderscore}}disj\ split\ add{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{5F}{\isacharunderscore}}diff{\isaliteral{5F}{\isacharunderscore}}split{\isaliteral{29}{\isacharparenright}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+We conclude this section with a comparison of our proof with
+Hopcroft\index{Hopcroft, J. E.} and Ullman's\index{Ullman, J. D.}
+\cite[p.\ts81]{HopcroftUllman}.
+For a start, the textbook
+grammar, for no good reason, excludes the empty word, thus complicating
+matters just a little bit: they have 8 instead of our 7 productions.
+
+More importantly, the proof itself is different: rather than
+separating the two directions, they perform one induction on the
+length of a word. This deprives them of the beauty of rule induction,
+and in the easy direction (correctness) their reasoning is more
+detailed than our \isa{auto}. For the hard part (completeness), they
+consider just one of the cases that our \isa{simp{\isaliteral{5F}{\isacharunderscore}}all} disposes of
+automatically. Then they conclude the proof by saying about the
+remaining cases: ``We do this in a manner similar to our method of
+proof for part (1); this part is left to the reader''. But this is
+precisely the part that requires the intermediate value theorem and
+thus is not at all similar to the other cases (which are automatic in
+Isabelle). The authors are at least cavalier about this point and may
+even have overlooked the slight difficulty lurking in the omitted
+cases. Such errors are found in many pen-and-paper proofs when they
+are scrutinized formally.%
+\index{grammars!defining inductively|)}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: