:: A Small Computer Model with Push-Down Stack
::  by JingChao Chen
::
:: Received June 15, 1999
:: Copyright (c) 1999-2019 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, INT_1, XBOOLE_0, FINSEQ_1,
      RELAT_1, ARYTM_3, FUNCT_1, CARD_3, AMI_1, FUNCOP_1, COMPLEX1, XXREAL_0,
      ARYTM_1, ZFMISC_1, FUNCT_5, SCMPDS_1, GROUP_9;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, CARD_1, FUNCT_2,
      BINOP_1, ORDINAL1, NUMBERS, XCMPLX_0, CARD_3, INT_1, NAT_1, FINSEQ_1,
      FUNCOP_1, XXREAL_0, FUNCT_5, AMI_2, INT_2, COMPOS_0, SCMPDS_I;
 constructors NAT_1, NAT_D, FUNCT_5, AMI_2, RELSET_1, FUNCOP_1, COMPOS_0,
      SCMPDS_I, BINOP_1;
 registrations ORDINAL1, RELSET_1, XREAL_0, INT_1, FINSEQ_1, CARD_3, AMI_2,
      ORDINAL2, XXREAL_0, FUNCT_1, FUNCT_2, SCM_INST, SCMPDS_I;
 requirements NUMERALS, SUBSET, BOOLE;
 definitions TARSKI, FINSEQ_1;
 theorems AMI_2, FINSEQ_1, TARSKI, FUNCT_1, FUNCT_2, INT_1, XBOOLE_0, XBOOLE_1,
      FUNCT_5;
 schemes BINOP_1;

begin :: Preliminaries

reserve
  i, j, k for Element of NAT,
  I,I2,I3,I4 for Element of Segm 15,
  i1 for Element of NAT,
  d1,d2,d3,d4,d5 for Element of SCM-Data-Loc,
  k1,k2 for Integer;

::$CT 2

theorem
  for d be Element of SCM-Data-Loc holds d in SCM-Data-Loc \/ INT
by XBOOLE_1:7,TARSKI:def 3;

begin  :: The construction of SCM with Push-Down Stack
:: [0,goto L]
:: [1,return sp<-sp+0,count<-(sp)+2]
:: [2,a:=c(constant)]
:: [3,saveIC (a,k)]
:: [4,if(a,k)<>0 goto L ]
:: [5,if(a,k)<=0 goto L ]
:: [6,if(a,k)>=0 goto L ]
:: [7,(a,k):=c(constant) ]
:: [8,(a,k1)+k2]
:: [9, (a1,k1)+(a2,k2)]
:: [10,(a1,k1)-(a2,k2)]
:: [11,(a1,k1)*(a2,k2)]
:: [12,(a1,k1)/(a2,k2)]
:: [13,(a1,k1):=(a2,k2)]

definition
::$CD 5
  let s be SCM-State, a be Element of SCM-Data-Loc, n be Integer;
  func Address_Add(s,a,n) -> Element of SCM-Data-Loc equals
  [1,|.s.a+n.|];
  coherence by AMI_2:24;
end;

definition
  let s be SCM-State, n be Integer;
  func jump_address(s,n) -> Element of NAT equals
  |.(IC s qua Element of NAT)+n.|;
  coherence;
end;

definition
  let d be Element of SCM-Data-Loc, s be Integer;
  redefine func <*d,s*> -> FinSequence of SCM-Data-Loc \/ INT;
  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,FINSEQ_1:44;
      hence thesis by XBOOLE_0:def 3;
    end;
    suppose
A4:   x = 2;
A5:   s in INT by INT_1:def 2;
      y = s by A3,A4,FINSEQ_1:44;
      hence thesis by A5,XBOOLE_0:def 3;
    end;
  end;
end;

definition
::$CD 11
  let s be SCM-State, a be Element of SCM-Data-Loc;
  func PopInstrLoc(s,a) -> Element of NAT equals
  |.s.a.|+2;
  coherence;
end;

:: RetSP: Return Stack Pointer
:: RetIC: Return Instruction-Counter

::$CD 2

