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; Fri, 28 May 1993 12:57:04 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA02668; Fri, 28 May 93 04:47:02 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA02663; Fri, 28 May 93 04:46:52 -0700 Received: from puffin.cl.cam.ac.uk (user btg (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Fri, 28 May 1993 12:45:48 +0100 To: reetz Cc: info-hol@ted.cs.uidaho.edu Subject: Re: Elemination of @-terms In-Reply-To: Your message of "Fri, 28 May 93 09:42:55 +0700." <9305280943.AA02616@ted.cs.uidaho.edu> Date: Fri, 28 May 93 12:45:40 +0100 From: Brian Graham Message-Id: <"swan.cl.cam.:273990:930528114551"@cl.cam.ac.uk> Ralf Reetz writes: > I would like to proof the following goal: > > ([],--`(@m. ?vn. (m = F) /\ (vn = vn1)) = F`--); > A long time ago I wrote a tactic called SELECT_UNIQUE_TAC for precisely this sort of problem. In fact it fails on this particular problem --- an incorrect substitution was made in the proof function. I have corrected this now, and the code, followed by its application (in HOL88, sorry) are below. This correction will be incorporated in the paper "Dealing with the Choice Operator in HOL88", which is available in the contrib directory of HOL88, in the subdirectory `select'. Brian Graham % SELECT_UNIQUE_RULE: =================== "y" A1 |- Q[y] A2 |- !x y.(Q[x]/\Q[y]) ==> (x=y) =================================================== A1 U A2 |- (@x.Q[x]) = y Permits substitution for values specified by the Hilbert Choice operator with a specific value, if and only if unique existance of the specific value is proven. % let SELECT_UNIQUE_RULE y th1 th2 = let Q = (hd o conjuncts o fst o dest_imp o snd o strip_forall o concl)th2 in let x = (hd o (filter (C mem (frees Q))) o fst o strip_forall o concl) th2 in let Q' = mk_abs (x,Q) in let th1' = SUBST [SYM (BETA_CONV "^Q' ^y"), "b:bool"] "b:bool" th1 in (MP (SPECL ["$@ ^Q'"; y] th2) (CONJ (in1_conv_rule BETA_CONV (SELECT_INTRO th1')) th1));; % SELECT_UNIQUE_TAC: ================== [ A ] "(@x. Q[x]) = y" =================================================== [ A ] "Q[y]" [ A ] "!x y.(Q[x]/\Q[y]) ==> (x=y)" Given a goal that requires proof of the value specified by the Hilbert choice operator, it returns 2 subgoals: 1. "y" satisfies the predicate, and 2. unique existance of the value that satisfies the predicate. % let SELECT_UNIQUE_TAC:tactic (gl,g) = let Q,y = dest_eq g in let x,Qx = dest_select Q in let x' = variant (x.freesl(g.gl))x in let Qx' = subst [x', x] Qx in ([gl,subst [y,x]Qx; gl, "!^x ^x'. (^Qx /\ ^Qx') ==> (^x = ^x')"], (\thl. SELECT_UNIQUE_RULE y (hd thl) (hd (tl thl))));; % ============================================================= % g "(@(m:bool). ?(vn:*). (m = F) /\ (vn = vn1:*)) = F";; "(@m. ?vn. (m = F) /\ (vn = vn1)) = F" () : void #expand (SELECT_UNIQUE_TAC);; OK.. 2 subgoals "!m m'. (?vn. (m = F) /\ (vn = vn1)) /\ (?vn. (m' = F) /\ (vn = vn1)) ==> (m = m')" "?vn. (F = F) /\ (vn = vn1)" () : void #expand (EXISTS_TAC "vn1:*" THEN REWRITE_TAC[]);; OK.. goal proved |- ?vn. (F = F) /\ (vn = vn1) Previous subproof: "!m m'. (?vn. (m = F) /\ (vn = vn1)) /\ (?vn. (m' = F) /\ (vn = vn1)) ==> (m = m')" () : void #expand (REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);; OK.. goal proved |- !m m'. (?vn. (m = F) /\ (vn = vn1)) /\ (?vn. (m' = F) /\ (vn = vn1)) ==> (m = m') |- (@m. ?vn. (m = F) /\ (vn = vn1)) = F Previous subproof: goal proved () : void