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 |
284 \begin{tabular}{lcl} |
284 \begin{tabular}{lcl} |
285 @{thm[mode=Rule] aggressive.intros(1)[of "bs" "bs1" "rs" "r"]}\\ |
285 @{thm[mode=Rule] aggressive.intros(1)[of "bs" "bs1" "rs" "r"]}\\ |
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 |
290 into \mbox{@{term "ALT (SEQ a c) (SEQ b c)"}}, |
|
291 which cannot be done under the rrewrite rule because only alternatives which are |
|
292 children of another alternative can be spilled out. |
291 \<close> |
293 \<close> |
292 |
294 |
293 (*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)"}} |
294 into \mbox{@{term "ALT (SEQ a c) (SEQ b c)"}}, |
296 into \mbox{@{term "ALT (SEQ a c) (SEQ b c)"}}, |
295 which is cannot be done under the \<leadsto> rule because only alternatives which are |
297 which is cannot be done under the \<leadsto> rule because only alternatives which are |