86 " rsize (rsimp (RALTS (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)))) |
87 " rsize (rsimp (RALTS (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)))) |
87 \<le> Suc (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {})))" |
88 \<le> Suc (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {})))" |
88 |
89 |
89 sorry |
90 sorry |
90 |
91 |
|
92 lemma triangle_inequality_distinct: |
|
93 shows "sum_list (map rsize (rdistinct (a # rs) ss)) \<le> rsize a + (sum_list (map rsize (rdistinct rs ss)))" |
|
94 apply(arbitrary: ss) |
|
95 apply simp |
|
96 apply(case_tac "a \<in> ss") |
|
97 apply simp |
|
98 |
|
99 sorry |
|
100 |
|
101 lemma same_regex_property_after_map: |
|
102 shows "\<forall>s. P (f r2 s) \<Longrightarrow> \<forall>r \<in> set (map (f r2) Ss). P r" |
|
103 by auto |
|
104 |
|
105 lemma same_property_after_distinct: |
|
106 shows " \<forall>r \<in> set (map (f r2) Ss). P r \<Longrightarrow> \<forall>r \<in> set (rdistinct (map (f r2) Ss) xset). P r" |
|
107 apply(induct Ss arbitrary: xset) |
|
108 apply simp |
|
109 by auto |
|
110 |
|
111 lemma same_regex_property_after_distinct: |
|
112 shows "\<forall>s. P (f r2 s) \<Longrightarrow> \<forall>r \<in> set (rdistinct (map (f r2) Ss) xset). P r" |
|
113 apply(rule same_property_after_distinct) |
|
114 apply(rule same_regex_property_after_map) |
|
115 by simp |
|
116 |
|
117 lemma map_ders_is_list_of_ders: |
|
118 shows "\<forall>s. rsize (rders_simp r2 s) \<le> N2 \<Longrightarrow> |
|
119 \<forall>r \<in> set (rdistinct (map (rders_simp r2) Ss) {}). rsize r \<le> N2" |
|
120 apply(rule same_regex_property_after_distinct) |
|
121 by simp |
|
122 |
91 lemma seq_estimate_bounded: |
123 lemma seq_estimate_bounded: |
92 assumes "\<forall>s. rsize (rders_simp r1 s) \<le> N1" and "\<forall>s. rsize (rders_simp r2 s) \<le> N2" |
124 assumes "\<forall>s. rsize (rders_simp r1 s) \<le> N1" and "\<forall>s. rsize (rders_simp r2 s) \<le> N2" |
93 shows |
125 shows |
94 "Suc (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {}))) \<le> |
126 "Suc (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {}))) \<le> |
95 Suc (Suc (N1 + (rsize r2)) + (N2 * card (sizeNregex N2)))" |
127 Suc (Suc (N1 + (rsize r2)) + (N2 * card (sizeNregex N2)))" |
|
128 apply(subgoal_tac " (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {}))) \<le> |
|
129 (Suc (N1 + (rsize r2)) + (N2 * card (sizeNregex N2)))") |
|
130 apply force |
|
131 apply(subgoal_tac " (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {}))) \<le> |
|
132 (rsize (RSEQ (rders_simp r1 s) r2)) + (sum_list (map rsize (rdistinct (map (rders_simp r2) (vsuf s r1)) {})) )") |
|
133 prefer 2 |
|
134 using triangle_inequality_distinct apply blast |
|
135 apply(subgoal_tac " sum_list (map rsize (rdistinct (map (rders_simp r2) (vsuf s r1)) {})) \<le> N2 * card (sizeNregex N2) ") |
|
136 apply(subgoal_tac "rsize (RSEQ (rders_simp r1 s) r2) \<le> Suc (N1 + rsize r2)") |
|
137 apply linarith |
|
138 apply (simp add: assms(1)) |
|
139 apply(subgoal_tac "\<forall>r \<in> set (rdistinct (map (rders_simp r2) (vsuf s r1)) {}). rsize r \<le> N2") |
|
140 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) |
|
141 using assms(2) map_ders_is_list_of_ders by blast |
96 |
142 |
97 sorry |
|
98 |
143 |
99 lemma seq_closed_form_bounded: shows |
144 lemma seq_closed_form_bounded: shows |
100 "\<lbrakk>\<forall>s. rsize (rders_simp r1 s) \<le> N1 ; \<forall>s. rsize (rders_simp r2 s) \<le> N2\<rbrakk> \<Longrightarrow> |
145 "\<lbrakk>\<forall>s. rsize (rders_simp r1 s) \<le> N1 ; \<forall>s. rsize (rders_simp r2 s) \<le> N2\<rbrakk> \<Longrightarrow> |
101 rsize (rders_simp (RSEQ r1 r2) s) \<le> |
146 rsize (rders_simp (RSEQ r1 r2) s) \<le> |
102 max (Suc (Suc (N1 + (rsize r2)) + (N2 * card (sizeNregex N2)))) (rsize (RSEQ r1 r2)) " |
147 max (Suc (Suc (N1 + (rsize r2)) + (N2 * card (sizeNregex N2)))) (rsize (RSEQ r1 r2)) " |
143 |
188 |
144 |
189 |
145 |
190 |
146 |
191 |
147 |
192 |
148 |
|
149 |
|
150 |
|
151 |
|
152 |
|
153 |
|
154 |
|
155 |
|
156 |
|
157 |
|
158 (*Obsolete materials*) |
193 (*Obsolete materials*) |
159 |
|
160 |
|
161 lemma rexp_size_induct: |
|
162 shows "\<And>N r x5 a list. |
|
163 \<lbrakk> rsize r = Suc N; r = RALTS x5; |
|
164 x5 = a # list\<rbrakk> \<Longrightarrow>\<exists>i j. rsize a = i \<and> rsize (RALTS list) = j \<and> i + j = Suc N \<and> i \<le> N \<and> j \<le> N" |
|
165 apply(rule_tac x = "rsize a" in exI) |
|
166 apply(rule_tac x = "rsize (RALTS list)" in exI) |
|
167 apply(subgoal_tac "rsize a \<ge> 1") |
|
168 prefer 2 |
|
169 using One_nat_def non_zero_size apply presburger |
|
170 apply(subgoal_tac "rsize (RALTS list) \<ge> 1 ") |
|
171 prefer 2 |
|
172 using size_geq1 apply blast |
|
173 apply simp |
|
174 done |
|
175 |
|
176 |
|
177 |
|
178 |
|
179 |
|
180 |
|
181 |
|
182 |
|
183 |
|
184 |
|
185 |
|
186 |
|
187 |
|
188 |
|
189 |
|
190 |
|
191 |
|
192 |
|
193 |
|
194 |
|
195 |
|
196 |
|
197 lemma star_update_case1: |
|
198 shows "rnullable (rders_simp r s) \<Longrightarrow> star_update c r (s # Ss) = (s @ [c]) # [c] # (star_update c r Ss)" |
|
199 |
|
200 by force |
|
201 |
|
202 lemma star_update_case2: |
|
203 shows "\<not>rnullable (rders_simp r s) \<Longrightarrow> star_update c r (s # Ss) = (s @ [c]) # (star_update c r Ss)" |
|
204 by simp |
|
205 |
|
206 lemma bubble_break: shows "rflts [r, RZERO] = rflts [r]" |
|
207 apply(case_tac r) |
|
208 apply simp+ |
|
209 done |
|
210 |
|
211 lemma rsimp_alts_idem_aux1: |
|
212 shows "rsimp_ALTs (rdistinct (rflts [rsimp a]) {}) = rsimp (RALTS [a])" |
|
213 by force |
|
214 |
|
215 |
|
216 |
|
217 lemma rsimp_alts_idem_aux2: |
|
218 shows "rsimp a = rsimp (RALTS [a])" |
|
219 apply(simp) |
|
220 apply(case_tac "rsimp a") |
|
221 apply simp+ |
|
222 apply (metis no_alt_short_list_after_simp no_further_dB_after_simp) |
|
223 by simp |
|
224 |
|
225 lemma rsimp_alts_idem: |
|
226 shows "rsimp (rsimp_ALTs (a # as)) = rsimp (rsimp_ALTs (a # [(rsimp (rsimp_ALTs as))] ))" |
|
227 apply(induct as) |
|
228 apply(subgoal_tac "rsimp (rsimp_ALTs [a, rsimp (rsimp_ALTs [])]) = rsimp (rsimp_ALTs [a, RZERO])") |
|
229 prefer 2 |
|
230 apply simp |
|
231 using bubble_break rsimp_alts_idem_aux2 apply auto[1] |
|
232 apply(case_tac as) |
|
233 apply(subgoal_tac "rsimp_ALTs( aa # as) = aa") |
|
234 prefer 2 |
|
235 apply simp |
|
236 using head_one_more_simp apply fastforce |
|
237 apply(subgoal_tac "rsimp_ALTs (aa # as) = RALTS (aa # as)") |
|
238 prefer 2 |
|
239 |
|
240 using rsimp_ALTs.simps(3) apply presburger |
|
241 |
|
242 apply(simp only:) |
|
243 apply(subgoal_tac "rsimp_ALTs (a # aa # aaa # list) = RALTS (a # aa # aaa # list)") |
|
244 prefer 2 |
|
245 using rsimp_ALTs.simps(3) apply presburger |
|
246 apply(simp only:) |
|
247 apply(subgoal_tac "rsimp_ALTs [a, rsimp (RALTS (aa # aaa # list))] = RALTS (a # [rsimp (RALTS (aa # aaa # list))])") |
|
248 prefer 2 |
|
249 |
|
250 using rsimp_ALTs.simps(3) apply presburger |
|
251 apply(simp only:) |
|
252 using simp_flatten2 |
|
253 apply(subgoal_tac " rsimp (RALT a (rsimp (RALTS (aa # aaa # list)))) = rsimp (RALT a ((RALTS (aa # aaa # list)))) ") |
|
254 prefer 2 |
|
255 |
|
256 apply (metis head_one_more_simp list.simps(9) rsimp.simps(2)) |
|
257 apply (simp only:) |
|
258 done |
|
259 |
|
260 |
|
261 lemma rsimp_alts_idem2: |
|
262 shows "rsimp (rsimp_ALTs (a # as)) = rsimp (rsimp_ALTs ((rsimp a) # [(rsimp (rsimp_ALTs as))] ))" |
|
263 using head_one_more_simp rsimp_alts_idem by auto |
|
264 |
|
265 |
|
266 lemma evolution_step1: |
|
267 shows "rsimp |
|
268 (rsimp_ALTs |
|
269 (rder x (rsimp_SEQ (rders_simp r a) (RSTAR r)) # map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) = |
|
270 rsimp |
|
271 (rsimp_ALTs |
|
272 (rder x (rsimp_SEQ (rders_simp r a) (RSTAR r)) # [(rsimp (rsimp_ALTs (map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)))])) " |
|
273 using rsimp_alts_idem by auto |
|
274 |
|
275 lemma evolution_step2: |
|
276 assumes " rsimp (rsimp_ALTs (map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) = |
|
277 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))" |
|
278 shows "rsimp |
|
279 (rsimp_ALTs |
|
280 (rder x (rsimp_SEQ (rders_simp r a) (RSTAR r)) # map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) = |
|
281 rsimp |
|
282 (rsimp_ALTs |
|
283 (rder x (rsimp_SEQ (rders_simp r a) (RSTAR r)) # [ rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))])) " |
|
284 by (simp add: assms rsimp_alts_idem) |
|
285 |
|
286 lemma rsimp_seq_aux1: |
|
287 shows "r = RONE \<and> r2 = RSTAR r0 \<Longrightarrow> rsimp_SEQ r r2 = r2" |
|
288 apply simp |
|
289 done |
|
290 |
|
291 lemma multiple_alts_simp_flatten: |
|
292 shows "rsimp (RALT (RALT r1 r2) (rsimp_ALTs rs)) = rsimp (RALTS (r1 # r2 # rs))" |
|
293 by (metis Cons_eq_appendI append_self_conv2 rsimp_ALTs.simps(2) rsimp_ALTs.simps(3) rsimp_alts_idem simp_flatten) |
|
294 |
|
295 |
|
296 lemma evo3_main_aux1: |
|
297 shows "rsimp |
|
298 (RALT (RALT (RSEQ (rsimp (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r))) |
|
299 (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))) = |
|
300 rsimp |
|
301 (RALTS |
|
302 (RSEQ (rders_simp r (a @ [x])) (RSTAR r) # |
|
303 RSEQ (rders_simp r [x]) (RSTAR r) # map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))" |
|
304 apply(subgoal_tac "rsimp |
|
305 (RALT (RALT (RSEQ (rsimp (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r))) |
|
306 (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))) = |
|
307 rsimp |
|
308 (RALT (RALT (RSEQ ( (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r))) |
|
309 (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))) ") |
|
310 prefer 2 |
|
311 apply (simp add: rsimp_idem) |
|
312 apply (simp only:) |
|
313 apply(subst multiple_alts_simp_flatten) |
|
314 by simp |
|
315 |
|
316 |
|
317 lemma evo3_main_nullable: |
|
318 shows " |
|
319 \<And>a Ss. |
|
320 \<lbrakk>rsimp (rsimp_ALTs (map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) = |
|
321 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))); |
|
322 rders_simp r a \<noteq> RONE; rders_simp r a \<noteq> RZERO; rnullable (rders_simp r a)\<rbrakk> |
|
323 \<Longrightarrow> rsimp |
|
324 (rsimp_ALTs |
|
325 [rder x (RSEQ (rders_simp r a) (RSTAR r)), |
|
326 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))]) = |
|
327 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r (a # Ss))))" |
|
328 apply(subgoal_tac "rder x (RSEQ (rders_simp r a) (RSTAR r)) |
|
329 = RALT (RSEQ (rder x (rders_simp r a)) (RSTAR r)) (RSEQ (rder x r) (RSTAR r))") |
|
330 prefer 2 |
|
331 apply simp |
|
332 apply(simp only:) |
|
333 apply(subgoal_tac "star_update x r (a # Ss) = (a @ [x]) # [x] # (star_update x r Ss)") |
|
334 prefer 2 |
|
335 using star_update_case1 apply presburger |
|
336 apply(simp only:) |
|
337 apply(subst List.list.map(2))+ |
|
338 apply(subgoal_tac "rsimp |
|
339 (rsimp_ALTs |
|
340 [RALT (RSEQ (rder x (rders_simp r a)) (RSTAR r)) (RSEQ (rder x r) (RSTAR r)), |
|
341 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))]) = |
|
342 rsimp |
|
343 (RALTS |
|
344 [RALT (RSEQ (rder x (rders_simp r a)) (RSTAR r)) (RSEQ (rder x r) (RSTAR r)), |
|
345 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))])") |
|
346 prefer 2 |
|
347 using rsimp_ALTs.simps(3) apply presburger |
|
348 apply(simp only:) |
|
349 apply(subgoal_tac " rsimp |
|
350 (rsimp_ALTs |
|
351 (rsimp_SEQ (rders_simp r (a @ [x])) (RSTAR r) # |
|
352 rsimp_SEQ (rders_simp r [x]) (RSTAR r) # map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))) |
|
353 = |
|
354 rsimp |
|
355 (RALTS |
|
356 (rsimp_SEQ (rders_simp r (a @ [x])) (RSTAR r) # |
|
357 rsimp_SEQ (rders_simp r [x]) (RSTAR r) # map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))") |
|
358 |
|
359 prefer 2 |
|
360 using rsimp_ALTs.simps(3) apply presburger |
|
361 apply (simp only:) |
|
362 apply(subgoal_tac " rsimp |
|
363 (RALT (RALT (RSEQ (rder x (rders_simp r a)) (RSTAR r)) (RSEQ ( (rder x r)) (RSTAR r))) |
|
364 (rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))))) = |
|
365 rsimp |
|
366 (RALT (RALT (RSEQ (rsimp (rder x (rders_simp r a))) (RSTAR r)) (RSEQ (rsimp (rder x r)) (RSTAR r))) |
|
367 (rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))))") |
|
368 prefer 2 |
|
369 apply (simp add: rsimp_idem) |
|
370 apply(simp only:) |
|
371 apply(subgoal_tac " rsimp |
|
372 (RALT (RALT (RSEQ (rsimp (rder x (rders_simp r a))) (RSTAR r)) (RSEQ (rsimp (rder x r)) (RSTAR r))) |
|
373 (rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))))) = |
|
374 rsimp |
|
375 (RALT (RALT (RSEQ (rsimp (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r))) |
|
376 (rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))))") |
|
377 prefer 2 |
|
378 using rders_simp_append rders_simp_one_char rsimp_idem apply presburger |
|
379 apply(simp only:) |
|
380 apply(subgoal_tac " rsimp |
|
381 (RALTS |
|
382 (rsimp_SEQ (rders_simp r (a @ [x])) (RSTAR r) # |
|
383 rsimp_SEQ (rders_simp r [x]) (RSTAR r) # map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))) = |
|
384 rsimp |
|
385 (RALTS |
|
386 (RSEQ (rders_simp r (a @ [x])) (RSTAR r) # |
|
387 RSEQ (rders_simp r [x]) (RSTAR r) # map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))") |
|
388 prefer 2 |
|
389 apply (smt (z3) idiot2 list.simps(9) rrexp.distinct(9) rsimp.simps(1) rsimp.simps(2) rsimp.simps(3) rsimp.simps(4) rsimp.simps(6) rsimp_idem) |
|
390 apply(simp only:) |
|
391 apply(subgoal_tac " rsimp |
|
392 (RALT (RALT (RSEQ (rsimp (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r))) |
|
393 (rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))))) = |
|
394 rsimp |
|
395 (RALT (RALT (RSEQ (rsimp (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r))) |
|
396 ( (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))))) ") |
|
397 prefer 2 |
|
398 using rsimp_idem apply force |
|
399 apply(simp only:) |
|
400 using evo3_main_aux1 by blast |
|
401 |
|
402 |
|
403 lemma evo3_main_not1: |
|
404 shows " \<not>rnullable (rders_simp r a) \<Longrightarrow> rder x (RSEQ (rders_simp r a) (RSTAR r)) = RSEQ (rder x (rders_simp r a)) (RSTAR r)" |
|
405 by fastforce |
|
406 |
|
407 |
|
408 lemma evo3_main_not2: |
|
409 shows "\<not>rnullable (rders_simp r a) \<Longrightarrow> rsimp |
|
410 (rsimp_ALTs |
|
411 (rder x (RSEQ (rders_simp r a) (RSTAR r)) # rs)) = rsimp |
|
412 (rsimp_ALTs |
|
413 ((RSEQ (rders_simp r (a @ [x])) (RSTAR r)) # rs))" |
|
414 by (simp add: rders_simp_append rsimp_alts_idem2 rsimp_idem) |
|
415 |
|
416 lemma evo3_main_not3: |
|
417 shows "rsimp |
|
418 (rsimp_ALTs |
|
419 (rsimp_SEQ r1 (RSTAR r) # rs)) = |
|
420 rsimp (rsimp_ALTs |
|
421 (RSEQ r1 (RSTAR r) # rs))" |
|
422 by (metis idiot2 rrexp.distinct(9) rsimp.simps(1) rsimp.simps(3) rsimp.simps(4) rsimp.simps(6) rsimp_alts_idem rsimp_alts_idem2) |
|
423 |
|
424 |
|
425 lemma evo3_main_notnullable: |
|
426 shows "\<And>a Ss. |
|
427 \<lbrakk>rsimp (rsimp_ALTs (map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) = |
|
428 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))); |
|
429 rders_simp r a \<noteq> RONE; rders_simp r a \<noteq> RZERO; \<not>rnullable (rders_simp r a)\<rbrakk> |
|
430 \<Longrightarrow> rsimp |
|
431 (rsimp_ALTs |
|
432 [rder x (RSEQ (rders_simp r a) (RSTAR r)), |
|
433 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))]) = |
|
434 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r (a # Ss))))" |
|
435 apply(subst star_update_case2) |
|
436 apply simp |
|
437 apply(subst List.list.map(2)) |
|
438 apply(subst evo3_main_not2) |
|
439 apply simp |
|
440 apply(subst evo3_main_not3) |
|
441 using rsimp_alts_idem by presburger |
|
442 |
|
443 |
|
444 lemma evo3_aux2: |
|
445 shows "rders_simp r a = RONE \<Longrightarrow> rsimp_SEQ (rders_simp (rders_simp r a) [x]) (RSTAR r) = RZERO" |
|
446 by simp |
|
447 lemma evo3_aux3: |
|
448 shows "rsimp (rsimp_ALTs (RZERO # rs)) = rsimp (rsimp_ALTs rs)" |
|
449 by (metis list.simps(8) list.simps(9) rdistinct.simps(1) rflts.simps(1) rflts.simps(2) rsimp.simps(2) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3) rsimp_alts_idem) |
|
450 |
|
451 lemma evo3_aux4: |
|
452 shows " rsimp |
|
453 (rsimp_ALTs |
|
454 [RSEQ (rder x r) (RSTAR r), |
|
455 rsimp (rsimp_ALTs rs)]) = |
|
456 rsimp |
|
457 (rsimp_ALTs |
|
458 (rsimp_SEQ (rders_simp r [x]) (RSTAR r) # rs))" |
|
459 by (metis rders_simp_one_char rsimp.simps(1) rsimp.simps(6) rsimp_alts_idem rsimp_alts_idem2) |
|
460 |
|
461 lemma evo3_aux5: |
|
462 shows "rders_simp r a \<noteq> RONE \<and> rders_simp r a \<noteq> RZERO \<Longrightarrow> rsimp_SEQ (rders_simp r a) (RSTAR r) = RSEQ (rders_simp r a) (RSTAR r)" |
|
463 using idiot2 by blast |
|
464 |
|
465 |
|
466 lemma evolution_step3: |
|
467 shows" \<And>a Ss. |
|
468 rsimp (rsimp_ALTs (map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) = |
|
469 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))) \<Longrightarrow> |
|
470 rsimp |
|
471 (rsimp_ALTs |
|
472 [rder x (rsimp_SEQ (rders_simp r a) (RSTAR r)), |
|
473 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))]) = |
|
474 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r (a # Ss))))" |
|
475 apply(case_tac "rders_simp r a = RONE") |
|
476 apply(subst rsimp_seq_aux1) |
|
477 apply simp |
|
478 apply(subst rder.simps(6)) |
|
479 apply(subgoal_tac "rnullable (rders_simp r a)") |
|
480 prefer 2 |
|
481 using rnullable.simps(2) apply presburger |
|
482 apply(subst star_update_case1) |
|
483 apply simp |
|
484 |
|
485 apply(subst List.list.map)+ |
|
486 apply(subst rders_simp_append) |
|
487 apply(subst evo3_aux2) |
|
488 apply simp |
|
489 apply(subst evo3_aux3) |
|
490 apply(subst evo3_aux4) |
|
491 apply simp |
|
492 apply(case_tac "rders_simp r a = RZERO") |
|
493 |
|
494 apply (simp add: rsimp_alts_idem2) |
|
495 apply(subgoal_tac "rders_simp r (a @ [x]) = RZERO") |
|
496 prefer 2 |
|
497 using rder.simps(1) rders_simp_append rders_simp_one_char rsimp.simps(3) apply presburger |
|
498 using rflts.simps(2) rsimp.simps(3) rsimp_SEQ.simps(1) apply presburger |
|
499 apply(subst evo3_aux5) |
|
500 apply simp |
|
501 apply(case_tac "rnullable (rders_simp r a) ") |
|
502 using evo3_main_nullable apply blast |
|
503 using evo3_main_notnullable apply blast |
|
504 done |
|
505 |
|
506 (* |
|
507 proof (prove) |
|
508 goal (1 subgoal): |
|
509 1. map f (a # s) = f a # map f s |
|
510 Auto solve_direct: the current goal can be solved directly with |
|
511 HOL.nitpick_simp(115): map ?f (?x21.0 # ?x22.0) = ?f ?x21.0 # map ?f ?x22.0 |
|
512 List.list.map(2): map ?f (?x21.0 # ?x22.0) = ?f ?x21.0 # map ?f ?x22.0 |
|
513 List.list.simps(9): map ?f (?x21.0 # ?x22.0) = ?f ?x21.0 # map ?f ?x22.0 |
|
514 *) |
|
515 lemma starseq_list_evolution: |
|
516 fixes r :: rrexp and Ss :: "char list list" and x :: char |
|
517 shows "rsimp (rsimp_ALTs (map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss) ) = |
|
518 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)) )" |
|
519 apply(induct Ss) |
|
520 apply simp |
|
521 apply(subst List.list.map(2)) |
|
522 apply(subst evolution_step2) |
|
523 apply simp |
|
524 |
|
525 |
|
526 sorry |
|
527 |
|
528 |
|
529 lemma star_seqs_produce_star_seqs: |
|
530 shows "rsimp (rsimp_ALTs (map (rder x \<circ> (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) |
|
531 = rsimp (rsimp_ALTs (map ( (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r)))) Ss))" |
|
532 by (meson comp_apply) |
|
533 |
|
534 lemma map_der_lambda_composition: |
|
535 shows "map (rder x) (map (\<lambda>s. f s) Ss) = map (\<lambda>s. (rder x (f s))) Ss" |
|
536 by force |
|
537 |
|
538 lemma ralts_vs_rsimpalts: |
|
539 shows "rsimp (RALTS rs) = rsimp (rsimp_ALTs rs)" |
|
540 by (metis evo3_aux3 rsimp_ALTs.simps(2) rsimp_ALTs.simps(3) simp_flatten2) |
|
541 |
|
542 |
|
543 lemma linearity_of_list_of_star_or_starseqs: |
|
544 fixes r::rrexp and Ss::"char list list" and x::char |
|
545 shows "\<exists>Ssa. rsimp (rder x (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss))) = |
|
546 rsimp (RALTS ( (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ssa)))" |
|
547 apply(subst rder_rsimp_ALTs_commute) |
|
548 apply(subst map_der_lambda_composition) |
|
549 using starseq_list_evolution |
|
550 apply(rule_tac x = "star_update x r Ss" in exI) |
|
551 apply(subst ralts_vs_rsimpalts) |
|
552 by simp |
|
553 |
|
554 |
|
555 |
|
556 (*certified correctness---does not depend on any previous sorry*) |
|
557 lemma star_list_push_der: shows " \<lbrakk>xs \<noteq> [] \<Longrightarrow> \<exists>Ss. rders_simp (RSTAR r) xs = rsimp (RALTS (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss)); |
|
558 xs @ [x] \<noteq> []; xs \<noteq> []\<rbrakk> \<Longrightarrow> |
|
559 \<exists>Ss. rders_simp (RSTAR r ) (xs @ [x]) = |
|
560 rsimp (RALTS (map (\<lambda>s1. (rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) ) Ss) )" |
|
561 apply(subgoal_tac "\<exists>Ss. rders_simp (RSTAR r) xs = rsimp (RALTS (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss))") |
|
562 prefer 2 |
|
563 apply blast |
|
564 apply(erule exE) |
|
565 apply(subgoal_tac "rders_simp (RSTAR r) (xs @ [x]) = rsimp (rder x (rsimp (RALTS (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss))))") |
|
566 prefer 2 |
|
567 using rders_simp_append |
|
568 using rders_simp_one_char apply presburger |
|
569 apply(rule_tac x= "Ss" in exI) |
|
570 apply(subgoal_tac " rsimp (rder x (rsimp (RALTS (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss)))) = |
|
571 rsimp (rsimp (rder x (RALTS (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss))))") |
|
572 prefer 2 |
|
573 using inside_simp_removal rsimp_idem apply presburger |
|
574 apply(subgoal_tac "rsimp (rsimp (rder x (RALTS (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss)))) = |
|
575 rsimp (rsimp (RALTS (map (rder x) (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss))))") |
|
576 prefer 2 |
|
577 using rder.simps(4) apply presburger |
|
578 apply(subgoal_tac "rsimp (rsimp (RALTS (map (rder x) (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss)))) = |
|
579 rsimp (rsimp (RALTS (map (\<lambda>s1. (rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r)))) Ss)))") |
|
580 apply (metis rsimp_idem) |
|
581 by (metis map_der_lambda_composition) |
|
582 |
194 |
583 |
195 |
584 |
196 |
585 end |
197 end |