:: A Theory of Sequential Files
:: by Hirofumi Fukura and Yatsuka Nakamura
::
:: Received August 12, 2005
:: Copyright (c) 2005-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, ORDINAL4, RELAT_1, CARD_1, SUBSET_1,
XXREAL_0, RFINSEQ, ARYTM_1, ARYTM_3, JORDAN3, FUNCT_1, FINSEQ_5, NAT_1,
PARTFUN1, FINSEQ_8, FILEREC1;
notations XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1,
NAT_D, RELAT_1, RFINSEQ, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, FINSEQ_4,
FINSEQ_6, FINSEQ_5, FINSEQ_8;
constructors NAT_1, RFINSEQ, NAT_D, FINSEQ_4, FINSEQ_5, CQC_LANG, FINSEQ_6,
FINSEQ_8, REAL_1, RELSET_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, XXREAL_0, XREAL_0, FINSEQ_1,
FINSEQ_5, ORDINAL1, CARD_1, NAT_1;
requirements NUMERALS, REAL, SUBSET, ARITHM;
begin
reserve a,b,c for set;
theorem :: FILEREC1:1
for p,q,r,s being FinSequence holds
p^q^r^s=p^(q^r)^s & p^q^r^s=(p^q)^(r^s) & p^(q^r)^s=(p^q)^(r^s);
theorem :: FILEREC1:2
for f being FinSequence holds f|(len f) = f;
theorem :: FILEREC1:3
for p,q being FinSequence st len p=0 holds q = p ^ q;
theorem :: FILEREC1:4
for D being non empty set,f being FinSequence of D, n,m being
Element of NAT st n<=m holds len (f/^m)<=len (f/^n);
theorem :: FILEREC1:5
for D being non empty set,f,g being FinSequence of D st len g>=1
holds mid(f^g,len f+1,len f+len g)=g;
theorem :: FILEREC1:6
for D being non empty set,f,g being FinSequence of D, i,j being
Element of NAT st 1<=i & i<=j & j<=len f holds mid(f^g,i,j)=mid(f,i,j);
theorem :: FILEREC1:7
for D being non empty set,f being FinSequence of D, i,j,n being
Element of NAT st 1<=i & i<=j & i<=len (f|n) & j<=len (f|n) holds mid(f,i,j)=
mid(f|n,i,j);
theorem :: FILEREC1:8
for D being non empty set,f being FinSequence of D st f=<*a*> holds a in D;
theorem :: FILEREC1:9
for D being non empty set,f being FinSequence of D st f=<*a,b*> holds
a in D & b in D;
theorem :: FILEREC1:10
for D being non empty set,f being FinSequence of D st f=<*a,b,c*>
holds a in D & b in D & c in D;
theorem :: FILEREC1:11
for f being FinSequence st f=<*a*> holds f|1=<*a*>;
theorem :: FILEREC1:12 :: FINSEQ_6:50
for D being non empty set,f being FinSequence of D st f=<*a,b*> holds
f/^1=<*b*>;
theorem :: FILEREC1:13
for D being non empty set,f being FinSequence of D st f=<*a,b,c*>
holds f|1=<*a*>;
theorem :: FILEREC1:14
for D being non empty set,f being FinSequence of D st f=<*a,b,c
*> holds f|2=<*a,b*>;
theorem :: FILEREC1:15
for D being non empty set,f being FinSequence of D st f=<*a,b,c*>
holds f/^1=<*b,c*>;
theorem :: FILEREC1:16
for D being non empty set,f being FinSequence of D st f=<*a,b,c*>
holds f/^2=<*c*>;
theorem :: FILEREC1:17
for f being FinSequence st len f=0 holds Rev f=f;
theorem :: FILEREC1:18
for D being non empty set, r being FinSequence of D,i being
Element of NAT st i<=len r holds Rev(r/^i)=(Rev r)|(len r-'i);
theorem :: FILEREC1:19
for D being non empty set,f,CR being FinSequence of D st not CR
is_substring_of f,1 & CR separates_uniquely holds instr(1,f^CR,CR)=len f +1;
theorem :: FILEREC1:20
for D being non empty set,f,CR being FinSequence of D st not CR
is_substring_of f,1 & CR separates_uniquely holds f^CR is_terminated_by CR;
::==========================================================================
:: file and record
::==========================================================================
notation
let D be set;
synonym File of D for FinSequence of D;
end;
definition
let D be non empty set, r,f,CR be File of D;
pred r is_a_record_of f,CR means
:: FILEREC1:def 1
(CR^r is_substring_of addcr(f,CR),1
or r is_preposition_of addcr(f,CR)) & r is_terminated_by CR;
end;
theorem :: FILEREC1:21
for D being non empty set,r being FinSequence of D holds ovlpart
(<*>D,r)=<*>D & ovlpart(r,<*>D)=<*>D;
theorem :: FILEREC1:22
for D being non empty set,CR being FinSequence of D holds CR
is_a_record_of <*>D,CR;
theorem :: FILEREC1:23
for D being non empty set,a,b be set,f,r,CR being File of D st a <> b
& CR = <*b*> & f = <*b,a,b*> & r = <*a,b*> holds CR is_a_record_of f,CR & r
is_a_record_of f,CR;
theorem :: FILEREC1:24
for D being non empty set,f,CR being File of D holds f is_preposition_of f^CR
;
theorem :: FILEREC1:25
for D being non empty set,f,CR being File of D holds f
is_preposition_of addcr(f,CR);
theorem :: FILEREC1:26
for D being non empty set,r,CR being File of D st CR
is_postposition_of r holds 0<=len r-len CR;
theorem :: FILEREC1:27
for D being non empty set,CR,r being File of D st CR
is_postposition_of r holds r=addcr(r,CR);
theorem :: FILEREC1:28
for D being non empty set,CR,r being File of D st
r is_terminated_by CR holds r=addcr(r,CR);
theorem :: FILEREC1:29
for D being non empty set,f,g being File of D st f is_terminated_by g
holds len g <=len f;
theorem :: FILEREC1:30
for D being non empty set,f,CR being File of D holds len addcr(f
,CR) >= len f & len addcr(f,CR) >= len CR;
theorem :: FILEREC1:31
for D being non empty set,f,g being FinSequence of D holds g =
ovlpart(f,g)^ovlrdiff(f,g);
theorem :: FILEREC1:32
for D being non empty set,f,g being FinSequence of D holds ovlcon(f,g)
= ovlldiff(f,g) ^ g;
theorem :: FILEREC1:33
for D being non empty set,CR,r being File of D holds addcr(r,CR)=
ovlldiff(r,CR)^CR;
theorem :: FILEREC1:34
for D being non empty set,r1,r2,f being File of D st f = r1 ^ r2
holds r1 is_substring_of f,1 & r2 is_substring_of f,1;
theorem :: FILEREC1:35
for D being non empty set,r1,r2,r3,f being File of D st f = r1 ^
r2 ^ r3 holds r1 is_substring_of f,1 & r2 is_substring_of f,1 & r3
is_substring_of f,1;
theorem :: FILEREC1:36
for D being non empty set,CR,r1,r2 being File of D st r1
is_terminated_by CR & r2 is_terminated_by CR holds CR^r2 is_substring_of addcr(
r1^r2,CR),1;
theorem :: FILEREC1:37
for D being non empty set,f,g being File of D,n being Element of
NAT st 00 holds g is_substring_of f,1
;
theorem :: FILEREC1:42
for D being non empty set, f,CR being File of D ex r being File of D
st r is_a_record_of f,CR;
theorem :: FILEREC1:43
for D being non empty set,f,CR,r being File of D st r is_a_record_of f
,CR holds r is_a_record_of r,CR;
theorem :: FILEREC1:44
for D being non empty set,CR,r1,r2,f being File of D st r1
is_terminated_by CR & r2 is_terminated_by CR & f = r1 ^ r2 holds r1
is_a_record_of f,CR & r2 is_a_record_of f,CR;