:: Insert Sort on SCM+FSA
::  by JingChao Chen
::
:: Received March 13, 1999
:: Copyright (c) 1999-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, SCMFSA7B, AMI_1, SCMFSA_2, SCMFSA6A, CARD_1, SF_MASTR,
      AMI_3, EXTPRO_1, RELAT_1, FUNCT_1, FUNCT_4, FUNCOP_1, CARD_3, SUBSET_1,
      TARSKI, SCMFSA8B, TURING_1, ARYTM_3, XBOOLE_0, FSM_1, SCMFSA_9, SCMFSA6C,
      SCMFSA6B, CIRCUIT2, GRAPHSP, MSUALG_1, SCM_HALT, XXREAL_0, NAT_1,
      SCMFSA8C, FINSEQ_1, ARYTM_1, INT_1, COMPLEX1, PARTFUN1, CLASSES1,
      VALUED_0, SCMBSORT, STRUCT_0, SCMISORT, PBOOLE, COMPOS_1, MEMSTR_0,
      AMISTD_1;
 notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
      XCMPLX_0, FUNCOP_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4,
      FUNCT_7, FINSEQ_1, CARD_3, VALUED_1, PBOOLE, STRUCT_0, MEMSTR_0,
      COMPOS_0, COMPOS_1, EXTPRO_1, SCMFSA_2, SCMFSA6A, SF_MASTR, AMISTD_1,
      SCMFSA6B, SCMFSA6C, SCMFSA7B, SCMFSA_9, SCMFSA8B, INT_1, SCMBSORT,
      FINSUB_1, SCMFSA8C, CLASSES1, RFINSEQ, SCM_HALT, INT_2, NAT_1, XXREAL_0,
      SCMFSA_M, SCMFSA_X;
 constructors DOMAIN_1, SETWISEO, XXREAL_0, REAL_1, INT_2, MEMSTR_0, SCMFSA6A,
      SCMFSA6B, SCMFSA6C, SCMFSA8A, SCMFSA8B, SCMFSA8C, SCMFSA_9, SFMASTR1,
      SCM_HALT, SCMBSORT, CLASSES1, AMISTD_2, RELSET_1, PRE_POLY, PBOOLE,
      SCMFSA7B, AMISTD_1, SCMFSA_3, FUNCT_4, SCMFSA_1, SF_MASTR, SCMFSA_M,
      FUNCT_7, SCMFSA_X, COMPOS_2;
 registrations FUNCT_1, RELSET_1, FUNCOP_1, XREAL_0, NAT_1, INT_1, CARD_3,
      STRUCT_0, SCMFSA_2, SCMFSA8C, SCMFSA6C, SCMFSA8A, SCMFSA_9, SCM_HALT,
      VALUED_0, ORDINAL1, FINSET_1, FUNCT_4, MEMSTR_0, AMISTD_2, SCMFSA10,
      SCMFSA6A, COMPOS_1, SFMASTR1, EXTPRO_1, AMI_3, SCMFSA_M, SCMFSA9A,
      SCMFSA8B, SCMFSA_X, COMPOS_2;
 requirements BOOLE, REAL, NUMERALS, SUBSET, ARITHM;


begin :: Preliminaries

reserve s for State of SCM+FSA,
  I for MacroInstruction of SCM+FSA,
  a for read-write Int-Location;

reserve i,j,k,n for Nat;

reserve P,P1,P2,Q for Instruction-Sequence of SCM+FSA;

::$CT

theorem :: SCMISORT:2
  for s being State of SCM+FSA, I being Program of SCM+FSA st I
  is_halting_on Initialized s,P holds for a be Int-Location
   holds IExec(I,P,s).a =
    Comput(P +* I,(Initialize Initialized s),
      LifeSpan(P +* I,Initialize Initialized s)).a;

begin  :: -- Basic property of while Macro ---

::$CT 3

