Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) 
          id <27213-0@swan.cl.cam.ac.uk>; Thu, 11 Jun 1992 11:37:10 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA05929;
          Thu, 11 Jun 92 01:29:05 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA05924;
          Thu, 11 Jun 92 01:28:59 -0700
Received: from cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl 
          id <24198-0@swan.cl.cam.ac.uk>; Thu, 11 Jun 1992 09:28:46 +0100
To: chou@edu.ucla.cs
Cc: info-hol@edu.uidaho.cs.ted, Wai.Wong@uk.ac.cam.cl
Subject: Re: UNDIRECTED graph theory in HOL?
In-Reply-To: Your message of Wed, 10 Jun 92 13:48:52 -0700. <9206102048.AA05549@maui.cs.ucla.edu>
Date: Thu, 11 Jun 92 09:28:13 +0100
From: Wai.Wong@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.226:11.05.92.08.29.03"@cl.cam.ac.uk>

Hi, Ching Tsun,

My graph theory can also represent undirected graph by replacing
each undirected edge with a pair of antiparallel edges provided you
always insert a pair when you building the
graph and always delete the pair. So, for example, you can define 
new insert and delete operations to keep the edges in pairs.

new_definition(`INSERT_UNDIRECT_EDGES`,
 "INSERT_UNDIRECT_EDGES (G:^Graph) v1 v2 x = (VS G),
     ((v1 IS_VERTEX G) /\ (v2 IS_VERTEX G) =>
      ((v1,v2,x) INSERT ((v2,v1,x) INSERT (ES G))) | (ES G))");;

new_definition(`DELETE_UNDIRECTED_EDGES`,
 "DELETE_UNDIRECTED_EDGE (G:^Graph) v1 v2 x = (VS G),
      (((ES G) DELETE (v1,v2,x)) DELETE (v2,v1,x))");;

where x is the label of the undirected edge.

Wai