theory Closure2
imports 
  Closures
  (* "~~/src/HOL/Proofs/Extraction/Higman" *)
begin

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 intro: emb.intros)

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 {[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(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:
  shows "lang (UP r) = SUPSEQ (lang r)"
by (induct r) (simp_all)

lemma regular_SUPSEQ: 
  fixes A::"'a::finite lang"
  assumes "regular A"
  shows "regular (SUPSEQ A)"
proof -
  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
qed

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



end