(*  Title:      HOL/Proofs/Extraction/Higman.thy

    Author:     Stefan Berghofer, TU Muenchen

    Author:     Monika Seisenberger, LMU Muenchen

*)

header {* Higman's lemma *}

theory Higman2

imports Main

begin

text {*

  Formalization by Stefan Berghofer and Monika Seisenberger,

  based on Coquand and Fridlender \cite{Coquand93}.

*}

datatype letter = A | B

inductive emb :: "letter list \<Rightarrow> letter list \<Rightarrow> bool"

where

   emb0 [Pure.intro]: "emb [] bs"

 | emb1 [Pure.intro]: "emb as bs \<Longrightarrow> emb as (b # bs)"

 | emb2 [Pure.intro]: "emb as bs \<Longrightarrow> emb (a # as) (a # bs)"

inductive L :: "letter list \<Rightarrow> letter list list \<Rightarrow> bool"

  for v :: "letter list"

where

   L0 [Pure.intro]: "emb w v \<Longrightarrow> L v (w # ws)"

 | L1 [Pure.intro]: "L v ws \<Longrightarrow> L v (w # ws)"

inductive good :: "letter list list \<Rightarrow> bool"

where

    good0 [Pure.intro]: "L w ws \<Longrightarrow> good (w # ws)"

  | good1 [Pure.intro]: "good ws \<Longrightarrow> good (w # ws)"

inductive R :: "letter \<Rightarrow> letter list list \<Rightarrow> letter list list \<Rightarrow> bool"

  for a :: letter

where

    R0 [Pure.intro]: "R a [] []"

  | R1 [Pure.intro]: "R a vs ws \<Longrightarrow> R a (w # vs) ((a # w) # ws)"

inductive T :: "letter \<Rightarrow> letter list list \<Rightarrow> letter list list \<Rightarrow> bool"

  for a :: letter

where

    T0 [Pure.intro]: "a \<noteq> b \<Longrightarrow> R b ws zs \<Longrightarrow> T a (w # zs) ((a # w) # zs)"

  | T1 [Pure.intro]: "T a ws zs \<Longrightarrow> T a (w # ws) ((a # w) # zs)"

  | T2 [Pure.intro]: "a \<noteq> b \<Longrightarrow> T a ws zs \<Longrightarrow> T a ws ((b # w) # zs)"

inductive bar :: "letter list list \<Rightarrow> bool"

where

    bar1 [Pure.intro]: "good ws \<Longrightarrow> bar ws"

  | bar2 [Pure.intro]: "(\<And>w. bar (w # ws)) \<Longrightarrow> bar ws"

theorem prop1: "bar ([] # ws)" by iprover

theorem lemma1: "L as ws \<Longrightarrow> L (a # as) ws"

  by (erule L.induct, iprover+)

lemma lemma2': "R a vs ws \<Longrightarrow> L as vs \<Longrightarrow> L (a # as) ws"

  apply (induct set: R)

  apply (erule L.cases)

  apply simp+

  apply (erule L.cases)

  apply simp_all

  apply (rule L0)

  apply (erule emb2)

  apply (erule L1)

  done

lemma lemma2: "R a vs ws \<Longrightarrow> good vs \<Longrightarrow> good ws"

  apply (induct set: R)

  apply iprover

  apply (erule good.cases)

  apply simp_all

  apply (rule good0)

  apply (erule lemma2')

  apply assumption

  apply (erule good1)

  done

lemma lemma3': "T a vs ws \<Longrightarrow> L as vs \<Longrightarrow> L (a # as) ws"

  apply (induct set: T)

  apply (erule L.cases)

  apply simp_all

  apply (rule L0)

  apply (erule emb2)

  apply (rule L1)

  apply (erule lemma1)

  apply (erule L.cases)

  apply simp_all

  apply iprover+

  done

lemma lemma3: "T a ws zs \<Longrightarrow> good ws \<Longrightarrow> good zs"

  apply (induct set: T)

  apply (erule good.cases)

  apply simp_all

  apply (rule good0)

  apply (erule lemma1)

  apply (erule good1)

  apply (erule good.cases)

  apply simp_all

  apply (rule good0)

  apply (erule lemma3')

  apply iprover+

  done

lemma lemma4: "R a ws zs \<Longrightarrow> ws \<noteq> [] \<Longrightarrow> T a ws zs"

  apply (induct set: R)

  apply iprover

  apply (case_tac vs)

  apply (erule R.cases)

  apply simp

  apply (case_tac a)

  apply (rule_tac b=B in T0)

  apply simp

  apply (rule R0)

  apply (rule_tac b=A in T0)

  apply simp

  apply (rule R0)

  apply simp

  apply (rule T1)

  apply simp

  done

lemma letter_neq: "(a::letter) \<noteq> b \<Longrightarrow> c \<noteq> a \<Longrightarrow> c = b"

  apply (case_tac a)

  apply (case_tac b)

  apply (case_tac c, simp, simp)

  apply (case_tac c, simp, simp)

  apply (case_tac b)

  apply (case_tac c, simp, simp)

  apply (case_tac c, simp, simp)

  done

lemma letter_eq_dec: "(a::letter) = b \<or> a \<noteq> b"

  apply (case_tac a)

  apply (case_tac b)

  apply simp

  apply simp

  apply (case_tac b)

  apply simp

  apply simp

  done

theorem prop2:

  assumes ab: "a \<noteq> b" and bar: "bar xs"

  shows "\<And>ys zs. bar ys \<Longrightarrow> T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs" using bar

proof induct

  fix xs zs assume "T a xs zs" and "good xs"

  hence "good zs" by (rule lemma3)

  then show "bar zs" by (rule bar1)

next

  fix xs ys

  assume I: "\<And>w ys zs. bar ys \<Longrightarrow> T a (w # xs) zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs"

  assume "bar ys"

  thus "\<And>zs. T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs"

  proof induct

    fix ys zs assume "T b ys zs" and "good ys"

    then have "good zs" by (rule lemma3)

    then show "bar zs" by (rule bar1)

  next

    fix ys zs assume I': "\<And>w zs. T a xs zs \<Longrightarrow> T b (w # ys) zs \<Longrightarrow> bar zs"

    and ys: "\<And>w. bar (w # ys)" and Ta: "T a xs zs" and Tb: "T b ys zs"

    show "bar zs"

    proof (rule bar2)

      fix w

      show "bar (w # zs)"

      proof (cases w)

        case Nil

        thus ?thesis by simp (rule prop1)

      next

        case (Cons c cs)

        from letter_eq_dec show ?thesis

        proof

          assume ca: "c = a"

          from ab have "bar ((a # cs) # zs)" by (iprover intro: I ys Ta Tb)

          thus ?thesis by (simp add: Cons ca)

        next

          assume "c \<noteq> a"

          with ab have cb: "c = b" by (rule letter_neq)

          from ab have "bar ((b # cs) # zs)" by (iprover intro: I' Ta Tb)

          thus ?thesis by (simp add: Cons cb)

        qed

      qed

    qed

  qed

qed

theorem prop3:

  assumes bar: "bar xs"

  shows "\<And>zs. xs \<noteq> [] \<Longrightarrow> R a xs zs \<Longrightarrow> bar zs" using bar

proof induct

  fix xs zs

  assume "R a xs zs" and "good xs"

  then have "good zs" by (rule lemma2)

  then show "bar zs" by (rule bar1)

next

  fix xs zs

  assume I: "\<And>w zs. w # xs \<noteq> [] \<Longrightarrow> R a (w # xs) zs \<Longrightarrow> bar zs"

  and xsb: "\<And>w. bar (w # xs)" and xsn: "xs \<noteq> []" and R: "R a xs zs"

  show "bar zs"

  proof (rule bar2)

    fix w

    show "bar (w # zs)"

    proof (induct w)

      case Nil

      show ?case by (rule prop1)

    next

      case (Cons c cs)

      from letter_eq_dec show ?case

      proof

        assume "c = a"

        thus ?thesis by (iprover intro: I [simplified] R)

      next

        from R xsn have T: "T a xs zs" by (rule lemma4)

        assume "c \<noteq> a"

        thus ?thesis by (iprover intro: prop2 Cons xsb xsn R T)

      qed

    qed

  qed

qed

theorem higman: "bar []"

proof (rule bar2)

  fix w

  show "bar [w]"

  proof (induct w)

    show "bar [[]]" by (rule prop1)

  next

    fix c cs assume "bar [cs]"

    thus "bar [c # cs]" by (rule prop3) (simp, iprover)

  qed

qed

notation

  emb ("_ \<preceq> _")

lemma substring_refl:

  "x \<preceq> x"

apply(induct x)

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}"

lemma

 "SUBSEQ (SUBSEQ C) = SUBSEQ C"

unfolding SUBSEQ_def

apply(auto)

apply(erule emb.induct)

apply(rule_tac x="xb" in bexI)

apply(rule emb.intros)

apply(simp)

apply(erule bexE)

apply(rule_tac x="y" in bexI)

apply(auto)[2]

apply(erule bexE)

sorry

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"

primrec

  is_prefix :: "'a list \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool"

where

    "is_prefix [] f = True"

  | "is_prefix (x # xs) f = (x = f (length xs) \<and> is_prefix xs f)"

theorem L_idx:

  assumes L: "L w ws"

  shows "is_prefix ws f \<Longrightarrow> \<exists>i. emb (f i) w \<and> i < length ws" using L

proof induct

  case (L0 v ws)

  hence "emb (f (length ws)) w" by simp

  moreover have "length ws < length (v # ws)" by simp

  ultimately show ?case by iprover

next

  case (L1 ws v)

  then obtain i where emb: "emb (f i) w" and "i < length ws"

    by simp iprover

  hence "i < length (v # ws)" by simp

  with emb show ?case by iprover

qed

theorem good_idx:

  assumes good: "good ws"

  shows "is_prefix ws f \<Longrightarrow> \<exists>i j. emb (f i) (f j) \<and> i < j" using good

proof induct

  case (good0 w ws)

  hence "w = f (length ws)" and "is_prefix ws f" by simp_all

  with good0 show ?case by (iprover dest: L_idx)

next

  case (good1 ws w)

  thus ?case by simp

qed

theorem bar_idx:

  assumes bar: "bar ws"

  shows "is_prefix ws f \<Longrightarrow> \<exists>i j. emb (f i) (f j) \<and> i < j" using bar

proof induct

  case (bar1 ws)

  thus ?case by (rule good_idx)

next

  case (bar2 ws)

  hence "is_prefix (f (length ws) # ws) f" by simp

  thus ?case by (rule bar2)

qed

text {*

Strong version: yields indices of words that can be embedded into each other.

*}

theorem higman_idx: "\<exists>(i::nat) j. emb (f i) (f j) \<and> i < j"

proof (rule bar_idx)

  show "bar []" by (rule higman)

  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)