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

from b have "x ∈ SUBSEQ A" by simp
then obtain x' where f: "x' ∈ A" and e: "subseq x x'"

from d e have "subseq y x'"
by (rule subseq_order.order_trans)
then have "y ∈ SUBSEQ A" using f
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"
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
```