Trindemossen-1

Release notes for HOL4, Trindemossen 1

(Released: 25 April 2024)

We are pleased to announce the Trindemossen 1 release of HOL4.
We have changed the name (from Kananaskis) because of the kernel change reflected by the new efficient compute tool (see below).

Contents

• New features
• Bugs fixed
• New theories
• New tools
• New Examples
• Incompatibilities

New features:

• The HOL_CONFIG environment variable is now consulted when HOL sessions begin, allowing for a custom hol-config configuration at a non-standard location, or potentially ignoring any present hol-config.
  If the variable is set, any other hol-config file will be ignored.
  If the value of HOL_CONFIG is a readable file, it will be used.

• There is a new theorem attribute, unlisted, which causes theorems to be saved/stored in the usual fashion but kept somewhat hidden from user-view.
  Such theorems can be accessed with DB.fetch, and may be passed to other tools though the action of other attributes, but will not appear in the results of DB.find and DB.match, and will not occur as SML bindings in theory files.

• Holmake will now look for .hol_preexec files in the hierarchy surrounding its invocation.
  The contents of such files will be executed by the shell before Holmake begins its work.
  See the DESCRIPTION manual for more.

• Holmake (at least under Poly/ML) now stores most of the products of theory-building in a “dot”-directory .holobjs.
  For example, if fooScript.sml is compiled, the result in the current directory is the addition of fooTheory.sig only.
  The files fooTheory.sml, fooTheory.dat, fooTheory.uo and fooTheory.ui are all deposited in the .holobjs directory.
  This reduces clutter.

• Paralleling the existing Excl form for removing specific theorems from a simplifier invocation, there is now a ExclSF form (also taking a string argument) that removes a simpset fragment from the simplifier.
  For example

       > simp[ExclSF "BOOL"] ([], “(λx. x + 1) (6 + 1)”);
       val it = ([([], “(λx. x + 1) 7”)], fn)
  

  where the BOOL fragment includes the treatment of β-reduction.

Bugs fixed:

• Fix a failure to define a polymorphic datatype with name a.

New theories:

• A theory of "contiguity types", as discussed in the paper Specifying Message Formats with Contiguity Types, ITP 2021. (DOI: 10.4230/LIPIcs.ITP.2021.30)

  Contiguity types express formal languages where later parts of a
  string may depend on information held earlier in the string. Thus
  contig types capture a class of context-sensitive languages. They
  are helpful for expressing serialized data containing, for example,
  variable length arrays. The soundness of a parameterized matcher is
  proved.

• permutes: The theory of permutations for general and finite sets, originally
  ported from HOL-Light's Library/permutations.ml.

• keccak: Defines the SHA-3 standard family of hash functions, based on the
  Keccak permutation and sponge construction. Keccak256, which is widely used
  in Ethereum, is included and was the basis for this work. A rudimentary
  computable version based on sptrees is included; faster evaluation using
  cvcompute is left for future work.

New tools:

• The linear decision procedure for the reals (REAL_ARITH, REAL_ARITH_TAC
  and REAL_ASM_ARITH_TAC) have been updated by porting the latest code from
  HOL-Light. There are two versions: those in the existing RealArith package
  only support integral-valued coefficients, while those in the new package
  RealField support rational-valued coefficients (this includes division of
  reals, e.g. |- x / 2 + x /2 = x can be proved by RealField.REAL_ARITH).
  Users can explicitly choose between different versions by explicitly opening
  RealArith or RealField in their proof scripts. If realLib were opened,
  the maximal backward compatibilities are provided by first trying the old
  solver (now available as RealArith.OLD_REAL_ARITH, etc.) and (if failed)
  then the new solver. Some existing proofs from HOL-Light can be ported to
  HOL4 more easily.

• New decision procedure for the reals ported from HOL-Light: REAL_FIELD,
  REAL_FIELD_TAC and REAL_ASM_FIELD_TAC (in the package RealField). These
  new tools first try RealField.REAL_ARITH and then turn to new solvers
  based on calculations of Grobner's Basis (from the new package Grobner).

• Multiplying large numbers more efficiently:

  In src/real there is a new library bitArithLib.sml which improves the
  performance of large multiplications for the types :num and :real.
  The library uses arithmetic of bitstrings in combination with the Karatsuba
  multiplication algorithm.
  To use the library, it has to be loaded before the functions that should be
  evaluated are defined.

• Fast in-logic computation primitive:
  A port of the Candle theorem prover's primitive rule for computation,
  described in the paper "Fast, Verified Computation for Candle" (ITP 2023),
  has been added to the kernel. The new compute primitive works on certain
  operations on a lisp-like datatype of pairs of numbers:

       Datatype: cv = Pair cv cv
                    | Num num
       End
  

  This datatype and its operations are defined in cvScript.sml, and the
  compute primitive cv_compute is accessible via the library
  cv_computeLib.sml (both in src/cv_compute).

  There is also new automation that enables the use of cv_compute on
  functional HOL definitions which do not use the :cv type. In particular,
  cv_trans translates such definitions into equivalent functions operating
  over the :cv type. These can then be evaluated using cv_eval, which uses
  cv_compute internally. Both cv_trans and cv_eval can be found in the
  new cv_transLib.

  Some usage examples are located in examples/cv_compute. See the
  DESCRIPTION manual for a full description of the functionality offered by
  cv_compute.

  NB. To support cv_compute, the definitions of DIV and MOD over natural
  numbers num have been given specifications for the case when the second
  operand is zero. We follow HOL Light and Candle in defining n DIV 0 = 0 and
  n MOD 0 = n. These changes make DIV and MOD match the way Candle's
  compute primitive handles DIV and MOD.

• Polarity-aware theorem-search. Extending what is available through DB.find and DB.match, the DB.polarity_search allows the user to search for explicitly negative or positive occurrences of the specified pattern.
  Thanks to Eric Hall for this contribution.

New examples:

