src/ZF/Constructible/MetaExists.thy
author wenzelm
Mon Dec 04 22:54:31 2017 +0100 (21 months ago)
changeset 67131 85d10959c2e4
parent 65449 c82e63b11b8b
child 69587 53982d5ec0bb
permissions -rw-r--r--
tuned signature;
paulson@13505
     1
(*  Title:      ZF/Constructible/MetaExists.thy
paulson@13505
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@13505
     3
*)
paulson@13505
     4
wenzelm@60770
     5
section\<open>The meta-existential quantifier\<close>
paulson@13314
     6
wenzelm@65449
     7
theory MetaExists imports ZF begin
paulson@13314
     8
wenzelm@61393
     9
text\<open>Allows quantification over any term.  Used to quantify over classes.
wenzelm@61393
    10
Yields a proposition rather than a FOL formula.\<close>
paulson@13314
    11
wenzelm@21233
    12
definition
wenzelm@61393
    13
  ex :: "(('a::{}) \<Rightarrow> prop) \<Rightarrow> prop"  (binder "\<Or>" 0) where
wenzelm@61393
    14
  "ex(P) == (\<And>Q. (\<And>x. PROP P(x) \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q)"
paulson@13314
    15
wenzelm@61393
    16
lemma meta_exI: "PROP P(x) ==> (\<Or>x. PROP P(x))"
wenzelm@13315
    17
proof (unfold ex_def)
paulson@13314
    18
  assume P: "PROP P(x)"
wenzelm@13315
    19
  fix Q
wenzelm@13315
    20
  assume PQ: "\<And>x. PROP P(x) \<Longrightarrow> PROP Q"
wenzelm@13315
    21
  from P show "PROP Q" by (rule PQ)
paulson@13314
    22
qed 
paulson@13314
    23
wenzelm@61393
    24
lemma meta_exE: "[|\<Or>x. PROP P(x);  \<And>x. PROP P(x) ==> PROP R |] ==> PROP R"
wenzelm@13315
    25
proof (unfold ex_def)
paulson@13314
    26
  assume QPQ: "\<And>Q. (\<And>x. PROP P(x) \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q"
paulson@13314
    27
  assume PR: "\<And>x. PROP P(x) \<Longrightarrow> PROP R"
paulson@13314
    28
  from PR show "PROP R" by (rule QPQ)
paulson@13314
    29
qed
paulson@13314
    30
paulson@13314
    31
end