Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Mon, 14 Dec 1992 18:48:56 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA07955; Mon, 14 Dec 92 09:47:28 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from utrhcs.cs.utwente.nl by ted.cs.uidaho.edu (16.6/1.34) id AA07950; Mon, 14 Dec 92 09:47:18 -0800 Received: from apollo.cs.utwente.nl by utrhcs (4.1/RBCS-2.3mx) id AA12431; Mon, 14 Dec 92 17:51:18 +0100 Received: from circus.cs.utwente.nl by apollo.cs.utwente.nl (4.1/RBCS-2.0) id AA05019; Mon, 14 Dec 92 17:51:15 +0100 Date: Mon, 14 Dec 92 17:51:15 +0100 From: blok@nl.utwente.cs (Rintcius Blok) Message-Id: <9212141651.AA05019@apollo.cs.utwente.nl> To: info-hol@edu.uidaho.cs.ted Hello, I have problems with modeling records in HOL. I am trying to model a record as a function from labels (say strings) to a sort of recursive sum type, in such a way that each label acesses another field (by different combinations of INL and INR). What I would like to create is a recursive sum type, that can be instantiated as e.g. (string,(num,EMPTY)recsum)recsum. I tried to use define_type to define this recursive sum type, but I could not succeed in reaching the kind of recursiveness I wanted: at different levels of recsum, different instantiations of *. Or to state this problem inductively: is it possible to define recsum as: 1. EMPTYSUM is of type recsum. 2. x is of type recsum if this type is of the form *+** at toplevel and ** is of type recsum. Is there someone who knows how to define this recursive sum type or knows an alternative way of modeling records in HOL? Any hint is welcome. Thanks, Rintcius.