equal
deleted
inserted
replaced
1 |
1 |
2 theory ClosedFormsBounds |
2 theory ClosedFormsBounds |
3 imports "GeneralRegexBound" "ClosedForms" |
3 imports "GeneralRegexBound" "ClosedForms" |
4 begin |
4 begin |
|
5 |
|
6 |
5 lemma alts_ders_lambda_shape_ders: |
7 lemma alts_ders_lambda_shape_ders: |
6 shows "\<forall>r \<in> set (map (\<lambda>r. rders_simp r ( s)) rs ). \<exists>r1 \<in> set rs. r = rders_simp r1 s" |
8 shows "\<forall>r \<in> set (map (\<lambda>r. rders_simp r ( s)) rs ). \<exists>r1 \<in> set rs. r = rders_simp r1 s" |
7 by (simp add: image_iff) |
9 by (simp add: image_iff) |
8 |
10 |
9 lemma rlist_bound: |
11 lemma rlist_bound: |
11 shows "rsizes rs \<le> N * (length rs)" |
13 shows "rsizes rs \<le> N * (length rs)" |
12 using assms |
14 using assms |
13 apply(induct rs) |
15 apply(induct rs) |
14 apply simp |
16 apply simp |
15 by simp |
17 by simp |
|
18 |
|
19 lemma distinct_list_size_len_bounded: |
|
20 assumes "\<forall>r \<in> set rs. rsize r \<le> N" "length rs \<le> lrs" |
|
21 shows "rsizes rs \<le> lrs * N " |
|
22 using assms |
|
23 by (metis rlist_bound dual_order.trans mult.commute mult_le_mono1) |
16 |
24 |
17 lemma alts_closed_form_bounded: |
25 lemma alts_closed_form_bounded: |
18 assumes "\<forall>r \<in> set rs. \<forall>s. rsize (rders_simp r s) \<le> N" |
26 assumes "\<forall>r \<in> set rs. \<forall>s. rsize (rders_simp r s) \<le> N" |
19 shows "rsize (rders_simp (RALTS rs) s) \<le> max (Suc (N * (length rs))) (rsize (RALTS rs))" |
27 shows "rsize (rders_simp (RALTS rs) s) \<le> max (Suc (N * (length rs))) (rsize (RALTS rs))" |
20 proof (cases s) |
28 proof (cases s) |
308 apply(case_tac "a \<in> ss") |
316 apply(case_tac "a \<in> ss") |
309 apply simp |
317 apply simp |
310 by (simp add: larger_acc_smaller_distinct_res) |
318 by (simp add: larger_acc_smaller_distinct_res) |
311 |
319 |
312 |
320 |
313 lemma distinct_list_size_len_bounded: |
|
314 assumes "\<forall>r \<in> set rs. rsize r \<le> N" "length rs \<le> lrs" |
|
315 shows "rsizes rs \<le> lrs * N " |
|
316 using assms |
|
317 by (metis rlist_bound dual_order.trans mult.commute mult_le_mono1) |
|
318 |
321 |
319 |
322 |
320 |
323 |
321 lemma rdistinct_same_set: |
324 lemma rdistinct_same_set: |
322 shows "r \<in> set rs \<longleftrightarrow> r \<in> set (rdistinct rs {})" |
325 shows "r \<in> set rs \<longleftrightarrow> r \<in> set (rdistinct rs {})" |