src/ZF/Constructible/MetaExists.thy
 author paulson Fri Aug 16 16:41:48 2002 +0200 (2002-08-16) changeset 13505 52a16cb7fefb parent 13315 685499c73215 child 13634 99a593b49b04 permissions -rw-r--r--
Relativized right up to L satisfies V=L!
 paulson@13505 1 (* Title: ZF/Constructible/MetaExists.thy paulson@13505 2 ID: \$Id\$ paulson@13505 3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory paulson@13505 4 Copyright 2002 University of Cambridge paulson@13505 5 *) paulson@13505 6 paulson@13314 7 header{*The meta-existential quantifier*} paulson@13314 8 paulson@13314 9 theory MetaExists = Main: paulson@13314 10 paulson@13314 11 text{*Allows quantification over any term having sort @{text logic}. Used to paulson@13314 12 quantify over classes. Yields a proposition rather than a FOL formula.*} paulson@13314 13 paulson@13314 14 constdefs paulson@13314 15 ex :: "(('a::logic) => prop) => prop" (binder "?? " 0) paulson@13314 16 "ex(P) == (!!Q. (!!x. PROP P(x) ==> PROP Q) ==> PROP Q)" paulson@13314 17 paulson@13314 18 syntax (xsymbols) paulson@13314 19 "?? " :: "[idts, o] => o" ("(3\_./ _)" [0, 0] 0) paulson@13314 20 paulson@13314 21 lemma meta_exI: "PROP P(x) ==> (?? x. PROP P(x))" wenzelm@13315 22 proof (unfold ex_def) paulson@13314 23 assume P: "PROP P(x)" wenzelm@13315 24 fix Q wenzelm@13315 25 assume PQ: "\x. PROP P(x) \ PROP Q" wenzelm@13315 26 from P show "PROP Q" by (rule PQ) paulson@13314 27 qed paulson@13314 28 paulson@13314 29 lemma meta_exE: "[| ?? x. PROP P(x); !!x. PROP P(x) ==> PROP R |] ==> PROP R" wenzelm@13315 30 proof (unfold ex_def) paulson@13314 31 assume QPQ: "\Q. (\x. PROP P(x) \ PROP Q) \ PROP Q" paulson@13314 32 assume PR: "\x. PROP P(x) \ PROP R" paulson@13314 33 from PR show "PROP R" by (rule QPQ) paulson@13314 34 qed paulson@13314 35 paulson@13314 36 end