# Theory MetaExists

Up to index of Isabelle/ZF/Constructible

theory MetaExists
imports Main
begin

    (*  Title:      ZF/Constructible/MetaExists.thy
        ID:         $Id: MetaExists.thy,v 1.6 2005/06/17 14:15:10 haftmann Exp $
        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.*}

    constdefs
      ex :: "(('a::{}) => prop) => prop"            (binder "?? " 0)
      "ex(P) == (!!Q. (!!x. PROP P(x) ==> PROP Q) ==> PROP Q)"

    syntax (xsymbols)
      "?? "        :: "[idts, o] => o"             ("(3\<Or>_./ _)" [0, 0] 0)

    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

lemma meta_exI:

      PROP P(x) ==> (?? x. PROP P(x))

lemma meta_exE:

      [| ?? x. PROP P(x); !!x. PROP P(x) ==> PROP R |] ==> PROP R