48 notation (latex output) |
48 notation (latex output) |
49 If ("(\<^latex>\<open>\\textrm{\<close>if\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>then\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>else\<^latex>\<open>}\<close> (_))" 10) and |
49 If ("(\<^latex>\<open>\\textrm{\<close>if\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>then\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>else\<^latex>\<open>}\<close> (_))" 10) and |
50 Cons ("_\<^latex>\<open>\\mbox{$\\,$}\<close>::\<^latex>\<open>\\mbox{$\\,$}\<close>_" [75,73] 73) and |
50 Cons ("_\<^latex>\<open>\\mbox{$\\,$}\<close>::\<^latex>\<open>\\mbox{$\\,$}\<close>_" [75,73] 73) and |
51 |
51 |
52 ZERO ("\<^bold>0" 81) and |
52 ZERO ("\<^bold>0" 81) and |
53 ONE ("\<^bold>1" 81) and |
53 ONE ("\<^bold>1" 81) and |
54 CH ("_" [1000] 80) and |
54 CH ("_" [1000] 80) and |
55 ALT ("_ + _" [77,77] 78) and |
55 ALT ("_ + _" [77,77] 77) and |
56 SEQ ("_ \<cdot> _" [77,77] 78) and |
56 SEQ ("_ \<cdot> _" [78,78] 78) and |
57 STAR ("_\<^sup>\<star>" [79] 78) and |
57 STAR ("_\<^sup>\<star>" [79] 78) and |
58 |
58 |
59 val.Void ("Empty" 78) and |
59 val.Void ("Empty" 78) and |
60 val.Char ("Char _" [1000] 78) and |
60 val.Char ("Char _" [1000] 78) and |
61 val.Left ("Left _" [79] 78) and |
61 val.Left ("Left _" [79] 78) and |
286 \end{tabular} |
286 \end{tabular} |
287 \end{center} |
287 \end{center} |
288 |
288 |
289 This rule allows us to simplify \mbox{@{term "(ALT (SEQ (ALT a b) c) (SEQ a c))"}} |
289 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)"}}, |
290 into \mbox{@{term "ALT (SEQ a c) (SEQ b c)"}}, |
291 which is cannot be done under the \mbox{ \<leadsto>} rule because only alternatives which are |
291 which cannot be done under the rrewrite rule because only alternatives which are |
292 children of another alternative can be spilled out. |
292 children of another alternative can be spilled out. |
293 \<close> |
293 \<close> |
294 |
294 |
295 (*This rule allows us to simplify \mbox{@{term "ALT (SEQ (ALT a b) c) (SEQ a c)"}} |
295 (*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)"}}, |
296 into \mbox{@{term "ALT (SEQ a c) (SEQ b c)"}}, |