--- a/Closures2.thy	Wed Aug 29 13:05:46 2012 +0000
+++ b/Closures2.thy	Wed Aug 29 13:09:36 2012 +0000
@@ -1,7 +1,8 @@
 theory Closures2
 imports 
   Closures
-  Higman
+  (*Higman*)
+  WQO_Finite_Lists
 begin
 
 section {* Closure under @{text SUBSEQ} and @{text SUPSEQ} *}
@@ -14,6 +15,7 @@
 declare  emb1 [intro]
 declare  emb2 [intro]
 
+(*
 lemma letter_UNIV:
   shows "UNIV = {A, B::letter}"
 apply(auto)
@@ -29,7 +31,7 @@
 hide_const A
 hide_const B
 hide_const R
-
+*)
 (*
 inductive 
   emb :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<preceq> _")
@@ -190,16 +192,16 @@
 | "UP (Star r) = Star Allreg"
 
 lemma lang_UP:
-  fixes r::"letter rexp"
+  fixes r::"'a::finite rexp"
   shows "lang (UP r) = SUPSEQ (lang r)"
 by (induct r) (simp_all)
 
 lemma regular_SUPSEQ: 
-  fixes A::"letter lang"
+  fixes A::"('a::finite) lang"
   assumes "regular A"
   shows "regular (SUPSEQ A)"
 proof -
-  from assms obtain r::"letter rexp" where "lang r = A" by auto
+  from assms obtain r::"'a::finite rexp" where "lang r = A" by auto
   then have "lang (UP r) = SUPSEQ A" by (simp add: lang_UP)
   then show "regular (SUPSEQ A)" by auto
 qed
@@ -236,6 +238,7 @@
   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"
@@ -252,13 +255,15 @@
   ultimately have "\<not>(f i \<preceq> f j)" using a by simp
   with e show "False" by simp
 qed
+*)
 
 definition
-  minimal :: "letter list \<Rightarrow> letter lang \<Rightarrow> bool"
+  minimal :: "'a::finite list \<Rightarrow> 'a lang \<Rightarrow> bool"
 where
   "minimal x A \<equiv> (\<forall>y \<in> A. y \<preceq> x \<longrightarrow> x \<preceq> y)"
 
 lemma main_lemma:
+  fixes A::"('a::finite) list set" 
   shows "\<exists>M. finite M \<and> SUPSEQ A = SUPSEQ M"
 proof -
   def M \<equiv> "{x \<in> A. minimal x A}"
@@ -288,7 +293,7 @@
 qed
 
 lemma closure_SUPSEQ:
-  fixes A::"letter lang" 
+  fixes A::"'a::finite lang" 
   shows "regular (SUPSEQ A)"
 proof -
   obtain M where a: "finite M" and b: "SUPSEQ A = SUPSEQ M"
@@ -299,7 +304,7 @@
 qed
 
 lemma closure_SUBSEQ:
-  fixes A::"letter lang"
+  fixes A::"'a::finite lang"
   shows "regular (SUBSEQ A)"
 proof -
   have "regular (SUPSEQ (- SUBSEQ A))" by (rule closure_SUPSEQ)