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

registration
let n be non zero Nat;
coherence ;
end;

definition
func SCM -> strict AMI-Struct over Segm 2 equals :: AMI_3:def 1
AMI-Struct(# SCM-Memory,(),SCM-Instr,SCM-OK,SCM-VAL,SCM-Exec #);
coherence
AMI-Struct(# 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 :

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
coherence ;
end;

registration
coherence by ;
end;

registration
cluster Int-like for Element of the carrier of SCM;
existence
ex b1 being Object of SCM st b1 is Int-like
proof end;
end;

definition 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

theorem Th2: :: AMI_3:2
for a, b being Data-Location
for s being State of SCM holds
( (Exec ((a := b),s)) . () = (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 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 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 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 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)) . () = 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)) . () = loc ) & ( s . a <> 0 implies (Exec ((a =0_goto loc),s)) . () = (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)) . () = loc ) & ( s . a <= 0 implies (Exec ((a >0_goto loc),s)) . () = (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 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
coherence 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 ;

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

theorem Th27: :: AMI_3:27
proof end;

theorem :: AMI_3:28
for d being Data-Location holds d in Data-Locations by ;

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;