:: 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 #);

registration

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

proof end;

end;

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

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

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

registration

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

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 Th4: :: AMI_3:1

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

begin

theorem Th8: :: AMI_3:2

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:3

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:4

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:5

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:6

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

proof end;

theorem Th15: :: 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 ) = 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

definition

let k be natural number ;
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 natural number holds dl. k = [1,k];

theorem :: AMI_3:10

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

theorem Th55: :: AMI_3:11

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 -> 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 natural number holds dl. i <> j

proof end;

theorem :: AMI_3:13

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

proof end;

begin

theorem :: AMI_3:14

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:15

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

theorem :: AMI_3:16

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

theorem :: AMI_3:17

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

theorem :: AMI_3:18

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

theorem :: AMI_3:19

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

theorem :: AMI_3:20

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

theorem :: AMI_3:21

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

theorem :: AMI_3:22

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

theorem :: AMI_3:23

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

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

theorem :: AMI_3:25

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

theorem :: AMI_3:26

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

theorem Th72: :: 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 Def2, Th72;

theorem Th74: :: AMI_3:29

for a being Data-Location holds not a in NAT

proof end;

theorem :: AMI_3:30

for a being Data-Location
for f being NAT -defined Function holds not a in dom f

proof end;