Journal of Formalized Mathematics
Volume 8, 1996
University of Bialystok
Copyright (c) 1996 Association of Mizar Users

On the Composition of Macro Instructions. Part II

by
Noriko Asamoto,
Yatsuka Nakamura,
Piotr Rudnicki, and
Andrzej Trybulec

MML identifier: SCMFSA6B
[ Mizar article, MML identifier index ]

environ

vocabulary FUNCT_1, RELAT_1, FUNCT_4, BOOLE, AMI_1, SCMFSA_2, SCMFSA6A, AMI_3,
CAT_1, SCM_1, INT_1, FUNCOP_1, FUNCT_7, SF_MASTR, AMI_5, FINSEQ_1, RELOC,
CARD_1, SCMFSA6B, CARD_3;
notation TARSKI, XBOOLE_0, NUMBERS, XCMPLX_0, XREAL_0, NAT_1, INT_1, RELAT_1,
FUNCT_1, FUNCT_2, FINSEQ_1, CARD_1, CQC_LANG, FUNCT_4, STRUCT_0, AMI_1,
AMI_3, SCM_1, AMI_5, FUNCT_7, SCMFSA_2, SCMFSA_4, SCMFSA_5, SCMFSA6A,
SF_MASTR;
constructors SCM_1, SCMFSA6A, SF_MASTR, FUNCT_7, SCMFSA_5, AMI_5, NAT_1,
MEMBERED;
clusters AMI_1, SCMFSA_2, FUNCT_1, SCMFSA_4, INT_1, SCMFSA6A, SF_MASTR,
CQC_LANG, RELSET_1, FRAENKEL, XREAL_0, MEMBERED, NUMBERS, ORDINAL2;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;

begin

canceled 2;

theorem :: SCMFSA6B:3
for f, g being Function, A being set st A /\ dom f c= A /\ dom g
holds (f+*g|A)|A = g|A;

begin

reserve m, n for Nat,
x for set,
i for Instruction of SCM+FSA,
I for Macro-Instruction,
a for Int-Location, f for FinSeq-Location,
l, l1 for Instruction-Location of SCM+FSA,
s,s1,s2 for State of SCM+FSA;

theorem :: SCMFSA6B:4
Start-At insloc 0 c= Initialized I;

theorem :: SCMFSA6B:5
I +* Start-At insloc n c= s implies I c= s;

theorem :: SCMFSA6B:6
(I +* Start-At insloc n)|the Instruction-Locations of SCM+FSA = I;

theorem :: SCMFSA6B:7
x in dom I implies I.x = (I +* Start-At insloc n).x;

theorem :: SCMFSA6B:8
Initialized I c= s implies I +* Start-At insloc 0 c= s;

theorem :: SCMFSA6B:9
not a in dom Start-At l;

theorem :: SCMFSA6B:10
not f in dom Start-At l;

theorem :: SCMFSA6B:11
not l1 in dom Start-At l;

theorem :: SCMFSA6B:12
not a in dom (I+*Start-At l);

theorem :: SCMFSA6B:13
not f in dom (I+*Start-At l);

theorem :: SCMFSA6B:14
s+*I+*Start-At insloc 0 = s+*Start-At insloc 0+*I;

begin ::  General theory

reserve N for non empty with_non-empty_elements set;

theorem :: SCMFSA6B:15
s = Following s implies for n holds (Computation s).n = s;

theorem :: SCMFSA6B:16
for S being halting IC-Ins-separated definite
(non empty non void AMI-Struct over N),
s being State of S st s is halting
holds Result s = (Computation s).LifeSpan s;

definition let N;
let S be IC-Ins-separated definite (non empty non void AMI-Struct over N);
let s be State of S, l be Instruction-Location of S, i be Instruction of S;
redefine func s+*(l,i) -> State of S;
end;

definition
let s be State of SCM+FSA, li be Int-Location, k be Integer;
redefine func s+*(li,k) -> State of SCM+FSA;
end;

theorem :: SCMFSA6B:17
for S being steady-programmed IC-Ins-separated definite
(non empty non void AMI-Struct over N)
for s being State of S, n
holds s|the Instruction-Locations of S
= ((Computation s).n)|the Instruction-Locations of S;

begin

definition let I be Macro-Instruction, s be State of SCM+FSA;
func IExec(I,s) -> State of SCM+FSA equals
:: SCMFSA6B:def 1

