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