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