466 using idem_after_simp1 apply presburger |
466 using idem_after_simp1 apply presburger |
467 apply simp+ |
467 apply simp+ |
468 apply(subgoal_tac "rsimp_ALTs (aa # list @ aaa # lista) = RALTS (aa # list @ aaa # lista)") |
468 apply(subgoal_tac "rsimp_ALTs (aa # list @ aaa # lista) = RALTS (aa # list @ aaa # lista)") |
469 apply simp |
469 apply simp |
470 using rsimpalts_conscons by presburger |
470 using rsimpalts_conscons by presburger |
471 |
471 |
|
472 |
|
473 |
|
474 |
|
475 lemma distinct_flts_no0: |
|
476 shows "rdistinct (rflts rs) (insert RZERO rset) = rdistinct (rflts rs) rset" |
|
477 apply(induct rs) |
|
478 apply simp |
|
479 apply(case_tac a) |
|
480 using rflts.simps(2) apply presburger |
|
481 sorry |
|
482 |
|
483 |
|
484 lemma simp_der_flts: |
|
485 shows "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) rset))= |
|
486 rsimp (RALTS (rdistinct (rflts (map (rder x) rs)) rset))" |
|
487 |
|
488 apply(induct rs arbitrary: rset) |
|
489 apply simp |
|
490 apply(case_tac a) |
|
491 apply simp |
|
492 apply(case_tac "RZERO \<in> rset") |
|
493 apply simp |
|
494 apply simp |
|
495 |
|
496 sorry |
|
497 |
|
498 |
472 lemma simp_der_pierce_flts: |
499 lemma simp_der_pierce_flts: |
473 shows " rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {})) = |
500 shows " rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {})) = |
474 rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {}))" |
501 rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {}))" |
475 oops |
502 sorry |
|
503 |
476 |
504 |
477 |
505 |
478 |
506 |
479 lemma simp_more_distinct: |
507 lemma simp_more_distinct: |
480 shows "rsimp (rsimp_ALTs (rsa @ rs)) = rsimp (rsimp_ALTs (rsa @ (rdistinct rs (set rsa)))) " |
508 shows "rsimp (rsimp_ALTs (rsa @ rs)) = rsimp (rsimp_ALTs (rsa @ (rdistinct rs (set rsa)))) " |
481 and "a1 \<in> set rsb \<Longrightarrow> rsimp (rsimp_ALTs (rsb @ a1 # rs)) = rsimp (rsimp_ALTs (rsb @ rs))" |
509 |
482 apply(induct rs arbitrary: rsa rsb a1) |
510 |
483 apply simp |
|
484 apply simp |
|
485 apply(case_tac " a \<in> set rsa") |
|
486 apply simp |
|
487 prefer 2 |
|
488 apply simp |
|
489 apply(drule_tac x = "rsa @ [a]" in meta_spec) |
|
490 apply simp |
|
491 |
511 |
492 |
512 |
493 sorry |
513 sorry |
494 |
514 |
495 lemma non_empty_list: |
515 lemma non_empty_list: |
754 apply(case_tac list) |
774 apply(case_tac list) |
755 apply(case_tac rs2) |
775 apply(case_tac rs2) |
756 apply simp |
776 apply simp |
757 using add0_isomorphic apply blast |
777 using add0_isomorphic apply blast |
758 apply simp |
778 apply simp |
759 sorry |
779 oops |
760 |
780 |
761 lemma alts_closed_form: shows |
781 lemma alts_closed_form: shows |
762 "rsimp (rders_simp (RALTS rs) s) = |
782 "rsimp (rders_simp (RALTS rs) s) = |
763 rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))" |
783 rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))" |
764 apply(induct s rule: rev_induct) |
784 apply(induct s rule: rev_induct) |