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; Tue, 2 Mar 1993 11:26:25 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA06218; Tue, 2 Mar 93 03:11:02 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from ganymede.inmos.co.uk by ted.cs.uidaho.edu (16.6/1.34) id AA06213; Tue, 2 Mar 93 03:10:41 -0800 Received: from frogland.inmos.co.uk by ganymede.inmos.co.uk; Tue, 2 Mar 93 11:10:11 GMT From: David Shepherd Message-Id: <19307.9303021110@frogland.inmos.co.uk> Subject: Re: pair proof To: blok@nl.utwente.cs (Rintcius Blok) Date: Tue, 2 Mar 1993 11:10:08 +0000 (GMT) Cc: info-hol@edu.uidaho.cs.ted (info-hol mailing list) In-Reply-To: <9303021014.AA00306@apollo.cs.utwente.nl> from "Rintcius Blok" at Mar 2, 93 11:14:23 am X-Mailer: ELM [version 2.4 PL20] Content-Type: text Content-Length: 6033 Rintcius Blok has said: > I have a problem with proving the following goal: > > g "!P.(!(x:*) (y:**).x IN X /\ y IN Y==>P(x,y))= > (!z.(FST z) IN X /\ (SND z) IN Y ==>P z)";; > > I think the proof is not difficult and can be very short, > but I cannot find/derive an appropriate theorem to "jump" from > the first pair repr. to the second. > > Is there anyone who can help? Below is some stuff which may help. They replace quantified tuples by iterated quantifications of components of the tuple. I hope the definitions don't depend on any of my other standard extensions! X_term_FORALL_CONV "(x0,...,xn)" "! z. P z" ------------------------------------------ (x0,...,xn) has compatible `shape` to z "(! z. P z) = (! x0 ... xn. P(x0,...xn)" X_term_FORALL_CONV constructs the term for you by generating a term for every leaf in the tree of pair constructions. X_term_FORALL_CONV "! z. P z" ------------------------------------------- "(! z. P z) = (! z_0 ... z_n. P(z_0,...,z_n) and similarily for exists, pair_FORALL, X_pair_FORALL etc just handle on level of pairing. In your example what you want to do is GEN_TAC THEN CONV_TAC(RAND_CONV pair_FORALL_CONV) THEN ONCE_REWRITE_TAC[FST;SND] THEN REFL_TAC and I think that will prove the goal. -------------------------------------------------------------------------- david shepherd: des@inmos.co.uk tel: 0454-616616 x 625 inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq Life doesn't imitate art, it imitates bad television - Husbands and Wives -------------------------------------------------------------------------- let is_pair_type ty = (not(is_vartype ty)) & ((fst o dest_type) ty = `prod`);; let numstr n = let mod m n = m - (n* (m/n)) in letrec f s n = if (n=0) then s else f ((ascii((mod n 26) + 97)).s) (n / 26) in implode(f [] n);; letref tempstr = (`tmp_`,1);; let init_tempstr s = tempstr:= (s^`_`,0);();; let gen_tmp ty = let (name,num) = tempstr in (tempstr := (name,num+1);mk_var(name^(string_of_int num),ty));; let strip' s = letrec f sl = if (hd sl = `'`) then f (tl sl) else sl in (implode o rev o f o rev o explode) s;; let gen_pair t = let (v,(op,[ty1;ty2])) = ((strip' # dest_type) o dest_var) t in (mk_var(v^`_l`,ty1),mk_var(v^`_r`,ty2));; let mk_tuple (s,ty) = letrec f ty = if (is_pair_type ty) then let [ty1;ty2] = (snd o dest_type)ty in mk_pair(f ty1,f ty2) else gen_tmp ty in (init_tempstr(strip' s);f ty);; let pair_EXISTS_THM = prove("! (f:((*#**)->bool)) . (? z . f z) = (?x y . f (x,y))", GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL [ EXISTS_TAC "FST(z:*#**)" THEN EXISTS_TAC "SND(z:*#**)" THEN ASM_REWRITE_TAC[PAIR] ; EXISTS_TAC"x:*,y:**" THEN POP_ASSUM ACCEPT_TAC ]);; let X_pair_EXISTS_CONV (v1,v2) tm = let tm' = (snd o dest_comb)tm in let (v,b) = dest_abs tm' in let th1 = MATCH_SPEC tm' pair_EXISTS_THM in CONV_RULE((RATOR_CONV o RAND_CONV o RAND_CONV)(ALPHA_CONV v THENC (ABS_CONV BETA_CONV)) THENC (RAND_CONV o RAND_CONV)(ALPHA_CONV v1 THENC (ABS_CONV o RAND_CONV)(ALPHA_CONV v2 THENC (ABS_CONV BETA_CONV)))) th1;; let pair_EXISTS_CONV tm = X_pair_EXISTS_CONV ((gen_pair o fst o dest_exists)tm) tm;; %---------------------------------------- term_EXISTS_CONV tm "? x . f x" --> "? v1 ... vn . f tm" where v1 ... vn are the variables in tm used to untuple the internal state in the specs etc copes with any shape of tm (i.e. untuples nested tuples) ----------------------------------------% letrec X_term_EXISTS_CONV tm t = if (is_pair tm) then let (tm1,tm2) = dest_pair tm in let v1 = genvar(type_of tm1) and v2 = genvar(type_of tm2) in ((X_pair_EXISTS_CONV(v1,v2)) THENC (RAND_CONV o ABS_CONV)(X_term_EXISTS_CONV tm2) THENC (X_term_EXISTS_CONV tm1)) t else (RAND_CONV (ALPHA_CONV tm) t);; let term_EXISTS_CONV t = if (is_exists t) & ((is_pair_type o type_of o fst o dest_exists)t) then X_term_EXISTS_CONV(mk_tuple((dest_var o fst o dest_exists)t))t else failwith `term_EXISTS_CONV`;; let REV = CONV_RULE(ONCE_DEPTH_CONV SYM_CONV);; let pair_FORALL_THM = prove("! (f:((*#**)->bool)) . (! z . f z) = (!x y . f (x,y))", GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL [ ASM_REWRITE_TAC[] ; GEN_TAC THEN ONCE_REWRITE_TAC[REV PAIR] THEN PURE_ASM_REWRITE_TAC[] ]);; let X_pair_FORALL_CONV (v1,v2) tm = let tm' = (snd o dest_comb)tm in let (v,b) = dest_abs tm' in let th1 = ISPEC tm' pair_FORALL_THM in CONV_RULE((RATOR_CONV o RAND_CONV o RAND_CONV)(ALPHA_CONV v THENC (ABS_CONV BETA_CONV)) THENC (RAND_CONV o RAND_CONV)(ALPHA_CONV v1 THENC (ABS_CONV o RAND_CONV)(ALPHA_CONV v2 THENC (ABS_CONV BETA_CONV)))) th1;; let pair_FORALL_CONV tm = X_pair_FORALL_CONV ((gen_pair o fst o dest_forall)tm) tm;; %---------------------------------------- term_FORALL_CONV tm "! x . f x" --> "! v1 ... vn . f tm" where v1 ... vn are the variables in tm used to untuple the internal state in the specs etc copes with any shape of tm (i.e. untuples nested tuples) ----------------------------------------% letrec X_term_FORALL_CONV tm t = let (tm1,tm2) = dest_pair tm in let (c1,v1) = if (is_var tm1) then (I,tm1) else ((\c.c THENC (X_term_FORALL_CONV tm1)), genvar(type_of tm1)) in let (c2,v2) = if (is_var tm2) then (I,tm2) else ((\c.c THENC (RAND_CONV o ABS_CONV) (X_term_FORALL_CONV tm2)), genvar(type_of tm2)) in ((c1 o c2)(X_pair_FORALL_CONV(v1,v2))) t;; let term_FORALL_CONV t = if (is_forall t) & ((is_pair_type o type_of o fst o dest_forall)t) then X_term_FORALL_CONV(mk_tuple((dest_var o fst o dest_forall)t))t else failwith `term_FORALL_CONV`;;