Appendix B.10 FINSEQ

B.10 FINSEQ_1

Segments of Natural Numbers and Finite Sequences
by Grzegorz Bancerek, and Krzysztof Hryniewiecki

reserve k,l,m,n,k1,k2 for Nat,
a,b,c for natural number,
x,y,z,y1,y2,X,Y for set,
f,g for Function;

def 1 func Seg n -> set equals { k : 1 <= k & k <= n };
redefine func Seg n -> Subset of NAT;

3 a in Seg b iff 1 <= a & a <= b;
4 Seg 0 = {} & Seg 1 = { 1 } & Seg 2 = { 1,2 };
5 a = 0 or a in Seg a;
6 a+1 in Seg(a+1);
7 a <= b iff Seg a c= Seg b;
8 Seg a = Seg b implies a = b;
9 c <= a implies
Seg c = Seg c /\ Seg a & Seg c = Seg a /\ Seg c;
10 (Seg c = Seg c /\ Seg a or Seg c = Seg a /\ Seg c )
implies c <= a;
11 Seg a \/ { a+1 } = Seg (a+1);

def 2 attr IT is FinSequence-like means ex n st dom IT = Seg n;
cluster FinSequence-like Function;
mode FinSequence is FinSequence-like Function;

reserve p,q,r,s,t for FinSequence;

cluster Seg n -> finite;
cluster FinSequence-like -> finite Function;

def 3 func Card p -> Nat means Seg it = dom p;
redefine func dom p -> Subset of NAT;

14 {} is FinSequence;
15 (ex k st dom f c= Seg k) implies ex p st f c= p;

scheme SeqEx{A()->Nat,P[set,set]}:
ex p st dom p = Seg A() & for k st k in Seg A() holds P[k,p.k]
provided
for k,y1,y2 st k in Seg A() & P[k,y1] & P[k,y2] holds y1=y2
and
for k st k in Seg A() ex x st P[k,x];

scheme SeqLambda{A()->Nat,F(set) -> set}:
ex p being FinSequence st len p = A() & for k st k in Seg A()
holds p.k=F(k);

16 z in p implies ex k st k in dom p & z=[k,p.k];
17 X = dom p & X = dom q & (for k st k in X holds p.k = q.k)
implies p=q;
18 ( (len p = len q) & for k st 1 <=k & k <= len p holds p.k=q.k )
implies p=q;
19 p|(Seg a) is FinSequence;
20 rng p c= dom f implies f*p is FinSequence;
21 a <= len p & q = p|(Seg a) implies len q = a & dom q = Seg a;

def 4 mode FinSequence of D -> FinSequence means rng it c= D;
cluster {} -> FinSequence-like;
cluster FinSequence-like PartFunc of NAT,D;

redefine mode FinSequence of D -> FinSequence-like PartFunc of NAT,D;

reserve D for set;

23 for p being FinSequence of D holds p|(Seg a) is FinSequence of D;
24 for D being non empty set
ex p being FinSequence of D st len p = a;

cluster empty FinSequence;

25 len p = 0 iff p = {};
26 p={} iff dom p = {};
27 p={} iff rng p= {};
29 for D be set holds {} is FinSequence of D;

cluster empty FinSequence of D;

def 5 func <*x*> -> set equals { [1,x] };
def 6 func <*>D -> empty FinSequence of D equals {};

32 p=<*>(D) iff len p = 0;

def 7 func p^q -> FinSequence means
dom it = Seg (len p + len q) &
(for k st k in dom p holds it.k=p.k) &
(for k st k in dom q holds it.(len p + k) = q.k);

35 len(p^q) = len p + len q;
36 (len p + 1 <= k & k <= len p + len q) implies (p^q).k=q.(k-len p);
37 len p < k & k <= len(p^q) implies (p^q).k = q.(k - len p);
38 k in dom (p^q) implies
(k in dom p or (ex n st n in dom q & k=len p + n));
39 dom p c= dom(p^q);
40 x in dom q implies ex k st k=x & len p + k in dom(p^q);
41 k in dom q implies len p + k in dom(p^q);
42 rng p c= rng(p^q);
43 rng q c= rng(p^q);
44 rng(p^q) = rng p \/ rng q;
45 p^q^r = p^(q^r);
46 p^r = q^r or r^p = r^q implies p = q;
47 p^{} = p & {}^p = p;
48 p^q = {} implies p={} & q={};

redefine func p^q -> FinSequence of D;

def 8 redefine func <*x*> -> Function means dom it = Seg 1 & it.1 = x;
cluster <*x*> -> Function-like Relation-like;
cluster <*x*> -> FinSequence-like;

50 p^q is FinSequence of D implies
p is FinSequence of D & q is FinSequence of D;

def 9 func <*x,y*> -> set equals <*x*>^<*y*>;
def 10 func <*x,y,z*> -> set equals <*x*>^<*y*>^<*z*>;

cluster <*x,y*> -> Function-like Relation-like;
cluster <*x,y,z*> -> Function-like Relation-like;
cluster <*x,y*> -> FinSequence-like;
cluster <*x,y,z*> -> FinSequence-like;

52 <*x*> = { [1,x] };
55 p=<*x*> iff dom p = Seg 1 & rng p = {x};
56 p=<*x*> iff len p = 1 & rng p = {x};
57 p = <*x*> iff len p = 1 & p.1 = x;
58 (<*x*>^p).1 = x;
59 (p^<*x*>).(len p + 1)=x;
60 <*x,y,z*>=<*x*>^<*y,z*> &
<*x,y,z*>=<*x,y*>^<*z*>;
61 p = <*x,y*> iff len p = 2 & p.1=x & p.2=y;
62 p = <*x,y,z*> iff len p = 3 & p.1 = x & p.2 = y & p.3 = z;
63 p <> {} implies ex q,x st p=q^<*x*>;

redefine func <*x*> -> FinSequence of D;

scheme IndSeq{P[FinSequence]}:
for p holds P[p]
provided
P[{}] and
for p,x st P[p] holds P[p^<*x*>];

64 for p,q,r,s being FinSequence st p^q = r^s & len p <= len r
ex t being FinSequence st p^t = r;

def 11 func D* -> set means x in it iff x is FinSequence of D;

cluster D* -> non empty;

66 {} in D*;

scheme SepSeq{D()->non empty set, P[FinSequence]}:
ex X st (for x holds x in X iff
ex p st (p in D()* & P[p] & x=p));

def 12 attr IT is FinSubsequence-like means ex k st dom IT c= Seg k;

cluster FinSubsequence-like Function;
mode FinSubsequence is FinSubsequence-like Function;

68 for p being FinSequence holds p is FinSubsequence;
69 p|X is FinSubsequence & X|p is FinSubsequence;

reserve p' for FinSubsequence;

def 13 given k such that X c= Seg k;
func Sgm X -> FinSequence of NAT means
rng it = X & for l,m,k1,k2 st
( 1 <= l & l < m & m <= len it &
k1=it.l & k2=it.m) holds k1 < k2;

71 rng Sgm dom p' = dom p';

def 14 func Seq p' -> Function equals p'* Sgm(dom p');

cluster Seq p' -> FinSequence-like;

72 for X st ex k st X c= Seg k holds Sgm X = {} iff X = {};
73 D is finite iff ex p st D = rng p;

cluster rng p -> finite;

74 Seg n,Seg m are_equipotent implies n = m;
75 Seg n,n are_equipotent;
76 Card Seg n = Card n;
77 X is finite implies ex n st X,Seg n are_equipotent;
78 for n being Nat holds
card Seg n = n & card n = n & card Card n = n;