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