432 repsented by @{text "Lam(EMPTY)"}, while transitions like $X_0 a$ is |
432 repsented by @{text "Lam(EMPTY)"}, while transitions like $X_0 a$ is |
433 represented by @{term "Trn X\<^isub>0 (CHAR a)"}. |
433 represented by @{term "Trn X\<^isub>0 (CHAR a)"}. |
434 *} |
434 *} |
435 |
435 |
436 text {* |
436 text {* |
437 The functions @{text "the_r"} and @{text "the_Trn"} are used to extract |
|
438 subcomponents from right hand side items. |
|
439 *} |
|
440 |
|
441 fun |
|
442 the_r :: "rhs_item \<Rightarrow> rexp" |
|
443 where |
|
444 "the_r (Lam r) = r" |
|
445 |
|
446 fun |
|
447 the_trn_rexp:: "rhs_item \<Rightarrow> rexp" |
|
448 where |
|
449 "the_trn_rexp (Trn Y r) = r" |
|
450 |
|
451 text {* |
|
452 Every right-hand side item @{text "itm"} defines a language given |
437 Every right-hand side item @{text "itm"} defines a language given |
453 by @{text "L(itm)"}, defined as: |
438 by @{text "L(itm)"}, defined as: |
454 *} |
439 *} |
455 |
440 |
456 overloading L_rhs_e \<equiv> "L:: rhs_item \<Rightarrow> lang" |
441 overloading L_rhs_e \<equiv> "L:: rhs_item \<Rightarrow> lang" |
516 The following @{text "trns_of rhs X"} returns all @{text "X"}-items in @{text "rhs"}. |
501 The following @{text "trns_of rhs X"} returns all @{text "X"}-items in @{text "rhs"}. |
517 *} |
502 *} |
518 |
503 |
519 definition |
504 definition |
520 "trns_of rhs X \<equiv> {Trn X r | r. Trn X r \<in> rhs}" |
505 "trns_of rhs X \<equiv> {Trn X r | r. Trn X r \<in> rhs}" |
521 |
|
522 text {* |
|
523 The following @{text "rexp_of rhs X"} combines all regular expressions in @{text "X"}-items |
|
524 using @{text "ALT"} to form a single regular expression. |
|
525 It will be used later to implement @{text "arden_variate"} and @{text "rhs_subst"}. |
|
526 *} |
|
527 |
|
528 definition |
|
529 "rexp_of rhs X \<equiv> \<Uplus> {r. Trn X r \<in> rhs}" |
|
530 |
|
531 text {* |
|
532 The following @{text "rexp_of_lam rhs"} combines pure regular expression items in @{text "rhs"} |
|
533 using @{text "ALT"} to form a single regular expression. |
|
534 When all variables inside @{text "rhs"} are eliminated, @{text "rexp_of_lam rhs"} |
|
535 is used to compute compute the regular expression corresponds to @{text "rhs"}. |
|
536 *} |
|
537 |
|
538 |
|
539 definition |
|
540 "rexp_of_lam rhs \<equiv> \<Uplus> {r. Lam r \<in> rhs}" |
|
541 |
506 |
542 text {* |
507 text {* |
543 The following @{text "attach_rexp rexp' itm"} attach |
508 The following @{text "attach_rexp rexp' itm"} attach |
544 the regular expression @{text "rexp'"} to |
509 the regular expression @{text "rexp'"} to |
545 the right of right hand side item @{text "itm"}. |
510 the right of right hand side item @{text "itm"}. |
724 assumes fin: "finite rhs" |
689 assumes fin: "finite rhs" |
725 shows "finite {r. Trn Y r \<in> rhs}" |
690 shows "finite {r. Trn Y r \<in> rhs}" |
726 proof - |
691 proof - |
727 have "finite {Trn Y r | Y r. Trn Y r \<in> rhs}" |
692 have "finite {Trn Y r | Y r. Trn Y r \<in> rhs}" |
728 by (rule rev_finite_subset[OF fin]) (auto) |
693 by (rule rev_finite_subset[OF fin]) (auto) |
729 then have "finite (the_trn_rexp ` {Trn Y r | Y r. Trn Y r \<in> rhs})" |
694 then have "finite ((\<lambda>(Y, r). Trn Y r) ` {(Y, r) | Y r. Trn Y r \<in> rhs})" |
730 by auto |
695 by (simp add: image_Collect) |
|
696 then have "finite {(Y, r) | Y r. Trn Y r \<in> rhs}" |
|
697 by (erule_tac finite_imageD) (simp add: inj_on_def) |
731 then show "finite {r. Trn Y r \<in> rhs}" |
698 then show "finite {r. Trn Y r \<in> rhs}" |
732 apply(erule_tac rev_finite_subset) |
699 by (erule_tac f="snd" in finite_surj) (auto simp add: image_def) |
733 apply(auto simp add: image_def) |
|
734 apply(rule_tac x="Trn Y x" in exI) |
|
735 apply(auto) |
|
736 done |
|
737 qed |
700 qed |
738 |
701 |
739 lemma finite_Lam: |
702 lemma finite_Lam: |
740 assumes fin:"finite rhs" |
703 assumes fin:"finite rhs" |
741 shows "finite {r. Lam r \<in> rhs}" |
704 shows "finite {r. Lam r \<in> rhs}" |
742 proof - |
705 proof - |
743 have "finite {Lam r | r. Lam r \<in> rhs}" |
706 have "finite {Lam r | r. Lam r \<in> rhs}" |
744 by (rule rev_finite_subset[OF fin]) (auto) |
707 by (rule rev_finite_subset[OF fin]) (auto) |
745 then have "finite (the_r ` {Lam r | r. Lam r \<in> rhs})" |
|
746 by auto |
|
747 then show "finite {r. Lam r \<in> rhs}" |
708 then show "finite {r. Lam r \<in> rhs}" |
748 apply(erule_tac rev_finite_subset) |
709 apply(simp add: image_Collect[symmetric]) |
749 apply(auto simp add: image_def) |
710 apply(erule finite_imageD) |
|
711 apply(auto simp add: inj_on_def) |
750 done |
712 done |
751 qed |
713 qed |
752 |
714 |
753 lemma rexp_of_empty: |
715 lemma rexp_of_empty: |
754 assumes finite:"finite rhs" |
716 assumes finite:"finite rhs" |
929 assumes l_eq_r: "X = L rhs" |
891 assumes l_eq_r: "X = L rhs" |
930 and not_empty: "[] \<notin> L (\<Uplus>{r. Trn X r \<in> rhs})" |
892 and not_empty: "[] \<notin> L (\<Uplus>{r. Trn X r \<in> rhs})" |
931 and finite: "finite rhs" |
893 and finite: "finite rhs" |
932 shows "X = L (arden_variate X rhs)" |
894 shows "X = L (arden_variate X rhs)" |
933 proof - |
895 proof - |
934 thm rexp_of_def |
|
935 def A \<equiv> "L (\<Uplus>{r. Trn X r \<in> rhs})" |
896 def A \<equiv> "L (\<Uplus>{r. Trn X r \<in> rhs})" |
936 def b \<equiv> "rhs - trns_of rhs X" |
897 def b \<equiv> "rhs - trns_of rhs X" |
937 def B \<equiv> "L b" |
898 def B \<equiv> "L b" |
938 have "X = B ;; A\<star>" |
899 have "X = B ;; A\<star>" |
939 proof- |
900 proof- |
1242 assumes ES_single: "ES = {(X, xrhs)}" |
1203 assumes ES_single: "ES = {(X, xrhs)}" |
1243 and Inv_ES: "Inv ES" |
1204 and Inv_ES: "Inv ES" |
1244 shows "\<exists> (r::rexp). L r = X" (is "\<exists> r. ?P r") |
1205 shows "\<exists> (r::rexp). L r = X" (is "\<exists> r. ?P r") |
1245 proof- |
1206 proof- |
1246 def A \<equiv> "arden_variate X xrhs" |
1207 def A \<equiv> "arden_variate X xrhs" |
1247 have "?P (rexp_of_lam A)" |
1208 have "?P (\<Uplus>{r. Lam r \<in> A})" |
1248 proof - |
1209 proof - |
1249 have "L (\<Uplus>{r. Lam r \<in> A}) = L ({Lam r | r. Lam r \<in> A})" |
1210 have "L (\<Uplus>{r. Lam r \<in> A}) = L ({Lam r | r. Lam r \<in> A})" |
1250 proof(rule rexp_of_lam_eq_lam_set) |
1211 proof(rule rexp_of_lam_eq_lam_set) |
1251 show "finite A" |
1212 show "finite A" |
1252 unfolding A_def |
1213 unfolding A_def |
1278 by(simp add:Inv_def ardenable_def rexp_of_empty finite_rhs_def) |
1239 by(simp add:Inv_def ardenable_def rexp_of_empty finite_rhs_def) |
1279 next |
1240 next |
1280 from Inv_ES ES_single show "finite xrhs" |
1241 from Inv_ES ES_single show "finite xrhs" |
1281 by (simp add:Inv_def finite_rhs_def) |
1242 by (simp add:Inv_def finite_rhs_def) |
1282 qed |
1243 qed |
1283 finally show ?thesis unfolding rexp_of_lam_def by simp |
1244 finally show ?thesis by simp |
1284 qed |
1245 qed |
1285 thus ?thesis by auto |
1246 thus ?thesis by auto |
1286 qed |
1247 qed |
1287 |
1248 |
1288 lemma every_eqcl_has_reg: |
1249 lemma every_eqcl_has_reg: |