:: On the compositions of macro instructions, Part III
:: by Noriko Asamoto , Yatsuka Nakamura , Piotr Rudnicki and Andrzej Trybulec
::
:: Received July 22, 1996
:: Copyright (c) 1996 Association of Mizar Users

set SA0 = Start-At (insloc 0 );

theorem :: SCMFSA6C:1

for a being Int-Location
for s being State of SCM+FSA
for I being parahalting keeping_0 Program of SCM+FSA
for J being parahalting Program of SCM+FSA holds (IExec (I ';' J),s) . a = (IExec J,(IExec I,s)) . a

proof end;

theorem :: SCMFSA6C:2

for f being FinSeq-Location
for s being State of SCM+FSA
for I being parahalting keeping_0 Program of SCM+FSA
for J being parahalting Program of SCM+FSA holds (IExec (I ';' J),s) . f = (IExec J,(IExec I,s)) . f

proof end;

definition

let i be Instruction of SCM+FSA ;
attr i is parahalting means :Def1: :: SCMFSA6C:def 1
Macro i is parahalting;
attr i is keeping_0 means :Def2: :: SCMFSA6C:def 2
Macro i is keeping_0;

end;

:: deftheorem Def1 defines parahalting SCMFSA6C:def 1 :

for i being Instruction of SCM+FSA holds
( i is parahalting iff Macro i is parahalting );

:: deftheorem Def2 defines keeping_0 SCMFSA6C:def 2 :

for i being Instruction of SCM+FSA holds
( i is keeping_0 iff Macro i is keeping_0 );

Lm1: Macro (halt SCM+FSA ) is parahalting

proof end;

Lm2: ( Macro (halt SCM+FSA ) is keeping_0 & Macro (halt SCM+FSA ) is parahalting )

proof end;

registration

cluster halt SCM+FSA -> parahalting keeping_0 ;
coherence
( halt SCM+FSA is keeping_0 & halt SCM+FSA is parahalting )

proof end;

end;

registration

cluster parahalting keeping_0 Element of the Instructions of SCM+FSA ;
existence
ex b₁ being Instruction of SCM+FSA st
( b₁ is keeping_0 & b₁ is parahalting )

proof end;

end;

registration

let i be parahalting Instruction of SCM+FSA ;
cluster Macro i -> parahalting ;
coherence
Macro i is parahalting by Def1;

end;

registration

let i be keeping_0 Instruction of SCM+FSA ;
cluster Macro i -> keeping_0 ;
coherence
Macro i is keeping_0 by Def2;

end;

registration

let a, b be Int-Location ;
cluster a := b -> parahalting ;
coherence
a := b is parahalting

proof end;

cluster AddTo a,b -> parahalting ;
coherence
AddTo a,b is parahalting

proof end;

cluster SubFrom a,b -> parahalting ;
coherence
SubFrom a,b is parahalting

proof end;

cluster MultBy a,b -> parahalting ;
coherence
MultBy a,b is parahalting

proof end;

cluster Divide a,b -> parahalting ;
coherence
Divide a,b is parahalting

proof end;

let f be FinSeq-Location ;
cluster b := f,a -> parahalting ;
coherence
b := f,a is parahalting

proof end;

cluster f,a := b -> parahalting keeping_0 ;
coherence
( f,a := b is parahalting & f,a := b is keeping_0 )

proof end;

end;

registration

let a be Int-Location ;
let f be FinSeq-Location ;
cluster a :=len f -> parahalting ;
coherence
a :=len f is parahalting

proof end;

cluster f :=<0,...,0> a -> parahalting keeping_0 ;
coherence
( f :=<0,...,0> a is parahalting & f :=<0,...,0> a is keeping_0 )

proof end;

end;

registration

let a be read-write Int-Location ;
let b be Int-Location ;
cluster a := b -> keeping_0 ;
coherence
a := b is keeping_0

proof end;

cluster AddTo a,b -> keeping_0 ;
coherence
AddTo a,b is keeping_0

proof end;

cluster SubFrom a,b -> keeping_0 ;
coherence
SubFrom a,b is keeping_0

proof end;

cluster MultBy a,b -> keeping_0 ;
coherence
MultBy a,b is keeping_0

proof end;

end;

registration

let a, b be read-write Int-Location ;
cluster Divide a,b -> keeping_0 ;
coherence
Divide a,b is keeping_0

proof end;

end;

registration

let a be Int-Location ;
let f be FinSeq-Location ;
let b be read-write Int-Location ;
cluster b := f,a -> keeping_0 ;
coherence
b := f,a is keeping_0

proof end;

end;

registration

