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: <1818.9301121430@frogland.inmos.co.uk>
Subject: Re: APPLY function on HOL
To: kikuchi@jp.ac.titech.cs (KIKUCHI Yutaka)
Date: Tue, 12 Jan 1993 14:30:49 +0000 (GMT)
Cc: info-hol@edu.uidaho.cs.ted, kikuchi@jp.ac.titech.cs
In-Reply-To: <9301121357.AA05118@jevex.cs.titech.ac.jp> from "KIKUCHI Yutaka" at Jan 12, 93 10:57:54 pm
Content-Type: text
Content-Length: 1429

KIKUCHI Yutaka has said:
> I want to define a function that takes two arguments,
> the first one is an arbitrary type function,
> the second one is an argument for the first.
> For example, we can use APPLY function in LISP for the perpose.
> (apply #'+ '(1 2 3)) => 6
> 
> In HOL, I guessed that the following would be okay,
> but It was a wrong guess.
> 
> new_recursive_definition false list_Axiom `APPLY`
>        "(APPLY f [] = f) /\
>         (APPLY f (CONS h tl) = APPLY (f h) tl)";;
> 
> How can I define such a function?

first define an accumulate function (similar to ML's itlist)

new_recursive_definition false list_Axiom `ACCUM`
  "(ACCUM (f:*->**->**) a [] = a) /\
   (ACCUM f a (CONS x xs) = ACCUM f (f a x) xs)";;

then "ACCUM f a xs" is (assuming f is infix) "a f xs_0 f xs_1 f ... f xs_n"

now you can define APPLY by

new_recursive_definition false list_Axiom `APPLY`
  "(APPLY f (CONS (x:*) xs) = ACCUM f x xs)";;

note that "(APPLY f [])" is left unspecified.

now

	"APPLY $+ [1;2;3]"
      = "ACCUM $+ 1 [2;3]"
      = "ACCUM $+ (1+2) [3]"
      = "ACCUM $+ ((1+2)+3) []"
      = "((1+2)+3)"
      = "6"

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
                New Year Resolution for 1993: Start using capital letters.