:: Curried and Uncurried Functions
::  by Grzegorz Bancerek
::
:: Received March 6, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies FUNCT_1, RELAT_1, XBOOLE_0, ZFMISC_1, TARSKI, SUBSET_1, MCART_1,
      FUNCT_2, PARTFUN1, CARD_1, FUNCOP_1, FUNCT_4, BINOP_1, FUNCT_5;
 notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, FUNCT_1,
      DOMAIN_1, WELLORD2, ORDINAL1, RELSET_1, FUNCT_2, MCART_1, BINOP_1,
      PARTFUN1, FUNCT_3, CARD_1, FUNCOP_1, FUNCT_4;
 constructors PARTFUN1, WELLORD2, BINOP_1, FUNCT_3, FUNCOP_1, FUNCT_4, CARD_1,
      RELSET_1, DOMAIN_1, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, XTUPLE_0;
 requirements SUBSET, BOOLE;


begin

reserve X,Y,Z,X1,X2,Y1,Y2 for set, x,y,z,t,x1,x2 for object,
  f,g,h,f1,f2,g1,g2 for Function;

scheme :: FUNCT_5:sch 1
  LambdaFS { FS()->set, f(object)-> object }:
 ex f st dom f = FS() & for g st g in FS () holds f.g = f(g);

theorem :: FUNCT_5:1
  ~{} = {};

::$CT 6

theorem :: FUNCT_5:8
  proj1 {} = {} & proj2 {} = {};

theorem :: FUNCT_5:9
  Y <> {} or [:X,Y:] <> {} or [:Y,X:] <> {} implies proj1 [:X,Y:]
  = X & proj2 [:Y,X:] = X;

theorem :: FUNCT_5:10
  proj1 [:X,Y:] c= X & proj2 [:X,Y:] c= Y;

theorem :: FUNCT_5:11
  Z c= [:X,Y:] implies proj1 Z c= X & proj2 Z c= Y;

theorem :: FUNCT_5:12
  proj1 {[x,y]} = {x} & proj2 {[x,y]} = {y};

theorem :: FUNCT_5:13
  proj1 {[x,y],[z,t]} = {x,z} & proj2 {[x,y],[z,t]} = {y,t};

theorem :: FUNCT_5:14
  not (ex x,y being object st [x,y] in X)
    implies proj1 X = {} & proj2 X = {};

theorem :: FUNCT_5:15
  proj1 X = {} or proj2 X = {} implies
   not ex x,y being object st [x,y] in X;

theorem :: FUNCT_5:16
  proj1 X = {} iff proj2 X = {};

theorem :: FUNCT_5:17
  proj1 dom f = proj2 dom ~f & proj2 dom f = proj1 dom ~f;

definition
  let f;
  func curry f -> Function means
:: FUNCT_5:def 1

  dom it = proj1 dom f & for x being object st x in
  proj1 dom f ex g st it.x = g & dom g = proj2 (dom f /\ [:{x},proj2 dom f:]) &
  for y st y in dom g holds g.y = f.(x,y);
  func uncurry f -> Function means
:: FUNCT_5:def 2

  (for t being object holds t in dom it iff ex x,g
,y st t = [x,y] & x in dom f & g = f.x & y in dom g) & for x,g st x in dom it &
  g = f.x`1 holds it.x = g.x`2;
end;

definition
  let f;
  func curry' f -> Function equals
:: FUNCT_5:def 3
  curry ~f;
  func uncurry' f -> Function equals
:: FUNCT_5:def 4
  ~(uncurry f);
end;

::$CT

registration let f;
 cluster curry f -> Function-yielding;
end;

theorem :: FUNCT_5:19
 for x,y being object holds
  [x,y] in dom f implies x in dom curry f;

theorem :: FUNCT_5:20
 for x,y being object holds
  [x,y] in dom f & g = (curry f).x implies y in dom g & g.y = f.(x ,y);

registration let f;
 cluster curry' f -> Function-yielding;
end;

theorem :: FUNCT_5:21
 for x,y being object holds
  [x,y] in dom f implies y in dom curry' f;

