:: Some Remarks on Simple Concrete Model of Computer
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received October 8, 1993
:: Copyright (c) 1993-2011 Association of Mizar Users

begin

definition

func SCM -> strict AMI-Struct of {INT} equals :: AMI_3:def 1
AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),SCM-Instr,(In ([0,{},{}],SCM-Instr)),SCM-OK,SCM-Exec #);
coherence
AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),SCM-Instr,(In ([0,{},{}],SCM-Instr)),SCM-OK,SCM-Exec #) is strict AMI-Struct of {INT} ;

end;

:: deftheorem defines SCM AMI_3:def 1 :
SCM = AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),SCM-Instr,(In ([0,{},{}],SCM-Instr)),SCM-OK,SCM-Exec #);

Lm1: NAT c= SCM-Memory
by XBOOLE_1:7;

registration

cluster SCM -> non empty stored-program standard-ins strict ;
coherence
( not SCM is empty & SCM is stored-program & SCM is standard-ins )

proof end;

end;

registration

cluster Relation-like NAT -defined Function-like -> the carrier of SCM -defined set ;
coherence
for b₁ being Function st b₁ is NAT -defined holds
b₁ is the carrier of SCM -defined

proof end;

end;

theorem :: AMI_3:1

canceled;

theorem :: AMI_3:2

canceled;

[0,{},{}] in SCM-Instr
by AMI_2:2;

then the haltF of SCM = [0,{},{}]
by FUNCT_7:def 1;

then Lm2: halt SCM = [0,{},{}]
;

registration

cluster SCM -> IC-Ins-separated definite proper-halt strict ;
coherence
( SCM is proper-halt & SCM is IC-Ins-separated & SCM is definite )

proof end;

end;

definition

mode Data-Location -> Object of SCM means :Def2: :: AMI_3:def 2
it in SCM-Data-Loc ;
existence
ex b₁ being Object of SCM st b₁ in SCM-Data-Loc

proof end;

end;

:: deftheorem Def2 defines Data-Location AMI_3:def 2 :
for b₁ being Object of SCM holds
( b₁ is Data-Location iff b₁ in SCM-Data-Loc );

definition

let s be State of SCM;
let d be Data-Location ;
:: original: .
redefine func s . d -> Integer;
coherence
s . d is Integer

proof end;

end;

definition

let a, b be Data-Location ;
func a := b -> Instruction of SCM equals :: AMI_3:def 3
[1,{},<*a,b*>];
correctness
coherence
[1,{},<*a,b*>] is Instruction of SCM;

proof end;

func AddTo (a,b) -> Instruction of SCM equals :: AMI_3:def 4
[2,{},<*a,b*>];
correctness
coherence
[2,{},<*a,b*>] is Instruction of SCM;

proof end;

func SubFrom (a,b) -> Instruction of SCM equals :: AMI_3:def 5
[3,{},<*a,b*>];
correctness
coherence
[3,{},<*a,b*>] is Instruction of SCM;

proof end;

func MultBy (a,b) -> Instruction of SCM equals :: AMI_3:def 6
[4,{},<*a,b*>];
correctness
coherence
[4,{},<*a,b*>] is Instruction of SCM;

proof end;

func Divide (a,b) -> Instruction of SCM equals :: AMI_3:def 7
[5,{},<*a,b*>];
correctness
coherence
[5,{},<*a,b*>] is Instruction of SCM;

proof end;

end;

:: deftheorem defines := AMI_3:def 3 :
for a, b being Data-Location holds a := b = [1,{},<*a,b*>];

:: deftheorem defines AddTo AMI_3:def 4 :
for a, b being Data-Location holds AddTo (a,b) = [2,{},<*a,b*>];

:: deftheorem defines SubFrom AMI_3:def 5 :
for a, b being Data-Location holds SubFrom (a,b) = [3,{},<*a,b*>];

:: deftheorem defines MultBy AMI_3:def 6 :
for a, b being Data-Location holds MultBy (a,b) = [4,{},<*a,b*>];

