Theory Relational_Calculus

section ‹Relational Calculus›

(*<*)
theory Relational_Calculus
imports
  Preliminaries
  "Deriving.Derive"
begin
(*>*)

subsection ‹First-order Terms›

datatype 'a "term" = Const 'a | Var nat

type_synonym 'a val = "nat ⇒ 'a"

fun fv_term_set :: "'a term ⇒ nat set" where
  "fv_term_set (Var n) = {n}"
| "fv_term_set _ = {}"

fun fv_fo_term_list :: "'a term ⇒ nat list" where
  "fv_fo_term_list (Var n) = [n]"
| "fv_fo_term_list _ = []"

definition fv_terms_set :: "('a term) list ⇒ nat set" where
  "fv_terms_set ts = ⋃(set (map fv_term_set ts))"

fun eval_term :: "'a val ⇒ 'a term ⇒ 'a" (infix "⋅" 60) where
  "eval_term σ (Const c) = c"
| "eval_term σ (Var n) = σ n"

definition eval_terms :: "'a val ⇒ ('a term) list ⇒ 'a list" (infix "⊙" 60) where
  "eval_terms σ ts = map (eval_term σ) ts"

lemma finite_set_term: "finite (set_term t)"
  by (cases t) auto

lemma finite_fv_term_set: "finite (fv_term_set t)"
  by (cases t) auto

lemma fv_term_setD: "n ∈ fv_term_set t ⟹ t = Var n"
  by (cases t) auto

lemma fv_term_set_cong: "fv_term_set t = fv_term_set (map_term f t)"
  by (cases t) auto

lemma fv_terms_setI: "Var m ∈ set ts ⟹ m ∈ fv_terms_set ts"
  by (induction ts) (auto simp: fv_terms_set_def)

lemma fv_terms_setD: "m ∈ fv_terms_set ts ⟹ Var m ∈ set ts"
  by (induction ts) (auto simp: fv_terms_set_def dest: fv_term_setD)

lemma finite_fv_terms_set: "finite (fv_terms_set ts)"
  by (auto simp: fv_terms_set_def finite_fv_term_set)

lemma fv_terms_set_cong: "fv_terms_set ts = fv_terms_set (map (map_term f) ts)"
  using fv_term_set_cong
  by (induction ts) (fastforce simp: fv_terms_set_def)+

lemma eval_term_cong: "(⋀n. n ∈ fv_term_set t ⟹ σ n = σ' n) ⟹
  eval_term σ t = eval_term σ' t"
  by (cases t) auto

lemma eval_terms_fv_terms_set: "σ ⊙ ts = σ' ⊙ ts ⟹ n ∈ fv_terms_set ts ⟹ σ n = σ' n"
proof (induction ts)
  case (Cons t ts)
  then show ?case
    by (cases t) (auto simp: eval_terms_def fv_terms_set_def)
qed (auto simp: eval_terms_def fv_terms_set_def)

lemma eval_terms_cong: "(⋀n. n ∈ fv_terms_set ts ⟹ σ n = σ' n) ⟹
  eval_terms σ ts = eval_terms σ' ts"
  by (auto simp: eval_terms_def fv_terms_set_def intro: eval_term_cong)

subsection ‹Relational Calculus Syntax and Semantics›

datatype (discs_sels) ('a, 'b) fmla =
  Pred 'b "('a term) list"
| Bool bool
| Eq nat "'a term"
| Neg "('a, 'b) fmla"
| Conj "('a, 'b) fmla" "('a, 'b) fmla"
| Disj "('a, 'b) fmla" "('a, 'b) fmla"
| Exists nat "('a, 'b) fmla"

derive linorder "term"
derive linorder fmla

fun fv :: "('a, 'b) fmla ⇒ nat set" where
  "fv (Pred _ ts) = fv_terms_set ts"
| "fv (Bool b) = {}"
| "fv (Eq x t') = {x} ∪ fv_term_set t'"
| "fv (Neg φ) = fv φ"
| "fv (Conj φ ψ) = fv φ ∪ fv ψ"
| "fv (Disj φ ψ) = fv φ ∪ fv ψ"
| "fv (Exists z φ) = fv φ - {z}"

definition exists where "exists x Q = (if x ∈ fv Q then Exists x Q else Q)"
abbreviation "Forall x Q ≡ Neg (Exists x (Neg Q))"
abbreviation "forall x Q ≡ Neg (exists x (Neg Q))"
abbreviation "Impl Q1 Q2 ≡ Disj (Neg Q1) Q2"

definition "EXISTS xs Q = fold Exists xs Q"

abbreviation close where
  "close Q ≡ EXISTS (sorted_list_of_set (fv Q)) Q"

lemma fv_exists[simp]: "fv (exists x Q) = fv Q - {x}"
  by (auto simp: exists_def)

lemma fv_EXISTS: "fv (EXISTS xs Q) = fv Q - set xs"
  by (induct xs arbitrary: Q) (auto simp: EXISTS_def)

lemma exists_Exists: "x ∈ fv Q ⟹ exists x Q = Exists x Q"
  by (auto simp: exists_def)

lemma is_Bool_exists[simp]: "is_Bool (exists x Q) = is_Bool Q"
  by (auto simp: exists_def is_Bool_def)

lemma finite_fv[simp]: "finite (fv φ)"
  by (induction φ rule: fv.induct)
     (auto simp: finite_fv_term_set finite_fv_terms_set)

lemma fv_close[simp]: "fv (close Q) = {}"
  by (subst fv_EXISTS) auto

type_synonym 'a table = "('a list) set"
type_synonym ('a, 'b) intp = "'b × nat ⇒ 'a table"

definition adom :: "('a, 'b) intp ⇒ 'a set" where
  "adom I = (⋃rn. ⋃xs ∈ I rn. set xs)"

fun sat :: "('a, 'b) fmla ⇒ ('a, 'b) intp ⇒ 'a val ⇒ bool" where
  "sat (Pred r ts) I σ ⟷ σ ⊙ ts ∈ I (r, length ts)"
| "sat (Bool b) I σ ⟷ b"
| "sat (Eq x t') I σ ⟷ σ x = σ ⋅ t'"
| "sat (Neg φ) I σ ⟷ ¬sat φ I σ"
| "sat (Conj φ ψ) I σ ⟷ sat φ I σ ∧ sat ψ I σ"
| "sat (Disj φ ψ) I σ ⟷ sat φ I σ ∨ sat ψ I σ"
| "sat (Exists z φ) I σ ⟷ (∃x. sat φ I (σ(z := x)))"

lemma sat_fv_cong: "(⋀n. n ∈ fv φ ⟹ σ n = σ' n) ⟹
  sat φ I σ ⟷ sat φ I σ'"
