Journal of Formalized Mathematics
Volume 10, 1998
University of Bialystok
Copyright (c) 1998 Association of Mizar Users

The Basic Properties of \SCM over Ring

by
Artur Kornilowicz

Received November 29, 1998

MML identifier: SCMRING2
[ Mizar article, MML identifier index ]

environ

vocabulary GR_CY_1, SCMFSA7B, FUNCSDOM, AMI_3, AMI_1, AMI_2, FUNCT_1, CAT_1,
BOOLE, FINSEQ_1, FUNCT_2, CARD_3, ARYTM_1, RLVECT_1, CQC_LANG, SCMRING1,
MCART_1, FUNCT_4, RELAT_1;
notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
GR_CY_1, STRUCT_0, RLVECT_1, VECTSP_1, FUNCSDOM, MCART_1, NUMBERS,
XREAL_0, CARD_3, NAT_1, FINSEQ_1, CQC_LANG, FUNCT_4, AMI_1, AMI_2, AMI_3,
SCMRING1;
constructors AMI_3, CAT_2, DOMAIN_1, FINSEQ_4, NAT_1, REALSET1, SCMRING1,
MEMBERED;
clusters AMI_1, CQC_LANG, SCMRING1, STRUCT_0, RELSET_1, AMI_5, AMI_3,
FINSEQ_5, XBOOLE_0, FRAENKEL, NAT_1, MEMBERED, NUMBERS, ORDINAL2;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;

begin  :: { \bf SCM } over ring

reserve i for Nat,
I for Element of Segm 8,
S for non empty 1-sorted,
t for Element of S,
x for set;

definition let R be good Ring;
func SCM R -> strict AMI-Struct over { the carrier of R } means
:: SCMRING2:def 1
the carrier of it = NAT &
the Instruction-Counter of it = 0 &
the Instruction-Locations of it = SCM-Instr-Loc &
the Instruction-Codes of it = Segm 8 &
the Instructions of it = SCM-Instr R &
the Object-Kind of it = SCM-OK R &
the Execution of it = SCM-Exec R;
end;

definition let R be good Ring;
cluster SCM R -> non empty non void;
end;

definition let R be good Ring,
s be State of SCM R,
a be Element of SCM-Data-Loc;
redefine func s.a -> Element of R;
end;

definition let R be good Ring;
mode Data-Location of R -> Object of SCM R means
:: SCMRING2:def 2
it in (the carrier of SCM R) \ (SCM-Instr-Loc \/ {0});
end;

reserve R for good Ring,
r for Element of R,
a, b, c, d1, d2 for Data-Location of R,
i1 for Instruction-Location of SCM R;

theorem :: SCMRING2:1
x is Data-Location of R iff x in SCM-Data-Loc;

definition let R be good Ring,
s be State of SCM R,
a be Data-Location of R;
redefine func s.a -> Element of R;
end;

theorem :: SCMRING2:2
[0,{}] in SCM-Instr S;

theorem :: SCMRING2:3
[0,{}] is Instruction of SCM R;

theorem :: SCMRING2:4
x in {1,2,3,4} implies [x,<*d1,d2*>] in SCM-Instr S;

theorem :: SCMRING2:5
[5,<*d1,t*>] in SCM-Instr S;

theorem :: SCMRING2:6
[6,<*i1*>] in SCM-Instr S;

theorem :: SCMRING2:7
[7,<*i1,d1*>] in SCM-Instr S;

definition let R be good Ring, a, b be Data-Location of R;
func a := b -> Instruction of SCM R equals
:: SCMRING2:def 3
[ 1, <*a, b*>];
func AddTo(a,b) -> Instruction of SCM R equals
:: SCMRING2:def 4
[ 2, <*a, b*>];
func SubFrom(a,b) -> Instruction of SCM R equals
:: SCMRING2:def 5
[ 3, <*a, b*>];
func MultBy(a,b) -> Instruction of SCM R equals
:: SCMRING2:def 6
[ 4, <*a, b*>];
end;

definition let R be good Ring, a be Data-Location of R,
r be Element of R;
func a := r -> Instruction of SCM R equals
:: SCMRING2:def 7
[ 5, <*a,r*>];
end;

definition let R be good Ring, l be Instruction-Location of SCM R;
func goto l -> Instruction of SCM R equals
:: SCMRING2:def 8
[ 6, <*l*>];
end;

