:: 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-2016 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 AMI_1, SCMFSA_2, FSM_1, CARD_1, SCMFSA6B, FUNCT_1, RELAT_1,
ARYTM_3, FUNCT_4, SCMFSA6A, TARSKI, XBOOLE_0, CIRCUIT2, NUMBERS, GRAPHSP,
AMI_3, XXREAL_0, SF_MASTR, FUNCOP_1, STRUCT_0, ARYTM_1, INT_1, COMPLEX1,
PARTFUN1, FINSEQ_1, FINSEQ_2, AOFA_I00, EXTPRO_1, SCMFSA6C, COMPOS_1,
NAT_1, AMISTD_1, FRECHET, TURING_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ENUMSET1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, NAT_1, INT_1, COMPLEX1, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1,
FINSEQ_2, FUNCOP_1, FUNCT_4, PBOOLE, STRUCT_0, MEMSTR_0, COMPOS_0,
COMPOS_1, COMPOS_2, EXTPRO_1, AMISTD_1, FUNCT_7, SCMFSA_M, SCMFSA_2,
SCMFSA10, SCMFSA6A, SF_MASTR, SCMFSA6B, XXREAL_0;
constructors DOMAIN_1, SETWISEO, XXREAL_0, INT_2, SCMFSA6A, SF_MASTR,
SCMFSA6B, RELSET_1, PRE_POLY, AMISTD_1, AMISTD_2, PBOOLE, FUNCT_4,
MEMSTR_0, SCMFSA_1, SCMFSA_M, FUNCT_7, SCMFSA10, COMPOS_2;
registrations FUNCT_1, FUNCOP_1, XREAL_0, INT_1, SCMFSA_2, SF_MASTR, SCMFSA6B,
ORDINAL1, RELSET_1, COMPOS_1, STRUCT_0, EXTPRO_1, FUNCT_4, MEMSTR_0,
AMI_3, COMPOS_0, SCMFSA_M, SCMFSA6A, SCMFSA10, CARD_1, AMISTD_2;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
begin :: Consequences of the main theorem from SCMFSA6B
reserve x for set,
i for Instruction of SCM+FSA,
a,b 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;
theorem :: SCMFSA6C:1
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).a = IExec(J,P,IExec(I,P,s)).a;
theorem :: SCMFSA6C:2
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).f = IExec(J,P,IExec(I,P,s)).f;
begin :: Properties of simple macro instructions
::$CD
definition
let i be Instruction of SCM+FSA;
:: attr i is parahalting means
:: :Def1:
:: Macro i is parahalting;
attr i is keeping_0 means
:: SCMFSA6C:def 2
Macro i is keeping_0;
end;
registration
cluster halt SCM+FSA -> keeping_0;
end;
registration
let i be sequential Instruction of SCM+FSA;
cluster Macro i -> parahalting;
end;
registration
let a, b be Int-Location;
let f be FinSeq-Location;
cluster (f,a) := b -> keeping_0;
end;
registration
let a be Int-Location, f be FinSeq-Location;
cluster f :=<0,...,0> a -> keeping_0;
end;
registration
let a be read-write Int-Location, b be Int-Location;
cluster a := b -> keeping_0;
cluster AddTo(a, b) -> keeping_0;
cluster SubFrom(a, b) -> keeping_0;
cluster MultBy(a, b) -> keeping_0;
end;
registration
cluster keeping_0 sequential for Instruction of SCM+FSA;
end;
registration
let i be keeping_0 Instruction of SCM+FSA;
cluster Macro i -> keeping_0;
end;
registration
let a, b be read-write Int-Location;
cluster Divide(a, b) -> keeping_0;
end;
registration
let a be Int-Location, f be FinSeq-Location, b be read-write Int-Location;
cluster b := (f,a) -> keeping_0;
end;
registration
let f be FinSeq-Location, b be read-write Int-Location;
cluster b :=len f -> keeping_0;
end;
registration
let i be sequential Instruction of SCM+FSA;
cluster Macro i -> really-closed;
end;
:: registration
:: let i be keeping_0 Instruction of SCM+FSA;
:: cluster Macro i -> really-closed;
:: coherence;
:: end;
registration let i be sequential Instruction of SCM+FSA, J be
parahalting really-closed Program of SCM+FSA; cluster i ";" J ->
parahalting really-closed;
end;
registration
let I be parahalting really-closed Program of SCM+FSA,
j be sequential Instruction of SCM+FSA;
cluster I ";" j -> parahalting really-closed;
end;
registration
let i,j be sequential Instruction of SCM+FSA;
cluster i ";" j -> parahalting really-closed;
end;
registration
let i be keeping_0 sequential Instruction of SCM+FSA,
J be keeping_0 really-closed Program of SCM+FSA;
cluster i ";" J -> keeping_0;
end;
registration
let I be keeping_0 really-closed Program of SCM+FSA,
j be keeping_0 sequential Instruction of SCM+FSA;
cluster I ";" j -> keeping_0;
end;
registration
let i, j be keeping_0 sequential Instruction of SCM+FSA;
cluster i ";" j -> keeping_0;
end;
begin :: Consequenses of the main theorem
::$CT
theorem :: SCMFSA6C:4
DataPart s1 = DataPart s2 implies DataPart Exec (i, s1) =
DataPart Exec (i, s2);
theorem :: SCMFSA6C:5
for i being sequential Instruction of SCM+FSA
holds Exec(i,Initialized s) = IExec(Macro i,P,s);
theorem :: SCMFSA6C:6
for I being keeping_0 parahalting really-closed Program of SCM+FSA,
j being sequential Instruction of SCM+FSA holds IExec(I ";" j,P,s).a
= Exec(j,IExec(I,P,s)).a;
theorem :: SCMFSA6C:7
for I being keeping_0 parahalting really-closed Program of SCM+FSA,
j being sequential Instruction of SCM+FSA
holds IExec(I ";" j,P,s).f = Exec(j,IExec(I,P,s)).f;
theorem :: SCMFSA6C:8
for i being keeping_0 sequential Instruction of SCM+FSA, j being
sequential Instruction of SCM+FSA holds IExec(i ";" j,P,s).a
= Exec(j, Exec(i,Initialized s)).a;
theorem :: SCMFSA6C:9
for i being keeping_0 sequential Instruction of SCM+FSA, j being
sequential Instruction of SCM+FSA holds IExec(i ";" j,P,s).f = Exec(j, Exec(i,
Initialized s)).f;
begin :: An example
definition
let a, b be Int-Location;
func swap (a, b) -> Program of SCM+FSA equals
:: SCMFSA6C:def 3
FirstNotUsed Macro (a := b) :=
a ";" (a := b) ";" (b := FirstNotUsed Macro (a := b));
end;
registration
let a, b be Int-Location;
cluster swap(a,b) -> parahalting really-closed;
end;
registration
let a, b be read-write Int-Location;
cluster swap(a,b) -> keeping_0;
end;
theorem :: SCMFSA6C:10
for a, b being read-write Int-Location holds IExec(swap(a,b),P,s).a =
s.b & IExec(swap(a,b),P,s).b = s.a;
theorem :: SCMFSA6C:11
UsedI*Loc swap(a, b) = {};
registration let i,j be sequential Instruction of SCM+FSA;
cluster i ';' j -> really-closed;
end;
registration
let I be really-closed MacroInstruction of SCM+FSA,
j be sequential Instruction of SCM+FSA;
cluster I ';' j -> really-closed;
end;
registration
let i be sequential Instruction of SCM+FSA,
J be really-closed MacroInstruction of SCM+FSA;
cluster i ';' J -> really-closed;
end;