Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: rait@za.ac.uct.mth.elc (Rait Harnett)
Message-Id: <9303100834.AA04021@elc.mth.uct.ac.za>
Subject: simultaneous inductive defns.
To: info-hol@edu.uidaho.cs.ted
Date: Wed, 10 Mar 93 10:34:38 EET
Cc: elc.mth.uct.ac.za!rait@za.ac.uct.ucthpx (Rait Harnett)

I have the following problem:

I need to define a type which arises from a BNF grammar very similar to
the grammar used to generate arithmetic expressions over the variables
a,b,c :
  E -> T|E+T|E-T 
  T -> F|TxF|T/F
  F -> a|b|c|(E).
(Yes I know that this is an unambiguous grammar, but so is the grammar I
need to embed in some existing type.)

The ML function define_type won't be handle this as I see it. One
way possible way to handle this would be to mechanize a formal
presentation of simultaneous inductive definitions. The presentation
I have in mind considers the closure of a collection of sets under a 
family of constructors. If the closure is freely generated in the
sense that elements of the sets making up the closure get into these
sets in a unique way, a certain type of recursive funtion definition
succeeds. Once one has implementation of such a theory in HOL I imagine
one could use it to define the grammar above as a subset of ({a,b,c}+
{+} + {-} + {x} + {/} + {()})ltree. So what one would essentially be
doing is applying the same techniques used by T. Melham in his paper
"Automating recursive type definitions in higher order logic".

I would be grateful to hear from anybody who has come across the same
problem and of how they managed to solve it.

Thanks,
Rait