Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Sat, 19 Dec 1992 15:32:43 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA06076; Sat, 19 Dec 92 05:26:38 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from koudai.cs.titech.ac.jp by ted.cs.uidaho.edu (16.6/1.34) id AA06071; Sat, 19 Dec 92 05:26:31 -0800 Received: by koudai.cs.titech.ac.jp (5.67+1.6W/koudai); Sat, 19 Dec 92 22:25:43 JST Received: by jevex.cs.titech.ac.jp (16.7/css1.5); Sat, 19 Dec 92 22:25:57 +0900 Message-Id: <9212191325.AA23663@jevex.cs.titech.ac.jp> To: info-hol@edu.uidaho.cs.ted Cc: kikuchi@jp.ac.titech.cs Subject: How to make a destoructor of the type tree Date: Sat, 19 Dec 92 22:25:56 JST From: KIKUCHI Yutaka Hello, HOL friends, We are novice at HOL and want to apply HOL for software verification, so we have been making experience on HOL. Now we face a question and cannot solve it. We would so appreciate receiving an answer or suggestions about what we should refer to. We tried to use the theory `tree`, but we could not make a destructor (selector function) as the following... --------------------------------------------------------------- kikuchi@mike[132] hol _ _ __ _ __ __ |___ |__| | | | |__| |__| | | | |__| |__ |__| |__| Version 2.0, built on 1/12/92 #new_theory `foo`;; () : void #new_parent `tree`;; Theory tree loaded () : void #let tree_Axiom = theorem `tree` `tree_Axiom`;; tree_Axiom = |- !f. ?! fn. !tl. fn(node tl) = f(MAP fn tl)tl #new_recursive_definition false tree_Axiom `get_children` # "get_children (node tl) = tl";; Badly typed application of: "get_children" which has type: ":tree -> (tree)list" to the argument term: "tl" which has type: ":(tree)list" evaluation failed Can't solve recursion equation: Can't instantiate existence theorem #quit();; --------------------------------------------------------------- What is wrong with us? Please tell us our mistake. Thank you very much. -- KIKUCHI Yutaka, The Department of Computer Science, Tokyo Institute of Technology Ookayama, Meguro, Tokyo 152 Japan E-mail: kikuchi@cs.titech.ac.jp Tel: +81-3-3728-7663 Fax: +81-3-3728-5021