Quelle  Prover.thy

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.›
datatype rule
  = AlphaDis | AlphaImp  | AlphaCon
  | BetaCon | BetaImp | BetaDis
  | DeltaUni | DeltaExi
  | NegNeg
  | GammaExi | GammaUni

subsection ‹Auxiliary functions›

text ‹Before defining what the rules do, we need to define a number of auxiliary functions needed
 for the semantics of the rules.›

text ‹listFunTm is a list of function and constant names in a term›
primrec listFunTm :: ‹tm ==> nat list› and listFunTms :: ‹tm list ==> nat list›where
  ‹listFunTm (Fun n ts) = n # listFunTms ts›
| ‹listFunTm (Var n) = []›
| ‹listFunTms [] = []›
| ‹listFunTms (t # ts) = listFunTm t @ listFunTms ts›

text ‹generateNew uses the ‹listFunTms› function to obtain a fresh function index›
definition generateNew :: ‹tm list ==> nat› where
  ‹generateNew ts ≡ 1 + foldr max (listFunTms ts) 0›

text ‹subtermTm returns a list of all terms occurring within a term›
primrec subtermTm :: ‹tm ==> tm list› where
  ‹subtermTm (Fun n ts) = Fun n ts # remdups (concat (map subtermTm ts))›
| ‹subtermTm (Var n) = [Var n]›

text ‹subtermFm returns a list of all terms occurring within a formula›
primrec subtermFm :: ‹fm ==> tm list› where
  ‹subtermFm (Pre _ ts) = concat (map subtermTm ts)›
| ‹subtermFm (Imp p q) = subtermFm p @ subtermFm q›
| ‹subtermFm (Dis p q) = subtermFm p @ subtermFm q›
| ‹subtermFm (Con p q) = subtermFm p @ subtermFm q›
| ‹subtermFm (Exi p) = subtermFm p›
| ‹subtermFm (Uni p) = subtermFm p›
| ‹subtermFm (Neg p) = subtermFm p›

text ‹subtermFms returns a list of all terms occurring within a list of formulas›
abbreviation ‹subtermFms z ≡ concat (map subtermFm z)›

text ‹subterms returns a list of all terms occurring within a sequent.
 This is used to determine which terms to instantiate Gamma-formulas with.
 We must always be able to instantiate Gamma-formulas, so if there are no terms in the sequent,
 the function simply returns a list containing the first function.›
definition subterms :: ‹sequent ==> tm list› where
  ‹subterms z ≡ case remdups (subtermFms z) of
 [] ==> [Fun 0 []]
 | ts ==> ts›

text ‹We need to be able to detect if a sequent is an axiom to know whether a branch of the proof
 is done. The disjunct ‹Neg (Neg p) ∈ set z› is not necessary for the prover, but makes the proof
 of the lemma ‹branchDone_contradiction› easier.›
fun branchDone :: ‹sequent ==> bool› where
  ‹branchDone [] = False›
| ‹branchDone (Neg p # z) = (p ∈ set z ∨ Neg (Neg p) ∈ set z ∨ branchDone z)›
| ‹branchDone (p # z) = (Neg p ∈ set z ∨ branchDone z)›

subsection ‹Effects of rules›

text ‹This defines the resulting formulas when applying a rule to a single formula.
 This definition mirrors the semantics of SeCaV.
 If the rule and the formula do not match, the resulting formula is simply the original formula.
 Parameter A should be the list of terms on the branch.›
definition parts :: ‹tm list ==> rule ==> fm ==> fm list list› where
  ‹parts A r f = (case (r, f) of
 (NegNeg, Neg (Neg p)) ==> [[p]]
 | (AlphaImp, Imp p q) ==> [[Neg p, q]]
 | (AlphaDis, Dis p q) ==> [[p, q]]
 | (AlphaCon, Neg (Con p q)) ==> [[Neg p, Neg q]]
 | (BetaImp, Neg (Imp p q)) ==> [[p], [Neg q]]
 | (BetaDis, Neg (Dis p q)) ==> [[Neg p], [Neg q]]
 | (BetaCon, Con p q) ==> [[p], [q]]
 | (DeltaExi, Neg (Exi p)) ==> [[Neg (sub 0 (Fun (generateNew A) []) p)]]
 | (DeltaUni, Uni p) ==> [[sub 0 (Fun (generateNew A) []) p]]
 | (GammaExi, Exi p) ==> [Exi p # map (λt. sub 0 t p) A]
 | (GammaUni, Neg (Uni p)) ==> [Neg (Uni p) # map (λt. Neg (sub 0 t p)) A]
 | _ ==> [[f]])›

text ‹This function defines the Cartesian product of two lists.
 This is needed to create the list of branches created when applying a beta rule.›
primrec list_prod :: ‹'a list list ==> 'a list list ==> 'a list list› where
  ‹list_prod _ [] = []›
| ‹list_prod hs (t # ts) = map (λh. h @ t) hs @ list_prod hs ts›

text ‹This function computes the children of a node in the proof tree.
 For Alpha rules, Delta rules and Gamma rules, there will be only one sequent, which is the result
 of applying the rule to every formula in the current sequent.
 For Beta rules, the proof tree will branch into two branches once for each formula in the sequent
 that matches the rule, which results in ‹2ⁿ› branches (created using 🪙‹list_prod›).
 The list of terms in the sequent needs to be updated after applying the rule to each formula since
 Delta rules and Gamma rules may introduce new terms.
 Note that any formulas that don't match the rule are left unchanged in the new sequent.›
primrec children :: ‹tm list ==> rule ==> sequent ==> sequent list› where
  ‹children _ _ [] = [[]]›
| ‹children A r (p # z) =
 (let hs = parts A r p; A' = remdups (A @ subtermFms (concat hs))
 in list_prod hs (children A' r z))›

text ‹The proof state is the combination of a list of terms and a sequent.›
type_synonym state = ‹tm list × sequent›

text ‹This function defines the effect of applying a rule to a proof state.
 If the sequent is an axiom, the effect is to end the branch of the proof tree, so an empty set of
 child branches is returned.
 Otherwise, we compute the children generated by applying the rule to the current proof state,
 then add any new subterms to the proof states of the children.›
primrec effect :: ‹rule ==> state ==> state fset› where
  ‹effect r (A, z) =
 (if branchDone z then {||} else
 fimage (λz'. (remdups (A @ subterms z @ subterms z'), z'))
 (fset_of_list (children (remdups (A @ subtermFms z)) r z)))›

subsection ‹The rule stream›

text ‹We need to define an infinite stream of rules that the prover should try to apply.
 Since rules simply do nothing if they don't fit the formulas in the sequent, the rule stream is
 just all rules in the order: Alpha, Delta, Beta, Gamma, which guarantees completeness.›
definition ‹rulesList ≡ [
 NegNeg, AlphaImp, AlphaDis, AlphaCon,
 DeltaExi, DeltaUni,
 BetaImp, BetaDis, BetaCon,
 GammaExi, GammaUni
 ›

text ‹By cycling the list of all rules we obtain an infinite stream with every rule occurring
 infinitely often.›
definition rules where
  ‹rules = cycle rulesList›

subsection ‹Abstract completeness›

text ‹We write effect as a relation to use it with the abstract completeness framework.›
definition eff where
  ‹eff ≡ λr s ss. effect r s = ss›

text ‹To use the framework, we need to prove enabledness.
 This is trivial because all of our rules are always enabled and simply do nothing if they don't
 match the formulas.›
lemma all_rules_enabled: ‹∀st. ∀r ∈ i.R (cycle rulesList). ∃sl. eff r st sl›
  unfolding eff_def by blast

text ‹The first step of the framework is to prove that our prover fits the framework.›
interpretation RuleSystem eff rules UNIV
  unfolding rules_def RuleSystem_def
  using all_rules_enabled stream.set_sel(1)
  by blast

text ‹Next, we need to prove that our rules are persistent.
 This is also trivial, since all of our rules are always enabled.›
lemma all_rules_persistent: ‹∀r. r ∈ R ⟶ per r›
  by (metis all_rules_enabled enabled_def per_def rules_def)

text ‹We can then prove that our prover fully fits the framework.›
interpretation PersistentRuleSystem eff rules UNIV
  unfolding PersistentRuleSystem_def RuleSystem_def PersistentRuleSystem_axioms_def
  using all_rules_persistent enabled_R
  by blast

text ‹We can then use the framework to define the prover.
 The mkTree function applies the rules to build the proof tree using the effect relation, but the
 prover is not actually executable yet.›
definition ‹secavProver ≡ mkTree rules›

abbreviation ‹rootSequent t ≡ snd (fst (root t))›

end