30 |
30 |
31 text {* |
31 text {* |
32 Sequential composition of two languages @{text "L1"} and @{text "L2"} |
32 Sequential composition of two languages @{text "L1"} and @{text "L2"} |
33 *} |
33 *} |
34 |
34 |
35 definition Seq :: "lang \<Rightarrow> lang \<Rightarrow> lang" ("_ ;; _" [100,100] 100) |
35 definition Seq :: "lang \<Rightarrow> lang \<Rightarrow> lang" (infixr ";;" 100) |
36 where |
36 where |
37 "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}" |
38 |
38 |
39 text {* Transitive closure of language @{text "L"}. *} |
39 text {* |
|
40 Transitive closure of language @{text "L"}. |
|
41 *} |
|
42 |
40 inductive_set |
43 inductive_set |
41 Star :: "lang \<Rightarrow> lang" ("_\<star>" [101] 102) |
44 Star :: "lang \<Rightarrow> lang" ("_\<star>" [101] 102) |
42 for L |
45 for L |
43 where |
46 where |
44 start[intro]: "[] \<in> L\<star>" |
47 start[intro]: "[] \<in> L\<star>" |
45 | step[intro]: "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1@s2 \<in> L\<star>" |
48 | step[intro]: "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1@s2 \<in> L\<star>" |
46 |
49 |
47 text {* Some properties of operator @{text ";;"}.*} |
50 text {* Some properties of operator @{text ";;"}. *} |
48 |
51 |
49 lemma seq_union_distrib: |
52 lemma seq_union_distrib_right: |
50 "(A \<union> B) ;; C = (A ;; C) \<union> (B ;; C)" |
53 shows "(A \<union> B) ;; C = (A ;; C) \<union> (B ;; C)" |
51 by (auto simp:Seq_def) |
54 unfolding Seq_def by auto |
|
55 |
|
56 lemma seq_union_distrib_left: |
|
57 shows "C ;; (A \<union> B) = (C ;; A) \<union> (C ;; B)" |
|
58 unfolding Seq_def by auto |
52 |
59 |
53 lemma seq_intro: |
60 lemma seq_intro: |
54 "\<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x @ y \<in> A ;; B " |
61 "\<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x @ y \<in> A ;; B " |
55 by (auto simp:Seq_def) |
62 by (auto simp:Seq_def) |
56 |
63 |
57 lemma seq_assoc: |
64 lemma seq_assoc: |
58 "(A ;; B) ;; C = A ;; (B ;; C)" |
65 shows "(A ;; B) ;; C = A ;; (B ;; C)" |
59 apply(auto simp:Seq_def) |
66 unfolding Seq_def |
60 apply blast |
67 apply(auto) |
|
68 apply(blast) |
61 by (metis append_assoc) |
69 by (metis append_assoc) |
62 |
70 |
63 lemma star_intro1[rule_format]: "x \<in> lang\<star> \<Longrightarrow> \<forall> y. y \<in> lang\<star> \<longrightarrow> x @ y \<in> lang\<star>" |
71 lemma seq_empty [simp]: |
|
72 shows "A ;; {[]} = A" |
|
73 and "{[]} ;; A = A" |
|
74 by (simp_all add: Seq_def) |
|
75 |
|
76 |
|
77 lemma star_intro1[rule_format]: |
|
78 "x \<in> lang\<star> \<Longrightarrow> \<forall> y. y \<in> lang\<star> \<longrightarrow> x @ y \<in> lang\<star>" |
64 by (erule Star.induct, auto) |
79 by (erule Star.induct, auto) |
65 |
80 |
66 lemma star_intro2: "y \<in> lang \<Longrightarrow> y \<in> lang\<star>" |
81 lemma star_intro2: "y \<in> lang \<Longrightarrow> y \<in> lang\<star>" |
67 by (drule step[of y lang "[]"], auto simp:start) |
82 by (drule step[of y lang "[]"], auto simp:start) |
68 |
83 |
72 |
87 |
73 lemma star_decom: |
88 lemma star_decom: |
74 "\<lbrakk>x \<in> lang\<star>; x \<noteq> []\<rbrakk> \<Longrightarrow>(\<exists> a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> lang \<and> b \<in> lang\<star>)" |
89 "\<lbrakk>x \<in> lang\<star>; x \<noteq> []\<rbrakk> \<Longrightarrow>(\<exists> a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> lang \<and> b \<in> lang\<star>)" |
75 by (induct x rule: Star.induct, simp, blast) |
90 by (induct x rule: Star.induct, simp, blast) |
76 |
91 |
77 lemma star_decom': |
92 lemma lang_star_cases: |
78 "\<lbrakk>x \<in> lang\<star>; x \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>a b. x = a @ b \<and> a \<in> lang\<star> \<and> b \<in> lang" |
93 shows "L\<star> = {[]} \<union> L ;; L\<star>" |
79 apply (induct x rule:Star.induct, simp) |
94 proof |
80 apply (case_tac "s2 = []") |
95 { fix x |
81 apply (rule_tac x = "[]" in exI, rule_tac x = s1 in exI, simp add:start) |
96 have "x \<in> L\<star> \<Longrightarrow> x \<in> {[]} \<union> L ;; L\<star>" |
82 apply (simp, (erule exE| erule conjE)+) |
97 unfolding Seq_def |
83 by (rule_tac x = "s1 @ a" in exI, rule_tac x = b in exI, simp add:step) |
98 by (induct rule: Star.induct) (auto) |
|
99 } |
|
100 then show "L\<star> \<subseteq> {[]} \<union> L ;; L\<star>" by auto |
|
101 next |
|
102 show "{[]} \<union> L ;; L\<star> \<subseteq> L\<star>" |
|
103 unfolding Seq_def by auto |
|
104 qed |
|
105 |
|
106 fun |
|
107 pow :: "lang \<Rightarrow> nat \<Rightarrow> lang" (infixl "\<up>" 100) |
|
108 where |
|
109 "A \<up> 0 = {[]}" |
|
110 | "A \<up> (Suc n) = A ;; (A \<up> n)" |
|
111 |
|
112 lemma star_pow_eq: |
|
113 shows "A\<star> = (\<Union>n. A \<up> n)" |
|
114 proof - |
|
115 { fix n x |
|
116 assume "x \<in> (A \<up> n)" |
|
117 then have "x \<in> A\<star>" |
|
118 by (induct n arbitrary: x) (auto simp add: Seq_def) |
|
119 } |
|
120 moreover |
|
121 { fix x |
|
122 assume "x \<in> A\<star>" |
|
123 then have "\<exists>n. x \<in> A \<up> n" |
|
124 proof (induct rule: Star.induct) |
|
125 case start |
|
126 have "[] \<in> A \<up> 0" by auto |
|
127 then show "\<exists>n. [] \<in> A \<up> n" by blast |
|
128 next |
|
129 case (step s1 s2) |
|
130 have "s1 \<in> A" by fact |
|
131 moreover |
|
132 have "\<exists>n. s2 \<in> A \<up> n" by fact |
|
133 then obtain n where "s2 \<in> A \<up> n" by blast |
|
134 ultimately |
|
135 have "s1 @ s2 \<in> A \<up> (Suc n)" by (auto simp add: Seq_def) |
|
136 then show "\<exists>n. s1 @ s2 \<in> A \<up> n" by blast |
|
137 qed |
|
138 } |
|
139 ultimately show "A\<star> = (\<Union>n. A \<up> n)" by auto |
|
140 qed |
|
141 |
|
142 lemma |
|
143 shows seq_Union_left: "B ;; (\<Union>n. A \<up> n) = (\<Union>n. B ;; (A \<up> n))" |
|
144 and seq_Union_right: "(\<Union>n. A \<up> n) ;; B = (\<Union>n. (A \<up> n) ;; B)" |
|
145 unfolding Seq_def by auto |
|
146 |
|
147 lemma seq_pow_comm: |
|
148 shows "A ;; (A \<up> n) = (A \<up> n) ;; A" |
|
149 by (induct n) (simp_all add: seq_assoc[symmetric]) |
|
150 |
|
151 lemma seq_star_comm: |
|
152 shows "A ;; A\<star> = A\<star> ;; A" |
|
153 unfolding star_pow_eq |
|
154 unfolding seq_Union_left |
|
155 unfolding seq_pow_comm |
|
156 unfolding seq_Union_right |
|
157 by simp |
|
158 |
|
159 text {* Two lemmas about the length of strings in @{text "A \<up> n"} *} |
|
160 |
|
161 lemma pow_length: |
|
162 assumes a: "[] \<notin> A" |
|
163 and b: "s \<in> A \<up> Suc n" |
|
164 shows "n < length s" |
|
165 using b |
|
166 proof (induct n arbitrary: s) |
|
167 case 0 |
|
168 have "s \<in> A \<up> Suc 0" by fact |
|
169 with a have "s \<noteq> []" by auto |
|
170 then show "0 < length s" by auto |
|
171 next |
|
172 case (Suc n) |
|
173 have ih: "\<And>s. s \<in> A \<up> Suc n \<Longrightarrow> n < length s" by fact |
|
174 have "s \<in> A \<up> Suc (Suc n)" by fact |
|
175 then obtain s1 s2 where eq: "s = s1 @ s2" and *: "s1 \<in> A" and **: "s2 \<in> A \<up> Suc n" |
|
176 by (auto simp add: Seq_def) |
|
177 from ih ** have "n < length s2" by simp |
|
178 moreover have "0 < length s1" using * a by auto |
|
179 ultimately show "Suc n < length s" unfolding eq |
|
180 by (simp only: length_append) |
|
181 qed |
|
182 |
|
183 lemma seq_pow_length: |
|
184 assumes a: "[] \<notin> A" |
|
185 and b: "s \<in> B ;; (A \<up> Suc n)" |
|
186 shows "n < length s" |
|
187 proof - |
|
188 from b obtain s1 s2 where eq: "s = s1 @ s2" and *: "s2 \<in> A \<up> Suc n" |
|
189 unfolding Seq_def by auto |
|
190 from * have " n < length s2" by (rule pow_length[OF a]) |
|
191 then show "n < length s" using eq by simp |
|
192 qed |
|
193 |
|
194 |
|
195 section {* A slightly modified version of Arden's lemma *} |
|
196 |
|
197 text {* |
|
198 Arden's lemma expressed at the level of languages, rather |
|
199 than the level of regular expression. |
|
200 *} |
|
201 |
|
202 |
|
203 lemma ardens_helper: |
|
204 assumes eq: "X = X ;; A \<union> B" |
|
205 shows "X = X ;; (A \<up> Suc n) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))" |
|
206 proof (induct n) |
|
207 case 0 |
|
208 show "X = X ;; (A \<up> Suc 0) \<union> (\<Union>(m::nat)\<in>{0..0}. B ;; (A \<up> m))" |
|
209 using eq by simp |
|
210 next |
|
211 case (Suc n) |
|
212 have ih: "X = X ;; (A \<up> Suc n) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))" by fact |
|
213 also have "\<dots> = (X ;; A \<union> B) ;; (A \<up> Suc n) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))" using eq by simp |
|
214 also have "\<dots> = X ;; (A \<up> Suc (Suc n)) \<union> (B ;; (A \<up> Suc n)) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))" |
|
215 by (simp add: seq_union_distrib_right seq_assoc) |
|
216 also have "\<dots> = X ;; (A \<up> Suc (Suc n)) \<union> (\<Union>m\<in>{0..Suc n}. B ;; (A \<up> m))" |
|
217 by (auto simp add: le_Suc_eq) |
|
218 finally show "X = X ;; (A \<up> Suc (Suc n)) \<union> (\<Union>m\<in>{0..Suc n}. B ;; (A \<up> m))" . |
|
219 qed |
|
220 |
|
221 theorem ardens_revised: |
|
222 assumes nemp: "[] \<notin> A" |
|
223 shows "X = X ;; A \<union> B \<longleftrightarrow> X = B ;; A\<star>" |
|
224 proof |
|
225 assume eq: "X = B ;; A\<star>" |
|
226 have "A\<star> = {[]} \<union> A\<star> ;; A" |
|
227 unfolding seq_star_comm[symmetric] |
|
228 by (rule lang_star_cases) |
|
229 then have "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)" |
|
230 unfolding Seq_def by simp |
|
231 also have "\<dots> = B \<union> B ;; (A\<star> ;; A)" |
|
232 unfolding seq_union_distrib_left by simp |
|
233 also have "\<dots> = B \<union> (B ;; A\<star>) ;; A" |
|
234 by (simp only: seq_assoc) |
|
235 finally show "X = X ;; A \<union> B" |
|
236 using eq by blast |
|
237 next |
|
238 assume eq: "X = X ;; A \<union> B" |
|
239 { fix n::nat |
|
240 have "B ;; (A \<up> n) \<subseteq> X" using ardens_helper[OF eq, of "n"] by auto } |
|
241 then have "B ;; A\<star> \<subseteq> X" unfolding star_pow_eq Seq_def |
|
242 by (auto simp add: UNION_def) |
|
243 moreover |
|
244 { fix s::string |
|
245 obtain k where "k = length s" by auto |
|
246 then have not_in: "s \<notin> X ;; (A \<up> Suc k)" |
|
247 using seq_pow_length[OF nemp] by blast |
|
248 assume "s \<in> X" |
|
249 then have "s \<in> X ;; (A \<up> Suc k) \<union> (\<Union>m\<in>{0..k}. B ;; (A \<up> m))" |
|
250 using ardens_helper[OF eq, of "k"] by auto |
|
251 then have "s \<in> (\<Union>m\<in>{0..k}. B ;; (A \<up> m))" using not_in by auto |
|
252 moreover |
|
253 have "(\<Union>m\<in>{0..k}. B ;; (A \<up> m)) \<subseteq> (\<Union>n. B ;; (A \<up> n))" by auto |
|
254 ultimately |
|
255 have "s \<in> B ;; A\<star>" unfolding star_pow_eq seq_Union_left |
|
256 by auto } |
|
257 then have "X \<subseteq> B ;; A\<star>" by auto |
|
258 ultimately |
|
259 show "X = B ;; A\<star>" by simp |
|
260 qed |
|
261 |
84 |
262 |
85 |
263 |
86 text {* The syntax of regular expressions is defined by the datatype @{text "rexp"}. *} |
264 text {* The syntax of regular expressions is defined by the datatype @{text "rexp"}. *} |
87 datatype rexp = |
265 datatype rexp = |
88 NULL |
266 NULL |
115 | "L_rexp (SEQ r1 r2) = (L_rexp r1) ;; (L_rexp r2)" |
293 | "L_rexp (SEQ r1 r2) = (L_rexp r1) ;; (L_rexp r2)" |
116 | "L_rexp (ALT r1 r2) = (L_rexp r1) \<union> (L_rexp r2)" |
294 | "L_rexp (ALT r1 r2) = (L_rexp r1) \<union> (L_rexp r2)" |
117 | "L_rexp (STAR r) = (L_rexp r)\<star>" |
295 | "L_rexp (STAR r) = (L_rexp r)\<star>" |
118 end |
296 end |
119 |
297 |
|
298 text {* |
|
299 To obtain equational system out of finite set of equivalent classes, a fold operation |
|
300 on finite set @{text "folds"} is defined. The use of @{text "SOME"} makes @{text "fold"} |
|
301 more robust than the @{text "fold"} in Isabelle library. The expression @{text "folds f"} |
|
302 makes sense when @{text "f"} is not @{text "associative"} and @{text "commutitive"}, |
|
303 while @{text "fold f"} does not. |
|
304 *} |
|
305 |
|
306 definition |
|
307 folds :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b" |
|
308 where |
|
309 "folds f z S \<equiv> SOME x. fold_graph f z S x" |
|
310 |
|
311 text {* |
|
312 The following lemma assures that the arbitrary choice made by the @{text "SOME"} in @{text "folds"} |
|
313 does not affect the @{text "L"}-value of the resultant regular expression. |
|
314 *} |
|
315 lemma folds_alt_simp [simp]: |
|
316 "finite rs \<Longrightarrow> L (folds ALT NULL rs) = \<Union> (L ` rs)" |
|
317 apply (rule set_eq_intro, simp add:folds_def) |
|
318 apply (rule someI2_ex, erule finite_imp_fold_graph) |
|
319 by (erule fold_graph.induct, auto) |
|
320 |
120 (* Just a technical lemma. *) |
321 (* Just a technical lemma. *) |
121 lemma [simp]: |
322 lemma [simp]: |
122 shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y" |
323 shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y" |
123 by simp |
324 by simp |
124 |
325 |
157 apply (clarsimp simp:finals_def str_eq_rel_def) |
358 apply (clarsimp simp:finals_def str_eq_rel_def) |
158 by (drule_tac x = "[]" in spec, auto) |
359 by (drule_tac x = "[]" in spec, auto) |
159 qed |
360 qed |
160 |
361 |
161 section {* Direction @{text "finite partition \<Rightarrow> regular language"}*} |
362 section {* Direction @{text "finite partition \<Rightarrow> regular language"}*} |
162 |
|
163 subsection {* |
|
164 Ardens lemma |
|
165 *} |
|
166 text {* Ardens lemma expressed at the level of language, rather than the level of regular expression. *} |
|
167 |
|
168 theorem ardens_revised: |
|
169 assumes nemp: "[] \<notin> A" |
|
170 shows "(X = X ;; A \<union> B) \<longleftrightarrow> (X = B ;; A\<star>)" |
|
171 proof |
|
172 assume eq: "X = B ;; A\<star>" |
|
173 have "A\<star> = {[]} \<union> A\<star> ;; A" |
|
174 by (auto simp:Seq_def star_intro3 star_decom') |
|
175 then have "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)" |
|
176 unfolding Seq_def by simp |
|
177 also have "\<dots> = B \<union> B ;; (A\<star> ;; A)" |
|
178 unfolding Seq_def by auto |
|
179 also have "\<dots> = B \<union> (B ;; A\<star>) ;; A" |
|
180 by (simp only:seq_assoc) |
|
181 finally show "X = X ;; A \<union> B" |
|
182 using eq by blast |
|
183 next |
|
184 assume eq': "X = X ;; A \<union> B" |
|
185 hence c1': "\<And> x. x \<in> B \<Longrightarrow> x \<in> X" |
|
186 and c2': "\<And> x y. \<lbrakk>x \<in> X; y \<in> A\<rbrakk> \<Longrightarrow> x @ y \<in> X" |
|
187 using Seq_def by auto |
|
188 show "X = B ;; A\<star>" |
|
189 proof |
|
190 show "B ;; A\<star> \<subseteq> X" |
|
191 proof- |
|
192 { fix x y |
|
193 have "\<lbrakk>y \<in> A\<star>; x \<in> X\<rbrakk> \<Longrightarrow> x @ y \<in> X " |
|
194 apply (induct arbitrary:x rule:Star.induct, simp) |
|
195 by (auto simp only:append_assoc[THEN sym] dest:c2') |
|
196 } thus ?thesis using c1' by (auto simp:Seq_def) |
|
197 qed |
|
198 next |
|
199 show "X \<subseteq> B ;; A\<star>" |
|
200 proof- |
|
201 { fix x |
|
202 have "x \<in> X \<Longrightarrow> x \<in> B ;; A\<star>" |
|
203 proof (induct x taking:length rule:measure_induct) |
|
204 fix z |
|
205 assume hyps: |
|
206 "\<forall>y. length y < length z \<longrightarrow> y \<in> X \<longrightarrow> y \<in> B ;; A\<star>" |
|
207 and z_in: "z \<in> X" |
|
208 show "z \<in> B ;; A\<star>" |
|
209 proof (cases "z \<in> B") |
|
210 case True thus ?thesis by (auto simp:Seq_def start) |
|
211 next |
|
212 case False hence "z \<in> X ;; A" using eq' z_in by auto |
|
213 then obtain za zb where za_in: "za \<in> X" |
|
214 and zab: "z = za @ zb \<and> zb \<in> A" and zbne: "zb \<noteq> []" |
|
215 using nemp unfolding Seq_def by blast |
|
216 from zbne zab have "length za < length z" by auto |
|
217 with za_in hyps have "za \<in> B ;; A\<star>" by blast |
|
218 hence "za @ zb \<in> B ;; A\<star>" using zab |
|
219 by (clarsimp simp:Seq_def, blast dest:star_intro3) |
|
220 thus ?thesis using zab by simp |
|
221 qed |
|
222 qed |
|
223 } thus ?thesis by blast |
|
224 qed |
|
225 qed |
|
226 qed |
|
227 |
|
228 subsection {* |
|
229 Defintions peculiar to this direction |
|
230 *} |
|
231 |
|
232 text {* |
|
233 To obtain equational system out of finite set of equivalent classes, a fold operation |
|
234 on finite set @{text "folds"} is defined. The use of @{text "SOME"} makes @{text "fold"} |
|
235 more robust than the @{text "fold"} in Isabelle library. The expression @{text "folds f"} |
|
236 makes sense when @{text "f"} is not @{text "associative"} and @{text "commutitive"}, |
|
237 while @{text "fold f"} does not. |
|
238 *} |
|
239 |
|
240 definition |
|
241 folds :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b" |
|
242 where |
|
243 "folds f z S \<equiv> SOME x. fold_graph f z S x" |
|
244 |
|
245 text {* |
|
246 The following lemma assures that the arbitrary choice made by the @{text "SOME"} in @{text "folds"} |
|
247 does not affect the @{text "L"}-value of the resultant regular expression. |
|
248 *} |
|
249 lemma folds_alt_simp [simp]: |
|
250 "finite rs \<Longrightarrow> L (folds ALT NULL rs) = \<Union> (L ` rs)" |
|
251 apply (rule set_eq_intro, simp add:folds_def) |
|
252 apply (rule someI2_ex, erule finite_imp_fold_graph) |
|
253 by (erule fold_graph.induct, auto) |
|
254 |
363 |
255 text {* |
364 text {* |
256 The relationship between equivalent classes can be described by an |
365 The relationship between equivalent classes can be described by an |
257 equational system. |
366 equational system. |
258 For example, in equational system \eqref{example_eqns}, $X_0, X_1$ are equivalent |
367 For example, in equational system \eqref{example_eqns}, $X_0, X_1$ are equivalent |