--- a/Closures2.thy Thu Sep 01 23:18:34 2011 +0000
+++ b/Closures2.thy Fri Sep 02 09:53:56 2011 +0000
@@ -5,6 +5,9 @@
(* "~~/src/HOL/Proofs/Extraction/Higman" *)
begin
+section {* Closure under @{text SUBSEQ} and @{text SUPSEQ} *}
+
+(* compatibility with Higman theory by Stefan *)
notation
emb ("_ \<preceq> _")
@@ -131,7 +134,7 @@
unfolding SUPSEQ_def by auto
lemma SUPSEQ_atom [simp]:
- shows "SUPSEQ {[a]} = UNIV \<cdot> {[a]} \<cdot> UNIV"
+ shows "SUPSEQ {[c]} = UNIV \<cdot> {[c]} \<cdot> UNIV"
unfolding SUPSEQ_def conc_def
by (auto) (metis append_Cons emb_cons_leftD)
@@ -204,106 +207,80 @@
shows "A \<subseteq> SUPSEQ A"
unfolding SUPSEQ_def by auto
-lemma w3:
- fixes T A::"letter lang"
- assumes eq: "T = - (SUBSEQ A)"
- shows "T = SUPSEQ T"
-apply(rule)
-apply(rule SUPSEQ_subset)
-apply(rule ccontr)
-apply(auto)
-apply(rule ccontr)
-apply(subgoal_tac "x \<in> SUBSEQ A")
-prefer 2
-apply(subst (asm) (2) eq)
-apply(simp)
-apply(simp add: SUPSEQ_def)
-apply(erule bexE)
-apply(subgoal_tac "y \<in> SUBSEQ A")
-prefer 2
-apply(simp add: SUBSEQ_def)
-apply(erule bexE)
-apply(rule_tac x="xa" in bexI)
-apply(rule emb_trans)
-apply(assumption)
-apply(assumption)
-apply(assumption)
-apply(subst (asm) (2) eq)
-apply(simp)
-done
+lemma SUBSEQ_complement:
+ shows "- (SUBSEQ A) = SUPSEQ (- (SUBSEQ A))"
+proof -
+ have "- (SUBSEQ A) \<subseteq> SUPSEQ (- (SUBSEQ A))"
+ by (rule SUPSEQ_subset)
+ moreover
+ have "SUPSEQ (- (SUBSEQ A)) \<subseteq> - (SUBSEQ A)"
+ proof (rule ccontr)
+ assume "\<not> (SUPSEQ (- (SUBSEQ A)) \<subseteq> - (SUBSEQ A))"
+ then obtain x where
+ a: "x \<in> SUPSEQ (- (SUBSEQ A))" and
+ b: "x \<notin> - (SUBSEQ A)" by auto
+
+ from a obtain y where c: "y \<in> - (SUBSEQ A)" and d: "y \<preceq> x"
+ by (auto simp add: SUPSEQ_def)
-lemma w4:
- shows "- (SUBSEQ A) = SUPSEQ (- (SUBSEQ A))"
-by (rule w3) (simp)
+ from b have "x \<in> SUBSEQ A" by simp
+ then obtain x' where f: "x' \<in> A" and e: "x \<preceq> x'"
+ by (auto simp add: SUBSEQ_def)
+
+ from d e have "y \<preceq> x'" by (rule emb_trans)
+ then have "y \<in> SUBSEQ A" using f
+ by (auto simp add: SUBSEQ_def)
+ with c show "False" by simp
+ qed
+ ultimately show "- (SUBSEQ A) = SUPSEQ (- (SUBSEQ A))" by simp
+qed
+
+lemma Higman_antichains:
+ assumes a: "\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y \<longrightarrow> \<not>(x \<preceq> y) \<and> \<not>(y \<preceq> x)"
+ shows "finite A"
+proof (rule ccontr)
+ assume "infinite A"
+ then obtain f::"nat \<Rightarrow> letter list" where b: "inj f" and c: "range f \<subseteq> A"
+ by (auto simp add: infinite_iff_countable_subset)
+ from higman_idx obtain i j where d: "i < j" and e: "f i \<preceq> f j" by blast
+ have "f i \<noteq> f j" using b d by (auto simp add: inj_on_def)
+ moreover
+ have "f i \<in> A" sorry
+ moreover
+ have "f j \<in> A" sorry
+ ultimately have "\<not>(f i \<preceq> f j)" using a by simp
+ with e show "False" by simp
+qed
definition
- minimal_in :: "letter list \<Rightarrow> letter lang \<Rightarrow> bool"
+ minimal :: "letter list \<Rightarrow> letter lang \<Rightarrow> bool"
where
- "minimal_in x A \<equiv> \<forall>y \<in> A. y \<preceq> x \<longrightarrow> y = x"
-
-lemma minimal_in2:
- shows "minimal_in x A = (\<forall>y \<in> A. y \<preceq> x \<longrightarrow> x \<preceq> y)"
-by (auto simp add: minimal_in_def intro: emb_antisym)
-
-lemma higman:
- assumes "\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y \<longrightarrow> \<not>(x \<preceq> y) \<and> \<not>(y \<preceq> x)"
- shows "finite A"
-apply(rule ccontr)
-apply(simp add: infinite_iff_countable_subset)
-apply(auto)
-apply(insert higman_idx)
-apply(drule_tac x="f" in meta_spec)
-apply(auto)
-using assms
-apply -
-apply(drule_tac x="f i" in bspec)
-apply(auto)[1]
-apply(drule_tac x="f j" in bspec)
-apply(auto)[1]
-apply(drule mp)
-apply(simp add: inj_on_def)
-apply(auto)[1]
-apply(auto)[1]
-done
-
-lemma minimal:
- assumes "minimal_in x A" "minimal_in y A"
- and "x \<noteq> y" "x \<in> A" "y \<in> A"
- shows "\<not>(x \<preceq> y) \<and> \<not>(y \<preceq> x)"
-using assms unfolding minimal_in_def
-by auto
+ "minimal x A = (\<forall>y \<in> A. y \<preceq> x \<longrightarrow> x \<preceq> y)"
lemma main_lemma:
- "\<exists>M. M \<subseteq> A \<and> finite M \<and> SUPSEQ A = SUPSEQ M"
+ shows "\<exists>M. M \<subseteq> A \<and> finite M \<and> SUPSEQ A = SUPSEQ M"
proof -
- def M \<equiv> "{x \<in> A. minimal_in x A}"
- have "M \<subseteq> A" unfolding M_def minimal_in_def by auto
+ def M \<equiv> "{x \<in> A. minimal x A}"
+ have "M \<subseteq> A" unfolding M_def minimal_def by auto
moreover
have "finite M"
- apply(rule higman)
- unfolding M_def minimal_in_def
- by auto
+ unfolding M_def minimal_def
+ by (rule Higman_antichains) (auto simp add: emb_antisym)
moreover
have "SUPSEQ A \<subseteq> SUPSEQ M"
- apply(rule)
- apply(simp only: SUPSEQ_def)
- apply(auto)[1]
- using emb_wf
- apply(erule_tac Q="{y' \<in> A. y' \<preceq> x}" and x="y" in wfE_min)
- apply(simp)
- apply(simp)
- apply(rule_tac x="z" in bexI)
- apply(simp)
- apply(simp add: M_def)
- apply(simp add: minimal_in2)
- apply(rule ballI)
- apply(rule impI)
- apply(drule_tac x="ya" in meta_spec)
- apply(simp)
- apply(case_tac "ya = z")
- apply(auto)[1]
- apply(simp)
- by (metis emb_trans)
+ proof
+ fix x
+ assume "x \<in> SUPSEQ A"
+ then obtain y where "y \<in> A" and "y \<preceq> x" by (auto simp add: SUPSEQ_def)
+ then have a: "y \<in> {y' \<in> A. y' \<preceq> x}" by simp
+ 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}"
+ using wfE_min[OF emb_wf a] by auto
+ then have "z \<in> M"
+ unfolding M_def minimal_def
+ by (auto intro: emb_trans)
+ with b show "x \<in> SUPSEQ M"
+ by (auto simp add: SUPSEQ_def)
+ qed
moreover
have "SUPSEQ M \<subseteq> SUPSEQ A"
by (auto simp add: SUPSEQ_def M_def)
@@ -327,14 +304,9 @@
shows "regular (SUBSEQ A)"
proof -
have "regular (SUPSEQ (- SUBSEQ A))" by (rule closure_SUPSEQ)
- then have "regular (- SUBSEQ A)"
- apply(subst w4)
- apply(assumption)
- done
+ then have "regular (- SUBSEQ A)" by (subst SUBSEQ_complement) (simp)
then have "regular (- (- (SUBSEQ A)))" by (rule closure_complement)
then show "regular (SUBSEQ A)" by simp
qed
-
-
end