# Theory Regular-Sets.Regular_Set

```(*  Author: Tobias Nipkow, Alex Krauss, Christian Urban  *)

section "Regular sets"

theory Regular_Set
imports Main
begin

type_synonym 'a lang = "'a list set"

definition conc :: "'a lang ⇒ 'a lang ⇒ 'a lang" (infixr "@@" 75) where
"A @@ B = {xs@ys | xs ys. xs:A & ys:B}"

text ‹checks the code preprocessor for set comprehensions›
export_code conc checking SML

overloading lang_pow == "compow :: nat ⇒ 'a lang ⇒ 'a lang"
begin
primrec lang_pow :: "nat ⇒ 'a lang ⇒ 'a lang" where
"lang_pow 0 A = {[]}" |
"lang_pow (Suc n) A = A @@ (lang_pow n A)"
end

text ‹for code generation›

definition lang_pow :: "nat ⇒ 'a lang ⇒ 'a lang" where
lang_pow_code_def [code_abbrev]: "lang_pow = compow"

lemma [code]:
"lang_pow (Suc n) A = A @@ (lang_pow n A)"
"lang_pow 0 A = {[]}"

hide_const (open) lang_pow

definition star :: "'a lang ⇒ 'a lang" where
"star A = (⋃n. A ^^ n)"

subsection‹@{term "(@@)"}›

lemma concI[simp,intro]: "u : A ⟹ v : B ⟹ u@v : A @@ B"

lemma concE[elim]:
assumes "w ∈ A @@ B"
obtains u v where "u ∈ A" "v ∈ B" "w = u@v"
using assms by (auto simp: conc_def)

lemma conc_mono: "A ⊆ C ⟹ B ⊆ D ⟹ A @@ B ⊆ C @@ D"
by (auto simp: conc_def)

lemma conc_empty[simp]: shows "{} @@ A = {}" and "A @@ {} = {}"
by auto

lemma conc_epsilon[simp]: shows "{[]} @@ A = A" and "A @@ {[]} = A"

lemma conc_assoc: "(A @@ B) @@ C = A @@ (B @@ C)"
by (auto elim!: concE) (simp only: append_assoc[symmetric] concI)

lemma conc_Un_distrib:
shows "A @@ (B ∪ C) = A @@ B ∪ A @@ C"
and   "(A ∪ B) @@ C = A @@ C ∪ B @@ C"
by auto

lemma conc_UNION_distrib:
shows "A @@ ⋃(M ` I) = ⋃((%i. A @@ M i) ` I)"
and   "⋃(M ` I) @@ A = ⋃((%i. M i @@ A) ` I)"
by auto

lemma conc_subset_lists: "A ⊆ lists S ⟹ B ⊆ lists S ⟹ A @@ B ⊆ lists S"
by(fastforce simp: conc_def in_lists_conv_set)

lemma Nil_in_conc[simp]: "[] ∈ A @@ B ⟷ [] ∈ A ∧ [] ∈ B"
by (metis append_is_Nil_conv concE concI)

lemma concI_if_Nil1: "[] ∈ A ⟹ xs : B ⟹ xs ∈ A @@ B"
by (metis append_Nil concI)

lemma conc_Diff_if_Nil1: "[] ∈ A ⟹ A @@ B = (A - {[]}) @@ B ∪ B"
by (fastforce elim: concI_if_Nil1)

lemma concI_if_Nil2: "[] ∈ B ⟹ xs : A ⟹ xs ∈ A @@ B"
by (metis append_Nil2 concI)

lemma conc_Diff_if_Nil2: "[] ∈ B ⟹ A @@ B = A @@ (B - {[]}) ∪ A"
by (fastforce elim: concI_if_Nil2)

lemma singleton_in_conc:
"[x] : A @@ B ⟷ [x] : A ∧ [] : B ∨ [] : A ∧ [x] : B"
by (fastforce simp: Cons_eq_append_conv append_eq_Cons_conv
conc_Diff_if_Nil1 conc_Diff_if_Nil2)

subsection‹@{term "A ^^ n"}›

lemma lang_pow_add: "A ^^ (n + m) = A ^^ n @@ A ^^ m"
by (induct n) (auto simp: conc_assoc)

lemma lang_pow_empty: "{} ^^ n = (if n = 0 then {[]} else {})"
by (induct n) auto

lemma lang_pow_empty_Suc[simp]: "({}::'a lang) ^^ Suc n = {}"

lemma conc_pow_comm:
shows "A @@ (A ^^ n) = (A ^^ n) @@ A"
by (induct n) (simp_all add: conc_assoc[symmetric])

lemma length_lang_pow_ub:
"∀w ∈ A. length w ≤ k ⟹ w : A^^n ⟹ length w ≤ k*n"
by(induct n arbitrary: w) (fastforce simp: conc_def)+

lemma length_lang_pow_lb:
"∀w ∈ A. length w ≥ k ⟹ w : A^^n ⟹ length w ≥ k*n"
by(induct n arbitrary: w) (fastforce simp: conc_def)+

lemma lang_pow_subset_lists: "A ⊆ lists S ⟹ A ^^ n ⊆ lists S"
by(induct n)(auto simp: conc_subset_lists)

assumes "[] ∈ A" "s ∈ A ^^ n"
shows "s ∈ A ^^ (n + m)"
using assms
apply(induct m arbitrary: n)
done

subsection‹@{const star}›

lemma star_subset_lists: "A ⊆ lists S ⟹ star A ⊆ lists S"
unfolding star_def by(blast dest: lang_pow_subset_lists)

lemma star_if_lang_pow[simp]: "w : A ^^ n ⟹ w : star A"
by (auto simp: star_def)

lemma Nil_in_star[iff]: "[] : star A"
proof (rule star_if_lang_pow)
show "[] : A ^^ 0" by simp
qed

lemma star_if_lang[simp]: assumes "w : A" shows "w : star A"
proof (rule star_if_lang_pow)
show "w : A ^^ 1" using ‹w : A› by simp
qed

lemma append_in_starI[simp]:
assumes "u : star A" and "v : star A" shows "u@v : star A"
proof -
from ‹u : star A› obtain m where "u : A ^^ m" by (auto simp: star_def)
moreover
from ‹v : star A› obtain n where "v : A ^^ n" by (auto simp: star_def)
thus ?thesis by simp
qed

lemma conc_star_star: "star A @@ star A = star A"
by (auto simp: conc_def)

lemma conc_star_comm:
shows "A @@ star A = star A @@ A"
unfolding star_def conc_pow_comm conc_UNION_distrib
by simp

lemma star_induct[consumes 1, case_names Nil append, induct set: star]:
assumes "w : star A"
and "P []"
and step: "!!u v. u : A ⟹ v : star A ⟹ P v ⟹ P (u@v)"
shows "P w"
proof -
{ fix n have "w : A ^^ n ⟹ P w"
by (induct n arbitrary: w) (auto intro: ‹P []› step star_if_lang_pow) }
with ‹w : star A› show "P w" by (auto simp: star_def)
qed

lemma star_empty[simp]: "star {} = {[]}"
by (auto elim: star_induct)

lemma star_epsilon[simp]: "star {[]} = {[]}"
by (auto elim: star_induct)

lemma star_idemp[simp]: "star (star A) = star A"
by (auto elim: star_induct)

lemma star_unfold_left: "star A = A @@ star A ∪ {[]}" (is "?L = ?R")
proof
show "?L ⊆ ?R" by (rule, erule star_induct) auto
qed auto

lemma concat_in_star: "set ws ⊆ A ⟹ concat ws : star A"
by (induct ws) simp_all

lemma in_star_iff_concat:
"w ∈ star A = (∃ws. set ws ⊆ A ∧ w = concat ws)"
(is "_ = (∃ws. ?R w ws)")
proof
assume "w : star A" thus "∃ws. ?R w ws"
proof induct
case Nil have "?R [] []" by simp
thus ?case ..
next
case (append u v)
then obtain ws where "set ws ⊆ A ∧ v = concat ws" by blast
with append have "?R (u@v) (u#ws)" by auto
thus ?case ..
qed
next
assume "∃us. ?R w us" thus "w : star A"
by (auto simp: concat_in_star)
qed

lemma star_conv_concat: "star A = {concat ws|ws. set ws ⊆ A}"
by (fastforce simp: in_star_iff_concat)

lemma star_insert_eps[simp]: "star (insert [] A) = star(A)"
proof-
{ fix us
have "set us ⊆ insert [] A ⟹ ∃vs. concat us = concat vs ∧ set vs ⊆ A"
(is "?P ⟹ ∃vs. ?Q vs")
proof
let ?vs = "filter (%u. u ≠ []) us"
show "?P ⟹ ?Q ?vs" by (induct us) auto
qed
} thus ?thesis by (auto simp: star_conv_concat)
qed

lemma star_unfold_left_Nil: "star A = (A - {[]}) @@ (star A) ∪ {[]}"
by (metis insert_Diff_single star_insert_eps star_unfold_left)

lemma star_Diff_Nil_fold: "(A - {[]}) @@ star A = star A - {[]}"
proof -
have "[] ∉ (A - {[]}) @@ star A" by simp
thus ?thesis using star_unfold_left_Nil by blast
qed

lemma star_decom:
assumes a: "x ∈ star A" "x ≠ []"
shows "∃a b. x = a @ b ∧ a ≠ [] ∧ a ∈ A ∧ b ∈ star A"
using a by (induct rule: star_induct) (blast)+

lemma star_pow:
assumes "s ∈ star A"
shows "∃n. s ∈ A ^^ n"
using assms
apply(induct)
apply(rule_tac x="0" in exI)
apply(auto)
apply(rule_tac x="Suc n" in exI)
apply(auto)
done

subsection ‹Left-Quotients of languages›

definition Deriv :: "'a ⇒ 'a lang ⇒ 'a lang"
where "Deriv x A = { xs. x#xs ∈ A }"

definition Derivs :: "'a list ⇒ 'a lang ⇒ 'a lang"
where "Derivs xs A = { ys. xs @ ys ∈ A }"

abbreviation
Derivss :: "'a list ⇒ 'a lang set ⇒ 'a lang"
where
"Derivss s As ≡ ⋃ (Derivs s ` As)"

