equal
deleted
inserted
replaced
361 "rders_simp c (s1 @ s2) = rders_simp (rders_simp c s1) s2" |
361 "rders_simp c (s1 @ s2) = rders_simp (rders_simp c s1) s2" |
362 apply(induct s1 arbitrary: c s2) |
362 apply(induct s1 arbitrary: c s2) |
363 apply(simp_all) |
363 apply(simp_all) |
364 done |
364 done |
365 |
365 |
366 lemma inside_simp_removal: |
366 |
367 shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)" |
|
368 sorry |
|
369 |
367 |
370 lemma set_related_list: |
368 lemma set_related_list: |
371 shows "distinct rs \<Longrightarrow> length rs = card (set rs)" |
369 shows "distinct rs \<Longrightarrow> length rs = card (set rs)" |
372 by (simp add: distinct_card) |
370 by (simp add: distinct_card) |
373 (*this section deals with the property of distinctBy: creates a list without duplicates*) |
371 (*this section deals with the property of distinctBy: creates a list without duplicates*) |
376 by force |
374 by force |
377 |
375 |
378 |
376 |
379 |
377 |
380 |
378 |
381 lemma rders_simp_same_simpders: |
|
382 shows "s \<noteq> [] \<Longrightarrow> rders_simp r s = rsimp (rders r s)" |
|
383 apply(induct s rule: rev_induct) |
|
384 apply simp |
|
385 apply(case_tac "xs = []") |
|
386 apply simp |
|
387 apply(simp add: rders_append rders_simp_append) |
|
388 using inside_simp_removal by blast |
|
389 |
|
390 |
379 |
391 |
380 |
392 |
381 |
393 lemma rders_simp_one_char: |
382 lemma rders_simp_one_char: |
394 shows "rders_simp r [c] = rsimp (rder c r)" |
383 shows "rders_simp r [c] = rsimp (rder c r)" |
429 |
418 |
430 |
419 |
431 lemma ders_simp_nullability: |
420 lemma ders_simp_nullability: |
432 shows "rnullable (rders r s) = rnullable (rders_simp r s)" |
421 shows "rnullable (rders r s) = rnullable (rders_simp r s)" |
433 sorry |
422 sorry |
|
423 |
|
424 lemma der_simp_nullability: |
|
425 shows "rnullable r = rnullable (rsimp r)" |
|
426 sorry |
|
427 |
434 |
428 |
435 lemma first_elem_seqder: |
429 lemma first_elem_seqder: |
436 shows "\<not>rnullable r1p \<Longrightarrow> map rsimp (rder x (RSEQ r1p r2) |
430 shows "\<not>rnullable r1p \<Longrightarrow> map rsimp (rder x (RSEQ r1p r2) |
437 # rs) = map rsimp ((RSEQ (rder x r1p) r2) # rs) " |
431 # rs) = map rsimp ((RSEQ (rder x r1p) r2) # rs) " |
438 by auto |
432 by auto |