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


begin

registration
cluster non zero natural  ->  non zero with_zero for set ;
coherence
 for b1 being non zero Nat holds b1 is with_zero
proofend;
end;

definition
func SCM  ->  strict AMI-Struct over 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 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 by STRUCT_0:def_1;
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
proofend;
end;

registration
cluster SCM  ->  IC-Ins-separated strict ;
coherence
 SCM is IC-Ins-separated
proofend;
end;

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

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

registration
let s be State of SCM;
let d be Data-Location;
clusters . d ->  integer ;
coherence
 s . d is integer
proofend;
end;

definition
canceled;
let a, b be Data-Location;
funca := b ->  Instruction of SCM equals :: AMI_3:def 3
[1,{},<*a,b*>];
correctness
coherence
[1,{},<*a,b*>] is Instruction of SCM;
proofend;
func AddTo (a,b) ->  Instruction of SCM equals :: AMI_3:def 4
[2,{},<*a,b*>];
correctness
coherence
[2,{},<*a,b*>] is Instruction of SCM;
proofend;
func SubFrom (a,b) ->  Instruction of SCM equals :: AMI_3:def 5
[3,{},<*a,b*>];
correctness
coherence
[3,{},<*a,b*>] is Instruction of SCM;
proofend;
func MultBy (a,b) ->  Instruction of SCM equals :: AMI_3:def 6
[4,{},<*a,b*>];
correctness
coherence
[4,{},<*a,b*>] is Instruction of SCM;
proofend;
func Divide (a,b) ->  Instruction of SCM equals :: AMI_3:def 7
[5,{},<*a,b*>];
correctness
coherence
[5,{},<*a,b*>] is Instruction of SCM;
proofend;
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;
proofend;
let a be Data-Location;
funca =0_goto loc ->  Instruction of SCM equals :: AMI_3:def 9
[7,<*loc*>,<*a*>];
correctness
coherence
[7,<*loc*>,<*a*>] is Instruction of SCM;
proofend;
funca >0_goto loc ->  Instruction of SCM equals :: AMI_3:def 10
[8,<*loc*>,<*a*>];
correctness
coherence
[8,<*loc*>,<*a*>] is Instruction of SCM;
proofend;
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, FUNCT_7:def_1;

begin

theorem Th2: :: AMI_3:2
for a, b being Data-Location
for s being State of SCM holds
( (Exec ((a := b),s)) . (IC ) = succ (IC s) &amp; (Exec ((a := b),s)) . a = s . b &amp; ( for c being Data-Location st c <> a holds
(Exec ((a := b),s)) . c = s . c ) )
proofend;

theorem Th3: :: 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) &amp; (Exec ((AddTo (a,b)),s)) . a = (s . a) + (s . b) &amp; ( for c being Data-Location st c <> a holds
(Exec ((AddTo (a,b)),s)) . c = s . c ) )
proofend;

theorem Th4: :: 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) &amp; (Exec ((SubFrom (a,b)),s)) . a = (s . a) - (s . b) &amp; ( for c being Data-Location st c <> a holds
(Exec ((SubFrom (a,b)),s)) . c = s . c ) )
proofend;

theorem Th5: :: 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) &amp; (Exec ((MultBy (a,b)),s)) . a = (s . a) * (s . b) &amp; ( for c being Data-Location st c <> a holds
(Exec ((MultBy (a,b)),s)) . c = s . c ) )
proofend;

theorem Th6: :: 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) &amp; ( a <> b implies (Exec ((Divide (a,b)),s)) . a = (s . a) div (s . b) ) &amp; (Exec ((Divide (a,b)),s)) . b = (s . a) mod (s . b) &amp; ( for c being Data-Location st c <> a &amp; c <> b holds
(Exec ((Divide (a,b)),s)) . c = s . c ) )
proofend;

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 &amp; (Exec ((SCM-goto loc),s)) . c = s . c )
proofend;

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 ) &amp; ( s . a <> 0 implies (Exec ((a =0_goto loc),s)) . (IC ) = succ (IC s) ) &amp; (Exec ((a =0_goto loc),s)) . c = s . c )
proofend;

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 ) &amp; ( s . a <= 0 implies (Exec ((a >0_goto loc),s)) . (IC ) = succ (IC s) ) &amp; (Exec ((a >0_goto loc),s)) . c = s . c )
proofend;

Lm2:  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
proofend;

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

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

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

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

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

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

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

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

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

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 ) )
proofend;

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

registration
cluster SCM  ->  strict halting ;
coherence
 SCM is halting
proofend;
end;

begin

definition
let k be Nat;
func dl. k ->  Data-Location equals :: AMI_3:def 11
[1,k];
coherence
 [1,k] is Data-Location
proofend;
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
proofend;

definition
let la be Data-Location;
let a be Integer;
:: original:.-->
redefine funcla .--> a ->  PartState of SCM;
coherence
 la .--> a is PartState of SCM
proofend;
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
proofend;
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 &amp; IC <> i )
proofend;

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

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;