:: The Formal Construction of Fuzzy Numbers
:: by Adam Grabowski
::
:: Received December 31, 2014
:: Copyright (c) 2014-2016 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;