Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Sat, 11 Jun 1994 13:33:50 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA09024; Sat, 11 Jun 1994 06:32:40 -0600 Sender: hol2000-request@lal.cs.byu.edu Errors-To: hol2000-request@lal.cs.byu.edu Precedence: bulk Received: from irafs1.ira.uka.de by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA09020; Sat, 11 Jun 1994 06:32:35 -0600 Received: from i80fs2.ira.uka.de (actually i80fs2) by irafs1 with SMTP (PP); Sat, 11 Jun 1994 14:26:55 +0200 Received: from ira.uka.de by i80fs2.ira.uka.de id <20087-0@i80fs2.ira.uka.de>; Sat, 11 Jun 1994 14:33:33 +0200 Date: Sat, 11 Jun 94 14:33:32 EDT From: reetz To: hol2000@leopard.cs.byu.edu Subject: pretty printing versus mk_const Message-Id: <"i80fs2.ira.089:11.05.94.12.33.38"@ira.uka.de> Consider the values of type ==`:num`== and type ==`:string`==, --`5`-- or --`"blabla"`--. As far as I know, these are represented WITHIN the logic as a constant, which itself is contructed by mk_thm. What are the reasons for it? As I see it: a) In fact, --`5 = SUC(SUC(SUC(SUC(SUC 0))))`--, meaning the representation of 5 WITHIN the logic is not very efficient, resulting into large terms. b) --`"blabla" = STRING (ASCII ...) (STRING (ASCII ...) (...))`-- has an efficient representation (==`:ascii list`==, in fact), but it is very hard to read. So, IMHO, we have examples where we can't have efficient representations AND good--readable terms at the same time. In my point of view, both types are candidates for reimplementation, where the representation WITHIN the logic in efficient AND the representation to the user is nice, i.e. extending the pretty-printer. By the way, then mk_thm wouldn't be needed anymore. Example: define type ==`:string`== being isomorph to ==`:ascii list`==, define type representation function --`EXPLODE:string -> ascii list`--, define type abstraction function --`IMPLODE:ascii list -> string`--, and then define the usual functions for constructing string as by functions over lists, thus getting all these nice already proven(!) theorems about lists for strings, too, e.g. define concatenation function --`(IMPLODE l1) SAPPEND (IMPLODE l2) = IMPLODE (APPEND l1 l2)`--. Finally, extend the pretty printer: every time it comes to something like --`IMPLODE x`--, try to prettyprint that to --`"x"`-- as far as possible (it might not be possible, of course, but then, it IS object to proving and important to see the represenation WITHIN the logic) or try to prettyprint --`x SAPPEND y`-- as --`x^y`--. val anonymous_hol_user_disclaimer = --`"if your only tool is a hammer, every problem looks like a nail!"`--; (* Ralf Reetz, reetz@ira.uka.de or reetz@informatik.uni-karlsruhe.de *)