src/HOL/TLA/TLA.thy
changeset 60588 750c533459b1
parent 60587 0318b43ee95c
child 60591 e0b77517f9a9
     1.1 --- a/src/HOL/TLA/TLA.thy	Fri Jun 26 11:44:22 2015 +0200
     1.2 +++ b/src/HOL/TLA/TLA.thy	Fri Jun 26 14:53:15 2015 +0200
     1.3 @@ -11,28 +11,28 @@
     1.4  
     1.5  consts
     1.6    (** abstract syntax **)
     1.7 -  Box        :: "('w::world) form => temporal"
     1.8 -  Dmd        :: "('w::world) form => temporal"
     1.9 -  leadsto    :: "['w::world form, 'v::world form] => temporal"
    1.10 -  Stable     :: "stpred => temporal"
    1.11 -  WF         :: "[action, 'a stfun] => temporal"
    1.12 -  SF         :: "[action, 'a stfun] => temporal"
    1.13 +  Box        :: "('w::world) form \<Rightarrow> temporal"
    1.14 +  Dmd        :: "('w::world) form \<Rightarrow> temporal"
    1.15 +  leadsto    :: "['w::world form, 'v::world form] \<Rightarrow> temporal"
    1.16 +  Stable     :: "stpred \<Rightarrow> temporal"
    1.17 +  WF         :: "[action, 'a stfun] \<Rightarrow> temporal"
    1.18 +  SF         :: "[action, 'a stfun] \<Rightarrow> temporal"
    1.19  
    1.20    (* Quantification over (flexible) state variables *)
    1.21 -  EEx        :: "('a stfun => temporal) => temporal"       (binder "Eex " 10)
    1.22 -  AAll       :: "('a stfun => temporal) => temporal"       (binder "Aall " 10)
    1.23 +  EEx        :: "('a stfun \<Rightarrow> temporal) \<Rightarrow> temporal"       (binder "Eex " 10)
    1.24 +  AAll       :: "('a stfun \<Rightarrow> temporal) \<Rightarrow> temporal"       (binder "Aall " 10)
    1.25  
    1.26    (** concrete syntax **)
    1.27  syntax
    1.28 -  "_Box"     :: "lift => lift"                        ("([]_)" [40] 40)
    1.29 -  "_Dmd"     :: "lift => lift"                        ("(<>_)" [40] 40)
    1.30 -  "_leadsto" :: "[lift,lift] => lift"                 ("(_ ~> _)" [23,22] 22)
    1.31 -  "_stable"  :: "lift => lift"                        ("(stable/ _)")
    1.32 -  "_WF"      :: "[lift,lift] => lift"                 ("(WF'(_')'_(_))" [0,60] 55)
    1.33 -  "_SF"      :: "[lift,lift] => lift"                 ("(SF'(_')'_(_))" [0,60] 55)
    1.34 +  "_Box"     :: "lift \<Rightarrow> lift"                        ("([]_)" [40] 40)
    1.35 +  "_Dmd"     :: "lift \<Rightarrow> lift"                        ("(<>_)" [40] 40)
    1.36 +  "_leadsto" :: "[lift,lift] \<Rightarrow> lift"                 ("(_ ~> _)" [23,22] 22)
    1.37 +  "_stable"  :: "lift \<Rightarrow> lift"                        ("(stable/ _)")
    1.38 +  "_WF"      :: "[lift,lift] \<Rightarrow> lift"                 ("(WF'(_')'_(_))" [0,60] 55)
    1.39 +  "_SF"      :: "[lift,lift] \<Rightarrow> lift"                 ("(SF'(_')'_(_))" [0,60] 55)
    1.40  
    1.41 -  "_EEx"     :: "[idts, lift] => lift"                ("(3EEX _./ _)" [0,10] 10)
    1.42 -  "_AAll"    :: "[idts, lift] => lift"                ("(3AALL _./ _)" [0,10] 10)
    1.43 +  "_EEx"     :: "[idts, lift] \<Rightarrow> lift"                ("(3EEX _./ _)" [0,10] 10)
    1.44 +  "_AAll"    :: "[idts, lift] \<Rightarrow> lift"                ("(3AALL _./ _)" [0,10] 10)
    1.45  
    1.46  translations
    1.47    "_Box"      ==   "CONST Box"
    1.48 @@ -54,11 +54,11 @@
    1.49    "sigma |= AALL x. F"    <= "_AAll x F sigma"
    1.50  
    1.51  syntax (xsymbols)
    1.52 -  "_Box"     :: "lift => lift"                        ("(\<box>_)" [40] 40)
    1.53 -  "_Dmd"     :: "lift => lift"                        ("(\<diamond>_)" [40] 40)
    1.54 -  "_leadsto" :: "[lift,lift] => lift"                 ("(_ \<leadsto> _)" [23,22] 22)
    1.55 -  "_EEx"     :: "[idts, lift] => lift"                ("(3\<exists>\<exists> _./ _)" [0,10] 10)
    1.56 -  "_AAll"    :: "[idts, lift] => lift"                ("(3\<forall>\<forall> _./ _)" [0,10] 10)
    1.57 +  "_Box"     :: "lift \<Rightarrow> lift"                        ("(\<box>_)" [40] 40)
    1.58 +  "_Dmd"     :: "lift \<Rightarrow> lift"                        ("(\<diamond>_)" [40] 40)
    1.59 +  "_leadsto" :: "[lift,lift] \<Rightarrow> lift"                 ("(_ \<leadsto> _)" [23,22] 22)
    1.60 +  "_EEx"     :: "[idts, lift] \<Rightarrow> lift"                ("(3\<exists>\<exists> _./ _)" [0,10] 10)
    1.61 +  "_AAll"    :: "[idts, lift] \<Rightarrow> lift"                ("(3\<forall>\<forall> _./ _)" [0,10] 10)
    1.62  
    1.63  axiomatization where
    1.64    (* Definitions of derived operators *)
    1.65 @@ -66,44 +66,44 @@
    1.66  
    1.67  axiomatization where
    1.68    boxInit:      "\<And>F. TEMP \<box>F  ==  TEMP \<box>Init F" and
    1.69 -  leadsto_def:  "\<And>F G. TEMP F \<leadsto> G  ==  TEMP \<box>(Init F --> \<diamond>G)" and
    1.70 -  stable_def:   "\<And>P. TEMP stable P  ==  TEMP \<box>($P --> P$)" and
    1.71 -  WF_def:       "TEMP WF(A)_v  ==  TEMP \<diamond>\<box> Enabled(<A>_v) --> \<box>\<diamond><A>_v" and
    1.72 -  SF_def:       "TEMP SF(A)_v  ==  TEMP \<box>\<diamond> Enabled(<A>_v) --> \<box>\<diamond><A>_v" and
    1.73 +  leadsto_def:  "\<And>F G. TEMP F \<leadsto> G  ==  TEMP \<box>(Init F \<longrightarrow> \<diamond>G)" and
    1.74 +  stable_def:   "\<And>P. TEMP stable P  ==  TEMP \<box>($P \<longrightarrow> P$)" and
    1.75 +  WF_def:       "TEMP WF(A)_v  ==  TEMP \<diamond>\<box> Enabled(<A>_v) \<longrightarrow> \<box>\<diamond><A>_v" and
    1.76 +  SF_def:       "TEMP SF(A)_v  ==  TEMP \<box>\<diamond> Enabled(<A>_v) \<longrightarrow> \<box>\<diamond><A>_v" and
    1.77    aall_def:     "TEMP (\<forall>\<forall>x. F x)  ==  TEMP \<not> (\<exists>\<exists>x. \<not> F x)"
    1.78  
    1.79  axiomatization where
    1.80  (* Base axioms for raw TLA. *)
    1.81 -  normalT:    "\<And>F G. |- \<box>(F --> G) --> (\<box>F --> \<box>G)" and    (* polymorphic *)
    1.82 -  reflT:      "\<And>F. |- \<box>F --> F" and         (* F::temporal *)
    1.83 -  transT:     "\<And>F. |- \<box>F --> \<box>\<box>F" and     (* polymorphic *)
    1.84 -  linT:       "\<And>F G. |- \<diamond>F & \<diamond>G --> (\<diamond>(F & \<diamond>G)) | (\<diamond>(G & \<diamond>F))" and
    1.85 -  discT:      "\<And>F. |- \<box>(F --> \<diamond>(\<not>F & \<diamond>F)) --> (F --> \<box>\<diamond>F)" and
    1.86 -  primeI:     "\<And>P. |- \<box>P --> Init P`" and
    1.87 -  primeE:     "\<And>P F. |- \<box>(Init P --> \<box>F) --> Init P` --> (F --> \<box>F)" and
    1.88 -  indT:       "\<And>P F. |- \<box>(Init P & \<not>\<box>F --> Init P` & F) --> Init P --> \<box>F" and
    1.89 -  allT:       "\<And>F. |- (\<forall>x. \<box>(F x)) = (\<box>(\<forall> x. F x))"
    1.90 +  normalT:    "\<And>F G. \<turnstile> \<box>(F \<longrightarrow> G) \<longrightarrow> (\<box>F \<longrightarrow> \<box>G)" and    (* polymorphic *)
    1.91 +  reflT:      "\<And>F. \<turnstile> \<box>F \<longrightarrow> F" and         (* F::temporal *)
    1.92 +  transT:     "\<And>F. \<turnstile> \<box>F \<longrightarrow> \<box>\<box>F" and     (* polymorphic *)
    1.93 +  linT:       "\<And>F G. \<turnstile> \<diamond>F & \<diamond>G \<longrightarrow> (\<diamond>(F & \<diamond>G)) | (\<diamond>(G & \<diamond>F))" and
    1.94 +  discT:      "\<And>F. \<turnstile> \<box>(F \<longrightarrow> \<diamond>(\<not>F & \<diamond>F)) \<longrightarrow> (F \<longrightarrow> \<box>\<diamond>F)" and
    1.95 +  primeI:     "\<And>P. \<turnstile> \<box>P \<longrightarrow> Init P`" and
    1.96 +  primeE:     "\<And>P F. \<turnstile> \<box>(Init P \<longrightarrow> \<box>F) \<longrightarrow> Init P` \<longrightarrow> (F \<longrightarrow> \<box>F)" and
    1.97 +  indT:       "\<And>P F. \<turnstile> \<box>(Init P & \<not>\<box>F \<longrightarrow> Init P` & F) \<longrightarrow> Init P \<longrightarrow> \<box>F" and
    1.98 +  allT:       "\<And>F. \<turnstile> (\<forall>x. \<box>(F x)) = (\<box>(\<forall> x. F x))"
    1.99  
   1.100  axiomatization where
   1.101 -  necT:       "\<And>F. |- F ==> |- \<box>F"      (* polymorphic *)
   1.102 +  necT:       "\<And>F. \<turnstile> F \<Longrightarrow> \<turnstile> \<box>F"      (* polymorphic *)
   1.103  
   1.104  axiomatization where
   1.105  (* Flexible quantification: refinement mappings, history variables *)
   1.106 -  eexI:       "|- F x --> (\<exists>\<exists>x. F x)" and
   1.107 -  eexE:       "[| sigma |= (\<exists>\<exists>x. F x); basevars vs;
   1.108 -                 (\<And>x. [| basevars (x, vs); sigma |= F x |] ==> (G sigma)::bool)
   1.109 -              |] ==> G sigma" and
   1.110 -  history:    "|- \<exists>\<exists>h. Init(h = ha) & \<box>(\<forall>x. $h = #x --> h` = hb x)"
   1.111 +  eexI:       "\<turnstile> F x \<longrightarrow> (\<exists>\<exists>x. F x)" and
   1.112 +  eexE:       "\<lbrakk> sigma \<Turnstile> (\<exists>\<exists>x. F x); basevars vs;
   1.113 +                 (\<And>x. \<lbrakk> basevars (x, vs); sigma \<Turnstile> F x \<rbrakk> \<Longrightarrow> (G sigma)::bool)
   1.114 +              \<rbrakk> \<Longrightarrow> G sigma" and
   1.115 +  history:    "\<turnstile> \<exists>\<exists>h. Init(h = ha) & \<box>(\<forall>x. $h = #x \<longrightarrow> h` = hb x)"
   1.116  
   1.117  
   1.118  (* Specialize intensional introduction/elimination rules for temporal formulas *)
   1.119  
   1.120 -lemma tempI [intro!]: "(\<And>sigma. sigma |= (F::temporal)) ==> |- F"
   1.121 +lemma tempI [intro!]: "(\<And>sigma. sigma \<Turnstile> (F::temporal)) \<Longrightarrow> \<turnstile> F"
   1.122    apply (rule intI)
   1.123    apply (erule meta_spec)
   1.124    done
   1.125  
   1.126 -lemma tempD [dest]: "|- (F::temporal) ==> sigma |= F"
   1.127 +lemma tempD [dest]: "\<turnstile> (F::temporal) \<Longrightarrow> sigma \<Turnstile> F"
   1.128    by (erule intD)
   1.129  
   1.130  
   1.131 @@ -118,7 +118,7 @@
   1.132    (rewrite_rule ctxt @{thms action_rews} (th RS @{thm tempD}))
   1.133      handle THM _ => action_unlift ctxt th;
   1.134  
   1.135 -(* Turn  |- F = G  into meta-level rewrite rule  F == G *)
   1.136 +(* Turn  \<turnstile> F = G  into meta-level rewrite rule  F == G *)
   1.137  val temp_rewrite = int_rewrite
   1.138  
   1.139  fun temp_use ctxt th =
   1.140 @@ -176,21 +176,21 @@
   1.141  lemmas STL2 = reflT
   1.142  
   1.143  (* The "polymorphic" (generic) variant *)
   1.144 -lemma STL2_gen: "|- \<box>F --> Init F"
   1.145 +lemma STL2_gen: "\<turnstile> \<box>F \<longrightarrow> Init F"
   1.146    apply (unfold boxInit [of F])
   1.147    apply (rule STL2)
   1.148    done
   1.149  
   1.150 -(* see also STL2_pr below: "|- \<box>P --> Init P & Init (P`)" *)
   1.151 +(* see also STL2_pr below: "\<turnstile> \<box>P \<longrightarrow> Init P & Init (P`)" *)
   1.152  
   1.153  
   1.154  (* Dual versions for \<diamond> *)
   1.155 -lemma InitDmd: "|- F --> \<diamond> F"
   1.156 +lemma InitDmd: "\<turnstile> F \<longrightarrow> \<diamond> F"
   1.157    apply (unfold dmd_def)
   1.158    apply (auto dest!: STL2 [temp_use])
   1.159    done
   1.160  
   1.161 -lemma InitDmd_gen: "|- Init F --> \<diamond>F"
   1.162 +lemma InitDmd_gen: "\<turnstile> Init F \<longrightarrow> \<diamond>F"
   1.163    apply clarsimp
   1.164    apply (drule InitDmd [temp_use])
   1.165    apply (simp add: dmdInitD)
   1.166 @@ -198,17 +198,17 @@
   1.167  
   1.168  
   1.169  (* ------------------------ STL3 ------------------------------------------- *)
   1.170 -lemma STL3: "|- (\<box>\<box>F) = (\<box>F)"
   1.171 +lemma STL3: "\<turnstile> (\<box>\<box>F) = (\<box>F)"
   1.172    by (auto elim: transT [temp_use] STL2 [temp_use])
   1.173  
   1.174  (* corresponding elimination rule introduces double boxes:
   1.175 -   [| (sigma |= \<box>F); (sigma |= \<box>\<box>F) ==> PROP W |] ==> PROP W
   1.176 +   \<lbrakk> (sigma \<Turnstile> \<box>F); (sigma \<Turnstile> \<box>\<box>F) \<Longrightarrow> PROP W \<rbrakk> \<Longrightarrow> PROP W
   1.177  *)
   1.178  lemmas dup_boxE = STL3 [temp_unlift, THEN iffD2, elim_format]
   1.179  lemmas dup_boxD = STL3 [temp_unlift, THEN iffD1]
   1.180  
   1.181  (* dual versions for \<diamond> *)
   1.182 -lemma DmdDmd: "|- (\<diamond>\<diamond>F) = (\<diamond>F)"
   1.183 +lemma DmdDmd: "\<turnstile> (\<diamond>\<diamond>F) = (\<diamond>F)"
   1.184    by (auto simp add: dmd_def [try_rewrite] STL3 [try_rewrite])
   1.185  
   1.186  lemmas dup_dmdE = DmdDmd [temp_unlift, THEN iffD2, elim_format]
   1.187 @@ -217,8 +217,8 @@
   1.188  
   1.189  (* ------------------------ STL4 ------------------------------------------- *)
   1.190  lemma STL4:
   1.191 -  assumes "|- F --> G"
   1.192 -  shows "|- \<box>F --> \<box>G"
   1.193 +  assumes "\<turnstile> F \<longrightarrow> G"
   1.194 +  shows "\<turnstile> \<box>F \<longrightarrow> \<box>G"
   1.195    apply clarsimp
   1.196    apply (rule normalT [temp_use])
   1.197     apply (rule assms [THEN necT, temp_use])
   1.198 @@ -226,15 +226,15 @@
   1.199    done
   1.200  
   1.201  (* Unlifted version as an elimination rule *)
   1.202 -lemma STL4E: "[| sigma |= \<box>F; |- F --> G |] ==> sigma |= \<box>G"
   1.203 +lemma STL4E: "\<lbrakk> sigma \<Turnstile> \<box>F; \<turnstile> F \<longrightarrow> G \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>G"
   1.204    by (erule (1) STL4 [temp_use])
   1.205  
   1.206 -lemma STL4_gen: "|- Init F --> Init G ==> |- \<box>F --> \<box>G"
   1.207 +lemma STL4_gen: "\<turnstile> Init F \<longrightarrow> Init G \<Longrightarrow> \<turnstile> \<box>F \<longrightarrow> \<box>G"
   1.208    apply (drule STL4)
   1.209    apply (simp add: boxInitD)
   1.210    done
   1.211  
   1.212 -lemma STL4E_gen: "[| sigma |= \<box>F; |- Init F --> Init G |] ==> sigma |= \<box>G"
   1.213 +lemma STL4E_gen: "\<lbrakk> sigma \<Turnstile> \<box>F; \<turnstile> Init F \<longrightarrow> Init G \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>G"
   1.214    by (erule (1) STL4_gen [temp_use])
   1.215  
   1.216  (* see also STL4Edup below, which allows an auxiliary boxed formula:
   1.217 @@ -245,19 +245,19 @@
   1.218  
   1.219  (* The dual versions for \<diamond> *)
   1.220  lemma DmdImpl:
   1.221 -  assumes prem: "|- F --> G"
   1.222 -  shows "|- \<diamond>F --> \<diamond>G"
   1.223 +  assumes prem: "\<turnstile> F \<longrightarrow> G"
   1.224 +  shows "\<turnstile> \<diamond>F \<longrightarrow> \<diamond>G"
   1.225    apply (unfold dmd_def)
   1.226    apply (fastforce intro!: prem [temp_use] elim!: STL4E [temp_use])
   1.227    done
   1.228  
   1.229 -lemma DmdImplE: "[| sigma |= \<diamond>F; |- F --> G |] ==> sigma |= \<diamond>G"
   1.230 +lemma DmdImplE: "\<lbrakk> sigma \<Turnstile> \<diamond>F; \<turnstile> F \<longrightarrow> G \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<diamond>G"
   1.231    by (erule (1) DmdImpl [temp_use])
   1.232  
   1.233  (* ------------------------ STL5 ------------------------------------------- *)
   1.234 -lemma STL5: "|- (\<box>F & \<box>G) = (\<box>(F & G))"
   1.235 +lemma STL5: "\<turnstile> (\<box>F & \<box>G) = (\<box>(F & G))"
   1.236    apply auto
   1.237 -  apply (subgoal_tac "sigma |= \<box> (G --> (F & G))")
   1.238 +  apply (subgoal_tac "sigma \<Turnstile> \<box> (G \<longrightarrow> (F & G))")
   1.239       apply (erule normalT [temp_use])
   1.240       apply (fastforce elim!: STL4E [temp_use])+
   1.241    done
   1.242 @@ -271,9 +271,9 @@
   1.243     Use "addSE2" etc. if you want to add this to a claset, otherwise it will loop!
   1.244  *)
   1.245  lemma box_conjE:
   1.246 -  assumes "sigma |= \<box>F"
   1.247 -     and "sigma |= \<box>G"
   1.248 -  and "sigma |= \<box>(F&G) ==> PROP R"
   1.249 +  assumes "sigma \<Turnstile> \<box>F"
   1.250 +     and "sigma \<Turnstile> \<box>G"
   1.251 +  and "sigma \<Turnstile> \<box>(F&G) \<Longrightarrow> PROP R"
   1.252    shows "PROP R"
   1.253    by (rule assms STL5 [temp_unlift, THEN iffD1] conjI)+
   1.254  
   1.255 @@ -288,7 +288,7 @@
   1.256     a bit kludgy in order to simulate "double elim-resolution".
   1.257  *)
   1.258  
   1.259 -lemma box_thin: "[| sigma |= \<box>F; PROP W |] ==> PROP W" .
   1.260 +lemma box_thin: "\<lbrakk> sigma \<Turnstile> \<box>F; PROP W \<rbrakk> \<Longrightarrow> PROP W" .
   1.261  
   1.262  ML {*
   1.263  fun merge_box_tac i =
   1.264 @@ -313,21 +313,21 @@
   1.265  method_setup merge_act_box = {* Scan.succeed (SIMPLE_METHOD' o merge_act_box_tac) *}
   1.266  
   1.267  (* rewrite rule to push universal quantification through box:
   1.268 -      (sigma |= \<box>(\<forall>x. F x)) = (\<forall>x. (sigma |= \<box>F x))
   1.269 +      (sigma \<Turnstile> \<box>(\<forall>x. F x)) = (\<forall>x. (sigma \<Turnstile> \<box>F x))
   1.270  *)
   1.271  lemmas all_box = allT [temp_unlift, symmetric]
   1.272  
   1.273 -lemma DmdOr: "|- (\<diamond>(F | G)) = (\<diamond>F | \<diamond>G)"
   1.274 +lemma DmdOr: "\<turnstile> (\<diamond>(F | G)) = (\<diamond>F | \<diamond>G)"
   1.275    apply (auto simp add: dmd_def split_box_conj [try_rewrite])
   1.276    apply (erule contrapos_np, merge_box, fastforce elim!: STL4E [temp_use])+
   1.277    done
   1.278  
   1.279 -lemma exT: "|- (\<exists>x. \<diamond>(F x)) = (\<diamond>(\<exists>x. F x))"
   1.280 +lemma exT: "\<turnstile> (\<exists>x. \<diamond>(F x)) = (\<diamond>(\<exists>x. F x))"
   1.281    by (auto simp: dmd_def Not_Rex [try_rewrite] all_box [try_rewrite])
   1.282  
   1.283  lemmas ex_dmd = exT [temp_unlift, symmetric]
   1.284  
   1.285 -lemma STL4Edup: "\<And>sigma. [| sigma |= \<box>A; sigma |= \<box>F; |- F & \<box>A --> G |] ==> sigma |= \<box>G"
   1.286 +lemma STL4Edup: "\<And>sigma. \<lbrakk> sigma \<Turnstile> \<box>A; sigma \<Turnstile> \<box>F; \<turnstile> F & \<box>A \<longrightarrow> G \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>G"
   1.287    apply (erule dup_boxE)
   1.288    apply merge_box
   1.289    apply (erule STL4E)
   1.290 @@ -335,7 +335,7 @@
   1.291    done
   1.292  
   1.293  lemma DmdImpl2:
   1.294 -    "\<And>sigma. [| sigma |= \<diamond>F; sigma |= \<box>(F --> G) |] ==> sigma |= \<diamond>G"
   1.295 +    "\<And>sigma. \<lbrakk> sigma \<Turnstile> \<diamond>F; sigma \<Turnstile> \<box>(F \<longrightarrow> G) \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<diamond>G"
   1.296    apply (unfold dmd_def)
   1.297    apply auto
   1.298    apply (erule notE)
   1.299 @@ -344,10 +344,10 @@
   1.300    done
   1.301  
   1.302  lemma InfImpl:
   1.303 -  assumes 1: "sigma |= \<box>\<diamond>F"
   1.304 -    and 2: "sigma |= \<box>G"
   1.305 -    and 3: "|- F & G --> H"
   1.306 -  shows "sigma |= \<box>\<diamond>H"
   1.307 +  assumes 1: "sigma \<Turnstile> \<box>\<diamond>F"
   1.308 +    and 2: "sigma \<Turnstile> \<box>G"
   1.309 +    and 3: "\<turnstile> F & G \<longrightarrow> H"
   1.310 +  shows "sigma \<Turnstile> \<box>\<diamond>H"
   1.311    apply (insert 1 2)
   1.312    apply (erule_tac F = G in dup_boxE)
   1.313    apply merge_box
   1.314 @@ -356,7 +356,7 @@
   1.315  
   1.316  (* ------------------------ STL6 ------------------------------------------- *)
   1.317  (* Used in the proof of STL6, but useful in itself. *)
   1.318 -lemma BoxDmd: "|- \<box>F & \<diamond>G --> \<diamond>(\<box>F & G)"
   1.319 +lemma BoxDmd: "\<turnstile> \<box>F & \<diamond>G \<longrightarrow> \<diamond>(\<box>F & G)"
   1.320    apply (unfold dmd_def)
   1.321    apply clarsimp
   1.322    apply (erule dup_boxE)
   1.323 @@ -366,14 +366,14 @@
   1.324    done
   1.325  
   1.326  (* weaker than BoxDmd, but more polymorphic (and often just right) *)
   1.327 -lemma BoxDmd_simple: "|- \<box>F & \<diamond>G --> \<diamond>(F & G)"
   1.328 +lemma BoxDmd_simple: "\<turnstile> \<box>F & \<diamond>G \<longrightarrow> \<diamond>(F & G)"
   1.329    apply (unfold dmd_def)
   1.330    apply clarsimp
   1.331    apply merge_box
   1.332    apply (fastforce elim!: notE STL4E [temp_use])
   1.333    done
   1.334  
   1.335 -lemma BoxDmd2_simple: "|- \<box>F & \<diamond>G --> \<diamond>(G & F)"
   1.336 +lemma BoxDmd2_simple: "\<turnstile> \<box>F & \<diamond>G \<longrightarrow> \<diamond>(G & F)"
   1.337    apply (unfold dmd_def)
   1.338    apply clarsimp
   1.339    apply merge_box
   1.340 @@ -381,15 +381,15 @@
   1.341    done
   1.342  
   1.343  lemma DmdImpldup:
   1.344 -  assumes 1: "sigma |= \<box>A"
   1.345 -    and 2: "sigma |= \<diamond>F"
   1.346 -    and 3: "|- \<box>A & F --> G"
   1.347 -  shows "sigma |= \<diamond>G"
   1.348 +  assumes 1: "sigma \<Turnstile> \<box>A"
   1.349 +    and 2: "sigma \<Turnstile> \<diamond>F"
   1.350 +    and 3: "\<turnstile> \<box>A & F \<longrightarrow> G"
   1.351 +  shows "sigma \<Turnstile> \<diamond>G"
   1.352    apply (rule 2 [THEN 1 [THEN BoxDmd [temp_use]], THEN DmdImplE])
   1.353    apply (rule 3)
   1.354    done
   1.355  
   1.356 -lemma STL6: "|- \<diamond>\<box>F & \<diamond>\<box>G --> \<diamond>\<box>(F & G)"
   1.357 +lemma STL6: "\<turnstile> \<diamond>\<box>F & \<diamond>\<box>G \<longrightarrow> \<diamond>\<box>(F & G)"
   1.358    apply (auto simp: STL5 [temp_rewrite, symmetric])
   1.359    apply (drule linT [temp_use])
   1.360     apply assumption
   1.361 @@ -410,13 +410,13 @@
   1.362  (* ------------------------ True / False ----------------------------------------- *)
   1.363  section "Simplification of constants"
   1.364  
   1.365 -lemma BoxConst: "|- (\<box>#P) = #P"
   1.366 +lemma BoxConst: "\<turnstile> (\<box>#P) = #P"
   1.367    apply (rule tempI)
   1.368    apply (cases P)
   1.369     apply (auto intro!: necT [temp_use] dest: STL2_gen [temp_use] simp: Init_simps)
   1.370    done
   1.371  
   1.372 -lemma DmdConst: "|- (\<diamond>#P) = #P"
   1.373 +lemma DmdConst: "\<turnstile> (\<diamond>#P) = #P"
   1.374    apply (unfold dmd_def)
   1.375    apply (cases P)
   1.376    apply (simp_all add: BoxConst [try_rewrite])
   1.377 @@ -428,10 +428,10 @@
   1.378  (* ------------------------ Further rewrites ----------------------------------------- *)
   1.379  section "Further rewrites"
   1.380  
   1.381 -lemma NotBox: "|- (\<not>\<box>F) = (\<diamond>\<not>F)"
   1.382 +lemma NotBox: "\<turnstile> (\<not>\<box>F) = (\<diamond>\<not>F)"
   1.383    by (simp add: dmd_def)
   1.384  
   1.385 -lemma NotDmd: "|- (\<not>\<diamond>F) = (\<box>\<not>F)"
   1.386 +lemma NotDmd: "\<turnstile> (\<not>\<diamond>F) = (\<box>\<not>F)"
   1.387    by (simp add: dmd_def)
   1.388  
   1.389  (* These are not declared by default, because they could be harmful,
   1.390 @@ -441,10 +441,10 @@
   1.391    NotBox [temp_unlift, THEN eq_reflection]
   1.392    NotDmd [temp_unlift, THEN eq_reflection]
   1.393  
   1.394 -lemma BoxDmdBox: "|- (\<box>\<diamond>\<box>F) = (\<diamond>\<box>F)"
   1.395 +lemma BoxDmdBox: "\<turnstile> (\<box>\<diamond>\<box>F) = (\<diamond>\<box>F)"
   1.396    apply (auto dest!: STL2 [temp_use])
   1.397    apply (rule ccontr)
   1.398 -  apply (subgoal_tac "sigma |= \<diamond>\<box>\<box>F & \<diamond>\<box>\<not>\<box>F")
   1.399 +  apply (subgoal_tac "sigma \<Turnstile> \<diamond>\<box>\<box>F & \<diamond>\<box>\<not>\<box>F")
   1.400     apply (erule thin_rl)
   1.401     apply auto
   1.402      apply (drule STL6 [temp_use])
   1.403 @@ -453,7 +453,7 @@
   1.404     apply (simp_all add: more_temp_simps1)
   1.405    done
   1.406  
   1.407 -lemma DmdBoxDmd: "|- (\<diamond>\<box>\<diamond>F) = (\<box>\<diamond>F)"
   1.408 +lemma DmdBoxDmd: "\<turnstile> (\<diamond>\<box>\<diamond>F) = (\<box>\<diamond>F)"
   1.409    apply (unfold dmd_def)
   1.410    apply (auto simp: BoxDmdBox [unfolded dmd_def, try_rewrite])
   1.411    done
   1.412 @@ -463,11 +463,11 @@
   1.413  
   1.414  (* ------------------------ Miscellaneous ----------------------------------- *)
   1.415  
   1.416 -lemma BoxOr: "\<And>sigma. [| sigma |= \<box>F | \<box>G |] ==> sigma |= \<box>(F | G)"
   1.417 +lemma BoxOr: "\<And>sigma. \<lbrakk> sigma \<Turnstile> \<box>F | \<box>G \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>(F | G)"
   1.418    by (fastforce elim!: STL4E [temp_use])
   1.419  
   1.420  (* "persistently implies infinitely often" *)
   1.421 -lemma DBImplBD: "|- \<diamond>\<box>F --> \<box>\<diamond>F"
   1.422 +lemma DBImplBD: "\<turnstile> \<diamond>\<box>F \<longrightarrow> \<box>\<diamond>F"
   1.423    apply clarsimp
   1.424    apply (rule ccontr)
   1.425    apply (simp add: more_temp_simps2)
   1.426 @@ -476,13 +476,13 @@
   1.427    apply simp
   1.428    done
   1.429  
   1.430 -lemma BoxDmdDmdBox: "|- \<box>\<diamond>F & \<diamond>\<box>G --> \<box>\<diamond>(F & G)"
   1.431 +lemma BoxDmdDmdBox: "\<turnstile> \<box>\<diamond>F & \<diamond>\<box>G \<longrightarrow> \<box>\<diamond>(F & G)"
   1.432    apply clarsimp
   1.433    apply (rule ccontr)
   1.434    apply (unfold more_temp_simps2)
   1.435    apply (drule STL6 [temp_use])
   1.436     apply assumption
   1.437 -  apply (subgoal_tac "sigma |= \<diamond>\<box>\<not>F")
   1.438 +  apply (subgoal_tac "sigma \<Turnstile> \<diamond>\<box>\<not>F")
   1.439     apply (force simp: dmd_def)
   1.440    apply (fastforce elim: DmdImplE [temp_use] STL4E [temp_use])
   1.441    done
   1.442 @@ -494,11 +494,11 @@
   1.443  section "priming"
   1.444  
   1.445  (* ------------------------ TLA2 ------------------------------------------- *)
   1.446 -lemma STL2_pr: "|- \<box>P --> Init P & Init P`"
   1.447 +lemma STL2_pr: "\<turnstile> \<box>P \<longrightarrow> Init P & Init P`"
   1.448    by (fastforce intro!: STL2_gen [temp_use] primeI [temp_use])
   1.449  
   1.450  (* Auxiliary lemma allows priming of boxed actions *)
   1.451 -lemma BoxPrime: "|- \<box>P --> \<box>($P & P$)"
   1.452 +lemma BoxPrime: "\<turnstile> \<box>P \<longrightarrow> \<box>($P & P$)"
   1.453    apply clarsimp
   1.454    apply (erule dup_boxE)
   1.455    apply (unfold boxInit_act)
   1.456 @@ -507,18 +507,18 @@
   1.457    done
   1.458  
   1.459  lemma TLA2:
   1.460 -  assumes "|- $P & P$ --> A"
   1.461 -  shows "|- \<box>P --> \<box>A"
   1.462 +  assumes "\<turnstile> $P & P$ \<longrightarrow> A"
   1.463 +  shows "\<turnstile> \<box>P \<longrightarrow> \<box>A"
   1.464    apply clarsimp
   1.465    apply (drule BoxPrime [temp_use])
   1.466    apply (auto simp: Init_stp_act_rev [try_rewrite] intro!: assms [temp_use]
   1.467      elim!: STL4E [temp_use])
   1.468    done
   1.469  
   1.470 -lemma TLA2E: "[| sigma |= \<box>P; |- $P & P$ --> A |] ==> sigma |= \<box>A"
   1.471 +lemma TLA2E: "\<lbrakk> sigma \<Turnstile> \<box>P; \<turnstile> $P & P$ \<longrightarrow> A \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>A"
   1.472    by (erule (1) TLA2 [temp_use])
   1.473  
   1.474 -lemma DmdPrime: "|- (\<diamond>P`) --> (\<diamond>P)"
   1.475 +lemma DmdPrime: "\<turnstile> (\<diamond>P`) \<longrightarrow> (\<diamond>P)"
   1.476    apply (unfold dmd_def)
   1.477    apply (fastforce elim!: TLA2E [temp_use])
   1.478    done
   1.479 @@ -529,13 +529,13 @@
   1.480  section "stable, invariant"
   1.481  
   1.482  lemma ind_rule:
   1.483 -   "[| sigma |= \<box>H; sigma |= Init P; |- H --> (Init P & \<not>\<box>F --> Init(P`) & F) |]
   1.484 -    ==> sigma |= \<box>F"
   1.485 +   "\<lbrakk> sigma \<Turnstile> \<box>H; sigma \<Turnstile> Init P; \<turnstile> H \<longrightarrow> (Init P & \<not>\<box>F \<longrightarrow> Init(P`) & F) \<rbrakk>
   1.486 +    \<Longrightarrow> sigma \<Turnstile> \<box>F"
   1.487    apply (rule indT [temp_use])
   1.488     apply (erule (2) STL4E)
   1.489    done
   1.490  
   1.491 -lemma box_stp_act: "|- (\<box>$P) = (\<box>P)"
   1.492 +lemma box_stp_act: "\<turnstile> (\<box>$P) = (\<box>P)"
   1.493    by (simp add: boxInit_act Init_simps)
   1.494  
   1.495  lemmas box_stp_actI = box_stp_act [temp_use, THEN iffD2]
   1.496 @@ -544,7 +544,7 @@
   1.497  lemmas more_temp_simps3 = box_stp_act [temp_rewrite] more_temp_simps2
   1.498  
   1.499  lemma INV1:
   1.500 -  "|- (Init P) --> (stable P) --> \<box>P"
   1.501 +  "\<turnstile> (Init P) \<longrightarrow> (stable P) \<longrightarrow> \<box>P"
   1.502    apply (unfold stable_def boxInit_stp boxInit_act)
   1.503    apply clarsimp
   1.504    apply (erule ind_rule)
   1.505 @@ -552,23 +552,23 @@
   1.506    done
   1.507  
   1.508  lemma StableT:
   1.509 -    "\<And>P. |- $P & A --> P` ==> |- \<box>A --> stable P"
   1.510 +    "\<And>P. \<turnstile> $P & A \<longrightarrow> P` \<Longrightarrow> \<turnstile> \<box>A \<longrightarrow> stable P"
   1.511    apply (unfold stable_def)
   1.512    apply (fastforce elim!: STL4E [temp_use])
   1.513    done
   1.514  
   1.515 -lemma Stable: "[| sigma |= \<box>A; |- $P & A --> P` |] ==> sigma |= stable P"
   1.516 +lemma Stable: "\<lbrakk> sigma \<Turnstile> \<box>A; \<turnstile> $P & A --> P` \<rbrakk> \<Longrightarrow> sigma \<Turnstile> stable P"
   1.517    by (erule (1) StableT [temp_use])
   1.518  
   1.519  (* Generalization of INV1 *)
   1.520 -lemma StableBox: "|- (stable P) --> \<box>(Init P --> \<box>P)"
   1.521 +lemma StableBox: "\<turnstile> (stable P) \<longrightarrow> \<box>(Init P \<longrightarrow> \<box>P)"
   1.522    apply (unfold stable_def)
   1.523    apply clarsimp
   1.524    apply (erule dup_boxE)
   1.525    apply (force simp: stable_def elim: STL4E [temp_use] INV1 [temp_use])
   1.526    done
   1.527  
   1.528 -lemma DmdStable: "|- (stable P) & \<diamond>P --> \<diamond>\<box>P"
   1.529 +lemma DmdStable: "\<turnstile> (stable P) & \<diamond>P \<longrightarrow> \<diamond>\<box>P"
   1.530    apply clarsimp
   1.531    apply (rule DmdImpl2)
   1.532     prefer 2
   1.533 @@ -579,7 +579,7 @@
   1.534  (* ---------------- (Semi-)automatic invariant tactics ---------------------- *)
   1.535  
   1.536  ML {*
   1.537 -(* inv_tac reduces goals of the form ... ==> sigma |= \<box>P *)
   1.538 +(* inv_tac reduces goals of the form ... \<Longrightarrow> sigma \<Turnstile> \<box>P *)
   1.539  fun inv_tac ctxt =
   1.540    SELECT_GOAL
   1.541      (EVERY
   1.542 @@ -589,7 +589,7 @@
   1.543        TRYALL (etac @{thm Stable})]);
   1.544  
   1.545  (* auto_inv_tac applies inv_tac and then tries to attack the subgoals
   1.546 -   in simple cases it may be able to handle goals like |- MyProg --> \<box>Inv.
   1.547 +   in simple cases it may be able to handle goals like \<turnstile> MyProg \<longrightarrow> \<box>Inv.
   1.548     In these simple cases the simplifier seems to be more useful than the
   1.549     auto-tactic, which applies too much propositional logic and simplifies
   1.550     too late.
   1.551 @@ -609,7 +609,7 @@
   1.552    Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o auto_inv_tac))
   1.553  *}
   1.554  
   1.555 -lemma unless: "|- \<box>($P --> P` | Q`) --> (stable P) | \<diamond>Q"
   1.556 +lemma unless: "\<turnstile> \<box>($P \<longrightarrow> P` | Q`) \<longrightarrow> (stable P) | \<diamond>Q"
   1.557    apply (unfold dmd_def)
   1.558    apply (clarsimp dest!: BoxPrime [temp_use])
   1.559    apply merge_box
   1.560 @@ -622,28 +622,28 @@
   1.561  section "recursive expansions"
   1.562  
   1.563  (* Recursive expansions of \<box> and \<diamond> for state predicates *)
   1.564 -lemma BoxRec: "|- (\<box>P) = (Init P & \<box>P`)"
   1.565 +lemma BoxRec: "\<turnstile> (\<box>P) = (Init P & \<box>P`)"
   1.566    apply (auto intro!: STL2_gen [temp_use])
   1.567     apply (fastforce elim!: TLA2E [temp_use])
   1.568    apply (auto simp: stable_def elim!: INV1 [temp_use] STL4E [temp_use])
   1.569    done
   1.570  
   1.571 -lemma DmdRec: "|- (\<diamond>P) = (Init P | \<diamond>P`)"
   1.572 +lemma DmdRec: "\<turnstile> (\<diamond>P) = (Init P | \<diamond>P`)"
   1.573    apply (unfold dmd_def BoxRec [temp_rewrite])
   1.574    apply (auto simp: Init_simps)
   1.575    done
   1.576  
   1.577 -lemma DmdRec2: "\<And>sigma. [| sigma |= \<diamond>P; sigma |= \<box>\<not>P` |] ==> sigma |= Init P"
   1.578 +lemma DmdRec2: "\<And>sigma. \<lbrakk> sigma \<Turnstile> \<diamond>P; sigma \<Turnstile> \<box>\<not>P` \<rbrakk> \<Longrightarrow> sigma \<Turnstile> Init P"
   1.579    apply (force simp: DmdRec [temp_rewrite] dmd_def)
   1.580    done
   1.581  
   1.582 -lemma InfinitePrime: "|- (\<box>\<diamond>P) = (\<box>\<diamond>P`)"
   1.583 +lemma InfinitePrime: "\<turnstile> (\<box>\<diamond>P) = (\<box>\<diamond>P`)"
   1.584    apply auto
   1.585     apply (rule classical)
   1.586     apply (rule DBImplBD [temp_use])
   1.587 -   apply (subgoal_tac "sigma |= \<diamond>\<box>P")
   1.588 +   apply (subgoal_tac "sigma \<Turnstile> \<diamond>\<box>P")
   1.589      apply (fastforce elim!: DmdImplE [temp_use] TLA2E [temp_use])
   1.590 -   apply (subgoal_tac "sigma |= \<diamond>\<box> (\<diamond>P & \<box>\<not>P`)")
   1.591 +   apply (subgoal_tac "sigma \<Turnstile> \<diamond>\<box> (\<diamond>P & \<box>\<not>P`)")
   1.592      apply (force simp: boxInit_stp [temp_use]
   1.593        elim!: DmdImplE [temp_use] STL4E [temp_use] DmdRec2 [temp_use])
   1.594     apply (force intro!: STL6 [temp_use] simp: more_temp_simps3)
   1.595 @@ -651,7 +651,7 @@
   1.596    done
   1.597  
   1.598  lemma InfiniteEnsures:
   1.599 -  "[| sigma |= \<box>N; sigma |= \<box>\<diamond>A; |- A & N --> P` |] ==> sigma |= \<box>\<diamond>P"
   1.600 +  "\<lbrakk> sigma \<Turnstile> \<box>N; sigma \<Turnstile> \<box>\<diamond>A; \<turnstile> A & N \<longrightarrow> P` \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>\<diamond>P"
   1.601    apply (unfold InfinitePrime [temp_rewrite])
   1.602    apply (rule InfImpl)
   1.603      apply assumption+
   1.604 @@ -661,32 +661,32 @@
   1.605  section "fairness"
   1.606  
   1.607  (* alternative definitions of fairness *)
   1.608 -lemma WF_alt: "|- WF(A)_v = (\<box>\<diamond>\<not>Enabled(<A>_v) | \<box>\<diamond><A>_v)"
   1.609 +lemma WF_alt: "\<turnstile> WF(A)_v = (\<box>\<diamond>\<not>Enabled(<A>_v) | \<box>\<diamond><A>_v)"
   1.610    apply (unfold WF_def dmd_def)
   1.611    apply fastforce
   1.612    done
   1.613  
   1.614 -lemma SF_alt: "|- SF(A)_v = (\<diamond>\<box>\<not>Enabled(<A>_v) | \<box>\<diamond><A>_v)"
   1.615 +lemma SF_alt: "\<turnstile> SF(A)_v = (\<diamond>\<box>\<not>Enabled(<A>_v) | \<box>\<diamond><A>_v)"
   1.616    apply (unfold SF_def dmd_def)
   1.617    apply fastforce
   1.618    done
   1.619  
   1.620  (* theorems to "box" fairness conditions *)
   1.621 -lemma BoxWFI: "|- WF(A)_v --> \<box>WF(A)_v"
   1.622 +lemma BoxWFI: "\<turnstile> WF(A)_v \<longrightarrow> \<box>WF(A)_v"
   1.623    by (auto simp: WF_alt [try_rewrite] more_temp_simps3 intro!: BoxOr [temp_use])
   1.624  
   1.625 -lemma WF_Box: "|- (\<box>WF(A)_v) = WF(A)_v"
   1.626 +lemma WF_Box: "\<turnstile> (\<box>WF(A)_v) = WF(A)_v"
   1.627    by (fastforce intro!: BoxWFI [temp_use] dest!: STL2 [temp_use])
   1.628  
   1.629 -lemma BoxSFI: "|- SF(A)_v --> \<box>SF(A)_v"
   1.630 +lemma BoxSFI: "\<turnstile> SF(A)_v \<longrightarrow> \<box>SF(A)_v"
   1.631    by (auto simp: SF_alt [try_rewrite] more_temp_simps3 intro!: BoxOr [temp_use])
   1.632  
   1.633 -lemma SF_Box: "|- (\<box>SF(A)_v) = SF(A)_v"
   1.634 +lemma SF_Box: "\<turnstile> (\<box>SF(A)_v) = SF(A)_v"
   1.635    by (fastforce intro!: BoxSFI [temp_use] dest!: STL2 [temp_use])
   1.636  
   1.637  lemmas more_temp_simps = more_temp_simps3 WF_Box [temp_rewrite] SF_Box [temp_rewrite]
   1.638  
   1.639 -lemma SFImplWF: "|- SF(A)_v --> WF(A)_v"
   1.640 +lemma SFImplWF: "\<turnstile> SF(A)_v \<longrightarrow> WF(A)_v"
   1.641    apply (unfold SF_def WF_def)
   1.642    apply (fastforce dest!: DBImplBD [temp_use])
   1.643    done
   1.644 @@ -702,28 +702,28 @@
   1.645  
   1.646  section "\<leadsto>"
   1.647  
   1.648 -lemma leadsto_init: "|- (Init F) & (F \<leadsto> G) --> \<diamond>G"
   1.649 +lemma leadsto_init: "\<turnstile> (Init F) & (F \<leadsto> G) \<longrightarrow> \<diamond>G"
   1.650    apply (unfold leadsto_def)
   1.651    apply (auto dest!: STL2 [temp_use])
   1.652    done
   1.653  
   1.654 -(* |- F & (F \<leadsto> G) --> \<diamond>G *)
   1.655 +(* \<turnstile> F & (F \<leadsto> G) \<longrightarrow> \<diamond>G *)
   1.656  lemmas leadsto_init_temp = leadsto_init [where 'a = behavior, unfolded Init_simps]
   1.657  
   1.658 -lemma streett_leadsto: "|- (\<box>\<diamond>Init F --> \<box>\<diamond>G) = (\<diamond>(F \<leadsto> G))"
   1.659 +lemma streett_leadsto: "\<turnstile> (\<box>\<diamond>Init F \<longrightarrow> \<box>\<diamond>G) = (\<diamond>(F \<leadsto> G))"
   1.660    apply (unfold leadsto_def)
   1.661    apply auto
   1.662      apply (simp add: more_temp_simps)
   1.663      apply (fastforce elim!: DmdImplE [temp_use] STL4E [temp_use])
   1.664     apply (fastforce intro!: InitDmd [temp_use] elim!: STL4E [temp_use])
   1.665 -  apply (subgoal_tac "sigma |= \<box>\<diamond>\<diamond>G")
   1.666 +  apply (subgoal_tac "sigma \<Turnstile> \<box>\<diamond>\<diamond>G")
   1.667     apply (simp add: more_temp_simps)
   1.668    apply (drule BoxDmdDmdBox [temp_use])
   1.669     apply assumption
   1.670    apply (fastforce elim!: DmdImplE [temp_use] STL4E [temp_use])
   1.671    done
   1.672  
   1.673 -lemma leadsto_infinite: "|- \<box>\<diamond>F & (F \<leadsto> G) --> \<box>\<diamond>G"
   1.674 +lemma leadsto_infinite: "\<turnstile> \<box>\<diamond>F & (F \<leadsto> G) \<longrightarrow> \<box>\<diamond>G"
   1.675    apply clarsimp
   1.676    apply (erule InitDmd [temp_use, THEN streett_leadsto [temp_unlift, THEN iffD2, THEN mp]])
   1.677    apply (simp add: dmdInitD)
   1.678 @@ -732,18 +732,18 @@
   1.679  (* In particular, strong fairness is a Streett condition. The following
   1.680     rules are sometimes easier to use than WF2 or SF2 below.
   1.681  *)
   1.682 -lemma leadsto_SF: "|- (Enabled(<A>_v) \<leadsto> <A>_v) --> SF(A)_v"
   1.683 +lemma leadsto_SF: "\<turnstile> (Enabled(<A>_v) \<leadsto> <A>_v) \<longrightarrow> SF(A)_v"
   1.684    apply (unfold SF_def)
   1.685    apply (clarsimp elim!: leadsto_infinite [temp_use])
   1.686    done
   1.687  
   1.688 -lemma leadsto_WF: "|- (Enabled(<A>_v) \<leadsto> <A>_v) --> WF(A)_v"
   1.689 +lemma leadsto_WF: "\<turnstile> (Enabled(<A>_v) \<leadsto> <A>_v) \<longrightarrow> WF(A)_v"
   1.690    by (clarsimp intro!: SFImplWF [temp_use] leadsto_SF [temp_use])
   1.691  
   1.692  (* introduce an invariant into the proof of a leadsto assertion.
   1.693 -   \<box>I --> ((P \<leadsto> Q)  =  (P /\ I \<leadsto> Q))
   1.694 +   \<box>I \<longrightarrow> ((P \<leadsto> Q)  =  (P /\ I \<leadsto> Q))
   1.695  *)
   1.696 -lemma INV_leadsto: "|- \<box>I & (P & I \<leadsto> Q) --> (P \<leadsto> Q)"
   1.697 +lemma INV_leadsto: "\<turnstile> \<box>I & (P & I \<leadsto> Q) \<longrightarrow> (P \<leadsto> Q)"
   1.698    apply (unfold leadsto_def)
   1.699    apply clarsimp
   1.700    apply (erule STL4Edup)
   1.701 @@ -751,24 +751,24 @@
   1.702    apply (auto simp: Init_simps dest!: STL2_gen [temp_use])
   1.703    done
   1.704  
   1.705 -lemma leadsto_classical: "|- (Init F & \<box>\<not>G \<leadsto> G) --> (F \<leadsto> G)"
   1.706 +lemma leadsto_classical: "\<turnstile> (Init F & \<box>\<not>G \<leadsto> G) \<longrightarrow> (F \<leadsto> G)"
   1.707    apply (unfold leadsto_def dmd_def)
   1.708    apply (force simp: Init_simps elim!: STL4E [temp_use])
   1.709    done
   1.710  
   1.711 -lemma leadsto_false: "|- (F \<leadsto> #False) = (\<box>~F)"
   1.712 +lemma leadsto_false: "\<turnstile> (F \<leadsto> #False) = (\<box>~F)"
   1.713    apply (unfold leadsto_def)
   1.714    apply (simp add: boxNotInitD)
   1.715    done
   1.716  
   1.717 -lemma leadsto_exists: "|- ((\<exists>x. F x) \<leadsto> G) = (\<forall>x. (F x \<leadsto> G))"
   1.718 +lemma leadsto_exists: "\<turnstile> ((\<exists>x. F x) \<leadsto> G) = (\<forall>x. (F x \<leadsto> G))"
   1.719    apply (unfold leadsto_def)
   1.720    apply (auto simp: allT [try_rewrite] Init_simps elim!: STL4E [temp_use])
   1.721    done
   1.722  
   1.723  (* basic leadsto properties, cf. Unity *)
   1.724  
   1.725 -lemma ImplLeadsto_gen: "|- \<box>(Init F --> Init G) --> (F \<leadsto> G)"
   1.726 +lemma ImplLeadsto_gen: "\<turnstile> \<box>(Init F \<longrightarrow> Init G) \<longrightarrow> (F \<leadsto> G)"
   1.727    apply (unfold leadsto_def)
   1.728    apply (auto intro!: InitDmd_gen [temp_use]
   1.729      elim!: STL4E_gen [temp_use] simp: Init_simps)
   1.730 @@ -777,19 +777,19 @@
   1.731  lemmas ImplLeadsto =
   1.732    ImplLeadsto_gen [where 'a = behavior and 'b = behavior, unfolded Init_simps]
   1.733  
   1.734 -lemma ImplLeadsto_simple: "\<And>F G. |- F --> G ==> |- F \<leadsto> G"
   1.735 +lemma ImplLeadsto_simple: "\<And>F G. \<turnstile> F \<longrightarrow> G \<Longrightarrow> \<turnstile> F \<leadsto> G"
   1.736    by (auto simp: Init_def intro!: ImplLeadsto_gen [temp_use] necT [temp_use])
   1.737  
   1.738  lemma EnsuresLeadsto:
   1.739 -  assumes "|- A & $P --> Q`"
   1.740 -  shows "|- \<box>A --> (P \<leadsto> Q)"
   1.741 +  assumes "\<turnstile> A & $P \<longrightarrow> Q`"
   1.742 +  shows "\<turnstile> \<box>A \<longrightarrow> (P \<leadsto> Q)"
   1.743    apply (unfold leadsto_def)
   1.744    apply (clarsimp elim!: INV_leadsto [temp_use])
   1.745    apply (erule STL4E_gen)
   1.746    apply (auto simp: Init_defs intro!: PrimeDmd [temp_use] assms [temp_use])
   1.747    done
   1.748  
   1.749 -lemma EnsuresLeadsto2: "|- \<box>($P --> Q`) --> (P \<leadsto> Q)"
   1.750 +lemma EnsuresLeadsto2: "\<turnstile> \<box>($P \<longrightarrow> Q`) \<longrightarrow> (P \<leadsto> Q)"
   1.751    apply (unfold leadsto_def)
   1.752    apply clarsimp
   1.753    apply (erule STL4E_gen)
   1.754 @@ -797,15 +797,15 @@
   1.755    done
   1.756  
   1.757  lemma ensures:
   1.758 -  assumes 1: "|- $P & N --> P` | Q`"
   1.759 -    and 2: "|- ($P & N) & A --> Q`"
   1.760 -  shows "|- \<box>N & \<box>(\<box>P --> \<diamond>A) --> (P \<leadsto> Q)"
   1.761 +  assumes 1: "\<turnstile> $P & N \<longrightarrow> P` | Q`"
   1.762 +    and 2: "\<turnstile> ($P & N) & A \<longrightarrow> Q`"
   1.763 +  shows "\<turnstile> \<box>N & \<box>(\<box>P \<longrightarrow> \<diamond>A) \<longrightarrow> (P \<leadsto> Q)"
   1.764    apply (unfold leadsto_def)
   1.765    apply clarsimp
   1.766    apply (erule STL4Edup)
   1.767     apply assumption
   1.768    apply clarsimp
   1.769 -  apply (subgoal_tac "sigmaa |= \<box>($P --> P` | Q`) ")
   1.770 +  apply (subgoal_tac "sigmaa \<Turnstile> \<box>($P \<longrightarrow> P` | Q`) ")
   1.771     apply (drule unless [temp_use])
   1.772     apply (clarsimp dest!: INV1 [temp_use])
   1.773    apply (rule 2 [THEN DmdImpl, temp_use, THEN DmdPrime [temp_use]])
   1.774 @@ -815,16 +815,16 @@
   1.775    done
   1.776  
   1.777  lemma ensures_simple:
   1.778 -  "[| |- $P & N --> P` | Q`;
   1.779 -      |- ($P & N) & A --> Q`
   1.780 -   |] ==> |- \<box>N & \<box>\<diamond>A --> (P \<leadsto> Q)"
   1.781 +  "\<lbrakk> \<turnstile> $P & N \<longrightarrow> P` | Q`;
   1.782 +      \<turnstile> ($P & N) & A \<longrightarrow> Q`
   1.783 +   \<rbrakk> \<Longrightarrow> \<turnstile> \<box>N & \<box>\<diamond>A \<longrightarrow> (P \<leadsto> Q)"
   1.784    apply clarsimp
   1.785    apply (erule (2) ensures [temp_use])
   1.786    apply (force elim!: STL4E [temp_use])
   1.787    done
   1.788  
   1.789  lemma EnsuresInfinite:
   1.790 -    "[| sigma |= \<box>\<diamond>P; sigma |= \<box>A; |- A & $P --> Q` |] ==> sigma |= \<box>\<diamond>Q"
   1.791 +    "\<lbrakk> sigma \<Turnstile> \<box>\<diamond>P; sigma \<Turnstile> \<box>A; \<turnstile> A & $P \<longrightarrow> Q` \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>\<diamond>Q"
   1.792    apply (erule leadsto_infinite [temp_use])
   1.793    apply (erule EnsuresLeadsto [temp_use])
   1.794    apply assumption
   1.795 @@ -834,64 +834,64 @@
   1.796  (*** Gronning's lattice rules (taken from TLP) ***)
   1.797  section "Lattice rules"
   1.798  
   1.799 -lemma LatticeReflexivity: "|- F \<leadsto> F"
   1.800 +lemma LatticeReflexivity: "\<turnstile> F \<leadsto> F"
   1.801    apply (unfold leadsto_def)
   1.802    apply (rule necT InitDmd_gen)+
   1.803    done
   1.804  
   1.805 -lemma LatticeTransitivity: "|- (G \<leadsto> H) & (F \<leadsto> G) --> (F \<leadsto> H)"
   1.806 +lemma LatticeTransitivity: "\<turnstile> (G \<leadsto> H) & (F \<leadsto> G) \<longrightarrow> (F \<leadsto> H)"
   1.807    apply (unfold leadsto_def)
   1.808    apply clarsimp
   1.809 -  apply (erule dup_boxE) (* \<box>\<box>(Init G --> H) *)
   1.810 +  apply (erule dup_boxE) (* \<box>\<box>(Init G \<longrightarrow> H) *)
   1.811    apply merge_box
   1.812    apply (clarsimp elim!: STL4E [temp_use])
   1.813    apply (rule dup_dmdD)
   1.814 -  apply (subgoal_tac "sigmaa |= \<diamond>Init G")
   1.815 +  apply (subgoal_tac "sigmaa \<Turnstile> \<diamond>Init G")
   1.816     apply (erule DmdImpl2)
   1.817     apply assumption
   1.818    apply (simp add: dmdInitD)
   1.819    done
   1.820  
   1.821 -lemma LatticeDisjunctionElim1: "|- (F | G \<leadsto> H) --> (F \<leadsto> H)"
   1.822 +lemma LatticeDisjunctionElim1: "\<turnstile> (F | G \<leadsto> H) \<longrightarrow> (F \<leadsto> H)"
   1.823    apply (unfold leadsto_def)
   1.824    apply (auto simp: Init_simps elim!: STL4E [temp_use])
   1.825    done
   1.826  
   1.827 -lemma LatticeDisjunctionElim2: "|- (F | G \<leadsto> H) --> (G \<leadsto> H)"
   1.828 +lemma LatticeDisjunctionElim2: "\<turnstile> (F | G \<leadsto> H) \<longrightarrow> (G \<leadsto> H)"
   1.829    apply (unfold leadsto_def)
   1.830    apply (auto simp: Init_simps elim!: STL4E [temp_use])
   1.831    done
   1.832  
   1.833 -lemma LatticeDisjunctionIntro: "|- (F \<leadsto> H) & (G \<leadsto> H) --> (F | G \<leadsto> H)"
   1.834 +lemma LatticeDisjunctionIntro: "\<turnstile> (F \<leadsto> H) & (G \<leadsto> H) \<longrightarrow> (F | G \<leadsto> H)"
   1.835    apply (unfold leadsto_def)
   1.836    apply clarsimp
   1.837    apply merge_box
   1.838    apply (auto simp: Init_simps elim!: STL4E [temp_use])
   1.839    done
   1.840  
   1.841 -lemma LatticeDisjunction: "|- (F | G \<leadsto> H) = ((F \<leadsto> H) & (G \<leadsto> H))"
   1.842 +lemma LatticeDisjunction: "\<turnstile> (F | G \<leadsto> H) = ((F \<leadsto> H) & (G \<leadsto> H))"
   1.843    by (auto intro: LatticeDisjunctionIntro [temp_use]
   1.844      LatticeDisjunctionElim1 [temp_use]
   1.845      LatticeDisjunctionElim2 [temp_use])
   1.846  
   1.847 -lemma LatticeDiamond: "|- (A \<leadsto> B | C) & (B \<leadsto> D) & (C \<leadsto> D) --> (A \<leadsto> D)"
   1.848 +lemma LatticeDiamond: "\<turnstile> (A \<leadsto> B | C) & (B \<leadsto> D) & (C \<leadsto> D) \<longrightarrow> (A \<leadsto> D)"
   1.849    apply clarsimp
   1.850 -  apply (subgoal_tac "sigma |= (B | C) \<leadsto> D")
   1.851 +  apply (subgoal_tac "sigma \<Turnstile> (B | C) \<leadsto> D")
   1.852    apply (erule_tac G = "LIFT (B | C)" in LatticeTransitivity [temp_use])
   1.853     apply (fastforce intro!: LatticeDisjunctionIntro [temp_use])+
   1.854    done
   1.855  
   1.856 -lemma LatticeTriangle: "|- (A \<leadsto> D | B) & (B \<leadsto> D) --> (A \<leadsto> D)"
   1.857 +lemma LatticeTriangle: "\<turnstile> (A \<leadsto> D | B) & (B \<leadsto> D) \<longrightarrow> (A \<leadsto> D)"
   1.858    apply clarsimp
   1.859 -  apply (subgoal_tac "sigma |= (D | B) \<leadsto> D")
   1.860 +  apply (subgoal_tac "sigma \<Turnstile> (D | B) \<leadsto> D")
   1.861     apply (erule_tac G = "LIFT (D | B)" in LatticeTransitivity [temp_use])
   1.862    apply assumption
   1.863    apply (auto intro: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use])
   1.864    done
   1.865  
   1.866 -lemma LatticeTriangle2: "|- (A \<leadsto> B | D) & (B \<leadsto> D) --> (A \<leadsto> D)"
   1.867 +lemma LatticeTriangle2: "\<turnstile> (A \<leadsto> B | D) & (B \<leadsto> D) \<longrightarrow> (A \<leadsto> D)"
   1.868    apply clarsimp
   1.869 -  apply (subgoal_tac "sigma |= B | D \<leadsto> D")
   1.870 +  apply (subgoal_tac "sigma \<Turnstile> B | D \<leadsto> D")
   1.871     apply (erule_tac G = "LIFT (B | D)" in LatticeTransitivity [temp_use])
   1.872     apply assumption
   1.873    apply (auto intro: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use])
   1.874 @@ -901,10 +901,10 @@
   1.875  section "Fairness rules"
   1.876  
   1.877  lemma WF1:
   1.878 -  "[| |- $P & N  --> P` | Q`;
   1.879 -      |- ($P & N) & <A>_v --> Q`;
   1.880 -      |- $P & N --> $(Enabled(<A>_v)) |]
   1.881 -  ==> |- \<box>N & WF(A)_v --> (P \<leadsto> Q)"
   1.882 +  "\<lbrakk> \<turnstile> $P & N  \<longrightarrow> P` | Q`;
   1.883 +      \<turnstile> ($P & N) & <A>_v \<longrightarrow> Q`;
   1.884 +      \<turnstile> $P & N \<longrightarrow> $(Enabled(<A>_v)) \<rbrakk>
   1.885 +  \<Longrightarrow> \<turnstile> \<box>N & WF(A)_v \<longrightarrow> (P \<leadsto> Q)"
   1.886    apply (clarsimp dest!: BoxWFI [temp_use])
   1.887    apply (erule (2) ensures [temp_use])
   1.888    apply (erule (1) STL4Edup)
   1.889 @@ -917,10 +917,10 @@
   1.890  
   1.891  (* Sometimes easier to use; designed for action B rather than state predicate Q *)
   1.892  lemma WF_leadsto:
   1.893 -  assumes 1: "|- N & $P --> $Enabled (<A>_v)"
   1.894 -    and 2: "|- N & <A>_v --> B"
   1.895 -    and 3: "|- \<box>(N & [~A]_v) --> stable P"
   1.896 -  shows "|- \<box>N & WF(A)_v --> (P \<leadsto> B)"
   1.897 +  assumes 1: "\<turnstile> N & $P \<longrightarrow> $Enabled (<A>_v)"
   1.898 +    and 2: "\<turnstile> N & <A>_v \<longrightarrow> B"
   1.899 +    and 3: "\<turnstile> \<box>(N & [~A]_v) \<longrightarrow> stable P"
   1.900 +  shows "\<turnstile> \<box>N & WF(A)_v \<longrightarrow> (P \<leadsto> B)"
   1.901    apply (unfold leadsto_def)
   1.902    apply (clarsimp dest!: BoxWFI [temp_use])
   1.903    apply (erule (1) STL4Edup)
   1.904 @@ -939,10 +939,10 @@
   1.905    done
   1.906  
   1.907  lemma SF1:
   1.908 -  "[| |- $P & N  --> P` | Q`;
   1.909 -      |- ($P & N) & <A>_v --> Q`;
   1.910 -      |- \<box>P & \<box>N & \<box>F --> \<diamond>Enabled(<A>_v) |]
   1.911 -  ==> |- \<box>N & SF(A)_v & \<box>F --> (P \<leadsto> Q)"
   1.912 +  "\<lbrakk> \<turnstile> $P & N  \<longrightarrow> P` | Q`;
   1.913 +      \<turnstile> ($P & N) & <A>_v \<longrightarrow> Q`;
   1.914 +      \<turnstile> \<box>P & \<box>N & \<box>F \<longrightarrow> \<diamond>Enabled(<A>_v) \<rbrakk>
   1.915 +  \<Longrightarrow> \<turnstile> \<box>N & SF(A)_v & \<box>F \<longrightarrow> (P \<leadsto> Q)"
   1.916    apply (clarsimp dest!: BoxSFI [temp_use])
   1.917    apply (erule (2) ensures [temp_use])
   1.918    apply (erule_tac F = F in dup_boxE)
   1.919 @@ -957,11 +957,11 @@
   1.920    done
   1.921  
   1.922  lemma WF2:
   1.923 -  assumes 1: "|- N & <B>_f --> <M>_g"
   1.924 -    and 2: "|- $P & P` & <N & A>_f --> B"
   1.925 -    and 3: "|- P & Enabled(<M>_g) --> Enabled(<A>_f)"
   1.926 -    and 4: "|- \<box>(N & [~B]_f) & WF(A)_f & \<box>F & \<diamond>\<box>Enabled(<M>_g) --> \<diamond>\<box>P"
   1.927 -  shows "|- \<box>N & WF(A)_f & \<box>F --> WF(M)_g"
   1.928 +  assumes 1: "\<turnstile> N & <B>_f \<longrightarrow> <M>_g"
   1.929 +    and 2: "\<turnstile> $P & P` & <N & A>_f \<longrightarrow> B"
   1.930 +    and 3: "\<turnstile> P & Enabled(<M>_g) \<longrightarrow> Enabled(<A>_f)"
   1.931 +    and 4: "\<turnstile> \<box>(N & [~B]_f) & WF(A)_f & \<box>F & \<diamond>\<box>Enabled(<M>_g) \<longrightarrow> \<diamond>\<box>P"
   1.932 +  shows "\<turnstile> \<box>N & WF(A)_f & \<box>F \<longrightarrow> WF(M)_g"
   1.933    apply (clarsimp dest!: BoxWFI [temp_use] BoxDmdBox [temp_use, THEN iffD2]
   1.934      simp: WF_def [where A = M])
   1.935    apply (erule_tac F = F in dup_boxE)
   1.936 @@ -970,7 +970,7 @@
   1.937     apply assumption
   1.938    apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]])
   1.939    apply (rule classical)
   1.940 -  apply (subgoal_tac "sigmaa |= \<diamond> (($P & P` & N) & <A>_f)")
   1.941 +  apply (subgoal_tac "sigmaa \<Turnstile> \<diamond> (($P & P` & N) & <A>_f)")
   1.942     apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use])
   1.943    apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use])
   1.944    apply (simp add: NotDmd [temp_use] not_angle [try_rewrite])
   1.945 @@ -979,8 +979,8 @@
   1.946       apply assumption+
   1.947    apply (drule STL6 [temp_use])
   1.948     apply assumption
   1.949 -  apply (erule_tac V = "sigmaa |= \<diamond>\<box>P" in thin_rl)
   1.950 -  apply (erule_tac V = "sigmaa |= \<box>F" in thin_rl)
   1.951 +  apply (erule_tac V = "sigmaa \<Turnstile> \<diamond>\<box>P" in thin_rl)
   1.952 +  apply (erule_tac V = "sigmaa \<Turnstile> \<box>F" in thin_rl)
   1.953    apply (drule BoxWFI [temp_use])
   1.954    apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE)
   1.955    apply merge_temp_box
   1.956 @@ -995,11 +995,11 @@
   1.957    done
   1.958  
   1.959  lemma SF2:
   1.960 -  assumes 1: "|- N & <B>_f --> <M>_g"
   1.961 -    and 2: "|- $P & P` & <N & A>_f --> B"
   1.962 -    and 3: "|- P & Enabled(<M>_g) --> Enabled(<A>_f)"
   1.963 -    and 4: "|- \<box>(N & [~B]_f) & SF(A)_f & \<box>F & \<box>\<diamond>Enabled(<M>_g) --> \<diamond>\<box>P"
   1.964 -  shows "|- \<box>N & SF(A)_f & \<box>F --> SF(M)_g"
   1.965 +  assumes 1: "\<turnstile> N & <B>_f \<longrightarrow> <M>_g"
   1.966 +    and 2: "\<turnstile> $P & P` & <N & A>_f \<longrightarrow> B"
   1.967 +    and 3: "\<turnstile> P & Enabled(<M>_g) \<longrightarrow> Enabled(<A>_f)"
   1.968 +    and 4: "\<turnstile> \<box>(N & [~B]_f) & SF(A)_f & \<box>F & \<box>\<diamond>Enabled(<M>_g) \<longrightarrow> \<diamond>\<box>P"
   1.969 +  shows "\<turnstile> \<box>N & SF(A)_f & \<box>F \<longrightarrow> SF(M)_g"
   1.970    apply (clarsimp dest!: BoxSFI [temp_use] simp: 2 [try_rewrite] SF_def [where A = M])
   1.971    apply (erule_tac F = F in dup_boxE)
   1.972    apply (erule_tac F = "TEMP \<diamond>Enabled (<M>_g) " in dup_boxE)
   1.973 @@ -1008,14 +1008,14 @@
   1.974     apply assumption
   1.975    apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]])
   1.976    apply (rule classical)
   1.977 -  apply (subgoal_tac "sigmaa |= \<diamond> (($P & P` & N) & <A>_f)")
   1.978 +  apply (subgoal_tac "sigmaa \<Turnstile> \<diamond> (($P & P` & N) & <A>_f)")
   1.979     apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use])
   1.980    apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use])
   1.981    apply (simp add: NotDmd [temp_use] not_angle [try_rewrite])
   1.982    apply merge_act_box
   1.983    apply (frule 4 [temp_use])
   1.984       apply assumption+
   1.985 -  apply (erule_tac V = "sigmaa |= \<box>F" in thin_rl)
   1.986 +  apply (erule_tac V = "sigmaa \<Turnstile> \<box>F" in thin_rl)
   1.987    apply (drule BoxSFI [temp_use])
   1.988    apply (erule_tac F = "TEMP \<diamond>Enabled (<M>_g)" in dup_boxE)
   1.989    apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE)
   1.990 @@ -1037,8 +1037,8 @@
   1.991  
   1.992  lemma wf_leadsto:
   1.993    assumes 1: "wf r"
   1.994 -    and 2: "\<And>x. sigma |= F x \<leadsto> (G | (\<exists>y. #((y,x):r) & F y))    "
   1.995 -  shows "sigma |= F x \<leadsto> G"
   1.996 +    and 2: "\<And>x. sigma \<Turnstile> F x \<leadsto> (G | (\<exists>y. #((y,x):r) & F y))    "
   1.997 +  shows "sigma \<Turnstile> F x \<leadsto> G"
   1.998    apply (rule 1 [THEN wf_induct])
   1.999    apply (rule LatticeTriangle [temp_use])
  1.1000     apply (rule 2)
  1.1001 @@ -1049,10 +1049,10 @@
  1.1002    done
  1.1003  
  1.1004  (* If r is well-founded, state function v cannot decrease forever *)
  1.1005 -lemma wf_not_box_decrease: "\<And>r. wf r ==> |- \<box>[ (v`, $v) : #r ]_v --> \<diamond>\<box>[#False]_v"
  1.1006 +lemma wf_not_box_decrease: "\<And>r. wf r \<Longrightarrow> \<turnstile> \<box>[ (v`, $v) : #r ]_v \<longrightarrow> \<diamond>\<box>[#False]_v"
  1.1007    apply clarsimp
  1.1008    apply (rule ccontr)
  1.1009 -  apply (subgoal_tac "sigma |= (\<exists>x. v=#x) \<leadsto> #False")
  1.1010 +  apply (subgoal_tac "sigma \<Turnstile> (\<exists>x. v=#x) \<leadsto> #False")
  1.1011     apply (drule leadsto_false [temp_use, THEN iffD1, THEN STL2_gen [temp_use]])
  1.1012     apply (force simp: Init_defs)
  1.1013    apply (clarsimp simp: leadsto_exists [try_rewrite] not_square [try_rewrite] more_temp_simps)
  1.1014 @@ -1061,7 +1061,7 @@
  1.1015     apply (auto simp: square_def angle_def)
  1.1016    done
  1.1017  
  1.1018 -(* "wf r  ==>  |- \<diamond>\<box>[ (v`, $v) : #r ]_v --> \<diamond>\<box>[#False]_v" *)
  1.1019 +(* "wf r  \<Longrightarrow>  \<turnstile> \<diamond>\<box>[ (v`, $v) : #r ]_v \<longrightarrow> \<diamond>\<box>[#False]_v" *)
  1.1020  lemmas wf_not_dmd_box_decrease =
  1.1021    wf_not_box_decrease [THEN DmdImpl, unfolded more_temp_simps]
  1.1022  
  1.1023 @@ -1070,14 +1070,14 @@
  1.1024  *)
  1.1025  lemma wf_box_dmd_decrease:
  1.1026    assumes 1: "wf r"
  1.1027 -  shows "|- \<box>\<diamond>((v`, $v) : #r) --> \<box>\<diamond><(v`, $v) \<notin> #r>_v"
  1.1028 +  shows "\<turnstile> \<box>\<diamond>((v`, $v) : #r) \<longrightarrow> \<box>\<diamond><(v`, $v) \<notin> #r>_v"
  1.1029    apply clarsimp
  1.1030    apply (rule ccontr)
  1.1031    apply (simp add: not_angle [try_rewrite] more_temp_simps)
  1.1032    apply (drule 1 [THEN wf_not_dmd_box_decrease [temp_use]])
  1.1033    apply (drule BoxDmdDmdBox [temp_use])
  1.1034     apply assumption
  1.1035 -  apply (subgoal_tac "sigma |= \<box>\<diamond> ((#False) ::action)")
  1.1036 +  apply (subgoal_tac "sigma \<Turnstile> \<box>\<diamond> ((#False) ::action)")
  1.1037     apply force
  1.1038    apply (erule STL4E)
  1.1039    apply (rule DmdImpl)
  1.1040 @@ -1087,9 +1087,9 @@
  1.1041  (* In particular, for natural numbers, if n decreases infinitely often
  1.1042     then it has to increase infinitely often.
  1.1043  *)
  1.1044 -lemma nat_box_dmd_decrease: "\<And>n::nat stfun. |- \<box>\<diamond>(n` < $n) --> \<box>\<diamond>($n < n`)"
  1.1045 +lemma nat_box_dmd_decrease: "\<And>n::nat stfun. \<turnstile> \<box>\<diamond>(n` < $n) \<longrightarrow> \<box>\<diamond>($n < n`)"
  1.1046    apply clarsimp
  1.1047 -  apply (subgoal_tac "sigma |= \<box>\<diamond><~ ((n`,$n) : #less_than) >_n")
  1.1048 +  apply (subgoal_tac "sigma \<Turnstile> \<box>\<diamond><~ ((n`,$n) : #less_than) >_n")
  1.1049     apply (erule thin_rl)
  1.1050     apply (erule STL4E)
  1.1051     apply (rule DmdImpl)
  1.1052 @@ -1106,11 +1106,11 @@
  1.1053  
  1.1054  lemma aallI:
  1.1055    assumes 1: "basevars vs"
  1.1056 -    and 2: "(\<And>x. basevars (x,vs) ==> sigma |= F x)"
  1.1057 -  shows "sigma |= (\<forall>\<forall>x. F x)"
  1.1058 +    and 2: "(\<And>x. basevars (x,vs) \<Longrightarrow> sigma \<Turnstile> F x)"
  1.1059 +  shows "sigma \<Turnstile> (\<forall>\<forall>x. F x)"
  1.1060    by (auto simp: aall_def elim!: eexE [temp_use] intro!: 1 dest!: 2 [temp_use])
  1.1061  
  1.1062 -lemma aallE: "|- (\<forall>\<forall>x. F x) --> F x"
  1.1063 +lemma aallE: "\<turnstile> (\<forall>\<forall>x. F x) \<longrightarrow> F x"
  1.1064    apply (unfold aall_def)
  1.1065    apply clarsimp
  1.1066    apply (erule contrapos_np)
  1.1067 @@ -1119,18 +1119,18 @@
  1.1068  
  1.1069  (* monotonicity of quantification *)
  1.1070  lemma eex_mono:
  1.1071 -  assumes 1: "sigma |= \<exists>\<exists>x. F x"
  1.1072 -    and 2: "\<And>x. sigma |= F x --> G x"
  1.1073 -  shows "sigma |= \<exists>\<exists>x. G x"
  1.1074 +  assumes 1: "sigma \<Turnstile> \<exists>\<exists>x. F x"
  1.1075 +    and 2: "\<And>x. sigma \<Turnstile> F x \<longrightarrow> G x"
  1.1076 +  shows "sigma \<Turnstile> \<exists>\<exists>x. G x"
  1.1077    apply (rule unit_base [THEN 1 [THEN eexE]])
  1.1078    apply (rule eexI [temp_use])
  1.1079    apply (erule 2 [unfolded intensional_rews, THEN mp])
  1.1080    done
  1.1081  
  1.1082  lemma aall_mono:
  1.1083 -  assumes 1: "sigma |= \<forall>\<forall>x. F(x)"
  1.1084 -    and 2: "\<And>x. sigma |= F(x) --> G(x)"
  1.1085 -  shows "sigma |= \<forall>\<forall>x. G(x)"
  1.1086 +  assumes 1: "sigma \<Turnstile> \<forall>\<forall>x. F(x)"
  1.1087 +    and 2: "\<And>x. sigma \<Turnstile> F(x) \<longrightarrow> G(x)"
  1.1088 +  shows "sigma \<Turnstile> \<forall>\<forall>x. G(x)"
  1.1089    apply (rule unit_base [THEN aallI])
  1.1090    apply (rule 2 [unfolded intensional_rews, THEN mp])
  1.1091    apply (rule 1 [THEN aallE [temp_use]])
  1.1092 @@ -1138,12 +1138,12 @@
  1.1093  
  1.1094  (* Derived history introduction rule *)
  1.1095  lemma historyI:
  1.1096 -  assumes 1: "sigma |= Init I"
  1.1097 -    and 2: "sigma |= \<box>N"
  1.1098 +  assumes 1: "sigma \<Turnstile> Init I"
  1.1099 +    and 2: "sigma \<Turnstile> \<box>N"
  1.1100      and 3: "basevars vs"
  1.1101 -    and 4: "\<And>h. basevars(h,vs) ==> |- I & h = ha --> HI h"
  1.1102 -    and 5: "\<And>h s t. [| basevars(h,vs); N (s,t); h t = hb (h s) (s,t) |] ==> HN h (s,t)"
  1.1103 -  shows "sigma |= \<exists>\<exists>h. Init (HI h) & \<box>(HN h)"
  1.1104 +    and 4: "\<And>h. basevars(h,vs) \<Longrightarrow> \<turnstile> I & h = ha \<longrightarrow> HI h"
  1.1105 +    and 5: "\<And>h s t. \<lbrakk> basevars(h,vs); N (s,t); h t = hb (h s) (s,t) \<rbrakk> \<Longrightarrow> HN h (s,t)"
  1.1106 +  shows "sigma \<Turnstile> \<exists>\<exists>h. Init (HI h) & \<box>(HN h)"
  1.1107    apply (rule history [temp_use, THEN eexE])
  1.1108    apply (rule 3)
  1.1109    apply (rule eexI [temp_use])
  1.1110 @@ -1161,7 +1161,7 @@
  1.1111     example of a history variable: existence of a clock
  1.1112  *)
  1.1113  
  1.1114 -lemma "|- \<exists>\<exists>h. Init(h = #True) & \<box>(h` = (~$h))"
  1.1115 +lemma "\<turnstile> \<exists>\<exists>h. Init(h = #True) & \<box>(h` = (~$h))"
  1.1116    apply (rule tempI)
  1.1117    apply (rule historyI)
  1.1118    apply (force simp: Init_defs intro!: unit_base [temp_use] necT [temp_use])+