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