(* Author: Dmitriy Traytel *) 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"])