equal
deleted
inserted
replaced
32 Sequential composition of two languages @{text "L1"} and @{text "L2"} |
32 Sequential composition of two languages @{text "L1"} and @{text "L2"} |
33 *} |
33 *} |
34 |
34 |
35 definition Seq :: "lang \<Rightarrow> lang \<Rightarrow> lang" (infixr ";;" 100) |
35 definition Seq :: "lang \<Rightarrow> lang \<Rightarrow> lang" (infixr ";;" 100) |
36 where |
36 where |
37 "L1 ;; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}" |
37 "A ;; B = {s\<^isub>1 @ s\<^isub>2 | s\<^isub>1 s\<^isub>2. s\<^isub>1 \<in> A \<and> s\<^isub>2 \<in> B}" |
38 |
38 |
39 text {* |
39 text {* |
40 Transitive closure of language @{text "L"}. |
40 Transitive closure of language @{text "L"}. |
41 *} |
41 *} |
42 |
42 |
689 shows "L (items_of rhs X) = X ;; (L (rexp_of rhs X))" |
689 shows "L (items_of rhs X) = X ;; (L (rexp_of rhs X))" |
690 proof - |
690 proof - |
691 have "finite ((snd \<circ> the_Trn) ` items_of rhs X)" using finite_items_of[OF finite] by auto |
691 have "finite ((snd \<circ> the_Trn) ` items_of rhs X)" using finite_items_of[OF finite] by auto |
692 thus ?thesis |
692 thus ?thesis |
693 apply (auto simp:rexp_of_def Seq_def items_of_def) |
693 apply (auto simp:rexp_of_def Seq_def items_of_def) |
694 apply (rule_tac x = s1 in exI, rule_tac x = s2 in exI, auto) |
694 apply (rule_tac x = "s\<^isub>1" in exI, rule_tac x = "s\<^isub>2" in exI, auto) |
695 by (rule_tac x= "Trn X r" in exI, auto simp:Seq_def) |
695 by (rule_tac x= "Trn X r" in exI, auto simp:Seq_def) |
696 qed |
696 qed |
697 |
697 |
698 lemma rexp_of_lam_eq_lam_set: |
698 lemma rexp_of_lam_eq_lam_set: |
699 assumes finite: "finite rhs" |
699 assumes finite: "finite rhs" |
705 qed |
705 qed |
706 |
706 |
707 lemma [simp]: |
707 lemma [simp]: |
708 " L (attach_rexp r xb) = L xb ;; L r" |
708 " L (attach_rexp r xb) = L xb ;; L r" |
709 apply (cases xb, auto simp:Seq_def) |
709 apply (cases xb, auto simp:Seq_def) |
710 by (rule_tac x = "s1 @ s1a" in exI, rule_tac x = s2a in exI,auto simp:Seq_def) |
710 apply(rule_tac x = "s\<^isub>1 @ s\<^isub>1'" in exI, rule_tac x = "s\<^isub>2'" in exI) |
|
711 apply(auto simp: Seq_def) |
|
712 done |
711 |
713 |
712 lemma lang_of_append_rhs: |
714 lemma lang_of_append_rhs: |
713 "L (append_rhs_rexp rhs r) = L rhs ;; L r" |
715 "L (append_rhs_rexp rhs r) = L rhs ;; L r" |
714 apply (auto simp:append_rhs_rexp_def image_def) |
716 apply (auto simp:append_rhs_rexp_def image_def) |
715 apply (auto simp:Seq_def) |
717 apply (auto simp:Seq_def) |
1209 lemma finals_in_partitions: |
1211 lemma finals_in_partitions: |
1210 "finals Lang \<subseteq> (UNIV // (\<approx>Lang))" |
1212 "finals Lang \<subseteq> (UNIV // (\<approx>Lang))" |
1211 by (auto simp:finals_def quotient_def) |
1213 by (auto simp:finals_def quotient_def) |
1212 |
1214 |
1213 theorem hard_direction: |
1215 theorem hard_direction: |
1214 assumes finite_CS: "finite (UNIV // (\<approx>Lang))" |
1216 assumes finite_CS: "finite (UNIV // \<approx>Lang)" |
1215 shows "\<exists> (reg::rexp). Lang = L reg" |
1217 shows "\<exists> (r::rexp). Lang = L r" |
1216 proof - |
1218 proof - |
1217 have "\<forall> X \<in> (UNIV // (\<approx>Lang)). \<exists> (reg::rexp). X = L reg" |
1219 have "\<forall> X \<in> (UNIV // (\<approx>Lang)). \<exists> (reg::rexp). X = L reg" |
1218 using finite_CS every_eqcl_has_reg by blast |
1220 using finite_CS every_eqcl_has_reg by blast |
1219 then obtain f |
1221 then obtain f |
1220 where f_prop: "\<forall> X \<in> (UNIV // (\<approx>Lang)). X = L ((f X)::rexp)" |
1222 where f_prop: "\<forall> X \<in> (UNIV // (\<approx>Lang)). X = L ((f X)::rexp)" |