:: On the Composition of Macro Instructions of Standard Computers
:: by Artur Korni{\l}owicz
::
:: Received April 14, 2000
:: Copyright (c) 2000-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, ORDINAL1, SETFAM_1, ARYTM_1, ARYTM_3, CARD_1, SUBSET_1,
AMI_1, XBOOLE_0, RELAT_1, TARSKI, FUNCOP_1, GLIB_000, GOBOARD5, AMISTD_1,
FUNCT_1, CARD_3, FRECHET, STRUCT_0, FSM_1, FUNCT_4, TURING_1, CIRCUIT2,
AMISTD_2, PARTFUN1, EXTPRO_1, NAT_1, RELOC, XXREAL_0, COMPOS_1, QUANTAL1,
GOBRD13, MEMSTR_0;
notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, ORDINAL1, SETFAM_1, MEMBERED,
RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4, PBOOLE, CARD_1, NUMBERS,
XCMPLX_0, XXREAL_0, NAT_1, CARD_3, FINSEQ_1, FUNCOP_1, NAT_D, FUNCT_7,
VALUED_0, VALUED_1, AFINSQ_1, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1,
MEASURE6, EXTPRO_1, AMISTD_1;
constructors WELLORD2, REALSET1, NAT_D, AMISTD_1, XXREAL_2, PRE_POLY,
AFINSQ_1, ORDINAL4, VALUED_1, NAT_1, FUNCT_7, PBOOLE, FUNCT_4, MEMSTR_0,
RELSET_1, MEASURE6, XTUPLE_0;
registrations RELAT_1, FUNCT_1, FUNCOP_1, FINSET_1, XREAL_0, NAT_1, MEMBERED,
CARD_3, STRUCT_0, AMISTD_1, CARD_1, FUNCT_4, AFINSQ_1, EXTPRO_1,
MEMSTR_0, MEASURE6, COMPOS_0, XTUPLE_0;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
begin :: Properties of AMI-Struct
reserve k, m for Nat,
x, x1, x2, x3, y, y1, y2, y3, X,Y,Z for set,
N for with_zero set;
theorem :: AMISTD_2:1
for I being Instruction of STC N holds JumpPart I = 0;
definition
let N be with_zero set,
S be IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N, I be Instruction of S;
attr I is with_explicit_jumps means
:: AMISTD_2:def 1
JUMP I = rng JumpPart I;
end;
definition
let N be with_zero set,
S be IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
attr S is with_explicit_jumps means
:: AMISTD_2:def 2
for I being Instruction of S holds I is with_explicit_jumps;
end;
registration
let N be with_zero set;
cluster standard for IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
end;
theorem :: AMISTD_2:2
for S being standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N, I being Instruction of S
st for f being Element of NAT holds NIC(I,f)={f+1}
holds JUMP I is empty;
registration
let N be with_zero set,
I be Instruction of STC N;
cluster JUMP I -> empty;
end;
theorem :: AMISTD_2:3
for T being InsType of the InstructionsF of STC N holds JumpParts T = {0};
registration
let N be with_zero set;
cluster STC N -> with_explicit_jumps;
end;
registration
let N be with_zero set;
cluster standard
halting with_explicit_jumps for IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
end;
registration
let N be with_zero set,
I be Instruction of Trivial-AMI N;
cluster JUMP I -> empty;
end;
registration
let N be with_zero set;
cluster Trivial-AMI N -> with_explicit_jumps;
end;
registration
let N be with_zero set;
cluster with_explicit_jumps halting
for IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;
end;
registration
let N be with_zero set;
let S be with_explicit_jumps IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
cluster -> with_explicit_jumps for Instruction of S;
end;
theorem :: AMISTD_2:4
for S being IC-Ins-separated non empty with_non-empty_values
AMI-Struct over N,
I being Instruction of S st I is halting holds JUMP I is empty;
registration
let N be with_zero set,
S be halting
IC-Ins-separated non empty with_non-empty_values AMI-Struct over N,
I be halting Instruction of S;
cluster JUMP I -> empty;
end;
theorem :: AMISTD_2:5
for S being halting with_explicit_jumps
IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N,
I being Instruction of S st I is ins-loc-free holds JUMP I is empty;
registration
let N be with_zero set,
S be with_explicit_jumps
IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
cluster halting -> ins-loc-free for Instruction of S;
end;
registration
let N be with_zero set,
S be with_explicit_jumps
IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;
cluster sequential -> ins-loc-free for Instruction of S;
end;
begin :: On the composition of macro instructions
registration
let N be with_zero set,
S be halting with_explicit_jumps IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N,
I be halting Instruction of S, k be Nat;
cluster IncAddr(I,k) -> halting;
end;
theorem :: AMISTD_2:6
for S being standard halting
with_explicit_jumps IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N,
I being Instruction of S st I is sequential
holds IncAddr(I,k) is sequential;
definition
let N be with_zero set,
S be halting
IC-Ins-separated non empty with_non-empty_values AMI-Struct over N,
I be Instruction of S;
attr I is IC-relocable means
:: AMISTD_2:def 3
for j,k being Nat, s being State of S
holds IC Exec(IncAddr(I,j),s) + k = IC Exec(IncAddr(I,j+k),IncIC(s,k));
end;
definition
let N be with_zero set,
S be halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
attr S is IC-relocable means
:: AMISTD_2:def 4
for I being Instruction of S holds I is IC-relocable;
end;
registration
let N be with_zero set,
S be with_explicit_jumps IC-Ins-separated halting
non empty with_non-empty_values AMI-Struct over N;
cluster sequential -> IC-relocable for Instruction of S;
end;
registration
let N be with_zero set,
S be with_explicit_jumps IC-Ins-separated halting
non empty with_non-empty_values AMI-Struct over N;
cluster halting -> IC-relocable for Instruction of S;
end;
registration
let N be with_zero set;
cluster STC N -> IC-relocable;
end;
registration
let N be with_zero set;
cluster halting with_explicit_jumps
for standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
end;
registration
let N be with_zero set;
cluster IC-relocable for
with_explicit_jumps halting
standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
end;
registration
let N be with_zero set,
S be IC-relocable IC-Ins-separated halting
non empty with_non-empty_values AMI-Struct over N;
cluster -> IC-relocable for Instruction of S;
end;
registration
let N be with_zero set,
S be with_explicit_jumps IC-Ins-separated halting
non empty with_non-empty_values AMI-Struct over N;
cluster IC-relocable for Instruction of S;
end;
theorem :: AMISTD_2:7
for S be halting
with_explicit_jumps
IC-Ins-separated non empty with_non-empty_values
AMI-Struct over N,
I being IC-relocable Instruction of S
for k being Nat, s being State of S
holds IC Exec(I,s) + k = IC Exec(IncAddr(I,k),IncIC(s,k));
registration
let N be with_zero set,
S be IC-relocable standard with_explicit_jumps
halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N,
F, G be really-closed Program of S;
cluster F ';' G -> really-closed;
end;
theorem :: AMISTD_2:8
for I being Instruction of Trivial-AMI N holds JumpPart I = 0;
theorem :: AMISTD_2:9
for T being InsType of the InstructionsF of Trivial-AMI N
holds JumpParts T = {0};
reserve n,m for Nat;
theorem :: AMISTD_2:10
for S being IC-Ins-separated non empty with_non-empty_values AMI-Struct over N
for s being State of S, I being Program of S
for P1,P2 being Instruction-Sequence of S
st I c= P1 & I c= P2 &
for m st m < n holds IC Comput(P2,s,m) in dom I
for m st m <= n holds Comput(P1,s,m) = Comput(P2,s,m);
theorem :: AMISTD_2:11
for S being IC-Ins-separated halting non empty with_non-empty_values
AMI-Struct over N,
P being Instruction-Sequence of S,
s being State of S st s = Following(P,s)
holds for n holds Comput(P,s,n) = s;