9 shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y" |
9 shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y" |
10 by simp |
10 by simp |
11 |
11 |
12 text {* Myhill-Nerode relation *} |
12 text {* Myhill-Nerode relation *} |
13 |
13 |
|
14 |
14 definition |
15 definition |
15 str_eq_rel :: "'a lang \<Rightarrow> ('a list \<times> 'a list) set" ("\<approx>_" [100] 100) |
16 str_eq :: "'a lang \<Rightarrow> ('a list \<times> 'a list) set" ("\<approx>_" [100] 100) |
16 where |
17 where |
17 "\<approx>A \<equiv> {(x, y). (\<forall>z. x @ z \<in> A \<longleftrightarrow> y @ z \<in> A)}" |
18 "\<approx>A \<equiv> {(x, y). (\<forall>z. x @ z \<in> A \<longleftrightarrow> y @ z \<in> A)}" |
|
19 |
|
20 abbreviation |
|
21 str_eq_applied :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<approx>_ _") |
|
22 where |
|
23 "x \<approx>A y \<equiv> (x, y) \<in> \<approx>A" |
18 |
24 |
19 definition |
25 definition |
20 finals :: "'a lang \<Rightarrow> 'a lang set" |
26 finals :: "'a lang \<Rightarrow> 'a lang set" |
21 where |
27 where |
22 "finals A \<equiv> {\<approx>A `` {s} | s . s \<in> A}" |
28 "finals A \<equiv> {\<approx>A `` {s} | s . s \<in> A}" |
23 |
29 |
24 lemma lang_is_union_of_finals: |
30 lemma lang_is_union_of_finals: |
25 shows "A = \<Union> finals A" |
31 shows "A = \<Union> finals A" |
26 unfolding finals_def |
32 unfolding finals_def |
27 unfolding Image_def |
33 unfolding Image_def |
28 unfolding str_eq_rel_def |
34 unfolding str_eq_def |
29 by (auto) (metis append_Nil2) |
35 by (auto) (metis append_Nil2) |
30 |
36 |
31 lemma finals_in_partitions: |
37 lemma finals_in_partitions: |
32 shows "finals A \<subseteq> (UNIV // \<approx>A)" |
38 shows "finals A \<subseteq> (UNIV // \<approx>A)" |
33 unfolding finals_def quotient_def |
39 unfolding finals_def quotient_def |
245 |
251 |
246 lemma defined_by_str: |
252 lemma defined_by_str: |
247 assumes "s \<in> X" "X \<in> UNIV // \<approx>A" |
253 assumes "s \<in> X" "X \<in> UNIV // \<approx>A" |
248 shows "X = \<approx>A `` {s}" |
254 shows "X = \<approx>A `` {s}" |
249 using assms |
255 using assms |
250 unfolding quotient_def Image_def str_eq_rel_def |
256 unfolding quotient_def Image_def str_eq_def |
251 by auto |
257 by auto |
252 |
258 |
253 lemma every_eqclass_has_transition: |
259 lemma every_eqclass_has_transition: |
254 assumes has_str: "s @ [c] \<in> X" |
260 assumes has_str: "s @ [c] \<in> X" |
255 and in_CS: "X \<in> UNIV // \<approx>A" |
261 and in_CS: "X \<in> UNIV // \<approx>A" |
261 moreover |
267 moreover |
262 have "X = \<approx>A `` {s @ [c]}" |
268 have "X = \<approx>A `` {s @ [c]}" |
263 using has_str in_CS defined_by_str by blast |
269 using has_str in_CS defined_by_str by blast |
264 then have "Y \<cdot> {[c]} \<subseteq> X" |
270 then have "Y \<cdot> {[c]} \<subseteq> X" |
265 unfolding Y_def Image_def conc_def |
271 unfolding Y_def Image_def conc_def |
266 unfolding str_eq_rel_def |
272 unfolding str_eq_def |
267 by clarsimp |
273 by clarsimp |
268 moreover |
274 moreover |
269 have "s \<in> Y" unfolding Y_def |
275 have "s \<in> Y" unfolding Y_def |
270 unfolding Image_def str_eq_rel_def by simp |
276 unfolding Image_def str_eq_def by simp |
271 ultimately show thesis using that by blast |
277 ultimately show thesis using that by blast |
272 qed |
278 qed |
273 |
279 |
274 lemma l_eq_r_in_eqs: |
280 lemma l_eq_r_in_eqs: |
275 assumes X_in_eqs: "(X, rhs) \<in> Init (UNIV // \<approx>A)" |
281 assumes X_in_eqs: "(X, rhs) \<in> Init (UNIV // \<approx>A)" |