proof (induction φ arbitrary: σ σ')
  case (Neg φ)
  show ?case
    using Neg(1)[of σ σ'] Neg(2)
    by auto
next
  case (Conj φ ψ)
  show ?case
    using Conj(1,2)[of σ σ'] Conj(3)
    by auto
next
  case (Disj φ ψ)
  show ?case
    using Disj(1,2)[of σ σ'] Disj(3)
    by auto
next
  case (Exists n φ)
  have "⋀x. sat φ I (σ(n := x)) = sat φ I (σ'(n := x))"
    using Exists(2)
    by (auto intro!: Exists(1))
  then show ?case
    by simp
qed (auto cong: eval_terms_cong eval_term_cong)

lemma sat_fun_upd: "n ∉ fv Q ⟹ sat Q I (σ(n := z)) = sat Q I σ"
  by (rule sat_fv_cong) auto

lemma sat_exists[simp]: "sat (exists n Q) I σ = (∃x. sat Q I (σ(n := x)))"
  by (auto simp add: exists_def sat_fun_upd)

abbreviation eq (infix "≈" 80) where
  "x ≈ y ≡ Eq x (Var y)"

definition equiv (infix "≜" 100) where
  "Q1 ≜ Q2 = (∀I σ. finite (adom I) ⟶ sat Q1 I σ ⟷ sat Q2 I σ)"

lemma equiv_refl[iff]: "Q ≜ Q"
  unfolding equiv_def by auto

lemma equiv_sym[sym]: "Q1 ≜ Q2 ⟹ Q2 ≜ Q1"
  unfolding equiv_def by auto

lemma equiv_trans[trans]: "Q1 ≜ Q2 ⟹ Q2 ≜ Q3 ⟹ Q1 ≜ Q3"
  unfolding equiv_def by auto

lemma equiv_Neg_cong[simp]: "Q ≜ Q' ⟹ Neg Q ≜ Neg Q'"
  unfolding equiv_def by auto

lemma equiv_Conj_cong[simp]: "Q1 ≜ Q1' ⟹ Q2 ≜ Q2' ⟹ Conj Q1 Q2 ≜ Conj Q1' Q2'"
  unfolding equiv_def by auto

lemma equiv_Disj_cong[simp]: "Q1 ≜ Q1' ⟹ Q2 ≜ Q2' ⟹ Disj Q1 Q2 ≜ Disj Q1' Q2'"
  unfolding equiv_def by auto

lemma equiv_Exists_cong[simp]: "Q ≜ Q' ⟹ Exists x Q ≜ Exists x Q'"
  unfolding equiv_def by auto

lemma equiv_Exists_exists_cong[simp]: "Q ≜ Q' ⟹ Exists x Q ≜ exists x Q'"
  unfolding equiv_def by auto

lemma equiv_Exists_Disj: "Exists x (Disj Q1 Q2) ≜ Disj (Exists x Q1) (Exists x Q2)"
  unfolding equiv_def by auto

lemma equiv_Disj_Assoc: "Disj (Disj Q1 Q2) Q3 ≜ Disj Q1 (Disj Q2 Q3)"
  unfolding equiv_def by auto

lemma foldr_Disj_equiv_cong[simp]:
  "list_all2 (≜) xs ys ⟹ b ≜ c ⟹ foldr Disj xs b ≜ foldr Disj ys c"
  by (induct xs ys arbitrary: b c rule: list.rel_induct) auto

lemma Exists_nonfree_equiv: "x ∉ fv Q ⟹ Exists x Q ≜ Q"
  unfolding equiv_def sat.simps
  by (metis exists_def sat_exists)

subsection ‹Constant Propagation›

fun cp where
  "cp (Eq x t) = (case t of Var y ⇒ if x = y then Bool True else x ≈ y | _ ⇒ Eq x t)"
| "cp (Neg Q) = (let Q' = cp Q in if is_Bool Q' then Bool (¬ un_Bool Q') else Neg Q')"
| "cp (Conj Q1 Q2) =
    (let Q1' = cp Q1; Q2' = cp Q2 in
    if is_Bool Q1' then if un_Bool Q1' then Q2' else Bool False
    else if is_Bool Q2' then if un_Bool Q2' then Q1' else Bool False
    else Conj Q1' Q2')"
| "cp (Disj Q1 Q2) =
    (let Q1' = cp Q1; Q2' = cp Q2 in
    if is_Bool Q1' then if un_Bool Q1' then Bool True else Q2'
    else if is_Bool Q2' then if un_Bool Q2' then Bool True else Q1'
    else Disj Q1' Q2')"
| "cp (Exists x Q) = exists x (cp Q)"
| "cp Q = Q"

lemma fv_cp: "fv (cp Q) ⊆ fv Q"
  by (induct Q) (auto simp: Let_def split: fmla.splits term.splits)

lemma cp_exists[simp]: "cp (exists x Q) = exists x (cp Q)"
  by (auto simp: exists_def fv_cp[THEN set_mp])

fun nocp where
  "nocp (Bool b) = False"
| "nocp (Pred p ts) = True"
| "nocp (Eq x t) = (t ≠ Var x)"
| "nocp (Neg Q) = nocp Q"
| "nocp (Conj Q1 Q2) = (nocp Q1 ∧ nocp Q2)"
| "nocp (Disj Q1 Q2) = (nocp Q1 ∧ nocp Q2)"
| "nocp (Exists x Q) = (x ∈ fv Q ∧ nocp Q)"

lemma nocp_exists[simp]: "nocp (exists x Q) = nocp Q"
  unfolding exists_def by auto

lemma nocp_cp_triv: "nocp Q ⟹ cp Q = Q"
  by (induct Q) (auto simp: exists_def is_Bool_def split: fmla.splits term.splits)

lemma is_Bool_cp_triv: "is_Bool Q ⟹ cp Q = Q"
  by (auto simp: is_Bool_def)

lemma nocp_cp_or_is_Bool: "nocp (cp Q) ∨ is_Bool (cp Q)"
  by (induct Q) (auto simp: Let_def split: fmla.splits term.splits)

lemma cp_idem[simp]: "cp (cp Q) = cp Q"
  using is_Bool_cp_triv nocp_cp_triv nocp_cp_or_is_Bool by blast

lemma sat_cp[simp]: "sat (cp Q) I σ = sat Q I σ"
  by (induct Q arbitrary: σ) (auto 0 0 simp: Let_def is_Bool_def split: term.splits fmla.splits)

lemma equiv_cp_cong[simp]: "Q ≜ Q' ⟹ cp Q ≜ cp Q'"
  by (auto simp: equiv_def)

lemma equiv_cp[simp]: "cp Q ≜ Q"
  by (auto simp: equiv_def)

definition cpropagated where "cpropagated Q = (nocp Q ∨ is_Bool Q)"

lemma cpropagated_cp[simp]: "cpropagated (cp Q)"
  by (auto simp: cpropagated_def nocp_cp_or_is_Bool)

lemma nocp_cpropagated[simp]: "nocp Q ⟹ cpropagated Q"
  by (auto simp: cpropagated_def)

lemma cpropagated_cp_triv: "cpropagated Q ⟹ cp Q = Q"
  by (auto simp: cpropagated_def nocp_cp_triv is_Bool_def)

lemma cpropagated_nocp: "cpropagated Q ⟹ x ∈ fv Q ⟹ nocp Q"
  by (auto simp: cpropagated_def is_Bool_def)

lemma cpropagated_simps[simp]:
  "cpropagated (Bool b) ⟷ True"
  "cpropagated (Pred p ts) ⟷ True"
  "cpropagated (Eq x t) ⟷ t ≠ Var x"
  "cpropagated (Neg Q) ⟷ nocp Q"
  "cpropagated (Conj Q1 Q2) ⟷ nocp Q1 ∧ nocp Q2"
  "cpropagated (Disj Q1 Q2) ⟷ nocp Q1 ∧ nocp Q2"
  "cpropagated (Exists x Q) ⟷ x ∈ fv Q ∧ nocp Q"
  by (auto simp: cpropagated_def)

subsection ‹Big Disjunction›

fun foldr1 where
  "foldr1 f (x # xs) z = foldr f xs x"
| "foldr1 f [] z = z"

definition DISJ where
  "DISJ G = foldr1 Disj (sorted_list_of_set G) (Bool False)"

lemma sat_foldr_Disj[simp]: "sat (foldr Disj xs Q) I σ = (∃Q ∈ set xs ∪ {Q}. sat Q I σ)"
  by (induct xs arbitrary: Q) auto

lemma sat_foldr1_Disj[simp]: "sat (foldr1 Disj xs Q) I σ = (if xs = [] then sat Q I σ else ∃Q ∈ set xs. sat Q I σ)"
  by (cases xs) auto

lemma sat_DISJ[simp]: "finite G ⟹ sat (DISJ G) I σ = (∃Q ∈ G. sat Q I σ)"
  unfolding DISJ_def by auto

lemma foldr_Disj_equiv: "insert Q (set Qs) = insert Q' (set Qs') ⟹ foldr Disj Qs Q ≜ foldr Disj Qs' Q'"
  by (auto simp: equiv_def set_eq_iff)

lemma foldr1_Disj_equiv: "set Qs = set Qs' ⟹ foldr1 Disj Qs (Bool False) ≜ foldr1 Disj Qs' (Bool False)"
  by (cases Qs; cases Qs') (auto simp: foldr_Disj_equiv)

lemma foldr1_Disj_equiv_cong[simp]:
  "list_all2 (≜) xs ys ⟹ b ≜ c ⟹ foldr1 Disj xs b ≜ foldr1 Disj ys c"
  by (erule list.rel_cases) auto

lemma Exists_foldr_Disj:
  "Exists x (foldr Disj xs b) ≜ foldr Disj (map (exists x) xs) (exists x b)"
  by (auto simp: equiv_def)

lemma Exists_foldr1_Disj:
  "Exists x (foldr1 Disj xs b) ≜ foldr1 Disj (map (exists x) xs) (exists x b)"
  by (auto simp: equiv_def)

lemma Exists_DISJ:
  "finite 𝒬 ⟹ Exists x (DISJ 𝒬) ≜ DISJ (exists x ` 𝒬)"
  unfolding DISJ_def
  by (rule equiv_trans[OF Exists_foldr1_Disj])
    (auto simp: exists_def intro!: foldr1_Disj_equiv equiv_trans[OF _ equiv_sym[OF equiv_cp]])

lemma Exists_cp_DISJ:
  "finite 𝒬 ⟹ Exists x (cp (DISJ 𝒬)) ≜ DISJ (exists x ` 𝒬)"
  by (rule equiv_trans[OF equiv_Exists_cong[OF equiv_cp] Exists_DISJ])

lemma Disj_empty[simp]: "DISJ {} = Bool False"
  unfolding DISJ_def by auto
lemma Disj_single[simp]: "DISJ {x} = x"
  unfolding DISJ_def by auto

lemma DISJ_insert[simp]: "finite X ⟹ DISJ (insert x X) ≜ Disj x (DISJ X)"
  by (induct X arbitrary: x rule: finite_induct) (auto simp: equiv_def)

lemma DISJ_union[simp]: "finite X ⟹ finite Y ⟹ DISJ (X ∪ Y) ≜ Disj (DISJ X) (DISJ Y)"
  by (induct X rule: finite_induct)
    (auto intro!: DISJ_insert[THEN equiv_trans] simp: equiv_def)

lemma DISJ_exists_pull_out: "finite 𝒬 ⟹ Q ∈ 𝒬 ⟹
  DISJ (exists x ` 𝒬) ≜ Disj (Exists x Q) (DISJ (exists x ` (𝒬 - {Q})))"
  by (auto simp: equiv_def)

lemma DISJ_push_in: "finite 𝒬 ⟹ Disj Q (DISJ 𝒬) ≜ DISJ (insert Q 𝒬)"
  by (auto simp: equiv_def)

lemma DISJ_insert_reorder: "finite 𝒬 ⟹ DISJ (insert (Disj Q1 Q2) 𝒬) ≜ DISJ (insert Q2 (insert Q1 𝒬))"
  by (auto simp: equiv_def)

lemma DISJ_insert_reorder': "finite 𝒬 ⟹ finite 𝒬' ⟹ DISJ (insert (Disj (DISJ 𝒬') Q2) 𝒬) ≜ DISJ (insert Q2 (𝒬' ∪ 𝒬))"
  by (auto simp: equiv_def)

lemma fv_foldr_Disj[simp]: "fv (foldr Disj Qs Q) = (fv Q ∪ (⋃Q ∈ set Qs. fv Q))"
  by (induct Qs) auto

lemma fv_foldr1_Disj[simp]: "fv (foldr1 Disj Qs Q) = (if Qs = [] then fv Q else (⋃Q ∈ set Qs. fv Q))"
  by (cases Qs) auto

lemma fv_DISJ: "finite 𝒬 ⟹ fv (DISJ 𝒬) ⊆ (⋃Q ∈ 𝒬. fv Q)"
  by (auto simp: DISJ_def dest!: fv_cp[THEN set_mp] split: if_splits)

lemma fv_DISJ_close[simp]: "finite 𝒬 ⟹ fv (DISJ (close ` 𝒬)) = {}"
  by (auto dest!: fv_DISJ[THEN set_mp, rotated 1])

lemma fv_cp_foldr_Disj: "∀Q∈set Qs ∪ {Q}. cpropagated Q ∧ fv Q = A ⟹ fv (cp (foldr Disj Qs Q)) = A"
  by (induct Qs) (auto simp: cpropagated_cp_triv Let_def is_Bool_def)

lemma fv_cp_foldr1_Disj: "cp (foldr1 Disj Qs (Bool False)) ≠ Bool False ⟹
  ∀Q∈set Qs. cpropagated Q ∧ fv Q = A ⟹
  fv (cp (foldr1 Disj Qs (Bool False))) = A"
  by (cases Qs) (auto simp: fv_cp_foldr_Disj)

lemma fv_cp_DISJ_eq: "finite 𝒬 ⟹ cp (DISJ 𝒬) ≠ Bool False ⟹ ∀Q ∈ 𝒬. cpropagated Q ∧ fv Q = A ⟹ fv (cp (DISJ 𝒬)) = A"
  by (auto simp: DISJ_def fv_cp_foldr1_Disj)

fun sub where
  "sub (Bool t) = {Bool t}"
| "sub (Pred p ts) = {Pred p ts}"
| "sub (Eq x t) = {Eq x t}"
| "sub (Neg Q) = insert (Neg Q) (sub Q)"
| "sub (Conj Q1 Q2) = insert (Conj Q1 Q2) (sub Q1 ∪ sub Q2)"
| "sub (Disj Q1 Q2) = insert (Disj Q1 Q2) (sub Q1 ∪ sub Q2)"
| "sub (Exists z Q) = insert (Exists z Q) (sub Q)"

lemma cpropagated_sub: "cpropagated Q ⟹ Q' ∈ sub Q ⟹ cpropagated Q'"
  by (induct Q) auto

lemma Exists_in_sub_cp_foldr_Disj:
  "Exists x Q' ∈ sub (cp (foldr Disj Qs Q)) ⟹ Exists x Q' ∈ sub (cp Q) ∨ (∃Q ∈ set Qs. Exists x Q' ∈ sub (cp Q))"
  by (induct Qs arbitrary: Q) (auto simp: Let_def split: if_splits)

lemma Exists_in_sub_cp_foldr1_Disj:
  "Exists x Q' ∈ sub (cp (foldr1 Disj Qs Q)) ⟹ Qs = [] ∧ Exists x Q' ∈ sub (cp Q) ∨ (∃Q ∈ set Qs. Exists x Q' ∈ sub (cp Q))"
  by (cases Qs) (auto simp: Exists_in_sub_cp_foldr_Disj)

lemma Exists_in_sub_cp_DISJ: "Exists x Q' ∈ sub (cp (DISJ 𝒬)) ⟹ finite 𝒬 ⟹ (∃Q ∈ 𝒬. Exists x Q' ∈ sub (cp Q))"
  unfolding DISJ_def by (drule Exists_in_sub_cp_foldr1_Disj) auto

lemma Exists_in_sub_foldr_Disj:
  "Exists x Q' ∈ sub (foldr Disj Qs Q) ⟹ Exists x Q' ∈ sub Q ∨ (∃Q ∈ set Qs. Exists x Q' ∈ sub Q)"
  by (induct Qs arbitrary: Q) (auto simp: Let_def split: if_splits)

lemma Exists_in_sub_foldr1_Disj:
  "Exists x Q' ∈ sub (foldr1 Disj Qs Q) ⟹ Qs = [] ∧ Exists x Q' ∈ sub Q ∨ (∃Q ∈ set Qs. Exists x Q' ∈ sub Q)"
  by (cases Qs) (auto simp: Exists_in_sub_foldr_Disj)

lemma Exists_in_sub_DISJ: "Exists x Q' ∈ sub (DISJ 𝒬) ⟹ finite 𝒬 ⟹ (∃Q ∈ 𝒬. Exists x Q' ∈ sub Q)"
  unfolding DISJ_def by (drule Exists_in_sub_foldr1_Disj) auto

subsection ‹Substitution›

fun subst_term ("_[_ →t _]" [90, 0, 0] 91) where
  "Var z[x →t y] = Var (if x = z then y else z)"
| "Const c[x →t y] = Const c"

abbreviation substs_term ("_[_ →t* _]" [90, 0, 0] 91) where
  "t[xs →t* ys] ≡ fold (λ(x, y) t. t[x →t y]) (zip xs ys) t"

lemma size_subst_term[simp]: "size (t[x →t y]) = size t"
  by (cases t) auto

lemma fv_subst_term[simp]: "fv_term_set (t[x →t y]) =
  (if x ∈ fv_term_set t then insert y (fv_term_set t - {x}) else fv_term_set t)"
  by (cases t) auto

definition "fresh2 x y Q = Suc (Max (insert x (insert y (fv Q))))"

function (sequential) subst :: "('a, 'b) fmla ⇒ nat ⇒ nat ⇒ ('a, 'b) fmla" ("_[_ → _]" [90, 0, 0] 91) where
  "Bool t[x → y] = Bool t"
| "Pred p ts[x → y] = Pred p (map (λt. t[x →t y]) ts)"
| "Eq z t[x → y] = Eq (if z = x then y else z) (t[x →t y])"
| "Neg Q[x → y] = Neg (Q[x → y])"
| "Conj Q1 Q2[x → y] = Conj (Q1[x → y]) (Q2[x → y])"
| "Disj Q1 Q2[x → y] = Disj (Q1[x → y]) (Q2[x → y])"
| "Exists z Q[x → y] = (if x = z then Exists x Q else
    if z = y then let z' = fresh2 x y Q in Exists z' (Q[z → z'][x → y]) else Exists z (Q[x → y]))"
  by pat_completeness auto

abbreviation substs ("_[_ →* _]" [90, 0, 0] 91) where
  "Q[xs →* ys] ≡ fold (λ(x, y) Q. Q[x → y]) (zip xs ys) Q"

lemma size_subst_p[simp]: "subst_dom (Q, x, y) ⟹ size (Q[x → y]) = size Q"
  by (induct Q x y rule: subst.pinduct) (auto simp: subst.psimps o_def Let_def exists_def)

termination by lexicographic_order

lemma size_subst[simp]: "size (Q[x → y]) = size Q"
  by (induct Q x y rule: subst.induct) (auto simp: o_def Let_def exists_def)

lemma fresh2_gt:
  "x < fresh2 x y Q"
  "y < fresh2 x y Q"
  "z ∈ fv Q ⟹ z < fresh2 x y Q"
  unfolding fresh2_def less_Suc_eq_le
  by (auto simp: max_def Max_ge_iff)

lemma fresh2:
  "x ≠ fresh2 x y Q"
  "y ≠ fresh2 x y Q"
  "fresh2 x y Q ∉ fv Q"
  using fresh2_gt(1)[of x y Q] fresh2_gt(2)[of y x Q] fresh2_gt(3)[of "fresh2 x y Q" Q x y]
  by auto

lemma fv_subst:
  "fv (Q[x → y]) = (if x ∈ fv Q then insert y (fv Q - {x}) else fv Q)"
  by (induct Q x y rule: subst.induct)
    (auto simp:  fv_terms_set_def Let_def fresh2 split: if_splits)

lemma subst_term_triv: "x ∉ fv_term_set t ⟹ t[x →t y] = t"
  by (cases t) auto

lemma subst_exists: "exists z Q[x → y] = (if z ∈ fv Q then if x = z then exists x Q else
    if z = y then let z' = fresh2 x y Q in exists z' (Q[z → z'][x → y]) else exists z (Q[x → y]) else Q[x → y])"
  by (auto simp: exists_def Let_def fv_subst fresh2 dest: sym)

lemma eval_subst[simp]: "σ ⋅ t[x →t y] = σ(x := σ y) ⋅ t"
  by (cases t) auto

lemma sat_subst[simp]: "sat (Q[x → y]) I σ = sat Q I (σ(x := σ y))"
  by (induct Q x y arbitrary: σ rule: subst.induct)
    (auto 0 3 simp: eval_terms_def o_def Let_def fun_upd_twist[symmetric] sat_fun_upd fresh2 dest: sym)

lemma substs_Bool[simp]: "length xs = length ys ⟹ Bool b[xs →* ys] = Bool b"
  by (induct xs ys rule: list_induct2) auto

lemma substs_Neg[simp]: "length xs = length ys ⟹ Neg Q[xs →* ys] = Neg (Q[xs →* ys])"
  by (induct xs ys arbitrary: Q rule: list_induct2) (auto simp: Let_def)

lemma substs_Conj[simp]: "length xs = length ys ⟹ Conj Q1 Q2[xs →* ys] = Conj (Q1[xs →* ys]) (Q2[xs →* ys])"
  by (induct xs ys arbitrary: Q1 Q2 rule: list_induct2) auto

lemma substs_Disj[simp]: "length xs = length ys ⟹ Disj Q1 Q2[xs →* ys] = Disj (Q1[xs →* ys]) (Q2[xs →* ys])"
  by (induct xs ys arbitrary: Q1 Q2 rule: list_induct2) auto

fun substs_bd where
  "substs_bd z (x # xs) (y # ys) Q = (if x = z then substs_bd z xs ys Q else
     if z = y then substs_bd (fresh2 x y Q) xs ys (Q[y → fresh2 x y Q][x → y]) else substs_bd z xs ys (Q[x → y]))"
| "substs_bd z _ _ _ = z"

fun substs_src where
  "substs_src z (x # xs) (y # ys) Q = (if x = z then substs_src z xs ys Q else
     if z = y then [y, x] @ substs_src (fresh2 x y Q) xs ys (Q[y → fresh2 x y Q][x → y]) else x # substs_src z xs ys (Q[x → y]))"
| "substs_src _ _ _ _ = []"

fun substs_dst where
  "substs_dst z (x # xs) (y # ys) Q = (if x = z then substs_dst z xs ys Q else
     if z = y then [fresh2 x y Q, y] @ substs_dst (fresh2 x y Q) xs ys (Q[y → fresh2 x y Q][x → y]) else y # substs_dst z xs ys (Q[x → y]))"
| "substs_dst _ _ _ _ = []"

lemma length_substs[simp]: "length xs = length ys ⟹ length (substs_src z xs ys Q) = length (substs_dst z xs ys Q)"
  by (induct xs ys arbitrary: z Q rule: list_induct2) auto

lemma substs_Exists[simp]: "length xs = length ys ⟹
  Exists z Q[xs →* ys] = Exists (substs_bd z xs ys Q) (Q[substs_src z xs ys Q →* substs_dst z xs ys Q])"
  by (induct xs ys arbitrary: Q z rule: list_induct2) (auto simp: Let_def intro: exI[of _ "[]"])

fun subst_var where
  "subst_var (x # xs) (y # ys) z = (if x = z then subst_var xs ys y else subst_var xs ys z)"
| "subst_var _ _ z = z"

lemma substs_Eq[simp]: "length xs = length ys ⟹ (Eq x t)[xs →* ys] = Eq (subst_var xs ys x) (t[xs →t* ys])"
  by (induct xs ys arbitrary: x t rule: list_induct2) auto

lemma substs_term_Var[simp]: "length xs = length ys ⟹ (Var x)[xs →t* ys] = Var (subst_var xs ys x)"
  by (induct xs ys arbitrary: x rule: list_induct2) auto

lemma substs_term_Const[simp]: "length xs = length ys ⟹ (Const c)[xs →t* ys] = Const c"
  by (induct xs ys rule: list_induct2) auto

lemma in_fv_substs:
  "length xs = length ys ⟹ x ∈ fv Q ⟹ subst_var xs ys x ∈ fv (Q[xs →* ys])"
  by (induct xs ys arbitrary: x Q rule: list_induct2) (auto simp: fv_subst)

lemma exists_cp_subst: "x ≠ y ⟹ exists x (cp (Q[x → y])) = cp (Q[x → y])"
  by (auto simp: exists_def fv_subst dest!: set_mp[OF fv_cp] split: if_splits)

subsection ‹Generated Variables›

inductive ap where
  Pred: "ap (Pred p ts)"
| Eqc: "ap (Eq x (Const c))"

inductive gen where
  "gen x (Bool False) {}"
| "ap Q ⟹ x ∈ fv Q ⟹ gen x Q {Q}"
| "gen x Q G ⟹ gen x (Neg (Neg Q)) G"
| "gen x (Conj (Neg Q1) (Neg Q2)) G ⟹ gen x (Neg (Disj Q1 Q2)) G"
| "gen x (Disj (Neg Q1) (Neg Q2)) G ⟹ gen x (Neg (Conj Q1 Q2)) G"
| "gen x Q1 G1 ⟹ gen x Q2 G2 ⟹ gen x (Disj Q1 Q2) (G1 ∪ G2)"
| "gen x Q1 G ∨ gen x Q2 G ⟹ gen x (Conj Q1 Q2) G"
| "gen y Q G ⟹ gen x (Conj Q (x ≈ y)) ((λQ. cp (Q[y → x])) ` G)"
| "gen y Q G ⟹ gen x (Conj Q (y ≈ x)) ((λQ. cp (Q[y → x])) ` G)"
| "x ≠ y ⟹ gen x Q G ⟹  gen x (Exists y Q) (exists y ` G)"

inductive gen' where
  "gen' x (Bool False) {}"
| "ap Q ⟹ x ∈ fv Q ⟹ gen' x Q {Q}"
| "gen' x Q G ⟹ gen' x (Neg (Neg Q)) G"
| "gen' x (Conj (Neg Q1) (Neg Q2)) G ⟹ gen' x (Neg (Disj Q1 Q2)) G"
| "gen' x (Disj (Neg Q1) (Neg Q2)) G ⟹ gen' x (Neg (Conj Q1 Q2)) G"
| "gen' x Q1 G1 ⟹ gen' x Q2 G2 ⟹ gen' x (Disj Q1 Q2) (G1 ∪ G2)"
| "gen' x Q1 G ∨ gen' x Q2 G ⟹ gen' x (Conj Q1 Q2) G"
| "gen' y Q G ⟹ gen' x (Conj Q (x ≈ y)) ((λQ. Q[y → x]) ` G)"
| "gen' y Q G ⟹ gen' x (Conj Q (y ≈ x)) ((λQ. Q[y → x]) ` G)"
| "x ≠ y ⟹ gen' x Q G ⟹  gen' x (Exists y Q) (exists y ` G)"

inductive qp where
  ap: "ap Q ⟹ qp Q"
| exists: "qp Q ⟹ qp (exists x Q)"

lemma qp_Exists: "qp Q ⟹ x ∈ fv Q ⟹ qp (Exists x Q)"
  by (metis qp.exists exists_def)

lemma qp_ExistsE: "qp (Exists x Q) ⟹ (qp Q ⟹ x ∈ fv Q ⟹ R) ⟹ R"
  by (induct "Exists x Q" rule: qp.induct) (auto elim!: ap.cases simp: exists_def split: if_splits)

fun qp_impl where
  "qp_impl (Eq x (Const c)) = True"
| "qp_impl (Pred x ts) = True"
| "qp_impl (Exists x Q) = (x ∈ fv Q ∧ qp Q)"
| "qp_impl _ = False"

lemma qp_imp_qp_impl: "qp Q ⟹ qp_impl Q"
  by (induct Q rule: qp.induct) (auto elim!: ap.cases simp: exists_def)

lemma qp_impl_imp_qp: "qp_impl Q ⟹ qp Q"
  by (induct Q rule: qp_impl.induct) (auto intro: ap.intros qp_Exists qp.ap)

lemma qp_code[code]: "qp Q = qp_impl Q"
  using qp_imp_qp_impl qp_impl_imp_qp by blast

lemma ap_cp: "ap Q ⟹ ap (cp Q)"
  by (induct Q rule: ap.induct) (auto intro: ap.intros)

lemma qp_cp: "qp Q ⟹ qp (cp Q)"
  by (induct Q rule: qp.induct) (auto intro: qp.intros ap_cp)

lemma ap_substs: "ap Q ⟹ length xs = length ys ⟹ ap (Q[xs →* ys])"
proof (induct Q arbitrary: xs ys rule: ap.induct)
  case (Pred p ts)
  then show ?case
    by (induct xs ys arbitrary: ts rule: list_induct2) (auto intro!: ap.intros)
next
  case (Eqc x c)
  then show ?case
    by (induct xs ys arbitrary: x rule: list_induct2) (auto intro!: ap.intros)
qed

lemma ap_subst': "ap (Q[x → y]) ⟹ ap Q"
proof (induct "Q[x → y]" arbitrary: Q rule: ap.induct)
  case (Pred p ts)
  then show ?case
    by (cases Q) (auto simp: Let_def split: if_splits intro: ap.intros)
next
  case (Eqc x c)
  then show ?case
  proof (cases Q)
    case (Eq x t)
    with Eqc show ?thesis
      by (cases t) (auto intro: ap.intros)
  qed (auto simp: Let_def split: if_splits)
qed

lemma qp_substs: "qp Q ⟹ length xs = length ys ⟹ qp (Q[xs →* ys])"
proof (induct Q arbitrary: xs ys rule: qp.induct)
  case (ap Q)
  then show ?case
    by (rule qp.ap[OF ap_substs])
next
  case (exists Q z)
  from exists(3,1,2) show ?case
  proof (induct xs ys arbitrary: Q z rule: list_induct2)
    case Nil
    then show ?case
      by (auto intro: qp.intros)
  next
    case (Cons x xs y ys)
    have [simp]: "Q[x → y][xs →* ys] = Q[x # xs →* y # ys]" for Q :: "('a, 'b) fmla" and x y xs ys
      by auto
    have IH1[simp]: "qp (Q[x → y])" for x y
      using Cons(4)[of "[x]" "[y]"] by auto
    have IH2[simp]: "qp (Q[x → y][a → b])" for x y a b
      using Cons(4)[of "[x, a]" "[y, b]"] by auto
    note zip_Cons_Cons[simp del]
    show ?case
      unfolding zip_Cons_Cons fold.simps prod.case o_apply subst_exists using Cons(1,3)
      by (auto simp: Let_def intro!: qp.intros(2) Cons(2,4))
  qed
qed

lemma qp_subst: "qp Q ⟹ qp (Q[x → y])"
  using qp_substs[of Q "[x]" "[y]"] by auto

lemma qp_Neg[dest]: "qp (Neg Q) ⟹ False"
  by (rule qp.induct[where P = "λQ'. Q' = Neg Q ⟶ False", THEN mp]) (auto elim!: ap.cases simp: exists_def)

lemma qp_Disj[dest]: "qp (Disj Q1 Q2) ⟹ False"
  by (rule qp.induct[where P = "λQ. Q = Disj Q1 Q2 ⟶ False", THEN mp]) (auto elim!: ap.cases simp: exists_def)

lemma qp_Conj[dest]: "qp (Conj Q1 Q2) ⟹ False"
  by (rule qp.induct[where P = "λQ. Q = Conj Q1 Q2 ⟶ False", THEN mp]) (auto elim!: ap.cases simp: exists_def)

lemma qp_eq[dest]: "qp (x ≈ y) ⟹ False"
  by (rule qp.induct[where P = "λQ. (∃x y. Q = x ≈ y) ⟶ False", THEN mp]) (auto elim!: ap.cases simp: exists_def)

lemma qp_subst': "qp (Q[x → y]) ⟹ qp Q"
proof (induct Q x y rule: subst.induct)
  case (3 z t x y)
  then show ?case
    by (cases t) (auto intro!: ap Eqc split: if_splits)
qed (auto 0 3 simp: qp_Exists fv_subst Let_def fresh2 Pred ap dest: sym elim!: qp_ExistsE split: if_splits)

lemma qp_subst_eq[simp]: "qp (Q[x → y]) = qp Q"
  using qp_subst qp_subst' by blast

lemma gen_qp: "gen x Q G ⟹ Qqp ∈ G ⟹ qp Qqp"
  by (induct x Q G arbitrary: Qqp rule: gen.induct) (auto intro: qp.intros ap.intros qp_cp)

lemma gen'_qp: "gen' x Q G ⟹ Qqp ∈ G ⟹ qp Qqp"
  by (induct x Q G arbitrary: Qqp rule: gen'.induct) (auto intro: qp.intros ap.intros)

lemma ap_cp_triv: "ap Q ⟹ cp Q = Q"
  by (induct Q rule: ap.induct) auto

lemma qp_cp_triv: "qp Q ⟹ cp Q = Q"
  by (induct Q rule: qp.induct) (auto simp: ap_cp_triv)

lemma ap_cp_subst_triv: "ap Q ⟹ cp (Q[x → y]) = Q[x → y]"
  by (induct Q rule: ap.induct) auto

lemma qp_cp_subst_triv: "qp Q ⟹ cp (Q[x → y]) = Q[x → y]"
  by (induct Q rule: qp.induct)
    (auto simp: exists_def qp_cp_triv Let_def fv_subst fresh2 ap_cp_subst_triv dest: sym)

lemma gen_nocp_intros:
  "gen y Q G ⟹ gen x (Conj Q (x ≈ y)) ((λQ. Q[y → x]) ` G)"
  "gen y Q G ⟹ gen x (Conj Q (y ≈ x)) ((λQ. Q[y → x]) ` G)"
  by (metis (no_types, lifting) gen.intros(8) gen_qp image_cong qp_cp_subst_triv,
      metis (no_types, lifting) gen.intros(9) gen_qp image_cong qp_cp_subst_triv)

lemma gen'_cp_intros:
  "gen' y Q G ⟹ gen' x (Conj Q (x ≈ y)) ((λQ. cp (Q[y → x])) ` G)"
  "gen' y Q G ⟹ gen' x (Conj Q (y ≈ x)) ((λQ. cp (Q[y → x])) ` G)"
  by (metis (no_types, lifting) gen'.intros(8) gen'_qp image_cong qp_cp_subst_triv,
      metis (no_types, lifting) gen'.intros(9) gen'_qp image_cong qp_cp_subst_triv)

lemma gen'_gen: "gen' x Q G ⟹ gen x Q G"
  by (induct x Q G rule: gen'.induct) (auto intro!: gen.intros gen_nocp_intros)

lemma gen_gen': "gen x Q G ⟹ gen' x Q G"
  by (induct x Q G rule: gen.induct) (auto intro!: gen'.intros gen'_cp_intros)

lemma gen_eq_gen': "gen = gen'"
  using gen'_gen gen_gen' by blast

lemmas gen_induct[consumes 1] = gen'.induct[folded gen_eq_gen']

abbreviation Gen where "Gen x Q ≡ (∃G. gen x Q G)"

lemma qp_Gen: "qp Q ⟹ x ∈ fv Q ⟹ Gen x Q"
  by (induct Q rule: qp.induct) (force simp: exists_def intro: gen.intros)+

lemma qp_gen: "qp Q ⟹ x ∈ fv Q ⟹ gen x Q {Q}"
  by (induct Q rule: qp.induct)
    (force simp: exists_def intro: gen.intros dest: gen.intros(10))+

lemma gen_foldr_Disj:
  "list_all2 (gen x) Qs Gs ⟹ gen x Q G ⟹ GG = G ∪ (⋃G ∈ set Gs. G) ⟹
  gen x (foldr Disj Qs Q) GG"
proof (induct Qs Gs arbitrary: Q G GG rule: list.rel_induct)
  case (Cons Q' Qs G' Gs)
  then have GG: "GG = G' ∪ (G ∪ (⋃G ∈ set Gs. G))"
    by auto
  from Cons(1,3-) show ?case
    unfolding foldr.simps o_apply GG
    by (intro gen.intros Cons(2)[OF _ refl]) auto
qed simp

lemma gen_foldr1_Disj:
  "list_all2 (gen x) Qs Gs ⟹ gen x Q G ⟹ GG = (if Qs = [] then G else (⋃G ∈ set Gs. G)) ⟹
  gen x (foldr1 Disj Qs Q) GG"
  by (erule list.rel_cases) (auto simp: gen_foldr_Disj)

lemma gen_Bool_True[simp]: "gen x (Bool True) G = False"
  by (auto elim: gen.cases)

lemma gen_Bool_False[simp]: "gen x (Bool False) G = (G = {})"
  by (auto elim: gen.cases intro: gen.intros)

lemma gen_Gen_cp: "gen x Q G ⟹ Gen x (cp Q)"
  by (induct x Q G rule: gen_induct)
    (auto split: if_splits simp: Let_def ap_cp_triv is_Bool_def exists_def intro: gen.intros)

lemma Gen_cp: "Gen x Q ⟹ Gen x (cp Q)"
  by (metis gen_Gen_cp)

lemma Gen_DISJ: "finite 𝒬 ⟹ ∀Q ∈ 𝒬. qp Q ∧ x ∈ fv Q ⟹ Gen x (DISJ 𝒬)"
  unfolding DISJ_def
  by (rule exI gen_foldr1_Disj[where Gs="map (λQ. {Q}) (sorted_list_of_set 𝒬)" and G="{}"])+
    (auto simp: list.rel_map qp_cp_triv qp_gen gen.intros intro!: list.rel_refl_strong)

lemma Gen_cp_DISJ: "finite 𝒬 ⟹ ∀Q ∈ 𝒬. qp Q ∧ x ∈ fv Q ⟹ Gen x (cp (DISJ 𝒬))"
  by (rule Gen_cp Gen_DISJ)+

lemma gen_Pred[simp]:
  "gen z (Pred p ts) G ⟷ z ∈ fv_terms_set ts ∧ G = {Pred p ts}"
  by (auto elim: gen.cases intro: gen.intros ap.intros)

lemma gen_Eq[simp]:
  "gen z (Eq a t) G ⟷ z = a ∧ (∃c. t = Const c ∧ G = {Eq a t})"
  by (auto elim: gen.cases elim!: ap.cases intro: gen.intros ap.intros)

lemma gen_empty_cp: "gen z Q G ⟹ G = {} ⟹ cp Q = Bool False"
  by (induct z Q G rule: gen_induct)
    (fastforce simp: Let_def exists_def split: if_splits)+

inductive genempty where
  "genempty (Bool False)"
| "genempty Q ⟹ genempty (Neg (Neg Q))"
| "genempty (Conj (Neg Q1) (Neg Q2)) ⟹ genempty (Neg (Disj Q1 Q2))"
| "genempty (Disj (Neg Q1) (Neg Q2)) ⟹ genempty (Neg (Conj Q1 Q2))"
| "genempty Q1 ⟹ genempty Q2 ⟹ genempty (Disj Q1 Q2)"
| "genempty Q1 ∨ genempty Q2 ⟹ genempty (Conj Q1 Q2)"
| "genempty Q ⟹ genempty (Conj Q (x ≈ y))"
| "genempty Q ⟹ genempty (Conj Q (y ≈ x))"
| "genempty Q ⟹ genempty (Exists y Q)"

lemma gen_genempty: "gen z Q G ⟹ G = {} ⟹ genempty Q"
  by (induct z Q G rule: gen.induct) (auto intro: genempty.intros)

lemma genempty_substs: "genempty Q ⟹ length xs = length ys ⟹ genempty (Q[xs →* ys])"
  by (induct Q arbitrary: xs ys rule: genempty.induct) (auto intro: genempty.intros)

lemma genempty_substs_Exists: "genempty Q ⟹ length xs = length ys ⟹ genempty (Exists y Q[xs →* ys])"
  by (auto intro!: genempty.intros genempty_substs)

lemma genempty_cp: "genempty Q ⟹ cp Q = Bool False"
  by (induct Q rule: genempty.induct)
    (auto simp: Let_def exists_def split: if_splits)

lemma gen_empty_cp_substs:
  "gen x Q {} ⟹ length xs = length ys ⟹ cp (Q[xs →* ys]) = Bool False"
  by (rule genempty_cp[OF genempty_substs[OF gen_genempty[OF _ refl]]])

lemma gen_empty_cp_substs_Exists:
  "gen x Q {} ⟹ length xs = length ys ⟹ cp (Exists y Q[xs →* ys]) = Bool False"
  by (rule genempty_cp[OF genempty_substs_Exists[OF gen_genempty[OF _ refl]]])

lemma gen_Gen_substs_Exists:
  "length xs = length ys ⟹ x ≠ y ⟹ x ∈ fv Q ⟹
   (⋀xs ys. length xs = length ys ⟹ Gen (subst_var xs ys x) (cp (Q[xs →* ys]))) ⟹
   Gen (subst_var xs ys x) (cp (Exists y Q[xs →* ys]))"
proof (induct xs ys arbitrary: y x Q rule: list_induct2)
  case Nil
  from Nil(1) Nil(3)[of "[]" "[]"] show ?case
    by (auto simp: exists_def intro: gen.intros)
next
  case (Cons xx xs yy ys)
  have "Gen (subst_var xs ys yy) (cp (Q[[y,x]@xs →* [fresh2 x y Q,yy]@ys]))"
    if "length xs = length ys" and "x ≠ y" for xs ys
    using Cons(5)[of "[y,x]@xs" "[fresh2 x y Q,yy]@ys"] that Cons.prems by auto
  moreover have "Gen (subst_var xs ys x) (cp (Q[[yy,xx]@xs →* [fresh2 xx yy Q,yy]@ys]))"
    if "length xs = length ys" "x ≠ yy" "x ≠ xx" for xs ys
    using Cons(5)[of "[yy,xx]@xs" "[fresh2 xx yy Q,yy]@ys"] that Cons.prems by auto
  moreover have "Gen (subst_var xs ys yy) (cp (Q[[x]@xs →* [yy]@ys]))"
    if "length xs = length ys" and "x = xx" for xs ys
    using Cons(5)[of "[x]@xs" "[yy]@ys"] that Cons.prems by auto
  moreover have "Gen (subst_var xs ys x) (cp (Q[[xx]@xs →* [yy]@ys]))"
    if "length xs = length ys" and "x ≠ xx" for xs ys
    using Cons(5)[of "[xx]@xs" "[yy]@ys"] that Cons.prems by auto
  ultimately show ?case using Cons
    by (auto simp: Let_def fresh2 fv_subst intro: Cons(2) simp del: substs_Exists split: if_splits)
qed

lemma gen_fv:
  "gen x Q G ⟹ Qqp ∈ G ⟹ x ∈ fv Qqp ∧ fv Qqp ⊆ fv Q"
  by (induct x Q G arbitrary: Qqp rule: gen_induct)
    (force simp: fv_subst dest: fv_cp[THEN set_mp])+

lemma gen_sat:
  fixes x :: nat
  shows "gen x Q G ⟹ sat Q I σ ⟹ ∃Qqp ∈ G. sat Qqp I σ"
  by (induct x Q G arbitrary: σ rule: gen_induct)
    (auto 6 0 simp: fun_upd_idem intro: UnI1 UnI2)

subsection ‹Variable Erasure›

fun erase :: "('a, 'b) fmla ⇒ nat ⇒ ('a, 'b) fmla" (infix "⊥" 65) where
  "Bool t ⊥ x = Bool t"
| "Pred p ts ⊥ x = (if x ∈ fv_terms_set ts then Bool False else Pred p ts)"
| "Eq z t ⊥ x = (if t = Var z then Bool True else
     if x = z ∨ x ∈ fv_term_set t then Bool False else Eq z t)"
| "Neg Q ⊥ x = Neg (Q ⊥ x)"
| "Conj Q1 Q2 ⊥ x = Conj (Q1 ⊥ x) (Q2 ⊥ x)"
| "Disj Q1 Q2 ⊥ x = Disj (Q1 ⊥ x) (Q2 ⊥ x)"
| "Exists z Q ⊥ x = (if x = z then Exists x Q else Exists z (Q ⊥ x))"

lemma fv_erase: "fv (Q ⊥ x) ⊆ fv Q - {x}"
  by (induct Q) auto

lemma ap_cp_erase: "ap Q ⟹ x ∈ fv Q ⟹ cp (Q ⊥ x) = Bool False"
  by (induct Q rule: ap.induct) auto

lemma qp_cp_erase: "qp Q ⟹ x ∈ fv Q ⟹ cp (Q ⊥ x) = Bool False"
  by (induct Q rule: qp.induct) (auto simp: exists_def ap_cp_erase split: if_splits)

lemma sat_erase: "sat (Q ⊥ x) I (σ(x := z)) = sat (Q ⊥ x) I σ"
  by (rule sat_fun_upd) (auto dest: fv_erase[THEN set_mp])

lemma exists_cp_erase: "exists x (cp (Q ⊥ x)) = cp (Q ⊥ x)"
  by (auto simp: exists_def dest: set_mp[OF fv_cp] set_mp[OF fv_erase])

lemma gen_cp_erase:
  fixes x :: nat
  shows "gen x Q G ⟹ Qqp ∈ G ⟹ cp (Qqp ⊥ x) = Bool False"
  by (metis gen_qp qp_cp_erase gen_fv)

subsection ‹Generated Variables and Substitutions›

lemma gen_Gen_cp_substs: "gen z Q G ⟹ length xs = length ys ⟹
  Gen (subst_var xs ys z) (cp (Q[xs →* ys]))"
proof (induct z Q G arbitrary: xs ys rule: gen_induct)
  case (2 Q x)
  show ?case
    by (subst ap_cp_triv) (rule exI gen.intros(2) ap_substs 2 in_fv_substs)+
next
  case (3 x Q G)
  then show ?case
    by (fastforce simp: Let_def intro: gen.intros)
next
  case (4 x Q1 Q2 G)
  from 4(2)[of xs ys] 4(1,3) show ?case
    by (auto simp: Let_def is_Bool_def intro!: gen.intros(4) split: if_splits)
next
  case (5 x Q1 Q2 G)
  from 5(2)[of xs ys] 5(1,3) show ?case
    by (auto simp: Let_def is_Bool_def intro!: gen.intros(5) split: if_splits)
next
  case (6 x Q1 G1 Q2 G2)
  from 6(2,4)[of xs ys] 6(1,3,5) show ?case
    by (auto simp: Let_def is_Bool_def intro!: gen.intros(6) split: if_splits)
next
  case (7 x Q1 G Q2)
  from 7(1) show ?case
  proof (elim disjE conjE, goal_cases L R)
    case L
    from L(1) L(2)[rule_format, of xs ys] 7(2) show ?case
    by (auto simp: Let_def is_Bool_def intro!: gen.intros(7) split: if_splits)
  next
    case R
    from R(1) R(2)[rule_format, of xs ys] 7(2) show ?case
    by (auto simp: Let_def is_Bool_def intro!: gen.intros(7) split: if_splits)
  qed
next
  case (8 y Q G x)
  from 8(2)[of xs ys] 8(1,3) show ?case
    by (auto simp: Let_def is_Bool_def intro!: gen.intros(8) split: if_splits)
next
  case (9 y Q G x)
  from 9(2)[of xs ys] 9(1,3) show ?case
    by (auto simp: Let_def is_Bool_def intro!: gen.intros(9) split: if_splits)
next
  case (10 x y Q G)
  show ?case
  proof (cases "x ∈ fv Q")
    case True
    with 10(4,1) show ?thesis using 10(3)
      by (rule gen_Gen_substs_Exists)
  next
    case False
    with 10(2) have "G = {}"
      by (auto dest: gen_fv)
    with 10(2,4) have "cp (Q[xs →* ys]) = Bool False"
      by (auto intro!: gen_empty_cp_substs[of x])
    with 10(2,4) have "cp (Exists y Q[xs →* ys]) = Bool False" unfolding ‹G = {}›
      by (intro gen_empty_cp_substs_Exists)
    then show ?thesis
      by auto
  qed
qed (fastforce simp: Let_def is_Bool_def intro!: gen.intros split: if_splits)+

lemma Gen_cp_substs: "Gen z Q ⟹ length xs = length ys ⟹ Gen (subst_var xs ys z) (cp (Q[xs →* ys]))"
  by (blast intro: gen_Gen_cp_substs)

lemma Gen_cp_subst: "Gen z Q ⟹ z ≠ x ⟹ Gen z (cp (Q[x → y]))"
  using Gen_cp_substs[of z Q "[x]" "[y]"] by auto

lemma substs_bd_fv: "length xs = length ys ⟹ substs_bd z xs ys Q ∈ fv (Q[substs_src z xs ys Q →* substs_dst z xs ys Q]) ⟹ z ∈ fv Q"
proof (induct xs ys arbitrary: z Q rule: list_induct2)
  case (Cons x xs y ys)
  from Cons(1,3) show ?case
    by (auto 0 4 simp: fv_subst fresh2 dest: Cons(2) sym split: if_splits)
qed simp

lemma Gen_substs_bd: "length xs = length ys ⟹
  (⋀xs ys. length xs = length ys ⟹ Gen (subst_var xs ys z) (cp (Qz[xs →* ys]))) ⟹
  Gen (substs_bd z xs ys Qz) (cp (Qz[substs_src z xs ys Qz →* substs_dst z xs ys Qz]))"
proof (induct xs ys arbitrary: z Qz rule: list_induct2)
  case Nil
  from Nil(1)[of "[]" "[]"] show ?case
    by simp
next
  case (Cons x xs y ys)
  have "Gen (subst_var xs ys (fresh2 x y Qz)) (cp (Qz[y → fresh2 x y Qz][x → y][xs →* ys]))"
    if "length xs = length ys" "z = y" for xs ys
    using that Cons(3)[of "[y,x]@xs" "[fresh2 x y Qz,y]@ys"]
    by (auto simp: fresh2)
  moreover have "Gen (subst_var xs ys z) (cp (Qz[x → y][xs →* ys]))"
    if "length xs = length ys" "x ≠ z" for xs ys
    using that Cons(3)[of "[x]@xs" "[y]@ys"]
    by (auto simp: fresh2)
  ultimately show ?case using Cons(1,3)
    by (auto intro!: Cons(2))
qed

subsection ‹Safe-Range Queries›

definition nongens where
  "nongens Q = {x ∈ fv Q. ¬ Gen x Q}"

abbreviation rrf where
  "rrf Q ≡ nongens Q = {}"

definition rrb where
  "rrb Q = (∀y Qy. Exists y Qy ∈ sub Q ⟶ Gen y Qy)"

lemma rrb_simps[simp]:
  "rrb (Bool b) = True"
  "rrb (Pred p ts) = True"
  "rrb (Eq x t) = True"
  "rrb (Neg Q) = rrb Q"
  "rrb (Disj Q1 Q2) = (rrb Q1 ∧ rrb Q2)"
  "rrb (Conj Q1 Q2) = (rrb Q1 ∧ rrb Q2)"
  "rrb (Exists y Qy) = (Gen y Qy ∧ rrb Qy)"
  "rrb (exists y Qy) = ((y ∈ fv Qy ⟶ Gen y Qy) ∧ rrb Qy)"
  by (auto simp: rrb_def exists_def)

lemma ap_rrb[simp]: "ap Q ⟹ rrb Q"
  by (cases Q rule: ap.cases) auto

lemma qp_rrb[simp]: "qp Q ⟹ rrb Q"
  by (induct Q rule: qp.induct) (auto simp: qp_Gen)

lemma rrb_cp: "rrb Q ⟹ rrb (cp Q)"
  by (induct Q rule: cp.induct)
    (auto split: term.splits simp: Let_def exists_def Gen_cp dest!: fv_cp[THEN set_mp])

lemma gen_Gen_erase: "gen x Q G ⟹ Gen x (Q ⊥ z)"
  by (induct x Q G rule: gen_induct)
    (auto 0 4 intro: gen.intros qp.intros ap.intros elim!: ap.cases)

lemma Gen_erase: "Gen x Q ⟹ Gen x (Q ⊥ z)"
  by (metis gen_Gen_erase)

lemma rrb_erase: "rrb Q ⟹ rrb (Q ⊥ x)"
  by (induct Q x rule: erase.induct)
    (auto split: term.splits simp: Let_def exists_def Gen_erase dest!: fv_cp[THEN set_mp])

lemma rrb_DISJ[simp]: "finite 𝒬 ⟹ (∀Q ∈ 𝒬. rrb Q) ⟹ rrb (DISJ 𝒬)"
  by (auto simp: rrb_def dest!: Exists_in_sub_DISJ)

lemma rrb_cp_substs: "rrb Q ⟹ length xs = length ys ⟹ rrb (cp (Q[xs →* ys]))"
proof (induct "size Q" arbitrary: Q xs ys rule: less_induct)
  case less
  then show ?case
  proof (cases Q)
    case (Exists z Qz)
    from less(2,3) show ?thesis
      unfolding Exists substs_Exists[OF less(3)] cp.simps rrb_simps
      by (intro conjI impI less(1) Gen_substs_bd Gen_cp_substs) (simp_all add: Exists)
  qed (auto simp: Let_def ap_cp ap_substs ap.intros split: term.splits)
qed

lemma rrb_cp_subst: "rrb Q ⟹ rrb (cp (Q[x → y]))"
  using rrb_cp_substs[of Q "[x]" "[y]"]
  by auto

definition "sr Q = (rrf Q ∧ rrb Q)"

lemma nongens_cp: "nongens (cp Q) ⊆ nongens Q"
  unfolding nongens_def by (auto dest: gen_Gen_cp fv_cp[THEN set_mp])

lemma sr_Disj: "fv Q1 = fv Q2 ⟹ sr (Disj Q1 Q2) = (sr Q1 ∧ sr Q2)"
  by (auto 0 4 simp: sr_def nongens_def elim!: ap.cases elim: gen.cases intro: gen.intros)

lemma sr_foldr_Disj: "∀Q' ∈ set Qs. fv Q' = fv Q  ⟹ sr (foldr Disj Qs Q) ⟷ (∀Q ∈ set Qs. sr Q) ∧ sr Q"
  by (induct Qs) (auto simp: sr_Disj)

lemma sr_foldr1_Disj: "∀Q' ∈ set Qs. fv Q' = X  ⟹ sr (foldr1 Disj Qs Q) ⟷ (if Qs = [] then sr Q else (∀Q ∈ set Qs. sr Q))"
  by (cases Qs) (auto simp: sr_foldr_Disj)

lemma sr_False[simp]: "sr (Bool False)"
  by (auto simp: sr_def nongens_def)

lemma sr_cp: "sr Q ⟹ sr (cp Q)"
  by (auto simp: rrb_cp sr_def dest: nongens_cp[THEN set_mp])

lemma sr_DISJ: "finite 𝒬 ⟹ ∀Q' ∈ 𝒬. fv Q' = X ⟹ (∀Q ∈ 𝒬. sr Q) ⟹ sr (DISJ 𝒬)"
  by (auto simp: DISJ_def sr_foldr1_Disj[of _ X] sr_cp)

lemma sr_Conj_eq: "sr Q ⟹ x ∈ fv Q ∨ y ∈ fv Q ⟹ sr (Conj Q (x ≈ y))"
  by (auto simp: sr_def nongens_def intro: gen.intros)

subsection ‹Simplification›

locale simplification =
  fixes simp :: "('a::{infinite, linorder}, 'b :: linorder) fmla ⇒ ('a, 'b) fmla"
    and simplified :: "('a, 'b) fmla ⇒ bool"
  assumes sat_simp: "sat (simp Q) I σ = sat Q I σ"
      and fv_simp: "fv (simp Q) ⊆ fv Q"
      and rrb_simp: "rrb Q ⟹ rrb (simp Q)"
      and gen_Gen_simp: "gen x Q G ⟹ Gen x (simp Q)"
      and fv_simp_Disj_same: "fv (simp Q1) = X ⟹ fv (simp Q2) = X ⟹ fv (simp (Disj Q1 Q2)) = X"
      and simp_False: "simp (Bool False) = Bool False"
      and simplified_sub: "simplified Q ⟹ Q' ∈ sub Q ⟹ simplified Q'"
      and simplified_Conj_eq: "simplified Q ⟹ x ≠ y ⟹ x ∈ fv Q ∨ y ∈ fv Q ⟹ simplified (Conj Q (x ≈ y))"
      and simplified_fv_simp: "simplified Q ⟹ fv (simp Q) = fv Q"
      and simplified_simp: "simplified (simp Q)"
      and simplified_cp: "simplified (cp Q)"
begin

lemma Gen_simp: "Gen x Q ⟹ Gen x (simp Q)"
  by (metis gen_Gen_simp)

lemma nongens_simp: "nongens (simp Q) ⊆ nongens Q"
  using Gen_simp by (auto simp: nongens_def dest!: fv_simp[THEN set_mp])

lemma sr_simp: "sr Q ⟹ sr (simp Q)"
  by (auto simp: rrb_simp sr_def dest: nongens_simp[THEN set_mp])

lemma equiv_simp_cong: "Q ≜ Q' ⟹ simp Q ≜ simp Q'"
  by (auto simp: equiv_def sat_simp)

lemma equiv_simp: "simp Q ≜ Q"
  by (auto simp: equiv_def sat_simp)

lemma fv_simp_foldr_Disj: "∀Q∈set Qs ∪ {Q}. simplified Q ∧ fv Q = A ⟹
  fv (simp (foldr Disj Qs Q)) = A"
  by (induct Qs) (auto simp: Let_def is_Bool_def simplified_fv_simp fv_simp_Disj_same)

lemma fv_simp_foldr1_Disj: "simp (foldr1 Disj Qs (Bool False)) ≠ Bool False ⟹
  ∀Q∈set Qs. simplified Q ∧ fv Q = A ⟹
  fv (simp (foldr1 Disj Qs (Bool False))) = A"
  by (cases Qs) (auto simp: fv_simp_foldr_Disj simp_False)

lemma fv_simp_DISJ_eq:
  "finite 𝒬 ⟹ simp (DISJ 𝒬) ≠ Bool False ⟹ ∀Q ∈ 𝒬. simplified Q ∧ fv Q = A ⟹ fv (simp (DISJ 𝒬)) = A"
  by (auto simp: DISJ_def fv_simp_foldr1_Disj)

end

subsection ‹Covered Variables›

inductive cov where
  Eq_self: "cov x (x ≈ x) {}"
| nonfree: "x ∉ fv Q ⟹ cov x Q {}"
| EqL: "x ≠ y ⟹ cov x (x ≈ y) {x ≈ y}"
| EqR: "x ≠ y ⟹ cov x (y ≈ x) {x ≈ y}"
| ap: "ap Q ⟹ x ∈ fv Q ⟹ cov x Q {Q}"
| Neg: "cov x Q G ⟹ cov x (Neg Q) G"
| Disj: "cov x Q1 G1 ⟹ cov x Q2 G2 ⟹ cov x (Disj Q1 Q2) (G1 ∪ G2)"
| DisjL: "cov x Q1 G ⟹ cp (Q1 ⊥ x) = Bool True ⟹ cov x (Disj Q1 Q2) G"
| DisjR: "cov x Q2 G ⟹ cp (Q2 ⊥ x) = Bool True ⟹ cov x (Disj Q1 Q2) G"
| Conj: "cov x Q1 G1 ⟹ cov x Q2 G2 ⟹ cov x (Conj Q1 Q2) (G1 ∪ G2)"
| ConjL: "cov x Q1 G ⟹ cp (Q1 ⊥ x) = Bool False ⟹ cov x (Conj Q1 Q2) G"
| ConjR: "cov x Q2 G ⟹ cp (Q2 ⊥ x) = Bool False ⟹ cov x (Conj Q1 Q2) G"
| Exists: "x ≠ y ⟹ cov x Q G ⟹ x ≈ y ∉ G ⟹ cov x (Exists y Q) (exists y ` G)"
| Exists_gen: "x ≠ y ⟹ cov x Q G ⟹ gen y Q Gy ⟹ cov x (Exists y Q) ((exists y ` (G - {x ≈ y})) ∪ ((λQ. cp (Q[y → x])) ` Gy))"

inductive cov' where
  Eq_self: "cov' x (x ≈ x) {}"
| nonfree: "x ∉ fv Q ⟹ cov' x Q {}"
| EqL: "x ≠ y ⟹ cov' x (x ≈ y) {x ≈ y}"
| EqR: "x ≠ y ⟹ cov' x (y ≈ x) {x ≈ y}"
| ap: "ap Q ⟹ x ∈ fv Q ⟹ cov' x Q {Q}"
| Neg: "cov' x Q G ⟹ cov' x (Neg Q) G"
| Disj: "cov' x Q1 G1 ⟹ cov' x Q2 G2 ⟹ cov' x (Disj Q1 Q2) (G1 ∪ G2)"
| DisjL: "cov' x Q1 G ⟹ cp (Q1 ⊥ x) = Bool True ⟹ cov' x (Disj Q1 Q2) G"
| DisjR: "cov' x Q2 G ⟹ cp (Q2 ⊥ x) = Bool True ⟹ cov' x (Disj Q1 Q2) G"
| Conj: "cov' x Q1 G1 ⟹ cov' x Q2 G2 ⟹ cov' x (Conj Q1 Q2) (G1 ∪ G2)"
| ConjL: "cov' x Q1 G ⟹ cp (Q1 ⊥ x) = Bool False ⟹ cov' x (Conj Q1 Q2) G"
| ConjR: "cov' x Q2 G ⟹ cp (Q2 ⊥ x) = Bool False ⟹ cov' x (Conj Q1 Q2) G"
| Exists: "x ≠ y ⟹ cov' x Q G ⟹ x ≈ y ∉ G ⟹ cov' x (Exists y Q) (exists y ` G)"
| Exists_gen: "x ≠ y ⟹ cov' x Q G ⟹ gen y Q Gy ⟹ cov' x (Exists y Q) ((exists y ` (G - {x ≈ y})) ∪ ((λQ. Q[y → x]) ` Gy))"

lemma cov_nocp_intros:
  "x ≠ y ⟹ cov x Q G ⟹ gen y Q Gy ⟹ cov x (Exists y Q) ((exists y ` (G - {x ≈ y})) ∪ ((λQ. Q[y → x]) ` Gy))"
  by (metis (no_types, lifting) cov.Exists_gen gen_qp image_cong qp_cp_subst_triv)

lemma cov'_cp_intros:
  "x ≠ y ⟹ cov' x Q G ⟹ gen y Q Gy ⟹ cov' x (Exists y Q) ((exists y ` (G - {x ≈ y})) ∪ ((λQ. cp (Q[y → x])) ` Gy))"
  by (metis (no_types, lifting) cov'.Exists_gen gen_qp image_cong qp_cp_subst_triv)

lemma cov'_cov: "cov' x Q G ⟹ cov x Q G"
  by (induct x Q G rule: cov'.induct) (force intro: cov.intros cov_nocp_intros)+

lemma cov_cov': "cov x Q G ⟹ cov' x Q G"
  by (induct x Q G rule: cov.induct) (force intro: cov'.intros cov'_cp_intros)+

lemma cov_eq_cov': "cov = cov'"
  using cov'_cov cov_cov' by blast

lemmas cov_induct[consumes 1, case_names Eq_self nonfree EqL EqR ap Neg Disj DisjL DisjR Conj ConjL ConjR Exists Exists_gen] =
  cov'.induct[folded cov_eq_cov']

lemma ex_cov: "rrb Q ⟹ x ∈ fv Q ⟹ ∃G. cov x Q G"
proof (induct Q)
  case (Eq z t)
  then show ?case
    by (cases t) (auto 6 0 intro: cov.intros ap.intros)
next
  case (Exists z Q)
  then obtain G Gz where "cov x Q G" "gen z Q Gz" "x ≠ z"
    by force
  then show ?case
    by (cases "x ≈ z ∈ G") (auto intro: cov.intros)
qed (auto intro: cov.intros ap.intros)

definition qps where
  "qps G = {Q ∈ G. qp Q}"

lemma qps_qp: "Q ∈ qps G ⟹ qp Q"
  by (auto simp: qps_def)

lemma qps_in: "Q ∈ qps G ⟹ Q ∈ G"
  by (auto simp: qps_def)

lemma qps_empty[simp]: "qps {} = {}"
  by (auto simp: qps_def)

lemma qps_insert: "qps (insert Q Qs) = (if qp Q then insert Q (qps Qs) else qps Qs)"
  by (auto simp: qps_def)

lemma qps_union[simp]: "qps (X ∪ Y) = qps X ∪ qps Y"
  by (auto simp: qps_def)

lemma finite_qps[simp]: "finite G ⟹ finite (qps G)"
  by (auto simp: qps_def)

lemma qps_exists[simp]: "x ≠ y ⟹ qps (exists y ` G) = exists y ` qps G"
  by (auto simp: qps_def image_iff exists_def qp_Exists elim: qp_ExistsE)

lemma qps_subst[simp]: "qps ((λQ. Q[x → y]) ` G) = (λQ. Q[x → y]) ` qps G"
  by (auto simp: qps_def image_iff exists_def)

lemma qps_minus[simp]: "qps (G - {x ≈ y}) = qps G"
  by (auto simp: qps_def)

lemma gen_qps[simp]: "gen x Q G ⟹ qps G = G"
  by (auto dest: gen_qp simp: qps_def)

lemma qps_rrb[simp]: "Q ∈ qps G ⟹ rrb Q"
  by (auto simp: qps_def)

definition eqs where
  "eqs x G = {y. x ≠ y ∧ x ≈ y ∈ G}"

lemma eqs_in: "y ∈ eqs x G ⟹ x ≈ y ∈ G"
  by (auto simp: eqs_def)

lemma eqs_noteq: "y ∈ eqs x Q ⟹ x ≠ y"
  unfolding eqs_def by auto

lemma eqs_empty[simp]: "eqs x {} = {}"
  by (auto simp: eqs_def)

lemma eqs_union[simp]: "eqs x (X ∪ Y) = eqs x X ∪ eqs x Y"
  by (auto simp: eqs_def)

lemma finite_eqs[simp]: "finite G ⟹ finite (eqs x G)"
  by (force simp: eqs_def image_iff elim!: finite_surj[where f = "λQ. SOME y. Q = x ≈ y"])

lemma eqs_exists[simp]: "x ≠ y ⟹ eqs x (exists y ` G) = eqs x G - {y}"
  by (auto simp: eqs_def exists_def image_iff)

lemma notin_eqs[simp]: "x ≈ y ∉ G ⟹ y ∉ eqs x G"
  by (auto simp: eqs_def)

lemma eqs_minus[simp]: "eqs x (G - {x ≈ y}) = eqs x G - {y}"
  by (auto simp: eqs_def)

lemma Var_eq_subst_iff: "Var z = t[x →t y] ⟷ (if z = x then x = y ∧ t = Var x else
  if z = y then t = Var x ∨ t = Var y else t = Var z)"
  by (cases t) auto

lemma Eq_eq_subst_iff: "y ≈ z = Q[x → y] ⟷ (if z = x then x = y ∧ Q = x ≈ x else
  Q = x ≈ z ∨ Q = y ≈ z ∨ (z = y ∧ Q ∈ {x ≈ x, y ≈ y, y ≈ x}))"
  by (cases Q) (auto simp: Let_def Var_eq_subst_iff split: if_splits)

lemma eqs_subst[simp]: "x ≠ y ⟹ eqs y ((λQ. Q[x → y]) ` G) = (eqs y G - {x}) ∪ (eqs x G - {y})"
  by (auto simp: eqs_def image_iff exists_def Eq_eq_subst_iff)

lemma gen_eqs[simp]: "gen x Q G ⟹ eqs z G = {}"
  by (auto dest: gen_qp simp: eqs_def)

lemma eqs_insert: "eqs x (insert Q Qs) = (case Q of z ≈ y ⇒
  if z = x ∧ z ≠ y then insert y (eqs x Qs) else eqs x Qs | _ ⇒ eqs x Qs)"
  by (auto simp: eqs_def split: fmla.splits term.splits)

lemma eqs_insert': "y ≠ x ⟹ eqs x (insert (x ≈ y) Qs) = insert y (eqs x Qs)"
  by (auto simp: eqs_def split: fmla.splits term.splits)

lemma eqs_code[code]: "eqs x G = (λeq. case eq of y ≈ z ⇒ z) ` (Set.filter (λeq. case eq of y ≈ z ⇒ x = y ∧ x ≠ z | _ => False) G)"
  by (auto simp: eqs_def image_iff Set.filter_def split: term.splits fmla.splits)

lemma gen_finite[simp]: "gen x Q G ⟹ finite G"
  by (induct x Q G rule: gen_induct) auto

lemma cov_finite[simp]: "cov x Q G ⟹ finite G"
  by (induct x Q G rule: cov.induct) auto

lemma gen_sat_erase: "gen y Q Gy ⟹ sat (Q ⊥ x) I σ ⟹ ∃Q∈Gy. sat Q I σ"
  by (induct y Q Gy arbitrary: σ rule: gen_induct)
    (force elim!: ap.cases dest: sym gen_sat split: if_splits)+

lemma cov_sat_erase: "cov x Q G ⟹
  sat (Neg (Disj (DISJ (qps G)) (DISJ ((λy. x ≈ y) ` eqs x G)))) I σ ⟹
  sat Q I σ ⟷ sat (cp (Q ⊥ x)) I σ"
  unfolding sat_cp
proof (induct x Q G arbitrary: σ rule: cov_induct)
  case (Eq_self x)
  then show ?case
    by auto
next
  case (nonfree x Q)
  from nonfree(1) show ?case
    by (induct Q arbitrary: σ) auto
next
  case (EqL x y)
  then show ?case
    by (auto simp: eqs_def)
next
  case (EqR x y)
  then show ?case
    by (auto simp: eqs_def)
next
  case (ap Q x)
  then show ?case
    by (auto simp: qps_def qp.intros elim!: ap.cases)
next
  case (Neg x Q G)
  then show ?case
    by auto
next
  case (Disj x Q1 G1 Q2 G2)
  then show ?case
    by auto
next
  case (DisjL x Q1 G Q2)
  then have "sat (Q1 ⊥ x) I σ"
    by (subst sat_cp[symmetric]) auto
  with DisjL show ?case
    by auto
next
  case (DisjR x Q2 G Q1)
  then have "sat (Q2 ⊥ x) I σ"
    by (subst sat_cp[symmetric]) auto
  with DisjR show ?case
    by auto
next
  case (Conj x Q1 G1 Q2 G2)
  then show ?case
    by auto
next
  case (ConjL x Q1 G Q2)
  then have "¬ sat (Q1 ⊥ x) I σ"
    by (subst sat_cp[symmetric]) auto
  with ConjL show ?case
    by auto
next
  case (ConjR x Q2 G Q1)
  then have "¬ sat (Q2 ⊥ x) I σ"
    by (subst sat_cp[symmetric]) auto
  with ConjR show ?case
    by auto
next
  case (Exists x y Q G)
  then show ?case
    by fastforce
next
  case (Exists_gen x y Q G Gy)
  show ?case
    unfolding sat.simps erase.simps Exists_gen(1)[THEN eq_False[THEN iffD2]] if_False
  proof (intro ex_cong1)
    fix z
    show "sat Q I (σ(y := z)) = sat (Q ⊥ x) I (σ(y := z))"
    proof (cases "z = σ x")
      case True
      with Exists_gen(2,4,5) show ?thesis
        by (auto dest: gen_sat gen_sat_erase simp: ball_Un)
    next
      case False
      with Exists_gen(1,2,4,5) show ?thesis
        by (intro Exists_gen(3)) (auto simp: ball_Un fun_upd_def)
    qed
  qed
qed

lemma cov_fv_aux: "cov x Q G ⟹ Qqp ∈ G ⟹ x ∈ fv Qqp ∧ fv Qqp - {x} ⊆ fv Q"
  by (induct x Q G arbitrary: Qqp rule: cov_induct)
    (auto simp: fv_subst subset_eq gen_fv[THEN conjunct1]
      gen_fv[THEN conjunct2, THEN set_mp] dest: gen_fv split: if_splits)

lemma cov_fv: "cov x Q G ⟹ x ∈ fv Q ⟹ Qqp ∈ G ⟹ x ∈ fv Qqp ∧ fv Qqp ⊆ fv Q"
  using cov_fv_aux[of x Q G Qqp] by auto

lemma Gen_Conj:
  "Gen x Q1 ⟹ Gen x (Conj Q1 Q2)"
  "Gen x Q2 ⟹ Gen x (Conj Q1 Q2)"
  by (auto intro: gen.intros)

lemma cov_Gen_qps: "cov x Q G ⟹ x ∈ fv Q ⟹ Gen x (Conj Q (DISJ (qps G)))"
  by (intro Gen_Conj(2) Gen_DISJ) (auto simp: qps_def dest: cov_fv)

lemma cov_equiv:
  assumes "cov x Q G" "⋀Q I σ. sat (simp Q) I σ = sat Q I σ"
  shows "Q ≜ Disj (simp (Conj Q (DISJ (qps G))))
    (Disj (DISJ ((λy. Conj (cp (Q[x → y])) (x ≈ y)) ` eqs x G))
    (Conj (Q ⊥ x) (Neg (Disj (DISJ (qps G)) (DISJ ((λy. x ≈ y) ` eqs x G))))))"
  (is "_ ≜ ?rhs")
unfolding equiv_def proof (intro allI impI)
  fix I σ
  show "sat Q I σ = sat ?rhs I σ"
    using cov_sat_erase[OF assms(1), of I σ] assms
    by (fastforce dest: sym simp del: cp.simps)
qed

fun csts_term where
  "csts_term (Var x) = {}"
| "csts_term (Const c) = {c}"

fun csts where
  "csts (Bool b) = {}"
| "csts (Pred p ts) = (⋃t ∈ set ts. csts_term t)"
| "csts (Eq x t) = csts_term t"
| "csts (Neg Q) = csts Q"
| "csts (Conj Q1 Q2) = csts Q1 ∪ csts Q2"
| "csts (Disj Q1 Q2) = csts Q1 ∪ csts Q2"
| "csts (Exists x Q) = csts Q"

lemma finite_csts_term[simp]: "finite (csts_term t)"
  by (induct t) auto

lemma finite_csts[simp]: "finite (csts t)"
  by (induct t) auto

lemma ap_fresh_val: "ap Q ⟹ σ x ∉ adom I ⟹ σ x ∉ csts Q ⟹ sat Q I σ ⟹ x ∉ fv Q"
proof (induct Q pred: ap)
  case (Pred p ts)
  show ?case unfolding fv.simps fv_terms_set_def set_map UN_iff bex_simps
  proof safe
    fix t
    assume "t ∈ set ts" "x ∈ fv_term_set t"
    with Pred show "False"
      by (cases t) (force simp: adom_def eval_terms_def)+
  qed
qed auto

lemma qp_fresh_val: "qp Q ⟹ σ x ∉ adom I ⟹ σ x ∉ csts Q ⟹ sat Q I σ ⟹ x ∉ fv Q"
proof (induct Q arbitrary: σ rule: qp.induct)
  case (ap Q)
  then show ?case by (rule ap_fresh_val)
next
  case (exists Q z)
  from exists(2)[of σ] exists(2)[of "σ(z := _)"] exists(1,3-) show ?case
    by (cases "x = z") (auto simp: exists_def fun_upd_def split: if_splits)
qed

lemma ex_fresh_val:
  fixes Q :: "('a :: infinite, 'b) fmla"
  assumes "finite (adom I)" "finite A"
  shows "∃x. x ∉ adom I ∧ x ∉ csts Q ∧ x ∉ A"
  by (metis UnCI assms ex_new_if_finite finite_Un finite_csts infinite_UNIV)

definition fresh_val :: "('a :: infinite, 'b) fmla ⇒ ('a, 'b) intp ⇒ 'a set ⇒ 'a" where
  "fresh_val Q I A = (SOME x. x ∉ adom I ∧ x ∉ csts Q ∧ x ∉ A)"

lemma fresh_val:
  "finite (adom I) ⟹ finite A ⟹ fresh_val Q I A ∉ adom I"
  "finite (adom I) ⟹ finite A ⟹ fresh_val Q I A ∉ csts Q"
  "finite (adom I) ⟹ finite A ⟹ fresh_val Q I A ∉ A"
  using someI_ex[OF ex_fresh_val, of I A Q]
  by (auto simp: fresh_val_def)

lemma csts_exists[simp]: "csts (exists x Q) = csts Q"
  by (auto simp: exists_def)

lemma csts_term_subst_term[simp]: "csts_term (t[x →t y]) = csts_term t"
  by (cases t) auto

lemma csts_subst[simp]: "csts (Q[x → y]) = csts Q"
  by (induct Q x y rule: subst.induct) (auto simp: Let_def)

lemma gen_csts: "gen x Q G ⟹ Qqp ∈ G ⟹ csts Qqp ⊆ csts Q"
  by (induct x Q G arbitrary: Qqp rule: gen_induct) (auto simp: subset_eq)

lemma cov_csts: "cov x Q G ⟹ Qqp ∈ G ⟹ csts Qqp ⊆ csts Q"
  by (induct x Q G arbitrary: Qqp rule: cov_induct)
    (auto simp: subset_eq gen_csts[THEN set_mp])

lemma not_self_eqs[simp]: "x ∉ eqs x G"
  by (auto simp: eqs_def)

lemma (in simplification) cov_Exists_equiv:
  fixes Q :: "('a :: {infinite, linorder}, 'b :: linorder) fmla"
  assumes "cov x Q G" "x ∈ fv Q"
  shows "Exists x Q ≜ Disj (Exists x (simp (Conj Q (DISJ (qps G)))))
    (Disj (DISJ ((λy. cp (Q[x → y])) ` eqs x G)) (cp (Q ⊥ x)))"
proof -
  have "Exists x Q ≜ Exists x (Disj (simp (Conj Q (DISJ (qps G))))
    (Disj (DISJ ((λy. Conj (cp (Q[x → y])) (x ≈ y)) ` eqs x G))
      (Conj (Q ⊥ x) (Neg (Disj (DISJ (qps G)) (DISJ ((≈) x ` eqs x G)))))))"
    by (rule equiv_Exists_cong[OF cov_equiv[OF assms(1) sat_simp]])
  also have "… ≜ Disj (Exists x (simp (Conj Q (DISJ (qps G))))) (Disj
    (Exists x (DISJ ((λy. Conj (cp (Q[x → y])) (x ≈ y)) ` eqs x G)))
      (Exists x (Conj (Q ⊥ x) (Neg (Disj (DISJ (qps G)) (DISJ ((≈) x ` eqs x G)))))))"
    by (auto intro!: equiv_trans[OF equiv_Exists_Disj] equiv_Disj_cong[OF equiv_refl])
  also have "… ≜ Disj (Exists x (simp (Conj Q (DISJ (qps G)))))
    (Disj (DISJ ((λy. cp (Q[x → y])) ` eqs x G)) (cp (Q ⊥ x)))"
  proof (rule equiv_Disj_cong[OF equiv_refl equiv_Disj_cong])
    show "Exists x (DISJ ((λy. Conj (cp (Q[x → y])) (x ≈ y)) ` eqs x G)) ≜ DISJ ((λy. cp (Q[x → y])) ` eqs x G)"
      using assms(1) unfolding equiv_def
      by simp (auto simp: eqs_def)
  next
    show "Exists x (Conj (Q ⊥ x) (Neg (Disj (DISJ (qps G)) (DISJ ((≈) x ` eqs x G))))) ≜ cp (Q ⊥ x)"
      unfolding equiv_def sat.simps sat_erase sat_cp
        sat_DISJ[OF finite_qps[OF cov_finite[OF assms(1)]]]
        sat_DISJ[OF finite_imageI[OF finite_eqs[OF cov_finite[OF assms(1)]]]]
    proof (intro allI impI)
      fix I :: "('a, 'b) intp" and σ
      assume "finite (adom I)"
      then show "(∃z. sat (Q ⊥ x) I σ ∧ ¬ ((∃Q∈qps G. sat Q I (σ(x := z))) ∨ (∃Q∈(≈) x ` eqs x G. sat Q I (σ(x := z))))) =
        sat (Q ⊥ x) I σ"
        using fresh_val[OF _ finite_imageI[OF finite_fv], of I Q σ Q] assms
        by (auto 0 3 simp: qps_def eqs_def intro!: exI[of _ "fresh_val Q I  (σ ` fv Q)"]
            dest: cov_fv cov_csts[THEN set_mp]
            qp_fresh_val[where σ="σ(x := fresh_val Q I (σ ` fv Q))" and x=x and I=I])
    qed
  qed
  finally show ?thesis .
