:: Normal Computers
:: by Andrzej Trybulec
::
:: Received March 3, 2008
:: Copyright (c) 2008 Association of Mizar Users

registration

let N be set ;
let S be AMI-Struct of NAT ,N;
cluster -> natural Instruction-Location of S;
coherence
for b₁ being Instruction-Location of S holds b₁ is natural ;

end;

notation

let N be set ;
let S be AMI-Struct of NAT ,N;
let l be Instruction-Location of S;
synonym Next l for succ N;

end;

definition

let N be set ;
let S be AMI-Struct of NAT ,N;
let l be Instruction-Location of S;
:: original: Next
redefine func Next l -> Instruction-Location of S;
coherence
Next is Instruction-Location of S by AMI_1:def 4;

end;

definition

let N be set ;
let S be AMI-Struct of NAT ,N;
let l be Instruction-Location of S;
let k be Nat;
:: original: +
redefine func l + k -> Instruction-Location of S;
coherence
l + k is Instruction-Location of S

proof end;

:: original: -'
redefine func l -' k -> Instruction-Location of S;
coherence
l -' k is Instruction-Location of S

proof end;

end;

definition

let N be with_non-empty_elements set ;
let S be non empty stored-program definite AMI-Struct of NAT ,N;
let p be FinPartState of S;
let k be Element of NAT ;
:: original: Shift
redefine func Shift p,k -> FinPartState of S;
coherence
Shift p,k is FinPartState of S

proof end;

end;

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program definite AMI-Struct of NAT ,N;
let p be programmed FinPartState of S;
let k be Element of NAT ;
cluster Shift p,k -> programmed FinPartState of S;
coherence
Shift p,k is programmed FinPartState of S

proof end;

end;

definition

let IL, N be set ;
let S be AMI-Struct of IL,N;
let p be finite PartFunc of NAT ,the Instructions of S;
let k be Element of NAT ;
:: original: Shift
redefine func Shift p,k -> finite PartFunc of NAT ,the Instructions of S;
coherence
Shift p,k is finite PartFunc of NAT ,the Instructions of S

proof end;

end;

definition

let IL, N be set ;
let S be AMI-Struct of IL,N;
mode preProgram of S is programmed FinPartState of S;

end;

definition

let F be Function;
attr F is initial means :Def1: :: SCMNORM:def 1
for m, n being Nat st n in dom F & m < n holds
m in dom F;

end;

:: deftheorem Def1 defines initial SCMNORM:def 1 :

for F being Function holds
( F is initial iff for m, n being Nat st n in dom F & m < n holds
m in dom F );

registration

cluster empty -> initial set ;
coherence
for b₁ being Function st b₁ is empty holds
b₁ is initial

proof end;

end;

registration

let IL, N be set ;
let S be AMI-Struct of IL,N;
cluster empty Element of sproduct the Object-Kind of S;
existence
ex b₁ being FinPartState of S st b₁ is empty

proof end;

end;

registration

let IL, N be set ;
let S be AMI-Struct of IL,N;
cluster empty -> programmed Element of sproduct the Object-Kind of S;
coherence
for b₁ being FinPartState of S st b₁ is empty holds
b₁ is programmed

proof end;

end;

registration

let IL, N be set ;
let S be AMI-Struct of IL,N;
cluster initial Element of sproduct the Object-Kind of S;
existence
ex b₁ being preProgram of S st b₁ is initial

proof end;

end;

definition

let IL, N be set ;
let S be AMI-Struct of IL,N;
mode Program of S is initial preProgram of S;

end;

theorem :: SCMNORM:1

for IL being set
for n being Element of NAT
for S being AMI-Struct of NAT ,IL
for I, J being FinPartState of S holds Shift (ProgramPart (I +* J)),n = (Shift (ProgramPart I),n) +* (Shift (ProgramPart J),n)

proof end;

registration

cluster -> initial set ;
coherence
for b₁ being XFinSequence holds b₁ is initial

proof end;

end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program halting definite AMI-Struct of NAT ,N;
func Stop S -> Program of S equals :: SCMNORM:def 2
<%(halt S)%>;
coherence
<%(halt S)%> is Program of S

proof end;

end;

:: deftheorem defines Stop SCMNORM:def 2 :

