SFMASTR2: Another { \bf times } Macro Instruction

:: Another { \bf times } Macro Instruction
:: by Piotr Rudnicki
::
:: Received June 4, 1998
:: Copyright (c) 1998 Association of Mizar Users

set D = Int-Locations \/ FinSeq-Locations ;

set SAt = Start-At (insloc 0 );

set IL = NAT ;

theorem Th1: :: SFMASTR2:1

for s being State of SCM+FSA
for b being Int-Location
for I being Program of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s & not b in UsedIntLoc I holds
(IExec I,s) . b = (Initialize s) . b

proof end;

theorem :: SFMASTR2:2

for s being State of SCM+FSA
for f being FinSeq-Location
for I being Program of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s & not f in UsedInt*Loc I holds
(IExec I,s) . f = (Initialize s) . f

proof end;

theorem Th3: :: SFMASTR2:3

for s being State of SCM+FSA
for a being Int-Location
for I being Program of SCM+FSA st ( ( I is_closed_on Initialize s & I is_halting_on Initialize s ) or I is parahalting ) & ( s . (intloc 0 ) = 1 or not a is read-only ) & not a in UsedIntLoc I holds
(IExec I,s) . a = s . a

proof end;

theorem Th4: :: SFMASTR2:4

for s being State of SCM+FSA
for I being Program of SCM+FSA st s . (intloc 0 ) = 1 holds
( I is_closed_on s iff I is_closed_on Initialize s )

proof end;

theorem Th5: :: SFMASTR2:5

for s being State of SCM+FSA
for I being Program of SCM+FSA st s . (intloc 0 ) = 1 holds
( I is_closed_on s & I is_halting_on s iff ( I is_closed_on Initialize s & I is_halting_on Initialize s ) )

proof end;

theorem Th6: :: SFMASTR2:6

for s1, s2 being State of SCM+FSA
for Iloc being Subset of Int-Locations
for Floc being Subset of FinSeq-Locations holds
( s1 | (Iloc \/ Floc) = s2 | (Iloc \/ Floc) iff ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location st x in Floc holds
s1 . x = s2 . x ) ) )

proof end;

theorem Th7: :: SFMASTR2:7

for s1, s2 being State of SCM+FSA
for Iloc being Subset of Int-Locations holds
( s1 | (Iloc \/ FinSeq-Locations ) = s2 | (Iloc \/ FinSeq-Locations ) iff ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location holds s1 . x = s2 . x ) ) )

proof end;

definition

let a be Int-Location ;
let I be Program of SCM+FSA ;
func times a,I -> Program of SCM+FSA equals :: SFMASTR2:def 1
((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a) ';' (while>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(I ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0 ))));
correctness ;

end;

:: deftheorem defines times SFMASTR2:def 1 :

notation

let a be Int-Location ;
let I be Program of SCM+FSA ;
synonym a times I for times a,I;

end;

theorem Th8: :: SFMASTR2:8

for b being Int-Location
for I being Program of SCM+FSA holds {b} \/ (UsedIntLoc I) c= UsedIntLoc (times b,I)

proof end;

theorem :: SFMASTR2:9

for b being Int-Location
for I being Program of SCM+FSA holds UsedInt*Loc (times b,I) = UsedInt*Loc I

proof end;

registration

let I be good Program of SCM+FSA ;
let a be Int-Location ;
cluster times a,I -> good ;
coherence ;

end;

definition

let s be State of SCM+FSA ;
let I be Program of SCM+FSA ;
let a be Int-Location ;
func StepTimes a,I,s -> Function of NAT , product the Object-Kind of SCM+FSA equals :: SFMASTR2:def 2
StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(I ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialize s));
correctness ;

end;

:: deftheorem defines StepTimes SFMASTR2:def 2 :

theorem Th10: :: SFMASTR2:10

for s being State of SCM+FSA
for a being Int-Location
for J being good Program of SCM+FSA holds ((StepTimes a,J,s) . 0 ) . (intloc 0 ) = 1

proof end;

theorem Th11: :: SFMASTR2:11

for s being State of SCM+FSA
for a being Int-Location
for J being good Program of SCM+FSA st ( s . (intloc 0 ) = 1 or not a is read-only ) holds
((StepTimes a,J,s) . 0 ) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = s . a

proof end;

theorem Th12: :: SFMASTR2:12

