Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <05782-0@swan.cl.cam.ac.uk>; Wed, 29 Apr 1992 14:02:42 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA15764; Wed, 29 Apr 92 05:49:27 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from utrhcs.cs.utwente.nl by ted.cs.uidaho.edu (16.6/1.34) id AA15760; Wed, 29 Apr 92 05:49:03 -0700 Received: from perseus.cs.utwente.nl by utrhcs.cs.utwente.nl (4.1/RBCS-2.2mx) id AA03445; Wed, 29 Apr 92 14:49:00 +0200 Received: from utis58.cs.utwente.nl by perseus.cs.utwente.nl (4.1/RBCS-2.0) id AA26628; Wed, 29 Apr 92 14:48:56 +0200 Date: Wed, 29 Apr 92 14:48:56 +0200 From: vdvoort@nl.utwente.cs (Mark van de Voort) Message-Id: <9204291248.AA26628@perseus.cs.utwente.nl> To: info-hol@edu.uidaho.cs.ted Subject: Re: Well-founded induction Regarding Sreeranga Rajan's recent query: > I was wondering if there has been effort in HOL to admit > recursive definitions by Well-founded induction wherein I could > specify a non-decreasing lexicographic relation on the arguments to > the recurive function as a measure of its admittance. I'm currently working on an introduction mechanism for recursive definitions which allow Well-founded induction. The idea is to use this mechanism for a direct introduction of Miranda (TM) style function definitions. I indeed use a measure to introduce these functions. I have available a TeX-report on the introduction mechanism. Another report on the derivation of definition specific induction theorems is due in a month or so. I can mail these on request. > Jeff pointed out to me on how to get around this by using other nice > features of higher-order logic, Can these nice features be explained easily. I would be most interested. Mark.