:: On Multiset Ordering
:: by Grzegorz Bancerek
::
:: Received December 31, 2015
:: Copyright (c) 2015-2018 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 TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELAT_2, FINSET_1, ARYTM_1,
ARYTM_3, FUNCT_1, PARTFUN1, BINOP_1, XXREAL_0, VALUED_0, NUMBERS, CARD_1,
MESFUNC1, STRUCT_0, ALGSTR_0, MONOID_1, ORDERS_2, PRE_POLY, BAGORD_2,
ZFMISC_1, NAT_1, FUNCOP_1, ORDERS_1, REWRITE1, FINSEQ_1, ORDINAL4,
GROEB_1, CARD_3, INTERVA1, MIDSP_1, GRAPH_2, MCART_1, BAGORDER;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELAT_1, RELAT_2,
RELSET_1, NECKLACE, FUNCT_1, PARTFUN1, BINOP_1, CARD_1, FINSEQ_1,
FINSEQ_2, FINSET_1, VALUED_0, NUMBERS, FUNCT_2, XXREAL_0, XCMPLX_0,
NAT_1, NAT_D, REWRITE1, GRAPH_2, STRUCT_0, ALGSTR_0, MONOID_1, ORDERS_2,
WAYBEL_4, PRE_POLY, FINSEQ_6;
constructors DOMAIN_1, RELSET_1, NECKLACE, BINOP_2, WAYBEL_4, REWRITE1,
GRAPH_2, NAT_D, MONOID_1, FINSEQ_6, PRE_POLY;
registrations XBOOLE_0, SUBSET_1, RELSET_1, ORDINAL1, XREAL_0, VALUED_0,
STRUCT_0, ORDERS_2, MONOID_0, CARD_1, PRE_POLY, FINSEQ_1, FINSET_1,
REWRITE1, NAT_1, RELAT_1, XTUPLE_0, FINSEQ_6;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
begin
theorem :: BAGORD_2:1
for m,n being Nat holds n = (m-'(m-'n))+(n-'m);
theorem :: BAGORD_2:2
for n,m being Nat holds m-'n >= m-n;
theorem :: BAGORD_2:3
for m,n,x,y being Nat st n = (m-'x)+y holds m-'n <= x & n-'m <= y;
theorem :: BAGORD_2:4
for m,n,x,y being Nat st x <= m & n = (m-'x)+y holds x-'(m-'n) = y-'(n-'m);
theorem :: BAGORD_2:5
for k,x1,x2,y1,y2 being Nat st x2 <= k & x1 <= (k-'x2)+y2
holds x2+(x1-'y2) <= k &
(((k-'x2)+y2)-'x1)+y1 = (k-'(x2+(x1-'y2)))+((y2-'x1)+y1);
theorem :: BAGORD_2:6
for x,y being Nat st x+y > 0 holds x > 0 or y > 0;
reserve a,b for object, I,J for set;
registration
let I; let J be non empty set;
cluster -> total for Function of I,J;
end;
registration
cluster asymmetric transitive non empty for RelStr;
end;
registration
let I;
cluster asymmetric transitive for Relation of I;
end;
registration
let R be transitive RelStr;
cluster the InternalRel of R -> transitive;
end;
registration
let R be asymmetric RelStr;
cluster the InternalRel of R -> asymmetric;
end;
registration
let I;
let p,q be I-valued FinSequence;
cluster p^q -> I-valued;
end;
theorem :: BAGORD_2:7
for p,q being FinSequence st p^q is I-valued
holds p is I-valued & q is I-valued;
registration
let I;
let f be I-valued FinSequence;
let n be Nat;
cluster f|n -> I-valued;
end;
theorem :: BAGORD_2:8
for p being FinSequence st a in rng p
ex q,r being FinSequence st p = q^<*a*>^r;
theorem :: BAGORD_2:9
for p,q being FinSequence holds p c< q iff len p < len q &
for i being Nat st i in dom p holds p.i = q.i;
theorem :: BAGORD_2:10
for p,q,r being FinSequence holds r^p c< r^q iff p c< q;
definition
let R be asymmetric non empty RelStr;
let x,y be Element of R;
redefine pred x <= y;
asymmetry;
end;
theorem :: BAGORD_2:11
for R being asymmetric non empty RelStr
for x,y being Element of R holds x <= y iff x < y;
begin
definition
let I;
mode multiset of I is Element of finite-MultiSet_over I;
end;
registration
let I;
cluster -> I-defined natural-valued for multiset of I;
end;
registration
let I;
cluster -> total for multiset of I;
end;
definition
let m be natural-valued Function;
redefine func support m equals
:: BAGORD_2:def 1
m"(NAT\{0});
end;
registration
let I;
cluster -> finite-support for multiset of I;
end;
theorem :: BAGORD_2:12
a is multiset of I iff a is bag of I;
theorem :: BAGORD_2:13
1.finite-MultiSet_over I = EmptyBag I;
definition
let R be RelStr;
let x,y be Element of R;
pred x ## y means
:: BAGORD_2:def 2
not x <= y & not y <= x;
symmetry;
end;
definition
struct(multMagma,RelStr) RelMultMagma (#
carrier -> set,
multF -> BinOp of the carrier,
InternalRel -> Relation of the carrier
#);
end;
definition
struct(multLoopStr,RelStr) RelMonoid (#
carrier -> set,
multF -> BinOp of the carrier,
OneF -> Element of the carrier,
InternalRel -> Relation of the carrier
#);
end;
definition
let M be multLoopStr;
mode RelExtension of M -> RelMonoid means
:: BAGORD_2:def 3
the multLoopStr of it = the multLoopStr of M;
end;
registration
let M be non empty multLoopStr;
cluster -> non empty for RelExtension of M;
end;
registration
let M be multLoopStr;
cluster strict for RelExtension of M;
end;
theorem :: BAGORD_2:14
for N being multLoopStr, M being RelExtension of N holds
a is Element of M iff a is Element of N;
theorem :: BAGORD_2:15
for N being multLoopStr, M being RelExtension of N holds 1.N = 1.M;
registration
let I;
let M be RelExtension of finite-MultiSet_over I;
cluster -> Function-like Relation-like for Element of M;
end;
registration
let I;
let M be RelExtension of finite-MultiSet_over I;
cluster -> I-defined natural-valued finite-support for Element of M;
end;
registration
let I;
let M be RelExtension of finite-MultiSet_over I;
cluster -> total for Element of M;
end;
theorem :: BAGORD_2:16
for M being RelExtension of finite-MultiSet_over I holds
the carrier of M = Bags I;
scheme :: BAGORD_2:sch 1
RelEx{M() -> non empty multLoopStr, R[object,object]}:
ex N being strict RelExtension of M() st
for x,y being Element of N holds x <= y iff R[x,y];
theorem :: BAGORD_2:17
for N being multLoopStr, M1,M2 being strict RelExtension of N
st for m,n being Element of M1 for x,y being Element of M2 st m = x & n = y
holds m <= n iff x <= y
holds M1 = M2;
begin
definition
let R be non empty RelStr;
func DershowitzMannaOrder R -> strict RelExtension of
finite-MultiSet_over the carrier of R means
:: BAGORD_2:def 4
for m,n being Element of it holds m <= n iff ex x,y being Element of it st
1.it <> x divides n & m = (n -' x) + y &
for b being Element of R st y.b > 0
ex a being Element of R st x.a > 0 & b <= a;
end;
theorem :: BAGORD_2:18
for m,n being bag of I holds n = (m-'(m-'n))+(n-'m);
theorem :: BAGORD_2:19
for m,n,x,y being bag of I st n = (m-'x)+y holds m-'n divides x &
n-'m divides y;
theorem :: BAGORD_2:20
for m,n,x,y being bag of I st x divides m & n = (m-'x)+y holds
x-'(m-'n) = y-'(n-'m);
theorem :: BAGORD_2:21
for m,x,y being bag of I st x divides m & x <> y holds m <> (m-'x)+y;
theorem :: BAGORD_2:22
for I being non empty set, R being Relation of I
for r being RedSequence of R
st len r > 1 holds r.len r in I;
theorem :: BAGORD_2:23
for R being asymmetric transitive Relation of I
for r being RedSequence of R holds r is one-to-one;
theorem :: BAGORD_2:24
for R being asymmetric transitive non empty RelStr
for X being set st X is finite & ex x being Element of R st x in X
ex x being Element of R st x is_maximal_in X;
theorem :: BAGORD_2:25
for m,n being bag of I holds m-'n divides m;
registration
let I;
cluster -> Function-like Relation-like for Element of Bags I;
end;
theorem :: BAGORD_2:26
for m,n being bag of I holds
m-'n <> EmptyBag I or m = n or n-'m <> EmptyBag I;
definition
let R being asymmetric transitive non empty RelStr;
redefine func DershowitzMannaOrder R means
:: BAGORD_2:def 5
for m,n being Element of it holds m <= n iff m <> n &
for a being Element of R st m.a > n.a
ex b being Element of R st a <= b & m.b < n.b;
end;
theorem :: BAGORD_2:27
for k,x1,x2,y1,y2 being bag of I st x2 divides k & x1 divides (k-'x2)+y2
holds x2+(x1-'y2) divides k &
(((k-'x2)+y2)-'x1)+y1 = (k-'(x2+(x1-'y2)))+((y2-'x1)+y1);
registration
let R be asymmetric transitive non empty RelStr;
cluster DershowitzMannaOrder R -> asymmetric transitive;
end;
definition
let I;
func DivOrder I -> Relation of Bags I means
:: BAGORD_2:def 6
for b1,b2 being bag of I holds [b1,b2] in it iff b1 <> b2 & b1 divides b2;
end;
theorem :: BAGORD_2:28
for a,b,c being bag of I st a divides b divides c holds a divides c;
registration
let I;
cluster DivOrder I -> asymmetric transitive;
end;
theorem :: BAGORD_2:29
for R being asymmetric transitive non empty RelStr holds
DivOrder the carrier of R c= the InternalRel of DershowitzMannaOrder R;
theorem :: BAGORD_2:30
for R being asymmetric transitive non empty RelStr
st the InternalRel of R is empty
holds the InternalRel of DershowitzMannaOrder R = DivOrder the carrier of R;
theorem :: BAGORD_2:31
for R1,R2 being asymmetric transitive non empty RelStr
st the carrier of R1 = the carrier of R2 &
the InternalRel of R1 c= the InternalRel of R2
holds the InternalRel of DershowitzMannaOrder R1
c= the InternalRel of DershowitzMannaOrder R2;
begin
definition
let I;
let f be (Bags I)-valued FinSequence;
func Sum f -> bag of I means
:: BAGORD_2:def 7
ex F being Function of NAT, Bags I st
it = F.len f &
F.0 = EmptyBag I &
for i being Nat
for b being bag of I
st i < len f & b = f.(i + 1)
holds F.(i + 1) = F.i + b;
end;
theorem :: BAGORD_2:32
Sum (<*>Bags I) = EmptyBag I;
registration
let I;
let b be bag of I;
cluster <*b*> -> Bags I-valued for FinSequence;
end;
theorem :: BAGORD_2:33
for p being Bags I-valued FinSequence, b being bag of I holds
Sum (p^<*b*>) = Sum p + b;
reserve b for bag of I;
theorem :: BAGORD_2:34
Sum <*b*> = b;
theorem :: BAGORD_2:35
for p,q being Bags I-valued FinSequence holds
Sum (p^q) = Sum p + Sum q;
theorem :: BAGORD_2:36
for p being Bags I-valued FinSequence holds Sum (<*b*>^p) = b + Sum p;
theorem :: BAGORD_2:37
for p being Bags I-valued FinSequence st b in rng p holds b divides Sum p;
theorem :: BAGORD_2:38
for p being Bags I-valued FinSequence, i being object st i in support Sum p
ex b st b in rng p & i in support b;
definition
let I,b;
mode partition of b -> Bags I-valued FinSequence means
:: BAGORD_2:def 8
b = Sum it;
end;
definition
let I,b;
redefine func <*b*> -> partition of b;
end;
definition
let R be RelStr;
let M be RelExtension of finite-MultiSet_over the carrier of R;
let b be Element of M;
let p be partition of b;
attr p is co-ordered means
:: BAGORD_2:def 9
for i being Nat st i in dom p & i+1 in dom p
for b1,b2 being Element of M st b1 = p.i & b2 = p.(i+1) holds b2 <= b1;
end;
definition
let R be non empty RelStr;
let b be bag of the carrier of R;
let p be partition of b;
attr p is ordered means
:: BAGORD_2:def 10
(for m being bag of the carrier of R st m in rng p
for x being Element of R st m.x > 0 holds m.x = b.x) &
(for m being bag of the carrier of R st m in rng p
for x,y being Element of R st m.x > 0 & m.y > 0 & x <> y
holds x ## y) &
(for m being bag of the carrier of R st m in rng p
holds m <> EmptyBag the carrier of R) &
(for i being Nat st i in dom p & i+1 in dom p
for x being Element of R st (p/.(i+1)).x > 0
ex y being Element of R st (p/.i).y > 0 & x <= y);
end;
reserve R for asymmetric transitive non empty RelStr,
a,b,c for bag of the carrier of R,
x,y,z for Element of R;
theorem :: BAGORD_2:39
<*a*> is ordered iff a <> EmptyBag the carrier of R &
for x,y st a.x > 0 & a.y > 0 & x <> y holds x ## y;
theorem :: BAGORD_2:40
for p being Bags I-valued FinSequence
for a,b being bag of I holds
<*a*>^p is partition of b iff a divides b & p is partition of b-'a;
reserve p for partition of b-'a, q for partition of b;
theorem :: BAGORD_2:41
q = <*a*>^p & q is ordered implies p is ordered;
definition
let I;
let m be bag of I;
let J be set;
func m|J -> bag of I means
:: BAGORD_2:def 11
for i being object st i in I holds (i in J implies it.i = m.i) &
(not i in J implies it.i = 0);
end;
reserve J for set, m for bag of I;
theorem :: BAGORD_2:42
support (m|J) = J /\ support m;
theorem :: BAGORD_2:43
(m|J)+(m|(I\J)) = m;
theorem :: BAGORD_2:44
m|J divides m;
theorem :: BAGORD_2:45
support m c= J implies m|J = m;
theorem :: BAGORD_2:46
support(m-'(m|J)) = (support m)\J;
theorem :: BAGORD_2:47
q is ordered & q = <*a*>^p & a.x > 0 implies a.x = b.x;
theorem :: BAGORD_2:48
q is ordered & q = <*a*>^p & a.x > 0 & a.y > 0 & x <> y implies x ## y;
theorem :: BAGORD_2:49
q is ordered & q = <*a*>^p implies a <> EmptyBag the carrier of R;
theorem :: BAGORD_2:50
for c being bag of the carrier of R,
r being Bags the carrier of R-valued FinSequence
st q is ordered & q = <*a,c*>^r & c.y > 0
ex x st a.x > 0 & y <= x;
theorem :: BAGORD_2:51
x in I & (for y st y in I & y <> x holds x ## y) implies x is_maximal_in I;
theorem :: BAGORD_2:52
q is ordered & q = <*a*>^p & c in rng p & c.x > 0 implies
ex y st a.y > 0 & x <= y;
theorem :: BAGORD_2:53
q is ordered & q = <*a*>^p implies (x is_maximal_in support b iff a.x > 0);
theorem :: BAGORD_2:54
q is ordered & q = <*a*>^p implies a = b|{x:x is_maximal_in support b};
theorem :: BAGORD_2:55
for p being Bags I-valued FinSequence st Sum p = EmptyBag I &
for a being bag of I st a in rng p holds a <> EmptyBag I
holds p = {};
theorem :: BAGORD_2:56
for a,b being bag of I st a <> EmptyBag I holds a+b <> EmptyBag I;
theorem :: BAGORD_2:57
for p,q being partition of b st p is ordered & q is ordered holds p = q;
definition
let I;
let a,b be bag of I;
redefine func [a,b] -> Element of [:Bags I,Bags I:];
end;
theorem :: BAGORD_2:58
a <> EmptyBag the carrier of R implies {x:x is_maximal_in support a} <> {};
definition
let R,b;
func OrderedPartition b -> Bags the carrier of R-valued FinSequence means
:: BAGORD_2:def 12
ex F,G being Function of NAT, Bags the carrier of R st F.0 = b &
G.0 = EmptyBag the carrier of R &
(for i being Nat holds G.(i+1) = (F.i)|{x:x is_maximal_in support (F.i)} &
F.(i+1) = (F.i)-'(G.(i+1))) &
ex i being Nat st F.i = EmptyBag the carrier of R & it = G|Seg i &
for j being Nat st j < i holds F.j <> EmptyBag the carrier of R;
end;
definition
let R,b;
redefine func OrderedPartition b -> partition of b;
end;
registration
let R,b;
cluster OrderedPartition b -> ordered for partition of b;
end;
theorem :: BAGORD_2:59
b = EmptyBag the carrier of R iff OrderedPartition b = {};
definition
let R;
func PrecM R -> strict RelExtension of finite-MultiSet_over the carrier of R
means
:: BAGORD_2:def 13
for m,n being Element of it holds m <= n iff m <> n &
for x st m.x > 0 holds m.x < n.x or ex y st n.y > 0 & x <= y;
end;
registration
let R;
cluster PrecM R -> asymmetric transitive;
end;
definition
let I;
let R be Relation of I,I;
func LexOrder(I,R) -> Relation of I* means
:: BAGORD_2:def 14
for p,q being I-valued FinSequence holds [p,q] in it iff p c< q or
ex k being Nat st k in dom p & k in dom q & [p.k,q.k] in R &
for n being Nat st 1 <= n < k holds p.n = q.n;
end;
registration
let I;
let R be transitive Relation of I;
cluster LexOrder(I,R) -> transitive;
end;
registration
let I;
let R be asymmetric Relation of I;
cluster LexOrder(I,R) -> asymmetric;
end;
theorem :: BAGORD_2:60
for R being asymmetric Relation of I
for p,q,r being I-valued FinSequence holds
[p,q] in LexOrder(I,R) iff [r^p,r^q] in LexOrder(I,R);
definition
let R;
func PrecPrecM R -> strict RelExtension of
finite-MultiSet_over the carrier of R means
:: BAGORD_2:def 15
for m,n being Element of it holds m <= n iff
[OrderedPartition m, OrderedPartition n] in
LexOrder(the carrier of PrecM R, the InternalRel of PrecM R);
end;
registration
let R;
cluster PrecPrecM R -> asymmetric transitive;
end;
theorem :: BAGORD_2:61
for a,b being Element of DershowitzMannaOrder R st a <= b
holds b <> EmptyBag the carrier of R;
theorem :: BAGORD_2:62
for a,b,c,d being Element of DershowitzMannaOrder R
for e being bag of the carrier of R st a <= b & e divides a & e divides b
holds c = a-'e & d = b-'e implies c <= d;
theorem :: BAGORD_2:63
for p being Bags I-valued FinSequence, x being object
st x in I & (Sum p).x > 0
ex i being Nat st i in dom p & (p/.i).x > 0;
theorem :: BAGORD_2:64
q is ordered & (q/.1).x = 0 & b.x > 0 implies
ex y st (q/.1).y > 0 & x <= y;