(*
File: TLA/TLA.thy
Author: Stephan Merz
Copyright: 1998 University of Munich
Theory Name: TLA
Logic Image: HOL
The temporal level of TLA.
*)
TLA = Init +
consts
(** abstract syntax **)
Box :: ('w::world) form => temporal
Dmd :: ('w::world) form => temporal
leadsto :: ['w::world form, 'v::world form] => temporal
Stable :: stpred => temporal
WF :: [action, 'a stfun] => temporal
SF :: [action, 'a stfun] => temporal
(* Quantification over (flexible) state variables *)
EEx :: ('a stfun => temporal) => temporal (binder "Eex " 10)
AAll :: ('a stfun => temporal) => temporal (binder "Aall " 10)
(** concrete syntax **)
syntax
"_Box" :: lift => lift ("([]_)" [40] 40)
"_Dmd" :: lift => lift ("(<>_)" [40] 40)
"_leadsto" :: [lift,lift] => lift ("(_ ~> _)" [23,22] 22)
"_stable" :: lift => lift ("(stable/ _)")
"_WF" :: [lift,lift] => lift ("(WF'(_')'_(_))" [0,60] 55)
"_SF" :: [lift,lift] => lift ("(SF'(_')'_(_))" [0,60] 55)
"_EEx" :: [idts, lift] => lift ("(3EEX _./ _)" [0,10] 10)
"_AAll" :: [idts, lift] => lift ("(3AALL _./ _)" [0,10] 10)
translations
"_Box" == "Box"
"_Dmd" == "Dmd"
"_leadsto" == "leadsto"
"_stable" == "Stable"
"_WF" == "WF"
"_SF" == "SF"
"_EEx v A" == "Eex v. A"
"_AAll v A" == "Aall v. A"
"sigma |= []F" <= "_Box F sigma"
"sigma |= <>F" <= "_Dmd F sigma"
"sigma |= F ~> G" <= "_leadsto F G sigma"
"sigma |= stable P" <= "_stable P sigma"
"sigma |= WF(A)_v" <= "_WF A v sigma"
"sigma |= SF(A)_v" <= "_SF A v sigma"
"sigma |= EEX x. F" <= "_EEx x F sigma"
"sigma |= AALL x. F" <= "_AAll x F sigma"
syntax (symbols)
"_Box" :: lift => lift ("(\\<box>_)" [40] 40)
"_Dmd" :: lift => lift ("(\\<diamond>_)" [40] 40)
"_leadsto" :: [lift,lift] => lift ("(_ \\<leadsto> _)" [23,22] 22)
"_EEx" :: [idts, lift] => lift ("(3\\<exists>\\<exists> _./ _)" [0,10] 10)
"_AAll" :: [idts, lift] => lift ("(3\\<forall>\\<forall> _./ _)" [0,10] 10)
rules
(* Definitions of derived operators *)
dmd_def "TEMP <>F == TEMP ~[]~F"
boxInit "TEMP []F == TEMP []Init F"
leadsto_def "TEMP F ~> G == TEMP [](Init F --> <>G)"
stable_def "TEMP stable P == TEMP []($P --> P$)"
WF_def "TEMP WF(A)_v == TEMP <>[] Enabled(<A>_v) --> []<><A>_v"
SF_def "TEMP SF(A)_v == TEMP []<> Enabled(<A>_v) --> []<><A>_v"
aall_def "TEMP (AALL x. F x) == TEMP ~ (EEX x. ~ F x)"
(* Base axioms for raw TLA. *)
normalT "|- [](F --> G) --> ([]F --> []G)" (* polymorphic *)
reflT "|- []F --> F" (* F::temporal *)
transT "|- []F --> [][]F" (* polymorphic *)
linT "|- <>F & <>G --> (<>(F & <>G)) | (<>(G & <>F))"
discT "|- [](F --> <>(~F & <>F)) --> (F --> []<>F)"
primeI "|- []P --> Init P`"
primeE "|- [](Init P --> []F) --> Init P` --> (F --> []F)"
indT "|- [](Init P & ~[]F --> Init P` & F) --> Init P --> []F"
allT "|- (! x. [](F x)) = ([](! x. F x))"
necT "|- F ==> |- []F" (* polymorphic *)
(* Flexible quantification: refinement mappings, history variables *)
eexI "|- F x --> (EEX x. F x)"
eexE "[| sigma |= (EEX x. F x); basevars vs;
(!!x. [| basevars (x, vs); sigma |= F x |] ==> (G sigma)::bool)
|] ==> G sigma"
history "|- EEX h. Init(h = ha) & [](!x. $h = #x --> h` = hb x)"
end