Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Message-Id: <9301091235.AA28014@jevex.cs.titech.ac.jp>
To: info-hol@edu.uidaho.cs.ted
Subject: Re: How to make a destructor of the type tree
Date: Sat, 09 Jan 1993 21:34:59 JST
From: KIKUCHI Yutaka <kikuchi@jp.ac.titech.cs>

Hello, info-hol people.

I said:
> > 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";;

We guessed this way would work well because of the example of list type,
but we were incorrect.

Dr. Tom Melham said:

> However, here's how you might define your destructor function
> by hand:
> 
>   let thm1 = ISPEC "\x:((tree)list)list.\tl:(tree)list.tl" tree_Axiom;;
>   let thm2 = EXISTENCE (BETA_RULE thm1);;
>   let children =
>       new_specification `children` [`constant`,`children`] thm2;;

This is the solusion, which works very well.

Dr. David Shepherd said:
> 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`

Actually, we tried this way at first. As you said we failed on HOL88.
I think it is so convinient if we use the way.

Thank you very much for the reply,
and I am sorry for my late respose because of my new year vacation.

--
KIKUCHI Yutaka,
The Department of Computer Science, Tokyo Institute of Technology
Ookayama, Meguro, Tokyo 152 Japan

E-mail: kikuchi@cs.titech.ac.jp
Tel: +81-3-3728-7663
Fax: +81-3-3728-5021