:: Another { \bf times } Macro Instruction
::  by Piotr Rudnicki
::
:: Received June 4, 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, FSM_1, SCMFSA_2, SF_MASTR, AMI_1, SCMFSA7B, SUBSET_1,
      XBOOLE_0, CARD_1, SCMFSA6B, FUNCT_1, FUNCT_4, SCMFSA6A, TARSKI, RELAT_1,
      ARYTM_3, GRAPHSP, MSUALG_1, SFMASTR1, SCMFSA_9, AMI_3, CARD_3, XXREAL_0,
      ARYTM_1, SCMFSA9A, COMPLEX1, SFMASTR2, NAT_1, EXTPRO_1, SCMFSA6C,
      COMPOS_1, MEMSTR_0, AMISTD_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, INT_2,
      XXREAL_0, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4, PBOOLE, CARD_3, FUNCOP_1,
      STRUCT_0, MEMSTR_0, AMISTD_1, COMPOS_1, EXTPRO_1, SCMFSA_2, SCMFSA6A,
      SCMFSA6B, SF_MASTR, SCMFSA6C, SCMFSA7B, SCMFSA_9, SFMASTR1, SCMFSA9A,
      NAT_1, SCMFSA_M, SCMFSA_X;
 constructors XXREAL_0, INT_2, PRE_FF, SCMFSA6A, SCMFSA6B, SCMFSA6C, SCMFSA_9,
      SFMASTR1, SCMFSA9A, RELSET_1, PRE_POLY, PBOOLE, SCMFSA8A, SCMFSA7B,
      AMISTD_2, AMISTD_1, SCMFSA_7, FUNCT_4, MEMSTR_0, SCMFSA_1, SCMFSA_M,
      SF_MASTR, SCMFSA_X, COMPOS_2;
 registrations FUNCT_1, ORDINAL1, RELSET_1, FINSET_1, XXREAL_0, XREAL_0, NAT_1,
      INT_1, CARD_3, SCMFSA_2, SF_MASTR, SCMFSA6C, SCMFSA_9, SFMASTR1,
      COMPOS_1, FUNCT_4, MEMSTR_0, AMI_3, SCMFSA_M, SCMFSA6A, SCMFSA8C,
      SCMFSA10, SCMFSA_X, COMPOS_2;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;


begin :: SCM+FSA preliminaries

reserve s, s1, s2 for State of SCM+FSA,
  p, p1 for Instruction-Sequence of SCM+FSA,
  a, b for Int-Location,
  d for read-write Int-Location,
  f for FinSeq-Location,
  I for MacroInstruction of SCM+FSA,
  J for good MacroInstruction of SCM+FSA,
  k, m for Nat;

theorem :: SFMASTR2:1
  for I being really-closed Program of SCM+FSA holds
I is_halting_on Initialized s,p & not
  b in UsedILoc I implies IExec(I,p,s).b = (Initialized s).b;

theorem :: SFMASTR2:2
  for I being really-closed Program of SCM+FSA holds
I is_halting_on Initialized s,p & not f in
  UsedI*Loc I implies IExec(I,p,s).f = (Initialized s).f;

theorem :: SFMASTR2:3
  for I being really-closed Program of SCM+FSA holds
  (I is_halting_on Initialized s,p or I is parahalting ) &
  (s.intloc 0 = 1 or a is read-write) & not a in UsedILoc I
  implies IExec(I,p,s).a = s.a;

::$CT 2

begin :: Another times macro instruction

definition
  let a be Int-Location, I be MacroInstruction of SCM+FSA;
  func times*(a, I) -> MacroInstruction of SCM+FSA equals
:: SFMASTR2:def 1
  while>0 ( 1-stRWNotIn ({a} \/ UsedILoc I),
      I ";" SubFrom(1-stRWNotIn ({a} \/ UsedILoc I), intloc 0) );
end;

definition
  let a be Int-Location, I be MacroInstruction of SCM+FSA;
  func times(a, I) -> MacroInstruction of SCM+FSA equals
:: SFMASTR2:def 2
  (1-stRWNotIn ({a} \/ UsedILoc I)) := a ";" times*(a, I);
end;

registration
  let a be Int-Location, I be really-closed MacroInstruction of SCM+FSA;
  cluster times*(a,I) -> really-closed;
