From Mike Gordon 6 Apr 89
Date: Thu, 6 Apr 89 16:57 BST
From: Mike Gordon <mjcg%cam.sri.com%ai.sri.com@munnari.oz>
To: info-hol@clover.ucdavis.edu
Subject: HOL88 news and bug report
Status: RO

                 |============================|
                 |                            |
                 | HOL 88 NEWS AND BUG REPORT |
                 | -------------------------- |
                 |                            |
                 |        Mike Gordon         |
                 |                            |
                 |   Cambridge, 6 April 1989  |
                 |                            |
                 |============================|


The next release of HOL will be HOL88.1.05 and will be sent to HOL
distribution sites within the next few days.  Version 1.05 contains a number
of features to support libraries in a uniform way, together with five new
libraries.

   1. The ICL tautology checker (code for this has already been distributed
      via info-hol).

   2. A theory containing definitions of the concepts of monotonicity,
      continuity, fixed-points and chain-completeness (i.e. admitting
      induction) for polymorphic predicates. Various basic lemmas are proved,
      concluding with the validity of Scott induction (also called
      fixed-point induction and computation induction) in the following form:

         |- !(p:(*->bool)->bool) fun.
             ADMITS_INDUCTION p /\
             CONTINUOUS fun     /\
             p BOTTOM           /\
             (!f. p f ==> p(fun f))
             ==>
             p(FIX fun)

  3. The experimental tools to support programming logics in HOL
     decribed in the paper:

       "Mechanizing Programming Logics in Higher Order Logic",
       by M.J.C. Gordon, in "Current Trends in Hardware Verification and
       Automated Theorem Proving" edited by P.A. Subrahmanyam and
       Graham Birtwistle, Springer-Verlag, 1989.

     This library is provided primarily to help readers of the paper who
     want more details. The tools in the library were implemented to test
     the ideas and are not likely to be useful for serious software
     verification. Eventually, it is hoped to implement practical tools
     to support reasoning about imperative programs.

  4. Elsa Gunter's library developing first-order and higher-order group
     theory, including the notions of subgroup, left coset, normal subgroup,
     quotient group, homomorphism, and isomorphism.

  5. Elsa Gunther's development of the basic algebraic and order-
     theoretic structure of the integers and basic algebraic properties
     of modular arithmetic.

-------------------------------------------------------------------------

Since HOL88.1.00 was released a number of small bugs have emerged. These
are mainly due to differences between the the version of Franz Lisp used at
SRI (currently Opus 38.69) and other versions.

A bug in GEN_TAC has also come to light. This causes the tactic to fail
in some circumstances where it should work. Specifically, if GEN_TAC
is applied to a goal

   [t1; ... ;tn], !x.t

where "x" is free in one of the assumptions t1, ... ,tn, then although the
correct subgoal is produced, i.e.

   [t1; ... ;tn], t[x'/x]

(where "x'" is a variant of "x" not free in the assumptions), the proof part
is

   \[th]. GEN "x" (INST ["x","x'"] th)

which will generate a failure from GEN "x", as "x" is free in the assumptions.
The fix is to rename "x'" back to "x" by alpha-conversion after the
generalization, rather than by instantiation before it. A suitable proof
function to do this is:

   \[th]. let th' = GEN "x'" th
          in
          EQ_MP (GEN_ALPHA_CONV "x" (concl th')) th'

To fix HOL replace the definition of X_GEN_TAC in ml/tactics.ml by:

   let X_GEN_TAC x' :tactic =
    if not(is_var x')
     then failwith `X_GEN_TAC`
     else
      \(asl,w).((let x,body = dest_forall w
                 in
                 if x=x'
                  then
                   ([(asl,body)], \[th]. GEN x' th)
                  else
                   ([(asl,subst[x',x]body)],
                     \[th]. let th' = GEN x' th
                            in
                            EQ_MP (GEN_ALPHA_CONV x (concl th')) th'))
                ? failwith `X_GEN_TAC`);;

This also slighly optimizes the tactic to avoid a redundant substitution
and alpha-conversion when "x" is not free in the assumptions.

All known bugs are corrected in HOL88.1.05.

-------------------------------------------------------------------------