• Dependability Analysis:
  Dependability is an umbrella term encompassing Reliability, Availability and Maintainability.
  Two widely used dependability modeling techniques have been formalized namely, Reliability Block Diagrams (RBD) and Fault Trees (FT).
  Both these techniques graphically analyze the causes and factors contributing the functioning and failure of the system under study.
  Moreover, these dependability techniques have been highly recommended by several safety standards, such as IEC61508, ISO26262 and EN50128,
  for developing safe hardware and software systems.

  The new recursive datatypes are defined to model RBD and FT providing compositional features in order to analyze complex systems with arbitrary
  number of components.

      Datatype: rbd = series (rbd list)
                    | parallel (rbd list)
                    | atomic (α event)
      End
  
      Datatype: gate = AND (gate list)
                     | OR (gate list)
                     | NOT gate
                     | atomic (α event)
      End
  

  Some case studies are also formalized and placed with dependability theories, for illustration purposes, including smart grids, WSN data transport protocols, satellite solar arrays, virtual data centers, oil and gas pipeline systems and an air traffic management system.

• large_numberTheory (in examples/probability): various versions of The Law of Large Numbers (LLN) of Probability Theory.

  Some LLN theorems (WLLN_uncorrelated and SLLN_uncorrelated) previously in probabilityTheory
  are now moved to large_numberTheory with unified statements.

• Vector and Matrix theories (in examples/vector) translated from HOL-Light's Multivariate/vectors.ml.

• Relevant Logic (in examples/logic/relevant-logic): material contributed by James Taylor, mechanising a number of foundational results for propositional relevant logic.
  Three proof systems (two Hilbert, one natural deduction) are shown equivalent, and two model theories (the Routley-Meyer ternary-relation Kripke semantics, and Goldblatt’s “cover” semantics) are shown sound and complete with respect to the proof systems.

• armv8-memory-model (in examples/arm): a port by Anthony Fox of Viktor Vafeiadis’s Coq formalization of the Armv8 Memory Model, which is based on the official mixed-size Armv8 memory model and associated paper.

• __p-adic numbe...

Kananaskis-14

Release notes for HOL4, Kananaskis-14

(Released: 3 February 2021)

We are pleased to announce the Kananaskis-14 release of HOL4.

Contents

• New features
• Bugs fixed
• New theories
• New tools
• New Examples
• Incompatibilities

New features:

• The special Type syntax for making type abbreviations can now map to temp_type_abbrev (or temp_type_abbrev_pp) by adding the local attribute to the name of the abbreviation.

  For example

     Type foo[local] = “:num -> bool # num”
  

  or

     Type foo[local,pp] = “:num -> bool # num”
  

  Thanks to Magnus Myreen for the feature suggestion.

• We have added a special syntactic form Overload to replace various flavours of overload_on calls. The core syntax is exemplified by

     Overload foo = “myterm”
  

  Attributes can be added after the name. Possible attributes are local (for overloads that won’t be exported) and inferior to cause a call inferior_overload_on (which makes the overload the pretty-printer’s last choice).

  Thanks to Magnus Myreen for the feature suggestion.

• The Holmake tool will now build multiple targets across multiple directories in parallel. Previously, directories were attacked one at a time, and parallelisation only happened within those directories. Now everything is done at once. The existing -r option takes on a new meaning as part of this change: it now causes Holmake to build all targets in all directories accessible through INCLUDES directives. Without -r, Holmake will build just those dependencies necessary for the current set of targets (likely files/theories in the current directory).

• It is now possible to write let-expressions more smoothly inside monadic do-od blocks. Rather than have to write something like

     do
       x <- M1;
       let y = E
       in
         do
           z <- M2 x y;
           return (f z);
         od
     od
  

  one can replace the let-bindings with uses of the <<- arrow:

     do
       x <- M1;
       y <<- E;
       z <- M2 x y;
       return (f z)
     od
  

  (The <<- line above is semantically identical to writing y <- return E, but is nonetheless syntactic sugar for a let-expression.)

  The pretty-printer reverses this transformation.

  Thanks to Hrutvik Kanabar for the implementation of this feature.

• There is (yet) another high-level simplification entry-point: gs (standing for “global simplification”). Like the others in this family this has type

     thm list -> tactic
  

  and interprets theorems as rewrites as with the others. This tactic simplifies all of a goal by repeatedly simplifying goal assumptions in turn (assuming all other assumptions as it goes) until no change happens, and then finishes by simplifying the goal conclusion, assuming all of the (transformed) assumptions as it does so.

  There are three variants on this base (with the same type): gns, gvs and gnvs. The presence of the v indicates a tactic that eliminates variables (as is done by rw and some others), and the presence of the n causes assumptions to not be stripped as they are added back into the goal. Stripping (turned on by default) is the effect behind strip_assume_tac (and strip_tac) when these tactics add to the assumptions. It causes, for example, case-splits when disjunctions are added.

  We believe that gs will often be a better choice than the existing fs and rfs tactics.

• Automatic simplification of multiplicative terms over the real numbers is more aggressive and capable. Multiplicative terms are normalised, with coefficients being gathered, and variables sorted and grouped (e.g., z * 2 * x * 3 turns into 6 * (x * z)). In addition, common factors are eliminated on either side of relation symbols (<, ≤, and =), and occurrences of inv (⁻¹) and division are rearranged as much as possible (e.g., z * x pow 2 * 4 = x⁻¹ * 6 turns into x = 0 ∨ 2 * (x pow 3 * z) = 3). To turn off normalisation over relations within a file, use

     val _ = diminish_srw_ss [“RMULRELNORM_ss”]
  

  To additionally stop normalisation, use

     val _ = diminish_srw_ss [“RMULCANON_ss”]
  

  These behaviours can also be turned off in a more fine-grained way by using Excl invocations.

• The Induct_on tactic is now more generous in the goals it will work on when inducting on an inductively defined relation. For example, if one’s goal was

     ∀s t. FINITE (s ∪ t) ∧ s ⊆ t ⇒ some-concl
  

  and the aim was to do an induction using the principle associated with finite-ness’s inductive characterisation, one had to manually turn the goal into something like

     ∀s0. FINITE s0 ==> ∀s t. s0 = s ∪ t ∧ s ⊆ t ⇒ some-concl
  

  before applying Induct_on ‘FINITE’.

  Now, Induct_on does the necessary transformations first itself.

