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