# Theory Results

```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
```