let f be FinSeq-Location ;
let b be read-write Int-Location ;
cluster b :=len f -> keeping_0 ;
coherence
b :=len f is keeping_0

proof end;

end;

registration

let i be parahalting Instruction of SCM+FSA ;
let J be parahalting Program of SCM+FSA ;
cluster i ';' J -> parahalting ;
coherence
i ';' J is parahalting ;

end;

registration

let I be parahalting Program of SCM+FSA ;
let j be parahalting Instruction of SCM+FSA ;
cluster I ';' j -> parahalting ;
coherence
I ';' j is parahalting ;

end;

registration

let i, j be parahalting Instruction of SCM+FSA ;
cluster i ';' j -> parahalting ;
coherence
i ';' j is parahalting ;

end;

registration

let i be keeping_0 Instruction of SCM+FSA ;
let J be keeping_0 Program of SCM+FSA ;
cluster i ';' J -> keeping_0 ;
coherence
i ';' J is keeping_0 ;

end;

registration

let I be keeping_0 Program of SCM+FSA ;
let j be keeping_0 Instruction of SCM+FSA ;
cluster I ';' j -> keeping_0 ;
coherence
I ';' j is keeping_0 ;

end;

registration

let i, j be keeping_0 Instruction of SCM+FSA ;
cluster i ';' j -> keeping_0 ;
coherence
i ';' j is keeping_0 ;

end;

definition

let s be State of SCM+FSA ;
func Initialize s -> State of SCM+FSA equals :: SCMFSA6C:def 3
(s +* ((intloc 0 ) .--> 1)) +* (Start-At (insloc 0 ));
coherence
(s +* ((intloc 0 ) .--> 1)) +* (Start-At (insloc 0 )) is State of SCM+FSA

proof end;

end;

:: deftheorem defines Initialize SCMFSA6C:def 3 :

for s being State of SCM+FSA holds Initialize s = (s +* ((intloc 0 ) .--> 1)) +* (Start-At (insloc 0 ));

theorem Th3: :: SCMFSA6C:3

for s being State of SCM+FSA holds
( IC (Initialize s) = insloc 0 & (Initialize s) . (intloc 0 ) = 1 & ( for a being read-write Int-Location holds (Initialize s) . a = s . a ) & ( for f being FinSeq-Location holds (Initialize s) . f = s . f ) & ( for l being Instruction-Location of SCM+FSA holds (Initialize s) . l = s . l ) )

proof end;

theorem Th4: :: SCMFSA6C:4

for s1, s2 being State of SCM+FSA holds
( s1,s2 equal_outside NAT iff s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = s2 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) )

proof end;

theorem Th5: :: SCMFSA6C:5

for i being Instruction of SCM+FSA
for s1, s2 being State of SCM+FSA st DataPart s1 = DataPart s2 holds
DataPart (Exec i,s1) = DataPart (Exec i,s2)

proof end;

Lm3: now

let I be parahalting keeping_0 Program of SCM+FSA ; :: thesis: for s being State of SCM+FSA holds DataPart (Initialize (IExec I,s)) = DataPart (IExec I,s)
let s be State of SCM+FSA ; :: thesis: DataPart (Initialize (IExec I,s)) = DataPart (IExec I,s)
set IE = IExec I,s;
set IF = Int-Locations \/ FinSeq-Locations ;

now

A1: ( dom (Initialize (IExec I,s)) = the carrier of SCM+FSA & dom (IExec I,s) = the carrier of SCM+FSA ) by AMI_1:79;
hence A2: dom (DataPart (Initialize (IExec I,s))) = (dom (IExec I,s)) /\ (Int-Locations \/ FinSeq-Locations ) by RELAT_1:90, SCMFSA_2:127; :: thesis: for x being set st x in dom (DataPart (Initialize (IExec I,s))) holds
(DataPart (Initialize (IExec I,s))) . b₂ = (IExec I,s) . b₂
let x be set ; :: thesis: ( x in dom (DataPart (Initialize (IExec I,s))) implies (DataPart (Initialize (IExec I,s))) . b₁ = (IExec I,s) . b₁ )
assume A3: x in dom (DataPart (Initialize (IExec I,s))) ; :: thesis: (DataPart (Initialize (IExec I,s))) . b₁ = (IExec I,s) . b₁
dom (Initialize (IExec I,s)) = (Int-Locations \/ FinSeq-Locations ) \/ ({(IC SCM+FSA )} \/ NAT ) by A1, SCMFSA_2:8, XBOOLE_1:4;
then A4: dom (DataPart (Initialize (IExec I,s))) = Int-Locations \/ FinSeq-Locations by A1, A2, XBOOLE_1:21;

