3 "~~/src/HOL/Library/List_Prefix" |
3 "~~/src/HOL/Library/List_Prefix" |
4 begin |
4 begin |
5 |
5 |
6 section {* Direction @{text "regular language \<Rightarrow> finite partition"} *} |
6 section {* Direction @{text "regular language \<Rightarrow> finite partition"} *} |
7 |
7 |
8 definition |
8 definition |
9 str_eq :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<approx>_ _") |
9 tag_eq :: "('a list \<Rightarrow> 'b) \<Rightarrow> ('a list \<times> 'a list) set" ("=_=") |
10 where |
10 where |
11 "x \<approx>A y \<equiv> (x, y) \<in> (\<approx>A)" |
11 "=tag= \<equiv> {(x, y). tag x = tag y}" |
12 |
12 |
13 lemma str_eq_def2: |
13 abbreviation |
14 shows "\<approx>A = {(x, y) | x y. x \<approx>A y}" |
14 tag_eq_applied :: "'a list \<Rightarrow> ('a list \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> bool" ("_ =_= _") |
|
15 where |
|
16 "x =tag= y \<equiv> (x, y) \<in> =tag=" |
|
17 |
|
18 lemma test: |
|
19 shows "(\<approx>A) `` {x} = (\<approx>A) `` {y} \<longleftrightarrow> x \<approx>A y" |
15 unfolding str_eq_def |
20 unfolding str_eq_def |
16 by simp |
21 by auto |
17 |
22 |
18 definition |
23 lemma test_refined_intro: |
19 tag_eq_rel :: "('a list \<Rightarrow> 'b) \<Rightarrow> ('a list \<times> 'a list) set" ("=_=") |
24 assumes "\<And>x y z. \<lbrakk>x =tag= y; x @ z \<in> A\<rbrakk> \<Longrightarrow> y @ z \<in> A" |
20 where |
25 shows "=tag= \<subseteq> \<approx>A" |
21 "=tag= \<equiv> {(x, y). tag x = tag y}" |
26 using assms |
|
27 unfolding str_eq_def tag_eq_def |
|
28 apply(clarify, simp (no_asm_use)) |
|
29 by metis |
|
30 |
22 |
31 |
23 lemma finite_eq_tag_rel: |
32 lemma finite_eq_tag_rel: |
24 assumes rng_fnt: "finite (range tag)" |
33 assumes rng_fnt: "finite (range tag)" |
25 shows "finite (UNIV // =tag=)" |
34 shows "finite (UNIV // =tag=)" |
26 proof - |
35 proof - |
99 shows "finite (UNIV // \<approx>A)" |
108 shows "finite (UNIV // \<approx>A)" |
100 proof (rule_tac refined_partition_finite [of "=tag="]) |
109 proof (rule_tac refined_partition_finite [of "=tag="]) |
101 show "finite (UNIV // =tag=)" by (rule finite_eq_tag_rel[OF rng_fnt]) |
110 show "finite (UNIV // =tag=)" by (rule finite_eq_tag_rel[OF rng_fnt]) |
102 next |
111 next |
103 from same_tag_eqvt |
112 from same_tag_eqvt |
104 show "=tag= \<subseteq> \<approx>A" unfolding tag_eq_rel_def str_eq_def |
113 show "=tag= \<subseteq> \<approx>A" unfolding tag_eq_def str_eq_def |
105 by auto |
114 by blast |
106 next |
115 next |
107 show "equiv UNIV =tag=" |
116 show "equiv UNIV =tag=" |
108 unfolding equiv_def tag_eq_rel_def refl_on_def sym_def trans_def |
117 unfolding equiv_def tag_eq_def refl_on_def sym_def trans_def |
109 by auto |
118 by auto |
110 next |
119 next |
111 show "equiv UNIV (\<approx>A)" |
120 show "equiv UNIV (\<approx>A)" |
112 unfolding equiv_def str_eq_rel_def sym_def refl_on_def trans_def |
121 unfolding equiv_def str_eq_def sym_def refl_on_def trans_def |
113 by blast |
122 by blast |
114 qed |
123 qed |
115 |
124 |
116 |
125 |
117 subsection {* The proof *} |
126 subsection {* The proof *} |
118 |
127 |
119 subsubsection {* The base case for @{const "Zero"} *} |
128 subsubsection {* The base case for @{const "Zero"} *} |
120 |
129 |
121 lemma quot_zero_eq: |
130 lemma quot_zero_eq: |
122 shows "UNIV // \<approx>{} = {UNIV}" |
131 shows "UNIV // \<approx>{} = {UNIV}" |
123 unfolding quotient_def Image_def str_eq_rel_def by auto |
132 unfolding quotient_def Image_def str_eq_def by auto |
124 |
133 |
125 lemma quot_zero_finiteI [intro]: |
134 lemma quot_zero_finiteI [intro]: |
126 shows "finite (UNIV // \<approx>{})" |
135 shows "finite (UNIV // \<approx>{})" |
127 unfolding quot_zero_eq by simp |
136 unfolding quot_zero_eq by simp |
128 |
137 |
163 then obtain y where h: "x = {z. (y, z) \<in> \<approx>{[c]}}" |
172 then obtain y where h: "x = {z. (y, z) \<in> \<approx>{[c]}}" |
164 unfolding quotient_def Image_def by blast |
173 unfolding quotient_def Image_def by blast |
165 show "x \<in> {{[]},{[c]}, UNIV - {[], [c]}}" |
174 show "x \<in> {{[]},{[c]}, UNIV - {[], [c]}}" |
166 proof - |
175 proof - |
167 { assume "y = []" hence "x = {[]}" using h |
176 { assume "y = []" hence "x = {[]}" using h |
168 by (auto simp:str_eq_rel_def) } |
177 by (auto simp: str_eq_def) } |
169 moreover |
178 moreover |
170 { assume "y = [c]" hence "x = {[c]}" using h |
179 { assume "y = [c]" hence "x = {[c]}" using h |
171 by (auto dest!:spec[where x = "[]"] simp:str_eq_rel_def) } |
180 by (auto dest!: spec[where x = "[]"] simp: str_eq_def) } |
172 moreover |
181 moreover |
173 { assume "y \<noteq> []" and "y \<noteq> [c]" |
182 { assume "y \<noteq> []" and "y \<noteq> [c]" |
174 hence "\<forall> z. (y @ z) \<noteq> [c]" by (case_tac y, auto) |
183 hence "\<forall> z. (y @ z) \<noteq> [c]" by (case_tac y, auto) |
175 moreover have "\<And> p. (p \<noteq> [] \<and> p \<noteq> [c]) = (\<forall> q. p @ q \<noteq> [c])" |
184 moreover have "\<And> p. (p \<noteq> [] \<and> p \<noteq> [c]) = (\<forall> q. p @ q \<noteq> [c])" |
176 by (case_tac p, auto) |
185 by (case_tac p, auto) |
177 ultimately have "x = UNIV - {[],[c]}" using h |
186 ultimately have "x = UNIV - {[],[c]}" using h |
178 by (auto simp add:str_eq_rel_def) |
187 by (auto simp add: str_eq_def) |
179 } |
188 } |
180 ultimately show ?thesis by blast |
189 ultimately show ?thesis by blast |
181 qed |
190 qed |
182 qed |
191 qed |
183 |
192 |
187 |
196 |
188 |
197 |
189 subsubsection {* The inductive case for @{const Plus} *} |
198 subsubsection {* The inductive case for @{const Plus} *} |
190 |
199 |
191 definition |
200 definition |
192 tag_str_Plus :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang)" |
201 tag_Plus :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang)" |
193 where |
202 where |
194 "tag_str_Plus A B \<equiv> (\<lambda>x. (\<approx>A `` {x}, \<approx>B `` {x}))" |
203 "tag_Plus A B \<equiv> (\<lambda>x. (\<approx>A `` {x}, \<approx>B `` {x}))" |
195 |
204 |
196 lemma quot_union_finiteI [intro]: |
205 lemma quot_plus_finiteI [intro]: |
197 assumes finite1: "finite (UNIV // \<approx>A)" |
206 assumes finite1: "finite (UNIV // \<approx>A)" |
198 and finite2: "finite (UNIV // \<approx>B)" |
207 and finite2: "finite (UNIV // \<approx>B)" |
199 shows "finite (UNIV // \<approx>(A \<union> B))" |
208 shows "finite (UNIV // \<approx>(A \<union> B))" |
200 proof (rule_tac tag = "tag_str_Plus A B" in tag_finite_imageD) |
209 proof (rule_tac tag = "tag_Plus A B" in tag_finite_imageD) |
201 have "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))" |
210 have "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))" |
202 using finite1 finite2 by auto |
211 using finite1 finite2 by auto |
203 then show "finite (range (tag_str_Plus A B))" |
212 then show "finite (range (tag_Plus A B))" |
204 unfolding tag_str_Plus_def quotient_def |
213 unfolding tag_Plus_def quotient_def |
205 by (rule rev_finite_subset) (auto) |
214 by (rule rev_finite_subset) (auto) |
206 next |
215 next |
207 show "\<And>x y. tag_str_Plus A B x = tag_str_Plus A B y \<Longrightarrow> x \<approx>(A \<union> B) y" |
216 show "\<And>x y. tag_Plus A B x = tag_Plus A B y \<Longrightarrow> x \<approx>(A \<union> B) y" |
208 unfolding tag_str_Plus_def |
217 unfolding tag_Plus_def |
209 unfolding str_eq_def |
218 unfolding str_eq_def |
210 unfolding str_eq_rel_def |
|
211 by auto |
219 by auto |
212 qed |
220 qed |
213 |
221 |
214 |
222 |
215 subsubsection {* The inductive case for @{text "Times"}*} |
223 subsubsection {* The inductive case for @{text "Times"}*} |
216 |
224 |
217 definition |
225 definition |
218 tag_str_Times :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang set)" |
226 "Partitions s \<equiv> {(u, v). u @ v = s}" |
219 where |
227 |
220 "tag_str_Times L1 L2 \<equiv> |
228 lemma conc_elim: |
221 (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa. xa \<le> x \<and> xa \<in> L1}))" |
229 assumes "x \<in> A \<cdot> B" |
222 |
230 shows "\<exists>(u, v) \<in> Partitions x. u \<in> A \<and> v \<in> B" |
223 lemma Seq_in_cases: |
231 using assms |
|
232 unfolding conc_def Partitions_def |
|
233 by auto |
|
234 |
|
235 lemma conc_intro: |
|
236 assumes "(u, v) \<in> Partitions x \<and> u \<in> A \<and> v \<in> B" |
|
237 shows "x \<in> A \<cdot> B" |
|
238 using assms |
|
239 unfolding conc_def Partitions_def |
|
240 by auto |
|
241 |
|
242 |
|
243 lemma y: |
|
244 "\<lbrakk>x \<in> A; x \<approx>A y\<rbrakk> \<Longrightarrow> y \<in> A" |
|
245 apply(simp add: str_eq_def) |
|
246 apply(drule_tac x="[]" in spec) |
|
247 apply(simp) |
|
248 done |
|
249 |
|
250 definition |
|
251 tag_Times3a :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang" |
|
252 where |
|
253 "tag_Times3a A B \<equiv> (\<lambda>x. \<approx>A `` {x})" |
|
254 |
|
255 definition |
|
256 tag_Times3b :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang) set" |
|
257 where |
|
258 "tag_Times3b A B \<equiv> |
|
259 (\<lambda>x. ({(\<approx>A `` {u}, \<approx>B `` {v}) | u v. (u, v) \<in> Partitions x}))" |
|
260 |
|
261 definition |
|
262 tag_Times3 :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang \<times> ('a lang \<times> 'a lang) set" |
|
263 where |
|
264 "tag_Times3 A B \<equiv> |
|
265 (\<lambda>x. (tag_Times3a A B x, tag_Times3b A B x))" |
|
266 |
|
267 lemma |
|
268 assumes a: "tag_Times3a A B x = tag_Times3a A B y" |
|
269 and b: "tag_Times3b A B x = tag_Times3b A B y" |
|
270 and c: "x @ z \<in> A \<cdot> B" |
|
271 shows "y @ z \<in> A \<cdot> B" |
|
272 proof - |
|
273 from c obtain u v where |
|
274 h1: "(u, v) \<in> Partitions (x @ z)" and |
|
275 h2: "u \<in> A" and |
|
276 h3: "v \<in> B" by (auto dest: conc_elim) |
|
277 from h1 have "x @ z = u @ v" unfolding Partitions_def by simp |
|
278 then obtain us |
|
279 where "(x = u @ us \<and> us @ z = v) \<or> (x @ us = u \<and> z = us @ v)" |
|
280 by (auto simp add: append_eq_append_conv2) |
|
281 moreover |
|
282 { assume eq: "x = u @ us" "us @ z = v" |
|
283 have "(\<approx>A `` {u}, \<approx>B `` {us}) \<in> tag_Times3b A B x" |
|
284 unfolding tag_Times3b_def Partitions_def using eq by auto |
|
285 then have "(\<approx>A `` {u}, \<approx>B `` {us}) \<in> tag_Times3b A B y" |
|
286 using b by simp |
|
287 then obtain u' us' where |
|
288 q1: "\<approx>A `` {u} = \<approx>A `` {u'}" and |
|
289 q2: "\<approx>B `` {us} = \<approx>B `` {us'}" and |
|
290 q3: "(u', us') \<in> Partitions y" |
|
291 by (auto simp add: tag_Times3b_def) |
|
292 from q1 h2 have "u' \<in> A" |
|
293 using y unfolding Image_def str_eq_def by blast |
|
294 moreover from q2 h3 eq |
|
295 have "us' @ z \<in> B" |
|
296 unfolding Image_def str_eq_def by auto |
|
297 ultimately have "y @ z \<in> A \<cdot> B" using q3 |
|
298 unfolding Partitions_def by auto |
|
299 } |
|
300 moreover |
|
301 { assume eq: "x @ us = u" "z = us @ v" |
|
302 have "(\<approx>A `` {x}) = tag_Times3a A B x" |
|
303 unfolding tag_Times3a_def by simp |
|
304 then have "(\<approx>A `` {x}) = tag_Times3a A B y" |
|
305 using a by simp |
|
306 then have "\<approx>A `` {x} = \<approx>A `` {y}" |
|
307 unfolding tag_Times3a_def by simp |
|
308 moreover |
|
309 have "x @ us \<in> A" using h2 eq by simp |
|
310 ultimately |
|
311 have "y @ us \<in> A" using y |
|
312 unfolding Image_def str_eq_def by blast |
|
313 then have "(y @ us) @ v \<in> A \<cdot> B" |
|
314 using h3 unfolding conc_def by blast |
|
315 then have "y @ z \<in> A \<cdot> B" using eq by simp |
|
316 } |
|
317 ultimately show "y @ z \<in> A \<cdot> B" by blast |
|
318 qed |
|
319 |
|
320 lemma conc_in_cases2: |
224 assumes "x @ z \<in> A \<cdot> B" |
321 assumes "x @ z \<in> A \<cdot> B" |
225 shows "(\<exists> x' \<le> x. x' \<in> A \<and> (x - x') @ z \<in> B) \<or> |
322 shows "(\<exists> x' \<le> x. x' \<in> A \<and> (x - x') @ z \<in> B) \<or> |
226 (\<exists> z' \<le> z. (x @ z') \<in> A \<and> (z - z') \<in> B)" |
323 (\<exists> z' \<le> z. (x @ z') \<in> A \<and> (z - z') \<in> B)" |
227 using assms |
324 using assms |
228 unfolding conc_def prefix_def |
325 unfolding conc_def prefix_def |
229 by (auto simp add: append_eq_append_conv2) |
326 by (auto simp add: append_eq_append_conv2) |
230 |
327 |
231 lemma tag_str_Times_injI: |
328 definition |
232 assumes eq_tag: "tag_str_Times A B x = tag_str_Times A B y" |
329 tag_Times :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang set)" |
|
330 where |
|
331 "tag_Times A B \<equiv> |
|
332 (\<lambda>x. (\<approx>A `` {x}, {(\<approx>B `` {x - x'}) | x'. x' \<le> x \<and> x' \<in> A}))" |
|
333 |
|
334 lemma tag_Times_injI: |
|
335 assumes eq_tag: "tag_Times A B x = tag_Times A B y" |
233 shows "x \<approx>(A \<cdot> B) y" |
336 shows "x \<approx>(A \<cdot> B) y" |
234 proof - |
337 proof - |
235 { fix x y z |
338 { fix x y z |
236 assume xz_in_seq: "x @ z \<in> A \<cdot> B" |
339 assume xz_in_seq: "x @ z \<in> A \<cdot> B" |
237 and tag_xy: "tag_str_Times A B x = tag_str_Times A B y" |
340 and tag_xy: "tag_Times A B x = tag_Times A B y" |
238 have"y @ z \<in> A \<cdot> B" |
341 have"y @ z \<in> A \<cdot> B" |
239 proof - |
342 proof - |
240 { (* first case with x' in A and (x - x') @ z in B *) |
343 { (* first case with x' in A and (x - x') @ z in B *) |
241 fix x' |
344 fix x' |
242 assume h1: "x' \<le> x" and h2: "x' \<in> A" and h3: "(x - x') @ z \<in> B" |
345 assume h1: "x' \<le> x" and h2: "x' \<in> A" and h3: "(x - x') @ z \<in> B" |
245 and "y' \<in> A" |
348 and "y' \<in> A" |
246 and "(y - y') @ z \<in> B" |
349 and "(y - y') @ z \<in> B" |
247 proof - |
350 proof - |
248 have "{\<approx>B `` {x - x'} |x'. x' \<le> x \<and> x' \<in> A} = |
351 have "{\<approx>B `` {x - x'} |x'. x' \<le> x \<and> x' \<in> A} = |
249 {\<approx>B `` {y - y'} |y'. y' \<le> y \<and> y' \<in> A}" (is "?Left = ?Right") |
352 {\<approx>B `` {y - y'} |y'. y' \<le> y \<and> y' \<in> A}" (is "?Left = ?Right") |
250 using tag_xy unfolding tag_str_Times_def by simp |
353 using tag_xy unfolding tag_Times_def by simp |
251 moreover |
354 moreover |
252 have "\<approx>B `` {x - x'} \<in> ?Left" using h1 h2 by auto |
355 have "\<approx>B `` {x - x'} \<in> ?Left" using h1 h2 by auto |
253 ultimately |
356 ultimately |
254 have "\<approx>B `` {x - x'} \<in> ?Right" by simp |
357 have "\<approx>B `` {x - x'} \<in> ?Right" by simp |
255 then obtain y' |
358 then obtain y' |
256 where eq_xy': "\<approx>B `` {x - x'} = \<approx>B `` {y - y'}" |
359 where eq_xy': "\<approx>B `` {x - x'} = \<approx>B `` {y - y'}" |
257 and pref_y': "y' \<le> y" and y'_in: "y' \<in> A" |
360 and pref_y': "y' \<le> y" and y'_in: "y' \<in> A" |
258 by simp blast |
361 by simp blast |
259 |
|
260 have "(x - x') \<approx>B (y - y')" using eq_xy' |
362 have "(x - x') \<approx>B (y - y')" using eq_xy' |
261 unfolding Image_def str_eq_rel_def str_eq_def by auto |
363 unfolding Image_def str_eq_def by auto |
262 with h3 have "(y - y') @ z \<in> B" |
364 with h3 have "(y - y') @ z \<in> B" |
263 unfolding str_eq_rel_def str_eq_def by simp |
365 unfolding str_eq_def by simp |
264 with pref_y' y'_in |
366 with pref_y' y'_in |
265 show ?thesis using that by blast |
367 show ?thesis using that by blast |
266 qed |
368 qed |
267 then have "y @ z \<in> A \<cdot> B" by (erule_tac prefixE) (auto simp: Seq_def) |
369 then have "y @ z \<in> A \<cdot> B" |
|
370 unfolding prefix_def by auto |
268 } |
371 } |
269 moreover |
372 moreover |
270 { (* second case with x @ z' in A and z - z' in B *) |
373 { (* second case with x @ z' in A and z - z' in B *) |
271 fix z' |
374 fix z' |
272 assume h1: "z' \<le> z" and h2: "(x @ z') \<in> A" and h3: "z - z' \<in> B" |
375 assume h1: "z' \<le> z" and h2: "(x @ z') \<in> A" and h3: "z - z' \<in> B" |
273 have "\<approx>A `` {x} = \<approx>A `` {y}" |
376 have "\<approx>A `` {x} = \<approx>A `` {y}" |
274 using tag_xy unfolding tag_str_Times_def by simp |
377 using tag_xy unfolding tag_Times_def by simp |
275 with h2 have "y @ z' \<in> A" |
378 with h2 have "y @ z' \<in> A" |
276 unfolding Image_def str_eq_rel_def str_eq_def by auto |
379 unfolding Image_def str_eq_def by auto |
277 with h1 h3 have "y @ z \<in> A \<cdot> B" |
380 with h1 h3 have "y @ z \<in> A \<cdot> B" |
278 unfolding prefix_def conc_def |
381 unfolding prefix_def conc_def |
279 by (auto) (metis append_assoc) |
382 by (auto) (metis append_assoc) |
280 } |
383 } |
281 ultimately show "y @ z \<in> A \<cdot> B" |
384 ultimately show "y @ z \<in> A \<cdot> B" |
282 using Seq_in_cases [OF xz_in_seq] by blast |
385 using conc_in_cases2 [OF xz_in_seq] by blast |
283 qed |
386 qed |
284 } |
387 } |
285 from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]] |
388 from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]] |
286 show "x \<approx>(A \<cdot> B) y" unfolding str_eq_def str_eq_rel_def by blast |
389 show "x \<approx>(A \<cdot> B) y" unfolding str_eq_def by blast |
287 qed |
390 qed |
288 |
391 |
289 lemma quot_seq_finiteI [intro]: |
392 lemma quot_conc_finiteI [intro]: |
290 fixes L1 L2::"'a lang" |
393 fixes A B::"'a lang" |
291 assumes fin1: "finite (UNIV // \<approx>L1)" |
394 assumes fin1: "finite (UNIV // \<approx>A)" |
292 and fin2: "finite (UNIV // \<approx>L2)" |
395 and fin2: "finite (UNIV // \<approx>B)" |
293 shows "finite (UNIV // \<approx>(L1 \<cdot> L2))" |
396 shows "finite (UNIV // \<approx>(A \<cdot> B))" |
294 proof (rule_tac tag = "tag_str_Times L1 L2" in tag_finite_imageD) |
397 proof (rule_tac tag = "tag_Times A B" in tag_finite_imageD) |
295 show "\<And>x y. tag_str_Times L1 L2 x = tag_str_Times L1 L2 y \<Longrightarrow> x \<approx>(L1 \<cdot> L2) y" |
398 show "\<And>x y. tag_Times A B x = tag_Times A B y \<Longrightarrow> x \<approx>(A \<cdot> B) y" |
296 by (rule tag_str_Times_injI) |
399 by (rule tag_Times_injI) |
297 next |
400 next |
298 have *: "finite ((UNIV // \<approx>L1) \<times> (Pow (UNIV // \<approx>L2)))" |
401 have *: "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))" |
299 using fin1 fin2 by auto |
402 using fin1 fin2 by auto |
300 show "finite (range (tag_str_Times L1 L2))" |
403 show "finite (range (tag_Times A B))" |
301 unfolding tag_str_Times_def |
404 unfolding tag_Times_def |
302 apply(rule finite_subset[OF _ *]) |
405 apply(rule finite_subset[OF _ *]) |
303 unfolding quotient_def |
406 unfolding quotient_def |
304 by auto |
407 by auto |
305 qed |
408 qed |
306 |
409 |
307 |
410 |
308 subsubsection {* The inductive case for @{const "Star"} *} |
411 subsubsection {* The inductive case for @{const "Star"} *} |
309 |
412 |
310 definition |
413 definition |
311 tag_str_Star :: "'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang) set" |
414 "SPartitions s \<equiv> {(u, v). u @ v = s \<and> u < s}" |
312 where |
415 |
313 "tag_str_Star L1 \<equiv> (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<in> L1\<star>})" |
416 lemma |
|
417 assumes "x \<in> A\<star>" "x \<noteq> []" |
|
418 shows "\<exists>(u, v) \<in> SPartitions x. u \<in> A\<star> \<and> v \<in> A\<star>" |
|
419 using assms |
|
420 apply(subst (asm) star_unfold_left) |
|
421 apply(simp) |
|
422 apply(simp add: conc_def) |
|
423 apply(erule exE)+ |
|
424 apply(erule conjE)+ |
|
425 apply(rule_tac x="([], xs @ ys)" in bexI) |
|
426 apply(simp) |
|
427 apply(simp add: SPartitions_def) |
|
428 apply(auto) |
|
429 apply (metis append_Cons list.exhaust strict_prefix_simps(2)) |
|
430 by (metis Nil_is_append_conv Nil_prefix xt1(11)) |
|
431 |
|
432 lemma |
|
433 assumes "x @ z \<in> A\<star>" "x \<noteq> []" |
|
434 shows "\<exists>(u, v) \<in> SPartitions x. u \<in> A\<star> \<and> v @ z \<in> A\<star>" |
|
435 using assms |
|
436 apply(subst (asm) star_unfold_left) |
|
437 apply(simp) |
|
438 apply(simp add: conc_def) |
|
439 apply(erule exE)+ |
|
440 apply(erule conjE)+ |
|
441 apply(rule_tac x="([], x)" in bexI) |
|
442 apply(simp) |
|
443 apply(simp add: SPartitions_def) |
|
444 by (metis Nil_prefix xt1(11)) |
|
445 |
|
446 lemma finite_set_has_max: |
|
447 "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists> max \<in> A. \<forall> a \<in> A. length a \<le> length max" |
|
448 apply (induct rule:finite.induct) |
|
449 apply(simp) |
|
450 by (metis (full_types) all_not_in_conv insertI1 insert_iff linorder_linear order_eq_iff order_trans prefix_length_le) |
|
451 |
|
452 |
|
453 |
|
454 definition |
|
455 tag_Star3 :: "'a lang \<Rightarrow> 'a list \<Rightarrow> (bool \<times> 'a lang) set" |
|
456 where |
|
457 "tag_Star3 A \<equiv> |
|
458 (\<lambda>x. ({(u \<in> A\<star>, \<approx>A `` {v}) | u v. (u, v) \<in> Partitions x}))" |
|
459 |
|
460 |
|
461 |
|
462 |
|
463 definition |
|
464 tag_Star :: "'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang) set" |
|
465 where |
|
466 "tag_Star A \<equiv> (\<lambda>x. {\<approx>A `` {x - xa} | xa. xa < x \<and> xa \<in> A\<star>})" |
314 |
467 |
315 text {* A technical lemma. *} |
468 text {* A technical lemma. *} |
316 lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> |
469 lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> |
317 (\<exists> max \<in> A. \<forall> a \<in> A. f a <= (f max :: nat))" |
470 (\<exists> max \<in> A. \<forall> a \<in> A. f a <= (f max :: nat))" |
318 proof (induct rule:finite.induct) |
471 proof (induct rule:finite.induct) |
347 apply (induct x rule:rev_induct, simp) |
500 apply (induct x rule:rev_induct, simp) |
348 apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \<union> {xs}") |
501 apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \<union> {xs}") |
349 by (auto simp:strict_prefix_def) |
502 by (auto simp:strict_prefix_def) |
350 |
503 |
351 |
504 |
352 lemma tag_str_Star_injI: |
505 lemma tag_Star_injI: |
353 fixes L\<^isub>1::"('a::finite) lang" |
506 fixes L\<^isub>1::"('a::finite) lang" |
354 assumes eq_tag: "tag_str_Star L\<^isub>1 v = tag_str_Star L\<^isub>1 w" |
507 assumes eq_tag: "tag_Star L\<^isub>1 v = tag_Star L\<^isub>1 w" |
355 shows "v \<approx>(L\<^isub>1\<star>) w" |
508 shows "v \<approx>(L\<^isub>1\<star>) w" |
356 proof- |
509 proof- |
357 { fix x y z |
510 { fix x y z |
358 assume xz_in_star: "x @ z \<in> L\<^isub>1\<star>" |
511 assume xz_in_star: "x @ z \<in> L\<^isub>1\<star>" |
359 and tag_xy: "tag_str_Star L\<^isub>1 x = tag_str_Star L\<^isub>1 y" |
512 and tag_xy: "tag_Star L\<^isub>1 x = tag_Star L\<^isub>1 y" |
360 have "y @ z \<in> L\<^isub>1\<star>" |
513 have "y @ z \<in> L\<^isub>1\<star>" |
361 proof(cases "x = []") |
514 proof(cases "x = []") |
362 case True |
515 case True |
363 with tag_xy have "y = []" |
516 with tag_xy have "y = []" |
364 by (auto simp add: tag_str_Star_def strict_prefix_def) |
517 by (auto simp add: tag_Star_def strict_prefix_def) |
365 thus ?thesis using xz_in_star True by simp |
518 thus ?thesis using xz_in_star True by simp |
366 next |
519 next |
367 case False |
520 case False |
368 let ?S = "{xa::('a::finite) list. xa < x \<and> xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>}" |
521 let ?S = "{xa::('a::finite) list. xa < x \<and> xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>}" |
369 have "finite ?S" |
522 have "finite ?S" |
384 where h5: "ya < y" and h6: "ya \<in> L\<^isub>1\<star>" |
537 where h5: "ya < y" and h6: "ya \<in> L\<^isub>1\<star>" |
385 and eq_xya: "(x - xa_max) \<approx>L\<^isub>1 (y - ya)" |
538 and eq_xya: "(x - xa_max) \<approx>L\<^isub>1 (y - ya)" |
386 proof- |
539 proof- |
387 from tag_xy have "{\<approx>L\<^isub>1 `` {x - xa} |xa. xa < x \<and> xa \<in> L\<^isub>1\<star>} = |
540 from tag_xy have "{\<approx>L\<^isub>1 `` {x - xa} |xa. xa < x \<and> xa \<in> L\<^isub>1\<star>} = |
388 {\<approx>L\<^isub>1 `` {y - xa} |xa. xa < y \<and> xa \<in> L\<^isub>1\<star>}" (is "?left = ?right") |
541 {\<approx>L\<^isub>1 `` {y - xa} |xa. xa < y \<and> xa \<in> L\<^isub>1\<star>}" (is "?left = ?right") |
389 by (auto simp:tag_str_Star_def) |
542 by (auto simp:tag_Star_def) |
390 moreover have "\<approx>L\<^isub>1 `` {x - xa_max} \<in> ?left" using h1 h2 by auto |
543 moreover have "\<approx>L\<^isub>1 `` {x - xa_max} \<in> ?left" using h1 h2 by auto |
391 ultimately have "\<approx>L\<^isub>1 `` {x - xa_max} \<in> ?right" by simp |
544 ultimately have "\<approx>L\<^isub>1 `` {x - xa_max} \<in> ?right" by simp |
392 thus ?thesis using that |
545 thus ?thesis using that |
393 apply (simp add:Image_def str_eq_rel_def str_eq_def) by blast |
546 apply (simp add: Image_def str_eq_def) by blast |
394 qed |
547 qed |
395 have "(y - ya) @ z \<in> L\<^isub>1\<star>" |
548 have "(y - ya) @ z \<in> L\<^isub>1\<star>" |
396 proof- |
549 proof- |
397 obtain za zb where eq_zab: "z = za @ zb" |
550 obtain za zb where eq_zab: "z = za @ zb" |
398 and l_za: "(y - ya)@za \<in> L\<^isub>1" and ls_zb: "zb \<in> L\<^isub>1\<star>" |
551 and l_za: "(y - ya)@za \<in> L\<^isub>1" and ls_zb: "zb \<in> L\<^isub>1\<star>" |
399 proof - |
552 proof - |
400 from h1 have "(x - xa_max) @ z \<noteq> []" |
553 from h1 have "(x - xa_max) @ z \<noteq> []" |
401 by (auto simp:strict_prefix_def elim:prefixE) |
554 unfolding strict_prefix_def prefix_def by auto |
402 from star_decom [OF h3 this] |
555 from star_decom [OF h3 this] |
403 obtain a b where a_in: "a \<in> L\<^isub>1" |
556 obtain a b where a_in: "a \<in> L\<^isub>1" |
404 and a_neq: "a \<noteq> []" and b_in: "b \<in> L\<^isub>1\<star>" |
557 and a_neq: "a \<noteq> []" and b_in: "b \<in> L\<^isub>1\<star>" |
405 and ab_max: "(x - xa_max) @ z = a @ b" by blast |
558 and ab_max: "(x - xa_max) @ z = a @ b" by blast |
406 let ?za = "a - (x - xa_max)" and ?zb = "b" |
559 let ?za = "a - (x - xa_max)" and ?zb = "b" |
426 using a_neq by simp |
579 using a_neq by simp |
427 ultimately show ?thesis using h4 by blast |
580 ultimately show ?thesis using h4 by blast |
428 qed } |
581 qed } |
429 ultimately show ?P1 and ?P2 by auto |
582 ultimately show ?P1 and ?P2 by auto |
430 qed |
583 qed |
431 hence "(x - xa_max)@?za \<in> L\<^isub>1" using a_in by (auto elim:prefixE) |
584 hence "(x - xa_max)@?za \<in> L\<^isub>1" using a_in unfolding prefix_def by auto |
432 with eq_xya have "(y - ya) @ ?za \<in> L\<^isub>1" |
585 with eq_xya have "(y - ya) @ ?za \<in> L\<^isub>1" |
433 by (auto simp:str_eq_def str_eq_rel_def) |
586 by (auto simp: str_eq_def) |
434 with eq_z and b_in |
587 with eq_z and b_in |
435 show ?thesis using that by blast |
588 show ?thesis using that by blast |
436 qed |
589 qed |
437 have "((y - ya) @ za) @ zb \<in> L\<^isub>1\<star>" using l_za ls_zb |
590 have "((y - ya) @ za) @ zb \<in> L\<^isub>1\<star>" using l_za ls_zb |
438 by (rule_tac append_in_starI) (auto) |
591 by (rule_tac append_in_starI) (auto) |
439 with eq_zab show ?thesis by simp |
592 with eq_zab show ?thesis by simp |
440 qed |
593 qed |
441 with h5 h6 show ?thesis |
594 with h5 h6 show ?thesis |
442 by (auto simp:strict_prefix_def elim: prefixE) |
595 unfolding strict_prefix_def prefix_def by auto |
443 qed |
596 qed |
444 } |
597 } |
445 from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]] |
598 from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]] |
446 show ?thesis unfolding str_eq_def str_eq_rel_def by blast |
599 show ?thesis unfolding str_eq_def by blast |
447 qed |
600 qed |
448 |
601 |
449 lemma quot_star_finiteI [intro]: |
602 lemma quot_star_finiteI [intro]: |
450 fixes A::"('a::finite) lang" |
603 fixes A::"('a::finite) lang" |
451 assumes finite1: "finite (UNIV // \<approx>A)" |
604 assumes finite1: "finite (UNIV // \<approx>A)" |
452 shows "finite (UNIV // \<approx>(A\<star>))" |
605 shows "finite (UNIV // \<approx>(A\<star>))" |
453 proof (rule_tac tag = "tag_str_Star A" in tag_finite_imageD) |
606 proof (rule_tac tag = "tag_Star A" in tag_finite_imageD) |
454 show "\<And>x y. tag_str_Star A x = tag_str_Star A y \<Longrightarrow> x \<approx>(A\<star>) y" |
607 show "\<And>x y. tag_Star A x = tag_Star A y \<Longrightarrow> x \<approx>(A\<star>) y" |
455 by (rule tag_str_Star_injI) |
608 by (rule tag_Star_injI) |
456 next |
609 next |
457 have *: "finite (Pow (UNIV // \<approx>A))" |
610 have *: "finite (Pow (UNIV // \<approx>A))" |
458 using finite1 by auto |
611 using finite1 by auto |
459 show "finite (range (tag_str_Star A))" |
612 show "finite (range (tag_Star A))" |
460 unfolding tag_str_Star_def |
613 unfolding tag_Star_def |
461 apply(rule finite_subset[OF _ *]) |
614 apply(rule finite_subset[OF _ *]) |
462 unfolding quotient_def |
615 unfolding quotient_def |
463 by auto |
616 by auto |
464 qed |
617 qed |
465 |
618 |