# Theory WS1S

```(* Author: Dmitriy Traytel *)

section ‹WS1S›

(*<*)
theory WS1S
imports Formula Pi_Regular_Operators "HOL-Library.Stream"
begin
(*>*)

subsection ‹Encodings›

definition "cut_same x s = stake (LEAST n. sdrop n s = sconst x) s"

abbreviation "poss I ≡ (⋃x∈set I. case x of Inl p ⇒ {p} | Inr P ⇒ P)"

declare smap_sconst[simp]

lemma (in wellorder) min_Least:
"⟦∃n. P n; ∃n. Q n⟧ ⟹ min (Least P) (Least Q) = (LEAST n. P n ∨ Q n)"
proof (intro sym[OF Least_equality])
fix y assume "P y ∨ Q y"
thus "min (Least P) (Least Q) ≤ y"
proof (elim disjE)
assume "P y"
hence "Least P ≤ y" by (auto intro: LeastI2_wellorder)
thus "min (Least P) (Least Q) ≤ y" unfolding min_def by auto
next
assume "Q y"
hence "Least Q ≤ y" by (auto intro: LeastI2_wellorder)
thus "min (Least P) (Least Q) ≤ y" unfolding min_def by auto
qed
qed (metis LeastI_ex min_def)

lemma sconst_collapse: "y ## sconst y = sconst y"
by (subst (2) siterate.ctr) auto

lemma shift_sconst_inj: "⟦length x = length y; x @- sconst z = y @- sconst z⟧ ⟹ x = y"
by (induct rule: list_induct2) auto

context formula
begin

definition "any ≡ hd Σ"

lemma any_Σ[simp]: "any ∈ set Σ"
unfolding any_def by (auto simp: nonempty intro: someI[of _ "hd Σ"])

lemma any_σ[simp]: "length bs = n ⟹ (any, bs) ∈ set (σ Σ n)"
by (auto simp: σ_def set_n_lists)

fun stream_enc :: "'a interp ⇒ ('a × bool list) stream" where
"stream_enc (w, I) = smap2 (enc_atom I) nats (w @- sconst any)"

lemma tl_stream_enc[simp]: "smap π (stream_enc (w, x # I)) = stream_enc (w, I)"
by (auto simp: comp_def π_def)

lemma enc_atom_max: "⟦∀x∈set I. case x of Inl p ⇒ p ≤ n | Inr P ⇒ ∀p∈P. p ≤ n; n ≤ n'⟧ ⟹
enc_atom I (Suc n') a = (a, replicate (length I) False)"
by (induct I) (auto split: sum.splits)

lemma ex_Loop_stream_enc:
assumes "∀x ∈ set I. case x of Inr P ⇒ finite P | _ ⇒ True"
shows "∃n. sdrop n (stream_enc (w, I)) = sconst (any, replicate (length I) False)"
proof -
from assms have "∃n > length w. ∀x∈set I. case x of Inl p ⇒ p ≤ n | Inr P ⇒ ∀p∈P. p ≤ n"
proof (induct I)
case (Cons x I)
then obtain n where IH: "length w < n"
"∀x∈set I. case x of Inl p ⇒ p ≤ n | Inr P ⇒ ∀p∈P. p ≤ n" by auto
thus ?case
proof (cases x)
case (Inl p)
with IH show ?thesis
by (intro exI[of _ "max p n"]) (fastforce split: sum.splits)
next
case (Inr P)
with IH Cons(2) show ?thesis
by (intro exI[of _ "max (Max P) n"]) (fastforce dest: Max_ge split: sum.splits)
qed
qed auto
then obtain n where "length w < n" "∀x∈set I. case x of Inl p ⇒ p ≤ n | Inr P ⇒ ∀p∈P. p ≤ n"
by (elim exE conjE)
hence "sdrop (Suc n) (stream_enc (w, I)) = sconst (any, replicate (length I) False)"
(is "?s1 n = ?s2")
by (intro stream.coinduct[of "λs1 s2. ∃n'≥ n. s1 = ?s1 n' ∧ s2 = ?s2"])
(auto simp: enc_atom_max dest: le_SucI)
thus ?thesis by blast
qed

lemma length_snth_enc[simp]: "length (snd (stream_enc (w, I) !! n)) = length I"
by auto

lemma sset_singleton[simp]: "sset s ⊆ {x} ⟷ sset s = {x}"
by (cases s) auto

lemma drop_sconstE: "⟦drop n w @- sconst y = sconst y; p < length w; ¬ p < n⟧ ⟹ w ! p = y"
unfolding not_less sconst_alt proof (induct p arbitrary: w n)
case (Suc p)
with Suc(1)[of 0 "tl w"] show ?case
by (cases w n rule: list.exhaust[case_product nat.exhaust]) auto

lemma less_length_cut_same:
"⟦(w @- sconst y) !! p = a⟧ ⟹ a = y ∨ (p < length (cut_same y (w @- sconst y)) ∧ w ! p = a)"
unfolding cut_same_def length_stake
by (rule LeastI2_ex[OF exI[of _ "length w"]])
(auto simp: sdrop_shift shift_snth split: if_split_asm elim!: drop_sconstE)

lemma less_length_cut_same_Inl:
"⟦(∀x ∈ set I. case x of Inr P ⇒ finite P | _ ⇒ True); r < length I; I ! r = Inl p⟧ ⟹
p < length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))"
unfolding cut_same_def length_stake
by (erule LeastI2_ex[OF ex_Loop_stream_enc ccontr],
metis)

lemma less_length_cut_same_Inr:
"⟦(∀x ∈ set I. case x of Inr P ⇒ finite P | _ ⇒ True); r < length I; I ! r = Inr P⟧ ⟹
∀p ∈ P. p < length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))"
unfolding cut_same_def length_stake
by (rule ballI, erule LeastI2_ex[OF ex_Loop_stream_enc ccontr],
metis)

fun enc :: "'a interp ⇒ ('a × bool list) list set" where
"enc (w, I) = {x. ∃n. x = (cut_same (any, replicate (length I) False) (stream_enc (w, I)) @
replicate n (any, replicate (length I) False))}"

lemma cut_same_all[simp]: "cut_same x (sconst x) = []"
unfolding cut_same_def by (auto intro: Least_equality)

lemma cut_same_stop[simp]:
assumes "x ≠ y"
shows "cut_same x (xs @- y ## sconst x) = xs @ [y]" (is "cut_same x ?s = _")
proof -
have "(LEAST n. sdrop n ?s = sconst x) = Suc (length xs)"
proof (rule Least_equality)
show "sdrop (Suc (length xs)) ?s = sconst x" by (auto simp: sdrop_shift)
next
fix m assume *: "sdrop m ?s = sconst x"
{ assume "m < Suc (length xs)"
hence "m ≤ length xs" by simp
then obtain ys where "sdrop m ?s = ys @- y ## sconst x"
by atomize_elim (induct m arbitrary: xs, auto)
with * obtain "ys @- y ## sconst x = sconst x" by simp
from arg_cong[OF this, of "sdrop (length ys)"] have "y ## sconst x = sconst x"
by (auto simp: sdrop_shift)
with assms have False by (metis siterate.code stream.inject)
}
thus "Suc (length xs) ≤ m" by (blast intro: leI)
qed
thus ?thesis unfolding cut_same_def stake_shift by simp
qed

lemma cut_same_shift_sconst: "∃n. w = cut_same x (w @- sconst x) @ replicate n x"
proof (induct w rule: rev_induct)
case (snoc a w)
then obtain n where "w = cut_same x (w @- sconst x) @ replicate n x" by blast
thus ?case
by (cases "a = x")
(auto simp: id_def[symmetric] siterate.code[of id, simplified id_apply, symmetric]
replicate_append_same[symmetric] intro!: exI[of _ "Suc n"])

lemma set_cut_same: "set (cut_same x (w @- sconst x)) ⊆ set w"
proof (induct w rule: rev_induct)
case (snoc a w)
thus ?case by (cases "a = x")
(auto simp: id_def[symmetric] siterate.code[of id, simplified id_apply, symmetric])

lemma stream_enc_cut_same:
assumes "(∀x ∈ set I. case x of Inr P ⇒ finite P | _ ⇒ True)"
shows "stream_enc (w, I) = cut_same (any, replicate (length I) False) (stream_enc (w, I)) @-
sconst (any, replicate (length I) False)"
unfolding cut_same_def
by (rule trans[OF sym[OF stake_sdrop] arg_cong2[of _ _ _ _ "(@-)", OF refl]])
(rule LeastI_ex[OF ex_Loop_stream_enc[OF assms]])

lemma stream_enc_enc:
assumes "(∀x ∈ set I. case x of Inr P ⇒ finite P | _ ⇒ True)" and  v: "v ∈ enc (w, I)"
shows "stream_enc (w, I) = v @- sconst (any, replicate (length I) False)"
(is "?s = ?v @- sconst ?F")
proof -
from assms(1) obtain n where "sdrop n (stream_enc (w, I)) = sconst ?F" by (metis ex_Loop_stream_enc)
moreover from v obtain m where "?v = cut_same ?F ?s @ replicate m ?F" by auto
ultimately show "?s = v @- sconst ?F"
by (auto simp del: stream_enc.simps intro: stream_enc_cut_same[OF assms(1)])
qed

lemma stream_enc_enc_some:
assumes "(∀x ∈ set I. case x of Inr P ⇒ finite P | _ ⇒ True)"
shows "stream_enc (w, I) = (SOME v. v ∈ enc (w, I)) @- sconst (any, replicate (length I) False)"
by (rule stream_enc_enc[OF assms], rule someI_ex) auto

lemma enc_unique_length: "v ∈ enc (w, I) ⟹ ∀v'. length v' = length v ∧ v' ∈ enc (w, I) ⟶ v = v'"
by auto

lemma sdrop_sconst: "sdrop n s = sconst x ⟹ n ≤ m ⟹ s !! m = x"
by (metis le_iff_add sdrop_snth snth_siterate[of id, simplified id_funpow id_apply])

lemma fin_cut_same_tl:
assumes "∃n. sdrop n s = sconst x"
shows "fin_cut_same (π x) (map π (cut_same x s)) = cut_same (π x) (smap π s)"
proof -
define min where "min = (LEAST n. sdrop n s = sconst x)"
from assms have min: "sdrop min s = sconst x" "⋀m. sdrop m s = sconst x ⟹ min ≤ m"
unfolding min_def by (auto intro: LeastI Least_le)
have Ex: "∃n. drop n (map π (stake min s)) = replicate (length (map π (stake min s)) - n) (π x)"
by (auto intro: exI[of _ "length (map π (stake min s))"])
have "fin_cut_same (π x) (map π (cut_same x s)) =
map π (stake  (LEAST n.
map π (stake (min - n) (sdrop n s)) = replicate (min - n) (π x) ∨ sdrop n s = sconst x) s)"
unfolding fin_cut_same_def cut_same_def take_map take_stake min_Least[OF Ex assms, folded min_def]
min_def[symmetric] by (auto simp: drop_map drop_stake)
also have "(λn. map π (stake (min - n) (sdrop n s)) = replicate (min - n) (π x) ∨ sdrop n s = sconst x) =
(λn. smap π (sdrop n s) = sconst (π x))"
proof (rule ext, unfold smap_alt snth_siterate[of id, simplified id_funpow id_apply], safe)
fix n m
assume "map π (stake (min - n) (sdrop n s)) = replicate (min - n) (π x)"
hence "∀y∈set (stake (min - n) (sdrop n s)). π y = π x"
by (intro iffD1[OF map_eq_conv]) (metis length_stake map_replicate_const)
hence "∀i<min - n. π (sdrop n s !! i) = π x"
unfolding all_set_conv_all_nth by (auto simp: sdrop_snth)
thus "π (sdrop n s !! m) = π x"
proof (cases "m < min - n")
case False
hence "min ≤ n + m" by linarith
hence "sdrop n s !! m = x" unfolding sdrop_snth by (rule sdrop_sconst[OF min(1)])
thus ?thesis by simp
qed auto
next
fix n
assume "∀m. π (sdrop n s !! m) = π x"
thus "map π (stake (min - n) (sdrop n s)) = replicate (min - n) (π x)"
unfolding stake_smap[symmetric] smap_alt[symmetric, of π "sdrop n s" "sconst (π x)", simplified]
by (auto simp: map_replicate_const)
qed auto
finally show ?thesis unfolding cut_same_def sdrop_smap stake_smap .
qed

lemma tl_enc[simp]:
assumes "∀x ∈ set (x # I). case x of Inr P ⇒ finite P | _ ⇒ True"
shows "SAMEQUOT (any, replicate (length I) False) (map π ` enc (w, x # I)) = enc (w, I)"
unfolding SAMEQUOT_def
by (fastforce simp: assms π_def
fin_cut_same_tl[OF ex_Loop_stream_enc[OF assms], unfolded π_def, simplified, symmetric])

lemma encD:
"⟦v ∈ enc (w, I); (∀x ∈ set I. case x of Inr P ⇒ finite P | _ ⇒ True)⟧ ⟹
v = map (case_prod (enc_atom I)) (zip [0 ..< length v] (stake (length v) (w @- sconst any)))"
by (erule box_equals[OF sym[OF arg_cong[of _ _ "stake (length v)" ,OF stream_enc_enc]]])
(auto simp: stake_shift sdrop_shift stake_add[symmetric] map_replicate_const)

lemma enc_Inl: "⟦x ∈ enc (w, I); (∀x ∈ set I. case x of Inr P ⇒ finite P | _ ⇒ True);
m < length I; I ! m = Inl p⟧ ⟹ p < length x ∧ snd (x ! p) ! m"
by (auto dest!: less_length_cut_same_Inl[of _ _ _ w] simp: nth_append cut_same_def)

lemma enc_Inr: assumes "x ∈ enc (w, I)" "∀x ∈ set I. case x of Inr P ⇒ finite P | _ ⇒ True"
"M < length I" "I ! M = Inr P"
shows "p ∈ P ⟷ p < length x ∧ snd (x ! p) ! M"
proof
assume "p ∈ P" with assms show "p < length x ∧ snd (x ! p) ! M"
by (auto dest!: less_length_cut_same_Inr[of _ _ _ w] simp: nth_append cut_same_def)
next
assume "p < length x ∧ snd (x ! p) ! M"
thus "p ∈ P" using assms by (subst (asm) (2) encD[OF assms(1,2)]) auto
qed

lemma enc_length:
assumes "enc (w, I) = enc (w', I')"
shows "length I = length I'"
proof -
let ?cL = "λw I. cut_same (any, replicate (length I) False) (stream_enc (w, I))"
let ?w = "λw I m. ?cL w I @ replicate (m - length (?cL w I)) (any, replicate (length I) False)"
let ?max = "max (length (?cL w I)) (length (?cL w' I')) + 1"
from assms have "?w w I ?max ∈ enc (w, I)" "?w w' I' ?max ∈ enc (w', I')" by auto
hence "?w w I ?max = ?w w' I' ?max" using enc_unique_length assms by (simp del: enc.simps)
moreover have "last (?w w I ?max) = (any, replicate (length I) False)"
"last (?w w' I' ?max) = (any, replicate (length I') False)" by auto
ultimately show "length I = length I'" by auto
qed

lemma enc_stream_enc:
"⟦(∀x ∈ set I. case x of Inr P ⇒ finite P | _ ⇒ True);
(∀x ∈ set I'. case x of Inr P ⇒ finite P | _ ⇒ True);
enc (w, I) = enc (w', I')⟧ ⟹ stream_enc (w, I) = stream_enc (w', I')"
by (rule box_equals[OF _ sym[OF stream_enc_enc_some] sym[OF stream_enc_enc_some]])
(auto dest: enc_length simp del: enc.simps)

abbreviation "wf_interp w I ≡
((∀a ∈ set w. a ∈ set Σ) ∧ (∀x ∈ set I. case x of Inr P ⇒ finite P | _ ⇒ True))"

fun wf_interp_for_formula :: "'a interp ⇒ 'a formula ⇒ bool" where
"wf_interp_for_formula (w, I) φ =
(wf_interp w I ∧
(∀n ∈ FOV φ. case I ! n of Inl _ ⇒ True | _ ⇒ False) ∧
(∀n ∈ SOV φ. case I ! n of Inl _ ⇒ False | Inr _ ⇒ True))"

fun satisfies :: "'a interp ⇒ 'a formula ⇒ bool" (infix "⊨" 50) where
"(w, I) ⊨ FQ a m = ((case I ! m of Inl p ⇒ if p < length w then w ! p else any) = a)"
| "(w, I) ⊨ FLess m1 m2 = ((case I ! m1 of Inl p ⇒ p) < (case I ! m2 of Inl p ⇒ p))"
| "(w, I) ⊨ FIn m M = ((case I ! m of Inl p ⇒ p) ∈ (case I ! M of Inr P ⇒ P))"
| "(w, I) ⊨ FNot φ = (¬ (w, I) ⊨ φ)"
| "(w, I) ⊨ (FOr φ⇩1 φ⇩2) = ((w, I) ⊨ φ⇩1 ∨ (w, I) ⊨ φ⇩2)"
| "(w, I) ⊨ (FAnd φ⇩1 φ⇩2) = ((w, I) ⊨ φ⇩1 ∧ (w, I) ⊨ φ⇩2)"
| "(w, I) ⊨ (FExists φ) = (∃p. (w, Inl p # I) ⊨ φ)"
| "(w, I) ⊨ (FEXISTS φ) = (∃P. finite P ∧ (w, Inr P # I) ⊨ φ)"

definition lang⇩W⇩S⇩1⇩S :: "nat ⇒ 'a formula ⇒ ('a × bool list) list set" where
"lang⇩W⇩S⇩1⇩S n φ = ⋃{enc (w, I) | w I . length I = n ∧ wf_interp_for_formula (w, I) φ ∧ (w, I) ⊨ φ}"

lemma encD_ex: "⟦x ∈ enc (w, I); (∀x ∈ set I. case x of Inr P ⇒ finite P | _ ⇒ True)⟧ ⟹
∃n. x = map (case_prod (enc_atom I)) (zip [0 ..< n] (stake n (w @- sconst any)))"
by (auto dest!: encD simp del: enc.simps)

lemma enc_set_σ: "⟦x ∈ enc (w, I); (∀x ∈ set I. case x of Inr P ⇒ finite P | _ ⇒ True);
length I = n; a ∈ set x; set w ⊆ set Σ⟧ ⟹ a ∈ set (σ Σ n)"
by (force dest: encD_ex intro: enc_atom_σ simp: in_set_zip shift_snth simp del: enc.simps)

definition "positions_in_row s i =
Option.these (sset (smap2 (λp (_, bs). if nth bs i then Some p else None) nats s))"

lemma positions_in_row: "positions_in_row s i = {p. snd (s !! p) ! i}"
unfolding positions_in_row_def Option.these_def smap2_szip stream.set_map sset_range
by (auto split: if_split_asm intro!: image_eqI[of _ the] split: prod.splits)

lemma positions_in_row_unique: "∃!p. snd (s !! p) ! i ⟹
the_elem (positions_in_row s i) = (THE p. snd (s !! p) ! i)"
by (rule the1I2) (auto simp: the_elem_def positions_in_row)

lemma positions_in_row_nth: "∃!p. snd (s !! p) ! i ⟹
snd (s !! the_elem (positions_in_row s i)) ! i"
unfolding positions_in_row_unique by (rule the1I2) auto

definition "dec_word s = cut_same any (smap fst s)"

lemma dec_word_stream_enc: "dec_word (stream_enc (w, I)) = cut_same any (w @- sconst any)"
unfolding dec_word_def by (auto intro!: arg_cong[of _ _ "cut_same any"] simp: smap2_alt)

definition "stream_dec n FO (s :: ('a × bool list) stream) = map (λi.
if i ∈ FO
then Inl (the_elem (positions_in_row s i))
else Inr (positions_in_row s i)) [0..<n]"

lemma stream_dec_Inl: "⟦i ∈ FO; i < n⟧ ⟹ ∃p. stream_dec n FO s ! i = Inl p"
unfolding stream_dec_def using nth_map[of n "[0..<n]"] by auto

lemma stream_dec_not_Inr: "⟦stream_dec n FO s ! i = Inr P; i ∈ FO; i < n⟧ ⟹ False"
unfolding stream_dec_def using nth_map[of n "[0..<n]"] by auto

lemma stream_dec_Inr: "⟦i ∉ FO; i < n⟧ ⟹ ∃P. stream_dec n FO s ! i = Inr P"
unfolding stream_dec_def using nth_map[of n "[0..<n]"] by auto

lemma stream_dec_not_Inl: "⟦stream_dec n FO s ! i = Inl p; i ∉ FO; i < n⟧ ⟹ False"
unfolding stream_dec_def using nth_map[of n "[0..<n]"] by auto

lemma Inr_dec_finite: "⟦∀i<n. finite {p. snd (s !! p) ! i}; Inr P ∈ set (stream_dec n FO s)⟧ ⟹
finite P"
unfolding stream_dec_def by (auto simp: positions_in_row)

lemma enc_atom_dec:
"⟦∀p. length (snd (s !! p)) = n; ∀i ∈ FO. i < n ⟶ (∃!p. snd (s !! p) ! i); a = fst (s !! p)⟧ ⟹
enc_atom (stream_dec n FO s) p a = s !! p"
unfolding stream_dec_def
by (rule sym, subst surjective_pairing[of "s !! p"])
(auto intro!: nth_equalityI simp: positions_in_row simp del: prod.collapse split: if_split_asm,
(metis positions_in_row positions_in_row_nth)+)

lemma length_stream_dec[simp]: "length (stream_dec n FO x) = n"
unfolding stream_dec_def by auto

lemma stream_enc_dec:
"⟦∃n. sdrop n (smap fst s) = sconst any;
stream_all (λx. length (snd x) = n) s; ∀i ∈ FO. (∃!p. snd (s !! p) ! i)⟧ ⟹
stream_enc (dec_word s, stream_dec n FO s) = s"
unfolding dec_word_def
by (drule LeastI_ex)
(auto intro!: enc_atom_dec simp: smap2_alt cut_same_def
simp del: stake_smap sdrop_smap
intro!: trans[OF arg_cong2[of _ _ _ _ "(!!)"] snth_smap]
trans[OF arg_cong2[of _ _ _ _ "(@-)"] stake_sdrop])

lemma stream_enc_unique:
"i < length I ⟹ ∃p. I ! i = Inl p ⟹ ∃!p. snd (stream_enc (w, I) !! p) ! i"
by auto

lemma stream_dec_enc_Inl:
"⟦stream_dec n FO (stream_enc (w, I)) ! i = Inl p'; I ! i = Inl p; i ∈ FO; i < n; length I = n⟧ ⟹
p = p'"
unfolding stream_dec_def
by (auto intro!: trans[OF _ sym[OF  positions_in_row_unique[OF stream_enc_unique]]]
simp del: stream_enc.simps) simp

lemma stream_dec_enc_Inr:
"⟦stream_dec n FO (stream_enc (w, I)) ! i = Inr P'; I ! i = Inr P; i ∉ FO; i < n; length I = n⟧ ⟹
P = P'"
unfolding stream_dec_def positions_in_row by auto

lemma Collect_snth: "{p. P ((x ## s) !! p)} ⊆ {0} ∪ Suc ` {p. P (s !! p)}"
unfolding image_def by (auto simp: gr0_conv_Suc)

lemma finite_True_in_row: "∀i < n. finite {p. snd ((w @- sconst (any, replicate n False)) !! p) ! i}"
by (induct w) (auto simp: id_def[symmetric] intro: finite_subset[OF Collect_snth])

lemma lang_ENC:
assumes "FO ⊆ {0 ..< n}" "SO ⊆ {0 ..< n} - FO"
shows "lang n (ENC n FO) = ⋃{enc (w, I) | w I . length I = n ∧ wf_interp w I ∧
(∀i ∈ FO. case I ! i of Inl _ ⇒ True | Inr _ ⇒ False) ∧
(∀i ∈ SO. case I ! i of Inl _ ⇒ False | Inr _ ⇒ True)}"
(is "?L = ?R")
proof (intro equalityI subsetI)
fix x assume L: "x ∈ ?L"
from assms(1) have fin: "finite FO" by (auto simp: finite_subset)
have *: "set x ⊆ set (σ Σ n)" using subsetD[OF assms(1)]
bspec[OF wf_lang_wf_word[OF wf_rexp_ENC[OF fin]] L]
by (cases n) (auto simp: wf_word)
let ?s = "x @- sconst (any, replicate n False)"
from assms have "list_all (λbs. length (snd bs) = n) x"
using * by (auto simp: list_all_iff σ_def set_n_lists)
hence "stream_all (λx. length (snd x) = n) (x @- sconst (any, replicate n False))"
by (auto simp only: stream_all_shift sset_sconst length_replicate snd_conv)
moreover
{ fix m assume "m ∈ FO"
with assms have "m < n" by (auto simp: max_idx_vars)
with L ‹m ∈ FO› assms obtain u z v where uzv: "x = u @ z @ v"
"u ∈ star (lang n (Atom (Arbitrary_Except m False)))"
"z ∈ lang n (Atom (Arbitrary_Except m True))"
"v ∈ star (lang n (Atom (Arbitrary_Except m False)))" unfolding ENC_def
by (cases n)
(auto simp: not_less max_idx_vars valid_ENC_def fin intro!: wf_rexp_valid_ENC finite_FOV
dest!: iffD1[OF lang_flatten_INTERSECT, rotated -1], fast)
with ‹m < n› have "∃!p.  snd (x ! p) ! m ∧ p < length x"
proof (intro ex1I[of _ "length u"])
fix p assume "m < n" "snd (x ! p) ! m ∧ p < length x"
with star_Arbitrary_ExceptD[OF uzv(2)] Arbitrary_ExceptD[OF uzv(3)] star_Arbitrary_ExceptD[OF uzv(4)]
show "p = length u" by (cases rule: linorder_cases) (auto simp: nth_append uzv(1))
qed (auto dest!: Arbitrary_ExceptD)
then obtain p where p: "p < length x" "snd (x ! p) ! m"
"⋀q. snd (x ! q) ! m ∧ q < length x ⟶ q = p" by auto
from this(1,2) have "∃!p. snd (?s !! p) ! m"
proof (intro ex1I[of _ p])
fix q from p(1,2) p(3)[of q] ‹m < n› show "snd (?s !! q) ! m ⟹ q = p"
by (cases "q < length x")  auto
qed auto
}
moreover have "sdrop (length x) (smap fst (x @- sconst (any, replicate n False))) = sconst any"
unfolding sdrop_smap by (simp add: sdrop_shift)
ultimately have enc_dec: "stream_enc (dec_word ?s, stream_dec n FO ?s) =
x @- sconst (any, replicate n False)" by (intro stream_enc_dec) auto
define I where "I = stream_dec n FO ?s"
with assms have "wf_interp (dec_word ?s) I ∧
(∀i ∈ FO. case I ! i of Inl _ ⇒ True | Inr _ ⇒ False) ∧
(∀i ∈ SO. case I ! i of Inl _ ⇒ False | Inr _ ⇒ True)" unfolding I_def dec_word_def
by (auto dest: stream_dec_not_Inr stream_dec_not_Inl simp: σ_def  max_idx_vars
dest!: subsetD[OF set_cut_same[of any "map fst x"]] subsetD[OF *]  split: sum.splits)
(auto simp: stream_dec_def positions_in_row finite_True_in_row)
moreover have "length I = n" unfolding I_def by simp
moreover have "x ∈ enc (dec_word ?s, I)" unfolding I_def
by (simp add: enc_dec cut_same_shift_sconst del: stream_enc.simps)
ultimately show "x ∈ ?R" by blast
next
fix x assume "x ∈ ?R"
then obtain w I where I: "x ∈ enc (w, I)" "wf_interp w I ∧
(∀i ∈ FO. case I ! i of Inl _ ⇒ True | Inr _ ⇒ False) ∧
(∀i ∈ SO. case I ! i of Inl _ ⇒ False | Inr _ ⇒ True)" "length I = n" by blast
{ fix i from I(2) have "(w @- sconst any) !! i ∈ set Σ" by (cases "i < length w") auto } note * = this
from I have "x @- sconst (any, replicate (length I) False) = stream_enc (w, I)" (is "x @- ?F = ?s")
by (intro stream_enc_enc[symmetric]) auto
with * ‹length I = n› have "∀x ∈ set x. length (snd x) = n ∧ fst x ∈ set Σ"
by (auto dest!: shift_snth_less[of _ _ ?F, symmetric] simp: in_set_conv_nth)
thus "x ∈ ?L"
proof (cases "FO = {}")
case False
hence nonempty: "valid_ENC n ` FO ≠ {}" by simp
have finite: "finite (valid_ENC n ` FO)" by (rule finite_imageI[OF finite_subset[OF assms(1)]]) simp
from False assms(1) have "0 < n" by (cases n) (auto split: dest!: max_idx_vars)
with wf_rexp_valid_ENC assms have wf_rexp: "∀x ∈ valid_ENC n ` FO. wf n x"
by (auto simp: max_idx_vars)
{ fix r assume "r ∈ FO"
with I(2) obtain p where p: "I ! r = Inl p" by (cases "I ! r") auto
from ‹r ∈ FO› assms I(2,3) have r: "r < length I" by (auto dest!: max_idx_vars)
from p I(1,2) r have "p < length x"
using less_length_cut_same_Inl[of I r p w] by auto
with p I r *
have "[x ! p] ∈ lang n (Atom (Arbitrary_Except r True))"
by (subst encD[of x w I]) (auto simp del: lang.simps intro!: enc_atom_lang_Arbitrary_Except_True)
moreover
from p I r * have "take p x ∈ star (lang n (Atom (Arbitrary_Except r False)))"
by (subst encD[of x]) (auto  simp del: lang.simps simp: in_set_conv_nth intro!: Ball_starI enc_atom_lang_Arbitrary_Except_False)
moreover
from p I r * have "drop (Suc p) x ∈ star (lang n (Atom (Arbitrary_Except r False)))"
by (subst encD[of x]) (auto simp: in_set_conv_nth simp del: lang.simps snth.simps intro!: Ball_starI enc_atom_lang_Arbitrary_Except_False)
ultimately have "take p x @ [x ! p] @ drop (p + 1) x ∈ lang n (valid_ENC n r)"
using ‹0 < n› unfolding valid_ENC_def by (auto simp del: append.simps)
hence "x ∈ lang n (valid_ENC n r)" using id_take_nth_drop[OF ‹p < length x›] by auto
}
with False lang_flatten_INTERSECT[OF finite nonempty wf_rexp] show ?thesis by (auto simp: ENC_def)
qed (simp add: ENC_def, auto simp: σ_def set_n_lists image_iff)
qed

