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