equal
deleted
inserted
replaced
102 |
102 |
103 lemma rsimpalts_conscons: |
103 lemma rsimpalts_conscons: |
104 shows "rsimp_ALTs (r1 # rsa @ r2 # rsb) = RALTS (r1 # rsa @ r2 # rsb)" |
104 shows "rsimp_ALTs (r1 # rsa @ r2 # rsb) = RALTS (r1 # rsa @ r2 # rsb)" |
105 by (metis Nil_is_append_conv list.exhaust rsimp_ALTs.simps(3)) |
105 by (metis Nil_is_append_conv list.exhaust rsimp_ALTs.simps(3)) |
106 |
106 |
|
107 lemma rsimp_alts_equal: |
|
108 shows "rsimp_ALTs (rsa @ a # rsb @ a # rsc) = RALTS (rsa @ a # rsb @ a # rsc) " |
|
109 by (metis append_Cons append_Nil neq_Nil_conv rsimpalts_conscons) |
|
110 |
107 |
111 |
108 fun rsimp_SEQ :: " rrexp \<Rightarrow> rrexp \<Rightarrow> rrexp" |
112 fun rsimp_SEQ :: " rrexp \<Rightarrow> rrexp \<Rightarrow> rrexp" |
109 where |
113 where |
110 "rsimp_SEQ RZERO _ = RZERO" |
114 "rsimp_SEQ RZERO _ = RZERO" |
111 | "rsimp_SEQ _ RZERO = RZERO" |
115 | "rsimp_SEQ _ RZERO = RZERO" |
328 apply(case_tac "xs = []") |
332 apply(case_tac "xs = []") |
329 apply simp |
333 apply simp |
330 apply(simp add: rders_append rders_simp_append) |
334 apply(simp add: rders_append rders_simp_append) |
331 using inside_simp_removal by blast |
335 using inside_simp_removal by blast |
332 |
336 |
333 lemma simp_helps_der_pierce: |
337 |
334 shows " rsimp |
|
335 (rder x |
|
336 (rsimp_ALTs rs)) = |
|
337 rsimp |
|
338 (rsimp_ALTs |
|
339 (map (rder x ) |
|
340 rs |
|
341 ) |
|
342 )" |
|
343 sorry |
|
344 |
338 |
345 |
339 |
346 lemma rders_simp_one_char: |
340 lemma rders_simp_one_char: |
347 shows "rders_simp r [c] = rsimp (rder c r)" |
341 shows "rders_simp r [c] = rsimp (rder c r)" |
348 apply auto |
342 apply auto |
426 |
420 |
427 |
421 |
428 |
422 |
429 |
423 |
430 |
424 |
431 lemma simp_flatten2: |
425 |
432 shows "rsimp (RALTS (r # [RALTS rs])) = rsimp (RALTS (r # rs))" |
|
433 sorry |
|
434 |
426 |
435 |
427 |
436 lemma simp_flatten: |
428 lemma simp_flatten: |
437 shows "rsimp (RALTS ((RALTS rsa) # rsb)) = rsimp (RALTS (rsa @ rsb))" |
429 shows "rsimp (RALTS ((RALTS rsa) # rsb)) = rsimp (RALTS (rsa @ rsb))" |
438 |
430 |