lemma Deriv_empty[simp]:   "Deriv a {} = {}"
and Deriv_epsilon[simp]: "Deriv a {[]} = {}"
and Deriv_char[simp]:    "Deriv a {[b]} = (if a = b then {[]} else {})"
and Deriv_union[simp]:   "Deriv a (A ∪ B) = Deriv a A ∪ Deriv a B"
and Deriv_inter[simp]:   "Deriv a (A ∩ B) = Deriv a A ∩ Deriv a B"
and Deriv_compl[simp]:   "Deriv a (-A) = - Deriv a A"
and Deriv_Union[simp]:   "Deriv a (Union M) = Union(Deriv a ` M)"
and Deriv_UN[simp]:      "Deriv a (UN x:I. S x) = (UN x:I. Deriv a (S x))"
by (auto simp: Deriv_def)

lemma Der_conc [simp]:
shows "Deriv c (A @@ B) = (Deriv c A) @@ B ∪ (if [] ∈ A then Deriv c B else {})"
unfolding Deriv_def conc_def

lemma Deriv_star [simp]:
shows "Deriv c (star A) = (Deriv c A) @@ star A"
proof -
have "Deriv c (star A) = Deriv c ({[]} ∪ A @@ star A)"
by (metis star_unfold_left sup.commute)
also have "... = Deriv c (A @@ star A)"
unfolding Deriv_union by (simp)
also have "... = (Deriv c A) @@ (star A) ∪ (if [] ∈ A then Deriv c (star A) else {})"
by simp
also have "... =  (Deriv c A) @@ star A"
unfolding conc_def Deriv_def
using star_decom by (force simp add: Cons_eq_append_conv)
finally show "Deriv c (star A) = (Deriv c A) @@ star A" .
qed

