Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4); Fri, 15 Jan 1993 10:11:43 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA01180;
          Fri, 15 Jan 93 01:39:04 -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 AA01175;
          Fri, 15 Jan 93 01:38:55 -0800
Received: from teal.cl.cam.ac.uk (user rjb (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) to cl; Fri, 15 Jan 1993 09:37:03 +0000
To: shb@com.oracorp
Cc: info-hol@edu.uidaho.cs.ted
Subject: Re: new_recursive_definition limitation?
In-Reply-To: Your message of Thu, 14 Jan 93 17:51:04 -0500. <9301142251.AA07795@sparta.oracorp.com>
Date: Fri, 15 Jan 93 09:36:53 +0000
From: Richard Boulton <Richard.Boulton@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.932:15.01.93.09.37.18"@cl.cam.ac.uk>

Steve Brackin writes:
> It came as an unpleasant surprise that given
> 
>   let foo = define_type `foo` `foo = bar0 | bar1 foo foo`;;
> 
> and
> 
>   new_constant(`f`,":num->num");;
> 
> the command
> 
>   new_recursive_definition false foo `test1`
>   "(test1 bar0 = 1) /\
>    (test1 (bar1 f1 f2) = (test1 f1) + (test1 f2))";;
> 
> worked fine, but the command
> 
>   new_recursive_definition false foo `test2`
>   "(test2 f bar0 = 1) /\
>    (test2 f (bar1 f1 f2) = (test2 f f1) + (test2 f f2))";;
> 
> produced
> 
>   evaluation failed     Can't solve recursion equation: Can't derive
> existence theorem

I'm no expert on this, but I think the problem is with f being a constant.
The function being defined by new_recursive_definition can take several
arguments, but in the defining equations all but one of the arguments should be
variables. Thus the following works:

#new_recursive_definition false foo `test2`
#  "(test2 (g:num->num) bar0 = 1) /\
#   (test2 g (bar1 f1 f2) = (test2 g f1) + (test2 g f2))";;
|- (!g. test2 g bar0 = 1) /\
   (!g f1 f2. test2 g(bar1 f1 f2) = (test2 g f1) + (test2 g f2))

Why do you want to have a constant as an argument in the *definition*?

If it's simply a case of wanting to use `f' as the variable even though you've
made it a constant, then hide it while you're making the definition:

#hide_constant `f`;;
() : void

#new_recursive_definition false foo `test3`
#  "(test3 (f:num->num) bar0 = 1) /\
#   (test3 f (bar1 f1 f2) = (test3 f f1) + (test3 f f2))";;
|- (!f. test3 f bar0 = 1) /\
   (!f f1 f2. test3 f(bar1 f1 f2) = (test3 f f1) + (test3 f f2))

#unhide_constant `f`;;
() : void

Richard.