Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 29 Jun 1993 11:06:49 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA16067; Tue, 29 Jun 93 02:52:25 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from iraun1.ira.uka.de by ted.cs.uidaho.edu (16.6/1.34) id AA16062; Tue, 29 Jun 93 02:52:09 -0700 Message-Id: <9306290952.AA16062@ted.cs.uidaho.edu> Received: from ira.uka.de by iraun1.ira.uka.de with SMTP (PP) id <23853-0@iraun1.ira.uka.de>; Tue, 29 Jun 1993 11:30:56 +0200 Date: Tue, 29 Jun 93 11:32:32 MET DST From: schneide To: info-hol@ted.cs.uidaho.edu Subject: "not quite SPEC_TAC" Rob Shaw writes: |> This one should be pretty simple. Suppose that I have a goal which contains |> many similar subterms, say "f(g(x))". I want to replace all the "f(g(x))" |> with "y" (some completely free name), and also gain the assumption that |> [" y = f(g(x)) "]. SPEC_TAC does the substitution, but doesn't give me the |> assumption. How do I get both? One solution might be the following: 1. Prove the lemma [] |- ?y.f(g(x)) = y This is very simple: Just use this conversion (HOL90) fun LEMMA_CONV y t = let val g = mk_exists{Bvar=y,Body=mk_eq{lhs=t, rhs=y}} in TAC_PROOF(([],g), (EXISTS_TAC t THEN REWRITE_TAC[])) end;EXISTS_TAC (--`f(g(x))`--) THEN REWRITE_TAC[]; 2. You can now put this theorem in the assumption list of your goal (ASSUME_TAC) 3. Now you can remove the existential quantification (UNDISCH_HD_TAC THEN STRIP_TAC) 4. A simple ASM_REWRITE_TAC does the rest. Example: ======== val goal = ([],(--`f (g x) /\ f (g x) /\ g 0`--)) : 'a list * term fun UNDISCH_HD_TAC (asm,g) = (UNDISCH_TAC (hd asm))(asm,g); - set_goal goal; (--`f (g x) /\ f (g x) /\ g 0`--) ============================= val it = () : unit - e(ASSUME_TAC (LEMMA_CONV (--`y:bool`--) (--`f(g(x:num):bool):bool`--))); OK.. 1 subgoal: (--`f (g x) /\ f (g x) /\ g 0`--) ============================= (--`?y. f (g x) = y`--) val it = () : unit - e(UNDISCH_HD_TAC THEN STRIP_TAC); OK.. 1 subgoal: (--`f (g x) /\ f (g x) /\ g 0`--) ============================= (--`f (g x) = y`--) val it = () : unit - e(ASM_REWRITE_TAC[]); OK.. 1 subgoal: (--`y /\ y /\ g 0`--) ============================= (--`f (g x) = y`--) val it = () : unit Cheers, Klaus