4559
|
1 |
(* Title: HOLCF/IOA/meta_theory/TLS.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Olaf M"uller
|
|
4 |
Copyright 1997 TU Muenchen
|
|
5 |
|
|
6 |
A General Temporal Logic
|
|
7 |
|
|
8 |
*)
|
|
9 |
|
|
10 |
|
|
11 |
|
|
12 |
TL = Pred + Sequence +
|
|
13 |
|
|
14 |
default term
|
|
15 |
|
|
16 |
types
|
|
17 |
|
|
18 |
'a temporal = 'a Seq predicate
|
|
19 |
|
|
20 |
|
|
21 |
consts
|
|
22 |
|
|
23 |
|
|
24 |
suffix :: "'a Seq => 'a Seq => bool"
|
|
25 |
tsuffix :: "'a Seq => 'a Seq => bool"
|
|
26 |
|
|
27 |
validT :: "'a Seq predicate => bool"
|
|
28 |
|
|
29 |
unlift :: "'a lift => 'a"
|
|
30 |
|
|
31 |
Init ::"'a predicate => 'a temporal" ("<_>" [0] 1000)
|
|
32 |
|
|
33 |
Box ::"'a temporal => 'a temporal" ("[] (_)" [80] 80)
|
|
34 |
Diamond ::"'a temporal => 'a temporal" ("<> (_)" [80] 80)
|
|
35 |
Next ::"'a temporal => 'a temporal"
|
|
36 |
Leadsto ::"'a temporal => 'a temporal => 'a temporal" (infixr "~>" 22)
|
|
37 |
|
|
38 |
syntax (symbols)
|
|
39 |
"Box" ::"'a temporal => 'a temporal" ("\\<box> (_)" [80] 80)
|
|
40 |
"Diamond" ::"'a temporal => 'a temporal" ("\\<diamond> (_)" [80] 80)
|
|
41 |
"Leadsto" ::"'a temporal => 'a temporal => 'a temporal" (infixr "\\<leadsto>" 22)
|
|
42 |
|
|
43 |
defs
|
|
44 |
|
|
45 |
|
|
46 |
unlift_def
|
|
47 |
"unlift x == (case x of
|
12028
|
48 |
UU => arbitrary
|
4559
|
49 |
| Def y => y)"
|
|
50 |
|
|
51 |
(* this means that for nil and UU the effect is unpredictable *)
|
|
52 |
Init_def
|
10835
|
53 |
"Init P s == (P (unlift (HD$s)))"
|
4559
|
54 |
|
|
55 |
suffix_def
|
|
56 |
"suffix s2 s == ? s1. (Finite s1 & s = s1 @@ s2)"
|
|
57 |
|
|
58 |
tsuffix_def
|
|
59 |
"tsuffix s2 s == s2 ~= nil & s2 ~= UU & suffix s2 s"
|
|
60 |
|
|
61 |
Box_def
|
|
62 |
"([] P) s == ! s2. tsuffix s2 s --> P s2"
|
|
63 |
|
|
64 |
Next_def
|
10835
|
65 |
"(Next P) s == if (TL$s=UU | TL$s=nil) then (P s) else P (TL$s)"
|
4559
|
66 |
|
|
67 |
Diamond_def
|
|
68 |
"<> P == .~ ([] (.~ P))"
|
|
69 |
|
|
70 |
Leadsto_def
|
|
71 |
"P ~> Q == ([] (P .--> (<> Q)))"
|
|
72 |
|
|
73 |
validT_def
|
|
74 |
"validT P == ! s. s~=UU & s~=nil --> (s |= P)"
|
|
75 |
|
|
76 |
end |