Theory Prover

chapter ‹The prover›

section ‹Proof search procedure›

theory Prover
  imports SeCaV

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 listwhere
  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 2n branches (created using text‹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))