src/HOL/TLA/Action.thy
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 11703 6e5de8d4290a
child 17309 c43ed29bd197
permissions -rw-r--r--
import -> imports
     1 (* 
     2     File:	 TLA/Action.thy
     3     Author:      Stephan Merz
     4     Copyright:   1998 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 (** abstract syntax **)
    15 
    16 types
    17   'a trfun = "(state * state) => 'a"
    18   action   = bool trfun
    19 
    20 instance
    21   "*" :: (world, world) world
    22 
    23 consts
    24   (** abstract syntax **)
    25   before        :: 'a stfun => 'a trfun
    26   after         :: 'a stfun => 'a trfun
    27   unch          :: 'a stfun => action
    28 
    29   SqAct         :: [action, 'a stfun] => action
    30   AnAct         :: [action, 'a stfun] => action
    31   enabled       :: action => stpred
    32 
    33 (** concrete syntax **)
    34 
    35 syntax
    36   (* Syntax for writing action expressions in arbitrary contexts *)
    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"           ==   "after"
    54   "_prime"           =>   "_after"
    55   "_unchanged"       ==   "unch"
    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"
    63 
    64 rules
    65   unl_before    "(ACT $v) (s,t) == v s"
    66   unl_after     "(ACT v$) (s,t) == v t"
    67 
    68   unchanged_def "(s,t) |= unchanged v == (v t = v s)"
    69   square_def    "ACT [A]_v == ACT (A | unchanged v)"
    70   angle_def     "ACT <A>_v == ACT (A & ~ unchanged v)"
    71 
    72   enabled_def   "s |= Enabled A  ==  EX u. (s,u) |= A"
    73 end