imports 

  Closures

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

inductive 

  emb :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<preceq> _")

   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]:

by (induct x) (auto intro: emb.intros)

lemma emb_right [intro]:

using a by (induct arbitrary: y') (auto)

lemma emb_left [intro]:

using a by (induct y') (auto)

lemma emb_appendI [intro]:

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)

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)

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

 "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 {[a]} = UNIV \<cdot> {[a]} \<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(simp only: SUPSEQ_union) 

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

unfolding Allreg_def by auto

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

  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:

  shows "lang (UP r) = SUPSEQ (lang r)"

by (induct r) (simp_all)

lemma regular_SUPSEQ: 

  fixes A::"'a::finite lang"

  from assms obtain r::"'a::finite 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

lemma SUPSEQ_subset:

  shows "A \<subseteq> SUPSEQ A"

unfolding SUPSEQ_def by auto

lemma w3:

  assumes eq: "T = - (SUBSEQ A)"

  shows "T = SUPSEQ T"

apply(rule)

apply(rule SUPSEQ_subset)

apply(rule ccontr)

apply(auto)

apply(rule ccontr)

apply(subgoal_tac "x \<in> SUBSEQ A")

prefer 2

apply(subst (asm) (2) eq)

apply(simp)

apply(simp add: SUPSEQ_def)

apply(erule bexE)

apply(subgoal_tac "y \<in> SUBSEQ A")

prefer 2

apply(simp add: SUBSEQ_def)

apply(erule bexE)

apply(rule_tac x="xa" in bexI)

apply(rule emb_trans)

apply(assumption)

apply(assumption)

apply(assumption)

apply(subst (asm) (2) eq)

apply(simp)

done

lemma w4:

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

by (rule w3) (simp)

definition

  "minimal_in x L \<equiv> \<forall>y \<in> L. 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)"

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

lemma minimal:

  assumes "minimal_in x A" "minimal_in y A"

  and "x \<noteq> y" "x \<in> A" "y \<in> A"

  shows "\<not>(x \<preceq> y) \<and> \<not>(y \<preceq> x)"

using assms unfolding minimal_in_def 

by auto

lemma main_lemma:

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

proof -

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

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

  moreover

  have "finite M"

    apply(rule higman)

    unfolding M_def minimal_in_def

    by auto

  moreover

  have "SUPSEQ A \<subseteq> SUPSEQ M"

    apply(rule)

    apply(simp only: SUPSEQ_def)

    apply(auto)[1]

    using emb_wf

    apply(erule_tac Q="{y' \<in> A. y' \<preceq> x}" and x="y" in wfE_min)

    apply(simp)

    apply(simp)

    apply(rule_tac x="z" in bexI)

    apply(simp)

    apply(simp add: M_def)

    apply(simp add: minimal_in2)

    apply(rule ballI)

    apply(rule impI)

    apply(drule_tac x="ya" in meta_spec)

    apply(simp)

    apply(case_tac "ya = z")

    apply(auto)[1]

    apply(simp)

    by (metis emb_trans)

  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::"'a::finite 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::"'a::finite lang"

  shows "regular (SUBSEQ A)"

proof -

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

  then have "regular (- SUBSEQ A)" 

    apply(subst w4) 

    apply(assumption) 

    done

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

  then show "regular (SUBSEQ A)" by simp

qed