|
1 (* Author: Christian Urban, Xingyuan Zhang, Chunhan Wu *) |
1 theory Closure |
2 theory Closure |
2 imports Myhill_2 |
3 imports Derivs |
3 begin |
4 begin |
4 |
5 |
5 section {* Closure properties of regular languages *} |
6 section {* Closure properties of regular languages *} |
6 |
7 |
7 abbreviation |
8 abbreviation |
8 regular :: "lang \<Rightarrow> bool" |
9 regular :: "lang \<Rightarrow> bool" |
9 where |
10 where |
10 "regular A \<equiv> \<exists>r::rexp. A = L r" |
11 "regular A \<equiv> \<exists>r. A = L_rexp r" |
11 |
12 |
|
13 subsection {* Closure under set operations *} |
12 |
14 |
13 lemma closure_union[intro]: |
15 lemma closure_union[intro]: |
14 assumes "regular A" "regular B" |
16 assumes "regular A" "regular B" |
15 shows "regular (A \<union> B)" |
17 shows "regular (A \<union> B)" |
16 proof - |
18 proof - |
17 from assms obtain r1 r2::rexp where "L r1 = A" "L r2 = B" by auto |
19 from assms obtain r1 r2::rexp where "L_rexp r1 = A" "L_rexp r2 = B" by auto |
18 then have "A \<union> B = L (ALT r1 r2)" by simp |
20 then have "A \<union> B = L_rexp (ALT r1 r2)" by simp |
19 then show "regular (A \<union> B)" by blast |
21 then show "regular (A \<union> B)" by blast |
20 qed |
22 qed |
21 |
23 |
22 lemma closure_seq[intro]: |
24 lemma closure_seq[intro]: |
23 assumes "regular A" "regular B" |
25 assumes "regular A" "regular B" |
24 shows "regular (A ;; B)" |
26 shows "regular (A \<cdot> B)" |
25 proof - |
27 proof - |
26 from assms obtain r1 r2::rexp where "L r1 = A" "L r2 = B" by auto |
28 from assms obtain r1 r2::rexp where "L_rexp r1 = A" "L_rexp r2 = B" by auto |
27 then have "A ;; B = L (SEQ r1 r2)" by simp |
29 then have "A \<cdot> B = L_rexp (SEQ r1 r2)" by simp |
28 then show "regular (A ;; B)" by blast |
30 then show "regular (A \<cdot> B)" by blast |
29 qed |
31 qed |
30 |
32 |
31 lemma closure_star[intro]: |
33 lemma closure_star[intro]: |
32 assumes "regular A" |
34 assumes "regular A" |
33 shows "regular (A\<star>)" |
35 shows "regular (A\<star>)" |
34 proof - |
36 proof - |
35 from assms obtain r::rexp where "L r = A" by auto |
37 from assms obtain r::rexp where "L_rexp r = A" by auto |
36 then have "A\<star> = L (STAR r)" by simp |
38 then have "A\<star> = L_rexp (STAR r)" by simp |
37 then show "regular (A\<star>)" by blast |
39 then show "regular (A\<star>)" by blast |
38 qed |
40 qed |
|
41 |
|
42 text {* Closure under complementation is proved via the |
|
43 Myhill-Nerode theorem *} |
39 |
44 |
40 lemma closure_complement[intro]: |
45 lemma closure_complement[intro]: |
41 assumes "regular A" |
46 assumes "regular A" |
42 shows "regular (- A)" |
47 shows "regular (- A)" |
43 proof - |
48 proof - |
79 | "Rev (CHAR c) = CHAR c" |
83 | "Rev (CHAR c) = CHAR c" |
80 | "Rev (ALT r1 r2) = ALT (Rev r1) (Rev r2)" |
84 | "Rev (ALT r1 r2) = ALT (Rev r1) (Rev r2)" |
81 | "Rev (SEQ r1 r2) = SEQ (Rev r2) (Rev r1)" |
85 | "Rev (SEQ r1 r2) = SEQ (Rev r2) (Rev r1)" |
82 | "Rev (STAR r) = STAR (Rev r)" |
86 | "Rev (STAR r) = STAR (Rev r)" |
83 |
87 |
84 lemma rev_Seq: |
88 lemma rev_seq[simp]: |
85 "(rev ` A) ;; (rev ` B) = rev ` (B ;; A)" |
89 shows "rev ` (B \<cdot> A) = (rev ` A) \<cdot> (rev ` B)" |
86 unfolding Seq_def image_def |
90 unfolding Seq_def image_def |
87 apply(auto) |
91 by (auto) (metis rev_append)+ |
88 apply(rule_tac x="xb @ xa" in exI) |
|
89 apply(auto) |
|
90 done |
|
91 |
92 |
92 lemma rev_Star1: |
93 lemma rev_star1: |
93 assumes a: "s \<in> (rev ` A)\<star>" |
94 assumes a: "s \<in> (rev ` A)\<star>" |
94 shows "s \<in> rev ` (A\<star>)" |
95 shows "s \<in> rev ` (A\<star>)" |
95 using a |
96 using a |
96 proof(induct rule: star_induct) |
97 proof(induct rule: star_induct) |
97 case (step s1 s2) |
98 case (step s1 s2) |
102 then have "x2 @ x1 \<in> A\<star>" by (auto intro: star_intro1) |
103 then have "x2 @ x1 \<in> A\<star>" by (auto intro: star_intro1) |
103 then have "rev (x2 @ x1) \<in> rev ` A\<star>" using inj by (simp only: inj_image_mem_iff) |
104 then have "rev (x2 @ x1) \<in> rev ` A\<star>" using inj by (simp only: inj_image_mem_iff) |
104 then show "s1 @ s2 \<in> rev ` A\<star>" using eqs by simp |
105 then show "s1 @ s2 \<in> rev ` A\<star>" using eqs by simp |
105 qed (auto) |
106 qed (auto) |
106 |
107 |
107 lemma rev_Star2: |
108 lemma rev_star2: |
108 assumes a: "s \<in> A\<star>" |
109 assumes a: "s \<in> A\<star>" |
109 shows "rev s \<in> (rev ` A)\<star>" |
110 shows "rev s \<in> (rev ` A)\<star>" |
110 using a |
111 using a |
111 proof(induct rule: star_induct) |
112 proof(induct rule: star_induct) |
112 case (step s1 s2) |
113 case (step s1 s2) |
117 moreover |
118 moreover |
118 have "rev s2 \<in> (rev ` A)\<star>" by fact |
119 have "rev s2 \<in> (rev ` A)\<star>" by fact |
119 ultimately show "rev (s1 @ s2) \<in> (rev ` A)\<star>" by (auto intro: star_intro1) |
120 ultimately show "rev (s1 @ s2) \<in> (rev ` A)\<star>" by (auto intro: star_intro1) |
120 qed (auto) |
121 qed (auto) |
121 |
122 |
122 lemma rev_Star: |
123 lemma rev_star[simp]: |
123 "(rev ` A)\<star> = rev ` (A\<star>)" |
124 shows " rev ` (A\<star>) = (rev ` A)\<star>" |
124 using rev_Star1 rev_Star2 by auto |
125 using rev_star1 rev_star2 by auto |
125 |
126 |
126 lemma rev_lang: |
127 lemma rev_lang: |
127 "L (Rev r) = rev ` (L r)" |
128 shows "rev ` (L_rexp r) = L_rexp (Rev r)" |
128 by (induct r) (simp_all add: rev_Star rev_Seq image_Un) |
129 by (induct r) (simp_all add: image_Un) |
129 |
130 |
130 lemma closure_reversal[intro]: |
131 lemma closure_reversal[intro]: |
131 assumes "regular A" |
132 assumes "regular A" |
132 shows "regular (rev ` A)" |
133 shows "regular (rev ` A)" |
133 proof - |
134 proof - |
134 from assms obtain r::rexp where "L r = A" by auto |
135 from assms obtain r::rexp where "A = L_rexp r" by auto |
135 then have "L (Rev r) = rev ` A" by (simp add: rev_lang) |
136 then have "L_rexp (Rev r) = rev ` A" by (simp add: rev_lang) |
136 then show "regular (rev` A)" by blast |
137 then show "regular (rev` A)" by blast |
137 qed |
138 qed |
138 |
139 |
|
140 subsection {* Closure under left-quotients *} |
|
141 |
|
142 lemma closure_left_quotient: |
|
143 assumes "regular A" |
|
144 shows "regular (Ders_set B A)" |
|
145 proof - |
|
146 from assms obtain r::rexp where eq: "L_rexp r = A" by auto |
|
147 have fin: "finite (pders_set B r)" by (rule finite_pders_set) |
|
148 |
|
149 have "Ders_set B (L_rexp r) = (\<Union> L_rexp ` (pders_set B r))" |
|
150 by (simp add: Ders_set_pders_set) |
|
151 also have "\<dots> = L_rexp (\<Uplus>(pders_set B r))" using fin by simp |
|
152 finally have "Ders_set B A = L_rexp (\<Uplus>(pders_set B r))" using eq |
|
153 by simp |
|
154 then show "regular (Ders_set B A)" by auto |
|
155 qed |
|
156 |
139 |
157 |
140 end |
158 end |