Return-Path: <John.Harrison-request@cl.cam.ac.uk>
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 05:17:46 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA08623;
          Sun, 13 Jun 93 21:09:35 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from [128.120.56.188] by ted.cs.uidaho.edu (16.6/1.34) id AA08618;
          Sun, 13 Jun 93 21:09:30 -0700
Received: by toadflax.cs.ucdavis.edu (4.1/UCD.CS.2.3) id AA24775;
          Sun, 13 Jun 93 21:09:51 PDT
Date: Sun, 13 Jun 93 21:09:51 PDT
From: shaw@cs.ucdavis.edu (Rob Shaw)
Message-Id: <9306140409.AA24775@toadflax.cs.ucdavis.edu>
To: info-hol@ted.cs.uidaho.edu
Subject: Distinctness ?



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!

On a more theoretical plane, how does new_constant fit into all of
this? I mean, the type Thing contains exactly two distict values, but
what is to keep me from coming along and using new_constant to declare
three different constants of type :Thing? If I did so, they clearly
can not all be distinct.

Thanx again. 

Rob Shaw