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