Result(s+*Initialized I) +* s|the Instruction-Locations of SCM+FSA;
end;

definition let I be Macro-Instruction;
attr I is paraclosed means
:: SCMFSA6B:def 2
for s being State of SCM+FSA, n being Nat
st I +* Start-At insloc 0 c= s
holds IC (Computation s).n in dom I;

attr I is parahalting means
:: SCMFSA6B:def 3
I +* Start-At insloc 0 is halting;

attr I is keeping_0 means
:: SCMFSA6B:def 4
::Lkeep
for s being State of SCM+FSA st I +* Start-At insloc 0 c= s
for k being Nat holds ((Computation s).k).intloc 0 = s.intloc 0;
end;

definition
cluster parahalting Macro-Instruction;
end;

theorem :: SCMFSA6B:18
for I being parahalting Macro-Instruction
st I +* Start-At insloc 0 c= s holds s is halting;

theorem :: SCMFSA6B:19
for I being parahalting Macro-Instruction
st Initialized I c= s holds s is halting;

definition let I be parahalting Macro-Instruction;
cluster Initialized I -> halting;
end;

theorem :: SCMFSA6B:20
s2 +*(IC s2, goto IC s2) is not halting;

theorem :: SCMFSA6B:21
s1,s2 equal_outside the Instruction-Locations of SCM+FSA &
I c= s1 & I c= s2 &
(for m st m < n holds IC((Computation s2).m) in dom I)
implies
for m st m <= n holds
(Computation s1).m, (Computation s2 ).m equal_outside
the Instruction-Locations of SCM+FSA;

definition
cluster parahalting -> paraclosed Macro-Instruction;

cluster keeping_0 -> paraclosed Macro-Instruction;
end;

theorem :: SCMFSA6B:22
for I being parahalting Macro-Instruction,
holds not a in UsedIntLoc I implies (IExec(I, s)).a = s.a;

theorem :: SCMFSA6B:23
for I being parahalting Macro-Instruction
holds not f in UsedInt*Loc I implies (IExec(I, s)).f = s.f;

theorem :: SCMFSA6B:24
IC s = l & s.l = goto l implies s is not halting;

definition
cluster parahalting -> non empty Macro-Instruction;
end;

theorem :: SCMFSA6B:25  ::T9'
for I being parahalting Macro-Instruction holds dom I <> {};

theorem :: SCMFSA6B:26  ::T9
for I being parahalting Macro-Instruction holds insloc 0 in dom I;

