The abstract of the Mizar article:

The Construction and Computation of While-Loop Programs for SCMPDS

by

Jing-Chao Chen

Received June 14, 2000

MML identifier: SCMPDS_8

[ Mizar article, MML identifier index ]

environ

 vocabulary AMI_3, SCMPDS_2, AMI_1, AMI_2, SCMP_GCD, FUNCT_1, SCMPDS_3,
      RELAT_1, AMI_5, CARD_3, INT_1, SCMPDS_4, SCMFSA_9, CARD_1, SCMFSA6A,
      ARYTM_1, SCMFSA_7, SCMPDS_5, UNIALG_2, SCMFSA7B, FUNCT_4, SCMFSA6B,
      SCM_1, RELOC, FUNCT_7, BOOLE, SCMPDS_8;
 notation XBOOLE_0, SUBSET_1, FUNCT_2, NUMBERS, XCMPLX_0, XREAL_0, RELAT_1,
      FUNCT_1, FUNCT_4, RECDEF_1, INT_1, NAT_1, STRUCT_0, AMI_1, AMI_2, AMI_3,
      AMI_5, FUNCT_7, SCMPDS_2, SCMPDS_3, CARD_1, SCMPDS_4, SCM_1, SCMPDS_5,
      SCMPDS_6, SCMP_GCD, CARD_3, DOMAIN_1;
 constructors DOMAIN_1, NAT_1, AMI_5, RECDEF_1, SCMPDS_4, SCM_1, SCMPDS_5,
      SCMPDS_6, SCMP_GCD, MEMBERED;
 clusters AMI_1, INT_1, FUNCT_1, RELSET_1, SCMPDS_2, SCMFSA_4, SCMPDS_4,
      SCMPDS_5, SCMPDS_6, FRAENKEL, XREAL_0, MEMBERED, NUMBERS, ORDINAL2;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;


begin :: Preliminaries

reserve x,a for Int_position,
        s for State of SCMPDS;

theorem :: SCMPDS_8:1     :: see SCMPDS_3:32
 for a be Int_position ex i being Nat
  st a = intpos i;

definition
 let t be State of SCMPDS;
 func Dstate(t) -> State of SCMPDS means
:: SCMPDS_8:def 1
  for x be set holds
    (x in SCM-Data-Loc implies it.x = t.x)
    & ( x in the Instruction-Locations of SCMPDS implies it.x = goto 0) &
    (x=IC SCMPDS implies it.x=inspos 0);
end;

theorem :: SCMPDS_8:2
 for t1,t2 being State of SCMPDS st t1|SCM-Data-Loc=t2|SCM-Data-Loc
 holds Dstate(t1)=Dstate(t2);

theorem :: SCMPDS_8:3
 for t being State of SCMPDS,i being Instruction of SCMPDS
 st InsCode i in {0,4,5,6} holds Dstate(t)=Dstate(Exec(i,t));

theorem :: SCMPDS_8:4
 (Dstate(s)).a=s.a;

theorem :: SCMPDS_8:5
 for a be Int_position holds
 (ex f be Function of product the Object-Kind of SCMPDS,NAT st
     for s being State of SCMPDS holds
 (s.a <= 0 implies f.s =0) & (s.a > 0 implies f.s=s.a));

begin :: The construction and several basic properties of while<0 program
:: while (a,i)<0 do I
definition
 let a be Int_position, i be Integer,I be Program-block;
 func while<0(a,i,I) -> Program-block equals
:: SCMPDS_8:def 2
    (a,i)>=0_goto (card I +2) ';' I ';' goto -(card I+1);
end;

definition
   let I be shiftable Program-block,a be Int_position,i be Integer;
   cluster while<0(a,i,I) -> shiftable;
end;

definition
   let I be No-StopCode Program-block, a be Int_position,i be Integer;
   cluster while<0(a,i,I) -> No-StopCode;
end;

theorem :: SCMPDS_8:6
 for a be Int_position,i be Integer,I be Program-block holds
  card while<0(a,i,I)= card I +2;

theorem :: SCMPDS_8:7
 for a be Int_position,i be Integer,m be Nat,I be Program-block holds
   m < card I+2 iff inspos m in dom while<0(a,i,I);

