10217
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{AB}%
|
17056
|
4 |
%
|
|
5 |
\isadelimtheory
|
|
6 |
%
|
|
7 |
\endisadelimtheory
|
|
8 |
%
|
|
9 |
\isatagtheory
|
|
10 |
%
|
|
11 |
\endisatagtheory
|
|
12 |
{\isafoldtheory}%
|
|
13 |
%
|
|
14 |
\isadelimtheory
|
|
15 |
%
|
|
16 |
\endisadelimtheory
|
10225
|
17 |
%
|
10878
|
18 |
\isamarkupsection{Case Study: A Context Free Grammar%
|
10395
|
19 |
}
|
11866
|
20 |
\isamarkuptrue%
|
10236
|
21 |
%
|
|
22 |
\begin{isamarkuptext}%
|
10242
|
23 |
\label{sec:CFG}
|
11494
|
24 |
\index{grammars!defining inductively|(}%
|
10236
|
25 |
Grammars are nothing but shorthands for inductive definitions of nonterminals
|
|
26 |
which represent sets of strings. For example, the production
|
|
27 |
$A \to B c$ is short for
|
|
28 |
\[ w \in B \Longrightarrow wc \in A \]
|
10878
|
29 |
This section demonstrates this idea with an example
|
|
30 |
due to Hopcroft and Ullman, a grammar for generating all words with an
|
|
31 |
equal number of $a$'s and~$b$'s:
|
10236
|
32 |
\begin{eqnarray}
|
|
33 |
S &\to& \epsilon \mid b A \mid a B \nonumber\\
|
|
34 |
A &\to& a S \mid b A A \nonumber\\
|
|
35 |
B &\to& b S \mid a B B \nonumber
|
|
36 |
\end{eqnarray}
|
10878
|
37 |
At the end we say a few words about the relationship between
|
|
38 |
the original proof \cite[p.\ts81]{HopcroftUllman} and our formal version.
|
10236
|
39 |
|
10299
|
40 |
We start by fixing the alphabet, which consists only of \isa{a}'s
|
10878
|
41 |
and~\isa{b}'s:%
|
10236
|
42 |
\end{isamarkuptext}%
|
17175
|
43 |
\isamarkuptrue%
|
|
44 |
\isacommand{datatype}\isamarkupfalse%
|
40406
|
45 |
\ alfa\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{7C}{\isacharbar}}\ b%
|
10236
|
46 |
\begin{isamarkuptext}%
|
|
47 |
\noindent
|
10299
|
48 |
For convenience we include the following easy lemmas as simplification rules:%
|
10236
|
49 |
\end{isamarkuptext}%
|
17175
|
50 |
\isamarkuptrue%
|
|
51 |
\isacommand{lemma}\isamarkupfalse%
|
40406
|
52 |
\ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
17056
|
53 |
%
|
|
54 |
\isadelimproof
|
|
55 |
%
|
|
56 |
\endisadelimproof
|
|
57 |
%
|
|
58 |
\isatagproof
|
17175
|
59 |
\isacommand{by}\isamarkupfalse%
|
40406
|
60 |
\ {\isaliteral{28}{\isacharparenleft}}case{\isaliteral{5F}{\isacharunderscore}}tac\ x{\isaliteral{2C}{\isacharcomma}}\ auto{\isaliteral{29}{\isacharparenright}}%
|
17056
|
61 |
\endisatagproof
|
|
62 |
{\isafoldproof}%
|
|
63 |
%
|
|
64 |
\isadelimproof
|
|
65 |
%
|
|
66 |
\endisadelimproof
|
11866
|
67 |
%
|
10236
|
68 |
\begin{isamarkuptext}%
|
|
69 |
\noindent
|
|
70 |
Words over this alphabet are of type \isa{alfa\ list}, and
|
23733
|
71 |
the three nonterminals are declared as sets of such words.
|
10878
|
72 |
The productions above are recast as a \emph{mutual} inductive
|
10242
|
73 |
definition\index{inductive definition!simultaneous}
|
10878
|
74 |
of \isa{S}, \isa{A} and~\isa{B}:%
|
10236
|
75 |
\end{isamarkuptext}%
|
17175
|
76 |
\isamarkuptrue%
|
40406
|
77 |
\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse%
|
23733
|
78 |
\isanewline
|
40406
|
79 |
\ \ S\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}alfa\ list\ set{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline
|
|
80 |
\ \ A\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}alfa\ list\ set{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline
|
|
81 |
\ \ B\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}alfa\ list\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
23733
|
82 |
\isakeyword{where}\isanewline
|
40406
|
83 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ S{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
84 |
{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ b{\isaliteral{23}{\isacharhash}}w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ S{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
85 |
{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a{\isaliteral{23}{\isacharhash}}w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ S{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
10217
|
86 |
\isanewline
|
40406
|
87 |
{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ S\ \ \ \ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a{\isaliteral{23}{\isacharhash}}w\ \ \ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
88 |
{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ v{\isaliteral{5C3C696E3E}{\isasymin}}A{\isaliteral{3B}{\isacharsemicolon}}\ w{\isaliteral{5C3C696E3E}{\isasymin}}A\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ b{\isaliteral{23}{\isacharhash}}v{\isaliteral{40}{\isacharat}}w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
10217
|
89 |
\isanewline
|
40406
|
90 |
{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ S\ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ b{\isaliteral{23}{\isacharhash}}w\ \ \ {\isaliteral{5C3C696E3E}{\isasymin}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
91 |
{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ v\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B{\isaliteral{3B}{\isacharsemicolon}}\ w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a{\isaliteral{23}{\isacharhash}}v{\isaliteral{40}{\isacharat}}w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B{\isaliteral{22}{\isachardoublequoteclose}}%
|
10236
|
92 |
\begin{isamarkuptext}%
|
|
93 |
\noindent
|
10878
|
94 |
First we show that all words in \isa{S} contain the same number of \isa{a}'s and \isa{b}'s. Since the definition of \isa{S} is by mutual
|
|
95 |
induction, so is the proof: we show at the same time that all words in
|
27167
|
96 |
\isa{A} contain one more \isa{a} than \isa{b} and all words in \isa{B} contain one more \isa{b} than \isa{a}.%
|
10236
|
97 |
\end{isamarkuptext}%
|
17175
|
98 |
\isamarkuptrue%
|
|
99 |
\isacommand{lemma}\isamarkupfalse%
|
40406
|
100 |
\ correctness{\isaliteral{3A}{\isacharcolon}}\isanewline
|
|
101 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ S\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}w{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}a{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}w{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}b{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ \ \ \ \ {\isaliteral{5C3C616E643E}{\isasymand}}\isanewline
|
|
102 |
\ \ \ {\isaliteral{28}{\isacharparenleft}}w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}w{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}a{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}w{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}b{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\isanewline
|
|
103 |
\ \ \ {\isaliteral{28}{\isacharparenleft}}w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}w{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}b{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}w{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}a{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
|
17056
|
104 |
\isadelimproof
|
|
105 |
%
|
|
106 |
\endisadelimproof
|
|
107 |
%
|
|
108 |
\isatagproof
|
16069
|
109 |
%
|
|
110 |
\begin{isamarkuptxt}%
|
|
111 |
\noindent
|
40406
|
112 |
These propositions are expressed with the help of the predefined \isa{filter} function on lists, which has the convenient syntax \isa{{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}xs{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{5D}{\isacharbrackright}}}, the list of all elements \isa{x} in \isa{xs} such that \isa{P\ x}
|
16069
|
113 |
holds. Remember that on lists \isa{size} and \isa{length} are synonymous.
|
|
114 |
|
|
115 |
The proof itself is by rule induction and afterwards automatic:%
|
|
116 |
\end{isamarkuptxt}%
|
17175
|
117 |
\isamarkuptrue%
|
|
118 |
\isacommand{by}\isamarkupfalse%
|
40406
|
119 |
\ {\isaliteral{28}{\isacharparenleft}}rule\ S{\isaliteral{5F}{\isacharunderscore}}A{\isaliteral{5F}{\isacharunderscore}}B{\isaliteral{2E}{\isachardot}}induct{\isaliteral{2C}{\isacharcomma}}\ auto{\isaliteral{29}{\isacharparenright}}%
|
17056
|
120 |
\endisatagproof
|
|
121 |
{\isafoldproof}%
|
|
122 |
%
|
|
123 |
\isadelimproof
|
|
124 |
%
|
|
125 |
\endisadelimproof
|
11866
|
126 |
%
|
10236
|
127 |
\begin{isamarkuptext}%
|
|
128 |
\noindent
|
|
129 |
This may seem surprising at first, and is indeed an indication of the power
|
|
130 |
of inductive definitions. But it is also quite straightforward. For example,
|
|
131 |
consider the production $A \to b A A$: if $v,w \in A$ and the elements of $A$
|
10878
|
132 |
contain one more $a$ than~$b$'s, then $bvw$ must again contain one more $a$
|
|
133 |
than~$b$'s.
|
10236
|
134 |
|
|
135 |
As usual, the correctness of syntactic descriptions is easy, but completeness
|
|
136 |
is hard: does \isa{S} contain \emph{all} words with an equal number of
|
|
137 |
\isa{a}'s and \isa{b}'s? It turns out that this proof requires the
|
10878
|
138 |
following lemma: every string with two more \isa{a}'s than \isa{b}'s can be cut somewhere such that each half has one more \isa{a} than
|
10236
|
139 |
\isa{b}. This is best seen by imagining counting the difference between the
|
10283
|
140 |
number of \isa{a}'s and \isa{b}'s starting at the left end of the
|
|
141 |
word. We start with 0 and end (at the right end) with 2. Since each move to the
|
10236
|
142 |
right increases or decreases the difference by 1, we must have passed through
|
|
143 |
1 on our way from 0 to 2. Formally, we appeal to the following discrete
|
40406
|
144 |
intermediate value theorem \isa{nat{\isadigit{0}}{\isaliteral{5F}{\isacharunderscore}}intermed{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}val}
|
10236
|
145 |
\begin{isabelle}%
|
40406
|
146 |
\ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{3C}{\isacharless}}n{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6261723E}{\isasymbar}}f\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}\ f\ i{\isaliteral{5C3C6261723E}{\isasymbar}}\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\ f\ {\isadigit{0}}\ {\isaliteral{5C3C6C653E}{\isasymle}}\ k{\isaliteral{3B}{\isacharsemicolon}}\ k\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ n{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline
|
|
147 |
\isaindent{\ \ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}i{\isaliteral{5C3C6C653E}{\isasymle}}n{\isaliteral{2E}{\isachardot}}\ f\ i\ {\isaliteral{3D}{\isacharequal}}\ k%
|
10236
|
148 |
\end{isabelle}
|
40406
|
149 |
where \isa{f} is of type \isa{nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ int}, \isa{int} are the integers,
|
|
150 |
\isa{{\isaliteral{5C3C6261723E}{\isasymbar}}{\isaliteral{2E}{\isachardot}}{\isaliteral{5C3C6261723E}{\isasymbar}}} is the absolute value function\footnote{See
|
11308
|
151 |
Table~\ref{tab:ascii} in the Appendix for the correct \textsc{ascii}
|
11708
|
152 |
syntax.}, and \isa{{\isadigit{1}}} is the integer 1 (see \S\ref{sec:numbers}).
|
10236
|
153 |
|
11147
|
154 |
First we show that our specific function, the difference between the
|
10236
|
155 |
numbers of \isa{a}'s and \isa{b}'s, does indeed only change by 1 in every
|
|
156 |
move to the right. At this point we also start generalizing from \isa{a}'s
|
|
157 |
and \isa{b}'s to an arbitrary property \isa{P}. Otherwise we would have
|
|
158 |
to prove the desired lemma twice, once as stated above and once with the
|
|
159 |
roles of \isa{a}'s and \isa{b}'s interchanged.%
|
|
160 |
\end{isamarkuptext}%
|
17175
|
161 |
\isamarkuptrue%
|
|
162 |
\isacommand{lemma}\isamarkupfalse%
|
40406
|
163 |
\ step{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i\ {\isaliteral{3C}{\isacharless}}\ size\ w{\isaliteral{2E}{\isachardot}}\isanewline
|
|
164 |
\ \ {\isaliteral{5C3C6261723E}{\isasymbar}}{\isaliteral{28}{\isacharparenleft}}int{\isaliteral{28}{\isacharparenleft}}size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}take\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ w{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2D}{\isacharminus}}int{\isaliteral{28}{\isacharparenleft}}size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}take\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ w{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}P\ x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
|
|
165 |
\ \ \ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}int{\isaliteral{28}{\isacharparenleft}}size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}take\ i\ w{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2D}{\isacharminus}}int{\isaliteral{28}{\isacharparenleft}}size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}take\ i\ w{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}P\ x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6261723E}{\isasymbar}}\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}%
|
17056
|
166 |
\isadelimproof
|
|
167 |
%
|
|
168 |
\endisadelimproof
|
|
169 |
%
|
|
170 |
\isatagproof
|
16069
|
171 |
%
|
|
172 |
\begin{isamarkuptxt}%
|
|
173 |
\noindent
|
|
174 |
The lemma is a bit hard to read because of the coercion function
|
40406
|
175 |
\isa{int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ int}. It is required because \isa{size} returns
|
16069
|
176 |
a natural number, but subtraction on type~\isa{nat} will do the wrong thing.
|
|
177 |
Function \isa{take} is predefined and \isa{take\ i\ xs} is the prefix of
|
|
178 |
length \isa{i} of \isa{xs}; below we also need \isa{drop\ i\ xs}, which
|
|
179 |
is what remains after that prefix has been dropped from \isa{xs}.
|
|
180 |
|
|
181 |
The proof is by induction on \isa{w}, with a trivial base case, and a not
|
|
182 |
so trivial induction step. Since it is essentially just arithmetic, we do not
|
|
183 |
discuss it.%
|
|
184 |
\end{isamarkuptxt}%
|
17175
|
185 |
\isamarkuptrue%
|
|
186 |
\isacommand{apply}\isamarkupfalse%
|
40406
|
187 |
{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ w{\isaliteral{29}{\isacharparenright}}\isanewline
|
17175
|
188 |
\isacommand{apply}\isamarkupfalse%
|
40406
|
189 |
{\isaliteral{28}{\isacharparenleft}}auto\ simp\ add{\isaliteral{3A}{\isacharcolon}}\ abs{\isaliteral{5F}{\isacharunderscore}}if\ take{\isaliteral{5F}{\isacharunderscore}}Cons\ split{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{2E}{\isachardot}}split{\isaliteral{29}{\isacharparenright}}\isanewline
|
17175
|
190 |
\isacommand{done}\isamarkupfalse%
|
|
191 |
%
|
17056
|
192 |
\endisatagproof
|
|
193 |
{\isafoldproof}%
|
|
194 |
%
|
|
195 |
\isadelimproof
|
|
196 |
%
|
|
197 |
\endisadelimproof
|
11866
|
198 |
%
|
10236
|
199 |
\begin{isamarkuptext}%
|
11494
|
200 |
Finally we come to the above-mentioned lemma about cutting in half a word with two more elements of one sort than of the other sort:%
|
10236
|
201 |
\end{isamarkuptext}%
|
17175
|
202 |
\isamarkuptrue%
|
|
203 |
\isacommand{lemma}\isamarkupfalse%
|
40406
|
204 |
\ part{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\isanewline
|
|
205 |
\ {\isaliteral{22}{\isachardoublequoteopen}}size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}w{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}w{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}P\ x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2B}{\isacharplus}}{\isadigit{2}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\isanewline
|
|
206 |
\ \ {\isaliteral{5C3C6578697374733E}{\isasymexists}}i{\isaliteral{5C3C6C653E}{\isasymle}}size\ w{\isaliteral{2E}{\isachardot}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}take\ i\ w{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}take\ i\ w{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}P\ x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}%
|
17056
|
207 |
\isadelimproof
|
|
208 |
%
|
|
209 |
\endisadelimproof
|
|
210 |
%
|
|
211 |
\isatagproof
|
16069
|
212 |
%
|
|
213 |
\begin{isamarkuptxt}%
|
|
214 |
\noindent
|
|
215 |
This is proved by \isa{force} with the help of the intermediate value theorem,
|
|
216 |
instantiated appropriately and with its first premise disposed of by lemma
|
|
217 |
\isa{step{\isadigit{1}}}:%
|
|
218 |
\end{isamarkuptxt}%
|
17175
|
219 |
\isamarkuptrue%
|
|
220 |
\isacommand{apply}\isamarkupfalse%
|
40406
|
221 |
{\isaliteral{28}{\isacharparenleft}}insert\ nat{\isadigit{0}}{\isaliteral{5F}{\isacharunderscore}}intermed{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}val{\isaliteral{5B}{\isacharbrackleft}}OF\ step{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ of\ {\isaliteral{22}{\isachardoublequoteopen}}P{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}w{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline
|
17175
|
222 |
\isacommand{by}\isamarkupfalse%
|
|
223 |
\ force%
|
17056
|
224 |
\endisatagproof
|
|
225 |
{\isafoldproof}%
|
|
226 |
%
|
|
227 |
\isadelimproof
|
|
228 |
%
|
|
229 |
\endisadelimproof
|
11866
|
230 |
%
|
10236
|
231 |
\begin{isamarkuptext}%
|
|
232 |
\noindent
|
|
233 |
|
|
234 |
Lemma \isa{part{\isadigit{1}}} tells us only about the prefix \isa{take\ i\ w}.
|
10878
|
235 |
An easy lemma deals with the suffix \isa{drop\ i\ w}:%
|
10236
|
236 |
\end{isamarkuptext}%
|
17175
|
237 |
\isamarkuptrue%
|
|
238 |
\isacommand{lemma}\isamarkupfalse%
|
40406
|
239 |
\ part{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\isanewline
|
|
240 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}take\ i\ w\ {\isaliteral{40}{\isacharat}}\ drop\ i\ w{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
|
|
241 |
\ \ \ \ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}take\ i\ w\ {\isaliteral{40}{\isacharat}}\ drop\ i\ w{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}P\ x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2B}{\isacharplus}}{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
|
|
242 |
\ \ \ \ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}take\ i\ w{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}take\ i\ w{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}P\ x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline
|
|
243 |
\ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}drop\ i\ w{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}drop\ i\ w{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}P\ x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
17056
|
244 |
%
|
|
245 |
\isadelimproof
|
|
246 |
%
|
|
247 |
\endisadelimproof
|
|
248 |
%
|
|
249 |
\isatagproof
|
17175
|
250 |
\isacommand{by}\isamarkupfalse%
|
40406
|
251 |
{\isaliteral{28}{\isacharparenleft}}simp\ del{\isaliteral{3A}{\isacharcolon}}\ append{\isaliteral{5F}{\isacharunderscore}}take{\isaliteral{5F}{\isacharunderscore}}drop{\isaliteral{5F}{\isacharunderscore}}id{\isaliteral{29}{\isacharparenright}}%
|
17056
|
252 |
\endisatagproof
|
|
253 |
{\isafoldproof}%
|
|
254 |
%
|
|
255 |
\isadelimproof
|
|
256 |
%
|
|
257 |
\endisadelimproof
|
11866
|
258 |
%
|
10236
|
259 |
\begin{isamarkuptext}%
|
|
260 |
\noindent
|
11257
|
261 |
In the proof we have disabled the normally useful lemma
|
10878
|
262 |
\begin{isabelle}
|
40406
|
263 |
\isa{take\ n\ xs\ {\isaliteral{40}{\isacharat}}\ drop\ n\ xs\ {\isaliteral{3D}{\isacharequal}}\ xs}
|
10878
|
264 |
\rulename{append_take_drop_id}
|
|
265 |
\end{isabelle}
|
11257
|
266 |
to allow the simplifier to apply the following lemma instead:
|
|
267 |
\begin{isabelle}%
|
40406
|
268 |
\ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C696E3E}{\isasymin}}xs{\isaliteral{40}{\isacharat}}ys{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C696E3E}{\isasymin}}xs{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{40}{\isacharat}}\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C696E3E}{\isasymin}}ys{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{5D}{\isacharbrackright}}%
|
11257
|
269 |
\end{isabelle}
|
10236
|
270 |
|
|
271 |
To dispose of trivial cases automatically, the rules of the inductive
|
|
272 |
definition are declared simplification rules:%
|
|
273 |
\end{isamarkuptext}%
|
17175
|
274 |
\isamarkuptrue%
|
|
275 |
\isacommand{declare}\isamarkupfalse%
|
40406
|
276 |
\ S{\isaliteral{5F}{\isacharunderscore}}A{\isaliteral{5F}{\isacharunderscore}}B{\isaliteral{2E}{\isachardot}}intros{\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}%
|
10236
|
277 |
\begin{isamarkuptext}%
|
|
278 |
\noindent
|
|
279 |
This could have been done earlier but was not necessary so far.
|
|
280 |
|
|
281 |
The completeness theorem tells us that if a word has the same number of
|
10878
|
282 |
\isa{a}'s and \isa{b}'s, then it is in \isa{S}, and similarly
|
|
283 |
for \isa{A} and \isa{B}:%
|
10236
|
284 |
\end{isamarkuptext}%
|
17175
|
285 |
\isamarkuptrue%
|
|
286 |
\isacommand{theorem}\isamarkupfalse%
|
40406
|
287 |
\ completeness{\isaliteral{3A}{\isacharcolon}}\isanewline
|
|
288 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}w{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}a{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}w{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}b{\isaliteral{5D}{\isacharbrackright}}\ \ \ \ \ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ S{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\isanewline
|
|
289 |
\ \ \ {\isaliteral{28}{\isacharparenleft}}size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}w{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}a{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}w{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}b{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\isanewline
|
|
290 |
\ \ \ {\isaliteral{28}{\isacharparenleft}}size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}w{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}b{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ size{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}w{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}a{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ w\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
|
17056
|
291 |
\isadelimproof
|
|
292 |
%
|
|
293 |
\endisadelimproof
|
|
294 |
%
|
|
295 |
\isatagproof
|
16069
|
296 |
%
|
|
297 |
\begin{isamarkuptxt}%
|
|
298 |
\noindent
|
|
299 |
The proof is by induction on \isa{w}. Structural induction would fail here
|
|
300 |
because, as we can see from the grammar, we need to make bigger steps than
|
|
301 |
merely appending a single letter at the front. Hence we induct on the length
|
40406
|
302 |
of \isa{w}, using the induction rule \isa{length{\isaliteral{5F}{\isacharunderscore}}induct}:%
|
16069
|
303 |
\end{isamarkuptxt}%
|
17175
|
304 |
\isamarkuptrue%
|
|
305 |
\isacommand{apply}\isamarkupfalse%
|
40406
|
306 |
{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ w\ rule{\isaliteral{3A}{\isacharcolon}}\ length{\isaliteral{5F}{\isacharunderscore}}induct{\isaliteral{29}{\isacharparenright}}\isanewline
|
27167
|
307 |
\isacommand{apply}\isamarkupfalse%
|
40406
|
308 |
{\isaliteral{28}{\isacharparenleft}}rename{\isaliteral{5F}{\isacharunderscore}}tac\ w{\isaliteral{29}{\isacharparenright}}%
|
16069
|
309 |
\begin{isamarkuptxt}%
|
|
310 |
\noindent
|
40406
|
311 |
The \isa{rule} parameter tells \isa{induct{\isaliteral{5F}{\isacharunderscore}}tac} explicitly which induction
|
16069
|
312 |
rule to use. For details see \S\ref{sec:complete-ind} below.
|
|
313 |
In this case the result is that we may assume the lemma already
|
27167
|
314 |
holds for all words shorter than \isa{w}. Because the induction step renames
|
|
315 |
the induction variable we rename it back to \isa{w}.
|
16069
|
316 |
|
|
317 |
The proof continues with a case distinction on \isa{w},
|
|
318 |
on whether \isa{w} is empty or not.%
|
|
319 |
\end{isamarkuptxt}%
|
17175
|
320 |
\isamarkuptrue%
|
|
321 |
\isacommand{apply}\isamarkupfalse%
|
40406
|
322 |
{\isaliteral{28}{\isacharparenleft}}case{\isaliteral{5F}{\isacharunderscore}}tac\ w{\isaliteral{29}{\isacharparenright}}\isanewline
|
17175
|
323 |
\ \isacommand{apply}\isamarkupfalse%
|
40406
|
324 |
{\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{29}{\isacharparenright}}%
|
16069
|
325 |
\begin{isamarkuptxt}%
|
|
326 |
\noindent
|
|
327 |
Simplification disposes of the base case and leaves only a conjunction
|
|
328 |
of two step cases to be proved:
|
40406
|
329 |
if \isa{w\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{23}{\isacharhash}}\ v} and \begin{isabelle}%
|
|
330 |
\ \ \ \ \ length\ {\isaliteral{28}{\isacharparenleft}}if\ x\ {\isaliteral{3D}{\isacharequal}}\ a\ then\ {\isaliteral{5B}{\isacharbrackleft}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ v{\isaliteral{5D}{\isacharbrackright}}\ else\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
|
|
331 |
\isaindent{\ \ \ \ \ }length\ {\isaliteral{28}{\isacharparenleft}}if\ x\ {\isaliteral{3D}{\isacharequal}}\ b\ then\ {\isaliteral{5B}{\isacharbrackleft}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ v{\isaliteral{5D}{\isacharbrackright}}\ else\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}%
|
16069
|
332 |
\end{isabelle} then
|
40406
|
333 |
\isa{b\ {\isaliteral{23}{\isacharhash}}\ v\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A}, and similarly for \isa{w\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{23}{\isacharhash}}\ v}.
|
16069
|
334 |
We only consider the first case in detail.
|
|
335 |
|
|
336 |
After breaking the conjunction up into two cases, we can apply
|
|
337 |
\isa{part{\isadigit{1}}} to the assumption that \isa{w} contains two more \isa{a}'s than \isa{b}'s.%
|
|
338 |
\end{isamarkuptxt}%
|
17175
|
339 |
\isamarkuptrue%
|
|
340 |
\isacommand{apply}\isamarkupfalse%
|
40406
|
341 |
{\isaliteral{28}{\isacharparenleft}}rule\ conjI{\isaliteral{29}{\isacharparenright}}\isanewline
|
17175
|
342 |
\ \isacommand{apply}\isamarkupfalse%
|
40406
|
343 |
{\isaliteral{28}{\isacharparenleft}}clarify{\isaliteral{29}{\isacharparenright}}\isanewline
|
17175
|
344 |
\ \isacommand{apply}\isamarkupfalse%
|
40406
|
345 |
{\isaliteral{28}{\isacharparenleft}}frule\ part{\isadigit{1}}{\isaliteral{5B}{\isacharbrackleft}}of\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}a{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{2C}{\isacharcomma}}\ simplified{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline
|
17175
|
346 |
\ \isacommand{apply}\isamarkupfalse%
|
40406
|
347 |
{\isaliteral{28}{\isacharparenleft}}clarify{\isaliteral{29}{\isacharparenright}}%
|
16069
|
348 |
\begin{isamarkuptxt}%
|
|
349 |
\noindent
|
40406
|
350 |
This yields an index \isa{i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ length\ v} such that
|
16069
|
351 |
\begin{isabelle}%
|
40406
|
352 |
\ \ \ \ \ length\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}take\ i\ v\ {\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ length\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}take\ i\ v\ {\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}%
|
16069
|
353 |
\end{isabelle}
|
|
354 |
With the help of \isa{part{\isadigit{2}}} it follows that
|
|
355 |
\begin{isabelle}%
|
40406
|
356 |
\ \ \ \ \ length\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}drop\ i\ v\ {\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ length\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}drop\ i\ v\ {\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}%
|
16069
|
357 |
\end{isabelle}%
|
|
358 |
\end{isamarkuptxt}%
|
17175
|
359 |
\isamarkuptrue%
|
|
360 |
\ \isacommand{apply}\isamarkupfalse%
|
40406
|
361 |
{\isaliteral{28}{\isacharparenleft}}drule\ part{\isadigit{2}}{\isaliteral{5B}{\isacharbrackleft}}of\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}a{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{2C}{\isacharcomma}}\ simplified{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline
|
17175
|
362 |
\ \ \isacommand{apply}\isamarkupfalse%
|
40406
|
363 |
{\isaliteral{28}{\isacharparenleft}}assumption{\isaliteral{29}{\isacharparenright}}%
|
16069
|
364 |
\begin{isamarkuptxt}%
|
|
365 |
\noindent
|
40406
|
366 |
Now it is time to decompose \isa{v} in the conclusion \isa{b\ {\isaliteral{23}{\isacharhash}}\ v\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A}
|
|
367 |
into \isa{take\ i\ v\ {\isaliteral{40}{\isacharat}}\ drop\ i\ v},%
|
16069
|
368 |
\end{isamarkuptxt}%
|
17175
|
369 |
\isamarkuptrue%
|
|
370 |
\ \isacommand{apply}\isamarkupfalse%
|
40406
|
371 |
{\isaliteral{28}{\isacharparenleft}}rule{\isaliteral{5F}{\isacharunderscore}}tac\ n{\isadigit{1}}{\isaliteral{3D}{\isacharequal}}i\ \isakeyword{and}\ t{\isaliteral{3D}{\isacharequal}}v\ \isakeyword{in}\ subst{\isaliteral{5B}{\isacharbrackleft}}OF\ append{\isaliteral{5F}{\isacharunderscore}}take{\isaliteral{5F}{\isacharunderscore}}drop{\isaliteral{5F}{\isacharunderscore}}id{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}%
|
16069
|
372 |
\begin{isamarkuptxt}%
|
|
373 |
\noindent
|
|
374 |
(the variables \isa{n{\isadigit{1}}} and \isa{t} are the result of composing the
|
40406
|
375 |
theorems \isa{subst} and \isa{append{\isaliteral{5F}{\isacharunderscore}}take{\isaliteral{5F}{\isacharunderscore}}drop{\isaliteral{5F}{\isacharunderscore}}id})
|
16069
|
376 |
after which the appropriate rule of the grammar reduces the goal
|
40406
|
377 |
to the two subgoals \isa{take\ i\ v\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A} and \isa{drop\ i\ v\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A}:%
|
16069
|
378 |
\end{isamarkuptxt}%
|
17175
|
379 |
\isamarkuptrue%
|
|
380 |
\ \isacommand{apply}\isamarkupfalse%
|
40406
|
381 |
{\isaliteral{28}{\isacharparenleft}}rule\ S{\isaliteral{5F}{\isacharunderscore}}A{\isaliteral{5F}{\isacharunderscore}}B{\isaliteral{2E}{\isachardot}}intros{\isaliteral{29}{\isacharparenright}}%
|
16069
|
382 |
\begin{isamarkuptxt}%
|
|
383 |
Both subgoals follow from the induction hypothesis because both \isa{take\ i\ v} and \isa{drop\ i\ v} are shorter than \isa{w}:%
|
|
384 |
\end{isamarkuptxt}%
|
17175
|
385 |
\isamarkuptrue%
|
|
386 |
\ \ \isacommand{apply}\isamarkupfalse%
|
40406
|
387 |
{\isaliteral{28}{\isacharparenleft}}force\ simp\ add{\isaliteral{3A}{\isacharcolon}}\ min{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}iff{\isaliteral{5F}{\isacharunderscore}}disj{\isaliteral{29}{\isacharparenright}}\isanewline
|
17175
|
388 |
\ \isacommand{apply}\isamarkupfalse%
|
40406
|
389 |
{\isaliteral{28}{\isacharparenleft}}force\ split\ add{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{5F}{\isacharunderscore}}diff{\isaliteral{5F}{\isacharunderscore}}split{\isaliteral{29}{\isacharparenright}}%
|
16069
|
390 |
\begin{isamarkuptxt}%
|
40406
|
391 |
The case \isa{w\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{23}{\isacharhash}}\ v} is proved analogously:%
|
16069
|
392 |
\end{isamarkuptxt}%
|
17175
|
393 |
\isamarkuptrue%
|
|
394 |
\isacommand{apply}\isamarkupfalse%
|
40406
|
395 |
{\isaliteral{28}{\isacharparenleft}}clarify{\isaliteral{29}{\isacharparenright}}\isanewline
|
17175
|
396 |
\isacommand{apply}\isamarkupfalse%
|
40406
|
397 |
{\isaliteral{28}{\isacharparenleft}}frule\ part{\isadigit{1}}{\isaliteral{5B}{\isacharbrackleft}}of\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}b{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{2C}{\isacharcomma}}\ simplified{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline
|
17175
|
398 |
\isacommand{apply}\isamarkupfalse%
|
40406
|
399 |
{\isaliteral{28}{\isacharparenleft}}clarify{\isaliteral{29}{\isacharparenright}}\isanewline
|
17175
|
400 |
\isacommand{apply}\isamarkupfalse%
|
40406
|
401 |
{\isaliteral{28}{\isacharparenleft}}drule\ part{\isadigit{2}}{\isaliteral{5B}{\isacharbrackleft}}of\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}b{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{2C}{\isacharcomma}}\ simplified{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline
|
17175
|
402 |
\ \isacommand{apply}\isamarkupfalse%
|
40406
|
403 |
{\isaliteral{28}{\isacharparenleft}}assumption{\isaliteral{29}{\isacharparenright}}\isanewline
|
17175
|
404 |
\isacommand{apply}\isamarkupfalse%
|
40406
|
405 |
{\isaliteral{28}{\isacharparenleft}}rule{\isaliteral{5F}{\isacharunderscore}}tac\ n{\isadigit{1}}{\isaliteral{3D}{\isacharequal}}i\ \isakeyword{and}\ t{\isaliteral{3D}{\isacharequal}}v\ \isakeyword{in}\ subst{\isaliteral{5B}{\isacharbrackleft}}OF\ append{\isaliteral{5F}{\isacharunderscore}}take{\isaliteral{5F}{\isacharunderscore}}drop{\isaliteral{5F}{\isacharunderscore}}id{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline
|
17175
|
406 |
\isacommand{apply}\isamarkupfalse%
|
40406
|
407 |
{\isaliteral{28}{\isacharparenleft}}rule\ S{\isaliteral{5F}{\isacharunderscore}}A{\isaliteral{5F}{\isacharunderscore}}B{\isaliteral{2E}{\isachardot}}intros{\isaliteral{29}{\isacharparenright}}\isanewline
|
17175
|
408 |
\ \isacommand{apply}\isamarkupfalse%
|
40406
|
409 |
{\isaliteral{28}{\isacharparenleft}}force\ simp\ add{\isaliteral{3A}{\isacharcolon}}\ min{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}iff{\isaliteral{5F}{\isacharunderscore}}disj{\isaliteral{29}{\isacharparenright}}\isanewline
|
17175
|
410 |
\isacommand{by}\isamarkupfalse%
|
40406
|
411 |
{\isaliteral{28}{\isacharparenleft}}force\ simp\ add{\isaliteral{3A}{\isacharcolon}}\ min{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}iff{\isaliteral{5F}{\isacharunderscore}}disj\ split\ add{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{5F}{\isacharunderscore}}diff{\isaliteral{5F}{\isacharunderscore}}split{\isaliteral{29}{\isacharparenright}}%
|
17056
|
412 |
\endisatagproof
|
|
413 |
{\isafoldproof}%
|
|
414 |
%
|
|
415 |
\isadelimproof
|
|
416 |
%
|
|
417 |
\endisadelimproof
|
11866
|
418 |
%
|
10236
|
419 |
\begin{isamarkuptext}%
|
10878
|
420 |
We conclude this section with a comparison of our proof with
|
11494
|
421 |
Hopcroft\index{Hopcroft, J. E.} and Ullman's\index{Ullman, J. D.}
|
|
422 |
\cite[p.\ts81]{HopcroftUllman}.
|
|
423 |
For a start, the textbook
|
11257
|
424 |
grammar, for no good reason, excludes the empty word, thus complicating
|
|
425 |
matters just a little bit: they have 8 instead of our 7 productions.
|
10236
|
426 |
|
11158
|
427 |
More importantly, the proof itself is different: rather than
|
|
428 |
separating the two directions, they perform one induction on the
|
|
429 |
length of a word. This deprives them of the beauty of rule induction,
|
|
430 |
and in the easy direction (correctness) their reasoning is more
|
|
431 |
detailed than our \isa{auto}. For the hard part (completeness), they
|
40406
|
432 |
consider just one of the cases that our \isa{simp{\isaliteral{5F}{\isacharunderscore}}all} disposes of
|
11158
|
433 |
automatically. Then they conclude the proof by saying about the
|
|
434 |
remaining cases: ``We do this in a manner similar to our method of
|
|
435 |
proof for part (1); this part is left to the reader''. But this is
|
|
436 |
precisely the part that requires the intermediate value theorem and
|
|
437 |
thus is not at all similar to the other cases (which are automatic in
|
|
438 |
Isabelle). The authors are at least cavalier about this point and may
|
|
439 |
even have overlooked the slight difficulty lurking in the omitted
|
11494
|
440 |
cases. Such errors are found in many pen-and-paper proofs when they
|
|
441 |
are scrutinized formally.%
|
|
442 |
\index{grammars!defining inductively|)}%
|
10236
|
443 |
\end{isamarkuptext}%
|
17175
|
444 |
\isamarkuptrue%
|
17056
|
445 |
%
|
|
446 |
\isadelimtheory
|
|
447 |
%
|
|
448 |
\endisadelimtheory
|
|
449 |
%
|
|
450 |
\isatagtheory
|
|
451 |
%
|
|
452 |
\endisatagtheory
|
|
453 |
{\isafoldtheory}%
|
|
454 |
%
|
|
455 |
\isadelimtheory
|
|
456 |
%
|
|
457 |
\endisadelimtheory
|
10217
|
458 |
\end{isabellebody}%
|
|
459 |
%%% Local Variables:
|
|
460 |
%%% mode: latex
|
|
461 |
%%% TeX-master: "root"
|
|
462 |
%%% End:
|