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