:: 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 :: (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, XBOOLE_0, FINSEQ_1, SUBSET_1, NAT_1, XXREAL_0, ARYTM_3, RELAT_1, ARYTM_1, ORDINAL4, FUNCT_1, RFINSEQ, PARTFUN1, CARD_1, AFINSQ_1, FUNCT_4, TARSKI, FUNCT_7; notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, NAT_D, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, RFINSEQ, FUNCT_7, XXREAL_0; constructors PARTFUN1, FUNCT_4, XXREAL_0, REAL_1, NAT_1, INT_1, FINSEQ_4, RFINSEQ, NAT_D, FUNCT_7, RELSET_1; registrations XBOOLE_0, RELAT_1, FUNCT_1, XREAL_0, INT_1, FINSEQ_1, FUNCT_7, ORDINAL1, NAT_1; requirements REAL, NUMERALS, SUBSET, ARITHM; begin :: Some Basic Theorems reserve D for non empty set, f for FinSequence of D, p, p1, p2, p3, q for Element of D, i, j, k, l, n for Nat; theorem :: FINSEQ_7:1 1 <= i & j <= len f & i < j implies f = (f|(i-'1))^<*f.i*>^((f/^i)|(j -'i-'1))^<*f.j*>^(f/^j); theorem :: FINSEQ_7:2 for f,g,h being FinSequence holds len g = len h & len g < i & i <= len (g^f) implies (g^f).i = (h^f).i; theorem :: FINSEQ_7:3 for f,g being FinSequence st 1 <= i & i <= len f holds f.i = (g^f).(len g + i); theorem :: FINSEQ_7:4 i in dom(f/^n) implies (f/^n).i = f.(n+i); begin :: Definition of Replace Function and its properties 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; redefine func Replace(f, i, p) -> FinSequence of D equals :: FINSEQ_7:def 1 (f|(i-'1))^<*p*>^(f/^i) if 1 <= i & i <= len f otherwise f; end; theorem :: FINSEQ_7:5 len Replace(f, i, p) = len f; theorem :: FINSEQ_7:6 for f being FinSequence, i be Nat, p be set holds rng Replace(f, i, p) c= rng f \/ {p}; theorem :: FINSEQ_7:7 1 <= i & i <= len f implies p in rng Replace(f, i, p); theorem :: FINSEQ_7:8 1 <= i & i <= len f implies Replace(f, i, p)/.i = p; theorem :: FINSEQ_7:9 1 <= i & i <= len f implies for k st 0 < k & k <= len f - i holds Replace(f, i, p).(i + k) = (f/^i).k; theorem :: FINSEQ_7:10 1 <= k & k <= len f & k <> i implies Replace(f, i, p)/.k = f/.k; theorem :: FINSEQ_7:11 1 <= i & i < j & j <= len f implies Replace(Replace(f, j, q), i, p) = (f|(i-'1))^<*p*>^(f/^i)|(j-'i-'1)^<*q*>^(f/^j); theorem :: FINSEQ_7:12 Replace(<*p*>, 1, q) = <*q*>; theorem :: FINSEQ_7:13 Replace(<*p1, p2*>, 1, q) = <*q, p2*>; theorem :: FINSEQ_7:14 Replace(<*p1, p2*>, 2, q) = <*p1, q*>; theorem :: FINSEQ_7:15 Replace(<*p1, p2, p3*>, 1, q) = <*q, p2, p3*>; theorem :: FINSEQ_7:16 Replace(<*p1, p2, p3*>, 2, q) = <*p1, q, p3*>; theorem :: FINSEQ_7:17 Replace(<*p1, p2, p3*>, 3, q) = <*p1, p2, q*>; begin :: Definition of Swap Function and its properties registration let f be FinSequence; let i, j be Nat; cluster Swap(f, i, j) -> FinSequence-like; end; definition let D be non empty set; let f be FinSequence of D; let i, j be Nat; redefine func Swap(f, i, j) -> FinSequence of D equals :: 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; end; theorem :: FINSEQ_7:18 len Swap(f, i, j) = len f; theorem :: FINSEQ_7:19 Swap(f, i, i) = f; theorem :: FINSEQ_7:20 Swap(Swap(f,i,j),j,i) = f; theorem :: FINSEQ_7:21 Swap(f, i, j) = Swap(f, j, i); theorem :: FINSEQ_7:22 rng Swap(f,i,j) = rng f; theorem :: FINSEQ_7:23 Swap(<*p1, p2*>, 1, 2) = <*p2, p1*>; theorem :: FINSEQ_7:24 Swap(<*p1, p2, p3*>, 1, 2) = <*p2, p1, p3*>; theorem :: FINSEQ_7:25 Swap(<*p1, p2, p3*>, 1, 3) = <*p3, p2, p1*>; theorem :: FINSEQ_7:26 Swap(<*p1, p2, p3*>, 2, 3) = <*p1, p3, p2*>; theorem :: FINSEQ_7:27 1 <= i & i < j & j <= len f implies Swap(f, i, j) = (f|(i-'1))^ <*f/.j*>^(f/^i)|(j-'i-'1)^<*f/.i*>^(f/^j); theorem :: FINSEQ_7:28 1 < i & i <= len f implies Swap(f, 1, i) = <*f/.i*>^((f/^1)|(i-'2))^<* f/.1*>^(f/^i); theorem :: FINSEQ_7:29 1 <= i & i < len f implies Swap(f, i, len f) = (f|(i-'1))^<*f/.len f*> ^((f/^i)|(len f-'i-'1))^<*f/.i*>; theorem :: FINSEQ_7:30 i <> k & j <> k & 1 <= k & k <= len f implies Swap(f, i, j)/.k = f/.k; theorem :: FINSEQ_7:31 1 <= i & i <= len f & 1 <= j & j <= len f implies Swap(f, i, j) /.i = f/.j & Swap(f, i, j)/.j = f/.i; begin :: Properties of composed function of Replace Function and Swap Function theorem :: FINSEQ_7:32 1 <= i & i <= len f & 1 <= j & j <= len f implies Replace(Swap(f , i, j), i, p) = Swap(Replace(f, j, p), i, j); theorem :: FINSEQ_7:33 i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f implies Swap(Replace(f, k, p), i, j) = Replace(Swap(f, i, j), k, p); theorem :: FINSEQ_7:34 i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f & 1 <= k & k <= len f implies Swap(Swap(f, i, j), j, k) = Swap(Swap(f, i, k), i, j); theorem :: FINSEQ_7:35 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 implies Swap(Swap(f, i, j) , k, l) = Swap(Swap(f, k, l), i, j);