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; Sat, 8 May 1993 16:28:20 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA01786; Sat, 8 May 93 08:13:26 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA01781; Sat, 8 May 93 08:13:18 -0700 Received: from guillemot.cl.cam.ac.uk (user tfm (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Sat, 8 May 1993 16:12:37 +0100 To: Phil Windley Cc: Victor "A." Carreno , info-hol@ted.cs.uidaho.edu, Tom.Melham@cl.cam.ac.uk Subject: Re: concrete type definition In-Reply-To: Your message of Fri, 07 May 93 11:26:58 -0700. <199305071826.AA16576@panther.cs.uidaho.edu> Date: Sat, 08 May 93 16:12:31 +0100 From: Tom Melham Message-Id: <"swan.cl.cam.:023150:930508151244"@cl.cam.ac.uk> Phil Windley writes: > This only does it one way, however (i.e. ~(A = B) but not ~(B = A)), so you > have to break it apart and map GSYM onto iot and combine it with the others > to get a full set. Actually, GSYM works on conjunctions of equations, so one could just do: #let th1 = define_type `a_new_type` `the_thing = F_ITEM | S_ITEM | T_ITEM`;; th1 = |- !e0 e1 e2. ?! fn. (fn F_ITEM = e0) /\ (fn S_ITEM = e1) /\ (fn T_ITEM = e2) #let dist = prove_constructors_distinct th1;; dist = |- ~(F_ITEM = S_ITEM) /\ ~(F_ITEM = T_ITEM) /\ ~(S_ITEM = T_ITEM) #GSYM dist;; |- ~(S_ITEM = F_ITEM) /\ ~(T_ITEM = F_ITEM) /\ ~(T_ITEM = S_ITEM) 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. Tom