Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
To: David Shepherd <des@inmos.co.uk>
Cc: Wai.Wong@cl.cam.ac.uk (Wai Wong), shaw@cs.ucdavis.edu, 
    info-hol@ted.cs.uidaho.edu, Tom.Melham@cl.cam.ac.uk
Subject: Re: Distinctness ?
In-Reply-To: Your message of "Mon, 14 Jun 93 12:54:32 BST." <8397.9306141154@frogland.inmos.co.uk>
Date: Mon, 14 Jun 93 14:08:47 +0100
From: Tom Melham <Tom.Melham@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:041500:930614130857"@cl.cam.ac.uk>


David Shepherd points out:

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

Another possibility is to introduce a type with some structure. For example,
if you want a type with 16 elements, then

   let ty16 = FOO bool bool bool bool 

will do it.  Given that the function FOO is one-to-one, it is
pretty fast to prove inequality, say

  |- ~(FOO T T F T = FOO T T F F)
  
The only problem is the structure of such a "structured" type may 
not map nicely onto some natural structure in the problem domain.

Tom