author | paulson |
Mon, 08 Mar 2004 11:12:06 +0100 | |
changeset 14443 | 75910c7557c5 |
parent 11703 | 6e5de8d4290a |
child 17309 | c43ed29bd197 |
permissions | -rw-r--r-- |
3807 | 1 |
(* |
2 |
File: TLA/Action.thy |
|
3 |
Author: Stephan Merz |
|
6255 | 4 |
Copyright: 1998 University of Munich |
3807 | 5 |
|
6 |
Theory Name: Action |
|
7 |
Logic Image: HOL |
|
8 |
||
9 |
Define the action level of TLA as an Isabelle theory. |
|
10 |
*) |
|
11 |
||
12 |
Action = Intensional + Stfun + |
|
13 |
||
6255 | 14 |
(** abstract syntax **) |
15 |
||
3807 | 16 |
types |
6255 | 17 |
'a trfun = "(state * state) => 'a" |
18 |
action = bool trfun |
|
19 |
||
20 |
instance |
|
21 |
"*" :: (world, world) world |
|
3807 | 22 |
|
23 |
consts |
|
6255 | 24 |
(** abstract syntax **) |
25 |
before :: 'a stfun => 'a trfun |
|
26 |
after :: 'a stfun => 'a trfun |
|
27 |
unch :: 'a stfun => action |
|
28 |
||
29 |
SqAct :: [action, 'a stfun] => action |
|
30 |
AnAct :: [action, 'a stfun] => action |
|
31 |
enabled :: action => stpred |
|
32 |
||
33 |
(** concrete syntax **) |
|
34 |
||
35 |
syntax |
|
36 |
(* Syntax for writing action expressions in arbitrary contexts *) |
|
37 |
"ACT" :: lift => 'a ("(ACT _)") |
|
3807 | 38 |
|
6255 | 39 |
"_before" :: lift => lift ("($_)" [100] 99) |
40 |
"_after" :: lift => lift ("(_$)" [100] 99) |
|
41 |
"_unchanged" :: lift => lift ("(unchanged _)" [100] 99) |
|
42 |
||
43 |
(*** Priming: same as "after" ***) |
|
44 |
"_prime" :: lift => lift ("(_`)" [100] 99) |
|
45 |
||
46 |
"_SqAct" :: [lift, lift] => lift ("([_]'_(_))" [0,1000] 99) |
|
47 |
"_AnAct" :: [lift, lift] => lift ("(<_>'_(_))" [0,1000] 99) |
|
48 |
"_Enabled" :: lift => lift ("(Enabled _)" [100] 100) |
|
3807 | 49 |
|
6255 | 50 |
translations |
51 |
"ACT A" => "(A::state*state => _)" |
|
52 |
"_before" == "before" |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
53 |
"_after" == "after" |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
54 |
"_prime" => "_after" |
6255 | 55 |
"_unchanged" == "unch" |
56 |
"_SqAct" == "SqAct" |
|
57 |
"_AnAct" == "AnAct" |
|
58 |
"_Enabled" == "enabled" |
|
59 |
"w |= [A]_v" <= "_SqAct A v w" |
|
60 |
"w |= <A>_v" <= "_AnAct A v w" |
|
61 |
"s |= Enabled A" <= "_Enabled A s" |
|
62 |
"w |= unchanged f" <= "_unchanged f w" |
|
3807 | 63 |
|
64 |
rules |
|
6255 | 65 |
unl_before "(ACT $v) (s,t) == v s" |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
66 |
unl_after "(ACT v$) (s,t) == v t" |
3807 | 67 |
|
6255 | 68 |
unchanged_def "(s,t) |= unchanged v == (v t = v s)" |
69 |
square_def "ACT [A]_v == ACT (A | unchanged v)" |
|
70 |
angle_def "ACT <A>_v == ACT (A & ~ unchanged v)" |
|
3807 | 71 |
|
6255 | 72 |
enabled_def "s |= Enabled A == EX u. (s,u) |= A" |
3807 | 73 |
end |