for s being State of SCM+FSA
for a being Int-Location
for J being good Program of SCM+FSA
for k being Element of NAT st ((StepTimes a,J,s) . k) . (intloc 0 ) = 1 & J is_closed_on (StepTimes a,J,s) . k & J is_halting_on (StepTimes a,J,s) . k holds
( ((StepTimes a,J,s) . (k + 1)) . (intloc 0 ) = 1 & ( ((StepTimes a,J,s) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 implies ((StepTimes a,J,s) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = (((StepTimes a,J,s) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) - 1 ) )

proof end;

theorem Th13: :: SFMASTR2:13

for s being State of SCM+FSA
for a being Int-Location
for I being Program of SCM+FSA st ( s . (intloc 0 ) = 1 or not a is read-only ) holds
((StepTimes a,I,s) . 0 ) . a = s . a

proof end;

theorem :: SFMASTR2:14

for s being State of SCM+FSA
for a being Int-Location
for f being FinSeq-Location
for I being Program of SCM+FSA holds ((StepTimes a,I,s) . 0 ) . f = s . f

proof end;

definition

let s be State of SCM+FSA ;
let a be Int-Location ;
let I be Program of SCM+FSA ;
pred ProperTimesBody a,I,s means :Def3: :: SFMASTR2:def 3
for k being Element of NAT st k < s . a holds
( I is_closed_on (StepTimes a,I,s) . k & I is_halting_on (StepTimes a,I,s) . k );

end;

:: deftheorem Def3 defines ProperTimesBody SFMASTR2:def 3 :

theorem Th15: :: SFMASTR2:15

for s being State of SCM+FSA
for a being Int-Location
for I being Program of SCM+FSA st I is parahalting holds
ProperTimesBody a,I,s

proof end;

theorem Th16: :: SFMASTR2:16

for s being State of SCM+FSA
for a being Int-Location
for J being good Program of SCM+FSA st ProperTimesBody a,J,s holds
for k being Element of NAT st k <= s . a holds
((StepTimes a,J,s) . k) . (intloc 0 ) = 1

proof end;

theorem Th17: :: SFMASTR2:17

for s being State of SCM+FSA
for a being Int-Location
for J being good Program of SCM+FSA st ( s . (intloc 0 ) = 1 or not a is read-only ) & ProperTimesBody a,J,s holds
for k being Element of NAT st k <= s . a holds
(((StepTimes a,J,s) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + k = s . a

proof end;

theorem Th18: :: SFMASTR2:18

for s being State of SCM+FSA
for a being Int-Location
for J being good Program of SCM+FSA st ProperTimesBody a,J,s & 0 <= s . a & ( s . (intloc 0 ) = 1 or not a is read-only ) holds
for k being Element of NAT st k >= s . a holds
( ((StepTimes a,J,s) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = 0 & ((StepTimes a,J,s) . k) . (intloc 0 ) = 1 )

proof end;

theorem Th19: :: SFMASTR2:19

for s being State of SCM+FSA
for a being Int-Location
for I being Program of SCM+FSA st s . (intloc 0 ) = 1 holds
((StepTimes a,I,s) . 0 ) | ((UsedIntLoc I) \/ FinSeq-Locations ) = s | ((UsedIntLoc I) \/ FinSeq-Locations )

proof end;

theorem Th20: :: SFMASTR2:20

for s being State of SCM+FSA
for a being Int-Location
for J being good Program of SCM+FSA
for k being Element of NAT st ((StepTimes a,J,s) . k) . (intloc 0 ) = 1 & J is_halting_on Initialize ((StepTimes a,J,s) . k) & J is_closed_on Initialize ((StepTimes a,J,s) . k) & ((StepTimes a,J,s) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 holds
((StepTimes a,J,s) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations ) = (IExec J,((StepTimes a,J,s) . k)) | ((UsedIntLoc J) \/ FinSeq-Locations )

proof end;

theorem Th21: :: SFMASTR2:21

for s being State of SCM+FSA
for a being Int-Location
for J being good Program of SCM+FSA
for k being Element of NAT st ( ProperTimesBody a,J,s or J is parahalting ) & k < s . a & ( s . (intloc 0 ) = 1 or not a is read-only ) holds
((StepTimes a,J,s) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations ) = (IExec J,((StepTimes a,J,s) . k)) | ((UsedIntLoc J) \/ FinSeq-Locations )

proof end;

theorem :: SFMASTR2:22

for s being State of SCM+FSA
for a being Int-Location
for I being Program of SCM+FSA st s . a <= 0 & s . (intloc 0 ) = 1 holds
(IExec (times a,I),s) | ((UsedIntLoc I) \/ FinSeq-Locations ) = s | ((UsedIntLoc I) \/ FinSeq-Locations )

proof end;

theorem Th23: :: SFMASTR2:23

for s being State of SCM+FSA
for a being Int-Location
for J being good Program of SCM+FSA
for k being Element of NAT st s . a = k & ( ProperTimesBody a,J,s or J is parahalting ) & ( s . (intloc 0 ) = 1 or not a is read-only ) holds
DataPart (IExec (times a,J),s) = DataPart ((StepTimes a,J,s) . k)

proof end;

theorem Th24: :: SFMASTR2:24

for s being State of SCM+FSA
for a being Int-Location
for J being good Program of SCM+FSA st s . (intloc 0 ) = 1 & ( ProperTimesBody a,J,s or J is parahalting ) holds
( times a,J is_closed_on s & times a,J is_halting_on s )

proof end;

definition

let d be read-write Int-Location ;
func triv-times d -> Program of SCM+FSA equals :: SFMASTR2:def 4
times d,((while=0 d,(Macro (d := d))) ';' (SubFrom d,(intloc 0 )));
correctness ;

end;

:: deftheorem defines triv-times SFMASTR2:def 4 :

theorem :: SFMASTR2:25

for s being State of SCM+FSA
for d being read-write Int-Location st s . d <= 0 holds
(IExec (triv-times d),s) . d = s . d

proof end;

theorem :: SFMASTR2:26

for s being State of SCM+FSA
for d being read-write Int-Location st 0 <= s . d holds
(IExec (triv-times d),s) . d = 0

proof end;

definition

let N, result be Int-Location ;
func Fib-macro N,result -> Program of SCM+FSA equals :: SFMASTR2:def 5
(((((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}))))));
correctness ;

end;

:: deftheorem defines Fib-macro SFMASTR2:def 5 :

theorem :: SFMASTR2:27

for s being State of SCM+FSA
for N, result being read-write Int-Location st N <> result holds
for n being Element of NAT st n = s . N holds
( (IExec (Fib-macro N,result),s) . result = Fib n & (IExec (Fib-macro N,result),s) . N = s . N )

proof end;