The abstract of the Mizar article:

The Construction of \SCM over Ring

by

Artur Kornilowicz

Received November 29, 1998

MML identifier: SCMRING1

[ Mizar article, MML identifier index ]

environ

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


begin  :: The construction of { \bf SCM } over ring

reserve i, j, k for Nat,
        I for Element of Segm 8,
        i1, i2 for Element of SCM-Instr-Loc,
        d1, d2, d3, d4 for Element of SCM-Data-Loc,
        S for non empty 1-sorted;

definition
  cluster infinite -> non trivial set;
  cluster infinite -> non trivial 1-sorted;
end;

definition
 cluster trivial -> Abelian add-associative right_zeroed right_complementable
                    (non empty LoopStr);
 cluster trivial -> right_unital right-distributive (non empty doubleLoopStr);
end;

definition
 cluster -> natural Element of SCM-Data-Loc;
end;

definition
 cluster SCM-Instr -> non trivial;
 cluster SCM-Instr-Loc -> infinite;
end;

definition let S be non empty 1-sorted;
 func SCM-Instr S ->
          Subset of [: Segm 8, (union {the carrier of S} \/ NAT)* :] equals
:: SCMRING1:def 1

  { [0,{}] } \/
  { [I,<*a,b*>] where I is Element of Segm 8,
                      a, b is Element of SCM-Data-Loc: I in { 1,2,3,4 } } \/
  { [6,<*i*>] where i is Element of SCM-Instr-Loc: not contradiction } \/
  { [7,<*i,a*>] where i is Element of SCM-Instr-Loc,
                      a is Element of SCM-Data-Loc: not contradiction } \/
  { [5,<*a,r*>] where a is Element of SCM-Data-Loc,
                      r is Element of S: not contradiction };
end;

definition let S be non empty 1-sorted;
 cluster SCM-Instr S -> non trivial;
end;

definition let S be non empty 1-sorted;
 attr S is good means
:: SCMRING1:def 2
  the carrier of S <> SCM-Instr-Loc & the carrier of S <> SCM-Instr S;
end;

definition
 cluster trivial -> good (non empty 1-sorted);
end;

definition
 cluster strict trivial non empty 1-sorted;
end;

definition
 cluster strict trivial non empty doubleLoopStr;
end;

definition
 cluster strict trivial Ring;
end;

reserve G for good (non empty 1-sorted);

definition let S be non empty 1-sorted;
 func SCM-OK S ->
    Function of NAT, {the carrier of S} \/ { SCM-Instr S, SCM-Instr-Loc } means
:: SCMRING1:def 3

  it.0 = SCM-Instr-Loc &
  for k being Nat holds it.(2*k+1) = the carrier of S &
                        it.(2*k+2) = SCM-Instr S;
end;

definition let S be non empty 1-sorted;
 mode SCM-State of S is Element of product SCM-OK S;
end;

theorem :: SCMRING1:1
 SCM-Instr-Loc <> SCM-Instr S;

theorem :: SCMRING1:2
 (SCM-OK G).i = SCM-Instr-Loc iff i = 0;

theorem :: SCMRING1:3
 (SCM-OK G).i = the carrier of G iff ex k st i = 2*k+1;

theorem :: SCMRING1:4
 (SCM-OK G).i = SCM-Instr G iff ex k st i = 2*k+2;

theorem :: SCMRING1:5
 (SCM-OK G).d1 = the carrier of G;

theorem :: SCMRING1:6
 (SCM-OK G).i1 = SCM-Instr G;

theorem :: SCMRING1:7
 pi(product SCM-OK S,0) = SCM-Instr-Loc;

theorem :: SCMRING1:8
 pi(product SCM-OK G,d1) = the carrier of G;

theorem :: SCMRING1:9
   pi(product SCM-OK G,i1) = SCM-Instr G;

definition let S be non empty 1-sorted, s be SCM-State of S;
 func IC s -> Element of SCM-Instr-Loc equals
:: SCMRING1:def 4
    s.0;
end;

definition let R be good (non empty 1-sorted),
               s be SCM-State of R,
               u be Element of SCM-Instr-Loc;
 func SCM-Chg(s,u) -> SCM-State of R equals
:: SCMRING1:def 5
  s +* (0 .--> u);
end;

theorem :: SCMRING1:10
   for s being SCM-State of G, u being Element of SCM-Instr-Loc
  holds SCM-Chg(s,u).0 = u;

theorem :: SCMRING1:11
   for s being SCM-State of G, u being Element of SCM-Instr-Loc,
     mk being Element of SCM-Data-Loc
  holds SCM-Chg(s,u).mk = s.mk;

theorem :: SCMRING1:12
   for s being SCM-State of G,
     u, v being Element of SCM-Instr-Loc
  holds SCM-Chg(s,u).v = s.v;

definition let R be good (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
:: SCMRING1:def 6
  s +* (t .--> u);
end;

theorem :: SCMRING1:13
   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).0 = s.0;

theorem :: SCMRING1:14
   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;

theorem :: SCMRING1:15
   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;

