:: The Formal Construction of Fuzzy Numbers
::  by Adam Grabowski
::
:: Received December 31, 2014
:: Copyright (c) 2014-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 NUMBERS, XBOOLE_0, SUBSET_1, XXREAL_1, CARD_1, RELAT_1, TARSKI,
      FUNCT_1, XXREAL_0, PARTFUN1, ARYTM_1, ARYTM_3, COMPLEX1, FUZZY_1,
      GRAPH_2, MEASURE5, MSALIMIT, FUZNUM_1, REAL_1, ORDINAL2, XXREAL_2,
      TREES_1, RCOMP_1, ZFMISC_1, NUMPOLY1, JGRAPH_2, FUNCT_4, PRE_TOPC,
      FCONT_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XXREAL_0, XCMPLX_0, XXREAL_2,
      COMPLEX1, XREAL_0, FUNCT_1, PARTFUN1, FCONT_1, RELSET_1, FUNCT_4,
      RCOMP_1, MEASURE5, FUZZY_1;
 constructors COMPLEX1, RFUNCT_1, INTEGRA1, SEQ_4, RELSET_1, FUZZY_1, FCONT_1,
      FUNCT_4;
 registrations RELSET_1, NUMBERS, XXREAL_0, MEMBERED, XBOOLE_0, VALUED_0,
      FUNCT_2, XREAL_0, ORDINAL1, FCONT_1, RELAT_1, TOPREALB, FUNCT_4, FUNCT_1,
      XCMPLX_0, NAT_1, RCOMP_1;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;


begin :: Preliminaries: Affine Maps

