:: 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;