Structure MachineTransitionTheory
signature MachineTransitionTheory =
sig
type thm = Thm.thm
(* Definitions *)
val ChoosePath_def : thm
val Eq_def : thm
val FinPath_curried_def : thm
val FinPath_tupled_primitive_def : thm
val FnPair_def : thm
val IsTrace_curried_def : thm
val IsTrace_tupled_primitive_def : thm
val Live_def : thm
val MooreTrans_def : thm
val Moore_def : thm
val Next_def : thm
val Path_def : thm
val Prev_def : thm
val ReachBy_def : thm
val ReachIn_def : thm
val Reachable_def : thm
val Stable_def : thm
val Total_def : thm
val Totalise_def : thm
(* Theorems *)
val ABS_EXISTS_THM : thm
val ABS_ONE_ONE : thm
val COND_SIMP : thm
val EQ_COND : thm
val EXISTS_IMP_EQ : thm
val EXISTS_REP : thm
val FORALL_REP : thm
val FinFunEq : thm
val FinPathLemma : thm
val FinPathPathExists : thm
val FinPathThm : thm
val FinPath_def : thm
val FinPath_ind : thm
val FnPairAbs : thm
val FnPairExists : thm
val FnPairForall : thm
val IsTrace_def : thm
val IsTrace_ind : thm
val ModelCheckAlways : thm
val ModelCheckAlwaysCor1 : thm
val ModelCheckAlwaysCor2 : thm
val MoorePath : thm
val MooreReachable : thm
val MooreReachable1 : thm
val MooreReachable2 : thm
val MooreReachableCor1 : thm
val MooreReachableExists : thm
val MooreTransEq : thm
val ReachBy_ReachIn : thm
val ReachBy_fixedpoint : thm
val ReachBy_rec : thm
val ReachInFinPath : thm
val ReachInPath : thm
val ReachIn_rec : thm
val ReachIn_revrec : thm
val ReachableFinPath : thm
val ReachableMooreTrans : thm
val ReachablePath : thm
val ReachablePathThm : thm
val ReachableTotalise : thm
val Reachable_ReachBy : thm
val Reachable_Stable : thm
val TotalImpTotalise : thm
val TotalImpTotaliseLemma : thm
val TotalMooreTrans : thm
val TotalPathExists : thm
val TotalTotalise : thm
val TotaliseReachBy : thm
val TraceReachIn : thm
val MachineTransition_grammars : type_grammar.grammar * term_grammar.grammar
(*
[list] Parent theory of "MachineTransition"
[ChoosePath_def] Definition
|- (!R s. ChoosePath R s 0 = s) /\
!R s n. ChoosePath R s (SUC n) = @s'. R (ChoosePath R s n,s')
[Eq_def] Definition
|- !state0 state. Eq state0 state = (state0 = state)
[FinPath_curried_def] Definition
|- !x x1 x2. FinPath x x1 x2 = FinPath_tupled (x,x1,x2)
[FinPath_tupled_primitive_def] Definition
|- FinPath_tupled =
WFREC (@R'. WF R' /\ !n f s R. R' ((R,s),f,n) ((R,s),f,SUC n))
(\FinPath_tupled a.
case a of
((R,s),f,0) -> I (f 0 = s)
|| ((R,s),f,SUC n) ->
I (FinPath_tupled ((R,s),f,n) /\ R (f n,f (n + 1))))
[FnPair_def] Definition
|- !f g x. FnPair f g x = (f x,g x)
[IsTrace_curried_def] Definition
|- !x x1 x2 x3. IsTrace x x1 x2 x3 = IsTrace_tupled (x,x1,x2,x3)
[IsTrace_tupled_primitive_def] Definition
|- IsTrace_tupled =
WFREC
(@R'. WF R' /\ !s0 B tr Q s1 R. R' (R,Eq s1,Q,s1::tr) (R,B,Q,s0::s1::tr))
(\IsTrace_tupled a.
case a of
(R,B,Q,[]) -> I F
|| (R,B,Q,[s]) -> I (B s /\ Q s)
|| (R,B,Q,s::s1::tr) ->
I (B s /\ R (s,s1) /\ IsTrace_tupled (R,Eq s1,Q,s1::tr)))
[Live_def] Definition
|- !R. Live R = !state. ?state'. R (state,state')
[MooreTrans_def] Definition
|- !nextfn input state input' state'.
MooreTrans nextfn ((input,state),input',state') =
(state' = nextfn (input,state))
[Moore_def] Definition
|- !nextfn inputs states.
Moore nextfn (inputs,states) =
!t. states (t + 1) = nextfn (inputs t,states t)
[Next_def] Definition
|- !R B state. Next R B state = ?state_. B state_ /\ R (state_ ,state)
[Path_def] Definition
|- !R s f. Path (R,s) f = (f 0 = s) /\ !n. R (f n,f (n + 1))
[Prev_def] Definition
|- !R Q state. Prev R Q state = ?state'. R (state,state') /\ Q state'
[ReachBy_def] Definition
|- !R B n state. ReachBy R B n state = ?m. m <= n /\ ReachIn R B m state
[ReachIn_def] Definition
|- (!R B. ReachIn R B 0 = B) /\
!R B n. ReachIn R B (SUC n) = Next R (ReachIn R B n)
[Reachable_def] Definition
|- !R B state. Reachable R B state = ?n. ReachIn R B n state
[Stable_def] Definition
|- !R state. Stable R state = !state'. R (state,state') ==> (state' = state)
[Total_def] Definition
|- !R. Total R = !s. ?s'. R (s,s')
[Totalise_def] Definition
|- !R s s'. Totalise R (s,s') = R (s,s') \/ ~(?s''. R (s,s'')) /\ (s = s')
[ABS_EXISTS_THM] Theorem
|- !P rep.
TYPE_DEFINITION P rep ==>
?abs. (!a. abs (rep a) = a) /\ !r. P r = (rep (abs r) = r)
[ABS_ONE_ONE] Theorem
|- !abs rep.
(!a. abs (rep a) = a) /\ (!r. range r = (rep (abs r) = r)) ==>
!r. range r /\ range r' ==> ((abs r = abs r') = (r = r'))
[COND_SIMP] Theorem
|- ((if b then F else F) = F) /\ ((if b then F else T) = ~b) /\
((if b then T else F) = b) /\ ((if b then T else T) = T) /\
((if b then x else x) = x) /\ ((if b then b' else ~b') = (b = b')) /\
((if b then ~b' else b') = (b = ~b'))
[EQ_COND] Theorem
|- ((x = (if b then y else z)) = (if b then x = y else x = z)) /\
(((if b then y else z) = x) = (if b then y = x else z = x))
[EXISTS_IMP_EQ] Theorem
|- (?x. P x) ==> Q = !x. P x ==> Q
[EXISTS_REP] Theorem
|- !abs rep P Q.
(!a. abs (rep a) = a) /\ (!r. P r = (rep (abs r) = r)) ==>
((?a. Q a) = ?r. P r /\ Q (abs r))
[FORALL_REP] Theorem
|- !abs rep P Q.
(!a. abs (rep a) = a) /\ (!r. P r = (rep (abs r) = r)) ==>
((!a. Q a) = !r. P r ==> Q (abs r))
[FinFunEq] Theorem
|- (!m. m <= n + 1 ==> (f1 m = f2 m)) =
(!m. m <= n ==> (f1 m = f2 m)) /\ (f1 (n + 1) = f2 (n + 1))
[FinPathLemma] Theorem
|- !f1 f2 n.
(!m. m <= n ==> (f1 m = f2 m)) ==>
(FinPath (R,s) f1 n = FinPath (R,s) f2 n)
[FinPathPathExists] Theorem
|- !R B f s n.
Total R /\ FinPath (R,s) f n ==>
?g. (!m. m <= n ==> (f m = g m)) /\ Path (R,s) g
[FinPathThm] Theorem
|- !n. FinPath (R,s) f n = (f 0 = s) /\ !m. m < n ==> R (f m,f (m + 1))
[FinPath_def] Theorem
|- (FinPath (R,s) f 0 = (f 0 = s)) /\
(FinPath (R,s) f (SUC n) = FinPath (R,s) f n /\ R (f n,f (n + 1)))
[FinPath_ind] Theorem
|- !P.
(!R s f. P (R,s) f 0) /\ (!R s f n. P (R,s) f n ==> P (R,s) f (SUC n)) ==>
!v v1 v2 v3. P (v,v1) v2 v3
[FnPairAbs] Theorem
|- (!tr. FnPair (\n. FST (tr n)) (\n. SND (tr n)) = tr) /\
!tr1 tr2. (\n. (tr1 n,tr2 n)) = FnPair tr1 tr2
[FnPairExists] Theorem
|- !P. (?tr. P tr) = ?tr1 tr2. P (FnPair tr1 tr2)
[FnPairForall] Theorem
|- !P. (!tr. P tr) = !tr1 tr2. P (FnPair tr1 tr2)
[IsTrace_def] Theorem
|- (IsTrace R B Q [] = F) /\ (IsTrace R B Q [s] = B s /\ Q s) /\
(IsTrace R B Q (s0::s1::tr) =
B s0 /\ R (s0,s1) /\ IsTrace R (Eq s1) Q (s1::tr))
[IsTrace_ind] Theorem
|- !P.
(!R B Q. P R B Q []) /\ (!R B Q s. P R B Q [s]) /\
(!R B Q s0 s1 tr. P R (Eq s1) Q (s1::tr) ==> P R B Q (s0::s1::tr)) ==>
!v v1 v2 v3. P v v1 v2 v3
[ModelCheckAlways] Theorem
|- !R B P.
(!s. Reachable R B s ==> P s) ==>
!tr. B (tr 0) /\ (!t. R (tr t,tr (t + 1))) ==> !t. P (tr t)
[ModelCheckAlwaysCor1] Theorem
|- (!s1 s2. Reachable R B (s1,s2) ==> P s1) ==>
!tr. B (tr 0) /\ (!t. R (tr t,tr (t + 1))) ==> !t. P (FST (tr t))
[ModelCheckAlwaysCor2] Theorem
|- !R B P.
(!s1 s2. Reachable R B (s1,s2) ==> P s1) ==>
!tr1.
(?tr2.
B (tr1 0,tr2 0) /\ !t. R ((tr1 t,tr2 t),tr1 (t + 1),tr2 (t + 1))) ==>
!t. P (tr1 t)
[MoorePath] Theorem
|- Moore nextfn (inputs,states) =
Path (MooreTrans nextfn,inputs 0,states 0) (\t. (inputs t,states t))
[MooreReachable] Theorem
|- !B nextfn P.
(!inputs states.
B (inputs 0,states 0) /\ Moore nextfn (inputs,states) ==>
!t. P (inputs t,states t)) =
!s. Reachable (MooreTrans nextfn) B s ==> P s
[MooreReachable1] Theorem
|- (!inputs states.
B (inputs 0,states 0) /\ Moore nextfn (inputs,states) ==>
!t. P (inputs t,states t)) ==>
!s. Reachable (MooreTrans nextfn) B s ==> P s
[MooreReachable2] Theorem
|- (!s. Reachable (MooreTrans nextfn) B s ==> P s) ==>
!inputs states.
B (inputs 0,states 0) /\ Moore nextfn (inputs,states) ==>
!t. P (inputs t,states t)
[MooreReachableCor1] Theorem
|- !B nextfn.
(!inputs states.
B (inputs 0,states 0) /\
(!t. states (t + 1) = nextfn (inputs t,states t)) ==>
!t. P (inputs t,states t)) =
!s. Reachable (\((i,s),i',s'). s' = nextfn (i,s)) B s ==> P s
[MooreReachableExists] Theorem
|- (?inputs states.
(B (inputs 0,states 0) /\ Moore nextfn (inputs,states)) /\
?t. P (inputs t,states t)) =
?s. Reachable (MooreTrans nextfn) B s /\ P s
[MooreTransEq] Theorem
|- MooreTrans nextfn =
(\((input,state),input',state'). state' = nextfn (input,state))
[ReachBy_ReachIn] Theorem
|- (!R B state. ReachBy R B 0 state = B state) /\
!R B n state.
ReachBy R B (SUC n) state =
ReachBy R B n state \/ ReachIn R B (SUC n) state
[ReachBy_fixedpoint] Theorem
|- !R B n.
(ReachBy R B n = ReachBy R B (SUC n)) ==> (Reachable R B = ReachBy R B n)
[ReachBy_rec] Theorem
|- (!R B state. ReachBy R B 0 state = B state) /\
!R B n state.
ReachBy R B (SUC n) state =
ReachBy R B n state \/ ?state_. ReachBy R B n state_ /\ R (state_ ,state)
[ReachInFinPath] Theorem
|- !R B n s. ReachIn R B n s = ?f s0. B s0 /\ FinPath (R,s0) f n /\ (s = f n)
[ReachInPath] Theorem
|- !R B n s.
Total R ==> (ReachIn R B n s = ?f s0. B s0 /\ Path (R,s0) f /\ (s = f n))
[ReachIn_rec] Theorem
|- (!R B state. ReachIn R B 0 state = B state) /\
!R B n state.
ReachIn R B (SUC n) state =
?state_. ReachIn R B n state_ /\ R (state_ ,state)
[ReachIn_revrec] Theorem
|- (!R B state. ReachIn R B 0 state = B state) /\
!R B n state.
ReachIn R B (SUC n) state =
?state1 state2.
B state1 /\ R (state1,state2) /\ ReachIn R (Eq state2) n state
[ReachableFinPath] Theorem
|- !R B s. Reachable R B s = ?f s0 n. B s0 /\ FinPath (R,s0) f n /\ (s = f n)
[ReachableMooreTrans] Theorem
|- !B s.
Reachable (MooreTrans nextfn) B s =
?f s0. B s0 /\ Path (MooreTrans nextfn,s0) f /\ ?n. s = f n
[ReachablePath] Theorem
|- !R B s.
Total R ==>
(Reachable R B s = ?f s0. B s0 /\ Path (R,s0) f /\ ?n. s = f n)
[ReachablePathThm] Theorem
|- !R B s.
Reachable R B s = ?f s0. B s0 /\ Path (Totalise R,s0) f /\ ?n. s = f n
[ReachableTotalise] Theorem
|- Reachable (Totalise R) = Reachable R
[Reachable_ReachBy] Theorem
|- Reachable R B state = ?n. ReachBy R B n state
[Reachable_Stable] Theorem
|- Live R /\ (!state. ReachIn R B n state ==> Stable R state) ==>
!state. Reachable R B state /\ Stable R state = ReachIn R B n state
[TotalImpTotalise] Theorem
|- Total R ==> (Totalise R = R)
[TotalImpTotaliseLemma] Theorem
|- Total R ==> !s s'. R (s,s') = Totalise R (s,s')
[TotalMooreTrans] Theorem
|- Total (MooreTrans nextfn)
[TotalPathExists] Theorem
|- Total R ==> !s. Path (R,s) (ChoosePath R s)
[TotalTotalise] Theorem
|- Total (Totalise R)
[TotaliseReachBy] Theorem
|- !n s. ReachBy (Totalise R) B n s = ReachBy R B n s
[TraceReachIn] Theorem
|- !R B tr. B (tr 0) /\ (!n. R (tr n,tr (n + 1))) ==> !n. ReachIn R B n (tr n)
*)
end
HOL 4, Kananaskis-3