theorem :: SCMISORT:6
  for a being Int-Location,
  I being really-closed MacroInstruction of SCM+FSA,
       s being State of SCM+FSA,k being Nat
 st I is_halting_onInit s,P &
  k < LifeSpan(P +* I,Initialized s) &
 IC Comput(P +* while>0(a,I), Initialized s,1 + k)
  = IC Comput(P +* I, Initialized s,k) + 3 &
 DataPart Comput(P +* while>0(a,I), Initialized s,1 + k)
 = DataPart Comput(P +* I, Initialized s,k)
 holds IC Comput(P +* while>0(a,I), Initialized s,1 + k+1)
  = IC Comput(P +* I, Initialized s,k+1) + 3 &
  DataPart Comput(P +* while>0(a,I), Initialized s,1 + k+1)
 = DataPart Comput(P +* I, Initialized s,k+1);

theorem :: SCMISORT:7
  for a being Int-Location, I being really-closed MacroInstruction of SCM+FSA,
      s being State of SCM+FSA st
  I is_halting_onInit s,P &
 IC Comput(P +* while>0(a,I), Initialized s,1 + LifeSpan(P +* I,Initialized s))
  = IC Comput(P +* I, Initialized s, LifeSpan(P +* I,Initialized s)) + 3
   holds CurInstr(P +* while>0(a,I),
    Comput(P +* while>0(a,I),Initialized s,1 + LifeSpan(P +* I,Initialized s)))
  = goto 0;

theorem :: SCMISORT:8
  for s being State of SCM+FSA,
      I being really-closed MacroInstruction of SCM+FSA,
      a being read-write Int-Location st I is_halting_onInit s,P & s.a >0 holds
   IC Comput(P +* while>0(a,I),Initialized s,
    LifeSpan(P +* I,Initialized s) + 2) =  0 &
for k being Nat
 st k <= LifeSpan(P +* I,Initialized s) + 2
 holds IC Comput(P +* while>0(a,I),Initialized s,k) in dom while>0(a,I);

theorem :: SCMISORT:9 ::SCM_9_36
  for s being State of SCM+FSA,
      I being really-closed MacroInstruction of SCM+FSA,
      a be read-write Int-Location
   st I is_halting_onInit s,P & s.a >  0
  for k being Nat st
   k <= LifeSpan(P +* I,Initialized s) + 2
  holds IC Comput(P +* while>0(a,I), Initialized s,k) in dom while>0(a,I);

::$CT

theorem :: SCMISORT:11
  for s be State of SCM+FSA,
      I be InitHalting really-closed MacroInstruction of SCM+FSA,
      a be read-write Int-Location st s.a > 0
   ex s2 be State of SCM+FSA, k be  Nat st s2 = Initialized s &
   k =LifeSpan(P +* I,Initialized s) + 2 &
   IC Comput(P +* while>0(a,I), s2,k) =  0 &
    (for b be Int-Location
  holds Comput(P +* while>0(a,I), s2,k).b = IExec(I,P,s).b) &
   for f be FinSeq-Location holds
    Comput(P +* while>0(a,I), s2,k).f = IExec(I,P,s).f;

definition
  let s,I,a,P;
  func StepWhile>0(a,P,s,I) -> sequence of product the_Values_of
  SCM+FSA means
:: SCMISORT:def 1

  it.0 = s &
   for i being Nat
    holds it.(i+1)
    = Comput(P +* while>0(a,I), Initialized it.i,
     LifeSpan(P +* while>0(a,I) +* I,Initialized it.i) + 2);
end;

theorem :: SCMISORT:12
  StepWhile>0(a,P,s,I).(k+1) =StepWhile>0(a,P,StepWhile>0(a,P,s,I).k,I).1;

theorem :: SCMISORT:13
  for I being MacroInstruction of SCM+FSA,a being read-write Int-Location,
  s being State of SCM+FSA holds StepWhile>0(a,P,s,I).(0+1)
  = Comput(P +* while>0(a,I), Initialized s,
   LifeSpan(P +* while>0(a,I) +* I,Initialized s) + 2);

