702 (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) (star_updates list r0 [[a]])) {}))) |
702 (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) (star_updates list r0 [[a]])) {}))) |
703 \<le> (Suc (card (sizeNregex (Suc (N + rsize (RSTAR r0))))) * Suc (N + rsize (RSTAR r0))) ") |
703 \<le> (Suc (card (sizeNregex (Suc (N + rsize (RSTAR r0))))) * Suc (N + rsize (RSTAR r0))) ") |
704 apply auto[1] |
704 apply auto[1] |
705 using star_control_variant by blast |
705 using star_control_variant by blast |
706 |
706 |
707 |
|
708 lemma seq_list_estimate_control: shows |
|
709 " rsize (rsimp (RALTS (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)))) |
|
710 \<le> Suc (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {})))" |
|
711 by(metis alts_simp_control) |
|
712 |
|
713 lemma map_ders_is_list_of_ders: |
|
714 shows "\<forall>s. rsize (rders_simp r2 s) \<le> N2 \<Longrightarrow> |
|
715 \<forall>r \<in> set (rdistinct (map (rders_simp r2) Ss) {}). rsize r \<le> N2" |
|
716 apply(rule same_regex_property_after_distinct) |
|
717 by simp |
|
718 |
|
719 lemma seq_estimate_bounded: |
707 lemma seq_estimate_bounded: |
720 assumes "\<forall>s. rsize (rders_simp r1 s) \<le> N1" and "\<forall>s. rsize (rders_simp r2 s) \<le> N2" |
708 assumes "\<forall>s. rsize (rders_simp r1 s) \<le> N1" |
|
709 and "\<forall>s. rsize (rders_simp r2 s) \<le> N2" |
721 shows |
710 shows |
722 "Suc (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {}))) \<le> |
711 "Suc (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {}))) \<le> |
723 Suc (Suc (N1 + (rsize r2)) + (N2 * card (sizeNregex N2)))" |
712 Suc (Suc (N1 + (rsize r2)) + (N2 * card (sizeNregex N2)))" |
724 apply(subgoal_tac " (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {}))) \<le> |
713 proof - |
725 (Suc (N1 + (rsize r2)) + (N2 * card (sizeNregex N2)))") |
714 have a: "sum_list (map rsize (rdistinct (map (rders_simp r2) (vsuf s r1)) {})) \<le> N2 * card (sizeNregex N2)" |
726 apply force |
715 by (metis assms(2) distinct_list_rexp_up_to_certain_size_bouded_by_set_enumerating_up_to_that_size ex_map_conv mult.commute) |
727 apply(subgoal_tac " (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {}))) \<le> |
716 |
728 (rsize (RSEQ (rders_simp r1 s) r2)) + (sum_list (map rsize (rdistinct (map (rders_simp r2) (vsuf s r1)) {})) )") |
717 have "sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {})) \<le> |
729 prefer 2 |
718 rsize (RSEQ (rders_simp r1 s) r2) + sum_list (map rsize (rdistinct (map (rders_simp r2) (vsuf s r1)) {}))" |
730 using triangle_inequality_distinct apply blast |
719 using triangle_inequality_distinct by blast |
731 apply(subgoal_tac " sum_list (map rsize (rdistinct (map (rders_simp r2) (vsuf s r1)) {})) \<le> N2 * card (sizeNregex N2) ") |
720 also have "... \<le> rsize (RSEQ (rders_simp r1 s) r2) + N2 * card (sizeNregex N2)" |
732 apply(subgoal_tac "rsize (RSEQ (rders_simp r1 s) r2) \<le> Suc (N1 + rsize r2)") |
721 by (simp add: a) |
733 apply linarith |
722 also have "... \<le> Suc (N1 + (rsize r2) + N2 * card (sizeNregex N2))" |
734 apply (simp add: assms(1)) |
723 by (simp add: assms(1)) |
735 apply(subgoal_tac "\<forall>r \<in> set (rdistinct (map (rders_simp r2) (vsuf s r1)) {}). rsize r \<le> N2") |
724 finally show ?thesis |
736 apply (metis (no_types, opaque_lifting) assms(2) distinct_list_rexp_up_to_certain_size_bouded_by_set_enumerating_up_to_that_size ex_map_conv mult.commute) |
725 by force |
737 using assms(2) map_ders_is_list_of_ders by blast |
726 qed |
738 |
|
739 |
727 |
740 |
728 |
741 lemma seq_closed_form_bounded2: |
729 lemma seq_closed_form_bounded2: |
742 assumes "\<forall>s. rsize (rders_simp r1 s) \<le> N1" |
730 assumes "\<forall>s. rsize (rders_simp r1 s) \<le> N1" |
743 and "\<forall>s. rsize (rders_simp r2 s) \<le> N2" |
731 and "\<forall>s. rsize (rders_simp r2 s) \<le> N2" |
744 shows "rsize (rders_simp (RSEQ r1 r2) s) \<le> max (Suc (Suc (N1 + (rsize r2)) + (N2 * card (sizeNregex N2)))) (rsize (RSEQ r1 r2))" |
732 shows "rsize (rders_simp (RSEQ r1 r2) s) |
|
733 \<le> max (Suc (Suc (N1 + (rsize r2)) + (N2 * card (sizeNregex N2)))) (rsize (RSEQ r1 r2))" |
745 proof(cases s) |
734 proof(cases s) |
746 case Nil |
735 case Nil |
747 then show "rsize (rders_simp (RSEQ r1 r2) s) |
736 then show "rsize (rders_simp (RSEQ r1 r2) s) |
748 \<le> max (Suc (Suc (N1 + rsize r2) + N2 * card (sizeNregex N2))) (rsize (RSEQ r1 r2))" |
737 \<le> max (Suc (Suc (N1 + rsize r2) + N2 * card (sizeNregex N2))) (rsize (RSEQ r1 r2))" |
749 by simp |
738 by simp |
752 then have "rsize (rders_simp (RSEQ r1 r2) s) = |
741 then have "rsize (rders_simp (RSEQ r1 r2) s) = |
753 rsize (rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # (map (rders_simp r2) (vsuf s r1)))))" |
742 rsize (rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # (map (rders_simp r2) (vsuf s r1)))))" |
754 using seq_closed_form_variant by (metis list.discI) |
743 using seq_closed_form_variant by (metis list.discI) |
755 also have "... \<le> Suc (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {})))" |
744 also have "... \<le> Suc (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {})))" |
756 using alts_simp_control by blast |
745 using alts_simp_control by blast |
757 (*or using seq_list_estimate_control by blast*) |
|
758 also have "... \<le> Suc (Suc (N1 + (rsize r2)) + (N2 * card (sizeNregex N2)))" |
746 also have "... \<le> Suc (Suc (N1 + (rsize r2)) + (N2 * card (sizeNregex N2)))" |
759 using assms seq_estimate_bounded by blast |
747 using assms seq_estimate_bounded by blast |
760 ultimately show "rsize (rders_simp (RSEQ r1 r2) s) |
748 ultimately show "rsize (rders_simp (RSEQ r1 r2) s) |
761 \<le> max (Suc (Suc (N1 + rsize r2) + N2 * card (sizeNregex N2))) (rsize (RSEQ r1 r2))" |
749 \<le> max (Suc (Suc (N1 + rsize r2) + N2 * card (sizeNregex N2))) (rsize (RSEQ r1 r2))" |
762 by auto |
750 by auto |
763 qed |
751 qed |
764 |
|
765 thm seq_closed_form_bounded2 |
|
766 |
752 |
767 |
753 |
768 lemma rders_simp_bounded: |
754 lemma rders_simp_bounded: |
769 shows "\<exists>N. \<forall>s. rsize (rders_simp r s) \<le> N" |
755 shows "\<exists>N. \<forall>s. rsize (rders_simp r s) \<le> N" |
770 apply(induct r) |
756 apply(induct r) |