src/ZF/Constructible/MetaExists.thy
author paulson
Mon Jul 08 15:56:39 2002 +0200 (2002-07-08)
changeset 13314 84b9de3cbc91
child 13315 685499c73215
permissions -rw-r--r--
Defining a meta-existential quantifier.
Using it to streamline reflection proofs.
paulson@13314
     1
header{*The meta-existential quantifier*}
paulson@13314
     2
paulson@13314
     3
theory MetaExists = Main:
paulson@13314
     4
paulson@13314
     5
text{*Allows quantification over any term having sort @{text logic}.  Used to
paulson@13314
     6
quantify over classes.  Yields a proposition rather than a FOL formula.*}
paulson@13314
     7
paulson@13314
     8
constdefs
paulson@13314
     9
  ex :: "(('a::logic) => prop) => prop"            (binder "?? " 0)
paulson@13314
    10
  "ex(P) == (!!Q. (!!x. PROP P(x) ==> PROP Q) ==> PROP Q)"
paulson@13314
    11
paulson@13314
    12
syntax (xsymbols)
paulson@13314
    13
  "?? "        :: "[idts, o] => o"             ("(3\<Or>_./ _)" [0, 0] 0)
paulson@13314
    14
paulson@13314
    15
lemma meta_exI: "PROP P(x) ==> (?? x. PROP P(x))"
paulson@13314
    16
proof -
paulson@13314
    17
  assume P: "PROP P(x)"
paulson@13314
    18
  show "?? x. PROP P(x)"
paulson@13314
    19
  apply (unfold ex_def)
paulson@13314
    20
  proof -
paulson@13314
    21
    fix Q
paulson@13314
    22
    assume PQ: "\<And>x. PROP P(x) \<Longrightarrow> PROP Q"
paulson@13314
    23
    from P show "PROP Q" by (rule PQ)
paulson@13314
    24
  qed
paulson@13314
    25
qed 
paulson@13314
    26
paulson@13314
    27
lemma meta_exE: "[| ?? x. PROP P(x);  !!x. PROP P(x) ==> PROP R |] ==> PROP R"
paulson@13314
    28
apply (unfold ex_def)
paulson@13314
    29
proof -
paulson@13314
    30
  assume QPQ: "\<And>Q. (\<And>x. PROP P(x) \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q"
paulson@13314
    31
  assume PR: "\<And>x. PROP P(x) \<Longrightarrow> PROP R"
paulson@13314
    32
  from PR show "PROP R" by (rule QPQ)
paulson@13314
    33
qed
paulson@13314
    34
paulson@13314
    35
end