lemma Deriv_diff[simp]:
shows "Deriv c (A - B) = Deriv c A - Deriv c B"

lemma Deriv_lists[simp]: "c : S ⟹ Deriv c (lists S) = lists S"

lemma Derivs_simps [simp]:
shows "Derivs [] A = A"
and   "Derivs (c # s) A = Derivs s (Deriv c A)"
and   "Derivs (s1 @ s2) A = Derivs s2 (Derivs s1 A)"
unfolding Derivs_def Deriv_def by auto

lemma in_fold_Deriv: "v ∈ fold Deriv w L ⟷ w @ v ∈ L"
by (induct w arbitrary: L) (simp_all add: Deriv_def)

lemma Derivs_alt_def [code]: "Derivs w L = fold Deriv w L"
by (induct w arbitrary: L) simp_all

lemma Deriv_code [code]:
"Deriv x A = tl ` Set.filter (λxs. case xs of x' # _ ⇒ x = x' | _ ⇒ False) A"
by (auto simp: Deriv_def Set.filter_def image_iff tl_def split: list.splits)

subsection ‹Shuffle product›

definition Shuffle (infixr "∥" 80) where
"Shuffle A B = ⋃{shuffles xs ys | xs ys. xs ∈ A ∧ ys ∈ B}"

lemma Deriv_Shuffle[simp]:
"Deriv a (A ∥ B) = Deriv a A ∥ B ∪ A ∥ Deriv a B"
unfolding Shuffle_def Deriv_def by (fastforce simp: Cons_in_shuffles_iff neq_Nil_conv)

