Theory Eval_FO

theory Eval_FO
  imports "HOL-Library.Infinite_Typeclass" 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