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

begin

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)

proof end;

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

proof end;

begin

notation

let D be non empty set ;
let f be FinSequence of D;
let i be Nat;
let p be Element of D;
synonym Replace (f,i,p) for D +* (f,i);

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 b₁ being FinSequence of D holds
( ( 1 <= i & i <= len f implies ( b₁ = Replace (i,p,) iff b₁ = ((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) ) ) & ( ( not 1 <= i or not i <= len f ) implies ( b₁ = Replace (i,p,) iff b₁ = f ) ) )

proof end;

correctness
coherence
Replace (i,p,) is FinSequence of D;
consistency
for b₁ 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

canceled;

theorem :: FINSEQ_7:6

canceled;

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 holds len (Replace (f,i,p)) = len f by FUNCT_7:99;

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 holds rng (Replace (f,i,p)) c= (rng f) \/ {p} by FUNCT_7:102;

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
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:10

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:11

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 Th12: :: FINSEQ_7:12

for D being non empty set
for f being FinSequence of D
for p being Element of D
for k, i being Nat st 1 <= k & k <= len f & k <> i holds
(Replace (f,i,p)) /. k = f /. k

proof end;

theorem Th13: :: FINSEQ_7:13

for D being non empty set
for f being FinSequence of D
for q, p 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:14

for D being non empty set
for p, q being Element of D holds Replace (<*p*>,1,q) = <*q*>

proof end;

theorem Th15: :: FINSEQ_7:15

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 Th16: :: FINSEQ_7:16

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 Th17: :: FINSEQ_7:17

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 Th18: :: FINSEQ_7:18

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 Th19: :: FINSEQ_7:19

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;

begin

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 b₁ being FinSequence of D holds
( ( 1 <= i & i <= len f & 1 <= j & j <= len f implies ( b₁ = Swap (f,i,j) iff b₁ = 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 ( b₁ = Swap (f,i,j) iff b₁ = f ) ) )

proof end;

correctness
consistency
for b₁ 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 Th20: :: FINSEQ_7:20

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 Th21: :: FINSEQ_7:21

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:22

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 Th23: :: FINSEQ_7:23

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:24

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:105;

theorem :: FINSEQ_7:25

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:26

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:27

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:28

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 Th29: :: FINSEQ_7:29

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:30

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:31

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, k, j being Nat st i <> k & j <> k holds
(Swap (f,i,j)) . k = f . k

proof end;

theorem Th32: :: FINSEQ_7:32

for D being non empty set
for f being FinSequence of D
for i, k, j being Nat st i <> k & j <> k & 1 <= k & k <= len f holds
(Swap (f,i,j)) /. k = f /. k

proof end;

theorem Th33: :: FINSEQ_7:33

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;

begin

theorem Th34: :: FINSEQ_7:34

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 Th35: :: FINSEQ_7:35

for D being non empty set
for f being FinSequence of D
for p being Element of D
for i, k, j 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:36

for D being non empty set
for f being FinSequence of D
for i, k, j 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:37

for D being non empty set
for f being FinSequence of D
for i, k, j, 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;