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.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.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.351
1.352 -lemma NotDmd: "|- (~<>F) = ([]~F)"
1.353 +lemma NotDmd: "|- (\<not>\<diamond>F) = (\<box>\<not>F)"
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.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.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.617
1.618 -lemma leadsto_init: "|- (Init F) & (F ~> G) --> <>G"
1.619 +lemma leadsto_init: "|- (Init F) & (F \<leadsto> G) --> \<diamond>G"
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.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.631    apply auto
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.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.645    apply clarsimp
1.646    apply (erule InitDmd [temp_use, THEN streett_leadsto [temp_unlift, THEN iffD2, THEN mp]])
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.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.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.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.678    apply (force simp: Init_simps elim!: STL4E [temp_use])
1.679    done
1.680
1.681 -lemma leadsto_false: "|- (F ~> #False) = ([]~F)"
1.685    done
1.686
1.687 -lemma leadsto_exists: "|- ((EX x. F x) ~> G) = (ALL x. (F x ~> G))"
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.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.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.709    assumes "|- A & \$P --> Q`"
1.710 -  shows "|- []A --> (P ~> Q)"
1.711 +  shows "|- \<box>A --> (P \<leadsto> Q)"
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.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.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.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.767    apply (rule necT InitDmd_gen)+
1.768    done
1.769
1.770 -lemma LatticeTransitivity: "|- (G ~> H) & (F ~> G) --> (F ~> H)"
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.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.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.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.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.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.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.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.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])+
```