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<