Notes on HOL 4, Kananaskis-9 release

We are pleased to announce the Kananaskis-9 release of HOL 4.

Contents

• New features
• Bugs fixed
• New tools
• New examples
• Incompatibilities

New features:

• The Define function for making function definitions now treats each clause (each conjunct) of the definition as independent when assessing the types of the new functions’ parameters. For example, the following now works as a definition (termination still has to be proved manually):

   (f x = x + 1 + g (x > 4)) ∧
   (g x = if x then f 0 else 1)

In earlier releases, the parser would have rejected this because the two x parameters would have been required to have the same types (in the clause for f, the author wants x to have type :num, and in the clause for g, type :bool).

This feature is most useful when dealing with algebraic types with numerous constructors, where it can be a pain to keep the names of parameters under constructors apart.

Thanks to Scott Owens for the feature suggestion.

• The compilation of pattern-matching in function definitions now attempts to be cleverer about organising its nested case-splits. This should result in less complicated definitions (and accompanying induction principles).

Thanks to Thomas Türk for the implementation of this feature.

Bugs fixed:

• Type abbreviations involving array types (of the form ty1[ty2]) weren’t being pretty-printed. Thanks to Hamed Nemati for the bug report. (GitHub issue)
• It was possible to prove a theorem which caused an unexportable theory. Thanks to Joseph Chan for the bug report. (GitHub issue)
• The error messages printed by, and the documentation for, new_type_definition have been improved. Thanks to Rob Arthan for
  the bug report. (GitHub issue)
• Holmake’s parsing of nested conditional directives (ifdef, ifeq, ifndef etc.) was incorrect.
• Evaluation and simplification were not correctly handling (real valued) terms such as 0 * 1/2 and 1/2 * 0.
• Parsing code for tracking the way overloaded constants should be printed stored information in a data structure that grew unreasonably when theories were loaded. Thanks to Scott Owens for the bug report.
• The emacs mode got confused when called on to open a theory whose name included the substring _fun_. Thanks to Magnus Myreen for the bug report.

New tools:

• There is a new tactic HINT_EXISTS_TAC designed to instantiate existential goals. If the goal is of the form

   ∃x. P(x) ∧ Q(x) ∧ R(x)

and there is an assumption of the form Q(t) (say), then HINT_EXISTS_TAC applied to this goal will instantiate the existential with the term t.

Thanks to Vincent Aravantinos for the implementation of this tactic.

• A new tactic, suffices_by, an infix, taking two arguments, a quotation and a tactic. When ``some term suffices_by tac is executed, the system attempts to prove that `some term` implies the current goal by applying `tac`. The sub-goal(s) resulting from the application of `tac` will be presented to the user, along with `some term`. (GitHub issue)

New examples:

• Theories in examples/parsing to do with context-free languages, their properties and Parsing Expression Grammars. The material not to do with PEGs is derived from Aditi Barthwal’s PhD thesis, with more still to be updated and brought across.
• Theories in examples/ARM_security_properties provide proofs of several security lemmas for the ARM Instruction Set Architecture. To obtain guarantees that arbitrary (and unknown) user processes are able to run isolated from privileged software and other user processes, instruction level noninterference and integrity properties are provided, along with proofs that transitions to privileged modes can only occur in a controlled manner. A proof tool is included, which assists the verification of relational state predicates semi-automatically.

The work has been done as part of the PROSPER project by members from KTH Royal Institute of Technology and SICS Swedish ICT. Some of the obtained theorems are tied to that project (but can be adopted for others), while some guarantees are generally applicable.

Incompatibilities:

• The MEM constant has been replaced with an abbreviation that maps that string to λe l. e ∈ set l. In other words, if you enter MEM x mylist, the underlying term would be x ∈ set mylist (recall also that set is another name for LIST_TO_SET). The pretty-printer will reverse this transformation so that the same term will print as MEM e l. The entry-points for making MEM-terms in listSyntax do the right thing. Similarly, exporting code with EmitML will continue to work.

Thus, SML code that takes MEM-terms apart using functions like rand and rator will likely need to be adjusted. If the SML code uses listSyntax.{dest,mk,is}_mem, it will be fine. (GitHub issue)

• The case-constants generated for algebraic data types now have different types. The value that is “switched on” is now the first argument of the constant rather than the last. The names of these constants have also changed, emphasising the change. For example, the old constant for natural numbers, num_case had type

   α → (num → α) → num → α

Now the case constant for the natural numbers is called num_CASE and has type

   num → α → (num → α) → α

This change is invisible if the “case-of” syntax is used.

This change makes more efficient evaluation (with EVAL) of expressions with case constants possible.

In addition, the bool_case constant has been deleted entirely: when the arguments are flipped as above it becomes identical to COND (if-then-else). This means that simple case-expressions over booleans will print as if-then-else forms. Thus

   > ``case b of T => 1 | F => 3``;
   val it = ``if b then 1 else 3``: term

More complicated case expressions involving booleans will still print with the case form:

   > ``case p of (x,T) => 3 | (y,F) => y``;
   val it =
     ``case p of (x,T) => 3 | (x,F) => x``: term

At the ML level, we have tried to retain a degree of backwards compatibility. For example, the automatically defined case constants for algebraic types will still be saved in their home-theories with the name “type_case_def”. In addition, case terms for the core types of the system (options, lists, numbers, pairs, sums, etc) can still be constructed and destructed through functions in the relevant typeSyntax modules in the same way. For example, numSyntax.mk_num_case still has the type

   term * term * term -> term

and the returned term-triple still corresponds to the 0-case, the successor-case and the number-argument (in that order), as before. This is despite the fact that the underlying term has those sub-terms in a different order (the number-argument comes first). (GitHub issue)

• The various printing traces in the Goalstack module have been renamed to all be of the form "Goalstack.<some_name>". For example, what was the trace "goalstack print goal at top" is now "Goalstack.print_goal_at_top". This change collects all the goalstack-related traces together when the traces are listed (e.g., with the traces() command). There is also a new trace, "Goalstack.show_stack_subgoal_count", which, if true (the default), includes the number of sub-goals currently under consideration when a goalstack is printed.
• The -r command-line option to Holmake now forces recursive behaviour (even with cleaning targets, which is a new feature), rather than being a shorter form of the --rebuild_deps flag.

HOL 4, Kananaskis-9