:: Commands Structure
:: by Andrzej Trybulec
::
:: Copyright (c) 2010-2021 Association of Mizar Users

definition
let S be set ;
attr S is standard-ins means :Def1: :: COMPOS_0:def 1
ex X being non empty set st S c= [:NAT,(),(X *):];
end;

:: deftheorem Def1 defines standard-ins COMPOS_0:def 1 :
for S being set holds
( S is standard-ins iff ex X being non empty set st S c= [:NAT,(),(X *):] );

registration
coherence
proof end;
coherence
{[1,{},{}]} is standard-ins
proof end;
end;

notation
let x be object ;
synonym InsCode x for x 1_3 ;
synonym JumpPart x for x 2_3 ;
synonym AddressPart x for x `3_3 ;
end;

definition
let x be object ;
:: original: InsCode
redefine func InsCode x -> set ;
coherence
InsCode x is set
by TARSKI:1;
:: original: JumpPart
redefine func JumpPart x -> set ;
coherence
JumpPart x is set
by TARSKI:1;
redefine func AddressPart x -> set ;
coherence by TARSKI:1;
end;

registration
cluster non empty standard-ins for set ;
existence
ex b1 being set st
( not b1 is empty & b1 is standard-ins )
proof end;
end;

registration
let S be non empty standard-ins set ;
let I be Element of S;
coherence
for b1 being set st b1 = AddressPart I holds
( b1 is Function-like & b1 is Relation-like )
proof end;
coherence
for b1 being set st b1 = JumpPart I holds
( b1 is Function-like & b1 is Relation-like )
proof end;
end;

registration
let S be non empty standard-ins set ;
let I be Element of S;
coherence
for b1 being Function st b1 = AddressPart I holds
b1 is FinSequence-like
proof end;
coherence
for b1 being Function st b1 = JumpPart I holds
b1 is FinSequence-like
proof end;
end;

registration
let S be non empty standard-ins set ;
let x be Element of S;
coherence
proof end;
end;

registration
coherence
for b1 being set st b1 is standard-ins holds
b1 is Relation-like
;
end;

definition
let S be standard-ins set ;
func InsCodes S -> set equals :: COMPOS_0:def 2
proj1_3 S;
correctness
coherence
proj1_3 S is set
;
;
end;

:: deftheorem defines InsCodes COMPOS_0:def 2 :
for S being standard-ins set holds InsCodes S = proj1_3 S;

registration
let S be non empty standard-ins set ;
cluster InsCodes S -> non empty ;
coherence
not InsCodes S is empty
proof end;
end;

definition
let S be non empty standard-ins set ;
mode InsType of S is Element of InsCodes S;
end;

definition
let S be non empty standard-ins set ;
let I be Element of S;
:: original: InsCode
redefine func InsCode I -> InsType of S;
coherence
InsCode I is InsType of S
proof end;
end;

definition
let S be non empty standard-ins set ;
let T be InsType of S;
func JumpParts T -> set equals :: COMPOS_0:def 3
{ () where I is Element of S : InsCode I = T } ;
coherence
{ () where I is Element of S : InsCode I = T } is set
;
func AddressParts T -> set equals :: COMPOS_0:def 4
{ () where I is Element of S : InsCode I = T } ;
coherence
{ () where I is Element of S : InsCode I = T } is set
;
end;

:: deftheorem defines JumpParts COMPOS_0:def 3 :
for S being non empty standard-ins set
for T being InsType of S holds JumpParts T = { () where I is Element of S : InsCode I = T } ;

:: deftheorem defines AddressParts COMPOS_0:def 4 :
for S being non empty standard-ins set
for T being InsType of S holds AddressParts T = { () where I is Element of S : InsCode I = T } ;

registration
let S be non empty standard-ins set ;
let T be InsType of S;
coherence
proof end;
coherence
( not JumpParts T is empty & JumpParts T is functional )
proof end;
end;

definition
let S be non empty standard-ins set ;
attr S is homogeneous means :Def5: :: COMPOS_0:def 5
for I, J being Element of S st InsCode I = InsCode J holds
dom () = dom ();
::$CD attr S is J/A-independent means :Def6: :: COMPOS_0:def 7 for T being InsType of S for f1, f2 being natural-valued Function st f1 in JumpParts T & dom f1 = dom f2 holds for p being object st [T,f1,p] in S holds [T,f2,p] in S; end; :: deftheorem Def5 defines homogeneous COMPOS_0:def 5 : for S being non empty standard-ins set holds ( S is homogeneous iff for I, J being Element of S st InsCode I = InsCode J holds dom () = dom () ); :: deftheorem COMPOS_0:def 6 : canceled; :: deftheorem Def6 defines J/A-independent COMPOS_0:def 7 : for S being non empty standard-ins set holds ( S is J/A-independent iff for T being InsType of S for f1, f2 being natural-valued Function st f1 in JumpParts T & dom f1 = dom f2 holds for p being object st [T,f1,p] in S holds [T,f2,p] in S ); Lm1: for T being InsType of holds JumpParts T = proof end; registration coherence ( is J/A-independent & is homogeneous ) proof end; end; registration existence ex b1 being non empty standard-ins set st ( b1 is J/A-independent & b1 is homogeneous ) proof end; end; registration let S be non empty standard-ins homogeneous set ; let T be InsType of S; coherence proof end; end; registration let S be non empty standard-ins set ; let I be Element of S; coherence for b1 being Function st b1 = JumpPart I holds b1 is NAT -valued proof end; end; Lm2: for S being non empty standard-ins homogeneous set for I being Element of S for x being set st x in dom () holds (product" (JumpParts ())) . x c= NAT proof end; Lm3: for S being non empty standard-ins homogeneous set st S is J/A-independent holds for I being Element of S for x being set st x in dom () holds NAT c= (product" (JumpParts ())) . x proof end; theorem Th1: :: COMPOS_0:1 for S being non empty standard-ins set for I, J being Element of S st InsCode I = InsCode J & JumpPart I = JumpPart J & AddressPart I = AddressPart J holds I = J proof end; registration let S be non empty standard-ins homogeneous J/A-independent set ; let T be InsType of S; coherence proof end; end; definition let S be standard-ins set ; let I be Element of S; attr I is ins-loc-free means :Def7: :: COMPOS_0:def 8 JumpPart I is empty ; end; :: deftheorem Def7 defines ins-loc-free COMPOS_0:def 8 : for S being standard-ins set for I being Element of S holds ( I is ins-loc-free iff JumpPart I is empty ); registration let S be non empty standard-ins set ; let I be Element of S; coherence for b1 being Function st b1 = JumpPart I holds b1 is natural-valued ; end; definition let S be non empty standard-ins homogeneous J/A-independent set ; let I be Element of S; let k be Nat; func IncAddr (I,k) -> Element of S means :Def8: :: COMPOS_0:def 9 ( InsCode it = InsCode I & AddressPart it = AddressPart I & JumpPart it = k + () ); existence ex b1 being Element of S st ( InsCode b1 = InsCode I & AddressPart b1 = AddressPart I & JumpPart b1 = k + () ) proof end; uniqueness for b1, b2 being Element of S st InsCode b1 = InsCode I & AddressPart b1 = AddressPart I & JumpPart b1 = k + () & InsCode b2 = InsCode I & AddressPart b2 = AddressPart I & JumpPart b2 = k + () holds b1 = b2 by Th1; end; :: deftheorem Def8 defines IncAddr COMPOS_0:def 9 : for S being non empty standard-ins homogeneous J/A-independent set for I being Element of S for k being Nat for b4 being Element of S holds ( b4 = IncAddr (I,k) iff ( InsCode b4 = InsCode I & AddressPart b4 = AddressPart I & JumpPart b4 = k + () ) ); theorem :: COMPOS_0:2 canceled; ::$CT
theorem :: COMPOS_0:3
for S being non empty standard-ins homogeneous J/A-independent set
for I being Element of S holds IncAddr (I,0) = I
proof end;

theorem Th3: :: COMPOS_0:4
for k being Nat
for S being non empty standard-ins homogeneous J/A-independent set
for I being Element of S st I is ins-loc-free holds
proof end;

theorem :: COMPOS_0:5
for k being Nat
for S being non empty standard-ins homogeneous J/A-independent set
for I being Element of S holds JumpParts () = JumpParts (InsCode (IncAddr (I,k)))
proof end;

theorem Th5: :: COMPOS_0:6
for S being non empty standard-ins homogeneous J/A-independent set
for I, J being Element of S st ex k being Nat st IncAddr (I,k) = IncAddr (J,k) holds
I = J
proof end;

theorem :: COMPOS_0:7
for k, m being Nat
for S being non empty standard-ins homogeneous J/A-independent set
proof end;

theorem :: COMPOS_0:8
for S being non empty standard-ins homogeneous J/A-independent set
for I being Element of S
for x being set st x in dom () holds
() . x in (product" (JumpParts ())) . x
proof end;

registration
cluster {[0,{},{}],[1,{},{}]} -> standard-ins ;
coherence
{[0,{},{}],[1,{},{}]} is standard-ins
proof end;
end;

theorem Th8: :: COMPOS_0:9
for x being Element of {[0,{},{}],[1,{},{}]} holds JumpPart x = {}
proof end;

Lm4: for T being InsType of {[0,{},{}],[1,{},{}]} holds JumpParts T =
proof end;

registration
coherence
( {[0,{},{}],[1,{},{}]} is J/A-independent & {[0,{},{}],[1,{},{}]} is homogeneous )
proof end;
end;

theorem :: COMPOS_0:10
for S being non empty standard-ins set
for T being InsType of S ex I being Element of S st InsCode I = T
proof end;

theorem :: COMPOS_0:11
for S being non empty standard-ins homogeneous set
for I being Element of S st JumpPart I = {} holds
JumpParts () =
proof end;

:: Wymagamy, zeby zbior instrukcji mial instrukcje z InsCode rowym
:: zero i zeby ta instrukcja to byla [0,{},{}], a wiec ma byc jedyna
:: instrukcja o kodzie 0. Wymaga to modyfikacji
:: maszyny SCMPDS, gdzie z instrukcje halt robi goto 0 (tzn. przeskok
:: o 0);
definition
let X be set ;
attr X is with_halt means :Def9: :: COMPOS_0:def 10
[0,{},{}] in X;
end;

:: deftheorem Def9 defines with_halt COMPOS_0:def 10 :
for X being set holds
( X is with_halt iff [0,{},{}] in X );

registration
cluster with_halt -> non empty for set ;
coherence
for b1 being set st b1 is with_halt holds
not b1 is empty
;
end;

registration
coherence by TARSKI:def 1;
cluster {[0,{},{}],[1,{},{}]} -> with_halt ;
coherence
{[0,{},{}],[1,{},{}]} is with_halt
by TARSKI:def 2;
end;

registration
existence
ex b1 being set st
( b1 is with_halt & b1 is standard-ins )
proof end;
end;

registration
existence
ex b1 being standard-ins with_halt set st
( b1 is J/A-independent & b1 is homogeneous )
proof end;
end;

definition
let S be with_halt set ;
func halt S -> Element of S equals :: COMPOS_0:def 11
[0,{},{}];
coherence
[0,{},{}] is Element of S
by Def9;
end;

:: deftheorem defines halt COMPOS_0:def 11 :
for S being with_halt set holds halt S = [0,{},{}];

registration
let S be standard-ins with_halt set ;
coherence ;
end;

registration
let S be standard-ins with_halt set ;
cluster ins-loc-free for Element of S;
existence
ex b1 being Element of S st b1 is ins-loc-free
proof end;
end;

registration
let S be standard-ins with_halt set ;
let I be ins-loc-free Element of S;
cluster JumpPart I -> empty for set ;
coherence
for b1 being set st b1 = JumpPart I holds
b1 is empty
by Def7;
end;

theorem :: COMPOS_0:12
for k being Nat
for S being non empty standard-ins homogeneous J/A-independent with_halt set
for I being Element of S st IncAddr (I,k) = halt S holds
I = halt S
proof end;

definition
let S be non empty standard-ins homogeneous J/A-independent with_halt set ;
let i be Element of S;
attr i is No-StopCode means :: COMPOS_0:def 12
i <> halt S;
end;

:: deftheorem defines No-StopCode COMPOS_0:def 12 :
for S being non empty standard-ins homogeneous J/A-independent with_halt set
for i being Element of S holds
( i is No-StopCode iff i <> halt S );

definition end;

registration
existence
not for b1 being Instructions holds b1 is trivial
proof end;
end;