3807
|
1 |
(*
|
|
2 |
File: TLA/TLA.thy
|
|
3 |
Author: Stephan Merz
|
6255
|
4 |
Copyright: 1998 University of Munich
|
3807
|
5 |
|
|
6 |
Theory Name: TLA
|
|
7 |
Logic Image: HOL
|
|
8 |
|
|
9 |
The temporal level of TLA.
|
|
10 |
*)
|
|
11 |
|
7562
|
12 |
TLA = Init +
|
3807
|
13 |
|
|
14 |
consts
|
6255
|
15 |
(** abstract syntax **)
|
|
16 |
Box :: ('w::world) form => temporal
|
|
17 |
Dmd :: ('w::world) form => temporal
|
|
18 |
leadsto :: ['w::world form, 'v::world form] => temporal
|
|
19 |
Stable :: stpred => temporal
|
|
20 |
WF :: [action, 'a stfun] => temporal
|
|
21 |
SF :: [action, 'a stfun] => temporal
|
3807
|
22 |
|
|
23 |
(* Quantification over (flexible) state variables *)
|
6255
|
24 |
EEx :: ('a stfun => temporal) => temporal (binder "Eex " 10)
|
|
25 |
AAll :: ('a stfun => temporal) => temporal (binder "Aall " 10)
|
|
26 |
|
|
27 |
(** concrete syntax **)
|
|
28 |
syntax
|
|
29 |
"_Box" :: lift => lift ("([]_)" [40] 40)
|
|
30 |
"_Dmd" :: lift => lift ("(<>_)" [40] 40)
|
|
31 |
"_leadsto" :: [lift,lift] => lift ("(_ ~> _)" [23,22] 22)
|
|
32 |
"_stable" :: lift => lift ("(stable/ _)")
|
|
33 |
"_WF" :: [lift,lift] => lift ("(WF'(_')'_(_))" [0,60] 55)
|
|
34 |
"_SF" :: [lift,lift] => lift ("(SF'(_')'_(_))" [0,60] 55)
|
|
35 |
|
|
36 |
"_EEx" :: [idts, lift] => lift ("(3EEX _./ _)" [0,10] 10)
|
|
37 |
"_AAll" :: [idts, lift] => lift ("(3AALL _./ _)" [0,10] 10)
|
3807
|
38 |
|
|
39 |
translations
|
6255
|
40 |
"_Box" == "Box"
|
|
41 |
"_Dmd" == "Dmd"
|
|
42 |
"_leadsto" == "leadsto"
|
|
43 |
"_stable" == "Stable"
|
|
44 |
"_WF" == "WF"
|
|
45 |
"_SF" == "SF"
|
|
46 |
"_EEx v A" == "Eex v. A"
|
|
47 |
"_AAll v A" == "Aall v. A"
|
|
48 |
|
|
49 |
"sigma |= []F" <= "_Box F sigma"
|
|
50 |
"sigma |= <>F" <= "_Dmd F sigma"
|
|
51 |
"sigma |= F ~> G" <= "_leadsto F G sigma"
|
|
52 |
"sigma |= stable P" <= "_stable P sigma"
|
|
53 |
"sigma |= WF(A)_v" <= "_WF A v sigma"
|
|
54 |
"sigma |= SF(A)_v" <= "_SF A v sigma"
|
|
55 |
"sigma |= EEX x. F" <= "_EEx x F sigma"
|
|
56 |
"sigma |= AALL x. F" <= "_AAll x F sigma"
|
3807
|
57 |
|
3808
|
58 |
syntax (symbols)
|
6255
|
59 |
"_Box" :: lift => lift ("(\\<box>_)" [40] 40)
|
|
60 |
"_Dmd" :: lift => lift ("(\\<diamond>_)" [40] 40)
|
|
61 |
"_leadsto" :: [lift,lift] => lift ("(_ \\<leadsto> _)" [23,22] 22)
|
|
62 |
"_EEx" :: [idts, lift] => lift ("(3\\<exists>\\<exists> _./ _)" [0,10] 10)
|
|
63 |
"_AAll" :: [idts, lift] => lift ("(3\\<forall>\\<forall> _./ _)" [0,10] 10)
|
3808
|
64 |
|
3807
|
65 |
rules
|
6255
|
66 |
(* Definitions of derived operators *)
|
|
67 |
dmd_def "TEMP <>F == TEMP ~[]~F"
|
|
68 |
boxInit "TEMP []F == TEMP []Init F"
|
|
69 |
leadsto_def "TEMP F ~> G == TEMP [](Init F --> <>G)"
|
|
70 |
stable_def "TEMP stable P == TEMP []($P --> P$)"
|
|
71 |
WF_def "TEMP WF(A)_v == TEMP <>[] Enabled(<A>_v) --> []<><A>_v"
|
|
72 |
SF_def "TEMP SF(A)_v == TEMP []<> Enabled(<A>_v) --> []<><A>_v"
|
|
73 |
aall_def "TEMP (AALL x. F x) == TEMP ~ (EEX x. ~ F x)"
|
3807
|
74 |
|
6255
|
75 |
(* Base axioms for raw TLA. *)
|
|
76 |
normalT "|- [](F --> G) --> ([]F --> []G)" (* polymorphic *)
|
|
77 |
reflT "|- []F --> F" (* F::temporal *)
|
|
78 |
transT "|- []F --> [][]F" (* polymorphic *)
|
|
79 |
linT "|- <>F & <>G --> (<>(F & <>G)) | (<>(G & <>F))"
|
|
80 |
discT "|- [](F --> <>(~F & <>F)) --> (F --> []<>F)"
|
|
81 |
primeI "|- []P --> Init P`"
|
|
82 |
primeE "|- [](Init P --> []F) --> Init P` --> (F --> []F)"
|
|
83 |
indT "|- [](Init P & ~[]F --> Init P` & F) --> Init P --> []F"
|
|
84 |
allT "|- (! x. [](F x)) = ([](! x. F x))"
|
3807
|
85 |
|
6255
|
86 |
necT "|- F ==> |- []F" (* polymorphic *)
|
3807
|
87 |
|
|
88 |
(* Flexible quantification: refinement mappings, history variables *)
|
6255
|
89 |
eexI "|- F x --> (EEX x. F x)"
|
|
90 |
eexE "[| sigma |= (EEX x. F x); basevars vs;
|
|
91 |
(!!x. [| basevars (x, vs); sigma |= F x |] ==> (G sigma)::bool)
|
|
92 |
|] ==> G sigma"
|
|
93 |
history "|- EEX h. Init(h = ha) & [](!x. $h = #x --> h` = hb x)"
|
|
94 |
end
|