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: "Qset 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 
  Qset 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