Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <04193-0@swan.cl.cam.ac.uk>; Wed, 17 Jun 1992 16:57:29 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA02733; Wed, 17 Jun 92 06:40:22 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA02728; Wed, 17 Jun 92 06:39:53 -0700 Received: from guillemot.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <01483-0@swan.cl.cam.ac.uk>; Wed, 17 Jun 1992 14:40:18 +0100 To: John Harrison Cc: wishnu@nl.ruu.cs, info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl Subject: Re: inputs to new_recursive_definition In-Reply-To: Your message of Tue, 16 Jun 92 14:30:54 +0100. <"swan.cl.ca.474:16.05.92.13.31.18"@cl.cam.ac.uk> Date: Wed, 17 Jun 92 14:40:02 +0100 From: Tom Melham Message-Id: <"swan.cl.ca.491:17.05.92.13.40.26"@cl.cam.ac.uk> Regarding John Harrison's remark: > ... You don't need to have used `define_type' in order to define functions > over the type with `new_recursive_definition'... This is true. But I'd like to add that the recursion theorem you provide as input to new_recursive_definition must have the same form as the theorems that are proved by define_type. Note that ltree_Axiom does _not_ have this form. > For instance here is a definition of addition over the naturals: > > #new_recursive_definition true num_Axiom `add` > # "($add 0 n = n) /\ ($add (SUC m) n = SUC($add m n))";; > |- (!n. 0 add n = n) /\ (!m n. (SUC m) add n = SUC(m add n)) > > The theorem `num_Axiom' is the recursion principle... This works because it has been prearranged for num_Axiom, which is proved by hand, to have the form that _would_ result _if_ :num were defined using define_type. Tom