equal
deleted
inserted
replaced
215 @{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"]}\\ |
216 @{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"]}\\ |
217 @{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"]}\\ |
218 @{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"]}\\ |
219 @{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"]}\\ |
220 @{thm[mode=Axiom] rrewrite.intros(9)[of "bs" "bs\<^sub>1" "rs"]}\\ |
|
221 @{thm[mode=Axiom] rrewrite.intros(10)[of "bs" ]}\\ |
|
222 @{thm[mode=Axiom] rrewrite.intros(11)[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"]}\\ |
|
224 |
|
225 \end{tabular} |
220 \end{tabular} |
226 \end{center} |
221 \end{center} |
227 |
222 |
228 |
223 |
229 And these can be made compact by the following simplification function: |
224 And these can be made compact by the following simplification function: |
266 \end{lemma} |
261 \end{lemma} |
267 |
262 |
268 The nice thing about the above |
263 The nice thing about the above |
269 \<close> |
264 \<close> |
270 |
265 |
271 |
266 (* @{thm[mode=Axiom] rrewrite.intros(9)[of "bs" "bs\<^sub>1" "rs"]}\\ |
|
267 @{thm[mode=Axiom] rrewrite.intros(10)[of "bs" ]}\\ |
|
268 @{thm[mode=Axiom] rrewrite.intros(11)[of "bs" "r\<^sub>1"]}\\ |
|
269 @{thm[mode=Rule] rrewrite.intros(12)[of "a\<^sub>1" "a\<^sub>2" "bs" "rs\<^sub>a" "rs\<^sub>b" "rs\<^sub>c"]}\\ |
|
270 *) |
272 section \<open> Additional Simp Rules?\<close> |
271 section \<open> Additional Simp Rules?\<close> |
273 |
272 |
274 |
273 |
275 text \<open> |
274 text \<open> |
276 One question someone would ask is: |
275 One question someone would ask is: |
288 |
287 |
289 This rule allows us to simplify \mbox{@{term "(ALT (SEQ (ALT a b) c) (SEQ a c))"}} |
288 This rule allows us to simplify \mbox{@{term "(ALT (SEQ (ALT a b) c) (SEQ a c))"}} |
290 into \mbox{@{term "ALT (SEQ a c) (SEQ b c)"}}, |
289 into \mbox{@{term "ALT (SEQ a c) (SEQ b c)"}}, |
291 which cannot be done under the rrewrite rule because only alternatives which are |
290 which cannot be done under the rrewrite rule because only alternatives which are |
292 children of another alternative can be spilled out. |
291 children of another alternative can be spilled out. |
|
292 |
|
293 Now with this rule we have some examples where we get |
|
294 even smaller intermediate derivatives than not having this |
|
295 rule: |
|
296 $\textit{(a+aa)}^* \rightarrow \textit{(1+1a)(a+aa)}^* \rightarrow |
|
297 \textit{(1+a)(a+aa)}^* $ |
293 \<close> |
298 \<close> |
294 |
299 |
295 (*This rule allows us to simplify \mbox{@{term "ALT (SEQ (ALT a b) c) (SEQ a c)"}} |
300 (*This rule allows us to simplify \mbox{@{term "ALT (SEQ (ALT a b) c) (SEQ a c)"}} |
296 into \mbox{@{term "ALT (SEQ a c) (SEQ b c)"}}, |
301 into \mbox{@{term "ALT (SEQ a c) (SEQ b c)"}}, |
297 which is cannot be done under the \<leadsto> rule because only alternatives which are |
302 which is cannot be done under the \<leadsto> rule because only alternatives which are |