• The Inductive and CoInductive syntaxes now support labelling of specific rules. The supported syntax involves names in square brackets in column 0, as per the following:

     Inductive dbeta:
     [~redex:]
       (∀s t. dbeta (dAPP (dABS s) t) (nsub t 0 s)) ∧
     [~appL:]
       (∀s t u. dbeta s t ⇒ dbeta (dAPP s u) (dAPP t u)) ∧
     [~appR:]
       (∀s t u. dbeta s t ⇒ dbeta (dAPP u s) (dAPP u t)) ∧
     [~abs:]
       (∀s t. dbeta s t ⇒ dbeta (dABS s) (dABS t))
     End
  

  The use of the leading tilde (~) character causes the substitution of the “stem” name (here dbeta) and an underscore into the name. Thus in this case, there will be four theorems saved, the first of which will be called dbeta_redex, corresponding to the first conjunct. If there is no tilde, the name is taken exactly as given. Theorem attributes such as simp, compute etc. can be given in square brackets after the name and before the colon. For example, [~redex[simp]:].

  The given names are both saved into the theory (available for future users of the theory) and into the Poly/ML REPL.

• There is a new using infix available in the tactic language. It is an SML function of type tactic * thm -> tactic, and allows user-specification of theorems to use instead of the defaults. Currently, it works with the Induct_on, Induct, Cases_on and Cases tactics. All of these tactics consult global information in order to apply specific induction and cases theorems. If the using infix is used, they will attempt to use the provided theorem instead.

  Thus one can do a “backwards” list induction by writing

     Induct_on ‘mylist’ using listTheory.SNOC_INDUCT
  

  The using infix has tighter precedence than the various THEN operators so no extra parentheses are required.

Bugs fixed:

• In extrealTheory: the old definition of extreal_add wrongly allowed PosInf + NegInf = PosInf, while the definition of extreal_sub wrongly allowed PosInf - PosInf = PosInf and NegInf - NegInf = PosInf. Now these cases are unspecified, as is division-by-zero (which is indeed allowed for reals in realTheory). As a consequence, now all EXTREAL_SUM_IAMGE- related theorems require that there must be no mixing of PosInf and NegInf in the sum elements. A bug in ext_suminf with non-positive functions is also fixed.

  There is a minor backwards-incompatibility: the above changes may lead to more complicated proofs when using extreals, while better alignment with textbook proofs is achieved, on the other hand.

• Fix soundness bug in the HolyHammer translations to first-order. Lambda-lifting definitions were stated as local hypothesis but were printed in the TPTP format as global definitions. In a few cases, the global definition captured some type variables causing a soundness issue. Now, local hypothesis are printed locally under the quantification of type variables in the translated formula.

New theories:

• Univariate differential and integral calculus (based on Henstock-Kurzweil Integral, or gauge integral) in derivativeTheory and integrationTheory. Ported by Muhammad Qasim and Osman Hasan from HOL Light (up to 2015).

• Measure and probability theories based on extended real numbers, i.e., the type of measure (probability) is α set -> extreal. The following new (or updated) theories are provided:

  sigma_algebraTheory
  ~ Sigma-algebra and other system of sets

  measureTheory
  ~ Measure Theory defined on extended reals

  real_borelTheory
  ~ Borel-measurable sets generated from reals

  borelTheory
  ~ Borel sets (on extended reals) and Borel-measurable functions

  lebesgueTheory
  ~ Lebesgue integration theory

  martingaleTheory
  ~ Martingales based on sigma-finite filtered measure space

  probabilityTheory
  ~ Probability theory based on extended reals

  Notable theorems include: Carathéodory's Extension Theorem (for semirings), the construction of 1-dimensional Borel and Lebesgue measure spaces, Radon-Nikodym theorem, Tonelli and Fubini's theorems (product measures), Bayes' Rule (Conditional Probability), Kolmogorov 0-1 Law, Borel-Cantelli Lemma, Markov/Chebyshev's inequalities, convergence concepts of random sequences, and simple versions of the Law(s) of Large Numbers.

  There is a major backwards-incompatibility: old proof scripts based on real-valued measure and probability theories should now open the following ...

Kananaskis 13

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

(Released: 20 August 2019)

Contents

• New features
• Bugs fixed
• New theories
• New tools
• New Examples
• Incompatibilities

New features:

• We have implemented new syntaxes for store_thm and save_thm, which better satisfy the recommendation that name1 and name2 below should be the same:

     val name1 = store_thm("name2", tm, tac);
  

  Now we can remove the “code smell” by writing

     Theorem name: term-syntax
     Proof tac
     QED
  

  which might look like

     Theorem name:
       ∀x. P x ⇒ Q x
     Proof
       rpt strip_tac >> ...
     QED
  

  This latter form must have the Proof and QED keywords in column 0 in order for the lexing machinery to detect the end of the term and tactic respectively.
  Both forms map to applications of Q.store_thm underneath, with an ML binding also made to the appropriate name.
  Both forms allow for theorem attributes to be associated with the name, so that one can write

     Theorem ADD0[simp]: ∀x. x + 0 = x
     Proof tactic
     QED
  

  Finally, to replace

     val nm = save_thm(“nm”, thm_expr);
  

  one can now write

     Theorem nm = thm_expr
  

  These names can also be given attributes in the same way.

  There is also a new local attribute available for use with store_thm, save_thm and the Theorem syntax above.
  This attribute causes a theorem to not be exported when export_theory is called, making it local-only.
  Use of Theorem-local is thus an alternative to using prove or Q.prove.
  In addition, the Theorem-local combination can be abbreviated with Triviality; one can write Triviality foo[...] instead of Theorem foo[local,...].

