The abstract of the Mizar article:

Insert Sort on SCMPDS

by

Jing-Chao Chen

Received June 14, 2000

MML identifier: SCPISORT

[ Mizar article, MML identifier index ]

environ

 vocabulary AMI_3, SCMPDS_2, AMI_1, SCMPDS_4, CARD_1, SCMFSA6A, FINSEQ_1,
      INT_1, FUNCT_1, SCMP_GCD, RFUNCT_2, RELAT_1, RFINSEQ, AMI_2, SCMPDS_8,
      SCMPDS_5, SCMFSA6B, UNIALG_2, SCMFSA7B, SCMFSA_7, SCMPDS_7, ARYTM_1,
      RELOC, FUNCT_4, SCMPDS_3, FUNCT_7, SCM_1, BOOLE, AMI_5, SCMISORT,
      SCMFSA_9, SCMFSA8B, ABSVALUE, SCPISORT;
 notation XBOOLE_0, XCMPLX_0, XREAL_0, RELAT_1, FUNCT_1, FUNCT_4, INT_1, NAT_1,
      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, DOMAIN_1, FINSEQ_1,
      SCMPDS_7, SCMPDS_8, ABSVALUE, SFMASTR3, RFINSEQ;
 constructors REAL_1, DOMAIN_1, AMI_5, SCMPDS_4, SCM_1, SCMPDS_5, SCMPDS_6,
      SCMP_GCD, SCMPDS_7, SCMPDS_8, SFMASTR3, RFINSEQ, NAT_1, MEMBERED, RAT_1;
 clusters AMI_1, INT_1, FUNCT_1, RELSET_1, SCMPDS_2, SCMFSA_4, SCMPDS_4,
      SCMPDS_5, SCMPDS_6, SCMPDS_7, SCMPDS_8, WSIERP_1, NAT_1, FRAENKEL,
      XREAL_0, MEMBERED;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;


begin :: Preliminaries

reserve x for Int_position,
        n,p0 for Nat;

definition
 let f be FinSequence of INT,s be State of SCMPDS,m be Nat;
 pred f is_FinSequence_on s,m means
:: SCPISORT:def 1
  for i be Nat st 1 <= i & i <= len f holds f.i=s.intpos(m+i);
end;

theorem :: SCPISORT:1
 for f being FinSequence of INT,m,n be Nat st m >= n holds
 f is_non_decreasing_on m,n;

theorem :: SCPISORT:2
  for s being State of SCMPDS,n,m be Nat holds
     ex f be FinSequence of INT st len f=n &
     for i be Nat st 1<=i & i <= len f holds f.i=s.intpos(m+i);

theorem :: SCPISORT:3
   for s being State of SCMPDS,n,m be Nat holds
    ex f be FinSequence of INT st len f=n & f is_FinSequence_on s,m;

theorem :: SCPISORT:4
 for f,g be FinSequence of INT,m,n be Nat st 1<=n & n <= len f &
 1<=m & m <= len f & len f=len g & f.m=g.n & f.n=g.m &
 (for k be Nat st k<>m & k<>n & 1<=k & k <= len f holds f.k=g.k)
 holds f,g are_fiberwise_equipotent;

theorem :: SCPISORT:5   ::see SCMPDS_8:2
 for s1,s2 being State of SCMPDS st
     (for a being Int_position holds s1.a = s2.a)
 holds Dstate(s1)=Dstate(s2);

theorem :: SCPISORT:6    :: see SCMPDS_7:50
 for s being State of SCMPDS, I being No-StopCode Program-block,
 j being parahalting shiftable Instruction of SCMPDS st
 I is_closed_on s & I is_halting_on s
 holds (I ';' j) is_closed_on s & (I ';' j) is_halting_on s;

theorem :: SCPISORT:7   :: see SCMPDS_7:49
   for s being State of SCMPDS, I being No-StopCode Program-block,
 J being shiftable parahalting Program-block,a be Int_position st
   I is_closed_on s & I is_halting_on s
 holds IExec(I ';' J, s).a = IExec(J,IExec(I,s)).a;

