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