Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Mon, 14 Jun 1993 13:06:48 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA08764; Mon, 14 Jun 93 04:54:32 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from ganymede.inmos.co.uk by ted.cs.uidaho.edu (16.6/1.34) id AA08759; Mon, 14 Jun 93 04:54:26 -0700 Received: from frogland.inmos.co.uk by ganymede.inmos.co.uk; Mon, 14 Jun 93 12:54:43 BST From: David Shepherd Message-Id: <8397.9306141154@frogland.inmos.co.uk> Subject: Re: Distinctness ? To: Wai.Wong@cl.cam.ac.uk (Wai Wong) Date: Mon, 14 Jun 1993 12:54:32 +0100 (BST) Cc: shaw@cs.ucdavis.edu, info-hol@ted.cs.uidaho.edu, Wai.Wong@cl.cam.ac.uk In-Reply-To: <"swan.cl.cam.:293910:930614085736"@cl.cam.ac.uk> from "Wai Wong" at Jun 14, 93 09:57:18 am X-Mailer: ELM [version 2.4 PL20] Content-Type: text Content-Length: 1756 Wai Wong has said: > > Rob said: > > > Suppose I make a new finite type: > > > > let thing_Axiom = define_type `Thing` `Thing = TH1 | TH2 `;; > > > > Aren't I guaranteed that, TH1 and TH2 are distinct? That is, isn't it > > always true that the term (TH1 = TH2) is false? If so, is there any > > easy way to get REWRITE_TAC to know this fact for all possible pairs > > of a given enumerated type? With 17 values, I'd hate to have to prove > > 17-chose-2 theorems! > > In the HOL manual description volumn, Section 11.10.5, several functions for > working with user-defined types are described. One function, namely > > prove_constructors_distinct > > does exactly what you want: > > #let thing_Axiom = define_type `Thing` `Thing = TH1 | TH2 `;; > thing_Axiom = |- !e0 e1. ?! fn. (fn TH1 = e0) /\ (fn TH2 = e1) > > #prove_constructors_distinct thing_Axiom;; > |- ~(TH1 = TH2) The issue behind this question is that prove_constructors_distinct is fine when you've only got a few constructors (e.g. 2 here), but if you've got a lot of constructors then it produces a very big theorem (e.g. suppose you define a type for abstract micro-code address which may have 100s of values). What is really needed is a constructors_distinct_CONV which takes a type definition theorem and a equality term between to of teh constructors and proves this to be equal to F (or T in the reflexive case). -------------------------------------------------------------------------- david shepherd: des@inmos.co.uk tel: 0454-616616 x 625 inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq "They didn't like the rates, they don't like the poll tax, and they won't like the council tax." - Nicholas Ridley