equal
deleted
inserted
replaced
1 theory Closure2 |
1 theory Closures2 |
2 imports |
2 imports |
3 Closures |
3 Closures |
4 Higman |
4 Higman |
5 (* "~~/src/HOL/Proofs/Extraction/Higman" *) |
5 (* "~~/src/HOL/Proofs/Extraction/Higman" *) |
6 begin |
6 begin |
27 apply(simp add: letter_UNIV) |
27 apply(simp add: letter_UNIV) |
28 done |
28 done |
29 |
29 |
30 hide_const A |
30 hide_const A |
31 hide_const B |
31 hide_const B |
|
32 hide_const R |
32 |
33 |
33 (* |
34 (* |
34 inductive |
35 inductive |
35 emb :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<preceq> _") |
36 emb :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<preceq> _") |
36 where |
37 where |
253 qed |
254 qed |
254 |
255 |
255 definition |
256 definition |
256 minimal :: "letter list \<Rightarrow> letter lang \<Rightarrow> bool" |
257 minimal :: "letter list \<Rightarrow> letter lang \<Rightarrow> bool" |
257 where |
258 where |
258 "minimal x A = (\<forall>y \<in> A. y \<preceq> x \<longrightarrow> x \<preceq> y)" |
259 "minimal x A \<equiv> (\<forall>y \<in> A. y \<preceq> x \<longrightarrow> x \<preceq> y)" |
259 |
260 |
260 lemma main_lemma: |
261 lemma main_lemma: |
261 shows "\<exists>M. M \<subseteq> A \<and> finite M \<and> SUPSEQ A = SUPSEQ M" |
262 shows "\<exists>M. finite M \<and> SUPSEQ A = SUPSEQ M" |
262 proof - |
263 proof - |
263 def M \<equiv> "{x \<in> A. minimal x A}" |
264 def M \<equiv> "{x \<in> A. minimal x A}" |
264 have "M \<subseteq> A" unfolding M_def minimal_def by auto |
|
265 moreover |
|
266 have "finite M" |
265 have "finite M" |
267 unfolding M_def minimal_def |
266 unfolding M_def minimal_def |
268 by (rule Higman_antichains) (auto simp add: emb_antisym) |
267 by (rule Higman_antichains) (auto simp add: emb_antisym) |
269 moreover |
268 moreover |
270 have "SUPSEQ A \<subseteq> SUPSEQ M" |
269 have "SUPSEQ A \<subseteq> SUPSEQ M" |
276 obtain z where b: "z \<in> A" "z \<preceq> x" and c: "\<forall>y. y \<preceq> z \<and> y \<noteq> z \<longrightarrow> y \<notin> {y' \<in> A. y' \<preceq> x}" |
275 obtain z where b: "z \<in> A" "z \<preceq> x" and c: "\<forall>y. y \<preceq> z \<and> y \<noteq> z \<longrightarrow> y \<notin> {y' \<in> A. y' \<preceq> x}" |
277 using wfE_min[OF emb_wf a] by auto |
276 using wfE_min[OF emb_wf a] by auto |
278 then have "z \<in> M" |
277 then have "z \<in> M" |
279 unfolding M_def minimal_def |
278 unfolding M_def minimal_def |
280 by (auto intro: emb_trans) |
279 by (auto intro: emb_trans) |
281 with b show "x \<in> SUPSEQ M" |
280 with b(2) show "x \<in> SUPSEQ M" |
282 by (auto simp add: SUPSEQ_def) |
281 by (auto simp add: SUPSEQ_def) |
283 qed |
282 qed |
284 moreover |
283 moreover |
285 have "SUPSEQ M \<subseteq> SUPSEQ A" |
284 have "SUPSEQ M \<subseteq> SUPSEQ A" |
286 by (auto simp add: SUPSEQ_def M_def) |
285 by (auto simp add: SUPSEQ_def M_def) |
287 ultimately |
286 ultimately |
288 show "\<exists>M. M \<subseteq> A \<and> finite M \<and> SUPSEQ A = SUPSEQ M" by blast |
287 show "\<exists>M. finite M \<and> SUPSEQ A = SUPSEQ M" by blast |
289 qed |
288 qed |
290 |
289 |
291 lemma closure_SUPSEQ: |
290 lemma closure_SUPSEQ: |
292 fixes A::"letter lang" |
291 fixes A::"letter lang" |
293 shows "regular (SUPSEQ A)" |
292 shows "regular (SUPSEQ A)" |