theorem :: SCPISORT:8   :: see SCMPDS_7:49
   for s being State of SCMPDS, I being No-StopCode parahalting Program-block,
 J being shiftable Program-block,a be Int_position st J is_closed_on
 IExec(I,s) & J is_halting_on IExec(I,s) holds
  IExec(I ';' J, s).a = IExec(J,IExec(I,s)).a;

theorem :: SCPISORT:9     :: SCMPDS_7:43
   for s being State of SCMPDS, I being Program-block,J being shiftable
 parahalting Program-block st I is_closed_on s & I is_halting_on s
 holds I ';' J is_closed_on s & I ';' J is_halting_on s;

theorem :: SCPISORT:10     :: SCMPDS_7:43
   for s being State of SCMPDS, I being parahalting Program-block,J being
 shiftable Program-block st J is_closed_on IExec(I,s) & J is_halting_on
 IExec(I,s) holds
     I ';' J is_closed_on s & I ';' J is_halting_on s;

theorem :: SCPISORT:11      :: SCMPDS_7:43
   for s being State of SCMPDS, I being Program-block, j being parahalting
 shiftable Instruction of SCMPDS st I is_closed_on s & I is_halting_on s
 holds I ';' j is_closed_on s & I ';' j is_halting_on s;

begin :: Computing the Execution Result of For-loop Program by Loop-Invariant

scheme ForDownHalt { P[set],
 s() -> State of SCMPDS,I() -> No-StopCode shiftable Program-block,
 a() -> Int_position,i() -> Integer,n() -> Nat}:
    (P[s()] or not P[s()]) &
     for-down(a(),i(),n(),I()) is_closed_on s() &
     for-down(a(),i(),n(),I()) is_halting_on s()
provided
 n() > 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() ';' AddTo(a(),i(),-n()),t).a()=t.a() &
        IExec(I() ';' AddTo(a(),i(),-n()),t).DataLoc(s().a(),i())
        =t.DataLoc(s().a(),i())-n() &
        I() is_closed_on t & I() is_halting_on t &
        P[Dstate(IExec(I() ';' AddTo(a(),i(),-n()),t))];

scheme ForDownExec { P[set],
 s() -> State of SCMPDS,I() -> No-StopCode shiftable Program-block,
 a() -> Int_position,i() -> Integer,n() -> Nat}:
    (P[s()] or not P[s()]) &
    IExec(for-down(a(),i(),n(),I()),s()) =
 IExec(for-down(a(),i(),n(),I()),IExec(I() ';' AddTo(a(),i(),-n()),s()))
provided
 n() > 0 and
 s().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() ';' AddTo(a(),i(),-n()),t).a()=t.a() &
        IExec(I() ';' AddTo(a(),i(),-n()),t).DataLoc(s().a(),i())
        =t.DataLoc(s().a(),i())-n() &
        I() is_closed_on t & I() is_halting_on t &
        P[Dstate(IExec(I() ';' AddTo(a(),i(),-n()),t))];

scheme ForDownEnd { P[set],
 s() -> State of SCMPDS,I() -> No-StopCode shiftable Program-block,
 a() -> Int_position,i() -> Integer,n() -> Nat}:
    (P[s()] or not P[s()]) &
    IExec(for-down(a(),i(),n(),I()),s()).DataLoc(s().a(),i()) <= 0 &
     P[Dstate IExec(for-down(a(),i(),n(),I()),s())]
provided
 n() > 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() ';' AddTo(a(),i(),-n()),t).a()=t.a() &
        IExec(I() ';' AddTo(a(),i(),-n()),t).DataLoc(s().a(),i())
        =t.DataLoc(s().a(),i())-n() &
        I() is_closed_on t & I() is_halting_on t &
        P[Dstate(IExec(I() ';' AddTo(a(),i(),-n()),t))];

theorem :: SCPISORT:12
 for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
 a,x,y be Int_position, i,c be Integer,n be Nat st
  n > 0 & s.x >= s.y +c &
 for t be State of SCMPDS st
   t.x >= t.y +c & t.a=s.a & t.DataLoc(s.a,i) > 0
 holds IExec(I ';' AddTo(a,i,-n),t).a=t.a &
    IExec(I ';' AddTo(a,i,-n),t).DataLoc(s.a,i)=t.DataLoc(s.a,i)-n &
    I is_closed_on t & I is_halting_on t &
    IExec(I ';' AddTo(a,i,-n),t).x>=IExec(I ';' AddTo(a,i,-n),t).y+c
