:: Commands Structure
:: by Andrzej Trybulec
::
:: Received May 20, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users


begin

definition
let S be set ;
attrS 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
proofend;
cluster{[1,{},{}]} ->  standard-ins ;
coherence
 {[1,{},{}]} is standard-ins
proofend;
end;

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

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

registration
let S be non empty standard-ins set ;
let I be Element of S;
cluster AddressPart I ->  Relation-like Function-like ;
coherence
 ( AddressPart I is Function-like & AddressPart I is Relation-like )
proofend;
cluster JumpPart I ->  Relation-like Function-like ;
coherence
 ( JumpPart I is Function-like & JumpPart I is Relation-like )
proofend;
end;

registration
let S be non empty standard-ins set ;
let I be Element of S;
cluster AddressPart I ->  FinSequence-like ;
coherence
 AddressPart I is FinSequence-like
proofend;
cluster JumpPart I ->  FinSequence-like ;
coherence
 JumpPart I is FinSequence-like
proofend;
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
proofend;
end;

registration
cluster standard-ins  ->  Relation-like for set ;
coherence
 for b1 being set st b1 is standard-ins holds
b1 is Relation-like
proofend;
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
proofend;
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
proofend;
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
proofend;
cluster JumpParts T ->  non empty functional ;
coherence
 ( not JumpParts T is empty & JumpParts T is functional )
proofend;
end;

definition
let S be non empty standard-ins set ;
attrS 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);
canceled;
attrS is J/A-independent  means :Def7: :: 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 set 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 Def7 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 set st [T,f1,p] in S holds
[T,f2,p] in S );

Lm1:  for T being InsType of {[0,{},{}]} holds JumpParts T = {0}
proofend;

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

registration
cluster non empty Relation-like standard-ins homogeneous J/A-independent for set ;
existence
 ex b1 being non empty standard-ins set st
( b1 is J/A-independent & b1 is homogeneous )
proofend;
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
proofend;
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 b1 being Function st b1 = JumpPart I holds
b1 is NAT -valued
proofend;
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
proofend;

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

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

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
proofend;
end;

definition
let S be standard-ins set ;
let I be Element of S;
attrI is ins-loc-free  means :Def8: :: COMPOS_0:def 8
 JumpPart I is empty ;
end;

:: deftheorem Def8 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 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 :Def9: :: COMPOS_0:def 9
( InsCode it = InsCode I & AddressPart it = AddressPart I & JumpPart it = k + (JumpPart I) );
existence
 ex b1 being Element of S st
( InsCode b1 = InsCode I & AddressPart b1 = AddressPart I & JumpPart b1 = k + (JumpPart I) )
proofend;
uniqueness
 for b1, b2 being Element of S st InsCode b1 = InsCode I & AddressPart b1 = AddressPart I & JumpPart b1 = k + (JumpPart I) & InsCode b2 = InsCode I & AddressPart b2 = AddressPart I & JumpPart b2 = k + (JumpPart I) holds
b1 = b2 by Th1;
end;

:: deftheorem Def9 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 + (JumpPart I) ) );

theorem :: COMPOS_0:2
canceled;

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

theorem Th4: :: 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
proofend;

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)))
proofend;

theorem Th6: :: 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
proofend;

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))
proofend;

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

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

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

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

registration
cluster{[0,{},{}],[1,{},{}]} ->  homogeneous J/A-independent ;
coherence
 ( {[0,{},{}],[1,{},{}]} is J/A-independent & {[0,{},{}],[1,{},{}]} is homogeneous )
proofend;
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
proofend;

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}
proofend;

begin

:: 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 ;
attrX is with_halt  means :Def10: :: COMPOS_0:def 10
[0,{},{}] in X;
end;

:: deftheorem Def10 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 by Def10;
end;

registration
cluster{[0,{},{}]} ->  with_halt ;
coherence
 {[0,{},{}]} is with_halt
proofend;
cluster{[0,{},{}],[1,{},{}]} ->  with_halt ;
coherence
 {[0,{},{}],[1,{},{}]} is with_halt
proofend;
end;

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

registration
cluster non empty Relation-like standard-ins homogeneous J/A-independent with_halt for set ;
existence
 ex b1 being standard-ins with_halt set st
( b1 is J/A-independent & b1 is homogeneous )
proofend;
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 Def10;
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
proofend;
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
proofend;
end;

registration
let S be standard-ins with_halt set ;
let I be ins-loc-free Element of S;
cluster JumpPart I ->  empty ;
coherence
 JumpPart I is empty by Def8;
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
proofend;

definition
let S be non empty standard-ins homogeneous J/A-independent with_halt set ;
let i be Element of S;
attri 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 );

begin

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 b1 being Instructions holds b1 is trivial
proofend;
end;