equal
deleted
inserted
replaced
263 And that yields the correctness result: |
263 And that yields the correctness result: |
264 \begin{lemma} |
264 \begin{lemma} |
265 @{thm blexersimp_correctness} |
265 @{thm blexersimp_correctness} |
266 \end{lemma} |
266 \end{lemma} |
267 |
267 |
268 The nice thing about the aove |
268 The nice thing about the above |
269 \<close> |
269 \<close> |
270 |
270 |
|
271 |
|
272 section \<open> Additional Simp Rules?\<close> |
|
273 |
|
274 |
|
275 text \<open> |
|
276 One question someone would ask is: |
|
277 can we add more "atomic" simplification/rewriting rules, |
|
278 so the simplification is even more aggressive, making |
|
279 the intermediate results smaller, and therefore more space-efficient? |
|
280 For example, one might want to do open up alternatives who is a child |
|
281 of a sequence: |
|
282 |
|
283 \begin{center} |
|
284 \begin{tabular}{lcl} |
|
285 @{thm[mode=Rule] aggressive.intros(1)[of "bs" "bs1" "rs" "r"]}\\ |
|
286 \end{tabular} |
|
287 \end{center} |
|
288 |
|
289 |
|
290 This rule allows us to simplify \mbox{@{term "ALT (SEQ (ALT a b) c) (SEQ a c)"}} |
|
291 into \mbox{@{term "ALT (SEQ a c) (SEQ b c)"}}, |
|
292 which is cannot be done under the \<leadsto> rule because only alternatives which are |
|
293 children of another alternative can be spilled out. |
|
294 \<close> |
271 |
295 |
272 |
296 |
273 section \<open>Introduction\<close> |
297 section \<open>Introduction\<close> |
274 |
298 |
275 |
299 |
2053 \<close> |
2077 \<close> |
2054 (*<*) |
2078 (*<*) |
2055 end |
2079 end |
2056 (*>*) |
2080 (*>*) |
2057 |
2081 |
|
2082 |
|
2083 |
2058 (* |
2084 (* |
|
2085 |
|
2086 \begin{center} |
|
2087 \begin{tabular} |
|
2088 @{thm[mode=Rule] aggressive.intros(1)[of "bs" "bs1" "rs" "r"]} |
|
2089 end{tabular} |
|
2090 \end{center} |
|
2091 |
|
2092 |
2059 |
2093 |
2060 \begin{center} |
2094 \begin{center} |
2061 \begin{tabular}{lcl} |
2095 \begin{tabular}{lcl} |
2062 @{thm (lhs) code.simps(1)} & $\dn$ & @{thm (rhs) code.simps(1)}\\ |
2096 @{thm (lhs) code.simps(1)} & $\dn$ & @{thm (rhs) code.simps(1)}\\ |
2063 @{thm (lhs) code.simps(2)} & $\dn$ & @{thm (rhs) code.simps(2)}\\ |
2097 @{thm (lhs) code.simps(2)} & $\dn$ & @{thm (rhs) code.simps(2)}\\ |