Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Date: Tue, 9 Jun 92 13:24:02 EST
From: symdchon@au.edu.anu.mehta (donald syme )
Message-Id: <9206090324.AA03336@mehta>
To: info-hol@edu.uidaho.cs.ted
Subject: HOL: Struggling with mutually recursive types


To all who might be able to help:

I am a fairly new HOL user, and am presently working on entering the formal definition of ML into HOL.  Most of the work has already been done, but some of the problems with mutually recursive types were never solved by the guy whose work I'm taking over. 

SO... after combing the HOL info lists I downloaded the AAP mutually recursive type package and the "PH" package also.  I also have the example by Tom Melham on how to hack up a type definition for a particular case.  Having read the discussions back in April, I was wondering what the best course of action is for a type struture as complex as used in ML.  Do I:
	a) use axioms to define the required type properties and try to prove the necessary induction results from these. (and I presume develop my own tactics to make use of these induction results)
	b) try to modify the AAP package to do the type definition correctly.
	c) try to hack up my own implementation of the type structure following Tom Melham's lead.  (This looks hard for 15+ types)

If anyone has anymore examples of any of the above, I would love to see them.  I am finding it difficult the exact forms that the induction theorems should take, and even how to prove the induction therorems from the type definition theorem.


Many thanks,

Donald Syme