theorem :: SCMPDS_8:8
 for a be Int_position,i be Integer,I be Program-block holds
    while<0(a,i,I).inspos 0=(a,i)>=0_goto (card I +2) &
    while<0(a,i,I).inspos (card I+1)=goto -(card I+1);

theorem :: SCMPDS_8:9
 for s being State of SCMPDS,I being Program-block,a being Int_position,
 i being Integer st s.DataLoc(s.a,i) >= 0 holds
 while<0(a,i,I) is_closed_on s & while<0(a,i,I) is_halting_on s;

theorem :: SCMPDS_8:10
 for s being State of SCMPDS,I being Program-block,a,c being Int_position,
 i being Integer st s.DataLoc(s.a,i) >= 0 holds
 IExec(while<0(a,i,I),s) = s +* Start-At inspos (card I + 2);

theorem :: SCMPDS_8:11
   for s being State of SCMPDS,I being Program-block,a being Int_position,
 i being Integer st s.DataLoc(s.a,i) >= 0 holds
   IC IExec(while<0(a,i,I),s) = inspos (card I + 2);

theorem :: SCMPDS_8:12
   for s being State of SCMPDS,I being Program-block,a,b being Int_position,
 i being Integer st s.DataLoc(s.a,i) >= 0 holds
   IExec(while<0(a,i,I),s).b = s.b;

scheme WhileLHalt { F(State of SCMPDS)-> Nat,
 s() -> State of SCMPDS,I() -> No-StopCode shiftable Program-block,
 a() -> Int_position,i() -> Integer,P[State of SCMPDS]}:
   (F(s())=F(s()) or P[s()]) &
   while<0(a(),i(),I()) is_closed_on s() &
   while<0(a(),i(),I()) is_halting_on s()
provided
 card I() > 0 and
 (for t be State of SCMPDS st P[Dstate t] & F(Dstate(t))=0 holds
    t.DataLoc(s().a(),i()) >= 0) and
 P[Dstate s()] and
 for t be State of SCMPDS st
       P[Dstate t] & t.a()=s().a() & t.DataLoc(s().a(),i()) < 0
    holds IExec(I(),t).a()=t.a() & I() is_closed_on t &
        I() is_halting_on t & F(Dstate IExec(I(),t)) < F(Dstate t) &
        P[Dstate(IExec(I(),t))];

scheme WhileLExec { F(State of SCMPDS)-> Nat,
 s() -> State of SCMPDS,I() -> No-StopCode shiftable Program-block,
 a() -> Int_position,i() -> Integer,P[State of SCMPDS]}:
   (F(s())=F(s()) or P[s()]) &
   IExec(while<0(a(),i(),I()),s()) =
    IExec(while<0(a(),i(),I()),IExec(I(),s()))
provided
 card I() > 0 and
 s().DataLoc(s().a(),i()) < 0 and
 (for t be State of SCMPDS st P[Dstate t] & F(Dstate(t))=0 holds
    t.DataLoc(s().a(),i()) >= 0) and
 P[Dstate s()] and
 for t be State of SCMPDS st
       P[Dstate t] & t.a()=s().a() & t.DataLoc(s().a(),i()) < 0
    holds IExec(I(),t).a()=t.a() & I() is_closed_on t &
        I() is_halting_on t & F(Dstate IExec(I(),t)) < F(Dstate t) &
        P[Dstate(IExec(I(),t))];

theorem :: SCMPDS_8:13
   for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
 a be Int_position, i be Integer,X be set, f being Function of
 product the Object-Kind of SCMPDS,NAT st card I > 0 &
 ( for t be State of SCMPDS st f.Dstate(t)=0 holds t.DataLoc(s.a,i) >= 0 ) &
 (for t be State of SCMPDS st
    (for x be Int_position st x in X holds t.x=s.x) &
    t.a=s.a & t.DataLoc(s.a,i) < 0
   holds IExec(I,t).a=t.a & f.Dstate(IExec(I,t)) < f.Dstate(t) &
    I is_closed_on t & I is_halting_on t &
     for x be Int_position st x in X holds IExec(I,t).x=t.x)
 holds
     while<0(a,i,I) is_closed_on s & while<0(a,i,I) is_halting_on s;

