# Theory Eval_FO

```theory Eval_FO
imports Infinite FO
begin

datatype 'a eval_res = Fin "'a table" | Infin | Wf_error

locale eval_fo =
fixes wf :: "('a :: infinite, 'b) fo_fmla ⇒ ('b × nat ⇒ 'a list set) ⇒ 't ⇒ bool"
and abs :: "('a fo_term) list ⇒ 'a table ⇒ 't"
and rep :: "'t ⇒ 'a table"
and res :: "'t ⇒ 'a eval_res"
and eval_bool :: "bool ⇒ 't"
and eval_eq :: "'a fo_term ⇒ 'a fo_term ⇒ 't"
and eval_neg :: "nat list ⇒ 't ⇒ 't"
and eval_conj :: "nat list ⇒ 't ⇒ nat list ⇒ 't ⇒ 't"
and eval_ajoin :: "nat list ⇒ 't ⇒ nat list ⇒ 't ⇒ 't"
and eval_disj :: "nat list ⇒ 't ⇒ nat list ⇒ 't ⇒ 't"
and eval_exists :: "nat ⇒ nat list ⇒ 't ⇒ 't"
and eval_forall :: "nat ⇒ nat list ⇒ 't ⇒ 't"
assumes fo_rep: "wf φ I t ⟹ rep t = proj_sat φ I"
and fo_res_fin: "wf φ I t ⟹ finite (rep t) ⟹ res t = Fin (rep t)"
and fo_res_infin: "wf φ I t ⟹ ¬finite (rep t) ⟹ res t = Infin"
and fo_abs: "finite (I (r, length ts)) ⟹ wf (Pred r ts) I (abs ts (I (r, length ts)))"
and fo_bool: "wf (Bool b) I (eval_bool b)"
and fo_eq: "wf (Eqa trm trm') I (eval_eq trm trm')"
and fo_neg: "wf φ I t ⟹ wf (Neg φ) I (eval_neg (fv_fo_fmla_list φ) t)"
and fo_conj: "wf φ I tφ ⟹ wf ψ I tψ ⟹ (case ψ of Neg ψ' ⇒ False | _ ⇒ True) ⟹
wf (Conj φ ψ) I (eval_conj (fv_fo_fmla_list φ) tφ (fv_fo_fmla_list ψ) tψ)"
and fo_ajoin: "wf φ I tφ ⟹ wf ψ' I tψ' ⟹
wf (Conj φ (Neg ψ')) I (eval_ajoin (fv_fo_fmla_list φ) tφ (fv_fo_fmla_list ψ') tψ')"
and fo_disj: "wf φ I tφ ⟹ wf ψ I tψ ⟹
wf (Disj φ ψ) I (eval_disj (fv_fo_fmla_list φ) tφ (fv_fo_fmla_list ψ) tψ)"
and fo_exists: "wf φ I t ⟹ wf (Exists i φ) I (eval_exists i (fv_fo_fmla_list φ) t)"
and fo_forall: "wf φ I t ⟹ wf (Forall i φ) I (eval_forall i (fv_fo_fmla_list φ) t)"
begin

fun eval_fmla :: "('a, 'b) fo_fmla ⇒ ('a table, 'b) fo_intp ⇒ 't" where
"eval_fmla (Pred r ts) I = abs ts (I (r, length ts))"
| "eval_fmla (Bool b) I = eval_bool b"
| "eval_fmla (Eqa t t') I = eval_eq t t'"
| "eval_fmla (Neg φ) I = eval_neg (fv_fo_fmla_list φ) (eval_fmla φ I)"
| "eval_fmla (Conj φ ψ) I = (let nsφ = fv_fo_fmla_list φ; nsψ = fv_fo_fmla_list ψ;
Xφ = eval_fmla φ I in
case ψ of Neg ψ' ⇒ let Xψ' = eval_fmla ψ' I in
eval_ajoin nsφ Xφ (fv_fo_fmla_list ψ') Xψ'
| _ ⇒ eval_conj nsφ Xφ nsψ (eval_fmla ψ I))"
| "eval_fmla (Disj φ ψ) I = eval_disj (fv_fo_fmla_list φ) (eval_fmla φ I)
(fv_fo_fmla_list ψ) (eval_fmla ψ I)"
| "eval_fmla (Exists i φ) I = eval_exists i (fv_fo_fmla_list φ) (eval_fmla φ I)"
| "eval_fmla (Forall i φ) I = eval_forall i (fv_fo_fmla_list φ) (eval_fmla φ I)"

lemma eval_fmla_correct:
fixes φ :: "('a :: infinite, 'b) fo_fmla"
assumes "wf_fo_intp φ I"
shows "wf φ I (eval_fmla φ I)"
using assms
proof (induction φ I rule: eval_fmla.induct)
case (1 r ts I)
then show ?case
using fo_abs
by auto
next
case (2 b I)
then show ?case
using fo_bool
by auto
next
case (3 t t' I)
then show ?case
using fo_eq
by auto
next
case (4 φ I)
then show ?case
using fo_neg
by auto
next
case (5 φ ψ I)
have fins: "wf_fo_intp φ I" "wf_fo_intp ψ I"
using 5(10)
by auto
have evalφ: "wf φ I (eval_fmla φ I)"
using 5(1)[OF _ _ fins(1)]
by auto
show ?case
proof (cases "∃ψ'. ψ = Neg ψ'")
case True
then obtain ψ' where ψ_def: "ψ = Neg ψ'"
by auto
have fin: "wf_fo_intp ψ' I"
using fins(2)
by (auto simp: ψ_def)
have evalψ': "wf ψ' I (eval_fmla ψ' I)"
using 5(5)[OF _ _ _ ψ_def fin]
by auto
show ?thesis
unfolding ψ_def
using fo_ajoin[OF evalφ evalψ']
by auto
next
case False
then have evalψ: "wf ψ I (eval_fmla ψ I)"
using 5 fins(2)
by (cases ψ) auto
have eval: "eval_fmla (Conj φ ψ) I = eval_conj (fv_fo_fmla_list φ) (eval_fmla φ I)
(fv_fo_fmla_list ψ) (eval_fmla ψ I)"
using False
by (auto simp: Let_def split: fo_fmla.splits)
show "wf (Conj φ ψ) I (eval_fmla (Conj φ ψ) I)"
using fo_conj[OF evalφ evalψ, folded eval] False
by (auto split: fo_fmla.splits)
qed
next
case (6 φ ψ I)
then show ?case
using fo_disj
by auto
next
case (7 i φ I)
then show ?case
using fo_exists
by auto
next
case (8 i φ I)
then show ?case
using fo_forall
by auto
qed

definition eval :: "('a, 'b) fo_fmla ⇒ ('a table, 'b) fo_intp ⇒ 'a eval_res" where
"eval φ I = (if wf_fo_intp φ I then res (eval_fmla φ I) else Wf_error)"

lemma eval_fmla_proj_sat:
fixes φ :: "('a :: infinite, 'b) fo_fmla"
assumes "wf_fo_intp φ I"
shows "rep (eval_fmla φ I) = proj_sat φ I"
using eval_fmla_correct[OF assms]
by (auto simp: fo_rep)

lemma eval_sound:
fixes φ :: "('a :: infinite, 'b) fo_fmla"
assumes "eval φ I = Fin Z"
shows "Z = proj_sat φ I"
proof -
have "wf φ I (eval_fmla φ I)"
using eval_fmla_correct assms
by (auto simp: eval_def split: if_splits)
then show ?thesis
using assms fo_res_fin fo_res_infin
by (fastforce simp: eval_def fo_rep split: if_splits)
qed

lemma eval_complete:
fixes φ :: "('a :: infinite, 'b) fo_fmla"
assumes "eval φ I = Infin"
shows "infinite (proj_sat φ I)"
proof -
have "wf φ I (eval_fmla φ I)"
using eval_fmla_correct assms
by (auto simp: eval_def split: if_splits)
then show ?thesis
using assms fo_res_fin
by (auto simp: eval_def fo_rep split: if_splits)
qed

end

end
```