Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Date: Thu, 6 Aug 92 12:20:18 -0700
From: toal@edu.ucla.cs (Ray J. Toal)
Message-Id: <9208061920.AA29299@ewa.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted
Subject: need more pattern support?
Cc: toal@edu.ucla.cs


Hi,

I was wondering if the ML function new_inductive_definition (from the
ind_defs library) *requires* currying, or if I've made a silly mistake
in the following:

  #let ZZZ = "Z:num#num->bool";;
  ZZZ = "Z" : term

  #new_inductive_definition false `ZZZ` ("^ZZZ(x,y)", []);;
  - : (goal list -> (thm list # thm))

  #let z = it;;
  z = - : (goal list -> (thm list # thm))

  #z [ [], "^ZZZ(8,3)" ];;
  evaluation failed     non-variable in pattern

Of course the following works:

  #let QQQ = "Q:num->num->bool";;
  QQQ = "Q" : term

  #new_inductive_definition false `QQQ` ("^QQQ x y", []);;
  - : (goal list -> (thm list # thm))

  #let q = it;;
  q = - : (goal list -> (thm list # thm))
 
  #q [ [], "^QQQ 8 3" ];;
  ([|- Q 8 3], |- !P'. P' 8 3 ==> (!x y. Q x y ==> P' x y))
  : (thm list # thm)

I know, for example, that you cannot use new_recursive_definition with 
"multiple patterns" on the left hand side of equations and that constructors
in define_type must be curried ....

Is anyone working on making HOL a little more flexible in these areas?
I remember hearing that someone was working on tupled quantification;
another useful contribution would allow HOL "functions" to look more like
functions in Standard ML.  Too great of a task?

Ray Toal