• Relatedly, there is a similar syntax for making definitions.
  The idiom is to write

     Definition name[attrs]:
       def
     End
  

  Or

     Definition name[attrs]:
       def
     Termination
       tactic
     End
  

  The latter form maps to a call to tDefine; the former to xDefine.
  In both cases, the name is taken to be the name of the theorem stored to disk (it does not have a suffix such as _def appended to it), and is also the name of the local SML binding.
  The attributes given by attrs can be any standard attribute (such as simp), and/or drawn from Definition-specific options:

  • the attribute schematic alllows the definition to be schematic;
  • the attribute nocompute stops the definition from being added to the global compset used by EVAL
  • the attribute induction=iname makes the induction theorem that is automatically derived for definitions with interesting termination be called iname.
    If this is omitted, the name chosen will be derived from the name of the definition: if name ends with _def or _DEF, the induction name will replace this suffix with _ind or _IND respectively; otherwise the induction name will simply be name with _ind appended.

  Whether or not the induction= attribute is used, the induction theorem is also made available as an SML binding under the appropriate name.
  This means that one does not need to follow one’s definition with a call to something like DB.fetch or theorem just to make the induction theorem available at the SML level.

• Similarly, there are analogous Inductive and CoInductive syntaxes for defining inductive and coinductive relations (using Hol_reln and Hol_coreln underneath).
  The syntax is

     Inductive stem:
        quoted term material
     End
  

  or

     CoInductive stem:
        quoted term material
     End
  

  where, as above, the Inductive, CoInductive and End keywords must be in the leftmost column of the script file.
  The stem part of the syntax drives the selection of the various theorem names (e.g., stem_rules, stem_ind, stem_cases and stem_strongind for inductive definitions) for both the SML environment and the exported theory.
  The actual names of new constants in the quoted term material do not affect these bindings.

• Finally, there are new syntaxes for Datatype and type-abbreviation.
  Users can replace val _ = Datatype`...` with

     Datatype: ...
     End
  

  and val _ = type_abbrev("name", ty) with

     Type name = ty
  

  if the abbreviation should introduce pretty-printing (which would be done with type_abbrev_pp), the syntax is

     Type name[pp] = ty
  

  Note that in both Type forms the ty is a correct ML value, and may thus require quoting.
  For example, the set abbreviation is established with

     Type set = “:α -> bool”
  

• Holmake now understands targets whose suffixes are the string Theory to be instructions to build all of the files associated with a theory.
  Previously, to specifically get fooTheory built, it was necessary to write

     Holmake fooTheory.uo
  

  which is not particularly intuitive.

  Thanks to Magnus Myreen for the feature suggestion.

• Users can now remove rewrites from simpsets, adjusting the behaviour of the simplifier.
  This can be done with the -* operator

     SIMP_TAC (bool_ss -* [“APPEND_ASSOC”]) [] >> ...
  

  or with the Excl form in a theorem list:

     simp[Excl “APPEND_ASSOC”] >> ...
  

  The stateful simpset (which is behind srw_ss() and tactics such as simp, rw and fs) can also be affected more permanently by making calls to delsimps:

     val _ = delsimps [“APPEND_ASSOC”]
  

  Such a call will affect the stateful simpset for the rest of the containing script-file and in all scripts that inherit this theory.
  As is typical, there is a temp_delsimps that removes the rewrite for the containing script-file only.

• Users can now require that a simplification tactic use particular rewrites.
  This is done with the Req0 and ReqD special forms.
  The Req0 form requires that the goalstate(s) pertaining after the application of the tactic have no sub-terms that match the pattern of the theorems’ left-hand sides.
  The ReqD form requires that the number of matching sub-terms should have decreased.
  (This latter is implicitly a requirement that the original goal did have some matching sub-terms.)
  We hope that both forms will be useful in creating maintainable tactics.
  See the DESCRIPTION manual for more details.

  Thanks to Magnus Myreen for this feature suggestion (Github issue).

• The emacs editor mode now automatically switches new HOL sessions to the directory of the (presumably script) file where the command is invoked.
  Relatedly there is a backwards incompatibility: the commands for creating new sessions now also always create fresh sessions (previously, they would try to make an existing session visible if there was one running).

• The emacs mode’s M-h H command used to try to send the whole buffer to the new HOL session when there was no region high-lighted.
  Now the behaviour is to send everything up to the cursor.
  This seems preferable: it helps when debugging to be able to have everything up to a problem-point immediately fed into a fresh session.
  (The loading of the material (whole prefix or selected region) is done “quietly”, with the interactive flag false.)

• Holmakefiles can now refer to the new variable DEFAULT_TARGETS in order to generate a list of the targets in the current directory that Holmake would attempt to build by default.
  This provides an easier way to adjust makefiles than that suggested in the release notes for Kananaskis-10.

• String literals can now be injected into other types (in much the same way as numeric literals are injected into types such as real and rat).
  Either the standard double-quotes can be used, or two flavours of guillemet, allowing e.g., “‹foo bar›”, and “«injected-HOL-string\n»”.
  Ambiguous situations are resolved with the standard overloading resolution machinery.
  See the REFERENCE manual’s description of the add_strliteral_form function for details.

• The Q.SPEC_THEN function (also available as qspec_then in bossLib) now type-instantiates provided theorems à la ISPEC, and tries all possible parses of the provided quotation in order to make this work.
  The Q.ISPEC_THEN function is deprecated.

Bugs fixed:

• smlTimeout.timeout: The thread attributes are now given which eliminates concurrency issues during TacticToe recording.
  This function now raises the exception FunctionTimeout instead of Interrupt if the argument function exceeds the time limit.

New theories:

• real_topologyTheory: a rather complete theory of Elementary
  Topology in Euclidean Space, ported by Muhammad Qasim and Osman
  Hasan from HOL-light (up to 2015). The part of General Topology
  (independent of realTheory) is now available at
  topologyTheory; the old topologyTheory is renamed to
  metricTheory.

  There is a minor backwards-incompatibility: old proof scripts using
  the metric-related results in previous topologyTheory should now
  open metricTheory instead. (Thanks to Chun Tian for this work.)

• nlistTheory: a development of the bijection between lists of natural numbers and natural numbers.
  Many operation...

Kananaskis-12

Release notes for HOL4, Kananaskis-12

(Released: 20 June 2018)

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

We would like to dedicate this release to the memory of Mike Gordon (1948–2017), HOL’s first developer and the leader of the research group to which many of us were attached at various stages of our careers.

