# HG changeset patch
# User urbanc
# Date 1314957236 0
# Node ID 5f7b7ad498dd756a1dde554f84c4752c9bdc5d8c
# Parent  191769fc68c3bf71e602446ab30a9452623bcaf3
cleaned up proofs

diff -r 191769fc68c3 -r 5f7b7ad498dd Closures2.thy
--- 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