164 For example, the regular expression $(a+aa)^*$ after taking |
164 For example, the regular expression $(a+aa)^*$ after taking |
165 derivative against just 10 $a$s will have size 8192. |
165 derivative against just 10 $a$s will have size 8192. |
166 |
166 |
167 %TODO: add figure for this? |
167 %TODO: add figure for this? |
168 |
168 |
|
169 |
|
170 Therefore, we insert a simplification phase |
|
171 after each derivation step, as defined below: |
169 \begin{lemma} |
172 \begin{lemma} |
170 @{thm blexer_simp_def} |
173 @{thm blexer_simp_def} |
171 \end{lemma} |
174 \end{lemma} |
172 |
175 |
|
176 The simplification function is given as follows: |
173 |
177 |
174 \begin{center} |
178 \begin{center} |
175 \begin{tabular}{lcl} |
179 \begin{tabular}{lcl} |
176 @{thm (lhs) bsimp.simps(1)[of "bs" "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bsimp.simps(1)[of "bs" "r\<^sub>1" "r\<^sub>2"]}\\ |
180 @{thm (lhs) bsimp.simps(1)[of "bs" "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bsimp.simps(1)[of "bs" "r\<^sub>1" "r\<^sub>2"]}\\ |
177 @{thm (lhs) bsimp.simps(2)} & $\dn$ & @{thm (rhs) bsimp.simps(2)}\\ |
181 @{thm (lhs) bsimp.simps(2)} & $\dn$ & @{thm (rhs) bsimp.simps(2)}\\ |
178 @{thm (lhs) bsimp.simps(3)} & $\dn$ & @{thm (rhs) bsimp.simps(3)}\\ |
182 @{thm (lhs) bsimp.simps(3)} & $\dn$ & @{thm (rhs) bsimp.simps(3)}\\ |
179 @{thm (lhs) intern.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) intern.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\ |
183 |
|
184 \end{tabular} |
|
185 \end{center} |
|
186 |
|
187 And the two helper functions are: |
|
188 \begin{center} |
|
189 \begin{tabular}{lcl} |
|
190 @{thm (lhs) bsimp_AALTs.simps(2)[of "bs\<^sub>1" "r" ]} & $\dn$ & @{thm (rhs) bsimp.simps(1)[of "bs\<^sub>1" "r" ]}\\ |
|
191 @{thm (lhs) bsimp_AALTs.simps(2)} & $\dn$ & @{thm (rhs) bsimp.simps(2)}\\ |
|
192 @{thm (lhs) bsimp_AALTs.simps(3)} & $\dn$ & @{thm (rhs) bsimp.simps(3)}\\ |
|
193 |
180 \end{tabular} |
194 \end{tabular} |
181 \end{center} |
195 \end{center} |
182 |
196 |
183 |
197 |
184 This might sound trivial in the case of producing a YES/NO answer, |
198 This might sound trivial in the case of producing a YES/NO answer, |
201 @{thm[mode=Rule] rrewrite.intros(4)[of "r\<^sub>1" "r\<^sub>2" "bs" "r\<^sub>3"]}\\ |
215 @{thm[mode=Rule] rrewrite.intros(4)[of "r\<^sub>1" "r\<^sub>2" "bs" "r\<^sub>3"]}\\ |
202 @{thm[mode=Rule] rrewrite.intros(5)[of "r\<^sub>3" "r\<^sub>4" "bs" "r\<^sub>1"]}\\ |
216 @{thm[mode=Rule] rrewrite.intros(5)[of "r\<^sub>3" "r\<^sub>4" "bs" "r\<^sub>1"]}\\ |
203 @{thm[mode=Rule] rrewrite.intros(6)[of "r" "r'" "bs" "rs\<^sub>1" "rs\<^sub>2"]}\\ |
217 @{thm[mode=Rule] rrewrite.intros(6)[of "r" "r'" "bs" "rs\<^sub>1" "rs\<^sub>2"]}\\ |
204 @{thm[mode=Axiom] rrewrite.intros(7)[of "bs" "rs\<^sub>a" "rs\<^sub>b"]}\\ |
218 @{thm[mode=Axiom] rrewrite.intros(7)[of "bs" "rs\<^sub>a" "rs\<^sub>b"]}\\ |
205 @{thm[mode=Axiom] rrewrite.intros(8)[of "bs" "rs\<^sub>a" "bs\<^sub>1" "rs\<^sub>1" "rs\<^sub>b"]}\\ |
219 @{thm[mode=Axiom] rrewrite.intros(8)[of "bs" "rs\<^sub>a" "bs\<^sub>1" "rs\<^sub>1" "rs\<^sub>b"]}\\ |
206 @{thm[mode=Axiom] rrewrite.intros(9)[of "bs" "r\<^sub>2"]}\\ |
220 @{thm[mode=Axiom] rrewrite.intros(9)[of "bs" "bs\<^sub>1" "rs"]}\\ |
207 @{thm[mode=Axiom] rrewrite.intros(10)[of "bs" "r\<^sub>1"]}\\ |
221 @{thm[mode=Axiom] rrewrite.intros(10)[of "bs" ]}\\ |
208 @{thm[mode=Axiom] rrewrite.intros(11)[of "bs" ]}\\ |
222 @{thm[mode=Axiom] rrewrite.intros(11)[of "bs" "r\<^sub>1"]}\\ |
209 @{thm[mode=Axiom] rrewrite.intros(12)[of "bs" "r\<^sub>1"]}\\ |
223 @{thm[mode=Rule] rrewrite.intros(12)[of "a\<^sub>1" "a\<^sub>2" "bs" "rs\<^sub>a" "rs\<^sub>b" "rs\<^sub>c"]}\\ |
210 @{thm[mode=Rule] rrewrite.intros(13)[of "a\<^sub>1" "a\<^sub>2" "bs" "rs\<^sub>a" "rs\<^sub>b" "rs\<^sub>c"]}\\ |
|
211 |
224 |
212 \end{tabular} |
225 \end{tabular} |
213 \end{center} |
226 \end{center} |
214 |
227 |
215 |
228 |