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)

lemma distinct_remdups_adj_sort: "sorted xs ⟹ distinct (remdups_adj xs)"
  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)
     (auto simp add: sorted_insort intro: distinct_remdups_adj_sort)

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