end;

registration
  let a be Int-Location, I be really-closed MacroInstruction of SCM+FSA;
  cluster times(a,I) -> really-closed;
end;

::$CT 2

theorem :: SFMASTR2:8
  {b} \/ UsedILoc I c= UsedILoc times(b, I);

theorem :: SFMASTR2:9
  UsedI*Loc times(b, I) = UsedI*Loc I;

registration
  let I be good MacroInstruction of SCM+FSA, a be Int-Location;
  cluster times(a, I) -> good;
end;

definition let p;
  let s be State of SCM+FSA, I be MacroInstruction of SCM+FSA,
      a be Int-Location;
  func StepTimes(a, I, p, s) ->
   sequence of  product the_Values_of SCM+FSA equals
:: SFMASTR2:def 3
  StepWhile>0(1-stRWNotIn ({a} \/ UsedILoc I),
    I ";" SubFrom(1-stRWNotIn ({a} \/ UsedILoc I), intloc 0), p,
  Exec(1-stRWNotIn ({a} \/ UsedILoc I) := a, Initialized s));
end;

theorem :: SFMASTR2:10
  StepTimes(a,J,p,s).0.intloc 0 = 1;

theorem :: SFMASTR2:11
  s.intloc 0 = 1 or a is read-write implies StepTimes(a,J,p,s).0.(
  1-stRWNotIn ({a} \/ UsedILoc J)) = s.a;

theorem :: SFMASTR2:12
 for J being good really-closed MacroInstruction of SCM+FSA holds
  StepTimes(a,J,p,s).k.intloc 0 = 1 &
  J is_halting_on StepTimes(a,J,p,s).k, p+*times*(a,J) implies
   StepTimes(a,J,p,s).(k+1).intloc 0 = 1 &
  (StepTimes(a,J,p,s).k.(1-stRWNotIn ({a} \/ UsedILoc J)) > 0
  implies StepTimes(a,J,p,s).(k+1).(1-stRWNotIn ({a} \/ UsedILoc J)) =
  StepTimes(a,J,p,s).k.(1-stRWNotIn ({a} \/ UsedILoc J)) - 1);

theorem :: SFMASTR2:13
  s.intloc 0 = 1 or a is read-write implies StepTimes(a,I,p,s).0.a
  = s.a;

theorem :: SFMASTR2:14
  StepTimes(a,I,p,s).0.f = s.f;

definition let p;
  let s be State of SCM+FSA, a be Int-Location,
      I be MacroInstruction of SCM+FSA;
  pred ProperTimesBody a, I, s, p means
:: SFMASTR2:def 4
  for k being Nat st k < s.a
   holds I is_halting_on StepTimes(a,I,p,s).k,p+*times*(a,I);
end;

theorem :: SFMASTR2:15
  I is parahalting implies ProperTimesBody a,I,s,p;

theorem :: SFMASTR2:16
 for J being good really-closed MacroInstruction of SCM+FSA holds
  ProperTimesBody a,J,s,p implies for k st k <= s.a holds
  StepTimes(a,J,p,s).k.intloc 0 = 1;

theorem :: SFMASTR2:17
 for J being good really-closed MacroInstruction of SCM+FSA holds
  (s.intloc 0 = 1 or a is read-write) & ProperTimesBody a,J,s,p
  implies for k st k <= s.a holds StepTimes(a,J,p,s).k.(1-stRWNotIn({a} \/
  UsedILoc J))+k = s.a;

theorem :: SFMASTR2:18
 for J being good really-closed MacroInstruction of SCM+FSA holds
  ProperTimesBody a,J,s,p & 0 <= s.a & (s.intloc 0 = 1 or a is
read-write) implies
 for k st k >= s.a holds StepTimes(a,J,p,s).k.(1-stRWNotIn({
  a} \/ UsedILoc J)) = 0 & StepTimes(a,J,p,s).k.intloc 0 = 1;

theorem :: SFMASTR2:19
  s.intloc 0 = 1 implies StepTimes(a,I,p,s).0 | ((UsedILoc I) \/
  FinSeq-Locations) = s | ((UsedILoc I) \/ FinSeq-Locations);