:: deftheorem defines Divide AMI_3:def 7 :
for a, b being Data-Location holds Divide (a,b) = [5,{},<*a,b*>];

definition

let loc be Nat;
func SCM-goto loc -> Instruction of SCM equals :: AMI_3:def 8
[6,<*loc*>,{}];
correctness
coherence
[6,<*loc*>,{}] is Instruction of SCM;

proof end;

let a be Data-Location ;
func a =0_goto loc -> Instruction of SCM equals :: AMI_3:def 9
[7,<*loc*>,<*a*>];
correctness
coherence
[7,<*loc*>,<*a*>] is Instruction of SCM;

proof end;

func a >0_goto loc -> Instruction of SCM equals :: AMI_3:def 10
[8,<*loc*>,<*a*>];
correctness
coherence
[8,<*loc*>,<*a*>] is Instruction of SCM;

proof end;

end;

:: deftheorem defines SCM-goto AMI_3:def 8 :
for loc being Nat holds SCM-goto loc = [6,<*loc*>,{}];

:: deftheorem defines =0_goto AMI_3:def 9 :
for loc being Nat
for a being Data-Location holds a =0_goto loc = [7,<*loc*>,<*a*>];

:: deftheorem defines >0_goto AMI_3:def 10 :
for loc being Nat
for a being Data-Location holds a >0_goto loc = [8,<*loc*>,<*a*>];

theorem :: AMI_3:3

canceled;

theorem Th4: :: AMI_3:4

IC = NAT by AMI_2:30, FUNCT_7:def 1;

begin

theorem :: AMI_3:5

canceled;

theorem :: AMI_3:6

canceled;

theorem :: AMI_3:7

canceled;

theorem Th8: :: AMI_3:8

for a, b being Data-Location
for s being State of SCM holds
( (Exec ((a := b),s)) . (IC ) = succ (IC s) & (Exec ((a := b),s)) . a = s . b & ( for c being Data-Location st c <> a holds
(Exec ((a := b),s)) . c = s . c ) )

proof end;

theorem Th9: :: AMI_3:9

