:: Composition of Machines, Instructions and Programs
:: by Andrzej Trybulec
::
:: Received May 20, 2010
:: Copyright (c) 2010-2021 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 SUBSET_1, XBOOLE_0, FUNCT_1, NUMBERS, CARD_1, FUNCOP_1, FUNCT_4,
RELAT_1, TARSKI, CAT_1, FINSET_1, NAT_1, AFINSQ_1, AMISTD_1, AMISTD_2,
ARYTM_1, VALUED_1, PARTFUN1, ZFMISC_1, AMI_1, ARYTM_3, EXTPRO_1, PBOOLE,
COMPOS_1, RELOC, TURING_1, XXREAL_0, SCMFSA_7, INT_1, SCMPDS_4, ORDINAL4,
SCMFSA6A, FINSEQ_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, MCART_1, SUBSET_1, SETFAM_1,
ORDINAL1, PBOOLE, FUNCT_7, CARD_1, CARD_3, XXREAL_0, XCMPLX_0, RELAT_1,
FUNCT_1, PARTFUN1, FINSET_1, NUMBERS, INT_1, NAT_1, NAT_D, FUNCOP_1,
FUNCT_4, FINSEQ_1, FUNCT_2, DOMAIN_1, VALUED_0, VALUED_1, AFINSQ_1,
STRUCT_0, COMPOS_0;
constructors SETFAM_1, DOMAIN_1, FUNCT_4, XXREAL_0, RELSET_1, FUNCT_7,
PRE_POLY, PBOOLE, AFINSQ_1, NAT_D, WELLORD2, STRUCT_0, COMPOS_0,
XTUPLE_0;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FUNCOP_1,
FUNCT_4, FINSET_1, XREAL_0, RELSET_1, PBOOLE, AFINSQ_1, VALUED_1,
XCMPLX_0, NAT_1, MEMBERED, CARD_1, XXREAL_0, ORDINAL5, COMPOS_0,
XTUPLE_0;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
begin :: General concepts
reserve x,A for set, i,j,k,m,n, l, l1, l2 for Nat;
reserve D for non empty set, z for Nat;
definition
struct COM-Struct(#
InstructionsF -> Instructions
#);
end;
definition
::$CD 7
func Trivial-COM -> strict COM-Struct means
:: COMPOS_1:def 8
the InstructionsF of it = {[0,{},{}]};
end;
definition
let S be COM-Struct;
mode Instruction of S is Element of the InstructionsF of S;
end;
definition
::$CD
let S be COM-Struct;
func halt S -> Instruction of S equals
:: COMPOS_1:def 10
halt the InstructionsF of S;
end;
:: Definicje musi zachowac, zeby nie musiec pisac
:: halt SCM-Instr, zamiast halt SCM, zreszta wyrzucenie jej
:: spowodowaloby problemy z typowaniem.
definition
let S be COM-Struct;
let I be (the InstructionsF of S)-valued Function;
attr I is halt-free means
:: COMPOS_1:def 11
not halt S in rng I;
end;
begin :: General theory
reserve S for COM-Struct;
reserve ins for Element of the InstructionsF of S;
definition
let S be COM-Struct;
mode Instruction-Sequence of S is
(the InstructionsF of S)-valued ManySortedSet of NAT;
end;
definition
let S be COM-Struct;
let P be Instruction-Sequence of S, k be Nat;
redefine func P.k -> Instruction of S;
end;
begin
definition
let S be (COM-Struct);
let p be NAT-defined (the InstructionsF of S)-valued Function, l be set;
pred p halts_at l means
:: COMPOS_1:def 12
l in dom p & p.l = halt S;
end;
definition
let S be COM-Struct;
let s be Instruction-Sequence of S, l be Nat;
redefine pred s halts_at l means
:: COMPOS_1:def 13
s.l = halt S;
end;
begin :: Closedness of finite partial states
notation
let S be COM-Struct;
let i be Instruction of S;
synonym Load i for <%i%>;
end;
registration
let S;
cluster initial 1-element NAT-defined
(the InstructionsF of S)-valued for Function;
end;
definition
let S be COM-Struct;
mode preProgram of S is finite
NAT-defined (the InstructionsF of S)-valued Function;
end;
definition
let S be COM-Struct,
F be non empty preProgram of S;
attr F is halt-ending means
:: COMPOS_1:def 14
F.(LastLoc F) = halt S;
attr F is unique-halt means
:: COMPOS_1:def 15
for f being Nat st
F.f = halt S & f in dom F holds f = LastLoc F;
end;
registration
let S be COM-Struct;
cluster halt-ending -> non halt-free for non empty preProgram of S;
end;
registration
let S be COM-Struct;
cluster trivial initial non empty for preProgram of S;
end;
definition
let S be COM-Struct;
mode Program of S is initial non empty preProgram of S;
end;
::$CT
theorem :: COMPOS_1:2
for ins being Element of the InstructionsF of Trivial-COM holds
InsCode ins = 0;
begin :: Addenda
definition
let S be COM-Struct;
func Stop S -> preProgram of S equals
:: COMPOS_1:def 16
Load halt S;
end;
:: registration
:: let S be COM-Struct;
:: cluster Stop S -> initial non empty;
:: coherence;
:: end;
registration
let S be COM-Struct;
cluster Stop S ->
initial non empty NAT-defined (the InstructionsF of S)-valued trivial;
end;
registration
let S be COM-Struct;
cluster Stop S -> halt-ending unique-halt;
end;
registration let S;
cluster halt-ending unique-halt trivial for Program of S;
end;
definition let S;
mode MacroInstruction of S is halt-ending unique-halt Program of S;
end;
registration
let S be COM-Struct;
cluster initial non empty for preProgram of S;
end;
theorem :: COMPOS_1:3
0 in dom Stop S;
theorem :: COMPOS_1:4
card Stop S = 1;
reserve k, m for Nat,
x, x1, x2, x3, y, y1, y2, y3, X,Y,Z for set;
begin :: Properties of AMI-Struct
theorem :: COMPOS_1:5
for I being Instruction of Trivial-COM holds JumpPart I = 0;
theorem :: COMPOS_1:6
for T being InsType of the InstructionsF of Trivial-COM
holds JumpParts T = {0};
registration
let S be COM-Struct;
cluster trivial -> unique-halt for non empty preProgram of S;
end;
::$CT
theorem :: COMPOS_1:8
for F being MacroInstruction of S st card F = 1 holds F = Stop S;
theorem :: COMPOS_1:9
for S being COM-Struct holds LastLoc Stop S = 0;
begin :: On the composition of macro instructions
definition
::$CD 4
let S be COM-Struct, p be preProgram of S, k be Nat;
func IncAddr(p,k) ->
NAT-defined (the InstructionsF of S)-valued finite Function
means
:: COMPOS_1:def 21
dom it = dom p &
for m being Nat st m in dom p holds it.m = IncAddr(p/.m,k);
end;
registration
let S be COM-Struct, F be preProgram of S, k be Nat;
cluster IncAddr(F,k) -> NAT-defined (the InstructionsF of S)-valued;
end;
registration
let S be COM-Struct, F be empty preProgram of S, k be Nat;
cluster IncAddr(F,k) -> empty;
end;
registration
let S be COM-Struct, F be non empty preProgram of S, k be Nat;
cluster IncAddr(F,k) -> non empty;
end;
registration
let S be COM-Struct, F be initial preProgram of S, k be Nat;
cluster IncAddr(F,k) -> initial;
end;
::$CT 6
registration let S be COM-Struct, F be preProgram of S;
reduce IncAddr(F,0) to F;
end;
::$CT
theorem :: COMPOS_1:17
for S being COM-Struct, F being preProgram of S
holds IncAddr(IncAddr(F,k),m) = IncAddr(F,k+m);
definition
let S be COM-Struct, p be preProgram of S, k be Nat;
func Reloc(p,k) ->
finite NAT-defined (the InstructionsF of S)-valued Function
equals
:: COMPOS_1:def 22
Shift(IncAddr(p,k),k);
end;
theorem :: COMPOS_1:18
for S being COM-Struct, F being Program of S,
G being non empty preProgram of S
holds dom CutLastLoc F misses dom Reloc(G,card F -' 1);
theorem :: COMPOS_1:19
for F being unique-halt Program of S,
I being Nat st I in dom CutLastLoc F
holds (CutLastLoc F).I <> halt S;
definition
let S be COM-Struct;
let F, G be non empty preProgram of S;
func F ';' G -> preProgram of S equals
:: COMPOS_1:def 23
CutLastLoc F +* Reloc(G,card F -' 1);
end;
registration
let S be COM-Struct, F, G be non empty preProgram of S;
cluster F ';' G -> non empty
(the InstructionsF of S)-valued NAT-defined;
end;
theorem :: COMPOS_1:20
for S being COM-Struct, F being Program of S,
G being non empty preProgram of S
holds card (F ';' G) = card F + card G - 1 &
card (F ';' G) = card F + card G -' 1;
registration
let S be COM-Struct;
let F, G be Program of S;
cluster F ';' G -> initial;
end;
theorem :: COMPOS_1:21
for S being COM-Struct, F, G being Program of S
holds dom F c= dom (F ';' G);
registration
let S being COM-Struct, F, G being Program of S;
cluster F ';' G -> initial non empty;
end;
theorem :: COMPOS_1:22
for S being COM-Struct, F, G being Program of S
holds CutLastLoc F c= CutLastLoc (F ';' G);
theorem :: COMPOS_1:23
for S being COM-Struct, F, G being Program of S
holds (F ';' G).LastLoc F = IncAddr(G,card F -' 1).0;
theorem :: COMPOS_1:24
for S being COM-Struct, F, G being Program of S,
f being Nat st f < card F - 1
holds IncAddr(F,card F -' 1).f = IncAddr(F ';' G, card F -' 1).f;
registration
let S be COM-Struct;
let F be Program of S;
let G be halt-ending Program of S;
cluster F ';' G -> halt-ending;
end;
registration
let S be COM-Struct;
let F be MacroInstruction of S;
let G be unique-halt Program of S;
cluster F ';' G -> unique-halt;
end;
definition
let S be COM-Struct;
let F, G be MacroInstruction of S;
redefine func F ';' G -> MacroInstruction of S;
end;
registration let S be COM-Struct, k;
reduce IncAddr(Stop S, k) to Stop S;
end;
::$CT
theorem :: COMPOS_1:26
for k being Nat
for S being COM-Struct
holds Shift(Stop S, k) = k .--> halt S;
registration let S be COM-Struct, F being MacroInstruction of S;
reduce F ';' Stop S to F;
end;
theorem :: COMPOS_1:27
for S being COM-Struct,
F being MacroInstruction of S
holds F ';' Stop S = F;
registration let S be COM-Struct, F be MacroInstruction of S;
reduce Stop S ';' F to F;
end;
theorem :: COMPOS_1:28
for S being COM-Struct,
F being MacroInstruction of S
holds Stop S ';' F = F;
theorem :: COMPOS_1:29
for S being COM-Struct, F, G, H being MacroInstruction of S
holds F ';' G ';' H = F ';' (G ';' H);
::$CT 2
begin :: Addenda
reserve i, j, k for Nat,
n for Nat,
l,il for Nat;
theorem :: COMPOS_1:32
for k being Nat holds
for p being finite NAT-defined (the InstructionsF of S)-valued Function
holds dom Reloc(p,k) = dom Shift(p,k);
theorem :: COMPOS_1:33
for k being Nat holds
for p being finite NAT-defined (the InstructionsF of S)-valued Function
holds dom Reloc(p,k) = { j+k where j is Nat:j in dom p };
theorem :: COMPOS_1:34
for i,j being Nat holds
for p being NAT-defined (the InstructionsF of S)-valued finite Function
holds Shift(IncAddr(p,i),j) = IncAddr(Shift(p,j),i);
theorem :: COMPOS_1:35
for g being NAT-defined (the InstructionsF of S)-valued finite Function
for k being Nat holds
for I being Instruction of S holds
il in dom g & I = g.il implies
IncAddr(I, k) = Reloc(g, k).(il + k);
reserve
i,j,k for Instruction of S,
I,J,K for Program of S;
definition
let S be COM-Struct;
let i be Instruction of S;
redefine func Load i -> preProgram of S;
end;
reserve k1,k2 for Integer;
reserve l,l1,loc for Nat;
definition
let S be COM-Struct;
let I be initial preProgram of S;
func stop I -> preProgram of S equals
:: COMPOS_1:def 24
I ^ Stop S;
end;
registration let S be COM-Struct;
let I be initial preProgram of S;
cluster stop I -> initial non empty;
end;
reserve i1,i2 for Instruction of S;
theorem :: COMPOS_1:36
0 in dom stop I;
begin :: SCMFSA6A
reserve
i,j,k for Instruction of S,
I,J,K for Program of S;
definition
let S be COM-Struct;
let i be Instruction of S;
func Macro i -> preProgram of S equals
:: COMPOS_1:def 25
stop Load i;
end;
registration let S;
let i;
cluster Macro i -> initial non empty;
end;
begin :: SCMFSA7B
reserve m for Nat;
registration
let S be COM-Struct;
cluster Stop S -> halt-ending;
end;
registration
let S be COM-Struct;
cluster non halt-free for Program of S;
end;
registration
let S be COM-Struct;
let p be NAT-defined (the InstructionsF of S)-valued Function,
q be non halt-free
NAT-defined (the InstructionsF of S)-valued Function;
cluster p +* q -> non halt-free;
end;
registration
let S be COM-Struct;
let p be finite non halt-free
NAT-defined (the InstructionsF of S)-valued Function,
k be Nat;
cluster Reloc(p,k) -> non halt-free;
end;
registration
let S be COM-Struct;
cluster non halt-free non empty for Program of S;
end;
::$CT 4
theorem :: COMPOS_1:41
for S being COM-Struct
for p,q being
finite NAT-defined (the InstructionsF of S)-valued Function
holds IncAddr(p +* q, n) = IncAddr(p,n) +* IncAddr(q,n);
theorem :: COMPOS_1:42
for S being COM-Struct
for p,q being finite NAT-defined (the InstructionsF of S)-valued Function,
k be Nat
holds Reloc(p+*q,k) = Reloc(p,k)+*Reloc(q,k);
theorem :: COMPOS_1:43
for S being COM-Struct
for p being finite NAT-defined (the InstructionsF of S)-valued Function,
m,n be Nat
holds Reloc(Reloc(p,m), n) = Reloc(p, m + n);
theorem :: COMPOS_1:44
for S being COM-Struct
for P,Q being NAT-defined (the InstructionsF of S)-valued finite Function,
k being Nat st
P c= Q holds Reloc(P,k) c= Reloc(Q,k);
registration let S be COM-Struct;
let P be preProgram of S;
reduce Reloc(P,0) to P;
end;
theorem :: COMPOS_1:45
for S being COM-Struct
for P being preProgram of S holds Reloc(P,0) = P;
theorem :: COMPOS_1:46
for S being COM-Struct
for k being Nat holds
for P being preProgram of S holds
il in dom P iff il + k in dom Reloc(P,k);
theorem :: COMPOS_1:47
for S be COM-Struct
for i being Instruction of S
for f being Function of the InstructionsF of S, the InstructionsF of S
st f = (id the InstructionsF of S) +* (halt S .--> i)
for s being finite NAT-defined (the InstructionsF of S)-valued Function
holds IncAddr(f*s,n)
= ((id the InstructionsF of S) +* (halt S .--> IncAddr(i,n)))* IncAddr(s,n);
reserve I,J for Program of S;
theorem :: COMPOS_1:48
dom I misses dom Reloc(J, card I);
theorem :: COMPOS_1:49
for I being preProgram of S holds card Reloc(I, m) = card I;
:: from SCMPDS_5, 2011.05.16, A.T.
reserve i for Instruction of S,
I for Program of S;
theorem :: COMPOS_1:50
x in dom Load i iff x = 0;
reserve loc for Nat;
theorem :: COMPOS_1:51
loc in dom stop I & (stop I).loc <> halt S implies loc in dom I;
theorem :: COMPOS_1:52
dom Load i = { 0} & (Load i).0 = i;
theorem :: COMPOS_1:53
0 in dom Load i;
theorem :: COMPOS_1:54
card Load i = 1;
theorem :: COMPOS_1:55
card stop I = card I + 1;
theorem :: COMPOS_1:56
card Macro i = 2;
theorem :: COMPOS_1:57
0 in dom Macro i & 1 in dom Macro i;
theorem :: COMPOS_1:58
(Macro i).0 = i;
theorem :: COMPOS_1:59
(Macro i).1 = halt S;
theorem :: COMPOS_1:60
x in dom Macro i iff x= 0 or x= 1;
theorem :: COMPOS_1:61
dom Macro i = {0,1};
theorem :: COMPOS_1:62
loc in dom I implies loc in dom stop I;
theorem :: COMPOS_1:63
for I being initial preProgram of S st loc in dom I
holds (stop I).loc=I.loc;
theorem :: COMPOS_1:64
card I in dom stop I & (stop I).card I = halt S;
:: from SCMPDS_7, 2011.05.27, A.T.
theorem :: COMPOS_1:65
loc in dom I implies Shift(stop I,n).(loc+n)=Shift(I,n).(loc+n);
theorem :: COMPOS_1:66
Shift(stop I,n). n=Shift(I,n). n;
:: from SCMPDS_5, 2011.05.27,A.T.
registration let S be COM-Struct;
cluster empty for preProgram of S;
end;
registration let S be COM-Struct;
cluster empty -> halt-free for preProgram of S;
end;
definition
::$CD
let S be COM-Struct;
let IT be NAT-defined (the InstructionsF of S)-valued Function;
redefine attr IT is halt-free means
:: COMPOS_1:def 27
for x being Nat st x in dom IT holds IT.x <> halt S;
end;
registration let S be COM-Struct;
cluster halt-free -> unique-halt for non empty preProgram of S;
end;
theorem :: COMPOS_1:67
rng Macro i = {i, halt S};
registration let S;
let p be initial preProgram of S;
reduce CutLastLoc stop p to p;
end;
theorem :: COMPOS_1:68
for p being initial preProgram of S
holds CutLastLoc stop p = p;
registration let S be COM-Struct;
let p be halt-free initial preProgram of S;
cluster stop p -> unique-halt;
end;
registration let S;
let I be Program of S, J be non halt-free Program of S;
cluster I ';' J -> non halt-free;
end;
theorem :: COMPOS_1:69
for I being Program of S holds CutLastLoc stop I = I;
theorem :: COMPOS_1:70
InsCode halt S = 0;
theorem :: COMPOS_1:71
for S being COM-Struct, I being initial preProgram of S
holds card stop I -' 1 = card I;
theorem :: COMPOS_1:72
for S being COM-Struct, I being initial preProgram of S
holds card stop I = card I + 1;
theorem :: COMPOS_1:73
LastLoc stop I = card I;
registration
let S,I;
cluster stop I -> halt-ending;
end;
theorem :: COMPOS_1:74
Macro IncAddr(i,n) = IncAddr(Macro i,n);
theorem :: COMPOS_1:75
I ';' J = (CutLastLoc I) ^ IncAddr(J,card I -' 1);
theorem :: COMPOS_1:76
IncAddr(Macro i,n) = IncAddr(Load i,n) ^ Stop S;
theorem :: COMPOS_1:77
for S being COM-Struct, F, G being Program of S,
n being Nat st n < LastLoc F
holds F.n = (F ';' G).n;