holds
   for-down(a,i,n,I) is_closed_on s & for-down(a,i,n,I) is_halting_on s;

theorem :: SCPISORT:13
 for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
 a,x,y be Int_position, i,c be Integer,n be Nat st
  n > 0 & s.x >= s.y +c & s.DataLoc(s.a,i) > 0 &
 for t be State of SCMPDS st
   t.x >= t.y +c & t.a=s.a & t.DataLoc(s.a,i) > 0
 holds IExec(I ';' AddTo(a,i,-n),t).a=t.a &
    IExec(I ';' AddTo(a,i,-n),t).DataLoc(s.a,i)=t.DataLoc(s.a,i)-n &
    I is_closed_on t & I is_halting_on t &
    IExec(I ';' AddTo(a,i,-n),t).x>=IExec(I ';' AddTo(a,i,-n),t).y+c
holds
    IExec(for-down(a,i,n,I),s) =
    IExec(for-down(a,i,n,I),IExec(I ';' AddTo(a,i,-n),s));

theorem :: SCPISORT:14
   for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
 a be Int_position, i be Integer,n be Nat
 st s.DataLoc(s.a,i) > 0 & n > 0 & card I > 0 &
    a <> DataLoc(s.a,i) & (for t be State of SCMPDS st t.a=s.a
 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)
 holds
     for-down(a,i,n,I) is_closed_on s & for-down(a,i,n,I) is_halting_on s;

begin :: A Program for Insert Sort
:: n -> intpos 2,  x1 -> intpos 3
definition
 let n,p0 be Nat;
 func insert-sort(n,p0) -> Program-block equals
:: SCPISORT:def 2
       ((GBP:=0) ';'
       ((GBP,1):=0) ';'
       ((GBP,2):=(n-1)) ';'
       ((GBP,3):=p0)) ';'
       for-down(GBP,2,1,
          AddTo(GBP,3,1) ';'
          ((GBP,4):=(GBP,3)) ';'
          AddTo(GBP,1,1) ';'
          ((GBP,6):=(GBP,1)) ';'
          while>0(GBP,6,
            ((GBP,5):=(intpos 4,-1)) ';'
            SubFrom(GBP,5,intpos 4,0) ';'
            if>0(GBP,5,
              ((GBP,5):=(intpos 4,-1)) ';'
                ((intpos 4,-1):=(intpos 4,0)) ';'
                ((intpos 4,0 ):=(GBP,5)) ';'
                AddTo(GBP,4,-1) ';' AddTo(GBP,6,-1),
              Load ((GBP,6):=0)
            )
         )
      );
end;

begin :: The Property of Insert Sort and Its Correctness

theorem :: SCPISORT:15
     card insert-sort (n,p0) = 23;

theorem :: SCPISORT:16
    p0 >= 7 implies insert-sort (n,p0) is parahalting;

theorem :: SCPISORT:17
 for s being State of SCMPDS,f,g be FinSequence of INT,k0,k being Nat
 st s.a4 >= 7+s.a6 & s.GBP=0 & k=s.a6 & k0=s.a4-s.a6-1 &
  f is_FinSequence_on s,k0 &
  g is_FinSequence_on IExec(Insert_the_k1_item,s),k0 &
  len f=len g & len f > k & f is_non_decreasing_on 1,k
 holds
  f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,k+1 &
  (for i be Nat st i>k+1 & i <= len f holds f.i=g.i) &
  (for i be Nat st 1 <= i & i <= k+1 holds
    ex j be Nat st 1 <= j & j <= k+1 & g.i=f.j);

theorem :: SCPISORT:18
   for s being State of SCMPDS,f,g be FinSequence of INT,p0,n being Nat
 st p0 >= 6 & len f=n & len g = n & f is_FinSequence_on s,p0 &
    g is_FinSequence_on IExec(insert-sort(n,p0+1),s),p0 holds
    f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n;