:: Weakly Standard Ordering of Instruction Locations
:: by Andrzej Trybulec , Piotr Rudnicki and Artur Korni{\l}owicz
::
:: Received April 22, 2010
:: Copyright (c) 2010-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 NUMBERS, XBOOLE_0, SUBSET_1, AMI_1, FSM_1, FUNCT_4, FUNCOP_1,
RELAT_1, TARSKI, FUNCT_1, CARD_3, ZFMISC_1, CIRCUIT2, NAT_1, GLIB_000,
XXREAL_0, PARTFUN1, FINSEQ_1, ARYTM_3, GRAPH_2, CARD_1, FUNCT_2,
FINSEQ_4, ARYTM_1, FINSET_1, FRECHET, WAYBEL_0, MEMBERED, AMISTD_1,
EXTPRO_1, AMI_WSTD, STRUCT_0, COMPOS_1, QUANTAL1, GOBRD13, MEMSTR_0,
FUNCT_7, ORDINAL1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, ORDINAL1,
CARD_1, XXREAL_0, NUMBERS, XCMPLX_0, NAT_1, MEMBERED, FUNCT_1, RELSET_1,
PARTFUN1, DOMAIN_1, CARD_3, FINSEQ_1, FINSEQ_4, FUNCOP_1, FINSET_1,
FUNCT_4, FUNCT_7, MEASURE6, STRUCT_0, GRAPH_2, NAT_D, XXREAL_2, MEMSTR_0,
COMPOS_0, COMPOS_1, EXTPRO_1, FUNCT_2, AMISTD_1;
constructors WELLORD2, REAL_1, FINSEQ_4, REALSET1, NAT_D, XXREAL_2, RELSET_1,
PRE_POLY, GRAPH_2, AMISTD_1, FUNCT_7, FUNCT_4, PBOOLE, XTUPLE_0;
registrations RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSET_1,
XREAL_0, NAT_1, MEMBERED, FINSEQ_1, CARD_3, FUNCT_7, JORDAN1J, CARD_1,
XXREAL_2, RELSET_1, FUNCT_4, AMISTD_1, EXTPRO_1, PRE_POLY, MEMSTR_0,
MEASURE6, COMPOS_0, XTUPLE_0, ORDINAL1;
requirements NUMERALS, BOOLE, REAL, SUBSET, ARITHM;
begin :: Ami-Struct
reserve x for set,
D for non empty set,
k, n for Element of NAT,
z for Nat;
reserve N for with_zero set,
S for
IC-Ins-separated non empty with_non-empty_values AMI-Struct over N,
i for Element of the InstructionsF of S,
l, l1, l2, l3 for Element of NAT,
s for State of S;
reserve ss for Element of product the_Values_of S;
begin :: Ordering of Instruction Locations
definition
let N,S; let l1,l2 be Nat;
pred l1 <= l2, S means
:: AMI_WSTD:def 1
ex f being non empty FinSequence of NAT st f/.1
= l1 & f/.len f = l2 & for n st 1 <= n & n < len f
holds f/.(n+1) in SUCC(f/.n,S);
end;
theorem :: AMI_WSTD:1
for N,S for l1,l2 being Nat holds
l1 <= l2,S & l2 <= l3, S implies l1 <= l3, S;
definition
let N, S;
attr S is InsLoc-antisymmetric means
:: AMI_WSTD:def 2
for l1, l2 st l1 <= l2, S & l2 <= l1, S holds
l1 = l2;
end;
definition
let N, S;
attr S is weakly_standard means
:: AMI_WSTD:def 3
ex f being sequence of NAT st f is
bijective & for m, n being Element of NAT holds m <= n iff f.m <= f.n, S;
end;
theorem :: AMI_WSTD:2
for f1, f2 being sequence of NAT st f1 is bijective & (for
m, n being Element of NAT holds m <= n iff f1.m <= f1.n,S) & f2 is bijective &
(for m, n being Element of NAT holds m <= n iff f2.m <= f2.n, S) holds f1 = f2
;
theorem :: AMI_WSTD:3
for f being sequence of NAT st f is bijective holds
(for m, n being Element of NAT holds m <= n iff f.m <= f.n, S)
iff for k being Element of NAT holds f.(k+1) in SUCC(f.k,S) &
for j being Element of NAT st f.j in SUCC(f.k,S) holds k <= j;
theorem :: AMI_WSTD:4
S is weakly_standard iff ex f being sequence of NAT st f is
bijective & for k being Element of NAT holds f.(k+1) in SUCC(f.k,S) & for j
being Element of NAT st f.j in SUCC(f.k,S) holds k <= j;
begin
registration
let N be with_zero set;
cluster STC N -> weakly_standard;
end;
registration
let N be with_zero set;
cluster weakly_standard halting
for IC-Ins-separated non empty with_non-empty_values AMI-Struct
over N;
end;
reserve T for weakly_standard
IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N;
definition
let N be with_zero set,
S be weakly_standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N, k be natural Number;
func il.(S,k) -> Element of NAT means
:: AMI_WSTD:def 4
ex f being
sequence of NAT st f is bijective & (for m, n being Element of NAT holds
m <= n iff f.m <= f.n, S) & it = f.k;
end;
theorem :: AMI_WSTD:5
for N,T
for k1, k2 being Nat st il.(T,k1) = il.(T,k2) holds
k1 = k2;
theorem :: AMI_WSTD:6
for l being Nat ex k being Nat st l = il.(T,k);
definition
let N be with_zero set,
S be weakly_standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N, l be Nat;
func locnum(l,S) -> Nat means
:: AMI_WSTD:def 5
il.(S,it) = l;
end;
definition
let N be with_zero set,
S be weakly_standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N, l be Nat;
redefine func locnum(l,S) -> Element of NAT;
end;
theorem :: AMI_WSTD:7
for l1, l2 being Element of NAT holds locnum(l1,T) =
locnum(l2,T) implies l1 = l2;
theorem :: AMI_WSTD:8
for N,T
for k1, k2 being natural Number holds
il.(T,k1) <= il.(T,k2), T iff k1 <= k2;
theorem :: AMI_WSTD:9
for N,T
for l1, l2 being Element of NAT holds locnum(l1,T) <=
locnum(l2,T) iff l1 <= l2, T;
theorem :: AMI_WSTD:10
for N,T holds T is InsLoc-antisymmetric;
registration
let N;
cluster weakly_standard -> InsLoc-antisymmetric
for IC-Ins-separated non
empty with_non-empty_values AMI-Struct over N;
end;
definition
let N be with_zero set,
S be weakly_standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N, f be
Element of NAT, k be Nat;
func f +(k,S) -> Element of NAT equals
:: AMI_WSTD:def 6
il.(S,locnum(f,S) + k);
end;
theorem :: AMI_WSTD:11
for f being Element of NAT holds f + (0,T) = f;
theorem :: AMI_WSTD:12
for f, g being Element of NAT st f + (z,T) = g + (z,T)
holds f = g;
theorem :: AMI_WSTD:13
for f being Element of NAT
holds locnum(f,T) + z = locnum(f+(z,T),T);
definition
let N be with_zero set,
S be weakly_standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N, f be
Element of NAT;
func NextLoc(f,S) -> Element of NAT equals
:: AMI_WSTD:def 7
f + (1,S);
end;
theorem :: AMI_WSTD:14
for f being Element of NAT
holds NextLoc(f,T) = il.(T,locnum(f,T)+ 1);
theorem :: AMI_WSTD:15
for f being Element of NAT holds f <> NextLoc(f,T);
theorem :: AMI_WSTD:16
for f, g being Element of NAT st NextLoc(f,T) = NextLoc(g,T)
holds f = g;
theorem :: AMI_WSTD:17
il.(STC N, z) = z;
theorem :: AMI_WSTD:18
for i being Instruction of STC N, s being State of STC N st InsCode i
= 1 holds IC Exec(i,s) = NextLoc(IC s,STC N);
theorem :: AMI_WSTD:19
for l being Element of NAT, i being Element of the
InstructionsF of STC N st InsCode i = 1 holds NIC(i, l) = {NextLoc(l,STC N)};
theorem :: AMI_WSTD:20
for l being Element of NAT holds SUCC(l,STC N) = {l, NextLoc(l,STC N)};
definition
let N be with_zero set,
S be weakly_standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N, i be Instruction of
S;
attr i is sequential means
:: AMI_WSTD:def 8
for s being State of S holds Exec(i, s).IC S = NextLoc(IC s,S);
end;
theorem :: AMI_WSTD:21
for S being weakly_standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N, il being Element of NAT,
i being Instruction of S st i is sequential holds NIC(i,il)
= {NextLoc(il,S)};
theorem :: AMI_WSTD:22
for S being weakly_standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N,
i being Instruction of S st i is sequential
holds i is non halting;
registration
let N;
let S be weakly_standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
cluster sequential -> non halting for Instruction of S;
cluster halting -> non sequential for Instruction of S;
end;
begin :: Closedness of finite partial states
definition
let N be with_zero set;
let S be weakly_standard IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N;
let F be NAT-defined (the InstructionsF of S)-valued Function;
attr F is para-closed means
:: AMI_WSTD:def 9
for s being State of S st IC s = il.(S,0)
for k being Element of NAT holds IC Comput(F,s,k) in dom F;
end;
theorem :: AMI_WSTD:23
for S being weakly_standard IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N,
F being NAT-defined (the InstructionsF of S)-valued
finite Function st F is really-closed & il.(S,0) in dom F holds F is
para-closed;
theorem :: AMI_WSTD:24
for S being weakly_standard halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N holds il.(S,0) .-->
halt S qua NAT-defined (the InstructionsF of S)-valued
finite Function is really-closed;
definition
let N be with_zero set;
let S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over
N;
let F be (the InstructionsF of S)-valued NAT-defined finite Function;
attr F is lower means
:: AMI_WSTD:def 10
for l being Element of NAT st l in
dom F holds for m being Element of NAT st m <= l, S
holds m in dom F;
end;
registration
let N be with_zero set,
S be IC-Ins-separated non
empty with_non-empty_values AMI-Struct over N;
cluster empty -> lower
for finite (the InstructionsF of S)-valued NAT-defined Function;
end;
theorem :: AMI_WSTD:25
for i being Element of the InstructionsF of T
holds il.(T,0) .--> i is lower;
registration
let N be with_zero set;
let S be weakly_standard IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N;
cluster lower 1-element for NAT-defined
(the InstructionsF of S)-valued finite Function;
end;
theorem :: AMI_WSTD:26
for F being lower non empty
NAT-defined (the InstructionsF of T)-valued finite Function
holds il.(T,0) in dom F;
theorem :: AMI_WSTD:27
for P being lower
NAT-defined (the InstructionsF of T)-valued finite Function
holds z < card P iff il.(T,z) in dom P;
definition
let N be with_zero set;
let S be weakly_standard IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N;
let F be non empty
NAT-defined (the InstructionsF of S)-valued finite Function;
func LastLoc F -> Element of NAT means
:: AMI_WSTD:def 11
ex M being finite non empty natural-membered set
st M = { locnum(l,S) where l is
Element of NAT : l in dom F } & it = il.(S, max M);
end;
theorem :: AMI_WSTD:28
for F being non empty
NAT-defined (the InstructionsF of T)-valued finite Function
holds LastLoc F in dom F;
theorem :: AMI_WSTD:29
for F, G being non empty
NAT-defined (the InstructionsF of T)-valued finite Function
st F c= G
holds LastLoc F <= LastLoc G, T;
theorem :: AMI_WSTD:30
for F being non empty
NAT-defined (the InstructionsF of T)-valued finite Function,
l being
Element of NAT st l in dom F holds l <= LastLoc F, T;
theorem :: AMI_WSTD:31
for F being lower non empty
NAT-defined (the InstructionsF of T)-valued finite Function,
G being non empty NAT-defined
NAT-defined (the InstructionsF of T)-valued finite Function
holds F c= G & LastLoc F = LastLoc G
implies F = G;
theorem :: AMI_WSTD:32
for F being lower non empty
NAT-defined (the InstructionsF of T)-valued finite Function
holds LastLoc F = il.(T, card F -' 1);
registration
let N be with_zero set,
S be weakly_standard
IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;
cluster really-closed lower non empty -> para-closed for NAT-defined
(the InstructionsF of S)-valued finite Function;
end;
definition
let N be with_zero set,
S be weakly_standard halting
IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, F
be non empty NAT-defined (the InstructionsF of S)-valued finite Function;
attr F is halt-ending means
:: AMI_WSTD:def 12
F.(LastLoc F) = halt S;
attr F is unique-halt means
:: AMI_WSTD:def 13
for f being Element of NAT st
F.f = halt S & f in dom F holds f = LastLoc F;
end;
registration
let N be with_zero set;
let S be weakly_standard halting IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N;
cluster halt-ending unique-halt trivial
for lower non empty
NAT-defined (the InstructionsF of S)-valued finite Function;
end;
registration
let N be with_zero set;
let S be weakly_standard halting IC-Ins-separated
non empty
with_non-empty_values AMI-Struct over N;
cluster trivial really-closed lower non empty
for NAT-defined (the InstructionsF of S)-valued finite Function;
end;
registration
let N be with_zero set;
let S be weakly_standard halting IC-Ins-separated
non empty
with_non-empty_values AMI-Struct over N;
cluster halt-ending unique-halt trivial really-closed
for lower non empty
NAT-defined (the InstructionsF of S)-valued finite Function;
end;
definition
let N be with_zero set;
let S be weakly_standard halting IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N;
mode pre-Macro of S is halt-ending unique-halt
lower non empty
NAT-defined (the InstructionsF of S)-valued finite Function;
end;
registration
let N be with_zero set;
let S be weakly_standard halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
cluster really-closed for pre-Macro of S;
end;
theorem :: AMI_WSTD:33
for N being with_zero set,
S being IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N,
l1, l2 being Element of NAT st SUCC(l1,S) = NAT
holds l1 <= l2, S;
:: from SCMRING4, 2008.03.13, A.T.
reserve i, j, k for Nat,
n for Element of NAT,
N for with_zero set,
S for weakly_standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N,
l for Element of NAT,
f for FinPartState of S;
definition
let N be with_zero set,
S be weakly_standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N, loc be
Element of NAT, k be Nat;
func loc -' (k,S) -> Element of NAT equals
:: AMI_WSTD:def 14
il.(S, (locnum(loc,S)) -' k);
end;
theorem :: AMI_WSTD:34
l -' (0,S) = l;
theorem :: AMI_WSTD:35
l + (k,S) -' (k,S) = l;