# 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"

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 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"

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 = {}"

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)
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

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(drule star_decom)
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"

lemma lQuot_lists[simp]: "c : S ⟹ lQuot c (lists S) = lists S"

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"

lemma rQuot_lists[simp]: "c : S ⟹ rQuot c (lists S) = lists S"

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"

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

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)"
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))"
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 "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
(*>*)
```