The official download tarball for this release is available from Sourceforge, with shasum equal to 8d4754f11411c15501a23c218c0fe5561607de6c, or attached below.

Contents

• New features
• Bugs fixed
• New theories
• New tools
• New Examples
• Incompatibilities

New features:

• Holmake under Poly/ML (i.e., for the moment only Unix-like systems (including OSX/MacOS, and Windows with Cygwin or the Linux subsystem)) now runs build scripts concurrently when targets do not depend on each other.
  The degree of parallelisation depends on the -j flag, and is set to 4 by default.
  Output from the build processes is logged into a .hollogs sub-directory rather than interleaved randomly to standard out.

• Theory files generated from script files now load faster.
  The machinery enabling this generates xTheory.dat files alongside xTheory.sig and xTheory.sml files.
  Thanks to Thibault Gauthier for the work implementing this.

• We now support monadic syntax with a do-notation inspired by Haskell’s.
  For example, the mapM function might be defined:

     Define‘(mapM f [] = return []) ∧
            (mapM f (x::xs) =
                   do
                     y <- f x;
                     ys <- mapM f xs;
                     return (y::ys);
                   od)’;
  

  The HOL type system cannot support this definition in its full polymorphic generality.
  In particular, the above definition will actually be made with respect to a specific monad instance (list, option, state, reader, etc).
  There are API entry-points for declaring and enabling monads in the monadsyntax module.
  For more details see the DESCRIPTION manual.

• Users can define their own colours for printing types, and free and bound variables when printing to ANSI terminals by using the PPBackEnd.ansi_terminal backend.
  (The default behaviour on what is called the vt100_terminal is to have free variables blue, bound variables green, type variables purple and type operators “blue-green”.)
  Thanks to Adam Nelson for this feature.
  Configuring colours under emacs is done within emacs by configuring faces such as hol-bound-variable.

• We now support the infix $ notation for function application from Haskell.
  For example

     f $ g x $ h y
  

  is a low-parenthesis way of writing f (g x (h y)).
  The dollar-operator is a low-precedence (tighter than infix , but looser than other standard operators), right-associative infix.
  This is a “parse-only technology”; the pretty-printer will always use the “traditional” syntax with parentheses as necessary and what might be viewed as an invisible infix application operator.

Bugs fixed:

• Pretty-printing of record type declarations to TeX now works even if there are multiple types with the same name (necessarily from different theory segments) in the overall theory.

• Pretty-printing has changed to better mesh with Poly/ML’s native printing, meaning that HOL values embedded in other values (e.g., lists, records) should print better.

New theories:

• We have promoted the theories of cardinality results for various flavours of infinite sets, and of ordinal numbers to src from examples.
  There is a minor backwards-incompatibility: references to examples/set-theory/hol_sets (in Holmakefile INCLUDES specifications for example) should simply be deleted.
  Any theory can build on these theories (cardinalTheory, ordinalTheory) simply by open-ing them in the relevant script file.

New tools:

• For every algebraic type, the TypeBase now automatically proves what we term “case-equality” rewrite theorems that have LHSes of the form

    ((case x of con1_pattern => e1 | con2_pattern => e2 ...) = v)
  

  For example, the case-equality theorem for the α option type is

    (option_CASE opt nc sc = v) ⇔
       (opt = NONE) ∧ (nc = v) ∨
       ∃x. (opt = SOME x) ∧ (sc x = v)
  

  where option_CASE opt nc sc is the general form of the term that underlies a case expression over an option value opt.

  These theorems can be powerful aids in simplifications (imagine for example that v is T and nc is F), so we have made it easy to include them in arguments to simp, fs, rw etc.
  The CaseEq function takes a string and returns the corresponding theorem, so that CaseEq "option" will return the theorem above.
  The CaseEqs function takes a list of strings so that the simplifier-argument list doesn’t need to repeat CaseEq invocations, and finally, AllCaseEqs() returns a conjunction of all the TypeBase’s case-equality theorems.
  Then one might write something like

     simp[AllCaseEqs(), thm1, thm2]
  

  for example.

New examples:

• We have resurrected Monica Nesi’s CCS example (from the days of HOL88, in examples/CCS), ported and extended by Chun Tian (based on HOL4’s co-induction package Hol_coreln).
  This includes all classical results of strong/weak bisimilarities and observation congruence, the theory of congruence for CCS, several versions of “bisimulation up to”, “coarsest congruence contained in weak bisimilarity”, and “unique solution of equations” theorems, mainly from Robin Milner’s book, and Davide Sangiorgi’s “unique solutions of contractions” theorem published in 2017.
  There’s also a decision procedure written in SML for computing CCS transitions with the result automatically proved.

• Speaking of HOL88, we have also recovered an old hardware example.
  This work is the verification of a version of a “toy microprocessor” that came to be called Tamarack (see Section 5 of the HOL history paper).
  First done in a system called LCF_LSM by Mike Gordon (around 1983), this was then redone in HOL88 by Jeff Joyce in 1989, and these sources are now ported and available under examples/hardware.
  Thanks to Larry Paulson for finding the HOL88 originals, and to Ramana Kumar and Thomas Tuerk for doing the work porting these to HOL4.

• A theory of the basic syntax and semantics of Linear Temporal Logic formulas, along with a verified translation of such formulas into Generalised Büchi Automata via alternating automata (in examples/logic/ltl).
  This work is by Simon Jantsch.

• A theory of Lambek calculus (categorial grammars of natural or formal languages), in examples/formal-languages/lambek. Ported from Coq contribs by Chun Tian. c.f. "The Logic of Categorial Grammars" by Richard Moot and Christian Retoré.

• A library for regular expressions (examples/formal-languages/regular), including a compiler from regexps to table-driven DFAs. Proofs include standard regexp identities along with the correctness of the compiler. Also, there is a standalone tool regexp2dfa that generates DFAs in a variety of languages. The library also supplies (informal and formal) parsers for regexps in Python syntax. See the README for more details.

Incompatibilities:

• We have decided that the behaviour of irule (aka IRULE_TAC) should not include the finishing rpt conj_tac.
  If users want that after the implicational theorem has been matched against, it is easy enough to add.
  See the Github issue.

