:: Memory Structures
:: by Andrzej Trybulec
::
:: Received April 28, 2011
:: Copyright (c) 2011-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 STRUCT_0, SUBSET_1, XBOOLE_0, FUNCT_1, NUMBERS, CARD_3, CARD_1,
FUNCOP_1, FUNCT_4, RELAT_1, TARSKI, CAT_1, FSM_1, FINSET_1, NAT_1,
ARYTM_1, PARTFUN1, AMI_1, ARYTM_3, COMPOS_1, SCMFSA6C, XXREAL_0,
SUPINF_2, MEMSTR_0, PBOOLE, GOBRD13, QUANTAL1, SCMFSA9A;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ORDINAL1, PBOOLE, FUNCT_7,
CARD_1, CARD_3, XCMPLX_0, RELAT_1, FUNCT_1, PARTFUN1, FINSET_1, NUMBERS,
INT_1, NAT_1, NAT_D, FUNCOP_1, FUNCT_4, AFINSQ_1, FINSEQ_1, FUNCT_2,
DOMAIN_1, VALUED_0, VALUED_1, STRUCT_0, XXREAL_0, MEASURE6;
constructors SETFAM_1, DOMAIN_1, FUNCT_4, XXREAL_0, RELSET_1, FUNCT_7,
PRE_POLY, PBOOLE, AFINSQ_1, NAT_D, WELLORD2, STRUCT_0;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FUNCOP_1,
FUNCT_4, FINSET_1, XREAL_0, CARD_3, STRUCT_0, RELSET_1, PBOOLE, NAT_1,
CARD_1, MEASURE6;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Terminology
reserve x,N for set,
k for Nat;
definition let N;
struct (ZeroStr) Mem-Struct over N (# carrier -> set,
ZeroF -> Element of the carrier,
Object-Kind -> Function of the carrier, N,
ValuesF -> ManySortedSet of N
#);
end;
reserve N for with_zero set;
:: wymaganie zeby N byl 'with_zero' jest troche na zapas
:: na razie wykorzystujemy tylko rejestracje, ze 'with_zero'
:: musi byc 'non empty' i w definicji Trivial-Mem N
:: ale tutaj mozna sie tego pozbyc, biorac zamiast 0
:: the Element of N i potrzebujemy tylko to, ze N jest niepusty
definition let N;
func Trivial-Mem N -> strict Mem-Struct over N means
:: MEMSTR_0:def 1
the carrier of it = {0} & the ZeroF of it = 0 &
the Object-Kind of it = 0 .--> 0 &
the ValuesF of it = N --> NAT;
end;
registration let N;
cluster Trivial-Mem N -> 1-element;
end;
registration let N;
cluster 1-element for Mem-Struct over N;
end;
notation let N;
let S be Mem-Struct over N;
synonym IC S for 0.S;
synonym Data-Locations S for NonZero S;
end;
registration
:: gdzie to ma byc, dlaczego nie dziala SETFAM_1
cluster with_zero -> non empty for set;
end;
definition let N;
let S be Mem-Struct over N;
func the_Values_of S -> ManySortedSet of the carrier of S equals
:: MEMSTR_0:def 2
(the ValuesF of S)*(the Object-Kind of S);
end;
definition let N;
let S be Mem-Struct over N;
mode PartState of S is (the carrier of S)-defined
(the_Values_of S)-compatible Function;
end;
:: Jest potrzeba zagwarantowania, ze
:: the_Values_of S is non-empty
:: to bylo wczsniej obsluzone, ze stary N byl
:: with_non-empty_elements
:: teraz jest to wlasnosc Mem-Str
:: sa tutaj rozne warianty, najprosciej jednak napisac co wymgamy:
definition let N;
let S be Mem-Struct over N;
attr S is with_non-empty_values means
:: MEMSTR_0:def 3
the_Values_of S is non-empty;
end;
registration let N;
cluster Trivial-Mem N ->with_non-empty_values;
end;
registration let N;
cluster with_non-empty_values for Mem-Struct over N;
end;
registration let N;
let S be with_non-empty_values Mem-Struct over N;
cluster the_Values_of S -> non-empty;
end;
definition let N;
let S be with_non-empty_values Mem-Struct over N;
mode State of S is total PartState of S;
end;
definition let N;
let S be Mem-Struct over N;
mode Object of S is Element of S;
end;
begin :: the Object Kind
definition let N;
let S be non empty Mem-Struct over N;
let o be Object of S;
func ObjectKind o -> Element of N equals
:: MEMSTR_0:def 4
(the Object-Kind of S).o;
end;
definition let N;
let S be non empty Mem-Struct over N;
let o be Object of S;
func Values o -> set equals
:: MEMSTR_0:def 5
(the_Values_of S).o;
end;
:: Jezeli dodamy wartosci, to pewnie nie unikniemy zdefiniowania
:: funktora, ktory odpowiada staremu Object-Kind
:: np. the_Object-Kind_of, lub the_Values_of
:: i wtedy podmiana nie powinna byc zbyt skomplikowana.
:: Poza tym trzeba bedzie zmienic komputery, dodajac pole ValuesF
:: wykorzystac mozna atrybut with_zero, ale trzeba wprowadzic nowy:
:: (the ValuesF of S).0 = NAT
definition let N;
let IT be non empty Mem-Struct over N;
attr IT is IC-Ins-separated means
:: MEMSTR_0:def 6
Values IC IT = NAT;
end;
registration let N;
cluster Trivial-Mem N -> IC-Ins-separated;
end;
registration let N;
cluster IC-Ins-separated with_non-empty_values strict
for 1-element Mem-Struct over N;
end;
definition
let N;
let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N;
let p be PartState of S;
func IC p -> Element of NAT equals
:: MEMSTR_0:def 7
p.IC S;
end;
theorem :: MEMSTR_0:1
for S being IC-Ins-separated 1-element with_non-empty_values Mem-Struct over N
for s1, s2 being State of S st IC s1 = IC s2 holds s1= s2;
registration
let N;
let S be non empty with_non-empty_values Mem-Struct over N,
o be Object of S;
cluster Values o -> non empty;
end;
registration
let N;
let S be IC-Ins-separated non empty
with_non-empty_values Mem-Struct over N;
let la be Object of S;
let a be Element of Values la;
cluster la .--> a -> (the_Values_of S)-compatible;
let lb be Object of S;
let b be Element of Values lb;
cluster (la,lb) --> (a,b) -> (the_Values_of S)-compatible;
end;
theorem :: MEMSTR_0:2
for S being non empty with_non-empty_values Mem-Struct over N
for s being State of S holds IC S in dom s;
reserve S for IC-Ins-separated non empty with_non-empty_values
Mem-Struct over N;
definition
let N;
let S be Mem-Struct over N;
let p be PartState of S;
func DataPart p -> PartState of S equals
:: MEMSTR_0:def 8
p | Data-Locations S;
projectivity;
end;
definition
let N; let S be Mem-Struct over N;
let p be PartState of S;
attr p is data-only means
:: MEMSTR_0:def 9
dom p misses {IC S};
end;
registration
let N; let S be Mem-Struct over N;
cluster empty -> data-only for PartState of S;
end;
registration
let N; let S be Mem-Struct over N;
cluster empty for PartState of S;
end;
theorem :: MEMSTR_0:3
for N for S being Mem-Struct over N
for p being PartState of S holds not IC S in dom DataPart p;
theorem :: MEMSTR_0:4
for N for S being Mem-Struct over N for p being
PartState of S holds {IC S} misses dom DataPart p;
theorem :: MEMSTR_0:5
for p being data-only PartState of S, q being PartState of S
holds p c= q iff p c= DataPart q;
registration
let N;
let S be Mem-Struct over N;
let p be PartState of S;
cluster DataPart p -> data-only;
end;
theorem :: MEMSTR_0:6
for S being Mem-Struct over N, p being PartState
of S holds p is data-only iff dom p c= Data-Locations S;
theorem :: MEMSTR_0:7
for S being Mem-Struct over N, p being data-only PartState of S
holds DataPart p = p;
reserve s for State of S;
theorem :: MEMSTR_0:8
Data-Locations S c= dom s;
theorem :: MEMSTR_0:9
dom DataPart s = Data-Locations S;
theorem :: MEMSTR_0:10
for d being data-only PartState of S holds not IC S in dom d;
theorem :: MEMSTR_0:11
for p being PartState of S, d being data-only PartState of S
holds IC(p+*d) = IC p;
reserve p for PartState of S;
theorem :: MEMSTR_0:12
for p being PartState of S holds DataPart p c= p;
theorem :: MEMSTR_0:13
dom s = {IC S} \/ Data-Locations S;
theorem :: MEMSTR_0:14
dom p /\ Data-Locations S = dom DataPart p;
registration let N;
let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N,
l be Nat, s be State of S;
cluster s+*(IC S,l) -> (the_Values_of S)-compatible;
end;
begin :: The value of the Instruction Counter
definition
let N;
let S be IC-Ins-separated non empty
with_non-empty_values Mem-Struct over N;
let l be Nat;
func Start-At(l,S) -> PartState of S equals
:: MEMSTR_0:def 10
IC S .--> l;
end;
definition
let N;
let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N,
l be Nat;
let p be PartState of S;
attr p is l-started means
:: MEMSTR_0:def 11
IC S in dom p & IC p = l;
end;
registration
let N;
let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N,
l be Nat;
cluster Start-At(l,S) -> l-started non empty;
end;
theorem :: MEMSTR_0:15
for l being Nat holds IC S in dom Start-At(l,S);
theorem :: MEMSTR_0:16
for n being Nat
holds IC(p +* Start-At( n,S)) = n;
registration
let N;
let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N,
l be Nat;
cluster l-started for State of S;
end;
registration
let N;
let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N,
l be Nat,
p being PartState of S,
q be l-started PartState of S;
cluster p +* q -> l-started;
end;
definition
let N;
let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N,
l be Nat;
let s be State of S;
redefine attr s is l-started means
:: MEMSTR_0:def 12
IC s = l;
end;
theorem :: MEMSTR_0:17
for S being IC-Ins-separated non empty with_non-empty_values
Mem-Struct over N,
l being Nat,
p being l-started PartState of S
for s being PartState of S st p c= s holds s is l-started;
theorem :: MEMSTR_0:18
for s being State of S holds Start-At(IC s,S) = s | {IC S};
theorem :: MEMSTR_0:19
for S being IC-Ins-separated non empty with_non-empty_values
Mem-Struct over N
for p being PartState of S st IC S in
dom p holds p = Start-At(IC p,S) +* DataPart p;
theorem :: MEMSTR_0:20
for S be IC-Ins-separated non empty
with_non-empty_values Mem-Struct over N, l be Nat
holds DataPart Start-At(l,S) = {};
theorem :: MEMSTR_0:21
for l1,l2,k being Nat holds Start-At(l1+k,S) =
Start-At(l2+k,S) iff Start-At(l1,S) = Start-At(l2,S);
theorem :: MEMSTR_0:22
for l1,l2,k being Nat st Start-At(l1,S) = Start-At(l2,S)
holds Start-At(l1 -' k,S) = Start-At(l2 -' k,S);
theorem :: MEMSTR_0:23
for d being data-only PartState of S, k being Nat
holds d tolerates Start-At(k,S);
theorem :: MEMSTR_0:24
for S being IC-Ins-separated non empty with_non-empty_values Mem-Struct over N
for p being PartState of S st IC S in dom p
holds dom p = {IC S} \/ dom DataPart p;
theorem :: MEMSTR_0:25
for S being IC-Ins-separated non empty with_non-empty_values
Mem-Struct over N
for s being State of S
holds dom s = {IC S} \/ dom DataPart s;
theorem :: MEMSTR_0:26
for p being PartState of S st IC S in dom p
holds p = DataPart p +* Start-At (IC p,S);
theorem :: MEMSTR_0:27
IC S in dom (p +* Start-At( k,S));
theorem :: MEMSTR_0:28
p +* Start-At( k,S) c= s implies IC s = k;
theorem :: MEMSTR_0:29
for S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N,
l be Nat
for p be PartState of S
holds p is l-started iff Start-At(l,S) c= p;
registration let N,S; let k be Nat;
let p be k-started PartState of S, d be data-only PartState of S;
cluster p +* d -> k-started;
end;
theorem :: MEMSTR_0:30
Start-At(IC s,S) c= s;
theorem :: MEMSTR_0:31
for s being State of S
holds s +* Start-At(IC s,S) = s;
theorem :: MEMSTR_0:32
dom p c= {IC S} \/ dom DataPart p;
theorem :: MEMSTR_0:33
for S being IC-Ins-separated non empty with_non-empty_values
Mem-Struct over N
for s be State of S holds s = s|(Data-Locations S \/ {IC S});
theorem :: MEMSTR_0:34
for S being IC-Ins-separated non empty with_non-empty_values
Mem-Struct over N
for s1,s2 be State of S
st s1|(Data-Locations S \/ {IC S}) = s2|(Data-Locations S \/ {IC S})
holds s1 = s2;
theorem :: MEMSTR_0:35
IC S in dom p implies p = Start-At(IC p,S) +* DataPart p;
theorem :: MEMSTR_0:36
for p being PartState of S, k,l being Nat
holds p +* Start-At(k,S) +* Start-At(l,S) = p +* Start-At(l,S);
theorem :: MEMSTR_0:37
for p being PartState of S st IC S in dom p
holds p +* Start-At(IC p,S) = p;
theorem :: MEMSTR_0:38
p +* Start-At(k,S) c= s implies IC s = k;
theorem :: MEMSTR_0:39
for p being PartState of S holds Start-At(0,S) c= p implies IC p = 0;
theorem :: MEMSTR_0:40
for p being PartState of S st Start-At(k,S) c= p holds IC p = k;
registration let N;
let S be IC-Ins-separated non empty
with_non-empty_values Mem-Struct over N;
cluster non empty for PartState of S;
end;
theorem :: MEMSTR_0:41
for S being IC-Ins-separated non empty with_non-empty_values
Mem-Struct over N
for p being non empty PartState of S
holds dom p meets {IC S} \/ Data-Locations S;
begin :: Initialize
definition let N;
let S be IC-Ins-separated non empty
with_non-empty_values Mem-Struct over N;
let p be PartState of S;
func Initialize p -> PartState of S equals
:: MEMSTR_0:def 13
p +* Start-At(0,S);
projectivity;
end;
registration let N,S;
let p be PartState of S;
cluster Initialize p -> 0-started;
end;
theorem :: MEMSTR_0:42
for S being IC-Ins-separated non empty
with_non-empty_values Mem-Struct over N,
p being PartState of S
holds dom Initialize p = dom p \/ {IC S};
theorem :: MEMSTR_0:43
for x being set st x in dom Initialize p holds x in dom p or x = IC S;
theorem :: MEMSTR_0:44
for p being 0-started PartState of S
holds Initialize p = p;
theorem :: MEMSTR_0:45
for p being PartState of S
holds DataPart Initialize p = DataPart p;
theorem :: MEMSTR_0:46
for s being State of S st IC s = 0 holds Initialize s = s;
registration let N,S;
let s be State of S;
cluster Initialize s -> total;
end;
theorem :: MEMSTR_0:47
for p being PartState of S
holds Initialize p c= s implies IC s = 0;
theorem :: MEMSTR_0:48
for p being PartState of S holds IC S in dom Initialize p;
theorem :: MEMSTR_0:49
for p,q being PartState of S holds IC S in dom(p +* Initialize q);
theorem :: MEMSTR_0:50
for S being IC-Ins-separated non empty
with_non-empty_values Mem-Struct over N
for p,q being PartState of S
holds Initialize p c= q implies Start-At(0,S) c= q;
begin :: Increment & Decrement, of the Instruction Counter
definition let N,S;
let p be PartState of S, k be Nat;
func IncIC(p,k) -> PartState of S equals
:: MEMSTR_0:def 14
p +* Start-At(IC p+k,S);
end;
theorem :: MEMSTR_0:51
for p being PartState of S, k being Nat
holds DataPart IncIC(p,k) = DataPart p;
theorem :: MEMSTR_0:52
for p being PartState of S, k being Nat holds IC S in dom IncIC(p,k);
theorem :: MEMSTR_0:53
for p being PartState of S, k being Nat
holds IC IncIC (p,k) = IC p + k;
theorem :: MEMSTR_0:54
for d being data-only PartState of S, k being Nat
holds IncIC(p+*d,k) = IncIC(p,k) +* d;
theorem :: MEMSTR_0:55
for p being PartState of S, k being Nat holds
Start-At(IC p+k,S) c= IncIC (p,k);
theorem :: MEMSTR_0:56
for p being PartState of S st IC S in dom p
holds IncIC( p,k) = DataPart p +* Start-At ((IC p) +k,S);
registration
let N,S;
let s be State of S, k be Nat;
cluster IncIC(s,k) -> total;
end;
theorem :: MEMSTR_0:57
for p being PartState of S, i,j being Nat
holds IncIC(IncIC(p,i),j) = IncIC(p,i+j);
theorem :: MEMSTR_0:58
for p being PartState of S, j,k being Nat
holds IncIC(p +* Start-At(j,S),k) = p +* Start-At(j+k,S);
theorem :: MEMSTR_0:59
for k being Nat
holds IC IncIC(s,k) -' k = IC s;
theorem :: MEMSTR_0:60
for p,q being PartState of S, k being Nat st IC S in dom q
holds IncIC(p+*q,k) = p +* IncIC(q,k);
theorem :: MEMSTR_0:61
for S being IC-Ins-separated non empty with_non-empty_values Mem-Struct over N
for k being Nat, p being PartState of S,
s1, s2 being State of S st p c= s1 & IncIC(p,k) c= s2
holds p c= s1 +* DataPart s2;
theorem :: MEMSTR_0:62
for S being IC-Ins-separated non empty with_non-empty_values Mem-Struct over N
for p being PartState of S, k being Nat
holds DataPart p c= IncIC(p,k);
definition let N,S;
let p be PartState of S, k be Nat;
func DecIC(p,k) -> PartState of S equals
:: MEMSTR_0:def 15
p +* Start-At(IC p-'k,S);
end;
theorem :: MEMSTR_0:63
for p being PartState of S, k being Nat
holds DataPart DecIC(p,k) = DataPart p;
theorem :: MEMSTR_0:64
for k being Nat holds IC S in dom DecIC(p,k);
theorem :: MEMSTR_0:65
for p being PartState of S, k being Nat
holds IC DecIC (p,k) = IC p -' k;
theorem :: MEMSTR_0:66
for p being PartState of S,
d being data-only PartState of S, k being Nat
holds DecIC(p+*d,k) = DecIC(p,k) +* d;
theorem :: MEMSTR_0:67
for p being PartState of S,k being Nat holds
Start-At(IC p-'k,S) c= DecIC (p,k);
theorem :: MEMSTR_0:68
for p being PartState of S, k being Nat st IC S in dom p
holds DecIC( p,k) = DataPart p +* Start-At ((IC p) -'k,S);
registration
let N,S;
let s be State of S, k be Nat;
cluster DecIC(s,k) -> total;
end;
theorem :: MEMSTR_0:69
for p being PartState of S, i,j being Nat
holds DecIC(DecIC(p,i),j) = DecIC(p,i+j);
theorem :: MEMSTR_0:70
for p being PartState of S, j,k being Nat
holds DecIC(p +* Start-At(j,S),k) = p +* Start-At(j-'k,S);
theorem :: MEMSTR_0:71
for s being State of S, k being Nat st k <= IC s
holds IC DecIC(s,k) + k = IC s;
theorem :: MEMSTR_0:72
for p,q being PartState of S, k being Nat st IC S in dom q
holds DecIC(p+*q,k) = p +* DecIC(q,k);
theorem :: MEMSTR_0:73
for p being PartState of S, k being Nat st IC S in dom p
holds DecIC(IncIC(p,k),k) = p;
theorem :: MEMSTR_0:74
for p,q being PartState of S, k being Nat st IC S in dom q
holds DecIC(p+*IncIC(q,k),k) = p +* q;
registration let N,S; let k be Nat;
let p be k-started PartState of S;
cluster DecIC(p,k) -> 0-started;
end;
begin :: Finite Partial States
registration
let N;
let S be IC-Ins-separated non empty
with_non-empty_values Mem-Struct over N;
let l be Nat;
cluster Start-At(l,S) -> finite;
end;
definition let N;
let S be Mem-Struct over N;
mode FinPartState of S is finite PartState of S;
end;
registration
let N;
let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N,
l be Nat;
cluster l-started for FinPartState of S;
end;
registration
let N;
let S be Mem-Struct over N;
let p be FinPartState of S;
cluster DataPart p -> finite;
end;
registration let N,S;
let p be FinPartState of S;
cluster Initialize p -> finite;
end;
registration let N,S;
let p be FinPartState of S, k be Nat;
cluster IncIC(p,k) -> finite;
end;
registration let N,S;
let p be FinPartState of S, k be Nat;
cluster DecIC(p,k) -> finite;
end;
definition
let N;
let S be with_non-empty_values Mem-Struct over N;
func FinPartSt S -> Subset of sproduct the_Values_of S equals
:: MEMSTR_0:def 16
{ p where p is Element of sproduct the_Values_of S: p is finite };
end;
theorem :: MEMSTR_0:75
for S be with_non-empty_values Mem-Struct over N
for p being FinPartState of S holds p in FinPartSt S;
registration
let N;
let S be with_non-empty_values Mem-Struct over N;
cluster FinPartSt S -> non empty;
end;
theorem :: MEMSTR_0:76
for S being with_non-empty_values Mem-Struct over N,
p being Element of FinPartSt S holds
p is FinPartState of S;
definition
let N,S;
let IT be PartFunc of FinPartSt S,FinPartSt S;
attr IT is data-only means
:: MEMSTR_0:def 17
for p being PartState of S st p in dom IT holds p is data-only &
for q being PartState of S st q = IT.p holds q is data-only;
end;
registration let N,S;
cluster data-only for PartFunc of FinPartSt S, FinPartSt S;
end;
begin :: Addenda
theorem :: MEMSTR_0:77
for A being non empty with_non-empty_values Mem-Struct over N, s
being State of A, o being Object of A holds s.o in Values o;
theorem :: MEMSTR_0:78
for A being IC-Ins-separated non empty with_non-empty_values
Mem-Struct over N
for s1,s2 being State of A st IC s1= IC s2 & DataPart s1 =
DataPart s2 holds s1=s2;
theorem :: MEMSTR_0:79
for s being State of S, l being Nat
holds DataPart s = DataPart(s +* Start-At(l,S));
theorem :: MEMSTR_0:80
for s1,s2 be State of S holds
DataPart s1 = DataPart s2 implies
Initialize s1 = Initialize s2;
theorem :: MEMSTR_0:81
the_Values_of Trivial-Mem N = 0 .--> NAT;
::from SCMFSA9A
definition let N,S;
let f be Function of product the_Values_of S, NAT;
attr f is on_data_only means
:: MEMSTR_0:def 18
for s1, s2 being State of S st DataPart s1 = DataPart s2
holds f.s1 = f.s2;
end;