src/HOL/TLA/Action.thy
changeset 62146 324bc1ffba12
parent 61853 fb7756087101
child 69597 ff784d5a5bfb
     1.1 --- a/src/HOL/TLA/Action.thy	Mon Jan 11 21:21:02 2016 +0100
     1.2 +++ b/src/HOL/TLA/Action.thy	Mon Jan 11 22:23:03 2016 +0100
     1.3 @@ -9,25 +9,19 @@
     1.4  imports Stfun
     1.5  begin
     1.6  
     1.7 -
     1.8 -(** abstract syntax **)
     1.9 -
    1.10 -type_synonym 'a trfun = "(state * state) \<Rightarrow> 'a"
    1.11 -type_synonym action   = "bool trfun"
    1.12 +type_synonym 'a trfun = "state \<times> state \<Rightarrow> 'a"
    1.13 +type_synonym action = "bool trfun"
    1.14  
    1.15  instance prod :: (world, world) world ..
    1.16  
    1.17 -consts
    1.18 -  (** abstract syntax **)
    1.19 -  before        :: "'a stfun \<Rightarrow> 'a trfun"
    1.20 -  after         :: "'a stfun \<Rightarrow> 'a trfun"
    1.21 -  unch          :: "'a stfun \<Rightarrow> action"
    1.22 +definition enabled :: "action \<Rightarrow> stpred"
    1.23 +  where "enabled A s \<equiv> \<exists>u. (s,u) \<Turnstile> A"
    1.24 +
    1.25  
    1.26 -  SqAct         :: "[action, 'a stfun] \<Rightarrow> action"
    1.27 -  AnAct         :: "[action, 'a stfun] \<Rightarrow> action"
    1.28 -  enabled       :: "action \<Rightarrow> stpred"
    1.29 -
    1.30 -(** concrete syntax **)
    1.31 +consts
    1.32 +  before :: "'a stfun \<Rightarrow> 'a trfun"
    1.33 +  after :: "'a stfun \<Rightarrow> 'a trfun"
    1.34 +  unch :: "'a stfun \<Rightarrow> action"
    1.35  
    1.36  syntax
    1.37    (* Syntax for writing action expressions in arbitrary contexts *)
    1.38 @@ -40,8 +34,6 @@
    1.39    (*** Priming: same as "after" ***)
    1.40    "_prime"      :: "lift \<Rightarrow> lift"                    ("(_`)" [100] 99)
    1.41  
    1.42 -  "_SqAct"      :: "[lift, lift] \<Rightarrow> lift"            ("([_]'_(_))" [0,1000] 99)
    1.43 -  "_AnAct"      :: "[lift, lift] \<Rightarrow> lift"            ("(<_>'_(_))" [0,1000] 99)
    1.44    "_Enabled"    :: "lift \<Rightarrow> lift"                    ("(Enabled _)" [100] 100)
    1.45  
    1.46  translations
    1.47 @@ -50,25 +42,30 @@
    1.48    "_after"           ==   "CONST after"
    1.49    "_prime"           =>   "_after"
    1.50    "_unchanged"       ==   "CONST unch"
    1.51 -  "_SqAct"           ==   "CONST SqAct"
    1.52 -  "_AnAct"           ==   "CONST AnAct"
    1.53    "_Enabled"         ==   "CONST enabled"
    1.54 -  "w \<Turnstile> [A]_v"       <=   "_SqAct A v w"
    1.55 -  "w \<Turnstile> <A>_v"       <=   "_AnAct A v w"
    1.56    "s \<Turnstile> Enabled A"   <=   "_Enabled A s"
    1.57    "w \<Turnstile> unchanged f" <=   "_unchanged f w"
    1.58  
    1.59  axiomatization where
    1.60    unl_before:    "(ACT $v) (s,t) \<equiv> v s" and
    1.61    unl_after:     "(ACT v$) (s,t) \<equiv> v t" and
    1.62 -
    1.63    unchanged_def: "(s,t) \<Turnstile> unchanged v \<equiv> (v t = v s)"
    1.64  
    1.65 -defs
    1.66 -  square_def:    "ACT [A]_v \<equiv> ACT (A \<or> unchanged v)"
    1.67 -  angle_def:     "ACT <A>_v \<equiv> ACT (A \<and> \<not> unchanged v)"
    1.68 +
    1.69 +definition SqAct :: "[action, 'a stfun] \<Rightarrow> action"
    1.70 +  where square_def: "SqAct A v \<equiv> ACT (A \<or> unchanged v)"
    1.71 +
    1.72 +definition AnAct :: "[action, 'a stfun] \<Rightarrow> action"
    1.73 +  where angle_def: "AnAct A v \<equiv> ACT (A \<and> \<not> unchanged v)"
    1.74  
    1.75 -  enabled_def:   "s \<Turnstile> Enabled A  \<equiv>  \<exists>u. (s,u) \<Turnstile> A"
    1.76 +syntax
    1.77 +  "_SqAct" :: "[lift, lift] \<Rightarrow> lift"  ("([_]'_(_))" [0, 1000] 99)
    1.78 +  "_AnAct" :: "[lift, lift] \<Rightarrow> lift"  ("(<_>'_(_))" [0, 1000] 99)
    1.79 +translations
    1.80 +  "_SqAct" == "CONST SqAct"
    1.81 +  "_AnAct" == "CONST AnAct"
    1.82 +  "w \<Turnstile> [A]_v" \<leftharpoondown> "_SqAct A v w"
    1.83 +  "w \<Turnstile> <A>_v" \<leftharpoondown> "_AnAct A v w"
    1.84  
    1.85  
    1.86  (* The following assertion specializes "intI" for any world type