1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{AB}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 % |
|
18 \isamarkupsection{Case Study: A Context Free Grammar% |
|
19 } |
|
20 \isamarkuptrue% |
|
21 % |
|
22 \begin{isamarkuptext}% |
|
23 \label{sec:CFG} |
|
24 \index{grammars!defining inductively|(}% |
|
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 \] |
|
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: |
|
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} |
|
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. |
|
39 |
|
40 We start by fixing the alphabet, which consists only of \isa{a}'s |
|
41 and~\isa{b}'s:% |
|
42 \end{isamarkuptext}% |
|
43 \isamarkuptrue% |
|
44 \isacommand{datatype}\isamarkupfalse% |
|
45 \ alfa\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{7C}{\isacharbar}}\ b% |
|
46 \begin{isamarkuptext}% |
|
47 \noindent |
|
48 For convenience we include the following easy lemmas as simplification rules:% |
|
49 \end{isamarkuptext}% |
|
50 \isamarkuptrue% |
|
51 \isacommand{lemma}\isamarkupfalse% |
|
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 |
|
53 % |
|
54 \isadelimproof |
|
55 % |
|
56 \endisadelimproof |
|
57 % |
|
58 \isatagproof |
|
59 \isacommand{by}\isamarkupfalse% |
|
60 \ {\isaliteral{28}{\isacharparenleft}}case{\isaliteral{5F}{\isacharunderscore}}tac\ x{\isaliteral{2C}{\isacharcomma}}\ auto{\isaliteral{29}{\isacharparenright}}% |
|
61 \endisatagproof |
|
62 {\isafoldproof}% |
|
63 % |
|
64 \isadelimproof |
|
65 % |
|
66 \endisadelimproof |
|
67 % |
|
68 \begin{isamarkuptext}% |
|
69 \noindent |
|
70 Words over this alphabet are of type \isa{alfa\ list}, and |
|
71 the three nonterminals are declared as sets of such words. |
|
72 The productions above are recast as a \emph{mutual} inductive |
|
73 definition\index{inductive definition!simultaneous} |
|
74 of \isa{S}, \isa{A} and~\isa{B}:% |
|
75 \end{isamarkuptext}% |
|
76 \isamarkuptrue% |
|
77 \isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse% |
|
78 \isanewline |
|
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 |
|
82 \isakeyword{where}\isanewline |
|
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 |
|
86 \isanewline |
|
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 |
|
89 \isanewline |
|
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}}% |
|
92 \begin{isamarkuptext}% |
|
93 \noindent |
|
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 |
|
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}.% |
|
97 \end{isamarkuptext}% |
|
98 \isamarkuptrue% |
|
99 \isacommand{lemma}\isamarkupfalse% |
|
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}}% |
|
104 \isadelimproof |
|
105 % |
|
106 \endisadelimproof |
|
107 % |
|
108 \isatagproof |
|
109 % |
|
110 \begin{isamarkuptxt}% |
|
111 \noindent |
|
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} |
|
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}% |
|
117 \isamarkuptrue% |
|
118 \isacommand{by}\isamarkupfalse% |
|
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}}% |
|
120 \endisatagproof |
|
121 {\isafoldproof}% |
|
122 % |
|
123 \isadelimproof |
|
124 % |
|
125 \endisadelimproof |
|
126 % |
|
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$ |
|
132 contain one more $a$ than~$b$'s, then $bvw$ must again contain one more $a$ |
|
133 than~$b$'s. |
|
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 |
|
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 |
|
139 \isa{b}. This is best seen by imagining counting the difference between the |
|
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 |
|
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 |
|
144 intermediate value theorem \isa{nat{\isadigit{0}}{\isaliteral{5F}{\isacharunderscore}}intermed{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}val} |
|
145 \begin{isabelle}% |
|
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% |
|
148 \end{isabelle} |
|
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 |
|
151 Table~\ref{tab:ascii} in the Appendix for the correct \textsc{ascii} |
|
152 syntax.}, and \isa{{\isadigit{1}}} is the integer 1 (see \S\ref{sec:numbers}). |
|
153 |
|
154 First we show that our specific function, the difference between the |
|
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}% |
|
161 \isamarkuptrue% |
|
162 \isacommand{lemma}\isamarkupfalse% |
|
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}}% |
|
166 \isadelimproof |
|
167 % |
|
168 \endisadelimproof |
|
169 % |
|
170 \isatagproof |
|
171 % |
|
172 \begin{isamarkuptxt}% |
|
173 \noindent |
|
174 The lemma is a bit hard to read because of the coercion function |
|
175 \isa{int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ int}. It is required because \isa{size} returns |
|
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}% |
|
185 \isamarkuptrue% |
|
186 \isacommand{apply}\isamarkupfalse% |
|
187 {\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ w{\isaliteral{29}{\isacharparenright}}\isanewline |
|
188 \isacommand{apply}\isamarkupfalse% |
|
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 |
|
190 \isacommand{done}\isamarkupfalse% |
|
191 % |
|
192 \endisatagproof |
|
193 {\isafoldproof}% |
|
194 % |
|
195 \isadelimproof |
|
196 % |
|
197 \endisadelimproof |
|
198 % |
|
199 \begin{isamarkuptext}% |
|
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:% |
|
201 \end{isamarkuptext}% |
|
202 \isamarkuptrue% |
|
203 \isacommand{lemma}\isamarkupfalse% |
|
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}}% |
|
207 \isadelimproof |
|
208 % |
|
209 \endisadelimproof |
|
210 % |
|
211 \isatagproof |
|
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}% |
|
219 \isamarkuptrue% |
|
220 \isacommand{apply}\isamarkupfalse% |
|
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 |
|
222 \isacommand{by}\isamarkupfalse% |
|
223 \ force% |
|
224 \endisatagproof |
|
225 {\isafoldproof}% |
|
226 % |
|
227 \isadelimproof |
|
228 % |
|
229 \endisadelimproof |
|
230 % |
|
231 \begin{isamarkuptext}% |
|
232 \noindent |
|
233 |
|
234 Lemma \isa{part{\isadigit{1}}} tells us only about the prefix \isa{take\ i\ w}. |
|
235 An easy lemma deals with the suffix \isa{drop\ i\ w}:% |
|
236 \end{isamarkuptext}% |
|
237 \isamarkuptrue% |
|
238 \isacommand{lemma}\isamarkupfalse% |
|
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 |
|
244 % |
|
245 \isadelimproof |
|
246 % |
|
247 \endisadelimproof |
|
248 % |
|
249 \isatagproof |
|
250 \isacommand{by}\isamarkupfalse% |
|
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}}% |
|
252 \endisatagproof |
|
253 {\isafoldproof}% |
|
254 % |
|
255 \isadelimproof |
|
256 % |
|
257 \endisadelimproof |
|
258 % |
|
259 \begin{isamarkuptext}% |
|
260 \noindent |
|
261 In the proof we have disabled the normally useful lemma |
|
262 \begin{isabelle} |
|
263 \isa{take\ n\ xs\ {\isaliteral{40}{\isacharat}}\ drop\ n\ xs\ {\isaliteral{3D}{\isacharequal}}\ xs} |
|
264 \rulename{append_take_drop_id} |
|
265 \end{isabelle} |
|
266 to allow the simplifier to apply the following lemma instead: |
|
267 \begin{isabelle}% |
|
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}}% |
|
269 \end{isabelle} |
|
270 |
|
271 To dispose of trivial cases automatically, the rules of the inductive |
|
272 definition are declared simplification rules:% |
|
273 \end{isamarkuptext}% |
|
274 \isamarkuptrue% |
|
275 \isacommand{declare}\isamarkupfalse% |
|
276 \ S{\isaliteral{5F}{\isacharunderscore}}A{\isaliteral{5F}{\isacharunderscore}}B{\isaliteral{2E}{\isachardot}}intros{\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}% |
|
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 |
|
282 \isa{a}'s and \isa{b}'s, then it is in \isa{S}, and similarly |
|
283 for \isa{A} and \isa{B}:% |
|
284 \end{isamarkuptext}% |
|
285 \isamarkuptrue% |
|
286 \isacommand{theorem}\isamarkupfalse% |
|
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}}% |
|
291 \isadelimproof |
|
292 % |
|
293 \endisadelimproof |
|
294 % |
|
295 \isatagproof |
|
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 |
|
302 of \isa{w}, using the induction rule \isa{length{\isaliteral{5F}{\isacharunderscore}}induct}:% |
|
303 \end{isamarkuptxt}% |
|
304 \isamarkuptrue% |
|
305 \isacommand{apply}\isamarkupfalse% |
|
306 {\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ w\ rule{\isaliteral{3A}{\isacharcolon}}\ length{\isaliteral{5F}{\isacharunderscore}}induct{\isaliteral{29}{\isacharparenright}}\isanewline |
|
307 \isacommand{apply}\isamarkupfalse% |
|
308 {\isaliteral{28}{\isacharparenleft}}rename{\isaliteral{5F}{\isacharunderscore}}tac\ w{\isaliteral{29}{\isacharparenright}}% |
|
309 \begin{isamarkuptxt}% |
|
310 \noindent |
|
311 The \isa{rule} parameter tells \isa{induct{\isaliteral{5F}{\isacharunderscore}}tac} explicitly which induction |
|
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 |
|
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}. |
|
316 |
|
317 The proof continues with a case distinction on \isa{w}, |
|
318 on whether \isa{w} is empty or not.% |
|
319 \end{isamarkuptxt}% |
|
320 \isamarkuptrue% |
|
321 \isacommand{apply}\isamarkupfalse% |
|
322 {\isaliteral{28}{\isacharparenleft}}case{\isaliteral{5F}{\isacharunderscore}}tac\ w{\isaliteral{29}{\isacharparenright}}\isanewline |
|
323 \ \isacommand{apply}\isamarkupfalse% |
|
324 {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{29}{\isacharparenright}}% |
|
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: |
|
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}}% |
|
332 \end{isabelle} then |
|
333 \isa{b\ {\isaliteral{23}{\isacharhash}}\ v\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A}, and similarly for \isa{w\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{23}{\isacharhash}}\ v}. |
|
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}% |
|
339 \isamarkuptrue% |
|
340 \isacommand{apply}\isamarkupfalse% |
|
341 {\isaliteral{28}{\isacharparenleft}}rule\ conjI{\isaliteral{29}{\isacharparenright}}\isanewline |
|
342 \ \isacommand{apply}\isamarkupfalse% |
|
343 {\isaliteral{28}{\isacharparenleft}}clarify{\isaliteral{29}{\isacharparenright}}\isanewline |
|
344 \ \isacommand{apply}\isamarkupfalse% |
|
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 |
|
346 \ \isacommand{apply}\isamarkupfalse% |
|
347 {\isaliteral{28}{\isacharparenleft}}clarify{\isaliteral{29}{\isacharparenright}}% |
|
348 \begin{isamarkuptxt}% |
|
349 \noindent |
|
350 This yields an index \isa{i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ length\ v} such that |
|
351 \begin{isabelle}% |
|
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}}% |
|
353 \end{isabelle} |
|
354 With the help of \isa{part{\isadigit{2}}} it follows that |
|
355 \begin{isabelle}% |
|
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}}% |
|
357 \end{isabelle}% |
|
358 \end{isamarkuptxt}% |
|
359 \isamarkuptrue% |
|
360 \ \isacommand{apply}\isamarkupfalse% |
|
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 |
|
362 \ \ \isacommand{apply}\isamarkupfalse% |
|
363 {\isaliteral{28}{\isacharparenleft}}assumption{\isaliteral{29}{\isacharparenright}}% |
|
364 \begin{isamarkuptxt}% |
|
365 \noindent |
|
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},% |
|
368 \end{isamarkuptxt}% |
|
369 \isamarkuptrue% |
|
370 \ \isacommand{apply}\isamarkupfalse% |
|
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}}% |
|
372 \begin{isamarkuptxt}% |
|
373 \noindent |
|
374 (the variables \isa{n{\isadigit{1}}} and \isa{t} are the result of composing the |
|
375 theorems \isa{subst} and \isa{append{\isaliteral{5F}{\isacharunderscore}}take{\isaliteral{5F}{\isacharunderscore}}drop{\isaliteral{5F}{\isacharunderscore}}id}) |
|
376 after which the appropriate rule of the grammar reduces the goal |
|
377 to the two subgoals \isa{take\ i\ v\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A} and \isa{drop\ i\ v\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A}:% |
|
378 \end{isamarkuptxt}% |
|
379 \isamarkuptrue% |
|
380 \ \isacommand{apply}\isamarkupfalse% |
|
381 {\isaliteral{28}{\isacharparenleft}}rule\ S{\isaliteral{5F}{\isacharunderscore}}A{\isaliteral{5F}{\isacharunderscore}}B{\isaliteral{2E}{\isachardot}}intros{\isaliteral{29}{\isacharparenright}}% |
|
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}% |
|
385 \isamarkuptrue% |
|
386 \ \ \isacommand{apply}\isamarkupfalse% |
|
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 |
|
388 \ \isacommand{apply}\isamarkupfalse% |
|
389 {\isaliteral{28}{\isacharparenleft}}force\ split\ add{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{5F}{\isacharunderscore}}diff{\isaliteral{5F}{\isacharunderscore}}split{\isaliteral{29}{\isacharparenright}}% |
|
390 \begin{isamarkuptxt}% |
|
391 The case \isa{w\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{23}{\isacharhash}}\ v} is proved analogously:% |
|
392 \end{isamarkuptxt}% |
|
393 \isamarkuptrue% |
|
394 \isacommand{apply}\isamarkupfalse% |
|
395 {\isaliteral{28}{\isacharparenleft}}clarify{\isaliteral{29}{\isacharparenright}}\isanewline |
|
396 \isacommand{apply}\isamarkupfalse% |
|
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 |
|
398 \isacommand{apply}\isamarkupfalse% |
|
399 {\isaliteral{28}{\isacharparenleft}}clarify{\isaliteral{29}{\isacharparenright}}\isanewline |
|
400 \isacommand{apply}\isamarkupfalse% |
|
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 |
|
402 \ \isacommand{apply}\isamarkupfalse% |
|
403 {\isaliteral{28}{\isacharparenleft}}assumption{\isaliteral{29}{\isacharparenright}}\isanewline |
|
404 \isacommand{apply}\isamarkupfalse% |
|
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 |
|
406 \isacommand{apply}\isamarkupfalse% |
|
407 {\isaliteral{28}{\isacharparenleft}}rule\ S{\isaliteral{5F}{\isacharunderscore}}A{\isaliteral{5F}{\isacharunderscore}}B{\isaliteral{2E}{\isachardot}}intros{\isaliteral{29}{\isacharparenright}}\isanewline |
|
408 \ \isacommand{apply}\isamarkupfalse% |
|
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 |
|
410 \isacommand{by}\isamarkupfalse% |
|
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}}% |
|
412 \endisatagproof |
|
413 {\isafoldproof}% |
|
414 % |
|
415 \isadelimproof |
|
416 % |
|
417 \endisadelimproof |
|
418 % |
|
419 \begin{isamarkuptext}% |
|
420 We conclude this section with a comparison of our proof with |
|
421 Hopcroft\index{Hopcroft, J. E.} and Ullman's\index{Ullman, J. D.} |
|
422 \cite[p.\ts81]{HopcroftUllman}. |
|
423 For a start, the textbook |
|
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. |
|
426 |
|
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 |
|
432 consider just one of the cases that our \isa{simp{\isaliteral{5F}{\isacharunderscore}}all} disposes of |
|
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 |
|
440 cases. Such errors are found in many pen-and-paper proofs when they |
|
441 are scrutinized formally.% |
|
442 \index{grammars!defining inductively|)}% |
|
443 \end{isamarkuptext}% |
|
444 \isamarkuptrue% |
|
445 % |
|
446 \isadelimtheory |
|
447 % |
|
448 \endisadelimtheory |
|
449 % |
|
450 \isatagtheory |
|
451 % |
|
452 \endisatagtheory |
|
453 {\isafoldtheory}% |
|
454 % |
|
455 \isadelimtheory |
|
456 % |
|
457 \endisadelimtheory |
|
458 \end{isabellebody}% |
|
459 %%% Local Variables: |
|
460 %%% mode: latex |
|
461 %%% TeX-master: "root" |
|
462 %%% End: |
|