73 apply(subgoal_tac "a \<noteq> aa") |
81 apply(subgoal_tac "a \<noteq> aa") |
74 prefer 2 |
82 prefer 2 |
75 apply simp |
83 apply simp |
76 apply simp |
84 apply simp |
77 done |
85 done |
|
86 |
|
87 lemma rdistinct_on_distinct: |
|
88 shows "distinct rs \<Longrightarrow> rdistinct rs {} = rs" |
|
89 apply(induct rs) |
|
90 apply simp |
|
91 apply(subgoal_tac "rdistinct rs {} = rs") |
|
92 prefer 2 |
|
93 apply simp |
|
94 using distinct_not_exist by fastforce |
|
95 |
|
96 lemma distinct_rdistinct_append: |
|
97 shows "distinct rs1 \<Longrightarrow> rdistinct (rs1 @ rsa) {} = rs1 @ (rdistinct rsa (set rs1))" |
|
98 sorry |
|
99 |
|
100 lemma rdistinct_concat_general: |
|
101 shows "rdistinct (rs1 @ rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))" |
|
102 sorry |
|
103 |
|
104 lemma rdistinct_set_equality: |
|
105 shows "set (rdistinct rs {}) = set rs" |
|
106 sorry |
|
107 |
|
108 lemma distinct_once_enough: |
|
109 shows "rdistinct (rs @ rsa) {} = rdistinct (rdistinct rs {} @ rsa) {}" |
|
110 apply(subgoal_tac "distinct (rdistinct rs {})") |
|
111 apply(subgoal_tac |
|
112 " rdistinct (rdistinct rs {} @ rsa) {} = rdistinct rs {} @ (rdistinct rsa (set rs))") |
|
113 apply(simp only:) |
|
114 using rdistinct_concat_general apply blast |
|
115 apply (simp add: distinct_rdistinct_append rdistinct_set_equality) |
|
116 by (simp add: rdistinct_does_the_job) |
|
117 |
78 |
118 |
79 |
119 |
80 fun rflts :: "rrexp list \<Rightarrow> rrexp list" |
120 fun rflts :: "rrexp list \<Rightarrow> rrexp list" |
81 where |
121 where |
82 "rflts [] = []" |
122 "rflts [] = []" |
83 | "rflts (RZERO # rs) = rflts rs" |
123 | "rflts (RZERO # rs) = rflts rs" |
84 | "rflts ((RALTS rs1) # rs) = rs1 @ rflts rs" |
124 | "rflts ((RALTS rs1) # rs) = rs1 @ rflts rs" |
85 | "rflts (r1 # rs) = r1 # rflts rs" |
125 | "rflts (r1 # rs) = r1 # rflts rs" |
|
126 |
|
127 lemma rflts_def_idiot: |
|
128 shows "\<lbrakk> a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk> |
|
129 \<Longrightarrow> rflts (a # rs) = a # rflts rs" |
|
130 apply(case_tac a) |
|
131 apply simp_all |
|
132 done |
|
133 |
|
134 lemma rflts_def_idiot2: |
|
135 shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1; a \<in> set rs\<rbrakk> \<Longrightarrow> a \<in> set (rflts rs)" |
|
136 apply(induct rs) |
|
137 apply simp |
|
138 by (metis append.assoc in_set_conv_decomp insert_iff list.simps(15) rflts.simps(2) rflts.simps(3) rflts_def_idiot) |
|
139 |
|
140 |
|
141 |
|
142 lemma flts_append: |
|
143 shows "rflts (rs1 @ rs2) = rflts rs1 @ rflts rs2" |
|
144 apply(induct rs1) |
|
145 apply simp |
|
146 apply(case_tac a) |
|
147 apply simp+ |
|
148 done |
86 |
149 |
87 |
150 |
88 fun rsimp_ALTs :: " rrexp list \<Rightarrow> rrexp" |
151 fun rsimp_ALTs :: " rrexp list \<Rightarrow> rrexp" |
89 where |
152 where |
90 "rsimp_ALTs [] = RZERO" |
153 "rsimp_ALTs [] = RZERO" |
415 apply(simp add: rsimp_idem) |
468 apply(simp add: rsimp_idem) |
416 sorry |
469 sorry |
417 |
470 |
418 |
471 |
419 |
472 |
420 |
473 lemma idem_after_simp1: |
421 |
474 shows "rsimp_ALTs (rdistinct (rflts [rsimp aa]) {}) = rsimp aa" |
422 |
475 apply(case_tac "rsimp aa") |
423 |
476 apply simp+ |
424 |
477 apply (metis no_alt_short_list_after_simp no_further_dB_after_simp) |
|
478 by simp |
|
479 |
|
480 lemma identity_wwo0: |
|
481 shows "rsimp (rsimp_ALTs (RZERO # rs)) = rsimp (rsimp_ALTs rs)" |
|
482 by (metis idem_after_simp1 list.exhaust list.simps(8) list.simps(9) rflts.simps(2) rsimp.simps(2) rsimp.simps(3) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3)) |
|
483 |
|
484 |
|
485 lemma distinct_removes_last: |
|
486 shows "\<lbrakk>a \<in> set as\<rbrakk> |
|
487 \<Longrightarrow> rdistinct as rset = rdistinct (as @ [a]) rset" |
|
488 and "rdistinct (ab # as @ [ab]) rset1 = rdistinct (ab # as) rset1" |
|
489 apply(induct as arbitrary: rset ab rset1 a) |
|
490 apply simp |
|
491 apply simp |
|
492 apply(case_tac "aa \<in> rset") |
|
493 apply(case_tac "a = aa") |
|
494 apply (metis append_Cons) |
|
495 apply simp |
|
496 apply(case_tac "a \<in> set as") |
|
497 apply (metis append_Cons rdistinct.simps(2) set_ConsD) |
|
498 apply(case_tac "a = aa") |
|
499 prefer 2 |
|
500 apply simp |
|
501 apply (metis append_Cons) |
|
502 apply(case_tac "ab \<in> rset1") |
|
503 prefer 2 |
|
504 apply(subgoal_tac "rdistinct (ab # (a # as) @ [ab]) rset1 = |
|
505 ab # (rdistinct ((a # as) @ [ab]) (insert ab rset1))") |
|
506 prefer 2 |
|
507 apply force |
|
508 apply(simp only:) |
|
509 apply(subgoal_tac "rdistinct (ab # a # as) rset1 = ab # (rdistinct (a # as) (insert ab rset1))") |
|
510 apply(simp only:) |
|
511 apply(subgoal_tac "rdistinct ((a # as) @ [ab]) (insert ab rset1) = rdistinct (a # as) (insert ab rset1)") |
|
512 apply blast |
|
513 apply(case_tac "a \<in> insert ab rset1") |
|
514 apply simp |
|
515 apply (metis insertI1) |
|
516 apply simp |
|
517 apply (meson insertI1) |
|
518 apply simp |
|
519 apply(subgoal_tac "rdistinct ((a # as) @ [ab]) rset1 = rdistinct (a # as) rset1") |
|
520 apply simp |
|
521 by (metis append_Cons insert_iff insert_is_Un rdistinct.simps(2)) |
|
522 |
|
523 |
|
524 lemma distinct_removes_middle: |
|
525 shows "\<lbrakk>a \<in> set as\<rbrakk> |
|
526 \<Longrightarrow> rdistinct (as @ as2) rset = rdistinct (as @ [a] @ as2) rset" |
|
527 and "rdistinct (ab # as @ [ab] @ as3) rset1 = rdistinct (ab # as @ as3) rset1" |
|
528 apply(induct as arbitrary: rset rset1 ab as2 as3 a) |
|
529 apply simp |
|
530 apply simp |
|
531 apply(case_tac "a \<in> rset") |
|
532 apply simp |
|
533 apply metis |
|
534 apply simp |
|
535 apply (metis insertI1) |
|
536 apply(case_tac "a = ab") |
|
537 apply simp |
|
538 apply(case_tac "ab \<in> rset") |
|
539 apply simp |
|
540 apply presburger |
|
541 apply (meson insertI1) |
|
542 apply(case_tac "a \<in> rset") |
|
543 apply (metis (no_types, opaque_lifting) Un_insert_left append_Cons insert_iff rdistinct.simps(2) sup_bot_left) |
|
544 apply(case_tac "ab \<in> rset") |
|
545 apply simp |
|
546 apply (meson insert_iff) |
|
547 apply simp |
|
548 by (metis insertI1) |
|
549 |
|
550 |
|
551 lemma distinct_removes_middle3: |
|
552 shows "\<lbrakk>a \<in> set as\<rbrakk> |
|
553 \<Longrightarrow> rdistinct (as @ a #as2) rset = rdistinct (as @ as2) rset" |
|
554 using distinct_removes_middle(1) by fastforce |
|
555 |
|
556 lemma distinct_removes_last2: |
|
557 shows "\<lbrakk>a \<in> set as\<rbrakk> |
|
558 \<Longrightarrow> rdistinct as rset = rdistinct (as @ [a]) rset" |
|
559 by (simp add: distinct_removes_last(1)) |
|
560 |
|
561 lemma distinct_removes_middle2: |
|
562 shows "a \<in> set as \<Longrightarrow> rdistinct (as @ [a] @ rs) {} = rdistinct (as @ rs) {}" |
|
563 by (metis distinct_removes_middle(1)) |
|
564 |
|
565 lemma distinct_removes_list: |
|
566 shows "\<lbrakk> \<forall>r \<in> set rs. r \<in> set as\<rbrakk> \<Longrightarrow> rdistinct (as @ rs) {} = rdistinct as {}" |
|
567 apply(induct rs) |
|
568 apply simp+ |
|
569 apply(subgoal_tac "rdistinct (as @ a # rs) {} = rdistinct (as @ rs) {}") |
|
570 prefer 2 |
|
571 apply (metis append_Cons append_Nil distinct_removes_middle(1)) |
|
572 by presburger |
|
573 |
|
574 |
|
575 lemma spawn_simp_rsimpalts: |
|
576 shows "rsimp (rsimp_ALTs rs) = rsimp (rsimp_ALTs (map rsimp rs))" |
|
577 apply(cases rs) |
|
578 apply simp |
|
579 apply(case_tac list) |
|
580 apply simp |
|
581 apply(subst rsimp_idem[symmetric]) |
|
582 apply simp |
|
583 apply(subgoal_tac "rsimp_ALTs rs = RALTS rs") |
|
584 apply(simp only:) |
|
585 apply(subgoal_tac "rsimp_ALTs (map rsimp rs) = RALTS (map rsimp rs)") |
|
586 apply(simp only:) |
|
587 prefer 2 |
|
588 apply simp |
|
589 prefer 2 |
|
590 using rsimp_ALTs.simps(3) apply presburger |
|
591 apply auto |
|
592 apply(subst rsimp_idem)+ |
|
593 by (metis comp_apply rsimp_idem) |
|
594 |
|
595 |
|
596 |
|
597 |
|
598 inductive good1 :: "rrexp \<Rightarrow> bool" |
|
599 where |
|
600 "\<lbrakk>RZERO \<notin> set rs; \<nexists>rs1. RALTS rs1 \<in> set rs\<rbrakk> \<Longrightarrow> good1 (RALTS rs)" |
|
601 |"good1 RZERO" |
|
602 |"good1 RONE" |
|
603 |"good1 (RCHAR c)" |
|
604 |"good1 (RSEQ r1 r2)" |
|
605 |"good1 (RSTAR r0)" |
|
606 |
|
607 inductive goods :: "rrexp list \<Rightarrow> bool" |
|
608 where |
|
609 "goods []" |
|
610 |"\<lbrakk>goods rs; r \<noteq> RZERO; \<nexists>rs1. RALTS rs1 = r\<rbrakk> \<Longrightarrow> goods (r # rs)" |
|
611 |
|
612 lemma goods_good1: |
|
613 shows "goods rs = good1 (RALTS rs)" |
|
614 apply(induct rs) |
|
615 apply (simp add: good1.intros(1) goods.intros(1)) |
|
616 apply(case_tac "goods rs") |
|
617 apply(case_tac a) |
|
618 apply simp |
|
619 using good1.simps goods.cases apply auto[1] |
|
620 apply (simp add: good1.simps goods.intros(2)) |
|
621 apply (simp add: good1.simps goods.intros(2)) |
|
622 apply (simp add: good1.simps goods.intros(2)) |
|
623 using good1.simps goods.cases apply auto[1] |
|
624 apply (metis good1.cases good1.intros(1) goods.intros(2) rrexp.distinct(15) rrexp.distinct(21) rrexp.distinct(25) rrexp.distinct(29) rrexp.distinct(7) rrexp.distinct(9) rrexp.inject(3) set_ConsD) |
|
625 apply simp |
|
626 by (metis good1.cases good1.intros(1) goods.cases list.distinct(1) list.inject list.set_intros(2) rrexp.distinct(15) rrexp.distinct(29) rrexp.distinct(7) rrexp.inject(3) rrexp.simps(26) rrexp.simps(30)) |
|
627 |
|
628 lemma rsimp_good1: |
|
629 shows "rsimp r = r1 \<Longrightarrow> good1 r1" |
|
630 |
|
631 sorry |
|
632 |
|
633 lemma rsimp_no_dup: |
|
634 shows "rsimp r = RALTS rs \<Longrightarrow> distinct rs" |
|
635 sorry |
|
636 |
|
637 |
|
638 lemma rsimp_good1_2: |
|
639 shows "map rsimp rsa = [RALTS rs] \<Longrightarrow> good1 (RALTS rs)" |
|
640 by (metis Cons_eq_map_D rsimp_good1) |
|
641 |
|
642 |
|
643 |
|
644 lemma simp_singlealt_flatten: |
|
645 shows "rsimp (RALTS [RALTS rsa]) = rsimp (RALTS (rsa @ []))" |
|
646 apply(induct rsa) |
|
647 apply simp |
|
648 apply simp |
|
649 by (metis idem_after_simp1 list.simps(9) rsimp.simps(2)) |
|
650 |
|
651 |
|
652 lemma good1_rsimpalts: |
|
653 shows "rsimp r = RALTS rs \<Longrightarrow> rsimp_ALTs rs = RALTS rs" |
|
654 by (metis no_alt_short_list_after_simp) |
|
655 |
|
656 |
|
657 lemma good1_flts: |
|
658 shows "good1 (RALTS rs1) \<Longrightarrow> rflts rs1 = rs1" |
|
659 apply(induct rs1) |
|
660 apply simp |
|
661 by (metis good1.cases good1.intros(1) list.set_intros(1) rflts_def_idiot rrexp.distinct(21) rrexp.distinct(25) rrexp.distinct(29) rrexp.inject(3) rsimp.simps(3) rsimp.simps(4) rsimp_inner_idem4 set_subset_Cons subsetD) |
|
662 |
|
663 |
|
664 |
|
665 lemma good1_flatten: |
|
666 shows "\<lbrakk> rsimp r = (RALTS rs1)\<rbrakk> |
|
667 \<Longrightarrow> rflts (rsimp_ALTs rs1 # map rsimp rsb) = rflts (rs1 @ map rsimp rsb)" |
|
668 apply(subst good1_rsimpalts) |
|
669 apply simp+ |
|
670 apply(subgoal_tac "rflts (rs1 @ map rsimp rsb) = rs1 @ rflts (map rsimp rsb)") |
|
671 apply simp |
|
672 apply(subgoal_tac "good1 (RALTS rs1)") |
|
673 prefer 2 |
|
674 using rsimp_good1 apply blast |
|
675 using flts_append good1_flts by presburger |
|
676 |
|
677 lemma flatten_rsimpalts: |
|
678 shows "rflts (rsimp_ALTs (rdistinct (rflts (map rsimp rsa)) {}) # map rsimp rsb) = |
|
679 rflts ( (rdistinct (rflts (map rsimp rsa)) {}) @ map rsimp rsb)" |
|
680 apply(case_tac "map rsimp rsa") |
|
681 apply simp |
|
682 apply(case_tac "list") |
|
683 apply simp |
|
684 apply(case_tac a) |
|
685 apply simp+ |
|
686 apply(rename_tac rs1) |
|
687 apply(subgoal_tac "good1 (RALTS rs1)") |
|
688 apply(subgoal_tac "distinct rs1") |
|
689 apply(subst rdistinct_on_distinct) |
|
690 apply blast |
|
691 apply(subst rdistinct_on_distinct) |
|
692 apply blast |
|
693 using good1_flatten apply blast |
|
694 |
|
695 using rsimp_no_dup apply force |
|
696 |
|
697 using rsimp_good1_2 apply presburger |
|
698 |
|
699 apply simp+ |
|
700 apply(case_tac "rflts (a # aa # lista)") |
|
701 apply simp |
|
702 by (smt (verit) append_Cons append_Nil empty_iff good1_flatten list.distinct(1) rdistinct.simps(2) rsimp.simps(2) rsimp_ALTs.elims rsimp_good1) |
|
703 |
|
704 |
|
705 lemma flts_good_good: |
|
706 shows "\<forall>r \<in> set rs. good1 r \<Longrightarrow> good1 (RALTS (rflts rs ))" |
|
707 apply(induct rs) |
|
708 apply simp |
|
709 using goods.intros(1) goods_good1 apply auto[1] |
|
710 apply(case_tac "a") |
|
711 apply simp |
|
712 apply (metis goods.intros(2) goods_good1 list.set_intros(2) rflts.simps(4) rrexp.distinct(1) rrexp.distinct(15)) |
|
713 apply simp |
|
714 using goods.intros(2) goods_good1 apply blast |
|
715 using goods.intros(2) goods_good1 apply auto[1] |
|
716 apply(subgoal_tac "good1 a") |
|
717 apply (metis Un_iff good1.cases good1.intros(1) list.set_intros(2) rflts.simps(3) rrexp.distinct(15) rrexp.distinct(21) rrexp.distinct(25) rrexp.distinct(29) rrexp.distinct(7) rrexp.inject(3) set_append) |
|
718 apply simp |
|
719 by (metis goods.intros(2) goods_good1 list.set_intros(2) rflts.simps(7) rrexp.distinct(29) rrexp.distinct(9)) |
|
720 |
|
721 |
|
722 lemma simp_flatten_aux1: |
|
723 shows "\<forall>r \<in> set (map rsimp rsa). good1 r" |
|
724 apply(induct rsa) |
|
725 apply(simp add: goods.intros) |
|
726 using rsimp_good1 by auto |
|
727 |
|
728 |
|
729 |
|
730 lemma simp_flatten_aux: |
|
731 shows "\<forall>r \<in> set rs. good1 r \<Longrightarrow> rflts (rdistinct (rflts rs) {}) = (rdistinct (rflts rs) {})" |
|
732 sorry |
425 |
733 |
426 |
734 |
427 |
735 |
428 lemma simp_flatten: |
736 lemma simp_flatten: |
429 shows "rsimp (RALTS ((RALTS rsa) # rsb)) = rsimp (RALTS (rsa @ rsb))" |
737 shows "rsimp (RALTS ((RALTS rsa) # rsb)) = rsimp (RALTS (rsa @ rsb))" |
430 |
738 apply simp |
|
739 apply(subst flatten_rsimpalts) |
|
740 apply(simp add: flts_append) |
|
741 apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsa). good1 r") |
|
742 apply (metis distinct_once_enough simp_flatten_aux) |
|
743 using simp_flatten_aux1 by blast |
|
744 |
|
745 lemma simp_flatten3: |
|
746 shows "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))" |
431 sorry |
747 sorry |
432 |
748 |
433 |
749 |
434 |
750 |
435 fun vsuf :: "char list \<Rightarrow> rrexp \<Rightarrow> char list list" where |
751 fun vsuf :: "char list \<Rightarrow> rrexp \<Rightarrow> char list list" where |
453 where |
769 where |
454 "star_updates [] r Ss = Ss" |
770 "star_updates [] r Ss = Ss" |
455 | "star_updates (c # cs) r Ss = star_updates cs r (star_update c r Ss)" |
771 | "star_updates (c # cs) r Ss = star_updates cs r (star_update c r Ss)" |
456 |
772 |
457 |
773 |
458 |
774 lemma distinct_flts_no0: |
|
775 shows " rflts (map rsimp (rdistinct rs (insert RZERO rset))) = |
|
776 rflts (map rsimp (rdistinct rs rset)) " |
|
777 |
|
778 apply(induct rs arbitrary: rset) |
|
779 apply simp |
|
780 apply(case_tac a) |
|
781 apply simp+ |
|
782 apply (smt (verit, ccfv_SIG) rflts.simps(2) rflts.simps(3) rflts_def_idiot) |
|
783 prefer 2 |
|
784 apply simp |
|
785 by (smt (verit, ccfv_threshold) Un_insert_right insert_iff list.simps(9) rdistinct.simps(2) rflts.simps(2) rflts.simps(3) rflts_def_idiot rrexp.distinct(7)) |
|
786 |
|
787 lemma flts_removes0: |
|
788 shows " rflts (rs @ [RZERO]) = |
|
789 rflts rs" |
|
790 apply(induct rs) |
|
791 apply simp |
|
792 by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot) |
|
793 |
|
794 |
|
795 lemma rflts_spills_last: |
|
796 shows "a = RALTS rs \<Longrightarrow> rflts (rs1 @ [a]) = rflts rs1 @ rs" |
|
797 apply (induct rs1) |
|
798 apply simp |
|
799 by (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot) |
|
800 |
|
801 lemma flts_keeps1: |
|
802 shows " rflts (rs @ [RONE]) = |
|
803 rflts rs @ [RONE] " |
|
804 apply (induct rs) |
|
805 apply simp |
|
806 by (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot) |
|
807 |
|
808 lemma flts_keeps_others: |
|
809 shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk> \<Longrightarrow>rflts (rs @ [a]) = rflts rs @ [a]" |
|
810 apply(induct rs) |
|
811 apply simp |
|
812 apply (simp add: rflts_def_idiot) |
|
813 apply(case_tac a) |
|
814 apply simp |
|
815 using flts_keeps1 apply blast |
|
816 apply (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot) |
|
817 apply (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot) |
|
818 apply blast |
|
819 by (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot) |
|
820 |
|
821 lemma spilled_alts_contained: |
|
822 shows "\<lbrakk>a = RALTS rs ; a \<in> set rs1\<rbrakk> \<Longrightarrow> \<forall>r \<in> set rs. r \<in> set (rflts rs1)" |
|
823 apply(induct rs1) |
|
824 apply simp |
|
825 apply(case_tac "a = aa") |
|
826 apply simp |
|
827 apply(subgoal_tac " a \<in> set rs1") |
|
828 prefer 2 |
|
829 apply (meson set_ConsD) |
|
830 apply(case_tac aa) |
|
831 using rflts.simps(2) apply presburger |
|
832 apply fastforce |
|
833 apply fastforce |
|
834 apply fastforce |
|
835 apply fastforce |
|
836 by fastforce |
|
837 |
|
838 |
|
839 lemma distinct_removes_duplicate_flts: |
|
840 shows " a \<in> set rsa |
|
841 \<Longrightarrow> rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} = |
|
842 rdistinct (rflts (map rsimp rsa)) {}" |
|
843 apply(subgoal_tac "rsimp a \<in> set (map rsimp rsa)") |
|
844 prefer 2 |
|
845 apply simp |
|
846 apply(induct "rsimp a") |
|
847 apply simp |
|
848 using flts_removes0 apply presburger |
|
849 apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} = |
|
850 rdistinct (rflts (map rsimp rsa @ [RONE])) {}") |
|
851 apply (simp only:) |
|
852 apply(subst flts_keeps1) |
|
853 apply (metis distinct_removes_last2 rflts_def_idiot2 rrexp.simps(20) rrexp.simps(6)) |
|
854 apply presburger |
|
855 apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} = |
|
856 rdistinct ((rflts (map rsimp rsa)) @ [RCHAR x]) {}") |
|
857 apply (simp only:) |
|
858 prefer 2 |
|
859 apply (metis flts_keeps_others rrexp.distinct(21) rrexp.distinct(3)) |
|
860 apply (metis distinct_removes_last2 rflts_def_idiot2 rrexp.distinct(21) rrexp.distinct(3)) |
|
861 |
|
862 apply (metis distinct_removes_last2 flts_keeps_others rflts_def_idiot2 rrexp.distinct(25) rrexp.distinct(5)) |
|
863 prefer 2 |
|
864 apply (metis distinct_removes_last2 flts_keeps_others flts_removes0 rflts_def_idiot2 rrexp.distinct(29)) |
|
865 apply(subgoal_tac "rflts (map rsimp rsa @ [rsimp a]) = rflts (map rsimp rsa) @ x") |
|
866 prefer 2 |
|
867 apply (simp add: rflts_spills_last) |
|
868 apply(simp only:) |
|
869 apply(subgoal_tac "\<forall> r \<in> set x. r \<in> set (rflts (map rsimp rsa))") |
|
870 prefer 2 |
|
871 using spilled_alts_contained apply presburger |
|
872 using distinct_removes_list by blast |
459 |
873 |
460 |
874 |
461 |
875 |
462 (*some basic facts about rsimp*) |
876 (*some basic facts about rsimp*) |
463 |
877 |