lemma shuffle_subset_lists:
assumes "A ⊆ lists S" "B ⊆ lists S"
shows "A ∥ B ⊆ lists S"
unfolding Shuffle_def proof safe
fix x and zs xs ys :: "'a list"
assume zs: "zs ∈ shuffles xs ys" "x ∈ set zs" and "xs ∈ A" "ys ∈ B"
with assms have "xs ∈ lists S" "ys ∈ lists S" by auto
with zs show "x ∈ S" by (induct xs ys arbitrary: zs rule: shuffles.induct) auto
qed

lemma Nil_in_Shuffle[simp]: "[] ∈ A ∥ B ⟷ [] ∈ A ∧ [] ∈ B"
unfolding Shuffle_def by force

lemma shuffle_Un_distrib:
shows "A ∥ (B ∪ C) = A ∥ B ∪ A ∥ C"
and   "A ∥ (B ∪ C) = A ∥ B ∪ A ∥ C"
unfolding Shuffle_def by fast+

lemma shuffle_UNION_distrib:
shows "A ∥ ⋃(M ` I) = ⋃((%i. A ∥ M i) ` I)"
and   "⋃(M ` I) ∥ A = ⋃((%i. M i ∥ A) ` I)"
unfolding Shuffle_def by fast+

lemma Shuffle_empty[simp]:
"A ∥ {} = {}"
"{} ∥ B = {}"
unfolding Shuffle_def by auto

lemma Shuffle_eps[simp]:
"A ∥ {[]} = A"
"{[]} ∥ B = B"
unfolding Shuffle_def by auto

subsection ‹Arden's Lemma›

lemma arden_helper:
assumes eq: "X = A @@ X ∪ B"
shows "X = (A ^^ Suc n) @@ X ∪ (⋃m≤n. (A ^^ m) @@ B)"
proof (induct n)
case 0
show "X = (A ^^ Suc 0) @@ X ∪ (⋃m≤0. (A ^^ m) @@ B)"
using eq by simp
next
case (Suc n)
have ih: "X = (A ^^ Suc n) @@ X ∪ (⋃m≤n. (A ^^ m) @@ B)" by fact
also have "… = (A ^^ Suc n) @@ (A @@ X ∪ B) ∪ (⋃m≤n. (A ^^ m) @@ B)" using eq by simp
also have "… = (A ^^ Suc (Suc n)) @@ X ∪ ((A ^^ Suc n) @@ B) ∪ (⋃m≤n. (A ^^ m) @@ B)"
by (simp add: conc_Un_distrib conc_assoc[symmetric] conc_pow_comm)
also have "… = (A ^^ Suc (Suc n)) @@ X ∪ (⋃m≤Suc n. (A ^^ m) @@ B)"
finally show "X = (A ^^ Suc (Suc n)) @@ X ∪ (⋃m≤Suc n. (A ^^ m) @@ B)" .
qed

