Theory Pi_Regular_Set

(*  Author: Tobias Nipkow, Alex Krauss, Dmitriy Traytel  *)

section "Regular Sets"

(*<*)
theory Pi_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}"

lemma [code]:
  "A @@ B = (%(xs, ys). xs @ ys) ` (A × B)"
  unfolding conc_def by auto

overloading word_pow == "compow :: nat ⇒ 'a list ⇒ 'a list"
begin
  primrec word_pow :: "nat ⇒ 'a list ⇒ 'a list" where
  "word_pow 0 w = []" |
  "word_pow (Suc n) w = w @ word_pow n w"
end

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

lemma word_pow_alt: "compow n w = concat (replicate n w)"
  by (induct n) auto

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


subsection‹Concatenation of Languages›

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 hom_image_conc: "⟦⋀xs ys. f (xs @ ys) = f xs @ f ys⟧ ⟹ f ` (A @@ B) = f ` A @@ f ` B"
  unfolding conc_def by (auto simp: image_iff) metis

lemma map_image_conc[simp]: "map f ` (A @@ B) = map f ` A @@ map f ` B"
  by (simp add: hom_image_conc)

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


subsection‹Iteration of Languages›

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

lemma lang_pow_simps: "(A ^^ Suc n) = (A ^^ n @@ A)"
  using lang_pow_add[of n "Suc 0" A] by auto

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:
  "ALL 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:
  "ALL 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 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 = (EX ws. set ws ⊆ A & w = concat ws & [] ∉ set ws)"
  (is "_ = (EX ws. ?R w ws)")
proof
  assume "w : star A" thus "EX ws. ?R w ws"
  proof induct
    case Nil have "?R [] []" by simp
    thus ?case ..
  next
    case (append u v)
    moreover
    then obtain ws where "set ws ⊆ A ∧ v = concat ws ∧ [] ∉ set ws" by blast
    ultimately have "?R (u@v) (if u = [] then ws else u#ws)" by auto
    thus ?case ..
  qed
