:: Commands Structure
:: by Andrzej Trybulec
::
:: Received May 20, 2010
:: 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,(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,(NAT *),(X *):] );

registration

cluster {[0,{},{}]} -> standard-ins ;

coherence
{[0,{},{}]} is standard-ins

proof end;

cluster {[1,{},{}]} -> standard-ins ;

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;
:: original: AddressPart
redefine func AddressPart x -> set ;
coherence
AddressPart x is set by TARSKI:1;

end;

registration

cluster non empty standard-ins for set ;

existence
ex b₁ being set st
( not b₁ is empty & b₁ is standard-ins )

proof end;

end;

registration

let S be non empty standard-ins set ;
let I be Element of S;

cluster AddressPart I -> Relation-like Function-like for set ;

coherence
for b₁ being set st b₁ = AddressPart I holds
( b₁ is Function-like & b₁ is Relation-like )

proof end;

cluster JumpPart I -> Relation-like Function-like for set ;

coherence
for b₁ being set st b₁ = JumpPart I holds
( b₁ is Function-like & b₁ is Relation-like )

proof end;

end;

registration

let S be non empty standard-ins set ;
let I be Element of S;

cluster AddressPart I -> FinSequence-like for Function;

coherence
for b₁ being Function st b₁ = AddressPart I holds
b₁ is FinSequence-like

proof end;

cluster JumpPart I -> FinSequence-like for Function;

coherence
for b₁ being Function st b₁ = JumpPart I holds
b₁ is FinSequence-like

proof end;

end;

registration

let S be non empty standard-ins set ;
let x be Element of S;

cluster InsCode x -> natural ;

coherence
InsCode x is natural

proof end;

end;

registration

cluster standard-ins -> Relation-like for set ;

coherence
for b₁ being set st b₁ is standard-ins holds
b₁ 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
{ (JumpPart I) where I is Element of S : InsCode I = T } ;

coherence
{ (JumpPart I) where I is Element of S : InsCode I = T } is set ;

func AddressParts T -> set equals :: COMPOS_0:def 4
{ (AddressPart I) where I is Element of S : InsCode I = T } ;

coherence
{ (AddressPart I) 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 = { (JumpPart I) 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 = { (AddressPart I) where I is Element of S : InsCode I = T } ;

registration

let S be non empty standard-ins set ;
let T be InsType of S;

cluster AddressParts T -> functional ;

coherence
AddressParts T is functional

proof end;

cluster JumpParts T -> non empty functional ;

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 (JumpPart I) = dom (JumpPart J);

::$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 (JumpPart I) = dom (JumpPart J) );

:: 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 {[0,{},{}]} holds JumpParts T = {0}

proof end;

registration

cluster {[0,{},{}]} -> homogeneous J/A-independent ;

coherence
( {[0,{},{}]} is J/A-independent & {[0,{},{}]} is homogeneous )

proof end;

end;

registration

cluster non empty Relation-like standard-ins homogeneous J/A-independent for set ;

existence
ex b₁ being non empty standard-ins set st
( b₁ is J/A-independent & b₁ is homogeneous )

proof end;

end;

registration

let S be non empty standard-ins homogeneous set ;
let T be InsType of S;

cluster JumpParts T -> with_common_domain ;

coherence
JumpParts T is with_common_domain

proof end;

end;

registration

let S be non empty standard-ins set ;
let I be Element of S;

cluster JumpPart I -> NAT -valued for Function;

coherence
for b₁ being Function st b₁ = JumpPart I holds
b₁ 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 (JumpPart I) holds
(product" (JumpParts (InsCode I))) . 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 (JumpPart I) holds
NAT c= (product" (JumpParts (InsCode I))) . 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;

cluster JumpParts T -> product-like ;

coherence
JumpParts T is product-like

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;

cluster JumpPart I -> natural-valued for Function;

coherence
for b₁ being Function st b₁ = JumpPart I holds
b₁ 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 + (JumpPart I) );

existence
ex b₁ being Element of S st
( InsCode b₁ = InsCode I & AddressPart b₁ = AddressPart I & JumpPart b₁ = k + (JumpPart I) )

proof end;

uniqueness
for b₁, b₂ being Element of S st InsCode b₁ = InsCode I & AddressPart b₁ = AddressPart I & JumpPart b₁ = k + (JumpPart I) & InsCode b₂ = InsCode I & AddressPart b₂ = AddressPart I & JumpPart b₂ = k + (JumpPart I) holds
b₁ = b₂ 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 b₄ being Element of S holds
( b₄ = IncAddr (I,k) iff ( InsCode b₄ = InsCode I & AddressPart b₄ = AddressPart I & JumpPart b₄ = k + (JumpPart I) ) );

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
IncAddr (I,k) = I

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 (InsCode I) = 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
for I being Element of S holds IncAddr ((IncAddr (I,k)),m) = IncAddr (I,(k + m))

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 (JumpPart I) holds
(JumpPart I) . x in (product" (JumpParts (InsCode I))) . 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 = {0}

proof end;

registration

cluster {[0,{},{}],[1,{},{}]} -> homogeneous J/A-independent ;

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 (InsCode I) = {0}

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 b₁ being set st b₁ is with_halt holds
not b₁ is empty ;

end;

registration

cluster {[0,{},{}]} -> with_halt ;

coherence
{[0,{},{}]} is with_halt by TARSKI:def 1;

cluster {[0,{},{}],[1,{},{}]} -> with_halt ;

coherence
{[0,{},{}],[1,{},{}]} is with_halt by TARSKI:def 2;

end;

registration

cluster standard-ins with_halt for set ;

existence
ex b₁ being set st
( b₁ is with_halt & b₁ is standard-ins )

proof end;

end;

registration

cluster non empty Relation-like standard-ins homogeneous J/A-independent with_halt for set ;

existence
ex b₁ being standard-ins with_halt set st
( b₁ is J/A-independent & b₁ 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 ;

cluster halt S -> ins-loc-free ;

coherence
halt S is ins-loc-free ;

end;

registration

let S be standard-ins with_halt set ;

cluster ins-loc-free for Element of S;

existence
ex b₁ being Element of S st b₁ 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 b₁ being set st b₁ = JumpPart I holds
b₁ 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

mode Instructions is standard-ins homogeneous J/A-independent with_halt set ;

end;

registration

cluster non empty non trivial Relation-like standard-ins homogeneous J/A-independent with_halt for set ;

existence
not for b₁ being Instructions holds b₁ is trivial

proof end;

end;