for N being non empty with_non-empty_elements set
for S being non empty stored-program halting definite AMI-Struct of NAT ,N holds Stop S = <%(halt S)%>;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program halting definite AMI-Struct of NAT ,N;
cluster Stop S -> non empty ;
coherence
not Stop S is empty ;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program halting definite AMI-Struct of NAT ,N;
cluster non empty programmed initial Element of sproduct the Object-Kind of S;
existence
ex b₁ being FinPartState of S st
( b₁ is initial & b₁ is programmed & not b₁ is empty )

proof end;

end;

theorem :: SCMNORM:2

for N being non empty with_non-empty_elements set
for S being non empty stored-program halting definite AMI-Struct of NAT ,N holds 0 in dom (Stop S)

proof end;

theorem :: SCMNORM:3

for N being non empty with_non-empty_elements set
for S being non empty stored-program halting definite AMI-Struct of NAT ,N holds card (Stop S) = 1

proof end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program halting definite AMI-Struct of NAT ,N;
let p be finite PartFunc of NAT ,the Instructions of S;
func [p] -> preProgram of S equals :: SCMNORM:def 3
p;
coherence
p is preProgram of S

proof end;

end;

:: deftheorem defines [ SCMNORM:def 3 :

for N being non empty with_non-empty_elements set
for S being non empty stored-program halting definite AMI-Struct of NAT ,N
for p being finite PartFunc of NAT ,the Instructions of S holds [p] = p;

definition

let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program definite AMI-Struct of IL,N;
let p be FinPartState of S;
:: original: ProgramPart
redefine func ProgramPart p -> finite PartFunc of IL,the Instructions of S;
coherence
ProgramPart p is finite PartFunc of IL,the Instructions of S

proof end;

end;

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of NAT ,N;
let I be initial FinPartState of S;
cluster ProgramPart I -> initial Function;
coherence
ProgramPart I is initial Function

proof end;

end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty IC-Ins-separated AMI-Struct of NAT ,N;
let p be finite PartFunc of NAT ,the Instructions of S;
let s be State of S;
assume Z: IC s in dom p ;
func CurInstr p,s -> Instruction of S equals :Def4: :: SCMNORM:def 4
p . (IC s);
coherence
p . (IC s) is Instruction of S by Z, PARTFUN1:27;

end;

:: deftheorem Def4 defines CurInstr SCMNORM:def 4 :

for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of NAT ,N
for p being finite PartFunc of NAT ,the Instructions of S
for s being State of S st IC s in dom p holds
CurInstr p,s = p . (IC s);

definition

let N be non empty with_non-empty_elements set ;
let S be non empty IC-Ins-separated AMI-Struct of NAT ,N;
let p be finite PartFunc of NAT ,the Instructions of S;
let s be State of S;
func Following p,s -> State of S equals :: SCMNORM:def 5
Exec (CurInstr p,s),s;
coherence
Exec (CurInstr p,s),s is State of S ;

end;

:: deftheorem defines Following SCMNORM:def 5 :

for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of NAT ,N
for p being finite PartFunc of NAT ,the Instructions of S
for s being State of S holds Following p,s = Exec (CurInstr p,s),s;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty IC-Ins-separated AMI-Struct of NAT ,N;
let p be finite PartFunc of NAT ,the Instructions of S;
deffunc H₁( set , State of S) -> State of S = Following p,$2;
let s be State of S;
let k be Nat;
func Comput p,s,k -> State of S means :Def6: :: SCMNORM:def 6
ex f being Function of NAT , product the Object-Kind of S st
( it = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following p,(f . i) ) );
existence
ex b₁ being State of S ex f being Function of NAT , product the Object-Kind of S st
( b₁ = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following p,(f . i) ) )

proof end;

uniqueness
for b₁, b₂ being State of S st ex f being Function of NAT , product the Object-Kind of S st
( b₁ = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following p,(f . i) ) ) & ex f being Function of NAT , product the Object-Kind of S st
( b₂ = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following p,(f . i) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines Comput SCMNORM:def 6 :

for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of NAT ,N
for p being finite PartFunc of NAT ,the Instructions of S
for s being State of S
for k being Nat
for b₆ being State of S holds
( b₆ = Comput p,s,k iff ex f being Function of NAT , product the Object-Kind of S st
( b₆ = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following p,(f . i) ) ) );

