Theory MetaExists

(*  Title:      ZF/Constructible/MetaExists.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
*)

section‹The meta-existential quantifier›

theory MetaExists imports ZF begin

text‹Allows quantification over any term.  Used to quantify over classes.
Yields a proposition rather than a FOL formula.›

definition
  ex :: "(('a::{}) ⇒ prop) ⇒ prop"  (binder ‹⋁› 0) where
  "ex(P) ≡ (⋀Q. (⋀x. PROP P(x) ⟹ PROP Q) ⟹ PROP Q)"

lemma meta_exI: "PROP P(x) ⟹ (⋁x. PROP P(x))"
proof (unfold ex_def)
  assume P: "PROP P(x)"
  fix Q
  assume PQ: "⋀x. PROP P(x) ⟹ PROP Q"
  from P show "PROP Q" by (rule PQ)
qed 

lemma meta_exE: "⟦⋁x. PROP P(x);  ⋀x. PROP P(x) ⟹ PROP R⟧ ⟹ PROP R"
proof (unfold ex_def)
  assume QPQ: "⋀Q. (⋀x. PROP P(x) ⟹ PROP Q) ⟹ PROP Q"
  assume PR: "⋀x. PROP P(x) ⟹ PROP R"
  from PR show "PROP R" by (rule QPQ)
qed

end