:: Standard Ordering of Instruction Locations
:: by Andrzej Trybulec , Piotr Rudnicki and 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, XBOOLE_0, SUBSET_1, SETFAM_1, AMI_1, FSM_1, FUNCT_4,
FUNCOP_1, RELAT_1, TARSKI, STRUCT_0, FUNCT_1, CARD_3, ZFMISC_1, CIRCUIT2,
CAT_1, NAT_1, GLIB_000, XXREAL_0, PARTFUN1, FINSEQ_1, ARYTM_3, CARD_1,
GOBOARD5, FUNCT_2, FINSEQ_4, ARYTM_1, FINSET_1, FRECHET, AMISTD_1,
EXTPRO_1, COMPOS_1, AMISTD_2, SCMFSA6B, QUANTAL1, GOBRD13, MEMSTR_0,
FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, SETFAM_1, ORDINAL1,
CARD_1, XXREAL_0, NUMBERS, XCMPLX_0, NAT_1, MEMBERED, FUNCT_1, RELSET_1,
PARTFUN1, XTUPLE_0, MCART_1, VALUED_1, DOMAIN_1, CARD_3, FINSEQ_1,
FINSEQ_4, FUNCOP_1, FINSET_1, FUNCT_4, FUNCT_7, AFINSQ_1, PBOOLE,
MEASURE6, STRUCT_0, GRAPH_2, NAT_D, XXREAL_2, MEMSTR_0, COMPOS_0,
COMPOS_1, EXTPRO_1, FUNCT_2;
constructors WELLORD2, REAL_1, FINSEQ_4, REALSET1, NAT_D, XXREAL_2, COMPOS_1,
EXTPRO_1, RELSET_1, PRE_POLY, GRAPH_2, AFINSQ_1, MCART_1, FUNCT_7,
PBOOLE, XXREAL_1, FUNCT_4, MEASURE6, MEMSTR_0, XTUPLE_0;
registrations SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, FINSET_1,
XREAL_0, NAT_1, MEMBERED, FINSEQ_1, CARD_3, FUNCT_7, STRUCT_0, CARD_1,
RELSET_1, FUNCT_4, AFINSQ_1, COMPOS_1, EXTPRO_1, PRE_POLY, MEMSTR_0,
MEASURE6, COMPOS_0, XTUPLE_0, INT_1;
requirements NUMERALS, BOOLE, REAL, SUBSET, ARITHM;
begin :: AMI-Struct
reserve x for set,
D for non empty set,
k, n for Nat,
z for Nat;
reserve
N for with_zero set,
S for IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N,
i for Element of the InstructionsF of S,
l, l1, l2, l3 for Nat,
s for State of S;
registration
let N be with_zero set, S be
with_non-empty_values AMI-Struct over N,
i be Element of the InstructionsF of S, s be State of S;
cluster ((the Execution of S).i).s -> Function-like Relation-like;
end;
registration let N;
cluster non empty with_non-empty_values for AMI-Struct over N;
end;
definition
let N be with_zero set;
let S be non empty with_non-empty_values AMI-Struct over N;
let T be InsType of the InstructionsF of S;
attr T is jump-only means
:: AMISTD_1:def 1
for s being State of S, o being Object of S, I
being Instruction of S st InsCode I = T &
o in Data-Locations S
holds Exec(I, s).o = s.o;
end;
definition
let N be with_zero set;
let S be non empty with_non-empty_values AMI-Struct over N;
let I be Instruction of S;
attr I is jump-only means
:: AMISTD_1:def 2
InsCode I is jump-only;
end;
reserve ss for Element of product the_Values_of S;
definition
let N,S; let l be Nat;
let i be Element of the InstructionsF of S;
func NIC(i,l) -> Subset of NAT equals
:: AMISTD_1:def 3
{ IC Exec(i,ss) : IC ss = l };
end;
registration
let N be with_zero set,
S be IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N, i be Element of the
InstructionsF of S, l be Nat;
cluster NIC(i,l) -> non empty;
end;
definition
let N,S,i;
func JUMP i -> Subset of NAT equals
:: AMISTD_1:def 4
meet the set of all NIC(i,l) ;
end;
definition
let N,S; let l be Nat;
func SUCC(l,S) -> Subset of NAT equals
:: AMISTD_1:def 5
union the set of all NIC(i,l) \ JUMP i ;
end;
theorem :: AMISTD_1:1
for i being Element of the InstructionsF of S
st for l being Nat holds NIC(i,l)={l}
holds JUMP i is empty;
theorem :: AMISTD_1:2
for S being IC-Ins-separated non empty with_non-empty_values
AMI-Struct over N,
il being Nat, i being Instruction of S st i is halting
holds NIC(i,il) = {il};
begin :: Ordering of Instruction Locations
definition
let N, S;
attr S is standard means
:: AMISTD_1:def 6
for m, n being Nat holds m <= n iff
ex f being non empty FinSequence of NAT st f/.1 = m & f/.len f = n &
for n st 1 <= n & n < len f holds f/.(n+1) in SUCC(f/.n,S);
end;
theorem :: AMISTD_1:3
S is standard iff
for k being Nat holds k+1 in SUCC(k,S) &
for j being Nat st j in SUCC(k,S) holds k <= j;
begin :: Standard trivial computer
definition
let N be with_zero set;
func STC N -> strict AMI-Struct over N means
:: AMISTD_1:def 7
the carrier of it = {0} & IC it = 0 &
the InstructionsF of it = {[0,0,0],[1,0,0]} &
the Object-Kind of it = (0 .--> 0) &
the ValuesF of it = N --> NAT &
ex f being Function of product the_Values_of it,
product the_Values_of it st
(for s being Element of product the_Values_of it
holds f.s = s+*(0 .-->(In(s.0,NAT) + 1))) &
the Execution of it = ([1,0,0] .--> f) +*
([0,0,0] .--> id product the_Values_of it);
end;
registration
let N be with_zero set;
cluster STC N -> finite non empty;
end;
registration
let N be with_zero set;
cluster STC N -> with_non-empty_values;
end;
registration
let N be with_zero set;
cluster STC N -> IC-Ins-separated;
end;
theorem :: AMISTD_1:4
for i being Instruction of STC N st InsCode i = 0 holds i is halting;
theorem :: AMISTD_1:5
for i being Instruction of STC N st InsCode i = 1 holds i is non halting;
theorem :: AMISTD_1:6
for i being Element of the InstructionsF of STC N
holds InsCode i = 1 or InsCode i = 0;
theorem :: AMISTD_1:7
for i being Instruction of STC N holds i is jump-only;
registration let N;
cluster -> ins-loc-free for Instruction of STC N;
end;
theorem :: AMISTD_1:8
for l being Nat st l = z holds SUCC(l,STC N) = {z, z+1};
registration
let N be with_zero set;
cluster STC N -> standard;
end;
registration
let N be with_zero set;
cluster STC N -> halting;
end;
registration
let N be with_zero set;
cluster standard halting for IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
end;
reserve T for standard IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N;
theorem :: AMISTD_1:9
for i being Instruction of STC N, s being State of STC N st InsCode i = 1
holds Exec(i,s).IC STC N = IC s + 1;
theorem :: AMISTD_1:10
for l being Nat, i being Element of the
InstructionsF of STC N st InsCode i = 1 holds NIC(i, l) = {l+1};
theorem :: AMISTD_1:11
for l being Nat holds SUCC(l,STC N) = {l, l + 1};
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 sequential means
:: AMISTD_1:def 8
for s being State of S holds Exec(i, s).IC S = IC s + 1;
end;
theorem :: AMISTD_1:12
for S being IC-Ins-separated non empty with_non-empty_values
AMI-Struct over N,
il being Nat, i being Instruction of S st i is sequential
holds NIC(i,il) = {il + 1};
registration
let N;
let S be IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
cluster sequential -> non halting for Instruction of S;
cluster halting -> non sequential for Instruction of S;
end;
theorem :: AMISTD_1:13
for T being IC-Ins-separated non empty with_non-empty_values AMI-Struct over N
for i being Instruction of T st JUMP i is non empty holds i is non
sequential;
begin :: Closedness of finite partial states
definition
let N be with_zero set;
let S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;
let F be finite preProgram of S;
attr F is really-closed means
:: AMISTD_1:def 9
for l being Nat st l in dom F holds NIC (F/.l, l) c= dom F;
end;
::$CD
definition
let N be with_zero set;
let S be halting IC-Ins-separated non empty with_non-empty_values
AMI-Struct over N;
let F be NAT-defined (the InstructionsF of S)-valued Function;
attr F is parahalting means
:: AMISTD_1:def 11
for s being 0-started State of S
for P being Instruction-Sequence of S st F c= P
holds P halts_on s;
end;
theorem :: AMISTD_1:14
for N being with_zero set
for S being IC-Ins-separated non empty with_non-empty_values AMI-Struct over N
for F being finite preProgram of S
holds F is really-closed iff
for s being State of S st IC s in dom F
for k being Nat holds IC Comput(F,s,k) in dom F;
registration let N;
let S be halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
cluster Stop S -> really-closed;
end;
::$CT 2
registration
let N be with_zero set;
let S be standard halting IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N;
cluster really-closed trivial for MacroInstruction of S;
end;
theorem :: AMISTD_1:17
for i being Instruction of Trivial-AMI(N) holds i is halting;
theorem :: AMISTD_1:18
for i being Element of the InstructionsF of Trivial-AMI N holds InsCode i = 0
;
begin :: Addenda
:: from SCMPDS_9, 2008.03.10, A.T.
theorem :: AMISTD_1:19
for N being with_zero set, S
being IC-Ins-separated non empty with_non-empty_values AMI-Struct over N,
i being Instruction of S, l being Nat
holds JUMP(i) c= NIC(i,l);
theorem :: AMISTD_1:20
for i being Instruction of STC N, s being State of STC N st InsCode i = 1
holds Exec(i,s) = IncIC(s,1);
registration let N; let p be PartState of STC N;
cluster DataPart p -> empty;
end;
theorem :: AMISTD_1:21
for N being with_zero set
for S being IC-Ins-separated non empty with_non-empty_values AMI-Struct over N
for F being finite preProgram of S
holds F is really-closed iff
for s being State of S st IC s in dom F
for P being Instruction-Sequence of S st F c= P
for k being Nat holds IC Comput(P,s,k) in dom F;
registration
let N be with_zero set;
let S be halting IC-Ins-separated non empty with_non-empty_values
AMI-Struct over N;
cluster parahalting
for finite non halt-free non empty
NAT-defined (the InstructionsF of S)-valued Function;
end;