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

registration

let n be non zero Nat;

cluster Segm n -> with_zero ;

coherence
Segm n is with_zero ;

end;

definition

func SCM -> strict AMI-Struct over Segm 2 equals :: AMI_3:def 1
AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),SCM-Instr,SCM-OK,SCM-VAL,SCM-Exec #);

coherence
AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),SCM-Instr,SCM-OK,SCM-VAL,SCM-Exec #) is strict AMI-Struct over Segm 2 ;

end;

:: deftheorem defines SCM AMI_3:def 1 :
SCM = AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),SCM-Instr,SCM-OK,SCM-VAL,SCM-Exec #);

registration

cluster SCM -> non empty strict ;

coherence
not SCM is empty ;

end;

Lm1: the_Values_of SCM = the ValuesF of SCM * the Object-Kind of SCM
.= SCM-VAL * SCM-OK ;

registration

cluster SCM -> with_non-empty_values strict ;

coherence
SCM is with_non-empty_values ;

end;

registration

cluster SCM -> IC-Ins-separated strict ;

coherence
SCM is IC-Ins-separated by AMI_2:22, SUBSET_1:def 8, AMI_2:6;

end;

registration

cluster Int-like for Element of the carrier of SCM;

existence
ex b₁ being Object of SCM st b₁ is Int-like

proof end;

end;

definition

mode Data-Location is Int-like Object of SCM;

end;

registration

let s be State of SCM;
let d be Data-Location;

cluster 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 AMI_3:def 2 :
canceled;

:: 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;
by SCM_INST:2;
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 Th1: :: AMI_3:1

IC = NAT by AMI_2:22, SUBSET_1:def 8;

theorem Th2: :: AMI_3:2

for a, b being Data-Location
for s being State of SCM holds
( (Exec ((a := b),s)) . (IC ) = (IC s) + 1 & (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 Th3: :: AMI_3:3

for a, b being Data-Location
for s being State of SCM holds
( (Exec ((AddTo (a,b)),s)) . (IC ) = (IC s) + 1 & (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 Th4: :: AMI_3:4

for a, b being Data-Location
for s being State of SCM holds
( (Exec ((SubFrom (a,b)),s)) . (IC ) = (IC s) + 1 & (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 Th5: :: AMI_3:5

for a, b being Data-Location
for s being State of SCM holds
( (Exec ((MultBy (a,b)),s)) . (IC ) = (IC s) + 1 & (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 Th6: :: AMI_3:6

for a, b being Data-Location
for s being State of SCM holds
( (Exec ((Divide (a,b)),s)) . (IC ) = (IC s) + 1 & ( 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:7

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 Th8: :: AMI_3:8

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 ) = (IC s) + 1 ) & (Exec ((a =0_goto loc),s)) . c = s . c )

proof end;

theorem Th9: :: AMI_3:9

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 ) = (IC s) + 1 ) & (Exec ((a >0_goto loc),s)) . c = s . c )

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

Lm9: for loc being Nat holds not SCM-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 a being Data-Location
for loc being Nat holds not a >0_goto loc is halting

proof end;

Lm12: 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;

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

proof end;

registration

cluster SCM -> strict halting ;

coherence
SCM is halting by Lm3;

end;

definition

let k be Nat;

func dl. k -> Data-Location equals :: AMI_3:def 11
[1,k];

coherence
[1,k] is Data-Location

proof end;

end;

:: deftheorem defines dl. AMI_3:def 11 :
for k being Nat holds dl. k = [1,k];

theorem :: AMI_3:10

for i, j being Nat st i <> j holds
dl. i <> dl. j by XTUPLE_0:1;

theorem Th11: :: AMI_3:11

for l being Data-Location holds Values l = INT by AMI_2:def 16, AMI_2:7;

definition

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

proof end;

end;

definition

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

proof end;

end;

theorem :: AMI_3:12

for i, j being Nat holds dl. i <> j ;

theorem :: AMI_3:13

for i being Nat holds
( IC <> dl. i & IC <> i ) by Th1;

theorem :: AMI_3:14

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

theorem :: AMI_3:15

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

theorem :: AMI_3:16

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

theorem :: AMI_3:17

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

theorem :: AMI_3:18

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

theorem :: AMI_3:19

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

theorem :: AMI_3:20

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

theorem :: AMI_3:21

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

theorem :: AMI_3:22

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

theorem :: AMI_3:23

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

theorem :: AMI_3:24

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

theorem :: AMI_3:25

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

theorem :: AMI_3:26

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

theorem Th27: :: AMI_3:27

Data-Locations = SCM-Data-Loc

proof end;

theorem :: AMI_3:28

for d being Data-Location holds d in Data-Locations by Th27, AMI_2:def 16;

theorem :: AMI_3:29

for s being SCM-State holds s is State of SCM by Lm1;

theorem :: AMI_3:30

for l being Element of SCM-Instr holds InsCode l <= 8 by SCM_INST:10;