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