theorem :: SCMISORT:14
  for I be MacroInstruction of SCM+FSA,a be read-write Int-Location, s be
  State of SCM+FSA,k,n be Nat st
   IC StepWhile>0(a,P,s,I).k = 0 &
   StepWhile>0(a,P,s,I).k
    = Comput(P +* while>0(a,I),Initialized s,n) &
    StepWhile>0(a,P,s,I).k.intloc 0=1
  holds
   StepWhile>0(a,P,s,I).k
    = Initialized StepWhile>0(a,P,s,I).k &
   StepWhile>0(a,P,s,I).(k+1)
    = Comput(P +* while>0(a,I), Initialized s,
           n +(LifeSpan(P +* while>0(a,I) +* I,
       Initialized StepWhile>0(a,P,s,I).k) + 2));

theorem :: SCMISORT:15
  for I be really-closed MacroInstruction of SCM+FSA,
      a be read-write Int-Location, s be State
of SCM+FSA st ex f being Function of product the_Values_of SCM+FSA,NAT st
  (for k being Nat holds ( f.(StepWhile>0(a,P,s,I).k) <> 0
   implies f.(StepWhile>0(a,P,s,I).(k+1)) < f.(StepWhile>0(a,P,s,I).k) &
  I is_halting_onInit StepWhile>0(a,P,s,I).k,P+*while>0(a,I)) &
  (StepWhile>0(a,P,s,I).(k+1)).intloc 0=1 &
   ( f.(StepWhile>0(a,P,s,I).k)=0 iff (StepWhile>0(a,P,s,I).k).a <= 0 ) )
    holds while>0(a,I) is_halting_onInit s,P;

::$CT

theorem :: SCMISORT:17
  for I be good InitHalting really-closed MacroInstruction of SCM+FSA,
      a be read-write
Int-Location st (for s be State of SCM+FSA,P holds IExec(I,P,s).a < s.a or
IExec(I,P,s).a <= 0) holds while>0(a,I) is InitHalting;

theorem :: SCMISORT:18
  for I be good InitHalting really-closed MacroInstruction of SCM+FSA,
      a be read-write
Int-Location st ex f being Function of (product the_Values_of SCM+FSA),INT
st (for s,t be State of SCM+FSA,P
 holds (f.s > 0 implies f.IExec(I,P,s) < f.s ) &
  (DataPart s = DataPart t implies f.s=f.t) & ( f.s <= 0 iff s.a <= 0 ) ) holds
  while>0(a,I) is InitHalting;

theorem :: SCMISORT:19
  for s be State of SCM+FSA, I be MacroInstruction of SCM+FSA, a be
  read-write Int-Location st s.a <= 0
   holds DataPart IExec(while>0(a,I),P,s) =
  DataPart Initialized s;

::$CT

theorem :: SCMISORT:21
  for s be State of SCM+FSA, I be MacroInstruction of SCM+FSA, f be
FinSeq-Location,a be read-write Int-Location st s.a <= 0
 holds IExec(while>0(a,I),P,s).f=s.f;

theorem :: SCMISORT:22
  for s be State of SCM+FSA, I be MacroInstruction of SCM+FSA, b be
Int-Location,a be read-write Int-Location st s.a <= 0
 holds IExec(while>0(a,I),P,s).b=(Initialized s).b;

theorem :: SCMISORT:23
  for s be State of SCM+FSA,
      I be good InitHalting really-closed MacroInstruction of
SCM+FSA, f be FinSeq-Location,a be read-write Int-Location st s.a > 0 & while>0
(a,I) is InitHalting
 holds IExec(while>0(a,I),P,s).f =IExec(while>0(a,I),P,IExec(I,P,
  s)).f;

theorem :: SCMISORT:24
  for s be State of SCM+FSA,
      I be good InitHalting really-closed MacroInstruction of
SCM+FSA, b be Int-Location,a be read-write Int-Location st s.a > 0 & while>0(a,
I) is InitHalting holds IExec(while>0(a,I),P,s).b
 =IExec(while>0(a,I),P,IExec(I,P,s))
  .b;

begin

definition
  let f be FinSeq-Location;
  func insert-sort f -> Program of SCM+FSA equals
