--- a/Closures2.thy	Thu Sep 01 20:26:30 2011 +0000
+++ b/Closures2.thy	Thu Sep 01 23:18:34 2011 +0000
@@ -1,24 +1,50 @@
 theory Closure2
 imports 
   Closures
+  Higman
   (* "~~/src/HOL/Proofs/Extraction/Higman" *)
 begin
 
+notation
+  emb ("_ \<preceq> _")
+
+declare  emb0 [intro]
+declare  emb1 [intro]
+declare  emb2 [intro]
+
+lemma letter_UNIV:
+  shows "UNIV = {A, B::letter}"
+apply(auto)
+apply(case_tac x)
+apply(auto)
+done
+
+instance letter :: finite
+apply(default)
+apply(simp add: letter_UNIV)
+done
+
+hide_const A
+hide_const B
+
+(*
 inductive 
   emb :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<preceq> _")
 where
    emb0 [intro]: "emb [] y"
  | emb1 [intro]: "emb x y \<Longrightarrow> emb x (c # y)"
  | emb2 [intro]: "emb x y \<Longrightarrow> emb (c # x) (c # y)"
+*)
 
 lemma emb_refl [intro]:
   shows "x \<preceq> x"
-by (induct x) (auto intro: emb.intros)
+by (induct x) (auto)
 
 lemma emb_right [intro]:
   assumes a: "x \<preceq> y"
   shows "x \<preceq> y @ y'"
-using a by (induct arbitrary: y') (auto)
+using a 
+by (induct arbitrary: y') (auto)
 
 lemma emb_left [intro]:
   assumes a: "x \<preceq> y"
@@ -160,15 +186,16 @@
 | "UP (Star r) = Star Allreg"
 
 lemma lang_UP:
+  fixes r::"letter rexp"
   shows "lang (UP r) = SUPSEQ (lang r)"
 by (induct r) (simp_all)
 
 lemma regular_SUPSEQ: 
-  fixes A::"'a::finite lang"
+  fixes A::"letter lang"
   assumes "regular A"
   shows "regular (SUPSEQ A)"
 proof -
-  from assms obtain r::"'a::finite rexp" where "lang r = A" by auto
+  from assms obtain r::"letter 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
@@ -178,6 +205,7 @@
 unfolding SUPSEQ_def by auto
 
 lemma w3:
+  fixes T A::"letter lang"
   assumes eq: "T = - (SUBSEQ A)"
   shows "T = SUPSEQ T"
 apply(rule)
@@ -209,16 +237,34 @@
 by (rule w3) (simp)
 
 definition
-  "minimal_in x L \<equiv> \<forall>y \<in> L. y \<preceq> x \<longrightarrow> y = x"
+  minimal_in :: "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 L = (\<forall>y \<in> L. y \<preceq> x \<longrightarrow> x \<preceq> y)"
+  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"
-sorry
+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"
@@ -266,7 +312,7 @@
 qed
 
 lemma closure_SUPSEQ:
-  fixes A::"'a::finite lang" 
+  fixes A::"letter lang" 
   shows "regular (SUPSEQ A)"
 proof -
   obtain M where a: "finite M" and b: "SUPSEQ A = SUPSEQ M"
@@ -277,7 +323,7 @@
 qed
 
 lemma closure_SUBSEQ:
-  fixes A::"'a::finite lang"
+  fixes A::"letter lang"
   shows "regular (SUBSEQ A)"
 proof -
   have "regular (SUPSEQ (- SUBSEQ A))" by (rule closure_SUPSEQ)