qed

definition "eval_on V Q I =
  (let xs = sorted_list_of_set V
  in {ds. length xs = length ds ∧ (∃σ. sat Q I (σ[xs :=* ds]))})"

definition "eval Q I = eval_on (fv Q) Q I"

lemmas eval_deep_def = eval_def[unfolded eval_on_def]

lemma (in simplification) cov_eval_fin:
  fixes Q :: "('a :: {infinite, linorder}, 'b :: linorder) fmla"
  assumes "cov x Q G" "x ∈ fv Q" "finite (adom I)" "⋀σ. ¬ sat (Q ⊥ x) I σ"
  shows "eval Q I = eval_on (fv Q) (Disj (simp (Conj Q (DISJ (qps G))))
    (DISJ ((λy. Conj (cp (Q[x → y])) (x ≈ y)) ` eqs x G))) I"
    (is "eval Q I = eval_on (fv Q) ?Q I")
proof -
  from assms(1) have fv: "fv ?Q ⊆ fv Q"
    by (auto dest!: fv_cp[THEN set_mp] fv_simp[THEN set_mp] fv_DISJ[THEN set_mp, rotated -1]
      eqs_in qps_in cov_fv[OF assms(1,2)] simp: fv_subst simp del: cp.simps split: if_splits)
  show ?thesis
    unfolding eval_deep_def eval_on_def Let_def fv
  proof (intro Collect_eqI arg_cong2[of _ _ _ _ "(∧)"] ex_cong1)
    fix ds σ
    show "sat Q I (σ[sorted_list_of_set (fv Q) :=* ds]) ⟷
          sat ?Q I (σ[sorted_list_of_set (fv Q) :=* ds])"
      by (subst cov_equiv[OF assms(1) sat_simp, unfolded equiv_def, rule_format, OF assms(3)])
        (auto simp: assms(4))
  qed simp
qed

lemma (in simplification) cov_sat_fin:
  fixes Q :: "('a :: {infinite, linorder}, 'b :: linorder) fmla"
  assumes "cov x Q G" "x ∈ fv Q" "finite (adom I)" "⋀σ. ¬ sat (Q ⊥ x) I σ"
  shows "sat Q I σ = sat (Disj (simp (Conj Q (DISJ (qps G))))
    (DISJ ((λy. Conj (cp (Q[x → y])) (x ≈ y)) ` eqs x G))) I σ"
    (is "sat Q I σ = sat ?Q I σ")
