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) outside ac.uk; Tue, 30 Mar 1993 21:28:29 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA03783;
          Tue, 30 Mar 93 12:11:58 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA03778;
          Tue, 30 Mar 93 12:11:52 -0800
Received: from LocalHost.cs.ucla.edu 
          by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA12578;
          Tue, 30 Mar 93 12:11:40 -0800
Message-Id: <9303302011.AA12578@maui.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted
Subject: Re: Curried/Un-Curried type constructors
Date: Tue, 30 Mar 93 12:11:38 PST
From: chou@edu.ucla.cs

The following remarks apply to HOL88; I don't know enough HOL90
to know whether they apply to HOL90 as well.

Steve Brackin asked:

> 3. new_recursive_definition definitions that allowed direct reference
>    to the elements of tuples, as in
> 

>      `(myfunction (foo(x,y)) = (2*x + y)) /\
>       (myfunction (bar(x,y,z)) = (3*z))`
> 

>    where foo and bar are both constructors for the concrete-recursive
>    type blah.

There is actually a simple work-around via let-CONV, as the following
HOL session illustrates:

%=============================================================================
#new_theory `blah` ;;
() : void

#let blah_AXIOM = define_type `blah_AXIOM`
#`
#  blah = foo (num # num # num) | gee (num # num) blah
#` ;;
blah_AXIOM = 

|- !f0 f1.
    ?! fn. (!p. fn(foo p) = f0 p) /\ (!p b. fn(gee p b) = f1(fn b)p b)

#let myfun_DEF = new_recursive_definition false blah_AXIOM `myfun_DEF`
#"
#  ( myfun (foo t1) = let (x,y,z) = t1 in (2 * x + y - z) ) /\
#  ( myfun (gee t2 b) = let (x,y) = t2 in (x * y - (myfun b)) )
#" ;;
myfun_DEF = 

|- (!t1. myfun(foo t1) = (let (x,y,z) = t1 in 2 * (x + (y - z)))) /\
   (!t2 b. myfun(gee t2 b) = (let (x,y) = t2 in x * (y - (myfun b))))

#let myfun_DEF' =
#  let (def1, def2) = (CONJ_PAIR myfun_DEF)
#  in
#  let def1' = (GEN_ALL o CONV_RULE (TOP_DEPTH_CONV let_CONV))
#              (SPEC "(x,y,z) : num # num # num" def1)
#  and def2' = (GEN_ALL o CONV_RULE (TOP_DEPTH_CONV let_CONV))
#              (SPEC "(x,y) : num # num" def2)
#  in
#  (CONJ def1' def2') ;;
myfun_DEF' = 

|- (!x y z. myfun(foo(x,y,z)) = 2 * (x + (y - z))) /\
   (!x y b. myfun(gee(x,y)b) = x * (y - (myfun b)))
=============================================================================%

It is not too hard to automate the insertion and removal of
let-expressions so that one can start with

  " ( myfun (foo (x,y,z)) = (2 * x + y - z) ) /\
    ( myfun (gee (x,y) b) = (x * y - (myfun b)) ) "

as the input to (an enhanced version of) new_recursive_definition.

- Ching Tsun