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);
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
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13315
diff changeset
     3
*)
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13315
diff changeset
     4
13314
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
     5
header{*The meta-existential quantifier*}
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
     6
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14854
diff changeset
     7
theory MetaExists imports Main begin
13314
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
     8
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
     9
text{*Allows quantification over any term having sort @{text logic}.  Used to
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    10
quantify over classes.  Yields a proposition rather than a FOL formula.*}
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    11
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 16417
diff changeset
    12
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    13
  ex :: "(('a::{}) => prop) => prop"  (binder "?? " 0) where
13314
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    14
  "ex(P) == (!!Q. (!!x. PROP P(x) ==> PROP Q) ==> PROP Q)"
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    15
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 16417
diff changeset
    16
notation (xsymbols)
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 16417
diff changeset
    17
  ex  (binder "\<Or>" 0)
13314
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    18
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    19
lemma meta_exI: "PROP P(x) ==> (?? x. PROP P(x))"
13315
wenzelm
parents: 13314
diff changeset
    20
proof (unfold ex_def)
13314
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    21
  assume P: "PROP P(x)"
13315
wenzelm
parents: 13314
diff changeset
    22
  fix Q
wenzelm
parents: 13314
diff changeset
    23
  assume PQ: "\<And>x. PROP P(x) \<Longrightarrow> PROP Q"
wenzelm
parents: 13314
diff changeset
    24
  from P show "PROP Q" by (rule PQ)
13314
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    25
qed 
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    26
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    27
lemma meta_exE: "[| ?? x. PROP P(x);  !!x. PROP P(x) ==> PROP R |] ==> PROP R"
13315
wenzelm
parents: 13314
diff changeset
    28
proof (unfold ex_def)
13314
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    29
  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
    30
  assume PR: "\<And>x. PROP P(x) \<Longrightarrow> PROP R"
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    31
  from PR show "PROP R" by (rule QPQ)
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    32
qed
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    33
84b9de3cbc91 Defining a meta-existential quantifier.
paulson
parents:
diff changeset
    34
end