theorem :: SCMPDS_8:14
   for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
 a be Int_position, i be Integer,X be set,f being Function of product the
 Object-Kind of SCMPDS,NAT st card I > 0 & s.DataLoc(s.a,i) < 0 &
 (for t be State of SCMPDS st f.Dstate(t)=0 holds t.DataLoc(s.a,i) >= 0 ) &
 (for t be State of SCMPDS st
    (for x be Int_position st x in X holds t.x=s.x) &
    t.a=s.a & t.DataLoc(s.a,i) < 0
   holds IExec(I,t).a=t.a & I is_closed_on t & I is_halting_on t &
    f.Dstate(IExec(I,t)) < f.Dstate(t) &
    for x be Int_position st x in X holds IExec(I,t).x=t.x)
 holds
    IExec(while<0(a,i,I),s) =IExec(while<0(a,i,I),IExec(I,s));

theorem :: SCMPDS_8:15
 for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
 a be Int_position, i be Integer,X be set st card I > 0 &
 (for t be State of SCMPDS st
   (for x be Int_position st x in X holds t.x=s.x) &
   t.a=s.a & t.DataLoc(s.a,i) < 0
 holds IExec(I,t).a=t.a & IExec(I,t).DataLoc(s.a,i) > t.DataLoc(s.a,i) &
   I is_closed_on t & I is_halting_on t &
  for x be Int_position st x in X holds IExec(I,t).x=t.x)
 holds
     while<0(a,i,I) is_closed_on s & while<0(a,i,I) is_halting_on s;

theorem :: SCMPDS_8:16
   for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
 a be Int_position,i be Integer,X be set st
  s.DataLoc(s.a,i) < 0 & card I > 0 &
  (for t be State of SCMPDS st
    (for x be Int_position st x in X holds t.x=s.x) &
    t.a=s.a & t.DataLoc(s.a,i) < 0
   holds IExec(I,t).a=t.a & IExec(I,t).DataLoc(s.a,i) > t.DataLoc(s.a,i) &
    I is_closed_on t & I is_halting_on t &
    for x be Int_position st x in X holds IExec(I,t).x=t.x)
 holds
   IExec(while<0(a,i,I),s) =IExec(while<0(a,i,I),IExec(I,s));

begin :: The construction and basic properties of while>0 program
:: while (a,i)>0 do I
definition
 let a be Int_position, i be Integer,I be Program-block;
 func while>0(a,i,I) -> Program-block equals
:: SCMPDS_8:def 3
   (a,i)<=0_goto (card I +2) ';' I ';' goto -(card I+1);
end;

definition
   let I be shiftable Program-block,a be Int_position,i be Integer;
   cluster while>0(a,i,I) -> shiftable;
end;

definition
   let I be No-StopCode Program-block,a be Int_position,i be Integer;
   cluster while>0(a,i,I) -> No-StopCode;
end;

theorem :: SCMPDS_8:17
 for a be Int_position,i be Integer,I be Program-block holds
  card while>0(a,i,I)= card I +2;

theorem :: SCMPDS_8:18
 for a be Int_position,i be Integer,m be Nat,I be Program-block holds
   m < card I+2 iff inspos m in dom while>0(a,i,I);

theorem :: SCMPDS_8:19
 for a be Int_position,i be Integer,I be Program-block holds
    while>0(a,i,I).inspos 0=(a,i)<=0_goto (card I +2) &
    while>0(a,i,I).inspos (card I+1)=goto -(card I+1);

theorem :: SCMPDS_8:20
 for s being State of SCMPDS,I being Program-block,a being Int_position,
 i being Integer st s.DataLoc(s.a,i) <= 0 holds
 while>0(a,i,I) is_closed_on s & while>0(a,i,I) is_halting_on s;

theorem :: SCMPDS_8:21
 for s being State of SCMPDS,I being Program-block,a,c being Int_position,
 i being Integer st s.DataLoc(s.a,i) <= 0 holds
 IExec(while>0(a,i,I),s) = s +* Start-At inspos (card I + 2);

theorem :: SCMPDS_8:22
   for s being State of SCMPDS,I being Program-block,a being Int_position,
 i being Integer st s.DataLoc(s.a,i) <= 0 holds
    IC IExec(while>0(a,i,I),s) = inspos (card I + 2);

