*** HOL2P System ***

This is an experimental implementation of the logic HOL2P [1] as an
extension and modification of John Harrison's HOL-LIGHT (2.20) theorem
prover [2]. From the user point of view, the HOL2P system is
essentially a variation of HOL-LIGHT with additional type and term
constructs as well as accompanying syntax, rules and tactics.


*** Warnings

The HOL2P system is made available with the aim of furthering research
into higher order theorem proving. The system is currently of
beta-version quality - it has not yet been widely tested and it might
still contain significant bugs.

Prospective users need to have a sound working knowledge of HOL-LIGHT,
and this is assumed in the instructions below.


*** Installation

This implementation of HOL2P depends on OCAML 3.09 (tried with
3.09.3). Installation should consist simply of unpacking the
zip-file, changing to the distribution directory and starting ocaml.
Then type

   #use "hol2p.ml";;                    

for running HOL2P. This will load the HOL2P logical core, as well as a
minimal set of HOL-LIGHT developments about booleans, classical
reasoning, inductive types, pairs, integers, and lists. Please modify
file Hol_light_lib/basic_lib.ml if you want to load further HOL-LIGHT
material.


*** Examples 

Please see the Example directory

   type_quantification.ml  (* simple type quantifier examples *) 
   functor.ml	           (* Functors and natural transformations *) 
   aop.ml		   (* "Algebra of Programming" [3] examples" *)
      
In order to run all included examples, load hol2p into OCaml, and type: 

   #use "hol2p_examples.ml";;        


*** HOL2P Syntax: Types and Terms 

The syntax of HOL2P types and terms is that of HOL-LIGHT with some
extensions and restrictions.

Universal types: (% 'A. T) 
   e.g. (% 'A. 'A list)  for (/\ 'A. 'A list)

Type abstraction terms: (\\ 'A. t)  
   e.g. (\\ 'A. (ID : 'A -> 'A)) for (/\ 'A. (ID : 'A -> 'A))

Type application terms: (t:T1)[:T2] 
   e.g.  (f : (% 'A. 'A))[:num] for   (f:(/\ 'A. 'A)) [num]) 

The indication of the type of the argument term t in a type
application term can be omitted if t is a constant, or if it is a
variable whose type has already been inferred by parsing of preceding
occurrences. In this case, the type application syntax becomes simply
t[:T]

In HOL2P, there is a smallness restriction on the bound type variables
in universal types and type abstraction terms, as well as the type
arguments of type application terms. Small type variables are
distinguished by a leading apostrophe, such as 'A. Type variables that
do not start with a leading apostrophe are taken to be unrestricted,
they are therefore not permissible in those places where a small type
is mandatory.

Type operator variables are distinguished by a leading underscore
character such as _T. Other type variables are not allowed to start
with that character. 

Like normal type variable, type operator variables can be
auto-generated by the system during parsing. Such variables are
numbered and have the form "_?n", for example "_?12345". Theorems
should normally not contain auto-generated system type operator
variables. The reason is explained below in the section about explicit
instantiation of theorems containing type operator variables.

Type inference in HOL2P is incomplete, and users sometimes need to add
explicit type (operator) variable instantations or type annotations.


*** Type quantification 

Type quantification notation is implemented as syntactic sugar that is
only relevant for parsing and printing. Within the system, HOL2P terms
as described above are used. The translations are:

   (!! A. t)   <=>   ((\\ 'A. t) = (\\ 'A. T))
   (?? A. t)   <=>   (~((\\ 'A. t) = (\\ 'A. F)))


*** Explicit Type (Operator) Instantiation for Parsing

When entering terms that involve (possibly implicit) type operator
variables, it is often neccessary to add explicit type (operator)
variable instantations or type annotations. This is so because the 
automatic type inference and term instantiation will match a type
operator variable only with a type constructor or another type
operator variable.

To make this clearer, consider constant FUNCTOR (see file example/functor.ml): 

   FUNCTOR: (% 'A 'B. ('A -> 'B) -> 'A _T -> 'B _T) -> bool 

and the following three inputs: 

(I1) FUNCTOR (\\ 'A 'B. (ID: ('A -> 'B) -> 'A  -> 'B))
(I2) FUNCTOR (\\ 'A 'B. (MAP: ('A -> 'B) -> 'A  list -> 'B list))
(I3) FUNCTOR (\\ 'A 'B. ((\f.MAP(MAP f)) 
                        :('A -> 'B) -> ('A list)list -> ('B list)list))

In the HOL2P system, only input (I2) will be parsed successfully to a
term, and that term will include an instance of FUNCTOR where the type
operator variable _T is replaced by the type constructor "list". Parsing
(I1) and (I3) will lead to a unification failure.

In order to overcome the problem with inputs (I1) and (I3), it is
necessary to inform the parser of the required replacement of _T in
the instantiation of FUNCTOR. For this purpose, an auxiliary construct
TYINST was introduced into the HOL2P system. It associates type
(operator) variables in constants with types resp. type operators. In
the example, we have:

(I1')  TYINST (_T: (% 'A. 'A)) FUNCTOR (\\ 'A 'B. ID) 
(I3')  TYINST (_T: (% 'A. ('A list) list)) FUNCTOR (\\ 'A 'B. \f.MAP(MAP f))

Please note that similar to normal HOL type annotations, TYINST is
purely an auxiliary device that guides type inference. It is not
contained in the term obtained from the parsing, and is also not
visible when terms are printed. The TYINST directive always applies to
a single argument which must be a constant containing the type
(operator) variable in question. Please see file functor.ml for more
examples, including cases of constants that require the instantiation
of more than one type operator variable.


*** Explicit Instantiation of Theorems containing Type Operator Variables 

When instantiating a theorem containing a type operator variable, the
HOL2P system has the same limitation as in the case of parsing,
e.g. the system will automatically only find those instantiations
where a type operator variable _T is replaced by a type constructor
such as "list" or another type operator variable. In cases where this
is insufficient, the HOL_LIGHT function INST_TYPE can be used to
explicitly instantiate both type operator variables as well as normal
type variables. For example, in the proofs that ID resp (MAP (MAP F))
are functors, the following explicit instantiations are necessary:

   ... SIMP_TAC[INST_TYPE [`: % 'A. 'A`,`:_T`]  FUNCTOR] ...
   ... SIMP_TAC[INST_TYPE [`: % 'A. ('A list)list`, `:_T`] FUNCTOR] ... 


*** Avoiding Auto-generated Type Operator Variables in Theorems 

It is usually a bad idea to let the system automatically invent type
operator variables in a theorem, and the user will be warned when such
a goal if formulated. The problem is caused by the fact that
automatically generated system type operator variables such as
"_?12345" can not be explicitly instantiated by the user, and hence
the INST_TYPE function can not be used to create custom instances of
such a theorem. Instead, when formulating a goal, users should
explicitly give a name (such as _T) to all occurring type operator
variables, either by adding suitable type annotations or by TYINST
directives, see files functor.ml and aop.ml for examples.


*** Implicit Type Applications in Terms 

HOL2P terms often contain type applications that appear redundant,
just as they do in System F. In order to improve the readability of
theorems, and to shorten the input, the HOL2P system allows to omit
certain type applications. When the parser encounters a universally
typed constant c that occurs in a context that does not have universal
type, type applications will be added to c until it is no longer of
universal type. As an example, here is the homomorphism composition
theorem from file aop.ml first stated with explicit type applications:

(? f2. HOMO (phi: % 'A 'B. ('A -> 'B) -> 'A _T -> 'B _T) [:'A] [:'B]) f1 f2 h1 
    /\ HOMO (phi [:'B] [:'C] f2 f3 h2) /\ FUNCTOR phi 
  ==> HOMO (phi[:'A][:'C]) f1 f3 (h2 o h1) 

and here is the goal statement when type applications are omitted: 

 (? f2. HOMO (phi: % 'A 'B. ('A -> 'B) -> 'A _T -> 'B _T) f1 f2 h1 
    /\ HOMO phi f2 f3 h2) /\ FUNCTOR phi ==> HOMO phi f1 f3 (h2 o h1)

The implicit addition of type applications also works for variables
provided the parser has already inferred that they belong to a
universal type. 

Users might prefer to input all type applications in terms
themselves. This can be enforced with the setting: 

   add_tyapps_automatically := false;; 

This flag only effects the parsing of terms. Terms are always shown
with full type applications in output.


*** Rules and Tactics  

The normal HOL-LIGHT rules and tactics also apply in HOL2P.  Some
HOL2P specific tactics are described in hol2p_tactics.ml. HOL2P
theorems and proofs can be found in the example files.


*** Hints and Caveats 

When entering terms including universally quantified types such as 
(f: %'A.'A), do not omit the blank before the "%" sign as the character
sequence ":%" will be parsed as a single token.

When explicitly instantiating a type operator variable using TYINST or
INST_TYPE, the replacement has to be written using the universal type
syntax such as `: % 'A. 'A list`, see the examples above.

The type of a constant can be identified with the HOL-LIGHT function
get_generic_type.


*** Credits 

The HOL2P system is essentially an extension and modification of the
HOL-LIGHT theorem prover. HOL-LIGHT was written by John Harrison, and
he deserves the credit for all the HOL-LIGHT code included or modified
in HOL2P. Of course, any errors made during the construction of HOL2P
are the sole responsibility of the HOL2P author.

Please see the accompanying HOL2P and HOL-LIGHT LICENSE files for
copyright declarations and conditions of use.


*** Finally

Please contact me if you have comments or questions about HOL2P.

Norbert Voelker (norbert@essex.ac.uk) 

******************


[1] Norbert Voelker. HOL2P - A System of Classical Higher Order Logic with
Second Order Polymorphism, Proceedings of TPHOLs'07, Kaiserslautern,
Germany, LNCS 4732, 2007. 

[2] John Harrison: The HOL Light theorem prover. 
See http://www.cl.cam.ac.uk/users/jrh13/hol-light/index.html. 

[3] Richard Bird and Oege de Moor: Algebra of Programming, Prentice Hall, 1996.