Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2);
          Sat, 19 Dec 1992 19:15:54 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA06168;
          Sat, 19 Dec 92 09:07:53 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA06163;
          Sat, 19 Dec 92 09:07:46 -0800
Received: from guillemot.cl.cam.ac.uk (user tfm) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.2) to cl; Sat, 19 Dec 1992 17:05:36 +0000
To: KIKUCHI Yutaka <kikuchi@jp.ac.titech.cs>
Cc: info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl
Subject: Re: How to make a destoructor of the type tree
In-Reply-To: Your message of Sat, 19 Dec 92 22:25:56 +0200. <9212191325.AA23663@jevex.cs.titech.ac.jp>
Date: Sat, 19 Dec 92 17:05:25 +0000
From: Tom Melham <Tom.Melham@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.096:19.11.92.17.05.39"@cl.cam.ac.uk>


Regarding:

> We tried to use the theory `tree`,
> but we could not make a destructor (selector function)
> as the following...

the characterizing theorem for type tree is

   tree_Axiom = |- !f. ?! fn. !tl. fn(node tl) = f(MAP fn tl)tl 

But this, unfortunately, is _not_ in the correct form for use
with new_recursive_definition, which works only for theorems
of the form returned by define_type. [See the info-hol archive
or the HOL manual for more information].

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;;

Best wishes,
Tom