Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: David Shepherd <des@uk.co.inmos>
Message-Id: <1940.9212210938@frogland.inmos.co.uk>
Subject: Re: How to make a destoructor of the type tree
To: kikuchi@jp.ac.titech.cs (KIKUCHI Yutaka)
Date: Mon, 21 Dec 1992 09:38:25 +0000 (GMT)
Cc: info-hol@edu.uidaho.cs.ted, kikuchi@jp.ac.titech.cs
In-Reply-To: <9212191325.AA23663@jevex.cs.titech.ac.jp> from "KIKUCHI Yutaka" at Dec 19, 92 10:25:56 pm
Content-Type: text
Content-Length: 1642

KIKUCHI Yutaka has said:
> 
> Hello, HOL friends,
> 
> We are novice at HOL and want to apply HOL for software verification,
> so we have been making experience on HOL.
> Now we face a question and cannot solve it.
> We would so appreciate receiving an answer
> or suggestions about what we should refer to.
> 
> We tried to use the theory `tree`,
> but we could not make a destructor (selector function)
> as the following...

> #let tree_Axiom = theorem `tree` `tree_Axiom`;;
> tree_Axiom = |- !f. ?! fn. !tl. fn(node tl) = f(MAP fn tl)tl
> 
> #new_recursive_definition false tree_Axiom `get_children`
> #                "get_children (node tl) = tl";;

the reason is that new_recursive_definition is only designed to work
with types produced by the recursive type definition mechanism. the
type ":tree" is not defined that way ... in fact it is one of the types
that is used by the recursive type definition mechanism to hold the
representation type of the new type. 

you may want to define a new type:

define_type `Tree` `Tree = Leaf * | Node Tree Tree`;;

to give binary trees. if you want a type like

`Tree = Leaf * | Node (Tree)list`

then i'm afraid that currently the type definition package can't help
you ... though from the procedings of the last HOL workshop something
to support these types may be being developed in hol90.

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
                1992: celebrate the quincentenary of columbus getting lost