theorem :: SCMFSA6B:27  ::T0
for J being parahalting Macro-Instruction st J +* Start-At insloc 0 c= s1
for n being Nat st ProgramPart Relocated(J,n) c= s2 &
IC s2 = insloc n &
s1 | (Int-Locations \/ FinSeq-Locations)
= s2 | (Int-Locations \/ FinSeq-Locations)
for i being Nat holds
IC (Computation s1).i + n = IC (Computation s2).i &
IncAddr(CurInstr ((Computation s1).i),n) = CurInstr ((Computation s2).i) &
(Computation s1).i | (Int-Locations \/ FinSeq-Locations)
= (Computation s2).i | (Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA6B:28  ::T13
for I being parahalting Macro-Instruction st
I +* Start-At insloc 0 c= s1 & I +* Start-At insloc 0 c= s2 &
s1,s2 equal_outside the Instruction-Locations of SCM+FSA holds
for k being Nat holds
(Computation s1).k, (Computation s2).k
equal_outside the Instruction-Locations of SCM+FSA &
CurInstr (Computation s1).k = CurInstr (Computation s2).k;

theorem :: SCMFSA6B:29  ::T14
for I being parahalting Macro-Instruction st
I +* Start-At insloc 0 c= s1 & I +* Start-At insloc 0 c= s2 &
s1,s2 equal_outside the Instruction-Locations of SCM+FSA holds
LifeSpan s1 = LifeSpan s2 &
Result s1, Result s2 equal_outside the Instruction-Locations of SCM+FSA;

theorem :: SCMFSA6B:30  ::T27
for I being parahalting Macro-Instruction
holds IC IExec(I,s) = IC Result (s +* Initialized I);

theorem :: SCMFSA6B:31
for I being non empty Macro-Instruction
holds insloc 0 in dom I & insloc 0 in dom Initialized I &
insloc 0 in dom (I +* Start-At insloc 0);

theorem :: SCMFSA6B:32
x in dom Macro i iff x = insloc 0 or x = insloc 1;

theorem :: SCMFSA6B:33
(Macro i).(insloc 0) = i &
(Macro i).(insloc 1) = halt SCM+FSA &
(Initialized Macro i).insloc 0 = i &
(Initialized Macro i).insloc 1 = halt SCM+FSA &
((Macro i) +* Start-At insloc 0).insloc 0 = i;

theorem :: SCMFSA6B:34
Initialized I c= s implies IC s = insloc 0;

definition
cluster keeping_0 parahalting Macro-Instruction;
end;

theorem :: SCMFSA6B:35
for I being keeping_0 parahalting Macro-Instruction
holds IExec(I, s).intloc 0 = 1;

begin :: The composition of macroinstructions

theorem :: SCMFSA6B:36
for I being paraclosed Macro-Instruction, J being Macro-Instruction
st I +* Start-At insloc 0 c= s & s is halting
for m st m <= LifeSpan s
holds (Computation s).m,(Computation(s+*(I ';' J))).m
equal_outside the Instruction-Locations of SCM+FSA;

theorem :: SCMFSA6B:37  ::Lemma01
for I being paraclosed Macro-Instruction
st s +*I is halting & Directed I c= s & Start-At insloc 0 c= s holds
IC (Computation s).(LifeSpan (s +*I) + 1)
= insloc card I;

theorem :: SCMFSA6B:38  ::Lemma02
for I being paraclosed Macro-Instruction
st s +*I is halting & Directed I c= s & Start-At insloc 0 c= s
holds
(Computation s).(LifeSpan (s +*I)) |
(Int-Locations \/ FinSeq-Locations) =
(Computation s).(LifeSpan (s +*I) + 1) |
(Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA6B:39  ::Lemma0
for I being parahalting Macro-Instruction
st Initialized I c= s holds
for k being Nat st k <= LifeSpan s holds
CurInstr (Computation (s +* Directed I)).k <> halt SCM+FSA;

theorem :: SCMFSA6B:40
for I being paraclosed Macro-Instruction
st s +* (I +* Start-At insloc 0) is halting
for J being Macro-Instruction, k being Nat
st k <= LifeSpan (s +* (I +* Start-At insloc 0))
holds (Computation (s +* (I +* Start-At insloc 0))).k,
(Computation (s +* ((I ';' J) +* Start-At insloc 0))).k
equal_outside the Instruction-Locations of SCM+FSA;

definition
let I, J be parahalting Macro-Instruction;
cluster I ';' J -> parahalting;
end;

theorem :: SCMFSA6B:41
for I being keeping_0 Macro-Instruction
st not s +* (I +* Start-At insloc 0) is halting
for J being Macro-Instruction, k being Nat
holds (Computation (s +* (I +* Start-At insloc 0))).k,
(Computation (s +* ((I ';' J) +* Start-At insloc 0))).k
equal_outside the Instruction-Locations of SCM+FSA;

theorem :: SCMFSA6B:42
for I being keeping_0 Macro-Instruction
st s +* I is halting
for J being paraclosed Macro-Instruction
st (I ';' J) +* Start-At insloc 0 c= s
for k being Nat
holds (Computation (Result(s +*I)
+* (J +* Start-At insloc 0))).k
+* Start-At (IC (Computation ((Result(s +*I))
+* (J +* Start-At insloc 0))).k + card I),
(Computation (s +* (I ';' J))).
(LifeSpan (s +* I)+1+k)
equal_outside the Instruction-Locations of SCM+FSA;

definition
let I, J be keeping_0 Macro-Instruction;
cluster I ';' J -> keeping_0;
end;

theorem :: SCMFSA6B:43  ::T22
for I being keeping_0 parahalting Macro-Instruction,
J being parahalting Macro-Instruction
holds
LifeSpan (s +* Initialized (I ';' J))
= LifeSpan (s +* Initialized I) + 1
+ LifeSpan (Result (s +* Initialized I) +* Initialized J);

theorem :: SCMFSA6B:44
for I being keeping_0 parahalting Macro-Instruction,
J being parahalting Macro-Instruction
holds
IExec(I ';' J,s) =
IExec(J,IExec(I,s)) +* Start-At (IC IExec(J,IExec(I,s)) + card I);