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 Jun 1994 11:10:39 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA29249;
          Fri, 10 Jun 1994 03:48:15 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.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 AA29243;
          Fri, 10 Jun 1994 03:48:08 -0600
Received: from sangam.ncst.ernet.in by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA05909;
          Fri, 10 Jun 1994 02:47:04 -0700
Received: from iitkgp.iitkgp.ernet.in (uucp@localhost) 
          by sangam.ncst.ernet.in (8.6.8.1/8.6.6) with UUCP id PAA23128 
          for info-hol@cs.uidaho.edu; Fri, 10 Jun 1994 15:16:38 +0530
Received: from cse .iitkgp.ernet.in (cse) 
          by iitkgp.ernet.in (4.1/SMI-4.1-MHS-7.0) id AA00981;
          Fri, 10 Jun 94 10:29:13+050
Received: by cse .iitkgp.ernet.in (5.59/ -3.1) id AA01419;
          Fri, 10 Jun 94 10:06:29 EDT
Date: Fri, 10 Jun 94 10:06:29 EDT
From: indra@cse.iitkgp.ernet.in (I. Chakraborty)
Message-Id: <9406101406.AA01419@cse .iitkgp.ernet.in>
To: info-hol@cs.uidaho.edu


      To the fellow-members of the HOL community:
      -------------------------------------------

      Subject: Definition of mutually recursive functions in HOL88
      -------------------------------------------------------------

	Can anyone suggest to me how I can define two
mutually recursive functions in HOL88? For example, suppose
I want to have two functions "evenlist" and "oddlist"
which will hold of two boolean lists having even and odd
number of True elements respectively as shown next:

	evenlist [] = T
	evenlist (CONS h t) = (h => oddlist t | evenlist t)

	oddlist [] = F
	oddlist (CONS h t)  = (h => evenlist t | oddlist t)

	Using the ML function "new_list_rec_definition" does not
allow me to do the above definitions.

		Indrajit Chakrabarti
		(research student)
		Deptt. of Computer Science & Engg.
		IIT Kharagpur
		email : indra@cse.iitkgp.ernet.in