Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
To: toal@edu.ucla.cs (Ray J. Toal)
Cc: info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl
Subject: Re: need more pattern support?
In-Reply-To: Your message of Thu, 06 Aug 92 12:20:18 -0700. <9208061920.AA29299@ewa.cs.ucla.edu>
Date: Fri, 07 Aug 92 09:46:07 +0100
From: Tom.Melham@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.069:07.07.92.08.46.15"@cl.cam.ac.uk>

RE: curried vs paired relations in the ind_defs library.
--------------------------------------------------------

Ray Toal asks:

> I was wondering if the ML function new_inductive_definition (from the
> ind_defs library) *requires* currying, ...

The short answer is "more-or-less".  In particular, the pattern
supplied to new_inductive_definition may not contain concrete pairs.
So, for example, the following is illegal:

   let R = "R:num#num -> bool";;

   new_inductive_definition false `R` ("^R (x,y)", []) ... ;;

On the other hand:

   new_inductive_definition false `R` ("^R (p:num#num)", []) ... ;;

*is* legal.  For example:

   new_inductive_definition false `R` ("^R p", []) [[], "^R (8,3)"] ;;

returns

  [|- R(8,3)], 
  |- !P. P(8,3) ==> (!p. R p ==> P p) : (thm list # thm)   

Note the form of the induction theorem.

There's no reason in principle why more flexibility with respect to
paired/tupled relations could not be built into ind_defs.  The main
difficulty is that the programming gets rather messy [I did not have
the time for it].  Consider, for example, what you would do with

   new_inductive_definition false `R` ("R (x,y,z)", ["y"]) ... ;;

Exercise: what would the induction theorem look like?  How would
you transform it into an induction tactic?

Tom