proof -
  from assms(1) have fv: "fv ?Q ⊆ fv Q"
    by (auto dest!: fv_cp[THEN set_mp] fv_simp[THEN set_mp] fv_DISJ[THEN set_mp, rotated -1]
      eqs_in qps_in cov_fv[OF assms(1,2)] simp: fv_subst simp del: cp.simps split: if_splits)
  show ?thesis
    by (subst cov_equiv[OF assms(1) sat_simp, unfolded equiv_def, rule_format, OF assms(3)])
      (auto simp: assms(4))
qed

lemma equiv_eval_eqI: "finite (adom I) ⟹ fv Q = fv Q' ⟹ Q ≜ Q' ⟹ eval Q I = eval Q' I"
  by (auto simp: eval_deep_def equiv_def)

lemma equiv_eval_on_eqI: "finite (adom I) ⟹ Q ≜ Q' ⟹ eval_on X Q I = eval_on X Q' I"
  by (auto simp: eval_on_def equiv_def)

lemma equiv_eval_on_eval_eqI: "finite (adom I) ⟹ fv Q ⊆ fv Q' ⟹ Q ≜ Q' ⟹ eval_on (fv Q') Q I = eval Q' I"
  by (auto simp: eval_deep_def eval_on_def equiv_def)

lemma finite_eval_on_Disj2D:
  assumes "finite X"
  shows "finite (eval_on X (Disj Q1 Q2) I) ⟹ finite (eval_on X Q2 I)"
  unfolding eval_on_def Let_def
  by (auto elim!: finite_subset[rotated])