:: SCMISORT:def 2
   (((intloc 2):= intloc 0) ";"
    ((intloc 3):= intloc 0) ";"
    ((intloc 4):= intloc 0) ";"
    ((intloc 5):= intloc 0) ";"
    ((intloc 6):= intloc 0)) ";"
    ((intloc 1):=len f) ";"
    SubFrom(intloc 1,intloc 0) ";"
    Times(intloc 1, (((intloc 2):=len f) ";"
    SubFrom(intloc 2,intloc 1) ";"
    ((intloc 3) := intloc 2) ";"
    AddTo(intloc 3,intloc 0) ";"
    ((intloc 6):=(f,intloc 3)) ";"
    SubFrom(intloc 4,intloc 4)) ";"
    while>0(intloc 2, ((intloc 5):=(f,intloc 2)) ";"
    SubFrom(intloc 5,intloc 6) ";"
    if>0(intloc 5, Macro SubFrom(intloc 2,intloc 2),
    AddTo(intloc 4,intloc 0) ";"
    SubFrom(intloc 2,intloc 0)) ) ";"
    Times(intloc 4, ((intloc 2):=intloc 3) ";"
    SubFrom(intloc 3,intloc 0) ";"
    ((intloc 5):=(f,intloc 2)) ";"
    ((intloc 6):=(f,intloc 3)) ";"
    ((f,intloc 2):= intloc 6) ";"
    ((f,intloc 3):=intloc 5) ) );
end;

definition
  func Insert-Sort-Algorithm -> Program of SCM+FSA equals
:: SCMISORT:def 3
  insert-sort fsloc 0;
end;

theorem :: SCMISORT:25
  for f being FinSeq-Location holds UsedILoc (insert-sort f) = {
  intloc 0,intloc 1,intloc 2,intloc 3,intloc 4,intloc 5,intloc 6};

theorem :: SCMISORT:26
  for f being FinSeq-Location holds UsedI*Loc (insert-sort f) = {f};

theorem :: SCMISORT:27
  for k1,k2,k3,k4 being Instruction of SCM+FSA holds card( k1 ";"
  k2 ";" k3 ";" k4) =8;

theorem :: SCMISORT:28
  for k1,k2,k3,k4,k5 being Instruction of SCM+FSA holds card( k1
  ";" k2 ";" k3 ";" k4 ";"k5) =10;

theorem :: SCMISORT:29
  for f being FinSeq-Location holds card insert-sort f = 71;

theorem :: SCMISORT:30
  for f being FinSeq-Location, k being Nat st k < 71
  holds  k in dom (insert-sort f);

theorem :: SCMISORT:31
  insert-sort (fsloc 0) is keepInt0_1 InitHalting;

theorem :: SCMISORT:32
  for s be State of SCM+FSA
   holds s.(fsloc 0), IExec(insert-sort (fsloc 0),P,s).(fsloc 0)
    are_fiberwise_equipotent &
 for i,j be Nat st i >=1 & j<=len (s.(fsloc 0)) & i<j
 for x1,x2 be Integer st x1 =IExec(insert-sort (fsloc 0),P,s).(fsloc 0).i &
     x2=IExec(insert-sort (fsloc 0),P,s).(fsloc 0).j
  holds x1 >= x2;

theorem :: SCMISORT:33
  for i being Nat, s being State of SCM+FSA,
  P being Instruction-Sequence of SCM+FSA
   st Insert-Sort-Algorithm c= P
  for w being FinSequence of INT
  st (Initialized ((fsloc 0) .--> w)) c= s
  holds IC Comput(P,s,i) in dom Insert-Sort-Algorithm;

theorem :: SCMISORT:34
  for s be State of SCM+FSA,t be FinSequence of INT, P st
  Initialize((intloc 0).-->1) +*(fsloc 0 .--> t) c= s &
  Insert-Sort-Algorithm c= P
   ex u being FinSequence of
  REAL st t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence
  of INT & (Result(P,s)).(fsloc 0) = u;

theorem :: SCMISORT:35
  for w being FinSequence of INT holds Initialized
   ((fsloc 0) .--> w) is Insert-Sort-Algorithm-autonomic;

registration
 cluster Insert-Sort-Algorithm -> non halt-free;
end;

theorem :: SCMISORT:36
  Insert-Sort-Algorithm, Initialize((intloc 0).-->1)
     computes Sorting-Function;