:: OSALG_1 semantic presentation

registration

let I be set ;
let f be ManySortedSet of I;
let p be FinSequence of I;
cluster p * f -> FinSequence-like ;
coherence

proof end;

end;

Lm1: for I being set
for f being ManySortedSet of I
for p being FinSequence of I holds
( dom (f * p) = dom p & len (f * p) = len p )

proof end;

definition

let S be non empty ManySortedSign ;
mode SortSymbol of S is Element of S;

end;

definition

let S be non empty ManySortedSign ;
mode OperSymbol of S is Element of the OperSymbols of S;

end;

definition

let S be non empty non void ManySortedSign ;
let o be OperSymbol of S;
:: original: the_result_sort_of
redefine func the_result_sort_of o -> Element of S;
coherence ;

end;

definition

attr c₁ is strict;
struct OverloadedMSSign -> ManySortedSign ;
aggr OverloadedMSSign(# carrier, OperSymbols, Overloading, Arity, ResultSort #) -> OverloadedMSSign ;
sel Overloading c₁ -> Equivalence_Relation of the OperSymbols of c₁;

end;

definition

attr c₁ is strict;
struct RelSortedSign -> ManySortedSign , RelStr ;
aggr RelSortedSign(# carrier, InternalRel, OperSymbols, Arity, ResultSort #) -> RelSortedSign ;

end;

definition

attr c₁ is strict;
struct OverloadedRSSign -> OverloadedMSSign , RelSortedSign ;
aggr OverloadedRSSign(# carrier, InternalRel, OperSymbols, Overloading, Arity, ResultSort #) -> OverloadedRSSign ;

end;

theorem Th1: :: OSALG_1:1

for A, O being non empty set
for R being Order of A
for Ol being Equivalence_Relation of O
for f being Function of O,A *
for g being Function of O,A holds
( not OverloadedRSSign(# A,R,O,Ol,f,g #) is empty & not OverloadedRSSign(# A,R,O,Ol,f,g #) is void & OverloadedRSSign(# A,R,O,Ol,f,g #) is reflexive & OverloadedRSSign(# A,R,O,Ol,f,g #) is transitive & OverloadedRSSign(# A,R,O,Ol,f,g #) is antisymmetric )

proof end;

registration

let A be non empty set ;
let R be Order of A;
let O be non empty set ;
let Ol be Equivalence_Relation of O;
let f be Function of O,A * ;
let g be Function of O,A;
cluster OverloadedRSSign(# A,R,O,Ol,f,g #) -> non empty reflexive transitive antisymmetric ;
coherence by Th1;

end;

definition

let S be OverloadedRSSign ;
canceled;
attr S is order-sorted means :Def2: :: OSALG_1:def 2
( S is reflexive & S is transitive & S is antisymmetric );

end;

:: deftheorem OSALG_1:def 1 :

:: deftheorem Def2 defines order-sorted OSALG_1:def 2 :

registration

cluster order-sorted -> reflexive transitive antisymmetric OverloadedRSSign ;
coherence by Def2;
cluster non empty non void strict order-sorted OverloadedRSSign ;
existence

proof end;

end;

registration

cluster non empty non void OverloadedMSSign ;
existence

proof end;

end;

definition

let S be non empty non void OverloadedMSSign ;
let x, y be OperSymbol of S;
pred x ~= y means :Def3: :: OSALG_1:def 3
[x,y] in the Overloading of S;
symmetry

proof end;

reflexivity

proof end;

end;

:: deftheorem Def3 defines ~= OSALG_1:def 3 :

theorem Th2: :: OSALG_1:2

for S being non empty non void OverloadedMSSign
for o, o1, o2 being OperSymbol of S st o ~= o1 & o1 ~= o2 holds
o ~= o2

proof end;

definition

let S be non empty non void OverloadedMSSign ;
attr S is discernable means :Def4: :: OSALG_1:def 4
for x, y being OperSymbol of S st x ~= y & the_arity_of x = the_arity_of y & the_result_sort_of x = the_result_sort_of y holds
x = y;
attr S is op-discrete means :Def5: :: OSALG_1:def 5
the Overloading of S = id the OperSymbols of S;

end;

:: deftheorem Def4 defines discernable OSALG_1:def 4 :

:: deftheorem Def5 defines op-discrete OSALG_1:def 5 :

theorem Th3: :: OSALG_1:3

for S being non empty non void OverloadedMSSign holds
( S is op-discrete iff for x, y being OperSymbol of S st x ~= y holds
x = y )

proof end;

theorem Th4: :: OSALG_1:4

for S being non empty non void OverloadedMSSign st S is op-discrete holds
S is discernable

proof end;

definition

let S0 be non empty non void ManySortedSign ;
func OSSign S0 -> non empty non void strict order-sorted OverloadedRSSign means :Def6: :: OSALG_1:def 6
( the carrier of S0 = the carrier of it & id the carrier of S0 = the InternalRel of it & the OperSymbols of S0 = the OperSymbols of it & id the OperSymbols of S0 = the Overloading of it & the Arity of S0 = the Arity of it & the ResultSort of S0 = the ResultSort of it );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def6 defines OSSign OSALG_1:def 6 :

theorem Th5: :: OSALG_1:5

for S0 being non empty non void ManySortedSign holds
( OSSign S0 is discrete & OSSign S0 is op-discrete )

proof end;

registration

cluster non empty reflexive transitive antisymmetric discrete non void strict order-sorted discernable op-discrete OverloadedRSSign ;
existence

proof end;

end;

registration

cluster non empty non void op-discrete -> non empty non void discernable OverloadedRSSign ;
coherence by Th4;

end;

registration

let S0 be non empty non void ManySortedSign ;
cluster OSSign S0 -> non empty reflexive transitive antisymmetric discrete non void strict order-sorted discernable op-discrete ;
coherence by Th5;

end;

definition

mode OrderSortedSign is non empty non void order-sorted discernable OverloadedRSSign ;

end;

definition

let S be non empty Poset;
let w1, w2 be Element of the carrier of S * ;
pred w1 <= w2 means :Def7: :: OSALG_1:def 7
( len w1 = len w2 & ( for i being set st i in dom w1 holds
for s1, s2 being Element of S st s1 = w1 . i & s2 = w2 . i holds
s1 <= s2 ) );
reflexivity ;

end;

:: deftheorem Def7 defines <= OSALG_1:def 7 :

theorem Th6: :: OSALG_1:6

for S being non empty Poset
for w1, w2 being Element of the carrier of S * st w1 <= w2 & w2 <= w1 holds
w1 = w2

proof end;

theorem Th7: :: OSALG_1:7

for S being non empty Poset
for w1, w2 being Element of the carrier of S * st S is discrete & w1 <= w2 holds
w1 = w2

proof end;

theorem Th8: :: OSALG_1:8

for S being OrderSortedSign
for o1, o2 being OperSymbol of S st S is discrete & o1 ~= o2 & the_arity_of o1 <= the_arity_of o2 & the_result_sort_of o1 <= the_result_sort_of o2 holds
o1 = o2

proof end;

definition

let S be OrderSortedSign;
let o be OperSymbol of S;
attr o is monotone means :Def8: :: OSALG_1:def 8
for o2 being OperSymbol of S st o ~= o2 & the_arity_of o <= the_arity_of o2 holds
the_result_sort_of o <= the_result_sort_of o2;

end;

:: deftheorem Def8 defines monotone OSALG_1:def 8 :

definition

let S be OrderSortedSign;
attr S is monotone means :Def9: :: OSALG_1:def 9
for o being OperSymbol of S holds o is monotone;

end;

:: deftheorem Def9 defines monotone OSALG_1:def 9 :

theorem Th9: :: OSALG_1:9

for S being OrderSortedSign st S is op-discrete holds
S is monotone

proof end;

registration

cluster monotone OverloadedRSSign ;
existence

proof end;

end;

registration

let S be monotone OrderSortedSign;
cluster monotone Element of the OperSymbols of S;
existence

proof end;

end;

registration

let S be monotone OrderSortedSign;
cluster -> monotone Element of the OperSymbols of S;
coherence by Def9;

end;

registration

cluster op-discrete -> reflexive transitive antisymmetric monotone OverloadedRSSign ;
coherence by Th9;

end;

theorem :: OSALG_1:10

for S being OrderSortedSign
for o1, o2 being OperSymbol of S st S is monotone & the_arity_of o1 = {} & o1 ~= o2 & the_arity_of o2 = {} holds
o1 = o2

proof end;

definition

let S be OrderSortedSign;
let o, o1 be OperSymbol of S;
let w1 be Element of the carrier of S * ;
pred o1 has_least_args_for o,w1 means :Def10: :: OSALG_1:def 10
( o ~= o1 & w1 <= the_arity_of o1 & ( for o2 being OperSymbol of S st o ~= o2 & w1 <= the_arity_of o2 holds
the_arity_of o1 <= the_arity_of o2 ) );
pred o1 has_least_sort_for o,w1 means :Def11: :: OSALG_1:def 11
( o ~= o1 & w1 <= the_arity_of o1 & ( for o2 being OperSymbol of S st o ~= o2 & w1 <= the_arity_of o2 holds
the_result_sort_of o1 <= the_result_sort_of o2 ) );

end;

:: deftheorem Def10 defines has_least_args_for OSALG_1:def 10 :

:: deftheorem Def11 defines has_least_sort_for OSALG_1:def 11 :

definition

let S be OrderSortedSign;
let o, o1 be OperSymbol of S;
let w1 be Element of the carrier of S * ;
pred o1 has_least_rank_for o,w1 means :Def12: :: OSALG_1:def 12
( o1 has_least_args_for o,w1 & o1 has_least_sort_for o,w1 );

end;

:: deftheorem Def12 defines has_least_rank_for OSALG_1:def 12 :

definition

let S be OrderSortedSign;
let o be OperSymbol of S;
attr o is regular means :Def13: :: OSALG_1:def 13
( o is monotone & ( for w1 being Element of the carrier of S * st w1 <= the_arity_of o holds
ex o1 being OperSymbol of S st o1 has_least_args_for o,w1 ) );

end;

:: deftheorem Def13 defines regular OSALG_1:def 13 :

definition

let SM be monotone OrderSortedSign;
attr SM is regular means :Def14: :: OSALG_1:def 14
for om being OperSymbol of SM holds om is regular;

end;

:: deftheorem Def14 defines regular OSALG_1:def 14 :

theorem Th11: :: OSALG_1:11

for SM being monotone OrderSortedSign holds
( SM is regular iff for o being OperSymbol of SM
for w1 being Element of the carrier of SM * st w1 <= the_arity_of o holds
ex o1 being OperSymbol of SM st o1 has_least_rank_for o,w1 )

proof end;

theorem Th12: :: OSALG_1:12

for SM being monotone OrderSortedSign st SM is op-discrete holds
SM is regular

proof end;

registration

cluster monotone regular OverloadedRSSign ;
existence

proof end;

end;

registration

cluster op-discrete monotone -> reflexive transitive antisymmetric monotone regular OverloadedRSSign ;
coherence by Th12;

end;

registration

let SR be monotone regular OrderSortedSign;
cluster -> monotone regular Element of the OperSymbols of SR;
coherence by Def14;

end;

theorem Th13: :: OSALG_1:13

for SR being monotone regular OrderSortedSign
for o, o3, o4 being OperSymbol of SR
for w1 being Element of the carrier of SR * st w1 <= the_arity_of o & o3 has_least_args_for o,w1 & o4 has_least_args_for o,w1 holds
o3 = o4

proof end;

definition

let SR be monotone regular OrderSortedSign;
let o be OperSymbol of SR;
let w1 be Element of the carrier of SR * ;
assume A1: w1 <= the_arity_of o ;
func LBound o,w1 -> OperSymbol of SR means :Def15: :: OSALG_1:def 15
it has_least_args_for o,w1;
existence by A1, Def13;
uniqueness by A1, Th13;

end;

:: deftheorem Def15 defines LBound OSALG_1:def 15 :

theorem Th14: :: OSALG_1:14

for SR being monotone regular OrderSortedSign
for o being OperSymbol of SR
for w1 being Element of the carrier of SR * st w1 <= the_arity_of o holds
LBound o,w1 has_least_rank_for o,w1

proof end;

definition

let R be non empty Poset;
let z be non empty set ;
func ConstOSSet R,z -> ManySortedSet of the carrier of R equals :: OSALG_1:def 16
the carrier of R --> z;
correctness

proof end;

end;

:: deftheorem defines ConstOSSet OSALG_1:def 16 :

theorem Th15: :: OSALG_1:15

for R being non empty Poset
for z being non empty set holds
( ConstOSSet R,z is non-empty & ( for s1, s2 being Element of R st s1 <= s2 holds
(ConstOSSet R,z) . s1 c= (ConstOSSet R,z) . s2 ) )

proof end;

definition

let R be non empty Poset;
let M be ManySortedSet of R;
canceled;
attr M is order-sorted means :Def18: :: OSALG_1:def 18
for s1, s2 being Element of R st s1 <= s2 holds
M . s1 c= M . s2;

end;

:: deftheorem OSALG_1:def 17 :

:: deftheorem Def18 defines order-sorted OSALG_1:def 18 :

theorem Th16: :: OSALG_1:16

for R being non empty Poset
for z being non empty set holds ConstOSSet R,z is order-sorted

proof end;

registration

let R be non empty Poset;
cluster order-sorted ManySortedSet of the carrier of R;
existence

proof end;

end;

definition

let R be non empty Poset;
let z be non empty set ;
:: original: ConstOSSet
redefine func ConstOSSet R,z -> order-sorted ManySortedSet of R;
coherence by Th16;

end;

definition

let R be non empty Poset;
mode OrderSortedSet of R is order-sorted ManySortedSet of R;

end;

registration

let R be non empty Poset;
cluster V2 ManySortedSet of the carrier of R;
existence

proof end;

end;

definition

let S be OrderSortedSign;
let M be MSAlgebra of S;
attr M is order-sorted means :Def19: :: OSALG_1:def 19
for s1, s2 being SortSymbol of S st s1 <= s2 holds
the Sorts of M . s1 c= the Sorts of M . s2;

end;

:: deftheorem Def19 defines order-sorted OSALG_1:def 19 :

theorem Th17: :: OSALG_1:17

for S being OrderSortedSign
for M being MSAlgebra of S holds
( M is order-sorted iff the Sorts of M is OrderSortedSet of S )

proof end;

definition

let S be OrderSortedSign;
let z be non empty set ;
let CH be ManySortedFunction of ((ConstOSSet S,z) # ) * the Arity of S,(ConstOSSet S,z) * the ResultSort of S;
func ConstOSA S,z,CH -> strict non-empty MSAlgebra of S means :Def20: :: OSALG_1:def 20
( the Sorts of it = ConstOSSet S,z & the Charact of it = CH );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def20 defines ConstOSA OSALG_1:def 20 :

theorem Th18: :: OSALG_1:18

for S being OrderSortedSign
for z being non empty set
for CH being ManySortedFunction of ((ConstOSSet S,z) # ) * the Arity of S,(ConstOSSet S,z) * the ResultSort of S holds ConstOSA S,z,CH is order-sorted

proof end;

registration

let S be OrderSortedSign;
cluster strict non-empty order-sorted MSAlgebra of S;
existence

proof end;

end;

registration

let S be OrderSortedSign;
let z be non empty set ;
let CH be ManySortedFunction of ((ConstOSSet S,z) # ) * the Arity of S,(ConstOSSet S,z) * the ResultSort of S;
cluster ConstOSA S,z,CH -> strict non-empty order-sorted ;
coherence by Th18;

end;

definition

let S be OrderSortedSign;
mode OSAlgebra of S is order-sorted MSAlgebra of S;

end;

theorem Th19: :: OSALG_1:19

for S being discrete OrderSortedSign
for M being MSAlgebra of S holds M is order-sorted

proof end;

registration

let S be discrete OrderSortedSign;
cluster -> order-sorted MSAlgebra of S;
coherence by Th19;

end;

theorem Th20: :: OSALG_1:20

for S being OrderSortedSign
for w1, w2 being Element of the carrier of S *
for A being OSAlgebra of S st w1 <= w2 holds
(the Sorts of A # ) . w1 c= (the Sorts of A # ) . w2

proof end;

definition

let S0 be non empty non void ManySortedSign ;
let M be MSAlgebra of S0;
func OSAlg M -> strict OSAlgebra of OSSign S0 means :: OSALG_1:def 21
( the Sorts of it = the Sorts of M & the Charact of it = the Charact of M );
uniqueness ;
existence

proof end;

end;

:: deftheorem defines OSAlg OSALG_1:def 21 :

theorem Th21: :: OSALG_1:21

for S being OrderSortedSign
for w1, w2, w3 being Element of the carrier of S * st w1 <= w2 & w2 <= w3 holds
w1 <= w3

proof end;

definition

let S be OrderSortedSign;
let o1, o2 be OperSymbol of S;
pred o1 <= o2 means :Def22: :: OSALG_1:def 22
( o1 ~= o2 & the_arity_of o1 <= the_arity_of o2 & the_result_sort_of o1 <= the_result_sort_of o2 );
reflexivity ;

end;

:: deftheorem Def22 defines <= OSALG_1:def 22 :

theorem :: OSALG_1:22

for S being OrderSortedSign
for o1, o2 being OperSymbol of S st o1 <= o2 & o2 <= o1 holds
o1 = o2

proof end;

theorem :: OSALG_1:23

for S being OrderSortedSign
for o1, o2, o3 being OperSymbol of S st o1 <= o2 & o2 <= o3 holds
o1 <= o3

proof end;

theorem Th24: :: OSALG_1:24

for S being OrderSortedSign
for o1, o2 being OperSymbol of S
for A being OSAlgebra of S st the_result_sort_of o1 <= the_result_sort_of o2 holds
Result o1,A c= Result o2,A

proof end;

theorem Th25: :: OSALG_1:25

for S being OrderSortedSign
for o1, o2 being OperSymbol of S
for A being OSAlgebra of S st the_arity_of o1 <= the_arity_of o2 holds
Args o1,A c= Args o2,A

proof end;

theorem :: OSALG_1:26

for S being OrderSortedSign
for o1, o2 being OperSymbol of S
for A being OSAlgebra of S st o1 <= o2 holds
( Args o1,A c= Args o2,A & Result o1,A c= Result o2,A )

proof end;

definition

let S be OrderSortedSign;
let A be OSAlgebra of S;
attr A is monotone means :Def23: :: OSALG_1:def 23
for o1, o2 being OperSymbol of S st o1 <= o2 holds
(Den o2,A) | (Args o1,A) = Den o1,A;

end;

:: deftheorem Def23 defines monotone OSALG_1:def 23 :

theorem Th27: :: OSALG_1:27

for S being OrderSortedSign
for A being non-empty OSAlgebra of S holds
( A is monotone iff for o1, o2 being OperSymbol of S st o1 <= o2 holds
Den o1,A c= Den o2,A )

proof end;

theorem :: OSALG_1:28

for S being OrderSortedSign
for A being OSAlgebra of S st ( S is discrete or S is op-discrete ) holds
A is monotone

proof end;

definition

let S be OrderSortedSign;
let z be non empty set ;
let z1 be Element of z;
func TrivialOSA S,z,z1 -> strict OSAlgebra of S means :Def24: :: OSALG_1:def 24
( the Sorts of it = ConstOSSet S,z & ( for o being OperSymbol of S holds Den o,it = (Args o,it) --> z1 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def24 defines TrivialOSA OSALG_1:def 24 :

theorem Th29: :: OSALG_1:29

for S being OrderSortedSign
for z being non empty set
for z1 being Element of z holds
( TrivialOSA S,z,z1 is non-empty & TrivialOSA S,z,z1 is monotone )

proof end;

registration

let S be OrderSortedSign;
cluster strict non-empty monotone MSAlgebra of S;
existence

proof end;

end;

registration

let S be OrderSortedSign;
let z be non empty set ;
let z1 be Element of z;
cluster TrivialOSA S,z,z1 -> strict non-empty monotone ;
coherence by Th29;

end;

definition

let S be OrderSortedSign;
func OperNames S -> non empty Subset-Family of the OperSymbols of S equals :: OSALG_1:def 25
Class the Overloading of S;
coherence ;

end;

:: deftheorem defines OperNames OSALG_1:def 25 :

registration

let S be OrderSortedSign;
cluster -> non empty Element of OperNames S;
coherence

proof end;

end;

definition

let S be OrderSortedSign;
mode OperName of S is Element of OperNames S;

end;

definition

let S be OrderSortedSign;
let op1 be OperSymbol of S;
func Name op1 -> OperName of S equals :: OSALG_1:def 26
Class the Overloading of S,op1;
coherence by EQREL_1:def 5;

end;

:: deftheorem defines Name OSALG_1:def 26 :

theorem Th30: :: OSALG_1:30

for S being OrderSortedSign
for op1, op2 being OperSymbol of S holds
( op1 ~= op2 iff op2 in Class the Overloading of S,op1 )

proof end;

theorem Th31: :: OSALG_1:31

for S being OrderSortedSign
for op1, op2 being OperSymbol of S holds
( op1 ~= op2 iff Name op1 = Name op2 )

proof end;

theorem :: OSALG_1:32

for S being OrderSortedSign
for X being set holds
( X is OperName of S iff ex op1 being OperSymbol of S st X = Name op1 )

proof end;

definition

let S be OrderSortedSign;
let o be OperName of S;
:: original: Element
redefine mode Element of o -> OperSymbol of S;
coherence

proof end;

end;

theorem Th33: :: OSALG_1:33

for S being OrderSortedSign
for on being OperName of S
for op being OperSymbol of S holds
( op is Element of on iff Name op = on )

proof end;

theorem Th34: :: OSALG_1:34

for SR being monotone regular OrderSortedSign
for op1, op2 being OperSymbol of SR
for w being Element of the carrier of SR * st op1 ~= op2 & len (the_arity_of op1) = len (the_arity_of op2) & w <= the_arity_of op1 & w <= the_arity_of op2 holds
LBound op1,w = LBound op2,w

proof end;

definition

let SR be monotone regular OrderSortedSign;
let on be OperName of SR;
let w be Element of the carrier of SR * ;
assume A1: ex op being Element of on st w <= the_arity_of op ;
func LBound on,w -> Element of on means :: OSALG_1:def 27
for op being Element of on st w <= the_arity_of op holds
it = LBound op,w;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines LBound OSALG_1:def 27 :

theorem :: OSALG_1:35

for S being monotone regular OrderSortedSign
for o being OperSymbol of S
for w1 being Element of the carrier of S * st w1 <= the_arity_of o holds
LBound o,w1 <= o

proof end;