src/HOL/TLA/Buffer/DBuffer.thy

--- a/src/HOL/TLA/Buffer/DBuffer.thy	Fri Jun 26 11:44:22 2015 +0200
+++ b/src/HOL/TLA/Buffer/DBuffer.thy	Fri Jun 26 14:53:15 2015 +0200
@@ -50,12 +50,12 @@
 
 
 (*** Proper initialization ***)
-lemma DBInit: "|- Init DBInit --> Init (BInit inp qc out)"
+lemma DBInit: "\<turnstile> Init DBInit \<longrightarrow> Init (BInit inp qc out)"
   by (auto simp: Init_def DBInit_def BInit_def)
 
 
 (*** Step simulation ***)
-lemma DB_step_simulation: "|- [DBNext]_(inp,mid,out,q1,q2) --> [Next inp qc out]_(inp,qc,out)"
+lemma DB_step_simulation: "\<turnstile> [DBNext]_(inp,mid,out,q1,q2) \<longrightarrow> [Next inp qc out]_(inp,qc,out)"
   apply (rule square_simulation)
    apply clarsimp
   apply (tactic
@@ -66,23 +66,23 @@
 (*** Simulation of fairness ***)
 
 (* Compute enabledness predicates for DBDeq and DBPass actions *)
-lemma DBDeq_visible: "|- <DBDeq>_(inp,mid,out,q1,q2) = DBDeq"
+lemma DBDeq_visible: "\<turnstile> <DBDeq>_(inp,mid,out,q1,q2) = DBDeq"
   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 \<noteq> #[])"
+    "\<turnstile> 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"
+lemma DBPass_visible: "\<turnstile> <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 \<noteq> #[])"
+    "\<turnstile> 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)
@@ -109,8 +109,8 @@
 *)
 
 (* Condition (1a) *)
-lemma DBFair_1a: "|- \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)  
-         --> (qc \<noteq> #[] & q2 = #[] \<leadsto> q2 \<noteq> #[])"
+lemma DBFair_1a: "\<turnstile> \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)  
+         \<longrightarrow> (qc \<noteq> #[] & q2 = #[] \<leadsto> q2 \<noteq> #[])"
   apply (rule WF1)
     apply (force simp: db_defs)
    apply (force simp: angle_def DBPass_def)
@@ -118,8 +118,8 @@
   done
 
 (* Condition (1) *)
-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> #[])"
+lemma DBFair_1: "\<turnstile> \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)  
+         \<longrightarrow> (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]])
@@ -130,8 +130,8 @@
   done
 
 (* Condition (2) *)
-lemma DBFair_2: "|- \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBDeq)_(inp,mid,out,q1,q2)  
-         --> (q2 \<noteq> #[] \<leadsto> DBDeq)"
+lemma DBFair_2: "\<turnstile> \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBDeq)_(inp,mid,out,q1,q2)  
+         \<longrightarrow> (q2 \<noteq> #[] \<leadsto> DBDeq)"
   apply (rule WF_leadsto)
     apply (force simp: DBDeq_enabled [temp_use])
    apply (force simp: angle_def)
@@ -139,9 +139,9 @@
   done
 
 (* High-level fairness *)
-lemma DBFair: "|- \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)  
+lemma DBFair: "\<turnstile> \<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)"
+         \<longrightarrow> 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]])
@@ -150,7 +150,7 @@
   done
 
 (*** Main theorem ***)
-lemma DBuffer_impl_Buffer: "|- DBuffer --> Buffer inp out"
+lemma DBuffer_impl_Buffer: "\<turnstile> DBuffer \<longrightarrow> Buffer inp out"
   apply (unfold DBuffer_def Buffer_def IBuffer_def)
   apply (force intro!: eexI [temp_use] DBInit [temp_use]
     DB_step_simulation [THEN STL4, temp_use] DBFair [temp_use])