# Theory FO

```theory FO
imports Main
begin

abbreviation "sorted_distinct xs ≡ sorted xs ∧ distinct xs"

datatype 'a fo_term = Const 'a | Var nat

type_synonym 'a val = "nat ⇒ 'a"

fun list_fo_term :: "'a fo_term ⇒ 'a list" where
"list_fo_term (Const c) = [c]"
| "list_fo_term _ = []"

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

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

definition fv_fo_terms_set :: "('a fo_term) list ⇒ nat set" where
"fv_fo_terms_set ts = ⋃(set (map fv_fo_term_set ts))"

fun fv_fo_terms_list_rec :: "('a fo_term) list ⇒ nat list" where
"fv_fo_terms_list_rec [] = []"
| "fv_fo_terms_list_rec (t # ts) = fv_fo_term_list t @ fv_fo_terms_list_rec ts"

definition fv_fo_terms_list :: "('a fo_term) list ⇒ nat list" where
"fv_fo_terms_list ts = remdups_adj (sort (fv_fo_terms_list_rec ts))"

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

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

lemma finite_set_fo_term: "finite (set_fo_term t)"
by (cases t) auto

lemma list_fo_term_set: "set (list_fo_term t) = set_fo_term t"
by (cases t) auto

lemma finite_fv_fo_term_set: "finite (fv_fo_term_set t)"
by (cases t) auto

lemma fv_fo_term_setD: "n ∈ fv_fo_term_set t ⟹ t = Var n"
by (cases t) auto

lemma fv_fo_term_set_list: "set (fv_fo_term_list t) = fv_fo_term_set t"
by (cases t) auto

lemma sorted_distinct_fv_fo_term_list: "sorted_distinct (fv_fo_term_list t)"
by (cases t) auto

lemma fv_fo_term_set_cong: "fv_fo_term_set t = fv_fo_term_set (map_fo_term f t)"
by (cases t) auto

lemma fv_fo_terms_setI: "Var m ∈ set ts ⟹ m ∈ fv_fo_terms_set ts"
by (induction ts) (auto simp: fv_fo_terms_set_def)

lemma fv_fo_terms_setD: "m ∈ fv_fo_terms_set ts ⟹ Var m ∈ set ts"
by (induction ts) (auto simp: fv_fo_terms_set_def dest: fv_fo_term_setD)

lemma finite_fv_fo_terms_set: "finite (fv_fo_terms_set ts)"
by (auto simp: fv_fo_terms_set_def finite_fv_fo_term_set)

lemma fv_fo_terms_set_list: "set (fv_fo_terms_list ts) = fv_fo_terms_set ts"
using fv_fo_term_set_list
unfolding fv_fo_terms_list_def
by (induction ts rule: fv_fo_terms_list_rec.induct)
(auto simp: fv_fo_terms_set_def set_insort_key)

by (induction xs rule: induct_list012) auto

lemma sorted_distinct_fv_fo_terms_list: "sorted_distinct (fv_fo_terms_list ts)"
unfolding fv_fo_terms_list_def
by (induction ts rule: fv_fo_terms_list_rec.induct)

lemma fv_fo_terms_set_cong: "fv_fo_terms_set ts = fv_fo_terms_set (map (map_fo_term f) ts)"
using fv_fo_term_set_cong
by (induction ts) (fastforce simp: fv_fo_terms_set_def)+

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

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

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

datatype ('a, 'b) fo_fmla =
Pred 'b "('a fo_term) list"
| Bool bool
| Eqa "'a fo_term" "'a fo_term"
| Neg "('a, 'b) fo_fmla"
| Conj "('a, 'b) fo_fmla" "('a, 'b) fo_fmla"
| Disj "('a, 'b) fo_fmla" "('a, 'b) fo_fmla"
| Exists nat "('a, 'b) fo_fmla"
| Forall nat "('a, 'b) fo_fmla"

fun fv_fo_fmla_list_rec :: "('a, 'b) fo_fmla ⇒ nat list" where
"fv_fo_fmla_list_rec (Pred _ ts) = fv_fo_terms_list ts"
| "fv_fo_fmla_list_rec (Bool b) = []"
| "fv_fo_fmla_list_rec (Eqa t t') = fv_fo_term_list t @ fv_fo_term_list t'"
| "fv_fo_fmla_list_rec (Neg φ) = fv_fo_fmla_list_rec φ"
| "fv_fo_fmla_list_rec (Conj φ ψ) = fv_fo_fmla_list_rec φ @ fv_fo_fmla_list_rec ψ"
| "fv_fo_fmla_list_rec (Disj φ ψ) = fv_fo_fmla_list_rec φ @ fv_fo_fmla_list_rec ψ"
| "fv_fo_fmla_list_rec (Exists n φ) = filter (λm. n ≠ m) (fv_fo_fmla_list_rec φ)"
| "fv_fo_fmla_list_rec (Forall n φ) = filter (λm. n ≠ m) (fv_fo_fmla_list_rec φ)"

definition fv_fo_fmla_list :: "('a, 'b) fo_fmla ⇒ nat list" where
"fv_fo_fmla_list φ = remdups_adj (sort (fv_fo_fmla_list_rec φ))"

fun fv_fo_fmla :: "('a, 'b) fo_fmla ⇒ nat set" where
"fv_fo_fmla (Pred _ ts) = fv_fo_terms_set ts"
| "fv_fo_fmla (Bool b) = {}"
| "fv_fo_fmla (Eqa t t') = fv_fo_term_set t ∪ fv_fo_term_set t'"
| "fv_fo_fmla (Neg φ) = fv_fo_fmla φ"
| "fv_fo_fmla (Conj φ ψ) = fv_fo_fmla φ ∪ fv_fo_fmla ψ"
| "fv_fo_fmla (Disj φ ψ) = fv_fo_fmla φ ∪ fv_fo_fmla ψ"
| "fv_fo_fmla (Exists n φ) = fv_fo_fmla φ - {n}"
| "fv_fo_fmla (Forall n φ) = fv_fo_fmla φ - {n}"

lemma finite_fv_fo_fmla: "finite (fv_fo_fmla φ)"
by (induction φ rule: fv_fo_fmla.induct)
(auto simp: finite_fv_fo_term_set finite_fv_fo_terms_set)

lemma fv_fo_fmla_list_set: "set (fv_fo_fmla_list φ) = fv_fo_fmla φ"
unfolding fv_fo_fmla_list_def
by (induction φ rule: fv_fo_fmla.induct) (auto simp: fv_fo_terms_set_list fv_fo_term_set_list)

lemma sorted_distinct_fv_list: "sorted_distinct (fv_fo_fmla_list φ)"
by (auto simp: fv_fo_fmla_list_def intro: distinct_remdups_adj_sort)

lemma length_fv_fo_fmla_list: "length (fv_fo_fmla_list φ) = card (fv_fo_fmla φ)"
using fv_fo_fmla_list_set[of φ] sorted_distinct_fv_list[of φ]
distinct_card[of "fv_fo_fmla_list φ"]
by auto

lemma fv_fo_fmla_list_eq: "fv_fo_fmla φ = fv_fo_fmla ψ ⟹ fv_fo_fmla_list φ = fv_fo_fmla_list ψ"
using fv_fo_fmla_list_set sorted_distinct_fv_list
by (metis sorted_distinct_set_unique)

lemma fv_fo_fmla_list_Conj: "fv_fo_fmla_list (Conj φ ψ) = fv_fo_fmla_list (Conj ψ φ)"
using fv_fo_fmla_list_eq[of "Conj φ ψ" "Conj ψ φ"]
by auto

type_synonym 'a table = "('a list) set"

type_synonym ('t, 'b) fo_intp = "'b × nat ⇒ 't"

fun wf_fo_intp :: "('a, 'b) fo_fmla ⇒ ('a table, 'b) fo_intp ⇒ bool" where
"wf_fo_intp (Pred r ts) I ⟷ finite (I (r, length ts))"
| "wf_fo_intp (Bool b) I ⟷ True"
| "wf_fo_intp (Eqa t t') I ⟷ True"
| "wf_fo_intp (Neg φ) I ⟷ wf_fo_intp φ I"
| "wf_fo_intp (Conj φ ψ) I ⟷ wf_fo_intp φ I ∧ wf_fo_intp ψ I"
| "wf_fo_intp (Disj φ ψ) I ⟷ wf_fo_intp φ I ∧ wf_fo_intp ψ I"
| "wf_fo_intp (Exists n φ) I ⟷ wf_fo_intp φ I"
| "wf_fo_intp (Forall n φ) I ⟷ wf_fo_intp φ I"

fun sat :: "('a, 'b) fo_fmla ⇒ ('a table, 'b) fo_intp ⇒ 'a val ⇒ bool" where
"sat (Pred r ts) I σ ⟷ σ ⊙ ts ∈ I (r, length ts)"
| "sat (Bool b) I σ ⟷ b"
| "sat (Eqa t t') I σ ⟷ σ ⋅ t = σ ⋅ t'"
| "sat (Neg φ) I σ ⟷ ¬sat φ I σ"
| "sat (Conj φ ψ) I σ ⟷ sat φ I σ ∧ sat ψ I σ"
| "sat (Disj φ ψ) I σ ⟷ sat φ I σ ∨ sat ψ I σ"
| "sat (Exists n φ) I σ ⟷ (∃x. sat φ I (σ(n := x)))"
| "sat (Forall n φ) I σ ⟷ (∀x. sat φ I (σ(n := x)))"

lemma sat_fv_cong: "(⋀n. n ∈ fv_fo_fmla φ ⟹ σ 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
next
case (Forall n φ)
have "⋀x. sat φ I (σ(n := x)) = sat φ I (σ'(n := x))"
using Forall(2)
by (auto intro!: Forall(1))
then show ?case
by simp
qed (auto cong: eval_terms_cong eval_term_cong)

definition proj_sat :: "('a, 'b) fo_fmla ⇒ ('a table, 'b) fo_intp ⇒ 'a table" where
"proj_sat φ I = (λσ. map σ (fv_fo_fmla_list φ)) ` {σ. sat φ I σ}"

end```