lemma finite_eval_Disj2D: "finite (eval (Disj Q1 Q2) I) ⟹ finite (eval Q2 I)"
  unfolding eval_deep_def Let_def
proof (safe elim!: finite_surj)
  fix ds σ
  assume "length (sorted_list_of_set (fv Q2)) = length ds" "sat Q2 I (σ[sorted_list_of_set (fv Q2) :=* ds])"
  moreover obtain zs where "zs ∈ extend (fv Q2) (sorted_list_of_set (fv Q1 ∪ fv Q2)) ds"
    using extend_nonempty by blast
  ultimately show "ds ∈ restrict (fv Q2) (sorted_list_of_set (fv (Disj Q1 Q2))) `
    {ds. length (sorted_list_of_set (fv (Disj Q1 Q2))) = length ds ∧
         (∃σ. sat (Disj Q1 Q2) I (σ[sorted_list_of_set (fv (Disj Q1 Q2)) :=* ds]))}"
    by (auto simp: Let_def image_iff restrict_extend fun_upds_extend length_extend
      elim!: sat_fv_cong[THEN iffD2, rotated -1]
      intro!: exI[of _ zs] exI[of _ σ] disjI2)
qed

lemma infinite_eval_Disj2:
  fixes Q1 Q2 :: "('a :: {infinite, linorder}, 'b :: linorder) fmla"
  assumes "fv Q2 ⊂ fv (Disj Q1 Q2)" "sat Q2 I σ"
  shows "infinite (eval (Disj Q1 Q2) I)"
