1 theory Closure2 |
1 theory Closure2 |
2 imports |
2 imports |
3 Closures |
3 Closures |
|
4 Higman |
4 (* "~~/src/HOL/Proofs/Extraction/Higman" *) |
5 (* "~~/src/HOL/Proofs/Extraction/Higman" *) |
5 begin |
6 begin |
6 |
7 |
|
8 notation |
|
9 emb ("_ \<preceq> _") |
|
10 |
|
11 declare emb0 [intro] |
|
12 declare emb1 [intro] |
|
13 declare emb2 [intro] |
|
14 |
|
15 lemma letter_UNIV: |
|
16 shows "UNIV = {A, B::letter}" |
|
17 apply(auto) |
|
18 apply(case_tac x) |
|
19 apply(auto) |
|
20 done |
|
21 |
|
22 instance letter :: finite |
|
23 apply(default) |
|
24 apply(simp add: letter_UNIV) |
|
25 done |
|
26 |
|
27 hide_const A |
|
28 hide_const B |
|
29 |
|
30 (* |
7 inductive |
31 inductive |
8 emb :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<preceq> _") |
32 emb :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<preceq> _") |
9 where |
33 where |
10 emb0 [intro]: "emb [] y" |
34 emb0 [intro]: "emb [] y" |
11 | emb1 [intro]: "emb x y \<Longrightarrow> emb x (c # y)" |
35 | emb1 [intro]: "emb x y \<Longrightarrow> emb x (c # y)" |
12 | emb2 [intro]: "emb x y \<Longrightarrow> emb (c # x) (c # y)" |
36 | emb2 [intro]: "emb x y \<Longrightarrow> emb (c # x) (c # y)" |
|
37 *) |
13 |
38 |
14 lemma emb_refl [intro]: |
39 lemma emb_refl [intro]: |
15 shows "x \<preceq> x" |
40 shows "x \<preceq> x" |
16 by (induct x) (auto intro: emb.intros) |
41 by (induct x) (auto) |
17 |
42 |
18 lemma emb_right [intro]: |
43 lemma emb_right [intro]: |
19 assumes a: "x \<preceq> y" |
44 assumes a: "x \<preceq> y" |
20 shows "x \<preceq> y @ y'" |
45 shows "x \<preceq> y @ y'" |
21 using a by (induct arbitrary: y') (auto) |
46 using a |
|
47 by (induct arbitrary: y') (auto) |
22 |
48 |
23 lemma emb_left [intro]: |
49 lemma emb_left [intro]: |
24 assumes a: "x \<preceq> y" |
50 assumes a: "x \<preceq> y" |
25 shows "x \<preceq> y' @ y" |
51 shows "x \<preceq> y' @ y" |
26 using a by (induct y') (auto) |
52 using a by (induct y') (auto) |
158 | "UP (Plus r1 r2) = Plus (UP r1) (UP r2)" |
184 | "UP (Plus r1 r2) = Plus (UP r1) (UP r2)" |
159 | "UP (Times r1 r2) = Times (UP r1) (UP r2)" |
185 | "UP (Times r1 r2) = Times (UP r1) (UP r2)" |
160 | "UP (Star r) = Star Allreg" |
186 | "UP (Star r) = Star Allreg" |
161 |
187 |
162 lemma lang_UP: |
188 lemma lang_UP: |
|
189 fixes r::"letter rexp" |
163 shows "lang (UP r) = SUPSEQ (lang r)" |
190 shows "lang (UP r) = SUPSEQ (lang r)" |
164 by (induct r) (simp_all) |
191 by (induct r) (simp_all) |
165 |
192 |
166 lemma regular_SUPSEQ: |
193 lemma regular_SUPSEQ: |
167 fixes A::"'a::finite lang" |
194 fixes A::"letter lang" |
168 assumes "regular A" |
195 assumes "regular A" |
169 shows "regular (SUPSEQ A)" |
196 shows "regular (SUPSEQ A)" |
170 proof - |
197 proof - |
171 from assms obtain r::"'a::finite rexp" where "lang r = A" by auto |
198 from assms obtain r::"letter rexp" where "lang r = A" by auto |
172 then have "lang (UP r) = SUPSEQ A" by (simp add: lang_UP) |
199 then have "lang (UP r) = SUPSEQ A" by (simp add: lang_UP) |
173 then show "regular (SUPSEQ A)" by auto |
200 then show "regular (SUPSEQ A)" by auto |
174 qed |
201 qed |
175 |
202 |
176 lemma SUPSEQ_subset: |
203 lemma SUPSEQ_subset: |
177 shows "A \<subseteq> SUPSEQ A" |
204 shows "A \<subseteq> SUPSEQ A" |
178 unfolding SUPSEQ_def by auto |
205 unfolding SUPSEQ_def by auto |
179 |
206 |
180 lemma w3: |
207 lemma w3: |
|
208 fixes T A::"letter lang" |
181 assumes eq: "T = - (SUBSEQ A)" |
209 assumes eq: "T = - (SUBSEQ A)" |
182 shows "T = SUPSEQ T" |
210 shows "T = SUPSEQ T" |
183 apply(rule) |
211 apply(rule) |
184 apply(rule SUPSEQ_subset) |
212 apply(rule SUPSEQ_subset) |
185 apply(rule ccontr) |
213 apply(rule ccontr) |
207 lemma w4: |
235 lemma w4: |
208 shows "- (SUBSEQ A) = SUPSEQ (- (SUBSEQ A))" |
236 shows "- (SUBSEQ A) = SUPSEQ (- (SUBSEQ A))" |
209 by (rule w3) (simp) |
237 by (rule w3) (simp) |
210 |
238 |
211 definition |
239 definition |
212 "minimal_in x L \<equiv> \<forall>y \<in> L. y \<preceq> x \<longrightarrow> y = x" |
240 minimal_in :: "letter list \<Rightarrow> letter lang \<Rightarrow> bool" |
|
241 where |
|
242 "minimal_in x A \<equiv> \<forall>y \<in> A. y \<preceq> x \<longrightarrow> y = x" |
213 |
243 |
214 lemma minimal_in2: |
244 lemma minimal_in2: |
215 shows "minimal_in x L = (\<forall>y \<in> L. y \<preceq> x \<longrightarrow> x \<preceq> y)" |
245 shows "minimal_in x A = (\<forall>y \<in> A. y \<preceq> x \<longrightarrow> x \<preceq> y)" |
216 by (auto simp add: minimal_in_def intro: emb_antisym) |
246 by (auto simp add: minimal_in_def intro: emb_antisym) |
217 |
247 |
218 lemma higman: |
248 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)" |
249 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" |
250 shows "finite A" |
221 sorry |
251 apply(rule ccontr) |
|
252 apply(simp add: infinite_iff_countable_subset) |
|
253 apply(auto) |
|
254 apply(insert higman_idx) |
|
255 apply(drule_tac x="f" in meta_spec) |
|
256 apply(auto) |
|
257 using assms |
|
258 apply - |
|
259 apply(drule_tac x="f i" in bspec) |
|
260 apply(auto)[1] |
|
261 apply(drule_tac x="f j" in bspec) |
|
262 apply(auto)[1] |
|
263 apply(drule mp) |
|
264 apply(simp add: inj_on_def) |
|
265 apply(auto)[1] |
|
266 apply(auto)[1] |
|
267 done |
222 |
268 |
223 lemma minimal: |
269 lemma minimal: |
224 assumes "minimal_in x A" "minimal_in y A" |
270 assumes "minimal_in x A" "minimal_in y A" |
225 and "x \<noteq> y" "x \<in> A" "y \<in> A" |
271 and "x \<noteq> y" "x \<in> A" "y \<in> A" |
226 shows "\<not>(x \<preceq> y) \<and> \<not>(y \<preceq> x)" |
272 shows "\<not>(x \<preceq> y) \<and> \<not>(y \<preceq> x)" |
264 ultimately |
310 ultimately |
265 show "\<exists>M. M \<subseteq> A \<and> finite M \<and> SUPSEQ A = SUPSEQ M" by blast |
311 show "\<exists>M. M \<subseteq> A \<and> finite M \<and> SUPSEQ A = SUPSEQ M" by blast |
266 qed |
312 qed |
267 |
313 |
268 lemma closure_SUPSEQ: |
314 lemma closure_SUPSEQ: |
269 fixes A::"'a::finite lang" |
315 fixes A::"letter lang" |
270 shows "regular (SUPSEQ A)" |
316 shows "regular (SUPSEQ A)" |
271 proof - |
317 proof - |
272 obtain M where a: "finite M" and b: "SUPSEQ A = SUPSEQ M" |
318 obtain M where a: "finite M" and b: "SUPSEQ A = SUPSEQ M" |
273 using main_lemma by blast |
319 using main_lemma by blast |
274 have "regular M" using a by (rule finite_regular) |
320 have "regular M" using a by (rule finite_regular) |
275 then have "regular (SUPSEQ M)" by (rule regular_SUPSEQ) |
321 then have "regular (SUPSEQ M)" by (rule regular_SUPSEQ) |
276 then show "regular (SUPSEQ A)" using b by simp |
322 then show "regular (SUPSEQ A)" using b by simp |
277 qed |
323 qed |
278 |
324 |
279 lemma closure_SUBSEQ: |
325 lemma closure_SUBSEQ: |
280 fixes A::"'a::finite lang" |
326 fixes A::"letter lang" |
281 shows "regular (SUBSEQ A)" |
327 shows "regular (SUBSEQ A)" |
282 proof - |
328 proof - |
283 have "regular (SUPSEQ (- SUBSEQ A))" by (rule closure_SUPSEQ) |
329 have "regular (SUPSEQ (- SUBSEQ A))" by (rule closure_SUPSEQ) |
284 then have "regular (- SUBSEQ A)" |
330 then have "regular (- SUBSEQ A)" |
285 apply(subst w4) |
331 apply(subst w4) |