src/HOL/TLA/Action.thy
author wenzelm
Wed Sep 07 20:22:39 2005 +0200 (2005-09-07)
changeset 17309 c43ed29bd197
parent 11703 6e5de8d4290a
child 21624 6f79647cf536
permissions -rw-r--r--
converted to Isar theory format;
     1 (*
     2     File:        TLA/Action.thy
     3     ID:          $Id$
     4     Author:      Stephan Merz
     5     Copyright:   1998 University of Munich
     6 
     7     Theory Name: Action
     8     Logic Image: HOL
     9 
    10 Define the action level of TLA as an Isabelle theory.
    11 *)
    12 
    13 theory Action
    14 imports Stfun
    15 begin
    16 
    17 
    18 (** abstract syntax **)
    19 
    20 types
    21   'a trfun = "(state * state) => 'a"
    22   action   = "bool trfun"
    23 
    24 instance
    25   "*" :: (world, world) world ..
    26 
    27 consts
    28   (** abstract syntax **)
    29   before        :: "'a stfun => 'a trfun"
    30   after         :: "'a stfun => 'a trfun"
    31   unch          :: "'a stfun => action"
    32 
    33   SqAct         :: "[action, 'a stfun] => action"
    34   AnAct         :: "[action, 'a stfun] => action"
    35   enabled       :: "action => stpred"
    36 
    37 (** concrete syntax **)
    38 
    39 syntax
    40   (* Syntax for writing action expressions in arbitrary contexts *)
    41   "ACT"         :: "lift => 'a"                      ("(ACT _)")
    42 
    43   "_before"     :: "lift => lift"                    ("($_)"  [100] 99)
    44   "_after"      :: "lift => lift"                    ("(_$)"  [100] 99)
    45   "_unchanged"  :: "lift => lift"                    ("(unchanged _)" [100] 99)
    46 
    47   (*** Priming: same as "after" ***)
    48   "_prime"      :: "lift => lift"                    ("(_`)" [100] 99)
    49 
    50   "_SqAct"      :: "[lift, lift] => lift"            ("([_]'_(_))" [0,1000] 99)
    51   "_AnAct"      :: "[lift, lift] => lift"            ("(<_>'_(_))" [0,1000] 99)
    52   "_Enabled"    :: "lift => lift"                    ("(Enabled _)" [100] 100)
    53 
    54 translations
    55   "ACT A"            =>   "(A::state*state => _)"
    56   "_before"          ==   "before"
    57   "_after"           ==   "after"
    58   "_prime"           =>   "_after"
    59   "_unchanged"       ==   "unch"
    60   "_SqAct"           ==   "SqAct"
    61   "_AnAct"           ==   "AnAct"
    62   "_Enabled"         ==   "enabled"
    63   "w |= [A]_v"       <=   "_SqAct A v w"
    64   "w |= <A>_v"       <=   "_AnAct A v w"
    65   "s |= Enabled A"   <=   "_Enabled A s"
    66   "w |= unchanged f" <=   "_unchanged f w"
    67 
    68 axioms
    69   unl_before:    "(ACT $v) (s,t) == v s"
    70   unl_after:     "(ACT v$) (s,t) == v t"
    71 
    72   unchanged_def: "(s,t) |= unchanged v == (v t = v s)"
    73   square_def:    "ACT [A]_v == ACT (A | unchanged v)"
    74   angle_def:     "ACT <A>_v == ACT (A & ~ unchanged v)"
    75 
    76   enabled_def:   "s |= Enabled A  ==  EX u. (s,u) |= A"
    77 
    78 ML {* use_legacy_bindings (the_context ()) *}
    79 
    80 end