:: The Basic Properties of { \bf SCM } over Ring
::  by Artur Korni{\l}owicz
::
:: Received November 29, 1998
:: Copyright (c) 1998-2021 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, XBOOLE_0, STRUCT_0, FUNCSDOM, AMI_3,
      AMI_1, AMI_2, FUNCT_7, TARSKI, RELAT_1, FSM_1, FUNCT_1, CAT_1, FINSEQ_1,
      GRAPHSP, FUNCT_2, CARD_3, ARYTM_3, ARYTM_1, SUPINF_2, FUNCOP_1, SCMRING1,
      GLIB_000, FUNCT_4, RECDEF_2, GOBRD13, MEMSTR_0, NAT_1;
 notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, DOMAIN_1, RELAT_1, FUNCT_1,
      ORDINAL1, CARD_1, FUNCT_2, RECDEF_2, XCMPLX_0, STRUCT_0, ALGSTR_0,
      VECTSP_1, CARD_3, FINSEQ_1, NUMBERS, FUNCOP_1, FUNCT_4, FUNCT_7,
      MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, AMI_2, AMI_3, SCMRINGI, SCMRING1;
 constructors FINSEQ_4, REALSET1, AMI_3, SCMRING1, PRE_POLY, FUNCT_7, RELSET_1;
 registrations ORDINAL1, RELSET_1, FUNCOP_1, FINSEQ_1, CARD_3, STRUCT_0, AMI_3,
      SCMRING1, AMI_2, FUNCT_1, EXTPRO_1, SCMRINGI, SCM_INST, XTUPLE_0, NAT_1,
      XCMPLX_0, ORDINAL2;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;


begin  :: { \bf SCM } over ring

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

 reserve R for Ring, T for InsType of SCM-Instr R;

definition
  let R be Ring;
  func SCM R -> strict AMI-Struct over Segm 2 means
:: SCMRING2:def 1

  the carrier of it = SCM-Memory & the ZeroF of it = NAT &
  the InstructionsF of it = SCM-Instr R &
  the Object-Kind of it = SCM-OK &
  the ValuesF of it = SCM-VAL R &
  the Execution of it = SCM-Exec R;
end;

registration
  let R be Ring;
  cluster SCM R -> non empty;
end;

registration
  let R be Ring;
  cluster SCM R -> with_non-empty_values;
end;

registration
 let R be Ring;
 cluster Int-like for Object of SCM R;
end;

definition
  let R be Ring;
  mode Data-Location of R is Int-like Object of SCM R;
::$CD
end;

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

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

definition
  let R be 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,{},{}] is Instruction of SCM R;

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

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

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

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

definition
  let R be 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 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 Ring, l be Nat;
  func goto(l,R) -> Instruction of SCM R equals
:: SCMRING2:def 8
  [6,<*l*>,{}];
end;

definition
  let R be Ring, l be Nat, 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:7
  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,R)) 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;

registration
  let R be non empty Ring;
  cluster SCM R -> IC-Ins-separated;
end;

theorem :: SCMRING2:8
  IC SCM R = NAT;

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



theorem :: SCMRING2:10
  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:11
  Exec(a := b, s).IC SCM R = IC s + 1 & Exec(a := b, s).a = s.b &
  for c st c <> a holds Exec(a := b, s).c = s.c;

theorem :: SCMRING2:12
  Exec(AddTo(a,b), s).IC SCM R = IC s + 1 & 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:13
  Exec(SubFrom(a,b), s).IC SCM R = IC s + 1 & 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:14
  Exec(MultBy(a,b), s).IC SCM R = IC s + 1 & 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:15
  Exec(goto(i1,R), s).IC SCM R = i1 & Exec(goto(i1,R), s).c = s.c;

theorem :: SCMRING2:16
  (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 = IC s + 1) & Exec(a =0_goto i1,
  s).c = s.c;

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

begin  :: Halt instruction

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

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

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

registration
  let R, i1;
  cluster goto(i1,R) -> non halting;
end;

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

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

registration
  let R;
  cluster SCM R -> halting;
end;

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

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

theorem :: SCMRING2:22
  Data-Locations SCM R = Data-Locations SCM;

theorem :: SCMRING2:23
  x is Data-Location of R iff x in Data-Locations SCM R;

theorem :: SCMRING2:24
 for R being Ring
  holds the_Values_of SCM R = (SCM-VAL R)*SCM-OK;

theorem :: SCMRING2:25
 for R being Ring holds
 (the carrier of SCM R) \ {NAT} = SCM-Data-Loc;