src/HOL/TLA/Buffer/DBuffer.thy

   DBPass_def:     "DBPass   == ACT  Deq inp q1 mid
                                  & (q2$ = $q2 @ [ mid$ ])
                                  & (out$ = $out)" and
   DBNext_def:     "DBNext   == ACT  (DBEnq | DBDeq | DBPass)" and
   DBuffer_def:    "DBuffer  == TEMP Init DBInit
-                                 & [][DBNext]_(inp,mid,out,q1,q2)
+                                 & \<box>[DBNext]_(inp,mid,out,q1,q2)
                                  & WF(DBDeq)_(inp,mid,out,q1,q2)
                                  & WF(DBPass)_(inp,mid,out,q1,q2)"
 
 
 declare qc_def [simp]

   apply (unfold angle_def DBDeq_def Deq_def)
   apply (safe, simp (asm_lr))+
   done
 
 lemma DBDeq_enabled: 
-    "|- Enabled (<DBDeq>_(inp,mid,out,q1,q2)) = (q2 ~= #[])"
+    "|- Enabled (<DBDeq>_(inp,mid,out,q1,q2)) = (q2 \<noteq> #[])"
   apply (unfold DBDeq_visible [action_rewrite])
   apply (force intro!: DB_base [THEN base_enabled, temp_use]
     elim!: enabledE simp: angle_def DBDeq_def Deq_def)
   done
 
 lemma DBPass_visible: "|- <DBPass>_(inp,mid,out,q1,q2) = DBPass"
   by (auto simp: angle_def DBPass_def Deq_def)
 
 lemma DBPass_enabled: 
-    "|- Enabled (<DBPass>_(inp,mid,out,q1,q2)) = (q1 ~= #[])"
+    "|- Enabled (<DBPass>_(inp,mid,out,q1,q2)) = (q1 \<noteq> #[])"
   apply (unfold DBPass_visible [action_rewrite])
   apply (force intro!: DB_base [THEN base_enabled, temp_use]
     elim!: enabledE simp: angle_def DBPass_def Deq_def)
   done
 
 
 (* The plan for proving weak fairness at the higher level is to prove
-   (0)  DBuffer => (Enabled (Deq inp qc out) ~> (Deq inp qc out))
+   (0)  DBuffer => (Enabled (Deq inp qc out) \<leadsto> (Deq inp qc out))
    which is in turn reduced to the two leadsto conditions
-   (1)  DBuffer => (Enabled (Deq inp qc out) ~> q2 ~= [])
-   (2)  DBuffer => (q2 ~= [] ~> DBDeq)
+   (1)  DBuffer => (Enabled (Deq inp qc out) \<leadsto> q2 \<noteq> [])
+   (2)  DBuffer => (q2 \<noteq> [] \<leadsto> DBDeq)
    and the fact that DBDeq implies <Deq inp qc out>_(inp,qc,out)
-   (and therefore DBDeq ~> <Deq inp qc out>_(inp,qc,out) trivially holds).
+   (and therefore DBDeq \<leadsto> <Deq inp qc out>_(inp,qc,out) trivially holds).
 
    Condition (1) is reduced to
-   (1a) DBuffer => (qc ~= [] /\ q2 = [] ~> q2 ~= [])
+   (1a) DBuffer => (qc \<noteq> [] /\ q2 = [] \<leadsto> q2 \<noteq> [])
    by standard leadsto rules (leadsto_classical) and rule Deq_enabledE.
 
    Both (1a) and (2) are proved from DBuffer's WF conditions by standard
    WF reasoning (Lamport's WF1 and WF_leadsto).
    The condition WF(Deq inp qc out) follows from (0) by rule leadsto_WF.
 
    One could use Lamport's WF2 instead.
 *)
 
 (* Condition (1a) *)
-lemma DBFair_1a: "|- [][DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)  
-         --> (qc ~= #[] & q2 = #[] ~> q2 ~= #[])"
+lemma DBFair_1a: "|- \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)  
+         --> (qc \<noteq> #[] & q2 = #[] \<leadsto> q2 \<noteq> #[])"
   apply (rule WF1)
     apply (force simp: db_defs)
    apply (force simp: angle_def DBPass_def)
   apply (force simp: DBPass_enabled [temp_use])
   done
 
 (* Condition (1) *)
-lemma DBFair_1: "|- [][DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)  
-         --> (Enabled (<Deq inp qc out>_(inp,qc,out)) ~> q2 ~= #[])"
+lemma DBFair_1: "|- \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)  
+         --> (Enabled (<Deq inp qc out>_(inp,qc,out)) \<leadsto> q2 \<noteq> #[])"
   apply clarsimp
   apply (rule leadsto_classical [temp_use])
   apply (rule DBFair_1a [temp_use, THEN LatticeTransitivity [temp_use]])
   apply assumption+
   apply (rule ImplLeadsto_gen [temp_use])
   apply (force intro!: necT [temp_use] dest!: STL2_gen [temp_use] Deq_enabledE [temp_use]
     simp add: Init_defs)
   done
 
 (* Condition (2) *)
-lemma DBFair_2: "|- [][DBNext]_(inp,mid,out,q1,q2) & WF(DBDeq)_(inp,mid,out,q1,q2)  
-         --> (q2 ~= #[] ~> DBDeq)"
+lemma DBFair_2: "|- \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBDeq)_(inp,mid,out,q1,q2)  
+         --> (q2 \<noteq> #[] \<leadsto> DBDeq)"
   apply (rule WF_leadsto)
     apply (force simp: DBDeq_enabled [temp_use])
    apply (force simp: angle_def)
   apply (force simp: db_defs elim!: Stable [temp_use])
   done
 
 (* High-level fairness *)
-lemma DBFair: "|- [][DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)  
+lemma DBFair: "|- \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)  
                                         & WF(DBDeq)_(inp,mid,out,q1,q2)   
          --> WF(Deq inp qc out)_(inp,qc,out)"
   apply (auto simp del: qc_def intro!: leadsto_WF [temp_use]
     DBFair_1 [temp_use, THEN [2] LatticeTransitivity [temp_use]]
     DBFair_2 [temp_use, THEN [2] LatticeTransitivity [temp_use]])