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