theorem :: FUNCT_5:22
 for x,y being object holds
  [x,y] in dom f & g = (curry' f).y implies x in dom g & g.x = f.(x,y);

theorem :: FUNCT_5:23
  dom curry' f = proj2 dom f;

theorem :: FUNCT_5:24
  [:X,Y:] <> {} & dom f = [:X,Y:] implies dom curry f = X & dom curry' f = Y;

theorem :: FUNCT_5:25
  dom f c= [:X,Y:] implies dom curry f c= X & dom curry' f c= Y;

theorem :: FUNCT_5:26
  rng f c= Funcs(X,Y) implies dom uncurry f = [:dom f,X:] & dom
  uncurry' f = [:X,dom f:];

theorem :: FUNCT_5:27
  not (ex x,y being object st [x,y] in dom f)
   implies curry f = {} & curry' f = {};

theorem :: FUNCT_5:28
  not (ex x st x in dom f & f.x is Function) implies uncurry f = {} &
  uncurry' f = {};

theorem :: FUNCT_5:29
  [:X,Y:] <> {} & dom f = [:X,Y:] & x in X implies ex g st (curry
  f).x = g & dom g = Y & rng g c= rng f & for y st y in Y holds g.y = f.(x,y);

theorem :: FUNCT_5:30
  x in dom curry f implies (curry f).x is Function;

theorem :: FUNCT_5:31
  x in dom curry f & g = (curry f).x implies dom g = proj2 (dom f
/\ [:{x},proj2 dom f:]) & dom g c= proj2 dom f & rng g c= rng f & for y st y in
  dom g holds g.y = f.(x,y) & [x,y] in dom f;

theorem :: FUNCT_5:32
  [:X,Y:] <> {} & dom f = [:X,Y:] & y in Y implies ex g st (curry'
  f).y = g & dom g = X & rng g c= rng f & for x st x in X holds g.x = f.(x,y);

theorem :: FUNCT_5:33
  x in dom curry' f implies (curry' f).x is Function;

theorem :: FUNCT_5:34
  x in dom curry' f & g = (curry' f).x implies dom g = proj1 (dom f /\
  [:proj1 dom f,{x}:]) & dom g c= proj1 dom f & rng g c= rng f & for y st y in
  dom g holds g.y = f.(y,x) & [y,x] in dom f;

theorem :: FUNCT_5:35
  dom f = [:X,Y:] implies rng curry f c= Funcs(Y,rng f) & rng
  curry' f c= Funcs(X,rng f);

theorem :: FUNCT_5:36
  rng curry f c= PFuncs(proj2 dom f,rng f) & rng curry' f c= PFuncs(
  proj1 dom f,rng f);

theorem :: FUNCT_5:37
  rng f c= PFuncs(X,Y) implies dom uncurry f c= [:dom f,X:] & dom
  uncurry' f c= [:X,dom f:];

theorem :: FUNCT_5:38
  x in dom f & g = f.x & y in dom g implies [x,y] in dom uncurry f
  & (uncurry f).(x,y) = g.y & g.y in rng uncurry f;

theorem :: FUNCT_5:39
  x in dom f & g = f.x & y in dom g implies [y,x] in dom uncurry' f & (
  uncurry' f).(y,x) = g.y & g.y in rng uncurry' f;

theorem :: FUNCT_5:40
  rng f c= PFuncs(X,Y) implies rng uncurry f c= Y & rng uncurry' f c= Y;

theorem :: FUNCT_5:41
  rng f c= Funcs(X,Y) implies rng uncurry f c= Y & rng uncurry' f c= Y;

theorem :: FUNCT_5:42
  curry {} = {} & curry' {} = {};

theorem :: FUNCT_5:43
  uncurry {} = {} & uncurry' {} = {};

theorem :: FUNCT_5:44
  dom f1 = [:X,Y:] & dom f2 = [:X,Y:] & curry f1 = curry f2 implies f1 = f2;

theorem :: FUNCT_5:45
  dom f1 = [:X,Y:] & dom f2 = [:X,Y:] & curry' f1 = curry' f2 implies f1 = f2;

theorem :: FUNCT_5:46
  rng f1 c= Funcs(X,Y) & rng f2 c= Funcs(X,Y) & X <> {} & uncurry
  f1 = uncurry f2 implies f1 = f2;

theorem :: FUNCT_5:47
  rng f1 c= Funcs(X,Y) & rng f2 c= Funcs(X,Y) & X <> {} & uncurry' f1 =
  uncurry' f2 implies f1 = f2;

theorem :: FUNCT_5:48
  rng f c= Funcs(X,Y) & X <> {} implies curry uncurry f = f &
  curry' uncurry' f = f;

theorem :: FUNCT_5:49
  dom f = [:X,Y:] implies uncurry curry f = f & uncurry' curry' f = f;

theorem :: FUNCT_5:50
  dom f c= [:X,Y:] implies uncurry curry f = f & uncurry' curry' f = f;

theorem :: FUNCT_5:51
  rng f c= PFuncs(X,Y) & not {} in rng f implies curry uncurry f =
  f & curry' uncurry' f = f;

theorem :: FUNCT_5:52
  dom f1 c= [:X,Y:] & dom f2 c= [:X,Y:] & curry f1 = curry f2 implies f1 = f2;

