Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <24152-0@swan.cl.cam.ac.uk>; Tue, 11 Aug 1992 14:53:39 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA26063; Tue, 11 Aug 92 06:43:04 -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 AA26058; Tue, 11 Aug 92 06:42:54 -0700 Received: from cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <23853-0@swan.cl.cam.ac.uk>; Tue, 11 Aug 1992 14:37:29 +0100 To: David Shepherd Cc: Wai.Wong@uk.ac.cam.cl (Wai Wong), info-hol@edu.uidaho.cs.ted (info-hol mailing list) Subject: Re: Conditional rewriting In-Reply-To: Your message of Tue, 11 Aug 92 11:32:08 +0100. <7846.9208111032@frogland.inmos.co.uk> Date: Tue, 11 Aug 92 14:36:42 +0100 From: Wai Wong Message-Id: <"swan.cl.ca.865:11.07.92.13.38.01"@cl.cam.ac.uk> Thanks David, but the tactic you suggested does only half of what I want, ie. the u in the input theorem has to be EXACTLY match the goal or a subterm of the goal. Maybe I should have written my spec. more accurately--- the input theorem should be: !x. P[x] ==> (u[x] = v[x]) and the x should be instatiated to match (subterm of) the goal. Inspired by your suggestion, I come up with the following : let COND_REWRITE_TAC th (asl,gl) = let mconv = `MCONV` in let mcon = \tm. (PART_MATCH (lhs o snd o dest_imp) th tm) ? failwith mconv in letrec MATCH_CONV tm = [mcon tm] ??[mconv] (if is_comb tm then (let rator,rand = dest_comb tm in flat (map MATCH_CONV [rator; rand])) if is_abs tm then (let bv,body = dest_abs tm in let thms = MATCH_CONV body in filter (\th. not(mem bv (thm_frees th))) thms) else []) in (let thms = MATCH_CONV gl in let th = LIST_CONJ (map UNDISCH_ALL thms) in SUBGOAL_THEN (list_mk_conj (hyp th)) STRIP_ASSUME_TAC THENL[ REPEAT CONJ_TAC THEN TRY (FIRST_ASSUM ACCEPT_TAC); SUBST_TAC(CONJUNCTS th)]) (asl,gl) ? failwith `COND_REWRITE_TAC`;; where SUBGOAL_THEN is similar to SUPPOSE_TAC but it is in the system so no library is needed. Below are a few examples: HOL88> SUC_PRE;; SUC_PRE = |- !n. 0 < n ==> (SUC(PRE n) = n) HOL88> let tm = "(\e.SUC(PRE e))x = SUC(PRE (a + b))";; tm = "(\e. SUC(PRE e))x = SUC(PRE(a + b))" : term Run time: 0.1s HOL88> g tm;; "(\e. SUC(PRE e))x = SUC(PRE(a + b))" () : void Run time: 0.0s HOL88> e(COND_REWRITE_TAC SUC_PRE);; OK.. 2 subgoals "(\e. SUC(PRE e))x = a + b" [ "0 < (a + b)" ] "0 < (a + b)" () : void Run time: 0.4s Intermediate theorems generated: 21 HOL88> let tm2 = "(\e. SUC(PRE e) = x)y";; tm2 = "(\e. SUC(PRE e) = x)y" : term Run time: 0.1s HOL88> g tm2;; "(\e. SUC(PRE e) = x)y" () : void Run time: 0.1s HOL88> e(COND_REWRITE_TAC SUC_PRE);; OK.. evaluation failed COND_REWRITE_TAC HOL88> let tm3 = "(\e. SUC(PRE x) = e)y";; tm2 = "(\e. SUC(PRE x) = e)y" : term Run time: 0.0s HOL88> g tm3;; "(\e. SUC(PRE x) = e)y" () : void Run time: 0.0s HOL88> e(COND_REWRITE_TAC SUC_PRE);; OK.. 2 subgoals "(\e. x = e)y" [ "0 < x" ] "0 < x" () : void Run time: 0.4s Intermediate theorems generated: 20 HOL88> let tm4 = "SUC(PRE(SUC x)) = SUC(PRE(a + b))";; tm4 = "SUC(PRE(SUC x)) = SUC(PRE(a + b))" : term Run time: 0.0s HOL88> g tm4;; "SUC(PRE(SUC x)) = SUC(PRE(a + b))" () : void Run time: 0.0s HOL88> e(COND_REWRITE_TAC SUC_PRE);; OK.. 3 subgoals "SUC x = a + b" [ "0 < (SUC x)" ] [ "0 < (a + b)" ] "0 < (a + b)" "0 < (SUC x)" () : void Run time: 0.4s Intermediate theorems generated: 30 Wai