:: The Construction of { \bf SCM } over Ring
:: by Artur Korni{\l}owicz
::
:: Received November 29, 1998
:: Copyright (c) 1998-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, CARD_1, AMI_2, XBOOLE_0, STRUCT_0, ZFMISC_1,
ARYTM_3, SUPINF_2, RELAT_1, FINSEQ_1, FUNCSDOM, FUNCT_1, CARD_3, AMI_1,
FUNCT_4, FUNCOP_1, ARYTM_1, FUNCT_5, TARSKI, SCMRING1, GROUP_9, AFINSQ_1,
PBOOLE, ORDINAL1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, FUNCT_1,
FUNCT_2, BINOP_1, PBOOLE, AFINSQ_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0,
STRUCT_0, ALGSTR_0, VECTSP_1, MCART_1, CARD_3, FINSEQ_1, FUNCOP_1,
FUNCT_4, FUNCT_5, AMI_2, SCMRINGI;
constructors REALSET2, FUNCT_5, RELSET_1, AMI_2, FUNCOP_1, COMPOS_1, SCMRINGI,
BINOP_1, FUNCT_4, XTUPLE_0, XCMPLX_0;
registrations XBOOLE_0, ORDINAL1, FUNCOP_1, FINSEQ_1, CARD_3, STRUCT_0, AMI_2,
CARD_1, ORDINAL2, FUNCT_1, FUNCT_2, RELSET_1, AFINSQ_1, SCM_INST,
XCMPLX_0, NAT_1;
requirements NUMERALS, SUBSET, BOOLE;
definitions TARSKI, FINSEQ_1, FUNCT_1;
equalities FUNCOP_1, ORDINAL1;
theorems AMI_2, CARD_3, FUNCOP_1, FINSEQ_1, FUNCT_1, FUNCT_2, FUNCT_4, TARSKI,
ZFMISC_1, XBOOLE_0, ORDINAL1, RELAT_1, PARTFUN1, AFINSQ_1, FUNCT_5,
XTUPLE_0;
schemes BINOP_1;
begin :: The construction of { \bf SCM } over ring
reserve i, j, k for Element of NAT,
I for Element of Segm 8,
i1, i2 for Element of NAT,
d1, d2, d3, d4 for Element of SCM-Data-Loc,
S for non empty 1-sorted;
reserve G for non empty 1-sorted;
definition
::$CD 2
let S be non empty 1-sorted;
func SCM-VAL S -> ManySortedSet of Segm 2 equals
<%NAT,the carrier of S%>;
coherence;
end;
Lm1:
dom((SCM-VAL S)*SCM-OK) = SCM-Memory
proof
A1: dom SCM-OK = SCM-Memory by PARTFUN1:def 2;
len <%NAT,the carrier of S %> = 2 by AFINSQ_1:38;
then rng SCM-OK c= dom(SCM-VAL S) by RELAT_1:def 19;
hence dom((SCM-VAL S)*SCM-OK) = SCM-Memory by A1,RELAT_1:27;
end;
::$CT
theorem Th1:
((SCM-VAL G)*SCM-OK).NAT = NAT
proof
A1: NAT in SCM-Memory by AMI_2:22;
then NAT in dom SCM-OK by PARTFUN1:def 2;
then
A2: ((SCM-VAL G)*SCM-OK).NAT = (SCM-VAL G).(SCM-OK.NAT) by FUNCT_1:13;
((SCM-VAL G)*SCM-OK).NAT = (SCM-VAL G).0 by A2,A1,AMI_2:def 4;
hence thesis;
end;
theorem Th2:
for i being Element of SCM-Memory st i in SCM-Data-Loc
holds ((SCM-VAL G)*SCM-OK).i = the carrier of G
proof
let i be Element of SCM-Memory;
i in SCM-Memory;
then i in dom SCM-OK by PARTFUN1:def 2;
then
A1: ((SCM-VAL G)*SCM-OK).i = (SCM-VAL G).(SCM-OK.i) by FUNCT_1:13;
assume i in SCM-Data-Loc;
then ((SCM-VAL G)*SCM-OK).i = (SCM-VAL G).1 by A1,AMI_2:def 4;
hence thesis;
end;
registration let G;
cluster ((SCM-VAL G)*SCM-OK) -> non-empty;
coherence
proof set F = ((SCM-VAL G)*SCM-OK);
let n be object;
assume
A1: n in dom F;
dom F = SCM-Memory by Lm1;
then per cases by A1,AMI_2:26;
suppose
A2: n = NAT;
((SCM-VAL G)*SCM-OK).n = NAT by A2,Th1;
hence F.n is non empty;
end;
suppose n in SCM-Data-Loc;
then ((SCM-VAL G)*SCM-OK).n = the carrier of G by Th2;
hence F.n is non empty;
end;
end;
end;
definition
let S be non empty 1-sorted;
mode SCM-State of S is Element of product((SCM-VAL S)*SCM-OK);
end;
theorem
((SCM-VAL G)*SCM-OK).d1 = the carrier of G by Th2;
theorem Th4:
pi(product((SCM-VAL G)*SCM-OK),NAT) = NAT
proof
NAT in dom((SCM-VAL G)*SCM-OK) by Lm1,AMI_2:22;
hence pi(product((SCM-VAL G)*SCM-OK),NAT)
= ((SCM-VAL G)*SCM-OK).NAT by CARD_3:12
.= NAT by Th1;
end;
theorem Th5:
for a being Element of SCM-Data-Loc
holds pi(product((SCM-VAL G)*SCM-OK),a) = the carrier of G
proof
let a be Element of SCM-Data-Loc;
a in SCM-Memory;
then a in dom((SCM-VAL G)*SCM-OK) by Lm1;
hence pi(product((SCM-VAL G)*SCM-OK),a)
= ((SCM-VAL G)*SCM-OK).a by CARD_3:12
.= the carrier of G by Th2;
end;
definition
let G; let s be SCM-State of G;
func IC s -> Element of NAT equals
s.NAT;
coherence
proof
s.NAT in pi(product((SCM-VAL G)*SCM-OK),NAT) by CARD_3:def 6;
hence thesis by Th4;
end;
end;
definition
let R be non empty 1-sorted, s be SCM-State of R, u be natural Number;
func SCM-Chg(s,u) -> SCM-State of R equals
s +* (NAT .--> u);
coherence
proof
A1: now
let x be object;
assume
A2: x in dom((SCM-VAL R)*SCM-OK);
per cases;
suppose
A3: x = NAT;
NAT in dom(NAT .--> u) by TARSKI:def 1;
then (s +* (NAT .--> u)).NAT = (NAT .--> u).NAT by FUNCT_4:13
.= u by FUNCOP_1:72;
then (s +* (NAT .--> u)).NAT in NAT by ORDINAL1:def 12;
hence (s +* (NAT .--> u)).x in ((SCM-VAL R)*SCM-OK).x by A3,Th1;
end;
suppose
A4: x <> NAT;
not x in dom(NAT .--> u) by A4,TARSKI:def 1;
then (s +* (NAT .--> u)).x = s.x by FUNCT_4:11;
hence (s +* (NAT .--> u)).x in ((SCM-VAL R)*SCM-OK).x by A2,CARD_3:9;
end;
end;
A5: dom((SCM-VAL R)*SCM-OK) = SCM-Memory by Lm1;
then dom s = SCM-Memory by CARD_3:9;
then dom(s +* (NAT .--> u)) = SCM-Memory \/ dom(NAT .--> u) by
FUNCT_4:def 1
.= SCM-Memory \/ {NAT}
.= dom((SCM-VAL R)*SCM-OK) by A5,AMI_2:22,ZFMISC_1:40;
hence thesis by A1,CARD_3:9;
end;
end;
theorem
for s being SCM-State of G, u being natural Number holds SCM-Chg(s,u).NAT = u
proof
let s be SCM-State of G, u be natural Number;
NAT in dom(NAT .--> u) by TARSKI:def 1;
hence SCM-Chg(s,u).NAT = (NAT .--> u).NAT by FUNCT_4:13
.= u by FUNCOP_1:72;
end;
theorem
for s being SCM-State of G, u being natural Number, mk being Element of
SCM-Data-Loc holds SCM-Chg(s,u).mk = s.mk
proof
let s be SCM-State of G, u be natural Number, mk be Element of SCM-Data-Loc;
NAT in SCM-Memory by AMI_2:22;
then SCM-OK.NAT = 0 & SCM-OK.mk = 1 by AMI_2:def 4;
then not mk in dom(NAT .--> u) by TARSKI:def 1;
hence thesis by FUNCT_4:11;
end;
theorem
for s being SCM-State of G, u, v being natural Number
holds SCM-Chg(s,u).v = s.v
proof
let s be SCM-State of G, u, v be natural Number;
not v in dom(NAT .--> u) by TARSKI:def 1;
hence thesis by FUNCT_4:11;
end;
definition
let R be non empty 1-sorted, s be SCM-State of R, t be Element of
SCM-Data-Loc, u be Element of R;
func SCM-Chg(s,t,u) -> SCM-State of R equals
s +* (t .--> u);
coherence
proof
A1: now
let x be object;
assume
A2: x in dom((SCM-VAL R)*SCM-OK);
per cases;
suppose
A3: x = t;
t in dom(t .--> u) by TARSKI:def 1;
then (s +* (t .--> u)).t = (t .--> u).t by FUNCT_4:13
.= u by FUNCOP_1:72;
then (s +* (t .--> u)).t in the carrier of R;
hence (s +* (t .--> u)).x in ((SCM-VAL R)*SCM-OK).x by A3,Th2;
end;
suppose
A4: x <> t;
not x in dom(t .--> u) by A4,TARSKI:def 1;
then (s +* (t .--> u)).x = s.x by FUNCT_4:11;
hence (s +* (t .--> u)).x in ((SCM-VAL R)*SCM-OK).x by A2,CARD_3:9;
end;
end;
A5: dom((SCM-VAL R)*SCM-OK) = SCM-Memory by Lm1;
then dom s = SCM-Memory by CARD_3:9;
then dom(s +* (t .--> u)) = SCM-Memory \/ dom(t .--> u) by FUNCT_4:def 1
.= SCM-Memory \/ {t}
.= dom((SCM-VAL R)*SCM-OK) by A5,ZFMISC_1:40;
hence thesis by A1,CARD_3:9;
end;
end;
theorem
for s being SCM-State of G, t being Element of SCM-Data-Loc, u being
Element of G holds SCM-Chg(s,t,u).NAT = s.NAT
proof
let s be SCM-State of G, t be Element of SCM-Data-Loc, u be Element of G;
NAT in SCM-Memory by AMI_2:22;
then SCM-OK.NAT = 0 & SCM-OK.t = 1 by AMI_2:def 4;
then not NAT in dom(t .--> u) by TARSKI:def 1;
hence thesis by FUNCT_4:11;
end;
theorem
for s being SCM-State of G, t being Element of SCM-Data-Loc, u being
Element of G holds SCM-Chg(s,t,u).t = u
proof
let s be SCM-State of G, t be Element of SCM-Data-Loc, u be Element of G;
t in dom(t .--> u) by TARSKI:def 1;
hence SCM-Chg(s,t,u).t = (t .--> u).t by FUNCT_4:13
.= u by FUNCOP_1:72;
end;
theorem
for s being SCM-State of G, t being Element of SCM-Data-Loc, u being
Element of G, mk being Element of SCM-Data-Loc st mk <> t holds SCM-Chg(s,t,u).
mk = s.mk
proof
let s be SCM-State of G, t be Element of SCM-Data-Loc, u be Element of G, mk
be Element of SCM-Data-Loc such that
A1: mk <> t;
not mk in dom(t .--> u) by A1,TARSKI:def 1;
hence thesis by FUNCT_4:11;
end;
definition
let R be non empty 1-sorted, s be SCM-State of R, a be Element of
SCM-Data-Loc;
redefine func s.a -> Element of R; :: redefines . (FUNCT_1, definition)
coherence
proof
s.a in pi(product((SCM-VAL R)*SCM-OK),a) by CARD_3:def 6;
hence thesis by Th5;
end;
end;
definition
let S be non empty 1-sorted, d be Element of SCM-Data-Loc, s be Element of S;
redefine func <*d,s*> -> FinSequence of SCM-Data-Loc \/ the carrier of S; :: redefines <* (FINSEQ_1, definition)
coherence
proof
let y be object;
A1: dom <*d,s*> = {1,2} by FINSEQ_1:2,89;
assume y in rng <*d,s*>;
then consider x being object such that
A2: x in dom <*d,s*> and
A3: <*d,s*>.x = y by FUNCT_1:def 3;
per cases by A2,A1,TARSKI:def 2;
suppose
x = 1;
then y = d by A3;
hence thesis by XBOOLE_0:def 3;
end;
suppose
x = 2;
then y = s by A3;
hence thesis by XBOOLE_0:def 3;
end;
end;
end;
definition
::$CD 7
let R be Ring, x be Element of SCM-Instr R, s be SCM-State of R;
func SCM-Exec-Res (x,s) -> SCM-State of R equals
SCM-Chg(SCM-Chg(s, x address_1, s.(x address_2)), IC s + 1)
if ex mk, ml being Element of SCM-Data-Loc st x = [1,{},<*mk,ml*>],
SCM-Chg(SCM-Chg(s, x address_1, s.(x address_1)+s.(x address_2)), IC s + 1)
if ex mk, ml being Element of SCM-Data-Loc st x = [2,{},<*mk,ml*>],
SCM-Chg(SCM-Chg(s, x address_1, s.(x address_1)-s.(x address_2)), IC s + 1)
if ex mk, ml being Element of SCM-Data-Loc st x = [3,{},<*mk,ml*>],
SCM-Chg(SCM-Chg(s, x address_1, s.(x address_1)*s.(x address_2)), IC s + 1)
if ex mk, ml being Element of SCM-Data-Loc st x = [4,{},<*mk,ml*>],
SCM-Chg(s, x jump_address)
if ex mk being Element of NAT st x = [6,<*mk*>,{}],
SCM-Chg(s, IFEQ(s.(x cond_address), 0.R, x cjump_address, IC s + 1))
if ex mk being Element of NAT, ml being Element of SCM-Data-Loc
st x = [7,<*mk*>,<*ml*>],
SCM-Chg(SCM-Chg(s, x const_address, x const_value), IC s + 1)
if ex mk being Element of SCM-Data-Loc, r being Element of R
st x = [5,{},<*mk,r*>]
otherwise s;
coherence;
consistency by XTUPLE_0:3;
end;
definition
let R be Ring;
func SCM-Exec R -> Action of SCM-Instr R,
product((SCM-VAL R)*SCM-OK) means
for x being Element of SCM-Instr R, y being SCM-State of R
holds (it.x).y = SCM-Exec-Res (x,y);
existence
proof
deffunc U(Element of SCM-Instr R, SCM-State of R) = SCM-Exec-Res($1,$2);
consider f being
Function of [:SCM-Instr R,product((SCM-VAL R)*SCM-OK):], product
((SCM-VAL R)*SCM-OK) such that
A1: for x being Element of SCM-Instr R, y being SCM-State of R holds f
.(x,y) = U(x,y) from BINOP_1:sch 4;
take curry f;
let x be Element of SCM-Instr R, y be SCM-State of R;
thus (curry f).x.y = f.(x,y) by FUNCT_5:69
.= SCM-Exec-Res(x,y) by A1;
end;
uniqueness
proof
let f, g be Action of SCM-Instr R, product((SCM-VAL R)*SCM-OK) such that
A2: for x being Element of SCM-Instr R, y being SCM-State of R holds (
f.x).y = SCM-Exec-Res(x,y) and
A3: for x being Element of SCM-Instr R, y being SCM-State of R holds (
g.x).y = SCM-Exec-Res(x,y);
now
let x be Element of SCM-Instr R;
reconsider gx = g.x, fx = f.x
as Function of product((SCM-VAL R)*SCM-OK), product
((SCM-VAL R)*SCM-OK) by FUNCT_2:66;
now
let y be SCM-State of R;
thus fx.y = SCM-Exec-Res(x,y) by A2
.= gx.y by A3;
end;
hence f.x = g.x by FUNCT_2:63;
end;
hence f = g by FUNCT_2:63;
end;
end;
::$CT 6
theorem
for s being SCM-State of S holds dom s = SCM-Memory
proof let s be SCM-State of S;
dom s = dom((SCM-VAL S)*SCM-OK) by CARD_3:9;
hence thesis by Lm1;
end;