Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
To: cclai@ruby.ee.nsysu.edu.tw (Chi-Chia Lai)
Cc: info-hol@leopard.cs.byu.edu, tfm@dcs.gla.ac.uk
Subject: Re: abstract data type in Isabelle
In-Reply-To: Your message of "Mon, 06 Mar 1995 17:17:16 CST." <9503060917.AA03843@Ruby.ee.nsysu.edu.tw>
Date: Mon, 06 Mar 1995 20:09:56 +0000
From: Tom Melham <tfm@dcs.gla.ac.uk>
Message-ID: <"swan.cl.cam.:039780:950306214546"@cl.cam.ac.uk>


>    It seems that the HOL system[Gordon] can support the definition of
>    abstract data type.(we can know this from the paper "A simple Graph
>    Theory and Its Application in Railway Signalling"[Wai Wong,1992,IEEE].

There are numerous type definitions described in the HOL literature.
Many of these are what I would call "concrete type definitions",
in the sense that they are basically free algebras (trees, and such
like). However, "abstract" data types are also possible, though
the ADT methodology (abstracting from the representation and using
abstract properties only) is enforced only by conventions governing
the use of the logic, and not by the system itself.  For numerous
examples, see:

   T. F. Melham, `Automating Recursive Type Definitions in 
   Higher Order Logic', in Current Trends in Hardware Verification and
   Automated Theorem Proving, edited by G. Birtwistle and 
   P. A. Subrahmanyam (Springer-Verlag, 1989), pp. 341-386.

which can be found via my WWW page (http://www.dcs.gla.ac.uk/~tfm/).
I believe Isabelle also has some support for type definitions.

As regards true abstract type definitions, my long-standing proposal
for adding a type specification rule to the HOL logic will allow us
to have these.  See

   T. F. Melham, `The HOL Logic Extended with Quantification over 
   Type Variables', Formal Methods in System Design,
   vol. 3, nos. 1-2 (August 1993), pp. 7-24.

for a partial explanation.  I hope to incorporate this proposal
into HOL2000, the next gerenation of HOL theorem prover.

Tom