Theory Completeness

section ‹Completeness›

theory Completeness
  imports Countermodel EPathHintikka
begin

text ‹In this theory, we prove that the prover is complete with regards to the SeCaV proof system
  using the abstract completeness framework.›

text ‹We start out by specializing the abstract completeness theorem to our prover.
  It is necessary to reproduce the final theorem here so we can alter it to state that our prover
  produces a proof tree instead of simply stating that a proof tree exists.›
theorem epath_prover_completeness:
  fixes A :: tm list and z :: fm list
  defines t  secavProver (A, z)
  shows (fst (root t) = (A, z)  wf t  tfinite t) 
    ( steps. fst (shd steps) = (A, z)  epath steps  Saturated steps)
    (is ?A  ?B)
proof -
  { assume ¬ ?A
    with assms have ¬ tfinite (mkTree rules (A, z))
      unfolding secavProver_def using wf_mkTree fair_rules by simp
    then obtain steps where ipath (mkTree rules (A, z)) steps using Konig by blast
    with assms have fst (shd steps) = (A, z)  epath steps  Saturated steps
      by (metis UNIV_I fair_rules ipath.cases ipath_mkTree_Saturated mkTree.simps(1) prod.sel(1)
          wf_ipath_epath wf_mkTree)
    then have ?B by blast
  }
  then show ?thesis by blast
qed

text ‹This is an abbreviation for validity under our bounded semantics
  (for well-formed interpretations).›
abbreviation
  uvalid z  u (e :: nat  tm) f g. is_env u e  is_fdenot u f 
    (p  set z. usemantics u e f g p)

text ‹The sequent in the first state of a saturated escape path is not valid.
  This follows from our results in the theories EPathHintikka and Countermodel.›
lemma epath_countermodel:
  assumes fst (shd steps) = (A, z) and epath steps and Saturated steps
  shows ¬ uvalid z
proof
  assume uvalid z
  moreover have Hintikka (tree_fms steps) (is Hintikka ?S)
    using assms escape_path_Hintikka assms by simp
  moreover have p  set z. p  tree_fms steps
    using assms shd_sset by (metis Pair_inject prod.collapse pseq_def pseq_in_tree_fms)
  then have g. p  set z. ¬ usemantics (terms ?S) (E ?S) (F ?S) g p
    using calculation(2) Hintikka_counter_model assms by blast
  moreover have is_env (terms ?S) (E ?S) is_fdenot (terms ?S) (F ?S)
    using is_env_E is_fdenot_F by blast+
  ultimately show False
    by blast
qed

text ‹Combining the results above, we can prove completeness with regards to our bounded
  semantics: if a sequent is valid under our bounded semantics, the prover will produce a finite,
  well-formed proof tree with the sequent at its root.›
theorem prover_completeness_usemantics:
  fixes A :: tm list
  assumes uvalid z
  defines t  secavProver (A, z)
  shows fst (root t) = (A, z)  wf t  tfinite t
  using assms epath_prover_completeness epath_countermodel by blast

text ‹Since our bounded semantics are sound, we can derive our main completeness theorem as
  a corollary: if a sequent is provable in the SeCaV proof system, the prover will produce a finite,
  well-formed proof tree with the sequent at its root.›
corollary prover_completeness_SeCaV:
  fixes A :: tm list
  assumes  z
  defines t  secavProver (A, z)
  shows fst (root t) = (A, z)  wf t  tfinite t
proof -
  have uvalid z
    using assms sound_usemantics by blast
  then show ?thesis
    using assms prover_completeness_usemantics by blast
qed

end