for a, b being Data-Location
for s being State of SCM holds
( (Exec ((AddTo (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((AddTo (a,b)),s)) . a = (s . a) + (s . b) & ( for c being Data-Location st c <> a holds
(Exec ((AddTo (a,b)),s)) . c = s . c ) )

proof end;

theorem Th10: :: AMI_3:10

for a, b being Data-Location
for s being State of SCM holds
( (Exec ((SubFrom (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((SubFrom (a,b)),s)) . a = (s . a) - (s . b) & ( for c being Data-Location st c <> a holds
(Exec ((SubFrom (a,b)),s)) . c = s . c ) )

proof end;

theorem Th11: :: AMI_3:11

for a, b being Data-Location
for s being State of SCM holds
( (Exec ((MultBy (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((MultBy (a,b)),s)) . a = (s . a) * (s . b) & ( for c being Data-Location st c <> a holds
(Exec ((MultBy (a,b)),s)) . c = s . c ) )

proof end;

theorem Th12: :: AMI_3:12

for a, b being Data-Location
for s being State of SCM holds
( (Exec ((Divide (a,b)),s)) . (IC ) = succ (IC s) & ( a <> b implies (Exec ((Divide (a,b)),s)) . a = (s . a) div (s . b) ) & (Exec ((Divide (a,b)),s)) . b = (s . a) mod (s . b) & ( for c being Data-Location st c <> a & c <> b holds
(Exec ((Divide (a,b)),s)) . c = s . c ) )

proof end;

theorem :: AMI_3:13

for c being Data-Location
for loc being Nat
for s being State of SCM holds
( (Exec ((SCM-goto loc),s)) . (IC ) = loc & (Exec ((SCM-goto loc),s)) . c = s . c )

proof end;

theorem Th14: :: AMI_3:14

for a, c being Data-Location
for loc being Nat
for s being State of SCM holds
( ( s . a = 0 implies (Exec ((a =0_goto loc),s)) . (IC ) = loc ) & ( s . a <> 0 implies (Exec ((a =0_goto loc),s)) . (IC ) = succ (IC s) ) & (Exec ((a =0_goto loc),s)) . c = s . c )

proof end;

theorem Th15: :: AMI_3:15

for a, c being Data-Location
for loc being Nat
for s being State of SCM holds
( ( s . a > 0 implies (Exec ((a >0_goto loc),s)) . (IC ) = loc ) & ( s . a <= 0 implies (Exec ((a >0_goto loc),s)) . (IC ) = succ (IC s) ) & (Exec ((a >0_goto loc),s)) . c = s . c )

proof end;

Lm3: for I being Instruction of SCM st ex s being State of SCM st (Exec (I,s)) . (IC ) = succ (IC s) holds
not I is halting

proof end;

Lm4: for I being Instruction of SCM st I = [0,{},{}] holds
I is halting

proof end;

Lm5: for a, b being Data-Location holds not a := b is halting

proof end;

Lm6: for a, b being Data-Location holds not AddTo (a,b) is halting

proof end;

Lm7: for a, b being Data-Location holds not SubFrom (a,b) is halting

proof end;

Lm8: for a, b being Data-Location holds not MultBy (a,b) is halting

proof end;

Lm9: for a, b being Data-Location holds not Divide (a,b) is halting

proof end;

Lm10: for loc being Nat holds not SCM-goto loc is halting

proof end;

Lm11: for a being Data-Location
for loc being Nat holds not a =0_goto loc is halting

proof end;

Lm12: for a being Data-Location
for loc being Nat holds not a >0_goto loc is halting

proof end;

Lm13: for I being set holds
( I is Instruction of SCM iff ( I = [0,{},{}] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo (a,b) or ex a, b being Data-Location st I = SubFrom (a,b) or ex a, b being Data-Location st I = MultBy (a,b) or ex a, b being Data-Location st I = Divide (a,b) or ex loc being Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc ) )

proof end;

Lm14: for W being Instruction of SCM st W is halting holds
W = [0,{},{}]

proof end;

registration

cluster SCM -> strict halting ;
coherence
SCM is halting

proof end;

end;

Lm15: halt SCM = [0,{},{}]
by Lm14;

begin

theorem :: AMI_3:16

canceled;

theorem :: AMI_3:17

canceled;

theorem :: AMI_3:18

canceled;

theorem :: AMI_3:19

canceled;

theorem :: AMI_3:20

canceled;

theorem :: AMI_3:21

canceled;

theorem :: AMI_3:22

canceled;

theorem :: AMI_3:23

canceled;

theorem :: AMI_3:24

canceled;

theorem :: AMI_3:25

canceled;

theorem :: AMI_3:26

canceled;

theorem :: AMI_3:27

canceled;

theorem :: AMI_3:28

canceled;

theorem :: AMI_3:29

canceled;

theorem :: AMI_3:30

canceled;

theorem :: AMI_3:31

canceled;

theorem :: AMI_3:32

canceled;

theorem :: AMI_3:33

canceled;

theorem :: AMI_3:34

canceled;

theorem :: AMI_3:35

canceled;

theorem :: AMI_3:36

canceled;

theorem :: AMI_3:37

canceled;

theorem :: AMI_3:38

canceled;

theorem :: AMI_3:39

canceled;

theorem :: AMI_3:40

canceled;

theorem :: AMI_3:41

canceled;

theorem :: AMI_3:42

canceled;

theorem :: AMI_3:43

canceled;

theorem :: AMI_3:44

canceled;

theorem :: AMI_3:45

canceled;

theorem :: AMI_3:46

canceled;

theorem :: AMI_3:47

canceled;

theorem :: AMI_3:48

canceled;

theorem :: AMI_3:49

canceled;

theorem :: AMI_3:50

canceled;

theorem Th51: :: AMI_3:51

SCM is realistic

proof end;

registration

cluster SCM -> realistic strict ;
coherence
SCM is realistic

proof end;

end;

definition

let k be natural number ;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
func dl. k -> Data-Location equals :: AMI_3:def 19
[1,k];
coherence
[1,k] is Data-Location

proof end;

canceled;

end;

:: deftheorem AMI_3:def 11 :
canceled;

:: deftheorem AMI_3:def 12 :
canceled;

:: deftheorem AMI_3:def 13 :
canceled;

:: deftheorem AMI_3:def 14 :
canceled;

:: deftheorem AMI_3:def 15 :
canceled;

:: deftheorem AMI_3:def 16 :
canceled;

:: deftheorem AMI_3:def 17 :
canceled;

:: deftheorem AMI_3:def 18 :
canceled;

:: deftheorem defines dl. AMI_3:def 19 :
for k being natural number holds dl. k = [1,k];

:: deftheorem AMI_3:def 20 :
canceled;

theorem :: AMI_3:52

for i, j being natural number st i <> j holds
dl. i <> dl. j by ZFMISC_1:33;

theorem :: AMI_3:53

canceled;

theorem :: AMI_3:54

canceled;

theorem Th55: :: AMI_3:55

for l being Data-Location holds ObjectKind l = INT

proof end;

definition

let la be Data-Location ;
let a be Integer;
:: original: .-->
redefine func la .--> a -> FinPartState of SCM;
coherence
la .--> a is FinPartState of SCM

proof end;

end;

definition

let la, lb be Data-Location ;
let a, b be Integer;
:: original: -->
redefine func (la,lb) --> (a,b) -> FinPartState of SCM;
coherence
(la,lb) --> (a,b) is FinPartState of SCM

proof end;

end;

theorem :: AMI_3:56

for i, j being natural number holds dl. i <> j

proof end;

theorem :: AMI_3:57

for i being natural number holds
( IC <> dl. i & IC <> i )

proof end;

begin

theorem :: AMI_3:58

for I being Instruction of SCM st ex s being State of SCM st (Exec (I,s)) . (IC ) = succ (IC s) holds
not I is halting by Lm3;

theorem :: AMI_3:59

for I being Instruction of SCM st I = [0,{},{}] holds
I is halting by Lm4;

theorem :: AMI_3:60

for a, b being Data-Location holds not a := b is halting by Lm5;

theorem :: AMI_3:61

for a, b being Data-Location holds not AddTo (a,b) is halting by Lm6;

theorem :: AMI_3:62

for a, b being Data-Location holds not SubFrom (a,b) is halting by Lm7;

theorem :: AMI_3:63

for a, b being Data-Location holds not MultBy (a,b) is halting by Lm8;

theorem :: AMI_3:64

for a, b being Data-Location holds not Divide (a,b) is halting by Lm9;

theorem :: AMI_3:65

for loc being Nat holds not SCM-goto loc is halting by Lm10;

theorem :: AMI_3:66

for a being Data-Location
for loc being Nat holds not a =0_goto loc is halting by Lm11;

theorem :: AMI_3:67

for a being Data-Location
for loc being Nat holds not a >0_goto loc is halting by Lm12;

theorem :: AMI_3:68

canceled;

theorem :: AMI_3:69

for I being set holds
( I is Instruction of SCM iff ( I = [0,{},{}] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo (a,b) or ex a, b being Data-Location st I = SubFrom (a,b) or ex a, b being Data-Location st I = MultBy (a,b) or ex a, b being Data-Location st I = Divide (a,b) or ex loc being Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc ) ) by Lm13;

theorem :: AMI_3:70

for I being Instruction of SCM st I is halting holds
I = halt SCM by Lm14, Lm15;

theorem :: AMI_3:71

halt SCM = [0,{},{}] by Lm14;

theorem Th72: :: AMI_3:72

Data-Locations SCM = SCM-Data-Loc

proof end;

theorem :: AMI_3:73

for d being Data-Location holds d in Data-Locations SCM

proof end;