5 \isamarkupsection{Case Study: A Context Free Grammar% |
5 \isamarkupsection{Case Study: A Context Free Grammar% |
6 } |
6 } |
7 % |
7 % |
8 \begin{isamarkuptext}% |
8 \begin{isamarkuptext}% |
9 \label{sec:CFG} |
9 \label{sec:CFG} |
|
10 \index{grammars!defining inductively|(}% |
10 Grammars are nothing but shorthands for inductive definitions of nonterminals |
11 Grammars are nothing but shorthands for inductive definitions of nonterminals |
11 which represent sets of strings. For example, the production |
12 which represent sets of strings. For example, the production |
12 $A \to B c$ is short for |
13 $A \to B c$ is short for |
13 \[ w \in B \Longrightarrow wc \in A \] |
14 \[ w \in B \Longrightarrow wc \in A \] |
14 This section demonstrates this idea with an example |
15 This section demonstrates this idea with an example |
127 \end{isamarkuptxt}% |
128 \end{isamarkuptxt}% |
128 \isacommand{apply}{\isacharparenleft}induct\ w{\isacharparenright}\isanewline |
129 \isacommand{apply}{\isacharparenleft}induct\ w{\isacharparenright}\isanewline |
129 \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
130 \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
130 \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}zabs{\isacharunderscore}def\ take{\isacharunderscore}Cons\ split{\isacharcolon}nat{\isachardot}split\ if{\isacharunderscore}splits{\isacharparenright}% |
131 \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}zabs{\isacharunderscore}def\ take{\isacharunderscore}Cons\ split{\isacharcolon}nat{\isachardot}split\ if{\isacharunderscore}splits{\isacharparenright}% |
131 \begin{isamarkuptext}% |
132 \begin{isamarkuptext}% |
132 Finally we come to the above mentioned lemma about cutting in half a word with two |
133 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:% |
133 more elements of one sort than of the other sort:% |
|
134 \end{isamarkuptext}% |
134 \end{isamarkuptext}% |
135 \isacommand{lemma}\ part{\isadigit{1}}{\isacharcolon}\isanewline |
135 \isacommand{lemma}\ part{\isadigit{1}}{\isacharcolon}\isanewline |
136 \ {\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 |
136 \ {\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 |
137 \ \ {\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}% |
137 \ \ {\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}% |
138 \begin{isamarkuptxt}% |
138 \begin{isamarkuptxt}% |
197 rule to use. For details see \S\ref{sec:complete-ind} below. |
197 rule to use. For details see \S\ref{sec:complete-ind} below. |
198 In this case the result is that we may assume the lemma already |
198 In this case the result is that we may assume the lemma already |
199 holds for all words shorter than \isa{w}. |
199 holds for all words shorter than \isa{w}. |
200 |
200 |
201 The proof continues with a case distinction on \isa{w}, |
201 The proof continues with a case distinction on \isa{w}, |
202 i.e.\ if \isa{w} is empty or not.% |
202 on whether \isa{w} is empty or not.% |
203 \end{isamarkuptxt}% |
203 \end{isamarkuptxt}% |
204 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ w{\isacharparenright}\isanewline |
204 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ w{\isacharparenright}\isanewline |
205 \ \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}% |
205 \ \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}% |
206 \begin{isamarkuptxt}% |
206 \begin{isamarkuptxt}% |
207 \noindent |
207 \noindent |
264 \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isanewline |
264 \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isanewline |
265 \ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline |
265 \ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline |
266 \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}% |
266 \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}% |
267 \begin{isamarkuptext}% |
267 \begin{isamarkuptext}% |
268 We conclude this section with a comparison of our proof with |
268 We conclude this section with a comparison of our proof with |
269 Hopcroft and Ullman's \cite[p.\ts81]{HopcroftUllman}. For a start, the textbook |
269 Hopcroft\index{Hopcroft, J. E.} and Ullman's\index{Ullman, J. D.} |
|
270 \cite[p.\ts81]{HopcroftUllman}. |
|
271 For a start, the textbook |
270 grammar, for no good reason, excludes the empty word, thus complicating |
272 grammar, for no good reason, excludes the empty word, thus complicating |
271 matters just a little bit: they have 8 instead of our 7 productions. |
273 matters just a little bit: they have 8 instead of our 7 productions. |
272 |
274 |
273 More importantly, the proof itself is different: rather than |
275 More importantly, the proof itself is different: rather than |
274 separating the two directions, they perform one induction on the |
276 separating the two directions, they perform one induction on the |
281 proof for part (1); this part is left to the reader''. But this is |
283 proof for part (1); this part is left to the reader''. But this is |
282 precisely the part that requires the intermediate value theorem and |
284 precisely the part that requires the intermediate value theorem and |
283 thus is not at all similar to the other cases (which are automatic in |
285 thus is not at all similar to the other cases (which are automatic in |
284 Isabelle). The authors are at least cavalier about this point and may |
286 Isabelle). The authors are at least cavalier about this point and may |
285 even have overlooked the slight difficulty lurking in the omitted |
287 even have overlooked the slight difficulty lurking in the omitted |
286 cases. This is not atypical for pen-and-paper proofs, once analysed in |
288 cases. Such errors are found in many pen-and-paper proofs when they |
287 detail.% |
289 are scrutinized formally.% |
|
290 \index{grammars!defining inductively|)}% |
288 \end{isamarkuptext}% |
291 \end{isamarkuptext}% |
289 \end{isabellebody}% |
292 \end{isabellebody}% |
290 %%% Local Variables: |
293 %%% Local Variables: |
291 %%% mode: latex |
294 %%% mode: latex |
292 %%% TeX-master: "root" |
295 %%% TeX-master: "root" |