theorem :: SCMRING1:16
   for s being SCM-State of G, t being Element of SCM-Data-Loc,
     u being Element of G,
     v being Element of SCM-Instr-Loc
  holds SCM-Chg(s,t,u).v = s.v;

definition let R be good (non empty 1-sorted),
               s be SCM-State of R,
               a be Element of SCM-Data-Loc;
 redefine func s.a -> Element of R;
end;

definition let S be non empty 1-sorted, x be Element of SCM-Instr S;
 given mk, ml being Element of SCM-Data-Loc, I such that
 x = [ I, <*mk, ml*>];
 func x address_1 -> Element of SCM-Data-Loc means
:: SCMRING1:def 7
  ex f being FinSequence of SCM-Data-Loc st f = x`2 & it = f/.1;

 func x address_2 -> Element of SCM-Data-Loc means
:: SCMRING1:def 8
  ex f being FinSequence of SCM-Data-Loc st f = x`2 & it = f/.2;
end;

theorem :: SCMRING1:17
   for x being Element of SCM-Instr S, mk, ml being Element of SCM-Data-Loc
  st x = [ I, <*mk, ml*>] holds
 x address_1 = mk & x address_2 = ml;

definition let R be non empty 1-sorted, x be Element of SCM-Instr R;
 given mk being Element of SCM-Instr-Loc, I such that
 x = [ I, <*mk*>];
 func x jump_address -> Element of SCM-Instr-Loc means
:: SCMRING1:def 9
  ex f being FinSequence of SCM-Instr-Loc st f = x`2 & it = f/.1;
end;

theorem :: SCMRING1:18
   for x being Element of SCM-Instr S, mk being Element of SCM-Instr-Loc
  st x = [ I, <*mk*>] holds
 x jump_address = mk;

definition let S be non empty 1-sorted, x be Element of SCM-Instr S;
 given mk being Element of SCM-Instr-Loc,
       ml being Element of SCM-Data-Loc, I such that
 x = [ I, <*mk,ml*>];
 func x cjump_address -> Element of SCM-Instr-Loc means
:: SCMRING1:def 10
  ex mk being Element of SCM-Instr-Loc,
     ml being Element of SCM-Data-Loc st <*mk,ml*> = x`2 & it = <*mk,ml*>/.1;

 func x cond_address -> Element of SCM-Data-Loc means
:: SCMRING1:def 11
  ex mk being Element of SCM-Instr-Loc,
     ml being Element of SCM-Data-Loc st <*mk,ml*> = x`2 & it = <*mk,ml*>/.2;
end;

theorem :: SCMRING1:19
   for x being Element of SCM-Instr S, mk being Element of SCM-Instr-Loc,
     ml being Element of SCM-Data-Loc
  st x = [ I, <*mk,ml*>]
  holds x cjump_address = mk & x cond_address = ml;

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

definition let S be non empty 1-sorted, x be Element of SCM-Instr S;
 given mk being Element of SCM-Data-Loc, r being Element of S,
       I such that
 x = [ I, <*mk, r*>];
 func x const_address -> Element of SCM-Data-Loc means
:: SCMRING1:def 12
  ex f being FinSequence of SCM-Data-Loc \/ the carrier of S
   st f = x`2 & it = f/.1;

 func x const_value -> Element of S means
:: SCMRING1:def 13
  ex f being FinSequence of SCM-Data-Loc \/ the carrier of S
   st f = x`2 & it = f/.2;
end;

theorem :: SCMRING1:20
   for x being Element of SCM-Instr S, mk being Element of SCM-Data-Loc,
     r being Element of S st x = [ I, <*mk, r*>] holds
  x const_address = mk & x const_value = r;

definition let R be good 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
:: SCMRING1:def 14
    SCM-Chg(SCM-Chg(s, x address_1, s.(x address_2)), Next IC s)
        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)), Next IC s)
        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)), Next IC s)
        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)), Next IC s)
        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 SCM-Instr-Loc st x = [ 6, <*mk*>],
  SCM-Chg(s, IFEQ(s.(x cond_address), 0.R, x cjump_address, Next IC s))
        if ex mk being Element of SCM-Instr-Loc,
              ml being Element of SCM-Data-Loc st x = [ 7, <*mk, ml*>],
  SCM-Chg(SCM-Chg(s, x const_address, x const_value), Next IC s)
        if ex mk being Element of SCM-Data-Loc,
               r being Element of R st x = [ 5, <*mk, r*>]
  otherwise s;
end;

definition let S be non empty 1-sorted,
     f be Function of SCM-Instr S, Funcs(product SCM-OK S, product SCM-OK S),
     x be Element of SCM-Instr S;
 cluster f.x -> Function-like Relation-like;
end;

definition let R be good Ring;
 func SCM-Exec R ->
      Function of SCM-Instr R, Funcs(product SCM-OK R, product SCM-OK R) means
:: SCMRING1:def 15
    for x being Element of SCM-Instr R, y being SCM-State of R holds
   (it.x).y = SCM-Exec-Res (x,y);
end;