theorem :: FUNCT_5:53
  dom f1 c= [:X,Y:] & dom f2 c= [:X,Y:] & curry' f1 = curry' f2 implies f1 = f2
;

theorem :: FUNCT_5:54
  rng f1 c= PFuncs(X,Y) & rng f2 c= PFuncs(X,Y) & not {} in rng f1 & not
  {} in rng f2 & uncurry f1 = uncurry f2 implies f1 = f2;

theorem :: FUNCT_5:55
  rng f1 c= PFuncs(X,Y) & rng f2 c= PFuncs(X,Y) & not {} in rng f1 & not
  {} in rng f2 & uncurry' f1 = uncurry' f2 implies f1 = f2;

theorem :: FUNCT_5:56
  X c= Y implies Funcs(Z,X) c= Funcs(Z,Y);

theorem :: FUNCT_5:57
  Funcs({},X) = {{}};

theorem :: FUNCT_5:58
 for x being object holds
  X,Funcs({x},X) are_equipotent & card X = card Funcs({x},X);

theorem :: FUNCT_5:59
  Funcs(X,{x}) = {X --> x};

theorem :: FUNCT_5:60
  X1,Y1 are_equipotent & X2,Y2 are_equipotent implies Funcs(X1,X2)
  ,Funcs(Y1,Y2) are_equipotent & card Funcs(X1,X2) = card Funcs(Y1,Y2);

theorem :: FUNCT_5:61
  card X1 = card Y1 & card X2 = card Y2 implies card Funcs(X1,X2) = card
  Funcs(Y1,Y2);

theorem :: FUNCT_5:62
  X1 misses X2 implies Funcs(X1 \/ X2,X),[:Funcs(X1,X),Funcs(X2,X):]
  are_equipotent & card Funcs(X1 \/ X2,X) = card [:Funcs(X1,X),Funcs(X2,X):];

theorem :: FUNCT_5:63
  Funcs([:X,Y:],Z),Funcs(X,Funcs(Y,Z)) are_equipotent & card Funcs([:X,Y
  :],Z) = card Funcs(X,Funcs(Y,Z));

theorem :: FUNCT_5:64
  Funcs(Z,[:X,Y:]),[:Funcs(Z,X),Funcs(Z,Y):] are_equipotent & card Funcs
  (Z,[:X,Y:]) = card [:Funcs(Z,X),Funcs(Z,Y):];

theorem :: FUNCT_5:65
  x <> y implies Funcs(X,{x,y}),bool X are_equipotent & card Funcs(X,{x,
  y}) = card bool X;

theorem :: FUNCT_5:66
  x <> y implies Funcs({x,y},X),[:X,X:] are_equipotent & card Funcs({x,y
  },X) = card [:X,X:];

begin :: Addenda
:: from VECTSP_2, MIDSP_1, 2007.11.26, A.T.

notation
  synonym op0 for 0;
end;

definition
  redefine func op0 -> Element of {0};
end;

definition
  func op1 -> set equals
:: FUNCT_5:def 5
  0 .--> 0;
  func op2 -> set equals
:: FUNCT_5:def 6
  (0,0) :-> 0;
end;

definition
  redefine func op1 -> UnOp of {0};
  redefine func op2 -> BinOp of {0};
end;

:: from CAT_2, 2011.11.25, A.T.

reserve C,D,E for non empty set;
reserve c for Element of C,
  d for Element of D;

definition
  let D,X,E;
  let F be FUNCTION_DOMAIN of X,E;
  let f be Function of D,F;
  let d be Element of D;
  redefine func f.d -> Element of F;
end;

reserve f for Function of [:C,D:],E;

theorem :: FUNCT_5:67
  curry f is Function of C,Funcs(D,E);

theorem :: FUNCT_5:68
  curry' f is Function of D,Funcs(C,E);

definition
  let C,D,E,f;
  redefine func curry f -> Function of C,Funcs(D,E);
  redefine func curry' f -> Function of D,Funcs(C,E);
end;

theorem :: FUNCT_5:69
  f.(c,d) = ((curry f).c).d;

theorem :: FUNCT_5:70
  f.(c,d) = ((curry' f).d).c;

:: 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);
  redefine func uncurry f -> Function of [:A,B:],C;
end;

theorem :: FUNCT_5:71
  for A,B,C being non empty set, f being Function of A,Funcs(B,C)
  holds curry uncurry f = f;

theorem :: FUNCT_5:72
  for A,B,C being non empty set, f being Function of A, Funcs(B,C)
for a being Element of A, b being Element of B
      holds (uncurry f).(a,b) = f.a.b;