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  (mn. (A ^^ m) @@ B)"
proof (induct n)
  case 0 
  show "X = (A ^^ Suc 0) @@ X  (m0. (A ^^ m) @@ B)"
    using eq by simp
next
  case (Suc n)
  have ih: "X = (A ^^ Suc n) @@ X  (mn. (A ^^ m) @@ B)" by fact
  also have " = (A ^^ Suc n) @@ (A @@ X  B)  (mn. (A ^^ m) @@ B)" using eq by simp
  also have " = (A ^^ Suc (Suc n)) @@ X  ((A ^^ Suc n) @@ B)  (mn. (A ^^ m) @@ B)"
    by (simp add: conc_Un_distrib conc_assoc[symmetric] conc_pow_comm)
  also have " = (A ^^ Suc (Suc n)) @@ X  (mSuc n. (A ^^ m) @@ B)"
    by (auto simp add: atMost_Suc)
  finally show "X = (A ^^ Suc (Suc n)) @@ X  (mSuc 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)  (mn. B @@ (A ^^ m))"
proof (induct n)
  case 0 
  show "X = X @@ (A ^^ Suc 0)  (m0. B @@ (A ^^ m))"
    using eq by simp
next
  case (Suc n)
  have ih: "X = X @@ (A ^^ Suc n)  (mn. B @@ (A ^^ m))" by fact
  also have " = (X @@ A  B) @@ (A ^^ Suc n)  (mn. B @@ (A ^^ m))" using eq by simp
  also have " = X @@ (A ^^ Suc (Suc n))  (B @@ (A ^^ Suc n))  (mn. B @@ (A ^^ m))"
    by (simp add: conc_Un_distrib conc_assoc)
  also have " = X @@ (A ^^ Suc (Suc n))  (mSuc n. B @@ (A ^^ m))"
    by (auto simp add: atMost_Suc)
  finally show "X = X @@ (A ^^ Suc (Suc n))  (mSuc 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