ROUGHIF1: Formal Development of Rough Inclusion Functions

proof end;

end;

registration

let R be finite 1-sorted ;

cluster -> finite for Element of bool the carrier of R;

end;

theorem LemmaSet: :: ROUGHIF1:2

for R being 1-sorted
for X, Y being Subset of R holds
( X c= Y iff (X `) \/ Y = [#] R )

proof end;

theorem LemmaCard: :: ROUGHIF1:3

for R being finite 1-sorted
for X, Y being Subset of R holds
( card (X \/ Y) = card Y iff X c= Y )

proof end;

theorem LemmaCard2: :: ROUGHIF1:4

for R being finite 1-sorted
for X, Y being Subset of R st card ((X `) \/ Y) = card ([#] R) holds
(X `) \/ Y = [#] R by CARD_2:102;

registration

let R be non empty 1-sorted ;
let X be Subset of R;

reduce ([#] R) \/ X to [#] R;

reducibility by XBOOLE_1:12;

reduce ([#] R) /\ X to X;

reducibility by XBOOLE_1:28;

end;

definition

let R be finite Approximation_Space;
let X, Y be Subset of R;

func kappa (X,Y) -> Element of [.0,1.] equals :KappaDef: :: ROUGHIF1:def 1
(card (X /\ Y)) / (card X) if X <> {}
otherwise 1;

proof end;

consistency ;

end;

:: deftheorem KappaDef defines kappa ROUGHIF1:def 1 :

theorem :: ROUGHIF1:5

for R being finite Approximation_Space
for X being Subset of R holds kappa (({} R),X) = 1 by KappaDef;

theorem Prop1a: :: ROUGHIF1:6

for R being finite Approximation_Space
for X, Y being Subset of R holds
( kappa (X,Y) = 1 iff X c= Y )

proof end;

theorem Prop1b: :: ROUGHIF1:7

for R being finite Approximation_Space
for X, Y, Z being Subset of R st Y c= Z holds
kappa (X,Y) <= kappa (X,Z)

proof end;

theorem :: ROUGHIF1:8

for R being finite Approximation_Space
for X, Y, Z being Subset of R st Z c= Y & Y c= X holds
kappa (X,Z) <= kappa (Y,Z)

proof end;

theorem Prop1d: :: ROUGHIF1:9

for R being finite Approximation_Space
for X, Y, Z being Subset of R holds kappa (X,(Y \/ Z)) <= (kappa (X,Y)) + (kappa (X,Z))

proof end;

theorem Prop1e: :: ROUGHIF1:10

for R being finite Approximation_Space
for X, Y, Z being Subset of R st X <> {} & Y misses Z holds
kappa (X,(Y \/ Z)) = (kappa (X,Y)) + (kappa (X,Z))

proof end;

definition

let R be 1-sorted ;
mode preRoughInclusionFunction of R is Function of [:(bool the carrier of R),(bool the carrier of R):],[.0,1.];

end;

definition

let R be 1-sorted ;
mode preRIF of R is preRoughInclusionFunction of R;

end;

scheme :: ROUGHIF1:sch 1
BinOpEq{ F₁() -> non empty 1-sorted , F₂( Subset of F₁(), Subset of F₁()) -> Element of [.0,1.] } :

for f1, f2 being preRIF of F₁() st ( for x, y being Subset of F₁() holds f1 . (x,y) = F₂(x,y) ) & ( for x, y being Subset of F₁() holds f2 . (x,y) = F₂(x,y) ) holds
f1 = f2

proof end;

definition

let R be finite Approximation_Space;

func kappa R -> preRIF of R means :DefKappa: :: ROUGHIF1:def 2
for x, y being Subset of R holds it . (x,y) = kappa (x,y);

proof end;

uniqueness

proof end;

end;

:: deftheorem DefKappa defines kappa ROUGHIF1:def 2 :

definition

let R be finite Approximation_Space;
let X, Y be Subset of R;

func kappa_1 (X,Y) -> Element of [.0,1.] equals :Kappa1: :: ROUGHIF1:def 3
(card Y) / (card (X \/ Y)) if X \/ Y <> {}
otherwise 1;

proof end;

consistency ;

func kappa_2 (X,Y) -> Element of [.0,1.] equals :: ROUGHIF1:def 4
(card ((X `) \/ Y)) / (card ([#] R));

proof end;

end;

:: deftheorem Kappa1 defines kappa_1 ROUGHIF1:def 3 :

:: deftheorem defines kappa_2 ROUGHIF1:def 4 :

definition

let R be finite Approximation_Space;

func kappa_1 R -> preRIF of R means :DefKappa1: :: ROUGHIF1:def 5
for x, y being Subset of R holds it . (x,y) = kappa_1 (x,y);

proof end;

uniqueness

proof end;

func kappa_2 R -> preRIF of R means :DefKappa2: :: ROUGHIF1:def 6
for x, y being Subset of R holds it . (x,y) = kappa_2 (x,y);

proof end;

uniqueness

proof end;

end;

:: deftheorem DefKappa1 defines kappa_1 ROUGHIF1:def 5 :

:: deftheorem DefKappa2 defines kappa_2 ROUGHIF1:def 6 :

theorem Prop11a: :: ROUGHIF1:11

for R being finite Approximation_Space
for X, Y being Subset of R holds
( kappa_1 (X,Y) = 1 iff X c= Y )

proof end;

theorem Prop11b: :: ROUGHIF1:12

for R being finite Approximation_Space
for X, Y being Subset of R holds
( kappa_2 (X,Y) = 1 iff X c= Y )

proof end;

theorem LemmaProp4a: :: ROUGHIF1:13

for R being finite Approximation_Space
for X, Y being Subset of R st kappa_1 (X,Y) = 0 holds
Y = {}

proof end;

theorem Prop4a: :: ROUGHIF1:14

for R being finite Approximation_Space
for X, Y being Subset of R st X <> {} holds
( kappa_1 (X,Y) = 0 iff Y = {} )

proof end;

theorem Prop4b: :: ROUGHIF1:15

for R being finite Approximation_Space
for X, Y being Subset of R holds
( kappa_2 (X,Y) = 0 iff ( X = [#] R & Y = {} ) )

proof end;

theorem Prop2b: :: ROUGHIF1:16

for R being finite Approximation_Space
for X, Y, Z being Subset of R st Y c= Z holds
kappa_1 (X,Y) <= kappa_1 (X,Z)

proof end;

theorem Prop3b: :: ROUGHIF1:17

for R being finite Approximation_Space
for X, Y, Z being Subset of R st Y c= Z holds
kappa_2 (X,Y) <= kappa_2 (X,Z)

proof end;

theorem Lemma2: :: ROUGHIF1:18

for R being finite Approximation_Space
for X being Subset of R holds kappa_1 (({} R),X) = 1

proof end;

theorem Lemma3: :: ROUGHIF1:19

for R being finite Approximation_Space
for X being Subset of R holds kappa_2 (({} R),X) = 1

proof end;

definition

let R be non empty RelStr ;
let f be preRIF of R;

attr f is satisfying_RIF1 means :RIF1Def: :: ROUGHIF1:def 7
for X, Y being Subset of R holds
( f . (X,Y) = 1 iff X c= Y );

attr f is satisfying_RIF2 means :: ROUGHIF1:def 8
for X, Y, Z being Subset of R st Y c= Z holds
f . (X,Y) <= f . (X,Z);

attr f is satisfying_RIF3 means :: ROUGHIF1:def 9
for X being Subset of R st X <> {} holds
f . (X,({} R)) = 0 ;

attr f is satisfying_RIF4 means :: ROUGHIF1:def 10
for X, Y being Subset of R st f . (X,Y) = 0 holds
X misses Y;

end;

:: deftheorem RIF1Def defines satisfying_RIF1 ROUGHIF1:def 7 :

:: deftheorem defines satisfying_RIF2 ROUGHIF1:def 8 :

:: deftheorem defines satisfying_RIF3 ROUGHIF1:def 9 :

:: deftheorem defines satisfying_RIF4 ROUGHIF1:def 10 :

:: Towards weak quasi-RIFs, will be developed later on

definition

let R be non empty RelStr ;
let f be preRIF of R;

attr f is satisfying_RIF0 means :: ROUGHIF1:def 11
for X, Y being Subset of R st X c= Y holds
f . (X,Y) = 1;

attr f is satisfying_RIF01 means :: ROUGHIF1:def 12
for X, Y being Subset of R st f . (X,Y) = 1 holds
X c= Y;

attr f is satisfying_RIF2* means :: ROUGHIF1:def 13
for X, Y, Z being Subset of R st f . (Y,Z) = 1 holds
f . (X,Y) <= f . (X,Z);

end;

:: deftheorem defines satisfying_RIF0 ROUGHIF1:def 11 :

:: deftheorem defines satisfying_RIF01 ROUGHIF1:def 12 :

:: deftheorem defines satisfying_RIF2* ROUGHIF1:def 13 :

:: rif1 -> (rif2 iff rif2*)
:: qRifs are rif0 and rif2*
:: weak qRIFs are rif0 and rif2

registration

let R be non empty RelStr ;

cluster V6() V18([:(bool the carrier of R),(bool the carrier of R):],[.0,1.]) satisfying_RIF1 -> satisfying_RIF0 satisfying_RIF01 for Element of bool [:[:(bool the carrier of R),(bool the carrier of R):],[.0,1.]:];

coherence ;

cluster V6() V18([:(bool the carrier of R),(bool the carrier of R):],[.0,1.]) satisfying_RIF0 satisfying_RIF01 -> satisfying_RIF1 for Element of bool [:[:(bool the carrier of R),(bool the carrier of R):],[.0,1.]:];

end;

registration

let R be finite Approximation_Space;

cluster kappa R -> satisfying_RIF1 ;

proof end;

cluster kappa R -> satisfying_RIF2 ;

proof end;

cluster kappa_1 R -> satisfying_RIF1 ;

proof end;

cluster kappa_1 R -> satisfying_RIF2 ;

proof end;

cluster kappa_2 R -> satisfying_RIF1 ;

proof end;

cluster kappa_2 R -> satisfying_RIF2 ;

proof end;

end;

registration

let R be finite Approximation_Space;

cluster V6() V18([:(bool the carrier of R),(bool the carrier of R):],[.0,1.]) finite satisfying_RIF1 satisfying_RIF2 for Element of bool [:[:(bool the carrier of R),(bool the carrier of R):],[.0,1.]:];

proof end;

end;

theorem RIF2Iff: :: ROUGHIF1:20

for R being finite Approximation_Space
for f being satisfying_RIF1 preRIF of R holds
( f is satisfying_RIF2 iff f is satisfying_RIF2* )

proof end;

registration

let R be finite Approximation_Space;

cluster V6() V18([:(bool the carrier of R),(bool the carrier of R):],[.0,1.]) satisfying_RIF1 satisfying_RIF2 -> satisfying_RIF1 satisfying_RIF2* for Element of bool [:[:(bool the carrier of R),(bool the carrier of R):],[.0,1.]:];

coherence by RIF2Iff;

cluster V6() V18([:(bool the carrier of R),(bool the carrier of R):],[.0,1.]) satisfying_RIF1 satisfying_RIF2* -> satisfying_RIF1 satisfying_RIF2 for Element of bool [:[:(bool the carrier of R),(bool the carrier of R):],[.0,1.]:];

coherence by RIF2Iff;

end;

registration

let R be finite Approximation_Space;

cluster kappa R -> satisfying_RIF0 satisfying_RIF2* ;

end;

registration

let R be finite Approximation_Space;

cluster V6() V18([:(bool the carrier of R),(bool the carrier of R):],[.0,1.]) finite satisfying_RIF1 satisfying_RIF2 satisfying_RIF0 satisfying_RIF2* for Element of bool [:[:(bool the carrier of R),(bool the carrier of R):],[.0,1.]:];

proof end;

end;

definition

let R be finite Approximation_Space;
mode RoughInclusionFunction of R is satisfying_RIF1 satisfying_RIF2 preRoughInclusionFunction of R;

end;

definition

let R be finite Approximation_Space;
mode quasi-RoughInclusionFunction of R is satisfying_RIF0 satisfying_RIF2* preRIF of R;
mode weak_quasi-RoughInclusionFunction of R is satisfying_RIF2 satisfying_RIF0 preRIF of R;

end;

definition

let R be finite Approximation_Space;
mode RIF of R is RoughInclusionFunction of R;
mode qRIF of R is quasi-RoughInclusionFunction of R;
mode wqRIF of R is weak_quasi-RoughInclusionFunction of R;

end;

:: The following three should be obvious (Proposition 3)
:: kappa R is RIF of R;
:: kappa_1 R is RIF of R;
:: kappa_2 R is RIF of R;

theorem :: ROUGHIF1:21

for R being finite Approximation_Space
for X, Z, W being Subset of R st X <> {} & Z \/ W = [#] R & Z misses W holds
(kappa (X,Z)) + (kappa (X,W)) = 1

proof end;

theorem LemmaProp2b: :: ROUGHIF1:22

for R being finite Approximation_Space
for X, Y being Subset of R st kappa (X,Y) = 0 holds
X misses Y

proof end;

theorem Prop2b: :: ROUGHIF1:23

for R being finite Approximation_Space
for X, Y being Subset of R st X <> {} holds
( kappa (X,Y) = 0 iff X misses Y )

proof end;

theorem Prop2c: :: ROUGHIF1:24

for R being finite Approximation_Space
for X being Subset of R st X <> {} holds
kappa (X,({} R)) = 0

proof end;

theorem :: ROUGHIF1:25

for R being finite Approximation_Space
for X, Y, Z being Subset of R st X <> {} & X misses Y holds
( kappa (X,(Z \ Y)) = kappa (X,(Z \/ Y)) & kappa (X,(Z \/ Y)) = kappa (X,Z) )

proof end;

Test1: for R being finite Approximation_Space
for Y, Z, W being Subset of R st Z misses W holds
kappa ((Y \/ Z),W) <= kappa (Y,W)

proof end;

Test2: for R being finite Approximation_Space
for Y, Z, W being Subset of R st Z misses W holds
kappa (Y,W) <= kappa ((Y \ Z),W)

proof end;

theorem :: ROUGHIF1:26

for R being finite Approximation_Space
for Y, Z, W being Subset of R st Z misses W holds
( kappa ((Y \/ Z),W) <= kappa (Y,W) & kappa (Y,W) <= kappa ((Y \ Z),W) ) by Test1, Test2;

Test1AAA: for R being finite Approximation_Space
for Y, Z, W being Subset of R st Y misses Z & Z c= W holds
kappa ((Y \/ Z),W) >= kappa (Y,W)

proof end;

Test2AAA: for R being finite Approximation_Space
for Y, Z, W being Subset of R st Y misses Z & Z c= W holds
kappa (Y,W) >= kappa ((Y \ Z),W)

proof end;

theorem :: ROUGHIF1:27

for R being finite Approximation_Space
for Y, Z, W being Subset of R st Z misses Y & Z c= W holds
( kappa ((Y \ Z),W) <= kappa (Y,W) & kappa (Y,W) <= kappa ((Y \/ Z),W) ) by Test1AAA, Test2AAA;

registration

let R be finite Approximation_Space;
let X be non empty Subset of R;

cluster kappa (X,({} R)) -> empty ;

coherence by Prop2c;

end;

theorem Kappa1RIF4: :: ROUGHIF1:28

for R being finite Approximation_Space
for X, Y being Subset of R st kappa_1 (X,Y) = 0 holds
X misses Y

proof end;

theorem Kappa2RIF4: :: ROUGHIF1:29

for R being finite Approximation_Space
for X, Y being Subset of R st kappa_2 (X,Y) = 0 holds
X misses Y

proof end;

registration

let R be finite Approximation_Space;

cluster kappa R -> satisfying_RIF4 ;

proof end;

cluster kappa_1 R -> satisfying_RIF4 ;

proof end;

cluster kappa_2 R -> satisfying_RIF4 ;

proof end;

end;

theorem :: ROUGHIF1:30

for R being finite Approximation_Space
for X, Y being Subset of R holds
( kappa (X,Y) <= kappa_1 (X,Y) & kappa_1 (X,Y) <= kappa_2 (X,Y) )

proof end;

theorem :: ROUGHIF1:31

for R being finite Approximation_Space
for X, Y being Subset of R holds kappa_1 (X,Y) = kappa ((X \/ Y),Y)

proof end;

LemmaKap1: for R being finite Approximation_Space
for X, Y being Subset of R holds kappa (X,Y) = kappa (X,(X /\ Y))

proof end;

LemmaKap2: for R being finite Approximation_Space
for X, Y being Subset of R holds kappa_1 (X,(X /\ Y)) = kappa_1 ((X \ Y),(X /\ Y))

proof end;

LemmaKap3: for R being finite Approximation_Space
for X, Y being Subset of R holds kappa (X,(X /\ Y)) = kappa_1 (X,(X /\ Y))

proof end;

Lemma4f1: for R being finite Approximation_Space
for X, Y being Subset of R holds kappa_2 (X,Y) = kappa (([#] R),((X `) \/ Y))

proof end;

Lemma4f2: for R being finite Approximation_Space
for X, Y being Subset of R holds kappa (([#] R),((X `) \/ Y)) = (kappa (([#] R),(X `))) + (kappa (([#] R),(X /\ Y)))

proof end;

theorem :: ROUGHIF1:32

for R being finite Approximation_Space
for X, Y being Subset of R holds
( kappa_2 (X,Y) = kappa (([#] R),((X `) \/ Y)) & kappa (([#] R),((X `) \/ Y)) = (kappa (([#] R),(X `))) + (kappa (([#] R),(X /\ Y))) ) by Lemma4f1, Lemma4f2;

theorem :: ROUGHIF1:33

for R being finite Approximation_Space
for X, Y being Subset of R holds
( kappa (X,Y) = kappa (X,(X /\ Y)) & kappa (X,(X /\ Y)) = kappa_1 (X,(X /\ Y)) & kappa_1 (X,(X /\ Y)) = kappa_1 ((X \ Y),(X /\ Y)) ) by LemmaKap1, LemmaKap2, LemmaKap3;

theorem :: ROUGHIF1:34

for R being finite Approximation_Space
for X, Y being Subset of R st X \/ Y = [#] R holds
kappa_1 (X,Y) = kappa_2 (X,Y)

proof end;

theorem :: ROUGHIF1:35

for R being finite Approximation_Space
for X, Y being Subset of R st X <> {} holds
1 - (kappa (X,Y)) = kappa (X,(Y `))

proof end;

:: are distinct -- Example 1 and 2 translated
:: calculations in Mizar seem to be too complex, my propositions are a bit
:: shorter than in the original

definition

let X be set ;

func DiscreteApproxSpace X -> strict RelStr equals :: ROUGHIF1:def 14
RelStr(# X,(id X) #);

end;

:: deftheorem defines DiscreteApproxSpace ROUGHIF1:def 14 :

registration

let X be set ;

cluster DiscreteApproxSpace X -> strict with_equivalence ;

end;

registration

let X be non empty set ;

cluster DiscreteApproxSpace X -> non empty strict ;

end;

registration

let X be finite set ;

cluster DiscreteApproxSpace X -> finite strict ;