# HG changeset patch
# User lcp
# Date 797775502 -7200
# Node ID 04ef9b8ef1af7063f4e5dbe6cd36c7a5f8a6fcd5
# Parent  6664d0b54d0fbab0e164a56c973f63b0aae306d4
Defined vv1 using let.  Introduced gg1, gg2.

diff -r 6664d0b54d0f -r 04ef9b8ef1af src/ZF/AC/WO6_WO1.thy
--- a/src/ZF/AC/WO6_WO1.thy	Thu Apr 13 14:15:36 1995 +0200
+++ b/src/ZF/AC/WO6_WO1.thy	Thu Apr 13 14:18:22 1995 +0200
@@ -6,16 +6,23 @@
 
 From the book "Equivalents of the Axiom of Choice" by Rubin & Rubin,
 pages 2-5
+
+
+  vv1_def "vv1(f,m,b) == if(f`b ~= 0,   \
+\          domain(uu(f, b, thing(f,b,g,d),   \
+\          LEAST d. domain(uu(f, b, thing(f,b,g,d), d)) ~= 0 &   \
+\          domain(uu(f,b, thing(f,b,g,d), d)) lepoll m)), 0)"
+
 *)
 
-WO6_WO1 = "rel_is_fun" + AC_Equiv +
+WO6_WO1 = "rel_is_fun" + AC_Equiv + Let +
 
 consts
 (* Auxiliary definitions used in proof *)
-  NN       :: "i => i"
-  uu       :: "[i, i, i, i] => i"
-  vv1, ww1 :: "[i, i, i] => i"
-  vv2, ww2 :: "[i, i, i, i] => i"
+  NN            :: "i => i"
+  uu            :: "[i, i, i, i] => i"
+  vv1, ww1, gg1 :: "[i, i, i] => i"
+  vv2, ww2, gg2 :: "[i, i, i, i] => i"
 
 defs
 
@@ -23,23 +30,27 @@
 \			    (UN b<a. f`b) = y & (ALL b<a. f`b lepoll m)}"
 
   uu_def  "uu(f, beta, gamma, delta) == (f`beta * f`gamma) Int f`delta"
+
+  (*Definitions for case 1*)
+
+  vv1_def "vv1(f,m,b) ==   						\
+\   	   let g = LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 &	\
+\	                           domain(uu(f,b,g,d)) lepoll m));   	\
+\	       d = LEAST d. domain(uu(f,b,g,d)) ~= 0 &   		\
+\                           domain(uu(f,b,g,d)) lepoll m		\
+\	   in  if(f`b ~= 0, domain(uu(f,b,g,d)), 0)"
+
+  ww1_def "ww1(f,m,b) == f`b - vv1(f,m,b)"
+
+  gg1_def "gg1(f,a,m) == lam b:a++a. if (b<a, vv1(f,m,b), ww1(f,m,b--a))"
   
-  vv1_def "vv1(f,b,m) == if(f`b ~= 0,   \
-\          domain(uu(f,b,   \
-\          LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 &   \
-\	   domain(uu(f,b,g,d)) lesspoll m)),   \
-\          LEAST d. domain(uu(f,b,   \
-\          LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 &   \
-\	   domain(uu(f,b,g,d)) lesspoll m)), d)) ~= 0 &   \
-\          domain(uu(f,b,   \
-\          LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 &   \
-\	   domain(uu(f,b,g,d)) lesspoll m)), d)) lesspoll m)), 0)"
-
-  ww1_def "ww1(f,b,m) == f`b - vv1(f,b,m)"
+  (*Definitions for case 2*)
 
   vv2_def "vv2(f,b,g,s) ==   \
-\	   if(f`g ~= 0, {uu(f,b,g,LEAST d. uu(f,b,g,d) ~= 0)`s}, 0)"
+\	   if(f`g ~= 0, {uu(f, b, g, LEAST d. uu(f,b,g,d) ~= 0)`s}, 0)"
 
   ww2_def "ww2(f,b,g,s) == f`g - vv2(f,b,g,s)"
 
+  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))"
+  
 end