author | kleing |
Wed, 14 Apr 2004 14:13:05 +0200 | |
changeset 14565 | c6dc17aab88a |
parent 12114 | a8e860c86252 |
child 17309 | c43ed29bd197 |
permissions | -rw-r--r-- |
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 |
|
12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
9517
diff
changeset
|
58 |
syntax (xsymbols) |
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 |
|
14565 | 65 |
syntax (HTML output) |
66 |
"_EEx" :: [idts, lift] => lift ("(3\\<exists>\\<exists> _./ _)" [0,10] 10) |
|
67 |
"_AAll" :: [idts, lift] => lift ("(3\\<forall>\\<forall> _./ _)" [0,10] 10) |
|
68 |
||
3807 | 69 |
rules |
6255 | 70 |
(* Definitions of derived operators *) |
71 |
dmd_def "TEMP <>F == TEMP ~[]~F" |
|
72 |
boxInit "TEMP []F == TEMP []Init F" |
|
73 |
leadsto_def "TEMP F ~> G == TEMP [](Init F --> <>G)" |
|
74 |
stable_def "TEMP stable P == TEMP []($P --> P$)" |
|
75 |
WF_def "TEMP WF(A)_v == TEMP <>[] Enabled(<A>_v) --> []<><A>_v" |
|
76 |
SF_def "TEMP SF(A)_v == TEMP []<> Enabled(<A>_v) --> []<><A>_v" |
|
77 |
aall_def "TEMP (AALL x. F x) == TEMP ~ (EEX x. ~ F x)" |
|
3807 | 78 |
|
6255 | 79 |
(* Base axioms for raw TLA. *) |
80 |
normalT "|- [](F --> G) --> ([]F --> []G)" (* polymorphic *) |
|
81 |
reflT "|- []F --> F" (* F::temporal *) |
|
82 |
transT "|- []F --> [][]F" (* polymorphic *) |
|
83 |
linT "|- <>F & <>G --> (<>(F & <>G)) | (<>(G & <>F))" |
|
84 |
discT "|- [](F --> <>(~F & <>F)) --> (F --> []<>F)" |
|
85 |
primeI "|- []P --> Init P`" |
|
86 |
primeE "|- [](Init P --> []F) --> Init P` --> (F --> []F)" |
|
87 |
indT "|- [](Init P & ~[]F --> Init P` & F) --> Init P --> []F" |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7562
diff
changeset
|
88 |
allT "|- (ALL x. [](F x)) = ([](ALL x. F x))" |
3807 | 89 |
|
6255 | 90 |
necT "|- F ==> |- []F" (* polymorphic *) |
3807 | 91 |
|
92 |
(* Flexible quantification: refinement mappings, history variables *) |
|
6255 | 93 |
eexI "|- F x --> (EEX x. F x)" |
94 |
eexE "[| sigma |= (EEX x. F x); basevars vs; |
|
95 |
(!!x. [| basevars (x, vs); sigma |= F x |] ==> (G sigma)::bool) |
|
96 |
|] ==> G sigma" |
|
97 |
history "|- EEX h. Init(h = ha) & [](!x. $h = #x --> h` = hb x)" |
|
98 |
end |