Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Date: Tue, 13 Oct 92 17:25:40 +0100
From: vdvoort@nl.utwente.cs (Mark van de Voort)
Message-Id: <9210131625.AA04906@perseus.cs.utwente.nl>
To: info-hol@edu.uidaho.cs.ted
Subject: Re: recursive definitions using transfinite induction
In-Reply-To: Mail from 'Tom Melham <Tom.Melham@cl.cam.ac.uk>' dated: Sun, 11 Oct 92 14:07:39 +0100

Message 164:
>From info-hol-request@ted.cs.uidaho.edu Sun Oct 11 14:21:43 1992
Return-Path: <info-hol-request@ted.cs.uidaho.edu>
Received: from utrhcs.cs.utwente.nl by perseus.cs.utwente.nl (4.1/RBCS-2.0)
	id AA02264; Sun, 11 Oct 92 14:21:41 +0100
Errors-To: info-hol-request@ted.cs.uidaho.edu
Received: from ted.cs.uidaho.edu by utrhcs.cs.utwente.nl (4.1/RBCS-2.3mx)
	id AA27834; Sun, 11 Oct 92 14:21:33 +0100
Errors-To: info-hol-request@ted.cs.uidaho.edu
Received: by ted.cs.uidaho.edu (16.6/1.34)
	id AA11559; Sun, 11 Oct 92 06:09:22 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34)
	id AA11554; Sun, 11 Oct 92 06:09:12 -0700
Received: from scaup.cl.cam.ac.uk (user tfm) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.2) to cl; Sun, 11 Oct 1992 14:07:50 +0100
To: austel@cs.ucla.edu (Vernon Austel)
Cc: info-hol@ted.cs.uidaho.edu, Tom.Melham@cl.cam.ac.uk
Subject: Re: recursive definitions using transfinite induction
In-Reply-To: Your message of Fri, 09 Oct 92 13:32:10 -0700. <9210092032.AA01293@maui.cs.ucla.edu>
Date: Sun, 11 Oct 92 14:07:39 +0100
From: Tom Melham <Tom.Melham@cl.cam.ac.uk>
Message-Id: <"swan.cl.ca.483:11.09.92.13.08.03"@cl.cam.ac.uk>
Status: R

Tom Melham writes
#> 
#> austel@edu.ucla.cs (Vernon Austel) writes:
#> > As I understand it, the recursive definition facility in HOL is based on
#> > this axiom of induction:
#> > 
#> >     INDUCTION |- !P. (P 0 /\ (!n. P n ==> P(SUC n))) ==> !n. P n
#> > 
#> > giving this recursion axiom on natural numbers:
#> > 
#> >     num_Axiom |- !e. !f. ?! fn. ((fn 0) = e) /\ (!n. fn(SUC n) = f (fn n) n)
#> 
#> Actually, the recursive definition facility is based on num_Axiom. See
#> section 11.9.5 (new edition) or 11.7.4 (old edition) of DESCRIPTION.  The
#> INDUCTION theorem follows from the uniqueness part of num_Axiom.
#> 
#> > What if I want to write a predicate like this, though?
#> > 
#> > 	f 0 x = ...
#> > 	f n x = ?n' n'' x' x''. 
#> > 		(n = n' + n'') /\ 
#> > 		x = NODE x' x'' /\
#> > 		f n' x' /\
#> > 		f n'' x''
#> > 
#> > It seems to me that this definition could be based on the more
#> > general axiom of induction found in the more_arithmetic library:
#> > 
#> >   GEN_INDUCTION |- !P. P 0 /\ (!n. (!m. m < n ==> P m) ==> P n) ==> (!n. P n)
#> > 
#> > Has anyone actually done this?
#> > If not, any pointers on how to do this (or simulate it)?
#> > (I have an idea involving lists of functions, but it looks a bit messy).
#> 
#> There are various implementations being developed for more general recursive
#> definitions than are presently built into HOL.  See Wim Ploegaerts' paper
#> in the proceedings of the 1991 HOL User's meeting and Mark van der Voort's
#> paper in the 1992 participant's proceedings.
#> 
#> Tom

Vernon, you might want to look at these papers, 
but if you are interested in a quick
solution they will not provide you with an answer.
Both papers presuppose a destructor style of definitions. 
Furthermore my own implementation has trouble with the existential 
quantification in your definition, 
and as far as I can tell so has the package of Wim Ploegaerts. 

I am interested though in this problem. To me it seems that an 
equivalent formulation might be in terms of relations between your
tree 'x' and the natural number 'n'. If this is the case I think
you might want to take a look at Tom Melham's inductive relation
definition package, as this poses less restrictions on the form
of the relation introduced.

I do however agree that the definition as you give it specifies a
function whose existence can be shown. At the moment I do not see how
this can be mechanised.

Mark