proof -
  from assms(1) obtain z where "z ∈ fv Q1" "z ∉ fv Q2"
    by auto
  then have "d ∈ (λds. lookup (sorted_list_of_set (fv Q1 ∪ fv Q2)) ds z) ` eval (Disj Q1 Q2) I" for d
    using assms(2)
    by (auto simp: fun_upds_map_self eval_deep_def Let_def length_extend intro!: exI[of _ σ] disjI2 imageI
        dest!: ex_lookup_extend[of _ _ "(sorted_list_of_set (fv Q1 ∪ fv Q2))" "map σ (sorted_list_of_set (fv Q2))" d]
        elim!: sat_fv_cong[THEN iffD2, rotated -1] fun_upds_extend[THEN trans])
  then show ?thesis
    by (rule infinite_surj[OF infinite_UNIV, OF subsetI])
qed

lemma infinite_eval_on_Disj2:
  fixes Q1 Q2 :: "('a :: {infinite, linorder}, 'b :: linorder) fmla"
  assumes "fv Q2 ⊂ X" "fv Q1 ⊆ X""finite X" "sat Q2 I σ"
  shows "infinite (eval_on X (Disj Q1 Q2) I)"
proof -
  from assms(1) obtain z where "z ∈ X" "z ∉ fv Q2"
    by auto
  then have "d ∈ (λds. lookup (sorted_list_of_set X) ds z) ` eval_on X (Disj Q1 Q2) I" for d
    using assms ex_lookup_extend[of z "fv Q2" "(sorted_list_of_set X)" "map σ (sorted_list_of_set (fv Q2))" d]
    by (auto simp: fun_upds_map_self eval_on_def Let_def subset_eq length_extend intro!: exI[of _ σ] disjI2 imageI
        elim!: sat_fv_cong[THEN iffD2, rotated -1] fun_upds_extend[rotated -1, THEN trans])
  then show ?thesis
    by (rule infinite_surj[OF infinite_UNIV, OF subsetI])
