202 |
205 |
203 lemma SUPSEQ_subset: |
206 lemma SUPSEQ_subset: |
204 shows "A \<subseteq> SUPSEQ A" |
207 shows "A \<subseteq> SUPSEQ A" |
205 unfolding SUPSEQ_def by auto |
208 unfolding SUPSEQ_def by auto |
206 |
209 |
207 lemma w3: |
210 lemma SUBSEQ_complement: |
208 fixes T A::"letter lang" |
|
209 assumes eq: "T = - (SUBSEQ A)" |
|
210 shows "T = SUPSEQ T" |
|
211 apply(rule) |
|
212 apply(rule SUPSEQ_subset) |
|
213 apply(rule ccontr) |
|
214 apply(auto) |
|
215 apply(rule ccontr) |
|
216 apply(subgoal_tac "x \<in> SUBSEQ A") |
|
217 prefer 2 |
|
218 apply(subst (asm) (2) eq) |
|
219 apply(simp) |
|
220 apply(simp add: SUPSEQ_def) |
|
221 apply(erule bexE) |
|
222 apply(subgoal_tac "y \<in> SUBSEQ A") |
|
223 prefer 2 |
|
224 apply(simp add: SUBSEQ_def) |
|
225 apply(erule bexE) |
|
226 apply(rule_tac x="xa" in bexI) |
|
227 apply(rule emb_trans) |
|
228 apply(assumption) |
|
229 apply(assumption) |
|
230 apply(assumption) |
|
231 apply(subst (asm) (2) eq) |
|
232 apply(simp) |
|
233 done |
|
234 |
|
235 lemma w4: |
|
236 shows "- (SUBSEQ A) = SUPSEQ (- (SUBSEQ A))" |
211 shows "- (SUBSEQ A) = SUPSEQ (- (SUBSEQ A))" |
237 by (rule w3) (simp) |
212 proof - |
|
213 have "- (SUBSEQ A) \<subseteq> SUPSEQ (- (SUBSEQ A))" |
|
214 by (rule SUPSEQ_subset) |
|
215 moreover |
|
216 have "SUPSEQ (- (SUBSEQ A)) \<subseteq> - (SUBSEQ A)" |
|
217 proof (rule ccontr) |
|
218 assume "\<not> (SUPSEQ (- (SUBSEQ A)) \<subseteq> - (SUBSEQ A))" |
|
219 then obtain x where |
|
220 a: "x \<in> SUPSEQ (- (SUBSEQ A))" and |
|
221 b: "x \<notin> - (SUBSEQ A)" by auto |
|
222 |
|
223 from a obtain y where c: "y \<in> - (SUBSEQ A)" and d: "y \<preceq> x" |
|
224 by (auto simp add: SUPSEQ_def) |
|
225 |
|
226 from b have "x \<in> SUBSEQ A" by simp |
|
227 then obtain x' where f: "x' \<in> A" and e: "x \<preceq> x'" |
|
228 by (auto simp add: SUBSEQ_def) |
|
229 |
|
230 from d e have "y \<preceq> x'" by (rule emb_trans) |
|
231 then have "y \<in> SUBSEQ A" using f |
|
232 by (auto simp add: SUBSEQ_def) |
|
233 with c show "False" by simp |
|
234 qed |
|
235 ultimately show "- (SUBSEQ A) = SUPSEQ (- (SUBSEQ A))" by simp |
|
236 qed |
|
237 |
|
238 lemma Higman_antichains: |
|
239 assumes a: "\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y \<longrightarrow> \<not>(x \<preceq> y) \<and> \<not>(y \<preceq> x)" |
|
240 shows "finite A" |
|
241 proof (rule ccontr) |
|
242 assume "infinite A" |
|
243 then obtain f::"nat \<Rightarrow> letter list" where b: "inj f" and c: "range f \<subseteq> A" |
|
244 by (auto simp add: infinite_iff_countable_subset) |
|
245 from higman_idx obtain i j where d: "i < j" and e: "f i \<preceq> f j" by blast |
|
246 have "f i \<noteq> f j" using b d by (auto simp add: inj_on_def) |
|
247 moreover |
|
248 have "f i \<in> A" sorry |
|
249 moreover |
|
250 have "f j \<in> A" sorry |
|
251 ultimately have "\<not>(f i \<preceq> f j)" using a by simp |
|
252 with e show "False" by simp |
|
253 qed |
238 |
254 |
239 definition |
255 definition |
240 minimal_in :: "letter list \<Rightarrow> letter lang \<Rightarrow> bool" |
256 minimal :: "letter list \<Rightarrow> letter lang \<Rightarrow> bool" |
241 where |
257 where |
242 "minimal_in x A \<equiv> \<forall>y \<in> A. y \<preceq> x \<longrightarrow> y = x" |
258 "minimal x A = (\<forall>y \<in> A. y \<preceq> x \<longrightarrow> x \<preceq> y)" |
243 |
|
244 lemma minimal_in2: |
|
245 shows "minimal_in x A = (\<forall>y \<in> A. y \<preceq> x \<longrightarrow> x \<preceq> y)" |
|
246 by (auto simp add: minimal_in_def intro: emb_antisym) |
|
247 |
|
248 lemma higman: |
|
249 assumes "\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y \<longrightarrow> \<not>(x \<preceq> y) \<and> \<not>(y \<preceq> x)" |
|
250 shows "finite A" |
|
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 |
|
268 |
|
269 lemma minimal: |
|
270 assumes "minimal_in x A" "minimal_in y A" |
|
271 and "x \<noteq> y" "x \<in> A" "y \<in> A" |
|
272 shows "\<not>(x \<preceq> y) \<and> \<not>(y \<preceq> x)" |
|
273 using assms unfolding minimal_in_def |
|
274 by auto |
|
275 |
259 |
276 lemma main_lemma: |
260 lemma main_lemma: |
277 "\<exists>M. M \<subseteq> A \<and> finite M \<and> SUPSEQ A = SUPSEQ M" |
261 shows "\<exists>M. M \<subseteq> A \<and> finite M \<and> SUPSEQ A = SUPSEQ M" |
278 proof - |
262 proof - |
279 def M \<equiv> "{x \<in> A. minimal_in x A}" |
263 def M \<equiv> "{x \<in> A. minimal x A}" |
280 have "M \<subseteq> A" unfolding M_def minimal_in_def by auto |
264 have "M \<subseteq> A" unfolding M_def minimal_def by auto |
281 moreover |
265 moreover |
282 have "finite M" |
266 have "finite M" |
283 apply(rule higman) |
267 unfolding M_def minimal_def |
284 unfolding M_def minimal_in_def |
268 by (rule Higman_antichains) (auto simp add: emb_antisym) |
285 by auto |
|
286 moreover |
269 moreover |
287 have "SUPSEQ A \<subseteq> SUPSEQ M" |
270 have "SUPSEQ A \<subseteq> SUPSEQ M" |
288 apply(rule) |
271 proof |
289 apply(simp only: SUPSEQ_def) |
272 fix x |
290 apply(auto)[1] |
273 assume "x \<in> SUPSEQ A" |
291 using emb_wf |
274 then obtain y where "y \<in> A" and "y \<preceq> x" by (auto simp add: SUPSEQ_def) |
292 apply(erule_tac Q="{y' \<in> A. y' \<preceq> x}" and x="y" in wfE_min) |
275 then have a: "y \<in> {y' \<in> A. y' \<preceq> x}" by simp |
293 apply(simp) |
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}" |
294 apply(simp) |
277 using wfE_min[OF emb_wf a] by auto |
295 apply(rule_tac x="z" in bexI) |
278 then have "z \<in> M" |
296 apply(simp) |
279 unfolding M_def minimal_def |
297 apply(simp add: M_def) |
280 by (auto intro: emb_trans) |
298 apply(simp add: minimal_in2) |
281 with b show "x \<in> SUPSEQ M" |
299 apply(rule ballI) |
282 by (auto simp add: SUPSEQ_def) |
300 apply(rule impI) |
283 qed |
301 apply(drule_tac x="ya" in meta_spec) |
|
302 apply(simp) |
|
303 apply(case_tac "ya = z") |
|
304 apply(auto)[1] |
|
305 apply(simp) |
|
306 by (metis emb_trans) |
|
307 moreover |
284 moreover |
308 have "SUPSEQ M \<subseteq> SUPSEQ A" |
285 have "SUPSEQ M \<subseteq> SUPSEQ A" |
309 by (auto simp add: SUPSEQ_def M_def) |
286 by (auto simp add: SUPSEQ_def M_def) |
310 ultimately |
287 ultimately |
311 show "\<exists>M. M \<subseteq> A \<and> finite M \<and> SUPSEQ A = SUPSEQ M" by blast |
288 show "\<exists>M. M \<subseteq> A \<and> finite M \<and> SUPSEQ A = SUPSEQ M" by blast |