# HG changeset patch
# User urbanc
# Date 1314170662 0
# Node ID 580e0632917147a3493f6b73db66ea87cba4bf63
# Parent  300198795eb42373c1e2714ba99d5b8509c999bc
just test

diff -r 300198795eb4 -r 580e06329171 Higman2.thy
--- a/Higman2.thy	Tue Aug 23 12:36:43 2011 +0000
+++ b/Higman2.thy	Wed Aug 24 07:24:22 2011 +0000
@@ -6,7 +6,7 @@
 header {* Higman's lemma *}
 
 theory Higman2
-imports Closures
+imports Main
 begin
 
 text {*
@@ -233,18 +233,28 @@
   qed
 qed
 
-inductive substring ("_ \<preceq> _")
-where
-  "[] \<preceq> y"
-| "x \<preceq> y \<Longrightarrow> c # x \<preceq> y"
-| "x \<preceq> y \<Longrightarrow> c # x \<preceq> c # y" 
+notation
+  emb ("_ \<preceq> _")
+
+
 
 lemma substring_refl:
   "x \<preceq> x"
 apply(induct x)
-apply(auto intro: substring.intros)
+apply(auto intro: emb.intros)
 done
 
+lemma substring_trans:
+  assumes a: "x1 \<preceq> x2" and b: "x2 \<preceq> x3"
+  shows "x1 \<preceq> x3"
+using a b
+apply(induct arbitrary: x3)
+apply(auto intro: emb.intros)
+apply(rotate_tac 2)
+apply(erule emb.cases)
+apply(simp_all)
+sorry 
+
 definition
  "SUBSEQ C \<equiv> {x. \<exists>y \<in> C. x \<preceq> y}"
 
@@ -252,30 +262,56 @@
  "SUBSEQ (SUBSEQ C) = SUBSEQ C"
 unfolding SUBSEQ_def
 apply(auto)
-apply(erule substring.induct)
+apply(erule emb.induct)
 apply(rule_tac x="xb" in bexI)
-apply(rule substring.intros)
+apply(rule emb.intros)
 apply(simp)
 apply(erule bexE)
-apply(rule_tac x="ya" in bexI)
-apply(rule substring.intros)
+apply(rule_tac x="y" in bexI)
 apply(auto)[2]
 apply(erule bexE)
-apply(rule_tac x="ya" in bexI)
-apply(rule substring.intros)
-apply(auto)[2]
-apply(rule_tac x="x" in exI)
-apply(rule conjI)
-apply(rule_tac x="y" in bexI)
-apply(auto)[2]
-apply(rule substring_refl)
-done
+sorry
 
-lemma
+lemma substring_closed:
   "x \<in> SUBSEQ C \<and> y \<preceq> x \<Longrightarrow> y \<in> SUBSEQ C"
 unfolding SUBSEQ_def
 apply(auto)
+apply(rule_tac x="xa" in bexI)
+apply(rule substring_trans)
+apply(auto)
+done
 
+lemma "SUBSEQ C \<subseteq> UNIV"
+unfolding SUBSEQ_def
+apply(auto)
+done
+
+
+
+ML {*
+@{term "UNIV - (C::string set)"}
+*}
+
+lemma
+  assumes "finite S"
+  shows "finite (UNIV - {y. \<forall>z \<in> S. \<not>(z \<preceq> y)})"
+oops
+ 
+
+
+lemma a: "\<forall>x \<in> SUBSEQ C. \<exists>y \<in> C. x \<preceq> y"
+unfolding SUBSEQ_def 
+apply(auto)
+done
+
+lemma b:
+  shows "\<exists>S \<subseteq> SUBSEQ C. S \<noteq>{} \<and> (y \<in> C \<longleftrightarrow> (\<forall>z \<in> S. \<not>(z \<preceq> y)))"
+sorry
+
+lemma "False"
+using b a
+apply(blast)
+done
 
 definition
  "CLOSED C \<equiv> C = SUBSEQ C"
@@ -341,6 +377,172 @@
   show "is_prefix [] f" by simp
 qed
 
+definition
+  myeq ("~~")
+where
+  "~~ \<equiv> {(x, y). x \<preceq> y \<and> y \<preceq> x}"
+
+abbreviation
+  myeq_applied ("_ ~~~ _")
+where
+  "x ~~~ y \<equiv> (x, y) \<in> ~~"
+
+
+definition
+ "minimal x Y \<equiv> (x \<in> Y \<and> (\<forall>y \<in> Y. y \<preceq> x \<longrightarrow> x \<preceq> y))"
+
+definition
+ "downclosed Y \<equiv> (\<forall>x \<in> Y. \<forall>y. y \<preceq> x \<longrightarrow> y \<in> Y)" 
+
+
+lemma g:
+  assumes "minimal x Y" "y ~~~ x" "downclosed Y"
+  shows "minimal y Y"
+using assms
+apply(simp add: minimal_def)
+apply(rule conjI)
+apply(simp add: downclosed_def)
+apply(simp add: myeq_def)
+apply(auto)[1]
+apply(rule ballI)
+apply(rule impI)
+apply(simp add: downclosed_def)
+apply(simp add: myeq_def)
+apply(erule conjE)
+apply(rotate_tac 5)
+apply(drule_tac x="ya" in bspec)
+apply(auto)[1]
+apply(drule mp)
+apply(erule conjE)
+apply(rule substring_trans)
+apply(auto)[2]
+apply(rule substring_trans)
+apply(auto)[2]
+done
+
+thm Least_le
+
+lemma
+  assumes a: "\<exists>(i::nat) j. (f i) \<preceq> (f j) \<and> i < j"
+  and "downclosed Y"
+  shows "\<exists>S. finite S \<and> (\<forall>x \<in> Y. \<exists>y \<in> S. \<not> (y \<preceq> x))"
+proof -
+  def Ymin \<equiv> "{x. minimal x Y}"
+  have "downclosed Ymin"
+  unfolding Ymin_def downclosed_def
+  apply(auto)
+  apply(simp add: minimal_def)
+  apply(rule conjI)
+  using assms(2)
+  apply(simp add: downclosed_def)
+  apply(auto)[1]
+  apply(rule ballI) 
+  apply(rule impI)
+  apply(erule conjE)
+  apply(drule_tac x="ya" in bspec)
+  apply(simp)
+  apply(drule mp)
+  apply(rule substring_trans)
+  apply(auto)[2]
+  apply(rule substring_trans)
+  apply(auto)[2]
+  done
+  def Yeq \<equiv> "Ymin // ~~"
+  def Ypick \<equiv> "(\<lambda>X. SOME x. x \<in> X) ` Yeq" 
+  have "finite Ypick" sorry
+  moreover
+  thm LeastI_ex
+  have "(\<forall>x \<in> Y. \<exists>y \<in> Ypick. (\<not> (y \<preceq> x)))"
+  apply(rule ballI)
+  apply(subgoal_tac "\<exists>y. y \<in> Ypick")
+  apply(erule exE)
+  apply(rule_tac x="y" in bexI)
+  apply(subgoal_tac "y \<in> Ymin")
+  apply(simp add: Ymin_def minimal_def)
+  apply(subgoal_tac "~~ `` {y} \<in> Yeq")
+  apply(simp add: Yeq_def quotient_def Image_def)
+  apply(erule bexE)
+  apply(simp add: Ymin_def)
+  apply(subgoal_tac "y ~~~ xa")
+  apply(drule g)
+  apply(assumption)
+  apply(rule assms(2))
+  apply(simp add: minimal_def)
+  apply(erule conjE)
+  apply(drule_tac x="x" in bspec)
+  apply(assumption)
+  
+lemma
+  assumes a: "\<exists>(i::nat) j. (f i) \<preceq> (f j) \<and> i < j"
+  and b: "downclosed Y" 
+  and c: "Y \<noteq> {}"
+  shows "\<exists>S. finite S \<and> (Y = {y. (\<forall>z \<in> S. \<not>(z \<preceq> y))})"
+proof -
+  def Ybar \<equiv> "- Y"
+  def M \<equiv> "{x \<in> Ybar. minimal x Ybar}"
+  def Cpre \<equiv> "M // ~~"
+  def C \<equiv> "(\<lambda>X. SOME x. x \<in> X) ` Cpre"
+  have "finite C" sorry
+  moreover
+  have "\<forall>x \<in> Y. \<exists>y \<in> C.  y \<preceq> x" sorry
+  then have "\<forall>x. (x \<in> Ybar) \<longleftrightarrow> (\<exists>z \<in> C. z \<preceq> x)"
+  apply(auto simp add: Ybar_def)
+    apply(rule allI)
+    apply(rule iffI)
+    prefer 2
+    apply(erule bexE)
+    apply(case_tac "x \<in> Y")
+    prefer 2
+    apply(simp add: Ybar_def)
+    apply(subgoal_tac "z \<in> Y")
+    apply(simp add: C_def)
+    apply(simp add: Cpre_def)
+    apply(simp add: M_def Ybar_def)
+    apply(simp add: quotient_def)
+    apply(simp add: myeq_def)
+    apply(simp add: image_def)
+    apply(rule_tac x="x" in exI)
+    apply(simp)
+    apply(rule conjI)
+    apply(simp add: minimal_def)
+    apply(rule ballI)
+    apply(simp)
+    apply(rule impI)
+    prefer 3
+    apply(simp add: Ybar_def)
+    apply(rule notI)
+    apply(simp add: C_def Cpre_def M_def Ybar_def quotient_def)
+
+    prefer 2
+    apply(rule someI2_ex)
+    apply(rule_tac x="x" in exI) 
+    apply(simp add: substring_refl)
+    apply(auto)[1]
+    using b
+    apply -
+    sorry
+  ultimately
+  have "\<exists>S. finite S \<and> (\<forall>y. y \<in> Y  = (\<forall>z \<in> S. \<not>(z \<preceq> y)))"
+    apply -
+    apply(rule_tac x="C" in exI)
+    apply(simp)
+    apply(rule allI)
+    apply(rule iffI) 
+    apply(drule_tac x="y" in spec)
+    apply(simp add: Ybar_def)
+    apply(simp add: Ybar_def)
+    apply(case_tac "y \<in> Y")
+    apply(simp)
+    apply(drule_tac x="y" in spec)
+    apply(simp)
+    done
+    then show ?thesis
+    by (auto)
+qed      
+
+
+thm higman_idx
+
 text {*
 Weak version: only yield sequence containing words
 that can be embedded into each other.