Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <04106-0@swan.cl.cam.ac.uk>; Thu, 19 Mar 1992 02:46:03 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA28372; Wed, 18 Mar 92 18:31:45 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from atc.boeing.com by ted.cs.uidaho.edu (16.6/1.34) id AA28368; Wed, 18 Mar 92 18:31:41 -0800 Original-Received: by atc.boeing.com on Wed, 18 Mar 92 18:30:07 PST PP-warning: Illegal Received field on preceding line Received: from lilith.bcs.eca by espresso.bcs.eca (4.1/SMI-4.1) id AA00968; Wed, 18 Mar 92 18:32:37 PST Date: Wed, 18 Mar 92 18:32:37 PST From: mjhealy@com.boeing.espresso (Michael J. Healy 5-3576) Message-Id: <9203190232.AA00968@espresso.bcs.eca> To: info-hol@edu.uidaho.cs.ted Subject: Problem Does anybody have an answer for the following problem? We're still using HOL 1.11. We have it installed with Lucid, on Sparcstations. We had succeeded in proving an elementary fact about propositional knowledge bases. This example was originally Case 0 in an induction proof of a lemma. We were able to prove the lemma, but when we tried to encapsulate the proof for the theory using prove_thm, we got the message writing to process: no more processes, hol Here's what we have: new_theory `turkey`;; load_library `sets`;; new_type_abbrev(`atom`,": num");; new_type_abbrev(`literal`,": atom # bool");; new_type_abbrev(`pterm`,": literal set");; new_type_abbrev(`dnf`,": pterm set");; new_type_abbrev(`rule`,": pterm # literal");; new_type_abbrev(`pkb`,": (atom set # atom set) # (rule set)");; new_type_abbrev(`state`,": pterm");; let fire_def = new_definition (`fire_def`, "fire (r:rule) (s:state) = (SUBSET (FST r) s)");; let inference_def = new_definition (`inference_def`, "inference (p:literal) (r:rule) (s:state) = ((fire r s) /\ ((SND r) = p))");; let f_infer1_DEF = new_prim_rec_definition (`f_infer1_DEF`, "(f_infer1 (p:literal) (s:state) (k:pkb) 0 = ((?(r:rule). ((IN r (SND k)) /\ (inference p r s))) \/ (p IN s))) /\ (f_infer1 (p:literal) (s:state) (k:pkb) (SUC n) = ((?(r:rule). ((IN r (SND k)) /\ (?(pt2:state). (inference p r pt2) /\ (!(q:literal). (IN q pt2) ==> (f_infer1 q s k n))))) \/ (f_infer1 p s k n))) ");; set_goal ([], " ! (k:pkb) (n:num). (! (r:rule). ((r IN (SND k)) ==> ~(FST r = EMPTY))) ==> (! (l:literal). ~f_infer1 l EMPTY k 0) ");; expand (REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[f_infer1_DEF;DE_MORGAN_THM] THEN GEN_TAC THEN CONJ_TAC THENL [((CONV_TAC NOT_EXISTS_CONV) THEN REWRITE_TAC[DE_MORGAN_THM;(GEN "t1:bool" (GEN "t2:bool" (SYM (SPEC "t2:bool" (SPEC "t1:bool" IMP_DISJ_THM)))))] THEN GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[inference_def;DE_MORGAN_THM] THEN ONCE_REWRITE_TAC[DISJ_SYM] THEN REWRITE_TAC[GEN "t1:bool" (GEN "t2:bool" (SYM (SPEC "t2:bool" (SPEC "t1:bool" IMP_DISJ_THM))))] THEN DISCH_TAC THEN REWRITE_TAC[fire_def] THEN (ASSUM_LIST (\thms. (ASSUME_TAC ( (MP ((SPEC "r:rule") (el 3 thms)) (el 2 thms)))))) THEN (UNDISCH_TAC "~(FST (r:rule) = EMPTY)") THEN (CONV_TAC CONTRAPOS_CONV) THEN REWRITE_TAC[] THEN REWRITE_TAC[SUBSET_UNION_ABSORPTION] THEN ONCE_REWRITE_TAC[UNION_SYM] THEN REWRITE_TAC[UNION]); REWRITE_TAC[IN]]);; The above works, yielding "goal proved". The following, however, yields the message about writing to processes: let infer_nothing_0 = prove_thm(`infer_nothing_0`, " ! (k:pkb) (n:num). (! (r:rule). ((r IN (SND k)) ==> ~(FST r = EMPTY))) ==> (! (l:literal). ~f_infer1 l EMPTY k 0) ", REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[f_infer1_DEF;DE_MORGAN_THM] THEN GEN_TAC THEN CONJ_TAC THENL [((CONV_TAC NOT_EXISTS_CONV) THEN REWRITE_TAC[DE_MORGAN_THM;(GEN "t1:bool" (GEN "t2:bool" (SYM (SPEC "t2:bool" (SPEC "t1:bool" IMP_DISJ_THM)))))] THEN GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[inference_def;DE_MORGAN_THM] THEN ONCE_REWRITE_TAC[DISJ_SYM] THEN REWRITE_TAC[GEN "t1:bool" (GEN "t2:bool" (SYM (SPEC "t2:bool" (SPEC "t1:bool" IMP_DISJ_THM))))] THEN DISCH_TAC THEN REWRITE_TAC[fire_def] THEN (ASSUM_LIST (\thms. (ASSUME_TAC ( (MP ((SPEC "r:rule") (el 3 thms)) (el 2 thms)))))) THEN (UNDISCH_TAC "~(FST (r:rule) = EMPTY)") THEN (CONV_TAC CONTRAPOS_CONV) THEN REWRITE_TAC[] THEN REWRITE_TAC[SUBSET_UNION_ABSORPTION] THEN ONCE_REWRITE_TAC[UNION_SYM] THEN REWRITE_TAC[UNION]); REWRITE_TAC[IN]]);;