:: Some Remarks on Simple Concrete Model of Computer
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received October 8, 1993
:: Copyright (c) 1993 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 ,SCM-OK ,SCM-Exec #);
coherence
AMI-Struct(# SCM-Memory ,(In NAT ,SCM-Memory ),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 ,SCM-OK ,SCM-Exec #);

registration

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

proof end;

end;

theorem :: AMI_3:1

canceled;

theorem Th2: :: AMI_3:2

SCM is definite

proof end;

registration

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

proof end;

end;

definition

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

proof end;

end;

:: deftheorem Def2 defines Data-Location AMI_3:def 2 :

for b₁ being Object of holds
( b₁ is Data-Location iff b₁ in SCM-Data-Loc );

definition

let s be State of ;
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 equals :: AMI_3:def 3
[1,<*a,b*>];
correctness
coherence
[1,<*a,b*>] is Instruction of ;

proof end;

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

proof end;

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

proof end;

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

proof end;

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

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 goto loc -> Instruction of equals :: AMI_3:def 8
[6,<*loc*>];
correctness
coherence
[6,<*loc*>] is Instruction of ;

proof end;

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

proof end;

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

proof end;

end;

:: deftheorem defines goto AMI_3:def 8 :

for loc being Nat holds 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 SCM = 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 holds
( (Exec (a := b),s) . (IC SCM ) = Next & (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 holds
( (Exec (AddTo a,b),s) . (IC SCM ) = Next & (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 holds
( (Exec (SubFrom a,b),s) . (IC SCM ) = Next & (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 holds
( (Exec (MultBy a,b),s) . (IC SCM ) = Next & (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 holds
( (Exec (Divide a,b),s) . (IC SCM ) = Next & ( 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 holds
( (Exec (goto loc),s) . (IC SCM ) = loc & (Exec (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 holds
( ( s . a = 0 implies (Exec (a =0_goto loc),s) . (IC SCM ) = loc ) & ( s . a <> 0 implies (Exec (a =0_goto loc),s) . (IC SCM ) = Next ) & (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 holds
( ( s . a > 0 implies (Exec (a >0_goto loc),s) . (IC SCM ) = loc ) & ( s . a <= 0 implies (Exec (a >0_goto loc),s) . (IC SCM ) = Next ) & (Exec (a >0_goto loc),s) . c = s . c )

proof end;

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

proof end;

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

proof end;

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

proof end;

Lm4: for a, b being Data-Location holds not AddTo a,b is halting

proof end;

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

proof end;

Lm6: for a, b being Data-Location holds not MultBy a,b is halting

proof end;

Lm7: for a, b being Data-Location holds not Divide a,b is halting

proof end;

Lm8: for loc being Nat holds not goto loc is halting

proof end;

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

proof end;

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

proof end;

Lm11: for I being set holds
( I is Instruction of 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 = 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;

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

proof end;

registration

cluster SCM -> strict halting ;
coherence
SCM is halting

proof end;

end;

Lm13: halt SCM = [0 ,{} ]
by Lm12;

begin

Lm14: for s being State of
for i being Instruction of
for l being Instruction-Location of SCM holds (Exec i,s) . l = s . l

proof end;

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 -> strict steady-programmed realistic ;
coherence
( SCM is steady-programmed & 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;

func il. k -> Instruction-Location of SCM equals :: AMI_3:def 20
k;
coherence
k is Instruction-Location of SCM

proof end;

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 defines il. AMI_3:def 20 :

for k being natural number holds il. k = k;

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 ;
coherence
la .--> a is FinPartState of

proof end;

end;

definition

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

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 SCM <> dl. i & IC SCM <> i )

proof end;

begin

theorem :: AMI_3:58

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

theorem :: AMI_3:59

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

theorem :: AMI_3:60

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

theorem :: AMI_3:61

for a, b being Data-Location holds not AddTo a,b is halting by Lm4;

theorem :: AMI_3:62

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

theorem :: AMI_3:63

for a, b being Data-Location holds not MultBy a,b is halting by Lm6;

theorem :: AMI_3:64

for a, b being Data-Location holds not Divide a,b is halting by Lm7;

theorem :: AMI_3:65

for loc being Nat holds not goto loc is halting by Lm8;

theorem :: AMI_3:66

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

theorem :: AMI_3:67

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

theorem :: AMI_3:68

canceled;

theorem :: AMI_3:69

for I being set holds
( I is Instruction of 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 = 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 Lm11;

theorem :: AMI_3:70

for I being Instruction of st I is halting holds
I = halt SCM by Lm12, Lm13;

theorem :: AMI_3:71

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

theorem :: AMI_3:72

Data-Locations SCM = SCM-Data-Loc

proof end;