src/ZF/Constructible/MetaExists.thy
author wenzelm
Thu Dec 14 11:24:26 2017 +0100 (21 months ago)
changeset 67198 694f29a5433b
parent 65449 c82e63b11b8b
child 69587 53982d5ec0bb
permissions -rw-r--r--
merged
     1 (*  Title:      ZF/Constructible/MetaExists.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3 *)
     4 
     5 section\<open>The meta-existential quantifier\<close>
     6 
     7 theory MetaExists imports ZF begin
     8 
     9 text\<open>Allows quantification over any term.  Used to quantify over classes.
    10 Yields a proposition rather than a FOL formula.\<close>
    11 
    12 definition
    13   ex :: "(('a::{}) \<Rightarrow> prop) \<Rightarrow> prop"  (binder "\<Or>" 0) where
    14   "ex(P) == (\<And>Q. (\<And>x. PROP P(x) \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q)"
    15 
    16 lemma meta_exI: "PROP P(x) ==> (\<Or>x. PROP P(x))"
    17 proof (unfold ex_def)
    18   assume P: "PROP P(x)"
    19   fix Q
    20   assume PQ: "\<And>x. PROP P(x) \<Longrightarrow> PROP Q"
    21   from P show "PROP Q" by (rule PQ)
    22 qed 
    23 
    24 lemma meta_exE: "[|\<Or>x. PROP P(x);  \<And>x. PROP P(x) ==> PROP R |] ==> PROP R"
    25 proof (unfold ex_def)
    26   assume QPQ: "\<And>Q. (\<And>x. PROP P(x) \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q"
    27   assume PR: "\<And>x. PROP P(x) \<Longrightarrow> PROP R"
    28   from PR show "PROP R" by (rule QPQ)
    29 qed
    30 
    31 end