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
wenzelm@3807
     1
(* 
wenzelm@3807
     2
    File:	 TLA/Action.thy
wenzelm@3807
     3
    Author:      Stephan Merz
wenzelm@6255
     4
    Copyright:   1998 University of Munich
wenzelm@3807
     5
wenzelm@3807
     6
    Theory Name: Action
wenzelm@3807
     7
    Logic Image: HOL
wenzelm@3807
     8
wenzelm@3807
     9
Define the action level of TLA as an Isabelle theory.
wenzelm@3807
    10
*)
wenzelm@3807
    11
wenzelm@3807
    12
Action  =  Intensional + Stfun +
wenzelm@3807
    13
wenzelm@6255
    14
(** abstract syntax **)
wenzelm@6255
    15
wenzelm@3807
    16
types
wenzelm@6255
    17
  'a trfun = "(state * state) => 'a"
wenzelm@6255
    18
  action   = bool trfun
wenzelm@6255
    19
wenzelm@6255
    20
instance
wenzelm@6255
    21
  "*" :: (world, world) world
wenzelm@3807
    22
wenzelm@3807
    23
consts
wenzelm@6255
    24
  (** abstract syntax **)
wenzelm@6255
    25
  before        :: 'a stfun => 'a trfun
wenzelm@6255
    26
  after         :: 'a stfun => 'a trfun
wenzelm@6255
    27
  unch          :: 'a stfun => action
wenzelm@6255
    28
wenzelm@6255
    29
  SqAct         :: [action, 'a stfun] => action
wenzelm@6255
    30
  AnAct         :: [action, 'a stfun] => action
wenzelm@6255
    31
  enabled       :: action => stpred
wenzelm@6255
    32
wenzelm@6255
    33
(** concrete syntax **)
wenzelm@6255
    34
wenzelm@6255
    35
syntax
wenzelm@6255
    36
  (* Syntax for writing action expressions in arbitrary contexts *)
wenzelm@6255
    37
  "ACT"         :: lift => 'a                      ("(ACT _)")
wenzelm@3807
    38
wenzelm@6255
    39
  "_before"     :: lift => lift                    ("($_)"  [100] 99)
wenzelm@6255
    40
  "_after"      :: lift => lift                    ("(_$)"  [100] 99)
wenzelm@6255
    41
  "_unchanged"  :: lift => lift                    ("(unchanged _)" [100] 99)
wenzelm@6255
    42
wenzelm@6255
    43
  (*** Priming: same as "after" ***)
wenzelm@6255
    44
  "_prime"      :: lift => lift                    ("(_`)" [100] 99)
wenzelm@6255
    45
wenzelm@6255
    46
  "_SqAct"      :: [lift, lift] => lift            ("([_]'_(_))" [0,1000] 99)
wenzelm@6255
    47
  "_AnAct"      :: [lift, lift] => lift            ("(<_>'_(_))" [0,1000] 99)
wenzelm@6255
    48
  "_Enabled"    :: lift => lift                    ("(Enabled _)" [100] 100)
wenzelm@3807
    49
wenzelm@6255
    50
translations
wenzelm@6255
    51
  "ACT A"            =>   "(A::state*state => _)"
wenzelm@6255
    52
  "_before"          ==   "before"
wenzelm@9517
    53
  "_after"           ==   "after"
wenzelm@9517
    54
  "_prime"           =>   "_after"
wenzelm@6255
    55
  "_unchanged"       ==   "unch"
wenzelm@6255
    56
  "_SqAct"           ==   "SqAct"
wenzelm@6255
    57
  "_AnAct"           ==   "AnAct"
wenzelm@6255
    58
  "_Enabled"         ==   "enabled"
wenzelm@6255
    59
  "w |= [A]_v"       <=   "_SqAct A v w"
wenzelm@6255
    60
  "w |= <A>_v"       <=   "_AnAct A v w"
wenzelm@6255
    61
  "s |= Enabled A"   <=   "_Enabled A s"
wenzelm@6255
    62
  "w |= unchanged f" <=   "_unchanged f w"
wenzelm@3807
    63
wenzelm@3807
    64
rules
wenzelm@6255
    65
  unl_before    "(ACT $v) (s,t) == v s"
wenzelm@9517
    66
  unl_after     "(ACT v$) (s,t) == v t"
wenzelm@3807
    67
wenzelm@6255
    68
  unchanged_def "(s,t) |= unchanged v == (v t = v s)"
wenzelm@6255
    69
  square_def    "ACT [A]_v == ACT (A | unchanged v)"
wenzelm@6255
    70
  angle_def     "ACT <A>_v == ACT (A & ~ unchanged v)"
wenzelm@3807
    71
wenzelm@6255
    72
  enabled_def   "s |= Enabled A  ==  EX u. (s,u) |= A"
wenzelm@3807
    73
end