definition

let N be non empty with_non-empty_elements set ;
let S be non empty IC-Ins-separated AMI-Struct of NAT ,N;
let p be finite PartFunc of NAT ,the Instructions of S;
mode Autonomy of p -> FinPartState of S means :Def7: :: SCMNORM:def 7
for s1, s2 being State of S st it c= s1 & it c= s2 holds
for q1, q2 being finite PartFunc of NAT ,the Instructions of S st p c= q1 & p c= q2 holds
for i being Nat holds (Comput q1,s1,i) | (dom it) = (Comput q2,s2,i) | (dom it);
existence
ex b₁ being FinPartState of S st
for s1, s2 being State of S st b₁ c= s1 & b₁ c= s2 holds
for q1, q2 being finite PartFunc of NAT ,the Instructions of S st p c= q1 & p c= q2 holds
for i being Nat holds (Comput q1,s1,i) | (dom b₁) = (Comput q2,s2,i) | (dom b₁)

proof end;

end;

:: deftheorem Def7 defines Autonomy SCMNORM:def 7 :

for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of NAT ,N
for p being finite PartFunc of NAT ,the Instructions of S
for b₄ being FinPartState of S holds
( b₄ is Autonomy of p iff for s1, s2 being State of S st b₄ c= s1 & b₄ c= s2 holds
for q1, q2 being finite PartFunc of NAT ,the Instructions of S st p c= q1 & p c= q2 holds
for i being Nat holds (Comput q1,s1,i) | (dom b₄) = (Comput q2,s2,i) | (dom b₄) );

theorem :: SCMNORM:4

for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of NAT ,N
for p being finite PartFunc of NAT ,the Instructions of S
for s being State of S holds Comput p,s,0 = s

proof end;

theorem Tx1: :: SCMNORM:5

for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of NAT ,N
for p being finite PartFunc of NAT ,the Instructions of S
for s being State of S
for k being Nat holds Comput p,s,(k + 1) = Following p,(Comput p,s,k)

proof end;

theorem :: SCMNORM:6

for N being non empty with_non-empty_elements set
for S being non empty realistic AMI-Struct of NAT ,N
for p being FinPartState of S st IC S in dom p holds
not dom p c= NAT by AMI_1:def 21;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty halting IC-Ins-separated AMI-Struct of NAT ,N;
let f be finite PartFunc of NAT ,the Instructions of S;
let s be State of S;
pred f halts_on s means :Def8: :: SCMNORM:def 8
ex n being Element of NAT st
( IC (Comput f,s,n) in dom f & CurInstr f,(Comput f,s,n) = halt S );

end;

:: deftheorem Def8 defines halts_on SCMNORM:def 8 :

for N being non empty with_non-empty_elements set
for S being non empty halting IC-Ins-separated AMI-Struct of NAT ,N
for f being finite PartFunc of NAT ,the Instructions of S
for s being State of S holds
( f halts_on s iff ex n being Element of NAT st
( IC (Comput f,s,n) in dom f & CurInstr f,(Comput f,s,n) = halt S ) );

definition

let N be non empty with_non-empty_elements set ;
let S be non empty halting IC-Ins-separated AMI-Struct of NAT ,N;
let f be finite PartFunc of NAT ,the Instructions of S;
let p be Autonomy of f;
attr p is halting means :Def9: :: SCMNORM:def 9
for s being State of S st p c= s holds
f halts_on s;

end;

:: deftheorem Def9 defines halting SCMNORM:def 9 :

for N being non empty with_non-empty_elements set
for S being non empty halting IC-Ins-separated AMI-Struct of NAT ,N
for f being finite PartFunc of NAT ,the Instructions of S
for p being Autonomy of f holds
( p is halting iff for s being State of S st p c= s holds
f halts_on s );

theorem Th7: :: SCMNORM:7

for i, j being Nat st i <= j holds
for N being non empty with_non-empty_elements set
for S being non empty halting IC-Ins-separated AMI-Struct of NAT ,N
for f being finite PartFunc of NAT ,the Instructions of S
for s being State of S st CurInstr f,(Comput f,s,i) = halt S holds
Comput f,s,j = Comput f,s,i