definition
  let x be Element of SCMPDS-Instr, s be SCM-State;
  func SCM-Exec-Res (x,s) -> SCM-State equals
  SCM-Chg(s, jump_address(s,x const_INT ))
   if InsCode x = 14,
  SCM-Chg(SCM-Chg(s, x P21address, x P22const), IC s + 1)
   if InsCode x = 2,
  SCM-Chg(SCM-Chg(s,Address_Add(s,x P21address,x P22const),
   IC s qua Element of NAT),IC s + 1)
   if InsCode x = 3,
  SCM-Chg(SCM-Chg(s, x address_1,s.Address_Add(s,x address_1,RetSP)),
    PopInstrLoc(s,Address_Add(s,x address_1,RetIC)) )
   if InsCode x = 1,
  SCM-Chg(s,IFEQ(s.Address_Add(s,x P31address,x P32const), 0, IC s + 1,
        jump_address(s,x P33const )))
   if InsCode x = 4,
  SCM-Chg(s,IFGT(s.Address_Add(s,x P31address,x P32const), 0, IC
      s + 1,jump_address(s,x P33const )))
   if InsCode x = 5,
  SCM-Chg(s, IFGT(0, s.Address_Add(s,x P31address,x P32const), IC s + 1,
         jump_address(s,x P33const )))
   if InsCode x = 6,
  SCM-Chg(SCM-Chg(s,
    Address_Add(s,x P31address,x P32const), x P33const), IC s + 1)
   if InsCode x = 7,
  SCM-Chg(SCM-Chg(s,Address_Add(s,x P31address,x P32const),
      s.Address_Add(s,x P31address,x P32const)+ (x P33const)), IC s + 1)
   if InsCode x = 8,
  SCM-Chg(SCM-Chg(s,Address_Add(s,x P41address,x P43const),
      s.Address_Add(s,x P41address,x P43const)+
      s.Address_Add(s,x P42address,x P44const)),IC s + 1)
   if InsCode x = 9,
  SCM-Chg(SCM-Chg(s, Address_Add(s,x P41address,x P43const),
    s.Address_Add(s,x P41address,x P43const) - s.Address_Add(s,x
    P42address,x P44const)),IC s + 1)
   if InsCode x = 10,
  SCM-Chg(SCM-Chg(s, Address_Add(s,x P41address,x P43const),
      s.Address_Add(s,x P41address,x P43const) *
      s.Address_Add(s,x P42address,x P44const)),IC s + 1)
   if InsCode x = 11,
  SCM-Chg(SCM-Chg(s,Address_Add(s,x P41address,x P43const),
      s.Address_Add(s,x P42address,x P44const)), IC s + 1)
   if InsCode x = 13,
  SCM-Chg(SCM-Chg(SCM-Chg(s,Address_Add(s,x P41address,x P43const),
    s.Address_Add(s,x P41address,x P43const) div
    s.Address_Add(s,x P42address,x P44const)),
      Address_Add(s,x P42address,x P44const),
    s.Address_Add(s,x P41address,x P43const) mod
    s.Address_Add(s,x P42address,x P44const)), IC s + 1)
   if InsCode x = 12
  otherwise s;
  coherence;
  consistency;
end;

definition
  func SCMPDS-Exec -> Action of SCMPDS-Instr,
     product(SCM-VAL*SCM-OK) means
  for x being Element of SCMPDS-Instr, y being
  SCM-State holds (it.x).y = SCM-Exec-Res (x,y);
  existence
  proof
    consider f being
     Function of [:SCMPDS-Instr,product(SCM-VAL*SCM-OK):], product
    (SCM-VAL*SCM-OK) such that
A1: for x being Element of SCMPDS-Instr, y being SCM-State holds f.
    (x,y) = SCM-Exec-Res(x,y) from BINOP_1:sch 4;
    take curry f;
    let x be Element of SCMPDS-Instr, y be SCM-State;
    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 SCMPDS-Instr, product(SCM-VAL*SCM-OK) such that
A2: for x being Element of SCMPDS-Instr, y being SCM-State holds (f
    .x).y = SCM-Exec-Res(x,y) and
A3: for x being Element of SCMPDS-Instr, y being SCM-State holds (g
    .x).y = SCM-Exec-Res(x,y);
    now
      let x be Element of SCMPDS-Instr;
      reconsider gx = g.x, fx = f.x
       as Function of product(SCM-VAL*SCM-OK), product
      (SCM-VAL*SCM-OK) by FUNCT_2:66;
      now
        let y be SCM-State;
        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;