src/ZF/Constructible/MetaExists.thy
author wenzelm
Mon Jul 29 00:57:16 2002 +0200 (2002-07-29)
changeset 13428 99e52e78eb65
parent 13315 685499c73215
child 13505 52a16cb7fefb
permissions -rw-r--r--
eliminate open locales and special ML code;
     1 header{*The meta-existential quantifier*}
     2 
     3 theory MetaExists = Main:
     4 
     5 text{*Allows quantification over any term having sort @{text logic}.  Used to
     6 quantify over classes.  Yields a proposition rather than a FOL formula.*}
     7 
     8 constdefs
     9   ex :: "(('a::logic) => prop) => prop"            (binder "?? " 0)
    10   "ex(P) == (!!Q. (!!x. PROP P(x) ==> PROP Q) ==> PROP Q)"
    11 
    12 syntax (xsymbols)
    13   "?? "        :: "[idts, o] => o"             ("(3\<Or>_./ _)" [0, 0] 0)
    14 
    15 lemma meta_exI: "PROP P(x) ==> (?? x. PROP P(x))"
    16 proof (unfold ex_def)
    17   assume P: "PROP P(x)"
    18   fix Q
    19   assume PQ: "\<And>x. PROP P(x) \<Longrightarrow> PROP Q"
    20   from P show "PROP Q" by (rule PQ)
    21 qed 
    22 
    23 lemma meta_exE: "[| ?? x. PROP P(x);  !!x. PROP P(x) ==> PROP R |] ==> PROP R"
    24 proof (unfold ex_def)
    25   assume QPQ: "\<And>Q. (\<And>x. PROP P(x) \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q"
    26   assume PR: "\<And>x. PROP P(x) \<Longrightarrow> PROP R"
    27   from PR show "PROP R" by (rule QPQ)
    28 qed
    29 
    30 end