theorem :: SCMPDS_8:23
   for s being State of SCMPDS,I being Program-block,a,b being Int_position,
 i being Integer st s.DataLoc(s.a,i) <= 0 holds
   IExec(while>0(a,i,I),s).b = s.b;

scheme WhileGHalt { F(State of SCMPDS)-> Nat,
 s() -> State of SCMPDS,I() -> No-StopCode shiftable Program-block,
 a() -> Int_position,i() -> Integer,P[State of SCMPDS]}:
   (F(s())=F(s()) or P[s()]) &
   while>0(a(),i(),I()) is_closed_on s() &
   while>0(a(),i(),I()) is_halting_on s()
provided
 card I() > 0 and
 (for t be State of SCMPDS st P[Dstate t] & F(Dstate(t))=0 holds
    t.DataLoc(s().a(),i()) <= 0) and
 P[Dstate s()] and
 for t be State of SCMPDS st
       P[Dstate t] & t.a()=s().a() & t.DataLoc(s().a(),i()) > 0
    holds IExec(I(),t).a()=t.a() & I() is_closed_on t &
        I() is_halting_on t & F(Dstate IExec(I(),t)) < F(Dstate t) &
        P[Dstate(IExec(I(),t))];

scheme WhileGExec { F(State of SCMPDS)-> Nat,
 s() -> State of SCMPDS,I() -> No-StopCode shiftable Program-block,
 a() -> Int_position,i() -> Integer,P[State of SCMPDS]}:
   (F(s())=F(s()) or P[s()]) &
   IExec(while>0(a(),i(),I()),s()) =
    IExec(while>0(a(),i(),I()),IExec(I(),s()))
provided
 card I() > 0 and
 s().DataLoc(s().a(),i()) > 0 and
 (for t be State of SCMPDS st P[Dstate t] & F(Dstate(t))=0 holds
    t.DataLoc(s().a(),i()) <= 0) and
 P[Dstate s()] and
 for t be State of SCMPDS st
       P[Dstate t] & t.a()=s().a() & t.DataLoc(s().a(),i()) > 0
    holds IExec(I(),t).a()=t.a() & I() is_closed_on t &
        I() is_halting_on t & F(Dstate IExec(I(),t)) < F(Dstate t) &
        P[Dstate(IExec(I(),t))];

theorem :: SCMPDS_8:24
 for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
 a be Int_position,i,c be Integer,X,Y be set, f being Function of
 product the Object-Kind of SCMPDS,NAT st card I > 0 &
 ( for t be State of SCMPDS st f.Dstate(t)=0 holds t.DataLoc(s.a,i) <= 0 ) &
  (for x st x in X holds s.x >= c+s.DataLoc(s.a,i)) &
  (for t be State of SCMPDS st
    (for x st x in X holds t.x >= c+t.DataLoc(s.a,i)) &
    (for x st x in Y holds t.x=s.x) & t.a=s.a & t.DataLoc(s.a,i) > 0
   holds IExec(I,t).a=t.a & I is_closed_on t & I is_halting_on t &
    f.Dstate(IExec(I,t)) < f.Dstate(t) &
    (for x st x in X holds IExec(I,t).x >= c+IExec(I,t).DataLoc(s.a,i)) &
    for x st x in Y holds IExec(I,t).x=t.x)
holds
     while>0(a,i,I) is_closed_on s & while>0(a,i,I) is_halting_on s;

theorem :: SCMPDS_8:25
 for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
 a be Int_position, i,c be Integer,X,Y be set,f being Function of product
 the Object-Kind of SCMPDS,NAT st s.DataLoc(s.a,i) > 0 & card I > 0 &
 ( for t be State of SCMPDS st f.Dstate(t)=0 holds t.DataLoc(s.a,i) <= 0 ) &
 (for x st x in X holds s.x >= c+s.DataLoc(s.a,i)) &
 (for t be State of SCMPDS st
    (for x st x in X holds t.x >= c+t.DataLoc(s.a,i)) &
    (for x st x in Y holds t.x=s.x) & t.a=s.a & t.DataLoc(s.a,i) > 0
   holds IExec(I,t).a=t.a & I is_closed_on t & I is_halting_on t &
    f.Dstate(IExec(I,t)) < f.Dstate(t) &
    (for x st x in X holds IExec(I,t).x >= c+IExec(I,t).DataLoc(s.a,i)) &
    for x st x in Y holds IExec(I,t).x=t.x)
