src/HOL/TLA/Action.thy
 author wenzelm Wed Oct 08 11:50:33 1997 +0200 (1997-10-08) changeset 3807 82a99b090d9d child 6255 db63752140c7 permissions -rw-r--r--
A formalization of TLA in HOL -- by Stephan Merz;
1 (*
2     File:	 TLA/Action.thy
3     Author:      Stephan Merz
4     Copyright:   1997 University of Munich
6     Theory Name: Action
7     Logic Image: HOL
9 Define the action level of TLA as an Isabelle theory.
10 *)
12 Action  =  Intensional + Stfun +
14 types
15     state2      (* intention: pair of states *)
16     'a trfct = "('a, state2) term"
17     action   = "state2 form"
19 arities
20     state2 :: world
22 consts
23   mkstate2      :: "[state,state] => state2"  ("([[_,_]])")
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"
30   (* Priming *)
31   prime         :: "'a trfct => 'a trfct"            ("(_`)" [90] 89)
33   SqAct         :: "[action, 'a stfun] => action"    ("([_]'_(_))" [0,60] 59)
34   AnAct         :: "[action, 'a stfun] => action"    ("(<_>'_(_))" [0,60] 59)
35   Enabled       :: "action => stpred"
37 rules
38   (* The following says that state2 is generated by mkstate2 *)
39   state2_ext    "(!!s t. [[s,t]] |= (A::action)) ==> (st::state2) |= A"
41   unl_before    "(\$v) [[s,t]] == v s"
42   unl_after     "(v\$) [[s,t]] == v t"
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)`)"
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"
57   enabled_def   "(Enabled A) s  ==  EX u. A[[s,u]]"
58 end