Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Fri, 10 Dec 1993 11:35:23 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA03468;
          Fri, 10 Dec 1993 04:27:19 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA03464;
          Fri, 10 Dec 1993 04:27:18 -0700
Received: from imec.be by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) 
          id AA08326; Fri, 10 Dec 1993 03:23:51 -0800
Received: from imec.imec.be (imec) by imec.be (5.65c/IDA-1.4.4-IMEC) 
          id AA17409d; Fri, 10 Dec 1993 12:23:46 +0100
Date: Fri, 10 Dec 93 12:22:29 +0100
From: Catia Angelo <catia@imec.be>
Message-Id: <9312101122.AA00691@imec.imec.be>
Original-Received: by imec.imec.be Fri, 10 Dec 93 
                   12:22:29 +0100
PP-warning: Illegal Received field on preceding line
To: info-hol@cs.uidaho.edu
Subject: Re: Conversion for simplifying conjunction


Hi,

>> Does anyone out there has a conversion (preferably in HOL90)
>> that can take a conjunction and remove duplicate conjuncts?

The following conversion works in HOL88.2.0.

Catia Angelo
catia@imec.be

%------------------------------------------------------------------%
% REDUND_CONV takes a term that should be a conjunction and        %
% elimates the duplicate conjuncts.                                %
%------------------------------------------------------------------%
% #REDUND_CONV term;;                                              %
% |- (ch2 = ch1) /\                                                %
%    (out1 = ch1) /\                                               %
%    (ch1 = ch2) /\                                                %
%    (out2 = ch1) /\                                               %
%    (ch1 = ch2) =                                                 %
%    (ch2 = ch1) /\ (out1 = ch1) /\ (ch1 = ch2) /\ (out2 = ch1)    %
%------------------------------------------------------------------%

letrec clean list =
(if (list = []) then []
    else (hd list).(filter (\el. not (el = (hd list)))
                           (clean (tl list))));;

let REDUND_CONV term =
let list = conjuncts term in
let clean_list = clean list in
CONJUNCTS_CONV (term,(list_mk_conj clean_list));;