:: On a Mathematical Model of Programs
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received December 29, 1992
:: Copyright (c) 1992-2018 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, XBOOLE_0, CARD_1, ZFMISC_1, FINSEQ_1, FUNCT_1,
RELAT_1, AMI_1, PARTFUN1, XXREAL_0, TARSKI, AMI_2, RECDEF_2, UNIALG_1,
AMISTD_2, VALUED_0, COMPOS_0, NAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, CARD_1,
NUMBERS, RELAT_1, FUNCT_1, PARTFUN1, VALUED_0, XXREAL_0, MCART_1,
DOMAIN_1, FINSEQ_1, FINSEQ_4, RECDEF_2, COMPOS_0;
constructors DOMAIN_1, FINSEQ_4, FINSEQ_2, VALUED_1, COMPOS_0, XTUPLE_0;
registrations XBOOLE_0, ORDINAL1, XREAL_0, FINSEQ_1, RELAT_1, CARD_1, FUNCT_1,
COMPOS_0, VALUED_0, XTUPLE_0;
requirements NUMERALS, REAL, SUBSET, BOOLE;
begin :: A small concrete machine
reserve x,y,z for set;
notation
synonym SCM-Halt for 0;
end;
definition
redefine func SCM-Halt -> Element of Segm 9;
end;
definition
func SCM-Data-Loc -> set equals
:: SCM_INST:def 1
[:{1},NAT:];
end;
registration
cluster SCM-Data-Loc -> non empty;
end;
reserve I,J,K for Element of Segm 9,
i,a,a1,a2 for Nat,
b,b1,b2,c,c1 for Element of SCM-Data-Loc;
definition
func SCM-Instr -> non empty set equals
:: SCM_INST:def 2
{[SCM-Halt,{},{}] } \/ { [J,<*a*>,{}] : J = 6 }
\/ { [K,<*a1*>,<*b1*>] : K in { 7,8 } }
\/ { [I,{},<*b,c*>] : I in { 1,2,3,4,5} };
end;
theorem :: SCM_INST:1
[0,{},{}] in SCM-Instr;
registration
cluster SCM-Instr -> non empty;
end;
theorem :: SCM_INST:2
[6,<*a2*>,{}] in SCM-Instr;
theorem :: SCM_INST:3
x in { 7, 8 } implies [x,<*a2*>,<*b2*>] in SCM-Instr;
theorem :: SCM_INST:4
x in { 1,2,3,4,5} implies [x,{},<*b1,c1*>] in SCM-Instr;
definition
let x be Element of SCM-Instr;
given mk, ml being Element of SCM-Data-Loc, I such that
x = [ I, {}, <*mk, ml*>];
func x address_1 -> Element of SCM-Data-Loc means
:: SCM_INST:def 3
ex f being FinSequence of SCM-Data-Loc st f = x`3_3 & it = f/.1;
func x address_2 -> Element of SCM-Data-Loc means
:: SCM_INST:def 4
ex f being FinSequence of SCM-Data-Loc st f = x`3_3 & it = f/.2;
end;
theorem :: SCM_INST:5
for x being Element of SCM-Instr, mk, ml being Element of SCM-Data-Loc, I
st x = [ I, {}, <*mk, ml*>] holds x address_1 = mk & x address_2 = ml;
definition
let x be Element of SCM-Instr;
given mk being Nat, I such that
x = [ I, <*mk*>, {}];
func x jump_address -> Nat means
:: SCM_INST:def 5
ex f being FinSequence of NAT st f = x`2_3 & it = f/.1;
end;
theorem :: SCM_INST:6
for x being Element of SCM-Instr, mk being Nat, I st x = [
I, <*mk*>, {}] holds x jump_address = mk;
definition
let x be Element of SCM-Instr;
given mk being Nat, ml being Element of SCM-Data-Loc, I such that
x = [ I, <*mk*>, <*ml*>];
func x cjump_address -> Nat means
:: SCM_INST:def 6
ex mk being Element of NAT st <*mk*> = x`2_3 & it = <*mk*>/.1;
func x cond_address -> Element of SCM-Data-Loc means
:: SCM_INST:def 7
ex ml being Element of SCM-Data-Loc st <*ml*> = x`3_3 & it = <*ml*>/.1;
end;
theorem :: SCM_INST:7
for x being Element of SCM-Instr, mk being Nat, ml being
Element of SCM-Data-Loc, I
st x = [ I, <*mk*>, <*ml*>] holds x cjump_address = mk &
x cond_address = ml;
theorem :: SCM_INST:8
SCM-Instr c= [:NAT,NAT*,proj2 SCM-Instr:];
registration
cluster proj2 SCM-Instr -> FinSequence-membered;
end;
theorem :: SCM_INST:9
for x being Element of SCM-Instr holds
x in {[SCM-Halt,{},{}] } & InsCode x = 0 or
x in { [J,<*a*>,{}] : J = 6 } & InsCode x = 6 or
x in { [K,<*a1*>,<*b1*>] : K in { 7,8 } }
& (InsCode x = 7 or InsCode x = 8) or
x in { [I,{},<*b,c*>] : I in { 1,2,3,4,5} }
& (InsCode x = 1 or InsCode x = 2 or InsCode x = 3
or InsCode x = 4 or InsCode x = 5);
begin :: from AMI_3
reserve i,j,k for Nat;
registration
cluster SCM-Instr -> standard-ins;
end;
reserve I,J,K for Element of Segm 9,
a,a1,a2 for Nat,
b,b1,b2,c,c1 for Element of SCM-Data-Loc;
theorem :: SCM_INST:10
for l being Element of SCM-Instr holds InsCode l <= 8;
registration
cluster SCM-Instr -> homogeneous;
end;
reserve T for InsType of SCM-Instr,
I for Element of SCM-Instr;
registration
cluster SCM-Instr -> J/A-independent;
end;
registration
cluster SCM-Instr -> with_halt;
end;