1 theory Closure2 |
1 theory Closure2 |
2 imports Closures |
2 imports |
|
3 Closures |
|
4 (* "~~/src/HOL/Proofs/Extraction/Higman" *) |
3 begin |
5 begin |
4 |
6 |
5 inductive emb :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<preceq> _") |
7 inductive |
|
8 emb :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<preceq> _") |
6 where |
9 where |
7 emb0 [Pure.intro]: "emb [] bs" |
10 emb0 [intro]: "emb [] y" |
8 | emb1 [Pure.intro]: "emb as bs \<Longrightarrow> emb as (b # bs)" |
11 | emb1 [intro]: "emb x y \<Longrightarrow> emb x (c # y)" |
9 | emb2 [Pure.intro]: "emb as bs \<Longrightarrow> emb (a # as) (a # bs)" |
12 | emb2 [intro]: "emb x y \<Longrightarrow> emb (c # x) (c # y)" |
10 |
13 |
11 lemma emb_refl: |
14 lemma emb_refl [intro]: |
12 shows "x \<preceq> x" |
15 shows "x \<preceq> x" |
13 apply(induct x) |
16 by (induct x) (auto intro: emb.intros) |
14 apply(auto intro: emb.intros) |
17 |
15 done |
18 lemma emb_right [intro]: |
16 |
|
17 lemma emb_right: |
|
18 assumes a: "x \<preceq> y" |
19 assumes a: "x \<preceq> y" |
19 shows "x \<preceq> y @ y'" |
20 shows "x \<preceq> y @ y'" |
20 using a |
21 using a by (induct arbitrary: y') (auto) |
21 apply(induct arbitrary: y') |
22 |
22 apply(auto intro: emb.intros) |
23 lemma emb_left [intro]: |
23 done |
|
24 |
|
25 lemma emb_left: |
|
26 assumes a: "x \<preceq> y" |
24 assumes a: "x \<preceq> y" |
27 shows "x \<preceq> y' @ y" |
25 shows "x \<preceq> y' @ y" |
28 using a |
26 using a by (induct y') (auto) |
29 apply(induct y') |
27 |
30 apply(auto intro: emb.intros) |
28 lemma emb_appendI [intro]: |
31 done |
|
32 |
|
33 lemma emb_appendI: |
|
34 assumes a: "x \<preceq> x'" |
29 assumes a: "x \<preceq> x'" |
35 and b: "y \<preceq> y'" |
30 and b: "y \<preceq> y'" |
36 shows "x @ y \<preceq> x' @ y'" |
31 shows "x @ y \<preceq> x' @ y'" |
|
32 using a b by (induct) (auto) |
|
33 |
|
34 lemma emb_cons_leftD: |
|
35 assumes "a # x \<preceq> y" |
|
36 shows "\<exists>y1 y2. y = y1 @ [a] @ y2 \<and> x \<preceq> y2" |
|
37 using assms |
|
38 apply(induct x\<equiv>"a # x" y\<equiv>"y" arbitrary: a x y) |
|
39 apply(auto) |
|
40 apply(metis append_Cons) |
|
41 done |
|
42 |
|
43 lemma emb_append_leftD: |
|
44 assumes "x1 @ x2 \<preceq> y" |
|
45 shows "\<exists>y1 y2. y = y1 @ y2 \<and> x1 \<preceq> y1 \<and> x2 \<preceq> y2" |
|
46 using assms |
|
47 apply(induct x1 arbitrary: x2 y) |
|
48 apply(auto) |
|
49 apply(drule emb_cons_leftD) |
|
50 apply(auto) |
|
51 apply(drule_tac x="x2" in meta_spec) |
|
52 apply(drule_tac x="y2" in meta_spec) |
|
53 apply(auto) |
|
54 apply(rule_tac x="y1 @ (a # y1a)" in exI) |
|
55 apply(rule_tac x="y2a" in exI) |
|
56 apply(auto) |
|
57 done |
|
58 |
|
59 lemma emb_trans: |
|
60 assumes a: "x1 \<preceq> x2" |
|
61 and b: "x2 \<preceq> x3" |
|
62 shows "x1 \<preceq> x3" |
37 using a b |
63 using a b |
38 apply(induct) |
64 apply(induct arbitrary: x3) |
39 apply(auto intro: emb.intros emb_left) |
65 apply(metis emb0) |
40 done |
66 apply(metis emb_cons_leftD emb_left) |
41 |
67 apply(drule_tac emb_cons_leftD) |
42 lemma emb_append: |
68 apply(auto) |
43 assumes a: "x \<preceq> y1 @ y2" |
69 done |
44 shows "\<exists>x1 x2. x = x1 @ x2 \<and> x1 \<preceq> y1 \<and> x2 \<preceq> y2" |
70 |
|
71 lemma emb_strict_length: |
|
72 assumes a: "x \<preceq> y" "x \<noteq> y" |
|
73 shows "length x < length y" |
45 using a |
74 using a |
46 apply(induct x y\<equiv>"y1 @ y2" arbitrary: y1 y2) |
75 by (induct) (auto simp add: less_Suc_eq) |
47 apply(auto intro: emb0)[1] |
76 |
48 apply(simp add: Cons_eq_append_conv) |
77 lemma emb_antisym: |
49 apply(auto)[1] |
78 assumes a: "x \<preceq> y" "y \<preceq> x" |
50 apply(rule_tac x="[]" in exI) |
79 shows "x = y" |
51 apply(rule_tac x="as" in exI) |
80 using a emb_strict_length |
52 apply(auto intro: emb.intros)[1] |
81 by (metis not_less_iff_gr_or_eq) |
53 apply(simp add: append_eq_append_conv2) |
82 |
54 apply(drule_tac x="ys'" in meta_spec) |
83 lemma emb_wf: |
55 apply(drule_tac x="y2" in meta_spec) |
84 shows "wf {(x, y). x \<preceq> y \<and> x \<noteq> y}" |
56 apply(auto)[1] |
85 proof - |
57 apply(rule_tac x="x1" in exI) |
86 have "wf (measure length)" by simp |
58 apply(rule_tac x="x2" in exI) |
87 moreover |
59 apply(auto intro: emb.intros)[1] |
88 have "{(x, y). x \<preceq> y \<and> x \<noteq> y} \<subseteq> measure length" |
60 apply(subst (asm) Cons_eq_append_conv) |
89 unfolding measure_def by (auto simp add: emb_strict_length) |
61 apply(auto)[1] |
90 ultimately |
62 apply(rule_tac x="[]" in exI) |
91 show "wf {(x, y). x \<preceq> y \<and> x \<noteq> y}" by (rule wf_subset) |
63 apply(rule_tac x="a # as" in exI) |
92 qed |
64 apply(auto intro: emb.intros)[1] |
93 |
65 apply(simp add: append_eq_append_conv2) |
94 subsection {* Sub- and Supsequences *} |
66 apply(drule_tac x="ys'" in meta_spec) |
|
67 apply(drule_tac x="y2" in meta_spec) |
|
68 apply(auto)[1] |
|
69 apply(rule_tac x="a # x1" in exI) |
|
70 apply(rule_tac x="x2" in exI) |
|
71 apply(auto intro: emb.intros)[1] |
|
72 done |
|
73 |
|
74 |
95 |
75 definition |
96 definition |
76 "SUBSEQ A \<equiv> {x. \<exists>y \<in> A. x \<preceq> y}" |
97 "SUBSEQ A \<equiv> {x. \<exists>y \<in> A. x \<preceq> y}" |
77 |
98 |
78 definition |
99 definition |
79 "SUPSEQ A \<equiv> (- SUBSEQ A) \<union> A" |
100 "SUPSEQ A \<equiv> {x. \<exists>y \<in> A. y \<preceq> x}" |
80 |
101 |
81 lemma [simp]: |
102 lemma SUPSEQ_simps [simp]: |
82 "SUBSEQ {} = {}" |
103 shows "SUPSEQ {} = {}" |
83 unfolding SUBSEQ_def |
104 and "SUPSEQ {[]} = UNIV" |
84 by auto |
105 unfolding SUPSEQ_def by auto |
85 |
106 |
86 lemma [simp]: |
107 lemma SUPSEQ_atom [simp]: |
87 "SUBSEQ {[]} = {[]}" |
108 shows "SUPSEQ {[a]} = UNIV \<cdot> {[a]} \<cdot> UNIV" |
88 unfolding SUBSEQ_def |
109 unfolding SUPSEQ_def conc_def |
89 apply(auto) |
110 by (auto) (metis append_Cons emb_cons_leftD) |
90 apply(erule emb.cases) |
111 |
91 apply(auto)[3] |
112 lemma SUPSEQ_union [simp]: |
92 apply(rule emb0) |
113 shows "SUPSEQ (A \<union> B) = SUPSEQ A \<union> SUPSEQ B" |
93 done |
114 unfolding SUPSEQ_def by auto |
94 |
115 |
95 lemma SUBSEQ_atom [simp]: |
116 lemma SUPSEQ_conc [simp]: |
96 "SUBSEQ {[a]} = {[], [a]}" |
117 shows "SUPSEQ (A \<cdot> B) = SUPSEQ A \<cdot> SUPSEQ B" |
97 apply(auto simp add: SUBSEQ_def) |
118 unfolding SUPSEQ_def conc_def |
98 apply(erule emb.cases) |
119 by (auto) (metis emb_append_leftD) |
99 apply(auto)[3] |
120 |
100 apply(erule emb.cases) |
121 lemma SUPSEQ_star [simp]: |
101 apply(auto)[3] |
122 shows "SUPSEQ (A\<star>) = UNIV" |
102 apply(erule emb.cases) |
|
103 apply(auto)[3] |
|
104 apply(rule emb0) |
|
105 apply(rule emb2) |
|
106 apply(rule emb0) |
|
107 done |
|
108 |
|
109 lemma SUBSEQ_union [simp]: |
|
110 "SUBSEQ (A \<union> B) = SUBSEQ A \<union> SUBSEQ B" |
|
111 unfolding SUBSEQ_def by auto |
|
112 |
|
113 lemma SUBSEQ_Union [simp]: |
|
114 fixes A :: "nat \<Rightarrow> 'a lang" |
|
115 shows "SUBSEQ (\<Union>n. (A n)) = (\<Union>n. (SUBSEQ (A n)))" |
|
116 unfolding SUBSEQ_def image_def by auto |
|
117 |
|
118 lemma SUBSEQ_conc1: |
|
119 "\<lbrakk>x \<in> SUBSEQ A; y \<in> SUBSEQ B\<rbrakk> \<Longrightarrow> x @ y \<in> SUBSEQ (A \<cdot> B)" |
|
120 unfolding SUBSEQ_def |
|
121 apply(auto) |
|
122 apply(rule_tac x="xa @ xaa" in bexI) |
|
123 apply(rule emb_appendI) |
|
124 apply(simp_all) |
|
125 done |
|
126 |
|
127 lemma SUBSEQ_conc2: |
|
128 "x \<in> SUBSEQ (A \<cdot> B) \<Longrightarrow> x \<in> (SUBSEQ A) \<cdot> (SUBSEQ B)" |
|
129 unfolding SUBSEQ_def conc_def |
|
130 apply(auto) |
|
131 apply(drule emb_append) |
|
132 apply(auto) |
|
133 done |
|
134 |
|
135 lemma SUBSEQ_conc [simp]: |
|
136 "SUBSEQ (A \<cdot> B) = SUBSEQ A \<cdot> SUBSEQ B" |
|
137 apply(auto) |
|
138 apply(simp add: SUBSEQ_conc2) |
|
139 apply(subst (asm) conc_def) |
|
140 apply(auto simp add: SUBSEQ_conc1) |
|
141 done |
|
142 |
|
143 lemma SUBSEQ_star1: |
|
144 assumes a: "x \<in> (SUBSEQ A)\<star>" |
|
145 shows "x \<in> SUBSEQ (A\<star>)" |
|
146 using a |
|
147 apply(induct rule: star_induct) |
|
148 apply(simp add: SUBSEQ_def) |
|
149 apply(rule_tac x="[]" in bexI) |
|
150 apply(rule emb0) |
|
151 apply(auto)[1] |
|
152 apply(drule SUBSEQ_conc1) |
|
153 apply(assumption) |
|
154 apply(subst star_unfold_left) |
123 apply(subst star_unfold_left) |
155 apply(simp only: SUBSEQ_union) |
124 apply(simp only: SUPSEQ_union) |
156 apply(simp) |
125 apply(simp) |
157 done |
126 done |
158 |
|
159 lemma SUBSEQ_star2_aux: |
|
160 assumes a: "x \<in> SUBSEQ (A ^^ n)" |
|
161 shows "x \<in> (SUBSEQ A)\<star>" |
|
162 using a |
|
163 apply(induct n arbitrary: x) |
|
164 apply(simp) |
|
165 apply(simp) |
|
166 apply(simp add: conc_def) |
|
167 apply(auto) |
|
168 done |
|
169 |
|
170 lemma SUBSEQ_star2: |
|
171 assumes a: "x \<in> SUBSEQ (A\<star>)" |
|
172 shows "x \<in> (SUBSEQ A)\<star>" |
|
173 using a |
|
174 apply(subst (asm) star_def) |
|
175 apply(auto simp add: SUBSEQ_star2_aux) |
|
176 done |
|
177 |
|
178 lemma SUBSEQ_star [simp]: |
|
179 shows "SUBSEQ (A\<star>) = (SUBSEQ A)\<star>" |
|
180 using SUBSEQ_star1 SUBSEQ_star2 by auto |
|
181 |
|
182 lemma SUBSEQ_fold: |
|
183 shows "SUBSEQ A \<union> A = SUBSEQ A" |
|
184 apply(auto simp add: SUBSEQ_def) |
|
185 apply(rule_tac x="x" in bexI) |
|
186 apply(auto simp add: emb_refl) |
|
187 done |
|
188 |
|
189 |
|
190 lemma SUPSEQ_union [simp]: |
|
191 "SUPSEQ (A \<union> B) = (SUPSEQ A \<union> B) \<inter> (SUPSEQ B \<union> A)" |
|
192 unfolding SUPSEQ_def |
|
193 by auto |
|
194 |
|
195 |
|
196 definition |
|
197 Notreg :: "'a::finite rexp \<Rightarrow> 'a rexp" |
|
198 where |
|
199 "Notreg r \<equiv> SOME r'. lang r' = - (lang r)" |
|
200 |
|
201 lemma [simp]: |
|
202 "lang (Notreg r) = - lang r" |
|
203 apply(simp add: Notreg_def) |
|
204 apply(rule someI2_ex) |
|
205 apply(auto) |
|
206 apply(subgoal_tac "regular (lang r)") |
|
207 apply(drule closure_complement) |
|
208 apply(auto) |
|
209 done |
|
210 |
|
211 definition |
|
212 Interreg :: "'a::finite rexp \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp" |
|
213 where |
|
214 "Interreg r1 r2 = Notreg (Plus (Notreg r1) (Notreg r2))" |
|
215 |
|
216 lemma [simp]: |
|
217 "lang (Interreg r1 r2) = (lang r1) \<inter> (lang r2)" |
|
218 by (simp add: Interreg_def) |
|
219 |
|
220 definition |
|
221 Diffreg :: "'a::finite rexp \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp" |
|
222 where |
|
223 "Diffreg r1 r2 = Notreg (Plus (Notreg r1) r2)" |
|
224 |
|
225 lemma [simp]: |
|
226 "lang (Diffreg r1 r2) = (lang r1) - (lang r2)" |
|
227 by (auto simp add: Diffreg_def) |
|
228 |
127 |
229 definition |
128 definition |
230 Allreg :: "'a::finite rexp" |
129 Allreg :: "'a::finite rexp" |
231 where |
130 where |
232 "Allreg \<equiv> \<Uplus>(Atom ` UNIV)" |
131 "Allreg \<equiv> \<Uplus>(Atom ` UNIV)" |
233 |
132 |
234 lemma Allreg_lang [simp]: |
133 lemma Allreg_lang [simp]: |
235 "lang Allreg = (\<Union>a. {[a]})" |
134 shows "lang Allreg = (\<Union>a. {[a]})" |
236 unfolding Allreg_def |
135 unfolding Allreg_def by auto |
237 by auto |
|
238 |
136 |
239 lemma [simp]: |
137 lemma [simp]: |
240 "(\<Union>a. {[a]})\<star> = UNIV" |
138 shows "(\<Union>a. {[a]})\<star> = UNIV" |
241 apply(auto) |
139 apply(auto) |
242 apply(induct_tac x rule: list.induct) |
140 apply(induct_tac x rule: list.induct) |
243 apply(auto) |
141 apply(auto) |
244 apply(subgoal_tac "[a] @ list \<in> (\<Union>a. {[a]})\<star>") |
142 apply(subgoal_tac "[a] @ list \<in> (\<Union>a. {[a]})\<star>") |
245 apply(simp) |
143 apply(simp) |
246 apply(rule append_in_starI) |
144 apply(rule append_in_starI) |
247 apply(auto) |
145 apply(auto) |
248 done |
146 done |
249 |
147 |
250 lemma Star_Allreg_lang [simp]: |
148 lemma Star_Allreg_lang [simp]: |
251 "lang (Star Allreg) = UNIV" |
149 shows "lang (Star Allreg) = UNIV" |
252 by (simp) |
150 by simp |
253 |
151 |
254 fun UP :: "'a::finite rexp \<Rightarrow> 'a rexp" |
152 fun |
|
153 UP :: "'a::finite rexp \<Rightarrow> 'a rexp" |
255 where |
154 where |
256 "UP (Zero) = Star Allreg" |
155 "UP (Zero) = Zero" |
257 | "UP (One) = Star Allreg" |
156 | "UP (One) = Star Allreg" |
258 | "UP (Atom c) = Times Allreg (Star Allreg)" |
157 | "UP (Atom c) = Times (Star Allreg) (Times (Atom c) (Star Allreg))" |
259 | "UP (Plus r1 r2) = Interreg (Plus (UP r1) (r2)) (Plus (UP r2) r1)" |
158 | "UP (Plus r1 r2) = Plus (UP r1) (UP r2)" |
260 | "UP (Times r1 r2) = |
159 | "UP (Times r1 r2) = Times (UP r1) (UP r2)" |
261 Plus (Notreg (Times (Plus (Notreg (UP r1)) r1) (Plus (Notreg (UP r2)) r2))) (Times r1 r2)" |
160 | "UP (Star r) = Star Allreg" |
262 | "UP (Star r) = Plus (Notreg (Star (Plus (Notreg (UP r)) r))) (Star r)" |
161 |
263 |
162 lemma lang_UP: |
264 lemma UP: |
163 shows "lang (UP r) = SUPSEQ (lang r)" |
265 "lang (UP r) = SUPSEQ (lang r)" |
164 by (induct r) (simp_all) |
266 apply(induct r) |
165 |
267 apply(simp add: SUPSEQ_def) |
166 lemma regular_SUPSEQ: |
268 apply(simp add: SUPSEQ_def) |
167 fixes A::"'a::finite lang" |
269 apply(simp add: Compl_eq_Diff_UNIV) |
|
270 apply(auto)[1] |
|
271 apply(simp add: SUPSEQ_def) |
|
272 apply(simp add: Compl_eq_Diff_UNIV) |
|
273 apply(rule sym) |
|
274 apply(rule_tac s="UNIV - {[]}" in trans) |
|
275 apply(auto)[1] |
|
276 apply(auto simp add: conc_def)[1] |
|
277 apply(case_tac x) |
|
278 apply(simp) |
|
279 apply(simp) |
|
280 apply(rule_tac x="[a]" in exI) |
|
281 apply(simp) |
|
282 apply(simp) |
|
283 apply(simp) |
|
284 apply(simp add: SUPSEQ_def) |
|
285 apply(simp add: Un_Int_distrib2) |
|
286 apply(simp add: Compl_partition2) |
|
287 apply(simp add: SUBSEQ_fold) |
|
288 apply(simp add: Un_Diff) |
|
289 apply(simp add: SUPSEQ_def) |
|
290 apply(simp add: Un_Int_distrib2) |
|
291 apply(simp add: Compl_partition2) |
|
292 apply(simp add: SUBSEQ_fold) |
|
293 done |
|
294 |
|
295 lemma SUPSEQ_reg: |
|
296 fixes A :: "'a::finite lang" |
|
297 assumes "regular A" |
168 assumes "regular A" |
298 shows "regular (SUPSEQ A)" |
169 shows "regular (SUPSEQ A)" |
299 proof - |
170 proof - |
300 from assms obtain r::"'a::finite rexp" where eq: "lang r = A" by auto |
171 from assms obtain r::"'a::finite rexp" where "lang r = A" by auto |
301 moreover |
172 then have "lang (UP r) = SUPSEQ A" by (simp add: lang_UP) |
302 have "lang (UP r) = SUPSEQ (lang r)" by (rule UP) |
173 then show "regular (SUPSEQ A)" by auto |
303 ultimately show "regular (SUPSEQ A)" by auto |
174 qed |
304 qed |
175 |
305 |
176 lemma SUPSEQ_subset: |
306 |
177 shows "A \<subseteq> SUPSEQ A" |
307 |
178 unfolding SUPSEQ_def by auto |
|
179 |
|
180 lemma w3: |
|
181 assumes eq: "T = - (SUBSEQ A)" |
|
182 shows "T = SUPSEQ T" |
|
183 apply(rule) |
|
184 apply(rule SUPSEQ_subset) |
|
185 apply(rule ccontr) |
|
186 apply(auto) |
|
187 apply(rule ccontr) |
|
188 apply(subgoal_tac "x \<in> SUBSEQ A") |
|
189 prefer 2 |
|
190 apply(subst (asm) (2) eq) |
|
191 apply(simp) |
|
192 apply(simp add: SUPSEQ_def) |
|
193 apply(erule bexE) |
|
194 apply(subgoal_tac "y \<in> SUBSEQ A") |
|
195 prefer 2 |
|
196 apply(simp add: SUBSEQ_def) |
|
197 apply(erule bexE) |
|
198 apply(rule_tac x="xa" in bexI) |
|
199 apply(rule emb_trans) |
|
200 apply(assumption) |
|
201 apply(assumption) |
|
202 apply(assumption) |
|
203 apply(subst (asm) (2) eq) |
|
204 apply(simp) |
|
205 done |
|
206 |
|
207 lemma w4: |
|
208 shows "- (SUBSEQ A) = SUPSEQ (- (SUBSEQ A))" |
|
209 by (rule w3) (simp) |
|
210 |
|
211 definition |
|
212 "minimal_in x L \<equiv> \<forall>y \<in> L. y \<preceq> x \<longrightarrow> y = x" |
|
213 |
|
214 lemma minimal_in2: |
|
215 shows "minimal_in x L = (\<forall>y \<in> L. y \<preceq> x \<longrightarrow> x \<preceq> y)" |
|
216 by (auto simp add: minimal_in_def intro: emb_antisym) |
|
217 |
|
218 lemma higman: |
|
219 assumes "\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y \<longrightarrow> \<not>(x \<preceq> y) \<and> \<not>(y \<preceq> x)" |
|
220 shows "finite A" |
|
221 sorry |
|
222 |
|
223 lemma minimal: |
|
224 assumes "minimal_in x A" "minimal_in y A" |
|
225 and "x \<noteq> y" "x \<in> A" "y \<in> A" |
|
226 shows "\<not>(x \<preceq> y) \<and> \<not>(y \<preceq> x)" |
|
227 using assms unfolding minimal_in_def |
|
228 by auto |
|
229 |
|
230 lemma main_lemma: |
|
231 "\<exists>M. M \<subseteq> A \<and> finite M \<and> SUPSEQ A = SUPSEQ M" |
|
232 proof - |
|
233 def M \<equiv> "{x \<in> A. minimal_in x A}" |
|
234 have "M \<subseteq> A" unfolding M_def minimal_in_def by auto |
|
235 moreover |
|
236 have "finite M" |
|
237 apply(rule higman) |
|
238 unfolding M_def minimal_in_def |
|
239 by auto |
|
240 moreover |
|
241 have "SUPSEQ A \<subseteq> SUPSEQ M" |
|
242 apply(rule) |
|
243 apply(simp only: SUPSEQ_def) |
|
244 apply(auto)[1] |
|
245 using emb_wf |
|
246 apply(erule_tac Q="{y' \<in> A. y' \<preceq> x}" and x="y" in wfE_min) |
|
247 apply(simp) |
|
248 apply(simp) |
|
249 apply(rule_tac x="z" in bexI) |
|
250 apply(simp) |
|
251 apply(simp add: M_def) |
|
252 apply(simp add: minimal_in2) |
|
253 apply(rule ballI) |
|
254 apply(rule impI) |
|
255 apply(drule_tac x="ya" in meta_spec) |
|
256 apply(simp) |
|
257 apply(case_tac "ya = z") |
|
258 apply(auto)[1] |
|
259 apply(simp) |
|
260 by (metis emb_trans) |
|
261 moreover |
|
262 have "SUPSEQ M \<subseteq> SUPSEQ A" |
|
263 by (auto simp add: SUPSEQ_def M_def) |
|
264 ultimately |
|
265 show "\<exists>M. M \<subseteq> A \<and> finite M \<and> SUPSEQ A = SUPSEQ M" by blast |
|
266 qed |
|
267 |
|
268 lemma closure_SUPSEQ: |
|
269 fixes A::"'a::finite lang" |
|
270 shows "regular (SUPSEQ A)" |
|
271 proof - |
|
272 obtain M where a: "finite M" and b: "SUPSEQ A = SUPSEQ M" |
|
273 using main_lemma by blast |
|
274 have "regular M" using a by (rule finite_regular) |
|
275 then have "regular (SUPSEQ M)" by (rule regular_SUPSEQ) |
|
276 then show "regular (SUPSEQ A)" using b by simp |
|
277 qed |
|
278 |
|
279 lemma closure_SUBSEQ: |
|
280 fixes A::"'a::finite lang" |
|
281 shows "regular (SUBSEQ A)" |
|
282 proof - |
|
283 have "regular (SUPSEQ (- SUBSEQ A))" by (rule closure_SUPSEQ) |
|
284 then have "regular (- SUBSEQ A)" |
|
285 apply(subst w4) |
|
286 apply(assumption) |
|
287 done |
|
288 then have "regular (- (- (SUBSEQ A)))" by (rule closure_complement) |
|
289 then show "regular (SUBSEQ A)" by simp |
|
290 qed |
|
291 |
308 |
292 |
309 |
293 |
310 end |
294 end |