Using HOL90, we have defined a number of new data types to describe IP datagrams, IPSEC security mechanisms, and mobile registration messages. Performing proofs however, remains a human-intensive process. To better support the use of our mechanized logic, we have developed a general infrastructure base, based on earlier work[12], for creating automated and interactive procedures to prove goals about inductively defined relations.
The infrastructure provides tools to build interactive functions and goal-directed support functions, procedures to eliminate existentially quantified variables from terms, and tactics to generalize existentially quantified rules. Many of the functions are generic, expecting as arguments the list of inference rules returned by new_inductive_definition and a list of the relevant combinators. In our case, the list of relevant combinators includes all of the type constructors from the newly defined types (key, keyuse, keyfact, item, and proposition).
For many applications, validation of the inductively defined rules is, at least initially, of greater importance than automated proofs. For the automated proofs to be useful, their construction must be understood. Thus, it is valuable for the automated procedures to inform the user what rules are relevant and when rules are applied to a goal.
Interactive support is provided by a collection of parameterized functions that suggest an appropriate rule to apply based on the current goal or a term. (suggested_rules() and rules_for_term(), respectively). Using these mechanisms, users don't need to remember all the rules that may apply, but can request a list of potentially useful rules. Many protocol logics have a significant number of inference rules ([4] lists 44 rules). Even SVO logic, which was designed to significantly reduce the number of rules compared with other protocol logics, requires 23 rules.
We have also developed a tactic generating function, make_suggest_tac that returns a tactic specialized for a list of inference rules and a list of combinators. The tactic searches for and then applies, an appropriate rule to apply based on the current goal. In practice, this tactic appears to provide a significant improvement over tactics that try every rule. The tactic also outputs what rules where chosen to apply in a given situation. The displayed list of decisions can assist the user understand why a proof is correct and often, why it fails.
A second general tactic EXISTS_ELIM_TAC has also been developed to search for witnesses to replace existentially quantified variables. The tactic searches the assumption list for candidates that match the variable's usage in the goal. After replacement, goals can often be reduced by rewriting with the assumption list. For performance considerations, the tactic defers rewriting until all existentially quantified variables have been replaced.
Using the above two tactics, a general strategy was developed and programmed into a tactic (IND_RULES_TAC). The initial proofs of the lemmas required a fair number of steps, but with the use of the IND_RULES_TAC, the proofs are performed with only a few tactics. The resulting proofs also require less time with fewer intermediate theorems generated. At this point in development, the tactic does not backtrack and so occasionally, the user must select the correct rule.
The final general support mechanism developed supports generalizing some of the rules returned by new_inductive_definition. When creating a new inductive definition, there are often rules with existentially quantified variables in the antecedent that could instead be universally quantified. While this is not always beneficial, in many cases, proofs are simplified.