Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Tue, 3 Nov 1992 14:34:12 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA00768; Tue, 3 Nov 92 06:19:08 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA00763; Tue, 3 Nov 92 06:18:58 -0800 Received: from guillemot.cl.cam.ac.uk (user tfm) by swan.cl.cam.ac.uk with SMTP (PP-6.2) to cl; Tue, 3 Nov 1992 14:07:30 +0000 To: info-hol@edu.uidaho.cs.ted Cc: Tom.Melham@uk.ac.cam.cl Subject: Re: mutually recursive types in HOL Date: Tue, 03 Nov 92 14:07:10 +0000 From: Tom Melham Message-Id: <"swan.cl.ca.595:03.10.92.14.08.33"@cl.cam.ac.uk> Vernon Austel writes: > Section 10.5.5 of the HOL DESCRIPTION describes ``type specification''. > This apparently generalizes type definition in way analogous > to how new_specification generalizes constant definition. > > Has this been implemented? If not, does anyone plan to? > Would someone please spell out in black and white what new > kinds of types this facility would allow us to define? The "type specification" rule in chapter 10 of DESCRIPTION does indeed generalize type definitions in the same way as constant specifications generalize constant definitions. The rule is G1 |- ?x. P x G2 |- (* ~=~ P) ==> Q ----------------------------------------------- G1 u G2 |- Q[ty/*] where "(* ~=~ P)" means there is a bijection between the values of type * and the set of values that satisfy P. This principle of definition is intended to allow new types to be introduced by loose specifications of their properties. The idea is that one finds a non-empty subset P of an existing type ty1 to represent the values of desired type. One then proves that if the type * (a type variable) is in bijection with this set, then the desired property Q holds of *. If this can be proved, then it is consistent to extend the logic with a new type expression ty for which Q[ty/*] holds. Note that the information implicit in the equation "* ~=~ P" is, as it were, lost after making the definition. All you know is that |- Q[ty/*]. You do not know that |- ty ~=~ P, as you would if you just made a normal type definition. This rule has *not* yet been implemented. For some further details, see my paper in the proceedings of this year's HOL user meeting. [I can make the postcript available if people are interested]. Tom