definition let R be good Ring, l be Instruction-Location of SCM R,
a be Data-Location of R;
func a=0_goto l -> Instruction of SCM R equals
:: SCMRING2:def 9
[ 7, <*l,a*>];
end;

theorem :: SCMRING2:8
for I being set holds I is Instruction of SCM R iff
I = [0,{}] or
(ex a,b st I = a:=b) or
(ex a,b st I = AddTo(a,b)) or
(ex a,b st I = SubFrom(a,b)) or
(ex a,b st I = MultBy(a,b)) or
(ex i1 st I = goto i1) or
(ex a,i1 st I = a=0_goto i1) or
ex a,r st I = a:=r;

reserve s for State of SCM R;

definition let R;
cluster SCM R -> IC-Ins-separated;
end;

theorem :: SCMRING2:9
IC SCM R = 0;

theorem :: SCMRING2:10
for S being SCM-State of R st S = s holds IC s = IC S;

definition let R be good Ring, i1 be Instruction-Location of SCM R;
func Next i1 -> Instruction-Location of SCM R means
:: SCMRING2:def 10
ex mj being Element of SCM-Instr-Loc st mj = i1 & it = Next mj;
end;

theorem :: SCMRING2:11
for i1 being Instruction-Location of SCM R,
mj being Element of SCM-Instr-Loc st mj = i1
holds Next mj = Next i1;

theorem :: SCMRING2:12
for I being Instruction of SCM R
for i being Element of SCM-Instr R st i = I
for S being SCM-State of R st S = s holds
Exec(I,s) = SCM-Exec-Res(i,S);

begin :: Users guide

theorem :: SCMRING2:13
Exec(a := b, s).IC SCM R = Next IC s &
Exec(a := b, s).a = s.b &
for c st c <> a holds Exec(a := b, s).c = s.c;

theorem :: SCMRING2:14
Exec(AddTo(a,b), s).IC SCM R = Next IC s &
Exec(AddTo(a,b), s).a = s.a + s.b &
for c st c <> a holds Exec(AddTo(a,b), s).c = s.c;

theorem :: SCMRING2:15
Exec(SubFrom(a,b), s).IC SCM R = Next IC s &
Exec(SubFrom(a,b), s).a = s.a - s.b &
for c st c <> a holds Exec(SubFrom(a,b), s).c = s.c;

theorem :: SCMRING2:16
Exec(MultBy(a,b), s).IC SCM R = Next IC s &
Exec(MultBy(a,b), s).a = s.a * s.b &
for c st c <> a holds Exec(MultBy(a,b), s).c = s.c;

theorem :: SCMRING2:17
Exec(goto i1, s).IC SCM R = i1 &
Exec(goto i1, s).c = s.c;

theorem :: SCMRING2:18
(s.a = 0.R implies Exec(a =0_goto i1, s).IC SCM R = i1) &
(s.a <> 0.R implies Exec(a =0_goto i1, s).IC SCM R = Next IC s) &
Exec(a =0_goto i1, s).c = s.c;

theorem :: SCMRING2:19
Exec(a := r, s).IC SCM R = Next IC s &
Exec(a := r, s).a = r &
for c st c <> a holds Exec(a := r, s).c = s.c;

begin  :: Halt instruction

theorem :: SCMRING2:20
for I being Instruction of SCM R st
ex s st Exec(I,s).IC SCM R = Next IC s
holds I is non halting;

theorem :: SCMRING2:21
for I being Instruction of SCM R st I = [0,{}] holds I is halting;

definition let R, a, b;
cluster a:=b -> non halting;
cluster AddTo(a,b) -> non halting;
cluster SubFrom(a,b) -> non halting;
cluster MultBy(a,b) -> non halting;
end;

definition let R, i1;
cluster goto i1 -> non halting;
end;

definition let R, a, i1;
cluster a =0_goto i1 -> non halting;
end;

definition let R, a, r;
cluster a:=r -> non halting;
end;

definition let R;
cluster SCM R -> halting definite data-oriented steady-programmed
realistic;
end;

canceled 7;

theorem :: SCMRING2:29
for I being Instruction of SCM R st I is halting holds I = halt SCM R;

theorem :: SCMRING2:30
halt SCM R = [0,{}];



Back to top