:: On Replace Function and Swap Function for Finite Sequences
:: by Hiroshi Yamazaki , Yoshinori Fujisawa and Yatsuka Nakamura
::
:: Received August 28, 2000
:: Copyright (c) 2000-2021 Association of Mizar Users


theorem :: FINSEQ_7:1
for D being non empty set
for f being FinSequence of D
for i, j being Nat st 1 <= i & j <= len f & i < j holds
f = ((((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f . j)*>) ^ (f /^ j)
proof end;

theorem :: FINSEQ_7:2
for i being Nat
for f, g, h being FinSequence st len g = len h & len g < i & i <= len (g ^ f) holds
(g ^ f) . i = (h ^ f) . i
proof end;

theorem :: FINSEQ_7:3
for i being Nat
for f, g being FinSequence st 1 <= i & i <= len f holds
f . i = (g ^ f) . ((len g) + i)
proof end;

theorem :: FINSEQ_7:4
for D being non empty set
for f being FinSequence of D
for i, n being Nat st i in dom (f /^ n) holds
(f /^ n) . i = f . (n + i) by FINSEQ_5:27;

Lm1: for i, j being Nat holds (j -' i) -' 1 = (j -' 1) -' i
proof end;

notation
let f be FinSequence;
let i be Nat;
let p be object ;
synonym Replace (f,i,p) for f +* (i,p);
end;

definition
let D be non empty set ;
let f be FinSequence of D;
let i be Nat;
let p be Element of D;
:: original: Replace
redefine func Replace (f,i,p) -> FinSequence of D equals :Def1: :: FINSEQ_7:def 1
((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) if ( 1 <= i & i <= len f )
otherwise f;
compatibility
for b1 being FinSequence of D holds
( ( 1 <= i & i <= len f implies ( b1 = Replace (f,i,p) iff b1 = ((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) ) ) & ( ( not 1 <= i or not i <= len f ) implies ( b1 = Replace (f,i,p) iff b1 = f ) ) )
proof end;
correctness
coherence
Replace (f,i,p) is FinSequence of D;
consistency
for b1 being FinSequence of D holds verum;
proof end;
end;

:: deftheorem Def1 defines Replace FINSEQ_7:def 1 :
for D being non empty set
for f being FinSequence of D
for i being Nat
for p being Element of D holds
( ( 1 <= i & i <= len f implies Replace (f,i,p) = ((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) ) & ( ( not 1 <= i or not i <= len f ) implies Replace (f,i,p) = f ) );

theorem :: FINSEQ_7:5
for D being non empty set
for f being FinSequence of D
for p being Element of D
for i being Nat holds len (Replace (f,i,p)) = len f by FUNCT_7:97;

theorem :: FINSEQ_7:6
for f being FinSequence
for i being Nat
for p being set holds rng (Replace (f,i,p)) c= (rng f) \/ {p} by FUNCT_7:100;

theorem :: FINSEQ_7:7
for D being non empty set
for f being FinSequence of D
for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
p in rng (Replace (f,i,p))
proof end;

Lm2: for D being non empty set
for f being FinSequence of D
for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
(Replace (f,i,p)) . i = p
proof end;

theorem :: FINSEQ_7:8
for D being non empty set
for f being FinSequence of D
for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
(Replace (f,i,p)) /. i = p
proof end;

theorem :: FINSEQ_7:9
for D being non empty set
for f being FinSequence of D
for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
for k being Nat st 0 < k & k <= (len f) - i holds
(Replace (f,i,p)) . (i + k) = (f /^ i) . k
proof end;

theorem Th10: :: FINSEQ_7:10
for D being non empty set
for f being FinSequence of D
for p being Element of D
for i, k being Nat st 1 <= k & k <= len f & k <> i holds
(Replace (f,i,p)) /. k = f /. k
proof end;

theorem Th11: :: FINSEQ_7:11
for D being non empty set
for f being FinSequence of D
for p, q being Element of D
for i, j being Nat st 1 <= i & i < j & j <= len f holds
Replace ((Replace (f,j,q)),i,p) = ((((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*q*>) ^ (f /^ j)
proof end;

theorem :: FINSEQ_7:12
for D being non empty set
for p, q being Element of D holds Replace (<*p*>,1,q) = <*q*>
proof end;

theorem Th13: :: FINSEQ_7:13
for D being non empty set
for p1, p2, q being Element of D holds Replace (<*p1,p2*>,1,q) = <*q,p2*>
proof end;

theorem Th14: :: FINSEQ_7:14
for D being non empty set
for p1, p2, q being Element of D holds Replace (<*p1,p2*>,2,q) = <*p1,q*>
proof end;

theorem Th15: :: FINSEQ_7:15
for D being non empty set
for p1, p2, p3, q being Element of D holds Replace (<*p1,p2,p3*>,1,q) = <*q,p2,p3*>
proof end;

theorem Th16: :: FINSEQ_7:16
for D being non empty set
for p1, p2, p3, q being Element of D holds Replace (<*p1,p2,p3*>,2,q) = <*p1,q,p3*>
proof end;

theorem Th17: :: FINSEQ_7:17
for D being non empty set
for p1, p2, p3, q being Element of D holds Replace (<*p1,p2,p3*>,3,q) = <*p1,p2,q*>
proof end;

registration
let f be FinSequence;
let i, j be Nat;
cluster Swap (f,i,j) -> FinSequence-like ;
correctness
coherence
Swap (f,i,j) is FinSequence-like ;
proof end;
end;

definition
let D be non empty set ;
let f be FinSequence of D;
let i, j be Nat;
:: original: Swap
redefine func Swap (f,i,j) -> FinSequence of D equals :Def2: :: FINSEQ_7:def 2
 Replace ((Replace (f,i,(f /. j))),j,(f /. i)) if ( 1 <= i & i <= len f & 1 <= j & j <= len f )
otherwise f;
coherence
Swap (f,i,j) is FinSequence of D
proof end;
compatibility
for b1 being FinSequence of D holds
( ( 1 <= i & i <= len f & 1 <= j & j <= len f implies ( b1 = Swap (f,i,j) iff b1 = Replace ((Replace (f,i,(f /. j))),j,(f /. i)) ) ) & ( ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) implies ( b1 = Swap (f,i,j) iff b1 = f ) ) )
proof end;
correctness
consistency
for b1 being FinSequence of D holds verum;
;
end;

:: deftheorem Def2 defines Swap FINSEQ_7:def 2 :
for D being non empty set
for f being FinSequence of D
for i, j being Nat holds
( ( 1 <= i & i <= len f & 1 <= j & j <= len f implies Swap (f,i,j) = Replace ((Replace (f,i,(f /. j))),j,(f /. i)) ) & ( ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) implies Swap (f,i,j) = f ) );

theorem Th18: :: FINSEQ_7:18
for D being non empty set
for f being FinSequence of D
for i, j being Nat holds len (Swap (f,i,j)) = len f
proof end;

Lm3: for D being non empty set
for f being FinSequence of D
for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds
( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i )
proof end;

theorem Th19: :: FINSEQ_7:19
for D being non empty set
for f being FinSequence of D
for i being Nat holds Swap (f,i,i) = f
proof end;

theorem :: FINSEQ_7:20
for D being non empty set
for f being FinSequence of D
for i, j being Nat holds Swap ((Swap (f,i,j)),j,i) = f
proof end;

theorem Th21: :: FINSEQ_7:21
for D being non empty set
for f being FinSequence of D
for i, j being Nat holds Swap (f,i,j) = Swap (f,j,i)
proof end;

theorem :: FINSEQ_7:22
for D being non empty set
for f being FinSequence of D
for i, j being Nat holds rng (Swap (f,i,j)) = rng f by FUNCT_7:103;

theorem :: FINSEQ_7:23
for D being non empty set
for p1, p2 being Element of D holds Swap (<*p1,p2*>,1,2) = <*p2,p1*>
proof end;

theorem :: FINSEQ_7:24
for D being non empty set
for p1, p2, p3 being Element of D holds Swap (<*p1,p2,p3*>,1,2) = <*p2,p1,p3*>
proof end;

theorem :: FINSEQ_7:25
for D being non empty set
for p1, p2, p3 being Element of D holds Swap (<*p1,p2,p3*>,1,3) = <*p3,p2,p1*>
proof end;

theorem :: FINSEQ_7:26
for D being non empty set
for p1, p2, p3 being Element of D holds Swap (<*p1,p2,p3*>,2,3) = <*p1,p3,p2*>
proof end;

theorem Th27: :: FINSEQ_7:27
for D being non empty set
for f being FinSequence of D
for i, j being Nat st 1 <= i & i < j & j <= len f holds
Swap (f,i,j) = ((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ j)
proof end;

theorem :: FINSEQ_7:28
for D being non empty set
for f being FinSequence of D
for i being Nat st 1 < i & i <= len f holds
Swap (f,1,i) = ((<*(f /. i)*> ^ ((f /^ 1) | (i -' 2))) ^ <*(f /. 1)*>) ^ (f /^ i)
proof end;

theorem :: FINSEQ_7:29
for D being non empty set
for f being FinSequence of D
for i being Nat st 1 <= i & i < len f holds
Swap (f,i,(len f)) = (((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*>
proof end;

Lm4: for D being non empty set
for f being FinSequence of D
for i, j, k being Nat st i <> k & j <> k holds
(Swap (f,i,j)) . k = f . k
proof end;

theorem Th30: :: FINSEQ_7:30
for D being non empty set
for f being FinSequence of D
for i, j, k being Nat st i <> k & j <> k & 1 <= k & k <= len f holds
(Swap (f,i,j)) /. k = f /. k
proof end;

theorem Th31: :: FINSEQ_7:31
for D being non empty set
for f being FinSequence of D
for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds
( (Swap (f,i,j)) /. i = f /. j & (Swap (f,i,j)) /. j = f /. i )
proof end;

theorem Th32: :: FINSEQ_7:32
for D being non empty set
for f being FinSequence of D
for p being Element of D
for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds
Replace ((Swap (f,i,j)),i,p) = Swap ((Replace (f,j,p)),i,j)
proof end;

theorem Th33: :: FINSEQ_7:33
for D being non empty set
for f being FinSequence of D
for p being Element of D
for i, j, k being Nat st i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f holds
Swap ((Replace (f,k,p)),i,j) = Replace ((Swap (f,i,j)),k,p)
proof end;

theorem :: FINSEQ_7:34
for D being non empty set
for f being FinSequence of D
for i, j, k being Nat st i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f & 1 <= k & k <= len f holds
Swap ((Swap (f,i,j)),j,k) = Swap ((Swap (f,i,k)),i,j)
proof end;

theorem :: FINSEQ_7:35
for D being non empty set
for f being FinSequence of D
for i, j, k, l being Nat st i <> k & j <> k & l <> i & l <> j & 1 <= i & i <= len f & 1 <= j & j <= len f & 1 <= k & k <= len f & 1 <= l & l <= len f holds
Swap ((Swap (f,i,j)),k,l) = Swap ((Swap (f,k,l)),i,j)
proof end;