42
|
1 |
theory Myhill_1
|
91
|
2 |
imports Main Folds While_Combinator
|
42
|
3 |
begin
|
|
4 |
|
|
5 |
section {* Preliminary definitions *}
|
|
6 |
|
43
|
7 |
types lang = "string set"
|
|
8 |
|
86
|
9 |
|
70
|
10 |
text {* Sequential composition of two languages *}
|
43
|
11 |
|
60
|
12 |
definition
|
|
13 |
Seq :: "lang \<Rightarrow> lang \<Rightarrow> lang" (infixr ";;" 100)
|
42
|
14 |
where
|
54
|
15 |
"A ;; B = {s\<^isub>1 @ s\<^isub>2 | s\<^isub>1 s\<^isub>2. s\<^isub>1 \<in> A \<and> s\<^isub>2 \<in> B}"
|
42
|
16 |
|
70
|
17 |
|
56
|
18 |
text {* Some properties of operator @{text ";;"}. *}
|
50
|
19 |
|
56
|
20 |
lemma seq_add_left:
|
|
21 |
assumes a: "A = B"
|
|
22 |
shows "C ;; A = C ;; B"
|
|
23 |
using a by simp
|
42
|
24 |
|
50
|
25 |
lemma seq_union_distrib_right:
|
|
26 |
shows "(A \<union> B) ;; C = (A ;; C) \<union> (B ;; C)"
|
|
27 |
unfolding Seq_def by auto
|
|
28 |
|
|
29 |
lemma seq_union_distrib_left:
|
|
30 |
shows "C ;; (A \<union> B) = (C ;; A) \<union> (C ;; B)"
|
|
31 |
unfolding Seq_def by auto
|
42
|
32 |
|
|
33 |
lemma seq_intro:
|
70
|
34 |
assumes a: "x \<in> A" "y \<in> B"
|
|
35 |
shows "x @ y \<in> A ;; B "
|
|
36 |
using a by (auto simp: Seq_def)
|
42
|
37 |
|
|
38 |
lemma seq_assoc:
|
50
|
39 |
shows "(A ;; B) ;; C = A ;; (B ;; C)"
|
|
40 |
unfolding Seq_def
|
|
41 |
apply(auto)
|
|
42 |
apply(blast)
|
42
|
43 |
by (metis append_assoc)
|
|
44 |
|
50
|
45 |
lemma seq_empty [simp]:
|
|
46 |
shows "A ;; {[]} = A"
|
|
47 |
and "{[]} ;; A = A"
|
|
48 |
by (simp_all add: Seq_def)
|
|
49 |
|
70
|
50 |
|
|
51 |
text {* Power and Star of a language *}
|
|
52 |
|
56
|
53 |
fun
|
|
54 |
pow :: "lang \<Rightarrow> nat \<Rightarrow> lang" (infixl "\<up>" 100)
|
|
55 |
where
|
|
56 |
"A \<up> 0 = {[]}"
|
|
57 |
| "A \<up> (Suc n) = A ;; (A \<up> n)"
|
50
|
58 |
|
56
|
59 |
definition
|
|
60 |
Star :: "lang \<Rightarrow> lang" ("_\<star>" [101] 102)
|
|
61 |
where
|
|
62 |
"A\<star> \<equiv> (\<Union>n. A \<up> n)"
|
|
63 |
|
70
|
64 |
|
56
|
65 |
lemma star_start[intro]:
|
|
66 |
shows "[] \<in> A\<star>"
|
|
67 |
proof -
|
|
68 |
have "[] \<in> A \<up> 0" by auto
|
|
69 |
then show "[] \<in> A\<star>" unfolding Star_def by blast
|
|
70 |
qed
|
|
71 |
|
|
72 |
lemma star_step [intro]:
|
|
73 |
assumes a: "s1 \<in> A"
|
|
74 |
and b: "s2 \<in> A\<star>"
|
|
75 |
shows "s1 @ s2 \<in> A\<star>"
|
|
76 |
proof -
|
|
77 |
from b obtain n where "s2 \<in> A \<up> n" unfolding Star_def by auto
|
|
78 |
then have "s1 @ s2 \<in> A \<up> (Suc n)" using a by (auto simp add: Seq_def)
|
|
79 |
then show "s1 @ s2 \<in> A\<star>" unfolding Star_def by blast
|
|
80 |
qed
|
42
|
81 |
|
56
|
82 |
lemma star_induct[consumes 1, case_names start step]:
|
|
83 |
assumes a: "x \<in> A\<star>"
|
|
84 |
and b: "P []"
|
|
85 |
and c: "\<And>s1 s2. \<lbrakk>s1 \<in> A; s2 \<in> A\<star>; P s2\<rbrakk> \<Longrightarrow> P (s1 @ s2)"
|
|
86 |
shows "P x"
|
|
87 |
proof -
|
|
88 |
from a obtain n where "x \<in> A \<up> n" unfolding Star_def by auto
|
|
89 |
then show "P x"
|
|
90 |
by (induct n arbitrary: x)
|
|
91 |
(auto intro!: b c simp add: Seq_def Star_def)
|
|
92 |
qed
|
|
93 |
|
|
94 |
lemma star_intro1:
|
|
95 |
assumes a: "x \<in> A\<star>"
|
|
96 |
and b: "y \<in> A\<star>"
|
|
97 |
shows "x @ y \<in> A\<star>"
|
|
98 |
using a b
|
|
99 |
by (induct rule: star_induct) (auto)
|
42
|
100 |
|
56
|
101 |
lemma star_intro2:
|
|
102 |
assumes a: "y \<in> A"
|
|
103 |
shows "y \<in> A\<star>"
|
|
104 |
proof -
|
|
105 |
from a have "y @ [] \<in> A\<star>" by blast
|
|
106 |
then show "y \<in> A\<star>" by simp
|
|
107 |
qed
|
|
108 |
|
|
109 |
lemma star_intro3:
|
|
110 |
assumes a: "x \<in> A\<star>"
|
|
111 |
and b: "y \<in> A"
|
|
112 |
shows "x @ y \<in> A\<star>"
|
|
113 |
using a b by (blast intro: star_intro1 star_intro2)
|
42
|
114 |
|
71
|
115 |
lemma star_cases:
|
|
116 |
shows "A\<star> = {[]} \<union> A ;; A\<star>"
|
|
117 |
proof
|
|
118 |
{ fix x
|
|
119 |
have "x \<in> A\<star> \<Longrightarrow> x \<in> {[]} \<union> A ;; A\<star>"
|
|
120 |
unfolding Seq_def
|
|
121 |
by (induct rule: star_induct) (auto)
|
|
122 |
}
|
|
123 |
then show "A\<star> \<subseteq> {[]} \<union> A ;; A\<star>" by auto
|
|
124 |
next
|
|
125 |
show "{[]} \<union> A ;; A\<star> \<subseteq> A\<star>"
|
|
126 |
unfolding Seq_def by auto
|
|
127 |
qed
|
|
128 |
|
42
|
129 |
lemma star_decom:
|
71
|
130 |
assumes a: "x \<in> A\<star>" "x \<noteq> []"
|
|
131 |
shows "\<exists>a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> A\<star>"
|
|
132 |
using a
|
86
|
133 |
by (induct rule: star_induct) (blast)+
|
42
|
134 |
|
50
|
135 |
lemma
|
|
136 |
shows seq_Union_left: "B ;; (\<Union>n. A \<up> n) = (\<Union>n. B ;; (A \<up> n))"
|
|
137 |
and seq_Union_right: "(\<Union>n. A \<up> n) ;; B = (\<Union>n. (A \<up> n) ;; B)"
|
|
138 |
unfolding Seq_def by auto
|
|
139 |
|
|
140 |
lemma seq_pow_comm:
|
|
141 |
shows "A ;; (A \<up> n) = (A \<up> n) ;; A"
|
|
142 |
by (induct n) (simp_all add: seq_assoc[symmetric])
|
|
143 |
|
|
144 |
lemma seq_star_comm:
|
|
145 |
shows "A ;; A\<star> = A\<star> ;; A"
|
86
|
146 |
unfolding Star_def seq_Union_left
|
|
147 |
unfolding seq_pow_comm seq_Union_right
|
50
|
148 |
by simp
|
|
149 |
|
86
|
150 |
|
50
|
151 |
text {* Two lemmas about the length of strings in @{text "A \<up> n"} *}
|
|
152 |
|
|
153 |
lemma pow_length:
|
|
154 |
assumes a: "[] \<notin> A"
|
|
155 |
and b: "s \<in> A \<up> Suc n"
|
|
156 |
shows "n < length s"
|
|
157 |
using b
|
|
158 |
proof (induct n arbitrary: s)
|
|
159 |
case 0
|
|
160 |
have "s \<in> A \<up> Suc 0" by fact
|
|
161 |
with a have "s \<noteq> []" by auto
|
|
162 |
then show "0 < length s" by auto
|
|
163 |
next
|
|
164 |
case (Suc n)
|
|
165 |
have ih: "\<And>s. s \<in> A \<up> Suc n \<Longrightarrow> n < length s" by fact
|
|
166 |
have "s \<in> A \<up> Suc (Suc n)" by fact
|
|
167 |
then obtain s1 s2 where eq: "s = s1 @ s2" and *: "s1 \<in> A" and **: "s2 \<in> A \<up> Suc n"
|
|
168 |
by (auto simp add: Seq_def)
|
|
169 |
from ih ** have "n < length s2" by simp
|
|
170 |
moreover have "0 < length s1" using * a by auto
|
|
171 |
ultimately show "Suc n < length s" unfolding eq
|
|
172 |
by (simp only: length_append)
|
|
173 |
qed
|
|
174 |
|
|
175 |
lemma seq_pow_length:
|
|
176 |
assumes a: "[] \<notin> A"
|
|
177 |
and b: "s \<in> B ;; (A \<up> Suc n)"
|
|
178 |
shows "n < length s"
|
|
179 |
proof -
|
|
180 |
from b obtain s1 s2 where eq: "s = s1 @ s2" and *: "s2 \<in> A \<up> Suc n"
|
|
181 |
unfolding Seq_def by auto
|
|
182 |
from * have " n < length s2" by (rule pow_length[OF a])
|
|
183 |
then show "n < length s" using eq by simp
|
|
184 |
qed
|
|
185 |
|
|
186 |
|
86
|
187 |
section {* A modified version of Arden's lemma *}
|
50
|
188 |
|
70
|
189 |
text {* A helper lemma for Arden *}
|
50
|
190 |
|
86
|
191 |
lemma arden_helper:
|
50
|
192 |
assumes eq: "X = X ;; A \<union> B"
|
|
193 |
shows "X = X ;; (A \<up> Suc n) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))"
|
|
194 |
proof (induct n)
|
|
195 |
case 0
|
|
196 |
show "X = X ;; (A \<up> Suc 0) \<union> (\<Union>(m::nat)\<in>{0..0}. B ;; (A \<up> m))"
|
|
197 |
using eq by simp
|
|
198 |
next
|
|
199 |
case (Suc n)
|
|
200 |
have ih: "X = X ;; (A \<up> Suc n) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))" by fact
|
|
201 |
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
|
|
202 |
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))"
|
|
203 |
by (simp add: seq_union_distrib_right seq_assoc)
|
|
204 |
also have "\<dots> = X ;; (A \<up> Suc (Suc n)) \<union> (\<Union>m\<in>{0..Suc n}. B ;; (A \<up> m))"
|
|
205 |
by (auto simp add: le_Suc_eq)
|
|
206 |
finally show "X = X ;; (A \<up> Suc (Suc n)) \<union> (\<Union>m\<in>{0..Suc n}. B ;; (A \<up> m))" .
|
|
207 |
qed
|
|
208 |
|
86
|
209 |
theorem arden:
|
50
|
210 |
assumes nemp: "[] \<notin> A"
|
|
211 |
shows "X = X ;; A \<union> B \<longleftrightarrow> X = B ;; A\<star>"
|
|
212 |
proof
|
|
213 |
assume eq: "X = B ;; A\<star>"
|
|
214 |
have "A\<star> = {[]} \<union> A\<star> ;; A"
|
|
215 |
unfolding seq_star_comm[symmetric]
|
71
|
216 |
by (rule star_cases)
|
56
|
217 |
then have "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"
|
|
218 |
by (rule seq_add_left)
|
50
|
219 |
also have "\<dots> = B \<union> B ;; (A\<star> ;; A)"
|
|
220 |
unfolding seq_union_distrib_left by simp
|
|
221 |
also have "\<dots> = B \<union> (B ;; A\<star>) ;; A"
|
|
222 |
by (simp only: seq_assoc)
|
|
223 |
finally show "X = X ;; A \<union> B"
|
|
224 |
using eq by blast
|
|
225 |
next
|
|
226 |
assume eq: "X = X ;; A \<union> B"
|
|
227 |
{ fix n::nat
|
86
|
228 |
have "B ;; (A \<up> n) \<subseteq> X" using arden_helper[OF eq, of "n"] by auto }
|
56
|
229 |
then have "B ;; A\<star> \<subseteq> X"
|
86
|
230 |
unfolding Seq_def Star_def UNION_def by auto
|
50
|
231 |
moreover
|
|
232 |
{ fix s::string
|
|
233 |
obtain k where "k = length s" by auto
|
|
234 |
then have not_in: "s \<notin> X ;; (A \<up> Suc k)"
|
|
235 |
using seq_pow_length[OF nemp] by blast
|
|
236 |
assume "s \<in> X"
|
|
237 |
then have "s \<in> X ;; (A \<up> Suc k) \<union> (\<Union>m\<in>{0..k}. B ;; (A \<up> m))"
|
86
|
238 |
using arden_helper[OF eq, of "k"] by auto
|
50
|
239 |
then have "s \<in> (\<Union>m\<in>{0..k}. B ;; (A \<up> m))" using not_in by auto
|
|
240 |
moreover
|
|
241 |
have "(\<Union>m\<in>{0..k}. B ;; (A \<up> m)) \<subseteq> (\<Union>n. B ;; (A \<up> n))" by auto
|
|
242 |
ultimately
|
56
|
243 |
have "s \<in> B ;; A\<star>"
|
86
|
244 |
unfolding seq_Union_left Star_def by auto }
|
50
|
245 |
then have "X \<subseteq> B ;; A\<star>" by auto
|
|
246 |
ultimately
|
|
247 |
show "X = B ;; A\<star>" by simp
|
|
248 |
qed
|
|
249 |
|
42
|
250 |
|
70
|
251 |
section {* Regular Expressions *}
|
48
|
252 |
|
|
253 |
datatype rexp =
|
|
254 |
NULL
|
|
255 |
| EMPTY
|
|
256 |
| CHAR char
|
|
257 |
| SEQ rexp rexp
|
|
258 |
| ALT rexp rexp
|
|
259 |
| STAR rexp
|
|
260 |
|
|
261 |
|
|
262 |
text {*
|
86
|
263 |
The function @{text L} is overloaded, with the idea that @{text "L x"}
|
|
264 |
evaluates to the language represented by the object @{text x}.
|
48
|
265 |
*}
|
|
266 |
|
70
|
267 |
consts L:: "'a \<Rightarrow> lang"
|
48
|
268 |
|
70
|
269 |
overloading L_rexp \<equiv> "L:: rexp \<Rightarrow> lang"
|
48
|
270 |
begin
|
|
271 |
fun
|
88
|
272 |
L_rexp :: "rexp \<Rightarrow> lang"
|
48
|
273 |
where
|
|
274 |
"L_rexp (NULL) = {}"
|
|
275 |
| "L_rexp (EMPTY) = {[]}"
|
|
276 |
| "L_rexp (CHAR c) = {[c]}"
|
|
277 |
| "L_rexp (SEQ r1 r2) = (L_rexp r1) ;; (L_rexp r2)"
|
|
278 |
| "L_rexp (ALT r1 r2) = (L_rexp r1) \<union> (L_rexp r2)"
|
|
279 |
| "L_rexp (STAR r) = (L_rexp r)\<star>"
|
|
280 |
end
|
|
281 |
|
88
|
282 |
|
86
|
283 |
text {* ALT-combination of a set or regulare expressions *}
|
50
|
284 |
|
76
|
285 |
abbreviation
|
|
286 |
Setalt ("\<Uplus>_" [1000] 999)
|
|
287 |
where
|
94
|
288 |
"\<Uplus>A \<equiv> folds ALT NULL A"
|
76
|
289 |
|
50
|
290 |
text {*
|
86
|
291 |
For finite sets, @{term Setalt} is preserved under @{term L}.
|
79
|
292 |
*}
|
70
|
293 |
|
50
|
294 |
lemma folds_alt_simp [simp]:
|
88
|
295 |
fixes rs::"rexp set"
|
70
|
296 |
assumes a: "finite rs"
|
76
|
297 |
shows "L (\<Uplus>rs) = \<Union> (L ` rs)"
|
94
|
298 |
unfolding folds_def
|
75
|
299 |
apply(rule set_eqI)
|
70
|
300 |
apply(rule someI2_ex)
|
|
301 |
apply(rule_tac finite_imp_fold_graph[OF a])
|
|
302 |
apply(erule fold_graph.induct)
|
|
303 |
apply(auto)
|
|
304 |
done
|
50
|
305 |
|
70
|
306 |
|
86
|
307 |
section {* Direction @{text "finite partition \<Rightarrow> regular language"} *}
|
|
308 |
|
|
309 |
|
70
|
310 |
text {* Just a technical lemma for collections and pairs *}
|
|
311 |
|
75
|
312 |
lemma Pair_Collect[simp]:
|
48
|
313 |
shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
|
|
314 |
by simp
|
|
315 |
|
86
|
316 |
text {* Myhill-Nerode relation *}
|
|
317 |
|
48
|
318 |
definition
|
71
|
319 |
str_eq_rel :: "lang \<Rightarrow> (string \<times> string) set" ("\<approx>_" [100] 100)
|
48
|
320 |
where
|
70
|
321 |
"\<approx>A \<equiv> {(x, y). (\<forall>z. x @ z \<in> A \<longleftrightarrow> y @ z \<in> A)}"
|
48
|
322 |
|
|
323 |
text {*
|
86
|
324 |
Among the equivalence clases of @{text "\<approx>A"}, the set @{text "finals A"}
|
|
325 |
singles out those which contains the strings from @{text A}.
|
48
|
326 |
*}
|
|
327 |
|
|
328 |
definition
|
71
|
329 |
finals :: "lang \<Rightarrow> lang set"
|
|
330 |
where
|
|
331 |
"finals A \<equiv> {\<approx>A `` {x} | x . x \<in> A}"
|
48
|
332 |
|
70
|
333 |
|
48
|
334 |
lemma lang_is_union_of_finals:
|
70
|
335 |
shows "A = \<Union> finals A"
|
|
336 |
unfolding finals_def
|
|
337 |
unfolding Image_def
|
|
338 |
unfolding str_eq_rel_def
|
|
339 |
apply(auto)
|
|
340 |
apply(drule_tac x = "[]" in spec)
|
|
341 |
apply(auto)
|
|
342 |
done
|
|
343 |
|
79
|
344 |
lemma finals_in_partitions:
|
|
345 |
shows "finals A \<subseteq> (UNIV // \<approx>A)"
|
94
|
346 |
unfolding finals_def quotient_def
|
76
|
347 |
by auto
|
|
348 |
|
86
|
349 |
section {* Equational systems *}
|
42
|
350 |
|
89
|
351 |
text {* The two kinds of terms in the rhs of equations. *}
|
|
352 |
|
42
|
353 |
datatype rhs_item =
|
86
|
354 |
Lam "rexp" (* Lambda-marker *)
|
70
|
355 |
| Trn "lang" "rexp" (* Transition *)
|
|
356 |
|
42
|
357 |
|
86
|
358 |
overloading L_rhs_item \<equiv> "L:: rhs_item \<Rightarrow> lang"
|
42
|
359 |
begin
|
86
|
360 |
fun L_rhs_item:: "rhs_item \<Rightarrow> lang"
|
42
|
361 |
where
|
86
|
362 |
"L_rhs_item (Lam r) = L r"
|
|
363 |
| "L_rhs_item (Trn X r) = X ;; L r"
|
42
|
364 |
end
|
|
365 |
|
70
|
366 |
overloading L_rhs \<equiv> "L:: rhs_item set \<Rightarrow> lang"
|
42
|
367 |
begin
|
70
|
368 |
fun L_rhs:: "rhs_item set \<Rightarrow> lang"
|
|
369 |
where
|
|
370 |
"L_rhs rhs = \<Union> (L ` rhs)"
|
42
|
371 |
end
|
|
372 |
|
96
|
373 |
lemma L_rhs_union_distrib:
|
|
374 |
fixes A B::"rhs_item set"
|
|
375 |
shows "L A \<union> L B = L (A \<union> B)"
|
|
376 |
by simp
|
|
377 |
|
|
378 |
|
|
379 |
|
86
|
380 |
text {* Transitions between equivalence classes *}
|
71
|
381 |
|
|
382 |
definition
|
92
|
383 |
transition :: "lang \<Rightarrow> char \<Rightarrow> lang \<Rightarrow> bool" ("_ \<Turnstile>_\<Rightarrow>_" [100,100,100] 100)
|
71
|
384 |
where
|
92
|
385 |
"Y \<Turnstile>c\<Rightarrow> X \<equiv> Y ;; {[c]} \<subseteq> X"
|
42
|
386 |
|
86
|
387 |
text {* Initial equational system *}
|
|
388 |
|
42
|
389 |
definition
|
96
|
390 |
"Init_rhs CS X \<equiv>
|
42
|
391 |
if ([] \<in> X) then
|
92
|
392 |
{Lam EMPTY} \<union> {Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}
|
42
|
393 |
else
|
92
|
394 |
{Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}"
|
42
|
395 |
|
86
|
396 |
definition
|
96
|
397 |
"Init CS \<equiv> {(X, Init_rhs CS X) | X. X \<in> CS}"
|
75
|
398 |
|
|
399 |
|
|
400 |
|
86
|
401 |
section {* Arden Operation on equations *}
|
42
|
402 |
|
|
403 |
text {*
|
86
|
404 |
The function @{text "attach_rexp r item"} SEQ-composes @{text r} to the
|
|
405 |
right of every rhs-item.
|
75
|
406 |
*}
|
42
|
407 |
|
70
|
408 |
fun
|
92
|
409 |
append_rexp :: "rexp \<Rightarrow> rhs_item \<Rightarrow> rhs_item"
|
42
|
410 |
where
|
92
|
411 |
"append_rexp r (Lam rexp) = Lam (SEQ rexp r)"
|
|
412 |
| "append_rexp r (Trn X rexp) = Trn X (SEQ rexp r)"
|
42
|
413 |
|
|
414 |
|
|
415 |
definition
|
92
|
416 |
"append_rhs_rexp rhs rexp \<equiv> (append_rexp rexp) ` rhs"
|
42
|
417 |
|
86
|
418 |
definition
|
94
|
419 |
"Arden X rhs \<equiv>
|
|
420 |
append_rhs_rexp (rhs - {Trn X r | r. Trn X r \<in> rhs}) (STAR (\<Uplus> {r. Trn X r \<in> rhs}))"
|
86
|
421 |
|
|
422 |
|
|
423 |
section {* Substitution Operation on equations *}
|
|
424 |
|
|
425 |
text {*
|
95
|
426 |
Suppose and equation @{text "X = xrhs"}, @{text "Subst"} substitutes
|
86
|
427 |
all occurences of @{text "X"} in @{text "rhs"} by @{text "xrhs"}.
|
71
|
428 |
*}
|
|
429 |
|
42
|
430 |
definition
|
94
|
431 |
"Subst rhs X xrhs \<equiv>
|
|
432 |
(rhs - {Trn X r | r. Trn X r \<in> rhs}) \<union> (append_rhs_rexp xrhs (\<Uplus> {r. Trn X r \<in> rhs}))"
|
42
|
433 |
|
|
434 |
text {*
|
86
|
435 |
@{text "eqs_subst ES X xrhs"} substitutes @{text xrhs} into every
|
|
436 |
equation of the equational system @{text ES}.
|
|
437 |
*}
|
42
|
438 |
|
97
|
439 |
types esystem = "(lang \<times> rhs_item set) set"
|
|
440 |
|
42
|
441 |
definition
|
97
|
442 |
Subst_all :: "esystem \<Rightarrow> lang \<Rightarrow> rhs_item set \<Rightarrow> esystem"
|
|
443 |
where
|
94
|
444 |
"Subst_all ES X xrhs \<equiv> {(Y, Subst yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}"
|
86
|
445 |
|
42
|
446 |
text {*
|
91
|
447 |
The following term @{text "remove ES Y yrhs"} removes the equation
|
|
448 |
@{text "Y = yrhs"} from equational system @{text "ES"} by replacing
|
|
449 |
all occurences of @{text "Y"} by its definition (using @{text "eqs_subst"}).
|
|
450 |
The @{text "Y"}-definition is made non-recursive using Arden's transformation
|
|
451 |
@{text "arden_variate Y yrhs"}.
|
|
452 |
*}
|
|
453 |
|
|
454 |
definition
|
96
|
455 |
"Remove ES X xrhs \<equiv>
|
|
456 |
Subst_all (ES - {(X, xrhs)}) X (Arden X xrhs)"
|
|
457 |
|
|
458 |
|
|
459 |
section {* While-combinator *}
|
91
|
460 |
|
|
461 |
text {*
|
96
|
462 |
The following term @{text "Iter X ES"} represents one iteration in the while loop.
|
91
|
463 |
It arbitrarily chooses a @{text "Y"} different from @{text "X"} to remove.
|
71
|
464 |
*}
|
42
|
465 |
|
91
|
466 |
definition
|
96
|
467 |
"Iter X ES \<equiv> (let (Y, yrhs) = SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> X \<noteq> Y
|
95
|
468 |
in Remove ES Y yrhs)"
|
42
|
469 |
|
97
|
470 |
lemma IterI2:
|
|
471 |
assumes "(Y, yrhs) \<in> ES"
|
|
472 |
and "X \<noteq> Y"
|
|
473 |
and "\<And>Y yrhs. \<lbrakk>(Y, yrhs) \<in> ES; X \<noteq> Y\<rbrakk> \<Longrightarrow> Q (Remove ES Y yrhs)"
|
|
474 |
shows "Q (Iter X ES)"
|
|
475 |
unfolding Iter_def using assms
|
|
476 |
by (rule_tac a="(Y, yrhs)" in someI2) (auto)
|
|
477 |
|
|
478 |
|
42
|
479 |
text {*
|
96
|
480 |
The following term @{text "Reduce X ES"} repeatedly removes characteriztion equations
|
91
|
481 |
for unknowns other than @{text "X"} until one is left.
|
42
|
482 |
*}
|
|
483 |
|
97
|
484 |
abbreviation
|
101
|
485 |
"Cond ES \<equiv> card ES \<noteq> 1"
|
97
|
486 |
|
91
|
487 |
definition
|
101
|
488 |
"Solve X ES \<equiv> while Cond (Iter X) ES"
|
97
|
489 |
|
91
|
490 |
text {*
|
97
|
491 |
Since the @{text "while"} combinator from HOL library is used to implement @{text "Solve X ES"},
|
91
|
492 |
the induction principle @{thm [source] while_rule} is used to proved the desired properties
|
97
|
493 |
of @{text "Solve X ES"}. For this purpose, an invariant predicate @{text "invariant"} is defined
|
91
|
494 |
in terms of a series of auxilliary predicates:
|
|
495 |
*}
|
86
|
496 |
|
|
497 |
section {* Invariants *}
|
|
498 |
|
97
|
499 |
text {* Every variable is defined at most once in @{text ES}. *}
|
75
|
500 |
|
42
|
501 |
definition
|
|
502 |
"distinct_equas ES \<equiv>
|
86
|
503 |
\<forall> X rhs rhs'. (X, rhs) \<in> ES \<and> (X, rhs') \<in> ES \<longrightarrow> rhs = rhs'"
|
70
|
504 |
|
97
|
505 |
|
42
|
506 |
text {*
|
86
|
507 |
Every equation in @{text ES} (represented by @{text "(X, rhs)"})
|
97
|
508 |
is valid, i.e. @{text "X = L rhs"}.
|
86
|
509 |
*}
|
|
510 |
|
42
|
511 |
definition
|
104
|
512 |
"sound_eqs ES \<equiv> \<forall>(X, rhs) \<in> ES. X = L rhs"
|
42
|
513 |
|
|
514 |
text {*
|
86
|
515 |
@{text "rhs_nonempty rhs"} requires regular expressions occuring in
|
|
516 |
transitional items of @{text "rhs"} do not contain empty string. This is
|
|
517 |
necessary for the application of Arden's transformation to @{text "rhs"}.
|
|
518 |
*}
|
70
|
519 |
|
42
|
520 |
definition
|
|
521 |
"rhs_nonempty rhs \<equiv> (\<forall> Y r. Trn Y r \<in> rhs \<longrightarrow> [] \<notin> L r)"
|
|
522 |
|
|
523 |
text {*
|
86
|
524 |
The following @{text "ardenable ES"} requires that Arden's transformation
|
|
525 |
is applicable to every equation of equational system @{text "ES"}.
|
|
526 |
*}
|
70
|
527 |
|
42
|
528 |
definition
|
97
|
529 |
"ardenable ES \<equiv> \<forall>(X, rhs) \<in> ES. rhs_nonempty rhs"
|
42
|
530 |
|
103
|
531 |
|
86
|
532 |
text {*
|
|
533 |
@{text "finite_rhs ES"} requires every equation in @{text "rhs"}
|
|
534 |
be finite.
|
|
535 |
*}
|
42
|
536 |
definition
|
103
|
537 |
"finite_rhs ES \<equiv> \<forall>(X, rhs) \<in> ES. finite rhs"
|
|
538 |
|
|
539 |
lemma finite_rhs_def2:
|
|
540 |
"finite_rhs ES = (\<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> finite rhs)"
|
|
541 |
unfolding finite_rhs_def by auto
|
42
|
542 |
|
|
543 |
text {*
|
86
|
544 |
@{text "classes_of rhs"} returns all variables (or equivalent classes)
|
42
|
545 |
occuring in @{text "rhs"}.
|
|
546 |
*}
|
86
|
547 |
|
42
|
548 |
definition
|
104
|
549 |
"rhss rhs \<equiv> {X | X r. Trn X r \<in> rhs}"
|
42
|
550 |
|
|
551 |
text {*
|
86
|
552 |
@{text "lefts_of ES"} returns all variables defined by an
|
|
553 |
equational system @{text "ES"}.
|
|
554 |
*}
|
42
|
555 |
definition
|
103
|
556 |
"lhss ES \<equiv> {Y | Y yrhs. (Y, yrhs) \<in> ES}"
|
42
|
557 |
|
|
558 |
text {*
|
104
|
559 |
The following @{text "valid_eqs ES"} requires that every variable occuring
|
86
|
560 |
on the right hand side of equations is already defined by some equation in @{text "ES"}.
|
|
561 |
*}
|
42
|
562 |
definition
|
104
|
563 |
"valid_eqs ES \<equiv> \<forall>(X, rhs) \<in> ES. rhss rhs \<subseteq> lhss ES"
|
42
|
564 |
|
|
565 |
|
|
566 |
text {*
|
86
|
567 |
The invariant @{text "invariant(ES)"} is a conjunction of all the previously defined constaints.
|
42
|
568 |
*}
|
|
569 |
definition
|
103
|
570 |
"invariant ES \<equiv> finite ES
|
|
571 |
\<and> finite_rhs ES
|
104
|
572 |
\<and> sound_eqs ES
|
103
|
573 |
\<and> distinct_equas ES
|
|
574 |
\<and> ardenable ES
|
104
|
575 |
\<and> valid_eqs ES"
|
42
|
576 |
|
96
|
577 |
|
|
578 |
lemma invariantI:
|
104
|
579 |
assumes "sound_eqs ES" "finite ES" "distinct_equas ES" "ardenable ES"
|
|
580 |
"finite_rhs ES" "valid_eqs ES"
|
96
|
581 |
shows "invariant ES"
|
|
582 |
using assms by (simp add: invariant_def)
|
|
583 |
|
42
|
584 |
subsection {* The proof of this direction *}
|
|
585 |
|
|
586 |
subsubsection {* Basic properties *}
|
|
587 |
|
|
588 |
text {*
|
|
589 |
The following are some basic properties of the above definitions.
|
|
590 |
*}
|
|
591 |
|
|
592 |
|
79
|
593 |
lemma finite_Trn:
|
|
594 |
assumes fin: "finite rhs"
|
|
595 |
shows "finite {r. Trn Y r \<in> rhs}"
|
|
596 |
proof -
|
|
597 |
have "finite {Trn Y r | Y r. Trn Y r \<in> rhs}"
|
|
598 |
by (rule rev_finite_subset[OF fin]) (auto)
|
81
|
599 |
then have "finite ((\<lambda>(Y, r). Trn Y r) ` {(Y, r) | Y r. Trn Y r \<in> rhs})"
|
|
600 |
by (simp add: image_Collect)
|
|
601 |
then have "finite {(Y, r) | Y r. Trn Y r \<in> rhs}"
|
|
602 |
by (erule_tac finite_imageD) (simp add: inj_on_def)
|
79
|
603 |
then show "finite {r. Trn Y r \<in> rhs}"
|
81
|
604 |
by (erule_tac f="snd" in finite_surj) (auto simp add: image_def)
|
79
|
605 |
qed
|
|
606 |
|
|
607 |
lemma finite_Lam:
|
96
|
608 |
assumes fin: "finite rhs"
|
79
|
609 |
shows "finite {r. Lam r \<in> rhs}"
|
|
610 |
proof -
|
|
611 |
have "finite {Lam r | r. Lam r \<in> rhs}"
|
|
612 |
by (rule rev_finite_subset[OF fin]) (auto)
|
|
613 |
then show "finite {r. Lam r \<in> rhs}"
|
81
|
614 |
apply(simp add: image_Collect[symmetric])
|
|
615 |
apply(erule finite_imageD)
|
|
616 |
apply(auto simp add: inj_on_def)
|
79
|
617 |
done
|
42
|
618 |
qed
|
|
619 |
|
|
620 |
lemma rexp_of_empty:
|
96
|
621 |
assumes finite: "finite rhs"
|
|
622 |
and nonempty: "rhs_nonempty rhs"
|
79
|
623 |
shows "[] \<notin> L (\<Uplus> {r. Trn X r \<in> rhs})"
|
42
|
624 |
using finite nonempty rhs_nonempty_def
|
79
|
625 |
using finite_Trn[OF finite]
|
97
|
626 |
by auto
|
42
|
627 |
|
|
628 |
lemma lang_of_rexp_of:
|
|
629 |
assumes finite:"finite rhs"
|
79
|
630 |
shows "L ({Trn X r| r. Trn X r \<in> rhs}) = X ;; (L (\<Uplus>{r. Trn X r \<in> rhs}))"
|
42
|
631 |
proof -
|
79
|
632 |
have "finite {r. Trn X r \<in> rhs}"
|
|
633 |
by (rule finite_Trn[OF finite])
|
|
634 |
then show ?thesis
|
|
635 |
apply(auto simp add: Seq_def)
|
96
|
636 |
apply(rule_tac x = "s\<^isub>1" in exI, rule_tac x = "s\<^isub>2" in exI)
|
|
637 |
apply(auto)
|
79
|
638 |
apply(rule_tac x= "Trn X xa" in exI)
|
96
|
639 |
apply(auto simp add: Seq_def)
|
79
|
640 |
done
|
42
|
641 |
qed
|
|
642 |
|
96
|
643 |
lemma lang_of_append:
|
|
644 |
"L (append_rexp r rhs_item) = L rhs_item ;; L r"
|
|
645 |
by (induct rule: append_rexp.induct)
|
|
646 |
(auto simp add: seq_assoc)
|
42
|
647 |
|
|
648 |
lemma lang_of_append_rhs:
|
|
649 |
"L (append_rhs_rexp rhs r) = L rhs ;; L r"
|
96
|
650 |
unfolding append_rhs_rexp_def
|
|
651 |
by (auto simp add: Seq_def lang_of_append)
|
42
|
652 |
|
104
|
653 |
lemma rhss_union_distrib:
|
|
654 |
shows "rhss (A \<union> B) = rhss A \<union> rhss B"
|
|
655 |
by (auto simp add: rhss_def)
|
42
|
656 |
|
103
|
657 |
lemma lhss_union_distrib:
|
|
658 |
shows "lhss (A \<union> B) = lhss A \<union> lhss B"
|
|
659 |
by (auto simp add: lhss_def)
|
42
|
660 |
|
|
661 |
|
|
662 |
subsubsection {* Intialization *}
|
|
663 |
|
|
664 |
text {*
|
86
|
665 |
The following several lemmas until @{text "init_ES_satisfy_invariant"} shows that
|
|
666 |
the initial equational system satisfies invariant @{text "invariant"}.
|
71
|
667 |
*}
|
42
|
668 |
|
|
669 |
lemma defined_by_str:
|
100
|
670 |
assumes "s \<in> X" "X \<in> UNIV // \<approx>A"
|
|
671 |
shows "X = \<approx>A `` {s}"
|
|
672 |
using assms
|
|
673 |
unfolding quotient_def Image_def str_eq_rel_def
|
|
674 |
by auto
|
42
|
675 |
|
|
676 |
lemma every_eqclass_has_transition:
|
|
677 |
assumes has_str: "s @ [c] \<in> X"
|
100
|
678 |
and in_CS: "X \<in> UNIV // \<approx>A"
|
|
679 |
obtains Y where "Y \<in> UNIV // \<approx>A" and "Y ;; {[c]} \<subseteq> X" and "s \<in> Y"
|
42
|
680 |
proof -
|
100
|
681 |
def Y \<equiv> "\<approx>A `` {s}"
|
|
682 |
have "Y \<in> UNIV // \<approx>A"
|
42
|
683 |
unfolding Y_def quotient_def by auto
|
|
684 |
moreover
|
100
|
685 |
have "X = \<approx>A `` {s @ [c]}"
|
42
|
686 |
using has_str in_CS defined_by_str by blast
|
|
687 |
then have "Y ;; {[c]} \<subseteq> X"
|
|
688 |
unfolding Y_def Image_def Seq_def
|
|
689 |
unfolding str_eq_rel_def
|
|
690 |
by clarsimp
|
|
691 |
moreover
|
|
692 |
have "s \<in> Y" unfolding Y_def
|
|
693 |
unfolding Image_def str_eq_rel_def by simp
|
100
|
694 |
ultimately show thesis using that by blast
|
42
|
695 |
qed
|
|
696 |
|
|
697 |
lemma l_eq_r_in_eqs:
|
100
|
698 |
assumes X_in_eqs: "(X, rhs) \<in> Init (UNIV // \<approx>A)"
|
|
699 |
shows "X = L rhs"
|
42
|
700 |
proof
|
100
|
701 |
show "X \<subseteq> L rhs"
|
42
|
702 |
proof
|
|
703 |
fix x
|
|
704 |
assume "(1)": "x \<in> X"
|
100
|
705 |
show "x \<in> L rhs"
|
42
|
706 |
proof (cases "x = []")
|
|
707 |
assume empty: "x = []"
|
|
708 |
thus ?thesis using X_in_eqs "(1)"
|
96
|
709 |
by (auto simp: Init_def Init_rhs_def)
|
42
|
710 |
next
|
|
711 |
assume not_empty: "x \<noteq> []"
|
|
712 |
then obtain clist c where decom: "x = clist @ [c]"
|
|
713 |
by (case_tac x rule:rev_cases, auto)
|
100
|
714 |
have "X \<in> UNIV // \<approx>A" using X_in_eqs by (auto simp:Init_def)
|
42
|
715 |
then obtain Y
|
100
|
716 |
where "Y \<in> UNIV // \<approx>A"
|
42
|
717 |
and "Y ;; {[c]} \<subseteq> X"
|
|
718 |
and "clist \<in> Y"
|
|
719 |
using decom "(1)" every_eqclass_has_transition by blast
|
|
720 |
hence
|
100
|
721 |
"x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // \<approx>A \<and> Y \<Turnstile>c\<Rightarrow> X}"
|
71
|
722 |
unfolding transition_def
|
|
723 |
using "(1)" decom
|
42
|
724 |
by (simp, rule_tac x = "Trn Y (CHAR c)" in exI, simp add:Seq_def)
|
71
|
725 |
thus ?thesis using X_in_eqs "(1)"
|
96
|
726 |
by (simp add: Init_def Init_rhs_def)
|
42
|
727 |
qed
|
|
728 |
qed
|
|
729 |
next
|
100
|
730 |
show "L rhs \<subseteq> X" using X_in_eqs
|
96
|
731 |
by (auto simp:Init_def Init_rhs_def transition_def)
|
42
|
732 |
qed
|
|
733 |
|
100
|
734 |
lemma test:
|
|
735 |
assumes X_in_eqs: "(X, rhs) \<in> Init (UNIV // \<approx>A)"
|
|
736 |
shows "X = \<Union> (L ` rhs)"
|
|
737 |
using assms
|
|
738 |
by (drule_tac l_eq_r_in_eqs) (simp)
|
|
739 |
|
|
740 |
|
96
|
741 |
lemma finite_Init_rhs:
|
42
|
742 |
assumes finite: "finite CS"
|
96
|
743 |
shows "finite (Init_rhs CS X)"
|
42
|
744 |
proof-
|
105
|
745 |
def S \<equiv> "{(Y, c)| Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}"
|
|
746 |
def h \<equiv> "\<lambda> (Y, c). Trn Y (CHAR c)"
|
|
747 |
have "finite (CS \<times> (UNIV::char set))" using finite by auto
|
|
748 |
then have "finite S" using S_def
|
|
749 |
by (rule_tac B = "CS \<times> UNIV" in finite_subset) (auto)
|
|
750 |
moreover have "{Trn Y (CHAR c) |Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X} = h ` S"
|
|
751 |
unfolding S_def h_def image_def by auto
|
|
752 |
ultimately
|
|
753 |
have "finite {Trn Y (CHAR c) |Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}" by auto
|
|
754 |
then show "finite (Init_rhs CS X)" unfolding Init_rhs_def transition_def by simp
|
42
|
755 |
qed
|
|
756 |
|
96
|
757 |
lemma Init_ES_satisfies_invariant:
|
|
758 |
assumes finite_CS: "finite (UNIV // \<approx>A)"
|
|
759 |
shows "invariant (Init (UNIV // \<approx>A))"
|
|
760 |
proof (rule invariantI)
|
104
|
761 |
show "sound_eqs (Init (UNIV // \<approx>A))"
|
|
762 |
unfolding sound_eqs_def
|
97
|
763 |
using l_eq_r_in_eqs by auto
|
96
|
764 |
show "finite (Init (UNIV // \<approx>A))" using finite_CS
|
|
765 |
unfolding Init_def by simp
|
|
766 |
show "distinct_equas (Init (UNIV // \<approx>A))"
|
|
767 |
unfolding distinct_equas_def Init_def by simp
|
|
768 |
show "ardenable (Init (UNIV // \<approx>A))"
|
|
769 |
unfolding ardenable_def Init_def Init_rhs_def rhs_nonempty_def
|
103
|
770 |
by auto
|
96
|
771 |
show "finite_rhs (Init (UNIV // \<approx>A))"
|
|
772 |
using finite_Init_rhs[OF finite_CS]
|
|
773 |
unfolding finite_rhs_def Init_def by auto
|
104
|
774 |
show "valid_eqs (Init (UNIV // \<approx>A))"
|
|
775 |
unfolding valid_eqs_def Init_def Init_rhs_def rhss_def lhss_def
|
96
|
776 |
by auto
|
42
|
777 |
qed
|
|
778 |
|
91
|
779 |
subsubsection {* Interation step *}
|
42
|
780 |
|
|
781 |
text {*
|
91
|
782 |
From this point until @{text "iteration_step"},
|
96
|
783 |
the correctness of the iteration step @{text "Iter X ES"} is proved.
|
71
|
784 |
*}
|
|
785 |
|
94
|
786 |
lemma Arden_keeps_eq:
|
42
|
787 |
assumes l_eq_r: "X = L rhs"
|
79
|
788 |
and not_empty: "[] \<notin> L (\<Uplus>{r. Trn X r \<in> rhs})"
|
42
|
789 |
and finite: "finite rhs"
|
94
|
790 |
shows "X = L (Arden X rhs)"
|
42
|
791 |
proof -
|
79
|
792 |
def A \<equiv> "L (\<Uplus>{r. Trn X r \<in> rhs})"
|
94
|
793 |
def b \<equiv> "rhs - {Trn X r | r. Trn X r \<in> rhs}"
|
42
|
794 |
def B \<equiv> "L b"
|
|
795 |
have "X = B ;; A\<star>"
|
|
796 |
proof-
|
94
|
797 |
have "L rhs = L({Trn X r | r. Trn X r \<in> rhs} \<union> b)" by (auto simp: b_def)
|
79
|
798 |
also have "\<dots> = X ;; A \<union> B"
|
|
799 |
unfolding L_rhs_union_distrib[symmetric]
|
|
800 |
by (simp only: lang_of_rexp_of finite B_def A_def)
|
|
801 |
finally show ?thesis
|
42
|
802 |
using l_eq_r not_empty
|
86
|
803 |
apply(rule_tac arden[THEN iffD1])
|
79
|
804 |
apply(simp add: A_def)
|
|
805 |
apply(simp)
|
|
806 |
done
|
42
|
807 |
qed
|
94
|
808 |
moreover have "L (Arden X rhs) = B ;; A\<star>"
|
|
809 |
by (simp only:Arden_def L_rhs_union_distrib lang_of_append_rhs
|
50
|
810 |
B_def A_def b_def L_rexp.simps seq_union_distrib_left)
|
42
|
811 |
ultimately show ?thesis by simp
|
|
812 |
qed
|
|
813 |
|
|
814 |
lemma append_keeps_finite:
|
|
815 |
"finite rhs \<Longrightarrow> finite (append_rhs_rexp rhs r)"
|
|
816 |
by (auto simp:append_rhs_rexp_def)
|
|
817 |
|
94
|
818 |
lemma Arden_keeps_finite:
|
|
819 |
"finite rhs \<Longrightarrow> finite (Arden X rhs)"
|
|
820 |
by (auto simp:Arden_def append_keeps_finite)
|
42
|
821 |
|
|
822 |
lemma append_keeps_nonempty:
|
|
823 |
"rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (append_rhs_rexp rhs r)"
|
|
824 |
apply (auto simp:rhs_nonempty_def append_rhs_rexp_def)
|
|
825 |
by (case_tac x, auto simp:Seq_def)
|
|
826 |
|
|
827 |
lemma nonempty_set_sub:
|
|
828 |
"rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (rhs - A)"
|
|
829 |
by (auto simp:rhs_nonempty_def)
|
|
830 |
|
|
831 |
lemma nonempty_set_union:
|
|
832 |
"\<lbrakk>rhs_nonempty rhs; rhs_nonempty rhs'\<rbrakk> \<Longrightarrow> rhs_nonempty (rhs \<union> rhs')"
|
|
833 |
by (auto simp:rhs_nonempty_def)
|
|
834 |
|
94
|
835 |
lemma Arden_keeps_nonempty:
|
|
836 |
"rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (Arden X rhs)"
|
|
837 |
by (simp only:Arden_def append_keeps_nonempty nonempty_set_sub)
|
42
|
838 |
|
|
839 |
|
94
|
840 |
lemma Subst_keeps_nonempty:
|
|
841 |
"\<lbrakk>rhs_nonempty rhs; rhs_nonempty xrhs\<rbrakk> \<Longrightarrow> rhs_nonempty (Subst rhs X xrhs)"
|
|
842 |
by (simp only:Subst_def append_keeps_nonempty nonempty_set_union nonempty_set_sub)
|
42
|
843 |
|
94
|
844 |
lemma Subst_keeps_eq:
|
42
|
845 |
assumes substor: "X = L xrhs"
|
|
846 |
and finite: "finite rhs"
|
94
|
847 |
shows "L (Subst rhs X xrhs) = L rhs" (is "?Left = ?Right")
|
42
|
848 |
proof-
|
94
|
849 |
def A \<equiv> "L (rhs - {Trn X r | r. Trn X r \<in> rhs})"
|
79
|
850 |
have "?Left = A \<union> L (append_rhs_rexp xrhs (\<Uplus>{r. Trn X r \<in> rhs}))"
|
94
|
851 |
unfolding Subst_def
|
79
|
852 |
unfolding L_rhs_union_distrib[symmetric]
|
|
853 |
by (simp add: A_def)
|
|
854 |
moreover have "?Right = A \<union> L ({Trn X r | r. Trn X r \<in> rhs})"
|
42
|
855 |
proof-
|
94
|
856 |
have "rhs = (rhs - {Trn X r | r. Trn X r \<in> rhs}) \<union> ({Trn X r | r. Trn X r \<in> rhs})" by auto
|
79
|
857 |
thus ?thesis
|
|
858 |
unfolding A_def
|
|
859 |
unfolding L_rhs_union_distrib
|
|
860 |
by simp
|
42
|
861 |
qed
|
79
|
862 |
moreover have "L (append_rhs_rexp xrhs (\<Uplus>{r. Trn X r \<in> rhs})) = L ({Trn X r | r. Trn X r \<in> rhs})"
|
42
|
863 |
using finite substor by (simp only:lang_of_append_rhs lang_of_rexp_of)
|
|
864 |
ultimately show ?thesis by simp
|
|
865 |
qed
|
|
866 |
|
94
|
867 |
lemma Subst_keeps_finite_rhs:
|
|
868 |
"\<lbrakk>finite rhs; finite yrhs\<rbrakk> \<Longrightarrow> finite (Subst rhs Y yrhs)"
|
|
869 |
by (auto simp:Subst_def append_keeps_finite)
|
42
|
870 |
|
94
|
871 |
lemma Subst_all_keeps_finite:
|
42
|
872 |
assumes finite:"finite (ES:: (string set \<times> rhs_item set) set)"
|
94
|
873 |
shows "finite (Subst_all ES Y yrhs)"
|
42
|
874 |
proof -
|
94
|
875 |
have "finite {(Ya, Subst yrhsa Y yrhs) |Ya yrhsa. (Ya, yrhsa) \<in> ES}"
|
42
|
876 |
(is "finite ?A")
|
|
877 |
proof-
|
97
|
878 |
def eqns' \<equiv> "{(Ya::lang, yrhsa) | Ya yrhsa. (Ya, yrhsa) \<in> ES}"
|
|
879 |
def h \<equiv> "\<lambda>(Ya::lang, yrhsa). (Ya, Subst yrhsa Y yrhs)"
|
42
|
880 |
have "finite (h ` eqns')" using finite h_def eqns'_def by auto
|
|
881 |
moreover have "?A = h ` eqns'" by (auto simp:h_def eqns'_def)
|
|
882 |
ultimately show ?thesis by auto
|
|
883 |
qed
|
94
|
884 |
thus ?thesis by (simp add:Subst_all_def)
|
42
|
885 |
qed
|
|
886 |
|
94
|
887 |
lemma Subst_all_keeps_finite_rhs:
|
|
888 |
"\<lbrakk>finite_rhs ES; finite yrhs\<rbrakk> \<Longrightarrow> finite_rhs (Subst_all ES Y yrhs)"
|
|
889 |
by (auto intro:Subst_keeps_finite_rhs simp add:Subst_all_def finite_rhs_def)
|
42
|
890 |
|
|
891 |
lemma append_rhs_keeps_cls:
|
104
|
892 |
"rhss (append_rhs_rexp rhs r) = rhss rhs"
|
|
893 |
apply (auto simp:rhss_def append_rhs_rexp_def)
|
42
|
894 |
apply (case_tac xa, auto simp:image_def)
|
|
895 |
by (rule_tac x = "SEQ ra r" in exI, rule_tac x = "Trn x ra" in bexI, simp+)
|
|
896 |
|
94
|
897 |
lemma Arden_removes_cl:
|
104
|
898 |
"rhss (Arden Y yrhs) = rhss yrhs - {Y}"
|
94
|
899 |
apply (simp add:Arden_def append_rhs_keeps_cls)
|
104
|
900 |
by (auto simp:rhss_def)
|
42
|
901 |
|
103
|
902 |
lemma lhss_keeps_cls:
|
|
903 |
"lhss (Subst_all ES Y yrhs) = lhss ES"
|
|
904 |
by (auto simp:lhss_def Subst_all_def)
|
42
|
905 |
|
94
|
906 |
lemma Subst_updates_cls:
|
104
|
907 |
"X \<notin> rhss xrhs \<Longrightarrow>
|
|
908 |
rhss (Subst rhs X xrhs) = rhss rhs \<union> rhss xrhs - {X}"
|
|
909 |
apply (simp only:Subst_def append_rhs_keeps_cls rhss_union_distrib)
|
|
910 |
by (auto simp:rhss_def)
|
42
|
911 |
|
104
|
912 |
lemma Subst_all_keeps_valid_eqs:
|
|
913 |
assumes sc: "valid_eqs (ES \<union> {(Y, yrhs)})" (is "valid_eqs ?A")
|
|
914 |
shows "valid_eqs (Subst_all ES Y (Arden Y yrhs))"
|
|
915 |
(is "valid_eqs ?B")
|
42
|
916 |
proof-
|
|
917 |
{ fix X xrhs'
|
|
918 |
assume "(X, xrhs') \<in> ?B"
|
|
919 |
then obtain xrhs
|
94
|
920 |
where xrhs_xrhs': "xrhs' = Subst xrhs Y (Arden Y yrhs)"
|
|
921 |
and X_in: "(X, xrhs) \<in> ES" by (simp add:Subst_all_def, blast)
|
104
|
922 |
have "rhss xrhs' \<subseteq> lhss ?B"
|
42
|
923 |
proof-
|
103
|
924 |
have "lhss ?B = lhss ES" by (auto simp add:lhss_def Subst_all_def)
|
104
|
925 |
moreover have "rhss xrhs' \<subseteq> lhss ES"
|
42
|
926 |
proof-
|
104
|
927 |
have "rhss xrhs' \<subseteq>
|
|
928 |
rhss xrhs \<union> rhss (Arden Y yrhs) - {Y}"
|
42
|
929 |
proof-
|
104
|
930 |
have "Y \<notin> rhss (Arden Y yrhs)"
|
94
|
931 |
using Arden_removes_cl by simp
|
|
932 |
thus ?thesis using xrhs_xrhs' by (auto simp:Subst_updates_cls)
|
42
|
933 |
qed
|
104
|
934 |
moreover have "rhss xrhs \<subseteq> lhss ES \<union> {Y}" using X_in sc
|
|
935 |
apply (simp only:valid_eqs_def lhss_union_distrib)
|
103
|
936 |
by (drule_tac x = "(X, xrhs)" in bspec, auto simp:lhss_def)
|
104
|
937 |
moreover have "rhss (Arden Y yrhs) \<subseteq> lhss ES \<union> {Y}"
|
42
|
938 |
using sc
|
104
|
939 |
by (auto simp add:Arden_removes_cl valid_eqs_def lhss_def)
|
42
|
940 |
ultimately show ?thesis by auto
|
|
941 |
qed
|
|
942 |
ultimately show ?thesis by simp
|
|
943 |
qed
|
104
|
944 |
} thus ?thesis by (auto simp only:Subst_all_def valid_eqs_def)
|
42
|
945 |
qed
|
|
946 |
|
96
|
947 |
lemma Subst_all_satisfies_invariant:
|
86
|
948 |
assumes invariant_ES: "invariant (ES \<union> {(Y, yrhs)})"
|
94
|
949 |
shows "invariant (Subst_all ES Y (Arden Y yrhs))"
|
96
|
950 |
proof (rule invariantI)
|
|
951 |
have Y_eq_yrhs: "Y = L yrhs"
|
104
|
952 |
using invariant_ES by (simp only:invariant_def sound_eqs_def, blast)
|
96
|
953 |
have finite_yrhs: "finite yrhs"
|
86
|
954 |
using invariant_ES by (auto simp:invariant_def finite_rhs_def)
|
42
|
955 |
have nonempty_yrhs: "rhs_nonempty yrhs"
|
86
|
956 |
using invariant_ES by (auto simp:invariant_def ardenable_def)
|
104
|
957 |
show "sound_eqs (Subst_all ES Y (Arden Y yrhs))"
|
96
|
958 |
proof-
|
|
959 |
have "Y = L (Arden Y yrhs)"
|
103
|
960 |
using Y_eq_yrhs invariant_ES finite_yrhs
|
|
961 |
using finite_Trn[OF finite_yrhs]
|
|
962 |
apply(rule_tac Arden_keeps_eq)
|
|
963 |
apply(simp_all)
|
|
964 |
unfolding invariant_def ardenable_def rhs_nonempty_def
|
|
965 |
apply(auto)
|
|
966 |
done
|
|
967 |
thus ?thesis using invariant_ES
|
104
|
968 |
unfolding invariant_def finite_rhs_def2 sound_eqs_def Subst_all_def
|
103
|
969 |
by (auto simp add: Subst_keeps_eq simp del: L_rhs.simps)
|
96
|
970 |
qed
|
|
971 |
show "finite (Subst_all ES Y (Arden Y yrhs))"
|
|
972 |
using invariant_ES by (simp add:invariant_def Subst_all_keeps_finite)
|
|
973 |
show "distinct_equas (Subst_all ES Y (Arden Y yrhs))"
|
86
|
974 |
using invariant_ES
|
94
|
975 |
by (auto simp:distinct_equas_def Subst_all_def invariant_def)
|
96
|
976 |
show "ardenable (Subst_all ES Y (Arden Y yrhs))"
|
|
977 |
proof -
|
|
978 |
{ fix X rhs
|
|
979 |
assume "(X, rhs) \<in> ES"
|
|
980 |
hence "rhs_nonempty rhs" using prems invariant_ES
|
97
|
981 |
by (auto simp add:invariant_def ardenable_def)
|
96
|
982 |
with nonempty_yrhs
|
|
983 |
have "rhs_nonempty (Subst rhs Y (Arden Y yrhs))"
|
|
984 |
by (simp add:nonempty_yrhs
|
|
985 |
Subst_keeps_nonempty Arden_keeps_nonempty)
|
|
986 |
} thus ?thesis by (auto simp add:ardenable_def Subst_all_def)
|
|
987 |
qed
|
|
988 |
show "finite_rhs (Subst_all ES Y (Arden Y yrhs))"
|
42
|
989 |
proof-
|
86
|
990 |
have "finite_rhs ES" using invariant_ES
|
|
991 |
by (simp add:invariant_def finite_rhs_def)
|
94
|
992 |
moreover have "finite (Arden Y yrhs)"
|
42
|
993 |
proof -
|
86
|
994 |
have "finite yrhs" using invariant_ES
|
|
995 |
by (auto simp:invariant_def finite_rhs_def)
|
94
|
996 |
thus ?thesis using Arden_keeps_finite by simp
|
42
|
997 |
qed
|
|
998 |
ultimately show ?thesis
|
94
|
999 |
by (simp add:Subst_all_keeps_finite_rhs)
|
42
|
1000 |
qed
|
104
|
1001 |
show "valid_eqs (Subst_all ES Y (Arden Y yrhs))"
|
|
1002 |
using invariant_ES Subst_all_keeps_valid_eqs by (simp add:invariant_def)
|
42
|
1003 |
qed
|
|
1004 |
|
97
|
1005 |
lemma Remove_in_card_measure:
|
|
1006 |
assumes finite: "finite ES"
|
|
1007 |
and in_ES: "(X, rhs) \<in> ES"
|
|
1008 |
shows "(Remove ES X rhs, ES) \<in> measure card"
|
|
1009 |
proof -
|
|
1010 |
def f \<equiv> "\<lambda> x. ((fst x)::lang, Subst (snd x) X (Arden X rhs))"
|
|
1011 |
def ES' \<equiv> "ES - {(X, rhs)}"
|
|
1012 |
have "Subst_all ES' X (Arden X rhs) = f ` ES'"
|
|
1013 |
apply (auto simp: Subst_all_def f_def image_def)
|
|
1014 |
by (rule_tac x = "(Y, yrhs)" in bexI, simp+)
|
|
1015 |
then have "card (Subst_all ES' X (Arden X rhs)) \<le> card ES'"
|
|
1016 |
unfolding ES'_def using finite by (auto intro: card_image_le)
|
|
1017 |
also have "\<dots> < card ES" unfolding ES'_def
|
|
1018 |
using in_ES finite by (rule_tac card_Diff1_less)
|
|
1019 |
finally show "(Remove ES X rhs, ES) \<in> measure card"
|
|
1020 |
unfolding Remove_def ES'_def by simp
|
42
|
1021 |
qed
|
97
|
1022 |
|
42
|
1023 |
|
94
|
1024 |
lemma Subst_all_cls_remains:
|
|
1025 |
"(X, xrhs) \<in> ES \<Longrightarrow> \<exists> xrhs'. (X, xrhs') \<in> (Subst_all ES Y yrhs)"
|
97
|
1026 |
by (auto simp: Subst_all_def)
|
42
|
1027 |
|
|
1028 |
lemma card_noteq_1_has_more:
|
103
|
1029 |
assumes card:"Cond ES"
|
|
1030 |
and e_in: "(X, xrhs) \<in> ES"
|
|
1031 |
and finite: "finite ES"
|
|
1032 |
shows "\<exists>(Y, yrhs) \<in> ES. (X, xrhs) \<noteq> (Y, yrhs)"
|
42
|
1033 |
proof-
|
103
|
1034 |
have "card ES > 1" using card e_in finite
|
|
1035 |
by (cases "card ES") (auto)
|
|
1036 |
then have "card (ES - {(X, xrhs)}) > 0"
|
|
1037 |
using finite e_in by auto
|
|
1038 |
then have "(ES - {(X, xrhs)}) \<noteq> {}" using finite by (rule_tac notI, simp)
|
|
1039 |
then show "\<exists>(Y, yrhs) \<in> ES. (X, xrhs) \<noteq> (Y, yrhs)"
|
|
1040 |
by auto
|
42
|
1041 |
qed
|
|
1042 |
|
97
|
1043 |
lemma iteration_step_measure:
|
91
|
1044 |
assumes Inv_ES: "invariant ES"
|
42
|
1045 |
and X_in_ES: "(X, xrhs) \<in> ES"
|
105
|
1046 |
and Cnd: "Cond ES "
|
97
|
1047 |
shows "(Iter X ES, ES) \<in> measure card"
|
|
1048 |
proof -
|
105
|
1049 |
have fin: "finite ES" using Inv_ES unfolding invariant_def by simp
|
97
|
1050 |
then obtain Y yrhs
|
|
1051 |
where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)"
|
105
|
1052 |
using Cnd X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
|
97
|
1053 |
then have "(Y, yrhs) \<in> ES " "X \<noteq> Y"
|
103
|
1054 |
using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def
|
|
1055 |
by auto
|
97
|
1056 |
then show "(Iter X ES, ES) \<in> measure card"
|
|
1057 |
apply(rule IterI2)
|
|
1058 |
apply(rule Remove_in_card_measure)
|
105
|
1059 |
apply(simp_all add: fin)
|
97
|
1060 |
done
|
|
1061 |
qed
|
|
1062 |
|
|
1063 |
lemma iteration_step_invariant:
|
|
1064 |
assumes Inv_ES: "invariant ES"
|
|
1065 |
and X_in_ES: "(X, xrhs) \<in> ES"
|
105
|
1066 |
and Cnd: "Cond ES"
|
97
|
1067 |
shows "invariant (Iter X ES)"
|
42
|
1068 |
proof -
|
91
|
1069 |
have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def)
|
42
|
1070 |
then obtain Y yrhs
|
|
1071 |
where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)"
|
105
|
1072 |
using Cnd X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
|
103
|
1073 |
then have "(Y, yrhs) \<in> ES" "X \<noteq> Y"
|
|
1074 |
using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def
|
|
1075 |
by auto
|
97
|
1076 |
then show "invariant (Iter X ES)"
|
|
1077 |
proof(rule IterI2)
|
|
1078 |
fix Y yrhs
|
|
1079 |
assume h: "(Y, yrhs) \<in> ES" "X \<noteq> Y"
|
|
1080 |
then have "ES - {(Y, yrhs)} \<union> {(Y, yrhs)} = ES" by auto
|
|
1081 |
then show "invariant (Remove ES Y yrhs)" unfolding Remove_def
|
|
1082 |
using Inv_ES by (rule_tac Subst_all_satisfies_invariant) (simp)
|
42
|
1083 |
qed
|
|
1084 |
qed
|
|
1085 |
|
97
|
1086 |
lemma iteration_step_ex:
|
|
1087 |
assumes Inv_ES: "invariant ES"
|
|
1088 |
and X_in_ES: "(X, xrhs) \<in> ES"
|
105
|
1089 |
and Cnd: "Cond ES"
|
97
|
1090 |
shows "\<exists>xrhs'. (X, xrhs') \<in> (Iter X ES)"
|
|
1091 |
proof -
|
|
1092 |
have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def)
|
|
1093 |
then obtain Y yrhs
|
|
1094 |
where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)"
|
105
|
1095 |
using Cnd X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
|
97
|
1096 |
then have "(Y, yrhs) \<in> ES " "X \<noteq> Y"
|
103
|
1097 |
using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def
|
|
1098 |
by auto
|
97
|
1099 |
then show "\<exists>xrhs'. (X, xrhs') \<in> (Iter X ES)"
|
|
1100 |
apply(rule IterI2)
|
|
1101 |
unfolding Remove_def
|
|
1102 |
apply(rule Subst_all_cls_remains)
|
|
1103 |
using X_in_ES
|
|
1104 |
apply(auto)
|
|
1105 |
done
|
|
1106 |
qed
|
|
1107 |
|
91
|
1108 |
|
|
1109 |
subsubsection {* Conclusion of the proof *}
|
42
|
1110 |
|
103
|
1111 |
lemma Solve:
|
|
1112 |
assumes fin: "finite (UNIV // \<approx>A)"
|
|
1113 |
and X_in: "X \<in> (UNIV // \<approx>A)"
|
104
|
1114 |
shows "\<exists>rhs. Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)} \<and> invariant {(X, rhs)}"
|
91
|
1115 |
proof -
|
104
|
1116 |
def Inv \<equiv> "\<lambda>ES. invariant ES \<and> (\<exists>rhs. (X, rhs) \<in> ES)"
|
103
|
1117 |
have "Inv (Init (UNIV // \<approx>A))" unfolding Inv_def
|
|
1118 |
using fin X_in by (simp add: Init_ES_satisfies_invariant, simp add: Init_def)
|
|
1119 |
moreover
|
|
1120 |
{ fix ES
|
|
1121 |
assume inv: "Inv ES" and crd: "Cond ES"
|
|
1122 |
then have "Inv (Iter X ES)"
|
|
1123 |
unfolding Inv_def
|
|
1124 |
by (auto simp add: iteration_step_invariant iteration_step_ex) }
|
|
1125 |
moreover
|
|
1126 |
{ fix ES
|
|
1127 |
assume "Inv ES" and "\<not> Cond ES"
|
104
|
1128 |
then have "\<exists>rhs'. ES = {(X, rhs')} \<and> invariant ES"
|
103
|
1129 |
unfolding Inv_def invariant_def
|
104
|
1130 |
apply (auto, rule_tac x = rhs in exI)
|
103
|
1131 |
apply (auto dest!: card_Suc_Diff1 simp: card_eq_0_iff)
|
|
1132 |
done
|
104
|
1133 |
then have "\<exists>rhs'. ES = {(X, rhs')} \<and> invariant {(X, rhs')}"
|
103
|
1134 |
by auto }
|
|
1135 |
moreover
|
|
1136 |
have "wf (measure card)" by simp
|
|
1137 |
moreover
|
|
1138 |
{ fix ES
|
|
1139 |
assume inv: "Inv ES" and crd: "Cond ES"
|
|
1140 |
then have "(Iter X ES, ES) \<in> measure card"
|
|
1141 |
unfolding Inv_def
|
97
|
1142 |
apply(clarify)
|
103
|
1143 |
apply(rule_tac iteration_step_measure)
|
97
|
1144 |
apply(auto)
|
103
|
1145 |
done }
|
|
1146 |
ultimately
|
104
|
1147 |
show "\<exists>rhs. Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)} \<and> invariant {(X, rhs)}"
|
103
|
1148 |
unfolding Solve_def by (rule while_rule)
|
42
|
1149 |
qed
|
91
|
1150 |
|
42
|
1151 |
lemma last_cl_exists_rexp:
|
91
|
1152 |
assumes Inv_ES: "invariant {(X, xrhs)}"
|
96
|
1153 |
shows "\<exists>r::rexp. L r = X"
|
42
|
1154 |
proof-
|
94
|
1155 |
def A \<equiv> "Arden X xrhs"
|
105
|
1156 |
have "rhss xrhs \<subseteq> {X}" using Inv_ES
|
|
1157 |
unfolding valid_eqs_def invariant_def rhss_def lhss_def
|
|
1158 |
by auto
|
|
1159 |
then have "rhss A = {}" unfolding A_def
|
|
1160 |
by (simp add: Arden_removes_cl)
|
|
1161 |
then have eq: "{Lam r | r. Lam r \<in> A} = A" unfolding rhss_def
|
|
1162 |
by (auto, case_tac x, auto)
|
|
1163 |
|
96
|
1164 |
have "finite A" using Inv_ES unfolding A_def invariant_def finite_rhs_def
|
|
1165 |
using Arden_keeps_finite by auto
|
105
|
1166 |
then have fin: "finite {r. Lam r \<in> A}" by (rule finite_Lam)
|
|
1167 |
|
|
1168 |
have "X = L xrhs" using Inv_ES unfolding invariant_def sound_eqs_def
|
|
1169 |
by simp
|
|
1170 |
then have "X = L A" using Inv_ES
|
|
1171 |
unfolding A_def invariant_def ardenable_def finite_rhs_def rhs_nonempty_def
|
|
1172 |
by (rule_tac Arden_keeps_eq) (simp_all add: finite_Trn)
|
|
1173 |
then have "X = L {Lam r | r. Lam r \<in> A}" using eq by simp
|
|
1174 |
then have "X = L (\<Uplus>{r. Lam r \<in> A})" using fin by auto
|
96
|
1175 |
then show "\<exists>r::rexp. L r = X" by blast
|
42
|
1176 |
qed
|
91
|
1177 |
|
42
|
1178 |
lemma every_eqcl_has_reg:
|
96
|
1179 |
assumes finite_CS: "finite (UNIV // \<approx>A)"
|
|
1180 |
and X_in_CS: "X \<in> (UNIV // \<approx>A)"
|
|
1181 |
shows "\<exists>r::rexp. L r = X"
|
42
|
1182 |
proof -
|
103
|
1183 |
from finite_CS X_in_CS
|
|
1184 |
obtain xrhs where "invariant {(X, xrhs)}"
|
|
1185 |
using Solve by metis
|
96
|
1186 |
then show "\<exists>r::rexp. L r = X"
|
103
|
1187 |
using last_cl_exists_rexp by auto
|
42
|
1188 |
qed
|
|
1189 |
|
96
|
1190 |
lemma bchoice_finite_set:
|
|
1191 |
assumes a: "\<forall>x \<in> S. \<exists>y. x = f y"
|
|
1192 |
and b: "finite S"
|
|
1193 |
shows "\<exists>ys. (\<Union> S) = \<Union>(f ` ys) \<and> finite ys"
|
|
1194 |
using bchoice[OF a] b
|
|
1195 |
apply(erule_tac exE)
|
|
1196 |
apply(rule_tac x="fa ` S" in exI)
|
|
1197 |
apply(auto)
|
|
1198 |
done
|
|
1199 |
|
|
1200 |
theorem Myhill_Nerode1:
|
70
|
1201 |
assumes finite_CS: "finite (UNIV // \<approx>A)"
|
|
1202 |
shows "\<exists>r::rexp. A = L r"
|
42
|
1203 |
proof -
|
105
|
1204 |
have fin: "finite (finals A)"
|
96
|
1205 |
using finals_in_partitions finite_CS by (rule finite_subset)
|
|
1206 |
have "\<forall>X \<in> (UNIV // \<approx>A). \<exists>r::rexp. X = L r"
|
42
|
1207 |
using finite_CS every_eqcl_has_reg by blast
|
96
|
1208 |
then have a: "\<forall>X \<in> finals A. \<exists>r::rexp. X = L r"
|
|
1209 |
using finals_in_partitions by auto
|
|
1210 |
then obtain rs::"rexp set" where "\<Union> (finals A) = \<Union>(L ` rs)" "finite rs"
|
105
|
1211 |
using fin by (auto dest: bchoice_finite_set)
|
96
|
1212 |
then have "A = L (\<Uplus>rs)"
|
|
1213 |
unfolding lang_is_union_of_finals[symmetric] by simp
|
|
1214 |
then show "\<exists>r::rexp. A = L r" by blast
|
42
|
1215 |
qed
|
|
1216 |
|
96
|
1217 |
|
42
|
1218 |
end |