• The behaviour of the by and suffices_by tactics has changed.
  Previously, a tactic of the form `term quotation` by tac allowed tac to fail to prove the sub-goal of the term quotation.
  (The result would then be two or more sub-goals, where the first few of these correspond to the state of trying to prove the term quotation after applying tac.)
  This is no longer the case: if tac does not prove the new sub-goal then the overall tactic fails.

  The old implementation of by is available under the name BasicProvers.byA, so it is possible to revert to the old behaviour with the following declaration at the head of one’s script file:

     val op by = BasicProvers.byA
  

  If one wanted to fix possibly broken occurrences to use the new semantics, the following Perl script might be helpful (it was used to adjust the core HOL sources):

     $/ = "\n\n";
  
     while (<>) {
         s/(`[^`]+`)(\s*)by(\s*)(ALL_TAC|all_tac)(\s*)(>-|THEN1)/\1 by/g;
         s/(Tactical\.)?REVERSE(\s*)\((`[^`]+`)(\s*)by(\s*)(ALL_TAC|all_tac)(\s*)\)(\s*)(THEN1|>-)(\s*)\(/\3 suffices_by\8(STRIP_TAC THEN /g;
         s/(Tactical\.)?REVERSE(\s*)\((`[^`]+`)(\s*)by(\s*)(ALL_TAC|all_tac)(\s*)\)(\s*)(THEN1|>-)(\s*)/\3 suffices_by /g;
         s/(`[^`]+`)(\s*)by(\s*)(ALL_TAC|all_tac)(\s*)/sg \1\5/g;
         print;
     }
  

  If the above is called byfix.pl (for example), then a reasonable invocation would be

     perl -i byfix.pl *Script.sml
  

  If one’s workflow was to write things like

     `subgoal` by ALL_TAC THEN1 (tac1 THEN tac2 THEN ...)
  

  and the same workflow makes

     `subgoal` by (tac1 THEN tac2 THEN ...)
  

  difficult (...

Kananaskis 11

Kananaskis-11

(Released: 3 March 2017)

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

New features:

• We have ported HOL Light’s PAT_CONV and PATH_CONV “conversionals”, providing nice machinery for applying conversions to specific sub-terms.

• The tactic PAT_ABBREV_TAC (also available in the Q module) can now use patterns that are more polymorphic than the sub-term in the goal that is ultimately matched. (Github issue)

• We have implemented the rule for constant specification described by Rob Arthan in HOL Constant Definition Done Right.
  The new primitive gen_prim_specification in the kernel is used to implement the new rule, gen_new_specification, and is also used to re-implement new_definition and new_specification.
  We removed prim_constant_definition from the kernel, but kept prim_specification because the new derivation of new_specification uses pairs.
  (Github pull-req)

• Various commands for moving over and selecting HOL tactics in the emacs mode have been improved.
  We have also added a new command hol-find-eval-next-tactic (bound to M-h M-e by default), which selects and highlights the next tactic in the source text, and then applies it to the current goal in the *HOL* buffer.
  This shortcuts the current idiom, which requires the tactic to be highlighted manually, and then applied via M-h e.
  (The advantage of the latter is that one can select specific tactic sequences to be applied all at once.)

• Record updates can now be more polymorphic. For example, if one defined

     Datatype`rcd = <| myset : α -> bool ; size : num |>`
  

  one used to get back an update constant for the myset field:

     rcd_myset_fupd : ((α -> bool) -> (α -> bool)) -> α rcd -> α rcd
  

  Now, the same constant is

     rcd_myset_fupd : ((α -> bool) -> (β -> bool)) -> α rcd -> β rcd
  

  One might use this to define

     Define`img (f:α->β) r = r with myset updated_by IMAGE f`
  

  This definition would have previously been rejected. (Github issue)

  This change can cause incompatibilities.
  If one wants the old behaviour, it should suffice to overload the record update syntax to use a more specific type.
  For example:

     val _ = gen_remove_ovl_mapping
               (GrammarSpecials.recfupd_special ^ "myset")
               ``λf x. rcd_myset_fupd f x``
  
     val _ = Parse.add_record_fupdate(
           "myset", Term.inst[beta |-> alpha] ``rcd_myset_fupd``);
  

• PolyML “heaps” are now implemented with its SaveState technology, used hierarchically.
  This should make heaps smaller as they now only save deltas over the last used heap.

Bugs fixed:

• An embarrassing infinite loop bug in the integration of the integer decision procedures (the Omega test, Cooper’s algorithm) into the simplifier was fixed.

• Theorems can now have names that are the same as SML constructor names (e.g., Empty). (Github issue)

• Holmake will now follow INCLUDES specifications from Holmakefiles when given “phony” targets to build on the command-line. (A typical phony target is all.) As in the past, it will still act only locally if given just a clean target (clean, cleanDeps or cleanAll). To clean recursively, you must also pass the -r flag to Holmake. (Github issue)

• We fixed three problems with Datatype. Thanks to Ramana Kumar for the reports.
  First, Datatype will no longer create a recursive type if the recursive instance is qualified with a theory name other than the current one.
  In other words,

      Datatype`num = C1 num$num | C2`
  

  won’t create a recursive type (assuming this is not called in theory num).
  (Hol_datatype had the same problem.)

  Second, Datatype will handle antiquotations in its input properly (Hol_datatype already did).

  Third, Datatype (and Hol_datatype) allows the definition of identical record types in different theories.

• Attempts to define constants or types with invalid names are now caught much earlier.
  An invalid name is one that contains “non-graphical” characters (as per SML’s Char.isGraph) or parentheses.
  This means that Unicode cannot be used in the kernel’s name for a constant, but certainly doesn’t prevent Unicode being used in overloaded notation.
  Functions such as overload_on, add_rule and set_mapped_fixity can still be used to create pretty notation with as many Unicode characters included as desired.

• Loading theories under Poly/ML would fail unnecessarily if the current directory was unwritable.
  Working in such directories will likely cause problems when and if an export_theory call is made, so there is a warning emitted in this situation, but the load now succeeds.
  Thanks to Narges Khakpour for the bug report.

• The function thm_to_string was creating ugly strings full of special codes (encoding type information) rather than using the “raw” backend.

• Bare record operations (e.g., rcdtype_field, the function that accesses field of type rcdtype) would occasionally pretty-print badly. (Github issue)

New tools:

• Holyhammer: A method for automatically finding relevant theorems for Metis.
  Given a term, the procedure selects a large number of lemmas through different predictors such as KNN or Mepo.
  These lemmas are given to the external provers E-prover (1.9), Vampire (2.6) or Z3 (4.0).
  The necessary lemmas in the provers' proofs are then returned to the user.
  Modifications to the kernels to track dependencies between theorems allow predictors to learn from the induced relation improving future predictions.
  The build of the source directory src/holyhammer needs ocaml (> 3.12.1) installed as well as a recent version of g++ that supports the C++11 standard.
  The three ATPs have to be installed independently.
  At least one of them should be present, preferably E-prover (1.9).

  Thanks to Thibault Gauthier for this tool.

• A principle for making coinductive definitions, Hol_coreln.
  The input syntax is the same as for Hol_reln, that is: a conjunction of introduction rules.
  For example, if one is representing coalgebraic lists as a subset of the type :num → α option, the coinductive predicate specifying the subset would be given as

     val (lrep_ok_rules, lrep_ok_coind, lrep_ok_cases) = Hol_coreln`
       lrep_ok (λn. NONE)
           ∧
       ∀h t.
         lrep_ok t
             ⇒
         lrep_ok (λn. if n = 0 then SOME h else t(n - 1))
     `;
  

  as is now done in src/llist/llistScript.sml.

  Thanks to Andrea Condoluci for this tool.

New examples:

• A theory of balanced binary trees (examples/balanced_bst), based on Haskell code by Leijen and Palamarchuk, and mechanised by Scott Owens. The type supports operations such as insert, union, delete, filters and folds. Operations are parameterised by comparison operators for comparing keys. Balanced trees can themselves be compared.

• A formalisation of pattern matches (examples/pattern_matches).
  Pattern matching is not directly supported by higher-order logic.
  HOL4’s parser therefore compiles case-expressions (case x of ...) to decision trees based on case constants.
  For non-trivial case expressions, there is a big discrepancy between the user’s view and this internal representation.
  The pattern_matches example defines a new general-purpose representation for case expressions that mirrors the input syntax in the internal representation closely.
  Because of this close connection, the new representation is more intuitive and often much more compact.
  Complicated parsers and pretty-printers are no longer required.
  Proofs can more closely follow the user’s intentions, and code generators (like CakeML) can produce better code.
  Moreover, the new representation is strictly more general than the currently used representation.
  The new representation allows for guards, patterns with multiple occurrences of the same bound variable, unbound variables, arithmetic expressions in patterns, and more.
  The example provides the definitions as well as tools to work with the new case-expressions.
  These tools include support for evaluating and simplifying them, a highly configurable pattern compilation algorithm inside the logic, and optimisations like detecting redundant rows and eliminating them.

Incompatibilities:

• The function optionSyntax.dest_none will now unwrap the type of its result, e.g., returning :α rather than :α option when applied to NONE : α option. This brings it into line with the behaviour of listSyntax.dest_nil. See this github issue.

• The functions Q.MATCH_RENAME_TAC and Q.MATCH_ASSUM_RENAME_TAC have been adjusted to lose their second arguments (the list of variable names that are not to be bound). For example, applying Q.MATCH_RENAME_TAC `(f x = Pair c1 c2) ⇒ X` ["X"] to the goal

       ?- (f x = Pair C'' C0') ⇒ (f C'' = f C0')
  

  used to result in the renamed goal

       ?- (f x = Pair c...
  

Kananaskis-10

Release notes for HOL4, Kananaskis-10

(Released: 10 November 2014)

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

Contents

• New features
• Bugs fixed
• New theories
• New tools
• Examples
• Incompatibilities

New features:

• Our TUTORIAL and LOGIC manuals are now available in Italian translations. Work on the DESCRIPTION manual is also far advanced. Many, many thanks to Domenico Masini for doing this work.

• The abbreviation tactics (Q.ABBREV_TAC and others) now handle abstractions as abbreviations better. In particular, if one sets up an abstraction as an abbreviation (e.g., Q.ABBREV_TAC f = (λn. 2 * n + 10)``), then the simplifier will find and replace instances not just of the abstraction itself (the old behaviour), but also instances of applications of the abstraction to arguments. For example, given the abbreviation for f above, the simplifier would turn a goal such as `2 * (z + 1) + 10 < 100` into `f (z + 1) < 100`.

• The MAX_SET function in pred_setTheory is now defined (to have value 0) on the empty set.

• There is an alternative syntax for specifying datatypes. Instead of the Hol_datatype entry-point, one can also use Datatype, which takes a slightly different syntax, inspired by Haskell. This does away with the use of the (somewhat confusing) of and => tokens.

  For example, one would define a simple type of binary tree with

     Datatype`tree = Lf num | Node tree tree`
  

  If the arguments to a constructor are not just simple types (expressible as single tokens), then they need to be enclosed in parentheses. For example:

     Datatype`mytype = Constr mytype ('a -> bool) | BaseCase`
  

  The Hol_datatype entry-point can continue to be used. However, the LaTeX output of EmitTeX uses the new format, and the various DATATYPE constructors used in the EmitML module take quotations in the new format, rather than the old.

• The arithmetic decision procedure for natural numbers will now prove slightly more goals by doing case-splits on boolean sub-terms that are not in the Presburger subset. This means that goals such as

     0 < y ⇒ x < x + (if P then y else y + 1)
  

  are now provable.

• The Vim mode for HOL now supports multiple simultaneous sessions. See its README for details.

• Many of the standard libraries now provide an add_X_compset : compset -> unit (e.g., add_pred_set_compset) to ease building of custom call-by-name evaluation conversions that don't, like EVAL, include everything in the_compset().

• Holmake has a new function, wildcard which allows expansion of “glob” patterns (e.g., *Script.sml) into lists of matching filenames.

• The standard pretty-printer now annotates constants with their types as well as variables. (Note that these annotations are typically only visible by using mouse-over tooltips in the emacs mode.) The annotation also includes the constant’s real name, in the form thy$name, making overloads easier to tell apart.

  For example, this means that it is possible to have integers, reals and numbers all in scope, to write something like MAP (+), and to then see what constants are involved by using the mouse. (See Github issue #39.)

• Unicode is handled slightly better on Windows systems. By default, the pretty-printer avoids printing with Unicode characters there, but can still parse Unicode input successfully. This is important because many of the examples distributed with HOL use Unicode characters in their scripts (nothing in src/ does). This behaviour can be adjusted by toggling the PP.avoid_unicode trace. On Windows this trace is initialised to true; elsewhere it is initialised to false.

Bugs fixed:

• Holmake was unnecessarily quiet when it compiled certain SML files.
• The “munging” code for turning HOL into LaTeX now does a better job of rendering data type definition theorems. (This change is independent of the new underlying syntax described earlier.)
• Pretty-printers added to the system with add_user_printer weren’t having terms-to-be-printed tested against the supplied patterns (except by the gross approximation provided by the built-in term-net structure). Thanks to Ramana Kumar for the bug report.
• Character literals weren’t pretty-printing to LaTeX. We also improved the handling of string literals. Thanks to Ramana Kumar for the bug reports.
• Piotr Trojanek found and fixed many documentation bugs in our various manuals.
• The remove_rules_for_term and temp_remove_rules_for_term functions tended to remove rules for binders as well as the desired rules.

New theories:

• A theory of “list ranges” (listRangeTheory). A range is a term written [ lo ..< hi ], meaning the list consisting of the (natural) numbers from lo up to, but not including, hi. The theory comes with some basic and obvious theorems, such as

     MEM i [lo ..< hi] ⇔ lo ≤ i ∧ i < hi
  

  and

     LENGTH [lo ..< hi] = hi - lo
  

• A new development in src/floating-point, which is a reworking of the theories in src/float. Key differences are listed below.

  1. The data representation:

     • The old ieeeTheory uses a pair :num # num to represent the exponent and fraction widths and a triple :num # num # num to represent sign, exponent and fraction values.

     • The new binary_ieeeTheory makes use of HOL records and bit-vectors. The floating-point type :(α, β) float has values of the form

         <| Sign : word1; Exponent : β word; Significand : α word |>
       

       The fraction and exponent widths are now constrained by the type, which facilitates type-checking and avoids having to pass size arguments to operations.

  2. The new development now supports standard bit-vector encoding schemes. The theory machine_ieeeTheory defines floating-point operations over 16-bit, 32-bit and 64-bit values. For example, the 16-bit floating point operations are defined by mapping to and from the type :(10, 5) float, which is given the type abbreviation :half. Theories for other sizes can be built using machine_ieeeLib.mk_fp_encoding.
  3. There is now syntax support via the structures binary_ieeeSyntax and machine_ieeeSyntax.
  4. Ground term evaluation is now supported for most operations. This can be enabled by loading binary_ieeeLib.
  5. The full development does not build under Moscow ML 2.01, as it makes use of the IEEEReal and PackRealBig basis structures.

• A theory of “simple Patricia trees” (sptreeTheory). This theory implements a type α sptree, which is a finite map from natural numbers to values of type α. (This type is not really a Patricia tree at all; for those, see the other theories in src/patricia.) Values of type α sptree feature efficient lookup, insertion, deletion and union (efficient when evaluated with EVAL or simplified). Though there is a efficient (linear-time) fold operation, it does not iterate over the key-value pairs in key-order.

New tools:

• New libraries enumLib and fmapalLib provide representations in pred_set and finite map types of enumerated constant sets and maps as minimum-depth binary search trees. A suitable total order on the set elements (map arguments) must be supplied, with a conversion for evaluating it; assistance with this is provided. The primary objective has been an IN_CONV, and a similar FAPPLY_CONV, operating with a logarithmic number of comparisons, but additional operations such as UNION_CONV, INTER_CONV, and FUPDATE_CONV are included and have reasonable asymptotic running times. A conversion TC_CONV implements Warshall’s algorithm for transitive closure of a binary relation (treated as a set-valued finite map).

Examples:

• The miniml example has been removed. This work has evolved into the CakeML project. That project’s git repository contains all of the material that was once in the HOL distribution, and, given its continuing evolution, much more besides.

Incompatibilities:

• In relationTheory, the theorems TC_CASES1 and TC_CASES2 have been renamed to TC_CASES1_E and TC_CASES2_E respectively, where the _E suffix indicates that these are elimination rules. In other words, these theorems are of the form TC R x y ⇒ .... This has been done so that new equivalences can be introduced under the old names. For example, TC_CASES1 now states

     TC R x z ⇔ R x z ∨ ∃y. R x y ∧ TC R y z
  

  This change makes the naming consistent with similar theorems RTC_CASES1 and RTC_CASES2 about the reflexive and transitive closure.

• A theorem stating

     ⊢ ¬(0 < n) ⇔ (n = 0)
  

  (for n a natural number) has been added to the automatic rewrites used by SRW_TAC and srw_ss().

• Some new automatic rewrites from pred_setTheory:

  • ⊢ DISJOINT (x INSERT s) t ⇔ DISJOINT s t ∧ x ∉ t (and the version of this with DISJOINT s (x INSERT t) as the l.h.s.)
  • ⊢ ∀f s. INJ f ∅ s
  • ⊢ ∀f s. INJ f s ∅ ⇔ (s = ∅)

• The add_binder and temp_add_binder entry-points in Parse have been removed. They are subsumed by set_fixity <name> Binder and temp_set_fixity <name> Binder respectively. In addition, add_binder was broken, creating an unloadable theory on export.

• There is a new automatic rewrite from oneTheory:

     ⊢ ∀v:one. v = ()
  

  stating that every value in the type one (analogue of SML’s unit type) is equal to the designated value ().

• Constants that print to the TeX backend as symbolic identifiers (e.g., non-alphanumeric tokens like +, **) are now a...

Kananaskis 9

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