1 theory Myhill_1 |
|
2 imports Main Folds Regular |
|
3 "~~/src/HOL/Library/While_Combinator" |
|
4 begin |
|
5 |
|
6 section {* Direction @{text "finite partition \<Rightarrow> regular language"} *} |
|
7 |
|
8 lemma Pair_Collect[simp]: |
|
9 shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y" |
|
10 by simp |
|
11 |
|
12 text {* Myhill-Nerode relation *} |
|
13 |
|
14 definition |
|
15 str_eq_rel :: "lang \<Rightarrow> (string \<times> string) set" ("\<approx>_" [100] 100) |
|
16 where |
|
17 "\<approx>A \<equiv> {(x, y). (\<forall>z. x @ z \<in> A \<longleftrightarrow> y @ z \<in> A)}" |
|
18 |
|
19 definition |
|
20 finals :: "lang \<Rightarrow> lang set" |
|
21 where |
|
22 "finals A \<equiv> {\<approx>A `` {s} | s . s \<in> A}" |
|
23 |
|
24 lemma lang_is_union_of_finals: |
|
25 shows "A = \<Union> finals A" |
|
26 unfolding finals_def |
|
27 unfolding Image_def |
|
28 unfolding str_eq_rel_def |
|
29 by (auto) (metis append_Nil2) |
|
30 |
|
31 lemma finals_in_partitions: |
|
32 shows "finals A \<subseteq> (UNIV // \<approx>A)" |
|
33 unfolding finals_def quotient_def |
|
34 by auto |
|
35 |
|
36 section {* Equational systems *} |
|
37 |
|
38 text {* The two kinds of terms in the rhs of equations. *} |
|
39 |
|
40 datatype rhs_trm = |
|
41 Lam "rexp" (* Lambda-marker *) |
|
42 | Trn "lang" "rexp" (* Transition *) |
|
43 |
|
44 |
|
45 overloading L_rhs_trm \<equiv> "L:: rhs_trm \<Rightarrow> lang" |
|
46 begin |
|
47 fun L_rhs_trm:: "rhs_trm \<Rightarrow> lang" |
|
48 where |
|
49 "L_rhs_trm (Lam r) = L r" |
|
50 | "L_rhs_trm (Trn X r) = X ;; L r" |
|
51 end |
|
52 |
|
53 overloading L_rhs \<equiv> "L:: rhs_trm set \<Rightarrow> lang" |
|
54 begin |
|
55 fun L_rhs:: "rhs_trm set \<Rightarrow> lang" |
|
56 where |
|
57 "L_rhs rhs = \<Union> (L ` rhs)" |
|
58 end |
|
59 |
|
60 lemma L_rhs_set: |
|
61 shows "L {Trn X r | r. P r} = \<Union>{L (Trn X r) | r. P r}" |
|
62 by (auto simp del: L_rhs_trm.simps) |
|
63 |
|
64 lemma L_rhs_union_distrib: |
|
65 fixes A B::"rhs_trm set" |
|
66 shows "L A \<union> L B = L (A \<union> B)" |
|
67 by simp |
|
68 |
|
69 |
|
70 |
|
71 text {* Transitions between equivalence classes *} |
|
72 |
|
73 definition |
|
74 transition :: "lang \<Rightarrow> char \<Rightarrow> lang \<Rightarrow> bool" ("_ \<Turnstile>_\<Rightarrow>_" [100,100,100] 100) |
|
75 where |
|
76 "Y \<Turnstile>c\<Rightarrow> X \<equiv> Y ;; {[c]} \<subseteq> X" |
|
77 |
|
78 text {* Initial equational system *} |
|
79 |
|
80 definition |
|
81 "Init_rhs CS X \<equiv> |
|
82 if ([] \<in> X) then |
|
83 {Lam EMPTY} \<union> {Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X} |
|
84 else |
|
85 {Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}" |
|
86 |
|
87 definition |
|
88 "Init CS \<equiv> {(X, Init_rhs CS X) | X. X \<in> CS}" |
|
89 |
|
90 |
|
91 section {* Arden Operation on equations *} |
|
92 |
|
93 fun |
|
94 Append_rexp :: "rexp \<Rightarrow> rhs_trm \<Rightarrow> rhs_trm" |
|
95 where |
|
96 "Append_rexp r (Lam rexp) = Lam (SEQ rexp r)" |
|
97 | "Append_rexp r (Trn X rexp) = Trn X (SEQ rexp r)" |
|
98 |
|
99 |
|
100 definition |
|
101 "Append_rexp_rhs rhs rexp \<equiv> (Append_rexp rexp) ` rhs" |
|
102 |
|
103 definition |
|
104 "Arden X rhs \<equiv> |
|
105 Append_rexp_rhs (rhs - {Trn X r | r. Trn X r \<in> rhs}) (STAR (\<Uplus> {r. Trn X r \<in> rhs}))" |
|
106 |
|
107 |
|
108 section {* Substitution Operation on equations *} |
|
109 |
|
110 definition |
|
111 "Subst rhs X xrhs \<equiv> |
|
112 (rhs - {Trn X r | r. Trn X r \<in> rhs}) \<union> (Append_rexp_rhs xrhs (\<Uplus> {r. Trn X r \<in> rhs}))" |
|
113 |
|
114 definition |
|
115 Subst_all :: "(lang \<times> rhs_trm set) set \<Rightarrow> lang \<Rightarrow> rhs_trm set \<Rightarrow> (lang \<times> rhs_trm set) set" |
|
116 where |
|
117 "Subst_all ES X xrhs \<equiv> {(Y, Subst yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}" |
|
118 |
|
119 definition |
|
120 "Remove ES X xrhs \<equiv> |
|
121 Subst_all (ES - {(X, xrhs)}) X (Arden X xrhs)" |
|
122 |
|
123 |
|
124 section {* While-combinator *} |
|
125 |
|
126 definition |
|
127 "Iter X ES \<equiv> (let (Y, yrhs) = SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> X \<noteq> Y |
|
128 in Remove ES Y yrhs)" |
|
129 |
|
130 lemma IterI2: |
|
131 assumes "(Y, yrhs) \<in> ES" |
|
132 and "X \<noteq> Y" |
|
133 and "\<And>Y yrhs. \<lbrakk>(Y, yrhs) \<in> ES; X \<noteq> Y\<rbrakk> \<Longrightarrow> Q (Remove ES Y yrhs)" |
|
134 shows "Q (Iter X ES)" |
|
135 unfolding Iter_def using assms |
|
136 by (rule_tac a="(Y, yrhs)" in someI2) (auto) |
|
137 |
|
138 abbreviation |
|
139 "Cond ES \<equiv> card ES \<noteq> 1" |
|
140 |
|
141 definition |
|
142 "Solve X ES \<equiv> while Cond (Iter X) ES" |
|
143 |
|
144 |
|
145 section {* Invariants *} |
|
146 |
|
147 definition |
|
148 "distinctness ES \<equiv> |
|
149 \<forall> X rhs rhs'. (X, rhs) \<in> ES \<and> (X, rhs') \<in> ES \<longrightarrow> rhs = rhs'" |
|
150 |
|
151 definition |
|
152 "soundness ES \<equiv> \<forall>(X, rhs) \<in> ES. X = L rhs" |
|
153 |
|
154 definition |
|
155 "ardenable rhs \<equiv> (\<forall> Y r. Trn Y r \<in> rhs \<longrightarrow> [] \<notin> L r)" |
|
156 |
|
157 definition |
|
158 "ardenable_all ES \<equiv> \<forall>(X, rhs) \<in> ES. ardenable rhs" |
|
159 |
|
160 definition |
|
161 "finite_rhs ES \<equiv> \<forall>(X, rhs) \<in> ES. finite rhs" |
|
162 |
|
163 lemma finite_rhs_def2: |
|
164 "finite_rhs ES = (\<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> finite rhs)" |
|
165 unfolding finite_rhs_def by auto |
|
166 |
|
167 definition |
|
168 "rhss rhs \<equiv> {X | X r. Trn X r \<in> rhs}" |
|
169 |
|
170 definition |
|
171 "lhss ES \<equiv> {Y | Y yrhs. (Y, yrhs) \<in> ES}" |
|
172 |
|
173 definition |
|
174 "validity ES \<equiv> \<forall>(X, rhs) \<in> ES. rhss rhs \<subseteq> lhss ES" |
|
175 |
|
176 lemma rhss_union_distrib: |
|
177 shows "rhss (A \<union> B) = rhss A \<union> rhss B" |
|
178 by (auto simp add: rhss_def) |
|
179 |
|
180 lemma lhss_union_distrib: |
|
181 shows "lhss (A \<union> B) = lhss A \<union> lhss B" |
|
182 by (auto simp add: lhss_def) |
|
183 |
|
184 |
|
185 definition |
|
186 "invariant ES \<equiv> finite ES |
|
187 \<and> finite_rhs ES |
|
188 \<and> soundness ES |
|
189 \<and> distinctness ES |
|
190 \<and> ardenable_all ES |
|
191 \<and> validity ES" |
|
192 |
|
193 |
|
194 lemma invariantI: |
|
195 assumes "soundness ES" "finite ES" "distinctness ES" "ardenable_all ES" |
|
196 "finite_rhs ES" "validity ES" |
|
197 shows "invariant ES" |
|
198 using assms by (simp add: invariant_def) |
|
199 |
|
200 |
|
201 subsection {* The proof of this direction *} |
|
202 |
|
203 lemma finite_Trn: |
|
204 assumes fin: "finite rhs" |
|
205 shows "finite {r. Trn Y r \<in> rhs}" |
|
206 proof - |
|
207 have "finite {Trn Y r | Y r. Trn Y r \<in> rhs}" |
|
208 by (rule rev_finite_subset[OF fin]) (auto) |
|
209 then have "finite ((\<lambda>(Y, r). Trn Y r) ` {(Y, r) | Y r. Trn Y r \<in> rhs})" |
|
210 by (simp add: image_Collect) |
|
211 then have "finite {(Y, r) | Y r. Trn Y r \<in> rhs}" |
|
212 by (erule_tac finite_imageD) (simp add: inj_on_def) |
|
213 then show "finite {r. Trn Y r \<in> rhs}" |
|
214 by (erule_tac f="snd" in finite_surj) (auto simp add: image_def) |
|
215 qed |
|
216 |
|
217 lemma finite_Lam: |
|
218 assumes fin: "finite rhs" |
|
219 shows "finite {r. Lam r \<in> rhs}" |
|
220 proof - |
|
221 have "finite {Lam r | r. Lam r \<in> rhs}" |
|
222 by (rule rev_finite_subset[OF fin]) (auto) |
|
223 then show "finite {r. Lam r \<in> rhs}" |
|
224 apply(simp add: image_Collect[symmetric]) |
|
225 apply(erule finite_imageD) |
|
226 apply(auto simp add: inj_on_def) |
|
227 done |
|
228 qed |
|
229 |
|
230 lemma rhs_trm_soundness: |
|
231 assumes finite:"finite rhs" |
|
232 shows "L ({Trn X r| r. Trn X r \<in> rhs}) = X ;; (L (\<Uplus>{r. Trn X r \<in> rhs}))" |
|
233 proof - |
|
234 have "finite {r. Trn X r \<in> rhs}" |
|
235 by (rule finite_Trn[OF finite]) |
|
236 then show "L ({Trn X r| r. Trn X r \<in> rhs}) = X ;; (L (\<Uplus>{r. Trn X r \<in> rhs}))" |
|
237 by (simp only: L_rhs_set L_rhs_trm.simps) (auto simp add: Seq_def) |
|
238 qed |
|
239 |
|
240 lemma lang_of_append_rexp: |
|
241 "L (Append_rexp r rhs_trm) = L rhs_trm ;; L r" |
|
242 by (induct rule: Append_rexp.induct) |
|
243 (auto simp add: seq_assoc) |
|
244 |
|
245 lemma lang_of_append_rexp_rhs: |
|
246 "L (Append_rexp_rhs rhs r) = L rhs ;; L r" |
|
247 unfolding Append_rexp_rhs_def |
|
248 by (auto simp add: Seq_def lang_of_append_rexp) |
|
249 |
|
250 |
|
251 |
|
252 subsubsection {* Intialization *} |
|
253 |
|
254 lemma defined_by_str: |
|
255 assumes "s \<in> X" "X \<in> UNIV // \<approx>A" |
|
256 shows "X = \<approx>A `` {s}" |
|
257 using assms |
|
258 unfolding quotient_def Image_def str_eq_rel_def |
|
259 by auto |
|
260 |
|
261 lemma every_eqclass_has_transition: |
|
262 assumes has_str: "s @ [c] \<in> X" |
|
263 and in_CS: "X \<in> UNIV // \<approx>A" |
|
264 obtains Y where "Y \<in> UNIV // \<approx>A" and "Y ;; {[c]} \<subseteq> X" and "s \<in> Y" |
|
265 proof - |
|
266 def Y \<equiv> "\<approx>A `` {s}" |
|
267 have "Y \<in> UNIV // \<approx>A" |
|
268 unfolding Y_def quotient_def by auto |
|
269 moreover |
|
270 have "X = \<approx>A `` {s @ [c]}" |
|
271 using has_str in_CS defined_by_str by blast |
|
272 then have "Y ;; {[c]} \<subseteq> X" |
|
273 unfolding Y_def Image_def Seq_def |
|
274 unfolding str_eq_rel_def |
|
275 by clarsimp |
|
276 moreover |
|
277 have "s \<in> Y" unfolding Y_def |
|
278 unfolding Image_def str_eq_rel_def by simp |
|
279 ultimately show thesis using that by blast |
|
280 qed |
|
281 |
|
282 lemma l_eq_r_in_eqs: |
|
283 assumes X_in_eqs: "(X, rhs) \<in> Init (UNIV // \<approx>A)" |
|
284 shows "X = L rhs" |
|
285 proof |
|
286 show "X \<subseteq> L rhs" |
|
287 proof |
|
288 fix x |
|
289 assume in_X: "x \<in> X" |
|
290 { assume empty: "x = []" |
|
291 then have "x \<in> L rhs" using X_in_eqs in_X |
|
292 unfolding Init_def Init_rhs_def |
|
293 by auto |
|
294 } |
|
295 moreover |
|
296 { assume not_empty: "x \<noteq> []" |
|
297 then obtain s c where decom: "x = s @ [c]" |
|
298 using rev_cases by blast |
|
299 have "X \<in> UNIV // \<approx>A" using X_in_eqs unfolding Init_def by auto |
|
300 then obtain Y where "Y \<in> UNIV // \<approx>A" "Y ;; {[c]} \<subseteq> X" "s \<in> Y" |
|
301 using decom in_X every_eqclass_has_transition by blast |
|
302 then have "x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // \<approx>A \<and> Y \<Turnstile>c\<Rightarrow> X}" |
|
303 unfolding transition_def |
|
304 using decom by (force simp add: Seq_def) |
|
305 then have "x \<in> L rhs" using X_in_eqs in_X |
|
306 unfolding Init_def Init_rhs_def by simp |
|
307 } |
|
308 ultimately show "x \<in> L rhs" by blast |
|
309 qed |
|
310 next |
|
311 show "L rhs \<subseteq> X" using X_in_eqs |
|
312 unfolding Init_def Init_rhs_def transition_def |
|
313 by auto |
|
314 qed |
|
315 |
|
316 lemma test: |
|
317 assumes X_in_eqs: "(X, rhs) \<in> Init (UNIV // \<approx>A)" |
|
318 shows "X = \<Union> (L ` rhs)" |
|
319 using assms l_eq_r_in_eqs by (simp) |
|
320 |
|
321 lemma finite_Init_rhs: |
|
322 assumes finite: "finite CS" |
|
323 shows "finite (Init_rhs CS X)" |
|
324 proof- |
|
325 def S \<equiv> "{(Y, c)| Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}" |
|
326 def h \<equiv> "\<lambda> (Y, c). Trn Y (CHAR c)" |
|
327 have "finite (CS \<times> (UNIV::char set))" using finite by auto |
|
328 then have "finite S" using S_def |
|
329 by (rule_tac B = "CS \<times> UNIV" in finite_subset) (auto) |
|
330 moreover have "{Trn Y (CHAR c) |Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X} = h ` S" |
|
331 unfolding S_def h_def image_def by auto |
|
332 ultimately |
|
333 have "finite {Trn Y (CHAR c) |Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}" by auto |
|
334 then show "finite (Init_rhs CS X)" unfolding Init_rhs_def transition_def by simp |
|
335 qed |
|
336 |
|
337 lemma Init_ES_satisfies_invariant: |
|
338 assumes finite_CS: "finite (UNIV // \<approx>A)" |
|
339 shows "invariant (Init (UNIV // \<approx>A))" |
|
340 proof (rule invariantI) |
|
341 show "soundness (Init (UNIV // \<approx>A))" |
|
342 unfolding soundness_def |
|
343 using l_eq_r_in_eqs by auto |
|
344 show "finite (Init (UNIV // \<approx>A))" using finite_CS |
|
345 unfolding Init_def by simp |
|
346 show "distinctness (Init (UNIV // \<approx>A))" |
|
347 unfolding distinctness_def Init_def by simp |
|
348 show "ardenable_all (Init (UNIV // \<approx>A))" |
|
349 unfolding ardenable_all_def Init_def Init_rhs_def ardenable_def |
|
350 by auto |
|
351 show "finite_rhs (Init (UNIV // \<approx>A))" |
|
352 using finite_Init_rhs[OF finite_CS] |
|
353 unfolding finite_rhs_def Init_def by auto |
|
354 show "validity (Init (UNIV // \<approx>A))" |
|
355 unfolding validity_def Init_def Init_rhs_def rhss_def lhss_def |
|
356 by auto |
|
357 qed |
|
358 |
|
359 subsubsection {* Interation step *} |
|
360 |
|
361 lemma Arden_keeps_eq: |
|
362 assumes l_eq_r: "X = L rhs" |
|
363 and not_empty: "ardenable rhs" |
|
364 and finite: "finite rhs" |
|
365 shows "X = L (Arden X rhs)" |
|
366 proof - |
|
367 def A \<equiv> "L (\<Uplus>{r. Trn X r \<in> rhs})" |
|
368 def b \<equiv> "{Trn X r | r. Trn X r \<in> rhs}" |
|
369 def B \<equiv> "L (rhs - b)" |
|
370 have not_empty2: "[] \<notin> A" |
|
371 using finite_Trn[OF finite] not_empty |
|
372 unfolding A_def ardenable_def by simp |
|
373 have "X = L rhs" using l_eq_r by simp |
|
374 also have "\<dots> = L (b \<union> (rhs - b))" unfolding b_def by auto |
|
375 also have "\<dots> = L b \<union> B" unfolding B_def by (simp only: L_rhs_union_distrib) |
|
376 also have "\<dots> = X ;; A \<union> B" |
|
377 unfolding b_def |
|
378 unfolding rhs_trm_soundness[OF finite] |
|
379 unfolding A_def |
|
380 by blast |
|
381 finally have "X = X ;; A \<union> B" . |
|
382 then have "X = B ;; A\<star>" |
|
383 by (simp add: arden[OF not_empty2]) |
|
384 also have "\<dots> = L (Arden X rhs)" |
|
385 unfolding Arden_def A_def B_def b_def |
|
386 by (simp only: lang_of_append_rexp_rhs L_rexp.simps) |
|
387 finally show "X = L (Arden X rhs)" by simp |
|
388 qed |
|
389 |
|
390 lemma Append_keeps_finite: |
|
391 "finite rhs \<Longrightarrow> finite (Append_rexp_rhs rhs r)" |
|
392 by (auto simp:Append_rexp_rhs_def) |
|
393 |
|
394 lemma Arden_keeps_finite: |
|
395 "finite rhs \<Longrightarrow> finite (Arden X rhs)" |
|
396 by (auto simp:Arden_def Append_keeps_finite) |
|
397 |
|
398 lemma Append_keeps_nonempty: |
|
399 "ardenable rhs \<Longrightarrow> ardenable (Append_rexp_rhs rhs r)" |
|
400 apply (auto simp:ardenable_def Append_rexp_rhs_def) |
|
401 by (case_tac x, auto simp:Seq_def) |
|
402 |
|
403 lemma nonempty_set_sub: |
|
404 "ardenable rhs \<Longrightarrow> ardenable (rhs - A)" |
|
405 by (auto simp:ardenable_def) |
|
406 |
|
407 lemma nonempty_set_union: |
|
408 "\<lbrakk>ardenable rhs; ardenable rhs'\<rbrakk> \<Longrightarrow> ardenable (rhs \<union> rhs')" |
|
409 by (auto simp:ardenable_def) |
|
410 |
|
411 lemma Arden_keeps_nonempty: |
|
412 "ardenable rhs \<Longrightarrow> ardenable (Arden X rhs)" |
|
413 by (simp only:Arden_def Append_keeps_nonempty nonempty_set_sub) |
|
414 |
|
415 |
|
416 lemma Subst_keeps_nonempty: |
|
417 "\<lbrakk>ardenable rhs; ardenable xrhs\<rbrakk> \<Longrightarrow> ardenable (Subst rhs X xrhs)" |
|
418 by (simp only: Subst_def Append_keeps_nonempty nonempty_set_union nonempty_set_sub) |
|
419 |
|
420 lemma Subst_keeps_eq: |
|
421 assumes substor: "X = L xrhs" |
|
422 and finite: "finite rhs" |
|
423 shows "L (Subst rhs X xrhs) = L rhs" (is "?Left = ?Right") |
|
424 proof- |
|
425 def A \<equiv> "L (rhs - {Trn X r | r. Trn X r \<in> rhs})" |
|
426 have "?Left = A \<union> L (Append_rexp_rhs xrhs (\<Uplus>{r. Trn X r \<in> rhs}))" |
|
427 unfolding Subst_def |
|
428 unfolding L_rhs_union_distrib[symmetric] |
|
429 by (simp add: A_def) |
|
430 moreover have "?Right = A \<union> L ({Trn X r | r. Trn X r \<in> rhs})" |
|
431 proof- |
|
432 have "rhs = (rhs - {Trn X r | r. Trn X r \<in> rhs}) \<union> ({Trn X r | r. Trn X r \<in> rhs})" by auto |
|
433 thus ?thesis |
|
434 unfolding A_def |
|
435 unfolding L_rhs_union_distrib |
|
436 by simp |
|
437 qed |
|
438 moreover have "L (Append_rexp_rhs xrhs (\<Uplus>{r. Trn X r \<in> rhs})) = L ({Trn X r | r. Trn X r \<in> rhs})" |
|
439 using finite substor by (simp only: lang_of_append_rexp_rhs rhs_trm_soundness) |
|
440 ultimately show ?thesis by simp |
|
441 qed |
|
442 |
|
443 lemma Subst_keeps_finite_rhs: |
|
444 "\<lbrakk>finite rhs; finite yrhs\<rbrakk> \<Longrightarrow> finite (Subst rhs Y yrhs)" |
|
445 by (auto simp: Subst_def Append_keeps_finite) |
|
446 |
|
447 lemma Subst_all_keeps_finite: |
|
448 assumes finite: "finite ES" |
|
449 shows "finite (Subst_all ES Y yrhs)" |
|
450 proof - |
|
451 def eqns \<equiv> "{(X::lang, rhs) |X rhs. (X, rhs) \<in> ES}" |
|
452 def h \<equiv> "\<lambda>(X::lang, rhs). (X, Subst rhs Y yrhs)" |
|
453 have "finite (h ` eqns)" using finite h_def eqns_def by auto |
|
454 moreover |
|
455 have "Subst_all ES Y yrhs = h ` eqns" unfolding h_def eqns_def Subst_all_def by auto |
|
456 ultimately |
|
457 show "finite (Subst_all ES Y yrhs)" by simp |
|
458 qed |
|
459 |
|
460 lemma Subst_all_keeps_finite_rhs: |
|
461 "\<lbrakk>finite_rhs ES; finite yrhs\<rbrakk> \<Longrightarrow> finite_rhs (Subst_all ES Y yrhs)" |
|
462 by (auto intro:Subst_keeps_finite_rhs simp add:Subst_all_def finite_rhs_def) |
|
463 |
|
464 lemma append_rhs_keeps_cls: |
|
465 "rhss (Append_rexp_rhs rhs r) = rhss rhs" |
|
466 apply (auto simp:rhss_def Append_rexp_rhs_def) |
|
467 apply (case_tac xa, auto simp:image_def) |
|
468 by (rule_tac x = "SEQ ra r" in exI, rule_tac x = "Trn x ra" in bexI, simp+) |
|
469 |
|
470 lemma Arden_removes_cl: |
|
471 "rhss (Arden Y yrhs) = rhss yrhs - {Y}" |
|
472 apply (simp add:Arden_def append_rhs_keeps_cls) |
|
473 by (auto simp:rhss_def) |
|
474 |
|
475 lemma lhss_keeps_cls: |
|
476 "lhss (Subst_all ES Y yrhs) = lhss ES" |
|
477 by (auto simp:lhss_def Subst_all_def) |
|
478 |
|
479 lemma Subst_updates_cls: |
|
480 "X \<notin> rhss xrhs \<Longrightarrow> |
|
481 rhss (Subst rhs X xrhs) = rhss rhs \<union> rhss xrhs - {X}" |
|
482 apply (simp only:Subst_def append_rhs_keeps_cls rhss_union_distrib) |
|
483 by (auto simp:rhss_def) |
|
484 |
|
485 lemma Subst_all_keeps_validity: |
|
486 assumes sc: "validity (ES \<union> {(Y, yrhs)})" (is "validity ?A") |
|
487 shows "validity (Subst_all ES Y (Arden Y yrhs))" (is "validity ?B") |
|
488 proof - |
|
489 { fix X xrhs' |
|
490 assume "(X, xrhs') \<in> ?B" |
|
491 then obtain xrhs |
|
492 where xrhs_xrhs': "xrhs' = Subst xrhs Y (Arden Y yrhs)" |
|
493 and X_in: "(X, xrhs) \<in> ES" by (simp add:Subst_all_def, blast) |
|
494 have "rhss xrhs' \<subseteq> lhss ?B" |
|
495 proof- |
|
496 have "lhss ?B = lhss ES" by (auto simp add:lhss_def Subst_all_def) |
|
497 moreover have "rhss xrhs' \<subseteq> lhss ES" |
|
498 proof- |
|
499 have "rhss xrhs' \<subseteq> rhss xrhs \<union> rhss (Arden Y yrhs) - {Y}" |
|
500 proof- |
|
501 have "Y \<notin> rhss (Arden Y yrhs)" |
|
502 using Arden_removes_cl by simp |
|
503 thus ?thesis using xrhs_xrhs' by (auto simp:Subst_updates_cls) |
|
504 qed |
|
505 moreover have "rhss xrhs \<subseteq> lhss ES \<union> {Y}" using X_in sc |
|
506 apply (simp only:validity_def lhss_union_distrib) |
|
507 by (drule_tac x = "(X, xrhs)" in bspec, auto simp:lhss_def) |
|
508 moreover have "rhss (Arden Y yrhs) \<subseteq> lhss ES \<union> {Y}" |
|
509 using sc |
|
510 by (auto simp add:Arden_removes_cl validity_def lhss_def) |
|
511 ultimately show ?thesis by auto |
|
512 qed |
|
513 ultimately show ?thesis by simp |
|
514 qed |
|
515 } thus ?thesis by (auto simp only:Subst_all_def validity_def) |
|
516 qed |
|
517 |
|
518 lemma Subst_all_satisfies_invariant: |
|
519 assumes invariant_ES: "invariant (ES \<union> {(Y, yrhs)})" |
|
520 shows "invariant (Subst_all ES Y (Arden Y yrhs))" |
|
521 proof (rule invariantI) |
|
522 have Y_eq_yrhs: "Y = L yrhs" |
|
523 using invariant_ES by (simp only:invariant_def soundness_def, blast) |
|
524 have finite_yrhs: "finite yrhs" |
|
525 using invariant_ES by (auto simp:invariant_def finite_rhs_def) |
|
526 have nonempty_yrhs: "ardenable yrhs" |
|
527 using invariant_ES by (auto simp:invariant_def ardenable_all_def) |
|
528 show "soundness (Subst_all ES Y (Arden Y yrhs))" |
|
529 proof - |
|
530 have "Y = L (Arden Y yrhs)" |
|
531 using Y_eq_yrhs invariant_ES finite_yrhs |
|
532 using finite_Trn[OF finite_yrhs] |
|
533 apply(rule_tac Arden_keeps_eq) |
|
534 apply(simp_all) |
|
535 unfolding invariant_def ardenable_all_def ardenable_def |
|
536 apply(auto) |
|
537 done |
|
538 thus ?thesis using invariant_ES |
|
539 unfolding invariant_def finite_rhs_def2 soundness_def Subst_all_def |
|
540 by (auto simp add: Subst_keeps_eq simp del: L_rhs.simps) |
|
541 qed |
|
542 show "finite (Subst_all ES Y (Arden Y yrhs))" |
|
543 using invariant_ES by (simp add:invariant_def Subst_all_keeps_finite) |
|
544 show "distinctness (Subst_all ES Y (Arden Y yrhs))" |
|
545 using invariant_ES |
|
546 unfolding distinctness_def Subst_all_def invariant_def by auto |
|
547 show "ardenable_all (Subst_all ES Y (Arden Y yrhs))" |
|
548 proof - |
|
549 { fix X rhs |
|
550 assume "(X, rhs) \<in> ES" |
|
551 hence "ardenable rhs" using invariant_ES |
|
552 by (auto simp add:invariant_def ardenable_all_def) |
|
553 with nonempty_yrhs |
|
554 have "ardenable (Subst rhs Y (Arden Y yrhs))" |
|
555 by (simp add:nonempty_yrhs |
|
556 Subst_keeps_nonempty Arden_keeps_nonempty) |
|
557 } thus ?thesis by (auto simp add:ardenable_all_def Subst_all_def) |
|
558 qed |
|
559 show "finite_rhs (Subst_all ES Y (Arden Y yrhs))" |
|
560 proof- |
|
561 have "finite_rhs ES" using invariant_ES |
|
562 by (simp add:invariant_def finite_rhs_def) |
|
563 moreover have "finite (Arden Y yrhs)" |
|
564 proof - |
|
565 have "finite yrhs" using invariant_ES |
|
566 by (auto simp:invariant_def finite_rhs_def) |
|
567 thus ?thesis using Arden_keeps_finite by simp |
|
568 qed |
|
569 ultimately show ?thesis |
|
570 by (simp add:Subst_all_keeps_finite_rhs) |
|
571 qed |
|
572 show "validity (Subst_all ES Y (Arden Y yrhs))" |
|
573 using invariant_ES Subst_all_keeps_validity by (simp add:invariant_def) |
|
574 qed |
|
575 |
|
576 lemma Remove_in_card_measure: |
|
577 assumes finite: "finite ES" |
|
578 and in_ES: "(X, rhs) \<in> ES" |
|
579 shows "(Remove ES X rhs, ES) \<in> measure card" |
|
580 proof - |
|
581 def f \<equiv> "\<lambda> x. ((fst x)::lang, Subst (snd x) X (Arden X rhs))" |
|
582 def ES' \<equiv> "ES - {(X, rhs)}" |
|
583 have "Subst_all ES' X (Arden X rhs) = f ` ES'" |
|
584 apply (auto simp: Subst_all_def f_def image_def) |
|
585 by (rule_tac x = "(Y, yrhs)" in bexI, simp+) |
|
586 then have "card (Subst_all ES' X (Arden X rhs)) \<le> card ES'" |
|
587 unfolding ES'_def using finite by (auto intro: card_image_le) |
|
588 also have "\<dots> < card ES" unfolding ES'_def |
|
589 using in_ES finite by (rule_tac card_Diff1_less) |
|
590 finally show "(Remove ES X rhs, ES) \<in> measure card" |
|
591 unfolding Remove_def ES'_def by simp |
|
592 qed |
|
593 |
|
594 |
|
595 lemma Subst_all_cls_remains: |
|
596 "(X, xrhs) \<in> ES \<Longrightarrow> \<exists> xrhs'. (X, xrhs') \<in> (Subst_all ES Y yrhs)" |
|
597 by (auto simp: Subst_all_def) |
|
598 |
|
599 lemma card_noteq_1_has_more: |
|
600 assumes card:"Cond ES" |
|
601 and e_in: "(X, xrhs) \<in> ES" |
|
602 and finite: "finite ES" |
|
603 shows "\<exists>(Y, yrhs) \<in> ES. (X, xrhs) \<noteq> (Y, yrhs)" |
|
604 proof- |
|
605 have "card ES > 1" using card e_in finite |
|
606 by (cases "card ES") (auto) |
|
607 then have "card (ES - {(X, xrhs)}) > 0" |
|
608 using finite e_in by auto |
|
609 then have "(ES - {(X, xrhs)}) \<noteq> {}" using finite by (rule_tac notI, simp) |
|
610 then show "\<exists>(Y, yrhs) \<in> ES. (X, xrhs) \<noteq> (Y, yrhs)" |
|
611 by auto |
|
612 qed |
|
613 |
|
614 lemma iteration_step_measure: |
|
615 assumes Inv_ES: "invariant ES" |
|
616 and X_in_ES: "(X, xrhs) \<in> ES" |
|
617 and Cnd: "Cond ES " |
|
618 shows "(Iter X ES, ES) \<in> measure card" |
|
619 proof - |
|
620 have fin: "finite ES" using Inv_ES unfolding invariant_def by simp |
|
621 then obtain Y yrhs |
|
622 where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" |
|
623 using Cnd X_in_ES by (drule_tac card_noteq_1_has_more) (auto) |
|
624 then have "(Y, yrhs) \<in> ES " "X \<noteq> Y" |
|
625 using X_in_ES Inv_ES unfolding invariant_def distinctness_def |
|
626 by auto |
|
627 then show "(Iter X ES, ES) \<in> measure card" |
|
628 apply(rule IterI2) |
|
629 apply(rule Remove_in_card_measure) |
|
630 apply(simp_all add: fin) |
|
631 done |
|
632 qed |
|
633 |
|
634 lemma iteration_step_invariant: |
|
635 assumes Inv_ES: "invariant ES" |
|
636 and X_in_ES: "(X, xrhs) \<in> ES" |
|
637 and Cnd: "Cond ES" |
|
638 shows "invariant (Iter X ES)" |
|
639 proof - |
|
640 have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def) |
|
641 then obtain Y yrhs |
|
642 where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" |
|
643 using Cnd X_in_ES by (drule_tac card_noteq_1_has_more) (auto) |
|
644 then have "(Y, yrhs) \<in> ES" "X \<noteq> Y" |
|
645 using X_in_ES Inv_ES unfolding invariant_def distinctness_def |
|
646 by auto |
|
647 then show "invariant (Iter X ES)" |
|
648 proof(rule IterI2) |
|
649 fix Y yrhs |
|
650 assume h: "(Y, yrhs) \<in> ES" "X \<noteq> Y" |
|
651 then have "ES - {(Y, yrhs)} \<union> {(Y, yrhs)} = ES" by auto |
|
652 then show "invariant (Remove ES Y yrhs)" unfolding Remove_def |
|
653 using Inv_ES |
|
654 by (rule_tac Subst_all_satisfies_invariant) (simp) |
|
655 qed |
|
656 qed |
|
657 |
|
658 lemma iteration_step_ex: |
|
659 assumes Inv_ES: "invariant ES" |
|
660 and X_in_ES: "(X, xrhs) \<in> ES" |
|
661 and Cnd: "Cond ES" |
|
662 shows "\<exists>xrhs'. (X, xrhs') \<in> (Iter X ES)" |
|
663 proof - |
|
664 have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def) |
|
665 then obtain Y yrhs |
|
666 where "(Y, yrhs) \<in> ES" "(X, xrhs) \<noteq> (Y, yrhs)" |
|
667 using Cnd X_in_ES by (drule_tac card_noteq_1_has_more) (auto) |
|
668 then have "(Y, yrhs) \<in> ES " "X \<noteq> Y" |
|
669 using X_in_ES Inv_ES unfolding invariant_def distinctness_def |
|
670 by auto |
|
671 then show "\<exists>xrhs'. (X, xrhs') \<in> (Iter X ES)" |
|
672 apply(rule IterI2) |
|
673 unfolding Remove_def |
|
674 apply(rule Subst_all_cls_remains) |
|
675 using X_in_ES |
|
676 apply(auto) |
|
677 done |
|
678 qed |
|
679 |
|
680 |
|
681 subsubsection {* Conclusion of the proof *} |
|
682 |
|
683 lemma Solve: |
|
684 assumes fin: "finite (UNIV // \<approx>A)" |
|
685 and X_in: "X \<in> (UNIV // \<approx>A)" |
|
686 shows "\<exists>rhs. Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)} \<and> invariant {(X, rhs)}" |
|
687 proof - |
|
688 def Inv \<equiv> "\<lambda>ES. invariant ES \<and> (\<exists>rhs. (X, rhs) \<in> ES)" |
|
689 have "Inv (Init (UNIV // \<approx>A))" unfolding Inv_def |
|
690 using fin X_in by (simp add: Init_ES_satisfies_invariant, simp add: Init_def) |
|
691 moreover |
|
692 { fix ES |
|
693 assume inv: "Inv ES" and crd: "Cond ES" |
|
694 then have "Inv (Iter X ES)" |
|
695 unfolding Inv_def |
|
696 by (auto simp add: iteration_step_invariant iteration_step_ex) } |
|
697 moreover |
|
698 { fix ES |
|
699 assume inv: "Inv ES" and not_crd: "\<not>Cond ES" |
|
700 from inv obtain rhs where "(X, rhs) \<in> ES" unfolding Inv_def by auto |
|
701 moreover |
|
702 from not_crd have "card ES = 1" by simp |
|
703 ultimately |
|
704 have "ES = {(X, rhs)}" by (auto simp add: card_Suc_eq) |
|
705 then have "\<exists>rhs'. ES = {(X, rhs')} \<and> invariant {(X, rhs')}" using inv |
|
706 unfolding Inv_def by auto } |
|
707 moreover |
|
708 have "wf (measure card)" by simp |
|
709 moreover |
|
710 { fix ES |
|
711 assume inv: "Inv ES" and crd: "Cond ES" |
|
712 then have "(Iter X ES, ES) \<in> measure card" |
|
713 unfolding Inv_def |
|
714 apply(clarify) |
|
715 apply(rule_tac iteration_step_measure) |
|
716 apply(auto) |
|
717 done } |
|
718 ultimately |
|
719 show "\<exists>rhs. Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)} \<and> invariant {(X, rhs)}" |
|
720 unfolding Solve_def by (rule while_rule) |
|
721 qed |
|
722 |
|
723 lemma every_eqcl_has_reg: |
|
724 assumes finite_CS: "finite (UNIV // \<approx>A)" |
|
725 and X_in_CS: "X \<in> (UNIV // \<approx>A)" |
|
726 shows "\<exists>r::rexp. X = L r" |
|
727 proof - |
|
728 from finite_CS X_in_CS |
|
729 obtain xrhs where Inv_ES: "invariant {(X, xrhs)}" |
|
730 using Solve by metis |
|
731 |
|
732 def A \<equiv> "Arden X xrhs" |
|
733 have "rhss xrhs \<subseteq> {X}" using Inv_ES |
|
734 unfolding validity_def invariant_def rhss_def lhss_def |
|
735 by auto |
|
736 then have "rhss A = {}" unfolding A_def |
|
737 by (simp add: Arden_removes_cl) |
|
738 then have eq: "{Lam r | r. Lam r \<in> A} = A" unfolding rhss_def |
|
739 by (auto, case_tac x, auto) |
|
740 |
|
741 have "finite A" using Inv_ES unfolding A_def invariant_def finite_rhs_def |
|
742 using Arden_keeps_finite by auto |
|
743 then have fin: "finite {r. Lam r \<in> A}" by (rule finite_Lam) |
|
744 |
|
745 have "X = L xrhs" using Inv_ES unfolding invariant_def soundness_def |
|
746 by simp |
|
747 then have "X = L A" using Inv_ES |
|
748 unfolding A_def invariant_def ardenable_all_def finite_rhs_def |
|
749 by (rule_tac Arden_keeps_eq) (simp_all add: finite_Trn) |
|
750 then have "X = L {Lam r | r. Lam r \<in> A}" using eq by simp |
|
751 then have "X = L (\<Uplus>{r. Lam r \<in> A})" using fin by auto |
|
752 then show "\<exists>r::rexp. X = L r" by blast |
|
753 qed |
|
754 |
|
755 lemma bchoice_finite_set: |
|
756 assumes a: "\<forall>x \<in> S. \<exists>y. x = f y" |
|
757 and b: "finite S" |
|
758 shows "\<exists>ys. (\<Union> S) = \<Union>(f ` ys) \<and> finite ys" |
|
759 using bchoice[OF a] b |
|
760 apply(erule_tac exE) |
|
761 apply(rule_tac x="fa ` S" in exI) |
|
762 apply(auto) |
|
763 done |
|
764 |
|
765 theorem Myhill_Nerode1: |
|
766 assumes finite_CS: "finite (UNIV // \<approx>A)" |
|
767 shows "\<exists>r::rexp. A = L r" |
|
768 proof - |
|
769 have fin: "finite (finals A)" |
|
770 using finals_in_partitions finite_CS by (rule finite_subset) |
|
771 have "\<forall>X \<in> (UNIV // \<approx>A). \<exists>r::rexp. X = L r" |
|
772 using finite_CS every_eqcl_has_reg by blast |
|
773 then have a: "\<forall>X \<in> finals A. \<exists>r::rexp. X = L r" |
|
774 using finals_in_partitions by auto |
|
775 then obtain rs::"rexp set" where "\<Union> (finals A) = \<Union>(L ` rs)" "finite rs" |
|
776 using fin by (auto dest: bchoice_finite_set) |
|
777 then have "A = L (\<Uplus>rs)" |
|
778 unfolding lang_is_union_of_finals[symmetric] by simp |
|
779 then show "\<exists>r::rexp. A = L r" by blast |
|
780 qed |
|
781 |
|
782 |
|
783 end |
|