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