:: 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;