Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
To: shaw@cs.ucdavis.edu (Rob Shaw)
Cc: info-hol@ted.cs.uidaho.edu, Wai.Wong@cl.cam.ac.uk
Subject: Re: Distinctness ?
In-Reply-To: Your message of "Sun, 13 Jun 93 21:09:51 PDT." <9306140409.AA24775@toadflax.cs.ucdavis.edu>
Date: Mon, 14 Jun 93 09:57:18 +0100
From: Wai Wong <Wai.Wong@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:293910:930614085736"@cl.cam.ac.uk>

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)


> 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.

The function new_constant merely introduces a constant into the current thoery. It
does not give it any value or meaning. You cannot do very much with such
a constant. I would not recommend you create constant in this way .
For ordinary application,  it is much better to use define_type,
new_definition, new_recursive_definition and so on to define new constant.

> Thanx again. 

You are welcome.


Wai