lemma Arden:
assumes "[] ∉ A"
shows "X = A @@ X ∪ B ⟷ X = star A @@ B"
proof
assume eq: "X = A @@ X ∪ B"
{ fix w assume "w : X"
let ?n = "size w"
from ‹[] ∉ A› have "∀u ∈ A. length u ≥ 1"
by (metis Suc_eq_plus1 add_leD2 le_0_eq length_0_conv not_less_eq_eq)
hence "∀u ∈ A^^(?n+1). length u ≥ ?n+1"
by (metis length_lang_pow_lb nat_mult_1)
hence "∀u ∈ A^^(?n+1)@@X. length u ≥ ?n+1"
by(auto simp only: conc_def length_append)
hence "w ∉ A^^(?n+1)@@X" by auto
hence "w : star A @@ B" using ‹w : X› using arden_helper[OF eq, where n="?n"]
by (auto simp add: star_def conc_UNION_distrib)
} moreover
{ fix w assume "w : star A @@ B"
hence "∃n. w ∈ A^^n @@ B" by(auto simp: conc_def star_def)
hence "w : X" using arden_helper[OF eq] by blast
} ultimately show "X = star A @@ B" by blast
next
assume eq: "X = star A @@ B"
have "star A = A @@ star A ∪ {[]}"
by (rule star_unfold_left)
then have "star A @@ B = (A @@ star A ∪ {[]}) @@ B"
by metis
also have "… = (A @@ star A) @@ B ∪ B"
unfolding conc_Un_distrib by simp
also have "… = A @@ (star A @@ B) ∪ B"
by (simp only: conc_assoc)
finally show "X = A @@ X ∪ B"
using eq by blast
qed

lemma reversed_arden_helper:
assumes eq: "X = X @@ A ∪ B"
shows "X = X @@ (A ^^ Suc n) ∪ (⋃m≤n. B @@ (A ^^ m))"
proof (induct n)
case 0
show "X = X @@ (A ^^ Suc 0) ∪ (⋃m≤0. B @@ (A ^^ m))"
using eq by simp
next
case (Suc n)
have ih: "X = X @@ (A ^^ Suc n) ∪ (⋃m≤n. B @@ (A ^^ m))" by fact
also have "… = (X @@ A ∪ B) @@ (A ^^ Suc n) ∪ (⋃m≤n. B @@ (A ^^ m))" using eq by simp
also have "… = X @@ (A ^^ Suc (Suc n)) ∪ (B @@ (A ^^ Suc n)) ∪ (⋃m≤n. B @@ (A ^^ m))"
also have "… = X @@ (A ^^ Suc (Suc n)) ∪ (⋃m≤Suc n. B @@ (A ^^ m))"
finally show "X = X @@ (A ^^ Suc (Suc n)) ∪ (⋃m≤Suc n. B @@ (A ^^ m))" .
qed

theorem reversed_Arden:
assumes nemp: "[] ∉ A"
shows "X = X @@ A ∪ B ⟷ X = B @@ star A"
proof
assume eq: "X = X @@ A ∪ B"
{ fix w assume "w : X"
let ?n = "size w"
from ‹[] ∉ A› have "∀u ∈ A. length u ≥ 1"
by (metis Suc_eq_plus1 add_leD2 le_0_eq length_0_conv not_less_eq_eq)
hence "∀u ∈ A^^(?n+1). length u ≥ ?n+1"
by (metis length_lang_pow_lb nat_mult_1)
hence "∀u ∈ X @@ A^^(?n+1). length u ≥ ?n+1"
by(auto simp only: conc_def length_append)
hence "w ∉ X @@ A^^(?n+1)" by auto
hence "w : B @@ star A" using ‹w : X› using reversed_arden_helper[OF eq, where n="?n"]
by (auto simp add: star_def conc_UNION_distrib)
} moreover
{ fix w assume "w : B @@ star A"
hence "∃n. w ∈ B @@ A^^n" by (auto simp: conc_def star_def)
hence "w : X" using reversed_arden_helper[OF eq] by blast
} ultimately show "X = B @@ star A" by blast
next
assume eq: "X = B @@ star A"
have "star A = {[]} ∪ star A @@ A"
unfolding conc_star_comm[symmetric]
by(metis Un_commute star_unfold_left)
then have "B @@ star A = B @@ ({[]} ∪ star A @@ A)"
by metis
also have "… = B ∪ B @@ (star A @@ A)"
unfolding conc_Un_distrib by simp
also have "… = B ∪ (B @@ star A) @@ A"
by (simp only: conc_assoc)
finally show "X = X @@ A ∪ B"
using eq by blast
qed

end
```