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