src/ZF/Constructible/MetaExists.thy
author ballarin
Thu Dec 11 18:30:26 2008 +0100 (2008-12-11)
changeset 29223 e09c53289830
parent 21404 eb85850d3eb7
child 32960 69916a850301
permissions -rw-r--r--
Conversion of HOL-Main and ZF to new locales.
     1 (*  Title:      ZF/Constructible/MetaExists.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4 *)
     5 
     6 header{*The meta-existential quantifier*}
     7 
     8 theory MetaExists imports Main begin
     9 
    10 text{*Allows quantification over any term having sort @{text logic}.  Used to
    11 quantify over classes.  Yields a proposition rather than a FOL formula.*}
    12 
    13 definition
    14   ex :: "(('a::{}) => prop) => prop"  (binder "?? " 0) where
    15   "ex(P) == (!!Q. (!!x. PROP P(x) ==> PROP Q) ==> PROP Q)"
    16 
    17 notation (xsymbols)
    18   ex  (binder "\<Or>" 0)
    19 
    20 lemma meta_exI: "PROP P(x) ==> (?? x. PROP P(x))"
    21 proof (unfold ex_def)
    22   assume P: "PROP P(x)"
    23   fix Q
    24   assume PQ: "\<And>x. PROP P(x) \<Longrightarrow> PROP Q"
    25   from P show "PROP Q" by (rule PQ)
    26 qed 
    27 
    28 lemma meta_exE: "[| ?? x. PROP P(x);  !!x. PROP P(x) ==> PROP R |] ==> PROP R"
    29 proof (unfold ex_def)
    30   assume QPQ: "\<And>Q. (\<And>x. PROP P(x) \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q"
    31   assume PR: "\<And>x. PROP P(x) \<Longrightarrow> PROP R"
    32   from PR show "PROP R" by (rule QPQ)
    33 qed
    34 
    35 end