:: Curried and Uncurried Functions :: by Grzegorz Bancerek :: :: Received March 6, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin scheme :: FUNCT_5:sch 1 LambdaFS{ F1() -> set , F2( set ) -> set } : ex f being Function st ( dom f = F1() & ( for g being Function st g in F1() holds f . g = F2(g) ) ) proofend; theorem Th1: :: FUNCT_5:1 ~ {} = {} proofend; theorem :: FUNCT_5:2 canceled; theorem :: FUNCT_5:3 canceled; theorem :: FUNCT_5:4 canceled; theorem :: FUNCT_5:5 canceled; theorem :: FUNCT_5:6 canceled; theorem :: FUNCT_5:7 canceled; theorem Th8: :: FUNCT_5:8 ( proj1 {} = {} & proj2 {} = {} ) ; theorem Th9: :: FUNCT_5:9 for Y, X being set st ( Y <> {} or [:X,Y:] <> {} or [:Y,X:] <> {} ) holds ( proj1 [:X,Y:] = X & proj2 [:Y,X:] = X ) proofend; theorem Th10: :: FUNCT_5:10 for X, Y being set holds ( proj1 [:X,Y:] c= X & proj2 [:X,Y:] c= Y ) proofend; theorem Th11: :: FUNCT_5:11 for Z, X, Y being set st Z c= [:X,Y:] holds ( proj1 Z c= X & proj2 Z c= Y ) proofend; theorem Th12: :: FUNCT_5:12 for x, y being set holds ( proj1 {[x,y]} = {x} & proj2 {[x,y]} = {y} ) proofend; theorem :: FUNCT_5:13 for x, y, z, t being set holds ( proj1 {[x,y],[z,t]} = {x,z} & proj2 {[x,y],[z,t]} = {y,t} ) proofend; theorem Th14: :: FUNCT_5:14 for X being set st ( for x, y being set holds not [x,y] in X ) holds ( proj1 X = {} & proj2 X = {} ) proofend; theorem :: FUNCT_5:15 for X being set st ( proj1 X = {} or proj2 X = {} ) holds for x, y being set holds not [x,y] in X by XTUPLE_0:def_12, XTUPLE_0:def_13; theorem :: FUNCT_5:16 for X being set holds ( proj1 X = {} iff proj2 X = {} ) proofend; theorem Th17: :: FUNCT_5:17 for f being Function holds ( proj1 (dom f) = proj2 (dom (~ f)) & proj2 (dom f) = proj1 (dom (~ f)) ) proofend; theorem :: FUNCT_5:18 for f being Relation holds ( proj1 f = dom f & proj2 f = rng f ) ; definition let f be Function; func curry f -> Function means :Def1: :: FUNCT_5:def 1 ( dom it = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds ex g being Function st ( it . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds g . y = f . (x,y) ) ) ) ); existence ex b1 being Function st ( dom b1 = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds ex g being Function st ( b1 . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds g . y = f . (x,y) ) ) ) ) proofend; uniqueness for b1, b2 being Function st dom b1 = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds ex g being Function st ( b1 . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds g . y = f . (x,y) ) ) ) & dom b2 = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds ex g being Function st ( b2 . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds g . y = f . (x,y) ) ) ) holds b1 = b2 proofend; func uncurry f -> Function means :Def2: :: FUNCT_5:def 2 ( ( for t being set holds ( t in dom it iff ex x being set ex g being Function ex y being set st ( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being set for g being Function st x in dom it & g = f . (x `1) holds it . x = g . (x `2) ) ); existence ex b1 being Function st ( ( for t being set holds ( t in dom b1 iff ex x being set ex g being Function ex y being set st ( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being set for g being Function st x in dom b1 & g = f . (x `1) holds b1 . x = g . (x `2) ) ) proofend; uniqueness for b1, b2 being Function st ( for t being set holds ( t in dom b1 iff ex x being set ex g being Function ex y being set st ( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being set for g being Function st x in dom b1 & g = f . (x `1) holds b1 . x = g . (x `2) ) & ( for t being set holds ( t in dom b2 iff ex x being set ex g being Function ex y being set st ( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being set for g being Function st x in dom b2 & g = f . (x `1) holds b2 . x = g . (x `2) ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines curry FUNCT_5:def_1_:_ for f, b2 being Function holds ( b2 = curry f iff ( dom b2 = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds ex g being Function st ( b2 . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds g . y = f . (x,y) ) ) ) ) ); :: deftheorem Def2 defines uncurry FUNCT_5:def_2_:_ for f, b2 being Function holds ( b2 = uncurry f iff ( ( for t being set holds ( t in dom b2 iff ex x being set ex g being Function ex y being set st ( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being set for g being Function st x in dom b2 & g = f . (x `1) holds b2 . x = g . (x `2) ) ) ); definition let f be Function; func curry' f -> Function equals :: FUNCT_5:def 3 curry (~ f); correctness coherence curry (~ f) is Function; ; func uncurry' f -> Function equals :: FUNCT_5:def 4 ~ (uncurry f); correctness coherence ~ (uncurry f) is Function; ; end; :: deftheorem defines curry' FUNCT_5:def_3_:_ for f being Function holds curry' f = curry (~ f); :: deftheorem defines uncurry' FUNCT_5:def_4_:_ for f being Function holds uncurry' f = ~ (uncurry f); theorem Th19: :: FUNCT_5:19 for x, y being set for f being Function st [x,y] in dom f holds ( x in dom (curry f) & (curry f) . x is Function ) proofend; theorem Th20: :: FUNCT_5:20 for x, y being set for f, g being Function st [x,y] in dom f & g = (curry f) . x holds ( y in dom g & g . y = f . (x,y) ) proofend; theorem :: FUNCT_5:21 for x, y being set for f being Function st [x,y] in dom f holds ( y in dom (curry' f) & (curry' f) . y is Function ) proofend; theorem Th22: :: FUNCT_5:22 for x, y being set for f, g being Function st [x,y] in dom f & g = (curry' f) . y holds ( x in dom g & g . x = f . (x,y) ) proofend; theorem :: FUNCT_5:23 for f being Function holds dom (curry' f) = proj2 (dom f) proofend; theorem Th24: :: FUNCT_5:24 for X, Y being set for f being Function st [:X,Y:] <> {} & dom f = [:X,Y:] holds ( dom (curry f) = X & dom (curry' f) = Y ) proofend; theorem Th25: :: FUNCT_5:25 for X, Y being set for f being Function st dom f c= [:X,Y:] holds ( dom (curry f) c= X & dom (curry' f) c= Y ) proofend; theorem Th26: :: FUNCT_5:26 for X, Y being set for f being Function st rng f c= Funcs (X,Y) holds ( dom (uncurry f) = [:(dom f),X:] & dom (uncurry' f) = [:X,(dom f):] ) proofend; theorem :: FUNCT_5:27 for f being Function st ( for x, y being set holds not [x,y] in dom f ) holds ( curry f = {} & curry' f = {} ) proofend; theorem :: FUNCT_5:28 for f being Function st ( for x being set holds ( not x in dom f or not f . x is Function ) ) holds ( uncurry f = {} & uncurry' f = {} ) proofend; theorem Th29: :: FUNCT_5:29 for X, Y, x being set for f being Function st [:X,Y:] <> {} & dom f = [:X,Y:] & x in X holds ex g being Function st ( (curry f) . x = g & dom g = Y & rng g c= rng f & ( for y being set st y in Y holds g . y = f . (x,y) ) ) proofend; theorem Th30: :: FUNCT_5:30 for x being set for f being Function st x in dom (curry f) holds (curry f) . x is Function proofend; theorem Th31: :: FUNCT_5:31 for x being set for f, g being Function st x in dom (curry f) & g = (curry f) . x holds ( dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & dom g c= proj2 (dom f) & rng g c= rng f & ( for y being set st y in dom g holds ( g . y = f . (x,y) & [x,y] in dom f ) ) ) proofend; theorem Th32: :: FUNCT_5:32 for X, Y, y being set for f being Function st [:X,Y:] <> {} & dom f = [:X,Y:] & y in Y holds ex g being Function st ( (curry' f) . y = g & dom g = X & rng g c= rng f & ( for x being set st x in X holds g . x = f . (x,y) ) ) proofend; theorem :: FUNCT_5:33 for x being set for f being Function st x in dom (curry' f) holds (curry' f) . x is Function by Th30; theorem :: FUNCT_5:34 for x being set for f, g being Function st x in dom (curry' f) & g = (curry' f) . x holds ( dom g = proj1 ((dom f) /\ [:(proj1 (dom f)),{x}:]) & dom g c= proj1 (dom f) & rng g c= rng f & ( for y being set st y in dom g holds ( g . y = f . (y,x) & [y,x] in dom f ) ) ) proofend; theorem Th35: :: FUNCT_5:35 for X, Y being set for f being Function st dom f = [:X,Y:] holds ( rng (curry f) c= Funcs (Y,(rng f)) & rng (curry' f) c= Funcs (X,(rng f)) ) proofend; theorem :: FUNCT_5:36 for f being Function holds ( rng (curry f) c= PFuncs ((proj2 (dom f)),(rng f)) & rng (curry' f) c= PFuncs ((proj1 (dom f)),(rng f)) ) proofend; theorem Th37: :: FUNCT_5:37 for X, Y being set for f being Function st rng f c= PFuncs (X,Y) holds ( dom (uncurry f) c= [:(dom f),X:] & dom (uncurry' f) c= [:X,(dom f):] ) proofend; theorem Th38: :: FUNCT_5:38 for x, y being set for f, g being Function st x in dom f & g = f . x & y in dom g holds ( [x,y] in dom (uncurry f) & (uncurry f) . (x,y) = g . y & g . y in rng (uncurry f) ) proofend; theorem :: FUNCT_5:39 for x, y being set for f, g being Function st x in dom f & g = f . x & y in dom g holds ( [y,x] in dom (uncurry' f) & (uncurry' f) . (y,x) = g . y & g . y in rng (uncurry' f) ) proofend; theorem Th40: :: FUNCT_5:40 for X, Y being set for f being Function st rng f c= PFuncs (X,Y) holds ( rng (uncurry f) c= Y & rng (uncurry' f) c= Y ) proofend; theorem Th41: :: FUNCT_5:41 for X, Y being set for f being Function st rng f c= Funcs (X,Y) holds ( rng (uncurry f) c= Y & rng (uncurry' f) c= Y ) proofend; theorem Th42: :: FUNCT_5:42 ( curry {} = {} & curry' {} = {} ) proofend; theorem Th43: :: FUNCT_5:43 ( uncurry {} = {} & uncurry' {} = {} ) proofend; theorem Th44: :: FUNCT_5:44 for X, Y being set for f1, f2 being Function st dom f1 = [:X,Y:] & dom f2 = [:X,Y:] & curry f1 = curry f2 holds f1 = f2 proofend; theorem Th45: :: FUNCT_5:45 for X, Y being set for f1, f2 being Function st dom f1 = [:X,Y:] & dom f2 = [:X,Y:] & curry' f1 = curry' f2 holds f1 = f2 proofend; theorem Th46: :: FUNCT_5:46 for X, Y being set for f1, f2 being Function st rng f1 c= Funcs (X,Y) & rng f2 c= Funcs (X,Y) & X <> {} & uncurry f1 = uncurry f2 holds f1 = f2 proofend; theorem :: FUNCT_5:47 for X, Y being set for f1, f2 being Function st rng f1 c= Funcs (X,Y) & rng f2 c= Funcs (X,Y) & X <> {} & uncurry' f1 = uncurry' f2 holds f1 = f2 proofend; theorem Th48: :: FUNCT_5:48 for X, Y being set for f being Function st rng f c= Funcs (X,Y) & X <> {} holds ( curry (uncurry f) = f & curry' (uncurry' f) = f ) proofend; theorem :: FUNCT_5:49 for X, Y being set for f being Function st dom f = [:X,Y:] holds ( uncurry (curry f) = f & uncurry' (curry' f) = f ) proofend; theorem Th50: :: FUNCT_5:50 for X, Y being set for f being Function st dom f c= [:X,Y:] holds ( uncurry (curry f) = f & uncurry' (curry' f) = f ) proofend; theorem Th51: :: FUNCT_5:51 for X, Y being set for f being Function st rng f c= PFuncs (X,Y) & not {} in rng f holds ( curry (uncurry f) = f & curry' (uncurry' f) = f ) proofend; theorem :: FUNCT_5:52 for X, Y being set for f1, f2 being Function st dom f1 c= [:X,Y:] & dom f2 c= [:X,Y:] & curry f1 = curry f2 holds f1 = f2 proofend; theorem :: FUNCT_5:53 for X, Y being set for f1, f2 being Function st dom f1 c= [:X,Y:] & dom f2 c= [:X,Y:] & curry' f1 = curry' f2 holds f1 = f2 proofend; theorem :: FUNCT_5:54 for X, Y being set for f1, f2 being Function st rng f1 c= PFuncs (X,Y) & rng f2 c= PFuncs (X,Y) & not {} in rng f1 & not {} in rng f2 & uncurry f1 = uncurry f2 holds f1 = f2 proofend; theorem :: FUNCT_5:55 for X, Y being set for f1, f2 being Function st rng f1 c= PFuncs (X,Y) & rng f2 c= PFuncs (X,Y) & not {} in rng f1 & not {} in rng f2 & uncurry' f1 = uncurry' f2 holds f1 = f2 proofend; theorem Th56: :: FUNCT_5:56 for X, Y, Z being set st X c= Y holds Funcs (Z,X) c= Funcs (Z,Y) proofend; theorem Th57: :: FUNCT_5:57 for X being set holds Funcs ({},X) = {{}} proofend; theorem :: FUNCT_5:58 for X, x being set holds ( X, Funcs ({x},X) are_equipotent & card X = card (Funcs ({x},X)) ) proofend; theorem Th59: :: FUNCT_5:59 for X, x being set holds Funcs (X,{x}) = {(X --> x)} proofend; theorem Th60: :: FUNCT_5:60 for X1, Y1, X2, Y2 being set st X1,Y1 are_equipotent & X2,Y2 are_equipotent holds ( Funcs (X1,X2), Funcs (Y1,Y2) are_equipotent & card (Funcs (X1,X2)) = card (Funcs (Y1,Y2)) ) proofend; theorem :: FUNCT_5:61 for X1, Y1, X2, Y2 being set st card X1 = card Y1 & card X2 = card Y2 holds card (Funcs (X1,X2)) = card (Funcs (Y1,Y2)) proofend; theorem :: FUNCT_5:62 for X1, X2, X being set st X1 misses X2 holds ( Funcs ((X1 \/ X2),X),[:(Funcs (X1,X)),(Funcs (X2,X)):] are_equipotent & card (Funcs ((X1 \/ X2),X)) = card [:(Funcs (X1,X)),(Funcs (X2,X)):] ) proofend; theorem :: FUNCT_5:63 for X, Y, Z being set holds ( Funcs ([:X,Y:],Z), Funcs (X,(Funcs (Y,Z))) are_equipotent & card (Funcs ([:X,Y:],Z)) = card (Funcs (X,(Funcs (Y,Z)))) ) proofend; theorem :: FUNCT_5:64 for Z, X, Y being set holds ( Funcs (Z,[:X,Y:]),[:(Funcs (Z,X)),(Funcs (Z,Y)):] are_equipotent & card (Funcs (Z,[:X,Y:])) = card [:(Funcs (Z,X)),(Funcs (Z,Y)):] ) proofend; theorem :: FUNCT_5:65 for x, y, X being set st x <> y holds ( Funcs (X,{x,y}), bool X are_equipotent & card (Funcs (X,{x,y})) = card (bool X) ) proofend; theorem :: FUNCT_5:66 for x, y, X being set st x <> y holds ( Funcs ({x,y},X),[:X,X:] are_equipotent & card (Funcs ({x,y},X)) = card [:X,X:] ) proofend; begin notation synonym op0 for 0 ; end; definition :: original:op0 redefine func op0 -> Element of 1; coherence op0 is Element of 1 by CARD_1:49, TARSKI:def_1; end; definition func op1 -> set equals :: FUNCT_5:def 5 0 .--> 0; coherence 0 .--> 0 is set ; func op2 -> set equals :: FUNCT_5:def 6 (0,0) :-> 0; coherence (0,0) :-> 0 is set ; end; :: deftheorem defines op1 FUNCT_5:def_5_:_ op1 = 0 .--> 0; :: deftheorem defines op2 FUNCT_5:def_6_:_ op2 = (0,0) :-> 0; definition :: original:op1 redefine func op1 -> UnOp of 1; coherence op1 is UnOp of 1 by CARD_1:49; :: original:op2 redefine func op2 -> BinOp of 1; coherence op2 is BinOp of 1 by CARD_1:49; end; definition let D be non empty set ; let X be set ; let E be non empty set ; let F be FUNCTION_DOMAIN of X,E; let f be Function of D,F; let d be Element of D; :: original:. redefine funcf . d -> Element of F; coherence f . d is Element of F proofend; end; theorem Th1: :: FUNCT_5:67 for C, D, E being non empty set for f being Function of [:C,D:],E holds curry f is Function of C,(Funcs (D,E)) proofend; theorem Th2: :: FUNCT_5:68 for D, C, E being non empty set for f being Function of [:C,D:],E holds curry' f is Function of D,(Funcs (C,E)) proofend; definition let C, D, E be non empty set ; let f be Function of [:C,D:],E; :: original:curry redefine func curry f -> Function of C,(Funcs (D,E)); coherence curry f is Function of C,(Funcs (D,E)) by Th1; :: original:curry' redefine func curry' f -> Function of D,(Funcs (C,E)); coherence curry' f is Function of D,(Funcs (C,E)) by Th2; end; theorem :: FUNCT_5:69 for C, D, E being non empty set for c being Element of C for d being Element of D for f being Function of [:C,D:],E holds f . (c,d) = ((curry f) . c) . d proofend; theorem :: FUNCT_5:70 for C, D, E being non empty set for c being Element of C for d being Element of D for f being Function of [:C,D:],E holds f . (c,d) = ((curry' f) . d) . c proofend; :: from ISOCAT_2, 2011.11.25, A.T. definition let A, B, C be non empty set ; let f be Function of A,(Funcs (B,C)); :: original:uncurry redefine func uncurry f -> Function of [:A,B:],C; coherence uncurry f is Function of [:A,B:],C proofend; end; theorem :: FUNCT_5:71 for A, B, C being non empty set for f being Function of A,(Funcs (B,C)) holds curry (uncurry f) = f proofend; theorem :: FUNCT_5:72 for A, B, C being non empty set for f being Function of A,(Funcs (B,C)) for a being Element of A for b being Element of B holds (uncurry f) . (a,b) = (f . a) . b proofend;