Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Message-Id: <9210090613.AA12803@maui.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted
Cc: chou@edu.ucla.cs
Subject: Tuple arguments in the LHS of a new_recursive_definition
Date: Thu, 08 Oct 92 23:13:28 PDT
From: chou@edu.ucla.cs

Consider the following HOL session:

  #new_list_rec_definition(`TEST_1`,
  #"
  #  ( TEST_1 (x,y) NIL        = x + y ) /\
  #  ( TEST_1 (x,y) (CONS h t) = x + y + h + TEST_1 (x,y) t )
  #") ;;
  evaluation failed     Can't solve recursion equation: Can't derive existence theorem
  
  #new_list_rec_definition(`TEST_2`,
  #"
  #  ( TEST_2 p NIL        = let (x,y) = p in (x + y) ) /\
  #  ( TEST_2 p (CONS h t) = let (x,y) = p in (x + y + h + TEST_2 (x,y) t) )
  #") ;;
  |- (!p. TEST_2 p[] = (let (x,y) = p in x + y)) /\
     (!p h t.
       TEST_2 p(CONS h t) =
       (let (x,y) = p in x + (y + (h + (TEST_2(x,y)t)))))

Clearly, TEST_1 and TEST_2 are the same function.  But the former
definition fails because of the tuple argument (x,y) in the LHS.
The same problem occurs with new_prim_rec_definition and
new_recursive_definition.  (Indeed, they are all defined in terms
of new_recursive_definition.)  But tuple arguments are allowed
in new_definition, as the following shows:

  #new_definition(`TEST_3`,
  #"
  #  TEST_3 (x,y) l = x + y + SUM l
  #") ;;
  |- !x y l. TEST_3(x,y)l = x + (y + (SUM l))

My question is: Is there any logical reason for disallowing tuple
arguments in the LHS of a new_recursive_definition?  If not, has
anyone written a fix?  I guess I can hack something to work in my
particular application, but it would be nice not to have to hack
it myself.  ;-)

Any solution is appreciated!

- Ching Tsun