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