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);
          Tue, 1 Dec 1992 19:57:55 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA10849;
          Tue, 1 Dec 92 11:39:32 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from nene.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA10843;
          Tue, 1 Dec 92 11:39:21 -0800
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by nene.cl.cam.ac.uk 
          with SMTP (PP-6.3) to cl; Tue, 1 Dec 1992 19:38:19 +0000
To: blok@nl.utwente.cs (Rintcius Blok)
Cc: info-hol@edu.uidaho.cs.ted
Subject: Re: recursive def. problem
In-Reply-To: Your message of Tue, 01 Dec 92 17:37:05 +0100. <9212011637.AA07134@apollo.cs.utwente.nl>
Date: Tue, 01 Dec 92 19:38:11 +0000
From: John Harrison <John.Harrison@uk.ac.cam.cl>
Message-Id: <"nene.cl.ca.734:01.12.92.19.38.21"@cl.cam.ac.uk>


Rintcius Blok asks:

> I have a problem with defining a simple looking function. I just
> want to write a recursive function based on the type (*)ltree,
> that returns the root of a ltree.
> I tried the following definition:
> 
> #new_recursive_definition false ltree_Axiom
> #  `GetTop`
> #  "GetTop (Node (top:*) desc) = top";;

I think the problem arises because |ltree_Axiom|, involving as it
does the MAPping of the function over a list of subtrees, is not
quite of the form expected by |new_recursive_definition|:

  |- !f. ?! fn. !v tl. fn(Node v tl) = f(MAP fn tl)v tl

However it is not too hard to do what you want `by hand':

  #let GetTop =
  #  let th1 = theorem `ltree` `ltree_Axiom` in
  #  let th2 = ISPEC "\(x:(*)list) (y:*) (z:* ltree list). y" th1 in
  #  let th3 = BETA_RULE th2 in
  #  let th4 = EXISTENCE th3 in
  #  new_specification `GetTop` [`constant`,`GetTop`] th4;;
  GetTop = |- !v tl. GetTop(Node v tl) = v
  Run time: 0.3s
  Intermediate theorems generated: 24

John.