Theory 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 = {[]}"
  by (simp_all add: lang_pow_code_def)

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"
by (auto simp add: conc_def)

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"
by (simp_all add:conc_def)

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 = {}"
by (simp add: lang_pow_empty)

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)

lemma empty_pow_add:
  assumes "[] ∈ A" "s ∈ A ^^ n"
  shows "s ∈ A ^^ (n + m)"
  using assms
  apply(induct m arbitrary: n)
  apply(auto simp add: concI_if_Nil1)
  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)
  ultimately have "u@v : A ^^ (m+n)" by (simp add: lang_pow_add)
  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
by (auto simp add: Cons_eq_append_conv)

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"
by(auto simp add: Deriv_def)

lemma Deriv_lists[simp]: "c : S ⟹ Deriv c (lists S) = lists S"
by(auto simp add: Deriv_def)

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)"
    by (auto simp add: atMost_Suc)
  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))"
    by (simp add: conc_Un_distrib conc_assoc)
  also have "… = X @@ (A ^^ Suc (Suc n)) ∪ (⋃m≤Suc n. B @@ (A ^^ m))"
    by (auto simp add: atMost_Suc)
  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