188 | "UP (Plus r1 r2) = Plus (UP r1) (UP r2)" |
190 | "UP (Plus r1 r2) = Plus (UP r1) (UP r2)" |
189 | "UP (Times r1 r2) = Times (UP r1) (UP r2)" |
191 | "UP (Times r1 r2) = Times (UP r1) (UP r2)" |
190 | "UP (Star r) = Star Allreg" |
192 | "UP (Star r) = Star Allreg" |
191 |
193 |
192 lemma lang_UP: |
194 lemma lang_UP: |
193 fixes r::"letter rexp" |
195 fixes r::"'a::finite rexp" |
194 shows "lang (UP r) = SUPSEQ (lang r)" |
196 shows "lang (UP r) = SUPSEQ (lang r)" |
195 by (induct r) (simp_all) |
197 by (induct r) (simp_all) |
196 |
198 |
197 lemma regular_SUPSEQ: |
199 lemma regular_SUPSEQ: |
198 fixes A::"letter lang" |
200 fixes A::"('a::finite) lang" |
199 assumes "regular A" |
201 assumes "regular A" |
200 shows "regular (SUPSEQ A)" |
202 shows "regular (SUPSEQ A)" |
201 proof - |
203 proof - |
202 from assms obtain r::"letter rexp" where "lang r = A" by auto |
204 from assms obtain r::"'a::finite rexp" where "lang r = A" by auto |
203 then have "lang (UP r) = SUPSEQ A" by (simp add: lang_UP) |
205 then have "lang (UP r) = SUPSEQ A" by (simp add: lang_UP) |
204 then show "regular (SUPSEQ A)" by auto |
206 then show "regular (SUPSEQ A)" by auto |
205 qed |
207 qed |
206 |
208 |
207 lemma SUPSEQ_subset: |
209 lemma SUPSEQ_subset: |
250 moreover |
253 moreover |
251 have "f j \<in> A" using c by auto |
254 have "f j \<in> A" using c by auto |
252 ultimately have "\<not>(f i \<preceq> f j)" using a by simp |
255 ultimately have "\<not>(f i \<preceq> f j)" using a by simp |
253 with e show "False" by simp |
256 with e show "False" by simp |
254 qed |
257 qed |
|
258 *) |
255 |
259 |
256 definition |
260 definition |
257 minimal :: "letter list \<Rightarrow> letter lang \<Rightarrow> bool" |
261 minimal :: "'a::finite list \<Rightarrow> 'a lang \<Rightarrow> bool" |
258 where |
262 where |
259 "minimal x A \<equiv> (\<forall>y \<in> A. y \<preceq> x \<longrightarrow> x \<preceq> y)" |
263 "minimal x A \<equiv> (\<forall>y \<in> A. y \<preceq> x \<longrightarrow> x \<preceq> y)" |
260 |
264 |
261 lemma main_lemma: |
265 lemma main_lemma: |
|
266 fixes A::"('a::finite) list set" |
262 shows "\<exists>M. finite M \<and> SUPSEQ A = SUPSEQ M" |
267 shows "\<exists>M. finite M \<and> SUPSEQ A = SUPSEQ M" |
263 proof - |
268 proof - |
264 def M \<equiv> "{x \<in> A. minimal x A}" |
269 def M \<equiv> "{x \<in> A. minimal x A}" |
265 have "finite M" |
270 have "finite M" |
266 unfolding M_def minimal_def |
271 unfolding M_def minimal_def |
286 ultimately |
291 ultimately |
287 show "\<exists>M. finite M \<and> SUPSEQ A = SUPSEQ M" by blast |
292 show "\<exists>M. finite M \<and> SUPSEQ A = SUPSEQ M" by blast |
288 qed |
293 qed |
289 |
294 |
290 lemma closure_SUPSEQ: |
295 lemma closure_SUPSEQ: |
291 fixes A::"letter lang" |
296 fixes A::"'a::finite lang" |
292 shows "regular (SUPSEQ A)" |
297 shows "regular (SUPSEQ A)" |
293 proof - |
298 proof - |
294 obtain M where a: "finite M" and b: "SUPSEQ A = SUPSEQ M" |
299 obtain M where a: "finite M" and b: "SUPSEQ A = SUPSEQ M" |
295 using main_lemma by blast |
300 using main_lemma by blast |
296 have "regular M" using a by (rule finite_regular) |
301 have "regular M" using a by (rule finite_regular) |
297 then have "regular (SUPSEQ M)" by (rule regular_SUPSEQ) |
302 then have "regular (SUPSEQ M)" by (rule regular_SUPSEQ) |
298 then show "regular (SUPSEQ A)" using b by simp |
303 then show "regular (SUPSEQ A)" using b by simp |
299 qed |
304 qed |
300 |
305 |
301 lemma closure_SUBSEQ: |
306 lemma closure_SUBSEQ: |
302 fixes A::"letter lang" |
307 fixes A::"'a::finite lang" |
303 shows "regular (SUBSEQ A)" |
308 shows "regular (SUBSEQ A)" |
304 proof - |
309 proof - |
305 have "regular (SUPSEQ (- SUBSEQ A))" by (rule closure_SUPSEQ) |
310 have "regular (SUPSEQ (- SUBSEQ A))" by (rule closure_SUPSEQ) |
306 then have "regular (- SUBSEQ A)" by (subst SUBSEQ_complement) (simp) |
311 then have "regular (- SUBSEQ A)" by (subst SUBSEQ_complement) (simp) |
307 then have "regular (- (- (SUBSEQ A)))" by (rule closure_complement) |
312 then have "regular (- (- (SUBSEQ A)))" by (rule closure_complement) |