Theory Completeness_Instance

section ‹Instance of completeness theorem›

theory Completeness_Instance imports Unification_Theorem Completeness begin

interpretation unification using unification by unfold_locales auto

thm lifting

lemma lift:
  assumes fin: "finite C ∧ finite D"
  assumes apart: "vars⇩l⇩s C ∩ vars⇩l⇩s D = {}"
  assumes inst⇩1: "instance_of⇩l⇩s C' C"
  assumes inst⇩2: "instance_of⇩l⇩s D' D"
  assumes appl: "applicable C' D' L' M' σ"
  shows "∃L M τ. applicable C D L M τ ∧
                   instance_of⇩l⇩s (resolution C' D' L' M' σ) (resolution C D L M τ)"
using assms lifting by metis

thm completeness

theorem complete:
  assumes finite_cs: "finite Cs" "∀C∈Cs. finite C"
  assumes unsat: "∀(F::hterm fun_denot) (G::hterm pred_denot) . ¬eval⇩c⇩s F G Cs"
  shows "∃Cs'. resolution_deriv Cs Cs' ∧ {} ∈ Cs'"
using assms completeness by -

thm completeness_countable

theorem complete_countable:
  assumes inf_uni: "infinite (UNIV :: ('u :: countable) set)"
  assumes finite_cs: "finite Cs" "∀C∈Cs. finite C"
  assumes unsat: "∀(F::'u fun_denot) (G::'u pred_denot). ¬eval⇩c⇩s F G Cs"
  shows "∃Cs'. resolution_deriv Cs Cs' ∧ {} ∈ Cs'"
using assms completeness_countable by -

thm completeness_nat

theorem complete_nat:
  assumes finite_cs: "finite Cs" "∀C∈Cs. finite C"
  assumes unsat: "∀(F::nat fun_denot) (G::nat pred_denot) . ¬eval⇩c⇩s F G Cs"
  shows "∃Cs'. resolution_deriv Cs Cs' ∧ {} ∈ Cs'"
using assms completeness_nat by -

end