more symbols;
authorwenzelm
Fri Jun 26 11:44:22 2015 +0200 (2015-06-26)
changeset 605870318b43ee95c
parent 60586 1d31e3a50373
child 60588 750c533459b1
more symbols;
src/HOL/TLA/Action.thy
src/HOL/TLA/Buffer/Buffer.thy
src/HOL/TLA/Buffer/DBuffer.thy
src/HOL/TLA/Inc/Inc.thy
src/HOL/TLA/Init.thy
src/HOL/TLA/Intensional.thy
src/HOL/TLA/Memory/MemClerk.thy
src/HOL/TLA/Memory/Memory.thy
src/HOL/TLA/Memory/MemoryImplementation.thy
src/HOL/TLA/Memory/MemoryParameters.thy
src/HOL/TLA/Memory/ProcedureInterface.thy
src/HOL/TLA/Memory/RPC.thy
src/HOL/TLA/Memory/RPCParameters.thy
src/HOL/TLA/Stfun.thy
src/HOL/TLA/TLA.thy
     1.1 --- a/src/HOL/TLA/Action.thy	Fri Jun 26 11:07:04 2015 +0200
     1.2 +++ b/src/HOL/TLA/Action.thy	Fri Jun 26 11:44:22 2015 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOL/TLA/Action.thy 
     1.5 +(*  Title:      HOL/TLA/Action.thy
     1.6      Author:     Stephan Merz
     1.7      Copyright:  1998 University of Munich
     1.8  *)
     1.9 @@ -66,9 +66,9 @@
    1.10  
    1.11  defs
    1.12    square_def:    "ACT [A]_v == ACT (A | unchanged v)"
    1.13 -  angle_def:     "ACT <A>_v == ACT (A & ~ unchanged v)"
    1.14 +  angle_def:     "ACT <A>_v == ACT (A & \<not> unchanged v)"
    1.15  
    1.16 -  enabled_def:   "s |= Enabled A  ==  EX u. (s,u) |= A"
    1.17 +  enabled_def:   "s |= Enabled A  ==  \<exists>u. (s,u) |= A"
    1.18  
    1.19  
    1.20  (* The following assertion specializes "intI" for any world type
    1.21 @@ -76,7 +76,7 @@
    1.22  *)
    1.23  
    1.24  lemma actionI [intro!]:
    1.25 -  assumes "!!s t. (s,t) |= A"
    1.26 +  assumes "\<And>s t. (s,t) |= A"
    1.27    shows "|- A"
    1.28    apply (rule assms intI prod.induct)+
    1.29    done
    1.30 @@ -87,11 +87,11 @@
    1.31  
    1.32  lemma pr_rews [int_rewrite]:
    1.33    "|- (#c)` = #c"
    1.34 -  "!!f. |- f<x>` = f<x` >"
    1.35 -  "!!f. |- f<x,y>` = f<x`,y` >"
    1.36 -  "!!f. |- f<x,y,z>` = f<x`,y`,z` >"
    1.37 -  "|- (! x. P x)` = (! x. (P x)`)"
    1.38 -  "|- (? x. P x)` = (? x. (P x)`)"
    1.39 +  "\<And>f. |- f<x>` = f<x` >"
    1.40 +  "\<And>f. |- f<x,y>` = f<x`,y` >"
    1.41 +  "\<And>f. |- f<x,y,z>` = f<x`,y`,z` >"
    1.42 +  "|- (\<forall>x. P x)` = (\<forall>x. (P x)`)"
    1.43 +  "|- (\<exists>x. P x)` = (\<exists>x. (P x)`)"
    1.44    by (rule actionI, unfold unl_after intensional_rews, rule refl)+
    1.45  
    1.46  
    1.47 @@ -137,7 +137,7 @@
    1.48  
    1.49  lemma busy_squareI: "(s,t) |= A ==> (s,t) |= [A]_v"
    1.50    by (simp add: square_def)
    1.51 -  
    1.52 +
    1.53  lemma squareE [elim]:
    1.54    "[| (s,t) |= [A]_v; A (s,t) ==> B (s,t); v t = v s ==> B (s,t) |] ==> B (s,t)"
    1.55    apply (unfold square_def action_rews)
    1.56 @@ -145,34 +145,34 @@
    1.57    apply simp_all
    1.58    done
    1.59  
    1.60 -lemma squareCI [intro]: "[| v t ~= v s ==> A (s,t) |] ==> (s,t) |= [A]_v"
    1.61 +lemma squareCI [intro]: "[| v t \<noteq> v s ==> A (s,t) |] ==> (s,t) |= [A]_v"
    1.62    apply (unfold square_def action_rews)
    1.63    apply (rule disjCI)
    1.64    apply (erule (1) meta_mp)
    1.65    done
    1.66  
    1.67 -lemma angleI [intro]: "!!s t. [| A (s,t); v t ~= v s |] ==> (s,t) |= <A>_v"
    1.68 +lemma angleI [intro]: "\<And>s t. [| A (s,t); v t \<noteq> v s |] ==> (s,t) |= <A>_v"
    1.69    by (simp add: angle_def)
    1.70  
    1.71 -lemma angleE [elim]: "[| (s,t) |= <A>_v; [| A (s,t); v t ~= v s |] ==> R |] ==> R"
    1.72 +lemma angleE [elim]: "[| (s,t) |= <A>_v; [| A (s,t); v t \<noteq> v s |] ==> R |] ==> R"
    1.73    apply (unfold angle_def action_rews)
    1.74    apply (erule conjE)
    1.75    apply simp
    1.76    done
    1.77  
    1.78  lemma square_simulation:
    1.79 -   "!!f. [| |- unchanged f & ~B --> unchanged g;    
    1.80 -            |- A & ~unchanged g --> B               
    1.81 +   "\<And>f. [| |- unchanged f & \<not>B --> unchanged g;
    1.82 +            |- A & \<not>unchanged g --> B
    1.83           |] ==> |- [A]_f --> [B]_g"
    1.84    apply clarsimp
    1.85    apply (erule squareE)
    1.86    apply (auto simp add: square_def)
    1.87    done
    1.88  
    1.89 -lemma not_square: "|- (~ [A]_v) = <~A>_v"
    1.90 +lemma not_square: "|- (\<not> [A]_v) = <\<not>A>_v"
    1.91    by (auto simp: square_def angle_def)
    1.92  
    1.93 -lemma not_angle: "|- (~ <A>_v) = [~A]_v"
    1.94 +lemma not_angle: "|- (\<not> <A>_v) = [\<not>A]_v"
    1.95    by (auto simp: square_def angle_def)
    1.96  
    1.97  
    1.98 @@ -181,13 +181,13 @@
    1.99  lemma enabledI: "|- A --> $Enabled A"
   1.100    by (auto simp add: enabled_def)
   1.101  
   1.102 -lemma enabledE: "[| s |= Enabled A; !!u. A (s,u) ==> Q |] ==> Q"
   1.103 +lemma enabledE: "[| s |= Enabled A; \<And>u. A (s,u) ==> Q |] ==> Q"
   1.104    apply (unfold enabled_def)
   1.105    apply (erule exE)
   1.106    apply simp
   1.107    done
   1.108  
   1.109 -lemma notEnabledD: "|- ~$Enabled G --> ~ G"
   1.110 +lemma notEnabledD: "|- \<not>$Enabled G --> \<not> G"
   1.111    by (auto simp add: enabled_def)
   1.112  
   1.113  (* Monotonicity *)
   1.114 @@ -203,7 +203,7 @@
   1.115  (* stronger variant *)
   1.116  lemma enabled_mono2:
   1.117    assumes min: "s |= Enabled F"
   1.118 -    and maj: "!!t. F (s,t) ==> G (s,t)"
   1.119 +    and maj: "\<And>t. F (s,t) ==> G (s,t)"
   1.120    shows "s |= Enabled G"
   1.121    apply (rule min [THEN enabledE])
   1.122    apply (rule enabledI [action_use])
   1.123 @@ -239,13 +239,13 @@
   1.124    apply (erule disjE enabled_disj1 [action_use] enabled_disj2 [action_use])+
   1.125    done
   1.126  
   1.127 -lemma enabled_ex: "|- Enabled (EX x. F x) = (EX x. Enabled (F x))"
   1.128 +lemma enabled_ex: "|- Enabled (\<exists>x. F x) = (\<exists>x. Enabled (F x))"
   1.129    by (force simp add: enabled_def)
   1.130  
   1.131  
   1.132  (* A rule that combines enabledI and baseE, but generates fewer instantiations *)
   1.133  lemma base_enabled:
   1.134 -    "[| basevars vs; EX c. ! u. vs u = c --> A(s,u) |] ==> s |= Enabled A"
   1.135 +    "[| basevars vs; \<exists>c. \<forall>u. vs u = c --> A(s,u) |] ==> s |= Enabled A"
   1.136    apply (erule exE)
   1.137    apply (erule baseE)
   1.138    apply (rule enabledI [action_use])
     2.1 --- a/src/HOL/TLA/Buffer/Buffer.thy	Fri Jun 26 11:07:04 2015 +0200
     2.2 +++ b/src/HOL/TLA/Buffer/Buffer.thy	Fri Jun 26 11:44:22 2015 +0200
     2.3 @@ -21,24 +21,24 @@
     2.4  
     2.5  defs
     2.6    BInit_def:   "BInit ic q oc    == PRED q = #[]"
     2.7 -  Enq_def:     "Enq ic q oc      == ACT (ic$ ~= $ic)
     2.8 +  Enq_def:     "Enq ic q oc      == ACT (ic$ \<noteq> $ic)
     2.9                                       & (q$ = $q @ [ ic$ ])
    2.10                                       & (oc$ = $oc)"
    2.11 -  Deq_def:     "Deq ic q oc      == ACT ($q ~= #[])
    2.12 +  Deq_def:     "Deq ic q oc      == ACT ($q \<noteq> #[])
    2.13                                       & (oc$ = hd< $q >)
    2.14                                       & (q$ = tl< $q >)
    2.15                                       & (ic$ = $ic)"
    2.16    Next_def:    "Next ic q oc     == ACT (Enq ic q oc | Deq ic q oc)"
    2.17    IBuffer_def: "IBuffer ic q oc  == TEMP Init (BInit ic q oc)
    2.18 -                                      & [][Next ic q oc]_(ic,q,oc)
    2.19 +                                      & \<box>[Next ic q oc]_(ic,q,oc)
    2.20                                        & WF(Deq ic q oc)_(ic,q,oc)"
    2.21 -  Buffer_def:  "Buffer ic oc     == TEMP (EEX q. IBuffer ic q oc)"
    2.22 +  Buffer_def:  "Buffer ic oc     == TEMP (\<exists>\<exists>q. IBuffer ic q oc)"
    2.23  
    2.24  
    2.25  (* ---------------------------- Data lemmas ---------------------------- *)
    2.26  
    2.27  (*FIXME: move to theory List? Maybe as (tl xs = xs) = (xs = [])"?*)
    2.28 -lemma tl_not_self [simp]: "xs ~= [] ==> tl xs ~= xs"
    2.29 +lemma tl_not_self [simp]: "xs \<noteq> [] ==> tl xs \<noteq> xs"
    2.30    by (auto simp: neq_Nil_conv)
    2.31  
    2.32  
    2.33 @@ -52,14 +52,14 @@
    2.34  
    2.35  (* Enabling condition for dequeue -- NOT NEEDED *)
    2.36  lemma Deq_enabled: 
    2.37 -    "!!q. basevars (ic,q,oc) ==> |- Enabled (<Deq ic q oc>_(ic,q,oc)) = (q ~= #[])"
    2.38 +    "\<And>q. basevars (ic,q,oc) ==> |- Enabled (<Deq ic q oc>_(ic,q,oc)) = (q \<noteq> #[])"
    2.39    apply (unfold Deq_visible [temp_rewrite])
    2.40    apply (force elim!: base_enabled [temp_use] enabledE [temp_use] simp: Deq_def)
    2.41    done
    2.42  
    2.43  (* For the left-to-right implication, we don't need the base variable stuff *)
    2.44  lemma Deq_enabledE: 
    2.45 -    "|- Enabled (<Deq ic q oc>_(ic,q,oc)) --> (q ~= #[])"
    2.46 +    "|- Enabled (<Deq ic q oc>_(ic,q,oc)) --> (q \<noteq> #[])"
    2.47    apply (unfold Deq_visible [temp_rewrite])
    2.48    apply (auto elim!: enabledE simp add: Deq_def)
    2.49    done
     3.1 --- a/src/HOL/TLA/Buffer/DBuffer.thy	Fri Jun 26 11:07:04 2015 +0200
     3.2 +++ b/src/HOL/TLA/Buffer/DBuffer.thy	Fri Jun 26 11:44:22 2015 +0200
     3.3 @@ -37,7 +37,7 @@
     3.4                                   & (out$ = $out)" and
     3.5    DBNext_def:     "DBNext   == ACT  (DBEnq | DBDeq | DBPass)" and
     3.6    DBuffer_def:    "DBuffer  == TEMP Init DBInit
     3.7 -                                 & [][DBNext]_(inp,mid,out,q1,q2)
     3.8 +                                 & \<box>[DBNext]_(inp,mid,out,q1,q2)
     3.9                                   & WF(DBDeq)_(inp,mid,out,q1,q2)
    3.10                                   & WF(DBPass)_(inp,mid,out,q1,q2)"
    3.11  
    3.12 @@ -72,7 +72,7 @@
    3.13    done
    3.14  
    3.15  lemma DBDeq_enabled: 
    3.16 -    "|- Enabled (<DBDeq>_(inp,mid,out,q1,q2)) = (q2 ~= #[])"
    3.17 +    "|- Enabled (<DBDeq>_(inp,mid,out,q1,q2)) = (q2 \<noteq> #[])"
    3.18    apply (unfold DBDeq_visible [action_rewrite])
    3.19    apply (force intro!: DB_base [THEN base_enabled, temp_use]
    3.20      elim!: enabledE simp: angle_def DBDeq_def Deq_def)
    3.21 @@ -82,7 +82,7 @@
    3.22    by (auto simp: angle_def DBPass_def Deq_def)
    3.23  
    3.24  lemma DBPass_enabled: 
    3.25 -    "|- Enabled (<DBPass>_(inp,mid,out,q1,q2)) = (q1 ~= #[])"
    3.26 +    "|- Enabled (<DBPass>_(inp,mid,out,q1,q2)) = (q1 \<noteq> #[])"
    3.27    apply (unfold DBPass_visible [action_rewrite])
    3.28    apply (force intro!: DB_base [THEN base_enabled, temp_use]
    3.29      elim!: enabledE simp: angle_def DBPass_def Deq_def)
    3.30 @@ -90,15 +90,15 @@
    3.31  
    3.32  
    3.33  (* The plan for proving weak fairness at the higher level is to prove
    3.34 -   (0)  DBuffer => (Enabled (Deq inp qc out) ~> (Deq inp qc out))
    3.35 +   (0)  DBuffer => (Enabled (Deq inp qc out) \<leadsto> (Deq inp qc out))
    3.36     which is in turn reduced to the two leadsto conditions
    3.37 -   (1)  DBuffer => (Enabled (Deq inp qc out) ~> q2 ~= [])
    3.38 -   (2)  DBuffer => (q2 ~= [] ~> DBDeq)
    3.39 +   (1)  DBuffer => (Enabled (Deq inp qc out) \<leadsto> q2 \<noteq> [])
    3.40 +   (2)  DBuffer => (q2 \<noteq> [] \<leadsto> DBDeq)
    3.41     and the fact that DBDeq implies <Deq inp qc out>_(inp,qc,out)
    3.42 -   (and therefore DBDeq ~> <Deq inp qc out>_(inp,qc,out) trivially holds).
    3.43 +   (and therefore DBDeq \<leadsto> <Deq inp qc out>_(inp,qc,out) trivially holds).
    3.44  
    3.45     Condition (1) is reduced to
    3.46 -   (1a) DBuffer => (qc ~= [] /\ q2 = [] ~> q2 ~= [])
    3.47 +   (1a) DBuffer => (qc \<noteq> [] /\ q2 = [] \<leadsto> q2 \<noteq> [])
    3.48     by standard leadsto rules (leadsto_classical) and rule Deq_enabledE.
    3.49  
    3.50     Both (1a) and (2) are proved from DBuffer's WF conditions by standard
    3.51 @@ -109,8 +109,8 @@
    3.52  *)
    3.53  
    3.54  (* Condition (1a) *)
    3.55 -lemma DBFair_1a: "|- [][DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)  
    3.56 -         --> (qc ~= #[] & q2 = #[] ~> q2 ~= #[])"
    3.57 +lemma DBFair_1a: "|- \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)  
    3.58 +         --> (qc \<noteq> #[] & q2 = #[] \<leadsto> q2 \<noteq> #[])"
    3.59    apply (rule WF1)
    3.60      apply (force simp: db_defs)
    3.61     apply (force simp: angle_def DBPass_def)
    3.62 @@ -118,8 +118,8 @@
    3.63    done
    3.64  
    3.65  (* Condition (1) *)
    3.66 -lemma DBFair_1: "|- [][DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)  
    3.67 -         --> (Enabled (<Deq inp qc out>_(inp,qc,out)) ~> q2 ~= #[])"
    3.68 +lemma DBFair_1: "|- \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)  
    3.69 +         --> (Enabled (<Deq inp qc out>_(inp,qc,out)) \<leadsto> q2 \<noteq> #[])"
    3.70    apply clarsimp
    3.71    apply (rule leadsto_classical [temp_use])
    3.72    apply (rule DBFair_1a [temp_use, THEN LatticeTransitivity [temp_use]])
    3.73 @@ -130,8 +130,8 @@
    3.74    done
    3.75  
    3.76  (* Condition (2) *)
    3.77 -lemma DBFair_2: "|- [][DBNext]_(inp,mid,out,q1,q2) & WF(DBDeq)_(inp,mid,out,q1,q2)  
    3.78 -         --> (q2 ~= #[] ~> DBDeq)"
    3.79 +lemma DBFair_2: "|- \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBDeq)_(inp,mid,out,q1,q2)  
    3.80 +         --> (q2 \<noteq> #[] \<leadsto> DBDeq)"
    3.81    apply (rule WF_leadsto)
    3.82      apply (force simp: DBDeq_enabled [temp_use])
    3.83     apply (force simp: angle_def)
    3.84 @@ -139,7 +139,7 @@
    3.85    done
    3.86  
    3.87  (* High-level fairness *)
    3.88 -lemma DBFair: "|- [][DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)  
    3.89 +lemma DBFair: "|- \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)  
    3.90                                          & WF(DBDeq)_(inp,mid,out,q1,q2)   
    3.91           --> WF(Deq inp qc out)_(inp,qc,out)"
    3.92    apply (auto simp del: qc_def intro!: leadsto_WF [temp_use]
     4.1 --- a/src/HOL/TLA/Inc/Inc.thy	Fri Jun 26 11:07:04 2015 +0200
     4.2 +++ b/src/HOL/TLA/Inc/Inc.thy	Fri Jun 26 11:44:22 2015 +0200
     4.3 @@ -48,7 +48,7 @@
     4.4    InitPhi_def:   "InitPhi == PRED x = # 0 & y = # 0" and
     4.5    M1_def:        "M1      == ACT  x$ = Suc<$x> & y$ = $y" and
     4.6    M2_def:        "M2      == ACT  y$ = Suc<$y> & x$ = $x" and
     4.7 -  Phi_def:       "Phi     == TEMP Init InitPhi & [][M1 | M2]_(x,y)
     4.8 +  Phi_def:       "Phi     == TEMP Init InitPhi & \<box>[M1 | M2]_(x,y)
     4.9                                   & WF(M1)_(x,y) & WF(M2)_(x,y)" and
    4.10  
    4.11    (* definitions for low-level program *)
    4.12 @@ -69,7 +69,7 @@
    4.13    N1_def:        "N1      == ACT  (alpha1 | beta1 | gamma1)" and
    4.14    N2_def:        "N2      == ACT  (alpha2 | beta2 | gamma2)" and
    4.15    Psi_def:       "Psi     == TEMP Init InitPsi
    4.16 -                               & [][N1 | N2]_(x,y,sem,pc1,pc2)
    4.17 +                               & \<box>[N1 | N2]_(x,y,sem,pc1,pc2)
    4.18                                 & SF(N1)_(x,y,sem,pc1,pc2)
    4.19                                 & SF(N2)_(x,y,sem,pc1,pc2)" and
    4.20  
    4.21 @@ -110,7 +110,7 @@
    4.22  lemma PsiInv_stutter: "|- unchanged (x,y,sem,pc1,pc2) & $PsiInv --> PsiInv$"
    4.23    by (auto simp: PsiInv_defs)
    4.24  
    4.25 -lemma PsiInv: "|- Psi --> []PsiInv"
    4.26 +lemma PsiInv: "|- Psi --> \<box>PsiInv"
    4.27    apply (invariant simp: Psi_def)
    4.28     apply (force simp: PsiInv_Init [try_rewrite] Init_def)
    4.29    apply (auto intro: PsiInv_alpha1 [try_rewrite] PsiInv_alpha2 [try_rewrite]
    4.30 @@ -123,7 +123,7 @@
    4.31     More realistic examples require user guidance anyway.
    4.32  *)
    4.33  
    4.34 -lemma "|- Psi --> []PsiInv"
    4.35 +lemma "|- Psi --> \<box>PsiInv"
    4.36    by (auto_invariant simp: PsiInv_defs Psi_defs)
    4.37  
    4.38  
    4.39 @@ -132,7 +132,7 @@
    4.40  lemma Init_sim: "|- Psi --> Init InitPhi"
    4.41    by (auto simp: InitPhi_def Psi_def InitPsi_def Init_def)
    4.42  
    4.43 -lemma Step_sim: "|- Psi --> [][M1 | M2]_(x,y)"
    4.44 +lemma Step_sim: "|- Psi --> \<box>[M1 | M2]_(x,y)"
    4.45    by (auto simp: square_def M1_def M2_def Psi_defs elim!: STL4E [temp_use])
    4.46  
    4.47  
    4.48 @@ -154,7 +154,7 @@
    4.49     the auxiliary lemmas are very similar.
    4.50  *)
    4.51  
    4.52 -lemma Stuck_at_b: "|- [][(N1 | N2) & ~ beta1]_(x,y,sem,pc1,pc2) --> stable(pc1 = #b)"
    4.53 +lemma Stuck_at_b: "|- \<box>[(N1 | N2) & \<not> beta1]_(x,y,sem,pc1,pc2) --> stable(pc1 = #b)"
    4.54    by (auto elim!: Stable squareE simp: Psi_defs)
    4.55  
    4.56  lemma N1_enabled_at_g: "|- pc1 = #g --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
    4.57 @@ -166,14 +166,14 @@
    4.58    done
    4.59  
    4.60  lemma g1_leadsto_a1:
    4.61 -  "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N1)_(x,y,sem,pc1,pc2) & []#True  
    4.62 -    --> (pc1 = #g ~> pc1 = #a)"
    4.63 +  "|- \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N1)_(x,y,sem,pc1,pc2) & \<box>#True  
    4.64 +    --> (pc1 = #g \<leadsto> pc1 = #a)"
    4.65    apply (rule SF1)
    4.66      apply (tactic
    4.67        {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
    4.68     apply (tactic
    4.69        {* action_simp_tac (@{context} addsimps @{thm angle_def} :: @{thms Psi_defs}) [] [] 1 *})
    4.70 -  (* reduce |- []A --> <>Enabled B  to  |- A --> Enabled B *)
    4.71 +  (* reduce |- \<box>A --> \<diamond>Enabled B  to  |- A --> Enabled B *)
    4.72    apply (auto intro!: InitDmd_gen [temp_use] N1_enabled_at_g [temp_use]
    4.73      dest!: STL2_gen [temp_use] simp: Init_def)
    4.74    done
    4.75 @@ -188,8 +188,8 @@
    4.76    done
    4.77  
    4.78  lemma g2_leadsto_a2:
    4.79 -  "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & []#True  
    4.80 -    --> (pc2 = #g ~> pc2 = #a)"
    4.81 +  "|- \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & \<box>#True  
    4.82 +    --> (pc2 = #g \<leadsto> pc2 = #a)"
    4.83    apply (rule SF1)
    4.84    apply (tactic {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
    4.85    apply (tactic {* action_simp_tac (@{context} addsimps @{thm angle_def} :: @{thms Psi_defs})
    4.86 @@ -207,8 +207,8 @@
    4.87    done
    4.88  
    4.89  lemma b2_leadsto_g2:
    4.90 -  "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & []#True  
    4.91 -    --> (pc2 = #b ~> pc2 = #g)"
    4.92 +  "|- \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & \<box>#True  
    4.93 +    --> (pc2 = #b \<leadsto> pc2 = #g)"
    4.94    apply (rule SF1)
    4.95      apply (tactic
    4.96        {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
    4.97 @@ -220,18 +220,18 @@
    4.98  
    4.99  (* Combine above lemmas: the second component will eventually reach pc2 = a *)
   4.100  lemma N2_leadsto_a:
   4.101 -  "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & []#True  
   4.102 -    --> (pc2 = #a | pc2 = #b | pc2 = #g ~> pc2 = #a)"
   4.103 +  "|- \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & \<box>#True  
   4.104 +    --> (pc2 = #a | pc2 = #b | pc2 = #g \<leadsto> pc2 = #a)"
   4.105    apply (auto intro!: LatticeDisjunctionIntro [temp_use])
   4.106      apply (rule LatticeReflexivity [temp_use])
   4.107     apply (rule LatticeTransitivity [temp_use])
   4.108    apply (auto intro!: b2_leadsto_g2 [temp_use] g2_leadsto_a2 [temp_use])
   4.109    done
   4.110  
   4.111 -(* Get rid of disjunction on the left-hand side of ~> above. *)
   4.112 +(* Get rid of disjunction on the left-hand side of \<leadsto> above. *)
   4.113  lemma N2_live:
   4.114 -  "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2)  
   4.115 -    --> <>(pc2 = #a)"
   4.116 +  "|- \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2)  
   4.117 +    --> \<diamond>(pc2 = #a)"
   4.118    apply (auto simp: Init_defs intro!: N2_leadsto_a [temp_use, THEN [2] leadsto_init [temp_use]])
   4.119    apply (case_tac "pc2 (st1 sigma)")
   4.120      apply auto
   4.121 @@ -249,9 +249,9 @@
   4.122    done
   4.123  
   4.124  lemma a1_leadsto_b1:
   4.125 -  "|- []($PsiInv & [(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2))       
   4.126 -         & SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2)   
   4.127 -         --> (pc1 = #a ~> pc1 = #b)"
   4.128 +  "|- \<box>($PsiInv & [(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2))       
   4.129 +         & SF(N1)_(x,y,sem,pc1,pc2) & \<box> SF(N2)_(x,y,sem,pc1,pc2)   
   4.130 +         --> (pc1 = #a \<leadsto> pc1 = #b)"
   4.131    apply (rule SF1)
   4.132    apply (tactic {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
   4.133    apply (tactic
   4.134 @@ -263,9 +263,9 @@
   4.135  
   4.136  (* Combine the leadsto properties for N1: it will arrive at pc1 = b *)
   4.137  
   4.138 -lemma N1_leadsto_b: "|- []($PsiInv & [(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2))              
   4.139 -         & SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2)   
   4.140 -         --> (pc1 = #b | pc1 = #g | pc1 = #a ~> pc1 = #b)"
   4.141 +lemma N1_leadsto_b: "|- \<box>($PsiInv & [(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2))              
   4.142 +         & SF(N1)_(x,y,sem,pc1,pc2) & \<box> SF(N2)_(x,y,sem,pc1,pc2)   
   4.143 +         --> (pc1 = #b | pc1 = #g | pc1 = #a \<leadsto> pc1 = #b)"
   4.144    apply (auto intro!: LatticeDisjunctionIntro [temp_use])
   4.145      apply (rule LatticeReflexivity [temp_use])
   4.146     apply (rule LatticeTransitivity [temp_use])
   4.147 @@ -273,9 +273,9 @@
   4.148        simp: split_box_conj)
   4.149    done
   4.150  
   4.151 -lemma N1_live: "|- []($PsiInv & [(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2))              
   4.152 -         & SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2)   
   4.153 -         --> <>(pc1 = #b)"
   4.154 +lemma N1_live: "|- \<box>($PsiInv & [(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2))              
   4.155 +         & SF(N1)_(x,y,sem,pc1,pc2) & \<box> SF(N2)_(x,y,sem,pc1,pc2)   
   4.156 +         --> \<diamond>(pc1 = #b)"
   4.157    apply (auto simp: Init_defs intro!: N1_leadsto_b [temp_use, THEN [2] leadsto_init [temp_use]])
   4.158    apply (case_tac "pc1 (st1 sigma)")
   4.159      apply auto
   4.160 @@ -291,8 +291,8 @@
   4.161  
   4.162  (* Now assemble the bits and pieces to prove that Psi is fair. *)
   4.163  
   4.164 -lemma Fair_M1_lemma: "|- []($PsiInv & [(N1 | N2)]_(x,y,sem,pc1,pc2))    
   4.165 -         & SF(N1)_(x,y,sem,pc1,pc2) & []SF(N2)_(x,y,sem,pc1,pc2)   
   4.166 +lemma Fair_M1_lemma: "|- \<box>($PsiInv & [(N1 | N2)]_(x,y,sem,pc1,pc2))    
   4.167 +         & SF(N1)_(x,y,sem,pc1,pc2) & \<box>SF(N2)_(x,y,sem,pc1,pc2)   
   4.168           --> SF(M1)_(x,y)"
   4.169    apply (rule_tac B = beta1 and P = "PRED pc1 = #b" in SF2)
   4.170     (* action premises *)
     5.1 --- a/src/HOL/TLA/Init.thy	Fri Jun 26 11:07:04 2015 +0200
     5.2 +++ b/src/HOL/TLA/Init.thy	Fri Jun 26 11:44:22 2015 +0200
     5.3 @@ -36,9 +36,9 @@
     5.4    Init_def:    "sigma |= Init F  ==  (first_world sigma) |= F"
     5.5  
     5.6  defs (overloaded)
     5.7 -  fw_temp_def: "first_world == %sigma. sigma"
     5.8 +  fw_temp_def: "first_world == \<lambda>sigma. sigma"
     5.9    fw_stp_def:  "first_world == st1"
    5.10 -  fw_act_def:  "first_world == %sigma. (st1 sigma, st2 sigma)"
    5.11 +  fw_act_def:  "first_world == \<lambda>sigma. (st1 sigma, st2 sigma)"
    5.12  
    5.13  lemma const_simps [int_rewrite, simp]:
    5.14    "|- (Init #True) = #True"
    5.15 @@ -46,14 +46,14 @@
    5.16    by (auto simp: Init_def)
    5.17  
    5.18  lemma Init_simps1 [int_rewrite]:
    5.19 -  "!!F. |- (Init ~F) = (~ Init F)"
    5.20 +  "\<And>F. |- (Init \<not>F) = (\<not> Init F)"
    5.21    "|- (Init (P --> Q)) = (Init P --> Init Q)"
    5.22    "|- (Init (P & Q)) = (Init P & Init Q)"
    5.23    "|- (Init (P | Q)) = (Init P | Init Q)"
    5.24    "|- (Init (P = Q)) = ((Init P) = (Init Q))"
    5.25 -  "|- (Init (!x. F x)) = (!x. (Init F x))"
    5.26 -  "|- (Init (? x. F x)) = (? x. (Init F x))"
    5.27 -  "|- (Init (?! x. F x)) = (?! x. (Init F x))"
    5.28 +  "|- (Init (\<forall>x. F x)) = (\<forall>x. (Init F x))"
    5.29 +  "|- (Init (\<exists>x. F x)) = (\<exists>x. (Init F x))"
    5.30 +  "|- (Init (\<exists>!x. F x)) = (\<exists>!x. (Init F x))"
    5.31    by (auto simp: Init_def)
    5.32  
    5.33  lemma Init_stp_act: "|- (Init $P) = (Init P)"
     6.1 --- a/src/HOL/TLA/Intensional.thy	Fri Jun 26 11:07:04 2015 +0200
     6.2 +++ b/src/HOL/TLA/Intensional.thy	Fri Jun 26 11:44:22 2015 +0200
     6.3 @@ -39,7 +39,7 @@
     6.4    ""            :: "var => lift"                         ("_")
     6.5    "_applC"      :: "[lift, cargs] => lift"               ("(1_/ _)" [1000, 1000] 999)
     6.6    ""            :: "lift => lift"                        ("'(_')")
     6.7 -  "_lambda"     :: "[idts, 'a] => lift"                  ("(3%_./ _)" [0, 3] 3)
     6.8 +  "_lambda"     :: "[idts, 'a] => lift"                  ("(3\<lambda>_./ _)" [0, 3] 3)
     6.9    "_constrain"  :: "[lift, type] => lift"                ("(_::_)" [4, 0] 3)
    6.10    ""            :: "lift => liftargs"                    ("_")
    6.11    "_liftargs"   :: "[lift, liftargs] => liftargs"        ("_,/ _")
    6.12 @@ -155,29 +155,17 @@
    6.13    "_liftMem"    :: "[lift, lift] => lift"                ("(_/ \<in> _)" [50, 51] 50)
    6.14    "_liftNotMem" :: "[lift, lift] => lift"                ("(_/ \<notin> _)" [50, 51] 50)
    6.15  
    6.16 -syntax (HTML output)
    6.17 -  "_liftNeq"    :: "[lift, lift] => lift"                (infixl "\<noteq>" 50)
    6.18 -  "_liftNot"    :: "lift => lift"                        ("\<not> _" [40] 40)
    6.19 -  "_liftAnd"    :: "[lift, lift] => lift"                (infixr "\<and>" 35)
    6.20 -  "_liftOr"     :: "[lift, lift] => lift"                (infixr "\<or>" 30)
    6.21 -  "_RAll"       :: "[idts, lift] => lift"                ("(3\<forall>_./ _)" [0, 10] 10)
    6.22 -  "_REx"        :: "[idts, lift] => lift"                ("(3\<exists>_./ _)" [0, 10] 10)
    6.23 -  "_REx1"       :: "[idts, lift] => lift"                ("(3\<exists>!_./ _)" [0, 10] 10)
    6.24 -  "_liftLeq"    :: "[lift, lift] => lift"                ("(_/ \<le> _)" [50, 51] 50)
    6.25 -  "_liftMem"    :: "[lift, lift] => lift"                ("(_/ \<in> _)" [50, 51] 50)
    6.26 -  "_liftNotMem" :: "[lift, lift] => lift"                ("(_/ \<notin> _)" [50, 51] 50)
    6.27 -
    6.28  defs
    6.29 -  Valid_def:   "|- A    ==  ALL w. w |= A"
    6.30 +  Valid_def:   "|- A    ==  \<forall>w. w |= A"
    6.31  
    6.32    unl_con:     "LIFT #c w  ==  c"
    6.33    unl_lift:    "lift f x w == f (x w)"
    6.34    unl_lift2:   "LIFT f<x, y> w == f (x w) (y w)"
    6.35    unl_lift3:   "LIFT f<x, y, z> w == f (x w) (y w) (z w)"
    6.36  
    6.37 -  unl_Rall:    "w |= ALL x. A x  ==  ALL x. (w |= A x)"
    6.38 -  unl_Rex:     "w |= EX x. A x   ==  EX x. (w |= A x)"
    6.39 -  unl_Rex1:    "w |= EX! x. A x  ==  EX! x. (w |= A x)"
    6.40 +  unl_Rall:    "w |= \<forall>x. A x  ==  \<forall>x. (w |= A x)"
    6.41 +  unl_Rex:     "w |= \<exists>x. A x   ==  \<exists> x. (w |= A x)"
    6.42 +  unl_Rex1:    "w |= \<exists>!x. A x  ==  \<exists>!x. (w |= A x)"
    6.43  
    6.44  
    6.45  subsection {* Lemmas and tactics for "intensional" logics. *}
    6.46 @@ -192,7 +180,7 @@
    6.47    apply (erule spec)
    6.48    done
    6.49  
    6.50 -lemma intI [intro!]: "(!!w. w |= A) ==> |- A"
    6.51 +lemma intI [intro!]: "(\<And>w. w |= A) ==> |- A"
    6.52    apply (unfold Valid_def)
    6.53    apply (rule allI)
    6.54    apply (erule meta_spec)
    6.55 @@ -207,21 +195,21 @@
    6.56  
    6.57  lemma int_simps:
    6.58    "|- (x=x) = #True"
    6.59 -  "|- (~#True) = #False"  "|- (~#False) = #True"  "|- (~~ P) = P"
    6.60 -  "|- ((~P) = P) = #False"  "|- (P = (~P)) = #False"
    6.61 -  "|- (P ~= Q) = (P = (~Q))"
    6.62 +  "|- (\<not>#True) = #False"  "|- (\<not>#False) = #True"  "|- (\<not>\<not> P) = P"
    6.63 +  "|- ((\<not>P) = P) = #False"  "|- (P = (\<not>P)) = #False"
    6.64 +  "|- (P \<noteq> Q) = (P = (\<not>Q))"
    6.65    "|- (#True=P) = P"  "|- (P=#True) = P"
    6.66    "|- (#True --> P) = P"  "|- (#False --> P) = #True"
    6.67    "|- (P --> #True) = #True"  "|- (P --> P) = #True"
    6.68 -  "|- (P --> #False) = (~P)"  "|- (P --> ~P) = (~P)"
    6.69 +  "|- (P --> #False) = (\<not>P)"  "|- (P --> \<not>P) = (\<not>P)"
    6.70    "|- (P & #True) = P"  "|- (#True & P) = P"
    6.71    "|- (P & #False) = #False"  "|- (#False & P) = #False"
    6.72 -  "|- (P & P) = P"  "|- (P & ~P) = #False"  "|- (~P & P) = #False"
    6.73 +  "|- (P & P) = P"  "|- (P & \<not>P) = #False"  "|- (\<not>P & P) = #False"
    6.74    "|- (P | #True) = #True"  "|- (#True | P) = #True"
    6.75    "|- (P | #False) = P"  "|- (#False | P) = P"
    6.76 -  "|- (P | P) = P"  "|- (P | ~P) = #True"  "|- (~P | P) = #True"
    6.77 -  "|- (! x. P) = P"  "|- (? x. P) = P"
    6.78 -  "|- (~Q --> ~P) = (P --> Q)"
    6.79 +  "|- (P | P) = P"  "|- (P | \<not>P) = #True"  "|- (\<not>P | P) = #True"
    6.80 +  "|- (\<forall>x. P) = P"  "|- (\<exists>x. P) = P"
    6.81 +  "|- (\<not>Q --> \<not>P) = (P --> Q)"
    6.82    "|- (P|Q --> R) = ((P-->R)&(Q-->R))"
    6.83    apply (unfold Valid_def intensional_rews)
    6.84    apply blast+
    6.85 @@ -296,10 +284,10 @@
    6.86  attribute_setup int_use =
    6.87    {* Scan.succeed (Thm.rule_attribute (int_use o Context.proof_of)) *}
    6.88  
    6.89 -lemma Not_Rall: "|- (~(! x. F x)) = (? x. ~F x)"
    6.90 +lemma Not_Rall: "|- (\<not>(\<forall>x. F x)) = (\<exists>x. \<not>F x)"
    6.91    by (simp add: Valid_def)
    6.92  
    6.93 -lemma Not_Rex: "|- (~ (? x. F x)) = (! x. ~ F x)"
    6.94 +lemma Not_Rex: "|- (\<not> (\<exists>x. F x)) = (\<forall>x. \<not> F x)"
    6.95    by (simp add: Valid_def)
    6.96  
    6.97  end
     7.1 --- a/src/HOL/TLA/Memory/MemClerk.thy	Fri Jun 26 11:07:04 2015 +0200
     7.2 +++ b/src/HOL/TLA/Memory/MemClerk.thy	Fri Jun 26 11:44:22 2015 +0200
     7.3 @@ -16,7 +16,7 @@
     7.4  definition
     7.5    (* state predicates *)
     7.6    MClkInit      :: "mClkRcvChType => mClkStType => PrIds => stpred"
     7.7 -  where "MClkInit rcv cst p = PRED (cst!p = #clkA  &  ~Calling rcv p)"
     7.8 +  where "MClkInit rcv cst p = PRED (cst!p = #clkA  &  \<not>Calling rcv p)"
     7.9  
    7.10  definition
    7.11    (* actions *)
    7.12 @@ -39,7 +39,7 @@
    7.13  definition
    7.14    MClkReply     :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
    7.15    where "MClkReply send rcv cst p = ACT
    7.16 -                           ~$Calling rcv p
    7.17 +                           \<not>$Calling rcv p
    7.18                           & $(cst!p) = #clkB
    7.19                           & Return send p MClkReplyVal<res<rcv!p>>
    7.20                           & (cst!p)$ = #clkA
    7.21 @@ -57,13 +57,13 @@
    7.22    MClkIPSpec    :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => temporal"
    7.23    where "MClkIPSpec send rcv cst p = TEMP
    7.24                             Init MClkInit rcv cst p
    7.25 -                         & [][ MClkNext send rcv cst p ]_(cst!p, rtrner send!p, caller rcv!p)
    7.26 +                         & \<box>[ MClkNext send rcv cst p ]_(cst!p, rtrner send!p, caller rcv!p)
    7.27                           & WF(MClkFwd send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)
    7.28                           & SF(MClkReply send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)"
    7.29  
    7.30  definition
    7.31    MClkISpec     :: "mClkSndChType => mClkRcvChType => mClkStType => temporal"
    7.32 -  where "MClkISpec send rcv cst = TEMP (ALL p. MClkIPSpec send rcv cst p)"
    7.33 +  where "MClkISpec send rcv cst = TEMP (\<forall>p. MClkIPSpec send rcv cst p)"
    7.34  
    7.35  lemmas MC_action_defs =
    7.36    MClkInit_def MClkFwd_def MClkRetry_def MClkReply_def MClkNext_def
    7.37 @@ -73,17 +73,17 @@
    7.38  (* The Clerk engages in an action for process p only if there is an outstanding,
    7.39     unanswered call for that process.
    7.40  *)
    7.41 -lemma MClkidle: "|- ~$Calling send p & $(cst!p) = #clkA --> ~MClkNext send rcv cst p"
    7.42 +lemma MClkidle: "|- \<not>$Calling send p & $(cst!p) = #clkA --> \<not>MClkNext send rcv cst p"
    7.43    by (auto simp: Return_def MC_action_defs)
    7.44  
    7.45 -lemma MClkbusy: "|- $Calling rcv p --> ~MClkNext send rcv cst p"
    7.46 +lemma MClkbusy: "|- $Calling rcv p --> \<not>MClkNext send rcv cst p"
    7.47    by (auto simp: Call_def MC_action_defs)
    7.48  
    7.49  
    7.50  (* Enabledness of actions *)
    7.51  
    7.52 -lemma MClkFwd_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==>  
    7.53 -      |- Calling send p & ~Calling rcv p & cst!p = #clkA   
    7.54 +lemma MClkFwd_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, cst!p) ==>  
    7.55 +      |- Calling send p & \<not>Calling rcv p & cst!p = #clkA   
    7.56           --> Enabled (MClkFwd send rcv cst p)"
    7.57    by (tactic {* action_simp_tac (@{context} addsimps [@{thm MClkFwd_def},
    7.58      @{thm Call_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
    7.59 @@ -97,8 +97,8 @@
    7.60           <MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p)"
    7.61    by (auto simp: angle_def MClkReply_def elim: Return_changed [temp_use])
    7.62  
    7.63 -lemma MClkReply_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==>  
    7.64 -      |- Calling send p & ~Calling rcv p & cst!p = #clkB   
    7.65 +lemma MClkReply_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, cst!p) ==>  
    7.66 +      |- Calling send p & \<not>Calling rcv p & cst!p = #clkB   
    7.67           --> Enabled (<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"
    7.68    apply (tactic {* action_simp_tac @{context}
    7.69      [@{thm MClkReply_change} RSN (2, @{thm enabled_mono})] [] 1 *})
    7.70 @@ -107,7 +107,7 @@
    7.71      [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
    7.72    done
    7.73  
    7.74 -lemma MClkReplyNotRetry: "|- MClkReply send rcv cst p --> ~MClkRetry send rcv cst p"
    7.75 +lemma MClkReplyNotRetry: "|- MClkReply send rcv cst p --> \<not>MClkRetry send rcv cst p"
    7.76    by (auto simp: MClkReply_def MClkRetry_def)
    7.77  
    7.78  end
     8.1 --- a/src/HOL/TLA/Memory/Memory.thy	Fri Jun 26 11:07:04 2015 +0200
     8.2 +++ b/src/HOL/TLA/Memory/Memory.thy	Fri Jun 26 11:44:22 2015 +0200
     8.3 @@ -63,31 +63,31 @@
     8.4                          #l : #MemLoc & ((rs!p)$ = $(mm!l))"
     8.5    (* a read that raises BadArg *)
     8.6    BadRead_def:       "BadRead mm rs p l == ACT
     8.7 -                        #l ~: #MemLoc & ((rs!p)$ = #BadArg)"
     8.8 +                        #l \<notin> #MemLoc & ((rs!p)$ = #BadArg)"
     8.9    (* the read action with l visible *)
    8.10    ReadInner_def:     "ReadInner ch mm rs p l == ACT
    8.11                           $(RdRequest ch p l)
    8.12                           & (GoodRead mm rs p l  |  BadRead mm rs p l)
    8.13                           & unchanged (rtrner ch ! p)"
    8.14    (* the read action with l quantified *)
    8.15 -  Read_def:          "Read ch mm rs p == ACT (EX l. ReadInner ch mm rs p l)"
    8.16 +  Read_def:          "Read ch mm rs p == ACT (\<exists>l. ReadInner ch mm rs p l)"
    8.17  
    8.18    (* similar definitions for the write action *)
    8.19    GoodWrite_def:     "GoodWrite mm rs p l v == ACT
    8.20                          #l : #MemLoc & #v : #MemVal
    8.21                          & ((mm!l)$ = #v) & ((rs!p)$ = #OK)"
    8.22    BadWrite_def:      "BadWrite mm rs p l v == ACT
    8.23 -                        ~ (#l : #MemLoc & #v : #MemVal)
    8.24 +                        \<not> (#l : #MemLoc & #v : #MemVal)
    8.25                          & ((rs!p)$ = #BadArg) & unchanged (mm!l)"
    8.26    WriteInner_def:    "WriteInner ch mm rs p l v == ACT
    8.27                          $(WrRequest ch p l v)
    8.28                          & (GoodWrite mm rs p l v  |  BadWrite mm rs p l v)
    8.29                          & unchanged (rtrner ch ! p)"
    8.30 -  Write_def:         "Write ch mm rs p l == ACT (EX v. WriteInner ch mm rs p l v)"
    8.31 +  Write_def:         "Write ch mm rs p l == ACT (\<exists>v. WriteInner ch mm rs p l v)"
    8.32  
    8.33    (* the return action *)
    8.34    MemReturn_def:     "MemReturn ch rs p == ACT
    8.35 -                       (   ($(rs!p) ~= #NotAResult)
    8.36 +                       (   ($(rs!p) \<noteq> #NotAResult)
    8.37                          & ((rs!p)$ = #NotAResult)
    8.38                          & Return ch p (rs!p))"
    8.39  
    8.40 @@ -99,33 +99,33 @@
    8.41    (* next-state relations for reliable / unreliable memory *)
    8.42    RNext_def:         "RNext ch mm rs p == ACT
    8.43                         (  Read ch mm rs p
    8.44 -                        | (EX l. Write ch mm rs p l)
    8.45 +                        | (\<exists>l. Write ch mm rs p l)
    8.46                          | MemReturn ch rs p)"
    8.47    UNext_def:         "UNext ch mm rs p == ACT
    8.48                          (RNext ch mm rs p | MemFail ch rs p)"
    8.49  
    8.50    RPSpec_def:        "RPSpec ch mm rs p == TEMP
    8.51                          Init(PInit rs p)
    8.52 -                        & [][ RNext ch mm rs p ]_(rtrner ch ! p, rs!p)
    8.53 +                        & \<box>[ RNext ch mm rs p ]_(rtrner ch ! p, rs!p)
    8.54                          & WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
    8.55                          & WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
    8.56    UPSpec_def:        "UPSpec ch mm rs p == TEMP
    8.57                          Init(PInit rs p)
    8.58 -                        & [][ UNext ch mm rs p ]_(rtrner ch ! p, rs!p)
    8.59 +                        & \<box>[ UNext ch mm rs p ]_(rtrner ch ! p, rs!p)
    8.60                          & WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
    8.61                          & WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
    8.62    MSpec_def:         "MSpec ch mm rs l == TEMP
    8.63                          Init(MInit mm l)
    8.64 -                        & [][ EX p. Write ch mm rs p l ]_(mm!l)"
    8.65 +                        & \<box>[ \<exists>p. Write ch mm rs p l ]_(mm!l)"
    8.66    IRSpec_def:        "IRSpec ch mm rs == TEMP
    8.67 -                        (ALL p. RPSpec ch mm rs p)
    8.68 -                        & (ALL l. #l : #MemLoc --> MSpec ch mm rs l)"
    8.69 +                        (\<forall>p. RPSpec ch mm rs p)
    8.70 +                        & (\<forall>l. #l : #MemLoc --> MSpec ch mm rs l)"
    8.71    IUSpec_def:        "IUSpec ch mm rs == TEMP
    8.72 -                        (ALL p. UPSpec ch mm rs p)
    8.73 -                        & (ALL l. #l : #MemLoc --> MSpec ch mm rs l)"
    8.74 +                        (\<forall>p. UPSpec ch mm rs p)
    8.75 +                        & (\<forall>l. #l : #MemLoc --> MSpec ch mm rs l)"
    8.76  
    8.77 -  RSpec_def:         "RSpec ch rs == TEMP (EEX mm. IRSpec ch mm rs)"
    8.78 -  USpec_def:         "USpec ch == TEMP (EEX mm rs. IUSpec ch mm rs)"
    8.79 +  RSpec_def:         "RSpec ch rs == TEMP (\<exists>\<exists>mm. IRSpec ch mm rs)"
    8.80 +  USpec_def:         "USpec ch == TEMP (\<exists>\<exists>mm rs. IUSpec ch mm rs)"
    8.81  
    8.82    MemInv_def:        "MemInv mm l == PRED  #l : #MemLoc --> mm!l : #MemVal"
    8.83  
    8.84 @@ -146,15 +146,15 @@
    8.85    by (force simp: UNext_def UPSpec_def IUSpec_def RM_temp_defs elim!: STL4E [temp_use] squareE)
    8.86  
    8.87  (* The memory spec implies the memory invariant *)
    8.88 -lemma MemoryInvariant: "|- MSpec ch mm rs l --> [](MemInv mm l)"
    8.89 +lemma MemoryInvariant: "|- MSpec ch mm rs l --> \<box>(MemInv mm l)"
    8.90    by (auto_invariant simp: RM_temp_defs RM_action_defs)
    8.91  
    8.92  (* The invariant is trivial for non-locations *)
    8.93 -lemma NonMemLocInvariant: "|- #l ~: #MemLoc --> [](MemInv mm l)"
    8.94 +lemma NonMemLocInvariant: "|- #l \<notin> #MemLoc --> \<box>(MemInv mm l)"
    8.95    by (auto simp: MemInv_def intro!: necT [temp_use])
    8.96  
    8.97  lemma MemoryInvariantAll:
    8.98 -    "|- (ALL l. #l : #MemLoc --> MSpec ch mm rs l) --> (ALL l. [](MemInv mm l))"
    8.99 +    "|- (\<forall>l. #l : #MemLoc --> MSpec ch mm rs l) --> (\<forall>l. \<box>(MemInv mm l))"
   8.100    apply clarify
   8.101    apply (auto elim!: MemoryInvariant [temp_use] NonMemLocInvariant [temp_use])
   8.102    done
   8.103 @@ -164,7 +164,7 @@
   8.104     We need this only for the reliable memory.
   8.105  *)
   8.106  
   8.107 -lemma Memoryidle: "|- ~$(Calling ch p) --> ~ RNext ch mm rs p"
   8.108 +lemma Memoryidle: "|- \<not>$(Calling ch p) --> \<not> RNext ch mm rs p"
   8.109    by (auto simp: Return_def RM_action_defs)
   8.110  
   8.111  (* Enabledness conditions *)
   8.112 @@ -172,8 +172,8 @@
   8.113  lemma MemReturn_change: "|- MemReturn ch rs p --> <MemReturn ch rs p>_(rtrner ch ! p, rs!p)"
   8.114    by (force simp: MemReturn_def angle_def)
   8.115  
   8.116 -lemma MemReturn_enabled: "!!p. basevars (rtrner ch ! p, rs!p) ==>
   8.117 -      |- Calling ch p & (rs!p ~= #NotAResult)
   8.118 +lemma MemReturn_enabled: "\<And>p. basevars (rtrner ch ! p, rs!p) ==>
   8.119 +      |- Calling ch p & (rs!p \<noteq> #NotAResult)
   8.120           --> Enabled (<MemReturn ch rs p>_(rtrner ch ! p, rs!p))"
   8.121    apply (tactic
   8.122      {* action_simp_tac @{context} [@{thm MemReturn_change} RSN (2, @{thm enabled_mono}) ] [] 1 *})
   8.123 @@ -182,14 +182,14 @@
   8.124        @{thm rtrner_def}]) [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
   8.125    done
   8.126  
   8.127 -lemma ReadInner_enabled: "!!p. basevars (rtrner ch ! p, rs!p) ==>
   8.128 +lemma ReadInner_enabled: "\<And>p. basevars (rtrner ch ! p, rs!p) ==>
   8.129        |- Calling ch p & (arg<ch!p> = #(read l)) --> Enabled (ReadInner ch mm rs p l)"
   8.130    apply (case_tac "l : MemLoc")
   8.131    apply (force simp: ReadInner_def GoodRead_def BadRead_def RdRequest_def
   8.132      intro!: exI elim!: base_enabled [temp_use])+
   8.133    done
   8.134  
   8.135 -lemma WriteInner_enabled: "!!p. basevars (mm!l, rtrner ch ! p, rs!p) ==>
   8.136 +lemma WriteInner_enabled: "\<And>p. basevars (mm!l, rtrner ch ! p, rs!p) ==>
   8.137        |- Calling ch p & (arg<ch!p> = #(write l v))
   8.138           --> Enabled (WriteInner ch mm rs p l v)"
   8.139    apply (case_tac "l:MemLoc & v:MemVal")
   8.140 @@ -197,18 +197,18 @@
   8.141      intro!: exI elim!: base_enabled [temp_use])+
   8.142    done
   8.143  
   8.144 -lemma ReadResult: "|- Read ch mm rs p & (!l. $(MemInv mm l)) --> (rs!p)` ~= #NotAResult"
   8.145 +lemma ReadResult: "|- Read ch mm rs p & (\<forall>l. $(MemInv mm l)) --> (rs!p)` \<noteq> #NotAResult"
   8.146    by (force simp: Read_def ReadInner_def GoodRead_def BadRead_def MemInv_def)
   8.147  
   8.148 -lemma WriteResult: "|- Write ch mm rs p l --> (rs!p)` ~= #NotAResult"
   8.149 +lemma WriteResult: "|- Write ch mm rs p l --> (rs!p)` \<noteq> #NotAResult"
   8.150    by (auto simp: Write_def WriteInner_def GoodWrite_def BadWrite_def)
   8.151  
   8.152 -lemma ReturnNotReadWrite: "|- (ALL l. $MemInv mm l) & MemReturn ch rs p
   8.153 -         --> ~ Read ch mm rs p & (ALL l. ~ Write ch mm rs p l)"
   8.154 +lemma ReturnNotReadWrite: "|- (\<forall>l. $MemInv mm l) & MemReturn ch rs p
   8.155 +         --> \<not> Read ch mm rs p & (\<forall>l. \<not> Write ch mm rs p l)"
   8.156    by (auto simp: MemReturn_def dest!: WriteResult [temp_use] ReadResult [temp_use])
   8.157  
   8.158  lemma RWRNext_enabled: "|- (rs!p = #NotAResult) & (!l. MemInv mm l)
   8.159 -         & Enabled (Read ch mm rs p | (? l. Write ch mm rs p l))
   8.160 +         & Enabled (Read ch mm rs p | (\<exists>l. Write ch mm rs p l))
   8.161           --> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))"
   8.162    by (force simp: RNext_def angle_def elim!: enabled_mono2
   8.163      dest: ReadResult [temp_use] WriteResult [temp_use])
   8.164 @@ -217,8 +217,8 @@
   8.165  (* Combine previous lemmas: the memory can make a visible step if there is an
   8.166     outstanding call for which no result has been produced.
   8.167  *)
   8.168 -lemma RNext_enabled: "!!p. !l. basevars (mm!l, rtrner ch!p, rs!p) ==>
   8.169 -      |- (rs!p = #NotAResult) & Calling ch p & (!l. MemInv mm l)
   8.170 +lemma RNext_enabled: "\<And>p. \<forall>l. basevars (mm!l, rtrner ch!p, rs!p) ==>
   8.171 +      |- (rs!p = #NotAResult) & Calling ch p & (\<forall>l. MemInv mm l)
   8.172           --> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))"
   8.173    apply (auto simp: enabled_disj [try_rewrite] intro!: RWRNext_enabled [temp_use])
   8.174    apply (case_tac "arg (ch w p)")
     9.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Fri Jun 26 11:07:04 2015 +0200
     9.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Fri Jun 26 11:44:22 2015 +0200
     9.3 @@ -63,7 +63,7 @@
     9.4  definition
     9.5    (* the environment action *)
     9.6    ENext         :: "PrIds => action"
     9.7 -  where "ENext p = ACT (? l. #l : #MemLoc & Call memCh p #(read l))"
     9.8 +  where "ENext p = ACT (\<exists>l. #l : #MemLoc & Call memCh p #(read l))"
     9.9  
    9.10  
    9.11  definition
    9.12 @@ -83,24 +83,24 @@
    9.13  definition
    9.14    HistP         :: "histType => PrIds => temporal"
    9.15    where "HistP rmhist p = (TEMP Init HInit rmhist p
    9.16 -                           & [][HNext rmhist p]_(c p,r p,m p, rmhist!p))"
    9.17 +                           & \<box>[HNext rmhist p]_(c p,r p,m p, rmhist!p))"
    9.18  
    9.19  definition
    9.20    Hist          :: "histType => temporal"
    9.21 -  where "Hist rmhist = TEMP (ALL p. HistP rmhist p)"
    9.22 +  where "Hist rmhist = TEMP (\<forall>p. HistP rmhist p)"
    9.23  
    9.24  definition
    9.25    (* the implementation *)
    9.26    IPImp          :: "PrIds => temporal"
    9.27 -  where "IPImp p = (TEMP (  Init ~Calling memCh p & [][ENext p]_(e p)
    9.28 +  where "IPImp p = (TEMP (  Init \<not>Calling memCh p & \<box>[ENext p]_(e p)
    9.29                         & MClkIPSpec memCh crCh cst p
    9.30                         & RPCIPSpec crCh rmCh rst p
    9.31                         & RPSpec rmCh mm ires p
    9.32 -                       & (ALL l. #l : #MemLoc --> MSpec rmCh mm ires l)))"
    9.33 +                       & (\<forall>l. #l : #MemLoc --> MSpec rmCh mm ires l)))"
    9.34  
    9.35  definition
    9.36    ImpInit        :: "PrIds => stpred"
    9.37 -  where "ImpInit p = PRED (  ~Calling memCh p
    9.38 +  where "ImpInit p = PRED (  \<not>Calling memCh p
    9.39                            & MClkInit crCh cst p
    9.40                            & RPCInit rmCh rst p
    9.41                            & PInit ires p)"
    9.42 @@ -122,7 +122,7 @@
    9.43  
    9.44  definition
    9.45    Implementation :: "temporal"
    9.46 -  where "Implementation = (TEMP ( (ALL p. Init (~Calling memCh p) & [][ENext p]_(e p))
    9.47 +  where "Implementation = (TEMP ( (\<forall>p. Init (\<not>Calling memCh p) & \<box>[ENext p]_(e p))
    9.48                                 & MClkISpec memCh crCh cst
    9.49                                 & RPCISpec crCh rmCh rst
    9.50                                 & IRSpec rmCh mm ires))"
    9.51 @@ -139,11 +139,11 @@
    9.52                  Calling memCh p = #ecalling
    9.53                & Calling crCh p  = #ccalling
    9.54                & (#ccalling --> arg<crCh!p> = MClkRelayArg<arg<memCh!p>>)
    9.55 -              & (~ #ccalling & cst!p = #clkB --> MVOKBARF<res<crCh!p>>)
    9.56 +              & (\<not> #ccalling & cst!p = #clkB --> MVOKBARF<res<crCh!p>>)
    9.57                & Calling rmCh p  = #rcalling
    9.58                & (#rcalling --> arg<rmCh!p> = RPCRelayArg<arg<crCh!p>>)
    9.59 -              & (~ #rcalling --> ires!p = #NotAResult)
    9.60 -              & (~ #rcalling & rst!p = #rpcB --> MVOKBA<res<rmCh!p>>)
    9.61 +              & (\<not> #rcalling --> ires!p = #NotAResult)
    9.62 +              & (\<not> #rcalling & rst!p = #rpcB --> MVOKBA<res<rmCh!p>>)
    9.63                & cst!p = #cs
    9.64                & rst!p = #rs
    9.65                & (rmhist!p = #hs1 | rmhist!p = #hs2)
    9.66 @@ -241,9 +241,9 @@
    9.67  
    9.68  section "History variable"
    9.69  
    9.70 -lemma HistoryLemma: "|- Init(ALL p. ImpInit p) & [](ALL p. ImpNext p)
    9.71 -         --> (EEX rmhist. Init(ALL p. HInit rmhist p)
    9.72 -                          & [](ALL p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)))"
    9.73 +lemma HistoryLemma: "|- Init(\<forall>p. ImpInit p) & \<box>(\<forall>p. ImpNext p)
    9.74 +         --> (\<exists>\<exists>rmhist. Init(\<forall>p. HInit rmhist p)
    9.75 +                          & \<box>(\<forall>p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)))"
    9.76    apply clarsimp
    9.77    apply (rule historyI)
    9.78        apply assumption+
    9.79 @@ -255,7 +255,7 @@
    9.80    apply (erule fun_cong)
    9.81    done
    9.82  
    9.83 -lemma History: "|- Implementation --> (EEX rmhist. Hist rmhist)"
    9.84 +lemma History: "|- Implementation --> (\<exists>\<exists>rmhist. Hist rmhist)"
    9.85    apply clarsimp
    9.86    apply (rule HistoryLemma [temp_use, THEN eex_mono])
    9.87      prefer 3
    9.88 @@ -274,14 +274,14 @@
    9.89  
    9.90  (* RPCFailure notin MemVals U {OK,BadArg} *)
    9.91  
    9.92 -lemma MVOKBAnotRF: "MVOKBA x ==> x ~= RPCFailure"
    9.93 +lemma MVOKBAnotRF: "MVOKBA x ==> x \<noteq> RPCFailure"
    9.94    apply (unfold MVOKBA_def)
    9.95    apply auto
    9.96    done
    9.97  
    9.98  (* NotAResult notin MemVals U {OK,BadArg,RPCFailure} *)
    9.99  
   9.100 -lemma MVOKBARFnotNR: "MVOKBARF x ==> x ~= NotAResult"
   9.101 +lemma MVOKBARFnotNR: "MVOKBARF x ==> x \<noteq> NotAResult"
   9.102    apply (unfold MVOKBARF_def)
   9.103    apply auto
   9.104    done
   9.105 @@ -294,32 +294,32 @@
   9.106  *)
   9.107  
   9.108  (* --- not used ---
   9.109 -lemma S1_excl: "|- S1 rmhist p --> S1 rmhist p & ~S2 rmhist p & ~S3 rmhist p &
   9.110 -    ~S4 rmhist p & ~S5 rmhist p & ~S6 rmhist p"
   9.111 +lemma S1_excl: "|- S1 rmhist p --> S1 rmhist p & \<not>S2 rmhist p & \<not>S3 rmhist p &
   9.112 +    \<not>S4 rmhist p & \<not>S5 rmhist p & \<not>S6 rmhist p"
   9.113    by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def S6_def)
   9.114  *)
   9.115  
   9.116 -lemma S2_excl: "|- S2 rmhist p --> S2 rmhist p & ~S1 rmhist p"
   9.117 +lemma S2_excl: "|- S2 rmhist p --> S2 rmhist p & \<not>S1 rmhist p"
   9.118    by (auto simp: S_def S1_def S2_def)
   9.119  
   9.120 -lemma S3_excl: "|- S3 rmhist p --> S3 rmhist p & ~S1 rmhist p & ~S2 rmhist p"
   9.121 +lemma S3_excl: "|- S3 rmhist p --> S3 rmhist p & \<not>S1 rmhist p & \<not>S2 rmhist p"
   9.122    by (auto simp: S_def S1_def S2_def S3_def)
   9.123  
   9.124 -lemma S4_excl: "|- S4 rmhist p --> S4 rmhist p & ~S1 rmhist p & ~S2 rmhist p & ~S3 rmhist p"
   9.125 +lemma S4_excl: "|- S4 rmhist p --> S4 rmhist p & \<not>S1 rmhist p & \<not>S2 rmhist p & \<not>S3 rmhist p"
   9.126    by (auto simp: S_def S1_def S2_def S3_def S4_def)
   9.127  
   9.128 -lemma S5_excl: "|- S5 rmhist p --> S5 rmhist p & ~S1 rmhist p & ~S2 rmhist p
   9.129 -                         & ~S3 rmhist p & ~S4 rmhist p"
   9.130 +lemma S5_excl: "|- S5 rmhist p --> S5 rmhist p & \<not>S1 rmhist p & \<not>S2 rmhist p
   9.131 +                         & \<not>S3 rmhist p & \<not>S4 rmhist p"
   9.132    by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def)
   9.133  
   9.134 -lemma S6_excl: "|- S6 rmhist p --> S6 rmhist p & ~S1 rmhist p & ~S2 rmhist p
   9.135 -                         & ~S3 rmhist p & ~S4 rmhist p & ~S5 rmhist p"
   9.136 +lemma S6_excl: "|- S6 rmhist p --> S6 rmhist p & \<not>S1 rmhist p & \<not>S2 rmhist p
   9.137 +                         & \<not>S3 rmhist p & \<not>S4 rmhist p & \<not>S5 rmhist p"
   9.138    by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def S6_def)
   9.139  
   9.140  
   9.141  (* ==================== Lemmas about the environment ============================== *)
   9.142  
   9.143 -lemma Envbusy: "|- $(Calling memCh p) --> ~ENext p"
   9.144 +lemma Envbusy: "|- $(Calling memCh p) --> \<not>ENext p"
   9.145    by (auto simp: ENext_def Call_def)
   9.146  
   9.147  (* ==================== Lemmas about the implementation's states ==================== *)
   9.148 @@ -447,7 +447,7 @@
   9.149      @{thm Calling_def}, @{thm MemInv_def}]) [] [] 1 *})
   9.150  
   9.151  lemma S4Read: "|- Read rmCh mm ires p & $(S4 rmhist p) & unchanged (e p, c p, r p)
   9.152 -         & HNext rmhist p & (!l. $MemInv mm l)
   9.153 +         & HNext rmhist p & (\<forall>l. $MemInv mm l)
   9.154           --> (S4 rmhist p)$ & unchanged (rmhist!p)"
   9.155    by (auto simp: Read_def dest!: S4ReadInner [temp_use])
   9.156  
   9.157 @@ -563,7 +563,7 @@
   9.158  (* Figure 16 is a predicate-action diagram for the implementation. *)
   9.159  
   9.160  lemma Step1_2_1: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
   9.161 -         & ~unchanged (e p, c p, r p, m p, rmhist!p)  & $S1 rmhist p
   9.162 +         & \<not>unchanged (e p, c p, r p, m p, rmhist!p)  & $S1 rmhist p
   9.163           --> (S2 rmhist p)$ & ENext p & unchanged (c p, r p, m p)"
   9.164    apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
   9.165        (map (temp_elim @{context})
   9.166 @@ -573,7 +573,7 @@
   9.167    done
   9.168  
   9.169  lemma Step1_2_2: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
   9.170 -         & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S2 rmhist p
   9.171 +         & \<not>unchanged (e p, c p, r p, m p, rmhist!p) & $S2 rmhist p
   9.172           --> (S3 rmhist p)$ & MClkFwd memCh crCh cst p
   9.173               & unchanged (e p, r p, m p, rmhist!p)"
   9.174    apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
   9.175 @@ -584,7 +584,7 @@
   9.176    done
   9.177  
   9.178  lemma Step1_2_3: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
   9.179 -         & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S3 rmhist p
   9.180 +         & \<not>unchanged (e p, c p, r p, m p, rmhist!p) & $S3 rmhist p
   9.181           --> ((S4 rmhist p)$ & RPCFwd crCh rmCh rst p & unchanged (e p, c p, m p, rmhist!p))
   9.182               | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
   9.183    apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
   9.184 @@ -596,10 +596,10 @@
   9.185    done
   9.186  
   9.187  lemma Step1_2_4: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
   9.188 -              & ~unchanged (e p, c p, r p, m p, rmhist!p)
   9.189 -              & $S4 rmhist p & (!l. $(MemInv mm l))
   9.190 +              & \<not>unchanged (e p, c p, r p, m p, rmhist!p)
   9.191 +              & $S4 rmhist p & (\<forall>l. $(MemInv mm l))
   9.192           --> ((S4 rmhist p)$ & Read rmCh mm ires p & unchanged (e p, c p, r p, rmhist!p))
   9.193 -             | ((S4 rmhist p)$ & (? l. Write rmCh mm ires p l) & unchanged (e p, c p, r p, rmhist!p))
   9.194 +             | ((S4 rmhist p)$ & (\<exists>l. Write rmCh mm ires p l) & unchanged (e p, c p, r p, rmhist!p))
   9.195               | ((S5 rmhist p)$ & MemReturn rmCh ires p & unchanged (e p, c p, r p))"
   9.196    apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
   9.197      (map (temp_elim @{context}) [@{thm S4EnvUnch}, @{thm S4ClerkUnch}, @{thm S4RPCUnch}]) 1 *})
   9.198 @@ -610,7 +610,7 @@
   9.199    done
   9.200  
   9.201  lemma Step1_2_5: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
   9.202 -              & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S5 rmhist p
   9.203 +              & \<not>unchanged (e p, c p, r p, m p, rmhist!p) & $S5 rmhist p
   9.204           --> ((S6 rmhist p)$ & RPCReply crCh rmCh rst p & unchanged (e p, c p, m p))
   9.205               | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
   9.206    apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
   9.207 @@ -621,7 +621,7 @@
   9.208    done
   9.209  
   9.210  lemma Step1_2_6: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
   9.211 -              & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S6 rmhist p
   9.212 +              & \<not>unchanged (e p, c p, r p, m p, rmhist!p) & $S6 rmhist p
   9.213           --> ((S1 rmhist p)$ & MClkReply memCh crCh cst p & unchanged (e p, r p, m p))
   9.214               | ((S3 rmhist p)$ & MClkRetry memCh crCh cst p & unchanged (e p,r p,m p,rmhist!p))"
   9.215    apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
   9.216 @@ -694,7 +694,7 @@
   9.217    done
   9.218  
   9.219  lemma Step1_4_4a: "|- Read rmCh mm ires p & $S4 rmhist p & (S4 rmhist p)$
   9.220 -         & unchanged (e p, c p, r p, rmhist!p) & (!l. $(MemInv mm l))
   9.221 +         & unchanged (e p, c p, r p, rmhist!p) & (\<forall>l. $(MemInv mm l))
   9.222           --> Read memCh mm (resbar rmhist) p"
   9.223    by (force simp: Read_def elim!: Step1_4_4a1 [temp_use])
   9.224  
   9.225 @@ -816,7 +816,7 @@
   9.226  
   9.227  (* Steps that leave all variables unchanged are safe, so I may assume
   9.228     that some variable changes in the proof that a step is safe. *)
   9.229 -lemma unchanged_safe: "|- (~unchanged (e p, c p, r p, m p, rmhist!p)
   9.230 +lemma unchanged_safe: "|- (\<not>unchanged (e p, c p, r p, m p, rmhist!p)
   9.231               --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p))
   9.232           --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   9.233    apply (split_idle simp: square_def)
   9.234 @@ -850,7 +850,7 @@
   9.235    done
   9.236  
   9.237  lemma S4safe: "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
   9.238 -         & (!l. $(MemInv mm l))
   9.239 +         & (\<forall>l. $(MemInv mm l))
   9.240           --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   9.241    apply clarsimp
   9.242    apply (rule unchanged_safeI)
   9.243 @@ -900,23 +900,23 @@
   9.244  *)
   9.245  
   9.246  lemma S1_RNextdisabled: "|- S1 rmhist p -->
   9.247 -         ~Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
   9.248 +         \<not>Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
   9.249    apply (tactic {* action_simp_tac (@{context} addsimps [@{thm angle_def},
   9.250      @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}, temp_elim @{context} @{thm Memoryidle}] 1 *})
   9.251    apply force
   9.252    done
   9.253  
   9.254  lemma S1_Returndisabled: "|- S1 rmhist p -->
   9.255 -         ~Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
   9.256 +         \<not>Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
   9.257    by (tactic {* action_simp_tac (@{context} addsimps [@{thm angle_def}, @{thm MemReturn_def},
   9.258      @{thm Return_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1 *})
   9.259  
   9.260 -lemma RNext_fair: "|- []<>S1 rmhist p
   9.261 +lemma RNext_fair: "|- \<box>\<diamond>S1 rmhist p
   9.262           --> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
   9.263    by (auto simp: WF_alt [try_rewrite] intro!: S1_RNextdisabled [temp_use]
   9.264      elim!: STL4E [temp_use] DmdImplE [temp_use])
   9.265  
   9.266 -lemma Return_fair: "|- []<>S1 rmhist p
   9.267 +lemma Return_fair: "|- \<box>\<diamond>S1 rmhist p
   9.268           --> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
   9.269    by (auto simp: WF_alt [try_rewrite]
   9.270      intro!: S1_Returndisabled [temp_use] elim!: STL4E [temp_use] DmdImplE [temp_use])
   9.271 @@ -942,9 +942,9 @@
   9.272      apply (simp_all add: S_def S2_def)
   9.273    done
   9.274  
   9.275 -lemma S2_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
   9.276 +lemma S2_live: "|- \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
   9.277           & WF(MClkFwd memCh crCh cst p)_(c p)
   9.278 -         --> (S2 rmhist p ~> S3 rmhist p)"
   9.279 +         --> (S2 rmhist p \<leadsto> S3 rmhist p)"
   9.280    by (rule WF1 S2_successors S2MClkFwd_successors S2MClkFwd_enabled)+
   9.281  
   9.282  (* ------------------------------ State S3 ------------------------------ *)
   9.283 @@ -969,15 +969,15 @@
   9.284     apply (simp_all add: S_def S3_def)
   9.285    done
   9.286  
   9.287 -lemma S3_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
   9.288 +lemma S3_live: "|- \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
   9.289           & WF(RPCNext crCh rmCh rst p)_(r p)
   9.290 -         --> (S3 rmhist p ~> S4 rmhist p | S6 rmhist p)"
   9.291 +         --> (S3 rmhist p \<leadsto> S4 rmhist p | S6 rmhist p)"
   9.292    by (rule WF1 S3_successors S3RPC_successors S3RPC_enabled)+
   9.293  
   9.294  (* ------------- State S4 -------------------------------------------------- *)
   9.295  
   9.296  lemma S4_successors: "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
   9.297 -        & (ALL l. $MemInv mm l)
   9.298 +        & (\<forall>l. $MemInv mm l)
   9.299          --> (S4 rmhist p)$ | (S5 rmhist p)$"
   9.300    apply split_idle
   9.301    apply (auto dest!: Step1_2_4 [temp_use])
   9.302 @@ -986,22 +986,22 @@
   9.303  (* --------- State S4a: S4 /\ (ires p = NotAResult) ------------------------ *)
   9.304  
   9.305  lemma S4a_successors: "|- $(S4 rmhist p & ires!p = #NotAResult)
   9.306 -         & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l)
   9.307 +         & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (\<forall>l. $MemInv mm l)
   9.308           --> (S4 rmhist p & ires!p = #NotAResult)$
   9.309 -             | ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$"
   9.310 +             | ((S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p)$"
   9.311    apply split_idle
   9.312    apply (auto dest!: Step1_2_4 [temp_use])
   9.313    done
   9.314  
   9.315  lemma S4aRNext_successors: "|- ($(S4 rmhist p & ires!p = #NotAResult)
   9.316 -         & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l))
   9.317 +         & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (\<forall>l. $MemInv mm l))
   9.318           & <RNext rmCh mm ires p>_(m p)
   9.319 -         --> ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$"
   9.320 +         --> ((S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p)$"
   9.321    by (auto simp: angle_def
   9.322      dest!: Step1_2_4 [temp_use] ReadResult [temp_use] WriteResult [temp_use])
   9.323  
   9.324  lemma S4aRNext_enabled: "|- $(S4 rmhist p & ires!p = #NotAResult)
   9.325 -         & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l)
   9.326 +         & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (\<forall>l. $MemInv mm l)
   9.327           --> $Enabled (<RNext rmCh mm ires p>_(m p))"
   9.328    apply (auto simp: m_def intro!: RNext_enabled [temp_use])
   9.329     apply (cut_tac MI_base)
   9.330 @@ -1009,30 +1009,30 @@
   9.331    apply (simp add: S_def S4_def)
   9.332    done
   9.333  
   9.334 -lemma S4a_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
   9.335 -         & (ALL l. $MemInv mm l)) & WF(RNext rmCh mm ires p)_(m p)
   9.336 +lemma S4a_live: "|- \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
   9.337 +         & (\<forall>l. $MemInv mm l)) & WF(RNext rmCh mm ires p)_(m p)
   9.338           --> (S4 rmhist p & ires!p = #NotAResult
   9.339 -              ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)"
   9.340 +              \<leadsto> (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p)"
   9.341    by (rule WF1 S4a_successors S4aRNext_successors S4aRNext_enabled)+
   9.342  
   9.343  (* ---------- State S4b: S4 /\ (ires p # NotAResult) --------------------------- *)
   9.344  
   9.345 -lemma S4b_successors: "|- $(S4 rmhist p & ires!p ~= #NotAResult)
   9.346 -         & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l)
   9.347 -         --> (S4 rmhist p & ires!p ~= #NotAResult)$ | (S5 rmhist p)$"
   9.348 +lemma S4b_successors: "|- $(S4 rmhist p & ires!p \<noteq> #NotAResult)
   9.349 +         & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (\<forall>l. $MemInv mm l)
   9.350 +         --> (S4 rmhist p & ires!p \<noteq> #NotAResult)$ | (S5 rmhist p)$"
   9.351    apply (split_idle simp: m_def)
   9.352    apply (auto dest!: WriteResult [temp_use] Step1_2_4 [temp_use] ReadResult [temp_use])
   9.353    done
   9.354  
   9.355 -lemma S4bReturn_successors: "|- ($(S4 rmhist p & ires!p ~= #NotAResult)
   9.356 +lemma S4bReturn_successors: "|- ($(S4 rmhist p & ires!p \<noteq> #NotAResult)
   9.357           & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
   9.358 -         & (ALL l. $MemInv mm l)) & <MemReturn rmCh ires p>_(m p)
   9.359 +         & (\<forall>l. $MemInv mm l)) & <MemReturn rmCh ires p>_(m p)
   9.360           --> (S5 rmhist p)$"
   9.361    by (force simp: angle_def dest!: Step1_2_4 [temp_use] dest: ReturnNotReadWrite [temp_use])
   9.362  
   9.363 -lemma S4bReturn_enabled: "|- $(S4 rmhist p & ires!p ~= #NotAResult)
   9.364 +lemma S4bReturn_enabled: "|- $(S4 rmhist p & ires!p \<noteq> #NotAResult)
   9.365           & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
   9.366 -         & (ALL l. $MemInv mm l)
   9.367 +         & (\<forall>l. $MemInv mm l)
   9.368           --> $Enabled (<MemReturn rmCh ires p>_(m p))"
   9.369    apply (auto simp: m_def intro!: MemReturn_enabled [temp_use])
   9.370     apply (cut_tac MI_base)
   9.371 @@ -1040,9 +1040,9 @@
   9.372    apply (simp add: S_def S4_def)
   9.373    done
   9.374  
   9.375 -lemma S4b_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (!l. $MemInv mm l))
   9.376 +lemma S4b_live: "|- \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (\<forall>l. $MemInv mm l))
   9.377           & WF(MemReturn rmCh ires p)_(m p)
   9.378 -         --> (S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p)"
   9.379 +         --> (S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p)"
   9.380    by (rule WF1 S4b_successors S4bReturn_successors S4bReturn_enabled)+
   9.381  
   9.382  (* ------------------------------ State S5 ------------------------------ *)
   9.383 @@ -1066,9 +1066,9 @@
   9.384     apply (simp_all add: S_def S5_def)
   9.385    done
   9.386  
   9.387 -lemma S5_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
   9.388 +lemma S5_live: "|- \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
   9.389           & WF(RPCNext crCh rmCh rst p)_(r p)
   9.390 -         --> (S5 rmhist p ~> S6 rmhist p)"
   9.391 +         --> (S5 rmhist p \<leadsto> S6 rmhist p)"
   9.392    by (rule WF1 S5_successors S5RPC_successors S5RPC_enabled)+
   9.393  
   9.394  (* ------------------------------ State S6 ------------------------------ *)
   9.395 @@ -1099,11 +1099,11 @@
   9.396        addsimps [@{thm S_def}, @{thm S6_def}]) [] []) *})
   9.397    done
   9.398  
   9.399 -lemma S6_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & $(ImpInv rmhist p))
   9.400 -         & SF(MClkReply memCh crCh cst p)_(c p) & []<>(S6 rmhist p)
   9.401 -         --> []<>(S1 rmhist p)"
   9.402 +lemma S6_live: "|- \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & $(ImpInv rmhist p))
   9.403 +         & SF(MClkReply memCh crCh cst p)_(c p) & \<box>\<diamond>(S6 rmhist p)
   9.404 +         --> \<box>\<diamond>(S1 rmhist p)"
   9.405    apply clarsimp
   9.406 -  apply (subgoal_tac "sigma |= []<> (<MClkReply memCh crCh cst p>_ (c p))")
   9.407 +  apply (subgoal_tac "sigma |= \<box>\<diamond> (<MClkReply memCh crCh cst p>_ (c p))")
   9.408     apply (erule InfiniteEnsures)
   9.409      apply assumption
   9.410     apply (tactic {* action_simp_tac @{context} []
   9.411 @@ -1115,26 +1115,26 @@
   9.412  
   9.413  (* --------------- aggregate leadsto properties----------------------------- *)
   9.414  
   9.415 -lemma S5S6LeadstoS6: "sigma |= S5 rmhist p ~> S6 rmhist p
   9.416 -      ==> sigma |= (S5 rmhist p | S6 rmhist p) ~> S6 rmhist p"
   9.417 +lemma S5S6LeadstoS6: "sigma |= S5 rmhist p \<leadsto> S6 rmhist p
   9.418 +      ==> sigma |= (S5 rmhist p | S6 rmhist p) \<leadsto> S6 rmhist p"
   9.419    by (auto intro!: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use])
   9.420  
   9.421 -lemma S4bS5S6LeadstoS6: "[| sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
   9.422 -         sigma |= S5 rmhist p ~> S6 rmhist p |]
   9.423 -      ==> sigma |= (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p | S6 rmhist p
   9.424 -                    ~> S6 rmhist p"
   9.425 +lemma S4bS5S6LeadstoS6: "[| sigma |= S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
   9.426 +         sigma |= S5 rmhist p \<leadsto> S6 rmhist p |]
   9.427 +      ==> sigma |= (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p | S6 rmhist p
   9.428 +                    \<leadsto> S6 rmhist p"
   9.429    by (auto intro!: LatticeDisjunctionIntro [temp_use]
   9.430      S5S6LeadstoS6 [temp_use] intro: LatticeTransitivity [temp_use])
   9.431  
   9.432  lemma S4S5S6LeadstoS6: "[| sigma |= S4 rmhist p & ires!p = #NotAResult
   9.433 -                  ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p;
   9.434 -         sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
   9.435 -         sigma |= S5 rmhist p ~> S6 rmhist p |]
   9.436 -      ==> sigma |= S4 rmhist p | S5 rmhist p | S6 rmhist p ~> S6 rmhist p"
   9.437 +                  \<leadsto> (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p;
   9.438 +         sigma |= S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
   9.439 +         sigma |= S5 rmhist p \<leadsto> S6 rmhist p |]
   9.440 +      ==> sigma |= S4 rmhist p | S5 rmhist p | S6 rmhist p \<leadsto> S6 rmhist p"
   9.441    apply (subgoal_tac "sigma |= (S4 rmhist p & ires!p = #NotAResult) |
   9.442 -    (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p | S6 rmhist p ~> S6 rmhist p")
   9.443 +    (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p | S6 rmhist p \<leadsto> S6 rmhist p")
   9.444     apply (erule_tac G = "PRED ((S4 rmhist p & ires!p = #NotAResult) |
   9.445 -     (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p | S6 rmhist p)" in
   9.446 +     (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p | S6 rmhist p)" in
   9.447       LatticeTransitivity [temp_use])
   9.448     apply (force simp: Init_defs intro!: ImplLeadsto_gen [temp_use] necT [temp_use])
   9.449    apply (rule LatticeDisjunctionIntro [temp_use])
   9.450 @@ -1144,12 +1144,12 @@
   9.451    apply (auto intro!: S4bS5S6LeadstoS6 [temp_use])
   9.452    done
   9.453  
   9.454 -lemma S3S4S5S6LeadstoS6: "[| sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p;
   9.455 +lemma S3S4S5S6LeadstoS6: "[| sigma |= S3 rmhist p \<leadsto> S4 rmhist p | S6 rmhist p;
   9.456           sigma |= S4 rmhist p & ires!p = #NotAResult
   9.457 -                  ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p;
   9.458 -         sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
   9.459 -         sigma |= S5 rmhist p ~> S6 rmhist p |]
   9.460 -      ==> sigma |= S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p ~> S6 rmhist p"
   9.461 +                  \<leadsto> (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p;
   9.462 +         sigma |= S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
   9.463 +         sigma |= S5 rmhist p \<leadsto> S6 rmhist p |]
   9.464 +      ==> sigma |= S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p \<leadsto> S6 rmhist p"
   9.465    apply (rule LatticeDisjunctionIntro [temp_use])
   9.466     apply (erule LatticeTriangle2 [temp_use])
   9.467     apply (rule S4S5S6LeadstoS6 [THEN LatticeTransitivity [temp_use]])
   9.468 @@ -1157,14 +1157,14 @@
   9.469          intro: ImplLeadsto_gen [temp_use] simp: Init_defs)
   9.470    done
   9.471  
   9.472 -lemma S2S3S4S5S6LeadstoS6: "[| sigma |= S2 rmhist p ~> S3 rmhist p;
   9.473 -         sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p;
   9.474 +lemma S2S3S4S5S6LeadstoS6: "[| sigma |= S2 rmhist p \<leadsto> S3 rmhist p;
   9.475 +         sigma |= S3 rmhist p \<leadsto> S4 rmhist p | S6 rmhist p;
   9.476           sigma |= S4 rmhist p & ires!p = #NotAResult
   9.477 -                  ~> S4 rmhist p & ires!p ~= #NotAResult | S5 rmhist p;
   9.478 -         sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
   9.479 -         sigma |= S5 rmhist p ~> S6 rmhist p |]
   9.480 +                  \<leadsto> S4 rmhist p & ires!p \<noteq> #NotAResult | S5 rmhist p;
   9.481 +         sigma |= S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
   9.482 +         sigma |= S5 rmhist p \<leadsto> S6 rmhist p |]
   9.483        ==> sigma |= S2 rmhist p | S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p
   9.484 -                   ~> S6 rmhist p"
   9.485 +                   \<leadsto> S6 rmhist p"
   9.486    apply (rule LatticeDisjunctionIntro [temp_use])
   9.487     apply (rule LatticeTransitivity [temp_use])
   9.488      prefer 2 apply assumption
   9.489 @@ -1173,14 +1173,14 @@
   9.490           intro: ImplLeadsto_gen [temp_use] simp: Init_defs)
   9.491    done
   9.492  
   9.493 -lemma NotS1LeadstoS6: "[| sigma |= []ImpInv rmhist p;
   9.494 -         sigma |= S2 rmhist p ~> S3 rmhist p;
   9.495 -         sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p;
   9.496 +lemma NotS1LeadstoS6: "[| sigma |= \<box>ImpInv rmhist p;
   9.497 +         sigma |= S2 rmhist p \<leadsto> S3 rmhist p;
   9.498 +         sigma |= S3 rmhist p \<leadsto> S4 rmhist p | S6 rmhist p;
   9.499           sigma |= S4 rmhist p & ires!p = #NotAResult
   9.500 -                  ~> S4 rmhist p & ires!p ~= #NotAResult | S5 rmhist p;
   9.501 -         sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
   9.502 -         sigma |= S5 rmhist p ~> S6 rmhist p |]
   9.503 -      ==> sigma |= ~S1 rmhist p ~> S6 rmhist p"
   9.504 +                  \<leadsto> S4 rmhist p & ires!p \<noteq> #NotAResult | S5 rmhist p;
   9.505 +         sigma |= S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
   9.506 +         sigma |= S5 rmhist p \<leadsto> S6 rmhist p |]
   9.507 +      ==> sigma |= \<not>S1 rmhist p \<leadsto> S6 rmhist p"
   9.508    apply (rule S2S3S4S5S6LeadstoS6 [THEN LatticeTransitivity [temp_use]])
   9.509         apply assumption+
   9.510    apply (erule INV_leadsto [temp_use])
   9.511 @@ -1189,9 +1189,9 @@
   9.512    apply (auto simp: ImpInv_def Init_defs intro!: necT [temp_use])
   9.513    done
   9.514  
   9.515 -lemma S1Infinite: "[| sigma |= ~S1 rmhist p ~> S6 rmhist p;
   9.516 -         sigma |= []<>S6 rmhist p --> []<>S1 rmhist p |]
   9.517 -      ==> sigma |= []<>S1 rmhist p"
   9.518 +lemma S1Infinite: "[| sigma |= \<not>S1 rmhist p \<leadsto> S6 rmhist p;
   9.519 +         sigma |= \<box>\<diamond>S6 rmhist p --> \<box>\<diamond>S1 rmhist p |]
   9.520 +      ==> sigma |= \<box>\<diamond>S1 rmhist p"
   9.521    apply (rule classical)
   9.522    apply (tactic {* asm_lr_simp_tac (@{context} addsimps
   9.523      [temp_use @{context} @{thm NotBox}, temp_rewrite @{context} @{thm NotDmd}]) 1 *})
   9.524 @@ -1204,12 +1204,12 @@
   9.525     a. memory invariant
   9.526     b. "implementation invariant": always in states S1,...,S6
   9.527  *)
   9.528 -lemma Step1_5_1a: "|- IPImp p --> (ALL l. []$MemInv mm l)"
   9.529 +lemma Step1_5_1a: "|- IPImp p --> (\<forall>l. \<box>$MemInv mm l)"
   9.530    by (auto simp: IPImp_def box_stp_act [temp_use] intro!: MemoryInvariantAll [temp_use])
   9.531  
   9.532 -lemma Step1_5_1b: "|- Init(ImpInit p & HInit rmhist p) & [](ImpNext p)
   9.533 -         & [][HNext rmhist p]_(c p, r p, m p, rmhist!p) & [](ALL l. $MemInv mm l)
   9.534 -         --> []ImpInv rmhist p"
   9.535 +lemma Step1_5_1b: "|- Init(ImpInit p & HInit rmhist p) & \<box>(ImpNext p)
   9.536 +         & \<box>[HNext rmhist p]_(c p, r p, m p, rmhist!p) & \<box>(\<forall>l. $MemInv mm l)
   9.537 +         --> \<box>ImpInv rmhist p"
   9.538    apply invariant
   9.539     apply (auto simp: Init_def ImpInv_def box_stp_act [temp_use]
   9.540       dest!: Step1_1 [temp_use] dest: S1_successors [temp_use] S2_successors [temp_use]
   9.541 @@ -1222,9 +1222,9 @@
   9.542    by (auto simp: Init_def intro!: Step1_1 [temp_use] Step1_3  [temp_use])
   9.543  
   9.544  (*** step simulation ***)
   9.545 -lemma Step1_5_2b: "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)
   9.546 -         & $ImpInv rmhist p & (!l. $MemInv mm l))
   9.547 -         --> [][UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   9.548 +lemma Step1_5_2b: "|- \<box>(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)
   9.549 +         & $ImpInv rmhist p & (\<forall>l. $MemInv mm l))
   9.550 +         --> \<box>[UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   9.551    by (auto simp: ImpInv_def elim!: STL4E [temp_use]
   9.552      dest!: S1safe [temp_use] S2safe [temp_use] S3safe [temp_use] S4safe [temp_use]
   9.553      S5safe [temp_use] S6safe [temp_use])
   9.554 @@ -1232,12 +1232,12 @@
   9.555  (*** Liveness ***)
   9.556  lemma GoodImpl: "|- IPImp p & HistP rmhist p
   9.557           -->   Init(ImpInit p & HInit rmhist p)
   9.558 -             & [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
   9.559 -             & [](ALL l. $MemInv mm l) & []($ImpInv rmhist p)
   9.560 +             & \<box>(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
   9.561 +             & \<box>(\<forall>l. $MemInv mm l) & \<box>($ImpInv rmhist p)
   9.562               & ImpLive p"
   9.563    apply clarsimp
   9.564 -    apply (subgoal_tac "sigma |= Init (ImpInit p & HInit rmhist p) & [] (ImpNext p) &
   9.565 -      [][HNext rmhist p]_ (c p, r p, m p, rmhist!p) & [] (ALL l. $MemInv mm l)")
   9.566 +    apply (subgoal_tac "sigma |= Init (ImpInit p & HInit rmhist p) & \<box> (ImpNext p) &
   9.567 +      \<box>[HNext rmhist p]_ (c p, r p, m p, rmhist!p) & \<box> (\<forall>l. $MemInv mm l)")
   9.568     apply (auto simp: split_box_conj [try_rewrite] box_stp_act [try_rewrite]
   9.569         dest!: Step1_5_1b [temp_use])
   9.570        apply (force simp: IPImp_def MClkIPSpec_def RPCIPSpec_def RPSpec_def
   9.571 @@ -1251,10 +1251,10 @@
   9.572    done
   9.573  
   9.574  (* The implementation is infinitely often in state S1... *)
   9.575 -lemma Step1_5_3a: "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
   9.576 -         & [](ALL l. $MemInv mm l)
   9.577 -         & []($ImpInv rmhist p) & ImpLive p
   9.578 -         --> []<>S1 rmhist p"
   9.579 +lemma Step1_5_3a: "|- \<box>(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
   9.580 +         & \<box>(\<forall>l. $MemInv mm l)
   9.581 +         & \<box>($ImpInv rmhist p) & ImpLive p
   9.582 +         --> \<box>\<diamond>S1 rmhist p"
   9.583    apply (clarsimp simp: ImpLive_def)
   9.584    apply (rule S1Infinite)
   9.585     apply (force simp: split_box_conj [try_rewrite] box_stp_act [try_rewrite]
   9.586 @@ -1264,13 +1264,13 @@
   9.587    done
   9.588  
   9.589  (* ... and therefore satisfies the fairness requirements of the specification *)
   9.590 -lemma Step1_5_3b: "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
   9.591 -         & [](ALL l. $MemInv mm l) & []($ImpInv rmhist p) & ImpLive p
   9.592 +lemma Step1_5_3b: "|- \<box>(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
   9.593 +         & \<box>(\<forall>l. $MemInv mm l) & \<box>($ImpInv rmhist p) & ImpLive p
   9.594           --> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
   9.595    by (auto intro!: RNext_fair [temp_use] Step1_5_3a [temp_use])
   9.596  
   9.597 -lemma Step1_5_3c: "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
   9.598 -         & [](ALL l. $MemInv mm l) & []($ImpInv rmhist p) & ImpLive p
   9.599 +lemma Step1_5_3c: "|- \<box>(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
   9.600 +         & \<box>(\<forall>l. $MemInv mm l) & \<box>($ImpInv rmhist p) & ImpLive p
   9.601           --> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
   9.602    by (auto intro!: Return_fair [temp_use] Step1_5_3a [temp_use])
   9.603  
   9.604 @@ -1296,25 +1296,25 @@
   9.605       apply (auto simp: square_def dest: S4Write [temp_use])
   9.606    done
   9.607  
   9.608 -lemma Step2_2: "|-   (ALL p. ImpNext p)
   9.609 -         & (ALL p. [HNext rmhist p]_(c p, r p, m p, rmhist!p))
   9.610 -         & (ALL p. $ImpInv rmhist p)
   9.611 -         & [EX q. Write rmCh mm ires q l]_(mm!l)
   9.612 -         --> [EX q. Write memCh mm (resbar rmhist) q l]_(mm!l)"
   9.613 +lemma Step2_2: "|-   (\<forall>p. ImpNext p)
   9.614 +         & (\<forall>p. [HNext rmhist p]_(c p, r p, m p, rmhist!p))
   9.615 +         & (\<forall>p. $ImpInv rmhist p)
   9.616 +         & [\<exists>q. Write rmCh mm ires q l]_(mm!l)
   9.617 +         --> [\<exists>q. Write memCh mm (resbar rmhist) q l]_(mm!l)"
   9.618    apply (auto intro!: squareCI elim!: squareE)
   9.619    apply (assumption | rule exI Step1_4_4b [action_use])+
   9.620      apply (force intro!: WriteS4 [temp_use])
   9.621     apply (auto dest!: Step2_2a [temp_use])
   9.622    done
   9.623  
   9.624 -lemma Step2_lemma: "|- [](  (ALL p. ImpNext p)
   9.625 -            & (ALL p. [HNext rmhist p]_(c p, r p, m p, rmhist!p))
   9.626 -            & (ALL p. $ImpInv rmhist p)
   9.627 -            & [EX q. Write rmCh mm ires q l]_(mm!l))
   9.628 -         --> [][EX q. Write memCh mm (resbar rmhist) q l]_(mm!l)"
   9.629 +lemma Step2_lemma: "|- \<box>(  (\<forall>p. ImpNext p)
   9.630 +            & (\<forall>p. [HNext rmhist p]_(c p, r p, m p, rmhist!p))
   9.631 +            & (\<forall>p. $ImpInv rmhist p)
   9.632 +            & [\<exists>q. Write rmCh mm ires q l]_(mm!l))
   9.633 +         --> \<box>[\<exists>q. Write memCh mm (resbar rmhist) q l]_(mm!l)"
   9.634    by (force elim!: STL4E [temp_use] dest!: Step2_2 [temp_use])
   9.635  
   9.636 -lemma Step2: "|- #l : #MemLoc & (ALL p. IPImp p & HistP rmhist p)
   9.637 +lemma Step2: "|- #l : #MemLoc & (\<forall>p. IPImp p & HistP rmhist p)
   9.638           --> MSpec memCh mm (resbar rmhist) l"
   9.639    apply (auto simp: MSpec_def)
   9.640     apply (force simp: IPImp_def MSpec_def)
    10.1 --- a/src/HOL/TLA/Memory/MemoryParameters.thy	Fri Jun 26 11:07:04 2015 +0200
    10.2 +++ b/src/HOL/TLA/Memory/MemoryParameters.thy	Fri Jun 26 11:44:22 2015 +0200
    10.3 @@ -27,20 +27,20 @@
    10.4  
    10.5  axiomatization where
    10.6    (* basic assumptions about the above constants and predicates *)
    10.7 -  BadArgNoMemVal:    "BadArg ~: MemVal" and
    10.8 -  MemFailNoMemVal:   "MemFailure ~: MemVal" and
    10.9 +  BadArgNoMemVal:    "BadArg \<notin> MemVal" and
   10.10 +  MemFailNoMemVal:   "MemFailure \<notin> MemVal" and
   10.11    InitValMemVal:     "InitVal : MemVal" and
   10.12 -  NotAResultNotVal:  "NotAResult ~: MemVal" and
   10.13 -  NotAResultNotOK:   "NotAResult ~= OK" and
   10.14 -  NotAResultNotBA:   "NotAResult ~= BadArg" and
   10.15 -  NotAResultNotMF:   "NotAResult ~= MemFailure"
   10.16 +  NotAResultNotVal:  "NotAResult \<notin> MemVal" and
   10.17 +  NotAResultNotOK:   "NotAResult \<noteq> OK" and
   10.18 +  NotAResultNotBA:   "NotAResult \<noteq> BadArg" and
   10.19 +  NotAResultNotMF:   "NotAResult \<noteq> MemFailure"
   10.20  
   10.21  lemmas [simp] =
   10.22    BadArgNoMemVal MemFailNoMemVal InitValMemVal NotAResultNotVal
   10.23    NotAResultNotOK NotAResultNotBA NotAResultNotMF
   10.24    NotAResultNotOK [symmetric] NotAResultNotBA [symmetric] NotAResultNotMF [symmetric]
   10.25  
   10.26 -lemma MemValNotAResultE: "[| x : MemVal; (x ~= NotAResult ==> P) |] ==> P"
   10.27 +lemma MemValNotAResultE: "[| x : MemVal; (x \<noteq> NotAResult ==> P) |] ==> P"
   10.28    using NotAResultNotVal by blast
   10.29  
   10.30  end
    11.1 --- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Fri Jun 26 11:07:04 2015 +0200
    11.2 +++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Fri Jun 26 11:44:22 2015 +0200
    11.3 @@ -58,23 +58,23 @@
    11.4  defs
    11.5    slice_def:     "(PRED (x!i)) s == x s i"
    11.6  
    11.7 -  caller_def:    "caller ch   == %s p. (cbit (ch s p), arg (ch s p))"
    11.8 -  rtrner_def:    "rtrner ch   == %s p. (rbit (ch s p), res (ch s p))"
    11.9 +  caller_def:    "caller ch   == \<lambda>s p. (cbit (ch s p), arg (ch s p))"
   11.10 +  rtrner_def:    "rtrner ch   == \<lambda>s p. (rbit (ch s p), res (ch s p))"
   11.11  
   11.12 -  Calling_def:   "Calling ch p  == PRED cbit< ch!p > ~= rbit< ch!p >"
   11.13 -  Call_def:      "(ACT Call ch p v)   == ACT  ~ $Calling ch p
   11.14 -                                     & (cbit<ch!p>$ ~= $rbit<ch!p>)
   11.15 +  Calling_def:   "Calling ch p  == PRED cbit< ch!p > \<noteq> rbit< ch!p >"
   11.16 +  Call_def:      "(ACT Call ch p v)   == ACT  \<not> $Calling ch p
   11.17 +                                     & (cbit<ch!p>$ \<noteq> $rbit<ch!p>)
   11.18                                       & (arg<ch!p>$ = $v)"
   11.19    Return_def:    "(ACT Return ch p v) == ACT  $Calling ch p
   11.20                                       & (rbit<ch!p>$ = $cbit<ch!p>)
   11.21                                       & (res<ch!p>$ = $v)"
   11.22    PLegalCaller_def:      "PLegalCaller ch p == TEMP
   11.23 -                             Init(~ Calling ch p)
   11.24 -                             & [][ ? a. Call ch p a ]_((caller ch)!p)"
   11.25 -  LegalCaller_def:       "LegalCaller ch == TEMP (! p. PLegalCaller ch p)"
   11.26 +                             Init(\<not> Calling ch p)
   11.27 +                             & \<box>[\<exists>a. Call ch p a ]_((caller ch)!p)"
   11.28 +  LegalCaller_def:       "LegalCaller ch == TEMP (\<forall>p. PLegalCaller ch p)"
   11.29    PLegalReturner_def:    "PLegalReturner ch p == TEMP
   11.30 -                                [][ ? v. Return ch p v ]_((rtrner ch)!p)"
   11.31 -  LegalReturner_def:     "LegalReturner ch == TEMP (! p. PLegalReturner ch p)"
   11.32 +                                \<box>[\<exists>v. Return ch p v ]_((rtrner ch)!p)"
   11.33 +  LegalReturner_def:     "LegalReturner ch == TEMP (\<forall>p. PLegalReturner ch p)"
   11.34  
   11.35  declare slice_def [simp]
   11.36  
    12.1 --- a/src/HOL/TLA/Memory/RPC.thy	Fri Jun 26 11:07:04 2015 +0200
    12.2 +++ b/src/HOL/TLA/Memory/RPC.thy	Fri Jun 26 11:44:22 2015 +0200
    12.3 @@ -28,7 +28,7 @@
    12.4    RPCISpec   :: "rpcSndChType => rpcRcvChType => rpcStType => temporal"
    12.5  
    12.6  defs
    12.7 -  RPCInit_def:       "RPCInit rcv rst p == PRED ((rst!p = #rpcA) & ~Calling rcv p)"
    12.8 +  RPCInit_def:       "RPCInit rcv rst p == PRED ((rst!p = #rpcA) & \<not>Calling rcv p)"
    12.9  
   12.10    RPCFwd_def:        "RPCFwd send rcv rst p == ACT
   12.11                           $(Calling send p)
   12.12 @@ -40,18 +40,18 @@
   12.13  
   12.14    RPCReject_def:     "RPCReject send rcv rst p == ACT
   12.15                             $(rst!p) = # rpcA
   12.16 -                         & ~IsLegalRcvArg<arg<$(send!p)>>
   12.17 +                         & \<not>IsLegalRcvArg<arg<$(send!p)>>
   12.18                           & Return send p #BadCall
   12.19                           & unchanged ((rst!p), (caller rcv!p))"
   12.20  
   12.21    RPCFail_def:       "RPCFail send rcv rst p == ACT
   12.22 -                           ~$(Calling rcv p)
   12.23 +                           \<not>$(Calling rcv p)
   12.24                           & Return send p #RPCFailure
   12.25                           & (rst!p)$ = #rpcA
   12.26                           & unchanged (caller rcv!p)"
   12.27  
   12.28    RPCReply_def:      "RPCReply send rcv rst p == ACT
   12.29 -                           ~$(Calling rcv p)
   12.30 +                           \<not>$(Calling rcv p)
   12.31                           & $(rst!p) = #rpcB
   12.32                           & Return send p res<rcv!p>
   12.33                           & (rst!p)$ = #rpcA
   12.34 @@ -65,10 +65,10 @@
   12.35  
   12.36    RPCIPSpec_def:     "RPCIPSpec send rcv rst p == TEMP
   12.37                             Init RPCInit rcv rst p
   12.38 -                         & [][ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
   12.39 +                         & \<box>[ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
   12.40                           & WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)"
   12.41  
   12.42 -  RPCISpec_def:      "RPCISpec send rcv rst == TEMP (ALL p. RPCIPSpec send rcv rst p)"
   12.43 +  RPCISpec_def:      "RPCISpec send rcv rst == TEMP (\<forall>p. RPCIPSpec send rcv rst p)"
   12.44  
   12.45  
   12.46  lemmas RPC_action_defs =
   12.47 @@ -81,10 +81,10 @@
   12.48     unanswered call for that process.
   12.49  *)
   12.50  
   12.51 -lemma RPCidle: "|- ~$(Calling send p) --> ~RPCNext send rcv rst p"
   12.52 +lemma RPCidle: "|- \<not>$(Calling send p) --> \<not>RPCNext send rcv rst p"
   12.53    by (auto simp: Return_def RPC_action_defs)
   12.54  
   12.55 -lemma RPCbusy: "|- $(Calling rcv p) & $(rst!p) = #rpcB --> ~RPCNext send rcv rst p"
   12.56 +lemma RPCbusy: "|- $(Calling rcv p) & $(rst!p) = #rpcB --> \<not>RPCNext send rcv rst p"
   12.57    by (auto simp: RPC_action_defs)
   12.58  
   12.59  (* RPC failure actions are visible. *)
   12.60 @@ -97,14 +97,14 @@
   12.61    by (force elim!: enabled_mono [temp_use] RPCFail_vis [temp_use])
   12.62  
   12.63  (* Enabledness of some actions *)
   12.64 -lemma RPCFail_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==>  
   12.65 -    |- ~Calling rcv p & Calling send p --> Enabled (RPCFail send rcv rst p)"
   12.66 +lemma RPCFail_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) ==>  
   12.67 +    |- \<not>Calling rcv p & Calling send p --> Enabled (RPCFail send rcv rst p)"
   12.68    by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCFail_def},
   12.69      @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
   12.70      [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
   12.71  
   12.72 -lemma RPCReply_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==>  
   12.73 -      |- ~Calling rcv p & Calling send p & rst!p = #rpcB  
   12.74 +lemma RPCReply_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) ==>  
   12.75 +      |- \<not>Calling rcv p & Calling send p & rst!p = #rpcB  
   12.76           --> Enabled (RPCReply send rcv rst p)"
   12.77    by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCReply_def},
   12.78      @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
    13.1 --- a/src/HOL/TLA/Memory/RPCParameters.thy	Fri Jun 26 11:07:04 2015 +0200
    13.2 +++ b/src/HOL/TLA/Memory/RPCParameters.thy	Fri Jun 26 11:44:22 2015 +0200
    13.3 @@ -30,10 +30,10 @@
    13.4  
    13.5  axiomatization where
    13.6    (* RPCFailure is different from MemVals and exceptions *)
    13.7 -  RFNoMemVal:        "RPCFailure ~: MemVal" and
    13.8 -  NotAResultNotRF:   "NotAResult ~= RPCFailure" and
    13.9 -  OKNotRF:           "OK ~= RPCFailure" and
   13.10 -  BANotRF:           "BadArg ~= RPCFailure"
   13.11 +  RFNoMemVal:        "RPCFailure \<notin> MemVal" and
   13.12 +  NotAResultNotRF:   "NotAResult \<noteq> RPCFailure" and
   13.13 +  OKNotRF:           "OK \<noteq> RPCFailure" and
   13.14 +  BANotRF:           "BadArg \<noteq> RPCFailure"
   13.15  
   13.16  defs
   13.17    IsLegalRcvArg_def: "IsLegalRcvArg ra ==
    14.1 --- a/src/HOL/TLA/Stfun.thy	Fri Jun 26 11:07:04 2015 +0200
    14.2 +++ b/src/HOL/TLA/Stfun.thy	Fri Jun 26 11:44:22 2015 +0200
    14.3 @@ -50,13 +50,13 @@
    14.4    basevars_def:  "stvars vs == range vs = UNIV"
    14.5  
    14.6  
    14.7 -lemma basevars: "!!vs. basevars vs ==> EX u. vs u = c"
    14.8 +lemma basevars: "\<And>vs. basevars vs ==> \<exists>u. vs u = c"
    14.9    apply (unfold basevars_def)
   14.10    apply (rule_tac b = c and f = vs in rangeE)
   14.11     apply auto
   14.12    done
   14.13  
   14.14 -lemma base_pair1: "!!x y. basevars (x,y) ==> basevars x"
   14.15 +lemma base_pair1: "\<And>x y. basevars (x,y) ==> basevars x"
   14.16    apply (simp (no_asm) add: basevars_def)
   14.17    apply (rule equalityI)
   14.18     apply (rule subset_UNIV)
   14.19 @@ -65,7 +65,7 @@
   14.20    apply auto
   14.21    done
   14.22  
   14.23 -lemma base_pair2: "!!x y. basevars (x,y) ==> basevars y"
   14.24 +lemma base_pair2: "\<And>x y. basevars (x,y) ==> basevars y"
   14.25    apply (simp (no_asm) add: basevars_def)
   14.26    apply (rule equalityI)
   14.27     apply (rule subset_UNIV)
   14.28 @@ -74,7 +74,7 @@
   14.29    apply auto
   14.30    done
   14.31  
   14.32 -lemma base_pair: "!!x y. basevars (x,y) ==> basevars x & basevars y"
   14.33 +lemma base_pair: "\<And>x y. basevars (x,y) ==> basevars x & basevars y"
   14.34    apply (rule conjI)
   14.35    apply (erule base_pair1)
   14.36    apply (erule base_pair2)
   14.37 @@ -89,7 +89,7 @@
   14.38    apply auto
   14.39    done
   14.40  
   14.41 -lemma baseE: "[| basevars v; !!x. v x = c ==> Q |] ==> Q"
   14.42 +lemma baseE: "[| basevars v; \<And>x. v x = c ==> Q |] ==> Q"
   14.43    apply (erule basevars [THEN exE])
   14.44    apply blast
   14.45    done
   14.46 @@ -99,7 +99,7 @@
   14.47     The following shows that there should not be duplicates in a "stvars" tuple:
   14.48  *)
   14.49  
   14.50 -lemma "!!v. basevars (v::bool stfun, v) ==> False"
   14.51 +lemma "\<And>v. basevars (v::bool stfun, v) ==> False"
   14.52    apply (erule baseE)
   14.53    apply (subgoal_tac "(LIFT (v,v)) x = (True, False)")
   14.54     prefer 2
    15.1 --- a/src/HOL/TLA/TLA.thy	Fri Jun 26 11:07:04 2015 +0200
    15.2 +++ b/src/HOL/TLA/TLA.thy	Fri Jun 26 11:44:22 2015 +0200
    15.3 @@ -60,49 +60,45 @@
    15.4    "_EEx"     :: "[idts, lift] => lift"                ("(3\<exists>\<exists> _./ _)" [0,10] 10)
    15.5    "_AAll"    :: "[idts, lift] => lift"                ("(3\<forall>\<forall> _./ _)" [0,10] 10)
    15.6  
    15.7 -syntax (HTML output)
    15.8 -  "_EEx"     :: "[idts, lift] => lift"                ("(3\<exists>\<exists> _./ _)" [0,10] 10)
    15.9 -  "_AAll"    :: "[idts, lift] => lift"                ("(3\<forall>\<forall> _./ _)" [0,10] 10)
   15.10 -
   15.11  axiomatization where
   15.12    (* Definitions of derived operators *)
   15.13 -  dmd_def:      "\<And>F. TEMP <>F  ==  TEMP ~[]~F"
   15.14 +  dmd_def:      "\<And>F. TEMP \<diamond>F  ==  TEMP \<not>\<box>\<not>F"
   15.15  
   15.16  axiomatization where
   15.17 -  boxInit:      "\<And>F. TEMP []F  ==  TEMP []Init F" and
   15.18 -  leadsto_def:  "\<And>F G. TEMP F ~> G  ==  TEMP [](Init F --> <>G)" and
   15.19 -  stable_def:   "\<And>P. TEMP stable P  ==  TEMP []($P --> P$)" and
   15.20 -  WF_def:       "TEMP WF(A)_v  ==  TEMP <>[] Enabled(<A>_v) --> []<><A>_v" and
   15.21 -  SF_def:       "TEMP SF(A)_v  ==  TEMP []<> Enabled(<A>_v) --> []<><A>_v" and
   15.22 -  aall_def:     "TEMP (AALL x. F x)  ==  TEMP ~ (EEX x. ~ F x)"
   15.23 +  boxInit:      "\<And>F. TEMP \<box>F  ==  TEMP \<box>Init F" and
   15.24 +  leadsto_def:  "\<And>F G. TEMP F \<leadsto> G  ==  TEMP \<box>(Init F --> \<diamond>G)" and
   15.25 +  stable_def:   "\<And>P. TEMP stable P  ==  TEMP \<box>($P --> P$)" and
   15.26 +  WF_def:       "TEMP WF(A)_v  ==  TEMP \<diamond>\<box> Enabled(<A>_v) --> \<box>\<diamond><A>_v" and
   15.27 +  SF_def:       "TEMP SF(A)_v  ==  TEMP \<box>\<diamond> Enabled(<A>_v) --> \<box>\<diamond><A>_v" and
   15.28 +  aall_def:     "TEMP (\<forall>\<forall>x. F x)  ==  TEMP \<not> (\<exists>\<exists>x. \<not> F x)"
   15.29  
   15.30  axiomatization where
   15.31  (* Base axioms for raw TLA. *)
   15.32 -  normalT:    "\<And>F G. |- [](F --> G) --> ([]F --> []G)" and    (* polymorphic *)
   15.33 -  reflT:      "\<And>F. |- []F --> F" and         (* F::temporal *)
   15.34 -  transT:     "\<And>F. |- []F --> [][]F" and     (* polymorphic *)
   15.35 -  linT:       "\<And>F G. |- <>F & <>G --> (<>(F & <>G)) | (<>(G & <>F))" and
   15.36 -  discT:      "\<And>F. |- [](F --> <>(~F & <>F)) --> (F --> []<>F)" and
   15.37 -  primeI:     "\<And>P. |- []P --> Init P`" and
   15.38 -  primeE:     "\<And>P F. |- [](Init P --> []F) --> Init P` --> (F --> []F)" and
   15.39 -  indT:       "\<And>P F. |- [](Init P & ~[]F --> Init P` & F) --> Init P --> []F" and
   15.40 -  allT:       "\<And>F. |- (ALL x. [](F x)) = ([](ALL x. F x))"
   15.41 +  normalT:    "\<And>F G. |- \<box>(F --> G) --> (\<box>F --> \<box>G)" and    (* polymorphic *)
   15.42 +  reflT:      "\<And>F. |- \<box>F --> F" and         (* F::temporal *)
   15.43 +  transT:     "\<And>F. |- \<box>F --> \<box>\<box>F" and     (* polymorphic *)
   15.44 +  linT:       "\<And>F G. |- \<diamond>F & \<diamond>G --> (\<diamond>(F & \<diamond>G)) | (\<diamond>(G & \<diamond>F))" and
   15.45 +  discT:      "\<And>F. |- \<box>(F --> \<diamond>(\<not>F & \<diamond>F)) --> (F --> \<box>\<diamond>F)" and
   15.46 +  primeI:     "\<And>P. |- \<box>P --> Init P`" and
   15.47 +  primeE:     "\<And>P F. |- \<box>(Init P --> \<box>F) --> Init P` --> (F --> \<box>F)" and
   15.48 +  indT:       "\<And>P F. |- \<box>(Init P & \<not>\<box>F --> Init P` & F) --> Init P --> \<box>F" and
   15.49 +  allT:       "\<And>F. |- (\<forall>x. \<box>(F x)) = (\<box>(\<forall> x. F x))"
   15.50  
   15.51  axiomatization where
   15.52 -  necT:       "\<And>F. |- F ==> |- []F"      (* polymorphic *)
   15.53 +  necT:       "\<And>F. |- F ==> |- \<box>F"      (* polymorphic *)
   15.54  
   15.55  axiomatization where
   15.56  (* Flexible quantification: refinement mappings, history variables *)
   15.57 -  eexI:       "|- F x --> (EEX x. F x)" and
   15.58 -  eexE:       "[| sigma |= (EEX x. F x); basevars vs;
   15.59 -                 (!!x. [| basevars (x, vs); sigma |= F x |] ==> (G sigma)::bool)
   15.60 +  eexI:       "|- F x --> (\<exists>\<exists>x. F x)" and
   15.61 +  eexE:       "[| sigma |= (\<exists>\<exists>x. F x); basevars vs;
   15.62 +                 (\<And>x. [| basevars (x, vs); sigma |= F x |] ==> (G sigma)::bool)
   15.63                |] ==> G sigma" and
   15.64 -  history:    "|- EEX h. Init(h = ha) & [](!x. $h = #x --> h` = hb x)"
   15.65 +  history:    "|- \<exists>\<exists>h. Init(h = ha) & \<box>(\<forall>x. $h = #x --> h` = hb x)"
   15.66  
   15.67  
   15.68  (* Specialize intensional introduction/elimination rules for temporal formulas *)
   15.69  
   15.70 -lemma tempI [intro!]: "(!!sigma. sigma |= (F::temporal)) ==> |- F"
   15.71 +lemma tempI [intro!]: "(\<And>sigma. sigma |= (F::temporal)) ==> |- F"
   15.72    apply (rule intI)
   15.73    apply (erule meta_spec)
   15.74    done
   15.75 @@ -145,20 +141,20 @@
   15.76  
   15.77  
   15.78  (* ------------------------------------------------------------------------- *)
   15.79 -(***           "Simple temporal logic": only [] and <>                     ***)
   15.80 +(***           "Simple temporal logic": only \<box> and \<diamond>                     ***)
   15.81  (* ------------------------------------------------------------------------- *)
   15.82  section "Simple temporal logic"
   15.83  
   15.84 -(* []~F == []~Init F *)
   15.85 -lemmas boxNotInit = boxInit [of "LIFT ~F", unfolded Init_simps] for F
   15.86 +(* \<box>\<not>F == \<box>\<not>Init F *)
   15.87 +lemmas boxNotInit = boxInit [of "LIFT \<not>F", unfolded Init_simps] for F
   15.88  
   15.89 -lemma dmdInit: "TEMP <>F == TEMP <> Init F"
   15.90 +lemma dmdInit: "TEMP \<diamond>F == TEMP \<diamond> Init F"
   15.91    apply (unfold dmd_def)
   15.92 -  apply (unfold boxInit [of "LIFT ~F"])
   15.93 +  apply (unfold boxInit [of "LIFT \<not>F"])
   15.94    apply (simp (no_asm) add: Init_simps)
   15.95    done
   15.96  
   15.97 -lemmas dmdNotInit = dmdInit [of "LIFT ~F", unfolded Init_simps] for F
   15.98 +lemmas dmdNotInit = dmdInit [of "LIFT \<not>F", unfolded Init_simps] for F
   15.99  
  15.100  (* boxInit and dmdInit cannot be used as rewrites, because they loop.
  15.101     Non-looping instances for state predicates and actions are occasionally useful.
  15.102 @@ -180,21 +176,21 @@
  15.103  lemmas STL2 = reflT
  15.104  
  15.105  (* The "polymorphic" (generic) variant *)
  15.106 -lemma STL2_gen: "|- []F --> Init F"
  15.107 +lemma STL2_gen: "|- \<box>F --> Init F"
  15.108    apply (unfold boxInit [of F])
  15.109    apply (rule STL2)
  15.110    done
  15.111  
  15.112 -(* see also STL2_pr below: "|- []P --> Init P & Init (P`)" *)
  15.113 +(* see also STL2_pr below: "|- \<box>P --> Init P & Init (P`)" *)
  15.114  
  15.115  
  15.116 -(* Dual versions for <> *)
  15.117 -lemma InitDmd: "|- F --> <> F"
  15.118 +(* Dual versions for \<diamond> *)
  15.119 +lemma InitDmd: "|- F --> \<diamond> F"
  15.120    apply (unfold dmd_def)
  15.121    apply (auto dest!: STL2 [temp_use])
  15.122    done
  15.123  
  15.124 -lemma InitDmd_gen: "|- Init F --> <>F"
  15.125 +lemma InitDmd_gen: "|- Init F --> \<diamond>F"
  15.126    apply clarsimp
  15.127    apply (drule InitDmd [temp_use])
  15.128    apply (simp add: dmdInitD)
  15.129 @@ -202,17 +198,17 @@
  15.130  
  15.131  
  15.132  (* ------------------------ STL3 ------------------------------------------- *)
  15.133 -lemma STL3: "|- ([][]F) = ([]F)"
  15.134 +lemma STL3: "|- (\<box>\<box>F) = (\<box>F)"
  15.135    by (auto elim: transT [temp_use] STL2 [temp_use])
  15.136  
  15.137  (* corresponding elimination rule introduces double boxes:
  15.138 -   [| (sigma |= []F); (sigma |= [][]F) ==> PROP W |] ==> PROP W
  15.139 +   [| (sigma |= \<box>F); (sigma |= \<box>\<box>F) ==> PROP W |] ==> PROP W
  15.140  *)
  15.141  lemmas dup_boxE = STL3 [temp_unlift, THEN iffD2, elim_format]
  15.142  lemmas dup_boxD = STL3 [temp_unlift, THEN iffD1]
  15.143  
  15.144 -(* dual versions for <> *)
  15.145 -lemma DmdDmd: "|- (<><>F) = (<>F)"
  15.146 +(* dual versions for \<diamond> *)
  15.147 +lemma DmdDmd: "|- (\<diamond>\<diamond>F) = (\<diamond>F)"
  15.148    by (auto simp add: dmd_def [try_rewrite] STL3 [try_rewrite])
  15.149  
  15.150  lemmas dup_dmdE = DmdDmd [temp_unlift, THEN iffD2, elim_format]
  15.151 @@ -222,7 +218,7 @@
  15.152  (* ------------------------ STL4 ------------------------------------------- *)
  15.153  lemma STL4:
  15.154    assumes "|- F --> G"
  15.155 -  shows "|- []F --> []G"
  15.156 +  shows "|- \<box>F --> \<box>G"
  15.157    apply clarsimp
  15.158    apply (rule normalT [temp_use])
  15.159     apply (rule assms [THEN necT, temp_use])
  15.160 @@ -230,38 +226,38 @@
  15.161    done
  15.162  
  15.163  (* Unlifted version as an elimination rule *)
  15.164 -lemma STL4E: "[| sigma |= []F; |- F --> G |] ==> sigma |= []G"
  15.165 +lemma STL4E: "[| sigma |= \<box>F; |- F --> G |] ==> sigma |= \<box>G"
  15.166    by (erule (1) STL4 [temp_use])
  15.167  
  15.168 -lemma STL4_gen: "|- Init F --> Init G ==> |- []F --> []G"
  15.169 +lemma STL4_gen: "|- Init F --> Init G ==> |- \<box>F --> \<box>G"
  15.170    apply (drule STL4)
  15.171    apply (simp add: boxInitD)
  15.172    done
  15.173  
  15.174 -lemma STL4E_gen: "[| sigma |= []F; |- Init F --> Init G |] ==> sigma |= []G"
  15.175 +lemma STL4E_gen: "[| sigma |= \<box>F; |- Init F --> Init G |] ==> sigma |= \<box>G"
  15.176    by (erule (1) STL4_gen [temp_use])
  15.177  
  15.178  (* see also STL4Edup below, which allows an auxiliary boxed formula:
  15.179 -       []A /\ F => G
  15.180 +       \<box>A /\ F => G
  15.181       -----------------
  15.182 -     []A /\ []F => []G
  15.183 +     \<box>A /\ \<box>F => \<box>G
  15.184  *)
  15.185  
  15.186 -(* The dual versions for <> *)
  15.187 +(* The dual versions for \<diamond> *)
  15.188  lemma DmdImpl:
  15.189    assumes prem: "|- F --> G"
  15.190 -  shows "|- <>F --> <>G"
  15.191 +  shows "|- \<diamond>F --> \<diamond>G"
  15.192    apply (unfold dmd_def)
  15.193    apply (fastforce intro!: prem [temp_use] elim!: STL4E [temp_use])
  15.194    done
  15.195  
  15.196 -lemma DmdImplE: "[| sigma |= <>F; |- F --> G |] ==> sigma |= <>G"
  15.197 +lemma DmdImplE: "[| sigma |= \<diamond>F; |- F --> G |] ==> sigma |= \<diamond>G"
  15.198    by (erule (1) DmdImpl [temp_use])
  15.199  
  15.200  (* ------------------------ STL5 ------------------------------------------- *)
  15.201 -lemma STL5: "|- ([]F & []G) = ([](F & G))"
  15.202 +lemma STL5: "|- (\<box>F & \<box>G) = (\<box>(F & G))"
  15.203    apply auto
  15.204 -  apply (subgoal_tac "sigma |= [] (G --> (F & G))")
  15.205 +  apply (subgoal_tac "sigma |= \<box> (G --> (F & G))")
  15.206       apply (erule normalT [temp_use])
  15.207       apply (fastforce elim!: STL4E [temp_use])+
  15.208    done
  15.209 @@ -275,9 +271,9 @@
  15.210     Use "addSE2" etc. if you want to add this to a claset, otherwise it will loop!
  15.211  *)
  15.212  lemma box_conjE:
  15.213 -  assumes "sigma |= []F"
  15.214 -     and "sigma |= []G"
  15.215 -  and "sigma |= [](F&G) ==> PROP R"
  15.216 +  assumes "sigma |= \<box>F"
  15.217 +     and "sigma |= \<box>G"
  15.218 +  and "sigma |= \<box>(F&G) ==> PROP R"
  15.219    shows "PROP R"
  15.220    by (rule assms STL5 [temp_unlift, THEN iffD1] conjI)+
  15.221  
  15.222 @@ -292,7 +288,7 @@
  15.223     a bit kludgy in order to simulate "double elim-resolution".
  15.224  *)
  15.225  
  15.226 -lemma box_thin: "[| sigma |= []F; PROP W |] ==> PROP W" .
  15.227 +lemma box_thin: "[| sigma |= \<box>F; PROP W |] ==> PROP W" .
  15.228  
  15.229  ML {*
  15.230  fun merge_box_tac i =
  15.231 @@ -317,29 +313,29 @@
  15.232  method_setup merge_act_box = {* Scan.succeed (SIMPLE_METHOD' o merge_act_box_tac) *}
  15.233  
  15.234  (* rewrite rule to push universal quantification through box:
  15.235 -      (sigma |= [](! x. F x)) = (! x. (sigma |= []F x))
  15.236 +      (sigma |= \<box>(\<forall>x. F x)) = (\<forall>x. (sigma |= \<box>F x))
  15.237  *)
  15.238  lemmas all_box = allT [temp_unlift, symmetric]
  15.239  
  15.240 -lemma DmdOr: "|- (<>(F | G)) = (<>F | <>G)"
  15.241 +lemma DmdOr: "|- (\<diamond>(F | G)) = (\<diamond>F | \<diamond>G)"
  15.242    apply (auto simp add: dmd_def split_box_conj [try_rewrite])
  15.243    apply (erule contrapos_np, merge_box, fastforce elim!: STL4E [temp_use])+
  15.244    done
  15.245  
  15.246 -lemma exT: "|- (EX x. <>(F x)) = (<>(EX x. F x))"
  15.247 +lemma exT: "|- (\<exists>x. \<diamond>(F x)) = (\<diamond>(\<exists>x. F x))"
  15.248    by (auto simp: dmd_def Not_Rex [try_rewrite] all_box [try_rewrite])
  15.249  
  15.250  lemmas ex_dmd = exT [temp_unlift, symmetric]
  15.251  
  15.252 -lemma STL4Edup: "!!sigma. [| sigma |= []A; sigma |= []F; |- F & []A --> G |] ==> sigma |= []G"
  15.253 +lemma STL4Edup: "\<And>sigma. [| sigma |= \<box>A; sigma |= \<box>F; |- F & \<box>A --> G |] ==> sigma |= \<box>G"
  15.254    apply (erule dup_boxE)
  15.255    apply merge_box
  15.256    apply (erule STL4E)
  15.257    apply assumption
  15.258    done
  15.259  
  15.260 -lemma DmdImpl2: 
  15.261 -    "!!sigma. [| sigma |= <>F; sigma |= [](F --> G) |] ==> sigma |= <>G"
  15.262 +lemma DmdImpl2:
  15.263 +    "\<And>sigma. [| sigma |= \<diamond>F; sigma |= \<box>(F --> G) |] ==> sigma |= \<diamond>G"
  15.264    apply (unfold dmd_def)
  15.265    apply auto
  15.266    apply (erule notE)
  15.267 @@ -348,10 +344,10 @@
  15.268    done
  15.269  
  15.270  lemma InfImpl:
  15.271 -  assumes 1: "sigma |= []<>F"
  15.272 -    and 2: "sigma |= []G"
  15.273 +  assumes 1: "sigma |= \<box>\<diamond>F"
  15.274 +    and 2: "sigma |= \<box>G"
  15.275      and 3: "|- F & G --> H"
  15.276 -  shows "sigma |= []<>H"
  15.277 +  shows "sigma |= \<box>\<diamond>H"
  15.278    apply (insert 1 2)
  15.279    apply (erule_tac F = G in dup_boxE)
  15.280    apply merge_box
  15.281 @@ -360,7 +356,7 @@
  15.282  
  15.283  (* ------------------------ STL6 ------------------------------------------- *)
  15.284  (* Used in the proof of STL6, but useful in itself. *)
  15.285 -lemma BoxDmd: "|- []F & <>G --> <>([]F & G)"
  15.286 +lemma BoxDmd: "|- \<box>F & \<diamond>G --> \<diamond>(\<box>F & G)"
  15.287    apply (unfold dmd_def)
  15.288    apply clarsimp
  15.289    apply (erule dup_boxE)
  15.290 @@ -370,14 +366,14 @@
  15.291    done
  15.292  
  15.293  (* weaker than BoxDmd, but more polymorphic (and often just right) *)
  15.294 -lemma BoxDmd_simple: "|- []F & <>G --> <>(F & G)"
  15.295 +lemma BoxDmd_simple: "|- \<box>F & \<diamond>G --> \<diamond>(F & G)"
  15.296    apply (unfold dmd_def)
  15.297    apply clarsimp
  15.298    apply merge_box
  15.299    apply (fastforce elim!: notE STL4E [temp_use])
  15.300    done
  15.301  
  15.302 -lemma BoxDmd2_simple: "|- []F & <>G --> <>(G & F)"
  15.303 +lemma BoxDmd2_simple: "|- \<box>F & \<diamond>G --> \<diamond>(G & F)"
  15.304    apply (unfold dmd_def)
  15.305    apply clarsimp
  15.306    apply merge_box
  15.307 @@ -385,15 +381,15 @@
  15.308    done
  15.309  
  15.310  lemma DmdImpldup:
  15.311 -  assumes 1: "sigma |= []A"
  15.312 -    and 2: "sigma |= <>F"
  15.313 -    and 3: "|- []A & F --> G"
  15.314 -  shows "sigma |= <>G"
  15.315 +  assumes 1: "sigma |= \<box>A"
  15.316 +    and 2: "sigma |= \<diamond>F"
  15.317 +    and 3: "|- \<box>A & F --> G"
  15.318 +  shows "sigma |= \<diamond>G"
  15.319    apply (rule 2 [THEN 1 [THEN BoxDmd [temp_use]], THEN DmdImplE])
  15.320    apply (rule 3)
  15.321    done
  15.322  
  15.323 -lemma STL6: "|- <>[]F & <>[]G --> <>[](F & G)"
  15.324 +lemma STL6: "|- \<diamond>\<box>F & \<diamond>\<box>G --> \<diamond>\<box>(F & G)"
  15.325    apply (auto simp: STL5 [temp_rewrite, symmetric])
  15.326    apply (drule linT [temp_use])
  15.327     apply assumption
  15.328 @@ -414,13 +410,13 @@
  15.329  (* ------------------------ True / False ----------------------------------------- *)
  15.330  section "Simplification of constants"
  15.331  
  15.332 -lemma BoxConst: "|- ([]#P) = #P"
  15.333 +lemma BoxConst: "|- (\<box>#P) = #P"
  15.334    apply (rule tempI)
  15.335    apply (cases P)
  15.336     apply (auto intro!: necT [temp_use] dest: STL2_gen [temp_use] simp: Init_simps)
  15.337    done
  15.338  
  15.339 -lemma DmdConst: "|- (<>#P) = #P"
  15.340 +lemma DmdConst: "|- (\<diamond>#P) = #P"
  15.341    apply (unfold dmd_def)
  15.342    apply (cases P)
  15.343    apply (simp_all add: BoxConst [try_rewrite])
  15.344 @@ -432,23 +428,23 @@
  15.345  (* ------------------------ Further rewrites ----------------------------------------- *)
  15.346  section "Further rewrites"
  15.347  
  15.348 -lemma NotBox: "|- (~[]F) = (<>~F)"
  15.349 +lemma NotBox: "|- (\<not>\<box>F) = (\<diamond>\<not>F)"
  15.350    by (simp add: dmd_def)
  15.351  
  15.352 -lemma NotDmd: "|- (~<>F) = ([]~F)"
  15.353 +lemma NotDmd: "|- (\<not>\<diamond>F) = (\<box>\<not>F)"
  15.354    by (simp add: dmd_def)
  15.355  
  15.356  (* These are not declared by default, because they could be harmful,
  15.357 -   e.g. []F & ~[]F becomes []F & <>~F !! *)
  15.358 +   e.g. \<box>F & \<not>\<box>F becomes \<box>F & \<diamond>\<not>F !! *)
  15.359  lemmas more_temp_simps1 =
  15.360    STL3 [temp_rewrite] DmdDmd [temp_rewrite] NotBox [temp_rewrite] NotDmd [temp_rewrite]
  15.361    NotBox [temp_unlift, THEN eq_reflection]
  15.362    NotDmd [temp_unlift, THEN eq_reflection]
  15.363  
  15.364 -lemma BoxDmdBox: "|- ([]<>[]F) = (<>[]F)"
  15.365 +lemma BoxDmdBox: "|- (\<box>\<diamond>\<box>F) = (\<diamond>\<box>F)"
  15.366    apply (auto dest!: STL2 [temp_use])
  15.367    apply (rule ccontr)
  15.368 -  apply (subgoal_tac "sigma |= <>[][]F & <>[]~[]F")
  15.369 +  apply (subgoal_tac "sigma |= \<diamond>\<box>\<box>F & \<diamond>\<box>\<not>\<box>F")
  15.370     apply (erule thin_rl)
  15.371     apply auto
  15.372      apply (drule STL6 [temp_use])
  15.373 @@ -457,7 +453,7 @@
  15.374     apply (simp_all add: more_temp_simps1)
  15.375    done
  15.376  
  15.377 -lemma DmdBoxDmd: "|- (<>[]<>F) = ([]<>F)"
  15.378 +lemma DmdBoxDmd: "|- (\<diamond>\<box>\<diamond>F) = (\<box>\<diamond>F)"
  15.379    apply (unfold dmd_def)
  15.380    apply (auto simp: BoxDmdBox [unfolded dmd_def, try_rewrite])
  15.381    done
  15.382 @@ -467,11 +463,11 @@
  15.383  
  15.384  (* ------------------------ Miscellaneous ----------------------------------- *)
  15.385  
  15.386 -lemma BoxOr: "!!sigma. [| sigma |= []F | []G |] ==> sigma |= [](F | G)"
  15.387 +lemma BoxOr: "\<And>sigma. [| sigma |= \<box>F | \<box>G |] ==> sigma |= \<box>(F | G)"
  15.388    by (fastforce elim!: STL4E [temp_use])
  15.389  
  15.390  (* "persistently implies infinitely often" *)
  15.391 -lemma DBImplBD: "|- <>[]F --> []<>F"
  15.392 +lemma DBImplBD: "|- \<diamond>\<box>F --> \<box>\<diamond>F"
  15.393    apply clarsimp
  15.394    apply (rule ccontr)
  15.395    apply (simp add: more_temp_simps2)
  15.396 @@ -480,13 +476,13 @@
  15.397    apply simp
  15.398    done
  15.399  
  15.400 -lemma BoxDmdDmdBox: "|- []<>F & <>[]G --> []<>(F & G)"
  15.401 +lemma BoxDmdDmdBox: "|- \<box>\<diamond>F & \<diamond>\<box>G --> \<box>\<diamond>(F & G)"
  15.402    apply clarsimp
  15.403    apply (rule ccontr)
  15.404    apply (unfold more_temp_simps2)
  15.405    apply (drule STL6 [temp_use])
  15.406     apply assumption
  15.407 -  apply (subgoal_tac "sigma |= <>[]~F")
  15.408 +  apply (subgoal_tac "sigma |= \<diamond>\<box>\<not>F")
  15.409     apply (force simp: dmd_def)
  15.410    apply (fastforce elim: DmdImplE [temp_use] STL4E [temp_use])
  15.411    done
  15.412 @@ -498,11 +494,11 @@
  15.413  section "priming"
  15.414  
  15.415  (* ------------------------ TLA2 ------------------------------------------- *)
  15.416 -lemma STL2_pr: "|- []P --> Init P & Init P`"
  15.417 +lemma STL2_pr: "|- \<box>P --> Init P & Init P`"
  15.418    by (fastforce intro!: STL2_gen [temp_use] primeI [temp_use])
  15.419  
  15.420  (* Auxiliary lemma allows priming of boxed actions *)
  15.421 -lemma BoxPrime: "|- []P --> []($P & P$)"
  15.422 +lemma BoxPrime: "|- \<box>P --> \<box>($P & P$)"
  15.423    apply clarsimp
  15.424    apply (erule dup_boxE)
  15.425    apply (unfold boxInit_act)
  15.426 @@ -512,17 +508,17 @@
  15.427  
  15.428  lemma TLA2:
  15.429    assumes "|- $P & P$ --> A"
  15.430 -  shows "|- []P --> []A"
  15.431 +  shows "|- \<box>P --> \<box>A"
  15.432    apply clarsimp
  15.433    apply (drule BoxPrime [temp_use])
  15.434    apply (auto simp: Init_stp_act_rev [try_rewrite] intro!: assms [temp_use]
  15.435      elim!: STL4E [temp_use])
  15.436    done
  15.437  
  15.438 -lemma TLA2E: "[| sigma |= []P; |- $P & P$ --> A |] ==> sigma |= []A"
  15.439 +lemma TLA2E: "[| sigma |= \<box>P; |- $P & P$ --> A |] ==> sigma |= \<box>A"
  15.440    by (erule (1) TLA2 [temp_use])
  15.441  
  15.442 -lemma DmdPrime: "|- (<>P`) --> (<>P)"
  15.443 +lemma DmdPrime: "|- (\<diamond>P`) --> (\<diamond>P)"
  15.444    apply (unfold dmd_def)
  15.445    apply (fastforce elim!: TLA2E [temp_use])
  15.446    done
  15.447 @@ -533,13 +529,13 @@
  15.448  section "stable, invariant"
  15.449  
  15.450  lemma ind_rule:
  15.451 -   "[| sigma |= []H; sigma |= Init P; |- H --> (Init P & ~[]F --> Init(P`) & F) |]  
  15.452 -    ==> sigma |= []F"
  15.453 +   "[| sigma |= \<box>H; sigma |= Init P; |- H --> (Init P & \<not>\<box>F --> Init(P`) & F) |]
  15.454 +    ==> sigma |= \<box>F"
  15.455    apply (rule indT [temp_use])
  15.456     apply (erule (2) STL4E)
  15.457    done
  15.458  
  15.459 -lemma box_stp_act: "|- ([]$P) = ([]P)"
  15.460 +lemma box_stp_act: "|- (\<box>$P) = (\<box>P)"
  15.461    by (simp add: boxInit_act Init_simps)
  15.462  
  15.463  lemmas box_stp_actI = box_stp_act [temp_use, THEN iffD2]
  15.464 @@ -547,32 +543,32 @@
  15.465  
  15.466  lemmas more_temp_simps3 = box_stp_act [temp_rewrite] more_temp_simps2
  15.467  
  15.468 -lemma INV1: 
  15.469 -  "|- (Init P) --> (stable P) --> []P"
  15.470 +lemma INV1:
  15.471 +  "|- (Init P) --> (stable P) --> \<box>P"
  15.472    apply (unfold stable_def boxInit_stp boxInit_act)
  15.473    apply clarsimp
  15.474    apply (erule ind_rule)
  15.475     apply (auto simp: Init_simps elim: ind_rule)
  15.476    done
  15.477  
  15.478 -lemma StableT: 
  15.479 -    "!!P. |- $P & A --> P` ==> |- []A --> stable P"
  15.480 +lemma StableT:
  15.481 +    "\<And>P. |- $P & A --> P` ==> |- \<box>A --> stable P"
  15.482    apply (unfold stable_def)
  15.483    apply (fastforce elim!: STL4E [temp_use])
  15.484    done
  15.485  
  15.486 -lemma Stable: "[| sigma |= []A; |- $P & A --> P` |] ==> sigma |= stable P"
  15.487 +lemma Stable: "[| sigma |= \<box>A; |- $P & A --> P` |] ==> sigma |= stable P"
  15.488    by (erule (1) StableT [temp_use])
  15.489  
  15.490  (* Generalization of INV1 *)
  15.491 -lemma StableBox: "|- (stable P) --> [](Init P --> []P)"
  15.492 +lemma StableBox: "|- (stable P) --> \<box>(Init P --> \<box>P)"
  15.493    apply (unfold stable_def)
  15.494    apply clarsimp
  15.495    apply (erule dup_boxE)
  15.496    apply (force simp: stable_def elim: STL4E [temp_use] INV1 [temp_use])
  15.497    done
  15.498  
  15.499 -lemma DmdStable: "|- (stable P) & <>P --> <>[]P"
  15.500 +lemma DmdStable: "|- (stable P) & \<diamond>P --> \<diamond>\<box>P"
  15.501    apply clarsimp
  15.502    apply (rule DmdImpl2)
  15.503     prefer 2
  15.504 @@ -583,7 +579,7 @@
  15.505  (* ---------------- (Semi-)automatic invariant tactics ---------------------- *)
  15.506  
  15.507  ML {*
  15.508 -(* inv_tac reduces goals of the form ... ==> sigma |= []P *)
  15.509 +(* inv_tac reduces goals of the form ... ==> sigma |= \<box>P *)
  15.510  fun inv_tac ctxt =
  15.511    SELECT_GOAL
  15.512      (EVERY
  15.513 @@ -593,7 +589,7 @@
  15.514        TRYALL (etac @{thm Stable})]);
  15.515  
  15.516  (* auto_inv_tac applies inv_tac and then tries to attack the subgoals
  15.517 -   in simple cases it may be able to handle goals like |- MyProg --> []Inv.
  15.518 +   in simple cases it may be able to handle goals like |- MyProg --> \<box>Inv.
  15.519     In these simple cases the simplifier seems to be more useful than the
  15.520     auto-tactic, which applies too much propositional logic and simplifies
  15.521     too late.
  15.522 @@ -613,7 +609,7 @@
  15.523    Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o auto_inv_tac))
  15.524  *}
  15.525  
  15.526 -lemma unless: "|- []($P --> P` | Q`) --> (stable P) | <>Q"
  15.527 +lemma unless: "|- \<box>($P --> P` | Q`) --> (stable P) | \<diamond>Q"
  15.528    apply (unfold dmd_def)
  15.529    apply (clarsimp dest!: BoxPrime [temp_use])
  15.530    apply merge_box
  15.531 @@ -625,29 +621,29 @@
  15.532  (* --------------------- Recursive expansions --------------------------------------- *)
  15.533  section "recursive expansions"
  15.534  
  15.535 -(* Recursive expansions of [] and <> for state predicates *)
  15.536 -lemma BoxRec: "|- ([]P) = (Init P & []P`)"
  15.537 +(* Recursive expansions of \<box> and \<diamond> for state predicates *)
  15.538 +lemma BoxRec: "|- (\<box>P) = (Init P & \<box>P`)"
  15.539    apply (auto intro!: STL2_gen [temp_use])
  15.540     apply (fastforce elim!: TLA2E [temp_use])
  15.541    apply (auto simp: stable_def elim!: INV1 [temp_use] STL4E [temp_use])
  15.542    done
  15.543  
  15.544 -lemma DmdRec: "|- (<>P) = (Init P | <>P`)"
  15.545 +lemma DmdRec: "|- (\<diamond>P) = (Init P | \<diamond>P`)"
  15.546    apply (unfold dmd_def BoxRec [temp_rewrite])
  15.547    apply (auto simp: Init_simps)
  15.548    done
  15.549  
  15.550 -lemma DmdRec2: "!!sigma. [| sigma |= <>P; sigma |= []~P` |] ==> sigma |= Init P"
  15.551 +lemma DmdRec2: "\<And>sigma. [| sigma |= \<diamond>P; sigma |= \<box>\<not>P` |] ==> sigma |= Init P"
  15.552    apply (force simp: DmdRec [temp_rewrite] dmd_def)
  15.553    done
  15.554  
  15.555 -lemma InfinitePrime: "|- ([]<>P) = ([]<>P`)"
  15.556 +lemma InfinitePrime: "|- (\<box>\<diamond>P) = (\<box>\<diamond>P`)"
  15.557    apply auto
  15.558     apply (rule classical)
  15.559     apply (rule DBImplBD [temp_use])
  15.560 -   apply (subgoal_tac "sigma |= <>[]P")
  15.561 +   apply (subgoal_tac "sigma |= \<diamond>\<box>P")
  15.562      apply (fastforce elim!: DmdImplE [temp_use] TLA2E [temp_use])
  15.563 -   apply (subgoal_tac "sigma |= <>[] (<>P & []~P`)")
  15.564 +   apply (subgoal_tac "sigma |= \<diamond>\<box> (\<diamond>P & \<box>\<not>P`)")
  15.565      apply (force simp: boxInit_stp [temp_use]
  15.566        elim!: DmdImplE [temp_use] STL4E [temp_use] DmdRec2 [temp_use])
  15.567     apply (force intro!: STL6 [temp_use] simp: more_temp_simps3)
  15.568 @@ -655,7 +651,7 @@
  15.569    done
  15.570  
  15.571  lemma InfiniteEnsures:
  15.572 -  "[| sigma |= []N; sigma |= []<>A; |- A & N --> P` |] ==> sigma |= []<>P"
  15.573 +  "[| sigma |= \<box>N; sigma |= \<box>\<diamond>A; |- A & N --> P` |] ==> sigma |= \<box>\<diamond>P"
  15.574    apply (unfold InfinitePrime [temp_rewrite])
  15.575    apply (rule InfImpl)
  15.576      apply assumption+
  15.577 @@ -665,27 +661,27 @@
  15.578  section "fairness"
  15.579  
  15.580  (* alternative definitions of fairness *)
  15.581 -lemma WF_alt: "|- WF(A)_v = ([]<>~Enabled(<A>_v) | []<><A>_v)"
  15.582 +lemma WF_alt: "|- WF(A)_v = (\<box>\<diamond>\<not>Enabled(<A>_v) | \<box>\<diamond><A>_v)"
  15.583    apply (unfold WF_def dmd_def)
  15.584    apply fastforce
  15.585    done
  15.586  
  15.587 -lemma SF_alt: "|- SF(A)_v = (<>[]~Enabled(<A>_v) | []<><A>_v)"
  15.588 +lemma SF_alt: "|- SF(A)_v = (\<diamond>\<box>\<not>Enabled(<A>_v) | \<box>\<diamond><A>_v)"
  15.589    apply (unfold SF_def dmd_def)
  15.590    apply fastforce
  15.591    done
  15.592  
  15.593  (* theorems to "box" fairness conditions *)
  15.594 -lemma BoxWFI: "|- WF(A)_v --> []WF(A)_v"
  15.595 +lemma BoxWFI: "|- WF(A)_v --> \<box>WF(A)_v"
  15.596    by (auto simp: WF_alt [try_rewrite] more_temp_simps3 intro!: BoxOr [temp_use])
  15.597  
  15.598 -lemma WF_Box: "|- ([]WF(A)_v) = WF(A)_v"
  15.599 +lemma WF_Box: "|- (\<box>WF(A)_v) = WF(A)_v"
  15.600    by (fastforce intro!: BoxWFI [temp_use] dest!: STL2 [temp_use])
  15.601  
  15.602 -lemma BoxSFI: "|- SF(A)_v --> []SF(A)_v"
  15.603 +lemma BoxSFI: "|- SF(A)_v --> \<box>SF(A)_v"
  15.604    by (auto simp: SF_alt [try_rewrite] more_temp_simps3 intro!: BoxOr [temp_use])
  15.605  
  15.606 -lemma SF_Box: "|- ([]SF(A)_v) = SF(A)_v"
  15.607 +lemma SF_Box: "|- (\<box>SF(A)_v) = SF(A)_v"
  15.608    by (fastforce intro!: BoxSFI [temp_use] dest!: STL2 [temp_use])
  15.609  
  15.610  lemmas more_temp_simps = more_temp_simps3 WF_Box [temp_rewrite] SF_Box [temp_rewrite]
  15.611 @@ -704,30 +700,30 @@
  15.612  
  15.613  (* ------------------------------ leads-to ------------------------------ *)
  15.614  
  15.615 -section "~>"
  15.616 +section "\<leadsto>"
  15.617  
  15.618 -lemma leadsto_init: "|- (Init F) & (F ~> G) --> <>G"
  15.619 +lemma leadsto_init: "|- (Init F) & (F \<leadsto> G) --> \<diamond>G"
  15.620    apply (unfold leadsto_def)
  15.621    apply (auto dest!: STL2 [temp_use])
  15.622    done
  15.623  
  15.624 -(* |- F & (F ~> G) --> <>G *)
  15.625 +(* |- F & (F \<leadsto> G) --> \<diamond>G *)
  15.626  lemmas leadsto_init_temp = leadsto_init [where 'a = behavior, unfolded Init_simps]
  15.627  
  15.628 -lemma streett_leadsto: "|- ([]<>Init F --> []<>G) = (<>(F ~> G))"
  15.629 +lemma streett_leadsto: "|- (\<box>\<diamond>Init F --> \<box>\<diamond>G) = (\<diamond>(F \<leadsto> G))"
  15.630    apply (unfold leadsto_def)
  15.631    apply auto
  15.632      apply (simp add: more_temp_simps)
  15.633      apply (fastforce elim!: DmdImplE [temp_use] STL4E [temp_use])
  15.634     apply (fastforce intro!: InitDmd [temp_use] elim!: STL4E [temp_use])
  15.635 -  apply (subgoal_tac "sigma |= []<><>G")
  15.636 +  apply (subgoal_tac "sigma |= \<box>\<diamond>\<diamond>G")
  15.637     apply (simp add: more_temp_simps)
  15.638    apply (drule BoxDmdDmdBox [temp_use])
  15.639     apply assumption
  15.640    apply (fastforce elim!: DmdImplE [temp_use] STL4E [temp_use])
  15.641    done
  15.642  
  15.643 -lemma leadsto_infinite: "|- []<>F & (F ~> G) --> []<>G"
  15.644 +lemma leadsto_infinite: "|- \<box>\<diamond>F & (F \<leadsto> G) --> \<box>\<diamond>G"
  15.645    apply clarsimp
  15.646    apply (erule InitDmd [temp_use, THEN streett_leadsto [temp_unlift, THEN iffD2, THEN mp]])
  15.647    apply (simp add: dmdInitD)
  15.648 @@ -736,18 +732,18 @@
  15.649  (* In particular, strong fairness is a Streett condition. The following
  15.650     rules are sometimes easier to use than WF2 or SF2 below.
  15.651  *)
  15.652 -lemma leadsto_SF: "|- (Enabled(<A>_v) ~> <A>_v) --> SF(A)_v"
  15.653 +lemma leadsto_SF: "|- (Enabled(<A>_v) \<leadsto> <A>_v) --> SF(A)_v"
  15.654    apply (unfold SF_def)
  15.655    apply (clarsimp elim!: leadsto_infinite [temp_use])
  15.656    done
  15.657  
  15.658 -lemma leadsto_WF: "|- (Enabled(<A>_v) ~> <A>_v) --> WF(A)_v"
  15.659 +lemma leadsto_WF: "|- (Enabled(<A>_v) \<leadsto> <A>_v) --> WF(A)_v"
  15.660    by (clarsimp intro!: SFImplWF [temp_use] leadsto_SF [temp_use])
  15.661  
  15.662  (* introduce an invariant into the proof of a leadsto assertion.
  15.663 -   []I --> ((P ~> Q)  =  (P /\ I ~> Q))
  15.664 +   \<box>I --> ((P \<leadsto> Q)  =  (P /\ I \<leadsto> Q))
  15.665  *)
  15.666 -lemma INV_leadsto: "|- []I & (P & I ~> Q) --> (P ~> Q)"
  15.667 +lemma INV_leadsto: "|- \<box>I & (P & I \<leadsto> Q) --> (P \<leadsto> Q)"
  15.668    apply (unfold leadsto_def)
  15.669    apply clarsimp
  15.670    apply (erule STL4Edup)
  15.671 @@ -755,24 +751,24 @@
  15.672    apply (auto simp: Init_simps dest!: STL2_gen [temp_use])
  15.673    done
  15.674  
  15.675 -lemma leadsto_classical: "|- (Init F & []~G ~> G) --> (F ~> G)"
  15.676 +lemma leadsto_classical: "|- (Init F & \<box>\<not>G \<leadsto> G) --> (F \<leadsto> G)"
  15.677    apply (unfold leadsto_def dmd_def)
  15.678    apply (force simp: Init_simps elim!: STL4E [temp_use])
  15.679    done
  15.680  
  15.681 -lemma leadsto_false: "|- (F ~> #False) = ([]~F)"
  15.682 +lemma leadsto_false: "|- (F \<leadsto> #False) = (\<box>~F)"
  15.683    apply (unfold leadsto_def)
  15.684    apply (simp add: boxNotInitD)
  15.685    done
  15.686  
  15.687 -lemma leadsto_exists: "|- ((EX x. F x) ~> G) = (ALL x. (F x ~> G))"
  15.688 +lemma leadsto_exists: "|- ((\<exists>x. F x) \<leadsto> G) = (\<forall>x. (F x \<leadsto> G))"
  15.689    apply (unfold leadsto_def)
  15.690    apply (auto simp: allT [try_rewrite] Init_simps elim!: STL4E [temp_use])
  15.691    done
  15.692  
  15.693  (* basic leadsto properties, cf. Unity *)
  15.694  
  15.695 -lemma ImplLeadsto_gen: "|- [](Init F --> Init G) --> (F ~> G)"
  15.696 +lemma ImplLeadsto_gen: "|- \<box>(Init F --> Init G) --> (F \<leadsto> G)"
  15.697    apply (unfold leadsto_def)
  15.698    apply (auto intro!: InitDmd_gen [temp_use]
  15.699      elim!: STL4E_gen [temp_use] simp: Init_simps)
  15.700 @@ -781,19 +777,19 @@
  15.701  lemmas ImplLeadsto =
  15.702    ImplLeadsto_gen [where 'a = behavior and 'b = behavior, unfolded Init_simps]
  15.703  
  15.704 -lemma ImplLeadsto_simple: "!!F G. |- F --> G ==> |- F ~> G"
  15.705 +lemma ImplLeadsto_simple: "\<And>F G. |- F --> G ==> |- F \<leadsto> G"
  15.706    by (auto simp: Init_def intro!: ImplLeadsto_gen [temp_use] necT [temp_use])
  15.707  
  15.708  lemma EnsuresLeadsto:
  15.709    assumes "|- A & $P --> Q`"
  15.710 -  shows "|- []A --> (P ~> Q)"
  15.711 +  shows "|- \<box>A --> (P \<leadsto> Q)"
  15.712    apply (unfold leadsto_def)
  15.713    apply (clarsimp elim!: INV_leadsto [temp_use])
  15.714    apply (erule STL4E_gen)
  15.715    apply (auto simp: Init_defs intro!: PrimeDmd [temp_use] assms [temp_use])
  15.716    done
  15.717  
  15.718 -lemma EnsuresLeadsto2: "|- []($P --> Q`) --> (P ~> Q)"
  15.719 +lemma EnsuresLeadsto2: "|- \<box>($P --> Q`) --> (P \<leadsto> Q)"
  15.720    apply (unfold leadsto_def)
  15.721    apply clarsimp
  15.722    apply (erule STL4E_gen)
  15.723 @@ -803,13 +799,13 @@
  15.724  lemma ensures:
  15.725    assumes 1: "|- $P & N --> P` | Q`"
  15.726      and 2: "|- ($P & N) & A --> Q`"
  15.727 -  shows "|- []N & []([]P --> <>A) --> (P ~> Q)"
  15.728 +  shows "|- \<box>N & \<box>(\<box>P --> \<diamond>A) --> (P \<leadsto> Q)"
  15.729    apply (unfold leadsto_def)
  15.730    apply clarsimp
  15.731    apply (erule STL4Edup)
  15.732     apply assumption
  15.733    apply clarsimp
  15.734 -  apply (subgoal_tac "sigmaa |= [] ($P --> P` | Q`) ")
  15.735 +  apply (subgoal_tac "sigmaa |= \<box>($P --> P` | Q`) ")
  15.736     apply (drule unless [temp_use])
  15.737     apply (clarsimp dest!: INV1 [temp_use])
  15.738    apply (rule 2 [THEN DmdImpl, temp_use, THEN DmdPrime [temp_use]])
  15.739 @@ -819,16 +815,16 @@
  15.740    done
  15.741  
  15.742  lemma ensures_simple:
  15.743 -  "[| |- $P & N --> P` | Q`;  
  15.744 -      |- ($P & N) & A --> Q`  
  15.745 -   |] ==> |- []N & []<>A --> (P ~> Q)"
  15.746 +  "[| |- $P & N --> P` | Q`;
  15.747 +      |- ($P & N) & A --> Q`
  15.748 +   |] ==> |- \<box>N & \<box>\<diamond>A --> (P \<leadsto> Q)"
  15.749    apply clarsimp
  15.750    apply (erule (2) ensures [temp_use])
  15.751    apply (force elim!: STL4E [temp_use])
  15.752    done
  15.753  
  15.754  lemma EnsuresInfinite:
  15.755 -    "[| sigma |= []<>P; sigma |= []A; |- A & $P --> Q` |] ==> sigma |= []<>Q"
  15.756 +    "[| sigma |= \<box>\<diamond>P; sigma |= \<box>A; |- A & $P --> Q` |] ==> sigma |= \<box>\<diamond>Q"
  15.757    apply (erule leadsto_infinite [temp_use])
  15.758    apply (erule EnsuresLeadsto [temp_use])
  15.759    apply assumption
  15.760 @@ -838,64 +834,64 @@
  15.761  (*** Gronning's lattice rules (taken from TLP) ***)
  15.762  section "Lattice rules"
  15.763  
  15.764 -lemma LatticeReflexivity: "|- F ~> F"
  15.765 +lemma LatticeReflexivity: "|- F \<leadsto> F"
  15.766    apply (unfold leadsto_def)
  15.767    apply (rule necT InitDmd_gen)+
  15.768    done
  15.769  
  15.770 -lemma LatticeTransitivity: "|- (G ~> H) & (F ~> G) --> (F ~> H)"
  15.771 +lemma LatticeTransitivity: "|- (G \<leadsto> H) & (F \<leadsto> G) --> (F \<leadsto> H)"
  15.772    apply (unfold leadsto_def)
  15.773    apply clarsimp
  15.774 -  apply (erule dup_boxE) (* [][] (Init G --> H) *)
  15.775 +  apply (erule dup_boxE) (* \<box>\<box>(Init G --> H) *)
  15.776    apply merge_box
  15.777    apply (clarsimp elim!: STL4E [temp_use])
  15.778    apply (rule dup_dmdD)
  15.779 -  apply (subgoal_tac "sigmaa |= <>Init G")
  15.780 +  apply (subgoal_tac "sigmaa |= \<diamond>Init G")
  15.781     apply (erule DmdImpl2)
  15.782     apply assumption
  15.783    apply (simp add: dmdInitD)
  15.784    done
  15.785  
  15.786 -lemma LatticeDisjunctionElim1: "|- (F | G ~> H) --> (F ~> H)"
  15.787 +lemma LatticeDisjunctionElim1: "|- (F | G \<leadsto> H) --> (F \<leadsto> H)"
  15.788    apply (unfold leadsto_def)
  15.789    apply (auto simp: Init_simps elim!: STL4E [temp_use])
  15.790    done
  15.791  
  15.792 -lemma LatticeDisjunctionElim2: "|- (F | G ~> H) --> (G ~> H)"
  15.793 +lemma LatticeDisjunctionElim2: "|- (F | G \<leadsto> H) --> (G \<leadsto> H)"
  15.794    apply (unfold leadsto_def)
  15.795    apply (auto simp: Init_simps elim!: STL4E [temp_use])
  15.796    done
  15.797  
  15.798 -lemma LatticeDisjunctionIntro: "|- (F ~> H) & (G ~> H) --> (F | G ~> H)"
  15.799 +lemma LatticeDisjunctionIntro: "|- (F \<leadsto> H) & (G \<leadsto> H) --> (F | G \<leadsto> H)"
  15.800    apply (unfold leadsto_def)
  15.801    apply clarsimp
  15.802    apply merge_box
  15.803    apply (auto simp: Init_simps elim!: STL4E [temp_use])
  15.804    done
  15.805  
  15.806 -lemma LatticeDisjunction: "|- (F | G ~> H) = ((F ~> H) & (G ~> H))"
  15.807 +lemma LatticeDisjunction: "|- (F | G \<leadsto> H) = ((F \<leadsto> H) & (G \<leadsto> H))"
  15.808    by (auto intro: LatticeDisjunctionIntro [temp_use]
  15.809      LatticeDisjunctionElim1 [temp_use]
  15.810      LatticeDisjunctionElim2 [temp_use])
  15.811  
  15.812 -lemma LatticeDiamond: "|- (A ~> B | C) & (B ~> D) & (C ~> D) --> (A ~> D)"
  15.813 +lemma LatticeDiamond: "|- (A \<leadsto> B | C) & (B \<leadsto> D) & (C \<leadsto> D) --> (A \<leadsto> D)"
  15.814    apply clarsimp
  15.815 -  apply (subgoal_tac "sigma |= (B | C) ~> D")
  15.816 +  apply (subgoal_tac "sigma |= (B | C) \<leadsto> D")
  15.817    apply (erule_tac G = "LIFT (B | C)" in LatticeTransitivity [temp_use])
  15.818     apply (fastforce intro!: LatticeDisjunctionIntro [temp_use])+
  15.819    done
  15.820  
  15.821 -lemma LatticeTriangle: "|- (A ~> D | B) & (B ~> D) --> (A ~> D)"
  15.822 +lemma LatticeTriangle: "|- (A \<leadsto> D | B) & (B \<leadsto> D) --> (A \<leadsto> D)"
  15.823    apply clarsimp
  15.824 -  apply (subgoal_tac "sigma |= (D | B) ~> D")
  15.825 +  apply (subgoal_tac "sigma |= (D | B) \<leadsto> D")
  15.826     apply (erule_tac G = "LIFT (D | B)" in LatticeTransitivity [temp_use])
  15.827    apply assumption
  15.828    apply (auto intro: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use])
  15.829    done
  15.830  
  15.831 -lemma LatticeTriangle2: "|- (A ~> B | D) & (B ~> D) --> (A ~> D)"
  15.832 +lemma LatticeTriangle2: "|- (A \<leadsto> B | D) & (B \<leadsto> D) --> (A \<leadsto> D)"
  15.833    apply clarsimp
  15.834 -  apply (subgoal_tac "sigma |= B | D ~> D")
  15.835 +  apply (subgoal_tac "sigma |= B | D \<leadsto> D")
  15.836     apply (erule_tac G = "LIFT (B | D)" in LatticeTransitivity [temp_use])
  15.837     apply assumption
  15.838    apply (auto intro: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use])
  15.839 @@ -905,10 +901,10 @@
  15.840  section "Fairness rules"
  15.841  
  15.842  lemma WF1:
  15.843 -  "[| |- $P & N  --> P` | Q`;    
  15.844 -      |- ($P & N) & <A>_v --> Q`;    
  15.845 -      |- $P & N --> $(Enabled(<A>_v)) |]    
  15.846 -  ==> |- []N & WF(A)_v --> (P ~> Q)"
  15.847 +  "[| |- $P & N  --> P` | Q`;
  15.848 +      |- ($P & N) & <A>_v --> Q`;
  15.849 +      |- $P & N --> $(Enabled(<A>_v)) |]
  15.850 +  ==> |- \<box>N & WF(A)_v --> (P \<leadsto> Q)"
  15.851    apply (clarsimp dest!: BoxWFI [temp_use])
  15.852    apply (erule (2) ensures [temp_use])
  15.853    apply (erule (1) STL4Edup)
  15.854 @@ -923,8 +919,8 @@
  15.855  lemma WF_leadsto:
  15.856    assumes 1: "|- N & $P --> $Enabled (<A>_v)"
  15.857      and 2: "|- N & <A>_v --> B"
  15.858 -    and 3: "|- [](N & [~A]_v) --> stable P"
  15.859 -  shows "|- []N & WF(A)_v --> (P ~> B)"
  15.860 +    and 3: "|- \<box>(N & [~A]_v) --> stable P"
  15.861 +  shows "|- \<box>N & WF(A)_v --> (P \<leadsto> B)"
  15.862    apply (unfold leadsto_def)
  15.863    apply (clarsimp dest!: BoxWFI [temp_use])
  15.864    apply (erule (1) STL4Edup)
  15.865 @@ -943,10 +939,10 @@
  15.866    done
  15.867  
  15.868  lemma SF1:
  15.869 -  "[| |- $P & N  --> P` | Q`;    
  15.870 -      |- ($P & N) & <A>_v --> Q`;    
  15.871 -      |- []P & []N & []F --> <>Enabled(<A>_v) |]    
  15.872 -  ==> |- []N & SF(A)_v & []F --> (P ~> Q)"
  15.873 +  "[| |- $P & N  --> P` | Q`;
  15.874 +      |- ($P & N) & <A>_v --> Q`;
  15.875 +      |- \<box>P & \<box>N & \<box>F --> \<diamond>Enabled(<A>_v) |]
  15.876 +  ==> |- \<box>N & SF(A)_v & \<box>F --> (P \<leadsto> Q)"
  15.877    apply (clarsimp dest!: BoxSFI [temp_use])
  15.878    apply (erule (2) ensures [temp_use])
  15.879    apply (erule_tac F = F in dup_boxE)
  15.880 @@ -964,8 +960,8 @@
  15.881    assumes 1: "|- N & <B>_f --> <M>_g"
  15.882      and 2: "|- $P & P` & <N & A>_f --> B"
  15.883      and 3: "|- P & Enabled(<M>_g) --> Enabled(<A>_f)"
  15.884 -    and 4: "|- [](N & [~B]_f) & WF(A)_f & []F & <>[]Enabled(<M>_g) --> <>[]P"
  15.885 -  shows "|- []N & WF(A)_f & []F --> WF(M)_g"
  15.886 +    and 4: "|- \<box>(N & [~B]_f) & WF(A)_f & \<box>F & \<diamond>\<box>Enabled(<M>_g) --> \<diamond>\<box>P"
  15.887 +  shows "|- \<box>N & WF(A)_f & \<box>F --> WF(M)_g"
  15.888    apply (clarsimp dest!: BoxWFI [temp_use] BoxDmdBox [temp_use, THEN iffD2]
  15.889      simp: WF_def [where A = M])
  15.890    apply (erule_tac F = F in dup_boxE)
  15.891 @@ -974,7 +970,7 @@
  15.892     apply assumption
  15.893    apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]])
  15.894    apply (rule classical)
  15.895 -  apply (subgoal_tac "sigmaa |= <> (($P & P` & N) & <A>_f)")
  15.896 +  apply (subgoal_tac "sigmaa |= \<diamond> (($P & P` & N) & <A>_f)")
  15.897     apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use])
  15.898    apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use])
  15.899    apply (simp add: NotDmd [temp_use] not_angle [try_rewrite])
  15.900 @@ -983,8 +979,8 @@
  15.901       apply assumption+
  15.902    apply (drule STL6 [temp_use])
  15.903     apply assumption
  15.904 -  apply (erule_tac V = "sigmaa |= <>[]P" in thin_rl)
  15.905 -  apply (erule_tac V = "sigmaa |= []F" in thin_rl)
  15.906 +  apply (erule_tac V = "sigmaa |= \<diamond>\<box>P" in thin_rl)
  15.907 +  apply (erule_tac V = "sigmaa |= \<box>F" in thin_rl)
  15.908    apply (drule BoxWFI [temp_use])
  15.909    apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE)
  15.910    apply merge_temp_box
  15.911 @@ -1002,26 +998,26 @@
  15.912    assumes 1: "|- N & <B>_f --> <M>_g"
  15.913      and 2: "|- $P & P` & <N & A>_f --> B"
  15.914      and 3: "|- P & Enabled(<M>_g) --> Enabled(<A>_f)"
  15.915 -    and 4: "|- [](N & [~B]_f) & SF(A)_f & []F & []<>Enabled(<M>_g) --> <>[]P"
  15.916 -  shows "|- []N & SF(A)_f & []F --> SF(M)_g"
  15.917 +    and 4: "|- \<box>(N & [~B]_f) & SF(A)_f & \<box>F & \<box>\<diamond>Enabled(<M>_g) --> \<diamond>\<box>P"
  15.918 +  shows "|- \<box>N & SF(A)_f & \<box>F --> SF(M)_g"
  15.919    apply (clarsimp dest!: BoxSFI [temp_use] simp: 2 [try_rewrite] SF_def [where A = M])
  15.920    apply (erule_tac F = F in dup_boxE)
  15.921 -  apply (erule_tac F = "TEMP <>Enabled (<M>_g) " in dup_boxE)
  15.922 +  apply (erule_tac F = "TEMP \<diamond>Enabled (<M>_g) " in dup_boxE)
  15.923    apply merge_temp_box
  15.924    apply (erule STL4Edup)
  15.925     apply assumption
  15.926    apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]])
  15.927    apply (rule classical)
  15.928 -  apply (subgoal_tac "sigmaa |= <> (($P & P` & N) & <A>_f)")
  15.929 +  apply (subgoal_tac "sigmaa |= \<diamond> (($P & P` & N) & <A>_f)")
  15.930     apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use])
  15.931    apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use])
  15.932    apply (simp add: NotDmd [temp_use] not_angle [try_rewrite])
  15.933    apply merge_act_box
  15.934    apply (frule 4 [temp_use])
  15.935       apply assumption+
  15.936 -  apply (erule_tac V = "sigmaa |= []F" in thin_rl)
  15.937 +  apply (erule_tac V = "sigmaa |= \<box>F" in thin_rl)
  15.938    apply (drule BoxSFI [temp_use])
  15.939 -  apply (erule_tac F = "TEMP <>Enabled (<M>_g)" in dup_boxE)
  15.940 +  apply (erule_tac F = "TEMP \<diamond>Enabled (<M>_g)" in dup_boxE)
  15.941    apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE)
  15.942    apply merge_temp_box
  15.943    apply (erule DmdImpldup)
  15.944 @@ -1041,8 +1037,8 @@
  15.945  
  15.946  lemma wf_leadsto:
  15.947    assumes 1: "wf r"
  15.948 -    and 2: "!!x. sigma |= F x ~> (G | (EX y. #((y,x):r) & F y))    "
  15.949 -  shows "sigma |= F x ~> G"
  15.950 +    and 2: "\<And>x. sigma |= F x \<leadsto> (G | (\<exists>y. #((y,x):r) & F y))    "
  15.951 +  shows "sigma |= F x \<leadsto> G"
  15.952    apply (rule 1 [THEN wf_induct])
  15.953    apply (rule LatticeTriangle [temp_use])
  15.954     apply (rule 2)
  15.955 @@ -1053,10 +1049,10 @@
  15.956    done
  15.957  
  15.958  (* If r is well-founded, state function v cannot decrease forever *)
  15.959 -lemma wf_not_box_decrease: "!!r. wf r ==> |- [][ (v`, $v) : #r ]_v --> <>[][#False]_v"
  15.960 +lemma wf_not_box_decrease: "\<And>r. wf r ==> |- \<box>[ (v`, $v) : #r ]_v --> \<diamond>\<box>[#False]_v"
  15.961    apply clarsimp
  15.962    apply (rule ccontr)
  15.963 -  apply (subgoal_tac "sigma |= (EX x. v=#x) ~> #False")
  15.964 +  apply (subgoal_tac "sigma |= (\<exists>x. v=#x) \<leadsto> #False")
  15.965     apply (drule leadsto_false [temp_use, THEN iffD1, THEN STL2_gen [temp_use]])
  15.966     apply (force simp: Init_defs)
  15.967    apply (clarsimp simp: leadsto_exists [try_rewrite] not_square [try_rewrite] more_temp_simps)
  15.968 @@ -1065,7 +1061,7 @@
  15.969     apply (auto simp: square_def angle_def)
  15.970    done
  15.971  
  15.972 -(* "wf r  ==>  |- <>[][ (v`, $v) : #r ]_v --> <>[][#False]_v" *)
  15.973 +(* "wf r  ==>  |- \<diamond>\<box>[ (v`, $v) : #r ]_v --> \<diamond>\<box>[#False]_v" *)
  15.974  lemmas wf_not_dmd_box_decrease =
  15.975    wf_not_box_decrease [THEN DmdImpl, unfolded more_temp_simps]
  15.976  
  15.977 @@ -1074,14 +1070,14 @@
  15.978  *)
  15.979  lemma wf_box_dmd_decrease:
  15.980    assumes 1: "wf r"
  15.981 -  shows "|- []<>((v`, $v) : #r) --> []<><(v`, $v) ~: #r>_v"
  15.982 +  shows "|- \<box>\<diamond>((v`, $v) : #r) --> \<box>\<diamond><(v`, $v) \<notin> #r>_v"
  15.983    apply clarsimp
  15.984    apply (rule ccontr)
  15.985    apply (simp add: not_angle [try_rewrite] more_temp_simps)
  15.986    apply (drule 1 [THEN wf_not_dmd_box_decrease [temp_use]])
  15.987    apply (drule BoxDmdDmdBox [temp_use])
  15.988     apply assumption
  15.989 -  apply (subgoal_tac "sigma |= []<> ((#False) ::action)")
  15.990 +  apply (subgoal_tac "sigma |= \<box>\<diamond> ((#False) ::action)")
  15.991     apply force
  15.992    apply (erule STL4E)
  15.993    apply (rule DmdImpl)
  15.994 @@ -1091,9 +1087,9 @@
  15.995  (* In particular, for natural numbers, if n decreases infinitely often
  15.996     then it has to increase infinitely often.
  15.997  *)
  15.998 -lemma nat_box_dmd_decrease: "!!n::nat stfun. |- []<>(n` < $n) --> []<>($n < n`)"
  15.999 +lemma nat_box_dmd_decrease: "\<And>n::nat stfun. |- \<box>\<diamond>(n` < $n) --> \<box>\<diamond>($n < n`)"
 15.1000    apply clarsimp
 15.1001 -  apply (subgoal_tac "sigma |= []<><~ ((n`,$n) : #less_than) >_n")
 15.1002 +  apply (subgoal_tac "sigma |= \<box>\<diamond><~ ((n`,$n) : #less_than) >_n")
 15.1003     apply (erule thin_rl)
 15.1004     apply (erule STL4E)
 15.1005     apply (rule DmdImpl)
 15.1006 @@ -1110,11 +1106,11 @@
 15.1007  
 15.1008  lemma aallI:
 15.1009    assumes 1: "basevars vs"
 15.1010 -    and 2: "(!!x. basevars (x,vs) ==> sigma |= F x)"
 15.1011 -  shows "sigma |= (AALL x. F x)"
 15.1012 +    and 2: "(\<And>x. basevars (x,vs) ==> sigma |= F x)"
 15.1013 +  shows "sigma |= (\<forall>\<forall>x. F x)"
 15.1014    by (auto simp: aall_def elim!: eexE [temp_use] intro!: 1 dest!: 2 [temp_use])
 15.1015  
 15.1016 -lemma aallE: "|- (AALL x. F x) --> F x"
 15.1017 +lemma aallE: "|- (\<forall>\<forall>x. F x) --> F x"
 15.1018    apply (unfold aall_def)
 15.1019    apply clarsimp
 15.1020    apply (erule contrapos_np)
 15.1021 @@ -1123,18 +1119,18 @@
 15.1022  
 15.1023  (* monotonicity of quantification *)
 15.1024  lemma eex_mono:
 15.1025 -  assumes 1: "sigma |= EEX x. F x"
 15.1026 -    and 2: "!!x. sigma |= F x --> G x"
 15.1027 -  shows "sigma |= EEX x. G x"
 15.1028 +  assumes 1: "sigma |= \<exists>\<exists>x. F x"
 15.1029 +    and 2: "\<And>x. sigma |= F x --> G x"
 15.1030 +  shows "sigma |= \<exists>\<exists>x. G x"
 15.1031    apply (rule unit_base [THEN 1 [THEN eexE]])
 15.1032    apply (rule eexI [temp_use])
 15.1033    apply (erule 2 [unfolded intensional_rews, THEN mp])
 15.1034    done
 15.1035  
 15.1036  lemma aall_mono:
 15.1037 -  assumes 1: "sigma |= AALL x. F(x)"
 15.1038 -    and 2: "!!x. sigma |= F(x) --> G(x)"
 15.1039 -  shows "sigma |= AALL x. G(x)"
 15.1040 +  assumes 1: "sigma |= \<forall>\<forall>x. F(x)"
 15.1041 +    and 2: "\<And>x. sigma |= F(x) --> G(x)"
 15.1042 +  shows "sigma |= \<forall>\<forall>x. G(x)"
 15.1043    apply (rule unit_base [THEN aallI])
 15.1044    apply (rule 2 [unfolded intensional_rews, THEN mp])
 15.1045    apply (rule 1 [THEN aallE [temp_use]])
 15.1046 @@ -1143,11 +1139,11 @@
 15.1047  (* Derived history introduction rule *)
 15.1048  lemma historyI:
 15.1049    assumes 1: "sigma |= Init I"
 15.1050 -    and 2: "sigma |= []N"
 15.1051 +    and 2: "sigma |= \<box>N"
 15.1052      and 3: "basevars vs"
 15.1053 -    and 4: "!!h. basevars(h,vs) ==> |- I & h = ha --> HI h"
 15.1054 -    and 5: "!!h s t. [| basevars(h,vs); N (s,t); h t = hb (h s) (s,t) |] ==> HN h (s,t)"
 15.1055 -  shows "sigma |= EEX h. Init (HI h) & [](HN h)"
 15.1056 +    and 4: "\<And>h. basevars(h,vs) ==> |- I & h = ha --> HI h"
 15.1057 +    and 5: "\<And>h s t. [| basevars(h,vs); N (s,t); h t = hb (h s) (s,t) |] ==> HN h (s,t)"
 15.1058 +  shows "sigma |= \<exists>\<exists>h. Init (HI h) & \<box>(HN h)"
 15.1059    apply (rule history [temp_use, THEN eexE])
 15.1060    apply (rule 3)
 15.1061    apply (rule eexI [temp_use])
 15.1062 @@ -1165,7 +1161,7 @@
 15.1063     example of a history variable: existence of a clock
 15.1064  *)
 15.1065  
 15.1066 -lemma "|- EEX h. Init(h = #True) & [](h` = (~$h))"
 15.1067 +lemma "|- \<exists>\<exists>h. Init(h = #True) & \<box>(h` = (~$h))"
 15.1068    apply (rule tempI)
 15.1069    apply (rule historyI)
 15.1070    apply (force simp: Init_defs intro!: unit_base [temp_use] necT [temp_use])+