src/ZF/Constructible/MetaExists.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 32960 69916a850301
child 58871 c399ae4b836f
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);

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

header{*The meta-existential quantifier*}

theory MetaExists imports Main begin

text{*Allows quantification over any term having sort @{text logic}.  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)"

notation (xsymbols)
  ex  (binder "\<Or>" 0)

lemma meta_exI: "PROP P(x) ==> (?? x. PROP P(x))"
proof (unfold ex_def)
  assume P: "PROP P(x)"
  fix Q
  assume PQ: "\<And>x. PROP P(x) \<Longrightarrow> 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: "\<And>Q. (\<And>x. PROP P(x) \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q"
  assume PR: "\<And>x. PROP P(x) \<Longrightarrow> PROP R"
  from PR show "PROP R" by (rule QPQ)
qed

end