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