author | wenzelm |
Fri, 09 Nov 2001 00:09:47 +0100 | |
changeset 12114 | a8e860c86252 |
parent 12028 | 52aa183c15bb |
child 12218 | 6597093b77e7 |
permissions | -rw-r--r-- |
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 |
||
12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
12028
diff
changeset
|
38 |
syntax (xsymbols) |
4559 | 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 |