theory Closure2

imports 

  Closures

  Higman

  (* "~~/src/HOL/Proofs/Extraction/Higman" *)

begin

section {* Closure under @{text SUBSEQ} and @{text SUPSEQ} *}

(* compatibility with Higman theory by Stefan *)

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)

lemma emb_right [intro]:

  assumes a: "x \<preceq> y"

  shows "x \<preceq> y @ y'"

using a 

by (induct arbitrary: y') (auto)

lemma emb_left [intro]:

  assumes a: "x \<preceq> y"

  shows "x \<preceq> y' @ y"

using a by (induct y') (auto)

lemma emb_appendI [intro]:

  assumes a: "x \<preceq> x'"

  and     b: "y \<preceq> y'"

  shows "x @ y \<preceq> x' @ y'"

using a b by (induct) (auto)

lemma emb_cons_leftD:

  assumes "a # x \<preceq> y"

  shows "\<exists>y1 y2. y = y1 @ [a] @ y2 \<and> x \<preceq> y2"

using assms

apply(induct x\<equiv>"a # x" y\<equiv>"y" arbitrary: a x y)

apply(auto)

apply(metis append_Cons)

done

lemma emb_append_leftD:

  assumes "x1 @ x2 \<preceq> y"

  shows "\<exists>y1 y2. y = y1 @ y2 \<and> x1 \<preceq> y1 \<and> x2 \<preceq> y2"

using assms

apply(induct x1 arbitrary: x2 y)

apply(auto)

apply(drule emb_cons_leftD)

apply(auto)

apply(drule_tac x="x2" in meta_spec)

apply(drule_tac x="y2" in meta_spec)

apply(auto)

apply(rule_tac x="y1 @ (a # y1a)" in exI)

apply(rule_tac x="y2a" in exI)

apply(auto)

done

lemma emb_trans:

  assumes a: "x1 \<preceq> x2"

  and     b: "x2 \<preceq> x3"

  shows "x1 \<preceq> x3"

using a b

apply(induct arbitrary: x3)

apply(metis emb0)

apply(metis emb_cons_leftD emb_left)

apply(drule_tac emb_cons_leftD)

apply(auto)

done

lemma emb_strict_length:

  assumes a: "x \<preceq> y" "x \<noteq> y" 

  shows "length x < length y"

using a

by (induct) (auto simp add: less_Suc_eq)

lemma emb_antisym:

  assumes a: "x \<preceq> y" "y \<preceq> x" 

  shows "x = y"

using a emb_strict_length

by (metis not_less_iff_gr_or_eq)

lemma emb_wf:

  shows "wf {(x, y). x \<preceq> y \<and> x \<noteq> y}"

proof -

  have "wf (measure length)" by simp

  moreover

  have "{(x, y). x \<preceq> y \<and> x \<noteq> y} \<subseteq> measure length"

    unfolding measure_def by (auto simp add: emb_strict_length)

  ultimately 

  show "wf {(x, y). x \<preceq> y \<and> x \<noteq> y}" by (rule wf_subset)

qed

subsection {* Sub- and Supsequences *}

definition

 "SUBSEQ A \<equiv> {x. \<exists>y \<in> A. x \<preceq> y}"

definition

 "SUPSEQ A \<equiv> {x. \<exists>y \<in> A. y \<preceq> x}"

lemma SUPSEQ_simps [simp]:

  shows "SUPSEQ {} = {}"

  and   "SUPSEQ {[]} = UNIV"

unfolding SUPSEQ_def by auto

lemma SUPSEQ_atom [simp]:

  shows "SUPSEQ {[c]} = UNIV \<cdot> {[c]} \<cdot> UNIV"

unfolding SUPSEQ_def conc_def

by (auto) (metis append_Cons emb_cons_leftD)

lemma SUPSEQ_union [simp]:

  shows "SUPSEQ (A \<union> B) = SUPSEQ A \<union> SUPSEQ B"

unfolding SUPSEQ_def by auto

lemma SUPSEQ_conc [simp]:

  shows "SUPSEQ (A \<cdot> B) = SUPSEQ A \<cdot> SUPSEQ B"

unfolding SUPSEQ_def conc_def

by (auto) (metis emb_append_leftD)

lemma SUPSEQ_star [simp]:

  shows "SUPSEQ (A\<star>) = UNIV"

apply(subst star_unfold_left)

apply(simp only: SUPSEQ_union) 

apply(simp)

done

definition

  Allreg :: "'a::finite rexp"

where

  "Allreg \<equiv> \<Uplus>(Atom ` UNIV)"

lemma Allreg_lang [simp]:

  shows "lang Allreg = (\<Union>a. {[a]})"

unfolding Allreg_def by auto

lemma [simp]:

  shows "(\<Union>a. {[a]})\<star> = UNIV"

apply(auto)

apply(induct_tac x rule: list.induct)

apply(auto)

apply(subgoal_tac "[a] @ list \<in> (\<Union>a. {[a]})\<star>")

apply(simp)

apply(rule append_in_starI)

apply(auto)

done

lemma Star_Allreg_lang [simp]:

  shows "lang (Star Allreg) = UNIV"

by simp

fun 

  UP :: "'a::finite rexp \<Rightarrow> 'a rexp"

where

  "UP (Zero) = Zero"

| "UP (One) = Star Allreg"

| "UP (Atom c) = Times (Star Allreg) (Times (Atom c) (Star Allreg))"   

| "UP (Plus r1 r2) = Plus (UP r1) (UP r2)"

| "UP (Times r1 r2) = Times (UP r1) (UP r2)"

| "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::"letter lang"

  assumes "regular A"

  shows "regular (SUPSEQ A)"

proof -

  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

lemma SUPSEQ_subset:

  shows "A \<subseteq> SUPSEQ A"

unfolding SUPSEQ_def by auto

lemma SUBSEQ_complement:

  shows "- (SUBSEQ A) = SUPSEQ (- (SUBSEQ A))"

proof -

  have "- (SUBSEQ A) \<subseteq> SUPSEQ (- (SUBSEQ A))"

    by (rule SUPSEQ_subset)

  moreover 

  have "SUPSEQ (- (SUBSEQ A)) \<subseteq> - (SUBSEQ A)"

  proof (rule ccontr)

    assume "\<not> (SUPSEQ (- (SUBSEQ A)) \<subseteq> - (SUBSEQ A))"

    then obtain x where 

       a: "x \<in> SUPSEQ (- (SUBSEQ A))" and 

       b: "x \<notin> - (SUBSEQ A)" by auto

    from a obtain y where c: "y \<in> - (SUBSEQ A)" and d: "y \<preceq> x"

      by (auto simp add: SUPSEQ_def)

    from b have "x \<in> SUBSEQ A" by simp

    then obtain x' where f: "x' \<in> A" and e: "x \<preceq> x'"

      by (auto simp add: SUBSEQ_def)

    from d e have "y \<preceq> x'" by (rule emb_trans)

    then have "y \<in> SUBSEQ A" using f

      by (auto simp add: SUBSEQ_def)

    with c show "False" by simp

  qed

  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"

proof (rule ccontr)

  assume "infinite A"

  then obtain f::"nat \<Rightarrow> letter list" where b: "inj f" and c: "range f \<subseteq> A"

    by (auto simp add: infinite_iff_countable_subset)

  from higman_idx obtain i j where d: "i < j" and e: "f i \<preceq> f j" by blast

  have "f i \<noteq> f j" using b d by (auto simp add: inj_on_def)

  moreover

  moreover

  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"

where

  "minimal x A = (\<forall>y \<in> A. y \<preceq> x \<longrightarrow> x \<preceq> y)"

lemma main_lemma:

  shows "\<exists>M. M \<subseteq> A \<and> finite M \<and> SUPSEQ A = SUPSEQ M"

proof -

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

  have "M \<subseteq> A" unfolding M_def minimal_def by auto

  moreover

  have "finite M"

    unfolding M_def minimal_def

    by (rule Higman_antichains) (auto simp add: emb_antisym)

  moreover

  have "SUPSEQ A \<subseteq> SUPSEQ M"

  proof

    fix x

    assume "x \<in> SUPSEQ A"

    then obtain y where "y \<in> A" and "y \<preceq> x" by (auto simp add: SUPSEQ_def)

    then have a: "y \<in> {y' \<in> A. y' \<preceq> x}" by simp

    obtain z where b: "z \<in> A" "z \<preceq> x" and c: "\<forall>y. y \<preceq> z \<and> y \<noteq> z \<longrightarrow> y \<notin> {y' \<in> A. y' \<preceq> x}"

      using wfE_min[OF emb_wf a] by auto

    then have "z \<in> M"

      unfolding M_def minimal_def

      by (auto intro: emb_trans)

    with b show "x \<in> SUPSEQ M"

      by (auto simp add: SUPSEQ_def)

  qed

  moreover

  have "SUPSEQ M \<subseteq> SUPSEQ A"

    by (auto simp add: SUPSEQ_def M_def)

  ultimately

  show "\<exists>M. M \<subseteq> A \<and> finite M \<and> SUPSEQ A = SUPSEQ M" by blast

qed

lemma closure_SUPSEQ:

  fixes A::"letter lang" 

  shows "regular (SUPSEQ A)"

proof -

  obtain M where a: "finite M" and b: "SUPSEQ A = SUPSEQ M"

    using main_lemma by blast

  have "regular M" using a by (rule finite_regular)

  then have "regular (SUPSEQ M)" by (rule regular_SUPSEQ)

  then show "regular (SUPSEQ A)" using b by simp

qed

lemma closure_SUBSEQ:

  fixes A::"letter lang"

  shows "regular (SUBSEQ A)"

proof -

  have "regular (SUPSEQ (- SUBSEQ A))" by (rule closure_SUPSEQ)

  then have "regular (- SUBSEQ A)" by (subst SUBSEQ_complement) (simp)

  then have "regular (- (- (SUBSEQ A)))" by (rule closure_complement)

  then show "regular (SUBSEQ A)" by simp

qed

end