qed

lemma cov_eval_inf:
  fixes Q :: "('a :: {infinite, linorder}, 'b :: linorder) fmla"
  assumes "cov x Q G" "x ∈ fv Q" "finite (adom I)" "sat (Q ⊥ x) I σ"
  shows "infinite (eval Q I)"
proof -
  let ?Q1 = "Conj Q (DISJ (qps G))"
  let ?Q2 = "DISJ ((λy. Conj (cp (Q[x → y])) (x ≈ y)) ` eqs x G)"
  define Q3 where "Q3 = Conj (Q ⊥ x) (Neg (Disj (DISJ (qps G)) (DISJ ((λy. x ≈ y) ` eqs x G))))"
  let ?Q = "Disj ?Q1 (Disj ?Q2 Q3)"
  from assms(1) have fv123: "fv ?Q1 ⊆ fv Q" "fv ?Q2 ⊆ fv Q" "fv Q3 ⊆ fv Q" and fin_fv[simp]: "finite (fv Q3)" unfolding Q3_def
    by (auto dest!: fv_cp[THEN set_mp] fv_DISJ[THEN set_mp, rotated 1] fv_erase[THEN set_mp]
      eqs_in qps_in cov_fv[OF assms(1,2)] simp: fv_subst simp del: cp.simps)
  then have fv: "fv ?Q ⊆ fv Q"
    by auto
  from assms(1,2,4) have sat: "sat Q3 I (σ(x := d))" if "d ∉ adom I ∪ csts Q ∪ σ ` fv Q" for d
    using that cov_fv[OF assms(1,2) qps_in] cov_fv[OF assms(1,2) eqs_in, of _ x]
      qp_fresh_val[OF qps_qp, of _ G "σ(x := d)" x I] cov_csts[OF assms(1) qps_in]
    by (auto 5 2 simp: image_iff Q3_def elim!: sat_fv_cong[THEN iffD2, rotated -1]
      dest: fv_erase[THEN set_mp] dest: eqs_in)
  from assms(3) have inf: "infinite {d. d ∉ adom I ∪ csts Q ∪ σ ` fv Q}"
    unfolding Compl_eq[symmetric] Compl_eq_Diff_UNIV
    by (intro Diff_infinite_finite) (auto simp: infinite_UNIV)
  { assume "x ∈ fv Q3"
    let ?f = "λds. lookup (sorted_list_of_set (fv Q)) ds x"
    from inf have "infinite (eval_on (fv Q) Q3 I)"
    proof (rule infinite_surj[where f="?f"], intro subsetI, elim CollectE)
      fix z
      assume "z ∉ adom I ∪ csts Q ∪ σ ` fv Q"
      with ‹x ∈ fv Q3› fv123 sat show "z ∈ ?f ` eval_on (fv Q) Q3 I"
        by (auto simp: eval_on_def image_iff Let_def fun_upds_single subset_eq simp del: cp.simps
          intro!: exI[of _ σ] exI[of _ "map (σ(x := z)) (sorted_list_of_set (fv Q))"])
    qed
    then have "infinite (eval_on (fv Q) ?Q I)"
      by (rule contrapos_nn) (auto dest!: finite_eval_on_Disj2D[rotated])
  }
  moreover
  { assume x: "x ∉ fv Q3"
    from inf obtain d where "d ∉ adom I ∪ csts Q ∪ σ ` fv Q"
      by (meson not_finite_existsD)
    with fv123 sat[of d] assms(2) x have "infinite (eval_on (fv Q) (Disj (Disj ?Q1 ?Q2) Q3) I)"
      by (intro infinite_eval_on_Disj2[of _"fv Q" _ _ "(σ(x := d))"]) (auto simp del: cp.simps)
    moreover have "eval_on (fv Q) (Disj (Disj ?Q1 ?Q2) Q3) I = eval_on (fv Q) ?Q I"
      by (rule equiv_eval_on_eqI[OF assms(3) equiv_Disj_Assoc])
    ultimately have "infinite (eval_on (fv Q) ?Q I)"
      by simp
  }
  moreover have "eval Q I = eval_on (fv Q) ?Q I"
    unfolding Q3_def
    by (rule equiv_eval_on_eval_eqI[symmetric, OF assms(3) fv[unfolded Q3_def] cov_equiv[OF assms(1) refl, THEN equiv_sym]])
  ultimately show ?thesis
    by auto
