:: A Mathematical Model of CPU
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received October 14, 1992
:: Copyright (c) 1992-2011 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, ORDINAL1,
CARD_1, FUNCOP_1, FUNCT_4, RELAT_1, TARSKI, CAT_1, FSM_1, SETFAM_1,
GLIB_000, FINSET_1, CIRCUIT2, NAT_1, ARYTM_3, XXREAL_0, MSUALG_1,
TURING_1, PARTFUN1, MCART_1, ZFMISC_1, GRAPHSP, ARYTM_1, FUNCT_7, AMI_1,
PBOOLE, SCMNORM, GROUP_9, RECDEF_2, COMPOS_1, AMISTD_1, GOBOARD5,
AMISTD_2, CARD_5, UNIALG_1, AMI_2, AMI_3, FINSEQ_1, INT_1, SCMPDS_2,
SCMPDS_1, COMPLEX1, FINSEQ_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, MCART_1, SUBSET_1, SETFAM_1, ORDINAL1,
PBOOLE, CARD_1, XXREAL_0, XCMPLX_0, INT_1, NAT_1, NAT_D, NUMBERS,
FUNCT_7, CARD_3, RELAT_1, FUNCT_1, PARTFUN1, INT_2, FINSET_1, FUNCOP_1,
FUNCT_4, FINSEQ_1, FINSEQ_2, FINSEQ_4, FUNCT_2, DOMAIN_1, RECDEF_2,
STRUCT_0, COMPOS_1, EXTPRO_1, AMISTD_1, AMISTD_2, AMI_2, AMI_3, SCMPDS_1,
SCMPDS_2;
constructors SETFAM_1, DOMAIN_1, FUNCT_4, XXREAL_0, FUNCT_7, GRAPH_2,
RELSET_1, PRE_POLY, PBOOLE, RECDEF_2, COMPOS_1, EXTPRO_1, AMISTD_1,
AMISTD_2, AMI_2, AMI_3, NAT_D, FINSEQ_4, CAT_2, INT_1, SCMPDS_1,
SCMPDS_2;
registrations XBOOLE_0, SETFAM_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2,
FUNCOP_1, FUNCT_4, FINSET_1, XREAL_0, FINSEQ_1, CARD_3, STRUCT_0, INT_1,
RELSET_1, GRFUNC_1, PRE_POLY, PBOOLE, COMPOS_1, EXTPRO_1, AMISTD_1,
AMISTD_2, AMI_2, AMI_3, SCMPDS_1, SCMPDS_2, NUMBERS, XXREAL_0;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: General concepts
reserve N for with_non-empty_elements set;
definition
canceled 12;
let N be with_non-empty_elements set;
let IT be non empty AMI-Struct over N;
attr IT is steady-programmed means
:: AMI_1:def 13
for s being State of IT, i being Instruction of IT,
l being Element of NAT
holds Exec(i,s).l = s.l;
end;
registration
let N be with_non-empty_elements set;
cluster Trivial-AMI N -> steady-programmed;
end;
registration
let N;
cluster IC-Ins-separated halting steady-programmed definite strict (non
empty stored-program AMI-Struct over N);
end;
begin :: General theory
reserve x,y,z,A,B for set,
f,g,h for Function,
i,j,k for Element of NAT;
reserve S for IC-Ins-separated definite
(non empty stored-program AMI-Struct over N),
s for State of S;
reserve E for set;
reserve N for non empty with_non-empty_elements set,
S for IC-Ins-separated definite (non empty stored-program AMI-Struct
over N),
s for State of S;
reserve n for Element of NAT;
canceled 53;
theorem :: AMI_1:54
for S being steady-programmed IC-Ins-separated definite (non
empty stored-program AMI-Struct over N)
for P being (the Instructions of S)-valued ManySortedSet of NAT
for s being State of S, i be
Element of NAT, k holds s.i = Comput(P,s,k).i;
registration
let N;
cluster halting steady-programmed realistic strict
(IC-Ins-separated definite (non empty stored-program AMI-Struct over N));
end;
canceled 26;
theorem :: AMI_1:81
for S being steady-programmed IC-Ins-separated definite (non
empty stored-program AMI-Struct over N) for p being NAT-defined PartState
of S
for P being (the Instructions of S)-valued ManySortedSet of NAT
for s being State of S st p c= s for k
holds p c= Comput(P,s,k);
canceled 4;
theorem :: AMI_1:86
for S being steady-programmed IC-Ins-separated definite (non empty
stored-program AMI-Struct over N), s being State of S,
P being (the Instructions of S)-valued ManySortedSet of NAT,
p being NAT-defined
PartState of S, k holds p c= s iff p c= Comput(P,s,k);
reserve N for with_non-empty_elements non empty set,
S for IC-Ins-separated (non empty AMI-Struct over N);
canceled 12;
theorem :: AMI_1:99
for S being steady-programmed IC-Ins-separated definite (non empty
stored-program AMI-Struct over N) for p being PartState of S,
P being (the Instructions of S)-valued ManySortedSet of NAT,
s being
State of S st p c= s for i being Element of NAT holds ProgramPart p c=
Comput(P,s,i);
canceled 17;
theorem :: AMI_1:117
for N being with_non-empty_elements set for S being
steady-programmed (non empty stored-program AMI-Struct over N) for i being
Instruction of S, s being State of S
holds ProgramPart Exec (i, s) = ProgramPart s;
canceled 5;
reserve m,n for Element of NAT;
theorem :: AMI_1:123
for S being steady-programmed IC-Ins-separated definite (non empty
stored-program AMI-Struct over N)
for P being (the Instructions of S)-valued ManySortedSet of NAT
for s being State of S, n being Nat
holds ProgramPart s = ProgramPart Comput(P,s,n);
theorem :: AMI_1:124
for N being with_non-empty_elements non empty set,
S being steady-programmed
IC-Ins-separated definite (non empty stored-program AMI-Struct over N),
p being NAT-defined (the Instructions of S)-valued Function,
s1,s2 being State of S
st p c= s1 & p c= s2
holds Comput(ProgramPart s1,s1,i) | dom p
= Comput(ProgramPart s2,s2,i) | dom p;
registration
let N be with_non-empty_elements set;
cluster STC N -> steady-programmed;
end;
registration
let N be with_non-empty_elements non empty set;
cluster standard halting realistic steady-programmed
standard-ins (IC-Ins-separated definite (non empty stored-program AMI-Struct
over N));
end;
begin :: Addenda
:: from SCMRING4, 2008.03.13, A.T.
reserve i, j, k for natural number,
n for Element of NAT,
N for with_non-empty_elements non empty set,
S for standard (IC-Ins-separated definite
(non empty stored-program AMI-Struct over N)),
l for Element of NAT,
f for FinPartState of S;
canceled 2;
registration
let N be with_non-empty_elements non empty set;
cluster standard regular J/A-independent homogeneous
halting realistic steady-programmed
with_explicit_jumps (IC-Ins-separated definite standard-ins
(non empty stored-program AMI-Struct over N));
end;
registration
let N be with_non-empty_elements non empty set;
cluster homogeneous realistic steady-programmed
halting
with_explicit_jumps Exec-preserving
(regular J/A-independent standard (standard-ins IC-Ins-separated definite
(non empty stored-program AMI-Struct over N)));
end;
registration
let N be with_non-empty_elements non empty set;
cluster IC-relocable (homogeneous realistic steady-programmed
with_explicit_jumps Exec-preserving halting
(regular J/A-independent standard (standard-ins IC-Ins-separated definite
(non empty stored-program AMI-Struct over N))));
end;
theorem :: AMI_1:127
for S being Exec-preserving IC-Ins-separated definite realistic
steady-programmed (non empty stored-program AMI-Struct over N),
s being State of S, i being Instruction of S,
p being NAT-defined FinPartState of S
holds Exec (i, s +* p) = Exec (i,s) +* p;
reserve d1,d2,d3,d4,d5 for Element of SCM-Data-Loc,
k1,k2,k3,k4,k5,k6 for
Integer;
reserve I for Instruction of SCMPDS;
theorem :: AMI_1:128
for s being State of SCMPDS, i being Instruction of SCMPDS, l
being Element of NAT holds Exec(i,s).l = s.l;
registration
cluster SCMPDS -> steady-programmed;
end;