Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Message-Id: <199305101615.AA19873@panther.cs.uidaho.edu>
To: info-hol@ted.cs.uidaho.edu
Subject: Re: concrete type definition
In-Reply-To: Your message of Sat, 08 May 93 16:12:31 +0100. <"swan.cl.cam.:023150:930508151244"@cl.cam.ac.uk>
Date: Mon, 10 May 93 09:15:12 -0700
From: Phil Windley <windley@panther.cs.uidaho.edu>


On Sat, 08 May 93 16:12:31 BST, Tom.Melham@cl.cam.ac.uk wrote:
+------------
| Actually, GSYM works on conjunctions of equations, so one
| could just do:

Ah, that's good to know.  I used to use sometyhing called SYM_RULE that I
got from Graham Birtwhistle.  Since GSYM came along I've just used it as a
direct substitute without worrying about the difference.

| The function prove_constructors_distinct was designed to prove only one 
| "direction" of the inequalities because it's so trivial to get the
| other direction.

I don't mind this kind of behavior for primitives, but I do believe that
this is the kind of thing that makes HOL difficult to use.  Sure its
trivial to write:

    let dist = prove_constructors_distinct th1;;

    let both_ways = CONJ dist (GSYM dist);;

But, its one more step that I have to do EVERY TIME I want to use this.  If
the users going to have to do it everytime or almost every time, why not
just do it in the first place no matter how trivial it is?  

This is just one more place to needlessly bump up against the theorem
prover.  As a community, we need to be more mindful of putting things
together in ways that won't cause needless frustration.  

--phil--