:: Extended Natural Numbers and Counters
:: by Sebastian Koch
::
:: Received October 25, 2020
:: Copyright (c) 2020-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, RELAT_1, TARSKI, XBOOLE_0, FUNCT_1, MEMBERED, SUBSET_1,
XCMPLX_0, XXREAL_0, INT_1, ORDINAL1, FUNCOP_1, FUNCT_4, FUNCT_2,
ZFMISC_1, ORDINAL2, ARYTM_3, NAT_1, SETFAM_1, CARD_1, AOFA_I00, CARD_3,
AFINSQ_1, PARTFUN1, ORDINAL4, CARD_2, VALUED_0, REAL_1, FINSET_1,
FUNCT_7, XXREAL_2, PBOOLE, COUNTERS;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1,
FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, FUNCT_4,
ORDINAL2, FINSET_1, CARD_1, PBOOLE, CARD_3, NUMBERS, XXREAL_0, XREAL_0,
INT_1, RAT_1, MEMBERED, VALUED_0, CARD_2, XXREAL_2, XXREAL_3, XCMPLX_0,
NAT_1, ORDINAL4, AFINSQ_1, AOFA_I00;
constructors XCMPLX_0, RAT_1, MEMBERED, FUNCOP_1, FUNCT_4, XXREAL_0, PARTFUN1,
NAT_1, SETFAM_1, RELSET_1, NUMBERS, XXREAL_3, FINSET_1, VALUED_0,
XXREAL_2, ENUMSET1, INT_1, CARD_1, PBOOLE, AOFA_I00, AFINSQ_1, CARD_2;
registrations MEMBERED, RELAT_1, FUNCOP_1, XREAL_0, RAT_1, ORDINAL1, INT_1,
FUNCT_1, XBOOLE_0, RELSET_1, FUNCT_2, SETFAM_1, SUBSET_1, PBOOLE, NAT_1,
NUMBERS, XXREAL_0, XXREAL_3, CARD_1, VALUED_0, XXREAL_2, FOMODEL0,
FINSET_1, AFINSQ_1, CAYLDICK, ORDINAL2, CARD_3, CATALG_1, ZFMISC_1,
CARD_2, CARD_5, ORDINAL4;
requirements SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
begin :: Extended natural numbers
definition
func ExtNAT -> Subset of ExtREAL equals
:: COUNTERS:def 1
NAT \/ {+infty};
end;
theorem :: COUNTERS:1
NAT c< ExtNAT & ExtNAT c< ExtREAL;
registration
cluster ExtNAT -> non empty infinite;
end;
definition
let x be object;
attr x is ext-natural means
:: COUNTERS:def 2
x in ExtNAT;
end;
registration
cluster +infty -> ext-natural;
cluster ext-natural -> ext-real for object;
cluster natural -> ext-natural for object;
cluster finite ext-natural -> natural for set;
end;
registration
cluster zero ext-natural for object;
cluster non zero ext-natural for object;
cluster ext-natural for number;
cluster -> ext-natural for Element of ExtNAT;
end;
definition
mode ExtNat is ext-natural ExtReal;
end;
registration
let x be ExtNat;
reduce In(x,ExtNAT) to x;
end;
registration
sethood of ExtNat;
end;
theorem :: COUNTERS:2
for x being object holds x is ExtNat iff x is Nat or x = +infty;
registration
cluster zero -> ext-natural for object;
cluster ext-natural -> non negative for ExtReal;
end;
registration
cluster -> non negative for ExtNat;
cluster non zero -> positive for ExtNat;
end;
reserve N,M,K for ExtNat;
registration
let N,M;
cluster min(N,M) -> ext-natural;
cluster max(N,M) -> ext-natural;
cluster N + M -> ext-natural;
cluster N * M -> ext-natural;
end;
theorem :: COUNTERS:3
0 <= N;
theorem :: COUNTERS:4
0 <> N implies 0 < N;
theorem :: COUNTERS:5
0 < N + 1;
theorem :: COUNTERS:6
M in NAT & N <= M implies N in NAT;
theorem :: COUNTERS:7
N < M implies N in NAT;
theorem :: COUNTERS:8
N <= M implies N * K <= M * K;
theorem :: COUNTERS:9
N = 0 or ex K st N = K + 1;
theorem :: COUNTERS:10
N + M = 0 implies N = 0 & M = 0;
registration
let M be ExtNat, N be non zero ExtNat;
cluster M + N -> non zero;
cluster N + M -> non zero;
end;
theorem :: COUNTERS:11
N <= M + 1 implies N <= M or N = M + 1;
theorem :: COUNTERS:12
N <= M & M <= N + 1 implies N = M or M = N + 1;
theorem :: COUNTERS:13
N <= M implies ex K st M = N + K;
theorem :: COUNTERS:14
N <= N + M;
theorem :: COUNTERS:15
N <= M implies N <= M + K;
theorem :: COUNTERS:16
N < 1 implies N = 0;
theorem :: COUNTERS:17
N * M = 1 implies N = 1;
theorem :: COUNTERS:18
K < K + N iff 1 <= N & K <> +infty;
theorem :: COUNTERS:19
K <> 0 & N = M * K implies M <= N;
theorem :: COUNTERS:20
M <= N implies M * K <= N * K;
theorem :: COUNTERS:21
K + M + N = K + (M + N);
theorem :: COUNTERS:22
K * (N+M) = K*N + K*M;
begin :: Sets of extended natural numbers
definition
let X be set;
attr X is ext-natural-membered means
:: COUNTERS:def 3
for x being object holds x in X implies x is ext-natural;
end;
registration
cluster empty -> ext-natural-membered for set;
cluster natural-membered -> ext-natural-membered for set;
cluster ext-natural-membered -> ext-real-membered for set;
cluster ExtNAT -> ext-natural-membered;
end;
registration
cluster non empty ext-natural-membered for set;
end;
theorem :: COUNTERS:23
for X being set holds X is ext-natural-membered iff X c= ExtNAT;
reserve X for ext-natural-membered set;
registration
let X;
cluster -> ext-natural for Element of X;
end;
theorem :: COUNTERS:24
for X being non empty ext-natural-membered set ex N st N in X;
theorem :: COUNTERS:25
(for N holds N in X) implies X = ExtNAT;
theorem :: COUNTERS:26
for Y being set st Y c= X holds Y is ext-natural-membered;
registration
let X;
cluster -> ext-natural-membered for Subset of X;
end;
registration
let N;
cluster {N} -> ext-natural-membered;
let M;
cluster {N,M} -> ext-natural-membered;
let K;
cluster {N,M,K} -> ext-natural-membered;
end;
registration
let X; let Y be ext-natural-membered set;
cluster X \/ Y -> ext-natural-membered;
end;
registration
let X; let Y be set;
cluster X /\ Y -> ext-natural-membered;
cluster X \ Y -> ext-natural-membered;
end;
registration
let X; let Y be ext-natural-membered set;
cluster X \+\ Y -> ext-natural-membered;
end;
definition
let X; let Y be set;
redefine pred X c= Y means
:: COUNTERS:def 4
N in X implies N in Y;
end;
definition
let X; let Y be ext-natural-membered set;
redefine pred X = Y means
:: COUNTERS:def 5
N in X iff N in Y;
end;
definition
let X; let Y be ext-natural-membered set;
redefine pred X misses Y means
:: COUNTERS:def 6
not ex N st N in X & N in Y;
end;
theorem :: COUNTERS:27
for F being set st(for X being set st X in F holds X is ext-natural-membered)
holds union F is ext-natural-membered;
theorem :: COUNTERS:28
for F, X being set st X in F & X is ext-natural-membered
holds meet F is ext-natural-membered;
scheme :: COUNTERS:sch 1
ENMSeparation {P[object]}:
ex X being ext-natural-membered set st for N holds N in X iff P[N];
definition
let X be ext-natural-membered set;
redefine mode UpperBound of X means
:: COUNTERS:def 7
for N holds N in X implies N <= it;
redefine mode LowerBound of X means
:: COUNTERS:def 8
for N holds N in X implies it <= N;
end;
registration
cluster -> bounded_below for ext-natural-membered set;
cluster non empty -> left_end for ext-natural-membered set;
end;
registration
let X;
cluster ext-natural for UpperBound of X;
cluster ext-natural for LowerBound of X;
cluster inf X -> ext-natural;
end;
registration
let X be non empty ext-natural-membered set;
cluster sup X -> ext-natural;
end;
registration
cluster non empty bounded_above -> right_end for ext-natural-membered set;
end;
definition
let X be left_end ext-natural-membered set;
redefine func min X -> ExtNat means
:: COUNTERS:def 9
it in X & for N st N in X holds it <= N;
end;
definition
let X be right_end ext-natural-membered set;
redefine func max X -> ExtNat means
:: COUNTERS:def 10
it in X & for N st N in X holds N <= it;
end;
begin :: Relations with extended natural numbers in range
definition
let R be Relation;
attr R is ext-natural-valued means
:: COUNTERS:def 11
rng R c= ExtNAT;
end;
registration
cluster empty -> ext-natural-valued for Relation;
cluster natural-valued -> ext-natural-valued for Relation;
cluster ext-natural-valued -> ExtNAT-valued ext-real-valued for Relation;
cluster ExtNAT-valued -> ext-natural-valued for Relation;
end;
registration
cluster ext-natural-valued for Function;
end;
registration
let R be ext-natural-valued Relation;
cluster rng R -> ext-natural-membered;
end;
theorem :: COUNTERS:29
for R being Relation, S being ext-natural-valued Relation st R c= S
holds R is ext-natural-valued;
registration
let R be ext-natural-valued Relation;
cluster -> ext-natural-valued for Subset of R;
end;
registration
let R, S be ext-natural-valued Relation;
cluster R \/ S -> ext-natural-valued;
end;
registration
let R be ext-natural-valued Relation, S be Relation;
cluster R /\ S -> ext-natural-valued;
cluster R \ S -> ext-natural-valued;
cluster S * R -> ext-natural-valued;
end;
registration
let R, S be ext-natural-valued Relation;
cluster R \+\ S -> ext-natural-valued;
end;
registration
let R be ext-natural-valued Relation, X be set;
cluster R.:X -> ext-natural-membered;
cluster R|X -> ext-natural-valued;
cluster X|`R -> ext-natural-valued;
end;
registration
let R be ext-natural-valued Relation, x be object;
cluster Im(R,x) -> ext-natural-membered;
end;
registration
let X;
cluster id X -> ext-natural-valued;
end;
definition
let f be Function;
redefine attr f is ext-natural-valued means
:: COUNTERS:def 12
for x being object st x in dom f holds f.x is ext-natural;
end;
theorem :: COUNTERS:30
for f being Function holds
f is ext-natural-valued iff for x being object holds f.x is ext-natural;
registration
let f be ext-natural-valued Function;
let x be object;
cluster f.x -> ext-natural;
end;
registration
let X be set; let N;
cluster X --> N -> ext-natural-valued;
end;
registration
let f,g be ext-natural-valued Function;
cluster f +* g -> ext-natural-valued;
end;
registration
let x be object; let N;
cluster x .--> N -> ext-natural-valued;
end;
registration
let Z be set; let X;
cluster -> ext-natural-valued for Relation of Z,X;
end;
registration
let Z be set; let X;
cluster [: Z, X :] -> ext-natural-valued for Relation of Z,X;
end;
registration
cluster non empty constant ext-natural-valued for Function;
end;
theorem :: COUNTERS:31
for f being non empty constant ext-natural-valued Function
ex N st for x being object st x in dom f holds f.x = N;
begin :: Ordinal preliminaries
:: into ORDINAL1 ?
theorem :: COUNTERS:32
for f being Function holds f is Ordinal-yielding iff
for x being object st x in dom f holds f.x is Ordinal;
:: into ORDINAL1 ?
registration
cluster ordinal -> c=-linear for set;
end;
:: into ORDINAL1 ? ::: generalize in ORDINAL2
registration
let f be Ordinal-yielding Function, x be object;
cluster f.x -> ordinal;
end;
:: into ORDINAL4 ?
registration
let A, B be non-empty Sequence;
cluster A^B -> non-empty;
end;
:: into CARD_1 ? ::: version of CARD_1:64
theorem :: COUNTERS:33
for X being set, x being object holds card(X --> x) = card X;
:: generalization of CARD_1:64
:: into CARD_1 ?
theorem :: COUNTERS:34
for c being Cardinal, x being object holds card(c --> x) = c;
:: into CARD_1 ?
registration
let X be trivial set;
cluster card X -> trivial;
end;
:: into CARD_2 ?
registration
let c1 be Cardinal, c2 be non empty Cardinal;
cluster c1 +` c2 -> non empty;
end;
:: into CARD_2 ?
theorem :: COUNTERS:35
for A being Ordinal holds A <> 0 & A <> 1 iff A is non trivial;
:: into CARD_2 ?
theorem :: COUNTERS:36
for A being Ordinal, B being infinite Cardinal st A in B holds A +^ B = B;
:: into CARD_3 ?
registration
let f be Cardinal-yielding Function, g be Function;
cluster f*g -> Cardinal-yielding;
end;
:: into CARD_3 ?
registration
cluster natural-valued -> Cardinal-yielding for Function;
end;
:: into CARD_3 ?
registration
let f be empty Function;
cluster disjoin f -> empty;
end;
:: into CARD_3 ?
registration
let f be empty-yielding Function;
cluster disjoin f -> empty-yielding;
end;
:: into CARD_3 ?
registration
let f be non empty-yielding Function;
cluster disjoin f -> non empty-yielding;
end;
:: into CARD_3 ?
registration
let f be empty-yielding Function;
cluster Union f -> empty;
end;
:: into CARD_3 ?
registration
cluster Cardinal-yielding -> Ordinal-yielding for Function;
end;
:: into CARD_3 ?
theorem :: COUNTERS:37
for f being Function, p being Permutation of dom f
holds Card(f*p) = (Card f)*p;
:: into CARD_3 ?
registration
let A be Sequence;
cluster Card A -> Sequence-like;
end;
:: into CARD_3 ?
theorem :: COUNTERS:38
for A, B being Sequence holds Card(A^B) = (Card A)^(Card B);
:: into CARD_3 ?
registration
let f be trivial Function;
cluster Card f -> trivial;
end;
:: into CARD_3 ?
registration
let f be non trivial Function;
cluster Card f -> non trivial;
end;
:: into CARD_3 ?
registration
let A, B be Cardinal-yielding Sequence;
cluster A^B -> Cardinal-yielding;
end;
:: into CARD_3 or AFINSQ_1 ?
registration
let c1 be Cardinal;
cluster <% c1 %> -> Cardinal-yielding;
let c2 be Cardinal;
cluster <% c1, c2 %> -> Cardinal-yielding;
let c3 be Cardinal;
cluster <% c1, c2, c3 %> -> Cardinal-yielding;
end;
:: into CARD_3 or AFINSQ_1 ?
registration
let X1, X2, X3 be non empty set;
cluster <% X1, X2, X3 %> -> non-empty;
end;
:: into AFINSQ_1 ?
registration
let A be infinite Ordinal;
cluster <% A %> -> non natural-valued;
let x be object;
cluster <% A, x %> -> non natural-valued;
cluster <% x, A %> -> non natural-valued;
let y be object;
cluster <% A, x, y %> -> non natural-valued;
cluster <% x, A, y %> -> non natural-valued;
cluster <% x, y, A %> -> non natural-valued;
end;
:: into AFINSQ_1 ?
registration
cluster non empty non-empty natural-valued for XFinSequence;
let x be object;
cluster <% x %> -> one-to-one;
end;
:: into AFINSQ_1 ?
theorem :: COUNTERS:39
for x, y being object holds dom <% x, y %> = {0,1} & rng <% x, y %> = {x,y};
:: into AFINSQ_1 ?
theorem :: COUNTERS:40
for x,y,z being object holds dom<% x,y,z %>={0,1,2} & rng<% x,y,z %>={x,y,z};
:: into AFINSQ_1 ?
registration
let x be object;
cluster <% x %> -> trivial;
let y be object;
cluster <% x, y %> -> non trivial;
let z be object;
cluster <% x, y, z %> -> non trivial;
end;
:: into AFINSQ_1 ?
registration
cluster non empty trivial for XFinSequence;
let D be non empty set;
cluster non empty trivial for XFinSequence of D;
end;
:: into AFINSQ_1 ?
theorem :: COUNTERS:41
for p being non empty trivial Sequence
ex x being object st p = <% x %>;
:: into AFINSQ_1 ?
theorem :: COUNTERS:42
for D being non empty set, p being non empty trivial Sequence of D
ex x being Element of D st p = <% x %>;
:: into AFINSQ_1 ?
theorem :: COUNTERS:43
<% 0 %> = id 1;
:: into AFINSQ_1 ?
theorem :: COUNTERS:44
<% 0, 1 %> = id 2;
:: into AFINSQ_1 ?
theorem :: COUNTERS:45
<% 0, 1, 2 %> = id 3;
:: into AFINSQ_1 ?
theorem :: COUNTERS:46
for x, y being object holds <% x, y %> * <% 1, 0 %> = <% y, x %>;
:: into AFINSQ_1 ?
theorem :: COUNTERS:47
for x, y, z being object holds <% x, y, z %> * <% 0, 2, 1 %> = <% x, z, y %>;
:: into AFINSQ_1 ?
theorem :: COUNTERS:48
for x, y, z being object holds <% x, y, z %> * <% 1, 0, 2 %> = <% y, x, z %>;
:: into AFINSQ_1 ?
theorem :: COUNTERS:49
for x, y, z being object holds <% x, y, z %> * <% 1, 2, 0 %> = <% y, z, x %>;
:: into AFINSQ_1 ?
theorem :: COUNTERS:50
for x, y, z being object holds <% x, y, z %> * <% 2, 0, 1 %> = <% z, x, y %>;
:: into AFINSQ_1 ?
theorem :: COUNTERS:51
for x, y, z being object holds <% x, y, z %> * <% 2, 1, 0 %> = <% z, y, x %>;
:: into AFINSQ_1 ?
theorem :: COUNTERS:52
for x,y being object st x <> y holds <% x, y %> is one-to-one;
:: into AFINSQ_1 ?
theorem :: COUNTERS:53
for x,y,z being object st x <> y & x <> z & y <> z
holds <% x, y, z %> is one-to-one;
begin :: Relations with cardinal domain
definition
let R be Relation;
attr R is with_cardinal_domain means
:: COUNTERS:def 13
ex c being Cardinal st dom R = c;
end;
registration
cluster empty -> with_cardinal_domain for Relation;
cluster finite Sequence-like -> with_cardinal_domain for Relation;
cluster with_cardinal_domain -> Sequence-like for Relation;
let c be Cardinal;
cluster -> with_cardinal_domain for ManySortedSet of c;
let x be object;
cluster c --> x -> with_cardinal_domain;
end;
registration
let X be set;
cluster -> with_cardinal_domain for Denumeration of X;
end;
registration
let c be Cardinal;
cluster -> with_cardinal_domain for Permutation of c;
end;
registration
cluster non empty trivial non-empty with_cardinal_domain
Cardinal-yielding for Function;
cluster non empty non trivial non-empty finite with_cardinal_domain
Cardinal-yielding for Function;
cluster non empty non-empty infinite with_cardinal_domain
natural-valued for Function;
cluster non trivial non-empty with_cardinal_domain
Cardinal-yielding non natural-valued for Function;
end;
registration
let R be with_cardinal_domain Relation;
cluster dom R -> cardinal;
end;
registration
let f be with_cardinal_domain Function;
identify dom f with card f;
end;
registration
let R be with_cardinal_domain Relation, P be total (rng R)-defined Relation;
cluster R * P -> with_cardinal_domain;
end;
registration
let g be Function, f be Denumeration of dom g;
cluster g * f -> with_cardinal_domain;
end;
registration
let f be with_cardinal_domain Function, p be Permutation of dom f;
cluster f * p -> with_cardinal_domain;
end;
theorem :: COUNTERS:54
for A, B being with_cardinal_domain Sequence st dom A in dom B
holds A^B is with_cardinal_domain;
registration
let p be XFinSequence, B be with_cardinal_domain Sequence;
cluster p^B -> with_cardinal_domain;
end;
definition
mode Counters is non empty with_cardinal_domain Cardinal-yielding Function;
end;
definition
mode Counters+ is
non empty non-empty with_cardinal_domain Cardinal-yielding Function;
end;