Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2);
          Fri, 9 Oct 1992 22:02:15 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA09343;
          Fri, 9 Oct 92 13:39:26 -0700
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 AA09331;
          Fri, 9 Oct 92 13:36:38 -0700
Received: by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA01293;
          Fri, 9 Oct 92 13:32:10 -0700
Date: Fri, 9 Oct 92 13:32:10 -0700
From: austel@edu.ucla.cs (Vernon Austel)
Message-Id: <9210092032.AA01293@maui.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted
Subject: recursive definitions using transfinite induction


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)


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).

Thanks,
Vernon