lemma lang_ENC_formula:
assumes "wf_formula n φ"
shows "lang n (ENC n (FOV φ)) = ⋃{enc (w, I) | w I . length I = n ∧ wf_interp_for_formula (w, I) φ}"
proof -
from assms max_idx_vars have *: "FOV φ ⊆ {0 ..< n}" "SOV φ ⊆ {0 ..< n} - FOV φ" by auto
show ?thesis unfolding lang_ENC[OF *] by simp
qed

subsection ‹Welldefinedness of enc wrt. Models›

lemma wf_interp_for_formula_FExists:
"⟦wf_formula (length I) (FExists φ)⟧⟹
wf_interp_for_formula (w, I) (FExists φ) ⟷ (∀p. wf_interp_for_formula (w, Inl p # I) φ)"
by (auto simp: nth_Cons' split: if_split_asm)

lemma wf_interp_for_formula_any_Inl: "wf_interp_for_formula (w, Inl p # I) φ ⟹
∀p. wf_interp_for_formula (w, Inl p # I) φ"
by (auto simp: nth_Cons' split: if_split_asm)

lemma wf_interp_for_formula_FEXISTS:
"⟦wf_formula (length I) (FEXISTS φ)⟧⟹
wf_interp_for_formula (w, I) (FEXISTS φ) ⟷ (∀P. finite P ⟶ wf_interp_for_formula (w, Inr P # I) φ)"
by (auto simp: nth_Cons' split: if_split_asm)

lemma wf_interp_for_formula_any_Inr: "wf_interp_for_formula (w, Inr P # I) φ ⟹
∀P. finite P ⟶ wf_interp_for_formula (w, Inr P # I) φ"
by (auto simp: nth_Cons' split: if_split_asm)

lemma wf_interp_for_formula_FOr:
"wf_interp_for_formula (w, I) (FOr φ1 φ2) =
(wf_interp_for_formula (w, I) φ1 ∧ wf_interp_for_formula (w, I) φ2)"
by auto

lemma wf_interp_for_formula_FAnd:
"wf_interp_for_formula (w, I) (FAnd φ1 φ2) =
(wf_interp_for_formula (w, I) φ1 ∧ wf_interp_for_formula (w, I) φ2)"
by auto

lemma enc_wf_interp:
"⟦wf_formula (length I) φ; wf_interp_for_formula (w, I) φ; x ∈ enc (w, I)⟧ ⟹
wf_interp_for_formula (dec_word (x @- sconst (any, replicate (length I) False)),
stream_dec (length I) (FOV φ) (x @- sconst (any, replicate (length I) False))) φ"
using
stream_dec_Inl[of _ "FOV φ" "length I" "stream_enc (w, I)", OF _ bspec[OF max_idx_vars]]
stream_dec_Inr[of _ "FOV φ" "length I" "stream_enc (w, I)", OF _ bspec[OF max_idx_vars]]
by (auto split: sum.splits intro: Inr_dec_finite[OF finite_True_in_row] simp: max_idx_vars dec_word_def
dest!: stream_dec_not_Inl stream_dec_not_Inr subsetD[OF set_cut_same] simp del: stream_enc.simps)
(auto simp: cut_same_def in_set_zip smap2_alt shift_snth)

lemma enc_atom_welldef: "∀x a. enc_atom I x a = enc_atom I' x a ⟹ m < length I ⟹
(case (I ! m, I' ! m) of (Inl p, Inl q) ⇒ p = q | (Inr P, Inr Q) ⇒ P = Q | _ ⇒ True)"
proof (induct "length I" arbitrary: I I' m)
case (Suc n I I')
then obtain x xs x' xs' where *: "I = x # xs" "I' = x' # xs'"
by (fastforce simp: Suc_length_conv map_eq_Cons_conv)
with Suc show ?case
proof (cases m)
case 0 thus ?thesis using Suc(3) unfolding *
by (cases x x' rule: sum.exhaust[case_product sum.exhaust]) auto
qed auto
qed simp

lemma stream_enc_welldef: "⟦stream_enc (w, I) = stream_enc (w', I'); wf_formula (length I) φ;
wf_interp_for_formula (w, I) φ; wf_interp_for_formula (w', I') φ⟧ ⟹
(w, I) ⊨ φ ⟷ (w', I') ⊨ φ"
proof (induction φ arbitrary: w w' I I')
case (FQ a m) thus ?case using enc_atom_welldef[of I I' m]
by (simp split: sum.splits add: smap2_alt shift_snth)
(metis snth_siterate[of id, simplified id_funpow id_apply])
next
case (FLess m1 m2) thus ?case using enc_atom_welldef[of I I' m1] enc_atom_welldef[of I I' m2]
by (auto split: sum.splits simp add: smap2_alt)
next
case (FIn m M) thus ?case using enc_atom_welldef[of I I' m] enc_atom_welldef[of I I' M]
by (auto split: sum.splits simp add: smap2_alt)
next
case (FOr φ1 φ2) show ?case unfolding satisfies.simps(5)
proof (intro disj_cong)
from FOr(3-6) show "(w, I) ⊨ φ1 ⟷ (w', I') ⊨ φ1"
by (intro FOr(1)) auto
next
from FOr(3-6) show "(w, I) ⊨ φ2 ⟷ (w', I') ⊨ φ2"
by (intro FOr(2)) auto
qed
next
case (FAnd φ1 φ2) show ?case unfolding satisfies.simps(6)
proof (intro conj_cong)
from FAnd(3-6) show "(w, I) ⊨ φ1 ⟷ (w', I') ⊨ φ1"
by (intro FAnd(1)) auto
next
from FAnd(3-6) show "(w, I) ⊨ φ2 ⟷ (w', I') ⊨ φ2"
by (intro FAnd(2)) auto
qed
next
case (FExists φ)
hence length: "length I' = length I" by (metis length_snth_enc)
show ?case
proof
assume "(w, I) ⊨ FExists φ"
with FExists.prems(3) obtain p where "(w, Inl p # I) ⊨ φ" by auto
moreover
with FExists.prems(1,2) have "(w', Inl p # I') ⊨ φ"
proof (intro iffD1[OF FExists.IH[of w "Inl p # I" w' "Inl p # I'"]])
from FExists.prems(2,3) show "wf_interp_for_formula (w, Inl p # I) φ"
by (blast dest: wf_interp_for_formula_FExists[of I])
next
from FExists.prems(2,4) show "wf_interp_for_formula (w', Inl p # I') φ"
by (blast dest: wf_interp_for_formula_FExists[of I', unfolded length])
qed (auto simp: smap2_alt split: sum.splits if_split_asm)
ultimately show "(w', I') ⊨ FExists φ" by auto
next
assume "(w', I') ⊨ FExists φ"
with FExists.prems(1,2,4) obtain p where "(w', Inl p # I') ⊨ φ" by auto
moreover
with FExists.prems(1,2) have "(w, Inl p # I) ⊨ φ"
proof (intro iffD2[OF FExists.IH[of w "Inl p # I" w' "Inl p # I'"]])
from FExists.prems(2,3) show "wf_interp_for_formula (w, Inl p # I) φ"
by (blast dest: wf_interp_for_formula_FExists[of I])
next
from FExists.prems(2,4) show "wf_interp_for_formula (w', Inl p # I') φ"
by (blast dest: wf_interp_for_formula_FExists[of I', unfolded length])
qed (auto simp: smap2_alt split: sum.splits if_split_asm)
ultimately show "(w, I) ⊨ FExists φ" by auto
qed
next
case (FEXISTS φ)
hence length: "length I' = length I" by (metis length_snth_enc)
show ?case
proof
assume "(w, I) ⊨ FEXISTS φ"
with FEXISTS.prems(3) obtain P where "finite P" "(w, Inr P # I) ⊨ φ" by auto
moreover
with FEXISTS.prems(1,2) have "(w', Inr P # I') ⊨ φ"
proof (intro iffD1[OF FEXISTS.IH[of w "Inr P # I" w' "Inr P # I'"]])
from FEXISTS.prems(2,3) ‹finite P› show "wf_interp_for_formula (w, Inr P # I) φ"
by (blast dest: wf_interp_for_formula_FEXISTS[of I])
next
from FEXISTS.prems(2,4) ‹finite P› show "wf_interp_for_formula (w', Inr P # I') φ"
by (blast dest: wf_interp_for_formula_FEXISTS[of I', unfolded length])
qed (auto simp: smap2_alt split: sum.splits if_split_asm)
ultimately show "(w', I') ⊨ FEXISTS φ" by auto
next
assume "(w', I') ⊨ FEXISTS φ"
with FEXISTS.prems(1,2,4) obtain P where "finite P" "(w', Inr P # I') ⊨ φ" by auto
moreover
with FEXISTS.prems have "(w, Inr P # I) ⊨ φ"
proof (intro iffD2[OF FEXISTS.IH[of w "Inr P # I" w' "Inr P # I'"]])
from FEXISTS.prems(2,3) ‹finite P› show "wf_interp_for_formula (w, Inr P # I) φ"
by (blast dest: wf_interp_for_formula_FEXISTS[of I])
next
from FEXISTS.prems(2,4) ‹finite P› show "wf_interp_for_formula (w', Inr P # I') φ"
by (blast dest: wf_interp_for_formula_FEXISTS[of I', unfolded length])
qed (auto simp: smap2_alt split: sum.splits if_split_asm)
ultimately show "(w, I) ⊨ FEXISTS φ" by auto
qed
qed auto

lemma lang⇩W⇩S⇩1⇩S_FOr:
assumes "wf_formula n (FOr φ⇩1 φ⇩2)"
shows "lang⇩W⇩S⇩1⇩S n (FOr φ⇩1 φ⇩2) ⊆
(lang⇩W⇩S⇩1⇩S n φ⇩1 ∪ lang⇩W⇩S⇩1⇩S n φ⇩2) ∩ ⋃{enc (w, I) | w I. length I = n ∧ wf_interp_for_formula (w, I) (FOr φ⇩1 φ⇩2)}"
(is "_ ⊆ (?L1 ∪ ?L2) ∩ ?ENC")
proof (intro equalityI subsetI)
fix x assume "x ∈ lang⇩W⇩S⇩1⇩S n (FOr φ⇩1 φ⇩2)"
then obtain w I where
*: "x ∈ enc (w, I)" "wf_interp_for_formula (w, I) (FOr φ⇩1 φ⇩2)" "length I = n" and
"satisfies (w, I) φ⇩1 ∨ satisfies (w, I) φ⇩2" unfolding lang⇩W⇩S⇩1⇩S_def by auto
thus "x ∈ (?L1 ∪ ?L2) ∩ ?ENC"
proof (elim disjE)
assume "satisfies (w, I) φ⇩1"
with * have "x ∈ ?L1" using assms unfolding lang⇩W⇩S⇩1⇩S_def by (fastforce simp del: enc.simps)
with * show ?thesis by auto
next
assume "satisfies (w, I) φ⇩2"
with * have "x ∈?L2" using assms unfolding lang⇩W⇩S⇩1⇩S_def by (fastforce simp del: enc.simps)
with * show ?thesis by auto
qed
qed

lemma lang⇩W⇩S⇩1⇩S_FAnd:
assumes "wf_formula n (FAnd φ⇩1 φ⇩2)"
shows "lang⇩W⇩S⇩1⇩S n (FAnd φ⇩1 φ⇩2) ⊆
lang⇩W⇩S⇩1⇩S n φ⇩1 ∩ lang⇩W⇩S⇩1⇩S n φ⇩2 ∩ ⋃{enc (w, I) | w I. length I = n ∧ wf_interp_for_formula (w, I) (FAnd φ⇩1 φ⇩2)}"
using assms unfolding lang⇩W⇩S⇩1⇩S_def by (fastforce simp del: enc.simps)

subsection ‹From WS1S to Regular expressions›

fun rexp_of :: "nat ⇒ 'a formula ⇒ ('a atom) rexp" where
"rexp_of n (FQ a m) =
Inter (TIMES [rexp.Not Zero, Atom (AQ m a), rexp.Not Zero])
(ENC n (FOV (FQ a m)))"
| "rexp_of n (FLess m1 m2) = (if m1 = m2 then Zero else
Inter (TIMES [rexp.Not Zero, Atom (Arbitrary_Except m1 True),
rexp.Not Zero, Atom (Arbitrary_Except m2 True),
rexp.Not Zero]) (ENC n (FOV (FLess m1 m2 :: 'a formula))))"
| "rexp_of n (FIn m M) =
Inter (TIMES [rexp.Not Zero, Atom (Arbitrary_Except2 m M), rexp.Not Zero])
(ENC n (FOV (FIn m M :: 'a formula)))"
| "rexp_of n (FNot φ) = Inter (rexp.Not (rexp_of n φ)) (ENC n (FOV (FNot φ)))"
| "rexp_of n (FOr φ⇩1 φ⇩2) = Inter (Plus (rexp_of n φ⇩1) (rexp_of n φ⇩2)) (ENC n (FOV (FOr φ⇩1 φ⇩2)))"
| "rexp_of n (FAnd φ⇩1 φ⇩2) = INTERSECT [rexp_of n φ⇩1, rexp_of n φ⇩2, ENC n (FOV (FAnd φ⇩1 φ⇩2))]"
| "rexp_of n (FExists φ) = samequot_exec (any, replicate n False) (Pr (rexp_of (n + 1) φ))"
| "rexp_of n (FEXISTS φ) = samequot_exec (any, replicate n False) (Pr (rexp_of (n + 1) φ))"

fun rexp_of_alt :: "nat ⇒ 'a formula ⇒ ('a atom) rexp" where
"rexp_of_alt n (FQ a m) =
TIMES [rexp.Not Zero, Atom (AQ m a), rexp.Not Zero]"
| "rexp_of_alt n (FLess m1 m2) = (if m1 = m2 then Zero else
TIMES [rexp.Not Zero, Atom (Arbitrary_Except m1 True),
rexp.Not Zero, Atom (Arbitrary_Except m2 True),
rexp.Not Zero])"
| "rexp_of_alt n (FIn m M) =
TIMES [rexp.Not Zero, Atom (Arbitrary_Except2 m M), rexp.Not Zero]"
| "rexp_of_alt n (FNot φ) = rexp.Not (rexp_of_alt n φ)"
| "rexp_of_alt n (FOr φ⇩1 φ⇩2) = Plus (rexp_of_alt n φ⇩1) (rexp_of_alt n φ⇩2)"
| "rexp_of_alt n (FAnd φ⇩1 φ⇩2) = Inter (rexp_of_alt n φ⇩1) (rexp_of_alt n φ⇩2)"
| "rexp_of_alt n (FExists φ) = samequot_exec (any, replicate n False) (Pr (Inter (rexp_of_alt (n + 1) φ) (ENC (Suc n) (FOV φ))))"
| "rexp_of_alt n (FEXISTS φ) = samequot_exec (any, replicate n False) (Pr (Inter (rexp_of_alt (n + 1) φ) (ENC (Suc n) (FOV φ))))"

definition "rexp_of' n φ = Inter (rexp_of_alt n φ) (ENC n (FOV φ))"

fun rexp_of_alt' :: "nat ⇒ 'a formula ⇒ ('a atom) rexp" where
"rexp_of_alt' n (FQ a m) = TIMES [Full, Atom (AQ m a), Full]"
| "rexp_of_alt' n (FLess m1 m2) = (if m1 = m2 then Zero else
TIMES [Full, Atom (Arbitrary_Except m1 True), Full, Atom (Arbitrary_Except m2 True), Full])"
| "rexp_of_alt' n (FIn m M) = TIMES [Full, Atom (Arbitrary_Except2 m M), Full]"
| "rexp_of_alt' n (FNot φ) = rexp.Not (rexp_of_alt' n φ)"
| "rexp_of_alt' n (FOr φ⇩1 φ⇩2) = Plus (rexp_of_alt' n φ⇩1) (rexp_of_alt' n φ⇩2)"
| "rexp_of_alt' n (FAnd φ⇩1 φ⇩2) = Inter (rexp_of_alt' n φ⇩1) (rexp_of_alt' n φ⇩2)"
| "rexp_of_alt' n (FExists φ) = samequot_exec (any, replicate n False) (Pr (Inter (rexp_of_alt' (n + 1) φ) (ENC (n + 1) {0})))"
| "rexp_of_alt' n (FEXISTS φ) = samequot_exec (any, replicate n False) (Pr (rexp_of_alt' (n + 1) φ))"

definition "rexp_of'' n φ = Inter (rexp_of_alt' n φ) (ENC n (FOV φ))"

lemma enc_eqI:
assumes "x ∈ enc (w, I)" "x ∈ enc (w', I')" "wf_interp_for_formula (w, I) φ" "wf_interp_for_formula (w', I') φ"
"length I = length I'"
shows "enc (w, I) = enc (w', I')"
proof -
from assms have "stream_enc (w, I) = stream_enc (w', I')"
by (intro box_equals[OF _ stream_enc_enc[symmetric] stream_enc_enc[symmetric]]) auto
thus ?thesis using assms(5) by auto
qed

lemma enc_eq_welldef:
"⟦enc (w, I) = enc (w', I'); wf_formula (length I) φ; wf_interp_for_formula (w, I) φ ;wf_interp_for_formula (w', I') φ⟧ ⟹
(w, I) ⊨ φ ⟷ (w', I') ⊨ φ"
by (intro stream_enc_welldef) (auto simp del: stream_enc.simps intro!: enc_stream_enc)

lemma enc_welldef:
"⟦x ∈ enc (w, I); x ∈ enc (w', I'); length I = length I'; wf_formula (length I) φ;
wf_interp_for_formula (w, I) φ ;wf_interp_for_formula (w', I') φ⟧ ⟹
(w, I) ⊨ φ ⟷ (w', I') ⊨ φ"
by (intro enc_eq_welldef[OF enc_eqI])

lemma wf_rexp_of: "wf_formula n φ ⟹ wf n (rexp_of n φ)"
by (induct φ arbitrary: n)
(auto intro!: wf_samequot_exec wf_rexp_ENC,
auto simp: max_idx_vars finite_FOV)

theorem lang⇩W⇩S⇩1⇩S_rexp_of: "wf_formula n φ ⟹ lang⇩W⇩S⇩1⇩S n φ = lang n (rexp_of n φ)"
(is "_ ⟹ _ = ?L n φ")
proof (induct φ arbitrary: n)
case (FQ a m)
show ?case
proof (intro equalityI subsetI)
fix x assume "x ∈ lang⇩W⇩S⇩1⇩S n (FQ a m)"
then obtain w I where
*: "x ∈ enc (w, I)" "wf_interp_for_formula (w, I) (FQ a m)" "length I = n" "(w, I) ⊨ FQ a m"
unfolding lang⇩W⇩S⇩1⇩S_def by blast
hence x_alt: "x = map (case_prod (enc_atom I)) (zip [0 ..< length x] (stake (length x) (w @- sconst any)))"
by (intro encD) auto
from FQ(1) *(2,4) obtain p where p: "I ! m = Inl p"
by (auto simp: all_set_conv_all_nth split: sum.splits)
with FQ(1) * have p_less: "p < length x"
by (auto simp del: stream_enc.simps intro: trans_less_add1[OF less_length_cut_same_Inl])
hence enc_atom: "x ! p = enc_atom I p ((w @- sconst any) !! p)" (is "_ = enc_atom _ _ ?p")
by (subst x_alt, simp)
with *(1) p_less(1) have "x = take p x @ [enc_atom I p ?p] @ drop (p + 1) x"
using id_take_nth_drop[of p x] by auto
moreover
from *(2,3,4) FQ(1) p have "[enc_atom I p ?p] ∈ lang n (Atom (AQ m a))"
by (auto simp del: lang.simps intro!: enc_atom_lang_AQ)
moreover from *(2,3) have "take p x ∈ lang n (rexp.Not Zero)"
by (subst x_alt) (auto simp: in_set_zip shift_snth intro!: enc_atom_σ dest!: in_set_takeD)
moreover from *(2,3) have "drop (Suc p) x ∈ lang n (rexp.Not Zero)"
by (subst x_alt) (auto simp: in_set_zip shift_snth intro!: enc_atom_σ dest!: in_set_dropD)
ultimately show "x ∈ ?L n (FQ a m)" using *(1,2,3)
unfolding rexp_of.simps lang.simps(6,9) rexp_of_list.simps lang_ENC_formula[OF FQ]
by (auto elim: ssubst simp del: o_apply append.simps lang.simps enc.simps)
next
fix x let ?x = "x @- sconst (any, replicate n False)"
assume x: "x ∈ ?L n (FQ a m)"
with FQ obtain w I where
I: "x ∈ enc (w, I)" "length I = n" "wf_interp_for_formula (w, I) (FQ a m)"
unfolding rexp_of.simps lang.simps lang_ENC_formula[OF FQ] by fastforce
hence stream_enc: "stream_enc (w, I) = ?x" using stream_enc_enc by auto
from I FQ obtain p where m: "I ! m = Inl p" "m < length I" by (auto split: sum.splits)
with I have "wf_interp_for_formula (dec_word ?x, stream_dec n {m} ?x) (FQ a m)" unfolding I(1)
using enc_wf_interp[OF FQ(1)[folded I(2)]] by auto
moreover
from x obtain u1 u u2 where "x = u1 @ u @ u2" "u ∈ lang n (Atom (AQ m a))"
unfolding rexp_of.simps lang.simps rexp_of_list.simps using concE by fast
with FQ(1) obtain v where v: "x = u1 @ [v] @ u2" "snd v ! m" "fst v = a"
using AQ_D[of u n m a] by fastforce
from v have u: "length u1 < length x" by auto
{ from v have "snd (x ! length u1) ! m" by auto
moreover
from m I have "p < length x" "snd (x ! p) ! m" by (auto dest: enc_Inl simp del: enc.simps)
moreover
from m I have ex1: "∃!p. snd (stream_enc (w, I) !! p) ! m" by (intro stream_enc_unique) auto
ultimately have "p = length u1" unfolding stream_enc using u I(3) by auto
} note * = this
from v have "v = x ! length u1" by simp
with u have "?x !! length u1 = v" by (auto simp: shift_snth)
with * m I v(3) have "(dec_word ?x, stream_dec n {m} ?x) ⊨ FQ a m"
using stream_enc_enc[OF _ I(1), symmetric] less_length_cut_same[of w "any" "length u1" a]
by (auto simp del: enc.simps stream_enc.simps simp: dec_word_stream_enc dest!:
stream_dec_enc_Inl stream_dec_not_Inr split: sum.splits)
(auto simp: smap2_alt cut_same_def)
moreover from m I(2)
have stream_enc_dec: "stream_enc (dec_word (stream_enc (w, I)), stream_dec n {m} (stream_enc (w, I))) = stream_enc (w, I)"
by (intro stream_enc_dec)
(auto simp: smap2_alt sdrop_snth shift_snth intro: stream_enc_unique,
auto simp: smap2_szip stream.set_map)
moreover from I have "wf_word n x" unfolding wf_word by (auto elim: enc_set_σ simp del: enc.simps)
ultimately show "x ∈ lang⇩W⇩S⇩1⇩S n (FQ a m)" unfolding lang⇩W⇩S⇩1⇩S_def using m I(1,3)
by (auto simp del: enc.simps stream_enc.simps intro!: exI[of _ "enc (dec_word ?x, stream_dec n {m} ?x)"],
fastforce simp del: enc.simps stream_enc.simps,
auto simp del: stream_enc.simps simp: stream_enc[symmetric] I(2))
qed
next
case (FLess m m')
show ?case
proof (cases "m = m'")
case False
thus ?thesis
proof (intro equalityI subsetI)
fix x assume "x ∈ lang⇩W⇩S⇩1⇩S n (FLess m m')"
then obtain w I where
*: "x ∈ enc (w, I)" "wf_interp_for_formula (w, I) (FLess m m')" "length I = n" "(w, I) ⊨ FLess m m'"
unfolding lang⇩W⇩S⇩1⇩S_def by blast
hence x_alt: "x = map (case_prod (enc_atom I)) (zip [0 ..< length x] (stake (length x) (w @- sconst any)))"
by (intro encD) auto
from FLess(1) *(2,4) obtain p q where pq: "I ! m = Inl p" "I ! m' = Inl q" "p < q"
by (auto simp: all_set_conv_all_nth split: sum.splits)
with FLess(1) *(1,2,3) have pq_less: "p < length x" "q < length x"
by (auto simp del: stream_enc.simps intro!: trans_less_add1[OF less_length_cut_same_Inl])
hence enc_atom: "x ! p = enc_atom I p ((w @- sconst any) !! p)" (is "_ = enc_atom _ _ ?p")
"x ! q = enc_atom I q ((w @- sconst any) !! q)" (is "_ = enc_atom _ _ ?q") by (subst x_alt, simp)+
with *(1) pq_less(1) have "x = take p x @ [enc_atom I p ?p] @ drop (p + 1) x"
using id_take_nth_drop[of p x] by auto
also have "drop (p + 1) x = take (q - p - 1) (drop (p + 1) x) @
[enc_atom I q ?q] @ drop (q - p) (drop (p + 1) x)" (is "_ = ?LHS")
using id_take_nth_drop[of "q - p - 1" "drop (p + 1) x"] pq pq_less(2) enc_atom(2) by auto
finally have "x = take p x @ [enc_atom I p ?p] @ ?LHS" .
moreover from *(2,3) FLess(1) pq(1)
have "[enc_atom I p ?p] ∈ lang n (Atom (Arbitrary_Except m True))"
by (intro enc_atom_lang_Arbitrary_Except_True) (auto simp: shift_snth)
moreover from *(2,3) FLess(1) pq(2)
have "[enc_atom I q ?q] ∈ lang n (Atom (Arbitrary_Except m' True))"
by (intro enc_atom_lang_Arbitrary_Except_True) (auto simp: shift_snth)
moreover from *(2,3) have "take p x ∈ lang n (rexp.Not Zero)"
by (subst x_alt) (auto simp: in_set_zip shift_snth intro!: enc_atom_σ dest!: in_set_takeD)
moreover from *(2,3) have "take (q - p - 1) (drop (Suc p) x) ∈ lang n (rexp.Not Zero)"
by (subst x_alt) (auto simp: in_set_zip shift_snth intro!: enc_atom_σ dest!: in_set_dropD in_set_takeD)
moreover from *(2,3) have "drop (q - p) (drop (Suc p) x) ∈ lang n (rexp.Not Zero)"
by (subst x_alt) (auto simp: in_set_zip shift_snth intro!: enc_atom_σ dest!: in_set_dropD)
ultimately show "x ∈ ?L n (FLess m m')" using *(1,2,3)
unfolding rexp_of.simps lang.simps(6,9) rexp_of_list.simps Int_Diff lang_ENC_formula[OF FLess] if_not_P[OF False]
by (auto elim: ssubst simp del: o_apply append.simps lang.simps enc.simps)
next
fix x let ?x = "x @- sconst (any, replicate n False)"
assume x: "x ∈ ?L n (FLess m m')"
with FLess obtain w I where
I: "x ∈ enc (w, I)" "length I = n" "wf_interp_for_formula (w, I) (FLess m m')"
unfolding rexp_of.simps lang.simps lang_ENC_formula[OF FLess] if_not_P[OF False] by fastforce
hence stream_enc: "stream_enc (w, I) = x @- sconst (any, replicate n False)" using stream_enc_enc by auto
from I FLess obtain p p' where m: "I ! m = Inl p" "m < length I" "I ! m' = Inl p'" "m' < length I"
by (auto split: sum.splits)
with I have "wf_interp_for_formula (dec_word ?x, stream_dec n {m, m'} ?x) (FLess m m')" unfolding I(1)
using enc_wf_interp[OF FLess(1)[folded I(2)]] by auto
moreover
from x obtain u1 u u2 u' u3 where "x = u1 @ u @ u2 @ u' @ u3"
"u ∈ lang n (Atom (Arbitrary_Except m True))" "u' ∈ lang n (Atom (Arbitrary_Except m' True))"
unfolding rexp_of.simps lang.simps rexp_of_list.simps if_not_P[OF False] using concE by fast
with FLess(1) obtain v v' where v: "x = u1 @ [v] @ u2 @ [v'] @ u3"
"snd v ! m" "snd v' ! m'" "fst v ∈ set Σ" "fst v' ∈ set Σ"
using Arbitrary_ExceptD[of u n m True] Arbitrary_ExceptD[of u' n m' True]
by simp (auto simp: σ_def)
hence u: "length u1 < length x" and u': "Suc (length u1 + length u2) < length x" (is "?u' < _") by auto
{ from v have "snd (x ! length u1) ! m" by auto
moreover
from m I have "p < length x" "snd (x ! p) ! m" by (auto dest: enc_Inl simp del: enc.simps)
moreover
from m I have ex1: "∃!p. snd (stream_enc (w, I) !! p) ! m" by (intro stream_enc_unique) auto
ultimately have "p = length u1" unfolding stream_enc using u I(3) by auto
}
{ from v have "snd (x ! ?u') ! m'" by (auto simp: nth_append)
moreover
from m I have "p' < length x" "snd (x ! p') ! m'" by (auto dest: enc_Inl simp del: enc.simps)
moreover
from m I have ex1: "∃!p. snd (stream_enc (w, I) !! p) ! m'" unfolding I(1) by (intro stream_enc_unique) auto
ultimately have "p' = ?u'" unfolding stream_enc using u' I(3) by auto (metis shift_snth_less)
} note * = this ‹p = length u1›
with m I have "(dec_word ?x, stream_dec n {m, m'} ?x) ⊨ FLess m m'"
using stream_enc_enc[OF _ I(1), symmetric]
by (auto dest: stream_dec_not_Inr stream_dec_enc_Inl split: sum.splits simp del: stream_enc.simps)
moreover from m I(2)
have stream_enc_dec: "stream_enc (dec_word (stream_enc (w, I)), stream_dec n {m, m'} (stream_enc (w, I))) = stream_enc (w, I)"
by (intro stream_enc_dec)
(auto simp: smap2_alt sdrop_snth shift_snth intro: stream_enc_unique,
auto simp: smap2_szip stream.set_map)
moreover from I have "wf_word n x" unfolding wf_word by (auto elim: enc_set_σ simp del: enc.simps)
ultimately show "x ∈ lang⇩W⇩S⇩1⇩S n (FLess m m')" unfolding lang⇩W⇩S⇩1⇩S_def using m I(1,3)
by (auto simp del: enc.simps stream_enc.simps intro!: exI[of _ "enc (dec_word ?x, stream_dec n {m, m'} ?x)"],
fastforce simp del: enc.simps stream_enc.simps,
auto simp del: stream_enc.simps simp: stream_enc[symmetric] I(2))
qed
qed (simp add: lang⇩W⇩S⇩1⇩S_def del: o_apply)
next
case (FIn m M)
show ?case
proof (intro equalityI subsetI)
fix x assume "x ∈ lang⇩W⇩S⇩1⇩S n (FIn m M)"
then obtain w I where
*: "x ∈ enc (w, I)" "wf_interp_for_formula (w, I) (FIn m M)" "length I = n" "(w, I) ⊨ FIn m M"
unfolding lang⇩W⇩S⇩1⇩S_def by blast
hence x_alt: "x = map (case_prod (enc_atom I)) (zip [0 ..< length x] (stake (length x) (w @- sconst any)))"
by (intro encD) auto
from FIn(1) *(2,4) obtain p P where p: "I ! m = Inl p" "I ! M = Inr P" "p ∈ P"
by (auto simp: all_set_conv_all_nth split: sum.splits)
with FIn(1) *(1,2,3) have p_less: "p < length x" "∀p ∈ P. p < length x"
by (auto simp del: stream_enc.simps intro: trans_less_add1[OF less_length_cut_same_Inl]
hence enc_atom: "x ! p = enc_atom I p ((w @- sconst any) !! p)" (is "_ = enc_atom _ _ ?p")
"∀p ∈ P. x ! p = enc_atom I p ((w @- sconst any) !! p)" (is "Ball _ (λp. _ = enc_atom _ _ (?P p))")
by (subst x_alt, simp)+
with *(1) p_less(1) have "x = take p x @ [enc_atom I p ?p] @ drop (p + 1) x"
using id_take_nth_drop[of p x] by auto
moreover
from *(2,3) FIn(1) p have "[enc_atom I p ?p] ∈ lang n (Atom (Arbitrary_Except2 m M))"
by (intro enc_atom_lang_Arbitrary_Except2) (auto simp: shift_snth)
moreover from *(2,3) have "take p x ∈ lang n (rexp.Not Zero)"
by (subst x_alt) (auto simp: in_set_zip shift_snth intro!: enc_atom_σ dest!: in_set_takeD)
moreover from *(2,3) have "drop (Suc p) x ∈ lang n (rexp.Not Zero)"
by (subst x_alt) (auto simp: in_set_zip shift_snth intro!: enc_atom_σ dest!: in_set_dropD)
ultimately show "x ∈ ?L n (FIn m M)" using *(1,2,3)
unfolding rexp_of.simps lang.simps(6,9) rexp_of_list.simps Int_Diff lang_ENC_formula[OF FIn]
by (auto elim: ssubst simp del: o_apply append.simps lang.simps enc.simps)
next
fix x let ?x = "x @- sconst (any, replicate n False)"
assume x: "x ∈ ?L n (FIn m M)"
with FIn obtain w I where
I: "x ∈ enc (w, I)" "length I = n" "wf_interp_for_formula (w, I) (FIn m M)"
unfolding rexp_of.simps lang.simps lang_ENC_formula[OF FIn] by fastforce
hence stream_enc: "stream_enc (w, I) = ?x" using stream_enc_enc by auto
from I FIn obtain p P where m: "I ! m = Inl p" "m < length I" "I ! M = Inr P" "M < length I"
by (auto split: sum.splits)
with I have "wf_interp_for_formula (dec_word ?x, stream_dec n {m} ?x) (FIn m M)" unfolding I(1)
using enc_wf_interp[OF FIn(1)[folded I(2)]] by auto
moreover
from x obtain u1 u u2 where "x = u1 @ u @ u2"
"u ∈ lang n (Atom (Arbitrary_Except2 m M))"
unfolding rexp_of.simps lang.simps rexp_of_list.simps using concE by fast
with FIn(1) obtain v where v: "x = u1 @ [v] @ u2" "snd v ! m" "snd v ! M" and "fst v ∈ set Σ"
using Arbitrary_Except2D[of u n m M] by simp (auto simp: σ_def)
from v have u: "length u1 < length x" by auto
{ from v have "snd (x ! length u1) ! m" by auto
moreover
from m I have "p < length x" "snd (x ! p) ! m" by (auto dest: enc_Inl simp del: enc.simps)
moreover
from m I have ex1: "∃!p. snd (stream_enc (```