equal
deleted
inserted
replaced
69 where |
69 where |
70 "rsimp_ALTs [] = RZERO" |
70 "rsimp_ALTs [] = RZERO" |
71 | "rsimp_ALTs [r] = r" |
71 | "rsimp_ALTs [r] = r" |
72 | "rsimp_ALTs rs = RALTS rs" |
72 | "rsimp_ALTs rs = RALTS rs" |
73 |
73 |
|
74 lemma rsimpalts_gte2elems: |
|
75 shows "size rlist \<ge> 2 \<Longrightarrow> rsimp_ALTs rlist = RALTS rlist" |
|
76 apply(induct rlist) |
|
77 apply simp |
|
78 apply(induct rlist) |
|
79 apply simp |
|
80 apply (metis Suc_le_length_iff rsimp_ALTs.simps(3)) |
|
81 by blast |
|
82 |
|
83 lemma rsimpalts_conscons: |
|
84 shows "rsimp_ALTs (r1 # rsa @ r2 # rsb) = RALTS (r1 # rsa @ r2 # rsb)" |
|
85 by (metis Nil_is_append_conv list.exhaust rsimp_ALTs.simps(3)) |
|
86 |
|
87 |
74 fun rsimp_SEQ :: " rrexp \<Rightarrow> rrexp \<Rightarrow> rrexp" |
88 fun rsimp_SEQ :: " rrexp \<Rightarrow> rrexp \<Rightarrow> rrexp" |
75 where |
89 where |
76 "rsimp_SEQ RZERO _ = RZERO" |
90 "rsimp_SEQ RZERO _ = RZERO" |
77 | "rsimp_SEQ _ RZERO = RZERO" |
91 | "rsimp_SEQ _ RZERO = RZERO" |
78 | "rsimp_SEQ RONE r2 = r2" |
92 | "rsimp_SEQ RONE r2 = r2" |
262 done |
276 done |
263 |
277 |
264 lemma rders_simp_append: |
278 lemma rders_simp_append: |
265 "rders_simp c (s1 @ s2) = rders_simp (rders_simp c s1) s2" |
279 "rders_simp c (s1 @ s2) = rders_simp (rders_simp c s1) s2" |
266 apply(induct s1 arbitrary: c s2) |
280 apply(induct s1 arbitrary: c s2) |
267 apply(simp_all) |
281 apply(simp_all) |
268 done |
282 done |
269 |
283 |
270 lemma inside_simp_removal: |
284 lemma inside_simp_removal: |
271 shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)" |
285 shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)" |
272 sorry |
286 sorry |
330 corollary rsimp_inner_idem3: |
344 corollary rsimp_inner_idem3: |
331 shows "rsimp r = RALTS rs \<Longrightarrow> map rsimp rs = rs" |
345 shows "rsimp r = RALTS rs \<Longrightarrow> map rsimp rs = rs" |
332 by (meson map_idI rsimp_inner_idem2) |
346 by (meson map_idI rsimp_inner_idem2) |
333 |
347 |
334 corollary rsimp_inner_idem4: |
348 corollary rsimp_inner_idem4: |
335 shows "rsimp r = RALTS rs \<Longrightarrow> flts rs = rs" |
349 shows "rsimp r = RALTS rs \<Longrightarrow> rflts rs = rs" |
336 sorry |
350 sorry |
337 |
351 |
338 |
352 |
339 lemma head_one_more_simp: |
353 lemma head_one_more_simp: |
340 shows "map rsimp (r # rs) = map rsimp (( rsimp r) # rs)" |
354 shows "map rsimp (r # rs) = map rsimp (( rsimp r) # rs)" |