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