246 

   247 lemma substring_trans:

   248   assumes a: "x1 \<preceq> x2" and b: "x2 \<preceq> x3"

   249   shows "x1 \<preceq> x3"

   250 using a b

   251 apply(induct arbitrary: x3)

   252 apply(auto intro: emb.intros)

   253 apply(rotate_tac 2)

   254 apply(erule emb.cases)

   255 apply(simp_all)

   256 sorry 

   379 

   380 definition

   381   myeq ("~~")

   382 where

   383   "~~ \<equiv> {(x, y). x \<preceq> y \<and> y \<preceq> x}"

   384 

   385 abbreviation

   386   myeq_applied ("_ ~~~ _")

   387 where

   388   "x ~~~ y \<equiv> (x, y) \<in> ~~"

   389 

   390 

   391 definition

   392  "minimal x Y \<equiv> (x \<in> Y \<and> (\<forall>y \<in> Y. y \<preceq> x \<longrightarrow> x \<preceq> y))"

   393 

   394 definition

   395  "downclosed Y \<equiv> (\<forall>x \<in> Y. \<forall>y. y \<preceq> x \<longrightarrow> y \<in> Y)" 

   396 

   397 

   398 lemma g:

   399   assumes "minimal x Y" "y ~~~ x" "downclosed Y"

   400   shows "minimal y Y"

   401 using assms

   402 apply(simp add: minimal_def)

   403 apply(rule conjI)

   404 apply(simp add: downclosed_def)

   405 apply(simp add: myeq_def)

   406 apply(auto)[1]

   407 apply(rule ballI)

   408 apply(rule impI)

   409 apply(simp add: downclosed_def)

   410 apply(simp add: myeq_def)

   411 apply(erule conjE)

   412 apply(rotate_tac 5)

   413 apply(drule_tac x="ya" in bspec)

   414 apply(auto)[1]

   415 apply(drule mp)

   416 apply(erule conjE)

   417 apply(rule substring_trans)

   418 apply(auto)[2]

   419 apply(rule substring_trans)

   420 apply(auto)[2]

   421 done

   422 

   423 thm Least_le

   424 

   425 lemma

   426   assumes a: "\<exists>(i::nat) j. (f i) \<preceq> (f j) \<and> i < j"

   427   and "downclosed Y"

   428   shows "\<exists>S. finite S \<and> (\<forall>x \<in> Y. \<exists>y \<in> S. \<not> (y \<preceq> x))"

   429 proof -

   430   def Ymin \<equiv> "{x. minimal x Y}"

   431   have "downclosed Ymin"

   432   unfolding Ymin_def downclosed_def

   433   apply(auto)

   434   apply(simp add: minimal_def)

   435   apply(rule conjI)

   436   using assms(2)

   437   apply(simp add: downclosed_def)

   438   apply(auto)[1]

   439   apply(rule ballI) 

   440   apply(rule impI)

   441   apply(erule conjE)

   442   apply(drule_tac x="ya" in bspec)

   443   apply(simp)

   444   apply(drule mp)

   445   apply(rule substring_trans)

   446   apply(auto)[2]

   447   apply(rule substring_trans)

   448   apply(auto)[2]

   449   done

   450   def Yeq \<equiv> "Ymin // ~~"

   451   def Ypick \<equiv> "(\<lambda>X. SOME x. x \<in> X) ` Yeq" 

   452   have "finite Ypick" sorry

   453   moreover

   454   thm LeastI_ex

   455   have "(\<forall>x \<in> Y. \<exists>y \<in> Ypick. (\<not> (y \<preceq> x)))"

   456   apply(rule ballI)

   457   apply(subgoal_tac "\<exists>y. y \<in> Ypick")

   458   apply(erule exE)

   459   apply(rule_tac x="y" in bexI)

   460   apply(subgoal_tac "y \<in> Ymin")

   461   apply(simp add: Ymin_def minimal_def)

   462   apply(subgoal_tac "~~ `` {y} \<in> Yeq")

   463   apply(simp add: Yeq_def quotient_def Image_def)

   464   apply(erule bexE)

   465   apply(simp add: Ymin_def)

   466   apply(subgoal_tac "y ~~~ xa")

   467   apply(drule g)

   468   apply(assumption)

   469   apply(rule assms(2))

   470   apply(simp add: minimal_def)

   471   apply(erule conjE)

   472   apply(drule_tac x="x" in bspec)

   473   apply(assumption)

   474   

   475 lemma

   476   assumes a: "\<exists>(i::nat) j. (f i) \<preceq> (f j) \<and> i < j"

   477   and b: "downclosed Y" 

   478   and c: "Y \<noteq> {}"

   479   shows "\<exists>S. finite S \<and> (Y = {y. (\<forall>z \<in> S. \<not>(z \<preceq> y))})"

   480 proof -

   481   def Ybar \<equiv> "- Y"

   482   def M \<equiv> "{x \<in> Ybar. minimal x Ybar}"

   483   def Cpre \<equiv> "M // ~~"

   484   def C \<equiv> "(\<lambda>X. SOME x. x \<in> X) ` Cpre"

   485   have "finite C" sorry

   486   moreover

   487   have "\<forall>x \<in> Y. \<exists>y \<in> C.  y \<preceq> x" sorry

   488   then have "\<forall>x. (x \<in> Ybar) \<longleftrightarrow> (\<exists>z \<in> C. z \<preceq> x)"

   489   apply(auto simp add: Ybar_def)

   490     apply(rule allI)

   491     apply(rule iffI)

   492     prefer 2

   493     apply(erule bexE)

   494     apply(case_tac "x \<in> Y")

   495     prefer 2

   496     apply(simp add: Ybar_def)

   497     apply(subgoal_tac "z \<in> Y")

   498     apply(simp add: C_def)

   499     apply(simp add: Cpre_def)

   500     apply(simp add: M_def Ybar_def)

   501     apply(simp add: quotient_def)

   502     apply(simp add: myeq_def)

   503     apply(simp add: image_def)

   504     apply(rule_tac x="x" in exI)

   505     apply(simp)

   506     apply(rule conjI)

   507     apply(simp add: minimal_def)

   508     apply(rule ballI)

   509     apply(simp)

   510     apply(rule impI)

   511     prefer 3

   512     apply(simp add: Ybar_def)

   513     apply(rule notI)

   514     apply(simp add: C_def Cpre_def M_def Ybar_def quotient_def)

   515 

   516     prefer 2

   517     apply(rule someI2_ex)

   518     apply(rule_tac x="x" in exI) 

   519     apply(simp add: substring_refl)

   520     apply(auto)[1]

   521     using b

   522     apply -

   523     sorry

   524   ultimately

   525   have "\<exists>S. finite S \<and> (\<forall>y. y \<in> Y  = (\<forall>z \<in> S. \<not>(z \<preceq> y)))"

   526     apply -

   527     apply(rule_tac x="C" in exI)

   528     apply(simp)

   529     apply(rule allI)

   530     apply(rule iffI) 

   531     apply(drule_tac x="y" in spec)

   532     apply(simp add: Ybar_def)

   533     apply(simp add: Ybar_def)

   534     apply(case_tac "y \<in> Y")

   535     apply(simp)

   536     apply(drule_tac x="y" in spec)

   537     apply(simp)

   538     done

   539     then show ?thesis

   540     by (auto)

   541 qed      

   542 

   543 

   544 thm higman_idx