Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Sat, 17 Apr 1993 13:51:21 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA08619; Sat, 17 Apr 93 05:43:17 -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 AA08614; Sat, 17 Apr 93 05:43:12 -0700 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Sat, 17 Apr 1993 13:42:58 +0100 To: val@com.netcom (Dewey Val Schorre) Cc: info-hol@edu.uidaho.cs.ted Subject: Re: Worried about mk_tac and the philosophy of ML In-Reply-To: Your message of Fri, 16 Apr 93 18:41:27 -0700. <9304170141.AA24517@netcom2.netcom.com> Date: Sat, 17 Apr 93 13:42:52 +0100 From: John Harrison Message-Id: <"swan.cl.ca.486:17.04.93.12.43.03"@cl.cam.ac.uk> It's true that |mk_thm| could lead to non-theorems looking like theorems, but then so could diving into LISP and hacking round, or editing theory files, or running HOL with some kind of filter between the user and the machine... A system can never be 100% secure; HOL at least makes it easy to be honest if that's your intention. Certainly another user could easily check you HOL proof to see that it doesn't cheat, using a few well-chosen greps, as Tom mentioned. Incidentally, I believe HOL's ancestor LCF had a similar function to |mk_thm|, but it would put falsity in the assumptions of the resulting theorem, hence preserving consistency. Of course it's easy to derive such a rule in HOL. I find |mk_thm| useful for: * Assuming separate lemmas while concentrating on a main theorem. Of course one could use |SUBGOAL_THEN| but it's nice to split proofs up into manageable bits. (Here speaks the man whose wellorder library contains a revolting 250- line proof of the Bourbaki fixpoint theorem...) Furthermore, |SUBGOAL_THEN| is problematic with theorems containing polymorphic types because the theorem is temporarily |ASSUME|d, e.g. #g "1 = 1";; "1 = 1" () : void Run time: 0.0s #e(SUBGOAL_THEN "!x:*. x = x" MATCH_ACCEPT_TAC);; OK.. evaluation failed MATCH_ACCEPT_TAC -- INST_TYPE: type variable free in assumptions There are the dangers you mentioned, firstly postulating lemmas which turn out to be false; secondly that you forget to prove them properly. However I haven't done either of these too often... * Redefining constants: HOL won't let you do this, and it's often tedious to have to rerun a complete session. However assuming your new constant has the same type as the old one, you can just use |mk_thm| to assert the new definition, and then in future sessions use the edited definition properly. If it has a different type, you'd have to use interface maps or something -- I've done that on occasion. * Testing which parts of derived inference rules are slow because they are doing theorem-proving. For example, replacing |AC_CONV| by |mk_thm| can often make a big difference, and this makes me think that maybe I should write a more efficient |AC_CONV|. John.