theorem :: SFMASTR2:20
 for J being good really-closed MacroInstruction of SCM+FSA holds
  StepTimes(a,J,p,s).k.intloc 0 = 1 &
  J is_halting_on Initialized StepTimes(a,J,p,s).k,p+*times*(a,J) &
StepTimes(a,J,p,s).k.(1-stRWNotIn ({a} \/ UsedILoc J)) > 0
 implies StepTimes(a,J,p,s).(k+1) | ((UsedILoc J) \/ FinSeq-Locations)
  = IExec(J,p+*times*(a,J),StepTimes(a,J,p,s).k)
       | ((UsedILoc J) \/ FinSeq-Locations);

theorem :: SFMASTR2:21
 for J being good really-closed MacroInstruction of SCM+FSA holds
  (ProperTimesBody a,J,s,p or J is parahalting) & k < s.a & (s.
  intloc 0 = 1 or a is read-write) implies StepTimes(a,J,p,s).(k+1) | ((
  UsedILoc J) \/ FinSeq-Locations)
   = IExec(J,p+*times*(a,J),StepTimes(a,J,p,s).k) | ((
  UsedILoc J) \/ FinSeq-Locations);

theorem :: SFMASTR2:22
 for I being really-closed MacroInstruction of SCM+FSA holds
  s.a <= 0 & s.intloc 0 = 1 implies IExec(times(a, I),p,s) | ((UsedILoc
  I) \/ FinSeq-Locations) = s | ((UsedILoc I) \/ FinSeq-Locations);

theorem :: SFMASTR2:23
 for J being good really-closed MacroInstruction of SCM+FSA holds
  s.a = k & (ProperTimesBody a,J,s,p or J is parahalting) & (s.
  intloc 0 = 1 or a is read-write) implies
   DataPart IExec(times(a,J),p,s) =
  DataPart StepTimes(a,J,p,s).k;

theorem :: SFMASTR2:24
 for J being good really-closed MacroInstruction of SCM+FSA holds
  s.intloc 0 = 1 & (ProperTimesBody a,J,s,p or J is parahalting)
  implies times(a, J) is_halting_on s,p;

begin  :: A trivial example

definition
  let d be read-write Int-Location;
  func triv-times(d) -> MacroInstruction of SCM+FSA equals
:: SFMASTR2:def 5
  times( d, while=0(d, Macro(d:= d)) ";" SubFrom(d, intloc 0) );
end;

registration
  let d be read-write Int-Location;
  cluster triv-times d -> really-closed;
end;

theorem :: SFMASTR2:25
  s.d <= 0 implies IExec(triv-times(d),p,s).d = s.d;

theorem :: SFMASTR2:26
  0 <= s.d implies IExec(triv-times(d),p,s).d = 0;

:: begin  :: A macro for the Fibonacci sequence

:: definition
::   let N, result be Int-Location;
::   func Fib-macro (N, result) -> Program of SCM+FSA equals
::   (1-stNotUsed times(N
::   , AddTo(result, (1-stRWNotIn {N, result}))";" swap(result, 1-stRWNotIn {N,
:: result}))) := N ";" (SubFrom(result, result)) ";" ((1-stRWNotIn {N, result}) :=
:: intloc 0) ";" times(N, AddTo(result, (1-stRWNotIn {N, result})) ";" swap(result
:: , (1-stRWNotIn {N, result})) ) ";" (N := (1-stNotUsed
:: times(N, AddTo(result, 1
::   -stRWNotIn {N, result})";"
::  swap(result, 1-stRWNotIn {N, result})
::   qua MacroInstruction of SCM+FSA
::   )
:: ));
::   correctness;
:: end;

:: registration
::   let N, result be Int-Location;
::   cluster Fib-macro (N, result) -> really-closed;
::   coherence;
:: end;

