src/HOL/TLA/Action.thy
changeset 17309 c43ed29bd197
parent 11703 6e5de8d4290a
child 21624 6f79647cf536
     1.1 --- a/src/HOL/TLA/Action.thy	Wed Sep 07 20:22:15 2005 +0200
     1.2 +++ b/src/HOL/TLA/Action.thy	Wed Sep 07 20:22:39 2005 +0200
     1.3 @@ -1,5 +1,6 @@
     1.4 -(* 
     1.5 -    File:	 TLA/Action.thy
     1.6 +(*
     1.7 +    File:        TLA/Action.thy
     1.8 +    ID:          $Id$
     1.9      Author:      Stephan Merz
    1.10      Copyright:   1998 University of Munich
    1.11  
    1.12 @@ -9,43 +10,46 @@
    1.13  Define the action level of TLA as an Isabelle theory.
    1.14  *)
    1.15  
    1.16 -Action  =  Intensional + Stfun +
    1.17 +theory Action
    1.18 +imports Stfun
    1.19 +begin
    1.20 +
    1.21  
    1.22  (** abstract syntax **)
    1.23  
    1.24  types
    1.25    'a trfun = "(state * state) => 'a"
    1.26 -  action   = bool trfun
    1.27 +  action   = "bool trfun"
    1.28  
    1.29  instance
    1.30 -  "*" :: (world, world) world
    1.31 +  "*" :: (world, world) world ..
    1.32  
    1.33  consts
    1.34    (** abstract syntax **)
    1.35 -  before        :: 'a stfun => 'a trfun
    1.36 -  after         :: 'a stfun => 'a trfun
    1.37 -  unch          :: 'a stfun => action
    1.38 +  before        :: "'a stfun => 'a trfun"
    1.39 +  after         :: "'a stfun => 'a trfun"
    1.40 +  unch          :: "'a stfun => action"
    1.41  
    1.42 -  SqAct         :: [action, 'a stfun] => action
    1.43 -  AnAct         :: [action, 'a stfun] => action
    1.44 -  enabled       :: action => stpred
    1.45 +  SqAct         :: "[action, 'a stfun] => action"
    1.46 +  AnAct         :: "[action, 'a stfun] => action"
    1.47 +  enabled       :: "action => stpred"
    1.48  
    1.49  (** concrete syntax **)
    1.50  
    1.51  syntax
    1.52    (* Syntax for writing action expressions in arbitrary contexts *)
    1.53 -  "ACT"         :: lift => 'a                      ("(ACT _)")
    1.54 +  "ACT"         :: "lift => 'a"                      ("(ACT _)")
    1.55  
    1.56 -  "_before"     :: lift => lift                    ("($_)"  [100] 99)
    1.57 -  "_after"      :: lift => lift                    ("(_$)"  [100] 99)
    1.58 -  "_unchanged"  :: lift => lift                    ("(unchanged _)" [100] 99)
    1.59 +  "_before"     :: "lift => lift"                    ("($_)"  [100] 99)
    1.60 +  "_after"      :: "lift => lift"                    ("(_$)"  [100] 99)
    1.61 +  "_unchanged"  :: "lift => lift"                    ("(unchanged _)" [100] 99)
    1.62  
    1.63    (*** Priming: same as "after" ***)
    1.64 -  "_prime"      :: lift => lift                    ("(_`)" [100] 99)
    1.65 +  "_prime"      :: "lift => lift"                    ("(_`)" [100] 99)
    1.66  
    1.67 -  "_SqAct"      :: [lift, lift] => lift            ("([_]'_(_))" [0,1000] 99)
    1.68 -  "_AnAct"      :: [lift, lift] => lift            ("(<_>'_(_))" [0,1000] 99)
    1.69 -  "_Enabled"    :: lift => lift                    ("(Enabled _)" [100] 100)
    1.70 +  "_SqAct"      :: "[lift, lift] => lift"            ("([_]'_(_))" [0,1000] 99)
    1.71 +  "_AnAct"      :: "[lift, lift] => lift"            ("(<_>'_(_))" [0,1000] 99)
    1.72 +  "_Enabled"    :: "lift => lift"                    ("(Enabled _)" [100] 100)
    1.73  
    1.74  translations
    1.75    "ACT A"            =>   "(A::state*state => _)"
    1.76 @@ -61,13 +65,16 @@
    1.77    "s |= Enabled A"   <=   "_Enabled A s"
    1.78    "w |= unchanged f" <=   "_unchanged f w"
    1.79  
    1.80 -rules
    1.81 -  unl_before    "(ACT $v) (s,t) == v s"
    1.82 -  unl_after     "(ACT v$) (s,t) == v t"
    1.83 +axioms
    1.84 +  unl_before:    "(ACT $v) (s,t) == v s"
    1.85 +  unl_after:     "(ACT v$) (s,t) == v t"
    1.86  
    1.87 -  unchanged_def "(s,t) |= unchanged v == (v t = v s)"
    1.88 -  square_def    "ACT [A]_v == ACT (A | unchanged v)"
    1.89 -  angle_def     "ACT <A>_v == ACT (A & ~ unchanged v)"
    1.90 +  unchanged_def: "(s,t) |= unchanged v == (v t = v s)"
    1.91 +  square_def:    "ACT [A]_v == ACT (A | unchanged v)"
    1.92 +  angle_def:     "ACT <A>_v == ACT (A & ~ unchanged v)"
    1.93  
    1.94 -  enabled_def   "s |= Enabled A  ==  EX u. (s,u) |= A"
    1.95 +  enabled_def:   "s |= Enabled A  ==  EX u. (s,u) |= A"
    1.96 +
    1.97 +ML {* use_legacy_bindings (the_context ()) *}
    1.98 +
    1.99  end