:: On Ordering of Bags
:: by Gilbert Lee and Piotr Rudnicki
::
:: Received March 12, 2002
:: Copyright (c) 2002-2021 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, FINSEQ_1, ARYTM_1, ARYTM_3,
XXREAL_0, CARD_1, NAT_1, PRE_POLY, FUNCT_1, RELAT_1, TARSKI, CLASSES1,
CARD_3, FINSEQ_2, PBOOLE, GRAPH_2, VALUED_0, FINSUB_1, FINSET_1, RELAT_2,
ORDERS_2, WAYBEL_4, STRUCT_0, WELLFND1, WELLORD1, ORDERS_1, ORDINAL1,
WELLORD2, ORDINAL4, REAL_1, FUNCOP_1, FUNCT_4, PARTFUN1, DICKSON,
RLVECT_2, ZFMISC_1, MCART_1, BAGORDER, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, RELAT_1, PBOOLE,
RELAT_2, RELSET_1, PARTFUN1, FINSET_1, FINSUB_1, ORDINAL1, FUNCT_7,
XTUPLE_0, MCART_1, WELLORD1, ORDERS_1, WELLFND1, CARD_1, NUMBERS,
VALUED_0, XXREAL_0, XREAL_0, FUNCT_1, PRE_POLY, CARD_3, NAT_D, FINSEQ_1,
FINSEQ_2, RVSUM_1, WSIERP_1, FUNCOP_1, FUNCT_2, SEQ_4, DOMAIN_1,
FINSEQOP, CLASSES1, RECDEF_1, NAT_1, STRUCT_0, WAYBEL_0, YELLOW_1,
WAYBEL_4, PRALG_1, ORDERS_2, DICKSON;
constructors DOMAIN_1, FINSEQOP, NAT_D, WSIERP_1, PRALG_1, TRIANG_1, WAYBEL_4,
WELLFND1, DICKSON, RECDEF_1, BINOP_2, SEQ_4, CLASSES1, RELSET_1, FUNCT_7,
REAL_1, XTUPLE_0, WELLORD1, PRE_POLY, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2,
FINSET_1, FINSUB_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, CARD_1, MEMBERED,
FINSEQ_1, CARD_5, STRUCT_0, ORDERS_2, WAYBEL_0, YELLOW_1, DICKSON,
VALUED_0, XXREAL_2, RELSET_1, PRE_POLY, WELLORD1, WELLORD2, XTUPLE_0;
requirements SUBSET, NUMERALS, REAL, BOOLE, ARITHM;
begin :: Preliminaries
theorem :: BAGORDER:1
for x,y,z being set st z in x & z in y holds x \ {z} = y \ {z} implies x = y;
theorem :: BAGORDER:2
for n, k being Element of NAT holds k in Seg n
iff k-1 is Element of NAT & k-1 < n;
registration
let f be finite-support Function, X be set;
cluster f|X -> finite-support;
end;
::$CT
theorem :: BAGORDER:4
for fs being FinSequence of NAT holds Sum fs = 0 iff fs = (len fs) |-> 0;
definition
let n,i,j be Nat, b be ManySortedSet of n;
func (i,j)-cut b -> ManySortedSet of j-'i means
:: BAGORDER:def 1
for k being Element of NAT st k in j-'i holds it.k = b.(i+k);
end;
registration
let n,i,j be Nat, b be natural-valued ManySortedSet of n;
cluster (i,j)-cut b -> natural-valued;
end;
registration
let n,i,j be Element of NAT, b be finite-support ManySortedSet of n;
cluster (i,j)-cut b -> finite-support;
end;
theorem :: BAGORDER:5
for n,i being Nat, a,b being ManySortedSet of n holds
a = b iff (0,i+1)-cut a = (0,i+1)-cut b & (i+1,n)-cut a = (i+1,n)-cut b;
definition
let x be non empty set, n be non zero Element of NAT;
func Fin (x,n) -> set equals
:: BAGORDER:def 2
{y where y is Subset of x : y is finite & y is non empty & card y c= n};
end;
registration
let x be non empty set, n be non zero Element of NAT;
cluster Fin (x,n) -> non empty;
end;
theorem :: BAGORDER:6
for R being antisymmetric transitive non empty RelStr,
X being finite Subset of R st X <> {} holds
ex x being Element of R st x in X & x is_maximal_wrt X, the InternalRel of R;
theorem :: BAGORDER:7
for R being antisymmetric transitive non empty RelStr,
X being finite Subset of R st X <> {} holds
ex x being Element of R st x in X & x is_minimal_wrt X, the InternalRel of R;
theorem :: BAGORDER:8
for R being non empty antisymmetric transitive RelStr,
f being sequence of R st f is descending
holds for j, i being Nat st if.j & [f.j,f.i] in the InternalRel of R;
definition
let R be non empty RelStr, s be sequence of R;
attr s is non-increasing means
:: BAGORDER:def 3
for i being Nat holds [s.(i+1),s.i] in the InternalRel of R;
end;
theorem :: BAGORDER:9
for R being non empty transitive RelStr, f being sequence of R
st f is non-increasing holds for j, i being Nat st i;
begin :: More about bags
definition
let n be Ordinal, b be bag of n;
func TotDegree b -> Nat means
:: BAGORDER:def 4
ex f being FinSequence of NAT
st it = Sum f & f = b*SgmX(RelIncl n, support b);
end;
theorem :: BAGORDER:12
for n being Ordinal, b being bag of n, s being finite Subset of n,
f, g being FinSequence of NAT
st f = b*SgmX(RelIncl n, support b) & g = b*SgmX(RelIncl n, support b \/ s)
holds Sum f = Sum g;
theorem :: BAGORDER:13
for n being Ordinal, a, b being bag of n
holds TotDegree (a+b) = TotDegree a + TotDegree b;
theorem :: BAGORDER:14
for n be Ordinal, a,b being bag of n
st b divides a holds TotDegree(a-'b) = TotDegree(a) - TotDegree(b);
theorem :: BAGORDER:15
for n being Ordinal, b being bag of n holds TotDegree b = 0 iff b = EmptyBag n;
theorem :: BAGORDER:16
for i,j,n being Nat holds (i,j)-cut EmptyBag n = EmptyBag (j-'i);
theorem :: BAGORDER:17
for i,j,n being Nat, a,b being bag of n
holds (i,j)-cut (a+b) = (i,j)-cut(a) + (i,j)-cut(b);
::$CT 2
theorem :: BAGORDER:20
for n, m being Ordinal, b being bag of n st m in n holds b|m is bag of m;
theorem :: BAGORDER:21
for n being set, a, b being bag of n
st b divides a holds support b c= support a;
begin :: Some Special Orders (Section 4.4)
definition
let n be set;
mode TermOrder of n is Order of Bags n;
end;
notation
let n be Ordinal;
synonym LexOrder n for BagOrder n;
end;
definition :: Definition 4.59 - admissible (specific for Bags)
let n be Ordinal, T be TermOrder of n;
attr T is admissible means
:: BAGORDER:def 5
T is_strongly_connected_in Bags n &
(for a being bag of n holds [EmptyBag n, a] in T) &
for a, b, c being bag of n st [a, b] in T holds [a+c, b+c] in T;
end;
theorem :: BAGORDER:22 :: 4.61 i) Lexicographical order is admissible
for n being Ordinal holds LexOrder n is admissible;
registration
let n be Ordinal;
cluster LexOrder n -> admissible;
end;
registration
let n be Ordinal;
cluster admissible for TermOrder of n;
end;
theorem :: BAGORDER:23
for o being infinite Ordinal holds LexOrder o is non well-ordering;
definition
let n be Ordinal;
func InvLexOrder n -> TermOrder of n means
:: BAGORDER:def 6
for p,q being bag of n holds [p,q] in it iff p = q or
ex i being Ordinal st i in n & p.i < q.i &
for k being Ordinal st i in k & k in n holds p.k = q.k;
end;
theorem :: BAGORDER:24 :: Ex 4.61 ii
for n being Ordinal holds InvLexOrder n is admissible;
registration
let n be Ordinal;
cluster InvLexOrder n -> admissible;
end;
theorem :: BAGORDER:25
for o being Ordinal holds InvLexOrder o is well-ordering;
definition
let n be Ordinal, o be TermOrder of n such that
for a,b,c being bag of n st [a,b] in o holds [a+c, b+c] in o;
func Graded o -> TermOrder of n means
:: BAGORDER:def 7
for a, b being bag of n holds [a,b] in it iff
( TotDegree a < TotDegree b or TotDegree a = TotDegree b & [a,b] in o );
end;
theorem :: BAGORDER:26 :: Exercise 4.61: iiia
for n being Ordinal, o being TermOrder of n
st (for a,b,c being bag of n st [a,b] in o
holds [a+c, b+c] in o) & o is_strongly_connected_in Bags n
holds Graded o is admissible;
definition
let n be Ordinal;
func GrLexOrder n -> TermOrder of n equals
:: BAGORDER:def 8
Graded LexOrder n;
func GrInvLexOrder n -> TermOrder of n equals
:: BAGORDER:def 9 :: Ex 4.61: iiic
Graded InvLexOrder n;
end;
theorem :: BAGORDER:27
:: Ex 4.61: iiib
for n being Ordinal holds GrLexOrder n is admissible;
registration
let n be Ordinal;
cluster GrLexOrder n -> admissible;
end;
theorem :: BAGORDER:28
for o being infinite Ordinal holds GrLexOrder o is non well-ordering;
theorem :: BAGORDER:29
for n being Ordinal holds GrInvLexOrder n is admissible;
registration
let n be Ordinal;
cluster GrInvLexOrder n -> admissible;
end;
theorem :: BAGORDER:30
for o being Ordinal holds GrInvLexOrder o is well-ordering;
definition
let i,n be Nat, o1 be TermOrder of (i+1),
o2 be TermOrder of (n-'(i+1));
func BlockOrder(i,n,o1,o2) -> TermOrder of n means
:: BAGORDER:def 10
for p,q being bag of n holds [p,q] in it iff
(0,i+1)-cut p <> (0,i+1)-cut q & [(0,i+1)-cut p,(0,i+1)-cut q] in o1 or
(0,i+1)-cut p = (0,i+1)-cut q & [(i+1,n)-cut p,(i+1,n)-cut q] in o2;
end;
theorem :: BAGORDER:31 ::E_4_61_iv: :: Exercise 4.61: iv
for i,n being Nat, o1 being TermOrder of (i+1),
o2 being TermOrder of (n-'(i+1)) st o1 is admissible & o2 is admissible
holds BlockOrder(i,n,o1,o2) is admissible;
definition
let n be Nat;
func NaivelyOrderedBags n -> strict RelStr means
:: BAGORDER:def 11
the carrier of it = Bags n &
for x,y being bag of n holds [x,y] in the InternalRel of it iff x divides y;
end;
theorem :: BAGORDER:32
for n being Nat holds the carrier of product(n --> OrderedNAT) = Bags n;
theorem :: BAGORDER:33
for n being Nat holds NaivelyOrderedBags n = product (n --> OrderedNAT);
theorem :: BAGORDER:34 ::T_4_62: :: Theorem 4.62
for n being Nat, o be TermOrder of n st o is admissible
holds the InternalRel of NaivelyOrderedBags n c= o & o is well-ordering;
begin :: Ordering of finite subsets
definition
let R be connected non empty Poset,
X be Element of Fin the carrier of R such that
X is non empty;
func PosetMin X -> Element of R means
:: BAGORDER:def 12 :: FPOSMIN :
it in X & it is_minimal_wrt X, the InternalRel of R;
func PosetMax X -> Element of R means
:: BAGORDER:def 13
it in X & it is_maximal_wrt X, the InternalRel of R;
end;
definition
let R be connected non empty Poset;
func FinOrd-Approx R ->
sequence of bool[: Fin the carrier of R, Fin the carrier of R:] means
:: BAGORDER:def 14
dom it = NAT & it.0 = {[x,y] where x, y is Element of Fin the carrier of R :
x = {} or (x<>{} & y <> {} & PosetMax x <> PosetMax y &
[PosetMax x,PosetMax y] in the InternalRel of R)} &
for n being Nat holds
it.(n+1) = {[x,y] where x,y is Element of Fin the carrier of R :
x <> {} & y <> {} &
PosetMax x = PosetMax y & [x \{PosetMax x}, y \{PosetMax y}] in it.n};
end;
theorem :: BAGORDER:35
for R being connected non empty Poset,
x,y being Element of Fin the carrier of R
holds [x,y] in union rng FinOrd-Approx R iff x = {} or
x<>{} & y<>{} & PosetMax x <> PosetMax y &
[PosetMax x,PosetMax y] in the InternalRel of R or
x<>{} & y<>{} & PosetMax x = PosetMax y &
[x\{PosetMax x},y\{PosetMax y}] in union rng FinOrd-Approx R;
theorem :: BAGORDER:36
for R being connected non empty Poset,
x being Element of Fin the carrier of R
st x <> {} holds not [x,{}] in union rng FinOrd-Approx R;
theorem :: BAGORDER:37
for R being connected non empty Poset,
a being Element of Fin the carrier of R
holds a\{PosetMax a} is Element of Fin the carrier of R;
theorem :: BAGORDER:38
for R being connected non empty Poset
holds union (rng FinOrd-Approx R) is Order of Fin the carrier of R;
definition
let R be connected non empty Poset;
func FinOrd R -> Order of Fin (the carrier of R) equals
:: BAGORDER:def 15
union rng FinOrd-Approx R;
end;
definition
let R be connected non empty Poset;
func FinPoset R -> Poset equals
:: BAGORDER:def 16
RelStr (# Fin the carrier of R, FinOrd R #);
end;
registration
let R be connected non empty Poset;
cluster FinPoset R -> non empty;
end;
theorem :: BAGORDER:39
for R being connected non empty Poset,a,b being Element of FinPoset R
holds [a,b] in the InternalRel of FinPoset R iff
ex x,y being Element of Fin the carrier of R st a = x & b = y & (x = {} or
x<>{} & y<>{} & PosetMax x <> PosetMax y &
[PosetMax x,PosetMax y] in the InternalRel of R or
x<>{} & y<>{} & PosetMax x = PosetMax y &
[x\{PosetMax x},y\{PosetMax y}] in FinOrd R);
registration
let R be connected non empty Poset;
cluster FinPoset R -> connected;
end;
definition
let R be connected non empty RelStr, C be non empty set such that
R is well_founded and
C c= the carrier of R;
func MinElement (C,R)-> Element of R means
:: BAGORDER:def 17
it in C & it is_minimal_wrt C, the InternalRel of R;
end;
theorem :: BAGORDER:40
for R being non empty RelStr, s being sequence of R, j being Nat
st s is descending holds s^\j is descending;
theorem :: BAGORDER:41 :: Theorem 4:69
for R being connected non empty Poset
st R is well_founded holds FinPoset R is well_founded;