1 |
1 |
2 theory ClosedFormsBounds |
2 theory ClosedFormsBounds |
3 imports "GeneralRegexBound" "ClosedForms" |
3 imports "GeneralRegexBound" "ClosedForms" |
4 begin |
4 begin |
5 |
5 |
|
6 lemma alts_ders_lambda_shape_ders: |
|
7 shows "\<forall>r \<in> set (map (\<lambda>r. rders_simp r ( s)) rs ). \<exists>r1 \<in> set rs. r = rders_simp r1 s" |
|
8 by (simp add: image_iff) |
|
9 |
|
10 |
|
11 |
|
12 lemma rlist_bound: |
|
13 shows "\<forall>r \<in> set rs. rsize r \<le> N \<Longrightarrow> sum_list (map rsize rs) \<le> N * (length rs)" |
|
14 apply(induct rs) |
|
15 apply simp |
|
16 by simp |
6 |
17 |
7 |
18 |
8 lemma alts_closed_form_bounded: shows |
19 lemma alts_closed_form_bounded: shows |
9 "\<forall>r \<in> set rs. \<forall>s. rsize(rders_simp r s ) \<le> N \<Longrightarrow> |
20 "\<forall>r \<in> set rs. \<forall>s. rsize(rders_simp r s ) \<le> N \<Longrightarrow> |
10 rsize (rders_simp (RALTS rs ) s) \<le> max (Suc ( N * (card (sizeNregex N)))) (rsize (RALTS rs) )" |
21 rsize (rders_simp (RALTS rs ) s) \<le> max (Suc ( N * (length rs))) (rsize (RALTS rs) )" |
11 apply(induct s) |
22 apply(induct s) |
12 apply simp |
23 apply simp |
13 apply(insert alts_closed_form_variant) |
24 apply(subst alts_closed_form_variant) |
14 |
25 apply force |
|
26 apply(subgoal_tac "rsize (rsimp (RALTS (map (\<lambda>r. rders_simp r (a # s)) rs))) \<le> rsize ( (RALTS (map (\<lambda>r. rders_simp r (a # s)) rs)))") |
|
27 prefer 2 |
|
28 using rsimp_mono apply presburger |
|
29 apply(subgoal_tac "rsize (RALTS (map (\<lambda>r. rders_simp r (a # s)) rs)) = |
|
30 Suc (sum_list (map rsize (map (\<lambda>r. rders_simp r (a # s)) rs)))") |
|
31 prefer 2 |
|
32 using rsize.simps(4) apply blast |
|
33 apply(subgoal_tac "sum_list (map rsize (map (\<lambda>r. rders_simp r (a # s)) rs )) \<le> N * (length rs) ") |
|
34 apply linarith |
|
35 apply(subgoal_tac "\<forall>r \<in> set (map (\<lambda>r. rders_simp r (a # s)) rs ). rsize r \<le> N") |
|
36 prefer 2 |
|
37 apply(subgoal_tac "\<forall>r \<in> set (map (\<lambda>r. rders_simp r (a # s)) rs ). \<exists>r1 \<in> set rs. r = rders_simp r1 (a # s)") |
|
38 prefer 2 |
|
39 using alts_ders_lambda_shape_ders apply presburger |
|
40 apply metis |
|
41 apply(frule rlist_bound) |
|
42 by fastforce |
|
43 |
|
44 |
|
45 lemma alts_simp_ineq_unfold: |
|
46 shows "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct (rflts (map rsimp rs)) {})))" |
|
47 using rsimp_aalts_smaller by auto |
|
48 |
|
49 lemma flts_has_no_zero: |
|
50 shows "rdistinct (rflts rs) rset = rdistinct (rflts rs) (insert RZERO rset)" |
|
51 |
|
52 sorry |
|
53 |
|
54 lemma not_mentioned_elem_distinct: |
|
55 shows "r \<noteq> a \<Longrightarrow> (r \<in> set (rdistinct rs {})) = (r \<in> set (rdistinct rs {a}))" |
|
56 sorry |
|
57 |
|
58 |
|
59 |
|
60 lemma flts_vs_nflts: |
|
61 shows "\<forall>r \<in> noalts_set. \<forall>xs. r \<noteq> RALTS xs |
|
62 \<and> (\<forall>a \<in> alts_set. \<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set) |
|
63 \<Longrightarrow> Suc (sum_list (map rsize (rdistinct ( rflts rs) (noalts_set \<union> corr_set) ))) |
|
64 \<le> Suc (sum_list (map rsize (rdistinct rs (noalts_set \<union> alts_set) )))" |
|
65 apply(induct rs arbitrary: noalts_set) |
|
66 apply simp |
|
67 |
|
68 sorry |
|
69 |
|
70 lemma distinct_simp_ineq_general: |
|
71 shows "rsimp ` no_simp = has_simp \<Longrightarrow>Suc (sum_list (map rsize (rdistinct (map rsimp rs) has_simp))) |
|
72 \<le> Suc (sum_list (map rsize (rdistinct rs no_simp)))" |
|
73 |
|
74 sorry |
|
75 |
|
76 |
|
77 lemma without_flts_ineq: |
|
78 shows " Suc (sum_list (map rsize (rdistinct (rflts rs) {}) )) \<le> |
|
79 Suc (sum_list (map rsize (rdistinct ( rs ) {} )))" |
|
80 by (metis empty_iff flts_vs_nflts sup_bot_left) |
|
81 |
|
82 |
|
83 |
|
84 |
|
85 lemma distinct_simp_ineq: |
|
86 shows "Suc (sum_list (map rsize (rdistinct (map rsimp rs) {}))) |
|
87 \<le> Suc (sum_list (map rsize (rdistinct rs {})))" |
15 |
88 |
16 sorry |
89 using distinct_simp_ineq_general by blast |
|
90 |
|
91 |
|
92 |
|
93 |
|
94 lemma alts_simp_control: |
|
95 shows "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct rs {})))" |
|
96 proof - |
|
97 have "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct (rflts (map rsimp rs)) {})))" |
|
98 |
|
99 using alts_simp_ineq_unfold by auto |
|
100 then have "\<dots> \<le> Suc (sum_list (map rsize (rdistinct (map rsimp rs) {})))" |
|
101 using without_flts_ineq by blast |
|
102 |
|
103 show "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct rs {})))" |
|
104 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) |
|
105 qed |
|
106 |
|
107 |
|
108 |
|
109 lemma rdistinct_equality1: |
|
110 shows "a \<notin> ss \<Longrightarrow> rdistinct (a # rs) ss = a # rdistinct rs (insert a ss) " |
|
111 by auto |
|
112 |
|
113 lemma larger_acc_smaller_distinct_res0: |
|
114 shows " ss \<subseteq> SS \<Longrightarrow> sum_list (map rsize (rdistinct rs SS)) \<le> sum_list (map rsize (rdistinct rs ss))" |
|
115 apply(induct rs arbitrary: ss SS) |
|
116 apply simp |
|
117 apply(case_tac "a \<in> ss") |
|
118 apply(subgoal_tac "a \<in> SS") |
|
119 apply simp |
|
120 apply blast |
|
121 apply(case_tac "a \<in> SS") |
|
122 apply simp |
|
123 apply(subgoal_tac "insert a ss \<subseteq> SS") |
|
124 apply simp |
|
125 apply (simp add: trans_le_add2) |
|
126 apply blast |
|
127 apply(simp) |
|
128 apply(subgoal_tac "insert a ss \<subseteq> insert a SS") |
|
129 apply blast |
|
130 by blast |
|
131 |
|
132 |
|
133 lemma larger_acc_smaller_distinct_res: |
|
134 shows " (sum_list (map rsize (rdistinct rs ss))) \<ge> (sum_list (map rsize (rdistinct rs (insert a ss))))" |
|
135 apply(subgoal_tac "ss \<subseteq> (insert a ss)") |
|
136 apply(rule larger_acc_smaller_distinct_res0) |
|
137 apply simp |
|
138 by (simp add: subset_insertI) |
|
139 |
|
140 lemma size_list_triangle1: |
|
141 shows "sum_list (map rsize (a # (rdistinct as ss))) \<ge> rsize a + sum_list (map rsize (rdistinct as (insert a ss)))" |
|
142 by (simp add: larger_acc_smaller_distinct_res) |
|
143 |
|
144 |
|
145 lemma triangle_inequality_distinct: |
|
146 shows "sum_list (map rsize (rdistinct (a # rs) ss)) \<le> rsize a + (sum_list (map rsize (rdistinct rs ss)))" |
|
147 apply(case_tac "a \<in> ss") |
|
148 apply simp |
|
149 apply(subst rdistinct_equality1) |
|
150 apply simp |
|
151 using size_list_triangle1 by auto |
|
152 |
|
153 lemma same_regex_property_after_map: |
|
154 shows "\<forall>s. P (f r2 s) \<Longrightarrow> \<forall>r \<in> set (map (f r2) Ss). P r" |
|
155 by auto |
|
156 |
|
157 lemma same_property_after_distinct: |
|
158 shows " \<forall>r \<in> set (map (f r2) Ss). P r \<Longrightarrow> \<forall>r \<in> set (rdistinct (map (f r2) Ss) xset). P r" |
|
159 apply(induct Ss arbitrary: xset) |
|
160 apply simp |
|
161 by auto |
|
162 |
|
163 lemma same_regex_property_after_distinct: |
|
164 shows "\<forall>s. P (f r2 s) \<Longrightarrow> \<forall>r \<in> set (rdistinct (map (f r2) Ss) xset). P r" |
|
165 apply(rule same_property_after_distinct) |
|
166 apply(rule same_regex_property_after_map) |
|
167 by simp |
|
168 |
|
169 |
|
170 |
|
171 lemma Sum_cons: |
|
172 shows "distinct (a # as) \<Longrightarrow> \<Sum> (set ((a::nat) # as)) = a + \<Sum> (set as)" |
|
173 by simp |
|
174 |
|
175 |
|
176 lemma distinct_list_sizeNregex_bounded: |
|
177 shows "distinct rs \<and> (\<forall> r \<in> (set rs). rsize r \<le> N) \<Longrightarrow> sum_list (map rsize rs) \<le> N * length rs" |
|
178 apply(induct rs) |
|
179 apply simp |
|
180 by simp |
|
181 |
|
182 |
|
183 lemma distinct_list_size_len_bounded: |
|
184 shows "distinct rs \<and> (\<forall>r \<in> set rs. rsize r \<le> N) \<and> length rs \<le> lrs \<Longrightarrow> sum_list (map rsize rs) \<le> lrs * N " |
|
185 by (metis distinct_list_sizeNregex_bounded dual_order.trans mult.commute mult_le_mono1) |
|
186 |
|
187 |
|
188 |
|
189 lemma rdistinct_same_set: |
|
190 shows "(r \<in> set rs) = (r \<in> set (rdistinct rs {}))" |
|
191 apply(induct rs) |
|
192 apply simp |
|
193 apply(case_tac "a \<in> set rs") |
|
194 apply(case_tac "r = a") |
|
195 apply (simp) |
|
196 apply (simp add: not_mentioned_elem_distinct) |
|
197 using not_mentioned_elem_distinct by fastforce |
|
198 |
|
199 |
|
200 |
|
201 lemma distinct_list_rexp_up_to_certain_size_bouded_by_set_enumerating_up_to_that_size: |
|
202 shows "\<forall>r\<in> set rs. (rsize r ) \<le> N \<Longrightarrow> sum_list (map rsize (rdistinct rs {})) \<le> |
|
203 (card (sizeNregex N))* N" |
|
204 apply(subgoal_tac "distinct (rdistinct rs {})") |
|
205 prefer 2 |
|
206 using rdistinct_does_the_job apply blast |
|
207 apply(subgoal_tac "length (rdistinct rs {}) \<le> card (sizeNregex N)") |
|
208 apply(rule distinct_list_size_len_bounded) |
|
209 apply(rule conjI)+ |
|
210 apply simp |
|
211 apply(rule conjI) |
|
212 apply (meson rdistinct_same_set) |
|
213 apply blast |
|
214 apply(subgoal_tac "\<forall>r \<in> set (rdistinct rs {}). rsize r \<le> N") |
|
215 prefer 2 |
|
216 apply (meson rdistinct_same_set) |
|
217 apply(subgoal_tac "length (rdistinct rs {}) = card (set (rdistinct rs {}))") |
|
218 prefer 2 |
|
219 using set_related_list apply blast |
|
220 apply(simp only:) |
|
221 by (metis card_mono finite_size_n mem_Collect_eq sizeNregex_def subset_code(1)) |
|
222 |
|
223 |
|
224 |
17 |
225 |
18 |
226 |
19 |
227 |
20 lemma star_closed_form_bounded_by_rdistinct_list_estimate: |
228 lemma star_closed_form_bounded_by_rdistinct_list_estimate: |
21 shows "rsize (rsimp ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) |
229 shows "rsize (rsimp ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) |
22 (star_updates s r0 [[c]]) ) ))) \<le> |
230 (star_updates s r0 [[c]]) ) ))) \<le> |
23 Suc (sum_list (map rsize (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) |
231 Suc (sum_list (map rsize (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) |
24 (star_updates s r0 [[c]]) ) {}) ) )" |
232 (star_updates s r0 [[c]]) ) {}) ) )" |
25 |
233 by (metis alts_simp_control ) |
26 sorry |
234 |
27 |
235 |
28 lemma distinct_list_rexp_up_to_certain_size_bouded_by_set_enumerating_up_to_that_size: |
236 |
29 shows "\<forall>r\<in> set rs. (rsize r ) \<le> N \<Longrightarrow> sum_list (map rsize (rdistinct rs {})) \<le> |
237 |
30 (card (sizeNregex N))* N" |
238 lemma star_lambda_form: |
31 |
239 shows "\<forall> r \<in> set (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) ls). |
32 sorry |
240 \<exists>s2. r = RSEQ (rders_simp r0 s2) (RSTAR r0) " |
|
241 by (meson ex_map_conv) |
33 |
242 |
34 |
243 |
35 lemma star_lambda_ders: |
244 lemma star_lambda_ders: |
36 shows " \<forall>s. rsize (rders_simp r0 s) \<le> N \<Longrightarrow> |
245 shows " \<forall>s. rsize (rders_simp r0 s) \<le> N \<Longrightarrow> |
37 \<forall>r\<in>set (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) (star_updates s r0 [[c]])). |
246 \<forall>r\<in>set (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) (star_updates s r0 [[c]])). |
38 rsize r \<le> Suc (N + rsize (RSTAR r0))" |
247 rsize r \<le> Suc (N + rsize (RSTAR r0))" |
39 sorry |
248 apply(insert star_lambda_form) |
|
249 apply(simp) |
|
250 done |
|
251 |
|
252 |
40 |
253 |
41 |
254 |
42 lemma star_control_bounded: |
255 lemma star_control_bounded: |
43 shows "\<forall>s. rsize (rders_simp r0 s) \<le> N \<Longrightarrow> |
256 shows "\<forall>s. rsize (rders_simp r0 s) \<le> N \<Longrightarrow> |
44 (sum_list (map rsize (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) |
257 (sum_list (map rsize (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) |
88 (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) (star_updates list r0 [[a]])) {}))) |
301 (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) (star_updates list r0 [[a]])) {}))) |
89 \<le> (Suc (card (sizeNregex (Suc (N + rsize (RSTAR r0))))) * Suc (N + rsize (RSTAR r0))) ") |
302 \<le> (Suc (card (sizeNregex (Suc (N + rsize (RSTAR r0))))) * Suc (N + rsize (RSTAR r0))) ") |
90 apply auto[1] |
303 apply auto[1] |
91 using star_control_variant by blast |
304 using star_control_variant by blast |
92 |
305 |
93 lemma alts_simp_ineq_unfold: |
|
94 shows "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct (rflts (map rsimp rs)) {})))" |
|
95 using rsimp_aalts_smaller by auto |
|
96 |
|
97 lemma flts_has_no_zero: |
|
98 shows "rdistinct (rflts rs) rset = rdistinct (rflts rs) (insert RZERO rset)" |
|
99 sorry |
|
100 |
|
101 lemma flts_vs_nflts: |
|
102 shows "\<forall>r \<in> noalts_set. \<forall>xs. r \<noteq> RALTS xs |
|
103 \<and> (\<forall>a \<in> alts_set. \<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set) |
|
104 \<Longrightarrow> Suc (sum_list (map rsize (rdistinct ( rflts rs) (noalts_set \<union> corr_set) ))) |
|
105 \<le> Suc (sum_list (map rsize (rdistinct rs (noalts_set \<union> alts_set) )))" |
|
106 apply(induct rs arbitrary: noalts_set) |
|
107 apply simp |
|
108 |
|
109 sorry |
|
110 |
|
111 |
|
112 lemma without_flts_ineq: |
|
113 shows " Suc (sum_list (map rsize (rdistinct (rflts rs) {}) )) \<le> |
|
114 Suc (sum_list (map rsize (rdistinct ( rs ) {} )))" |
|
115 by (metis empty_iff flts_vs_nflts sup_bot_left) |
|
116 |
|
117 |
|
118 lemma distinct_simp_ineq_general: |
|
119 shows "rsimp ` no_simp = has_simp \<Longrightarrow>Suc (sum_list (map rsize (rdistinct (map rsimp rs) has_simp))) |
|
120 \<le> Suc (sum_list (map rsize (rdistinct rs no_simp)))" |
|
121 sorry |
|
122 |
|
123 |
|
124 lemma distinct_simp_ineq: |
|
125 shows "Suc (sum_list (map rsize (rdistinct (map rsimp rs) {}))) |
|
126 \<le> Suc (sum_list (map rsize (rdistinct rs {})))" |
|
127 |
|
128 using distinct_simp_ineq_general by blast |
|
129 |
|
130 |
|
131 |
|
132 |
|
133 lemma alts_simp_control: |
|
134 shows "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct rs {})))" |
|
135 proof - |
|
136 have "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct (rflts (map rsimp rs)) {})))" |
|
137 |
|
138 using alts_simp_ineq_unfold by auto |
|
139 then have "\<dots> \<le> Suc (sum_list (map rsize (rdistinct (map rsimp rs) {})))" |
|
140 using without_flts_ineq by blast |
|
141 |
|
142 show "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct rs {})))" |
|
143 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) |
|
144 qed |
|
145 |
|
146 |
|
147 |
|
148 |
306 |
149 lemma seq_list_estimate_control: shows |
307 lemma seq_list_estimate_control: shows |
150 " rsize (rsimp (RALTS (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)))) |
308 " rsize (rsimp (RALTS (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)))) |
151 \<le> Suc (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {})))" |
309 \<le> Suc (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {})))" |
152 by(metis alts_simp_control) |
310 by(metis alts_simp_control) |
153 |
|
154 lemma rdistinct_equality1: |
|
155 shows "a \<notin> ss \<Longrightarrow> rdistinct (a # rs) ss = a # rdistinct rs (insert a ss) " |
|
156 by auto |
|
157 |
|
158 lemma larger_acc_smaller_distinct_res0: |
|
159 shows " ss \<subseteq> SS \<Longrightarrow> sum_list (map rsize (rdistinct rs SS)) \<le> sum_list (map rsize (rdistinct rs ss))" |
|
160 apply(induct rs arbitrary: ss SS) |
|
161 apply simp |
|
162 apply(case_tac "a \<in> ss") |
|
163 apply(subgoal_tac "a \<in> SS") |
|
164 apply simp |
|
165 apply blast |
|
166 apply(case_tac "a \<in> SS") |
|
167 apply simp |
|
168 apply(subgoal_tac "insert a ss \<subseteq> SS") |
|
169 apply simp |
|
170 apply (simp add: trans_le_add2) |
|
171 apply blast |
|
172 apply(simp) |
|
173 apply(subgoal_tac "insert a ss \<subseteq> insert a SS") |
|
174 apply blast |
|
175 by blast |
|
176 |
|
177 |
|
178 lemma larger_acc_smaller_distinct_res: |
|
179 shows " (sum_list (map rsize (rdistinct rs ss))) \<ge> (sum_list (map rsize (rdistinct rs (insert a ss))))" |
|
180 apply(subgoal_tac "ss \<subseteq> (insert a ss)") |
|
181 apply(rule larger_acc_smaller_distinct_res0) |
|
182 apply simp |
|
183 by (simp add: subset_insertI) |
|
184 |
|
185 lemma size_list_triangle1: |
|
186 shows "sum_list (map rsize (a # (rdistinct as ss))) \<ge> rsize a + sum_list (map rsize (rdistinct as (insert a ss)))" |
|
187 by (simp add: larger_acc_smaller_distinct_res) |
|
188 |
|
189 |
|
190 lemma triangle_inequality_distinct: |
|
191 shows "sum_list (map rsize (rdistinct (a # rs) ss)) \<le> rsize a + (sum_list (map rsize (rdistinct rs ss)))" |
|
192 apply(case_tac "a \<in> ss") |
|
193 apply simp |
|
194 apply(subst rdistinct_equality1) |
|
195 apply simp |
|
196 using size_list_triangle1 by auto |
|
197 |
|
198 lemma same_regex_property_after_map: |
|
199 shows "\<forall>s. P (f r2 s) \<Longrightarrow> \<forall>r \<in> set (map (f r2) Ss). P r" |
|
200 by auto |
|
201 |
|
202 lemma same_property_after_distinct: |
|
203 shows " \<forall>r \<in> set (map (f r2) Ss). P r \<Longrightarrow> \<forall>r \<in> set (rdistinct (map (f r2) Ss) xset). P r" |
|
204 apply(induct Ss arbitrary: xset) |
|
205 apply simp |
|
206 by auto |
|
207 |
|
208 lemma same_regex_property_after_distinct: |
|
209 shows "\<forall>s. P (f r2 s) \<Longrightarrow> \<forall>r \<in> set (rdistinct (map (f r2) Ss) xset). P r" |
|
210 apply(rule same_property_after_distinct) |
|
211 apply(rule same_regex_property_after_map) |
|
212 by simp |
|
213 |
311 |
214 lemma map_ders_is_list_of_ders: |
312 lemma map_ders_is_list_of_ders: |
215 shows "\<forall>s. rsize (rders_simp r2 s) \<le> N2 \<Longrightarrow> |
313 shows "\<forall>s. rsize (rders_simp r2 s) \<le> N2 \<Longrightarrow> |
216 \<forall>r \<in> set (rdistinct (map (rders_simp r2) Ss) {}). rsize r \<le> N2" |
314 \<forall>r \<in> set (rdistinct (map (rders_simp r2) Ss) {}). rsize r \<le> N2" |
217 apply(rule same_regex_property_after_distinct) |
315 apply(rule same_regex_property_after_distinct) |