Return-Path: Return-Path: Received: from nsf.ac.uk by swan.cl.cam.ac.uk via JANET with NIFTP to fgate (PP) id <5587-0@swan.cl.cam.ac.uk>; Sat, 20 Apr 1991 15:40:00 +0100 Received: from ted.cs.uidaho.edu.101.129.IN-ADDR.arpa by sun2.nsfnet-relay.ac.uk with SMTP inbound id <16750-0@sun2.nsfnet-relay.ac.uk>; Fri, 19 Apr 1991 20:02:56 +0100 Received: from panther.cs.uidaho.edu by ted.cs.uidaho.edu (15.11/1.34) id AA02389; Fri, 19 Apr 91 11:14:47 pdt Received: by panther.cs.uidaho.edu (5.57/Ultrix3.0-C) id AA00395; Fri, 19 Apr 91 11:16:44 -0700 Message-Id: <9104191816.AA00395@panther.cs.uidaho.edu> To: info-hol@edu.uidaho.cs.ted Subject: lattices Date: Fri, 19 Apr 91 11:16:43 PDT From: Phil Windley Has anyone done a theory of lattices in HOL? A brief look at the library and the contrib directory didn't show any such work in the distribution. The lattice I'm interested in representing in HOL is fairly large (22 members) but the lattice is fairly sparse (34 relationships). Representation isn't a problem since I can simply use a list of pairs, but defining join and then using the relation in a proof could prove to be messy. I'd appreciate any pointers. If no one has done one I'll probably develop a theory. --phil--