src/HOL/TLA/Action.thy
 changeset 6255 db63752140c7 parent 3807 82a99b090d9d child 9517 f58863b1406a
```     1.1 --- a/src/HOL/TLA/Action.thy	Mon Feb 08 13:02:42 1999 +0100
1.2 +++ b/src/HOL/TLA/Action.thy	Mon Feb 08 13:02:56 1999 +0100
1.3 @@ -1,7 +1,7 @@
1.4  (*
1.5      File:	 TLA/Action.thy
1.6      Author:      Stephan Merz
1.7 -    Copyright:   1997 University of Munich
1.8 +    Copyright:   1998 University of Munich
1.9
1.10      Theory Name: Action
1.11      Logic Image: HOL
1.12 @@ -11,50 +11,65 @@
1.13
1.14  Action  =  Intensional + Stfun +
1.15
1.16 +(** abstract syntax **)
1.17 +
1.18  types
1.19 -    state2      (* intention: pair of states *)
1.20 -    'a trfct = "('a, state2) term"
1.21 -    action   = "state2 form"
1.22 +  'a trfun = "(state * state) => 'a"
1.23 +  action   = bool trfun
1.24 +
1.25 +instance
1.26 +  "*" :: (world, world) world
1.27
1.28 -arities
1.29 -    state2 :: world
1.30 -
1.31  consts
1.32 -  mkstate2      :: "[state,state] => state2"  ("([[_,_]])")
1.33 +  (** abstract syntax **)
1.34 +  before        :: 'a stfun => 'a trfun
1.35 +  after         :: 'a stfun => 'a trfun
1.36 +  unch          :: 'a stfun => action
1.37 +
1.38 +  SqAct         :: [action, 'a stfun] => action
1.39 +  AnAct         :: [action, 'a stfun] => action
1.40 +  enabled       :: action => stpred
1.41 +
1.42 +(** concrete syntax **)
1.43 +
1.44 +syntax
1.45 +  (* Syntax for writing action expressions in arbitrary contexts *)
1.46 +  "ACT"         :: lift => 'a                      ("(ACT _)")
1.47
1.48 -  (* lift state variables to transition functions *)
1.49 -  before        :: "'a stfun => 'a trfct"            ("(\$_)"  [100] 99)
1.50 -  after         :: "'a stfun => 'a trfct"            ("(_\$)"  [100] 99)
1.51 -  unchanged     :: "'a stfun => action"
1.52 +  "_before"     :: lift => lift                    ("(\$_)"  [100] 99)
1.53 +  "_after"      :: lift => lift                    ("(_\$)"  [100] 99)
1.54 +  "_unchanged"  :: lift => lift                    ("(unchanged _)" [100] 99)
1.55 +
1.56 +  (*** Priming: same as "after" ***)
1.57 +  "_prime"      :: lift => lift                    ("(_`)" [100] 99)
1.58 +
1.59 +  "_SqAct"      :: [lift, lift] => lift            ("([_]'_(_))" [0,1000] 99)
1.60 +  "_AnAct"      :: [lift, lift] => lift            ("(<_>'_(_))" [0,1000] 99)
1.61 +  "_Enabled"    :: lift => lift                    ("(Enabled _)" [100] 100)
1.62
1.63 -  (* Priming *)
1.64 -  prime         :: "'a trfct => 'a trfct"            ("(_`)" [90] 89)
1.65 -
1.66 -  SqAct         :: "[action, 'a stfun] => action"    ("([_]'_(_))" [0,60] 59)
1.67 -  AnAct         :: "[action, 'a stfun] => action"    ("(<_>'_(_))" [0,60] 59)
1.68 -  Enabled       :: "action => stpred"
1.69 +translations
1.70 +  "ACT A"            =>   "(A::state*state => _)"
1.71 +  "_before"          ==   "before"
1.72 +  "_after"           =>   "_prime"
1.73 +  "_unchanged"       ==   "unch"
1.74 +  "_prime"           ==   "after"
1.75 +  "_SqAct"           ==   "SqAct"
1.76 +  "_AnAct"           ==   "AnAct"
1.77 +  "_Enabled"         ==   "enabled"
1.78 +  "w |= [A]_v"       <=   "_SqAct A v w"
1.79 +  "w |= <A>_v"       <=   "_AnAct A v w"
1.80 +  "s |= Enabled A"   <=   "_Enabled A s"
1.81 +  "w |= unchanged f" <=   "_unchanged f w"
1.82
1.83  rules
1.84 -  (* The following says that state2 is generated by mkstate2 *)
1.85 -  state2_ext    "(!!s t. [[s,t]] |= (A::action)) ==> (st::state2) |= A"
1.86 -
1.87 -  unl_before    "(\$v) [[s,t]] == v s"
1.88 -  unl_after     "(v\$) [[s,t]] == v t"
1.89 +  unl_before    "(ACT \$v) (s,t) == v s"
1.90 +  unl_after     "(ACT v`) (s,t) == v t"
1.91
1.92 -  pr_con        "(#c)` == #c"
1.93 -  pr_before     "(\$v)` == v\$"
1.94 -  (* no corresponding rule for "after"! *)
1.95 -  pr_lift       "(F[x])` == F[x`]"
1.96 -  pr_lift2      "(F[x,y])` == F[x`,y`]"
1.97 -  pr_lift3      "(F[x,y,z])` == F[x`,y`,z`]"
1.98 -  pr_all        "(RALL x. P(x))` == (RALL x. P(x)`)"
1.99 -  pr_ex         "(REX x. P(x))` == (REX x. P(x)`)"
1.100 +  unchanged_def "(s,t) |= unchanged v == (v t = v s)"
1.101 +  square_def    "ACT [A]_v == ACT (A | unchanged v)"
1.102 +  angle_def     "ACT <A>_v == ACT (A & ~ unchanged v)"
1.103
1.104 -  unchanged_def "(unchanged v) [[s,t]] == (v t = v s)"
1.105 -  square_def    "[A]_v == A .| unchanged v"
1.106 -  angle_def     "<A>_v == A .& .~ unchanged v"
1.107 -
1.108 -  enabled_def   "(Enabled A) s  ==  EX u. A[[s,u]]"
1.109 +  enabled_def   "s |= Enabled A  ==  EX u. (s,u) |= A"
1.110  end
1.111
1.112
```