doc-src/TutorialI/Inductive/document/AB.tex
changeset 10236 7626cb4e1407
parent 10225 b9fd52525b69
child 10237 875bf54b5d74
     1.1 --- a/doc-src/TutorialI/Inductive/document/AB.tex	Tue Oct 17 10:45:51 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Inductive/document/AB.tex	Tue Oct 17 13:28:57 2000 +0200
     1.3 @@ -3,123 +3,278 @@
     1.4  \def\isabellecontext{AB}%
     1.5  %
     1.6  \isamarkupsection{A context free grammar}
     1.7 -\isacommand{datatype}\ alfa\ {\isacharequal}\ a\ {\isacharbar}\ b\isanewline
     1.8 -\isanewline
     1.9 -\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isachartilde}{\isacharequal}\ a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ b{\isacharparenright}\ {\isacharampersand}\ {\isacharparenleft}x\ {\isachartilde}{\isacharequal}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ a{\isacharparenright}{\isachardoublequote}\isanewline
    1.10 +%
    1.11 +\begin{isamarkuptext}%
    1.12 +Grammars are nothing but shorthands for inductive definitions of nonterminals
    1.13 +which represent sets of strings. For example, the production
    1.14 +$A \to B c$ is short for
    1.15 +\[ w \in B \Longrightarrow wc \in A \]
    1.16 +This section demonstrates this idea with a standard example
    1.17 +\cite[p.\ 81]{HopcroftUllman}, a grammar for generating all words with an
    1.18 +equal number of $a$'s and $b$'s:
    1.19 +\begin{eqnarray}
    1.20 +S &\to& \epsilon \mid b A \mid a B \nonumber\\
    1.21 +A &\to& a S \mid b A A \nonumber\\
    1.22 +B &\to& b S \mid a B B \nonumber
    1.23 +\end{eqnarray}
    1.24 +At the end we say a few words about the relationship of the formalization
    1.25 +and the text in the book~\cite[p.\ 81]{HopcroftUllman}.
    1.26 +
    1.27 +We start by fixing the alpgabet, which consists only of \isa{a}'s
    1.28 +and \isa{b}'s:%
    1.29 +\end{isamarkuptext}%
    1.30 +\isacommand{datatype}\ alfa\ {\isacharequal}\ a\ {\isacharbar}\ b%
    1.31 +\begin{isamarkuptext}%
    1.32 +\noindent
    1.33 +For convenience we includ the following easy lemmas as simplification rules:%
    1.34 +\end{isamarkuptext}%
    1.35 +\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
    1.36  \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ x{\isacharparenright}\isanewline
    1.37 -\isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline
    1.38 -\isanewline
    1.39 +\isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
    1.40 +\begin{isamarkuptext}%
    1.41 +\noindent
    1.42 +Words over this alphabet are of type \isa{alfa\ list}, and
    1.43 +the three nonterminals are declare as sets of such words:%
    1.44 +\end{isamarkuptext}%
    1.45  \isacommand{consts}\ S\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline
    1.46  \ \ \ \ \ \ \ A\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline
    1.47 -\ \ \ \ \ \ \ B\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline
    1.48 -\isanewline
    1.49 +\ \ \ \ \ \ \ B\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}%
    1.50 +\begin{isamarkuptext}%
    1.51 +\noindent
    1.52 +The above productions are recast as a \emph{simultaneous} inductive
    1.53 +definition of \isa{S}, \isa{A} and \isa{B}:%
    1.54 +\end{isamarkuptext}%
    1.55  \isacommand{inductive}\ S\ A\ B\isanewline
    1.56  \isakeyword{intros}\isanewline
    1.57 -{\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}\ {\isacharcolon}\ S{\isachardoublequote}\isanewline
    1.58 -{\isachardoublequote}w\ {\isacharcolon}\ A\ {\isacharequal}{\isacharequal}{\isachargreater}\ b{\isacharhash}w\ {\isacharcolon}\ S{\isachardoublequote}\isanewline
    1.59 -{\isachardoublequote}w\ {\isacharcolon}\ B\ {\isacharequal}{\isacharequal}{\isachargreater}\ a{\isacharhash}w\ {\isacharcolon}\ S{\isachardoublequote}\isanewline
    1.60 -\isanewline
    1.61 -{\isachardoublequote}w\ {\isacharcolon}\ S\ {\isacharequal}{\isacharequal}{\isachargreater}\ a{\isacharhash}w\ {\isacharcolon}\ A{\isachardoublequote}\isanewline
    1.62 -{\isachardoublequote}{\isacharbrackleft}{\isacharbar}\ v{\isacharcolon}A{\isacharsemicolon}\ w{\isacharcolon}A\ {\isacharbar}{\isacharbrackright}\ {\isacharequal}{\isacharequal}{\isachargreater}\ b{\isacharhash}v{\isacharat}w\ {\isacharcolon}\ A{\isachardoublequote}\isanewline
    1.63 +\ \ {\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}\ {\isasymin}\ S{\isachardoublequote}\isanewline
    1.64 +\ \ {\isachardoublequote}w\ {\isasymin}\ A\ {\isasymLongrightarrow}\ b{\isacharhash}w\ {\isasymin}\ S{\isachardoublequote}\isanewline
    1.65 +\ \ {\isachardoublequote}w\ {\isasymin}\ B\ {\isasymLongrightarrow}\ a{\isacharhash}w\ {\isasymin}\ S{\isachardoublequote}\isanewline
    1.66  \isanewline
    1.67 -{\isachardoublequote}w\ {\isacharcolon}\ S\ {\isacharequal}{\isacharequal}{\isachargreater}\ b{\isacharhash}w\ {\isacharcolon}\ B{\isachardoublequote}\isanewline
    1.68 -{\isachardoublequote}{\isacharbrackleft}{\isacharbar}\ v{\isacharcolon}B{\isacharsemicolon}\ w{\isacharcolon}B\ {\isacharbar}{\isacharbrackright}\ {\isacharequal}{\isacharequal}{\isachargreater}\ a{\isacharhash}v{\isacharat}w\ {\isacharcolon}\ B{\isachardoublequote}\isanewline
    1.69 -\isanewline
    1.70 -\isacommand{thm}\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharbrackleft}no{\isacharunderscore}vars{\isacharbrackright}\isanewline
    1.71 -\isanewline
    1.72 -\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}w\ {\isacharcolon}\ S\ {\isacharminus}{\isacharminus}{\isachargreater}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}{\isacharparenright}\ {\isacharampersand}\isanewline
    1.73 -\ \ \ \ \ \ \ {\isacharparenleft}w\ {\isacharcolon}\ A\ {\isacharminus}{\isacharminus}{\isachargreater}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharampersand}\isanewline
    1.74 -\ \ \ \ \ \ \ {\isacharparenleft}w\ {\isacharcolon}\ B\ {\isacharminus}{\isacharminus}{\isachargreater}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
    1.75 -\isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharparenright}\isanewline
    1.76 -\isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline
    1.77 +\ \ {\isachardoublequote}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ a{\isacharhash}w\ \ \ {\isasymin}\ A{\isachardoublequote}\isanewline
    1.78 +\ \ {\isachardoublequote}{\isasymlbrakk}\ v{\isasymin}A{\isacharsemicolon}\ w{\isasymin}A\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ b{\isacharhash}v{\isacharat}w\ {\isasymin}\ A{\isachardoublequote}\isanewline
    1.79  \isanewline
    1.80 -\isacommand{lemma}\ intermed{\isacharunderscore}val{\isacharbrackleft}rule{\isacharunderscore}format{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharbrackright}{\isacharcolon}\isanewline
    1.81 -\ {\isachardoublequote}{\isacharparenleft}{\isacharbang}i{\isacharless}n{\isachardot}\ abs{\isacharparenleft}f{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isacharparenright}\ {\isacharless}{\isacharequal}\ {\isacharhash}{\isadigit{1}}{\isacharparenright}\ {\isacharminus}{\isacharminus}{\isachargreater}\ \isanewline
    1.82 -\ \ f\ {\isadigit{0}}\ {\isacharless}{\isacharequal}\ k\ {\isacharampersand}\ k\ {\isacharless}{\isacharequal}\ f\ n\ {\isacharminus}{\isacharminus}{\isachargreater}\ {\isacharparenleft}{\isacharquery}\ i\ {\isacharless}{\isacharequal}\ n{\isachardot}\ f\ i\ {\isacharequal}\ {\isacharparenleft}k{\isacharcolon}{\isacharcolon}int{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
    1.83 -\isacommand{apply}{\isacharparenleft}induct\ n{\isacharparenright}\isanewline
    1.84 -\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
    1.85 -\ \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline
    1.86 -\isacommand{apply}{\isacharparenleft}rule{\isacharparenright}\isanewline
    1.87 -\isacommand{apply}{\isacharparenleft}erule\ impE{\isacharparenright}\isanewline
    1.88 -\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
    1.89 -\isacommand{apply}{\isacharparenleft}rule{\isacharparenright}\isanewline
    1.90 -\isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ n\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
    1.91 -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
    1.92 -\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ {\isachardoublequote}k\ {\isacharequal}\ f{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}{\isacharparenright}\isanewline
    1.93 -\ \isacommand{apply}{\isacharparenleft}force{\isacharparenright}\isanewline
    1.94 -\isacommand{apply}{\isacharparenleft}erule\ impE{\isacharparenright}\isanewline
    1.95 -\ \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}zabs{\isacharunderscore}def\ split{\isacharcolon}split{\isacharunderscore}if{\isacharunderscore}asm{\isacharparenright}\isanewline
    1.96 -\ \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline
    1.97 -\isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}le{\isacharunderscore}SucI{\isacharparenright}\isanewline
    1.98 -\isanewline
    1.99 -\isacommand{lemma}\ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}ALL\ i\ {\isacharless}\ size\ w{\isachardot}\isanewline
   1.100 -\ \ abs{\isacharparenleft}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w\ {\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\ int{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w\ {\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharminus}\isanewline
   1.101 -\ \ \ \ \ \ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}take\ i\ w\ {\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\ int{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}take\ i\ w\ {\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharless}{\isacharequal}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}\isanewline
   1.102 +\ \ {\isachardoublequote}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ b{\isacharhash}w\ \ \ {\isasymin}\ B{\isachardoublequote}\isanewline
   1.103 +\ \ {\isachardoublequote}{\isasymlbrakk}\ v\ {\isasymin}\ B{\isacharsemicolon}\ w\ {\isasymin}\ B\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ a{\isacharhash}v{\isacharat}w\ {\isasymin}\ B{\isachardoublequote}%
   1.104 +\begin{isamarkuptext}%
   1.105 +\noindent
   1.106 +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
   1.107 +induction, so is this proof: we show at the same time that all words in
   1.108 +\isa{A} contain one more \isa{a} than \isa{b} and all words in \isa{B} contains one more \isa{b} than \isa{a}.%
   1.109 +\end{isamarkuptext}%
   1.110 +\isacommand{lemma}\ correctness{\isacharcolon}\isanewline
   1.111 +\ \ {\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
   1.112 +\ \ \ \ {\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
   1.113 +\ \ \ \ {\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}%
   1.114 +\begin{isamarkuptxt}%
   1.115 +\noindent
   1.116 +These propositions are expressed with the help of the predefined \isa{filter} function on lists, which has the convenient syntax \isa{filter\ P\ xs}, the list of all elements \isa{x} in \isa{xs} such that \isa{P\ x}
   1.117 +holds. The length of a list is usually written \isa{size}, and \isa{size} is merely a shorthand.
   1.118 +
   1.119 +The proof itself is by rule induction and afterwards automatic:%
   1.120 +\end{isamarkuptxt}%
   1.121 +\isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharparenright}\isanewline
   1.122 +\isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
   1.123 +\begin{isamarkuptext}%
   1.124 +\noindent
   1.125 +This may seem surprising at first, and is indeed an indication of the power
   1.126 +of inductive definitions. But it is also quite straightforward. For example,
   1.127 +consider the production $A \to b A A$: if $v,w \in A$ and the elements of $A$
   1.128 +contain one more $a$ than $b$'s, then $bvw$ must again contain one more $a$
   1.129 +than $b$'s.
   1.130 +
   1.131 +As usual, the correctness of syntactic descriptions is easy, but completeness
   1.132 +is hard: does \isa{S} contain \emph{all} words with an equal number of
   1.133 +\isa{a}'s and \isa{b}'s? It turns out that this proof requires the
   1.134 +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
   1.135 +\isa{b}. This is best seen by imagining counting the difference between the
   1.136 +number of \isa{a}'s than \isa{b}'s starting at the left end of the
   1.137 +word. We start at 0 and end (at the right end) with 2. Since each move to the
   1.138 +right increases or decreases the difference by 1, we must have passed through
   1.139 +1 on our way from 0 to 2. Formally, we appeal to the following discrete
   1.140 +intermediate value theorem \isa{nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val}
   1.141 +\begin{isabelle}%
   1.142 +\ \ \ \ \ {\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
   1.143 +\ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ i\ {\isasymle}\ n\ {\isasymand}\ f\ i\ {\isacharequal}\ k%
   1.144 +\end{isabelle}
   1.145 +where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers,
   1.146 +\isa{abs} is the absolute value function, and \isa{{\isacharhash}{\isadigit{1}}} is the
   1.147 +integer 1 (see \S\ref{sec:int}).
   1.148 +
   1.149 +First we show that the our specific function, the difference between the
   1.150 +numbers of \isa{a}'s and \isa{b}'s, does indeed only change by 1 in every
   1.151 +move to the right. At this point we also start generalizing from \isa{a}'s
   1.152 +and \isa{b}'s to an arbitrary property \isa{P}. Otherwise we would have
   1.153 +to prove the desired lemma twice, once as stated above and once with the
   1.154 +roles of \isa{a}'s and \isa{b}'s interchanged.%
   1.155 +\end{isamarkuptext}%
   1.156 +\isacommand{lemma}\ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i\ {\isacharless}\ size\ w{\isachardot}\isanewline
   1.157 +\ \ abs{\isacharparenleft}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ \ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\isanewline
   1.158 +\ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline
   1.159 +\ \ \ \ \ \ {\isacharminus}\isanewline
   1.160 +\ \ \ \ \ \ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ \ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\isanewline
   1.161 +\ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharless}{\isacharequal}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}%
   1.162 +\begin{isamarkuptxt}%
   1.163 +\noindent
   1.164 +The lemma is a bit hard to read because of the coercion function
   1.165 +\isa{{\isachardoublequote}int{\isacharcolon}{\isacharcolon}nat\ {\isasymRightarrow}\ int{\isachardoublequote}}. It is required because \isa{size} returns
   1.166 +a natural number, but \isa{{\isacharminus}} on \isa{nat} will do the wrong thing.
   1.167 +Function \isa{take} is predefined and \isa{take\ i\ xs} is the prefix of
   1.168 +length \isa{i} of \isa{xs}; below we als need \isa{drop\ i\ xs}, which
   1.169 +is what remains after that prefix has been dropped from \isa{xs}.
   1.170 +
   1.171 +The proof is by induction on \isa{w}, with a trivial base case, and a not
   1.172 +so trivial induction step. Since it is essentially just arithmetic, we do not
   1.173 +discuss it.%
   1.174 +\end{isamarkuptxt}%
   1.175  \isacommand{apply}{\isacharparenleft}induct\ w{\isacharparenright}\isanewline
   1.176  \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
   1.177 -\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}take{\isacharunderscore}Cons\ split{\isacharcolon}nat{\isachardot}split{\isacharparenright}\isanewline
   1.178 -\isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}\isanewline
   1.179 +\isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}zabs{\isacharunderscore}def\ take{\isacharunderscore}Cons\ split{\isacharcolon}nat{\isachardot}split\ if{\isacharunderscore}splits{\isacharparenright}%
   1.180 +\begin{isamarkuptext}%
   1.181 +Finally we come to the above mentioned lemma about cutting a word with two
   1.182 +more elements of one sort than of the other sort into two halfs:%
   1.183 +\end{isamarkuptext}%
   1.184 +\isacommand{lemma}\ part{\isadigit{1}}{\isacharcolon}\isanewline
   1.185 +\ {\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
   1.186 +\ \ {\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}%
   1.187 +\begin{isamarkuptxt}%
   1.188 +\noindent
   1.189 +This is proved with the help of the intermediate value theorem, instantiated
   1.190 +appropriately and with its first premise disposed of by lemma
   1.191 +\isa{step{\isadigit{1}}}.%
   1.192 +\end{isamarkuptxt}%
   1.193 +\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
   1.194 +\isacommand{apply}\ simp\isanewline
   1.195 +\isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}int{\isacharunderscore}Suc\ add{\isacharcolon}zdiff{\isacharunderscore}eq{\isacharunderscore}eq\ sym{\isacharbrackleft}OF\ int{\isacharunderscore}Suc{\isacharbrackright}{\isacharparenright}%
   1.196 +\begin{isamarkuptext}%
   1.197 +\noindent
   1.198 +The additional lemmas are needed to mediate between \isa{nat} and \isa{int}.
   1.199 +
   1.200 +Lemma \isa{part{\isadigit{1}}} tells us only about the prefix \isa{take\ i\ w}.
   1.201 +The suffix \isa{drop\ i\ w} is dealt with in the following easy lemma:%
   1.202 +\end{isamarkuptext}%
   1.203 +\isacommand{lemma}\ part{\isadigit{2}}{\isacharcolon}\isanewline
   1.204 +\ \ {\isachardoublequote}{\isasymlbrakk}size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\isanewline
   1.205 +\ \ \ \ size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}{\isacharsemicolon}\isanewline
   1.206 +\ \ \ \ 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
   1.207 +\ \ \ {\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
   1.208 +\isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharparenright}%
   1.209 +\begin{isamarkuptext}%
   1.210 +\noindent
   1.211 +Lemma \isa{append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id}, \isa{take\ n\ xs\ {\isacharat}\ drop\ n\ xs\ {\isacharequal}\ xs},
   1.212 +which is generally useful, needs to be disabled for once.
   1.213 +
   1.214 +To dispose of trivial cases automatically, the rules of the inductive
   1.215 +definition are declared simplification rules:%
   1.216 +\end{isamarkuptext}%
   1.217 +\isacommand{declare}\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharbrackleft}simp{\isacharbrackright}%
   1.218 +\begin{isamarkuptext}%
   1.219 +\noindent
   1.220 +This could have been done earlier but was not necessary so far.
   1.221 +
   1.222 +The completeness theorem tells us that if a word has the same number of
   1.223 +\isa{a}'s and \isa{b}'s, then it is in \isa{S}, and similarly and
   1.224 +simultaneously for \isa{A} and \isa{B}:%
   1.225 +\end{isamarkuptext}%
   1.226 +\isacommand{theorem}\ completeness{\isacharcolon}\isanewline
   1.227 +\ \ {\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
   1.228 +\ \ \ \ {\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
   1.229 +\ \ \ \ {\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}%
   1.230 +\begin{isamarkuptxt}%
   1.231 +\noindent
   1.232 +The proof is by induction on \isa{w}. Structural induction would fail here
   1.233 +because, as we can see from the grammar, we need to make bigger steps than
   1.234 +merely appending a single letter at the front. Hence we induct on the length
   1.235 +of \isa{w}, using the induction rule \isa{length{\isacharunderscore}induct}:%
   1.236 +\end{isamarkuptxt}%
   1.237 +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}%
   1.238 +\begin{isamarkuptxt}%
   1.239 +\noindent
   1.240 +The \isa{rule} parameter tells \isa{induct{\isacharunderscore}tac} explicitly which induction
   1.241 +rule to use. For details see \S\ref{sec:complete-ind} below.
   1.242 +In this case the result is that we may assume the lemma already
   1.243 +holds for all words shorter than \isa{w}.
   1.244 +
   1.245 +The proof continues with a case distinction on \isa{w},
   1.246 +i.e.\ if \isa{w} is empty or not.%
   1.247 +\end{isamarkuptxt}%
   1.248 +\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ w{\isacharparenright}\isanewline
   1.249 +\ \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}%
   1.250 +\begin{isamarkuptxt}%
   1.251 +\noindent
   1.252 +Simplification disposes of the base case and leaves only two step
   1.253 +cases to be proved:
   1.254 +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
   1.255 +\isa{b\ {\isacharhash}\ v\ {\isasymin}\ A}, and similarly for \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v}.
   1.256 +We only consider the first case in detail.
   1.257 +
   1.258 +After breaking the conjuction up into two cases, we can apply
   1.259 +\isa{part{\isadigit{1}}} to the assumption that \isa{w} contains two more \isa{a}'s than \isa{b}'s.%
   1.260 +\end{isamarkuptxt}%
   1.261  \isacommand{apply}{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline
   1.262  \ \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
   1.263 -\ \isacommand{apply}{\isacharparenleft}erule\ allE{\isacharparenright}\isanewline
   1.264 -\ \isacommand{apply}{\isacharparenleft}erule\ impE{\isacharparenright}\isanewline
   1.265 -\ \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline
   1.266 -\ \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline
   1.267 +\ \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
   1.268 +\ \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
   1.269 +\ \isacommand{apply}{\isacharparenleft}erule\ conjE{\isacharparenright}%
   1.270 +\begin{isamarkuptxt}%
   1.271 +\noindent
   1.272 +This yields an index \isa{i\ {\isasymle}\ length\ v} such that
   1.273 +\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}}}.
   1.274 +With the help of \isa{part{\isadigit{1}}} it follows that
   1.275 +\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}}}.%
   1.276 +\end{isamarkuptxt}%
   1.277 +\ \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
   1.278 +\ \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}%
   1.279 +\begin{isamarkuptxt}%
   1.280 +\noindent
   1.281 +Now it is time to decompose \isa{v} in the conclusion \isa{b\ {\isacharhash}\ v\ {\isasymin}\ A}
   1.282 +into \isa{take\ i\ v\ {\isacharat}\ drop\ i\ v},
   1.283 +after which the appropriate rule of the grammar reduces the goal
   1.284 +to the two subgoals \isa{take\ i\ v\ {\isasymin}\ A} and \isa{drop\ i\ v\ {\isasymin}\ A}:%
   1.285 +\end{isamarkuptxt}%
   1.286 +\ \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
   1.287 +\ \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}%
   1.288 +\begin{isamarkuptxt}%
   1.289 +\noindent
   1.290 +Both subgoals follow from the induction hypothesis because both \isa{take\ i\ v} and \isa{drop\ i\ v} are shorter than \isa{w}:%
   1.291 +\end{isamarkuptxt}%
   1.292 +\ \ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline
   1.293 +\ \isacommand{apply}{\isacharparenleft}force\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}%
   1.294 +\begin{isamarkuptxt}%
   1.295 +\noindent
   1.296 +Note that the variables \isa{n{\isadigit{1}}} and \isa{t} referred to in the
   1.297 +substitution step above come from the derived theorem \isa{subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}}.
   1.298 +
   1.299 +The case \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v} is proved completely analogously:%
   1.300 +\end{isamarkuptxt}%
   1.301  \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
   1.302 -\isacommand{apply}{\isacharparenleft}erule\ allE{\isacharparenright}\isanewline
   1.303 -\isacommand{apply}{\isacharparenleft}erule\ impE{\isacharparenright}\isanewline
   1.304 -\ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline
   1.305 -\isacommand{by}{\isacharparenleft}arith{\isacharparenright}\isanewline
   1.306 -\isanewline
   1.307 -\isanewline
   1.308 -\isacommand{lemma}\ part{\isadigit{1}}{\isacharcolon}\isanewline
   1.309 -\ {\isachardoublequote}size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ Suc{\isacharparenleft}Suc{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}{\isacharequal}{\isachargreater}\isanewline
   1.310 -\ \ EX\ i{\isacharless}{\isacharequal}size\ w{\isachardot}\ size{\isacharbrackleft}x{\isacharcolon}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}take\ i\ w{\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequote}\isanewline
   1.311 -\isacommand{apply}{\isacharparenleft}insert\ intermed{\isacharunderscore}val{\isacharbrackleft}OF\ step{\isadigit{1}}{\isacharcomma}\ of\ {\isachardoublequote}P{\isachardoublequote}\ {\isachardoublequote}w{\isachardoublequote}\ {\isachardoublequote}{\isacharhash}{\isadigit{1}}{\isachardoublequote}{\isacharbrackright}{\isacharparenright}\isanewline
   1.312 -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
   1.313 -\isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
   1.314 -\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}i\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
   1.315 -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
   1.316 -\isacommand{apply}{\isacharparenleft}rule\ int{\isacharunderscore}int{\isacharunderscore}eq{\isacharbrackleft}THEN\ iffD{\isadigit{1}}{\isacharbrackright}{\isacharparenright}\isanewline
   1.317 -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
   1.318 -\isacommand{by}{\isacharparenleft}arith{\isacharparenright}\isanewline
   1.319 -\isanewline
   1.320 -\isacommand{lemma}\ part{\isadigit{2}}{\isacharcolon}\isanewline
   1.321 -{\isachardoublequote}{\isacharbrackleft}{\isacharbar}\ size{\isacharbrackleft}x{\isacharcolon}take\ i\ xs\ {\isacharat}\ drop\ i\ xs{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}take\ i\ xs\ {\isacharat}\ drop\ i\ xs{\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}{\isacharsemicolon}\isanewline
   1.322 -\ \ \ \ size{\isacharbrackleft}x{\isacharcolon}take\ i\ xs{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}take\ i\ xs{\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}\ {\isacharbar}{\isacharbrackright}\isanewline
   1.323 -\ {\isacharequal}{\isacharequal}{\isachargreater}\ size{\isacharbrackleft}x{\isacharcolon}drop\ i\ xs{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}drop\ i\ xs{\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequote}\isanewline
   1.324 -\isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharparenright}\isanewline
   1.325 -\isanewline
   1.326 -\isacommand{lemmas}\ {\isacharbrackleft}simp{\isacharbrackright}\ {\isacharequal}\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros\isanewline
   1.327 -\isanewline
   1.328 -\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharminus}{\isacharminus}{\isachargreater}\ w\ {\isacharcolon}\ S{\isacharparenright}\ {\isacharampersand}\isanewline
   1.329 -\ \ \ \ \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}{\isacharminus}{\isachargreater}\ w\ {\isacharcolon}\ A{\isacharparenright}\ {\isacharampersand}\isanewline
   1.330 -\ \ \ \ \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}{\isacharminus}{\isachargreater}\ w\ {\isacharcolon}\ B{\isacharparenright}{\isachardoublequote}\isanewline
   1.331 -\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}\isanewline
   1.332 -\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ {\isachardoublequote}xs{\isachardoublequote}{\isacharparenright}\isanewline
   1.333 -\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
   1.334 -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
   1.335 -\isacommand{apply}{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline
   1.336 -\ \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
   1.337 -\ \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isacharpercent}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
   1.338 -\ \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
   1.339 -\ \isacommand{apply}{\isacharparenleft}erule\ conjE{\isacharparenright}\isanewline
   1.340 -\ \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isacharpercent}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
   1.341 -\ \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline
   1.342 -\ \isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ n{\isadigit{1}}{\isacharequal}i\ \isakeyword{and}\ t{\isacharequal}list\ \isakeyword{in}\ subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}{\isacharparenright}\isanewline
   1.343 -\ \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isanewline
   1.344 -\ \ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline
   1.345 -\ \isacommand{apply}{\isacharparenleft}force\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isanewline
   1.346 -\isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
   1.347 -\isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isacharpercent}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
   1.348 +\isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
   1.349  \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
   1.350  \isacommand{apply}{\isacharparenleft}erule\ conjE{\isacharparenright}\isanewline
   1.351 -\isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isacharpercent}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
   1.352 +\isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
   1.353  \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline
   1.354 -\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ n{\isadigit{1}}{\isacharequal}i\ \isakeyword{and}\ t{\isacharequal}list\ \isakeyword{in}\ subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}{\isacharparenright}\isanewline
   1.355 +\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
   1.356  \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isanewline
   1.357  \ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline
   1.358 -\isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isanewline
   1.359 +\isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}%
   1.360 +\begin{isamarkuptext}%
   1.361 +We conclude this section with a comparison of the above proof and the one
   1.362 +in the textbook \cite[p.\ 81]{HopcroftUllman}. For a start, the texbook
   1.363 +grammar, for no good reason, excludes the empty word, which complicates
   1.364 +matters just a little bit because we now have 8 instead of our 7 productions.
   1.365 +
   1.366 +More importantly, the proof itself is different: rather than separating the
   1.367 +two directions, they perform one induction on the length of a word. This
   1.368 +deprives them of the beauty of rule induction and in the easy direction
   1.369 +(correctness) their reasoning is more detailed than our \isa{auto}. For the
   1.370 +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
   1.371 +about the remaining cases: ``We do this in a manner similar to our method of
   1.372 +proof for part (1); this part is left to the reader''. But this is precisely
   1.373 +the part that requires the intermediate value theorem and thus is not at all
   1.374 +similar to the other cases (which are automatic in Isabelle). We conclude
   1.375 +that the authors are at least cavalier about this point and may even have
   1.376 +overlooked the slight difficulty lurking in the omitted cases. This is not
   1.377 +atypical for pen-and-paper proofs, once analysed in detail.%
   1.378 +\end{isamarkuptext}%
   1.379  \end{isabellebody}%
   1.380  %%% Local Variables:
   1.381  %%% mode: latex