1 (* |
1 (* |
2 File: TLA/Action.thy |
2 File: TLA/Action.thy |
|
3 ID: $Id$ |
3 Author: Stephan Merz |
4 Author: Stephan Merz |
4 Copyright: 1998 University of Munich |
5 Copyright: 1998 University of Munich |
5 |
6 |
6 Theory Name: Action |
7 Theory Name: Action |
7 Logic Image: HOL |
8 Logic Image: HOL |
8 |
9 |
9 Define the action level of TLA as an Isabelle theory. |
10 Define the action level of TLA as an Isabelle theory. |
10 *) |
11 *) |
11 |
12 |
12 Action = Intensional + Stfun + |
13 theory Action |
|
14 imports Stfun |
|
15 begin |
|
16 |
13 |
17 |
14 (** abstract syntax **) |
18 (** abstract syntax **) |
15 |
19 |
16 types |
20 types |
17 'a trfun = "(state * state) => 'a" |
21 'a trfun = "(state * state) => 'a" |
18 action = bool trfun |
22 action = "bool trfun" |
19 |
23 |
20 instance |
24 instance |
21 "*" :: (world, world) world |
25 "*" :: (world, world) world .. |
22 |
26 |
23 consts |
27 consts |
24 (** abstract syntax **) |
28 (** abstract syntax **) |
25 before :: 'a stfun => 'a trfun |
29 before :: "'a stfun => 'a trfun" |
26 after :: 'a stfun => 'a trfun |
30 after :: "'a stfun => 'a trfun" |
27 unch :: 'a stfun => action |
31 unch :: "'a stfun => action" |
28 |
32 |
29 SqAct :: [action, 'a stfun] => action |
33 SqAct :: "[action, 'a stfun] => action" |
30 AnAct :: [action, 'a stfun] => action |
34 AnAct :: "[action, 'a stfun] => action" |
31 enabled :: action => stpred |
35 enabled :: "action => stpred" |
32 |
36 |
33 (** concrete syntax **) |
37 (** concrete syntax **) |
34 |
38 |
35 syntax |
39 syntax |
36 (* Syntax for writing action expressions in arbitrary contexts *) |
40 (* Syntax for writing action expressions in arbitrary contexts *) |
37 "ACT" :: lift => 'a ("(ACT _)") |
41 "ACT" :: "lift => 'a" ("(ACT _)") |
38 |
42 |
39 "_before" :: lift => lift ("($_)" [100] 99) |
43 "_before" :: "lift => lift" ("($_)" [100] 99) |
40 "_after" :: lift => lift ("(_$)" [100] 99) |
44 "_after" :: "lift => lift" ("(_$)" [100] 99) |
41 "_unchanged" :: lift => lift ("(unchanged _)" [100] 99) |
45 "_unchanged" :: "lift => lift" ("(unchanged _)" [100] 99) |
42 |
46 |
43 (*** Priming: same as "after" ***) |
47 (*** Priming: same as "after" ***) |
44 "_prime" :: lift => lift ("(_`)" [100] 99) |
48 "_prime" :: "lift => lift" ("(_`)" [100] 99) |
45 |
49 |
46 "_SqAct" :: [lift, lift] => lift ("([_]'_(_))" [0,1000] 99) |
50 "_SqAct" :: "[lift, lift] => lift" ("([_]'_(_))" [0,1000] 99) |
47 "_AnAct" :: [lift, lift] => lift ("(<_>'_(_))" [0,1000] 99) |
51 "_AnAct" :: "[lift, lift] => lift" ("(<_>'_(_))" [0,1000] 99) |
48 "_Enabled" :: lift => lift ("(Enabled _)" [100] 100) |
52 "_Enabled" :: "lift => lift" ("(Enabled _)" [100] 100) |
49 |
53 |
50 translations |
54 translations |
51 "ACT A" => "(A::state*state => _)" |
55 "ACT A" => "(A::state*state => _)" |
52 "_before" == "before" |
56 "_before" == "before" |
53 "_after" == "after" |
57 "_after" == "after" |
59 "w |= [A]_v" <= "_SqAct A v w" |
63 "w |= [A]_v" <= "_SqAct A v w" |
60 "w |= <A>_v" <= "_AnAct A v w" |
64 "w |= <A>_v" <= "_AnAct A v w" |
61 "s |= Enabled A" <= "_Enabled A s" |
65 "s |= Enabled A" <= "_Enabled A s" |
62 "w |= unchanged f" <= "_unchanged f w" |
66 "w |= unchanged f" <= "_unchanged f w" |
63 |
67 |
64 rules |
68 axioms |
65 unl_before "(ACT $v) (s,t) == v s" |
69 unl_before: "(ACT $v) (s,t) == v s" |
66 unl_after "(ACT v$) (s,t) == v t" |
70 unl_after: "(ACT v$) (s,t) == v t" |
67 |
71 |
68 unchanged_def "(s,t) |= unchanged v == (v t = v s)" |
72 unchanged_def: "(s,t) |= unchanged v == (v t = v s)" |
69 square_def "ACT [A]_v == ACT (A | unchanged v)" |
73 square_def: "ACT [A]_v == ACT (A | unchanged v)" |
70 angle_def "ACT <A>_v == ACT (A & ~ unchanged v)" |
74 angle_def: "ACT <A>_v == ACT (A & ~ unchanged v)" |
71 |
75 |
72 enabled_def "s |= Enabled A == EX u. (s,u) |= A" |
76 enabled_def: "s |= Enabled A == EX u. (s,u) |= A" |
|
77 |
|
78 ML {* use_legacy_bindings (the_context ()) *} |
|
79 |
73 end |
80 end |