:: On the compositions of macro instructions, Part II
:: by Noriko Asamoto , Yatsuka Nakamura , Piotr Rudnicki and Andrzej Trybulec
::
:: Received July 22, 1996
:: Copyright (c) 1996-2017 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, SUBSET_1, AMI_1, SCMFSA_2, FSM_1, CARD_1, TARSKI,
SCMFSA6A, FUNCT_4, RELAT_1, XBOOLE_0, FUNCT_1, MSUALG_1, CIRCUIT2, AMI_3,
ARYTM_3, XXREAL_0, NAT_1, SF_MASTR, GRAPHSP, AMISTD_2, STRUCT_0,
VALUED_1, FUNCOP_1, SCMFSA6B, PARTFUN1, EXTPRO_1, RELOC, SCMFSA6C,
COMPOS_1, AMISTD_1;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, XXREAL_0, NAT_1, FUNCT_7, INT_1, RELAT_1, FUNCT_1, PARTFUN1,
AFINSQ_1, PBOOLE, FINSEQ_1, FUNCOP_1, FUNCT_4, VALUED_1, STRUCT_0,
MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, SCMFSA_2, AMISTD_1, AMISTD_2,
SCMFSA6A, SF_MASTR, SCMFSA_M;
constructors XXREAL_0, SCMFSA6A, SF_MASTR, AMISTD_1, AMISTD_2, MEMSTR_0,
RELSET_1, PRE_POLY, AMISTD_5, DOMAIN_1, PBOOLE, AMI_3, FUNCT_7, SCMFSA_1,
SCMFSA_M;
registrations ORDINAL1, FUNCOP_1, XREAL_0, NAT_1, INT_1, SCMFSA_2, SF_MASTR,
COMPOS_1, EXTPRO_1, SCMFSA_4, PRE_POLY, FUNCT_7, FUNCT_4, STRUCT_0,
MEMSTR_0, AMI_3, COMPOS_0, SCMFSA_M, AMISTD_1, SCMFSA10, AFINSQ_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin :: General theory
reserve m, n for Nat,
x for set,
i for Instruction of SCM+FSA,
I for Program of SCM+FSA,
a for Int-Location,
f for FinSeq-Location,
l, l1 for Nat,
s,s1,s2 for State of SCM+FSA,
P,P1,P2 for Instruction-Sequence of SCM+FSA;
definition
let I be Program of SCM+FSA, s be State of SCM+FSA;
let P be Instruction-Sequence of SCM+FSA;
func IExec(I,P,s) -> State of SCM+FSA equals
:: SCMFSA6B:def 1
Result(P+*I,Initialized s);
end;
definition
let I be Program of SCM+FSA;
::$CD 2
attr I is keeping_0 means
:: SCMFSA6B:def 4
for s being 0-started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I c= P
for k being Nat holds Comput(P,s,k).intloc 0 = s.intloc 0;
end;
registration
cluster Stop SCM+FSA -> parahalting keeping_0;
end;
registration
cluster really-closed parahalting keeping_0 for MacroInstruction of SCM+FSA;
end;
theorem :: SCMFSA6B:1
for s being 0-started State of SCM+FSA
for I being parahalting Program of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
st I c= P
holds P halts_on s;
theorem :: SCMFSA6B:2
for s being State of SCM+FSA
for I being parahalting Program of SCM+FSA
st Initialize((intloc 0).-->1) c= s
for P being Instruction-Sequence of SCM+FSA
st I c= P
holds P halts_on s;
theorem :: SCMFSA6B:3
for I being really-closed parahalting Program of SCM+FSA,
a being read-write Int-Location
holds not a in UsedILoc I implies IExec(I,P,s).a = s.a;
theorem :: SCMFSA6B:4
for I being parahalting really-closed Program of SCM+FSA
holds not f in UsedI*Loc I implies (IExec(I,P,s)).f = s.f;
theorem :: SCMFSA6B:5
IC s = l & P.l = goto l implies not P halts_on s;
registration
cluster parahalting -> non empty for Program of SCM+FSA;
end;
theorem :: SCMFSA6B:6
for s1 being 0-started State of SCM+FSA
for P,Q being Instruction-Sequence of SCM+FSA
for J being parahalting really-closed Program of SCM+FSA st J c= P
for n being Nat st Reloc(J,n) c= Q
& IC s2 = n & DataPart s1 = DataPart s2
for i being Nat holds
IC Comput(P,s1,i) + n = IC Comput(Q,s2,i) &
IncAddr(CurInstr(P,Comput(P,s1,i)),n) = CurInstr(Q,Comput(Q,s2,i)) &
DataPart Comput(P,s1,i) = DataPart Comput(Q,s2,i);
theorem :: SCMFSA6B:7
for s being 0-started State of SCM+FSA
for I being parahalting really-closed Program of SCM+FSA st I c= P1 & I c= P2
for k being Nat holds
Comput(P1,s,k) = Comput(P2,s,k) &
CurInstr(P1,Comput(P1,s,k)) = CurInstr(P2,Comput(P2,s,k));
theorem :: SCMFSA6B:8
for s being 0-started State of SCM+FSA
for I being parahalting really-closed Program of SCM+FSA
st I c= P1 & I c= P2
holds LifeSpan(P1,s) = LifeSpan(P2,s) & Result(P1,s) = Result(P2,s);
::$CT 2
theorem :: SCMFSA6B:11
for I being keeping_0 parahalting Program of SCM+FSA
holds IExec(I,P,s).intloc 0 = 1;
begin :: The composition of macroinstructions
theorem :: SCMFSA6B:12
for s being 0-started State of SCM+FSA
for I being really-closed Program of SCM+FSA, J being Program of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
st I c= P & P halts_on s
for m st m <= LifeSpan(P,s)
holds Comput(P,s,m) = Comput(P+*(I ";" J),s,m);
theorem :: SCMFSA6B:13
for s being 0-started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA
st P+*I halts_on s & Directed I c= P
holds IC Comput(P,s,LifeSpan(P+*I,s) + 1) = card I;
theorem :: SCMFSA6B:14
for s being 0-started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA
st P+*I halts_on s & Directed I c= P
holds DataPart Comput(P,s,LifeSpan(P+*I,s))
= DataPart Comput(P,s,LifeSpan(P+*I,s)+ 1);
theorem :: SCMFSA6B:15
for I being parahalting really-closed Program of SCM+FSA st
I c= P & Initialize((intloc 0).-->1) c= s
holds for k being Nat st k <= LifeSpan(P,s)
holds CurInstr(P+*Directed I,
Comput(P+*Directed I,s,k)) <> halt SCM+FSA;
theorem :: SCMFSA6B:16
for s being 0-started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA st P+*I halts_on s
for J being Program of SCM+FSA, k being Nat
st k <= LifeSpan(P+*I,s)
holds Comput(P+*I,s,k) = Comput(P+*(I ";" J), s,k);
registration
let I, J be parahalting really-closed Program of SCM+FSA;
cluster I ";" J -> parahalting;
end;
theorem :: SCMFSA6B:17
for s being 0-started State of SCM+FSA
for I being keeping_0 really-closed Program of SCM+FSA
st not P+* I halts_on s
for J being Program of SCM+FSA, k being Nat holds
Comput(P+*I,s,k) = Comput(P+*(I ";" J),s,k);
theorem :: SCMFSA6B:18
for s being 0-started State of SCM+FSA
for I being keeping_0 really-closed Program of SCM+FSA st P+*I halts_on s
for J being really-closed Program of SCM+FSA st I ";" J c= P
for k being Element of NAT holds
IncIC(Comput(P+*I+*J, Initialize Result(P+*I,s),k),card I)
= Comput(P+*(I ";" J),s,(LifeSpan(P+*I,s)+1+k));
registration
let I, J be keeping_0 really-closed Program of SCM+FSA;
cluster I ";" J -> keeping_0;
end;
theorem :: SCMFSA6B:19
for I being keeping_0 parahalting really-closed Program of SCM+FSA,
J being parahalting really-closed Program of SCM+FSA holds
LifeSpan(P+*(I ";" J),s +* Initialize((intloc 0).-->1)) =
LifeSpan(P+*I,s +* Initialize((intloc 0).-->1)) + 1 + LifeSpan(P+*I+*J,
Result(P+*I,s +* Initialize((intloc 0).-->1)) +*
Initialize((intloc 0).-->1));
theorem :: SCMFSA6B:20
for I being keeping_0 parahalting really-closed Program of SCM+FSA,
J being parahalting really-closed Program of SCM+FSA
holds IExec(I ";" J,P,s) = IncIC(IExec(J,P,IExec(I,P,s)),card I);
theorem :: SCMFSA6B:21
for P being Instruction-Sequence of SCM+FSA
holds not P +*(IC s, goto IC s) halts_on s;