:: 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
definition
func SCM -> strict AMI-Struct of
NAT ,
{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 NAT ,{INT }
;
end;
:: deftheorem defines SCM AMI_3:def 1 :
theorem :: AMI_3:1
canceled;
theorem Th2: :: AMI_3:2
:: deftheorem Def2 defines Data-Location AMI_3:def 2 :
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 ;
func AddTo a,
b -> Instruction of
SCM equals :: AMI_3:def 4
[2,<*a,b*>];
correctness
coherence
[2,<*a,b*>] is Instruction of SCM ;
func SubFrom a,
b -> Instruction of
SCM equals :: AMI_3:def 5
[3,<*a,b*>];
correctness
coherence
[3,<*a,b*>] is Instruction of SCM ;
func MultBy a,
b -> Instruction of
SCM equals :: AMI_3:def 6
[4,<*a,b*>];
correctness
coherence
[4,<*a,b*>] is Instruction of SCM ;
func Divide a,
b -> Instruction of
SCM equals :: AMI_3:def 7
[5,<*a,b*>];
correctness
coherence
[5,<*a,b*>] is Instruction of SCM ;
end;
:: deftheorem defines := AMI_3:def 3 :
:: deftheorem defines AddTo AMI_3:def 4 :
:: deftheorem defines SubFrom AMI_3:def 5 :
:: deftheorem defines MultBy AMI_3:def 6 :
:: deftheorem defines Divide AMI_3:def 7 :
definition
let loc be
Instruction-Location of
SCM ;
func goto loc -> Instruction of
SCM equals :: AMI_3:def 8
[6,<*loc*>];
correctness
coherence
[6,<*loc*>] is Instruction of SCM ;
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 ;
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 ;
end;
:: deftheorem defines goto AMI_3:def 8 :
:: deftheorem defines =0_goto AMI_3:def 9 :
:: deftheorem defines >0_goto AMI_3:def 10 :
theorem :: AMI_3:3
canceled;
theorem Th4: :: AMI_3:4
theorem :: AMI_3:5
canceled;
theorem :: AMI_3:6
canceled;
theorem :: AMI_3:7
canceled;
theorem Th8: :: AMI_3:8
theorem Th9: :: AMI_3:9
theorem Th10: :: AMI_3:10
theorem Th11: :: AMI_3:11
theorem Th12: :: AMI_3:12
theorem :: AMI_3:13
theorem Th14: :: AMI_3:14
theorem Th15: :: AMI_3:15
Lm1:
for I being Instruction of SCM st ex s being State of SCM st (Exec I,s) . (IC SCM ) = Next holds
not I is halting
Lm2:
for I being Instruction of SCM st I = [0 ,{} ] holds
I is halting
Lm3:
for a, b being Data-Location holds not a := b is halting
Lm4:
for a, b being Data-Location holds not AddTo a,b is halting
Lm5:
for a, b being Data-Location holds not SubFrom a,b is halting
Lm6:
for a, b being Data-Location holds not MultBy a,b is halting
Lm7:
for a, b being Data-Location holds not Divide a,b is halting
Lm8:
for loc being Instruction-Location of SCM holds not goto loc is halting
Lm9:
for a being Data-Location
for loc being Instruction-Location of SCM holds not a =0_goto loc is halting
Lm10:
for a being Data-Location
for loc being Instruction-Location of SCM holds not a >0_goto loc is halting
Lm11:
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 Instruction-Location of SCM st I = goto loc or ex a being Data-Location ex loc being Instruction-Location of SCM st I = a =0_goto loc or ex a being Data-Location ex loc being Instruction-Location of SCM st I = a >0_goto loc ) )
Lm12:
for W being Instruction of SCM st W is halting holds
W = [0 ,{} ]
Lm13:
halt SCM = [0 ,{} ]
by Lm12;
Lm14:
for s being State of SCM
for i being Instruction of SCM
for l being Instruction-Location of SCM holds (Exec i,s) . l = s . l
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
:: 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 :
:: deftheorem defines il. AMI_3:def 20 :
theorem :: AMI_3:52
theorem :: AMI_3:53
canceled;
theorem :: AMI_3:54
canceled;
theorem Th55: :: AMI_3:55
theorem :: AMI_3:56
theorem :: AMI_3:57
theorem :: AMI_3:58
theorem :: AMI_3:59
theorem :: AMI_3:60
theorem :: AMI_3:61
theorem :: AMI_3:62
theorem :: AMI_3:63
theorem :: AMI_3:64
theorem :: AMI_3:65
theorem :: AMI_3:66
theorem :: AMI_3:67
theorem :: AMI_3:68
canceled;
theorem :: AMI_3:69
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
Instruction-Location of
SCM st
I = goto loc or ex
a being
Data-Location ex
loc being
Instruction-Location of
SCM st
I = a =0_goto loc or ex
a being
Data-Location ex
loc being
Instruction-Location of
SCM st
I = a >0_goto loc ) )
by Lm11;
theorem :: AMI_3:70
theorem :: AMI_3:71
theorem :: AMI_3:72