equal
deleted
inserted
replaced
1 theory Myhill_1 |
1 theory Myhill_1 |
2 imports Main List_Prefix Prefix_subtract |
2 imports Main List_Prefix Prefix_subtract Prelude |
3 begin |
3 begin |
4 |
4 |
5 (* |
5 (* |
6 text {* |
6 text {* |
7 \begin{figure} |
7 \begin{figure} |
24 *) |
24 *) |
25 |
25 |
26 |
26 |
27 section {* Preliminary definitions *} |
27 section {* Preliminary definitions *} |
28 |
28 |
29 text {* Sequential composition of two languages @{text "L1"} and @{text "L2"} *} |
29 types lang = "string set" |
|
30 |
|
31 text {* |
|
32 Sequential composition of two languages @{text "L1"} and @{text "L2"} |
|
33 *} |
|
34 |
30 definition Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100) |
35 definition Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100) |
31 where |
36 where |
32 "L1 ;; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}" |
37 "L1 ;; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}" |
33 |
38 |
34 text {* Transitive closure of language @{text "L"}. *} |
39 text {* Transitive closure of language @{text "L"}. *} |
35 inductive_set |
40 inductive_set |
36 Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102) |
41 Star :: "lang \<Rightarrow> lang" ("_\<star>" [101] 102) |
37 for L :: "string set" |
42 for L |
38 where |
43 where |
39 start[intro]: "[] \<in> L\<star>" |
44 start[intro]: "[] \<in> L\<star>" |
40 | step[intro]: "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1@s2 \<in> L\<star>" |
45 | step[intro]: "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1@s2 \<in> L\<star>" |
41 |
46 |
42 text {* Some properties of operator @{text ";;"}.*} |
47 text {* Some properties of operator @{text ";;"}.*} |
191 The following lemma assures that the arbitrary choice made by the @{text "SOME"} in @{text "folds"} |
196 The following lemma assures that the arbitrary choice made by the @{text "SOME"} in @{text "folds"} |
192 does not affect the @{text "L"}-value of the resultant regular expression. |
197 does not affect the @{text "L"}-value of the resultant regular expression. |
193 *} |
198 *} |
194 lemma folds_alt_simp [simp]: |
199 lemma folds_alt_simp [simp]: |
195 "finite rs \<Longrightarrow> L (folds ALT NULL rs) = \<Union> (L ` rs)" |
200 "finite rs \<Longrightarrow> L (folds ALT NULL rs) = \<Union> (L ` rs)" |
196 apply (rule set_ext, simp add:folds_def) |
201 apply (rule set_eq_intro, simp add:folds_def) |
197 apply (rule someI2_ex, erule finite_imp_fold_graph) |
202 apply (rule someI2_ex, erule finite_imp_fold_graph) |
198 by (erule fold_graph.induct, auto) |
203 by (erule fold_graph.induct, auto) |
199 |
204 |
200 (* Just a technical lemma. *) |
205 (* Just a technical lemma. *) |
201 lemma [simp]: |
206 lemma [simp]: |
204 |
209 |
205 text {* |
210 text {* |
206 @{text "\<approx>L"} is an equivalent class defined by language @{text "Lang"}. |
211 @{text "\<approx>L"} is an equivalent class defined by language @{text "Lang"}. |
207 *} |
212 *} |
208 definition |
213 definition |
209 str_eq_rel ("\<approx>_") |
214 str_eq_rel ("\<approx>_" [100] 100) |
210 where |
215 where |
211 "\<approx>Lang \<equiv> {(x, y). (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)}" |
216 "\<approx>Lang \<equiv> {(x, y). (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)}" |
212 |
217 |
213 text {* |
218 text {* |
214 Among equivlant clases of @{text "\<approx>Lang"}, the set @{text "finals(Lang)"} singles out |
219 Among equivlant clases of @{text "\<approx>Lang"}, the set @{text "finals(Lang)"} singles out |