:: On Replace Function and Swap Function for Finite Sequences
:: by Hiroshi Yamazaki , Yoshinori Fujisawa and Yatsuka Nakamura
::
:: Received August 28, 2000
:: Copyright (c) 2000 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 Th7: :: 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

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