src/ZF/Constructible/MetaExists.thy
author wenzelm
Thu Sep 02 00:48:07 2010 +0200 (2010-09-02)
changeset 38980 af73cf0dc31f
parent 32960 69916a850301
child 58871 c399ae4b836f
permissions -rw-r--r--
turned show_question_marks into proper configuration option;
show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;
tuned;
     1 (*  Title:      ZF/Constructible/MetaExists.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3 *)
     4 
     5 header{*The meta-existential quantifier*}
     6 
     7 theory MetaExists imports Main begin
     8 
     9 text{*Allows quantification over any term having sort @{text logic}.  Used to
    10 quantify over classes.  Yields a proposition rather than a FOL formula.*}
    11 
    12 definition
    13   ex :: "(('a::{}) => prop) => prop"  (binder "?? " 0) where
    14   "ex(P) == (!!Q. (!!x. PROP P(x) ==> PROP Q) ==> PROP Q)"
    15 
    16 notation (xsymbols)
    17   ex  (binder "\<Or>" 0)
    18 
    19 lemma meta_exI: "PROP P(x) ==> (?? x. PROP P(x))"
    20 proof (unfold ex_def)
    21   assume P: "PROP P(x)"
    22   fix Q
    23   assume PQ: "\<And>x. PROP P(x) \<Longrightarrow> PROP Q"
    24   from P show "PROP Q" by (rule PQ)
    25 qed 
    26 
    27 lemma meta_exE: "[| ?? x. PROP P(x);  !!x. PROP P(x) ==> PROP R |] ==> PROP R"
    28 proof (unfold ex_def)
    29   assume QPQ: "\<And>Q. (\<And>x. PROP P(x) \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q"
    30   assume PR: "\<And>x. PROP P(x) \<Longrightarrow> PROP R"
    31   from PR show "PROP R" by (rule QPQ)
    32 qed
    33 
    34 end