|
1 (* Author: Christian Urban, Xingyuan Zhang, Chunhan Wu *) |
|
2 theory Closures |
|
3 imports Derivatives |
|
4 begin |
|
5 |
|
6 section {* Closure properties of regular languages *} |
|
7 |
|
8 abbreviation |
|
9 regular :: "'a lang \<Rightarrow> bool" |
|
10 where |
|
11 "regular A \<equiv> \<exists>r. A = lang r" |
|
12 |
|
13 subsection {* Closure under set operations *} |
|
14 |
|
15 lemma closure_union [intro]: |
|
16 assumes "regular A" "regular B" |
|
17 shows "regular (A \<union> B)" |
|
18 proof - |
|
19 from assms obtain r1 r2::"'a rexp" where "lang r1 = A" "lang r2 = B" by auto |
|
20 then have "A \<union> B = lang (Plus r1 r2)" by simp |
|
21 then show "regular (A \<union> B)" by blast |
|
22 qed |
|
23 |
|
24 lemma closure_seq [intro]: |
|
25 assumes "regular A" "regular B" |
|
26 shows "regular (A \<cdot> B)" |
|
27 proof - |
|
28 from assms obtain r1 r2::"'a rexp" where "lang r1 = A" "lang r2 = B" by auto |
|
29 then have "A \<cdot> B = lang (Times r1 r2)" by simp |
|
30 then show "regular (A \<cdot> B)" by blast |
|
31 qed |
|
32 |
|
33 lemma closure_star [intro]: |
|
34 assumes "regular A" |
|
35 shows "regular (A\<star>)" |
|
36 proof - |
|
37 from assms obtain r::"'a rexp" where "lang r = A" by auto |
|
38 then have "A\<star> = lang (Star r)" by simp |
|
39 then show "regular (A\<star>)" by blast |
|
40 qed |
|
41 |
|
42 text {* Closure under complementation is proved via the |
|
43 Myhill-Nerode theorem *} |
|
44 |
|
45 lemma closure_complement [intro]: |
|
46 fixes A::"('a::finite) lang" |
|
47 assumes "regular A" |
|
48 shows "regular (- A)" |
|
49 proof - |
|
50 from assms have "finite (UNIV // \<approx>A)" by (simp add: Myhill_Nerode) |
|
51 then have "finite (UNIV // \<approx>(-A))" by (simp add: str_eq_rel_def) |
|
52 then show "regular (- A)" by (simp add: Myhill_Nerode) |
|
53 qed |
|
54 |
|
55 lemma closure_difference [intro]: |
|
56 fixes A::"('a::finite) lang" |
|
57 assumes "regular A" "regular B" |
|
58 shows "regular (A - B)" |
|
59 proof - |
|
60 have "A - B = - (- A \<union> B)" by blast |
|
61 moreover |
|
62 have "regular (- (- A \<union> B))" |
|
63 using assms by blast |
|
64 ultimately show "regular (A - B)" by simp |
|
65 qed |
|
66 |
|
67 lemma closure_intersection [intro]: |
|
68 fixes A::"('a::finite) lang" |
|
69 assumes "regular A" "regular B" |
|
70 shows "regular (A \<inter> B)" |
|
71 proof - |
|
72 have "A \<inter> B = - (- A \<union> - B)" by blast |
|
73 moreover |
|
74 have "regular (- (- A \<union> - B))" |
|
75 using assms by blast |
|
76 ultimately show "regular (A \<inter> B)" by simp |
|
77 qed |
|
78 |
|
79 subsection {* Closure under string reversal *} |
|
80 |
|
81 fun |
|
82 Rev :: "'a rexp \<Rightarrow> 'a rexp" |
|
83 where |
|
84 "Rev Zero = Zero" |
|
85 | "Rev One = One" |
|
86 | "Rev (Atom c) = Atom c" |
|
87 | "Rev (Plus r1 r2) = Plus (Rev r1) (Rev r2)" |
|
88 | "Rev (Times r1 r2) = Times (Rev r2) (Rev r1)" |
|
89 | "Rev (Star r) = Star (Rev r)" |
|
90 |
|
91 lemma rev_seq[simp]: |
|
92 shows "rev ` (B \<cdot> A) = (rev ` A) \<cdot> (rev ` B)" |
|
93 unfolding conc_def image_def |
|
94 by (auto) (metis rev_append)+ |
|
95 |
|
96 lemma rev_star1: |
|
97 assumes a: "s \<in> (rev ` A)\<star>" |
|
98 shows "s \<in> rev ` (A\<star>)" |
|
99 using a |
|
100 proof(induct rule: star_induct) |
|
101 case (append s1 s2) |
|
102 have inj: "inj (rev::'a list \<Rightarrow> 'a list)" unfolding inj_on_def by auto |
|
103 have "s1 \<in> rev ` A" "s2 \<in> rev ` (A\<star>)" by fact+ |
|
104 then obtain x1 x2 where "x1 \<in> A" "x2 \<in> A\<star>" and eqs: "s1 = rev x1" "s2 = rev x2" by auto |
|
105 then have "x1 \<in> A\<star>" "x2 \<in> A\<star>" by (auto) |
|
106 then have "x2 @ x1 \<in> A\<star>" by (auto) |
|
107 then have "rev (x2 @ x1) \<in> rev ` A\<star>" using inj by (simp only: inj_image_mem_iff) |
|
108 then show "s1 @ s2 \<in> rev ` A\<star>" using eqs by simp |
|
109 qed (auto) |
|
110 |
|
111 lemma rev_star2: |
|
112 assumes a: "s \<in> A\<star>" |
|
113 shows "rev s \<in> (rev ` A)\<star>" |
|
114 using a |
|
115 proof(induct rule: star_induct) |
|
116 case (append s1 s2) |
|
117 have inj: "inj (rev::'a list \<Rightarrow> 'a list)" unfolding inj_on_def by auto |
|
118 have "s1 \<in> A"by fact |
|
119 then have "rev s1 \<in> rev ` A" using inj by (simp only: inj_image_mem_iff) |
|
120 then have "rev s1 \<in> (rev ` A)\<star>" by (auto) |
|
121 moreover |
|
122 have "rev s2 \<in> (rev ` A)\<star>" by fact |
|
123 ultimately show "rev (s1 @ s2) \<in> (rev ` A)\<star>" by (auto) |
|
124 qed (auto) |
|
125 |
|
126 lemma rev_star [simp]: |
|
127 shows " rev ` (A\<star>) = (rev ` A)\<star>" |
|
128 using rev_star1 rev_star2 by auto |
|
129 |
|
130 lemma rev_lang: |
|
131 shows "rev ` (lang r) = lang (Rev r)" |
|
132 by (induct r) (simp_all add: image_Un) |
|
133 |
|
134 lemma closure_reversal [intro]: |
|
135 assumes "regular A" |
|
136 shows "regular (rev ` A)" |
|
137 proof - |
|
138 from assms obtain r::"'a rexp" where "A = lang r" by auto |
|
139 then have "lang (Rev r) = rev ` A" by (simp add: rev_lang) |
|
140 then show "regular (rev` A)" by blast |
|
141 qed |
|
142 |
|
143 subsection {* Closure under left-quotients *} |
|
144 |
|
145 lemma closure_left_quotient: |
|
146 assumes "regular A" |
|
147 shows "regular (Ders_set B A)" |
|
148 proof - |
|
149 from assms obtain r::"'a rexp" where eq: "lang r = A" by auto |
|
150 have fin: "finite (pders_set B r)" by (rule finite_pders_set) |
|
151 |
|
152 have "Ders_set B (lang r) = (\<Union> lang ` (pders_set B r))" |
|
153 by (simp add: Ders_set_pders_set) |
|
154 also have "\<dots> = lang (\<Uplus>(pders_set B r))" using fin by simp |
|
155 finally have "Ders_set B A = lang (\<Uplus>(pders_set B r))" using eq |
|
156 by simp |
|
157 then show "regular (Ders_set B A)" by auto |
|
158 qed |
|
159 |
|
160 |
|
161 end |