:: The Instructions for the SCMPDS computer
:: by JingChao Chen
::
:: Received June 15, 1999
:: Copyright (c) 1999-2016 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, SUBSET_1, CARD_1, AMI_2, INT_1, XBOOLE_0, FINSEQ_1,
TARSKI, RELAT_1, FUNCT_1, AMI_1, PARTFUN1, XXREAL_0, ZFMISC_1, SCMPDS_1,
RECDEF_2, UNIALG_1, AMISTD_2, VALUED_0, COMPOS_0;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1,
FUNCT_1, PARTFUN1, MCART_1, ORDINAL1, CARD_1, NUMBERS, VALUED_0, INT_1,
FINSEQ_1, FINSEQ_4, XXREAL_0, RECDEF_2, COMPOS_0, SCM_INST;
constructors FINSEQ_4, AMI_2, DOMAIN_1, COMPOS_0, VALUED_0, XTUPLE_0, NUMBERS;
registrations XBOOLE_0, ORDINAL1, NUMBERS, INT_1, FINSEQ_1, XXREAL_0, FUNCT_1,
COMPOS_0, SCM_INST, VALUED_0, RELAT_1, FINSEQ_4, XTUPLE_0, CARD_1;
requirements NUMERALS, REAL, SUBSET, BOOLE;
begin :: Preliminaries
reserve
i, j, k for Element of NAT,
I,I2,I3,I4 for Element of Segm 15,
i1 for Element of NAT,
d1,d2,d3,d4,d5 for Element of SCM-Data-Loc,
k1,k2 for Integer;
theorem :: SCMPDS_I:1
for k be Integer holds k in SCM-Data-Loc \/ INT;
begin :: The construction of SCM with Push-Down Stack
:: [0,goto L]
:: [1,return sp<-sp+0,count<-(sp)+2]
:: [2,a:=c(constant)]
:: [3,saveIC (a,k)]
:: [4,if(a,k)<>0 goto L ]
:: [5,if(a,k)<=0 goto L ]
:: [6,if(a,k)>=0 goto L ]
:: [7,(a,k):=c(constant) ]
:: [8,(a,k1)+k2]
:: [9, (a1,k1)+(a2,k2)]
:: [10,(a1,k1)-(a2,k2)]
:: [11,(a1,k1)*(a2,k2)]
:: [12,(a1,k1)/(a2,k2)]
:: [13,(a1,k1):=(a2,k2)]
definition
func SCMPDS-Instr
-> set equals
:: SCMPDS_I:def 1
{[0,{},{}]}
\/ (the set of all [14,{},<*l*>] where l is Element of INT)
\/ (the set of all [1,{},<*sp*> ] where sp is Element of SCM-Data-Loc)
\/ { [I,{},<*v,c*>]
where I is Element of Segm 15,v is Element of SCM-Data-Loc,
c is Element of INT: I in {2,3} }
\/ { [I,{},<*v,c1,c2*>] where I is Element of Segm 15,
v is Element of SCM-Data-Loc, c1,c2 is Element of INT: I in {4,5,6,7,8} }
\/ { [I,{},<*v1,v2,c1,c2*>]
where I is Element of Segm 15, v1,v2 is Element of SCM-Data-Loc, c1,c2 is
Element of INT: I in {9,10,11,12,13} };
end;
theorem :: SCMPDS_I:2
[14,{},<*0*>] in SCMPDS-Instr;
registration
cluster SCMPDS-Instr -> non empty;
end;
definition
let d be Element of SCM-Data-Loc, s be Integer;
redefine func <*d,s*> -> FinSequence of SCM-Data-Loc \/ INT;
end;
definition
let x be Element of SCMPDS-Instr;
given mk be Element of SCM-Data-Loc, I such that
x = [I,{},<*mk*>];
func x address_1 -> Element of SCM-Data-Loc means
:: SCMPDS_I:def 2
ex f being FinSequence of SCM-Data-Loc st f = x`3_3 & it = f/.1;
end;
theorem :: SCMPDS_I:3
for x being Element of SCMPDS-Instr, mk being Element of SCM-Data-Loc
st x = [I,{},<*mk*>] holds x address_1 = mk;
definition
let x be Element of SCMPDS-Instr;
given r being Integer, I such that
x = [I,{},<*r*>];
func x const_INT -> Integer means
:: SCMPDS_I:def 3
ex f being FinSequence of INT st f = x`3_3 & it = f/.1;
end;
theorem :: SCMPDS_I:4
for x being Element of SCMPDS-Instr, k being Integer st x = [ I,{}, <*k*>
] holds x const_INT = k;
definition
let x be Element of SCMPDS-Instr;
given mk being Element of SCM-Data-Loc, r being Integer, I such that
x = [I,{},<*mk,r*>];
func x P21address -> Element of SCM-Data-Loc means
:: SCMPDS_I:def 4
ex f being FinSequence of SCM-Data-Loc \/ INT st f = x`3_3 & it = f/.1;
func x P22const -> Integer means
:: SCMPDS_I:def 5
ex f being FinSequence of SCM-Data-Loc \/ INT st f = x`3_3 & it = f/.2;
end;
theorem :: SCMPDS_I:5
for x being Element of SCMPDS-Instr, mk being Element of SCM-Data-Loc,
r being Integer st x = [I,{},<*mk,r*>] holds x P21address = mk & x P22const = r
;
definition
let x be Element of SCMPDS-Instr;
given m1 being Element of SCM-Data-Loc,k1,k2 be Integer,I such that
x = [I,{},<*m1,k1,k2*>];
func x P31address -> Element of SCM-Data-Loc means
:: SCMPDS_I:def 6
ex f being FinSequence of (SCM-Data-Loc \/ INT) st f = x`3_3 & it = f/.1;
func x P32const -> Integer means
:: SCMPDS_I:def 7
ex f being FinSequence of SCM-Data-Loc \/ INT st f = x`3_3 & it = f/.2;
func x P33const -> Integer means
:: SCMPDS_I:def 8
ex f being FinSequence of ( SCM-Data-Loc \/ INT) st f = x`3_3 & it = f/.3;
end;
theorem :: SCMPDS_I:6
for x being Element of SCMPDS-Instr, d1 being Element of SCM-Data-Loc,
k1,k2 being Integer st x = [I,{}, <*d1,k1,k2*>] holds x P31address = d1 & x
P32const = k1 & x P33const = k2;
definition
let x be Element of SCMPDS-Instr;
given m1,m2 being Element of SCM-Data-Loc,k1,k2 be Integer,I such that
x = [I,{},<*m1,m2,k1,k2*>];
func x P41address -> Element of SCM-Data-Loc means
:: SCMPDS_I:def 9
ex f being FinSequence of (SCM-Data-Loc \/ INT) st f = x`3_3 & it = f/.1;
func x P42address -> Element of SCM-Data-Loc means
:: SCMPDS_I:def 10
ex f being FinSequence of (SCM-Data-Loc \/ INT) st f = x`3_3 & it = f/.2;
func x P43const -> Integer means
:: SCMPDS_I:def 11
ex f being FinSequence of ( SCM-Data-Loc \/ INT) st f = x`3_3 & it = f/.3;
func x P44const -> Integer means
:: SCMPDS_I:def 12
ex f being FinSequence of ( SCM-Data-Loc \/ INT) st f = x`3_3 & it = f/.4;
end;
theorem :: SCMPDS_I:7
for x being Element of SCMPDS-Instr, d1,d2 being Element of
SCM-Data-Loc, k1,k2 being Integer st x = [I,{}, <*d1,d2,k1,k2*>] holds x
P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2;
:: RetSP: Return Stack Pointer
:: RetIC: Return Instruction-Counter
definition
func RetSP -> Element of NAT equals
:: SCMPDS_I:def 13
0;
func RetIC -> Element of NAT equals
:: SCMPDS_I:def 14
1;
end;
theorem :: SCMPDS_I:8
for x being Element of SCMPDS-Instr holds
x in {[0,{},{}]} & InsCode x = 0 or
x in the set of all [14,{},<*l*>] where l is Element of INT &
InsCode x = 14 or
x in the set of all [1,{},<*sp*> ] where sp is Element of SCM-Data-Loc
& InsCode x = 1 or
x in { [I,{},<*v,c*>]
where I is Element of Segm 15,v is Element of SCM-Data-Loc,
c is Element of INT: I in {2,3} }
& (InsCode x = 2 or InsCode x = 3) or
x in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15,
v is Element of SCM-Data-Loc, c1,c2 is Element of INT: I in {4,5,6,7,8} }
& (InsCode x = 4 or InsCode x = 5 or
InsCode x = 6 or InsCode x = 7 or InsCode x = 8) or
x in { [I,{},<*v1,v2,c1,c2*>]
where I is Element of Segm 15, v1,v2 is Element of SCM-Data-Loc, c1,c2 is
Element of INT: I in {9,10,11,12,13} }
& (InsCode x = 9 or InsCode x = 10 or InsCode x = 11
or InsCode x = 12 or InsCode x = 13);
begin
reserve x for set,
k for Element of NAT;
registration
cluster proj2 SCMPDS-Instr -> FinSequence-membered;
end;
registration
cluster SCMPDS-Instr -> standard-ins;
end;
registration
cluster SCMPDS-Instr -> homogeneous;
end;
registration
cluster SCMPDS-Instr -> J/A-independent;
end;
registration
cluster SCMPDS-Instr -> with_halt;
end;