513 |
513 |
514 lemma alts_simp_control: |
514 lemma alts_simp_control: |
515 shows "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct rs {})))" |
515 shows "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct rs {})))" |
516 proof - |
516 proof - |
517 have "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct (rflts (map rsimp rs)) {})))" |
517 have "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct (rflts (map rsimp rs)) {})))" |
518 |
518 using alts_simp_ineq_unfold by auto |
519 using alts_simp_ineq_unfold by auto |
519 moreover have "\<dots> \<le> Suc (sum_list (map rsize (rdistinct (map rsimp rs) {})))" |
520 then have "\<dots> \<le> Suc (sum_list (map rsize (rdistinct (map rsimp rs) {})))" |
|
521 using without_flts_ineq by blast |
520 using without_flts_ineq by blast |
522 |
521 ultimately show "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct rs {})))" |
523 show "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct rs {})))" |
522 by (meson distinct_simp_ineq order.trans) |
524 by (meson \<open>Suc (sum_list (map rsize (rdistinct (rflts (map rsimp rs)) {}))) \<le> Suc (sum_list (map rsize (rdistinct (map rsimp rs) {})))\<close> \<open>rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct (rflts (map rsimp rs)) {})))\<close> distinct_simp_ineq order_trans) |
|
525 qed |
523 qed |
526 |
524 |
527 |
525 |
528 |
526 |
529 lemma rdistinct_equality1: |
527 lemma rdistinct_equality1: |
737 apply(subgoal_tac "\<forall>r \<in> set (rdistinct (map (rders_simp r2) (vsuf s r1)) {}). rsize r \<le> N2") |
735 apply(subgoal_tac "\<forall>r \<in> set (rdistinct (map (rders_simp r2) (vsuf s r1)) {}). rsize r \<le> N2") |
738 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) |
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) |
739 using assms(2) map_ders_is_list_of_ders by blast |
737 using assms(2) map_ders_is_list_of_ders by blast |
740 |
738 |
741 |
739 |
742 lemma seq_closed_form_bounded: shows |
740 |
743 "\<lbrakk>\<forall>s. rsize (rders_simp r1 s) \<le> N1 ; \<forall>s. rsize (rders_simp r2 s) \<le> N2\<rbrakk> \<Longrightarrow> |
741 lemma seq_closed_form_bounded2: |
744 rsize (rders_simp (RSEQ r1 r2) s) \<le> |
742 assumes "\<forall>s. rsize (rders_simp r1 s) \<le> N1" |
745 max (Suc (Suc (N1 + (rsize r2)) + (N2 * card (sizeNregex N2)))) (rsize (RSEQ r1 r2)) " |
743 and "\<forall>s. rsize (rders_simp r2 s) \<le> N2" |
746 apply(case_tac s) |
744 shows "rsize (rders_simp (RSEQ r1 r2) s) \<le> max (Suc (Suc (N1 + (rsize r2)) + (N2 * card (sizeNregex N2)))) (rsize (RSEQ r1 r2))" |
747 apply simp |
745 proof(cases s) |
748 apply(subgoal_tac " (rders_simp (RSEQ r1 r2) s) = |
746 case Nil |
749 rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # (map (rders_simp r2) (vsuf s r1))))") |
747 then show "rsize (rders_simp (RSEQ r1 r2) s) |
750 prefer 2 |
748 \<le> max (Suc (Suc (N1 + rsize r2) + N2 * card (sizeNregex N2))) (rsize (RSEQ r1 r2))" |
751 using seq_closed_form_variant apply blast |
749 by simp |
752 apply(subgoal_tac "rsize (rsimp (RALTS (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)))) |
750 next |
753 \<le> |
751 case (Cons a list) |
754 Suc (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {})))") |
752 then have "rsize (rders_simp (RSEQ r1 r2) s) = |
755 apply(subgoal_tac "Suc (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {}))) |
753 rsize (rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # (map (rders_simp r2) (vsuf s r1)))))" |
756 \<le> Suc (Suc (N1 + (rsize r2)) + (N2 * card (sizeNregex N2)))") |
754 using seq_closed_form_variant by (metis list.discI) |
757 prefer 2 |
755 also have "... \<le> Suc (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {})))" |
758 using seq_estimate_bounded apply blast |
756 using alts_simp_control by blast |
759 apply(subgoal_tac "rsize (rders_simp (RSEQ r1 r2) s) \<le> Suc (Suc (N1 + rsize r2) + N2 * card (sizeNregex N2))") |
757 (*or using seq_list_estimate_control by blast*) |
760 using le_max_iff_disj apply blast |
758 also have "... \<le> Suc (Suc (N1 + (rsize r2)) + (N2 * card (sizeNregex N2)))" |
761 apply auto[1] |
759 using assms seq_estimate_bounded by blast |
762 using seq_list_estimate_control by presburger |
760 ultimately show "rsize (rders_simp (RSEQ r1 r2) s) |
763 |
761 \<le> max (Suc (Suc (N1 + rsize r2) + N2 * card (sizeNregex N2))) (rsize (RSEQ r1 r2))" |
764 |
762 by auto |
765 lemma rders_simp_bounded: shows |
763 qed |
766 "\<exists>N. \<forall>s. rsize (rders_simp r s) \<le> N" |
764 |
|
765 thm seq_closed_form_bounded2 |
|
766 |
|
767 |
|
768 lemma rders_simp_bounded: |
|
769 shows "\<exists>N. \<forall>s. rsize (rders_simp r s) \<le> N" |
767 apply(induct r) |
770 apply(induct r) |
768 apply(rule_tac x = "Suc 0 " in exI) |
771 apply(rule_tac x = "Suc 0 " in exI) |
769 using three_easy_cases0 apply force |
772 using three_easy_cases0 apply force |
770 using three_easy_cases1 apply blast |
773 using three_easy_cases1 apply blast |
771 using three_easy_casesC apply blast |
774 using three_easy_casesC apply blast |
772 using seq_closed_form_bounded apply blast |
775 apply(erule exE)+ |
|
776 apply(rule exI) |
|
777 apply(rule allI) |
|
778 apply(rule seq_closed_form_bounded2) |
|
779 apply(assumption) |
|
780 apply(assumption) |
773 apply (metis alts_closed_form_bounded size_list_estimation') |
781 apply (metis alts_closed_form_bounded size_list_estimation') |
774 using star_closed_form_bounded by blast |
782 using star_closed_form_bounded by blast |
775 |
783 |
776 |
784 |
777 |
785 |