src/ZF/Constructible/MetaExists.thy
author paulson
Fri, 16 Aug 2002 16:41:48 +0200
changeset 13505 52a16cb7fefb
parent 13315 685499c73215
child 13634 99a593b49b04
permissions -rw-r--r--
Relativized right up to L satisfies V=L!
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13315
diff changeset
     1
(*  Title:      ZF/Constructible/MetaExists.thy
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13315
diff changeset
     2
    ID:         $Id$
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13315
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13315
diff changeset
     4
    Copyright   2002  University of Cambridge
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13315
diff changeset
     5
*)
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13315
diff changeset
     6
13314
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
     7
header{*The meta-existential quantifier*}
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
     8
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
     9
theory MetaExists = Main:
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    10
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    11
text{*Allows quantification over any term having sort @{text logic}.  Used to
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    12
quantify over classes.  Yields a proposition rather than a FOL formula.*}
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    13
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    14
constdefs
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    15
  ex :: "(('a::logic) => prop) => prop"            (binder "?? " 0)
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    16
  "ex(P) == (!!Q. (!!x. PROP P(x) ==> PROP Q) ==> PROP Q)"
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    17
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    18
syntax (xsymbols)
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    19
  "?? "        :: "[idts, o] => o"             ("(3\<Or>_./ _)" [0, 0] 0)
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    20
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    21
lemma meta_exI: "PROP P(x) ==> (?? x. PROP P(x))"
13315
wenzelm
parents: 13314
diff changeset
    22
proof (unfold ex_def)
13314
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    23
  assume P: "PROP P(x)"
13315
wenzelm
parents: 13314
diff changeset
    24
  fix Q
wenzelm
parents: 13314
diff changeset
    25
  assume PQ: "\<And>x. PROP P(x) \<Longrightarrow> PROP Q"
wenzelm
parents: 13314
diff changeset
    26
  from P show "PROP Q" by (rule PQ)
13314
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    27
qed 
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    28
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    29
lemma meta_exE: "[| ?? x. PROP P(x);  !!x. PROP P(x) ==> PROP R |] ==> PROP R"
13315
wenzelm
parents: 13314
diff changeset
    30
proof (unfold ex_def)
13314
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    31
  assume QPQ: "\<And>Q. (\<And>x. PROP P(x) \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q"
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    32
  assume PR: "\<And>x. PROP P(x) \<Longrightarrow> PROP R"
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    33
  from PR show "PROP R" by (rule QPQ)
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    34
qed
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    35
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    36
end