qed

subsection ‹More on Evaluation›

lemma eval_Bool_False[simp]: "eval (Bool False) I = {}"
  by (auto simp: eval_deep_def)

lemma eval_on_False[simp]: "eval_on X (Bool False) I = {}"
  by (auto simp: eval_on_def)

lemma eval_DISJ_prune_unsat: "finite B ⟹ A ⊆ B ⟹ ∀Q ∈ B - A. ∀σ. ¬ sat Q I σ ⟹ eval_on X (DISJ A) I = eval_on X (DISJ B) I"
  by (auto simp: eval_on_def finite_subset)

lemma eval_DISJ: "finite 𝒬 ⟹ ∀Q ∈ 𝒬. fv Q = A ⟹ eval_on A (DISJ 𝒬) I = (⋃Q ∈ 𝒬. eval Q I)"
  by (auto simp: eval_deep_def eval_on_def)

lemma eval_cp_DISJ_closed: "finite 𝒬 ⟹ ∀Q ∈ 𝒬. fv Q = {} ⟹ eval (cp (DISJ 𝒬)) I = (⋃Q ∈ 𝒬. eval Q I)"
  using fv_DISJ[of 𝒬] fv_cp[of "DISJ 𝒬"] by (auto simp: eval_deep_def)

lemma (in simplification) eval_simp_DISJ_closed: "finite 𝒬 ⟹ ∀Q ∈ 𝒬. fv Q = {} ⟹ eval (simp (DISJ 𝒬)) I = (⋃Q ∈ 𝒬. eval Q I)"
  using fv_DISJ[of 𝒬] fv_simp[of "DISJ 𝒬"] by (auto simp: eval_deep_def sat_simp)

lemma eval_cong: "fv Q = fv Q' ⟹ (⋀σ. sat Q I σ = sat Q' I σ) ⟹ eval Q I = eval Q' I"
  by (auto simp: eval_deep_def)

lemma eval_on_cong: "(⋀σ. sat Q I σ = sat Q' I σ) ⟹ eval_on X Q I = eval_on X Q' I"
  by (auto simp: eval_on_def)

lemma eval_empty_alt: "eval Q I = {} ⟷ (∀σ. ¬ sat Q I σ)"
proof (intro iffI allI)
  fix σ
  assume "eval Q I = {}"
  then show "¬ sat Q I σ"
    by (auto simp: eval_deep_def fun_upds_map_self
      dest!: spec[of _ "map σ (sorted_list_of_set (fv Q))"] spec[of _ σ])
qed (auto simp: eval_deep_def)

lemma sat_EXISTS: "distinct xs ⟹ sat (EXISTS xs Q) I σ = (∃ds. length ds = length xs ∧ sat Q I (σ[xs :=* ds]))"
proof (induct xs arbitrary: Q σ)
  case (Cons x xs)
  then show ?case
    by (auto 0 3 simp: EXISTS_def length_Suc_conv fun_upds_twist fun_upd_def[symmetric])
qed (simp add: EXISTS_def)

lemma eval_empty_close: "eval (close Q) I = {} ⟷ (∀σ. ¬ sat Q I σ)"
  by (subst eval_empty_alt)
    (auto simp: sat_EXISTS fun_upds_map_self dest: spec2[of _ σ "map σ(sorted_list_of_set (fv Q))" for σ])

lemma infinite_eval_on_extra_variables:
  assumes "finite X" "fv (Q :: ('a :: infinite, 'b) fmla) ⊂ X" "∃σ. sat Q I σ"
  shows "infinite (eval_on X Q I)"
proof -
  from assms obtain x σ where "x ∈ X - fv Q" "fv Q ⊆ X" "sat Q I σ"
    by auto
  with assms(1) show ?thesis
    by (intro infinite_surj[OF infinite_UNIV, of "λds. ds ! index (sorted_list_of_set X) x"])
      (force simp: eval_on_def image_iff fun_upds_in
        elim!: sat_fv_cong[THEN iffD1, rotated]
        intro!: exI[of _ "map (λy. if x = y then _ else σ y) (sorted_list_of_set X)"] exI[of _ σ])
qed

lemma eval_on_cp: "eval_on X (cp Q) = eval_on X Q"
  by (auto simp: eval_on_def)

lemma (in simplification) eval_on_simp: "eval_on X (simp Q) = eval_on X Q"
  by (auto simp: eval_on_def sat_simp)

lemma (in simplification) eval_simp_False: "eval (simp (Bool False)) I = {}"
  using fv_simp[of "Bool False"] by (auto simp: eval_deep_def sat_simp)

abbreviation "idx_of_var x Q ≡ index (sorted_list_of_set (fv Q)) x"

lemma evalE: "ds ∈ eval Q I ⟹ (⋀σ. length ds = card (fv Q) ⟹ sat Q I (σ[sorted_list_of_set (fv Q) :=* ds]) ⟹ R) ⟹ R"
  unfolding eval_deep_def by auto

lemma infinite_eval_Conj:
  assumes "x ∉ fv Q" "infinite (eval Q I)"
  shows "infinite (eval (Conj Q (x ≈ y)) I)"
    (is "infinite (eval ?Qxy I)")
proof (cases "x = y")
  case True
  let ?f = "remove_nth (idx_of_var x ?Qxy)"
  let ?g = "insert_nth (idx_of_var x ?Qxy) undefined"
  show ?thesis
    using assms(2)
  proof (elim infinite_surj[of _ ?f], intro subsetI, elim evalE)
    fix ds σ
    assume ds: "length ds = card (fv Q)" "sat Q I (σ[sorted_list_of_set (fv Q) :=* ds])"
    show "ds ∈ ?f ` eval ?Qxy I"
    proof (intro image_eqI[of _ _ "?g ds"])
      from ds assms(1) True show "ds = ?f (?g ds)"
        by (intro remove_nth_insert_nth[symmetric])
          (auto simp: less_Suc_eq_le[symmetric] set_insort_key)
    next
      from ds assms(1) True show "?g ds ∈ eval ?Qxy I"
        by (auto simp: eval_deep_def Let_def length_insert_nth distinct_insort set_insort_key fun_upds_in
          simp del: insert_nth_take_drop elim!: sat_fv_cong[THEN iffD1, rotated]
          intro!: exI[of _ σ] trans[OF _ insert_nth_nth_index[symmetric]])
    qed
  qed
next
  case xy: False
  show ?thesis
  proof (cases "y ∈ fv Q")
    case True
    let ?f = "remove_nth (idx_of_var x ?Qxy)"
    let ?g = "λds. insert_nth (idx_of_var x ?Qxy) (ds ! idx_of_var y Q) ds"
    from assms(2) show ?thesis
    proof (elim infinite_surj[of _ ?f], intro subsetI, elim evalE)
      fix ds σ
      assume ds: "length ds = card (fv Q)" "sat Q I (σ[sorted_list_of_set (fv Q) :=* ds])"
      show "ds ∈ ?f ` eval ?Qxy I"
      proof (intro image_eqI[of _ _ "?g ds"])
        from ds assms(1) True show "ds = ?f (?g ds)"
          by (intro remove_nth_insert_nth[symmetric])
            (auto simp: less_Suc_eq_le[symmetric] set_insort_key)
      next
        from assms(1) True have "remove1 x (insort y (sorted_list_of_set (insert x (fv Q) - {y}))) = sorted_list_of_set (fv Q)"
          by (metis Diff_insert_absorb finite_fv finite_insert insert_iff
              sorted_list_of_set.fold_insort_key.remove sorted_list_of_set.sorted_key_list_of_set_remove)
        moreover have "index (insort y (sorted_list_of_set (insert x (fv Q) - {y}))) x ≤ length ds"
          using ds(1) assms(1) True
          by (subst less_Suc_eq_le[symmetric]) (auto simp: set_insort_key intro: index_less_size)
        ultimately show "?g ds ∈ eval ?Qxy I"
          using  ds assms(1) True
          by (auto simp: eval_deep_def Let_def length_insert_nth distinct_insort set_insort_key fun_upds_in nth_insert_nth
            simp del: insert_nth_take_drop elim!: sat_fv_cong[THEN iffD1, rotated]
            intro!: exI[of _ σ] trans[OF _ insert_nth_nth_index[symmetric]])
      qed
    qed
  next
    case False
    let ?Qxx = "Conj Q (x ≈ x)"
    let ?f = "remove_nth (idx_of_var x ?Qxx) o remove_nth (idx_of_var y ?Qxy)"
    let ?g1 = "insert_nth (idx_of_var y ?Qxy) undefined"
    let ?g2 = "insert_nth (idx_of_var x ?Qxx) undefined"
    let ?g = "?g1 o ?g2"
    from assms(2) show ?thesis
    proof (elim infinite_surj[of _ ?f], intro subsetI, elim evalE)
      fix ds σ
      assume ds: "length ds = card (fv Q)" "sat Q I (σ[sorted_list_of_set (fv Q) :=* ds])"
      then show "ds ∈ ?f ` eval ?Qxy I"
      proof (intro image_eqI[of _ _ "?g ds"])
        from ds assms(1) xy False show "ds = ?f (?g ds)"
          by (auto simp: less_Suc_eq_le[symmetric] set_insort_key index_less_size
            length_insert_nth remove_nth_insert_nth simp del: insert_nth_take_drop)
      next
        from ds(1) have "index (insort x (sorted_list_of_set (fv Q))) x ≤ length ds"
          by (auto simp: less_Suc_eq_le[symmetric] set_insort_key)
        moreover from ds(1) have "index (insort y (insort x (sorted_list_of_set (fv Q)))) y ≤ Suc (length ds)"
          by (auto simp: less_Suc_eq_le[symmetric] set_insort_key)
        ultimately show "?g ds ∈ eval ?Qxy I"
          using ds assms(1) xy False unfolding eval_deep_def Let_def
          by (auto simp: fun_upds_in distinct_insort set_insort_key length_insert_nth
            insert_nth_nth_index nth_insert_nth elim!: sat_fv_cong[THEN iffD1, rotated]
            intro!: exI[of _ σ] trans[OF _ insert_nth_nth_index[symmetric]] simp del: insert_nth_take_drop) []
      qed
    qed
  qed
    qed

lemma infinite_Implies_mono_on: "infinite (eval_on X Q I) ⟹ finite X ⟹ (⋀σ. sat (Impl Q Q') I σ) ⟹ infinite (eval_on X Q' I)"
  by (erule contrapos_nn, rule finite_subset[rotated]) (auto simp: eval_on_def image_iff)

(*<*)
end
(*>*)