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