src/ZF/Constructible/MetaExists.thy
 author wenzelm Thu Dec 14 11:24:26 2017 +0100 (21 months ago) changeset 67198 694f29a5433b parent 65449 c82e63b11b8b child 69587 53982d5ec0bb permissions -rw-r--r--
merged
```     1 (*  Title:      ZF/Constructible/MetaExists.thy
```
```     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     3 *)
```
```     4
```
```     5 section\<open>The meta-existential quantifier\<close>
```
```     6
```
```     7 theory MetaExists imports ZF begin
```
```     8
```
```     9 text\<open>Allows quantification over any term.  Used to quantify over classes.
```
```    10 Yields a proposition rather than a FOL formula.\<close>
```
```    11
```
```    12 definition
```
```    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)"
```
```    15
```
```    16 lemma meta_exI: "PROP P(x) ==> (\<Or>x. PROP P(x))"
```
```    17 proof (unfold ex_def)
```
```    18   assume P: "PROP P(x)"
```
```    19   fix Q
```
```    20   assume PQ: "\<And>x. PROP P(x) \<Longrightarrow> PROP Q"
```
```    21   from P show "PROP Q" by (rule PQ)
```
```    22 qed
```
```    23
```
```    24 lemma meta_exE: "[|\<Or>x. PROP P(x);  \<And>x. PROP P(x) ==> PROP R |] ==> PROP R"
```
```    25 proof (unfold ex_def)
```
```    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
```