src/ZF/Constructible/MetaExists.thy
 author paulson Wed Aug 21 15:57:24 2002 +0200 (2002-08-21) changeset 13513 b9e14471629c parent 13505 52a16cb7fefb child 13634 99a593b49b04 permissions -rw-r--r--
tweaks
```     1 (*  Title:      ZF/Constructible/MetaExists.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   2002  University of Cambridge
```
```     5 *)
```
```     6
```
```     7 header{*The meta-existential quantifier*}
```
```     8
```
```     9 theory MetaExists = Main:
```
```    10
```
```    11 text{*Allows quantification over any term having sort @{text logic}.  Used to
```
```    12 quantify over classes.  Yields a proposition rather than a FOL formula.*}
```
```    13
```
```    14 constdefs
```
```    15   ex :: "(('a::logic) => prop) => prop"            (binder "?? " 0)
```
```    16   "ex(P) == (!!Q. (!!x. PROP P(x) ==> PROP Q) ==> PROP Q)"
```
```    17
```
```    18 syntax (xsymbols)
```
```    19   "?? "        :: "[idts, o] => o"             ("(3\<Or>_./ _)" [0, 0] 0)
```
```    20
```
```    21 lemma meta_exI: "PROP P(x) ==> (?? x. PROP P(x))"
```
```    22 proof (unfold ex_def)
```
```    23   assume P: "PROP P(x)"
```
```    24   fix Q
```
```    25   assume PQ: "\<And>x. PROP P(x) \<Longrightarrow> PROP Q"
```
```    26   from P show "PROP Q" by (rule PQ)
```
```    27 qed
```
```    28
```
```    29 lemma meta_exE: "[| ?? x. PROP P(x);  !!x. PROP P(x) ==> PROP R |] ==> PROP R"
```
```    30 proof (unfold ex_def)
```
```    31   assume QPQ: "\<And>Q. (\<And>x. PROP P(x) \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q"
```
```    32   assume PR: "\<And>x. PROP P(x) \<Longrightarrow> PROP R"
```
```    33   from PR show "PROP R" by (rule QPQ)
```
```    34 qed
```
```    35
```
```    36 end
```