Theory Closures2

theory Closures2
imports 
  Closures
  Well_Quasi_Orders.Well_Quasi_Orders
begin

section ‹Closure under ‹SUBSEQ› and ‹SUPSEQ››

text ‹Properties about the embedding relation›

lemma subseq_strict_length:
  assumes a: "subseq x y" "x ≠ y" 
  shows "length x < length y"
using a
by (induct) (auto simp add: less_Suc_eq)

lemma subseq_wf:
  shows "wf {(x, y). subseq x y ∧ x ≠ y}"
proof -
  have "wf (measure length)" by simp
  moreover
  have "{(x, y). subseq x y ∧ x ≠ y} ⊆ measure length"
    unfolding measure_def by (auto simp add: subseq_strict_length)
  ultimately 
  show "wf {(x, y). subseq x y ∧ x ≠ y}" by (rule wf_subset)
qed

lemma subseq_good:
  shows "good subseq (f :: nat ⇒ ('a::finite) list)"
using wqo_on_imp_good[where f="f", OF wqo_on_lists_over_finite_sets]
by simp

lemma subseq_Higman_antichains:
  assumes a: "∀(x::('a::finite) list) ∈ A. ∀y ∈ A. x ≠ y ⟶ ¬(subseq x y) ∧ ¬(subseq y x)"
  shows "finite A"
proof (rule ccontr)
  assume "infinite A"
  then obtain f::"nat ⇒ 'a::finite list" where b: "inj f" and c: "range f ⊆ A"
    by (auto simp add: infinite_iff_countable_subset)
  from subseq_good[where f="f"] 
  obtain i j where d: "i < j" and e: "subseq (f i) (f j) ∨ f i = f j" 
    unfolding good_def
    by auto
  have "f i ≠ f j" using b d by (auto simp add: inj_on_def)
  moreover
  have "f i ∈ A" using c by auto
  moreover
  have "f j ∈ A" using c by auto
  ultimately have "¬(subseq (f i) (f j))" using a by simp
  with e show "False" by auto
qed

subsection ‹Sub- and Supersequences›

definition
 "SUBSEQ A ≡ {x::('a::finite) list. ∃y ∈ A. subseq x y}"

definition
 "SUPSEQ A ≡ {x::('a::finite) list. ∃y ∈ A. subseq y x}"

lemma SUPSEQ_simps [simp]:
  shows "SUPSEQ {} = {}"
  and   "SUPSEQ {[]} = UNIV"
unfolding SUPSEQ_def by auto

lemma SUPSEQ_atom [simp]:
  shows "SUPSEQ {[c]} = UNIV ⋅ {[c]} ⋅ UNIV"
unfolding SUPSEQ_def conc_def
by (auto dest: list_emb_ConsD)

lemma SUPSEQ_union [simp]:
  shows "SUPSEQ (A ∪ B) = SUPSEQ A ∪ SUPSEQ B"
unfolding SUPSEQ_def by auto

lemma SUPSEQ_conc [simp]:
  shows "SUPSEQ (A ⋅ B) = SUPSEQ A ⋅ SUPSEQ B"
unfolding SUPSEQ_def conc_def
apply(auto)
apply(drule list_emb_appendD)
apply(auto)
by (metis list_emb_append_mono)

lemma SUPSEQ_star [simp]:
  shows "SUPSEQ (A⋆) = UNIV"
apply(subst star_unfold_left)
apply(simp only: SUPSEQ_union) 
apply(simp)
done

subsection ‹Regular expression that recognises every character›

definition
  Allreg :: "'a::finite rexp"
where
  "Allreg ≡ ⨄(Atom ` UNIV)"

lemma Allreg_lang [simp]:
  shows "lang Allreg = (⋃a. {[a]})"
unfolding Allreg_def by auto

lemma [simp]:
  shows "(⋃a. {[a]})⋆ = UNIV"
apply(auto)
apply(induct_tac x)
apply(auto)
apply(subgoal_tac "[a] @ list ∈ (⋃a. {[a]})⋆")
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 ⇒ '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::"'a::finite rexp"
  shows "lang (UP r) = SUPSEQ (lang r)"
by (induct r) (simp_all)

lemma SUPSEQ_regular: 
  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:
  fixes A::"'a::finite list set"
  shows "A ⊆ SUPSEQ A"
unfolding SUPSEQ_def by auto

lemma SUBSEQ_complement:
  shows "- (SUBSEQ A) = SUPSEQ (- (SUBSEQ A))"
proof -
  have "- (SUBSEQ A) ⊆ SUPSEQ (- (SUBSEQ A))"
    by (rule SUPSEQ_subset)
  moreover 
  have "SUPSEQ (- (SUBSEQ A)) ⊆ - (SUBSEQ A)"
  proof (rule ccontr)
    assume "¬ (SUPSEQ (- (SUBSEQ A)) ⊆ - (SUBSEQ A))"
    then obtain x where 
       a: "x ∈ SUPSEQ (- (SUBSEQ A))" and 
       b: "x ∉ - (SUBSEQ A)" by auto

    from a obtain y where c: "y ∈ - (SUBSEQ A)" and d: "subseq y x"
      by (auto simp add: SUPSEQ_def)

    from b have "x ∈ SUBSEQ A" by simp
    then obtain x' where f: "x' ∈ A" and e: "subseq x x'"
      by (auto simp add: SUBSEQ_def)
    
    from d e have "subseq y x'"
      by (rule subseq_order.order_trans)
    then have "y ∈ 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

definition
  minimal :: "'a::finite list ⇒ 'a lang ⇒ bool"
where
  "minimal x A ≡ (∀y ∈ A. subseq y x ⟶ subseq x y)"

lemma main_lemma:
  shows "∃M. finite M ∧ SUPSEQ A = SUPSEQ M"
proof -
  define M where "M = {x ∈ A. minimal x A}"
  have "finite M"
    unfolding M_def minimal_def
    by (rule subseq_Higman_antichains) (auto simp add: subseq_order.antisym)
  moreover
  have "SUPSEQ A ⊆ SUPSEQ M"
  proof
    fix x
    assume "x ∈ SUPSEQ A"
    then obtain y where "y ∈ A" and "subseq y x" by (auto simp add: SUPSEQ_def)
    then have a: "y ∈ {y' ∈ A. subseq y' x}" by simp
    obtain z where b: "z ∈ A" "subseq z x" and c: "∀y. subseq y z ∧ y ≠ z ⟶ y ∉ {y' ∈ A. subseq y' x}"
      using wfE_min[OF subseq_wf a] by auto
    then have "z ∈ M"
      unfolding M_def minimal_def
      by (auto intro: subseq_order.order_trans)
    with b(2) show "x ∈ SUPSEQ M"
      by (auto simp add: SUPSEQ_def)
  qed
  moreover
  have "SUPSEQ M ⊆ SUPSEQ A"
    by (auto simp add: SUPSEQ_def M_def)
  ultimately
  show "∃M. finite M ∧ SUPSEQ A = SUPSEQ M" by blast
qed

subsection ‹Closure of @{const SUBSEQ} and @{const SUPSEQ}›

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 SUPSEQ_regular)
  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)" by (subst SUBSEQ_complement) (simp)
  then have "regular (- (- (SUBSEQ A)))" by (rule closure_complement)
  then show "regular (SUBSEQ A)" by simp
qed

end