proof end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty halting IC-Ins-separated AMI-Struct of NAT ,N;
let f be finite PartFunc of NAT ,the Instructions of S;
let s be State of S;
assume A1: f halts_on s ;
func Result f,s -> State of S means :Def10: :: SCMNORM:def 10
ex k being Element of NAT st
( it = Comput f,s,k & CurInstr f,it = halt S );
uniqueness
for b₁, b₂ being State of S st ex k being Element of NAT st
( b₁ = Comput f,s,k & CurInstr f,b₁ = halt S ) & ex k being Element of NAT st
( b₂ = Comput f,s,k & CurInstr f,b₂ = halt S ) holds
b₁ = b₂

proof end;

correctness
existence
ex b₁ being State of S ex k being Element of NAT st
( b₁ = Comput f,s,k & CurInstr f,b₁ = halt S );

proof end;

end;

:: deftheorem Def10 defines Result SCMNORM:def 10 :

for N being non empty with_non-empty_elements set
for S being non empty halting IC-Ins-separated AMI-Struct of NAT ,N
for f being finite PartFunc of NAT ,the Instructions of S
for s being State of S st f halts_on s holds
for b₅ being State of S holds
( b₅ = Result f,s iff ex k being Element of NAT st
( b₅ = Comput f,s,k & CurInstr f,b₅ = halt S ) );

definition