:: theorem
::   for N, result being read-write Int-Location st N <> result for n being
:: Element of NAT st n = s.N holds IExec(Fib-macro(N,result),p,s).result = Fib n &
::   IExec(Fib-macro(N,result),p,s).N = s.N
:: proof
::   let N, result be read-write Int-Location such that
:: A1: N <> result;
::   let n be Element of NAT;
::   set i1 = SubFrom(result, result);
::   set next = 1-stRWNotIn {N, result};
::   set Nsave = 1-stNotUsed times(N, AddTo(result, next)";"swap(result, next));
::   set i0 = Nsave := N;
::   set i2 = next := intloc 0;
::   set i30 = AddTo (result, next);
::   set I31 = swap(result, next);
::   set I301 = i30 ";" I31;
::   set i02 = i0 ";" i1 ";" i2;
::   set s1 = IExec(i02,p,s);
::   set I3 = times( N, I301 );
::   set ST = StepTimes(N, I301,p,s1);
::   assume
:: A2: n = s.N;
:: A3: not next in {N, result} by SCMFSA_M:25;
::   then
:: A4: next <> N by TARSKI:def 2;
:: A5: {N} \/ UsedILoc I301 c= UsedILoc I3 by Th6;
:: A6: Nsave = 1-stRWNotIn UsedILoc I3 by SFMASTR1:def 4;
::   then
:: A7: not Nsave in UsedILoc I3 by SCMFSA_M:25;
::   N in {N} by TARSKI:def 1;
::   then N in {N} \/ UsedILoc I301 by XBOOLE_0:def 3;
::   then
:: A8: Nsave <> N by A6,A5,SCMFSA_M:25;
:: A9: s1.N = Exec(i2, IExec(i0 ";" i1,p,s)).N by SCMFSA6C:6
::     .= IExec(i0 ";" i1,p,s).N by A4,SCMFSA_2:63
::     .= Exec(i1, Exec(i0, Initialized s)).N by SCMFSA6C:8
::     .= Exec(i0, Initialized s).N by A1,SCMFSA_2:65
::     .= (Initialized s).N by A8,SCMFSA_2:63
::     .= s.N by SCMFSA_M:37;
::   then
:: A10: DataPart IExec(I3,p,s1) = DataPart ST.n by A2,Th21;
::   defpred P[Nat] means $1 <= s1.N implies ST.$1.result = Fib $1 &
::   ST.$1.next = Fib ($1+1);
::   set UIFS = UsedILoc I301 \/ FinSeq-Locations;
::   set i4 = N := Nsave;
:: A11: UsedILoc I301 = (UsedIntLoc i30) \/ UsedILoc I31 by SF_MASTR:29
::     .= {result, next} \/ UsedILoc I31 by SF_MASTR:14;
::   next in {result, next} by TARSKI:def 2;
::   then
:: A12: next in UsedILoc I301 by A11,XBOOLE_0:def 3;
::   then next in {N} \/ UsedILoc I301 by XBOOLE_0:def 3;
::   then
:: A13: Nsave <> next by A6,A5,SCMFSA_M:25;
::   result in {result, next} by TARSKI:def 2;
::   then
:: A14: result in UsedILoc I301 by A11,XBOOLE_0:def 3;
::   then result in {N} \/ UsedILoc I301 by XBOOLE_0:def 3;
::   then
:: A15: Nsave <> result by A6,A5,SCMFSA_M:25;
:: A16: next <> result by A3,TARSKI:def 2;
:: A17: now
::     let k be Nat such that
:: A18: P[k];
::     thus P[k+1]
::     proof
:: A19:  k < k+1 by NAT_1:13;
::       assume
:: A20:  k+1 <= s1.N;
::       then k < s1.N by A19,XXREAL_0:2;
::       then
:: A21:  ST.(k+1) | UIFS = IExec(I301,p+*times*(N,I301),ST.k) | UIFS by Th19;
::       hence ST.(k+1).result = IExec(I301,p+*times*(N,I301),ST.k).result
::               by A14,SCMFSA_M:28
::         .= IExec(I31,p+*times*(N,I301),Exec(i30, Initialized ST.k)).result
::               by SCMFSA8B:9
::         .= Exec(i30, Initialized ST.k).next by SCMFSA6C:10
::         .= (Initialized ST.k).next by A16,SCMFSA_2:64
::         .= Fib (k+1) by A18,A20,A19,SCMFSA_M:37,XXREAL_0:2;
::       thus ST.(k+1).next
::           = IExec(I301,p+*times*(N,I301),ST.k).next by A12,A21,SCMFSA_M:28
::         .= IExec(I31,p+*times*(N,I301),Exec(i30, Initialized ST.k)).next
::             by SCMFSA8B:9
::         .= Exec(i30, Initialized ST.k).result by SCMFSA6C:10
::         .= (Initialized ST.k).result + (Initialized ST.k).next by SCMFSA_2:64
::         .= ST.k.result + (Initialized ST.k).next by SCMFSA_M:37
::         .= ST.k.result + ST.k.next by SCMFSA_M:37
::         .= Fib ((k+1)+1) by A18,A20,A19,PRE_FF:1,XXREAL_0:2;
::     end;
::   end;
:: A22: s1.Nsave = Exec(i2, IExec(i0 ";" i1,p,s)).Nsave by SCMFSA6C:6
::     .= IExec(i0 ";" i1,p,s).Nsave by A13,SCMFSA_2:63
::     .= Exec(i1, Exec(i0, Initialized s)).Nsave by SCMFSA6C:8
::     .= Exec(i0, Initialized s).Nsave by A15,SCMFSA_2:65
::     .= (Initialized s).N by SCMFSA_2:63
::     .= s.N by SCMFSA_M:37;
:: A23: i02 is_halting_on Initialized s,p by SCMFSA7B:19;
::   reconsider i02 as good Program of SCM+FSA;
:: A24: s1.next = Exec(i2, IExec(i0 ";" i1,p,s)).next by SCMFSA6C:6
::     .= IExec(i0 ";" i1,p,s).intloc 0 by SCMFSA_2:63
::     .= Exec(i1, Exec(i0, Initialized s)).intloc 0 by SCMFSA6C:8
::     .= Exec(i0, Initialized s).intloc 0 by SCMFSA_2:65
::     .= (Initialized s).intloc 0 by SCMFSA_2:63
::     .= Fib (0+1) by PRE_FF:1,SCMFSA_M:9;
:: A25: s1.intloc 0 = Exec(i2, IExec(i0 ";" i1,p,s)).intloc 0 by SCMFSA6C:6
::     .= IExec(i0 ";" i1,p,s).intloc 0 by SCMFSA_2:63
::     .= Exec(i1, Exec(i0, Initialized s)).intloc 0 by SCMFSA6C:8
::     .= Exec(i0, Initialized s).intloc 0 by SCMFSA_2:65
::     .= (Initialized s).intloc 0 by SCMFSA_2:63
::     .= 1 by SCMFSA_M:9;
:: A27: s1.result = Exec(i2, IExec(i0 ";" i1,p,s)).result by SCMFSA6C:6
::     .= IExec(i0 ";" i1,p,s).result by A16,SCMFSA_2:63
::     .= Exec(i1, Exec(i0, Initialized s)).result by SCMFSA6C:8
::     .= Exec(i0,Initialized s).result-Exec(i0, Initialized s).result by
:: SCMFSA_2:65
::     .= Fib 0 by PRE_FF:1;
:: A28: P[0]
::   proof
::     assume 0 <= s1.N;
:: A29: ST.0 | UIFS = s1 | UIFS by A25,Th17;
::     hence ST.0.result = Fib 0 by A14,A27,SCMFSA_M:28;
::     thus thesis by A12,A24,A29,SCMFSA_M:28;
::   end;
:: A30: for n being Nat holds P[n] from NAT_1:sch 2(A28, A17);
:: A31: I3 is_halting_on s1,p by A25,Th22;
::   then
:: A32: I3 is_halting_on Initialized s1,p by A25,SCMFSA8B:42;
::   thus
::   IExec(Fib-macro(N,result),p,s).result
::      = Exec(i4, IExec(i02 ";" I3,p,s)).result by A31,A23,SFMASTR1:3,11
::     .= IExec(i02 ";" I3,p,s).result by A1,SCMFSA_2:63
::     .= IExec(I3,p,s1).result by A31,SFMASTR1:7
::     .= ST.n.result by A10,SCMFSA_M:2
::     .= Fib n by A9,A30,A2;
::   thus IExec(Fib-macro(N,result),p,s).N = Exec(i4, IExec(i02 ";" I3,p,s)).N by
:: A31,A23,SFMASTR1:3,11
::     .= IExec(i02 ";" I3,p,s).Nsave by SCMFSA_2:63
::     .= IExec(I3,p,s1).Nsave by A31,SFMASTR1:7
::     .= s.N by A7,A22,A32,Th3;
:: end;