next
  assume "EX 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 & [] ∉ set ws}"
  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 ⟹ EX vs. concat us = concat vs ∧ set vs ⊆ A"
      (is "?P ⟹ EX 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_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 Ball_starI: "∀a ∈ set as. [a] ∈ A ⟹ as ∈ star A"
  by (induct as rule: rev_induct) auto

lemma map_image_star[simp]: "map f ` star A = star (map f ` A)"
  by (auto elim: star_induct) (auto elim: star_induct simp del: map_append simp: map_append[symmetric] intro!: imageI)

subsection ‹Left-Quotients of Languages›

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

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

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


lemma lQuot_empty[simp]:   "lQuot a {} = {}"
  and lQuot_epsilon[simp]: "lQuot a {[]} = {}"
  and lQuot_char[simp]:    "lQuot a {[b]} = (if a = b then {[]} else {})"
  and lQuot_chars[simp]:   "lQuot a {[b] | b. P b} = (if P a then {[]} else {})"
  and lQuot_union[simp]:   "lQuot a (A ∪ B) = lQuot a A ∪ lQuot a B"
  and lQuot_inter[simp]:   "lQuot a (A ∩ B) = lQuot a A ∩ lQuot a B"
  and lQuot_compl[simp]:   "lQuot a (-A) = - lQuot a A"
  by (auto simp: lQuot_def)

lemma lQuot_conc_subset: "lQuot a A @@ B ⊆ lQuot a (A @@ B)" (is "?L ⊆ ?R")
proof 
  fix w assume "w ∈ ?L"
  then obtain u v where "w = u @ v" "a # u ∈ A" "v ∈ B"
    by (auto simp: lQuot_def)
  then have "a # w ∈ A @@ B"
    by (auto intro: concI[of "a # u", simplified])
  thus "w ∈ ?R" by (auto simp: lQuot_def)
qed

lemma lQuot_conc [simp]: "lQuot c (A @@ B) = (lQuot c A) @@ B ∪ (if [] ∈ A then lQuot c B else {})"
  unfolding lQuot_def conc_def
  by (auto simp add: Cons_eq_append_conv)

lemma lQuot_star [simp]: "lQuot c (star A) = (lQuot c A) @@ star A"
proof -
  have incl: "[] ∈ A ⟹ lQuot c (star A) ⊆ (lQuot c A) @@ star A"
    unfolding lQuot_def conc_def 
    apply(auto simp add: Cons_eq_append_conv)
    apply(drule star_decom)
    apply(auto simp add: Cons_eq_append_conv)
    done

  have "lQuot c (star A) = lQuot c (A @@ star A ∪ {[]})"
    by (simp only: star_unfold_left[symmetric])
  also have "... = lQuot c (A @@ star A)"
    by (simp only: lQuot_union) (simp)
  also have "... =  (lQuot c A) @@ (star A) ∪ (if [] ∈ A then lQuot c (star A) else {})"
    by simp
   also have "... =  (lQuot c A) @@ star A"
    using incl by auto
  finally show "lQuot c (star A) = (lQuot c A) @@ star A" . 
qed

lemma lQuot_diff[simp]: "lQuot c (A - B) = lQuot c A - lQuot c B"
  by(auto simp add: lQuot_def)

lemma lQuot_lists[simp]: "c : S ⟹ lQuot c (lists S) = lists S"
  by(auto simp add: lQuot_def)

lemma lQuots_simps [simp]:
  shows "lQuots [] A = A"
  and   "lQuots (c # s) A = lQuots s (lQuot c A)"
  and   "lQuots (s1 @ s2) A = lQuots s2 (lQuots s1 A)"
  unfolding lQuots_def lQuot_def by auto

lemma lQuots_append[iff]: "v ∈ lQuots w A ⟷ w @ v ∈ A"
  by (induct w arbitrary: v A) (auto simp add: lQuot_def)

subsection ‹Right-Quotients of Languages›

definition rQuot :: "'a ⇒ 'a lang ⇒ 'a lang"
where "rQuot x A = { xs. xs @ [x] ∈ A }"

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

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

lemma rQuot_rev_lQuot: "rQuot x A = rev ` lQuot x (rev ` A)"
  unfolding rQuot_def lQuot_def by (auto simp: rev_swap[symmetric])

lemma rQuots_rev_lQuots: "rQuots x A = rev ` lQuots x (rev ` A)"
  unfolding rQuots_def lQuots_def by (auto simp: rev_swap[symmetric])

lemma rQuot_empty[simp]:   "rQuot a {} = {}"
  and rQuot_epsilon[simp]: "rQuot a {[]} = {}"
  and rQuot_char[simp]:    "rQuot a {[b]} = (if a = b then {[]} else {})"
  and rQuot_union[simp]:   "rQuot a (A ∪ B) = rQuot a A ∪ rQuot a B"
  and rQuot_inter[simp]:   "rQuot a (A ∩ B) = rQuot a A ∩ rQuot a B"
  and rQuot_compl[simp]:   "rQuot a (-A) = - rQuot a A"
  by (auto simp: rQuot_def)

lemma lQuot_rQuot: "lQuot a (rQuot b A) = rQuot b (lQuot a A)"
  unfolding lQuot_def rQuot_def by auto

lemma rQuot_lQuot: "rQuot a (lQuot b A) = lQuot b (rQuot a A)"
  unfolding lQuot_def rQuot_def by auto

lemma rev_simp_invert: "(xs @ [x] = rev zs) = (zs = x # rev xs)"
  by (induct zs) auto

lemma rev_append_invert: "(xs @ ys = rev zs) = (zs = rev ys @ rev xs)"
  by (induct xs arbitrary: ys rule: rev_induct) auto

lemma image_rev_lists[simp]: "rev ` lists S = lists S"
proof (intro set_eqI)
  fix xs
  show "xs ∈ rev ` lists S ⟷ xs ∈ lists S"
  proof (induct xs rule: rev_induct)
    case (snoc x xs)
    thus ?case by (auto intro!: image_eqI[of _ rev] simp: rev_simp_invert)
  qed simp
qed

lemma image_rev_conc[simp]: "rev ` (A @@ B) = rev ` B @@ rev ` A"
  by auto (auto simp: rev_append[symmetric] simp del: rev_append)

lemma image_rev_star[simp]: "rev ` star A = star (rev ` A)"
  by (auto elim: star_induct) (auto elim: star_induct simp: rev_append[symmetric] simp del: rev_append)

lemma rQuot_conc [simp]: "rQuot c (A @@ B) = A @@ (rQuot c B) ∪ (if [] ∈ B then rQuot c A else {})"
  unfolding rQuot_rev_lQuot by (auto simp: image_image image_Un)

lemma rQuot_star [simp]: "rQuot c (star A) = star A @@ (rQuot c A)"
  unfolding rQuot_rev_lQuot by (auto simp: image_image)

lemma rQuot_diff[simp]: "rQuot c (A - B) = rQuot c A - rQuot c B"
  by(auto simp add: rQuot_def)

lemma rQuot_lists[simp]: "c : S ⟹ rQuot c (lists S) = lists S"
  by(auto simp add: rQuot_def)

lemma rQuots_simps [simp]:
  shows "rQuots [] A = A"
  and   "rQuots (c # s) A = rQuots s (rQuot c A)"
  and   "rQuots (s1 @ s2) A = rQuots s2 (rQuots s1 A)"
  unfolding rQuots_def rQuot_def by auto

lemma rQuots_append[iff]: "v ∈ rQuots w A ⟷ v @ rev w ∈ A"
  by (induct w arbitrary: v A) (auto simp add: rQuot_def)

subsection ‹Two-Sided-Quotients of Languages›

definition biQuot :: "'a ⇒ 'a ⇒ 'a lang ⇒ 'a lang"
where "biQuot x y A = { xs. x # xs @ [y] ∈ A }"

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

abbreviation 
  biQuotss :: "'a list ⇒ 'a list ⇒ 'a lang set ⇒ 'a lang"
where
  "biQuotss xs ys As ≡ ⋃ (biQuots xs ys ` As)"

lemma biQuot_rQuot_lQuot: "biQuot x y A = rQuot y (lQuot x A)"
  unfolding biQuot_def rQuot_def lQuot_def by auto

lemma biQuot_lQuot_rQuot: "biQuot x y A = lQuot x (rQuot y A)"
  unfolding biQuot_def rQuot_def lQuot_def by auto

lemma biQuots_rQuots_lQuots: "biQuots x y A = rQuots y (lQuots x A)"
  unfolding biQuots_def rQuots_def lQuots_def by auto

lemma biQuots_lQuots_rQuots: "biQuots x y A = lQuots x (rQuots y A)"
  unfolding biQuots_def rQuots_def lQuots_def by auto

lemma biQuot_empty[simp]:   "biQuot a b {} = {}"
  and biQuot_epsilon[simp]: "biQuot a b {[]} = {}"
  and biQuot_char[simp]:    "biQuot a b {[c]} = {}"
  and biQuot_union[simp]:   "biQuot a b (A ∪ B) = biQuot a b A ∪ biQuot a b B"
  and biQuot_inter[simp]:   "biQuot a b (A ∩ B) = biQuot a b A ∩ biQuot a b B"
  and biQuot_compl[simp]:   "biQuot a b (-A) = - biQuot a b A"
  by (auto simp: biQuot_def)

lemma biQuot_conc [simp]: "biQuot a b (A @@ B) =
  lQuot a A @@ rQuot b B ∪
  (if [] ∈ A ∧ [] ∈ B then biQuot a b A ∪ biQuot a b B
  else if [] ∈ A then biQuot a b B
  else if [] ∈ B then biQuot a b A
  else {})"
  unfolding biQuot_rQuot_lQuot by auto

lemma biQuot_star [simp]: "biQuot a b (star A) = biQuot a b A ∪ lQuot a A @@ star A @@ rQuot b A"
  unfolding biQuot_rQuot_lQuot by auto

lemma biQuot_diff[simp]: "biQuot a b (A - B) = biQuot a b A - biQuot a b B"
  by(auto simp add: biQuot_def)

lemma biQuot_lists[simp]: "a : S ⟹ b : S ⟹ biQuot a b (lists S) = lists S"
  by(auto simp add: biQuot_def)

lemma biQuots_simps [simp]:
  shows "biQuots [] [] A = A"
  and   "biQuots (a#as) (b#bs) A = biQuots as bs (biQuot a b A)"
  and   "⟦length s1 = length t1; length s2 = length t2⟧ ⟹
    biQuots (s1 @ s2) (t1 @ t2) A = biQuots s2 t2 (biQuots s1 t1 A)"
  unfolding biQuots_def biQuot_def by auto

lemma biQuots_append[iff]: "v ∈ biQuots u w A ⟷ u @ v @ rev w ∈ A"
  unfolding biQuots_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 "ALL u : A. length u ≥ 1"
      by (metis Suc_eq_plus1 add_leD2 le_0_eq length_0_conv not_less_eq_eq)
    hence "ALL u : A^^(?n+1). length u ≥ ?n+1"
      by (metis length_lang_pow_lb nat_mult_1)
    hence "ALL 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 "EX 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 "ALL u : A. length u ≥ 1"
      by (metis Suc_eq_plus1 add_leD2 le_0_eq length_0_conv not_less_eq_eq)
    hence "ALL u : A^^(?n+1). length u ≥ ?n+1"
      by (metis length_lang_pow_lb nat_mult_1)
    hence "ALL 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 "EX 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

subsection ‹Lists of Fixed Length›

abbreviation listsN where "listsN n S ≡ {xs. xs ∈ lists S ∧ length xs = n}"

lemma tl_listsN: "A ⊆ listsN (n + 1) S ⟹ tl ` A ⊆ listsN n S"
proof (intro image_subsetI)
  fix xs assume "A ⊆ listsN (n + 1) S" "xs ∈ A"
  thus "tl xs ∈ listsN n S" by (induct xs) auto
qed

lemma map_tl_listsN: "A ⊆ lists (listsN (n + 1) S) ⟹ map tl ` A ⊆ lists (listsN n S)"
proof (intro image_subsetI)
  fix xss assume "A ⊆ lists (listsN (n + 1) S)" "xss ∈ A"
  hence "set xss ⊆ listsN (n + 1) S" by auto
  hence "∀xs ∈ set xss. tl xs ∈ listsN n S" using tl_listsN[of "set xss" S n] by auto
  thus "map tl xss ∈ lists (listsN n S)" by (induct xss) auto
qed

(*<*)
end
(*>*)