per cases ( x in Int-Locations or x in FinSeq-Locations ) by A3, A4, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis: (DataPart (Initialize (IExec I,s))) . b₁ = (IExec I,s) . b₁

then reconsider x' = x as Int-Location by SCMFSA_2:11;

hereby :: thesis: verum

per cases ( not x' is read-only or x' is read-only ) ;

suppose A5: not x' is read-only ; :: thesis: (DataPart (Initialize (IExec I,s))) . x = (IExec I,s) . x

thus (DataPart (Initialize (IExec I,s))) . x = (Initialize (IExec I,s)) . x by A3, A4, FUNCT_1:72, SCMFSA_2:127
.= (IExec I,s) . x by A5, Th3 ; :: thesis: verum

end;

suppose x' is read-only ; :: thesis: (DataPart (Initialize (IExec I,s))) . x = (IExec I,s) . x

then A6: x' = intloc 0 by SF_MASTR:def 5;
thus (DataPart (Initialize (IExec I,s))) . x = (Initialize (IExec I,s)) . x' by A3, A4, FUNCT_1:72, SCMFSA_2:127
.= 1 by A6, Th3
.= (IExec I,s) . x by A6, SCMFSA6B:35 ; :: thesis: verum

end;

end;

end;

end;

suppose x in FinSeq-Locations ; :: thesis: (DataPart (Initialize (IExec I,s))) . b₁ = (IExec I,s) . b₁

then reconsider x' = x as FinSeq-Location by SCMFSA_2:12;
thus (DataPart (Initialize (IExec I,s))) . x = (Initialize (IExec I,s)) . x' by A3, A4, FUNCT_1:72, SCMFSA_2:127
.= (IExec I,s) . x by Th3 ; :: thesis: verum

end;

end;

end;

hence DataPart (Initialize (IExec I,s)) = DataPart (IExec I,s) by FUNCT_1:68, SCMFSA_2:127; :: thesis: verum

end;

theorem Th6: :: SCMFSA6C:6

for s being State of SCM+FSA
for i being parahalting Instruction of SCM+FSA holds Exec i,(Initialize s) = IExec (Macro i),s

proof end;

theorem Th7: :: SCMFSA6C:7

for a being Int-Location
for s being State of SCM+FSA
for I being parahalting keeping_0 Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec (I ';' j),s) . a = (Exec j,(IExec I,s)) . a

proof end;

theorem Th8: :: SCMFSA6C:8

for f being FinSeq-Location
for s being State of SCM+FSA
for I being parahalting keeping_0 Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec (I ';' j),s) . f = (Exec j,(IExec I,s)) . f

proof end;

theorem Th9: :: SCMFSA6C:9

for a being Int-Location
for s being State of SCM+FSA
for i being parahalting keeping_0 Instruction of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec (i ';' j),s) . a = (Exec j,(Exec i,(Initialize s))) . a

proof end;

theorem :: SCMFSA6C:10

for f being FinSeq-Location
for s being State of SCM+FSA
for i being parahalting keeping_0 Instruction of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec (i ';' j),s) . f = (Exec j,(Exec i,(Initialize s))) . f

proof end;

definition

let a, b be Int-Location ;
func swap a,b -> Program of SCM+FSA equals :: SCMFSA6C:def 4
(((FirstNotUsed (Macro (a := b))) := a) ';' (a := b)) ';' (b := (FirstNotUsed (Macro (a := b))));
correctness
coherence
(((FirstNotUsed (Macro (a := b))) := a) ';' (a := b)) ';' (b := (FirstNotUsed (Macro (a := b)))) is Program of SCM+FSA ;
;

end;

:: deftheorem defines swap SCMFSA6C:def 4 :

for a, b being Int-Location holds swap a,b = (((FirstNotUsed (Macro (a := b))) := a) ';' (a := b)) ';' (b := (FirstNotUsed (Macro (a := b))));

registration

let a, b be Int-Location ;
cluster swap a,b -> parahalting ;
coherence
swap a,b is parahalting ;

end;

registration

let a, b be read-write Int-Location ;
cluster swap a,b -> keeping_0 ;
coherence
swap a,b is keeping_0 ;

end;

theorem :: SCMFSA6C:11

for s being State of SCM+FSA
for a, b being read-write Int-Location holds
( (IExec (swap a,b),s) . a = s . b & (IExec (swap a,b),s) . b = s . a )

proof end;

theorem :: SCMFSA6C:12

for a, b being Int-Location holds UsedInt*Loc (swap a,b) = {}

proof end;