90 lemma distinct_removes_middle2: |
94 lemma distinct_removes_middle2: |
91 shows "a \<in> set as \<Longrightarrow> rdistinct (as @ [a] @ rs) {} = rdistinct (as @ rs) {}" |
95 shows "a \<in> set as \<Longrightarrow> rdistinct (as @ [a] @ rs) {} = rdistinct (as @ rs) {}" |
92 by (metis distinct_removes_middle(1)) |
96 by (metis distinct_removes_middle(1)) |
93 |
97 |
94 lemma distinct_removes_list: |
98 lemma distinct_removes_list: |
95 shows "\<lbrakk>a \<in> set as; \<forall>r \<in> set rs. r \<in> set as\<rbrakk> \<Longrightarrow> rdistinct (as @ rs) {} = rdistinct as {}" |
99 shows "\<lbrakk> \<forall>r \<in> set rs. r \<in> set as\<rbrakk> \<Longrightarrow> rdistinct (as @ rs) {} = rdistinct as {}" |
96 apply(induct rs) |
100 apply(induct rs) |
97 apply simp+ |
101 apply simp+ |
98 apply(subgoal_tac "rdistinct (as @ aa # rs) {} = rdistinct (as @ rs) {}") |
102 apply(subgoal_tac "rdistinct (as @ a # rs) {} = rdistinct (as @ rs) {}") |
99 prefer 2 |
103 prefer 2 |
100 apply (metis append_Cons append_Nil distinct_removes_middle(1)) |
104 apply (metis append_Cons append_Nil distinct_removes_middle(1)) |
101 by presburger |
105 by presburger |
102 |
106 |
103 |
|
104 |
|
105 lemma simp_rdistinct_f: shows |
|
106 "f ` rset = frset \<Longrightarrow> rsimp (rsimp_ALTs (map f (rdistinct rs rset))) = |
|
107 rsimp (rsimp_ALTs (rdistinct (map f rs) frset)) " |
|
108 apply(induct rs arbitrary: rset) |
|
109 apply simp |
|
110 apply(case_tac "a \<in> rset") |
|
111 apply(case_tac " f a \<in> frset") |
|
112 apply simp |
|
113 apply blast |
|
114 apply(subgoal_tac "f a \<notin> frset") |
|
115 apply(simp) |
|
116 apply(subgoal_tac "f ` (insert a rset) = insert (f a) frset") |
|
117 prefer 2 |
|
118 apply (meson image_insert) |
|
119 |
|
120 oops |
|
121 |
107 |
122 lemma spawn_simp_rsimpalts: |
108 lemma spawn_simp_rsimpalts: |
123 shows "rsimp (rsimp_ALTs rs) = rsimp (rsimp_ALTs (map rsimp rs))" |
109 shows "rsimp (rsimp_ALTs rs) = rsimp (rsimp_ALTs (map rsimp rs))" |
124 apply(cases rs) |
110 apply(cases rs) |
125 apply simp |
111 apply simp |
137 using rsimp_ALTs.simps(3) apply presburger |
123 using rsimp_ALTs.simps(3) apply presburger |
138 apply auto |
124 apply auto |
139 apply(subst rsimp_idem)+ |
125 apply(subst rsimp_idem)+ |
140 by (metis comp_apply rsimp_idem) |
126 by (metis comp_apply rsimp_idem) |
141 |
127 |
142 lemma spawn_simp_distinct: |
|
143 shows "rsimp (rsimp_ALTs (rsa @ (rdistinct rs (set rsa)))) = rsimp (rsimp_ALTs (rsa @ rs)) |
|
144 \<and> (a1 \<in> set rsa1 \<longrightarrow> rsimp (rsimp_ALTs (rsa1 @ rs)) = rsimp (rsimp_ALTs (rsa1 @ a1 # rs))) |
|
145 \<and> rsimp (rsimp_ALTs (rsc @ rs)) = rsimp (rsimp_ALTs (rsc @ (rdistinct rs (set rsc))))" |
|
146 apply(induct rs arbitrary: rsa rsa1 a1 rsc) |
|
147 apply simp |
|
148 apply(subgoal_tac "rsimp (rsimp_ALTs (rsa1 @ [a1])) = rsimp (rsimp_ALTs (rsa1 @ (rdistinct [a1] (set rsa1))))") |
|
149 prefer 2 |
|
150 |
|
151 |
|
152 |
|
153 |
|
154 oops |
|
155 |
|
156 lemma inv_one_derx: |
|
157 shows " RONE = rder xa r2 \<Longrightarrow> r2 = RCHAR xa" |
|
158 apply(case_tac r2) |
|
159 apply simp+ |
|
160 using rrexp.distinct(1) apply presburger |
|
161 apply (metis rder.simps(5) rrexp.distinct(13) rrexp.simps(20)) |
|
162 apply simp+ |
|
163 done |
|
164 |
|
165 lemma shape_of_derseq: |
|
166 shows "rder x (RSEQ r1 r2) = RSEQ (rder x r1) r2 \<or> rder x (RSEQ r1 r2) = (RALT (RSEQ (rder x r1) r2) (rder x r2))" |
|
167 using rder.simps(5) by presburger |
|
168 lemma shape_of_derseq2: |
|
169 shows "rder x (RSEQ r11 r12) = RSEQ x41 x42 \<Longrightarrow> x41 = rder x r11" |
|
170 by (metis rrexp.distinct(25) rrexp.inject(2) shape_of_derseq) |
|
171 |
|
172 lemma alts_preimage_case1: |
|
173 shows "rder x r = RALTS [r] \<Longrightarrow> \<exists>ra. r = RALTS [ra]" |
|
174 apply(case_tac r) |
|
175 apply simp+ |
|
176 apply (metis rrexp.simps(12) rrexp.simps(20)) |
|
177 apply (metis rrexp.inject(3) rrexp.simps(30) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3) shape_of_derseq) |
|
178 apply auto[1] |
|
179 by auto |
|
180 |
|
181 lemma alts_preimage_case2: |
|
182 shows "rder x r = RALT r1 r2 \<Longrightarrow> \<exists>ra rb. (r = RSEQ ra rb \<or> r = RALT ra rb)" |
|
183 apply(case_tac r) |
|
184 apply simp+ |
|
185 apply (metis rrexp.distinct(15) rrexp.distinct(7)) |
|
186 apply simp |
|
187 apply auto[1] |
|
188 by auto |
|
189 |
|
190 lemma alts_preimage_case2_2: |
|
191 shows "rder x r = RALT r1 r2 \<Longrightarrow> (\<exists>ra rb. r = RSEQ ra rb) \<or> (\<exists>rc rd. r = RALT rc rd)" |
|
192 using alts_preimage_case2 by blast |
|
193 |
|
194 lemma alts_preimage_case3: |
|
195 shows "rder x r = RALT r1 r2 \<Longrightarrow> (\<exists>ra rb. r = RSEQ ra rb) \<or> (\<exists>rcs rc rd. r = RALTS rcs \<and> rcs = [rc, rd])" |
|
196 using alts_preimage_case2 by blast |
|
197 |
|
198 lemma star_seq: |
|
199 shows "rder x (RSEQ (RSTAR a) b) = RALT (RSEQ (RSEQ (rder x a) (RSTAR a)) b) (rder x b)" |
|
200 using rder.simps(5) rder.simps(6) rnullable.simps(6) by presburger |
|
201 |
|
202 lemma language_equality_id1: |
|
203 shows "\<not>rnullable a \<Longrightarrow> rder x (RSEQ (RSTAR a) b) = rder x (RALT (RSEQ (RSEQ a (RSTAR a)) b) b)" |
|
204 apply (subst star_seq) |
|
205 apply simp |
|
206 done |
|
207 |
|
208 |
|
209 |
|
210 lemma distinct_der_set: |
|
211 shows "(rder x) ` rset = dset \<Longrightarrow> |
|
212 rsimp (rsimp_ALTs (map (rder x) (rdistinct rs rset))) = rsimp ( rsimp_ALTs (rdistinct (map (rder x) rs) dset))" |
|
213 apply(induct rs arbitrary: rset dset) |
|
214 apply simp |
|
215 apply(case_tac "a \<in> rset") |
|
216 apply(subgoal_tac "rder x a \<in> dset") |
|
217 prefer 2 |
|
218 apply blast |
|
219 apply simp |
|
220 apply(case_tac "rder x a \<notin> dset") |
|
221 prefer 2 |
|
222 apply simp |
|
223 |
|
224 oops |
|
225 |
|
226 lemma map_concat_cons: |
128 lemma map_concat_cons: |
227 shows "map f rsa @ f a # rs = map f (rsa @ [a]) @ rs" |
129 shows "map f rsa @ f a # rs = map f (rsa @ [a]) @ rs" |
228 by simp |
130 by simp |
229 |
131 |
230 lemma neg_removal_element_of: |
132 lemma neg_removal_element_of: |
231 shows " \<not> a \<notin> aset \<Longrightarrow> a \<in> aset" |
133 shows " \<not> a \<notin> aset \<Longrightarrow> a \<in> aset" |
232 by simp |
134 by simp |
233 |
|
234 lemma simp_more_flts: |
|
235 shows "rsimp (rsimp_ALTs (rdistinct rs {})) = rsimp (rsimp_ALTs (rdistinct (rflts rs) {}))" |
|
236 |
|
237 oops |
|
238 |
|
239 lemma simp_more_distinct1: |
|
240 shows "rsimp (rsimp_ALTs rs) = rsimp (rsimp_ALTs (rdistinct rs {}))" |
|
241 apply(induct rs) |
|
242 apply simp |
|
243 apply simp |
|
244 oops |
|
245 |
|
246 |
|
247 (* |
|
248 \<and> |
|
249 rsimp (rsimp_ALTs (rsb @ (rdistinct rs (set rsb)))) = |
|
250 rsimp (rsimp_ALTs (rsb @ (rdistinct (rflts rs) (set rsb)))) |
|
251 *) |
|
252 lemma simp_removes_duplicate2: |
|
253 shows "a " |
|
254 |
|
255 oops |
|
256 |
135 |
257 lemma flts_removes0: |
136 lemma flts_removes0: |
258 shows " rflts (rs @ [RZERO]) = |
137 shows " rflts (rs @ [RZERO]) = |
259 rflts rs" |
138 rflts rs" |
260 apply(induct rs) |
139 apply(induct rs) |
639 apply(case_tac rs) |
511 apply(case_tac rs) |
640 apply simp |
512 apply simp |
641 using grewrites_append apply blast |
513 using grewrites_append apply blast |
642 by (meson greal_trans grewrites.simps grewrites_concat) |
514 by (meson greal_trans grewrites.simps grewrites_concat) |
643 |
515 |
|
516 fun alt_set:: "rrexp \<Rightarrow> rrexp set" |
|
517 where |
|
518 "alt_set (RALTS rs) = set rs \<union> \<Union> (alt_set ` (set rs))" |
|
519 | "alt_set r = {r}" |
|
520 |
|
521 lemma alt_set_has_all: |
|
522 shows "RALTS rs \<in> alt_set rx \<Longrightarrow> set rs \<subseteq> alt_set rx" |
|
523 apply(induct rx arbitrary: rs) |
|
524 apply simp_all |
|
525 apply(rename_tac rSS rss) |
|
526 using in_mono by fastforce |
|
527 |
|
528 |
|
529 |
|
530 |
|
531 lemma grewrite_equal_rsimp: |
|
532 shows "\<lbrakk>rs1 \<leadsto>g rs2; rsimp_ALTs (rdistinct (rflts (map rsimp rs1)) (rset \<union> \<Union>(alt_set ` rset))) = |
|
533 rsimp_ALTs (rdistinct (rflts (map rsimp rs2)) (rset \<union> \<Union>(alt_set ` rset)))\<rbrakk> |
|
534 \<Longrightarrow> rsimp_ALTs (rdistinct (rflts (rsimp r # map rsimp rs1)) (rset \<union> \<Union>(alt_set ` rset))) = |
|
535 rsimp_ALTs (rdistinct (rflts (rsimp r # map rsimp rs2)) (rset \<union> \<Union>(alt_set ` rset)))" |
|
536 apply(induct rs1 rs2 arbitrary:rset rule: grewrite.induct) |
|
537 apply simp |
|
538 apply (metis append_Cons append_Nil flts_middle0) |
|
539 apply(case_tac "rsimp r \<in> rset") |
|
540 apply simp |
|
541 oops |
|
542 |
|
543 |
|
544 |
|
545 lemma grewrite_equal_rsimp: |
|
546 shows "rs1 \<leadsto>g rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)" |
|
547 apply(induct rs1 rs2 rule: grewrite.induct) |
|
548 apply simp |
|
549 using simp_flatten apply blast |
|
550 prefer 2 |
|
551 apply (smt (verit) append.assoc append_Cons in_set_conv_decomp simp_removes_duplicate2) |
|
552 apply simp |
|
553 apply(case_tac "rdistinct (rflts (map rsimp rs1)) {}") |
|
554 apply(case_tac "rsimp r = RZERO") |
|
555 apply simp |
|
556 apply(case_tac "\<exists>rs. rsimp r = RALTS rs") |
|
557 prefer 2 |
|
558 |
|
559 apply(subgoal_tac "rdistinct (rflts (rsimp r # map rsimp rs1)) {} = |
|
560 rsimp r # rdistinct (rflts (map rsimp rs1)) {rsimp r}") |
|
561 prefer 2 |
|
562 apply (simp add: list.inject rflts_def_idiot) |
|
563 apply(simp only:) |
|
564 |
|
565 sorry |
|
566 |
|
567 |
644 lemma grewrites_equal_rsimp: |
568 lemma grewrites_equal_rsimp: |
645 shows "rs1 \<leadsto>g* rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)" |
569 shows "rs1 \<leadsto>g* rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)" |
646 apply simp |
570 apply (induct rs1 rs2 rule: grewrites.induct) |
647 sorry |
571 apply simp |
648 |
572 using grewrite_equal_rsimp by presburger |
|
573 |
|
574 |
|
575 |
|
576 |
|
577 lemma grewrites_equal_simp_2: |
|
578 shows "rsimp (RALTS rs1) = rsimp (RALTS rs2) \<Longrightarrow> rs1 \<leadsto>g* rs2" |
|
579 sorry |
|
580 |
|
581 lemma grewrites_last: |
|
582 shows "r # [RALTS rs] \<leadsto>g* r # rs" |
|
583 by (metis gr_in_rstar grewrite.intros(2) grewrite.intros(3) self_append_conv) |
|
584 |
|
585 lemma simp_flatten2: |
|
586 shows "rsimp (RALTS (r # [RALTS rs])) = rsimp (RALTS (r # rs))" |
|
587 using grewrites_equal_rsimp grewrites_last by blast |
649 |
588 |
650 lemma frewrites_middle: |
589 lemma frewrites_middle: |
651 shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> r # (RALTS rs # rs1) \<leadsto>f* r # (rs @ rs1)" |
590 shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> r # (RALTS rs # rs1) \<leadsto>f* r # (rs @ rs1)" |
652 by (simp add: fr_in_rstar frewrite.intros(2) frewrite.intros(3)) |
591 by (simp add: fr_in_rstar frewrite.intros(2) frewrite.intros(3)) |
653 |
592 |
709 apply(case_tac "a \<in> rset") |
639 apply(case_tac "a \<in> rset") |
710 apply simp |
640 apply simp |
711 apply (simp add: frewrites_cons) |
641 apply (simp add: frewrites_cons) |
712 done |
642 done |
713 |
643 |
714 |
644 (*Interesting lemma: not obvious but easily proven by sledgehammer*) |
|
645 |
|
646 |
|
647 |
|
648 |
|
649 (*lemma induction last rule not go through |
|
650 example: |
|
651 r # |
|
652 rdistinct rs1 |
|
653 (insert RZERO |
|
654 (insert r |
|
655 (rset \<union> |
|
656 \<Union> (alt_set ` |
|
657 rset)))) \<leadsto>g* r # |
|
658 rdistinct rs2 |
|
659 (insert RZERO (insert r (rset \<union> \<Union> (alt_set ` rset)))) |
|
660 rs2 = [+rs] rs3 = rs, |
|
661 r = +rs |
|
662 [] \<leadsto>g* rs which is wrong |
|
663 *) |
715 lemma frewrite_with_distinct: |
664 lemma frewrite_with_distinct: |
716 shows " \<lbrakk>rs2 \<leadsto>f rs3\<rbrakk> |
665 shows " \<lbrakk>rs2 \<leadsto>f rs3\<rbrakk> |
717 \<Longrightarrow> rdistinct rs2 |
666 \<Longrightarrow> rdistinct rs2 |
718 (insert RZERO (rset \<union> \<Union> (alt_set ` rset))) \<leadsto>f* |
667 (insert RZERO (rset \<union> \<Union> (alt_set ` rset))) \<leadsto>g* |
719 rdistinct rs3 |
668 rdistinct rs3 |
720 (insert RZERO (rset \<union> \<Union> (alt_set ` rset)))" |
669 (insert RZERO (rset \<union> \<Union> (alt_set ` rset)))" |
721 apply(induct rs2 rs3 rule: frewrite.induct) |
670 apply(induct rs2 rs3 arbitrary: rset rule: frewrite.induct) |
722 apply(case_tac "RZERO \<in> (rset \<union> \<Union> (alt_set ` rset))") |
671 apply(case_tac "RZERO \<in> (rset \<union> \<Union> (alt_set ` rset))") |
723 apply simp |
672 apply simp |
724 apply simp |
673 apply simp |
725 apply(case_tac "RALTS rs \<in> rset") |
674 |
726 apply simp |
675 |
727 apply(subgoal_tac "\<forall>r \<in> set rs. r \<in> \<Union> (alt_set ` rset)") |
676 oops |
728 apply(subgoal_tac " rdistinct (rs @ rsa) (insert RZERO (rset \<union> \<Union> (alt_set ` rset))) = |
677 |
729 rdistinct rsa (insert RZERO (rset \<union> \<Union> (alt_set ` rset)))") |
|
730 using frewrites.intros(1) apply presburger |
|
731 apply (simp add: rdistinct_concat2) |
|
732 apply simp |
|
733 using alt_set.simps(1) apply blast |
|
734 apply(case_tac "RALTS rs \<in> rset \<union> \<Union>(alt_set ` rset)") |
|
735 |
|
736 |
|
737 sorry |
|
738 |
678 |
739 |
679 |
740 lemma frewrites_with_distinct: |
680 lemma frewrites_with_distinct: |
|
681 shows "\<lbrakk>rsa \<leadsto>f rsb \<rbrakk> \<Longrightarrow> |
|
682 ( (rs1 @ (rdistinct rsa (insert RZERO (set rs1 \<union> \<Union>(alt_set ` (set rs1) )))) \<leadsto>g* |
|
683 rs1 @ (rdistinct rsb (insert RZERO (set rs1 \<union> \<Union>(alt_set ` (set rs1) ))))) |
|
684 \<or> ( rs1 @ (rdistinct rsb (insert RZERO (set rs1 \<union> \<Union>(alt_set ` (set rs1) )))) \<leadsto>g* |
|
685 rs1 @ (rdistinct rsa (insert RZERO (set rs1 \<union> \<Union>(alt_set ` (set rs1) ))))) |
|
686 ) |
|
687 " |
|
688 apply(induct rsa rsb arbitrary: rs1 rule: frewrite.induct) |
|
689 apply simp |
|
690 apply(case_tac "RALTS rs \<in> set rs1") |
|
691 apply(subgoal_tac "set rs \<subseteq> \<Union> (alt_set `set rs1)") |
|
692 apply (metis (full_types) Un_iff Un_insert_left |
|
693 Un_insert_right grewrites.intros(1) le_supI2 rdistinct.simps(2) rdistinct_concat) |
|
694 apply (metis Un_subset_iff Union_upper alt_set.simps(1) imageI) |
|
695 |
|
696 apply(case_tac "RALTS rs \<in> \<Union> (alt_set ` set rs1)") |
|
697 apply simp |
|
698 apply (smt (z3) UN_insert Un_iff alt_set.simps(1) alt_set_has_all dual_order.trans grewrites.intros(1) insert_absorb rdistinct_concat subset_insertI) |
|
699 |
|
700 |
|
701 oops |
|
702 |
|
703 |
|
704 |
|
705 lemma rd_flts_set: |
|
706 shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> rdistinct rs1 ({RZERO} \<union> (rset \<union> \<Union>(alt_set ` rset))) \<leadsto>g* |
|
707 rdistinct rs2 ({RZERO} \<union> (rset \<union> \<Union>(alt_set ` rset)))" |
|
708 apply(induct rs1 rs2 rule: frewrites.induct) |
|
709 apply simp |
|
710 oops |
|
711 |
|
712 lemma frewrite_simpeq: |
|
713 shows "rs1 \<leadsto>f rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)" |
|
714 apply(induct rs1 rs2 rule: frewrite.induct) |
|
715 apply simp |
|
716 using simp_flatten apply presburger |
|
717 by (meson grewrites_cons grewrites_equal_rsimp grewrites_equal_simp_2) |
|
718 |
|
719 lemma frewrite_rd_grewrites: |
|
720 shows "rs1 \<leadsto>f rs2 \<Longrightarrow> |
|
721 \<exists>rs3. (rs1 \<leadsto>g* rs3) \<and> (rs2 \<leadsto>g* rs3) " |
|
722 apply(induct rs1 rs2 rule: frewrite.induct) |
|
723 apply(rule_tac x = "rs" in exI) |
|
724 apply(rule conjI) |
|
725 apply(rule gr_in_rstar) |
|
726 apply(rule grewrite.intros) |
|
727 apply(rule grewrites.intros) |
|
728 using grewrite.intros(2) apply blast |
|
729 by (meson grewrites_cons) |
|
730 |
|
731 |
|
732 lemma frewrites_rd_grewrites: |
741 shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> |
733 shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> |
742 rs1 @ (rdistinct rsa (insert RZERO (set rs1 \<union> \<Union>(alt_set ` (set rs1) )))) \<leadsto>f* |
734 \<exists>rs3. (rs1 \<leadsto>g* rs3) \<and> (rs2 \<leadsto>g* rs3)" |
743 rs2 @ (rdistinct rsb (insert RZERO (set rs2 \<union> \<Union>(alt_set ` (set rs2) ))))" |
|
744 apply(induct rs1 rs2 rule: frewrites.induct) |
735 apply(induct rs1 rs2 rule: frewrites.induct) |
745 apply simp |
736 apply simp |
746 |
737 apply(rule exI) |
747 |
738 apply(rule grewrites.intros) |
748 sorry |
739 by (metis frewrite_simpeq grewrites_equal_rsimp grewrites_equal_simp_2) |
749 |
740 |
|
741 |
|
742 |
|
743 |
|
744 |
|
745 lemma frewrite_simpeq2: |
|
746 shows "rs1 \<leadsto>f rs2 \<Longrightarrow> rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS (rdistinct rs2 {}))" |
|
747 apply(induct rs1 rs2 rule: frewrite.induct) |
|
748 apply simp |
|
749 apply (simp add: distinct_flts_no0) |
|
750 apply simp |
750 (*a more refined notion of \<leadsto>* is needed, |
751 (*a more refined notion of \<leadsto>* is needed, |
751 this lemma fails when rs1 contains some RALTS rs where elements |
752 this lemma fails when rs1 contains some RALTS rs where elements |
752 of rs appear in later parts of rs1, which will be picked up by rs2 |
753 of rs appear in later parts of rs1, which will be picked up by rs2 |
753 and deduplicated*) |
754 and deduplicated*) |
754 lemma wrong_frewrites_with_distinct2: |
755 lemma frewrites_simpeq: |
755 shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> |
756 shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> |
756 (rdistinct rs1 {RZERO}) \<leadsto>f* rdistinct rs2 {RZERO}" |
757 rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS ( rdistinct rs2 {})) " |
757 oops |
758 apply(induct rs1 rs2 rule: frewrites.induct) |
|
759 apply simp |
|
760 |
|
761 sorry |
|
762 |
|
763 |
758 |
764 |
759 lemma frewrite_single_step: |
765 lemma frewrite_single_step: |
760 shows " rs2 \<leadsto>f rs3 \<Longrightarrow> rsimp (RALTS rs2) = rsimp (RALTS rs3)" |
766 shows " rs2 \<leadsto>f rs3 \<Longrightarrow> rsimp (RALTS rs2) = rsimp (RALTS rs3)" |
761 apply(induct rs2 rs3 rule: frewrite.induct) |
767 apply(induct rs2 rs3 rule: frewrite.induct) |
762 apply simp |
768 apply simp |
767 shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)" |
773 shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)" |
768 apply(induct rs1 rs2 rule: frewrites.induct) |
774 apply(induct rs1 rs2 rule: frewrites.induct) |
769 apply simp |
775 apply simp |
770 using frewrite_single_step by presburger |
776 using frewrite_single_step by presburger |
771 |
777 |
|
778 lemma grewrite_simpalts: |
|
779 shows " rs2 \<leadsto>g rs3 \<Longrightarrow> rsimp (rsimp_ALTs rs2) = rsimp (rsimp_ALTs rs3)" |
|
780 apply(induct rs2 rs3 rule : grewrite.induct) |
|
781 using identity_wwo0 apply presburger |
|
782 apply (metis frewrite.intros(1) frewrite_single_step identity_wwo0 rsimp_ALTs.simps(3) simp_flatten) |
|
783 apply (smt (verit, ccfv_SIG) gmany_steps_later grewrites.intros(1) grewrites_cons grewrites_equal_rsimp identity_wwo0 rsimp_ALTs.simps(3)) |
|
784 apply simp |
|
785 apply(subst rsimp_alts_equal) |
|
786 apply(case_tac "rsa = [] \<and> rsb = [] \<and> rsc = []") |
|
787 apply(subgoal_tac "rsa @ a # rsb @ rsc = [a]") |
|
788 apply (simp only:) |
|
789 apply (metis append_Nil frewrite.intros(1) frewrite_single_step identity_wwo0 rsimp_ALTs.simps(3) simp_removes_duplicate1(2)) |
|
790 apply simp |
|
791 by (smt (verit, best) append.assoc append_Cons frewrite.intros(1) frewrite_single_step identity_wwo0 in_set_conv_decomp rsimp_ALTs.simps(3) simp_removes_duplicate3) |
|
792 |
|
793 |
|
794 lemma grewrites_simpalts: |
|
795 shows " rs2 \<leadsto>g* rs3 \<Longrightarrow> rsimp (rsimp_ALTs rs2) = rsimp (rsimp_ALTs rs3)" |
|
796 apply(induct rs2 rs3 rule: grewrites.induct) |
|
797 apply simp |
|
798 using grewrite_simpalts by presburger |
|
799 (* |
772 lemma frewrites_dB_wwo0_simp: |
800 lemma frewrites_dB_wwo0_simp: |
773 shows "rdistinct rs1 {RZERO} \<leadsto>f* rdistinct rs2 {RZERO} |
801 shows "rdistinct rs1 {RZERO} \<leadsto>f* rdistinct rs2 {RZERO} |
774 \<Longrightarrow> rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS (rdistinct rs2 {}))" |
802 \<Longrightarrow> rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS (rdistinct rs2 {}))" |
|
803 |
|
804 sorry |
|
805 *) |
|
806 lemma "rsimp (rsimp_ALTs (RZERO # rdistinct (map (rder x) (rflts rs)) {RZERO})) = |
|
807 rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts rs)) {})) " |
775 |
808 |
776 sorry |
809 sorry |
777 |
810 |
778 |
811 |
779 |
812 |
780 lemma simp_der_flts: |
813 lemma simp_der_flts: |
781 shows "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) {})) = |
814 shows "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) {})) = |
782 rsimp (RALTS (rdistinct (rflts (map (rder x) rs)) {}))" |
815 rsimp (RALTS (rdistinct (rflts (map (rder x) rs)) {}))" |
783 apply(subgoal_tac "map (rder x) (rflts rs) \<leadsto>f* rflts (map (rder x) rs)") |
816 apply(subgoal_tac "map (rder x) (rflts rs) \<leadsto>f* rflts (map (rder x) rs)") |
784 apply(subgoal_tac "rdistinct (map (rder x) (rflts rs)) {RZERO} |
817 apply(subgoal_tac "rdistinct (map (rder x) (rflts rs)) {RZERO} |
785 \<leadsto>f* rdistinct ( rflts (map (rder x) rs)) {RZERO}") |
818 \<leadsto>g* rdistinct ( rflts (map (rder x) rs)) {RZERO}") |
786 apply(subgoal_tac "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) {})) |
819 apply(subgoal_tac "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) {})) |
787 = rsimp (RALTS ( rdistinct ( rflts (map (rder x) rs)) {}))") |
820 = rsimp (RALTS ( rdistinct ( rflts (map (rder x) rs)) {}))") |
788 apply meson |
821 apply meson |
789 using frewrites_dB_wwo0_simp apply blast |
822 apply (metis distinct_flts_no0 grewrites_equal_rsimp rsimp.simps(2)) |
790 using frewrites_with_distinct2 apply blast |
823 sorry |
791 using early_late_der_frewrites by blast |
824 |
|
825 |
|
826 |
|
827 |
|
828 |
|
829 |
|
830 |
|
831 |
|
832 lemma simp_der_pierce_flts_prelim: |
|
833 shows "rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts rs)) {})) |
|
834 = rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) rs)) {}))" |
|
835 apply(subgoal_tac "map (rder x) (rflts rs) \<leadsto>g* rflts (map (rder x) rs)") |
|
836 apply(subgoal_tac "rdistinct (map (rder x) (rflts rs)) {RZERO} \<leadsto>g* rdistinct (rflts (map (rder x) rs)) {RZERO}") |
|
837 using grewrites_equal_simp_2 grewrites_simpalts simp_der_flts apply blast |
|
838 apply (simp add: early_late_der_frewrites frewrites_with_distinct2_grewrites) |
|
839 using early_late_der_frewrites frewrites_equivalent_simp grewrites_equal_simp_2 by blast |
792 |
840 |
793 |
841 |
794 lemma simp_der_pierce_flts: |
842 lemma simp_der_pierce_flts: |
795 shows " rsimp ( |
843 shows " rsimp ( |
796 rsimp_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {}) |
844 rsimp_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {}) |
797 ) = |
845 ) = |
798 rsimp ( |
846 rsimp ( |
799 rsimp_ALTs (rdistinct (rflts (map (rder x) (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {}) |
847 rsimp_ALTs (rdistinct (rflts (map (rder x) (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {}) |
800 )" |
848 )" |
801 |
849 using simp_der_pierce_flts_prelim by presburger |
802 sorry |
|
803 |
|
804 |
850 |
805 |
851 |
806 |
852 |
807 lemma simp_more_distinct: |
853 lemma simp_more_distinct: |
808 shows "rsimp (rsimp_ALTs (rsa @ rs)) = rsimp (rsimp_ALTs (rsa @ (rdistinct rs (set rsa)))) " |
854 shows "rsimp (rsimp_ALTs (rsa @ rs)) = rsimp (rsimp_ALTs (rsa @ (rdistinct rs (set rsa)))) " |