Theory M2L
section ‹M2L›
theory M2L
imports Formula
begin
subsection ‹Encodings›
context formula
begin
fun enc :: "'a interp ⇒ ('a × bool list) list" where
"enc (w, I) = map_index (enc_atom I) w"
abbreviation "wf_interp w I ≡ (length w > 0 ∧
(∀a ∈ set w. a ∈ set Σ) ∧
(∀x ∈ set I. case x of Inl p ⇒ p < length w | Inr P ⇒ ∀p ∈ P. p < length w))"
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 | _ ⇒ True))"
fun satisfies :: "'a interp ⇒ 'a formula ⇒ bool" (infix ‹⊨› 50) where
"(w, I) ⊨ FQ a m = (w ! (case I ! m of Inl p ⇒ p) = 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. p ∈ {0 .. length w - 1} ∧ (w, Inl p # I) ⊨ φ)"
| "(w, I) ⊨ (FEXISTS φ) = (∃P. P ⊆ {0 .. length w - 1} ∧ (w, Inr P # I) ⊨ φ)"
definition lang⇩M⇩2⇩L :: "nat ⇒ 'a formula ⇒ ('a × bool list) list set" where
"lang⇩M⇩2⇩L n φ = {enc (w, I) | w I.
length I = n ∧ wf_interp_for_formula (w, I) φ ∧ satisfies (w, I) φ}"
definition "dec_word ≡ map fst"
definition "positions_in_row w i =
Option.these (set (map_index (λp a_bs. if nth (snd a_bs) i then Some p else None) w))"
definition "dec_interp n FO (w :: ('a × bool list) list) ≡ map (λi.
if i ∈ FO
then Inl (the_elem (positions_in_row w i))
else Inr (positions_in_row w i)) [0..<n]"
lemma positions_in_row: "positions_in_row w i = {p. p < length w ∧ snd (w ! p) ! i}"
unfolding positions_in_row_def Option.these_def by (auto intro!: image_eqI[of _ the])
lemma positions_in_row_unique: "∃!p. p < length w ∧ snd (w ! p) ! i ⟹
the_elem (positions_in_row w i) = (THE p. p < length w ∧ snd (w ! p) ! i)"
by (rule the1I2) (auto simp: the_elem_def positions_in_row)
lemma positions_in_row_length: "∃!p. p < length w ∧ snd (w ! p) ! i ⟹
the_elem (positions_in_row w i) < length w"
unfolding positions_in_row_unique by (rule the1I2) auto
lemma dec_interp_Inl: "⟦i ∈ FO; i < n⟧ ⟹ ∃p. dec_interp n FO x ! i = Inl p"
unfolding dec_interp_def using nth_map[of n "[0..<n]"] by auto
lemma dec_interp_not_Inr: "⟦dec_interp n FO x ! i = Inr P; i ∈ FO; i < n⟧ ⟹ False"
unfolding dec_interp_def using nth_map[of n "[0..<n]"] by auto
lemma dec_interp_Inr: "⟦i ∉ FO; i < n⟧ ⟹ ∃P. dec_interp n FO x ! i = Inr P"
unfolding dec_interp_def using nth_map[of n "[0..<n]"] by auto
lemma dec_interp_not_Inl: "⟦dec_interp n FO x ! i = Inl p; i ∉ FO; i < n⟧ ⟹ False"
unfolding dec_interp_def using nth_map[of n "[0..<n]"] by auto
lemma Inl_dec_interp_length:
assumes "∀i ∈ FO. ∃!p. p < length w ∧ snd (w ! p) ! i"
shows "Inl p ∈ set (dec_interp n FO w) ⟹ p < length w"
unfolding dec_interp_def by (auto intro: positions_in_row_length[OF bspec[OF assms]])
lemma Inr_dec_interp_length: "⟦Inr P ∈ set (dec_interp n FO w); p ∈ P⟧ ⟹ p < length w"
unfolding dec_interp_def by (auto simp: positions_in_row)
lemma the_elem_Collect[simp]:
assumes "∃!x. P x"
shows "the_elem (Collect P) = (The P)"
proof (unfold the_elem_def, rule the_equality)
from assms have "P (The P)" by (rule theI')
with assms show "Collect P = {The P}" by auto
fix x assume "Collect P = {x}"
then show "x = The P" by (auto intro: the_equality[symmetric])
qed
lemma enc_atom_dec:
"⟦wf_word n w; ∀i ∈ FO. i < n ⟶ (∃!p. p < length w ∧ snd (w ! p) ! i); p < length w⟧ ⟹
enc_atom (dec_interp n FO w) p (fst (w ! p)) = w ! p"
unfolding wf_word dec_interp_def map_filter_def Let_def
by (auto 0 4 simp: comp_def σ_def set_n_lists positions_in_row dest: nth_mem[of p w]
intro!: trans[OF iffD2[OF prod.inject] prod.collapse] nth_equalityI the_equality[symmetric]
intro: the1I2[of "λp. p < length w ∧ snd (w ! p) ! i" "λp. snd (w ! p) ! i" for i]
elim!: contrapos_np[of _ False])
lemma enc_dec:
"⟦wf_word n w; ∀i ∈ FO. i < n ⟶ (∃!p. p < length w ∧ snd (w ! p) ! i)⟧ ⟹
enc (dec_word w, dec_interp n FO w) = w"
unfolding enc.simps dec_word_def
by (intro trans[OF map_index_map map_index_congL] allI impI enc_atom_dec) assumption+
lemma dec_word_enc: "dec_word (enc (w, I)) = w"
unfolding dec_word_def by auto
lemma enc_unique:
assumes "wf_interp w I" "i < length I"
shows "∃p. I ! i = Inl p ⟹ ∃!p. p < length (enc (w, I)) ∧ snd (enc (w, I) ! p) ! i"
proof (erule exE)
fix p assume "I ! i = Inl p"
with assms show ?thesis by (auto simp: map_index all_set_conv_all_nth intro!: exI[of _ p])
qed
lemma dec_interp_enc_Inl:
"⟦dec_interp n FO (enc (w, I)) ! i = Inl p'; I ! i = Inl p; i ∈ FO; i < n; length I = n; p < length w; wf_interp w I⟧ ⟹
p = p'"
unfolding dec_interp_def using nth_map[of _ "[0..<n]"] positions_in_row_unique[OF enc_unique]
by (auto intro: sym[OF the_equality])
lemma dec_interp_enc_Inr:
"⟦dec_interp n FO (enc (w, I)) ! i = Inr P'; I ! i = Inr P; i ∉ FO; i < n; length I = n; ∀p ∈ P. p < length w⟧ ⟹
P = P'"
unfolding dec_interp_def positions_in_row by auto
lemma length_dec_interp[simp]: "length (dec_interp n FO x) = n"
by (auto simp: dec_interp_def)
lemma nth_dec_interp[simp]: "i < n ⟹ dec_interp n {} x ! i = Inr (positions_in_row x i)"
by (auto simp: dec_interp_def)
lemma set_σD[simp]: "(a, bs) ∈ set (σ Σ n) ⟹ a ∈ set Σ"
unfolding σ_def by auto
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 (cases "FO = {}")
case True with assms show ?thesis
by (force simp: ENC_def dec_word_def wf_word
in_set_conv_nth[of _ "dec_interp n {} x" for x] positions_in_row Ball_def
intro!: enc_atom_σ exI[of _ "dec_word x :: 'a list" for x] exI[of _ "dec_interp n {} x" for x]
enc_dec[of n _ "{}", symmetric, unfolded dec_word_def enc.simps map_index_map])
next
case False
hence nonempty: "valid_ENC n ` FO ≠ {}" by simp
have finite: "finite (valid_ENC n ` FO)"
by (intro finite_imageI[OF finite_subset[OF assms(1)]]) auto
from False assms(1) have "0 < n" by auto
with wf_rexp_valid_ENC assms(1) have wf_rexp: "∀x ∈ valid_ENC n ` FO. wf n x" by auto
{ fix r w I assume "r ∈ FO" and *: "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)"
then obtain p where p: "I ! r = Inl p" by (cases "I ! r") auto
moreover from ‹r ∈ FO› assms(1) *(1) have "r < length I" by auto
ultimately have "Inl p ∈ set I" by (auto simp add: in_set_conv_nth)
with *(2) have "p < length w" by auto
with *(2) obtain a where a: "w ! p = a" "a ∈ set Σ" by auto
from ‹r < length I› p *(1) ‹a ∈ set Σ›
have "[enc_atom I p a] ∈ lang n (Atom (Arbitrary_Except r True))"
by (intro enc_atom_lang_Arbitrary_Except_True) auto
moreover
from ‹r < length I› p *(1) ‹a ∈ set Σ› *(2) ‹p < length w›
have "take p (enc (w, I)) ∈ star (lang n (Atom (Arbitrary_Except r False)))"
by (auto simp: in_set_conv_nth simp del: lang.simps
intro!: Ball_starI enc_atom_lang_Arbitrary_Except_False) auto
moreover
from ‹r < length I› p *(1) ‹a ∈ set Σ› *(2) ‹p < length w›
have "drop (Suc p) (enc (w, I)) ∈ star (lang n (Atom (Arbitrary_Except r False)))"
by (auto simp: in_set_conv_nth simp del: lang.simps
intro!: Ball_starI enc_atom_lang_Arbitrary_Except_False) auto
ultimately have "take p (enc (w, I)) @ [enc_atom I p a] @ drop (p + 1) (enc (w, I)) ∈
lang n (valid_ENC n r)" using ‹0 < n› unfolding valid_ENC_def by (auto simp del: append.simps)
with ‹p < length w› a have "enc (w, I) ∈ lang n (valid_ENC n r)"
using id_take_nth_drop[of p "enc (w, I)"] by auto
}
hence "?R ⊆ ?L" using lang_flatten_INTERSECT[OF finite nonempty wf_rexp] by (auto simp add: ENC_def)
moreover
{ fix x assume "x ∈ (⋂r ∈ valid_ENC n ` FO. lang n r)"
hence r: "∀r ∈ FO. x ∈ lang n (valid_ENC n r)" by blast
have "length (dec_interp n FO x) = n" unfolding dec_interp_def by simp
moreover
{ fix r assume "r ∈ FO"
with assms have "r < n" by auto
from ‹r ∈ FO› r obtain u v w where uvw: "x = u @ v @ w"
"u ∈ star (lang n (Atom (Arbitrary_Except r False)))"
"v ∈ lang n (Atom (Arbitrary_Except r True))"
"w ∈ star (lang n (Atom (Arbitrary_Except r False)))" using ‹0 < n› unfolding valid_ENC_def
by (fastforce simp del: lang.simps(4))
hence "length u < length x" "⋀i. i < length x ⟶ snd (x ! i) ! r ⟷ i = length u"
by (auto simp: nth_append nth_Cons' split: if_split_asm simp del: lang.simps
dest!: Arbitrary_ExceptD[OF _ ‹r < n›]
dest: star_Arbitrary_ExceptD[OF _ ‹r < n›, of u]
elim!: iffD1[OF star_Arbitrary_ExceptD[OF _ ‹r < n›, of w False]]) auto
hence "∃!p. p < length x ∧ snd (x ! p) ! r" by auto
} note * = this
have x_wf_word: "wf_word n x" using wf_lang_wf_word[OF wf_rexp_valid_ENC] False r assms(1)
by auto
with * have "x = enc (dec_word x, dec_interp n FO x)" by (intro sym[OF enc_dec]) auto
moreover
from * have "wf_interp (dec_word x) (dec_interp n FO x)"
"(∀i ∈ FO. case dec_interp n FO x ! i of Inl _ ⇒ True | Inr _ ⇒ False)"
"(∀i ∈ SO. case dec_interp n FO x ! i of Inl _ ⇒ False | Inr _ ⇒ True)"
using False x_wf_word[unfolded wf_word, unfolded σ_def o_apply set_concat set_map set_n_lists, simplified] assms
Inl_dec_interp_length[OF ballI, of FO x _ n] Inr_dec_interp_length[of _ n FO x]
dec_interp_Inl[of _ FO n x] dec_interp_Inr[of _ FO n x]
by (fastforce simp add: dec_word_def split: sum.split)+
ultimately have "x ∈ ?R" by blast
}
with False lang_flatten_INTERSECT[OF finite nonempty wf_rexp] have "?L ⊆ ?R" by (auto simp add: ENC_def)
ultimately show ?thesis by blast
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 enc_alt_def:
"enc (w, x # I) = map_index (λn (a, bs). (a, (case x of Inl p ⇒ n = p | Inr P ⇒ n ∈ P) # bs)) (enc (w, I))"
by (auto simp: comp_def)
lemma enc_extend_interp: "enc (w, I) = enc (w', I') ⟹ enc (w, x # I) = enc (w', x # I')"
unfolding enc_alt_def by auto
lemma wf_interp_for_formula_FExists:
"⟦wf_formula (length I) (FExists φ); w ≠ []⟧⟹
wf_interp_for_formula (w, I) (FExists φ) ⟷
(∀p < length w. 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 < length w. 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 φ); w ≠ []⟧⟹
wf_interp_for_formula (w, I) (FEXISTS φ) ⟷ (∀P ⊆ {0 .. length w - 1}. wf_interp_for_formula (w, Inr P # I) φ)"
by (auto simp: neq_Nil_conv nth_Cons')
lemma wf_interp_for_formula_any_Inr: "wf_interp_for_formula (w, Inr P # I) φ ⟹
∀P ⊆ {0 .. length w - 1}. wf_interp_for_formula (w, Inr P # I) φ"
by (cases w) (auto simp: nth_Cons' split: if_split_asm)
lemma enc_word_length: "enc (w, I) = enc (w', I') ⟹ length w = length w'"
by (auto elim: map_index_eq_imp_length_eq)
lemma enc_length:
assumes "w ≠ []" "enc (w, I) = enc (w', I')"
shows "length I = length I'"
using assms
length_map[of "(λx. case x of Inl p ⇒ 0 = p | Inr P ⇒ 0 ∈ P)" I]
length_map[of "(λx. case x of Inl p ⇒ 0 = p | Inr P ⇒ 0 ∈ P)" I']
by (induct rule: list_induct2[OF enc_word_length[OF assms(2)]]) auto
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:
assumes "wf_formula (length I) φ" "wf_interp_for_formula (w, I) φ"
shows "wf_interp_for_formula (dec_word (enc (w, I)), dec_interp (length I) (FOV φ) (enc (w, I))) φ"
(is "wf_interp_for_formula (_, ?dec) φ")
unfolding dec_word_enc
proof -
{ fix i assume i: "i ∈ FOV φ"
with assms(2) have "∃p. I ! i = Inl p" by (cases "I ! i") auto
with i assms have "∃!p. p < length (enc (w, I)) ∧ snd (enc (w, I) ! p) ! i"
by (intro enc_unique[of w I i]) (auto intro!: bspec[OF max_idx_vars] split: sum.splits)
} note * = this
have "∀x ∈ set ?dec. case_sum (λp. p < length w) (λP. ∀p∈P. p < length w) x"
proof (intro ballI, split sum.split, safe)
fix p assume "Inl p ∈ set ?dec"
thus "p < length w" using Inl_dec_interp_length[OF ballI[OF *]] by auto
next
fix p P assume "Inr P ∈ set ?dec" "p ∈ P"
thus "p < length w" using Inr_dec_interp_length by fastforce
qed
thus "wf_interp_for_formula (w, ?dec) φ"
using assms
dec_interp_Inl[of _ "FOV φ" "length I" "enc (w, I)", OF _ bspec[OF max_idx_vars]]
dec_interp_Inr[of _ "FOV φ" "length I" "enc (w, I)", OF _ bspec[OF max_idx_vars]]
by (fastforce split: sum.splits)
qed
lemma enc_welldef: "⟦enc (w, I) = enc (w', I'); wf_formula (length I) φ;
wf_interp_for_formula (w, I) φ; wf_interp_for_formula (w', I') φ⟧ ⟹
satisfies (w, I) φ ⟷ satisfies (w', I') φ"
proof (induction φ arbitrary: I I')
case (FQ a m)
let ?dec = "λw I. (dec_word (enc (w, I)), dec_interp (length I) (FOV (FQ a m)) (enc (w, I)))"
from FQ(2,3) have "satisfies (w, I) (FQ a m) = satisfies (?dec w I) (FQ a m)"
unfolding dec_word_enc
using dec_interp_enc_Inl[of "length I" "{m}" w I m]
by (auto intro: nth_mem dest: dec_interp_not_Inr split: sum.splits) (metis nth_mem)+
moreover
from FQ(3) have *: "w ≠ []" by simp
from FQ(2,4) have "satisfies (w', I') (FQ a m) = satisfies (?dec w' I') (FQ a m)"
unfolding dec_word_enc enc_length[OF * FQ(1)]
using dec_interp_enc_Inl[of "length I'" "{m}" w' I' m]
by (auto dest: dec_interp_not_Inr split: sum.splits) (metis nth_mem)+
ultimately show ?case unfolding FQ(1) enc_length[OF * FQ(1)] ..
next
case (FLess m n)
let ?dec = "λw I. (dec_word (enc (w, I)), dec_interp (length I) (FOV (FLess m n)) (enc (w, I)))"
from FLess(2,3) have "satisfies (w, I) (FLess m n) = satisfies (?dec (TYPE ('a)) w I) (FLess m n)"
unfolding dec_word_enc
using dec_interp_enc_Inl[of "length I" "{m, n}" w I m] dec_interp_enc_Inl[of "length I" "{m, n}" w I n]
by (fastforce intro: nth_mem dest: dec_interp_not_Inr split: sum.splits)
moreover
from FLess(3) have *: "w ≠ []" by simp
from FLess(2,4) have "satisfies (w', I') (FLess m n) = satisfies (?dec (TYPE ('a)) w' I') (FLess m n)"
unfolding dec_word_enc enc_length[OF * FLess(1)]
using dec_interp_enc_Inl[of "length I'" "{m, n}" w' I' m] dec_interp_enc_Inl[of "length I'" "{m, n}" w' I' n]
by (fastforce intro: nth_mem dest: dec_interp_not_Inr split: sum.splits)
ultimately show ?case unfolding FLess(1) enc_length[OF * FLess(1)] ..
next
case (FIn m M)
let ?dec = "λw I. (dec_word (enc (w, I)), dec_interp (length I) (FOV (FIn m M)) (enc (w, I)))"
from FIn(2,3) have "satisfies (w, I) (FIn m M) = satisfies (?dec (TYPE ('a)) w I) (FIn m M)"
unfolding dec_word_enc
using dec_interp_enc_Inl[of "length I" "{m}" w I m] dec_interp_enc_Inr[of "length I" "{m}" w I M]
by (auto dest: dec_interp_not_Inr dec_interp_not_Inl split: sum.splits) (metis nth_mem)+
moreover
from FIn(3) have *: "w ≠ []" by simp
from FIn(2,4) have "satisfies (w', I') (FIn m M) = satisfies (?dec (TYPE ('a)) w' I') (FIn m M)"
unfolding dec_word_enc enc_length[OF * FIn(1)]
using dec_interp_enc_Inl[of "length I'" "{m}" w' I' m] dec_interp_enc_Inr[of "length I'" "{m}" w' I' M]
by (auto dest: dec_interp_not_Inr dec_interp_not_Inl split: sum.splits) (metis nth_mem)+
ultimately show ?case unfolding FIn(1) enc_length[OF * FIn(1)] ..
next
case (FOr φ1 φ2) show ?case unfolding satisfies.simps(5)
proof (intro disj_cong)
from FOr(3-6) show "satisfies (w, I) φ1 = satisfies (w', I') φ1"
by (intro FOr(1)) auto
next
from FOr(3-6) show "satisfies (w, I) φ2 = satisfies (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 "satisfies (w, I) φ1 = satisfies (w', I') φ1"
by (intro FAnd(1)) auto
next
from FAnd(3-6) show "satisfies (w, I) φ2 = satisfies (w', I') φ2"
by (intro FAnd(2)) auto
qed
next
case (FExists φ)
hence "w ≠ []" "w' ≠ []" by auto
hence length: "length w = length w'" "length I = length I'"
using enc_word_length[OF FExists.prems(1)] enc_length[OF _ FExists.prems(1)] by auto
show ?case
proof
assume "satisfies (w, I) (FExists φ)"
with FExists.prems(3) obtain p where "p < length w" "satisfies (w, Inl p # I) φ"
by (auto intro: ord_less_eq_trans[OF le_imp_less_Suc Suc_pred])
moreover
with FExists.prems have "satisfies (w', Inl p # I') φ"
proof (intro iffD1[OF FExists.IH[of "Inl p # I" "Inl p # I'"]])
from FExists.prems(2,3) ‹p < length w› show "wf_interp_for_formula (w, Inl p # I) φ"
by (blast dest: wf_interp_for_formula_FExists[of I, OF _ ‹w ≠ []›])
next
from FExists.prems(2,4) ‹p < length w› show "wf_interp_for_formula (w', Inl p # I') φ"
unfolding length by (blast dest: wf_interp_for_formula_FExists[of I', OF _ ‹w' ≠ []›])
qed (auto elim: enc_extend_interp simp del: enc.simps)
ultimately show "satisfies (w', I') (FExists φ)" using length by (auto intro!: exI[of _ p])
next
assume "satisfies (w', I') (FExists φ)"
with FExists.prems(1,2,4) obtain p where "p < length w'" "satisfies (w', Inl p # I') φ"
by (auto intro: ord_less_eq_trans[OF le_imp_less_Suc Suc_pred])
moreover
with FExists.prems have "satisfies (w, Inl p # I) φ"
proof (intro iffD2[OF FExists.IH[of "Inl p # I" "Inl p # I'"]])
from FExists.prems(2,3) ‹p < length w'› show "wf_interp_for_formula (w, Inl p # I) φ"
unfolding length[symmetric] by (blast dest: wf_interp_for_formula_FExists[of I, OF _ ‹w ≠ []›])
next
from FExists.prems(2,4) ‹p < length w'› show "wf_interp_for_formula (w', Inl p # I') φ"
unfolding length by (blast dest: wf_interp_for_formula_FExists[of I', OF _ ‹w' ≠ []›])
qed (auto elim: enc_extend_interp simp del: enc.simps)
ultimately show "satisfies (w, I) (FExists φ)" using length by (auto intro!: exI[of _ p])
qed
next
case (FEXISTS φ)
hence "w ≠ []" "w' ≠ []" by auto
hence length: "length w = length w'" "length I = length I'"
using enc_word_length[OF FEXISTS.prems(1)] enc_length[OF _ FEXISTS.prems(1)] by auto
show ?case
proof
assume "satisfies (w, I) (FEXISTS φ)"
then obtain P where P: "P ⊆ {0 .. length w - 1}" "satisfies (w, Inr P # I) φ" by auto
moreover
with FEXISTS.prems have "satisfies (w', Inr P # I') φ"
proof (intro iffD1[OF FEXISTS.IH[of "Inr P # I" "Inr P # I'"]])
from FEXISTS.prems(2,3) P(1) show "wf_interp_for_formula (w, Inr P # I) φ"
by (blast dest: wf_interp_for_formula_FEXISTS[of I, OF _ ‹w ≠ []›])
next
from FEXISTS.prems(2,4) P(1) show "wf_interp_for_formula (w', Inr P # I') φ"
unfolding length by (blast dest: wf_interp_for_formula_FEXISTS[of I', OF _ ‹w' ≠ []›])
qed (auto elim: enc_extend_interp simp del: enc.simps)
ultimately show "satisfies (w', I') (FEXISTS φ)" using length by (auto intro!: exI[of _ P])
next
assume "satisfies (w', I') (FEXISTS φ)"
then obtain P where P: "P ⊆ {0 .. length w' - 1}" "satisfies (w', Inr P # I') φ" by auto
moreover
with FEXISTS.prems have "satisfies (w, Inr P # I) φ"
proof (intro iffD2[OF FEXISTS.IH[of "Inr P # I" "Inr P # I'"]])
from FEXISTS.prems(2,3) P(1) show "wf_interp_for_formula (w, Inr P # I) φ"
unfolding length[symmetric] by (blast dest: wf_interp_for_formula_FEXISTS[of I, OF _ ‹w ≠ []›])
next
from FEXISTS.prems(2,4) P(1) show "wf_interp_for_formula (w', Inr P # I') φ"
unfolding length by (blast dest: wf_interp_for_formula_FEXISTS[of I', OF _ ‹w' ≠ []›])
qed (auto elim: enc_extend_interp simp del: enc.simps)
ultimately show "satisfies (w, I) (FEXISTS φ)" using length by (auto intro!: exI[of _ P])
qed
qed auto
lemma lang⇩M⇩2⇩L_FOr:
assumes "wf_formula n (FOr φ⇩1 φ⇩2)"
shows "lang⇩M⇩2⇩L n (FOr φ⇩1 φ⇩2) ⊆
(lang⇩M⇩2⇩L n φ⇩1 ∪ lang⇩M⇩2⇩L 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⇩M⇩2⇩L 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" "length w > 0" and
"satisfies (w, I) φ⇩1 ∨ satisfies (w, I) φ⇩2" unfolding lang⇩M⇩2⇩L_def by auto
thus "x ∈ (?L1 ∪ ?L2) ∩ ?ENC"
proof (elim disjE)
assume "satisfies (w, I) φ⇩1"
with * have "x ∈ ?L1" using assms unfolding lang⇩M⇩2⇩L_def by (fastforce)
with * show ?thesis by auto
next
assume "satisfies (w, I) φ⇩2"
with * have "x ∈?L2" using assms unfolding lang⇩M⇩2⇩L_def by (fastforce)
with * show ?thesis by auto
qed
qed
lemma lang⇩M⇩2⇩L_FAnd:
assumes "wf_formula n (FAnd φ⇩1 φ⇩2)"
shows "lang⇩M⇩2⇩L n (FAnd φ⇩1 φ⇩2) ⊆
lang⇩M⇩2⇩L n φ⇩1 ∩ lang⇩M⇩2⇩L n φ⇩2 ∩ {enc (w, I) | w I. length I = n ∧ wf_interp_for_formula (w, I) (FAnd φ⇩1 φ⇩2)}"
(is "_ ⊆ ?L1 ∩ ?L2 ∩ ?ENC")
using assms unfolding lang⇩M⇩2⇩L_def by (fastforce)
subsection ‹From M2L to Regular expressions›
fun rexp_of :: "nat ⇒ 'a formula ⇒ ('a atom) rexp" where
"rexp_of n (FQ a m) = Inter (TIMES [Full, Atom (AQ m a), Full]) (ENC n {m})"
| "rexp_of n (FLess m1 m2) = (if m1 = m2 then Zero else Inter
(TIMES [Full, Atom (Arbitrary_Except m1 True), Full, Atom (Arbitrary_Except m2 True), Full])
(ENC n {m1, m2}))"
| "rexp_of n (FIn m M) =
Inter (TIMES [Full, Atom (Arbitrary_Except2 m M), Full]) (ENC n {m})"
| "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 φ) = Pr (rexp_of (n + 1) φ)"
| "rexp_of n (FEXISTS φ) = Pr (rexp_of (n + 1) φ)"
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 φ) = Pr (Inter (rexp_of_alt (n + 1) φ) (ENC (n + 1) (FOV φ)))"
| "rexp_of_alt n (FEXISTS φ) = Pr (Inter (rexp_of_alt (n + 1) φ) (ENC (n + 1) (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 φ) = Pr (Inter (rexp_of_alt' (n + 1) φ) (ENC (n + 1) {0}))"
| "rexp_of_alt' n (FEXISTS φ) = Pr (rexp_of_alt' (n + 1) φ)"
definition "rexp_of'' n φ = Inter (rexp_of_alt' n φ) (ENC n (FOV φ))"
theorem lang⇩M⇩2⇩L_rexp_of: "wf_formula n φ ⟹ lang⇩M⇩2⇩L 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⇩M⇩2⇩L n (FQ a m)"
then obtain w I where
*: "x = enc (w, I)" "wf_interp_for_formula (w, I) (FQ a m)" "satisfies (w, I) (FQ a m)"
"length I = n"
unfolding lang⇩M⇩2⇩L_def by blast
with FQ(1) obtain p where p: "p < length w" "I ! m = Inl p" "w ! p = a"
by (auto simp: all_set_conv_all_nth split: sum.splits)
with *(1) have "x = take p (enc (w, I)) @ [enc_atom I p a] @ drop (p + 1) (enc (w, I))"
using id_take_nth_drop[of p "enc (w, I)"] by auto
moreover from *(4) FQ(1) p(2)
have "[enc_atom I p a] ∈ lang n (Atom (AQ m a))"
by (intro enc_atom_lang_AQ) auto
moreover from *(2,4) have "take p (enc (w, I)) ∈ lang n (Full)"
by (auto intro!: enc_atom_σ dest!: in_set_takeD)
moreover from *(2,4) have "drop (Suc p) (enc (w, I)) ∈ lang n (Full)"
by (auto intro!: enc_atom_σ dest!: in_set_dropD)
ultimately show "x ∈ ?L n (FQ a m)" using *(1,2,4)
unfolding rexp_of.simps lang.simps(6,9) rexp_of_list.simps Int_Diff
lang_ENC_formula[OF FQ, unfolded FOV.simps]
by (auto elim: ssubst simp del: o_apply append.simps lang.simps)
next
fix x assume x: "x ∈ ?L n (FQ a m)"
with FQ obtain w I p where m: "I ! m = Inl p" "m < length I" and
wI: "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, unfolded FOV.simps] Int_Diff
by atomize_elim (auto split: sum.splits)
hence "wf_interp_for_formula (dec_word x, dec_interp n {m} x) (FQ a m)" unfolding wI(1)
using enc_wf_interp[OF FQ(1)[folded wI(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
hence u: "length u1 < length x" by auto
{ from v have "snd (x ! length u1) ! m" by auto
moreover
from m wI have "p < length x" "snd (x ! p) ! m"
by (fastforce intro: nth_mem split: sum.splits)+
moreover
from m wI have ex1: "∃!p. p < length x ∧ snd (x ! p) ! m" unfolding wI(1) by (intro enc_unique) auto
ultimately have "p = length u1" using u by auto
} note * = this
from v have "v = enc (w, I) ! length u1" unfolding wI(1) by simp
hence "a = w ! length u1" using nth_map[OF u, of fst] unfolding wI(1) v(3)[symmetric] by auto
with * m wI have "satisfies (dec_word x, dec_interp n {m} x) (FQ a m)"
unfolding dec_word_enc[of w I, folded wI(1)]
by (auto simp del: enc.simps dest: dec_interp_not_Inr split: sum.splits)
(fastforce dest!: dec_interp_enc_Inl intro: nth_mem split: sum.splits)
moreover from wI have "wf_word n x" unfolding wf_word by (auto intro!: enc_atom_σ)
ultimately show "x ∈ lang⇩M⇩2⇩L n (FQ a m)" unfolding lang⇩M⇩2⇩L_def using m wI(3)
by (auto simp del: enc.simps intro!: exI[of _ "dec_word x"] exI[of _ "dec_interp n {m} x"]
intro: sym[OF enc_dec[OF _ ballI[OF impI[OF enc_unique[of w I, folded wI(1)]]]]])
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⇩M⇩2⇩L n (FLess m m')"
then obtain w I where
*: "x = enc (w, I)" "wf_interp_for_formula (w, I) (FLess m m')" "satisfies (w, I) (FLess m m')"
"length I = n"
unfolding lang⇩M⇩2⇩L_def by blast
with FLess(1) obtain p q where pq: "p < length w" "I ! m = Inl p" "q < length w" "I ! m' = Inl q" "p < q"
by (auto simp: all_set_conv_all_nth split: sum.splits)
with *(1) have "x = take p (enc (w, I)) @ [enc_atom I p (w ! p)] @ drop (p + 1) (enc (w, I))"
using id_take_nth_drop[of p "enc (w, I)"] by auto
also have "drop (p + 1) (enc (w, I)) = take (q - p - 1) (drop (p + 1) (enc (w, I))) @
[enc_atom I q (w ! q)] @ drop (q - p) (drop (p + 1) (enc (w, I)))" (is "_ = ?LHS")
using id_take_nth_drop[of "q - p - 1" "drop (p + 1) (enc (w, I))"] pq by auto
finally have "x = take p (enc (w, I)) @ [enc_atom I p (w ! p)] @ ?LHS" .
moreover from *(2,4) FLess(1) pq(1,2)
have "[enc_atom I p (w ! p)] ∈ lang n (Atom (Arbitrary_Except m True))"
by (intro enc_atom_lang_Arbitrary_Except_True) auto
moreover from *(2,4) FLess(1) pq(3,4)
have "[enc_atom I q (w ! q)] ∈ lang n (Atom (Arbitrary_Except m' True))"
by (intro enc_atom_lang_Arbitrary_Except_True) auto
moreover from *(2,4) have "take p (enc (w, I)) ∈ lang n (Full)"
by (auto intro!: enc_atom_σ dest!: in_set_takeD)
moreover from *(2,4) have "take (q - p - 1) (drop (Suc p) (enc (w, I))) ∈ lang n (Full)"
by (auto intro!: enc_atom_σ dest!: in_set_dropD in_set_takeD)
moreover from *(2,4) have "drop (q - p) (drop (Suc p) (enc (w, I))) ∈ lang n (Full)"
by (auto intro!: enc_atom_σ dest!: in_set_dropD)
ultimately show "x ∈ ?L n (FLess m m')" using *(1,2,4)
unfolding rexp_of.simps lang.simps(6,9) rexp_of_list.simps Int_Diff
lang_ENC_formula[OF FLess, unfolded FOV.simps] if_not_P[OF False]
by (auto elim: ssubst simp del: o_apply append.simps lang.simps)
next
fix x assume x: "x ∈ ?L n (FLess m m')"
with FLess obtain w I where
wI: "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, unfolded FOV.simps] Int_Diff
if_not_P[OF False]
by (fastforce split: sum.splits)
with 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 wI have "wf_interp_for_formula (dec_word x, dec_interp n {m, m'} x) (FLess m m')" unfolding wI(1)
using enc_wf_interp[OF FLess(1)[folded wI(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'"
using Arbitrary_ExceptD[of u n m True] Arbitrary_ExceptD[of u' n m' True] by fastforce
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 wI have "p < length x" "snd (x ! p) ! m"
by (fastforce intro: nth_mem split: sum.splits)+
moreover
from m wI have ex1: "∃!p. p < length x ∧ snd (x ! p) ! m" unfolding wI(1) by (intro enc_unique) auto
ultimately have "p = length u1" using u by auto
}
{ from v have "snd (x ! ?u') ! m'" by (auto simp: nth_append)
moreover
from m wI have "p' < length x" "snd (x ! p') ! m'"
by (fastforce intro: nth_mem split: sum.splits)+
moreover
from m wI have ex1: "∃!p. p < length x ∧ snd (x ! p) ! m'" unfolding wI(1) by (intro enc_unique) auto
ultimately have "p' = ?u'" using u' by auto
} note * = this ‹p = length u1›
with * m wI have "satisfies (dec_word x, dec_interp n {m, m'} x) (FLess m m')"
unfolding dec_word_enc[of w I, folded wI(1)]
by (auto simp del: enc.simps dest: dec_interp_not_Inr split: sum.splits)
(fastforce dest!: dec_interp_enc_Inl intro: nth_mem split: sum.splits)
moreover from wI have "wf_word n x" unfolding wf_word by (auto intro!: enc_atom_σ)
ultimately show "x ∈ lang⇩M⇩2⇩L n (FLess m m')" unfolding lang⇩M⇩2⇩L_def using m wI(3)
by (auto simp del: enc.simps intro!: exI[of _ "dec_word x"] exI[of _ "dec_interp n {m, m'} x"]
intro: sym[OF enc_dec[OF _ ballI[OF impI[OF enc_unique[of w I, folded wI(1)]]]]])
qed
qed (simp add: lang⇩M⇩2⇩L_def del: o_apply)
next
case (FIn m M)
show ?case
proof (intro equalityI subsetI)
fix x assume "x ∈ lang⇩M⇩2⇩L n (FIn m M)"
then obtain w I where
*: "x = enc (w, I)" "wf_interp_for_formula (w, I) (FIn m M)" "satisfies (w, I) (FIn m M)"
"length I = n"
unfolding lang⇩M⇩2⇩L_def by blast
with FIn(1) obtain p P where p: "p < length w" "I ! m = Inl p" "I ! M = Inr P" "p ∈ P"
by (auto simp: all_set_conv_all_nth split: sum.splits)
with *(1) have "x = take p (enc (w, I)) @ [enc_atom I p (w ! p)] @ drop (p + 1) (enc (w, I))"
using id_take_nth_drop[of p "enc (w, I)"] by auto
moreover
from *(2,4) FIn(1) p have "[enc_atom I p (w ! p)] ∈ lang n (Atom (Arbitrary_Except2 m M))"
by (intro enc_atom_lang_Arbitrary_Except2) auto
moreover from *(2,4) have "take p (enc (w, I)) ∈ lang n (Full)"
by (auto intro!: enc_atom_σ dest!: in_set_takeD)
moreover from *(2,4) have "drop (Suc p) (enc (w, I)) ∈ lang n (Full)"
by (auto intro!: enc_atom_σ dest!: in_set_dropD)
ultimately show "x ∈ ?L n (FIn m M)" using *(1,2,4)
unfolding rexp_of.simps lang.simps(6,9) rexp_of_list.simps Int_Diff
lang_ENC_formula[OF FIn, unfolded FOV.simps]
by (auto elim: ssubst simp del: o_apply append.simps lang.simps)
next
fix x assume x: "x ∈ ?L n (FIn m M)"
with FIn obtain w I where wI: "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, unfolded FOV.simps] Int_Diff
by (fastforce split: sum.splits)
with 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 wI have "wf_interp_for_formula (dec_word x, dec_interp n {m} x) (FIn m M)" unfolding wI(1)
using enc_wf_interp[OF FIn(1)[folded wI(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"
using Arbitrary_Except2D[of u n m M] 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 wI have "p < length x" "snd (x ! p) ! m"
by (fastforce intro: nth_mem split: sum.splits)+
moreover
from m wI have ex1: "∃!p. p < length x ∧ snd (x ! p) ! m" unfolding wI(1) by (intro enc_unique) auto
ultimately have "p = length u1" using u by auto
} note * = this
from v have "v = enc (w, I) ! length u1" unfolding wI(1) by simp
with v(3) m(3,4) u wI(1) have "length u1 ∈ P" by auto
with * m wI have "satisfies (dec_word x, dec_interp n {m} x) (FIn m M)"
unfolding dec_word_enc[of w I, folded wI(1)]
by (auto simp del: enc.simps dest: dec_interp_not_Inr dec_interp_not_Inl split: sum.splits)
(auto simp del: enc.simps dest!: dec_interp_enc_Inl dec_interp_enc_Inr dest: nth_mem split: sum.splits)
moreover from wI have "wf_word n x" unfolding wf_word by (auto intro!: enc_atom_σ)
ultimately show "x ∈ lang⇩M⇩2⇩L n (FIn m M)" unfolding lang⇩M⇩2⇩L_def using m wI(3)
by (auto simp del: enc.simps intro!: exI[of _ "dec_word x"] exI[of _ "dec_interp n {m} x"]
intro: sym[OF enc_dec[OF _ ballI[OF impI[OF enc_unique[of w I, folded wI(1)]]]]])
qed
next
case (FOr φ⇩1 φ⇩2)
from FOr(3) have IH1: "lang⇩M⇩2⇩L n φ⇩1 = lang n (rexp_of n φ⇩1) - {[]}"
by (intro FOr(1)) auto
from FOr(3) have IH2: "lang⇩M⇩2⇩L n φ⇩2 = lang n (rexp_of n φ⇩2) - {[]}"
by (intro FOr(2)) auto
show ?case
proof (intro equalityI subsetI)
fix x assume "x ∈ lang⇩M⇩2⇩L n (FOr φ⇩1 φ⇩2)" thus "x ∈ lang n (rexp_of n (FOr φ⇩1 φ⇩2)) - {[]}"
using lang⇩M⇩2⇩L_FOr[OF FOr(3)] unfolding lang_ENC_formula[OF FOr(3)] rexp_of.simps lang.simps
IH1 IH2 Int_Diff by auto
next
fix x assume "x ∈ lang n (rexp_of n (FOr φ⇩1 φ⇩2)) - {[]}"
then obtain w I where or: "x ∈ lang⇩M⇩2⇩L n φ⇩1 ∨ x ∈ lang⇩M⇩2⇩L n φ⇩2" and wI: "x = enc (w, I)" "length I = n"
"wf_interp_for_formula (w, I) (FOr φ⇩1 φ⇩2)"
unfolding lang_ENC_formula[OF FOr(3)] rexp_of.simps lang.simps IH1 IH2 Int_Diff by auto
have "satisfies (w, I) φ⇩1 ∨ satisfies (w, I) φ⇩2"
proof (intro mp[OF disj_mono[OF impI impI] or])
assume "x ∈ lang⇩M⇩2⇩L n φ⇩1"
with wI(2,3) FOr(3) show "satisfies (w, I) φ⇩1"
unfolding lang⇩M⇩2⇩L_def wI(1) wf_interp_for_formula_FOr
by (auto simp del: enc.simps dest!: iffD2[OF enc_welldef[of _ _ _ _ φ⇩1]])
next
assume "x ∈ lang⇩M⇩2⇩L n φ⇩2"
with wI(2,3) FOr(3) show "satisfies (w, I) φ⇩2"
unfolding lang⇩M⇩2⇩L_def wI(1) wf_interp_for_formula_FOr
by (auto simp del: enc.simps dest!: iffD2[OF enc_welldef[of _ _ _ _ φ⇩2]])
qed
with wI show "x ∈ lang⇩M⇩2⇩L n (FOr φ⇩1 φ⇩2)" unfolding lang⇩M⇩2⇩L_def by auto
qed
next
case (FAnd φ⇩1 φ⇩2)
from FAnd(3) have IH1: "lang⇩M⇩2⇩L n φ⇩1 = lang n (rexp_of n φ⇩1) - {[]}"
by (intro FAnd(1)) auto
from FAnd(3) have IH2: "lang⇩M⇩2⇩L n φ⇩2 = lang n (rexp_of n φ⇩2) - {[]}"
by (intro FAnd(2)) auto
show ?case
proof (intro equalityI subsetI)
fix x assume "x ∈ lang⇩M⇩2⇩L n (FAnd φ⇩1 φ⇩2)" thus "x ∈ lang n (rexp_of n (FAnd φ⇩1 φ⇩2)) - {[]}"
using lang⇩M⇩2⇩L_FAnd[OF FAnd(3)] unfolding lang_ENC_formula[OF FAnd(3)] rexp_of.simps
rexp_of_list.simps lang.simps IH1 IH2 Int_Diff by auto
next
fix x assume "x ∈ lang n (rexp_of n (FAnd φ⇩1 φ⇩2)) - {[]}"
then obtain w I where "and": "x ∈ lang⇩M⇩2⇩L n φ⇩1 ∧ x ∈ lang⇩M⇩2⇩L n φ⇩2" and wI: "x = enc (w, I)" "length I = n"
"wf_interp_for_formula (w, I) (FAnd φ⇩1 φ⇩2)"
unfolding lang_ENC_formula[OF FAnd(3)] rexp_of.simps rexp_of_list.simps lang.simps IH1 IH2
Int_Diff by auto
have "satisfies (w, I) φ⇩1 ∧ satisfies (w, I) φ⇩2"
proof (intro mp[OF conj_mono[OF impI impI] "and"])
assume "x ∈ lang⇩M⇩2⇩L n φ⇩1"
with wI(2,3) FAnd(3) show "satisfies (w, I) φ⇩1"
unfolding lang⇩M⇩2⇩L_def wI(1) wf_interp_for_formula_FAnd
by (auto simp del: enc.simps dest!: iffD2[OF enc_welldef[of _ _ _ _ φ⇩1]])
next
assume "x ∈ lang⇩M⇩2⇩L n φ⇩2"
with wI(2,3) FAnd(3) show "satisfies (w, I) φ⇩2"
unfolding lang⇩M⇩2⇩L_def wI(1) wf_interp_for_formula_FAnd
by (auto simp del: enc.simps dest!: iffD2[OF enc_welldef[of _ _ _ _ φ⇩2]])
qed
with wI show "x ∈ lang⇩M⇩2⇩L n (FAnd φ⇩1 φ⇩2)" unfolding lang⇩M⇩2⇩L_def by auto
qed
next
case (FNot φ)
hence IH: "?L n φ = lang⇩M⇩2⇩L n φ" by simp
show ?case
proof (intro equalityI subsetI)
fix x assume "x ∈ lang⇩M⇩2⇩L n (FNot φ)"
then obtain w I where
*: "x = enc (w, I)" "wf_interp_for_formula (w, I) φ" "length I = n" "length w > 0"
and unsat: "¬ (satisfies (w, I) φ)"
unfolding lang⇩M⇩2⇩L_def by auto
{ assume "x ∈ ?L n φ"
with IH have "satisfies (w, I) φ" using enc_welldef[of _ _ w I φ, OF _ _ _ *(2)] FNot(2)
unfolding *(1,3) lang⇩M⇩2⇩L_def by auto
}
with unsat have "x ∉ ?L n φ" by blast
with * show "x ∈ ?L n (FNot φ)" unfolding rexp_of.simps lang.simps
using lang_ENC_formula[OF FNot(2)] by (auto simp: comp_def intro!: enc_atom_σ)
next
fix x assume "x ∈ ?L n (FNot φ)"
with IH have "x ∈ lang n (ENC n (FOV (FNot φ))) - {[]}" and x: "x ∉ lang⇩M⇩2⇩L n φ" by (auto simp del: o_apply)
then obtain w I where *: "x = enc (w, I)" "wf_interp_for_formula (w, I) (FNot φ)" "length I = n"
unfolding lang_ENC_formula[OF FNot(2)] by blast
{ assume "¬ satisfies (w, I) (FNot φ)"
with * have "x ∈ lang⇩M⇩2⇩L n φ" unfolding lang⇩M⇩2⇩L_def by auto
}
with x * show "x ∈ lang⇩M⇩2⇩L n (FNot φ)" unfolding lang⇩M⇩2⇩L_def by blast
qed
next
case (FExists φ)
show ?case
proof (intro equalityI subsetI)
fix x assume "x ∈ lang⇩M⇩2⇩L n (FExists φ)"
then obtain w I p where
*: "x = enc (w, I)" "wf_interp_for_formula (w, I) (FExists φ)"
"length I = n" "length w > 0" "p ∈ {0 .. length w - 1}" "satisfies (w, Inl p # I) φ"
unfolding lang⇩M⇩2⇩L_def by auto
with FExists(2) have "enc (w, Inl p # I) ∈ ?L (Suc n) φ"
by (intro subsetD[OF equalityD1[OF FExists(1)], of "Suc n" "enc (w, Inl p # I)"])
(auto simp: lang⇩M⇩2⇩L_def nth_Cons' ord_less_eq_trans[OF le_imp_less_Suc Suc_pred[OF *(4)]]
split: if_split_asm sum.splits intro!: exI[of _ w] exI[of _ "Inl p # I"])
with *(1) show "x ∈ ?L n (FExists φ)"
by (auto simp: map_index intro!: image_eqI[of _ "map π"] simp del: o_apply) (auto simp: π_def)
next
fix x assume "x ∈ ?L n (FExists φ)"
then obtain x' where x: "x = map π x'" and "x' ∈ ?L (Suc n) φ" by (auto simp del: o_apply)
with FExists(2) have "x' ∈ lang⇩M⇩2⇩L (Suc n) φ"
by (intro subsetD[OF equalityD2[OF FExists(1)], of "Suc n" x'])
(auto split: if_split_asm sum.splits)
then obtain w I' where
*: "x' = enc (w, I')" "wf_interp_for_formula (w, I') φ" "length I' = Suc n" "satisfies (w, I') φ"
unfolding lang⇩M⇩2⇩L_def by auto
moreover then obtain I⇩0 I where "I' = I⇩0 # I" by (cases I') auto
moreover with FExists(2) *(2) obtain p where "I⇩0 = Inl p" "p < length w"
by (auto simp: nth_Cons' split: sum.splits if_split_asm)
ultimately have "x = enc (w, I)" "wf_interp_for_formula (w, I) (FExists φ)" "length I = n"
"length w > 0" "satisfies (w, I) (FExists φ)" using FExists(2) unfolding x
by (auto simp: map_tl nth_Cons' split: if_split_asm simp del: o_apply) (auto simp: π_def)
thus "x ∈ lang⇩M⇩2⇩L n (FExists φ)" unfolding lang⇩M⇩2⇩L_def by (auto intro!: exI[of _ w] exI[of _ I])
qed
next
case (FEXISTS φ)
show ?case
proof (intro equalityI subsetI)
fix x assume "x ∈ lang⇩M⇩2⇩L n (FEXISTS φ)"
then obtain w I P where
*: "x = enc (w, I)" "wf_interp_for_formula (w, I) (FEXISTS φ)"
"length I = n" "length w > 0" "P ⊆ {0 .. length w - 1}" "satisfies (w, Inr P # I) φ"
unfolding lang⇩M⇩2⇩L_def by auto
from *(4,5) have "∀p ∈ P. p < length w" by (cases w) auto
with *(2-4,6) FEXISTS(2) have "enc (w, Inr P # I) ∈ ?L (Suc n) φ"
by (intro subsetD[OF equalityD1[OF FEXISTS(1)], of "Suc n" "enc (w, Inr P # I)"])
(auto simp: lang⇩M⇩2⇩L_def nth_Cons' split: if_split_asm sum.splits
intro!: exI[of _ w] exI[of _ "Inr P # I"])
with *(1) show "x ∈ ?L n (FEXISTS φ)"
by (auto simp: map_index intro!: image_eqI[of _ "map π"] simp del: o_apply) (auto simp: π_def)
next
fix x assume "x ∈ ?L n (FEXISTS φ)"
then obtain x' where x: "x = map π x'" and x': "length x' > 0" and "x' ∈ ?L (Suc n) φ" by (auto simp del: o_apply)
with FEXISTS(2) have "x' ∈ lang⇩M⇩2⇩L (Suc n) φ"
by (intro subsetD[OF equalityD2[OF FEXISTS(1)], of "Suc n" x'])
(auto split: if_split_asm sum.splits)
then obtain w I' where
*: "x' = enc (w, I')" "wf_interp_for_formula (w, I') φ" "length I' = Suc n" "satisfies (w, I') φ"
unfolding lang⇩M⇩2⇩L_def by auto
moreover then obtain I⇩0 I where "I' = I⇩0 # I" by (cases I') auto
moreover with FEXISTS(2) *(2) obtain P where "I⇩0 = Inr P"
by (auto simp: nth_Cons' split: sum.splits if_split_asm)
moreover have "length w ≥ 1" using x' *(1) by (cases w) auto
ultimately have "x = enc (w, I)" "wf_interp_for_formula (w, I) (FEXISTS φ)" "length I = n"
"length w > 0" "satisfies (w, I) (FEXISTS φ)" using FEXISTS(2) unfolding x
by (auto simp add: map_tl nth_Cons' split: if_split_asm
intro!: exI[of _ P] simp del: o_apply) (auto simp: π_def)
thus "x ∈ lang⇩M⇩2⇩L n (FEXISTS φ)" unfolding lang⇩M⇩2⇩L_def by (auto intro!: exI[of _ w] exI[of _ I])
qed
qed
lemma wf_rexp_of: "wf_formula n φ ⟹ wf n (rexp_of n φ)"
by (induct φ arbitrary: n) (auto intro: wf_rexp_ENC simp: finite_FOV max_idx_vars)
lemma wf_rexp_of_alt: "wf_formula n φ ⟹ wf n (rexp_of_alt n φ)"
by (induct φ arbitrary: n) (auto simp: wf_rexp_ENC finite_FOV max_idx_vars)
lemma wf_rexp_of': "wf_formula n φ ⟹ wf n (rexp_of' n φ)"
unfolding rexp_of'_def by (auto simp: wf_rexp_ENC wf_rexp_of_alt finite_FOV max_idx_vars)
lemma wf_rexp_of_alt': "wf_formula n φ ⟹ wf n (rexp_of_alt' n φ)"
by (induct φ arbitrary: n) (auto simp: wf_rexp_ENC)
lemma wf_rexp_of'': "wf_formula n φ ⟹ wf n (rexp_of'' n φ)"
unfolding rexp_of''_def by (auto simp: wf_rexp_ENC wf_rexp_of_alt' finite_FOV max_idx_vars)
lemma ENC_Not: "ENC n (FOV (FNot φ)) = ENC n (FOV φ)"
unfolding ENC_def by auto
lemma ENC_And:
"wf_formula n (FAnd φ ψ) ⟹ lang n (ENC n (FOV (FAnd φ ψ))) - {[]} ⊆ lang n (ENC n (FOV φ)) ∩ lang n (ENC n (FOV ψ)) - {[]}"
proof
fix x assume wf: "wf_formula n (FAnd φ ψ)" and x: "x ∈ lang n (ENC n (FOV (FAnd φ ψ))) - {[]}"
hence wf1: "wf_formula n φ" and wf2: "wf_formula n ψ" by auto
from x obtain w I where wI: "x = enc (w, I)" "wf_interp_for_formula (w, I) (FAnd φ ψ)" "length I = n"
using lang_ENC_formula[OF wf] by blast
hence "wf_interp_for_formula (w, I) φ" "wf_interp_for_formula (w, I) ψ"
unfolding wf_interp_for_formula_FAnd by auto
hence "x ∈ (lang n (ENC n (FOV φ)) - {[]}) ∩ (lang n (ENC n (FOV ψ)) - {[]})"
unfolding lang_ENC_formula[OF wf1] lang_ENC_formula[OF wf2] using wI by auto
thus "x ∈ lang n (ENC n (FOV φ)) ∩ lang n (ENC n (FOV ψ)) - {[]}" by blast
qed
lemma ENC_Or:
"wf_formula n (FOr φ ψ) ⟹ lang n (ENC n (FOV (FOr φ ψ))) - {[]} ⊆ lang n (ENC n (FOV φ)) ∩ lang n (ENC n (FOV ψ)) - {[]}"
proof
fix x assume wf: "wf_formula n (FOr φ ψ)" and x: "x ∈ lang n (ENC n (FOV (FOr φ ψ))) - {[]}"
hence wf1: "wf_formula n φ" and wf2: "wf_formula n ψ" by auto
from x obtain w I where wI: "x = enc (w, I)" "wf_interp_for_formula (w, I) (FOr φ ψ)" "length I = n"
using lang_ENC_formula[OF wf] by blast
hence "wf_interp_for_formula (w, I) φ" "wf_interp_for_formula (w, I) ψ"
unfolding wf_interp_for_formula_FOr by auto
hence "x ∈ (lang n (ENC n (FOV φ)) - {[]}) ∩ (lang n (ENC n (FOV ψ)) - {[]})"
unfolding lang_ENC_formula[OF wf1] lang_ENC_formula[OF wf2] using wI by auto
thus "x ∈ lang n (ENC n (FOV φ)) ∩ lang n (ENC n (FOV ψ)) - {[]}" by blast
qed
lemma project_enc: "map π (enc (w, x # I)) = enc (w, I)"
unfolding π_def by auto
lemma list_list_eqI:
assumes "∀(_, x) ∈ set xs. x ≠ []" "∀(_, y) ∈ set ys. y ≠ []"
"map (λ(_, x). hd x) xs = map (λ(_, x). hd x) ys" "map π xs = map π ys"
shows "xs = ys"
proof -
from assms(4) have "length xs = length ys" by (metis length_map)
then show ?thesis using assms by (induct rule: list_induct2) (auto simp: π_def neq_Nil_conv)
qed
lemma project_enc_extend:
assumes "map π x = enc (w, I)" "∀(_, x) ∈ set x. x ≠ []"
shows "x = enc (w, Inr (positions_in_row x 0) # I)"
proof -
from arg_cong[OF assms(1), of "map fst"] have w: "w = map fst x" by (auto simp: π_def)
show ?thesis
proof (rule list_list_eqI[OF assms(2)], unfold project_enc)
show "map (λ(_, x). hd x) x = map (λ(_, x). hd x) (enc (w, Inr (positions_in_row x 0) # I))"
using assms(2) unfolding enc.simps map_index positions_in_row w
by (intro nth_equalityI) (auto dest!: nth_mem simp: hd_conv_nth)
qed (auto simp: assms(1))
qed
lemma ENC_Exists:
"wf_formula n (FExists φ) ⟹ lang n (ENC n (FOV (FExists φ))) - {[]} = map π ` lang (Suc n) (ENC (Suc n) (FOV φ)) - {[]}"
proof (intro equalityI subsetI)
fix x assume wf: "wf_formula n (FExists φ)" and x: "x ∈ lang n (ENC n (FOV (FExists φ))) - {[]}"
hence wf1: "wf_formula (Suc n) φ" by auto
from x obtain w I where wI: "x = enc (w, I)" "wf_interp_for_formula (w, I) (FExists φ)" "length I = n"
using lang_ENC_formula[OF wf] by blast
with x have "w ≠ []" by (cases w) auto
from wI(2) obtain p where "p < length w" "wf_interp_for_formula (w, Inl p # I) φ"
using wf_interp_for_formula_FExists[OF wf[folded wI(3)] ‹w ≠ []›] by auto
with wI(3) have "x ∈ map π ` (lang (Suc n) (ENC (Suc n) (FOV φ)) - {[]})"
unfolding wI(1) lang_ENC_formula[OF wf1] project_enc[symmetric, of w I "Inl p"]
by (intro imageI CollectI exI[of _ w] exI[of _ "Inl p # I"]) auto
thus "x ∈ map π ` lang (Suc n) (ENC (Suc n) (FOV φ)) - {[]}" by blast
next
fix x assume wf: "wf_formula n (FExists φ)" and "x ∈ map π ` lang (Suc n) (ENC (Suc n) (FOV φ)) - {[]}"
hence wf1: "wf_formula (Suc n) φ" and "0 ∈ FOV φ" and x: "x ∈ map π ` (lang (Suc n) (ENC (Suc n) (FOV φ)) - {[]})" by auto
from x obtain w I where wI: "x = map π (enc (w, I))" "wf_interp_for_formula (w, I) φ" "length I = Suc n"
using lang_ENC_formula[OF wf1] by auto
with ‹0 ∈ FOV φ› obtain p I' where I: "I = Inl p # I'" by (cases I) (fastforce split: sum.splits)+
with wI have wtlI: "x = enc (w, I')" "length I' = n" unfolding π_def by auto
with x have "w ≠ []" by (cases w) auto
have "wf_interp_for_formula (w, I') (FExists φ)"
using wf_interp_for_formula_FExists[OF wf[folded wtlI(2)] ‹w ≠ []›]
wf_interp_for_formula_any_Inl[OF wI(2)[unfolded I]] ..
with wtlI show "x ∈ lang n (ENC n (FOV (FExists φ))) - {[]}" unfolding lang_ENC_formula[OF wf] by blast
qed
lemma ENC_EXISTS:
"wf_formula n (FEXISTS φ) ⟹ lang n (ENC n (FOV (FEXISTS φ))) - {[]} = map π ` lang (Suc n) (ENC (Suc n) (FOV φ)) - {[]}"
proof (intro equalityI subsetI)
fix x assume wf: "wf_formula n (FEXISTS φ)" and x: "x ∈ lang n (ENC n (FOV (FEXISTS φ))) - {[]}"
hence wf1: "wf_formula (Suc n) φ" by auto
from x obtain w I where wI: "x = enc (w, I)" "wf_interp_for_formula (w, I) (FEXISTS φ)" "length I = n"
using lang_ENC_formula[OF wf] by blast
with x have "w ≠ []" by (cases w) auto
from wI(2) obtain P where "∀p ∈ P. p < length w" "wf_interp_for_formula (w, Inr P # I) φ"
using wf_interp_for_formula_FEXISTS[OF wf[folded wI(3)] ‹w ≠ []›] by auto
with wI(3) have "x ∈ map π ` (lang (Suc n) (ENC (Suc n) (FOV φ)) - {[]})"
unfolding wI(1) lang_ENC_formula[OF wf1] project_enc[symmetric, of w I "Inr P"]
by (intro imageI CollectI exI[of _ w] exI[of _ "Inr P # I"]) auto
thus "x ∈ map π ` lang (Suc n) (ENC (Suc n) (FOV φ)) - {[]}" by blast
next
fix x assume wf: "wf_formula n (FEXISTS φ)" and "x ∈ map π ` lang (Suc n) (ENC (Suc n) (FOV φ)) - {[]}"
hence wf1: "wf_formula (Suc n) φ" and "0 ∈ SOV φ" and x: "x ∈ map π ` (lang (Suc n) (ENC (Suc n) (FOV φ)) - {[]})" by auto
from x obtain w I where wI: "x = map π (enc (w, I))" "wf_interp_for_formula (w, I) φ" "length I = Suc n"
using lang_ENC_formula[OF wf1] by auto
with ‹0 ∈ SOV φ› obtain P I' where I: "I = Inr P # I'" by (cases I) (fastforce split: sum.splits)+
with wI have wtlI: "x = enc (w, I')" "length I' = n" unfolding π_def by auto
with x have "w ≠ []" by (cases w) auto
have "wf_interp_for_formula (w, I') (FEXISTS φ)"
using wf_interp_for_formula_FEXISTS[OF wf[folded wtlI(2)] ‹w ≠ []›]
wf_interp_for_formula_any_Inr[OF wI(2)[unfolded I]] ..
with wtlI show "x ∈ lang n (ENC n (FOV (FEXISTS φ))) - {[]}" unfolding lang_ENC_formula[OF wf] by blast
qed
lemma map_project_empty: "map π ` A - {[]} = map π ` (A - {[]})"
by auto
lemma lang⇩M⇩2⇩L_rexp_of_rexp_of':
"wf_formula n φ ⟹ lang n (rexp_of n φ) - {[]} = lang n (rexp_of' n φ) - {[]}"
unfolding rexp_of'_def proof (induction φ arbitrary: n)
case (FNot φ)
hence "wf_formula n φ" by simp
with FNot.IH show ?case unfolding rexp_of.simps rexp_of_alt.simps lang.simps ENC_Not by blast
next
case (FAnd φ⇩1 φ⇩2)
hence wf1: "wf_formula n φ⇩1" and wf2: "wf_formula n φ⇩2" by force+
from FAnd.IH(1)[OF wf1] FAnd.IH(2)[OF wf2] show ?case using ENC_And[OF FAnd.prems]
unfolding rexp_of.simps rexp_of_alt.simps lang.simps rexp_of_list.simps by blast
next
case (FOr φ⇩1 φ⇩2)
hence wf1: "wf_formula n φ⇩1" and wf2: "wf_formula n φ⇩2" by force+
from FOr.IH(1)[OF wf1] FOr.IH(2)[OF wf2] show ?case using ENC_Or[OF FOr.prems]
unfolding rexp_of.simps rexp_of_alt.simps lang.simps by blast
next
case (FExists φ)
hence wf: "wf_formula (n + 1) φ" by auto
show ?case using ENC_Exists[OF FExists.prems]
unfolding rexp_of.simps rexp_of_alt.simps lang.simps map_project_empty FExists.IH[OF wf] by auto
next
case (FEXISTS φ)
hence wf: "wf_formula (n + 1) φ" by auto
show ?case using ENC_EXISTS[OF FEXISTS.prems]
unfolding rexp_of.simps rexp_of_alt.simps lang.simps map_project_empty FEXISTS.IH[OF wf] by auto
qed auto
lemma Int_Diff_both: "A ∩ B - C = (A - C) ∩ (B - C)"
by auto
lemma lang_ENC_split:
assumes "finite X" "X = Y1 ∪ Y2" "n = 0 ∨ (∀p ∈ X. p < n)"
shows "lang n (ENC n X) = lang n (ENC n Y1) ∩ lang n (ENC n Y2)"
unfolding ENC_def lang_INTERSECT using assms lang_subset_lists[OF wf_rexp_valid_ENC, of n] by auto
lemma map_project_Int_ENC:
assumes "0 ∉ X" "X ⊆ {0 ..< n + 1}" "Z ⊆ lists ((set o σ Σ) (n + 1))"
shows "map π ` (Z ∩ lang (n + 1) (ENC (n + 1) X) - {[]}) =
map π ` Z ∩ lang n (ENC n ((λx. x - 1) ` X)) - {[]}"
proof -
let ?Y = "{0 ..< n + 1} - X"
let ?fX = "(λx. x - 1) ` X"
let ?fY = "{0 ..< n} - (λx. x - 1) ` X"
from assms have *: "(λx. x - 1) ` X ⊆ {0 ..< n}" by (cases n) auto
show ?thesis unfolding Int_Diff lang_ENC[OF assms(2) subset_refl] lang_ENC[OF * subset_refl]
proof (safe elim!: imageI)
fix w I
assume *: "length I = n + 1" "w ≠ []"
"∀i∈X. case I ! i of Inl x ⇒ True | Inr x ⇒ False"
"∀i∈?Y. case I ! i of Inl x ⇒ False | Inr x ⇒ True"
"∀a∈set w. a ∈ set Σ" "Ball (set I) (case_sum (λp. p < length w) (λP. ∀p∈P. p < length w))"
then obtain p Is where "I = p # Is" by (cases I) auto
then show "∃w' I'.
map π (enc (w, I)) = enc (w', I') ∧
length I' = n ∧ (0 < length w' ∧ (∀a∈set w'. a ∈ set Σ) ∧
Ball (set I') (case_sum (λp. p < length w') (λP. ∀p∈P. p < length w'))) ∧
(∀i∈?fX. case I' ! i of Inl x ⇒ True | Inr x ⇒ False) ∧
(∀i∈?fY. case I' ! i of Inl x ⇒ False | Inr x ⇒ True)"
proof (hypsubst, intro exI[of _ w] exI[of _ Is] conjI ballI project_enc)
fix i assume "i ∈ ?fY"
then show "case Is ! i of Inl x ⇒ False | Inr x ⇒ True"
using *[unfolded ‹I = p # Is›] assms(1)
by (cases "i = 0") (fastforce simp: nth_Cons' image_iff split: sum.splits if_splits)+
qed (insert *[unfolded ‹I = p # Is›] assms(1), auto simp: nth_Cons' split: sum.splits if_splits)
next
fix x w I
assume *: "w ≠ []" "x ∈ Z" "map π x = enc (w, I)"
"∀i∈?fX. case I ! i of Inl x ⇒ True | Inr x ⇒ False"
"∀i∈{0 ..< length I} - ?fX. case I ! i of Inl x ⇒ False | Inr x ⇒ True"
"∀a∈set w. a ∈ set Σ" "Ball (set I) (case_sum (λp. p < length w) (λP. ∀p∈P. p < length w))"
moreover from assms(1) have "∀x ∈ X. x > 0" "⋀x y. x - Suc 0 = y - Suc 0 ⟷
x = y ∨ (x = 0 ∧ y = Suc 0) ∨ (x = Suc 0 ∧ y = 0)"
by (metis neq0_conv) (metis One_nat_def Suc_diff_1 diff_0_eq_0 diff_self_eq_0 neq0_conv)
moreover from *(2) assms(3) have "x = enc (w, Inr (positions_in_row x 0) # I)"
apply (intro project_enc_extend [OF *(3)])
apply (simp only: σ_def)
apply auto
done
moreover from arg_cong[OF *(3), of length] have "length w = length x" by simp
ultimately show " map π x ∈ map π `
(Z ∩ {enc (w, I') |w I'. length I' = length I + 1 ∧ (0 < length w ∧ (∀a∈set w. a ∈ set Σ) ∧
Ball (set I') (case_sum (λp. p < length w) (λP. ∀p∈P. p < length w))) ∧
(∀i∈X. case I' ! i of Inl x ⇒ True | Inr x ⇒ False) ∧
(∀i∈{0..<length I + 1} - X. case I' ! i of Inl x ⇒ False | Inr x ⇒ True)})"
by (intro imageI CollectI conjI IntI exI[of _ w] exI[of _ "Inr (positions_in_row x 0) # I"])
(auto simp: nth_Cons' positions_in_row elim!: bspec simp del: enc.simps)
qed
qed
lemma map_project_ENC:
assumes "X ⊆ {0 ..< n + 1}" "Z ⊆ lists ((set o σ Σ) (n + 1))"
shows "map π ` (Z ∩ lang (n + 1) (ENC (n + 1) X) - {[]}) =
(if 0 ∈ X
then map π ` (Z ∩ lang (n + 1) (ENC (n + 1) {0})) ∩ lang n (ENC n ((λx. x - 1) ` (X - {0}))) - {[]}
else map π ` Z ∩ lang n (ENC n ((λx. x - 1) ` (X - {0}))) - {[]})"
(is "?L = (if _ then ?R1 else ?R2)")
proof (split if_splits, intro conjI impI)
assume 0: "0 ∉ X"
from assms have fin: "finite X" "finite ((λx. x - 1) ` X)"
by (auto elim: finite_subset intro!: finite_imageI[of "X"])
from 0 show "?L = ?R2" using map_project_Int_ENC[OF 0 assms]
unfolding lists_image[symmetric] π_σ
Int_absorb1[OF lang_subset_lists[OF wf_rexp_ENC[OF fin(1)]], of "n + 1"]
Int_absorb1[OF lang_subset_lists[OF wf_rexp_ENC[OF fin(2)]], of n]
by auto
next
assume "0 ∈ X"
hence 0: "0 ∉ X - {0}" and X: "X = {0} ∪ (X - {0})" by auto
from assms have fin: "finite X"
by (auto elim: finite_subset intro!: finite_imageI[of "X"])
have "?L = map π ` ((Z ∩ lang (n + 1) (ENC (n + 1) {0})) ∩ lang (n + 1) (ENC (n + 1) (X - {0})) - {[]})"
unfolding Int_assoc using assms by (subst lang_ENC_split[OF fin X, of "n + 1"]) auto
also have "… = ?R1"
using 0 assms by (elim map_project_Int_ENC) auto
finally show "?L = ?R1" .
qed
abbreviation "𝔏 ≡ project.lang (set ∘ σ Σ) π"
lemma lang⇩M⇩2⇩L_rexp_of'_rexp_of'':
"wf_formula n φ ⟹ lang n (rexp_of' n φ) - {[]} = lang n (rexp_of'' n φ) - {[]}"
unfolding rexp_of'_def rexp_of''_def
proof (induction φ arbitrary: n)
case (FNot φ)
hence "wf_formula n φ" by simp
with FNot.IH show ?case unfolding rexp_of_alt.simps rexp_of_alt'.simps lang.simps ENC_Not by blast
next
case (FAnd φ⇩1 φ⇩2)
hence wf1: "wf_formula n φ⇩1" and wf2: "wf_formula n φ⇩2" by force+
from FAnd.IH(1)[OF wf1] FAnd.IH(2)[OF wf2] show ?case using ENC_And[OF FAnd.prems]
unfolding rexp_of_alt.simps rexp_of_alt'.simps lang.simps rexp_of_list.simps by blast
next
case (FOr φ⇩1 φ⇩2)
hence wf1: "wf_formula n φ⇩1" and wf2: "wf_formula n φ⇩2" by force+
from FOr.IH(1)[OF wf1] FOr.IH(2)[OF wf2] show ?case using ENC_Or[OF FOr.prems]
unfolding rexp_of_alt.simps rexp_of_alt'.simps lang.simps rexp_of_list.simps by blast
next
case (FExists φ)
hence wf: "wf_formula (n + 1) φ" and 0: "0 ∈ FOV φ" by auto
then show ?case
using ENC_Exists[OF FExists.prems] map_project_ENC[of "FOV φ" n] max_idx_vars[of "n + 1" φ]
wf_rexp_of_alt'[OF wf] 0
unfolding rexp_of_alt.simps rexp_of_alt'.simps lang.simps Int_Diff_both
unfolding map_project_empty FExists.IH[OF wf, unfolded lang.simps]
by (intro trans[OF arg_cong2[of _ _ _ _ "(∩)", OF map_project_ENC[OF _ lang_subset_lists] refl]])
fastforce+
next
case (FEXISTS φ)
hence wf: "wf_formula (n + 1) φ" and 0: "0 ∉ FOV φ" by auto
then show ?case
using ENC_EXISTS[OF FEXISTS.prems] map_project_ENC[of "FOV φ" n] max_idx_vars[of "n + 1" φ]
wf_rexp_of_alt'[OF wf] 0
unfolding rexp_of_alt.simps rexp_of_alt'.simps lang.simps Int_Diff_both
unfolding map_project_empty FEXISTS.IH[OF wf, unfolded lang.simps]
by (intro trans[OF arg_cong2[of _ _ _ _ "(∩)", OF map_project_ENC[OF _ lang_subset_lists] refl]])
fastforce+
qed simp_all
theorem lang⇩M⇩2⇩L_rexp_of': "wf_formula n φ ⟹ lang⇩M⇩2⇩L n φ = lang n (rexp_of' n φ) - {[]}"
unfolding lang⇩M⇩2⇩L_rexp_of_rexp_of'[symmetric] by (rule lang⇩M⇩2⇩L_rexp_of)
theorem lang⇩M⇩2⇩L_rexp_of'': "wf_formula n φ ⟹ lang⇩M⇩2⇩L n φ = lang n (rexp_of'' n φ) - {[]}"
unfolding lang⇩M⇩2⇩L_rexp_of'_rexp_of''[symmetric] by (rule lang⇩M⇩2⇩L_rexp_of')
end
end