src/ZF/Constructible/MetaExists.thy
author wenzelm
Thu Sep 02 00:48:07 2010 +0200 (2010-09-02)
changeset 38980 af73cf0dc31f
parent 32960 69916a850301
child 58871 c399ae4b836f
permissions -rw-r--r--
turned show_question_marks into proper configuration option;
show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;
tuned;
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
paulson@13314
     5
header{*The meta-existential quantifier*}
paulson@13314
     6
haftmann@16417
     7
theory MetaExists imports Main begin
paulson@13314
     8
paulson@13314
     9
text{*Allows quantification over any term having sort @{text logic}.  Used to
paulson@13314
    10
quantify over classes.  Yields a proposition rather than a FOL formula.*}
paulson@13314
    11
wenzelm@21233
    12
definition
wenzelm@21404
    13
  ex :: "(('a::{}) => prop) => prop"  (binder "?? " 0) where
paulson@13314
    14
  "ex(P) == (!!Q. (!!x. PROP P(x) ==> PROP Q) ==> PROP Q)"
paulson@13314
    15
wenzelm@21233
    16
notation (xsymbols)
wenzelm@21233
    17
  ex  (binder "\<Or>" 0)
paulson@13314
    18
paulson@13314
    19
lemma meta_exI: "PROP P(x) ==> (?? x. PROP P(x))"
wenzelm@13315
    20
proof (unfold ex_def)
paulson@13314
    21
  assume P: "PROP P(x)"
wenzelm@13315
    22
  fix Q
wenzelm@13315
    23
  assume PQ: "\<And>x. PROP P(x) \<Longrightarrow> PROP Q"
wenzelm@13315
    24
  from P show "PROP Q" by (rule PQ)
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"
wenzelm@13315
    28
proof (unfold ex_def)
paulson@13314
    29
  assume QPQ: "\<And>Q. (\<And>x. PROP P(x) \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q"
paulson@13314
    30
  assume PR: "\<And>x. PROP P(x) \<Longrightarrow> PROP R"
paulson@13314
    31
  from PR show "PROP R" by (rule QPQ)
paulson@13314
    32
qed
paulson@13314
    33
paulson@13314
    34
end