Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Fri, 7 Apr 1995 18:24:06 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA066103054;
          Fri, 7 Apr 1995 10:44:14 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Received: from aun.uninett.no by leopard.cs.byu.edu 
          with SMTP (1.37.109.15/16.2) id AA066053035;
          Fri, 7 Apr 1995 10:43:55 -0600
X400-Received: by mta aun.uninett.no in /PRMD=uninett/ADMD= /C=no/; Relayed;
               Fri, 7 Apr 1995 13:55:46 +0200
X400-Received: by /PRMD=uninett/ADMD= /C=no/; Relayed;
               Fri, 7 Apr 1995 13:56:12 +0200
Date: Fri, 7 Apr 1995 13:56:12 +0200
X400-Originator: Einar-A.Snekkenes@ffi.no
X400-Recipients: info-hol@lal.cs.byu.edu
X400-Mts-Identifier: [/PRMD=uninett/ADMD= /C=no/;1278 95/04/07 13:56]
X400-Content-Type: P2-1984 (2)
Content-Identifier: 1278 95/04/07
From: Einar-A.Snekkenes@ffi.no
Message-Id: <"1278 95/04/07 13:56*/G=Einar-A/S=Snekkenes/O=ffi/PRMD=uninett/ADMD= /C=no/"@MHS>
To: info-hol@leopard.cs.byu.edu
Subject: Why "Extension by type specification" ?


------------------------------ Start of body part 1



%=============================================================
% Einar Snekkenes,        | X400 :
G=Einar-A;S=Snekkenes;O=ffi;PRMD=uninett;C=no;
% NDRE,                   | RFC  :  Einar-A.Snekkenes@FFI.NO
% P.B. 25,                | phone : +47 63-80-74-01
% N-2007 Kjeller,         |         +47 63-80-70-00
% Norway                  | fax   : +47 63-80-72-12


------------------------------ Start of body part 2

Why "Extension by type specification" ?

I've had a look at "Introduction to HOL" by M.J.C. Gordon
and T.F. Melham. In chapter 16 they present two ways
of extending a theory with a new type:

  1. Extension by type definition.
  2. Extension by type specification.

(1) is a special case of (2).
For $\Gamma=\{\}$ it seems like (2) can be obtained from (1) by applying
MP and INST_TYPE (see below).
I cannot see how (2) provides a significantly a more 
abstract way of defining new types. 

What is it I'm missing?

Best Regards,
Einar

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

Assume 
 p:'a -> bool, 
 'b,.q is a term-in-context
 f:'b -> 'a

For (2), we first have to establish

 ?x.p x                                                  (i)
 (?f. Type_Definition p f) ==> q                         (ii)

Making use of (1),(i) we obtain an instance of
 ?f. Type_Definition p f                                 (iii)
and create a new type,  say c.

Then instantiate (ii) with c, using INST_TYPE.           (iv)
Consequently, q[c/'b] can be obtained from (iii), (iv)
by MP.


------------------------------ End of body part 2