|
1 (* |
|
2 File: TLA/Action.thy |
|
3 Author: Stephan Merz |
|
4 Copyright: 1997 University of Munich |
|
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 |
|
14 types |
|
15 state2 (* intention: pair of states *) |
|
16 'a trfct = "('a, state2) term" |
|
17 action = "state2 form" |
|
18 |
|
19 arities |
|
20 state2 :: world |
|
21 |
|
22 consts |
|
23 mkstate2 :: "[state,state] => state2" ("([[_,_]])") |
|
24 |
|
25 (* lift state variables to transition functions *) |
|
26 before :: "'a stfun => 'a trfct" ("($_)" [100] 99) |
|
27 after :: "'a stfun => 'a trfct" ("(_$)" [100] 99) |
|
28 unchanged :: "'a stfun => action" |
|
29 |
|
30 (* Priming *) |
|
31 prime :: "'a trfct => 'a trfct" ("(_`)" [90] 89) |
|
32 |
|
33 SqAct :: "[action, 'a stfun] => action" ("([_]'_(_))" [0,60] 59) |
|
34 AnAct :: "[action, 'a stfun] => action" ("(<_>'_(_))" [0,60] 59) |
|
35 Enabled :: "action => stpred" |
|
36 |
|
37 rules |
|
38 (* The following says that state2 is generated by mkstate2 *) |
|
39 state2_ext "(!!s t. [[s,t]] |= (A::action)) ==> (st::state2) |= A" |
|
40 |
|
41 unl_before "($v) [[s,t]] == v s" |
|
42 unl_after "(v$) [[s,t]] == v t" |
|
43 |
|
44 pr_con "(#c)` == #c" |
|
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 |
|
59 |
|
60 |