Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Sun, 11 Oct 1992 14:17:54 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA11559; Sun, 11 Oct 92 06:09:22 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted 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@edu.ucla.cs (Vernon Austel) Cc: info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl 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 Message-Id: <"swan.cl.ca.483:11.09.92.13.08.03"@cl.cam.ac.uk> 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