1(*  Title:      ZF/Constructible/MetaExists.thy
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3*)
4
5section\<open>The meta-existential quantifier\<close>
6
7theory MetaExists imports ZF begin
8
9text\<open>Allows quantification over any term.  Used to quantify over classes.
10Yields a proposition rather than a FOL formula.\<close>
11
12definition
13  ex :: "(('a::{}) \<Rightarrow> prop) \<Rightarrow> prop"  (binder \<open>\<Or>\<close> 0) where
14  "ex(P) == (\<And>Q. (\<And>x. PROP P(x) \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q)"
15
16lemma meta_exI: "PROP P(x) ==> (\<Or>x. PROP P(x))"
17proof (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)
22qed 
23
24lemma meta_exE: "[|\<Or>x. PROP P(x);  \<And>x. PROP P(x) ==> PROP R |] ==> PROP R"
25proof (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)
29qed
30
31end
32