:: On state machines of calculating type
:: by Hisayoshi Kunimune , Grzegorz Bancerek and Yatsuka Nakamura
::
:: Received December 3, 2001
:: Copyright (c) 2001-2021 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, REAL_1, XBOOLE_0, SUBSET_1, FINSEQ_1, FSM_1, ARYTM_3,
FUNCT_1, XXREAL_0, ORDINAL4, FINSEQ_3, TARSKI, RELAT_1, PARTFUN1, CARD_1,
NAT_1, CARD_5, ZFMISC_1, ARYTM_1, STRUCT_0, GLIB_000, FUNCOP_1, BINOP_1,
ORDINAL1, ABSVALUE, MSUALG_1, FSM_2, FUNCT_7, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0,
XCMPLX_0, XREAL_0, REAL_1, ABSVALUE, NAT_1, DOMAIN_1, FUNCT_1, PARTFUN1,
FUNCT_2, BINOP_1, FUNCOP_1, FINSEQ_1, FINSEQ_3, FINSEQ_4, STRUCT_0,
FSM_1;
constructors REAL_1, SQUARE_1, ABSVALUE, FUNCOP_1, FINSEQ_3, FINSEQ_4,
BORSUK_1, FSM_1, VALUED_1, BINOP_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0,
NAT_1, FINSEQ_1, NAT_2, STRUCT_0, FSM_1, XREAL_0, CARD_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Calculating type
reserve x,y for Real,
i, j for non zero Element of NAT,
I, O for non empty set,
s,s1,s2,s3 for Element of I,
w, w1, w2 for FinSequence of I,
t for Element of O,
S for non empty FSM over I,
q, q1 for State of S;
notation
let I, S, q, w;
synonym GEN(w,q) for (q,w)-admissible;
end;
registration
let I, S, q, w;
cluster GEN(w, q) -> non empty;
end;
theorem :: FSM_2:1
GEN(<*s*>, q) = <*q, (the Tran of S).[q, s]*>;
theorem :: FSM_2:2
GEN(<*s1,s2*>, q) = <*q, (the Tran of S).[q, s1],
(the Tran of S).[(the Tran of S).[q, s1], s2]*>;
theorem :: FSM_2:3
GEN(<*s1,s2,s3*>, q) = <*q, (the Tran of S).[q, s1],
(the Tran of S).[(the Tran of S).[q, s1], s2],
(the Tran of S).[(the Tran of S).[(the Tran of S).[q, s1], s2],s3] *>;
definition
let I, S;
attr S is calculating_type means
:: FSM_2:def 1
for j holds for w1, w2 st w1.1 = w2.1 & j <= len(w1)+1 &
j <= len(w2)+1 holds GEN(w1, the InitS of S).j = GEN(w2, the InitS of S).j;
end;
theorem :: FSM_2:4
S is calculating_type implies for w1, w2 st w1.1 = w2.1 holds
GEN(w1, the InitS of S), GEN(w2, the InitS of S) are_c=-comparable;
theorem :: FSM_2:5
(for w1, w2 st w1.1 = w2.1 holds
GEN(w1, the InitS of S), GEN(w2, the InitS of S) are_c=-comparable)
implies S is calculating_type;
theorem :: FSM_2:6
S is calculating_type implies
for w1, w2 st w1.1 = w2.1 & len w1 = len w2 holds
GEN(w1, the InitS of S) = GEN(w2, the InitS of S);
theorem :: FSM_2:7
(for w1, w2 st w1.1 = w2.1 & len w1 = len w2 holds
GEN(w1, the InitS of S) = GEN(w2, the InitS of S))
implies S is calculating_type;
definition
let I, S, q, s;
pred q is_accessible_via s means
:: FSM_2:def 2
ex w be FinSequence of I st the InitS of S,<*s*>^w-leads_to q;
end;
definition
let I, S, q;
attr q is accessible means
:: FSM_2:def 3
ex w be FinSequence of I st the InitS of S,w-leads_to q;
end;
theorem :: FSM_2:8
q is_accessible_via s implies q is accessible;
theorem :: FSM_2:9
q is accessible & q <> the InitS of S implies ex s st q is_accessible_via s;
theorem :: FSM_2:10
the InitS of S is accessible;
theorem :: FSM_2:11
S is calculating_type & q is_accessible_via s implies
ex m being non zero Element of NAT st
for w st len w+1 >= m & w.1 = s holds q = GEN(w, the InitS of S).m &
for i st i < m holds GEN(w, the InitS of S).i <> q;
definition
let I, S;
attr S is regular means
:: FSM_2:def 4
for q being State of S holds q is accessible;
end;
theorem :: FSM_2:12
(for s1,s2,q holds (the Tran of S).[q,s1] = (the Tran of S).[ q,s2]) implies
S is calculating_type;
theorem :: FSM_2:13
for S st (for s1,s2,q st q<>the InitS of S holds
(the Tran of S).[q,s1] = (the Tran of S).[q,s2]) & for s,q1 holds
(the Tran of S).[q1,s] <> the InitS of S holds S is calculating_type;
theorem :: FSM_2:14
S is regular & S is calculating_type implies
for s1, s2, q st q<>the InitS of S holds GEN(<*s1*>,q).2 = GEN(<*s2*>,q).2;
theorem :: FSM_2:15
S is regular & S is calculating_type implies
for s1, s2, q st q<>the InitS of S holds
(the Tran of S).[q,s1] = (the Tran of S).[q,s2];
theorem :: FSM_2:16
S is regular & S is calculating_type implies for s, s1, s2, q st
(the Tran of S).[the InitS of S,s1] <>
(the Tran of S).[the InitS of S,s2] holds
(the Tran of S).[q,s] <> the InitS of S;
begin :: Machines with final states
definition
let I be set;
struct (FSM over I) SM_Final over I (# carrier -> set,
Tran -> Function of [: the carrier, I :], the carrier,
InitS -> Element of the carrier, FinalS -> Subset of the carrier #);
end;
registration
let I be set;
cluster non empty for SM_Final over I;
end;
definition
let I, s;
let S be non empty SM_Final over I;
pred s leads_to_final_state_of S means
:: FSM_2:def 5
ex q being State of S st q is_accessible_via s & q in the FinalS of S;
end;
definition
let I;
let S be non empty SM_Final over I;
attr S is halting means
:: FSM_2:def 6
s leads_to_final_state_of S;
end;
definition
let I be set, O be non empty set;
struct (SM_Final over I, Moore-FSM over I, O) Moore-SM_Final over I,O (#
carrier -> set, Tran -> Function of [: the carrier, I :], the carrier,
OFun -> Function of the carrier, O, InitS -> Element of the carrier,
FinalS -> Subset of the carrier #);
end;
registration
let I be set, O be non empty set;
cluster non empty strict for Moore-SM_Final over I, O;
end;
definition
let I, O;
let i,f be set;
let o be Function of {i,f}, O;
func I-TwoStatesMooreSM(i,f,o) -> non empty strict Moore-SM_Final over I, O
means
:: FSM_2:def 7
the carrier of it = {i,f} &
the Tran of it = [:{i,f}, I :] --> f & the OFun of it = o &
the InitS of it = i & the FinalS of it = {f};
end;
theorem :: FSM_2:17
for i,f being set, o being Function of {i,f}, O
for j st 1 < j & j <= len w+1 holds
GEN(w, the InitS of I-TwoStatesMooreSM(i,f,o)).j = f;
registration
let I, O;
let i,f be set;
let o be Function of {i,f}, O;
cluster I-TwoStatesMooreSM(i,f,o) -> calculating_type;
end;
registration
let I, O;
let i,f be set;
let o be Function of {i,f}, O;
cluster I-TwoStatesMooreSM(i,f,o) -> halting;
end;
reserve n, m, o, p for non zero Element of NAT,
M for non empty Moore-SM_Final over I, O,
q for State of M;
theorem :: FSM_2:18
M is calculating_type & s leads_to_final_state_of M implies
ex m being non zero Element of NAT st
(for w st len w+1 >= m & w.1 = s holds
GEN(w, the InitS of M).m in the FinalS of M) &
for w,j st j <= len w +1 & w.1 = s & j < m holds
not GEN(w, the InitS of M).j in the FinalS of M;
begin :: Correctness of a result of state machine
definition
let I, O, M, s;
let t be object;
pred t is_result_of s,M means
:: FSM_2:def 8
ex m st for w st w.1=s holds
(m <= len w+1 implies t = (the OFun of M).(GEN(w, the InitS of M).m) &
GEN(w, the InitS of M).m in the FinalS of M) &
for n st n < m & n <= len w+1 holds
not GEN(w, the InitS of M).n in the FinalS of M;
end;
theorem :: FSM_2:19
the InitS of M in the FinalS of M implies
(the OFun of M).the InitS of M is_result_of s, M;
theorem :: FSM_2:20
M is calculating_type & s leads_to_final_state_of M
implies ex t st t is_result_of s, M;
theorem :: FSM_2:21
s leads_to_final_state_of M implies
for t1, t2 being Element of O st t1 is_result_of s, M & t2 is_result_of s, M
holds t1 = t2;
theorem :: FSM_2:22
for X being non empty set for f being BinOp of X
for M being non empty Moore-SM_Final over [:X, X:], succ X
st M is calculating_type & the carrier of M = succ X & the FinalS of M = X &
the InitS of M = X & the OFun of M = id the carrier of M &
for x,y being Element of X holds
(the Tran of M).[the InitS of M, [x,y]] = f.(x,y) holds M is halting &
for x,y being Element of X holds f.(x,y) is_result_of [x,y], M;
theorem :: FSM_2:23
for M being non empty Moore-SM_Final over [:REAL, REAL:], succ REAL
st M is calculating_type & the carrier of M = succ REAL &
the FinalS of M = REAL & the InitS of M = REAL &
the OFun of M = id the carrier of M &
(for x,y st x >= y holds (the Tran of M).[the InitS of M, [x,y]] = x) &
(for x,y st x < y holds (the Tran of M).[the InitS of M, [x,y]] = y)
for x,y being Element of REAL holds max(x,y) is_result_of [x,y], M;
theorem :: FSM_2:24
for M being non empty Moore-SM_Final over [:REAL, REAL:], succ REAL
st M is calculating_type & the carrier of M = succ REAL &
the FinalS of M = REAL & the InitS of M = REAL &
the OFun of M = id the carrier of M &
(for x,y st x < y holds (the Tran of M).[the InitS of M, [x,y]] = x) &
(for x,y st x >= y holds (the Tran of M).[the InitS of M, [x,y]] = y)
for x,y being Element of REAL holds min(x,y) is_result_of [x,y], M;
theorem :: FSM_2:25
for M being non empty Moore-SM_Final over [:REAL, REAL:], succ REAL
st M is calculating_type & the carrier of M = succ REAL &
the FinalS of M = REAL & the InitS of M = REAL &
the OFun of M = id the carrier of M &
(for x,y holds (the Tran of M).[the InitS of M, [x,y]] = x+y)
for x,y being Element of REAL holds x+y is_result_of [x,y], M;
theorem :: FSM_2:26
for M being non empty Moore-SM_Final over [:REAL, REAL:], succ REAL
st M is calculating_type & the carrier of M = succ REAL &
the FinalS of M = REAL & the InitS of M = REAL &
the OFun of M = id the carrier of M &
(for x,y st x>0 or y>0 holds (the Tran of M).[the InitS of M, [x,y]] = 1) &
(for x,y st (x=0 or y=0) & x <= 0 & y <=0
holds (the Tran of M).[the InitS of M, [x,y]] = 0) &
(for x,y st x<0 & y<0 holds (the Tran of M).[the InitS of M, [x,y]] = -1)
for x,y being Element of REAL holds max(sgn x,sgn y) is_result_of [x,y], M;
registration
let I, O;
cluster calculating_type halting for non empty Moore-SM_Final over I, O;
end;
registration
let I;
cluster calculating_type halting for non empty SM_Final over I;
end;
definition
let I, O;
let M be calculating_type halting non empty Moore-SM_Final over I, O;
let s;
func Result(s, M) -> Element of O means
:: FSM_2:def 9
it is_result_of s, M;
end;
theorem :: FSM_2:27
for f being Function of {0, 1}, O holds
Result(s, I-TwoStatesMooreSM(0,1,f)) = f.1;
theorem :: FSM_2:28
for M being calculating_type halting
non empty Moore-SM_Final over [:REAL, REAL:], succ REAL
st the carrier of M = succ REAL & the FinalS of M = REAL &
the InitS of M = REAL & the OFun of M = id the carrier of M &
(for x,y st x >= y holds (the Tran of M).[the InitS of M, [x,y]] = x) &
(for x,y st x < y holds (the Tran of M).[the InitS of M, [x,y]] = y)
for x,y being Element of REAL holds Result([x,y], M) = max(x,y);
theorem :: FSM_2:29
for M being calculating_type halting
non empty Moore-SM_Final over [:REAL, REAL:], succ REAL
st the carrier of M = succ REAL & the FinalS of M = REAL &
the InitS of M = REAL & the OFun of M = id the carrier of M &
(for x,y st x < y holds (the Tran of M).[the InitS of M, [x,y]] = x) &
(for x,y st x >= y holds (the Tran of M).[the InitS of M, [x,y]] = y)
for x,y being Element of REAL holds Result([x,y], M) = min(x,y);
theorem :: FSM_2:30
for M being calculating_type halting
non empty Moore-SM_Final over [:REAL, REAL:], succ REAL
st the carrier of M = succ REAL & the FinalS of M = REAL &
the InitS of M = REAL & the OFun of M = id the carrier of M &
(for x,y holds (the Tran of M).[the InitS of M, [x,y]] = x+y)
for x,y being Element of REAL holds Result([x,y], M) = x+y;
theorem :: FSM_2:31
for M being calculating_type halting
non empty Moore-SM_Final over [:REAL, REAL:], succ REAL
st the carrier of M = succ REAL & the FinalS of M = REAL &
the InitS of M = REAL & the OFun of M = id the carrier of M &
(for x,y st x>0 or y>0 holds (the Tran of M).[the InitS of M, [x,y]] = 1) &
(for x,y st (x=0 or y=0) & x <= 0 & y <=0
holds (the Tran of M).[the InitS of M, [x,y]] = 0) &
(for x,y st x<0 & y<0 holds (the Tran of M).[the InitS of M, [x,y]] = -1)
for x,y being Element of REAL holds Result([x,y], M) = max(sgn x, sgn y);