1 (* Author: Christian Urban, Xingyuan Zhang, Chunhan Wu *) |
1 (* Author: Christian Urban, Xingyuan Zhang, Chunhan Wu *) |
2 theory Closures |
2 theory Closures |
3 imports Derivatives "~~/src/HOL/Library/Infinite_Set" |
3 imports Myhill "~~/src/HOL/Library/Infinite_Set" |
4 begin |
4 begin |
5 |
5 |
6 section {* Closure properties of regular languages *} |
6 section {* Closure properties of regular languages *} |
7 |
7 |
8 abbreviation |
8 abbreviation |
9 regular :: "'a lang \<Rightarrow> bool" |
9 regular :: "'a lang \<Rightarrow> bool" |
10 where |
10 where |
11 "regular A \<equiv> \<exists>r. A = lang r" |
11 "regular A \<equiv> \<exists>r. A = lang r" |
12 |
12 |
13 subsection {* Closure under set operations *} |
13 subsection {* Closure under @{text "\<union>"}, @{text "\<cdot>"} and @{text "\<star>"} *} |
14 |
14 |
15 lemma closure_union [intro]: |
15 lemma closure_union [intro]: |
16 assumes "regular A" "regular B" |
16 assumes "regular A" "regular B" |
17 shows "regular (A \<union> B)" |
17 shows "regular (A \<union> B)" |
18 proof - |
18 proof - |
37 from assms obtain r::"'a rexp" where "lang r = A" by auto |
37 from assms obtain r::"'a rexp" where "lang r = A" by auto |
38 then have "A\<star> = lang (Star r)" by simp |
38 then have "A\<star> = lang (Star r)" by simp |
39 then show "regular (A\<star>)" by blast |
39 then show "regular (A\<star>)" by blast |
40 qed |
40 qed |
41 |
41 |
|
42 subsection {* Closure under complementation *} |
|
43 |
42 text {* Closure under complementation is proved via the |
44 text {* Closure under complementation is proved via the |
43 Myhill-Nerode theorem *} |
45 Myhill-Nerode theorem *} |
44 |
46 |
45 lemma closure_complement [intro]: |
47 lemma closure_complement [intro]: |
46 fixes A::"('a::finite) lang" |
48 fixes A::"('a::finite) lang" |
49 proof - |
51 proof - |
50 from assms have "finite (UNIV // \<approx>A)" by (simp add: Myhill_Nerode) |
52 from assms have "finite (UNIV // \<approx>A)" by (simp add: Myhill_Nerode) |
51 then have "finite (UNIV // \<approx>(-A))" by (simp add: str_eq_def) |
53 then have "finite (UNIV // \<approx>(-A))" by (simp add: str_eq_def) |
52 then show "regular (- A)" by (simp add: Myhill_Nerode) |
54 then show "regular (- A)" by (simp add: Myhill_Nerode) |
53 qed |
55 qed |
|
56 |
|
57 subsection {* Closure under @{text "-"} and @{text "\<inter>"} *} |
54 |
58 |
55 lemma closure_difference [intro]: |
59 lemma closure_difference [intro]: |
56 fixes A::"('a::finite) lang" |
60 fixes A::"('a::finite) lang" |
57 assumes "regular A" "regular B" |
61 assumes "regular A" "regular B" |
58 shows "regular (A - B)" |
62 shows "regular (A - B)" |
141 qed |
145 qed |
142 |
146 |
143 subsection {* Closure under left-quotients *} |
147 subsection {* Closure under left-quotients *} |
144 |
148 |
145 abbreviation |
149 abbreviation |
146 "Ders_lang A B \<equiv> \<Union>x \<in> A. Ders x B" |
150 "Deriv_lang A B \<equiv> \<Union>x \<in> A. Derivs x B" |
147 |
151 |
148 lemma closure_left_quotient: |
152 lemma closure_left_quotient: |
149 assumes "regular A" |
153 assumes "regular A" |
150 shows "regular (Ders_lang B A)" |
154 shows "regular (Deriv_lang B A)" |
151 proof - |
155 proof - |
152 from assms obtain r::"'a rexp" where eq: "lang r = A" by auto |
156 from assms obtain r::"'a rexp" where eq: "lang r = A" by auto |
153 have fin: "finite (pders_lang B r)" by (rule finite_pders_lang) |
157 have fin: "finite (pderivs_lang B r)" by (rule finite_pderivs_lang) |
154 |
158 |
155 have "Ders_lang B (lang r) = (\<Union> lang ` (pders_lang B r))" |
159 have "Deriv_lang B (lang r) = (\<Union> lang ` (pderivs_lang B r))" |
156 by (simp add: Ders_pders pders_lang_def) |
160 by (simp add: Derivs_pderivs pderivs_lang_def) |
157 also have "\<dots> = lang (\<Uplus>(pders_lang B r))" using fin by simp |
161 also have "\<dots> = lang (\<Uplus>(pderivs_lang B r))" using fin by simp |
158 finally have "Ders_lang B A = lang (\<Uplus>(pders_lang B r))" using eq |
162 finally have "Deriv_lang B A = lang (\<Uplus>(pderivs_lang B r))" using eq |
159 by simp |
163 by simp |
160 then show "regular (Ders_lang B A)" by auto |
164 then show "regular (Deriv_lang B A)" by auto |
161 qed |
165 qed |
162 |
166 |
163 subsection {* Finite and co-finite set are regular *} |
167 subsection {* Finite and co-finite sets are regular *} |
164 |
168 |
165 lemma singleton_regular: |
169 lemma singleton_regular: |
166 shows "regular {s}" |
170 shows "regular {s}" |
167 proof (induct s) |
171 proof (induct s) |
168 case Nil |
172 case Nil |
203 then have "regular (-(- A))" by (rule closure_complement) |
207 then have "regular (-(- A))" by (rule closure_complement) |
204 then show "regular A" by simp |
208 then show "regular A" by simp |
205 qed |
209 qed |
206 |
210 |
207 |
211 |
208 subsection {* non-regularity of particular languages *} |
212 subsection {* Non-regularity for languages *} |
209 |
213 |
210 lemma continuation_lemma: |
214 lemma continuation_lemma: |
211 fixes A B::"('a::finite list) set" |
215 fixes A B::"('a::finite list) set" |
212 assumes reg: "regular A" |
216 assumes reg: "regular A" |
213 and inf: "infinite B" |
217 and inf: "infinite B" |
236 then obtain b where "b \<in> B" "b \<noteq> a" "b \<approx>A a" by blast |
240 then obtain b where "b \<in> B" "b \<noteq> a" "b \<approx>A a" by blast |
237 with in_a show "\<exists>x \<in> B. \<exists>y \<in> B. x \<noteq> y \<and> x \<approx>A y" |
241 with in_a show "\<exists>x \<in> B. \<exists>y \<in> B. x \<noteq> y \<and> x \<approx>A y" |
238 by blast |
242 by blast |
239 qed |
243 qed |
240 |
244 |
241 definition |
|
242 "ex1 a b \<equiv> {replicate n a @ replicate n b | n. True}" |
|
243 |
|
244 (* |
|
245 lemma |
|
246 fixes a b::"'a::finite" |
|
247 assumes "a \<noteq> b" |
|
248 shows "\<not> regular (ex1 a b)" |
|
249 proof - |
|
250 { assume a: "regular (ex1 a b)" |
|
251 def fool \<equiv> "{replicate i a | i. True}" |
|
252 have b: "infinite fool" |
|
253 unfolding fool_def |
|
254 unfolding infinite_iff_countable_subset |
|
255 apply(rule_tac x="\<lambda>i. replicate i a" in exI) |
|
256 apply(auto simp add: inj_on_def) |
|
257 done |
|
258 from a b have "\<exists>x \<in> fool. \<exists>y \<in> fool. x \<noteq> y \<and> x \<approx>(ex1 a b) y" |
|
259 using continuation_lemma by blast |
|
260 moreover |
|
261 have c: "\<forall>x \<in> fool. \<forall>y \<in> fool. x \<noteq> y \<longrightarrow> \<not>(x \<approx>(ex1 a b) y)" |
|
262 apply(rule ballI) |
|
263 apply(rule ballI) |
|
264 apply(rule impI) |
|
265 unfolding fool_def |
|
266 apply(simp) |
|
267 apply(erule exE)+ |
|
268 unfolding str_eq_def |
|
269 apply(simp) |
|
270 apply(rule_tac x="replicate i b" in exI) |
|
271 apply(simp add: ex1_def) |
|
272 apply(rule iffI) |
|
273 prefer 2 |
|
274 apply(rule_tac x="i" in exI) |
|
275 apply(simp) |
|
276 apply(rule allI) |
|
277 apply(rotate_tac 3) |
|
278 apply(thin_tac "?X") |
|
279 apply(auto) |
|
280 sorry |
|
281 ultimately have "False" by auto |
|
282 } |
|
283 then show "\<not> regular (ex1 a b)" by auto |
|
284 qed |
|
285 *) |
|
286 |
|
287 |
245 |
288 end |
246 end |