50 shows "Der c (A \<union> B) = Der c A \<union> Der c B" |
50 shows "Der c (A \<union> B) = Der c A \<union> Der c B" |
51 unfolding Der_def |
51 unfolding Der_def |
52 by auto |
52 by auto |
53 |
53 |
54 lemma Der_seq [simp]: |
54 lemma Der_seq [simp]: |
55 shows "Der c (A ;; B) = (Der c A) ;; B \<union> (Delta A ;; Der c B)" |
55 shows "Der c (A \<cdot> B) = (Der c A) \<cdot> B \<union> (Delta A \<cdot> Der c B)" |
56 unfolding Der_def Delta_def |
56 unfolding Der_def Delta_def |
57 unfolding Seq_def |
57 unfolding Seq_def |
58 by (auto simp add: Cons_eq_append_conv) |
58 by (auto simp add: Cons_eq_append_conv) |
59 |
59 |
60 lemma Der_star [simp]: |
60 lemma Der_star [simp]: |
61 shows "Der c (A\<star>) = (Der c A) ;; A\<star>" |
61 shows "Der c (A\<star>) = (Der c A) \<cdot> A\<star>" |
62 proof - |
62 proof - |
63 have incl: "Delta A ;; Der c (A\<star>) \<subseteq> (Der c A) ;; A\<star>" |
63 have incl: "Delta A \<cdot> Der c (A\<star>) \<subseteq> (Der c A) \<cdot> A\<star>" |
64 unfolding Der_def Delta_def Seq_def |
64 unfolding Der_def Delta_def Seq_def |
65 apply(auto) |
65 apply(auto) |
66 apply(drule star_decom) |
66 apply(drule star_decom) |
67 apply(auto simp add: Cons_eq_append_conv) |
67 apply(auto simp add: Cons_eq_append_conv) |
68 done |
68 done |
69 |
69 |
70 have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)" |
70 have "Der c (A\<star>) = Der c ({[]} \<union> A \<cdot> A\<star>)" |
71 by (simp only: star_cases[symmetric]) |
71 by (simp only: star_cases[symmetric]) |
72 also have "... = Der c (A ;; A\<star>)" |
72 also have "... = Der c (A \<cdot> A\<star>)" |
73 by (simp only: Der_union Der_empty) (simp) |
73 by (simp only: Der_union Der_empty) (simp) |
74 also have "... = (Der c A) ;; A\<star> \<union> (Delta A ;; Der c (A\<star>))" |
74 also have "... = (Der c A) \<cdot> A\<star> \<union> (Delta A \<cdot> Der c (A\<star>))" |
75 by simp |
75 by simp |
76 also have "... = (Der c A) ;; A\<star>" |
76 also have "... = (Der c A) \<cdot> A\<star>" |
77 using incl by auto |
77 using incl by auto |
78 finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" . |
78 finally show "Der c (A\<star>) = (Der c A) \<cdot> A\<star>" . |
79 qed |
79 qed |
80 |
80 |
81 |
81 |
82 lemma Ders_singleton: |
82 lemma Ders_singleton: |
83 shows "Ders [c] A = Der c A" |
83 shows "Ders [c] A = Der c A" |
124 |
124 |
125 termination |
125 termination |
126 by (relation "measure (length o fst)") (auto) |
126 by (relation "measure (length o fst)") (auto) |
127 |
127 |
128 lemma Delta_nullable: |
128 lemma Delta_nullable: |
129 shows "Delta (L r) = (if nullable r then {[]} else {})" |
129 shows "Delta (L_rexp r) = (if nullable r then {[]} else {})" |
130 unfolding Delta_def |
130 unfolding Delta_def |
131 by (induct r) (auto simp add: Seq_def split: if_splits) |
131 by (induct r) (auto simp add: Seq_def split: if_splits) |
132 |
132 |
133 lemma Der_der: |
133 lemma Der_der: |
134 fixes r::rexp |
134 fixes r::rexp |
135 shows "Der c (L r) = L (der c r)" |
135 shows "Der c (L_rexp r) = L_rexp (der c r)" |
136 by (induct r) (simp_all add: Delta_nullable) |
136 by (induct r) (simp_all add: Delta_nullable) |
137 |
137 |
138 lemma Ders_ders: |
138 lemma Ders_ders: |
139 fixes r::rexp |
139 fixes r::rexp |
140 shows "Ders s (L r) = L (ders s r)" |
140 shows "Ders s (L_rexp r) = L_rexp (ders s r)" |
141 apply(induct s rule: rev_induct) |
141 apply(induct s rule: rev_induct) |
142 apply(simp add: Ders_def) |
142 apply(simp add: Ders_def) |
143 apply(simp only: ders.simps) |
143 apply(simp only: ders.simps) |
144 apply(simp only: Ders_append) |
144 apply(simp only: Ders_append) |
145 apply(simp only: Ders_singleton) |
145 apply(simp only: Ders_singleton) |
193 apply(simp only: pders.simps) |
193 apply(simp only: pders.simps) |
194 apply(simp) |
194 apply(simp) |
195 done |
195 done |
196 |
196 |
197 lemma pder_set_lang: |
197 lemma pder_set_lang: |
198 shows "(\<Union> (L ` pder_set c R)) = (\<Union>r \<in> R. (\<Union>L ` (pder c r)))" |
198 shows "(\<Union> (L_rexp ` pder_set c R)) = (\<Union>r \<in> R. (\<Union>L_rexp ` (pder c r)))" |
199 unfolding image_def |
199 unfolding image_def |
200 by auto |
200 by auto |
201 |
201 |
202 lemma |
202 lemma |
203 shows seq_UNION_left: "B ;; (\<Union>n\<in>C. A n) = (\<Union>n\<in>C. B ;; A n)" |
203 shows seq_UNION_left: "B \<cdot> (\<Union>n\<in>C. A n) = (\<Union>n\<in>C. B \<cdot> A n)" |
204 and seq_UNION_right: "(\<Union>n\<in>C. A n) ;; B = (\<Union>n\<in>C. A n ;; B)" |
204 and seq_UNION_right: "(\<Union>n\<in>C. A n) \<cdot> B = (\<Union>n\<in>C. A n \<cdot> B)" |
205 unfolding Seq_def by auto |
205 unfolding Seq_def by auto |
206 |
206 |
207 lemma Der_pder: |
207 lemma Der_pder: |
208 fixes r::rexp |
208 fixes r::rexp |
209 shows "Der c (L r) = \<Union> L ` (pder c r)" |
209 shows "Der c (L_rexp r) = \<Union> L_rexp ` (pder c r)" |
210 by (induct r) (auto simp add: Delta_nullable seq_UNION_right) |
210 by (induct r) (auto simp add: Delta_nullable seq_UNION_right) |
211 |
211 |
212 lemma Ders_pders: |
212 lemma Ders_pders: |
213 fixes r::rexp |
213 fixes r::rexp |
214 shows "Ders s (L r) = \<Union> L ` (pders s r)" |
214 shows "Ders s (L_rexp r) = \<Union> L_rexp ` (pders s r)" |
215 proof (induct s rule: rev_induct) |
215 proof (induct s rule: rev_induct) |
216 case (snoc c s) |
216 case (snoc c s) |
217 have ih: "Ders s (L r) = \<Union> L ` (pders s r)" by fact |
217 have ih: "Ders s (L_rexp r) = \<Union> L_rexp ` (pders s r)" by fact |
218 have "Ders (s @ [c]) (L r) = Ders [c] (Ders s (L r))" |
218 have "Ders (s @ [c]) (L_rexp r) = Ders [c] (Ders s (L_rexp r))" |
219 by (simp add: Ders_append) |
219 by (simp add: Ders_append) |
220 also have "\<dots> = Der c (\<Union> L ` (pders s r))" using ih |
220 also have "\<dots> = Der c (\<Union> L_rexp ` (pders s r))" using ih |
221 by (simp add: Ders_singleton) |
221 by (simp add: Ders_singleton) |
222 also have "\<dots> = (\<Union>r\<in>pders s r. Der c (L r))" |
222 also have "\<dots> = (\<Union>r\<in>pders s r. Der c (L_rexp r))" |
223 unfolding Der_def image_def by auto |
223 unfolding Der_def image_def by auto |
224 also have "\<dots> = (\<Union>r\<in>pders s r. (\<Union> L ` (pder c r)))" |
224 also have "\<dots> = (\<Union>r\<in>pders s r. (\<Union> L_rexp ` (pder c r)))" |
225 by (simp add: Der_pder) |
225 by (simp add: Der_pder) |
226 also have "\<dots> = (\<Union>L ` (pder_set c (pders s r)))" |
226 also have "\<dots> = (\<Union>L_rexp ` (pder_set c (pders s r)))" |
227 by (simp add: pder_set_lang) |
227 by (simp add: pder_set_lang) |
228 also have "\<dots> = (\<Union>L ` (pders (s @ [c]) r))" |
228 also have "\<dots> = (\<Union>L_rexp ` (pders (s @ [c]) r))" |
229 by simp |
229 by simp |
230 finally show "Ders (s @ [c]) (L r) = \<Union>L ` pders (s @ [c]) r" . |
230 finally show "Ders (s @ [c]) (L_rexp r) = \<Union> L_rexp ` pders (s @ [c]) r" . |
231 qed (simp add: Ders_def) |
231 qed (simp add: Ders_def) |
232 |
232 |
233 lemma Ders_set_pders_set: |
233 lemma Ders_set_pders_set: |
234 fixes r::rexp |
234 fixes r::rexp |
235 shows "Ders_set A (L r) = (\<Union> L ` (pders_set A r))" |
235 shows "Ders_set A (L_rexp r) = (\<Union> L_rexp ` (pders_set A r))" |
236 by (simp add: Ders_set_Ders Ders_pders) |
236 by (simp add: Ders_set_Ders Ders_pders) |
237 |
237 |
238 lemma pders_NULL [simp]: |
238 lemma pders_NULL [simp]: |
239 shows "pders s NULL = {NULL}" |
239 shows "pders s NULL = {NULL}" |
240 by (induct s rule: rev_induct) (simp_all) |
240 by (induct s rule: rev_induct) (simp_all) |
253 |
253 |
254 definition |
254 definition |
255 "Suf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}" |
255 "Suf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}" |
256 |
256 |
257 lemma Suf: |
257 lemma Suf: |
258 shows "Suf (s @ [c]) = (Suf s) ;; {[c]} \<union> {[c]}" |
258 shows "Suf (s @ [c]) = (Suf s) \<cdot> {[c]} \<union> {[c]}" |
259 unfolding Suf_def Seq_def |
259 unfolding Suf_def Seq_def |
260 by (auto simp add: append_eq_append_conv2 append_eq_Cons_conv) |
260 by (auto simp add: append_eq_append_conv2 append_eq_Cons_conv) |
261 |
261 |
262 lemma Suf_Union: |
262 lemma Suf_Union: |
263 shows "(\<Union>v \<in> Suf s ;; {[c]}. P v) = (\<Union>v \<in> Suf s. P (v @ [c]))" |
263 shows "(\<Union>v \<in> Suf s \<cdot> {[c]}. P v) = (\<Union>v \<in> Suf s. P (v @ [c]))" |
264 by (auto simp add: Seq_def) |
264 by (auto simp add: Seq_def) |
265 |
265 |
266 lemma inclusion1: |
266 lemma inclusion1: |
267 shows "pder_set c (SEQS R r2) \<subseteq> SEQS (pder_set c R) r2 \<union> (pder c r2)" |
267 shows "pder_set c (SEQS R r2) \<subseteq> SEQS (pder_set c R) r2 \<union> (pder c r2)" |
268 apply(auto simp add: if_splits) |
268 apply(auto simp add: if_splits) |
275 case (snoc c s) |
275 case (snoc c s) |
276 have ih: "pders s (SEQ r1 r2) \<subseteq> SEQS (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2)" |
276 have ih: "pders s (SEQ r1 r2) \<subseteq> SEQS (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2)" |
277 by fact |
277 by fact |
278 have "pders (s @ [c]) (SEQ r1 r2) = pder_set c (pders s (SEQ r1 r2))" by simp |
278 have "pders (s @ [c]) (SEQ r1 r2) = pder_set c (pders s (SEQ r1 r2))" by simp |
279 also have "\<dots> \<subseteq> pder_set c (SEQS (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2))" |
279 also have "\<dots> \<subseteq> pder_set c (SEQS (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2))" |
280 using ih by auto |
280 using ih by (auto) (blast) |
281 also have "\<dots> = pder_set c (SEQS (pders s r1) r2) \<union> pder_set c (\<Union>v \<in> Suf s. pders v r2)" |
281 also have "\<dots> = pder_set c (SEQS (pders s r1) r2) \<union> pder_set c (\<Union>v \<in> Suf s. pders v r2)" |
282 by (simp) |
282 by (simp) |
283 also have "\<dots> = pder_set c (SEQS (pders s r1) r2) \<union> (\<Union>v \<in> Suf s. pder_set c (pders v r2))" |
283 also have "\<dots> = pder_set c (SEQS (pders s r1) r2) \<union> (\<Union>v \<in> Suf s. pder_set c (pders v r2))" |
284 by (simp) |
284 by (simp) |
285 also have "\<dots> \<subseteq> pder_set c (SEQS (pders s r1) r2) \<union> (pder c r2) \<union> (\<Union>v \<in> Suf s. pders (v @ [c]) r2)" |
285 also have "\<dots> \<subseteq> pder_set c (SEQS (pders s r1) r2) \<union> (pder c r2) \<union> (\<Union>v \<in> Suf s. pders (v @ [c]) r2)" |
307 also have "\<dots> \<subseteq> (pder_set c (\<Union>v\<in>Suf s. SEQS (pders v r) (STAR r)))" |
307 also have "\<dots> \<subseteq> (pder_set c (\<Union>v\<in>Suf s. SEQS (pders v r) (STAR r)))" |
308 using ih[OF asm] by blast |
308 using ih[OF asm] by blast |
309 also have "\<dots> = (\<Union>v\<in>Suf s. pder_set c (SEQS (pders v r) (STAR r)))" |
309 also have "\<dots> = (\<Union>v\<in>Suf s. pder_set c (SEQS (pders v r) (STAR r)))" |
310 by simp |
310 by simp |
311 also have "\<dots> \<subseteq> (\<Union>v\<in>Suf s. (SEQS (pder_set c (pders v r)) (STAR r) \<union> pder c (STAR r)))" |
311 also have "\<dots> \<subseteq> (\<Union>v\<in>Suf s. (SEQS (pder_set c (pders v r)) (STAR r) \<union> pder c (STAR r)))" |
312 using inclusion1 by blast |
312 using inclusion1 by (auto split: if_splits) |
313 also have "\<dots> = (\<Union>v\<in>Suf s. (SEQS (pder_set c (pders v r)) (STAR r))) \<union> pder c (STAR r)" |
313 also have "\<dots> = (\<Union>v\<in>Suf s. (SEQS (pder_set c (pders v r)) (STAR r))) \<union> pder c (STAR r)" |
314 using asm by (auto simp add: Suf_def) |
314 using asm by (auto simp add: Suf_def) |
315 also have "\<dots> = (\<Union>v\<in>Suf s. (SEQS (pders (v @ [c]) r) (STAR r))) \<union> (SEQS (pder c r) (STAR r))" |
315 also have "\<dots> = (\<Union>v\<in>Suf s. (SEQS (pders (v @ [c]) r) (STAR r))) \<union> (SEQS (pder c r) (STAR r))" |
316 by simp |
316 by simp |
317 also have "\<dots> = (\<Union>v\<in>Suf (s @ [c]). (SEQS (pders v r) (STAR r)))" |
317 also have "\<dots> = (\<Union>v\<in>Suf (s @ [c]). (SEQS (pders v r) (STAR r)))" |
442 qed |
442 qed |
443 |
443 |
444 |
444 |
445 lemma Myhill_Nerode3: |
445 lemma Myhill_Nerode3: |
446 fixes r::"rexp" |
446 fixes r::"rexp" |
447 shows "finite (UNIV // \<approx>(L r))" |
447 shows "finite (UNIV // \<approx>(L_rexp r))" |
448 proof - |
448 proof - |
449 have "finite (UNIV // =(\<lambda>x. pders x r)=)" |
449 have "finite (UNIV // =(\<lambda>x. pders x r)=)" |
450 proof - |
450 proof - |
451 have "range (\<lambda>x. pders x r) \<subseteq> {pders s r | s. s \<in> UNIV}" by auto |
451 have "range (\<lambda>x. pders x r) = {pders s r | s. s \<in> UNIV}" by auto |
452 moreover |
452 moreover |
453 have "finite {pders s r | s. s \<in> UNIV}" by (rule finite_pders2) |
453 have "finite {pders s r | s. s \<in> UNIV}" by (rule finite_pders2) |
454 ultimately |
454 ultimately |
455 have "finite (range (\<lambda>x. pders x r))" |
455 have "finite (range (\<lambda>x. pders x r))" |
456 by (rule finite_subset) |
456 by simp |
457 then show "finite (UNIV // =(\<lambda>x. pders x r)=)" |
457 then show "finite (UNIV // =(\<lambda>x. pders x r)=)" |
458 by (rule finite_eq_tag_rel) |
458 by (rule finite_eq_tag_rel) |
459 qed |
459 qed |
460 moreover |
460 moreover |
461 have " =(\<lambda>x. pders x r)= \<subseteq> \<approx>(L r)" |
461 have "=(\<lambda>x. pders x r)= \<subseteq> \<approx>(L_rexp r)" |
462 unfolding tag_eq_rel_def |
462 unfolding tag_eq_rel_def |
463 by (auto simp add: str_eq_def[symmetric] MN_Rel_Ders Ders_pders) |
463 unfolding str_eq_def2 |
|
464 unfolding MN_Rel_Ders |
|
465 unfolding Ders_pders |
|
466 by auto |
464 moreover |
467 moreover |
465 have "equiv UNIV =(\<lambda>x. pders x r)=" |
468 have "equiv UNIV =(\<lambda>x. pders x r)=" |
466 unfolding equiv_def refl_on_def sym_def trans_def |
469 unfolding equiv_def refl_on_def sym_def trans_def |
467 unfolding tag_eq_rel_def |
470 unfolding tag_eq_rel_def |
468 by auto |
471 by auto |
469 moreover |
472 moreover |
470 have "equiv UNIV (\<approx>(L r))" |
473 have "equiv UNIV (\<approx>(L_rexp r))" |
471 unfolding equiv_def refl_on_def sym_def trans_def |
474 unfolding equiv_def refl_on_def sym_def trans_def |
472 unfolding str_eq_rel_def |
475 unfolding str_eq_rel_def |
473 by auto |
476 by auto |
474 ultimately show "finite (UNIV // \<approx>(L r))" |
477 ultimately show "finite (UNIV // \<approx>(L_rexp r))" |
475 by (rule refined_partition_finite) |
478 by (rule refined_partition_finite) |
476 qed |
479 qed |
477 |
480 |
478 |
481 |
479 section {* Closure under Left-Quotients *} |
482 section {* Relating derivatives and partial derivatives *} |
480 |
|
481 lemma closure_left_quotient: |
|
482 assumes "regular A" |
|
483 shows "regular (Ders_set B A)" |
|
484 proof - |
|
485 from assms obtain r::rexp where eq: "L r = A" by auto |
|
486 have fin: "finite (pders_set B r)" by (rule finite_pders_set) |
|
487 |
|
488 have "Ders_set B (L r) = (\<Union> L ` (pders_set B r))" |
|
489 by (simp add: Ders_set_pders_set) |
|
490 also have "\<dots> = L (\<Uplus>(pders_set B r))" using fin by simp |
|
491 finally have "Ders_set B A = L (\<Uplus>(pders_set B r))" using eq |
|
492 by simp |
|
493 then show "regular (Ders_set B A)" by auto |
|
494 qed |
|
495 |
|
496 |
|
497 section {* Relating standard and partial derivations *} |
|
498 |
483 |
499 lemma |
484 lemma |
500 shows "(\<Union> L ` (pder c r)) = L (der c r)" |
485 shows "(\<Union> L_rexp ` (pder c r)) = L_rexp (der c r)" |
501 unfolding Der_der[symmetric] Der_pder by simp |
486 unfolding Der_der[symmetric] Der_pder by simp |
502 |
487 |
503 lemma |
488 lemma |
504 shows "(\<Union> L ` (pders s r)) = L (ders s r)" |
489 shows "(\<Union> L_rexp ` (pders s r)) = L_rexp (ders s r)" |
505 unfolding Ders_ders[symmetric] Ders_pders by simp |
490 unfolding Ders_ders[symmetric] Ders_pders by simp |
506 |
491 |
507 |
|
508 |
|
509 fun |
|
510 width :: "rexp \<Rightarrow> nat" |
|
511 where |
|
512 "width (NULL) = 0" |
|
513 | "width (EMPTY) = 0" |
|
514 | "width (CHAR c) = 1" |
|
515 | "width (ALT r1 r2) = width r1 + width r2" |
|
516 | "width (SEQ r1 r2) = width r1 + width r2" |
|
517 | "width (STAR r) = width r" |
|
518 |
|
519 |
|
520 |
|
521 end |
492 end |