theorem :: FUZNUM_1:1
  for a,b being Real st a <= b holds
    REAL \ ].a,b.[ <> {};

 reserve a,b,c,x for Real;

theorem :: FUZNUM_1:2
  AffineMap (1/(b-a),-a/(b-a)).a = 0;

theorem :: FUZNUM_1:3
  b - a <> 0 implies
    AffineMap (1/(b-a),-a/(b-a)).b = 1;

theorem :: FUZNUM_1:4
  c - b <> 0 implies
    AffineMap (-1/(c-b),c/(c-b)).b = 1;

theorem :: FUZNUM_1:5
  AffineMap (-1/(c-b),c/(c-b)).c = 0;

theorem :: FUZNUM_1:6
  b - a <> 0 & AffineMap (1/(b-a),-a/(b-a)).x = 1 implies
    x = b;

theorem :: FUZNUM_1:7
  c - b <> 0 & AffineMap (-1/(c-b),c/(c-b)).x = 1 implies
    x = b;

theorem :: FUZNUM_1:8
  rng AffineMap (0,a) = {a};

theorem :: FUZNUM_1:9
  for C being non empty Subset of REAL holds
    rng (AffineMap (0,a) | C) = {a};

theorem :: FUZNUM_1:10
  b - a > 0 implies
    rng ((AffineMap (1/(b-a),-a/(b-a)) | [.a,b.])) = [.0,1.];

theorem :: FUZNUM_1:11
  c - b > 0 implies
    rng ((AffineMap (-1/(c-b),c/(c-b)) | ].b,c.])) = [.0,1.[;

theorem :: FUZNUM_1:12
  c - b > 0 implies
    rng ((AffineMap (-1/(c-b),c/(c-b)) | [.b,c.])) = [.0,1.];

theorem :: FUZNUM_1:13
  (AffineMap (0,0)).x <> 1;

theorem :: FUZNUM_1:14
  AffineMap (0,1).b = 1;

theorem :: FUZNUM_1:15
  for a being Real holds AffineMap (0,b).a = b;

begin :: Towards Development of Fuzzy Numbers

 reserve C for non empty set;

definition let C be non empty set;
  mode FuzzySet of C is Membership_Func of C;
end;

definition let C be non empty set;
           let F be FuzzySet of C;
  attr F is normalized means
:: FUZNUM_1:def 1
    ex x being Element of C st
      F.x = 1;
end;

notation let C be non empty set;
         let F be FuzzySet of C;
  synonym F is normal for F is normalized;
end;

notation let C be non empty set;
         let F be FuzzySet of C;
  antonym F is subnormal for F is normal;
end;

definition let C be non empty set;
           let F be FuzzySet of C;
  attr F is strictly-normalized means
:: FUZNUM_1:def 2
    ex x being Element of C st
      F.x = 1 &
      for y being Element of C st F.y = 1 holds y = x;
end;

registration let C be non empty set;
  cluster strictly-normalized -> normalized for FuzzySet of C;
end;

definition let C be non empty set;
           let F be FuzzySet of C;
           let alpha be Real;
  func alpha-cut F -> Subset of C equals
:: FUZNUM_1:def 3
    { x where x is Element of C : F.x >= alpha };
end;

theorem :: FUZNUM_1:16
  for F being FuzzySet of C,
      alpha being Real holds
    alpha-cut F = F " ([. alpha, 1 .]);

registration let C;
  cluster UMF C -> normalized;
end;

registration let C;
  cluster normalized for FuzzySet of C;
end;

definition let C;
           let F be FuzzySet of C;
  func Core F -> Subset of C equals
:: FUZNUM_1:def 4
    { x where x is Element of C : F.x = 1 };
end;

theorem :: FUZNUM_1:17
  Core UMF C = C;

theorem :: FUZNUM_1:18
  Core EMF C = {};

registration let C;
  cluster Core EMF C -> empty;
end;

theorem :: FUZNUM_1:19
  for F being FuzzySet of C holds
    Core F = F " {1};

theorem :: FUZNUM_1:20
  for F being FuzzySet of C holds
    Core F = 1-cut F;

begin :: Convexity and the Height of a Fuzzy Set

definition let F be FuzzySet of REAL;
  attr F is f-convex means
:: FUZNUM_1:def 5
    for x1, x2 being Real,
        l being Real st 0 <= l & l <= 1 holds
      F.(l*x1 + (1-l)*x2) >= min(F.x1,F.x2);
end;

registration
  cluster UMF REAL -> f-convex;
  cluster EMF REAL -> f-convex;
end;

definition let C be non empty set;
           let F be FuzzySet of C;
  func height F -> ExtReal equals
:: FUZNUM_1:def 6
    sup rng F;
end;

theorem :: FUZNUM_1:21
  for F being FuzzySet of C holds
    0 <= height F & height F <= 1;

theorem :: FUZNUM_1:22
  for F being FuzzySet of C st
    F is normalized holds height F = 1;

begin :: Pasting aka Glueing Lemmas

theorem :: FUZNUM_1:23
  for f,g being PartFunc of REAL, REAL st
  f is continuous & g is continuous &
  ex x being object st dom f /\ dom g = {x} &
  for x being object st x in dom f /\ dom g holds f.x = g.x holds
    ex h being PartFunc of REAL, REAL st
    h = f +* g & for x being Real st
    x in dom f /\ dom g holds h is_continuous_in x;

theorem :: FUZNUM_1:24
  for f,g being PartFunc of REAL, REAL st
  f is continuous non empty & g is continuous non empty &
  (ex a,b,c being Real st dom f = [.a,b.] & dom g = [.b,c.]) &
  f tolerates g
    ex h being PartFunc of REAL, REAL st
    h = f +* g & for x being Real st x in dom h holds h is_continuous_in x;

theorem :: FUZNUM_1:25
  for f,g being PartFunc of REAL, REAL st
    f is continuous non empty &
    g is continuous non empty &
    (ex a,b,c being Real st dom f = [.a,b.] & dom g = [.b,c.]) &
    f tolerates g holds
      f +* g is continuous;

theorem :: FUZNUM_1:26
  for f, g being PartFunc of REAL, REAL st
    g is non empty &
    f = AffineMap (0,0) | (REAL \ ].a,b.[) &
    dom g = [.a,b.] & g.a = 0 & g.b = 0 holds
  f tolerates g;

theorem :: FUZNUM_1:27
  for f, g being PartFunc of REAL, REAL st
    g is continuous non empty & f = AffineMap (0,0) | (REAL \ ].a,b.[) &
  dom g = [.a,b.] & g.a = 0 & g.b = 0 holds
   ex h being PartFunc of REAL, REAL st h = f +* g &
  for x being Real st x in dom h holds h is_continuous_in x;

theorem :: FUZNUM_1:28
  for f, g being PartFunc of REAL, REAL st
    g is continuous non empty &
    f = AffineMap (0,0) | (REAL \ ].a,b.[) &
  dom g = [.a,b.] & g.a = 0 & g.b = 0 holds
    f +* g is continuous;

registration
  cluster non trivial closed_interval closed for Subset of REAL;
end;

begin :: Triangular and Trapezoidal Fuzzy Sets

definition let a,b,c be Real;
  assume that
  a < b and
  b < c;
  func TriangularFS (a,b,c) -> FuzzySet of REAL equals
:: FUZNUM_1:def 7
    AffineMap (0,0) | (REAL \ ].a,c.[)
      +* (AffineMap (1/(b-a),-a/(b-a)) | [.a,b.])
      +* (AffineMap (-1/(c-b),c/(c-b)) | [.b,c.]);
end;

::definition let C; let a,b,c be Real;
::  func TriangularFS (C,a,b,c) -> FuzzySet of C means
::    for x being Real st x in C holds
::    ((x <= a or c <= x) implies it.x = 0) &
::    (a <= x & x <= b implies it.x = (x-a)/(b-a)) &
::    (b <= x & x <= c implies it.x = (c-x)/(c-b));
::  correctness;
::end;

theorem :: FUZNUM_1:29
  for a,b,c being Real st a < b & b < c holds
    TriangularFS (a,b,c) is strictly-normalized;

theorem :: FUZNUM_1:30
  for a,b,c being Real st a < b & b < c holds
    TriangularFS (a,b,c) is continuous;

definition let a,b,c,d be Real;
  assume that
  a < b and
  b < c and
  c < d;
  func TrapezoidalFS (a,b,c,d) -> FuzzySet of REAL equals
:: FUZNUM_1:def 8
    AffineMap (0,0) | (REAL \ ].a,d.[)
      +* (AffineMap (1/(b-a),-a/(b-a)) | [.a,b.])
      +* (AffineMap (0,1) | [.b,c.])
      +* (AffineMap (-1/(d-c),d/(d-c)) | [.c,d.]);
end;

theorem :: FUZNUM_1:31
  for a,b,c,d being Real st a < b & b < c & c < d holds
    TrapezoidalFS (a,b,c,d) is normalized;

theorem :: FUZNUM_1:32
  for a,b,c,d being Real st a < b & b < c & c < d holds
    TrapezoidalFS (a,b,c,d) is continuous;

definition let F be FuzzySet of REAL;
  attr F is triangular means
:: FUZNUM_1:def 9
    ex a,b,c being Real st F = TriangularFS (a,b,c);
  attr F is trapezoidal means
:: FUZNUM_1:def 10
    ex a,b,c,d being Real st F = TrapezoidalFS (a,b,c,d);
end;

registration
  cluster triangular for FuzzySet of REAL;
  cluster trapezoidal for FuzzySet of REAL;
end;