holds
   IExec(while>0(a,i,I),s) =IExec(while>0(a,i,I),IExec(I,s));

theorem :: SCMPDS_8:26
   for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
 a be Int_position, i be Integer,X be set, f being Function of
 product the Object-Kind of SCMPDS,NAT st card I > 0 &
 (for t be State of SCMPDS st f.Dstate(t)=0 holds t.DataLoc(s.a,i) <= 0 ) &
 (for t be State of SCMPDS st
    (for x st x in X holds t.x=s.x) & t.a=s.a & t.DataLoc(s.a,i) > 0
   holds IExec(I,t).a=t.a & I is_closed_on t & I is_halting_on t &
    f.Dstate(IExec(I,t)) < f.Dstate(t) &
    for x st x in X holds IExec(I,t).x=t.x)
 holds
    while>0(a,i,I) is_closed_on s & while>0(a,i,I) is_halting_on s &
    (s.DataLoc(s.a,i) > 0 implies
    IExec(while>0(a,i,I),s) =IExec(while>0(a,i,I),IExec(I,s)));

theorem :: SCMPDS_8:27
 for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
 a be Int_position, i,c be Integer,X,Y be set st
 card I > 0 & (for x st x in X holds s.x >= c+s.DataLoc(s.a,i)) &
 (for t be State of SCMPDS st
   (for x st x in X holds t.x >= c+t.DataLoc(s.a,i)) &
   (for x st x in Y holds t.x=s.x) & t.a=s.a & t.DataLoc(s.a,i) > 0
 holds IExec(I,t).a=t.a & I is_closed_on t & I is_halting_on t &
   IExec(I,t).DataLoc(s.a,i) < t.DataLoc(s.a,i) &
   (for x st x in X holds IExec(I,t).x >= c+IExec(I,t).DataLoc(s.a,i)) &
   for x st x in Y holds IExec(I,t).x=t.x)
holds
   while>0(a,i,I) is_closed_on s & while>0(a,i,I) is_halting_on s &
   ( s.DataLoc(s.a,i) > 0 implies
      IExec(while>0(a,i,I),s) =IExec(while>0(a,i,I),IExec(I,s)));

theorem :: SCMPDS_8:28
   for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
 a be Int_position, i be Integer,X be set st card I > 0 &
 (for t be State of SCMPDS st
    (for x st x in X holds t.x=s.x) & t.a=s.a & t.DataLoc(s.a,i) > 0
   holds IExec(I,t).a=t.a & I is_closed_on t & I is_halting_on t &
    IExec(I,t).DataLoc(s.a,i) < t.DataLoc(s.a,i) &
    for x st x in X holds IExec(I,t).x=t.x)
 holds
    while>0(a,i,I) is_closed_on s & while>0(a,i,I) is_halting_on s &
    (s.DataLoc(s.a,i) > 0 implies
     IExec(while>0(a,i,I),s) =IExec(while>0(a,i,I),IExec(I,s)));

theorem :: SCMPDS_8:29
   for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
 a be Int_position, i,c be Integer,X be set st card I > 0 &
  (for x st x in X holds s.x >= c+s.DataLoc(s.a,i)) &
  (for t be State of SCMPDS st
    (for x st x in X holds t.x >= c+t.DataLoc(s.a,i)) &
    t.a=s.a & t.DataLoc(s.a,i) > 0
  holds IExec(I,t).a=t.a & I is_closed_on t & I is_halting_on t &
    IExec(I,t).DataLoc(s.a,i) < t.DataLoc(s.a,i) &
    for x st x in X holds IExec(I,t).x >= c+IExec(I,t).DataLoc(s.a,i))
 holds
   while>0(a,i,I) is_closed_on s & while>0(a,i,I) is_halting_on s &
   (s.DataLoc(s.a,i) > 0 implies
     IExec(while>0(a,i,I),s) =IExec(while>0(a,i,I),IExec(I,s)));