1 (* Author: Tobias Nipkow, Alex Krauss, Christian Urban *) |
|
2 |
|
3 section "Regular sets" |
|
4 |
|
5 theory Regular_Set |
|
6 imports Main |
|
7 begin |
|
8 |
|
9 type_synonym 'a lang = "'a list set" |
|
10 |
|
11 definition conc :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a lang" (infixr "@@" 75) where |
|
12 "A @@ B = {xs@ys | xs ys. xs:A & ys:B}" |
|
13 |
|
14 text {* checks the code preprocessor for set comprehensions *} |
|
15 export_code conc checking SML |
|
16 |
|
17 overloading lang_pow == "compow :: nat \<Rightarrow> 'a lang \<Rightarrow> 'a lang" |
|
18 begin |
|
19 primrec lang_pow :: "nat \<Rightarrow> 'a lang \<Rightarrow> 'a lang" where |
|
20 "lang_pow 0 A = {[]}" | |
|
21 "lang_pow (Suc n) A = A @@ (lang_pow n A)" |
|
22 end |
|
23 |
|
24 text {* for code generation *} |
|
25 |
|
26 definition lang_pow :: "nat \<Rightarrow> 'a lang \<Rightarrow> 'a lang" where |
|
27 lang_pow_code_def [code_abbrev]: "lang_pow = compow" |
|
28 |
|
29 lemma [code]: |
|
30 "lang_pow (Suc n) A = A @@ (lang_pow n A)" |
|
31 "lang_pow 0 A = {[]}" |
|
32 by (simp_all add: lang_pow_code_def) |
|
33 |
|
34 hide_const (open) lang_pow |
|
35 |
|
36 definition star :: "'a lang \<Rightarrow> 'a lang" where |
|
37 "star A = (\<Union>n. A ^^ n)" |
|
38 |
|
39 |
|
40 subsection{* @{term "op @@"} *} |
|
41 |
|
42 lemma concI[simp,intro]: "u : A \<Longrightarrow> v : B \<Longrightarrow> u@v : A @@ B" |
|
43 by (auto simp add: conc_def) |
|
44 |
|
45 lemma concE[elim]: |
|
46 assumes "w \<in> A @@ B" |
|
47 obtains u v where "u \<in> A" "v \<in> B" "w = u@v" |
|
48 using assms by (auto simp: conc_def) |
|
49 |
|
50 lemma conc_mono: "A \<subseteq> C \<Longrightarrow> B \<subseteq> D \<Longrightarrow> A @@ B \<subseteq> C @@ D" |
|
51 by (auto simp: conc_def) |
|
52 |
|
53 lemma conc_empty[simp]: shows "{} @@ A = {}" and "A @@ {} = {}" |
|
54 by auto |
|
55 |
|
56 lemma conc_epsilon[simp]: shows "{[]} @@ A = A" and "A @@ {[]} = A" |
|
57 by (simp_all add:conc_def) |
|
58 |
|
59 lemma conc_assoc: "(A @@ B) @@ C = A @@ (B @@ C)" |
|
60 by (auto elim!: concE) (simp only: append_assoc[symmetric] concI) |
|
61 |
|
62 lemma conc_Un_distrib: |
|
63 shows "A @@ (B \<union> C) = A @@ B \<union> A @@ C" |
|
64 and "(A \<union> B) @@ C = A @@ C \<union> B @@ C" |
|
65 by auto |
|
66 |
|
67 lemma conc_UNION_distrib: |
|
68 shows "A @@ UNION I M = UNION I (%i. A @@ M i)" |
|
69 and "UNION I M @@ A = UNION I (%i. M i @@ A)" |
|
70 by auto |
|
71 |
|
72 lemma conc_subset_lists: "A \<subseteq> lists S \<Longrightarrow> B \<subseteq> lists S \<Longrightarrow> A @@ B \<subseteq> lists S" |
|
73 by(fastforce simp: conc_def in_lists_conv_set) |
|
74 |
|
75 lemma Nil_in_conc[simp]: "[] \<in> A @@ B \<longleftrightarrow> [] \<in> A \<and> [] \<in> B" |
|
76 by (metis append_is_Nil_conv concE concI) |
|
77 |
|
78 lemma concI_if_Nil1: "[] \<in> A \<Longrightarrow> xs : B \<Longrightarrow> xs \<in> A @@ B" |
|
79 by (metis append_Nil concI) |
|
80 |
|
81 lemma conc_Diff_if_Nil1: "[] \<in> A \<Longrightarrow> A @@ B = (A - {[]}) @@ B \<union> B" |
|
82 by (fastforce elim: concI_if_Nil1) |
|
83 |
|
84 lemma concI_if_Nil2: "[] \<in> B \<Longrightarrow> xs : A \<Longrightarrow> xs \<in> A @@ B" |
|
85 by (metis append_Nil2 concI) |
|
86 |
|
87 lemma conc_Diff_if_Nil2: "[] \<in> B \<Longrightarrow> A @@ B = A @@ (B - {[]}) \<union> A" |
|
88 by (fastforce elim: concI_if_Nil2) |
|
89 |
|
90 lemma singleton_in_conc: |
|
91 "[x] : A @@ B \<longleftrightarrow> [x] : A \<and> [] : B \<or> [] : A \<and> [x] : B" |
|
92 by (fastforce simp: Cons_eq_append_conv append_eq_Cons_conv |
|
93 conc_Diff_if_Nil1 conc_Diff_if_Nil2) |
|
94 |
|
95 |
|
96 subsection{* @{term "A ^^ n"} *} |
|
97 |
|
98 lemma lang_pow_add: "A ^^ (n + m) = A ^^ n @@ A ^^ m" |
|
99 by (induct n) (auto simp: conc_assoc) |
|
100 |
|
101 lemma lang_pow_empty: "{} ^^ n = (if n = 0 then {[]} else {})" |
|
102 by (induct n) auto |
|
103 |
|
104 lemma lang_pow_empty_Suc[simp]: "({}::'a lang) ^^ Suc n = {}" |
|
105 by (simp add: lang_pow_empty) |
|
106 |
|
107 lemma conc_pow_comm: |
|
108 shows "A @@ (A ^^ n) = (A ^^ n) @@ A" |
|
109 by (induct n) (simp_all add: conc_assoc[symmetric]) |
|
110 |
|
111 lemma length_lang_pow_ub: |
|
112 "ALL w : A. length w \<le> k \<Longrightarrow> w : A^^n \<Longrightarrow> length w \<le> k*n" |
|
113 by(induct n arbitrary: w) (fastforce simp: conc_def)+ |
|
114 |
|
115 lemma length_lang_pow_lb: |
|
116 "ALL w : A. length w \<ge> k \<Longrightarrow> w : A^^n \<Longrightarrow> length w \<ge> k*n" |
|
117 by(induct n arbitrary: w) (fastforce simp: conc_def)+ |
|
118 |
|
119 lemma lang_pow_subset_lists: "A \<subseteq> lists S \<Longrightarrow> A ^^ n \<subseteq> lists S" |
|
120 by(induction n)(auto simp: conc_subset_lists[OF assms]) |
|
121 |
|
122 |
|
123 subsection{* @{const star} *} |
|
124 |
|
125 lemma star_subset_lists: "A \<subseteq> lists S \<Longrightarrow> star A \<subseteq> lists S" |
|
126 unfolding star_def by(blast dest: lang_pow_subset_lists) |
|
127 |
|
128 lemma star_if_lang_pow[simp]: "w : A ^^ n \<Longrightarrow> w : star A" |
|
129 by (auto simp: star_def) |
|
130 |
|
131 lemma Nil_in_star[iff]: "[] : star A" |
|
132 proof (rule star_if_lang_pow) |
|
133 show "[] : A ^^ 0" by simp |
|
134 qed |
|
135 |
|
136 lemma star_if_lang[simp]: assumes "w : A" shows "w : star A" |
|
137 proof (rule star_if_lang_pow) |
|
138 show "w : A ^^ 1" using `w : A` by simp |
|
139 qed |
|
140 |
|
141 lemma append_in_starI[simp]: |
|
142 assumes "u : star A" and "v : star A" shows "u@v : star A" |
|
143 proof - |
|
144 from `u : star A` obtain m where "u : A ^^ m" by (auto simp: star_def) |
|
145 moreover |
|
146 from `v : star A` obtain n where "v : A ^^ n" by (auto simp: star_def) |
|
147 ultimately have "u@v : A ^^ (m+n)" by (simp add: lang_pow_add) |
|
148 thus ?thesis by simp |
|
149 qed |
|
150 |
|
151 lemma conc_star_star: "star A @@ star A = star A" |
|
152 by (auto simp: conc_def) |
|
153 |
|
154 lemma conc_star_comm: |
|
155 shows "A @@ star A = star A @@ A" |
|
156 unfolding star_def conc_pow_comm conc_UNION_distrib |
|
157 by simp |
|
158 |
|
159 lemma star_induct[consumes 1, case_names Nil append, induct set: star]: |
|
160 assumes "w : star A" |
|
161 and "P []" |
|
162 and step: "!!u v. u : A \<Longrightarrow> v : star A \<Longrightarrow> P v \<Longrightarrow> P (u@v)" |
|
163 shows "P w" |
|
164 proof - |
|
165 { fix n have "w : A ^^ n \<Longrightarrow> P w" |
|
166 by (induct n arbitrary: w) (auto intro: `P []` step star_if_lang_pow) } |
|
167 with `w : star A` show "P w" by (auto simp: star_def) |
|
168 qed |
|
169 |
|
170 lemma star_empty[simp]: "star {} = {[]}" |
|
171 by (auto elim: star_induct) |
|
172 |
|
173 lemma star_epsilon[simp]: "star {[]} = {[]}" |
|
174 by (auto elim: star_induct) |
|
175 |
|
176 lemma star_idemp[simp]: "star (star A) = star A" |
|
177 by (auto elim: star_induct) |
|
178 |
|
179 lemma star_unfold_left: "star A = A @@ star A \<union> {[]}" (is "?L = ?R") |
|
180 proof |
|
181 show "?L \<subseteq> ?R" by (rule, erule star_induct) auto |
|
182 qed auto |
|
183 |
|
184 lemma concat_in_star: "set ws \<subseteq> A \<Longrightarrow> concat ws : star A" |
|
185 by (induct ws) simp_all |
|
186 |
|
187 lemma in_star_iff_concat: |
|
188 "w : star A = (EX ws. set ws \<subseteq> A & w = concat ws)" |
|
189 (is "_ = (EX ws. ?R w ws)") |
|
190 proof |
|
191 assume "w : star A" thus "EX ws. ?R w ws" |
|
192 proof induct |
|
193 case Nil have "?R [] []" by simp |
|
194 thus ?case .. |
|
195 next |
|
196 case (append u v) |
|
197 moreover |
|
198 then obtain ws where "set ws \<subseteq> A \<and> v = concat ws" by blast |
|
199 ultimately have "?R (u@v) (u#ws)" by auto |
|
200 thus ?case .. |
|
201 qed |
|
202 next |
|
203 assume "EX us. ?R w us" thus "w : star A" |
|
204 by (auto simp: concat_in_star) |
|
205 qed |
|
206 |
|
207 lemma star_conv_concat: "star A = {concat ws|ws. set ws \<subseteq> A}" |
|
208 by (fastforce simp: in_star_iff_concat) |
|
209 |
|
210 lemma star_insert_eps[simp]: "star (insert [] A) = star(A)" |
|
211 proof- |
|
212 { fix us |
|
213 have "set us \<subseteq> insert [] A \<Longrightarrow> EX vs. concat us = concat vs \<and> set vs \<subseteq> A" |
|
214 (is "?P \<Longrightarrow> EX vs. ?Q vs") |
|
215 proof |
|
216 let ?vs = "filter (%u. u \<noteq> []) us" |
|
217 show "?P \<Longrightarrow> ?Q ?vs" by (induct us) auto |
|
218 qed |
|
219 } thus ?thesis by (auto simp: star_conv_concat) |
|
220 qed |
|
221 |
|
222 lemma star_unfold_left_Nil: "star A = (A - {[]}) @@ (star A) \<union> {[]}" |
|
223 by (metis insert_Diff_single star_insert_eps star_unfold_left) |
|
224 |
|
225 lemma star_Diff_Nil_fold: "(A - {[]}) @@ star A = star A - {[]}" |
|
226 proof - |
|
227 have "[] \<notin> (A - {[]}) @@ star A" by simp |
|
228 thus ?thesis using star_unfold_left_Nil by blast |
|
229 qed |
|
230 |
|
231 lemma star_decom: |
|
232 assumes a: "x \<in> star A" "x \<noteq> []" |
|
233 shows "\<exists>a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> star A" |
|
234 using a by (induct rule: star_induct) (blast)+ |
|
235 |
|
236 |
|
237 subsection {* Left-Quotients of languages *} |
|
238 |
|
239 definition Deriv :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang" |
|
240 where "Deriv x A = { xs. x#xs \<in> A }" |
|
241 |
|
242 definition Derivs :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang" |
|
243 where "Derivs xs A = { ys. xs @ ys \<in> A }" |
|
244 |
|
245 abbreviation |
|
246 Derivss :: "'a list \<Rightarrow> 'a lang set \<Rightarrow> 'a lang" |
|
247 where |
|
248 "Derivss s As \<equiv> \<Union> (Derivs s ` As)" |
|
249 |
|
250 |
|
251 lemma Deriv_empty[simp]: "Deriv a {} = {}" |
|
252 and Deriv_epsilon[simp]: "Deriv a {[]} = {}" |
|
253 and Deriv_char[simp]: "Deriv a {[b]} = (if a = b then {[]} else {})" |
|
254 and Deriv_union[simp]: "Deriv a (A \<union> B) = Deriv a A \<union> Deriv a B" |
|
255 and Deriv_inter[simp]: "Deriv a (A \<inter> B) = Deriv a A \<inter> Deriv a B" |
|
256 and Deriv_compl[simp]: "Deriv a (-A) = - Deriv a A" |
|
257 and Deriv_Union[simp]: "Deriv a (Union M) = Union(Deriv a ` M)" |
|
258 and Deriv_UN[simp]: "Deriv a (UN x:I. S x) = (UN x:I. Deriv a (S x))" |
|
259 by (auto simp: Deriv_def) |
|
260 |
|
261 lemma Der_conc [simp]: |
|
262 shows "Deriv c (A @@ B) = (Deriv c A) @@ B \<union> (if [] \<in> A then Deriv c B else {})" |
|
263 unfolding Deriv_def conc_def |
|
264 by (auto simp add: Cons_eq_append_conv) |
|
265 |
|
266 lemma Deriv_star [simp]: |
|
267 shows "Deriv c (star A) = (Deriv c A) @@ star A" |
|
268 proof - |
|
269 have "Deriv c (star A) = Deriv c ({[]} \<union> A @@ star A)" |
|
270 by (metis star_unfold_left sup.commute) |
|
271 also have "... = Deriv c (A @@ star A)" |
|
272 unfolding Deriv_union by (simp) |
|
273 also have "... = (Deriv c A) @@ (star A) \<union> (if [] \<in> A then Deriv c (star A) else {})" |
|
274 by simp |
|
275 also have "... = (Deriv c A) @@ star A" |
|
276 unfolding conc_def Deriv_def |
|
277 using star_decom by (force simp add: Cons_eq_append_conv) |
|
278 finally show "Deriv c (star A) = (Deriv c A) @@ star A" . |
|
279 qed |
|
280 |
|
281 lemma Deriv_diff[simp]: |
|
282 shows "Deriv c (A - B) = Deriv c A - Deriv c B" |
|
283 by(auto simp add: Deriv_def) |
|
284 |
|
285 lemma Deriv_lists[simp]: "c : S \<Longrightarrow> Deriv c (lists S) = lists S" |
|
286 by(auto simp add: Deriv_def) |
|
287 |
|
288 lemma Derivs_simps [simp]: |
|
289 shows "Derivs [] A = A" |
|
290 and "Derivs (c # s) A = Derivs s (Deriv c A)" |
|
291 and "Derivs (s1 @ s2) A = Derivs s2 (Derivs s1 A)" |
|
292 unfolding Derivs_def Deriv_def by auto |
|
293 |
|
294 lemma in_fold_Deriv: "v \<in> fold Deriv w L \<longleftrightarrow> w @ v \<in> L" |
|
295 by (induct w arbitrary: L) (simp_all add: Deriv_def) |
|
296 |
|
297 lemma Derivs_alt_def: "Derivs w L = fold Deriv w L" |
|
298 by (induct w arbitrary: L) simp_all |
|
299 |
|
300 |
|
301 subsection {* Shuffle product *} |
|
302 |
|
303 fun shuffle where |
|
304 "shuffle [] ys = {ys}" |
|
305 | "shuffle xs [] = {xs}" |
|
306 | "shuffle (x # xs) (y # ys) = |
|
307 {x # w | w . w \<in> shuffle xs (y # ys)} \<union> |
|
308 {y # w | w . w \<in> shuffle (x # xs) ys}" |
|
309 |
|
310 lemma shuffle_empty2[simp]: "shuffle xs [] = {xs}" |
|
311 by (cases xs) auto |
|
312 |
|
313 lemma Nil_in_shuffle[simp]: "[] \<in> shuffle xs ys \<longleftrightarrow> xs = [] \<and> ys = []" |
|
314 by (induct xs ys rule: shuffle.induct) auto |
|
315 |
|
316 definition Shuffle (infixr "\<parallel>" 80) where |
|
317 "Shuffle A B = \<Union>{shuffle xs ys | xs ys. xs \<in> A \<and> ys \<in> B}" |
|
318 |
|
319 lemma shuffleE: |
|
320 "zs \<in> shuffle xs ys \<Longrightarrow> |
|
321 (zs = xs \<Longrightarrow> ys = [] \<Longrightarrow> P) \<Longrightarrow> |
|
322 (zs = ys \<Longrightarrow> xs = [] \<Longrightarrow> P) \<Longrightarrow> |
|
323 (\<And>x xs' z zs'. xs = x # xs' \<Longrightarrow> zs = z # zs' \<Longrightarrow> x = z \<Longrightarrow> zs' \<in> shuffle xs' ys \<Longrightarrow> P) \<Longrightarrow> |
|
324 (\<And>y ys' z zs'. ys = y # ys' \<Longrightarrow> zs = z # zs' \<Longrightarrow> y = z \<Longrightarrow> zs' \<in> shuffle xs ys' \<Longrightarrow> P) \<Longrightarrow> P" |
|
325 by (induct xs ys rule: shuffle.induct) auto |
|
326 |
|
327 lemma Cons_in_shuffle_iff: |
|
328 "z # zs \<in> shuffle xs ys \<longleftrightarrow> |
|
329 (xs \<noteq> [] \<and> hd xs = z \<and> zs \<in> shuffle (tl xs) ys \<or> |
|
330 ys \<noteq> [] \<and> hd ys = z \<and> zs \<in> shuffle xs (tl ys))" |
|
331 by (induct xs ys rule: shuffle.induct) auto |
|
332 |
|
333 lemma Deriv_Shuffle[simp]: |
|
334 "Deriv a (A \<parallel> B) = Deriv a A \<parallel> B \<union> A \<parallel> Deriv a B" |
|
335 unfolding Shuffle_def Deriv_def by (fastforce simp: Cons_in_shuffle_iff neq_Nil_conv) |
|
336 |
|
337 lemma shuffle_subset_lists: |
|
338 assumes "A \<subseteq> lists S" "B \<subseteq> lists S" |
|
339 shows "A \<parallel> B \<subseteq> lists S" |
|
340 unfolding Shuffle_def proof safe |
|
341 fix x and zs xs ys :: "'a list" |
|
342 assume zs: "zs \<in> shuffle xs ys" "x \<in> set zs" and "xs \<in> A" "ys \<in> B" |
|
343 with assms have "xs \<in> lists S" "ys \<in> lists S" by auto |
|
344 with zs show "x \<in> S" by (induct xs ys arbitrary: zs rule: shuffle.induct) auto |
|
345 qed |
|
346 |
|
347 lemma Nil_in_Shuffle[simp]: "[] \<in> A \<parallel> B \<longleftrightarrow> [] \<in> A \<and> [] \<in> B" |
|
348 unfolding Shuffle_def by force |
|
349 |
|
350 lemma shuffle_Un_distrib: |
|
351 shows "A \<parallel> (B \<union> C) = A \<parallel> B \<union> A \<parallel> C" |
|
352 and "A \<parallel> (B \<union> C) = A \<parallel> B \<union> A \<parallel> C" |
|
353 unfolding Shuffle_def by fast+ |
|
354 |
|
355 lemma shuffle_UNION_distrib: |
|
356 shows "A \<parallel> UNION I M = UNION I (%i. A \<parallel> M i)" |
|
357 and "UNION I M \<parallel> A = UNION I (%i. M i \<parallel> A)" |
|
358 unfolding Shuffle_def by fast+ |
|
359 |
|
360 lemma Shuffle_empty[simp]: |
|
361 "A \<parallel> {} = {}" |
|
362 "{} \<parallel> B = {}" |
|
363 unfolding Shuffle_def by auto |
|
364 |
|
365 lemma Shuffle_eps[simp]: |
|
366 "A \<parallel> {[]} = A" |
|
367 "{[]} \<parallel> B = B" |
|
368 unfolding Shuffle_def by auto |
|
369 |
|
370 |
|
371 subsection {* Arden's Lemma *} |
|
372 |
|
373 lemma arden_helper: |
|
374 assumes eq: "X = A @@ X \<union> B" |
|
375 shows "X = (A ^^ Suc n) @@ X \<union> (\<Union>m\<le>n. (A ^^ m) @@ B)" |
|
376 proof (induct n) |
|
377 case 0 |
|
378 show "X = (A ^^ Suc 0) @@ X \<union> (\<Union>m\<le>0. (A ^^ m) @@ B)" |
|
379 using eq by simp |
|
380 next |
|
381 case (Suc n) |
|
382 have ih: "X = (A ^^ Suc n) @@ X \<union> (\<Union>m\<le>n. (A ^^ m) @@ B)" by fact |
|
383 also have "\<dots> = (A ^^ Suc n) @@ (A @@ X \<union> B) \<union> (\<Union>m\<le>n. (A ^^ m) @@ B)" using eq by simp |
|
384 also have "\<dots> = (A ^^ Suc (Suc n)) @@ X \<union> ((A ^^ Suc n) @@ B) \<union> (\<Union>m\<le>n. (A ^^ m) @@ B)" |
|
385 by (simp add: conc_Un_distrib conc_assoc[symmetric] conc_pow_comm) |
|
386 also have "\<dots> = (A ^^ Suc (Suc n)) @@ X \<union> (\<Union>m\<le>Suc n. (A ^^ m) @@ B)" |
|
387 by (auto simp add: le_Suc_eq) |
|
388 finally show "X = (A ^^ Suc (Suc n)) @@ X \<union> (\<Union>m\<le>Suc n. (A ^^ m) @@ B)" . |
|
389 qed |
|
390 |
|
391 lemma Arden: |
|
392 assumes "[] \<notin> A" |
|
393 shows "X = A @@ X \<union> B \<longleftrightarrow> X = star A @@ B" |
|
394 proof |
|
395 assume eq: "X = A @@ X \<union> B" |
|
396 { fix w assume "w : X" |
|
397 let ?n = "size w" |
|
398 from `[] \<notin> A` have "ALL u : A. length u \<ge> 1" |
|
399 by (metis Suc_eq_plus1 add_leD2 le_0_eq length_0_conv not_less_eq_eq) |
|
400 hence "ALL u : A^^(?n+1). length u \<ge> ?n+1" |
|
401 by (metis length_lang_pow_lb nat_mult_1) |
|
402 hence "ALL u : A^^(?n+1)@@X. length u \<ge> ?n+1" |
|
403 by(auto simp only: conc_def length_append) |
|
404 hence "w \<notin> A^^(?n+1)@@X" by auto |
|
405 hence "w : star A @@ B" using `w : X` using arden_helper[OF eq, where n="?n"] |
|
406 by (auto simp add: star_def conc_UNION_distrib) |
|
407 } moreover |
|
408 { fix w assume "w : star A @@ B" |
|
409 hence "EX n. w : A^^n @@ B" by(auto simp: conc_def star_def) |
|
410 hence "w : X" using arden_helper[OF eq] by blast |
|
411 } ultimately show "X = star A @@ B" by blast |
|
412 next |
|
413 assume eq: "X = star A @@ B" |
|
414 have "star A = A @@ star A \<union> {[]}" |
|
415 by (rule star_unfold_left) |
|
416 then have "star A @@ B = (A @@ star A \<union> {[]}) @@ B" |
|
417 by metis |
|
418 also have "\<dots> = (A @@ star A) @@ B \<union> B" |
|
419 unfolding conc_Un_distrib by simp |
|
420 also have "\<dots> = A @@ (star A @@ B) \<union> B" |
|
421 by (simp only: conc_assoc) |
|
422 finally show "X = A @@ X \<union> B" |
|
423 using eq by blast |
|
424 qed |
|
425 |
|
426 |
|
427 lemma reversed_arden_helper: |
|
428 assumes eq: "X = X @@ A \<union> B" |
|
429 shows "X = X @@ (A ^^ Suc n) \<union> (\<Union>m\<le>n. B @@ (A ^^ m))" |
|
430 proof (induct n) |
|
431 case 0 |
|
432 show "X = X @@ (A ^^ Suc 0) \<union> (\<Union>m\<le>0. B @@ (A ^^ m))" |
|
433 using eq by simp |
|
434 next |
|
435 case (Suc n) |
|
436 have ih: "X = X @@ (A ^^ Suc n) \<union> (\<Union>m\<le>n. B @@ (A ^^ m))" by fact |
|
437 also have "\<dots> = (X @@ A \<union> B) @@ (A ^^ Suc n) \<union> (\<Union>m\<le>n. B @@ (A ^^ m))" using eq by simp |
|
438 also have "\<dots> = X @@ (A ^^ Suc (Suc n)) \<union> (B @@ (A ^^ Suc n)) \<union> (\<Union>m\<le>n. B @@ (A ^^ m))" |
|
439 by (simp add: conc_Un_distrib conc_assoc) |
|
440 also have "\<dots> = X @@ (A ^^ Suc (Suc n)) \<union> (\<Union>m\<le>Suc n. B @@ (A ^^ m))" |
|
441 by (auto simp add: le_Suc_eq) |
|
442 finally show "X = X @@ (A ^^ Suc (Suc n)) \<union> (\<Union>m\<le>Suc n. B @@ (A ^^ m))" . |
|
443 qed |
|
444 |
|
445 theorem reversed_Arden: |
|
446 assumes nemp: "[] \<notin> A" |
|
447 shows "X = X @@ A \<union> B \<longleftrightarrow> X = B @@ star A" |
|
448 proof |
|
449 assume eq: "X = X @@ A \<union> B" |
|
450 { fix w assume "w : X" |
|
451 let ?n = "size w" |
|
452 from `[] \<notin> A` have "ALL u : A. length u \<ge> 1" |
|
453 by (metis Suc_eq_plus1 add_leD2 le_0_eq length_0_conv not_less_eq_eq) |
|
454 hence "ALL u : A^^(?n+1). length u \<ge> ?n+1" |
|
455 by (metis length_lang_pow_lb nat_mult_1) |
|
456 hence "ALL u : X @@ A^^(?n+1). length u \<ge> ?n+1" |
|
457 by(auto simp only: conc_def length_append) |
|
458 hence "w \<notin> X @@ A^^(?n+1)" by auto |
|
459 hence "w : B @@ star A" using `w : X` using reversed_arden_helper[OF eq, where n="?n"] |
|
460 by (auto simp add: star_def conc_UNION_distrib) |
|
461 } moreover |
|
462 { fix w assume "w : B @@ star A" |
|
463 hence "EX n. w : B @@ A^^n" by (auto simp: conc_def star_def) |
|
464 hence "w : X" using reversed_arden_helper[OF eq] by blast |
|
465 } ultimately show "X = B @@ star A" by blast |
|
466 next |
|
467 assume eq: "X = B @@ star A" |
|
468 have "star A = {[]} \<union> star A @@ A" |
|
469 unfolding conc_star_comm[symmetric] |
|
470 by(metis Un_commute star_unfold_left) |
|
471 then have "B @@ star A = B @@ ({[]} \<union> star A @@ A)" |
|
472 by metis |
|
473 also have "\<dots> = B \<union> B @@ (star A @@ A)" |
|
474 unfolding conc_Un_distrib by simp |
|
475 also have "\<dots> = B \<union> (B @@ star A) @@ A" |
|
476 by (simp only: conc_assoc) |
|
477 finally show "X = X @@ A \<union> B" |
|
478 using eq by blast |
|
479 qed |
|
480 |
|
481 end |
|