--- a/src/HOL/TLA/Action.thy Mon Feb 08 13:02:42 1999 +0100
+++ b/src/HOL/TLA/Action.thy Mon Feb 08 13:02:56 1999 +0100
@@ -1,7 +1,7 @@
(*
File: TLA/Action.thy
Author: Stephan Merz
- Copyright: 1997 University of Munich
+ Copyright: 1998 University of Munich
Theory Name: Action
Logic Image: HOL
@@ -11,50 +11,65 @@
Action = Intensional + Stfun +
+(** abstract syntax **)
+
types
- state2 (* intention: pair of states *)
- 'a trfct = "('a, state2) term"
- action = "state2 form"
+ 'a trfun = "(state * state) => 'a"
+ action = bool trfun
+
+instance
+ "*" :: (world, world) world
-arities
- state2 :: world
-
consts
- mkstate2 :: "[state,state] => state2" ("([[_,_]])")
+ (** abstract syntax **)
+ before :: 'a stfun => 'a trfun
+ after :: 'a stfun => 'a trfun
+ unch :: 'a stfun => action
+
+ SqAct :: [action, 'a stfun] => action
+ AnAct :: [action, 'a stfun] => action
+ enabled :: action => stpred
+
+(** concrete syntax **)
+
+syntax
+ (* Syntax for writing action expressions in arbitrary contexts *)
+ "ACT" :: lift => 'a ("(ACT _)")
- (* lift state variables to transition functions *)
- before :: "'a stfun => 'a trfct" ("($_)" [100] 99)
- after :: "'a stfun => 'a trfct" ("(_$)" [100] 99)
- unchanged :: "'a stfun => action"
+ "_before" :: lift => lift ("($_)" [100] 99)
+ "_after" :: lift => lift ("(_$)" [100] 99)
+ "_unchanged" :: lift => lift ("(unchanged _)" [100] 99)
+
+ (*** Priming: same as "after" ***)
+ "_prime" :: lift => lift ("(_`)" [100] 99)
+
+ "_SqAct" :: [lift, lift] => lift ("([_]'_(_))" [0,1000] 99)
+ "_AnAct" :: [lift, lift] => lift ("(<_>'_(_))" [0,1000] 99)
+ "_Enabled" :: lift => lift ("(Enabled _)" [100] 100)
- (* Priming *)
- prime :: "'a trfct => 'a trfct" ("(_`)" [90] 89)
-
- SqAct :: "[action, 'a stfun] => action" ("([_]'_(_))" [0,60] 59)
- AnAct :: "[action, 'a stfun] => action" ("(<_>'_(_))" [0,60] 59)
- Enabled :: "action => stpred"
+translations
+ "ACT A" => "(A::state*state => _)"
+ "_before" == "before"
+ "_after" => "_prime"
+ "_unchanged" == "unch"
+ "_prime" == "after"
+ "_SqAct" == "SqAct"
+ "_AnAct" == "AnAct"
+ "_Enabled" == "enabled"
+ "w |= [A]_v" <= "_SqAct A v w"
+ "w |= <A>_v" <= "_AnAct A v w"
+ "s |= Enabled A" <= "_Enabled A s"
+ "w |= unchanged f" <= "_unchanged f w"
rules
- (* The following says that state2 is generated by mkstate2 *)
- state2_ext "(!!s t. [[s,t]] |= (A::action)) ==> (st::state2) |= A"
-
- unl_before "($v) [[s,t]] == v s"
- unl_after "(v$) [[s,t]] == v t"
+ unl_before "(ACT $v) (s,t) == v s"
+ unl_after "(ACT v`) (s,t) == v t"
- pr_con "(#c)` == #c"
- pr_before "($v)` == v$"
- (* no corresponding rule for "after"! *)
- pr_lift "(F[x])` == F[x`]"
- pr_lift2 "(F[x,y])` == F[x`,y`]"
- pr_lift3 "(F[x,y,z])` == F[x`,y`,z`]"
- pr_all "(RALL x. P(x))` == (RALL x. P(x)`)"
- pr_ex "(REX x. P(x))` == (REX x. P(x)`)"
+ unchanged_def "(s,t) |= unchanged v == (v t = v s)"
+ square_def "ACT [A]_v == ACT (A | unchanged v)"
+ angle_def "ACT <A>_v == ACT (A & ~ unchanged v)"
- unchanged_def "(unchanged v) [[s,t]] == (v t = v s)"
- square_def "[A]_v == A .| unchanged v"
- angle_def "<A>_v == A .& .~ unchanged v"
-
- enabled_def "(Enabled A) s == EX u. A[[s,u]]"
+ enabled_def "s |= Enabled A == EX u. (s,u) |= A"
end