39 the original proof \cite[p.\ts81]{HopcroftUllman} and our formal version. |
39 the original proof \cite[p.\ts81]{HopcroftUllman} and our formal version. |
40 |
40 |
41 We start by fixing the alphabet, which consists only of \isa{a}'s |
41 We start by fixing the alphabet, which consists only of \isa{a}'s |
42 and~\isa{b}'s:% |
42 and~\isa{b}'s:% |
43 \end{isamarkuptext}% |
43 \end{isamarkuptext}% |
44 \isamarkupfalse% |
44 \isamarkuptrue% |
45 \isacommand{datatype}\ alfa\ {\isacharequal}\ a\ {\isacharbar}\ b\isamarkuptrue% |
45 \isacommand{datatype}\isamarkupfalse% |
46 % |
46 \ alfa\ {\isacharequal}\ a\ {\isacharbar}\ b% |
47 \begin{isamarkuptext}% |
47 \begin{isamarkuptext}% |
48 \noindent |
48 \noindent |
49 For convenience we include the following easy lemmas as simplification rules:% |
49 For convenience we include the following easy lemmas as simplification rules:% |
50 \end{isamarkuptext}% |
50 \end{isamarkuptext}% |
51 \isamarkupfalse% |
51 \isamarkuptrue% |
52 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ b{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}x\ {\isasymnoteq}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ a{\isacharparenright}{\isachardoublequote}\isanewline |
52 \isacommand{lemma}\isamarkupfalse% |
53 % |
53 \ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymnoteq}\ a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ b{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}x\ {\isasymnoteq}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ a{\isacharparenright}{\isachardoublequoteclose}\isanewline |
54 \isadelimproof |
54 % |
55 % |
55 \isadelimproof |
56 \endisadelimproof |
56 % |
57 % |
57 \endisadelimproof |
58 \isatagproof |
58 % |
59 \isamarkupfalse% |
59 \isatagproof |
60 \isacommand{by}\ {\isacharparenleft}case{\isacharunderscore}tac\ x{\isacharcomma}\ auto{\isacharparenright}% |
60 \isacommand{by}\isamarkupfalse% |
61 \endisatagproof |
61 \ {\isacharparenleft}case{\isacharunderscore}tac\ x{\isacharcomma}\ auto{\isacharparenright}% |
62 {\isafoldproof}% |
62 \endisatagproof |
63 % |
63 {\isafoldproof}% |
64 \isadelimproof |
64 % |
65 % |
65 \isadelimproof |
66 \endisadelimproof |
66 % |
67 \isamarkuptrue% |
67 \endisadelimproof |
68 % |
68 % |
69 \begin{isamarkuptext}% |
69 \begin{isamarkuptext}% |
70 \noindent |
70 \noindent |
71 Words over this alphabet are of type \isa{alfa\ list}, and |
71 Words over this alphabet are of type \isa{alfa\ list}, and |
72 the three nonterminals are declared as sets of such words:% |
72 the three nonterminals are declared as sets of such words:% |
73 \end{isamarkuptext}% |
73 \end{isamarkuptext}% |
74 \isamarkupfalse% |
74 \isamarkuptrue% |
75 \isacommand{consts}\ S\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline |
75 \isacommand{consts}\isamarkupfalse% |
76 \ \ \ \ \ \ \ A\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline |
76 \ S\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}alfa\ list\ set{\isachardoublequoteclose}\isanewline |
77 \ \ \ \ \ \ \ B\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isamarkuptrue% |
77 \ \ \ \ \ \ \ A\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}alfa\ list\ set{\isachardoublequoteclose}\isanewline |
78 % |
78 \ \ \ \ \ \ \ B\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}alfa\ list\ set{\isachardoublequoteclose}% |
79 \begin{isamarkuptext}% |
79 \begin{isamarkuptext}% |
80 \noindent |
80 \noindent |
81 The productions above are recast as a \emph{mutual} inductive |
81 The productions above are recast as a \emph{mutual} inductive |
82 definition\index{inductive definition!simultaneous} |
82 definition\index{inductive definition!simultaneous} |
83 of \isa{S}, \isa{A} and~\isa{B}:% |
83 of \isa{S}, \isa{A} and~\isa{B}:% |
84 \end{isamarkuptext}% |
84 \end{isamarkuptext}% |
85 \isamarkupfalse% |
85 \isamarkuptrue% |
86 \isacommand{inductive}\ S\ A\ B\isanewline |
86 \isacommand{inductive}\isamarkupfalse% |
|
87 \ S\ A\ B\isanewline |
87 \isakeyword{intros}\isanewline |
88 \isakeyword{intros}\isanewline |
88 \ \ {\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}\ {\isasymin}\ S{\isachardoublequote}\isanewline |
89 \ \ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}\ {\isasymin}\ S{\isachardoublequoteclose}\isanewline |
89 \ \ {\isachardoublequote}w\ {\isasymin}\ A\ {\isasymLongrightarrow}\ b{\isacharhash}w\ {\isasymin}\ S{\isachardoublequote}\isanewline |
90 \ \ {\isachardoublequoteopen}w\ {\isasymin}\ A\ {\isasymLongrightarrow}\ b{\isacharhash}w\ {\isasymin}\ S{\isachardoublequoteclose}\isanewline |
90 \ \ {\isachardoublequote}w\ {\isasymin}\ B\ {\isasymLongrightarrow}\ a{\isacharhash}w\ {\isasymin}\ S{\isachardoublequote}\isanewline |
91 \ \ {\isachardoublequoteopen}w\ {\isasymin}\ B\ {\isasymLongrightarrow}\ a{\isacharhash}w\ {\isasymin}\ S{\isachardoublequoteclose}\isanewline |
91 \isanewline |
92 \isanewline |
92 \ \ {\isachardoublequote}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ a{\isacharhash}w\ \ \ {\isasymin}\ A{\isachardoublequote}\isanewline |
93 \ \ {\isachardoublequoteopen}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ a{\isacharhash}w\ \ \ {\isasymin}\ A{\isachardoublequoteclose}\isanewline |
93 \ \ {\isachardoublequote}{\isasymlbrakk}\ v{\isasymin}A{\isacharsemicolon}\ w{\isasymin}A\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ b{\isacharhash}v{\isacharat}w\ {\isasymin}\ A{\isachardoublequote}\isanewline |
94 \ \ {\isachardoublequoteopen}{\isasymlbrakk}\ v{\isasymin}A{\isacharsemicolon}\ w{\isasymin}A\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ b{\isacharhash}v{\isacharat}w\ {\isasymin}\ A{\isachardoublequoteclose}\isanewline |
94 \isanewline |
95 \isanewline |
95 \ \ {\isachardoublequote}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ b{\isacharhash}w\ \ \ {\isasymin}\ B{\isachardoublequote}\isanewline |
96 \ \ {\isachardoublequoteopen}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ b{\isacharhash}w\ \ \ {\isasymin}\ B{\isachardoublequoteclose}\isanewline |
96 \ \ {\isachardoublequote}{\isasymlbrakk}\ v\ {\isasymin}\ B{\isacharsemicolon}\ w\ {\isasymin}\ B\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ a{\isacharhash}v{\isacharat}w\ {\isasymin}\ B{\isachardoublequote}\isamarkuptrue% |
97 \ \ {\isachardoublequoteopen}{\isasymlbrakk}\ v\ {\isasymin}\ B{\isacharsemicolon}\ w\ {\isasymin}\ B\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ a{\isacharhash}v{\isacharat}w\ {\isasymin}\ B{\isachardoublequoteclose}% |
97 % |
|
98 \begin{isamarkuptext}% |
98 \begin{isamarkuptext}% |
99 \noindent |
99 \noindent |
100 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 |
100 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 |
101 induction, so is the proof: we show at the same time that all words in |
101 induction, so is the proof: we show at the same time that all words in |
102 \isa{A} contain one more \isa{a} than \isa{b} and all words in \isa{B} contains one more \isa{b} than \isa{a}.% |
102 \isa{A} contain one more \isa{a} than \isa{b} and all words in \isa{B} contains one more \isa{b} than \isa{a}.% |
103 \end{isamarkuptext}% |
103 \end{isamarkuptext}% |
104 \isamarkupfalse% |
104 \isamarkuptrue% |
105 \isacommand{lemma}\ correctness{\isacharcolon}\isanewline |
105 \isacommand{lemma}\isamarkupfalse% |
106 \ \ {\isachardoublequote}{\isacharparenleft}w\ {\isasymin}\ S\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}{\isacharparenright}\ \ \ \ \ {\isasymand}\isanewline |
106 \ correctness{\isacharcolon}\isanewline |
|
107 \ \ {\isachardoublequoteopen}{\isacharparenleft}w\ {\isasymin}\ S\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}{\isacharparenright}\ \ \ \ \ {\isasymand}\isanewline |
107 \ \ \ {\isacharparenleft}w\ {\isasymin}\ A\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isasymand}\isanewline |
108 \ \ \ {\isacharparenleft}w\ {\isasymin}\ A\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isasymand}\isanewline |
108 \ \ \ {\isacharparenleft}w\ {\isasymin}\ B\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}% |
109 \ \ \ {\isacharparenleft}w\ {\isasymin}\ B\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}% |
109 \isadelimproof |
110 \isadelimproof |
110 % |
111 % |
111 \endisadelimproof |
112 \endisadelimproof |
112 % |
113 % |
113 \isatagproof |
114 \isatagproof |
114 \isamarkuptrue% |
|
115 % |
115 % |
116 \begin{isamarkuptxt}% |
116 \begin{isamarkuptxt}% |
117 \noindent |
117 \noindent |
118 These propositions are expressed with the help of the predefined \isa{filter} function on lists, which has the convenient syntax \isa{{\isacharbrackleft}x{\isasymin}xs{\isachardot}\ P\ x{\isacharbrackright}}, the list of all elements \isa{x} in \isa{xs} such that \isa{P\ x} |
118 These propositions are expressed with the help of the predefined \isa{filter} function on lists, which has the convenient syntax \isa{{\isacharbrackleft}x{\isasymin}xs{\isachardot}\ P\ x{\isacharbrackright}}, the list of all elements \isa{x} in \isa{xs} such that \isa{P\ x} |
119 holds. Remember that on lists \isa{size} and \isa{length} are synonymous. |
119 holds. Remember that on lists \isa{size} and \isa{length} are synonymous. |
120 |
120 |
121 The proof itself is by rule induction and afterwards automatic:% |
121 The proof itself is by rule induction and afterwards automatic:% |
122 \end{isamarkuptxt}% |
122 \end{isamarkuptxt}% |
123 \isamarkupfalse% |
123 \isamarkuptrue% |
124 \isacommand{by}\ {\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharcomma}\ auto{\isacharparenright}% |
124 \isacommand{by}\isamarkupfalse% |
125 \endisatagproof |
125 \ {\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharcomma}\ auto{\isacharparenright}% |
126 {\isafoldproof}% |
126 \endisatagproof |
127 % |
127 {\isafoldproof}% |
128 \isadelimproof |
128 % |
129 % |
129 \isadelimproof |
130 \endisadelimproof |
130 % |
131 \isamarkuptrue% |
131 \endisadelimproof |
132 % |
132 % |
133 \begin{isamarkuptext}% |
133 \begin{isamarkuptext}% |
134 \noindent |
134 \noindent |
135 This may seem surprising at first, and is indeed an indication of the power |
135 This may seem surprising at first, and is indeed an indication of the power |
136 of inductive definitions. But it is also quite straightforward. For example, |
136 of inductive definitions. But it is also quite straightforward. For example, |
162 move to the right. At this point we also start generalizing from \isa{a}'s |
162 move to the right. At this point we also start generalizing from \isa{a}'s |
163 and \isa{b}'s to an arbitrary property \isa{P}. Otherwise we would have |
163 and \isa{b}'s to an arbitrary property \isa{P}. Otherwise we would have |
164 to prove the desired lemma twice, once as stated above and once with the |
164 to prove the desired lemma twice, once as stated above and once with the |
165 roles of \isa{a}'s and \isa{b}'s interchanged.% |
165 roles of \isa{a}'s and \isa{b}'s interchanged.% |
166 \end{isamarkuptext}% |
166 \end{isamarkuptext}% |
167 \isamarkupfalse% |
167 \isamarkuptrue% |
168 \isacommand{lemma}\ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i\ {\isacharless}\ size\ w{\isachardot}\isanewline |
168 \isacommand{lemma}\isamarkupfalse% |
|
169 \ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}i\ {\isacharless}\ size\ w{\isachardot}\isanewline |
169 \ \ {\isasymbar}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline |
170 \ \ {\isasymbar}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline |
170 \ \ \ {\isacharminus}\ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isasymbar}\ {\isasymle}\ {\isadigit{1}}{\isachardoublequote}% |
171 \ \ \ {\isacharminus}\ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isasymbar}\ {\isasymle}\ {\isadigit{1}}{\isachardoublequoteclose}% |
171 \isadelimproof |
172 \isadelimproof |
172 % |
173 % |
173 \endisadelimproof |
174 \endisadelimproof |
174 % |
175 % |
175 \isatagproof |
176 \isatagproof |
176 \isamarkuptrue% |
|
177 % |
177 % |
178 \begin{isamarkuptxt}% |
178 \begin{isamarkuptxt}% |
179 \noindent |
179 \noindent |
180 The lemma is a bit hard to read because of the coercion function |
180 The lemma is a bit hard to read because of the coercion function |
181 \isa{int\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ int}. It is required because \isa{size} returns |
181 \isa{int\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ int}. It is required because \isa{size} returns |
186 |
186 |
187 The proof is by induction on \isa{w}, with a trivial base case, and a not |
187 The proof is by induction on \isa{w}, with a trivial base case, and a not |
188 so trivial induction step. Since it is essentially just arithmetic, we do not |
188 so trivial induction step. Since it is essentially just arithmetic, we do not |
189 discuss it.% |
189 discuss it.% |
190 \end{isamarkuptxt}% |
190 \end{isamarkuptxt}% |
191 \isamarkupfalse% |
191 \isamarkuptrue% |
192 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w{\isacharparenright}\isanewline |
192 \isacommand{apply}\isamarkupfalse% |
193 \isamarkupfalse% |
193 {\isacharparenleft}induct{\isacharunderscore}tac\ w{\isacharparenright}\isanewline |
194 \isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ abs{\isacharunderscore}if\ take{\isacharunderscore}Cons\ split{\isacharcolon}\ nat{\isachardot}split{\isacharparenright}\isanewline |
194 \isacommand{apply}\isamarkupfalse% |
195 \isamarkupfalse% |
195 {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ abs{\isacharunderscore}if\ take{\isacharunderscore}Cons\ split{\isacharcolon}\ nat{\isachardot}split{\isacharparenright}\isanewline |
196 \isacommand{done}% |
196 \isacommand{done}\isamarkupfalse% |
197 \endisatagproof |
197 % |
198 {\isafoldproof}% |
198 \endisatagproof |
199 % |
199 {\isafoldproof}% |
200 \isadelimproof |
200 % |
201 % |
201 \isadelimproof |
202 \endisadelimproof |
202 % |
203 \isamarkuptrue% |
203 \endisadelimproof |
204 % |
204 % |
205 \begin{isamarkuptext}% |
205 \begin{isamarkuptext}% |
206 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:% |
206 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:% |
207 \end{isamarkuptext}% |
207 \end{isamarkuptext}% |
208 \isamarkupfalse% |
208 \isamarkuptrue% |
209 \isacommand{lemma}\ part{\isadigit{1}}{\isacharcolon}\isanewline |
209 \isacommand{lemma}\isamarkupfalse% |
210 \ {\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 |
210 \ part{\isadigit{1}}{\isacharcolon}\isanewline |
211 \ \ {\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}% |
211 \ {\isachardoublequoteopen}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 |
212 \isadelimproof |
212 \ \ {\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}}{\isachardoublequoteclose}% |
213 % |
213 \isadelimproof |
214 \endisadelimproof |
214 % |
215 % |
215 \endisadelimproof |
216 \isatagproof |
216 % |
217 \isamarkuptrue% |
217 \isatagproof |
218 % |
218 % |
219 \begin{isamarkuptxt}% |
219 \begin{isamarkuptxt}% |
220 \noindent |
220 \noindent |
221 This is proved by \isa{force} with the help of the intermediate value theorem, |
221 This is proved by \isa{force} with the help of the intermediate value theorem, |
222 instantiated appropriately and with its first premise disposed of by lemma |
222 instantiated appropriately and with its first premise disposed of by lemma |
223 \isa{step{\isadigit{1}}}:% |
223 \isa{step{\isadigit{1}}}:% |
224 \end{isamarkuptxt}% |
224 \end{isamarkuptxt}% |
225 \isamarkupfalse% |
225 \isamarkuptrue% |
226 \isacommand{apply}{\isacharparenleft}insert\ nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val{\isacharbrackleft}OF\ step{\isadigit{1}}{\isacharcomma}\ of\ {\isachardoublequote}P{\isachardoublequote}\ {\isachardoublequote}w{\isachardoublequote}\ {\isachardoublequote}{\isadigit{1}}{\isachardoublequote}{\isacharbrackright}{\isacharparenright}\isanewline |
226 \isacommand{apply}\isamarkupfalse% |
227 \isamarkupfalse% |
227 {\isacharparenleft}insert\ nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val{\isacharbrackleft}OF\ step{\isadigit{1}}{\isacharcomma}\ of\ {\isachardoublequoteopen}P{\isachardoublequoteclose}\ {\isachardoublequoteopen}w{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isadigit{1}}{\isachardoublequoteclose}{\isacharbrackright}{\isacharparenright}\isanewline |
228 \isacommand{by}\ force% |
228 \isacommand{by}\isamarkupfalse% |
229 \endisatagproof |
229 \ force% |
230 {\isafoldproof}% |
230 \endisatagproof |
231 % |
231 {\isafoldproof}% |
232 \isadelimproof |
232 % |
233 % |
233 \isadelimproof |
234 \endisadelimproof |
234 % |
235 \isamarkuptrue% |
235 \endisadelimproof |
236 % |
236 % |
237 \begin{isamarkuptext}% |
237 \begin{isamarkuptext}% |
238 \noindent |
238 \noindent |
239 |
239 |
240 Lemma \isa{part{\isadigit{1}}} tells us only about the prefix \isa{take\ i\ w}. |
240 Lemma \isa{part{\isadigit{1}}} tells us only about the prefix \isa{take\ i\ w}. |
241 An easy lemma deals with the suffix \isa{drop\ i\ w}:% |
241 An easy lemma deals with the suffix \isa{drop\ i\ w}:% |
242 \end{isamarkuptext}% |
242 \end{isamarkuptext}% |
243 \isamarkupfalse% |
243 \isamarkuptrue% |
244 \isacommand{lemma}\ part{\isadigit{2}}{\isacharcolon}\isanewline |
244 \isacommand{lemma}\isamarkupfalse% |
245 \ \ {\isachardoublequote}{\isasymlbrakk}size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\isanewline |
245 \ part{\isadigit{2}}{\isacharcolon}\isanewline |
|
246 \ \ {\isachardoublequoteopen}{\isasymlbrakk}size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\isanewline |
246 \ \ \ \ size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}{\isacharsemicolon}\isanewline |
247 \ \ \ \ size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}{\isacharsemicolon}\isanewline |
247 \ \ \ \ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isasymrbrakk}\isanewline |
248 \ \ \ \ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isasymrbrakk}\isanewline |
248 \ \ \ {\isasymLongrightarrow}\ size{\isacharbrackleft}x{\isasymin}drop\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}drop\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequote}\isanewline |
249 \ \ \ {\isasymLongrightarrow}\ size{\isacharbrackleft}x{\isasymin}drop\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}drop\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequoteclose}\isanewline |
249 % |
250 % |
250 \isadelimproof |
251 \isadelimproof |
251 % |
252 % |
252 \endisadelimproof |
253 \endisadelimproof |
253 % |
254 % |
254 \isatagproof |
255 \isatagproof |
255 \isamarkupfalse% |
256 \isacommand{by}\isamarkupfalse% |
256 \isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharparenright}% |
257 {\isacharparenleft}simp\ del{\isacharcolon}\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharparenright}% |
257 \endisatagproof |
258 \endisatagproof |
258 {\isafoldproof}% |
259 {\isafoldproof}% |
259 % |
260 % |
260 \isadelimproof |
261 \isadelimproof |
261 % |
262 % |
262 \endisadelimproof |
263 \endisadelimproof |
263 \isamarkuptrue% |
|
264 % |
264 % |
265 \begin{isamarkuptext}% |
265 \begin{isamarkuptext}% |
266 \noindent |
266 \noindent |
267 In the proof we have disabled the normally useful lemma |
267 In the proof we have disabled the normally useful lemma |
268 \begin{isabelle} |
268 \begin{isabelle} |
275 \end{isabelle} |
275 \end{isabelle} |
276 |
276 |
277 To dispose of trivial cases automatically, the rules of the inductive |
277 To dispose of trivial cases automatically, the rules of the inductive |
278 definition are declared simplification rules:% |
278 definition are declared simplification rules:% |
279 \end{isamarkuptext}% |
279 \end{isamarkuptext}% |
280 \isamarkupfalse% |
280 \isamarkuptrue% |
281 \isacommand{declare}\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharbrackleft}simp{\isacharbrackright}\isamarkuptrue% |
281 \isacommand{declare}\isamarkupfalse% |
282 % |
282 \ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharbrackleft}simp{\isacharbrackright}% |
283 \begin{isamarkuptext}% |
283 \begin{isamarkuptext}% |
284 \noindent |
284 \noindent |
285 This could have been done earlier but was not necessary so far. |
285 This could have been done earlier but was not necessary so far. |
286 |
286 |
287 The completeness theorem tells us that if a word has the same number of |
287 The completeness theorem tells us that if a word has the same number of |
288 \isa{a}'s and \isa{b}'s, then it is in \isa{S}, and similarly |
288 \isa{a}'s and \isa{b}'s, then it is in \isa{S}, and similarly |
289 for \isa{A} and \isa{B}:% |
289 for \isa{A} and \isa{B}:% |
290 \end{isamarkuptext}% |
290 \end{isamarkuptext}% |
291 \isamarkupfalse% |
291 \isamarkuptrue% |
292 \isacommand{theorem}\ completeness{\isacharcolon}\isanewline |
292 \isacommand{theorem}\isamarkupfalse% |
293 \ \ {\isachardoublequote}{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ \ \ \ \ {\isasymlongrightarrow}\ w\ {\isasymin}\ S{\isacharparenright}\ {\isasymand}\isanewline |
293 \ completeness{\isacharcolon}\isanewline |
|
294 \ \ {\isachardoublequoteopen}{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ \ \ \ \ {\isasymlongrightarrow}\ w\ {\isasymin}\ S{\isacharparenright}\ {\isasymand}\isanewline |
294 \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymlongrightarrow}\ w\ {\isasymin}\ A{\isacharparenright}\ {\isasymand}\isanewline |
295 \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymlongrightarrow}\ w\ {\isasymin}\ A{\isacharparenright}\ {\isasymand}\isanewline |
295 \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymlongrightarrow}\ w\ {\isasymin}\ B{\isacharparenright}{\isachardoublequote}% |
296 \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymlongrightarrow}\ w\ {\isasymin}\ B{\isacharparenright}{\isachardoublequoteclose}% |
296 \isadelimproof |
297 \isadelimproof |
297 % |
298 % |
298 \endisadelimproof |
299 \endisadelimproof |
299 % |
300 % |
300 \isatagproof |
301 \isatagproof |
301 \isamarkuptrue% |
|
302 % |
302 % |
303 \begin{isamarkuptxt}% |
303 \begin{isamarkuptxt}% |
304 \noindent |
304 \noindent |
305 The proof is by induction on \isa{w}. Structural induction would fail here |
305 The proof is by induction on \isa{w}. Structural induction would fail here |
306 because, as we can see from the grammar, we need to make bigger steps than |
306 because, as we can see from the grammar, we need to make bigger steps than |
307 merely appending a single letter at the front. Hence we induct on the length |
307 merely appending a single letter at the front. Hence we induct on the length |
308 of \isa{w}, using the induction rule \isa{length{\isacharunderscore}induct}:% |
308 of \isa{w}, using the induction rule \isa{length{\isacharunderscore}induct}:% |
309 \end{isamarkuptxt}% |
309 \end{isamarkuptxt}% |
310 \isamarkupfalse% |
310 \isamarkuptrue% |
311 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}\isamarkuptrue% |
311 \isacommand{apply}\isamarkupfalse% |
|
312 {\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}\isamarkupfalse% |
312 % |
313 % |
313 \begin{isamarkuptxt}% |
314 \begin{isamarkuptxt}% |
314 \noindent |
315 \noindent |
315 The \isa{rule} parameter tells \isa{induct{\isacharunderscore}tac} explicitly which induction |
316 The \isa{rule} parameter tells \isa{induct{\isacharunderscore}tac} explicitly which induction |
316 rule to use. For details see \S\ref{sec:complete-ind} below. |
317 rule to use. For details see \S\ref{sec:complete-ind} below. |
336 We only consider the first case in detail. |
338 We only consider the first case in detail. |
337 |
339 |
338 After breaking the conjunction up into two cases, we can apply |
340 After breaking the conjunction up into two cases, we can apply |
339 \isa{part{\isadigit{1}}} to the assumption that \isa{w} contains two more \isa{a}'s than \isa{b}'s.% |
341 \isa{part{\isadigit{1}}} to the assumption that \isa{w} contains two more \isa{a}'s than \isa{b}'s.% |
340 \end{isamarkuptxt}% |
342 \end{isamarkuptxt}% |
341 \isamarkupfalse% |
343 \isamarkuptrue% |
342 \isacommand{apply}{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline |
344 \isacommand{apply}\isamarkupfalse% |
343 \ \isamarkupfalse% |
345 {\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline |
344 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline |
346 \ \isacommand{apply}\isamarkupfalse% |
345 \ \isamarkupfalse% |
347 {\isacharparenleft}clarify{\isacharparenright}\isanewline |
346 \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline |
348 \ \isacommand{apply}\isamarkupfalse% |
347 \ \isamarkupfalse% |
349 {\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequoteclose}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline |
348 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isamarkuptrue% |
350 \ \isacommand{apply}\isamarkupfalse% |
349 % |
351 {\isacharparenleft}clarify{\isacharparenright}% |
350 \begin{isamarkuptxt}% |
352 \begin{isamarkuptxt}% |
351 \noindent |
353 \noindent |
352 This yields an index \isa{i\ {\isasymle}\ length\ v} such that |
354 This yields an index \isa{i\ {\isasymle}\ length\ v} such that |
353 \begin{isabelle}% |
355 \begin{isabelle}% |
354 \ \ \ \ \ length\ {\isacharbrackleft}x{\isasymin}take\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}take\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}% |
356 \ \ \ \ \ length\ {\isacharbrackleft}x{\isasymin}take\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}take\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}% |
356 With the help of \isa{part{\isadigit{2}}} it follows that |
358 With the help of \isa{part{\isadigit{2}}} it follows that |
357 \begin{isabelle}% |
359 \begin{isabelle}% |
358 \ \ \ \ \ length\ {\isacharbrackleft}x{\isasymin}drop\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}drop\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}% |
360 \ \ \ \ \ length\ {\isacharbrackleft}x{\isasymin}drop\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}drop\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}% |
359 \end{isabelle}% |
361 \end{isabelle}% |
360 \end{isamarkuptxt}% |
362 \end{isamarkuptxt}% |
361 \ \isamarkupfalse% |
363 \isamarkuptrue% |
362 \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline |
364 \ \isacommand{apply}\isamarkupfalse% |
363 \ \ \isamarkupfalse% |
365 {\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequoteclose}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline |
364 \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isamarkuptrue% |
366 \ \ \isacommand{apply}\isamarkupfalse% |
365 % |
367 {\isacharparenleft}assumption{\isacharparenright}% |
366 \begin{isamarkuptxt}% |
368 \begin{isamarkuptxt}% |
367 \noindent |
369 \noindent |
368 Now it is time to decompose \isa{v} in the conclusion \isa{b\ {\isacharhash}\ v\ {\isasymin}\ A} |
370 Now it is time to decompose \isa{v} in the conclusion \isa{b\ {\isacharhash}\ v\ {\isasymin}\ A} |
369 into \isa{take\ i\ v\ {\isacharat}\ drop\ i\ v},% |
371 into \isa{take\ i\ v\ {\isacharat}\ drop\ i\ v},% |
370 \end{isamarkuptxt}% |
372 \end{isamarkuptxt}% |
371 \ \isamarkupfalse% |
373 \isamarkuptrue% |
372 \isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ n{\isadigit{1}}{\isacharequal}i\ \isakeyword{and}\ t{\isacharequal}v\ \isakeyword{in}\ subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}{\isacharparenright}\isamarkuptrue% |
374 \ \isacommand{apply}\isamarkupfalse% |
373 % |
375 {\isacharparenleft}rule{\isacharunderscore}tac\ n{\isadigit{1}}{\isacharequal}i\ \isakeyword{and}\ t{\isacharequal}v\ \isakeyword{in}\ subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}{\isacharparenright}% |
374 \begin{isamarkuptxt}% |
376 \begin{isamarkuptxt}% |
375 \noindent |
377 \noindent |
376 (the variables \isa{n{\isadigit{1}}} and \isa{t} are the result of composing the |
378 (the variables \isa{n{\isadigit{1}}} and \isa{t} are the result of composing the |
377 theorems \isa{subst} and \isa{append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id}) |
379 theorems \isa{subst} and \isa{append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id}) |
378 after which the appropriate rule of the grammar reduces the goal |
380 after which the appropriate rule of the grammar reduces the goal |
379 to the two subgoals \isa{take\ i\ v\ {\isasymin}\ A} and \isa{drop\ i\ v\ {\isasymin}\ A}:% |
381 to the two subgoals \isa{take\ i\ v\ {\isasymin}\ A} and \isa{drop\ i\ v\ {\isasymin}\ A}:% |
380 \end{isamarkuptxt}% |
382 \end{isamarkuptxt}% |
381 \ \isamarkupfalse% |
383 \isamarkuptrue% |
382 \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isamarkuptrue% |
384 \ \isacommand{apply}\isamarkupfalse% |
383 % |
385 {\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}% |
384 \begin{isamarkuptxt}% |
386 \begin{isamarkuptxt}% |
385 Both subgoals follow from the induction hypothesis because both \isa{take\ i\ v} and \isa{drop\ i\ v} are shorter than \isa{w}:% |
387 Both subgoals follow from the induction hypothesis because both \isa{take\ i\ v} and \isa{drop\ i\ v} are shorter than \isa{w}:% |
386 \end{isamarkuptxt}% |
388 \end{isamarkuptxt}% |
387 \ \ \isamarkupfalse% |
389 \isamarkuptrue% |
388 \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline |
390 \ \ \isacommand{apply}\isamarkupfalse% |
389 \ \isamarkupfalse% |
391 {\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline |
390 \isacommand{apply}{\isacharparenleft}force\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isamarkuptrue% |
392 \ \isacommand{apply}\isamarkupfalse% |
391 % |
393 {\isacharparenleft}force\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}% |
392 \begin{isamarkuptxt}% |
394 \begin{isamarkuptxt}% |
393 The case \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v} is proved analogously:% |
395 The case \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v} is proved analogously:% |
394 \end{isamarkuptxt}% |
396 \end{isamarkuptxt}% |
395 \isamarkupfalse% |
397 \isamarkuptrue% |
396 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline |
398 \isacommand{apply}\isamarkupfalse% |
397 \isamarkupfalse% |
399 {\isacharparenleft}clarify{\isacharparenright}\isanewline |
398 \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline |
400 \isacommand{apply}\isamarkupfalse% |
399 \isamarkupfalse% |
401 {\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequoteclose}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline |
400 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline |
402 \isacommand{apply}\isamarkupfalse% |
401 \isamarkupfalse% |
403 {\isacharparenleft}clarify{\isacharparenright}\isanewline |
402 \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline |
404 \isacommand{apply}\isamarkupfalse% |
403 \ \isamarkupfalse% |
405 {\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequoteclose}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline |
404 \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline |
406 \ \isacommand{apply}\isamarkupfalse% |
405 \isamarkupfalse% |
407 {\isacharparenleft}assumption{\isacharparenright}\isanewline |
406 \isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ n{\isadigit{1}}{\isacharequal}i\ \isakeyword{and}\ t{\isacharequal}v\ \isakeyword{in}\ subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}{\isacharparenright}\isanewline |
408 \isacommand{apply}\isamarkupfalse% |
407 \isamarkupfalse% |
409 {\isacharparenleft}rule{\isacharunderscore}tac\ n{\isadigit{1}}{\isacharequal}i\ \isakeyword{and}\ t{\isacharequal}v\ \isakeyword{in}\ subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}{\isacharparenright}\isanewline |
408 \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isanewline |
410 \isacommand{apply}\isamarkupfalse% |
409 \ \isamarkupfalse% |
411 {\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isanewline |
410 \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline |
412 \ \isacommand{apply}\isamarkupfalse% |
411 \isamarkupfalse% |
413 {\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline |
412 \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}% |
414 \isacommand{by}\isamarkupfalse% |
413 \endisatagproof |
415 {\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}% |
414 {\isafoldproof}% |
416 \endisatagproof |
415 % |
417 {\isafoldproof}% |
416 \isadelimproof |
418 % |
417 % |
419 \isadelimproof |
418 \endisadelimproof |
420 % |
419 \isamarkuptrue% |
421 \endisadelimproof |
420 % |
422 % |
421 \begin{isamarkuptext}% |
423 \begin{isamarkuptext}% |
422 We conclude this section with a comparison of our proof with |
424 We conclude this section with a comparison of our proof with |
423 Hopcroft\index{Hopcroft, J. E.} and Ullman's\index{Ullman, J. D.} |
425 Hopcroft\index{Hopcroft, J. E.} and Ullman's\index{Ullman, J. D.} |
424 \cite[p.\ts81]{HopcroftUllman}. |
426 \cite[p.\ts81]{HopcroftUllman}. |