Quelle  Results.thy

section ‹Results›

theory Results imports Soundness Completeness Sequent_Calculus_Verifier begin

text ‹In this theory, we collect our soundness and completeness results and prove some extra results
 linking the SeCaV proof system, the usual semantics of SeCaV, and our bounded semantics.›

subsection ‹Alternate semantics›

text ‹The existence of a finite, well-formed proof tree with a formula at its root implies that the
 formula is valid under our bounded semantics.›
corollary prover_soundness_usemantics:
  assumes ‹tfinite t› ‹wf t› ‹is_env u e› ‹is_fdenot u f›
  shows ‹∃p ∈ set (rootSequent t). usemantics u e f g p›
  using assms prover_soundness_SeCaV sound_usemantics by blast

text ‹The prover returns a finite, well-formed proof tree if and only if the sequent to be proved is
 valid under our bounded semantics.›
theorem prover_usemantics:
  fixes A :: ‹tm list› and z :: ‹fm list›
  defines ‹t ≡ secavProver (A, z)›
  shows ‹tfinite t ∧ wf t ⟷ uvalid z›
  using assms prover_soundness_usemantics prover_completeness_usemantics
  unfolding secavProver_def by fastforce

text ‹The prover returns a finite, well-formed proof tree for a single formula if and only if the
 formula is valid under our bounded semantics.›
corollary
  fixes p :: fm
  defines ‹t ≡ secavProver ([], [p])›
  shows ‹tfinite t ∧ wf t ⟷ uvalid [p]›
  using assms prover_usemantics by simp

subsection ‹SeCaV›

text ‹The prover returns a finite, well-formed proof tree if and only if the sequent to be proven is
 provable in the SeCaV proof system.›
theorem prover_SeCaV:
  fixes A :: ‹tm list› and z :: ‹fm list›
  defines ‹t ≡ secavProver (A, z)›
  shows ‹tfinite t ∧ wf t ⟷ (⊨!!! z)›
  using assms prover_soundness_SeCaV prover_completeness_SeCaV
  unfolding secavProver_def by fastforce

text ‹The prover returns a finite, well-formed proof tree if and only if the single formula to be
 proven is provable in the SeCaV proof system.›
corollary
  fixes p :: fm
  defines ‹t ≡ secavProver ([], [p])›
  shows ‹tfinite t ∧ wf t ⟷ (⊨!!! [p])›
  using assms prover_SeCaV by blast

subsection ‹Semantics›

text ‹If the prover returns a finite, well-formed proof tree, some formula in the sequent at the
 root of the tree is valid under the usual SeCaV semantics.›
corollary prover_soundness_semantics:
  assumes ‹tfinite t› ‹wf t›
  shows ‹∃p ∈ set (rootSequent t). semantics e f g p›
  using assms prover_soundness_SeCaV sound by blast

text ‹If the prover returns a finite, well-formed proof tree, the single formula in the sequent at
 the root of the tree is valid under the usual SeCaV semantics.›
corollary
  assumes ‹tfinite t› ‹wf t› ‹snd (fst (root t)) = [p]›
  shows ‹semantics e f g p›
  using assms prover_soundness_SeCaV complete_sound(2) by metis

text ‹If a formula is valid under the usual SeCaV semantics, the prover will return a finite,
 well-formed proof tree with the formula at its root when called on it.›
corollary prover_completeness_semantics:
  fixes A :: ‹tm list›
  assumes ‹∀(e :: nat ==> nat hterm) f g. semantics e f g p›
  defines ‹t ≡ secavProver (A, [p])›
  shows ‹fst (root t) = (A, [p]) ∧ wf t ∧ tfinite t›
proof -
  have ‹⊨!!! [p]›
    using assms complete_sound(1) by blast
  then show ?thesis
    using assms prover_completeness_SeCaV by blast
qed

text ‹The prover produces a finite, well-formed proof tree for a formula if and only if that formula
 is valid under the usual SeCaV semantics.›
theorem prover_semantics:
  fixes A :: ‹tm list› and p :: fm
  defines ‹t ≡ secavProver (A, [p])›
  shows ‹tfinite t ∧ wf t ⟷ (∀(e :: nat ==> nat hterm) f g. semantics e f g p)›
  using assms prover_soundness_semantics prover_completeness_semantics
  unfolding secavProver_def by fastforce

text ‹Validity in the two semantics (in the proper universes) coincide.›
theorem semantics_usemantics:
  ‹(∀(e :: nat ==> nat hterm) f g. semantics e f g p) ⟷
 (∀(u :: tm set) e f g. is_env u e ⟶ is_fdenot u f ⟶ usemantics u e f g p)›
  using prover_semantics prover_usemantics by simp

end