src/ZF/AC/WO6_WO1.thy
 author clasohm Tue Feb 06 12:27:17 1996 +0100 (1996-02-06) changeset 1478 2b8c2a7547ab parent 1401 0c439768f45c child 6068 2d8f3e1f1151 permissions -rw-r--r--
expanded tabs
```     1 (*  Title:      ZF/AC/WO6_WO1.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Krzysztof Grabczewski
```
```     4
```
```     5 The proof of "WO6 ==> WO1".
```
```     6
```
```     7 From the book "Equivalents of the Axiom of Choice" by Rubin & Rubin,
```
```     8 pages 2-5
```
```     9 *)
```
```    10
```
```    11 WO6_WO1 = "rel_is_fun" + AC_Equiv + Let +
```
```    12
```
```    13 consts
```
```    14 (* Auxiliary definitions used in proof *)
```
```    15   NN            :: i => i
```
```    16   uu            :: [i, i, i, i] => i
```
```    17   vv1, ww1, gg1 :: [i, i, i] => i
```
```    18   vv2, ww2, gg2 :: [i, i, i, i] => i
```
```    19
```
```    20 defs
```
```    21
```
```    22   NN_def  "NN(y) == {m:nat. EX a. EX f. Ord(a) & domain(f)=a  &
```
```    23                             (UN b<a. f`b) = y & (ALL b<a. f`b lepoll m)}"
```
```    24
```
```    25   uu_def  "uu(f, beta, gamma, delta) == (f`beta * f`gamma) Int f`delta"
```
```    26
```
```    27   (*Definitions for case 1*)
```
```    28
```
```    29   vv1_def "vv1(f,m,b) ==
```
```    30            let g = LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 &
```
```    31                                    domain(uu(f,b,g,d)) lepoll m));
```
```    32                d = LEAST d. domain(uu(f,b,g,d)) ~= 0 &
```
```    33                            domain(uu(f,b,g,d)) lepoll m
```
```    34            in  if(f`b ~= 0, domain(uu(f,b,g,d)), 0)"
```
```    35
```
```    36   ww1_def "ww1(f,m,b) == f`b - vv1(f,m,b)"
```
```    37
```
```    38   gg1_def "gg1(f,a,m) == lam b:a++a. if (b<a, vv1(f,m,b), ww1(f,m,b--a))"
```
```    39
```
```    40   (*Definitions for case 2*)
```
```    41
```
```    42   vv2_def "vv2(f,b,g,s) ==
```
```    43            if(f`g ~= 0, {uu(f, b, g, LEAST d. uu(f,b,g,d) ~= 0)`s}, 0)"
```
```    44
```
```    45   ww2_def "ww2(f,b,g,s) == f`g - vv2(f,b,g,s)"
```
```    46
```
```    47   gg2_def "gg2(f,a,b,s) == lam g:a++a. if (g<a, vv2(f,b,g,s), ww2(f,b,g--a,s))"
```
```    48
```
```    49 end
```