1 (* |
1 (* |
2 File: TLA/Action.thy |
2 File: TLA/Action.thy |
3 Author: Stephan Merz |
3 Author: Stephan Merz |
4 Copyright: 1997 University of Munich |
4 Copyright: 1998 University of Munich |
5 |
5 |
6 Theory Name: Action |
6 Theory Name: Action |
7 Logic Image: HOL |
7 Logic Image: HOL |
8 |
8 |
9 Define the action level of TLA as an Isabelle theory. |
9 Define the action level of TLA as an Isabelle theory. |
10 *) |
10 *) |
11 |
11 |
12 Action = Intensional + Stfun + |
12 Action = Intensional + Stfun + |
13 |
13 |
|
14 (** abstract syntax **) |
|
15 |
14 types |
16 types |
15 state2 (* intention: pair of states *) |
17 'a trfun = "(state * state) => 'a" |
16 'a trfct = "('a, state2) term" |
18 action = bool trfun |
17 action = "state2 form" |
|
18 |
19 |
19 arities |
20 instance |
20 state2 :: world |
21 "*" :: (world, world) world |
21 |
22 |
22 consts |
23 consts |
23 mkstate2 :: "[state,state] => state2" ("([[_,_]])") |
24 (** abstract syntax **) |
|
25 before :: 'a stfun => 'a trfun |
|
26 after :: 'a stfun => 'a trfun |
|
27 unch :: 'a stfun => action |
24 |
28 |
25 (* lift state variables to transition functions *) |
29 SqAct :: [action, 'a stfun] => action |
26 before :: "'a stfun => 'a trfct" ("($_)" [100] 99) |
30 AnAct :: [action, 'a stfun] => action |
27 after :: "'a stfun => 'a trfct" ("(_$)" [100] 99) |
31 enabled :: action => stpred |
28 unchanged :: "'a stfun => action" |
|
29 |
32 |
30 (* Priming *) |
33 (** concrete syntax **) |
31 prime :: "'a trfct => 'a trfct" ("(_`)" [90] 89) |
|
32 |
34 |
33 SqAct :: "[action, 'a stfun] => action" ("([_]'_(_))" [0,60] 59) |
35 syntax |
34 AnAct :: "[action, 'a stfun] => action" ("(<_>'_(_))" [0,60] 59) |
36 (* Syntax for writing action expressions in arbitrary contexts *) |
35 Enabled :: "action => stpred" |
37 "ACT" :: lift => 'a ("(ACT _)") |
|
38 |
|
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) |
|
49 |
|
50 translations |
|
51 "ACT A" => "(A::state*state => _)" |
|
52 "_before" == "before" |
|
53 "_after" => "_prime" |
|
54 "_unchanged" == "unch" |
|
55 "_prime" == "after" |
|
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" |
36 |
63 |
37 rules |
64 rules |
38 (* The following says that state2 is generated by mkstate2 *) |
65 unl_before "(ACT $v) (s,t) == v s" |
39 state2_ext "(!!s t. [[s,t]] |= (A::action)) ==> (st::state2) |= A" |
66 unl_after "(ACT v`) (s,t) == v t" |
40 |
67 |
41 unl_before "($v) [[s,t]] == v s" |
68 unchanged_def "(s,t) |= unchanged v == (v t = v s)" |
42 unl_after "(v$) [[s,t]] == v t" |
69 square_def "ACT [A]_v == ACT (A | unchanged v)" |
|
70 angle_def "ACT <A>_v == ACT (A & ~ unchanged v)" |
43 |
71 |
44 pr_con "(#c)` == #c" |
72 enabled_def "s |= Enabled A == EX u. (s,u) |= A" |
45 pr_before "($v)` == v$" |
|
46 (* no corresponding rule for "after"! *) |
|
47 pr_lift "(F[x])` == F[x`]" |
|
48 pr_lift2 "(F[x,y])` == F[x`,y`]" |
|
49 pr_lift3 "(F[x,y,z])` == F[x`,y`,z`]" |
|
50 pr_all "(RALL x. P(x))` == (RALL x. P(x)`)" |
|
51 pr_ex "(REX x. P(x))` == (REX x. P(x)`)" |
|
52 |
|
53 unchanged_def "(unchanged v) [[s,t]] == (v t = v s)" |
|
54 square_def "[A]_v == A .| unchanged v" |
|
55 angle_def "<A>_v == A .& .~ unchanged v" |
|
56 |
|
57 enabled_def "(Enabled A) s == EX u. A[[s,u]]" |
|
58 end |
73 end |
59 |
74 |
60 |
75 |