let N be non empty with_non-empty_elements set ;
let S be non empty halting IC-Ins-separated realistic AMI-Struct of NAT ,N;
let f be finite PartFunc of NAT ,the Instructions of S;
let p be Autonomy of f;
assume A1: p is halting ;
consider h being State of S such that
A10: p c= h by CARD_3:97;
func Result f,p -> FinPartState of S means :: SCMNORM:def 11
for p' being State of S st p c= p' holds
it = (Result f,p') | (dom p);
existence
ex b₁ being FinPartState of S st
for p' being State of S st p c= p' holds
b₁ = (Result f,p') | (dom p)

proof end;

correctness
uniqueness
for b₁, b₂ being FinPartState of S st ( for p' being State of S st p c= p' holds
b₁ = (Result f,p') | (dom p) ) & ( for p' being State of S st p c= p' holds
b₂ = (Result f,p') | (dom p) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem defines Result SCMNORM:def 11 :

for N being non empty with_non-empty_elements set
for S being non empty halting IC-Ins-separated realistic AMI-Struct of NAT ,N
for f being finite PartFunc of NAT ,the Instructions of S
for p being Autonomy of f st p is halting holds
for b₅ being FinPartState of S holds
( b₅ = Result f,p iff for p' being State of S st p c= p' holds
b₅ = (Result f,p') | (dom p) );

definition

let N be non empty with_non-empty_elements set ;
let S be non empty halting IC-Ins-separated realistic AMI-Struct of NAT ,N;
let f be finite PartFunc of NAT ,the Instructions of S;
let p be FinPartState of S;
let F be Function;
pred f,p computes F means :: SCMNORM:def 12
for s being FinPartState of S st s in dom F holds
ex q being Autonomy of f st
( q = s +* p & q is halting & F . s c= Result f,q );

end;

:: deftheorem defines computes SCMNORM:def 12 :

for N being non empty with_non-empty_elements set
for S being non empty halting IC-Ins-separated realistic AMI-Struct of NAT ,N
for f being finite PartFunc of NAT ,the Instructions of S
for p being FinPartState of S
for F being Function holds
( f,p computes F iff for s being FinPartState of S st s in dom F holds
ex q being Autonomy of f st
( q = s +* p & q is halting & F . s c= Result f,q ) );

theorem :: SCMNORM:8

for N being non empty with_non-empty_elements set
for S being non empty halting IC-Ins-separated steady-programmed AMI-Struct of NAT ,N
for s being State of S
for f being finite PartFunc of NAT ,the Instructions of S
for k being Element of NAT st IC (Comput f,s,k) in dom f & f . (IC (Comput f,s,k)) = halt S holds
Result f,s = Comput f,s,k

proof end;

theorem :: SCMNORM:9

for N being with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of NAT ,N
for l1, l2 being Instruction-Location of S
for k being Element of NAT holds
( Start-At (l1 + k) = Start-At (l2 + k) iff Start-At l1 = Start-At l2 )

proof end;

theorem :: SCMNORM:10

for N being with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of NAT ,N
for l1, l2 being Instruction-Location of S
for k being Nat st Start-At l1 = Start-At l2 holds
Start-At (l1 -' k) = Start-At (l2 -' k)

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty IC-Ins-separated AMI-Struct of NAT ,N;
let p be FinPartState of S;
let k be Element of NAT ;
func IncrIC p,k -> FinPartState of S equals :: SCMNORM:def 13
p +* (Start-At ((IC p) + k));
correctness
coherence
p +* (Start-At ((IC p) + k)) is FinPartState of S;
;

end;

:: deftheorem defines IncrIC SCMNORM:def 13 :

for N being with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of NAT ,N
for p being FinPartState of S
for k being Element of NAT holds IncrIC p,k = p +* (Start-At ((IC p) + k));

theorem Th11: :: SCMNORM:11

for N being with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of NAT ,N
for l being Instruction-Location of S holds DataPart (Start-At l) = {} by AMI_1:138;

theorem :: SCMNORM:12

for N being with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of NAT ,N
for p being FinPartState of S
for k being Element of NAT holds DataPart (IncrIC p,k) = DataPart p

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty IC-Ins-separated AMI-Struct of NAT ,N;
let s be State of S;
func DataPart s -> PartState of S equals :: SCMNORM:def 14
s | (Data-Locations S);
coherence
s | (Data-Locations S) is PartState of S ;

end;

:: deftheorem defines DataPart SCMNORM:def 14 :

for N being with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of NAT ,N
for s being State of S holds DataPart s = s | (Data-Locations S);

theorem Th13: :: SCMNORM:13

for N being with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of NAT ,N
for s being State of S holds Data-Locations S c= dom s

proof end;

theorem :: SCMNORM:14

for N being with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of NAT ,N
for s being State of S holds dom (DataPart s) = Data-Locations S

proof end;

theorem Th15: :: SCMNORM:15

for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of NAT ,N holds NAT misses Data-Locations S

proof end;

theorem :: SCMNORM:16

for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of NAT ,N
for f being finite PartFunc of NAT ,the Instructions of S holds DataPart [f] = {}

proof end;

theorem Th17: :: SCMNORM:17

for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of NAT ,N
for l being Instruction-Location of S holds IC S in dom (Start-At l)

proof end;

theorem :: SCMNORM:18

for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of NAT ,N
for p being FinPartState of S
for k being Element of NAT holds IC S in dom (IncrIC p,k)

proof end;

theorem Th19: :: SCMNORM:19

for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of NAT ,N
for l being Instruction-Location of S holds IC (Start-At l) = l

proof end;

theorem :: SCMNORM:20

for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of NAT ,N
for p being FinPartState of S
for k being Element of NAT holds (IncrIC p,k) . (IC S) = (IC p) + k

proof end;

theorem Th21: :: SCMNORM:21

for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of NAT ,N holds not IC S in Data-Locations S

proof end;

theorem Th22: :: SCMNORM:22

for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of NAT ,N
for d being data-only FinPartState of S holds not IC S in dom d

proof end;

theorem Th23: :: SCMNORM:23

for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of NAT ,N
for p being FinPartState of S
for d being data-only FinPartState of S st IC S in dom p holds
IC (p +* d) = IC p

proof end;

theorem Th24: :: SCMNORM:24

for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of NAT ,N
for l being Instruction-Location of S
for d being data-only FinPartState of S holds d tolerates Start-At l

proof end;

theorem :: SCMNORM:25

for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of NAT ,N
for p being FinPartState of S
for k being Element of NAT
for d being data-only FinPartState of S st IC S in dom p holds
IncrIC (p +* d),k = (IncrIC p,k) +* d

proof end;

theorem :: SCMNORM:26

for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of NAT ,N
for d being data-only FinPartState of S
for f being finite PartFunc of NAT ,the Instructions of S holds d tolerates f

proof end;

theorem :: SCMNORM:27

for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of NAT ,N
for k being Element of NAT
for d being data-only FinPartState of S holds (IncrIC d,k) | NAT = {}

proof end;