# Theory Prover

chapter ‹The prover›
section ‹Proof search procedure›
theory Prover
imports SeCaV
"HOL-Library.Stream"
Abstract_Completeness.Abstract_Completeness
Abstract_Soundness.Finite_Proof_Soundness
"HOL-Library.Countable"
"HOL-Library.Code_Lazy"
begin
text ‹This theory defines the actual proof search procedure.›
subsection ‹Datatypes›
text ‹A sequent is a list of formulas›
type_synonym sequent = ‹fm list›
text ‹We introduce a number of rules to prove sequents.
These rules mirror the proof system of SeCaV, but are higher-level in the sense that they apply to
all formulas in the sequent at once. This obviates the need for the structural Ext rule.
There is also no Basic rule, since this is implicit in the prover.›