
diff -r 07593a0a27f4 -r effd8fcabca2 src/HOL/Hoare_Parallel/OG_Examples.thy
--- a/src/HOL/Hoare_Parallel/OG_Examples.thy	Tue Aug 27 23:54:23 2013 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Examples.thy	Wed Aug 28 00:18:50 2013 +0200
@@ -16,30 +16,30 @@
  hold :: nat
 
 lemma Petersons_mutex_1: 
-  "\<parallel>- .{\<acute>pr1=0 \<and> \<not>\<acute>in1 \<and> \<acute>pr2=0 \<and> \<not>\<acute>in2 }.  
-  COBEGIN .{\<acute>pr1=0 \<and> \<not>\<acute>in1}.  
-  WHILE True INV .{\<acute>pr1=0 \<and> \<not>\<acute>in1}.  
+  "\<parallel>- \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1 \<and> \<acute>pr2=0 \<and> \<not>\<acute>in2 \<rbrace>  
+  COBEGIN \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1\<rbrace>  
+  WHILE True INV \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1\<rbrace>  
   DO  
-  .{\<acute>pr1=0 \<and> \<not>\<acute>in1}. \<langle> \<acute>in1:=True,,\<acute>pr1:=1 \<rangle>;;  
-  .{\<acute>pr1=1 \<and> \<acute>in1}.  \<langle> \<acute>hold:=1,,\<acute>pr1:=2 \<rangle>;;  
-  .{\<acute>pr1=2 \<and> \<acute>in1 \<and> (\<acute>hold=1 \<or> \<acute>hold=2 \<and> \<acute>pr2=2)}.  
+  \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1\<rbrace> \<langle> \<acute>in1:=True,,\<acute>pr1:=1 \<rangle>;;  
+  \<lbrace>\<acute>pr1=1 \<and> \<acute>in1\<rbrace>  \<langle> \<acute>hold:=1,,\<acute>pr1:=2 \<rangle>;;  
+  \<lbrace>\<acute>pr1=2 \<and> \<acute>in1 \<and> (\<acute>hold=1 \<or> \<acute>hold=2 \<and> \<acute>pr2=2)\<rbrace>  
   AWAIT (\<not>\<acute>in2 \<or> \<not>(\<acute>hold=1)) THEN \<acute>pr1:=3 END;;    
-  .{\<acute>pr1=3 \<and> \<acute>in1 \<and> (\<acute>hold=1 \<or> \<acute>hold=2 \<and> \<acute>pr2=2)}. 
+  \<lbrace>\<acute>pr1=3 \<and> \<acute>in1 \<and> (\<acute>hold=1 \<or> \<acute>hold=2 \<and> \<acute>pr2=2)\<rbrace> 
    \<langle>\<acute>in1:=False,,\<acute>pr1:=0\<rangle> 
-  OD .{\<acute>pr1=0 \<and> \<not>\<acute>in1}.  
+  OD \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1\<rbrace>  
   \<parallel>  
-  .{\<acute>pr2=0 \<and> \<not>\<acute>in2}.  
-  WHILE True INV .{\<acute>pr2=0 \<and> \<not>\<acute>in2}.  
+  \<lbrace>\<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace>  
+  WHILE True INV \<lbrace>\<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace>  
   DO  
-  .{\<acute>pr2=0 \<and> \<not>\<acute>in2}. \<langle> \<acute>in2:=True,,\<acute>pr2:=1 \<rangle>;;  
-  .{\<acute>pr2=1 \<and> \<acute>in2}. \<langle>  \<acute>hold:=2,,\<acute>pr2:=2 \<rangle>;;  
-  .{\<acute>pr2=2 \<and> \<acute>in2 \<and> (\<acute>hold=2 \<or> (\<acute>hold=1 \<and> \<acute>pr1=2))}.  
+  \<lbrace>\<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace> \<langle> \<acute>in2:=True,,\<acute>pr2:=1 \<rangle>;;  
+  \<lbrace>\<acute>pr2=1 \<and> \<acute>in2\<rbrace> \<langle>  \<acute>hold:=2,,\<acute>pr2:=2 \<rangle>;;  
+  \<lbrace>\<acute>pr2=2 \<and> \<acute>in2 \<and> (\<acute>hold=2 \<or> (\<acute>hold=1 \<and> \<acute>pr1=2))\<rbrace>  
   AWAIT (\<not>\<acute>in1 \<or> \<not>(\<acute>hold=2)) THEN \<acute>pr2:=3  END;;    
-  .{\<acute>pr2=3 \<and> \<acute>in2 \<and> (\<acute>hold=2 \<or> (\<acute>hold=1 \<and> \<acute>pr1=2))}. 
+  \<lbrace>\<acute>pr2=3 \<and> \<acute>in2 \<and> (\<acute>hold=2 \<or> (\<acute>hold=1 \<and> \<acute>pr1=2))\<rbrace> 
     \<langle>\<acute>in2:=False,,\<acute>pr2:=0\<rangle> 
-  OD .{\<acute>pr2=0 \<and> \<not>\<acute>in2}.  
+  OD \<lbrace>\<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace>  
   COEND  
-  .{\<acute>pr1=0 \<and> \<not>\<acute>in1 \<and> \<acute>pr2=0 \<and> \<not>\<acute>in2}."
+  \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1 \<and> \<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace>"
 apply oghoare
 --{* 104 verification conditions. *}
 apply auto
@@ -57,37 +57,37 @@
  after2 :: bool
 
 lemma Busy_wait_mutex: 
- "\<parallel>-  .{True}.  
+ "\<parallel>-  \<lbrace>True\<rbrace>  
   \<acute>flag1:=False,, \<acute>flag2:=False,,  
-  COBEGIN .{\<not>\<acute>flag1}.  
+  COBEGIN \<lbrace>\<not>\<acute>flag1\<rbrace>  
         WHILE True  
-        INV .{\<not>\<acute>flag1}.  
-        DO .{\<not>\<acute>flag1}. \<langle> \<acute>flag1:=True,,\<acute>after1:=False \<rangle>;;  
-           .{\<acute>flag1 \<and> \<not>\<acute>after1}. \<langle> \<acute>turn:=1,,\<acute>after1:=True \<rangle>;;  
-           .{\<acute>flag1 \<and> \<acute>after1 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)}.  
+        INV \<lbrace>\<not>\<acute>flag1\<rbrace>  
+        DO \<lbrace>\<not>\<acute>flag1\<rbrace> \<langle> \<acute>flag1:=True,,\<acute>after1:=False \<rangle>;;  
+           \<lbrace>\<acute>flag1 \<and> \<not>\<acute>after1\<rbrace> \<langle> \<acute>turn:=1,,\<acute>after1:=True \<rangle>;;  
+           \<lbrace>\<acute>flag1 \<and> \<acute>after1 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)\<rbrace>  
             WHILE \<not>(\<acute>flag2 \<longrightarrow> \<acute>turn=2)  
-            INV .{\<acute>flag1 \<and> \<acute>after1 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)}.  
-            DO .{\<acute>flag1 \<and> \<acute>after1 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)}. SKIP OD;; 
-           .{\<acute>flag1 \<and> \<acute>after1 \<and> (\<acute>flag2 \<and> \<acute>after2 \<longrightarrow> \<acute>turn=2)}.
+            INV \<lbrace>\<acute>flag1 \<and> \<acute>after1 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)\<rbrace>  
+            DO \<lbrace>\<acute>flag1 \<and> \<acute>after1 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)\<rbrace> SKIP OD;; 
+           \<lbrace>\<acute>flag1 \<and> \<acute>after1 \<and> (\<acute>flag2 \<and> \<acute>after2 \<longrightarrow> \<acute>turn=2)\<rbrace>
             \<acute>flag1:=False  
         OD  
-       .{False}.  
+       \<lbrace>False\<rbrace>  
   \<parallel>  
-     .{\<not>\<acute>flag2}.  
+     \<lbrace>\<not>\<acute>flag2\<rbrace>  
         WHILE True  
-        INV .{\<not>\<acute>flag2}.  
-        DO .{\<not>\<acute>flag2}. \<langle> \<acute>flag2:=True,,\<acute>after2:=False \<rangle>;;  
-           .{\<acute>flag2 \<and> \<not>\<acute>after2}. \<langle> \<acute>turn:=2,,\<acute>after2:=True \<rangle>;;  
-           .{\<acute>flag2 \<and> \<acute>after2 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)}.  
+        INV \<lbrace>\<not>\<acute>flag2\<rbrace>  
+        DO \<lbrace>\<not>\<acute>flag2\<rbrace> \<langle> \<acute>flag2:=True,,\<acute>after2:=False \<rangle>;;  
+           \<lbrace>\<acute>flag2 \<and> \<not>\<acute>after2\<rbrace> \<langle> \<acute>turn:=2,,\<acute>after2:=True \<rangle>;;  
+           \<lbrace>\<acute>flag2 \<and> \<acute>after2 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)\<rbrace>  
             WHILE \<not>(\<acute>flag1 \<longrightarrow> \<acute>turn=1)  
-            INV .{\<acute>flag2 \<and> \<acute>after2 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)}.  
-            DO .{\<acute>flag2 \<and> \<acute>after2 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)}. SKIP OD;;  
-           .{\<acute>flag2 \<and> \<acute>after2 \<and> (\<acute>flag1 \<and> \<acute>after1 \<longrightarrow> \<acute>turn=1)}. 
+            INV \<lbrace>\<acute>flag2 \<and> \<acute>after2 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)\<rbrace>  
+            DO \<lbrace>\<acute>flag2 \<and> \<acute>after2 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)\<rbrace> SKIP OD;;  
+           \<lbrace>\<acute>flag2 \<and> \<acute>after2 \<and> (\<acute>flag1 \<and> \<acute>after1 \<longrightarrow> \<acute>turn=1)\<rbrace> 
             \<acute>flag2:=False  
         OD  
-       .{False}.  
+       \<lbrace>False\<rbrace>  
   COEND  
-  .{False}."
+  \<lbrace>False\<rbrace>"
 apply oghoare
 --{* 122 vc *}
 apply auto
@@ -100,21 +100,21 @@
  who :: nat
 
 lemma Semaphores_mutex: 
- "\<parallel>- .{i\<noteq>j}.  
+ "\<parallel>- \<lbrace>i\<noteq>j\<rbrace>  
   \<acute>out:=True ,,  
-  COBEGIN .{i\<noteq>j}.  
-       WHILE True INV .{i\<noteq>j}.  
-       DO .{i\<noteq>j}. AWAIT \<acute>out THEN  \<acute>out:=False,, \<acute>who:=i END;;  
-          .{\<not>\<acute>out \<and> \<acute>who=i \<and> i\<noteq>j}. \<acute>out:=True OD  
-       .{False}.  
+  COBEGIN \<lbrace>i\<noteq>j\<rbrace>  
+       WHILE True INV \<lbrace>i\<noteq>j\<rbrace>  
+       DO \<lbrace>i\<noteq>j\<rbrace> AWAIT \<acute>out THEN  \<acute>out:=False,, \<acute>who:=i END;;  
+          \<lbrace>\<not>\<acute>out \<and> \<acute>who=i \<and> i\<noteq>j\<rbrace> \<acute>out:=True OD  
+       \<lbrace>False\<rbrace>  
   \<parallel>  
-       .{i\<noteq>j}.  
-       WHILE True INV .{i\<noteq>j}.  
-       DO .{i\<noteq>j}. AWAIT \<acute>out THEN  \<acute>out:=False,,\<acute>who:=j END;;  
-          .{\<not>\<acute>out \<and> \<acute>who=j \<and> i\<noteq>j}. \<acute>out:=True OD  
-       .{False}.  
+       \<lbrace>i\<noteq>j\<rbrace>  
+       WHILE True INV \<lbrace>i\<noteq>j\<rbrace>  
+       DO \<lbrace>i\<noteq>j\<rbrace> AWAIT \<acute>out THEN  \<acute>out:=False,,\<acute>who:=j END;;  
+          \<lbrace>\<not>\<acute>out \<and> \<acute>who=j \<and> i\<noteq>j\<rbrace> \<acute>out:=True OD  
+       \<lbrace>False\<rbrace>  
   COEND  
-  .{False}."
+  \<lbrace>False\<rbrace>"
 apply oghoare
 --{* 38 vc *}
 apply auto
@@ -123,17 +123,17 @@
 subsubsection {* Peterson's Algorithm III: Parameterized version: *}
 
 lemma Semaphores_parameterized_mutex: 
- "0<n \<Longrightarrow> \<parallel>- .{True}.  
+ "0<n \<Longrightarrow> \<parallel>- \<lbrace>True\<rbrace>  
   \<acute>out:=True ,,  
  COBEGIN
   SCHEME [0\<le> i< n]
-    .{True}.  
-     WHILE True INV .{True}.  
-      DO .{True}. AWAIT \<acute>out THEN  \<acute>out:=False,, \<acute>who:=i END;;  
-         .{\<not>\<acute>out \<and> \<acute>who=i}. \<acute>out:=True OD
-    .{False}. 
+    \<lbrace>True\<rbrace>  
+     WHILE True INV \<lbrace>True\<rbrace>  
+      DO \<lbrace>True\<rbrace> AWAIT \<acute>out THEN  \<acute>out:=False,, \<acute>who:=i END;;  
+         \<lbrace>\<not>\<acute>out \<and> \<acute>who=i\<rbrace> \<acute>out:=True OD
+    \<lbrace>False\<rbrace> 
  COEND
-  .{False}." 
+  \<lbrace>False\<rbrace>" 
 apply oghoare
 --{* 20 vc *}
 apply auto
@@ -150,22 +150,22 @@
 lemma Ticket_mutex: 
  "\<lbrakk> 0<n; I=\<guillemotleft>n=length \<acute>turn \<and> 0<\<acute>nextv \<and> (\<forall>k l. k<n \<and> l<n \<and> k\<noteq>l 
     \<longrightarrow> \<acute>turn!k < \<acute>num \<and> (\<acute>turn!k =0 \<or> \<acute>turn!k\<noteq>\<acute>turn!l))\<guillemotright> \<rbrakk>
-   \<Longrightarrow> \<parallel>- .{n=length \<acute>turn}.  
+   \<Longrightarrow> \<parallel>- \<lbrace>n=length \<acute>turn\<rbrace>  
    \<acute>index:= 0,,
-   WHILE \<acute>index < n INV .{n=length \<acute>turn \<and> (\<forall>i<\<acute>index. \<acute>turn!i=0)}. 
+   WHILE \<acute>index < n INV \<lbrace>n=length \<acute>turn \<and> (\<forall>i<\<acute>index. \<acute>turn!i=0)\<rbrace> 
     DO \<acute>turn:= \<acute>turn[\<acute>index:=0],, \<acute>index:=\<acute>index +1 OD,,
   \<acute>num:=1 ,, \<acute>nextv:=1 ,, 
  COBEGIN
   SCHEME [0\<le> i< n]
-    .{\<acute>I}.  
-     WHILE True INV .{\<acute>I}.  
-      DO .{\<acute>I}. \<langle> \<acute>turn :=\<acute>turn[i:=\<acute>num],, \<acute>num:=\<acute>num+1 \<rangle>;;  
-         .{\<acute>I}. WAIT \<acute>turn!i=\<acute>nextv END;;
-         .{\<acute>I \<and> \<acute>turn!i=\<acute>nextv}. \<acute>nextv:=\<acute>nextv+1
+    \<lbrace>\<acute>I\<rbrace>  
+     WHILE True INV \<lbrace>\<acute>I\<rbrace>  
+      DO \<lbrace>\<acute>I\<rbrace> \<langle> \<acute>turn :=\<acute>turn[i:=\<acute>num],, \<acute>num:=\<acute>num+1 \<rangle>;;  
+         \<lbrace>\<acute>I\<rbrace> WAIT \<acute>turn!i=\<acute>nextv END;;
+         \<lbrace>\<acute>I \<and> \<acute>turn!i=\<acute>nextv\<rbrace> \<acute>nextv:=\<acute>nextv+1
       OD
-    .{False}. 
+    \<lbrace>False\<rbrace> 
  COEND
-  .{False}." 
+  \<lbrace>False\<rbrace>" 
 apply oghoare
 --{* 35 vc *}
 apply simp_all
@@ -259,40 +259,40 @@
       \<and> (\<not>\<acute>found \<and> a<\<acute> x \<longrightarrow> f(\<acute>x)\<noteq>0) \<guillemotright> ;  
     I2= \<guillemotleft>\<acute>y\<le>a+1 \<and> (\<acute>found \<longrightarrow> (a<\<acute>x \<and> f(\<acute>x)=0) \<or> (\<acute>y\<le>a \<and> f(\<acute>y)=0)) 
       \<and> (\<not>\<acute>found \<and> \<acute>y\<le>a \<longrightarrow> f(\<acute>y)\<noteq>0) \<guillemotright> \<rbrakk> \<Longrightarrow>  
-  \<parallel>- .{\<exists> u. f(u)=0}.  
+  \<parallel>- \<lbrace>\<exists> u. f(u)=0\<rbrace>  
   \<acute>turn:=1,, \<acute>found:= False,,  
   \<acute>x:=a,, \<acute>y:=a+1 ,,  
-  COBEGIN .{\<acute>I1}.  
+  COBEGIN \<lbrace>\<acute>I1\<rbrace>  
        WHILE \<not>\<acute>found  
-       INV .{\<acute>I1}.  
-       DO .{a\<le>\<acute>x \<and> (\<acute>found \<longrightarrow> \<acute>y\<le>a \<and> f(\<acute>y)=0) \<and> (a<\<acute>x \<longrightarrow> f(\<acute>x)\<noteq>0)}.  
+       INV \<lbrace>\<acute>I1\<rbrace>  
+       DO \<lbrace>a\<le>\<acute>x \<and> (\<acute>found \<longrightarrow> \<acute>y\<le>a \<and> f(\<acute>y)=0) \<and> (a<\<acute>x \<longrightarrow> f(\<acute>x)\<noteq>0)\<rbrace>  
           WAIT \<acute>turn=1 END;;  
-          .{a\<le>\<acute>x \<and> (\<acute>found \<longrightarrow> \<acute>y\<le>a \<and> f(\<acute>y)=0) \<and> (a<\<acute>x \<longrightarrow> f(\<acute>x)\<noteq>0)}.  
+          \<lbrace>a\<le>\<acute>x \<and> (\<acute>found \<longrightarrow> \<acute>y\<le>a \<and> f(\<acute>y)=0) \<and> (a<\<acute>x \<longrightarrow> f(\<acute>x)\<noteq>0)\<rbrace>  
           \<acute>turn:=2;;  
-          .{a\<le>\<acute>x \<and> (\<acute>found \<longrightarrow> \<acute>y\<le>a \<and> f(\<acute>y)=0) \<and> (a<\<acute>x \<longrightarrow> f(\<acute>x)\<noteq>0)}.    
+          \<lbrace>a\<le>\<acute>x \<and> (\<acute>found \<longrightarrow> \<acute>y\<le>a \<and> f(\<acute>y)=0) \<and> (a<\<acute>x \<longrightarrow> f(\<acute>x)\<noteq>0)\<rbrace>    
           \<langle> \<acute>x:=\<acute>x+1,,  
             IF f(\<acute>x)=0 THEN \<acute>found:=True ELSE SKIP FI\<rangle>  
        OD;;  
-       .{\<acute>I1  \<and> \<acute>found}.  
+       \<lbrace>\<acute>I1  \<and> \<acute>found\<rbrace>  
        \<acute>turn:=2  
-       .{\<acute>I1 \<and> \<acute>found}.  
+       \<lbrace>\<acute>I1 \<and> \<acute>found\<rbrace>  
   \<parallel>  
-      .{\<acute>I2}.  
+      \<lbrace>\<acute>I2\<rbrace>  
        WHILE \<not>\<acute>found  
-       INV .{\<acute>I2}.  
-       DO .{\<acute>y\<le>a+1 \<and> (\<acute>found \<longrightarrow> a<\<acute>x \<and> f(\<acute>x)=0) \<and> (\<acute>y\<le>a \<longrightarrow> f(\<acute>y)\<noteq>0)}.  
+       INV \<lbrace>\<acute>I2\<rbrace>  
+       DO \<lbrace>\<acute>y\<le>a+1 \<and> (\<acute>found \<longrightarrow> a<\<acute>x \<and> f(\<acute>x)=0) \<and> (\<acute>y\<le>a \<longrightarrow> f(\<acute>y)\<noteq>0)\<rbrace>  
           WAIT \<acute>turn=2 END;;  
-          .{\<acute>y\<le>a+1 \<and> (\<acute>found \<longrightarrow> a<\<acute>x \<and> f(\<acute>x)=0) \<and> (\<acute>y\<le>a \<longrightarrow> f(\<acute>y)\<noteq>0)}.  
+          \<lbrace>\<acute>y\<le>a+1 \<and> (\<acute>found \<longrightarrow> a<\<acute>x \<and> f(\<acute>x)=0) \<and> (\<acute>y\<le>a \<longrightarrow> f(\<acute>y)\<noteq>0)\<rbrace>  
           \<acute>turn:=1;;  
-          .{\<acute>y\<le>a+1 \<and> (\<acute>found \<longrightarrow> a<\<acute>x \<and> f(\<acute>x)=0) \<and> (\<acute>y\<le>a \<longrightarrow> f(\<acute>y)\<noteq>0)}.  
+          \<lbrace>\<acute>y\<le>a+1 \<and> (\<acute>found \<longrightarrow> a<\<acute>x \<and> f(\<acute>x)=0) \<and> (\<acute>y\<le>a \<longrightarrow> f(\<acute>y)\<noteq>0)\<rbrace>  
           \<langle> \<acute>y:=(\<acute>y - 1),,  
             IF f(\<acute>y)=0 THEN \<acute>found:=True ELSE SKIP FI\<rangle>  
        OD;;  
-       .{\<acute>I2 \<and> \<acute>found}.  
+       \<lbrace>\<acute>I2 \<and> \<acute>found\<rbrace>  
        \<acute>turn:=1  
-       .{\<acute>I2 \<and> \<acute>found}.  
+       \<lbrace>\<acute>I2 \<and> \<acute>found\<rbrace>  
   COEND  
-  .{f(\<acute>x)=0 \<or> f(\<acute>y)=0}."
+  \<lbrace>f(\<acute>x)=0 \<or> f(\<acute>y)=0\<rbrace>"
 apply oghoare
 --{* 98 verification conditions *}
 apply auto 
@@ -306,26 +306,26 @@
     \<and> (\<not>\<acute>found \<and> a<\<acute>x \<longrightarrow> f(\<acute>x)\<noteq>0)\<guillemotright>;  
  I2= \<guillemotleft>\<acute>y\<le>a+1 \<and> (\<acute>found \<longrightarrow> (a<\<acute>x \<and> f(\<acute>x)=0) \<or> (\<acute>y\<le>a \<and> f(\<acute>y)=0)) 
     \<and> (\<not>\<acute>found \<and> \<acute>y\<le>a \<longrightarrow> f(\<acute>y)\<noteq>0)\<guillemotright>\<rbrakk> \<Longrightarrow>  
-  \<parallel>- .{\<exists>u. f(u)=0}.  
+  \<parallel>- \<lbrace>\<exists>u. f(u)=0\<rbrace>  
   \<acute>found:= False,,  
   \<acute>x:=a,, \<acute>y:=a+1,,  
-  COBEGIN .{\<acute>I1}.  
+  COBEGIN \<lbrace>\<acute>I1\<rbrace>  
        WHILE \<not>\<acute>found  
-       INV .{\<acute>I1}.  
-       DO .{a\<le>\<acute>x \<and> (\<acute>found \<longrightarrow> \<acute>y\<le>a \<and> f(\<acute>y)=0) \<and> (a<\<acute>x \<longrightarrow> f(\<acute>x)\<noteq>0)}.  
+       INV \<lbrace>\<acute>I1\<rbrace>  
+       DO \<lbrace>a\<le>\<acute>x \<and> (\<acute>found \<longrightarrow> \<acute>y\<le>a \<and> f(\<acute>y)=0) \<and> (a<\<acute>x \<longrightarrow> f(\<acute>x)\<noteq>0)\<rbrace>  
           \<langle> \<acute>x:=\<acute>x+1,,IF f(\<acute>x)=0 THEN  \<acute>found:=True ELSE  SKIP FI\<rangle>  
        OD  
-       .{\<acute>I1 \<and> \<acute>found}.  
+       \<lbrace>\<acute>I1 \<and> \<acute>found\<rbrace>  
   \<parallel>  
-      .{\<acute>I2}.  
+      \<lbrace>\<acute>I2\<rbrace>  
        WHILE \<not>\<acute>found  
-       INV .{\<acute>I2}.  
-       DO .{\<acute>y\<le>a+1 \<and> (\<acute>found \<longrightarrow> a<\<acute>x \<and> f(\<acute>x)=0) \<and> (\<acute>y\<le>a \<longrightarrow> f(\<acute>y)\<noteq>0)}.  
+       INV \<lbrace>\<acute>I2\<rbrace>  
+       DO \<lbrace>\<acute>y\<le>a+1 \<and> (\<acute>found \<longrightarrow> a<\<acute>x \<and> f(\<acute>x)=0) \<and> (\<acute>y\<le>a \<longrightarrow> f(\<acute>y)\<noteq>0)\<rbrace>  
           \<langle> \<acute>y:=(\<acute>y - 1),,IF f(\<acute>y)=0 THEN  \<acute>found:=True ELSE  SKIP FI\<rangle>  
        OD  
-       .{\<acute>I2 \<and> \<acute>found}.  
+       \<lbrace>\<acute>I2 \<and> \<acute>found\<rbrace>  
   COEND  
-  .{f(\<acute>x)=0 \<or> f(\<acute>y)=0}."
+  \<lbrace>f(\<acute>x)=0 \<or> f(\<acute>y)=0\<rbrace>"
 apply oghoare
 --{* 20 vc *}
 apply auto
@@ -390,44 +390,44 @@
     p1= \<guillemotleft>\<acute>I1 \<and> \<acute>li=\<acute>ins\<guillemotright> ;  
     I2 = \<guillemotleft>\<acute>I \<and> (\<forall>k<\<acute>lj. (a ! k)=(\<acute>b ! k)) \<and> \<acute>lj\<le>length a\<guillemotright> ;
     p2 = \<guillemotleft>\<acute>I2 \<and> \<acute>lj=\<acute>outs\<guillemotright> \<rbrakk> \<Longrightarrow>   
-  \<parallel>- .{\<acute>INIT}.  
+  \<parallel>- \<lbrace>\<acute>INIT\<rbrace>  
  \<acute>ins:=0,, \<acute>outs:=0,, \<acute>li:=0,, \<acute>lj:=0,,
- COBEGIN .{\<acute>p1 \<and> \<acute>INIT}. 
+ COBEGIN \<lbrace>\<acute>p1 \<and> \<acute>INIT\<rbrace> 
    WHILE \<acute>li <length a 
-     INV .{\<acute>p1 \<and> \<acute>INIT}.   
-   DO .{\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li<length a}.  
+     INV \<lbrace>\<acute>p1 \<and> \<acute>INIT\<rbrace>   
+   DO \<lbrace>\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li<length a\<rbrace>  
        \<acute>vx:= (a ! \<acute>li);;  
-      .{\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li<length a \<and> \<acute>vx=(a ! \<acute>li)}. 
+      \<lbrace>\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li<length a \<and> \<acute>vx=(a ! \<acute>li)\<rbrace> 
         WAIT \<acute>ins-\<acute>outs < length \<acute>buffer END;; 
-      .{\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li<length a \<and> \<acute>vx=(a ! \<acute>li) 
-         \<and> \<acute>ins-\<acute>outs < length \<acute>buffer}. 
+      \<lbrace>\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li<length a \<and> \<acute>vx=(a ! \<acute>li) 
+         \<and> \<acute>ins-\<acute>outs < length \<acute>buffer\<rbrace> 
        \<acute>buffer:=(list_update \<acute>buffer (\<acute>ins mod (length \<acute>buffer)) \<acute>vx);; 
-      .{\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li<length a 
+      \<lbrace>\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li<length a 
          \<and> (a ! \<acute>li)=(\<acute>buffer ! (\<acute>ins mod (length \<acute>buffer))) 
-         \<and> \<acute>ins-\<acute>outs <length \<acute>buffer}.  
+         \<and> \<acute>ins-\<acute>outs <length \<acute>buffer\<rbrace>  
        \<acute>ins:=\<acute>ins+1;; 
-      .{\<acute>I1 \<and> \<acute>INIT \<and> (\<acute>li+1)=\<acute>ins \<and> \<acute>li<length a}.  
+      \<lbrace>\<acute>I1 \<and> \<acute>INIT \<and> (\<acute>li+1)=\<acute>ins \<and> \<acute>li<length a\<rbrace>  
        \<acute>li:=\<acute>li+1  
    OD  
-  .{\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li=length a}.  
+  \<lbrace>\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li=length a\<rbrace>  
   \<parallel>  
-  .{\<acute>p2 \<and> \<acute>INIT}.  
+  \<lbrace>\<acute>p2 \<and> \<acute>INIT\<rbrace>  
    WHILE \<acute>lj < length a  
-     INV .{\<acute>p2 \<and> \<acute>INIT}.  
-   DO .{\<acute>p2 \<and> \<acute>lj<length a \<and> \<acute>INIT}.  
+     INV \<lbrace>\<acute>p2 \<and> \<acute>INIT\<rbrace>  
+   DO \<lbrace>\<acute>p2 \<and> \<acute>lj<length a \<and> \<acute>INIT\<rbrace>  
         WAIT \<acute>outs<\<acute>ins END;; 
-      .{\<acute>p2 \<and> \<acute>lj<length a \<and> \<acute>outs<\<acute>ins \<and> \<acute>INIT}.  
+      \<lbrace>\<acute>p2 \<and> \<acute>lj<length a \<and> \<acute>outs<\<acute>ins \<and> \<acute>INIT\<rbrace>  
        \<acute>vy:=(\<acute>buffer ! (\<acute>outs mod (length \<acute>buffer)));; 
-      .{\<acute>p2 \<and> \<acute>lj<length a \<and> \<acute>outs<\<acute>ins \<and> \<acute>vy=(a ! \<acute>lj) \<and> \<acute>INIT}.  
+      \<lbrace>\<acute>p2 \<and> \<acute>lj<length a \<and> \<acute>outs<\<acute>ins \<and> \<acute>vy=(a ! \<acute>lj) \<and> \<acute>INIT\<rbrace>  
        \<acute>outs:=\<acute>outs+1;;  
-      .{\<acute>I2 \<and> (\<acute>lj+1)=\<acute>outs \<and> \<acute>lj<length a \<and> \<acute>vy=(a ! \<acute>lj) \<and> \<acute>INIT}.  
+      \<lbrace>\<acute>I2 \<and> (\<acute>lj+1)=\<acute>outs \<and> \<acute>lj<length a \<and> \<acute>vy=(a ! \<acute>lj) \<and> \<acute>INIT\<rbrace>  
        \<acute>b:=(list_update \<acute>b \<acute>lj \<acute>vy);; 
-      .{\<acute>I2 \<and> (\<acute>lj+1)=\<acute>outs \<and> \<acute>lj<length a \<and> (a ! \<acute>lj)=(\<acute>b ! \<acute>lj) \<and> \<acute>INIT}.  
+      \<lbrace>\<acute>I2 \<and> (\<acute>lj+1)=\<acute>outs \<and> \<acute>lj<length a \<and> (a ! \<acute>lj)=(\<acute>b ! \<acute>lj) \<and> \<acute>INIT\<rbrace>  
        \<acute>lj:=\<acute>lj+1  
    OD  
-  .{\<acute>p2 \<and> \<acute>lj=length a \<and> \<acute>INIT}.  
+  \<lbrace>\<acute>p2 \<and> \<acute>lj=length a \<and> \<acute>INIT\<rbrace>  
  COEND  
- .{ \<forall>k<length a. (a ! k)=(\<acute>b ! k)}."
+ \<lbrace> \<forall>k<length a. (a ! k)=(\<acute>b ! k)\<rbrace>"
 apply oghoare
 --{* 138 vc  *}
 apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
@@ -455,9 +455,9 @@
   a :: "nat \<Rightarrow> nat"
 
 lemma Example1: 
- "\<parallel>- .{True}.
-   COBEGIN SCHEME [0\<le>i<n] .{True}. \<acute>a:=\<acute>a (i:=0) .{\<acute>a i=0}. COEND 
-  .{\<forall>i < n. \<acute>a i = 0}."
+ "\<parallel>- \<lbrace>True\<rbrace>
+   COBEGIN SCHEME [0\<le>i<n] \<lbrace>True\<rbrace> \<acute>a:=\<acute>a (i:=0) \<lbrace>\<acute>a i=0\<rbrace> COEND 
+  \<lbrace>\<forall>i < n. \<acute>a i = 0\<rbrace>"
 apply oghoare
 apply simp_all
 done
@@ -466,11 +466,11 @@
 record Example1_list =
   A :: "nat list"
 lemma Example1_list: 
- "\<parallel>- .{n < length \<acute>A}. 
+ "\<parallel>- \<lbrace>n < length \<acute>A\<rbrace> 
    COBEGIN 
-     SCHEME [0\<le>i<n] .{n < length \<acute>A}. \<acute>A:=\<acute>A[i:=0] .{\<acute>A!i=0}. 
+     SCHEME [0\<le>i<n] \<lbrace>n < length \<acute>A\<rbrace> \<acute>A:=\<acute>A[i:=0] \<lbrace>\<acute>A!i=0\<rbrace> 
    COEND 
-    .{\<forall>i < n. \<acute>A!i = 0}."
+    \<lbrace>\<forall>i < n. \<acute>A!i = 0\<rbrace>"
 apply oghoare
 apply force+
 done
@@ -525,14 +525,14 @@
  x :: nat
 
 lemma Example_2: "0<n \<Longrightarrow> 
- \<parallel>- .{\<acute>x=0 \<and> (\<Sum>i=0..<n. \<acute>c i)=0}.  
+ \<parallel>- \<lbrace>\<acute>x=0 \<and> (\<Sum>i=0..<n. \<acute>c i)=0\<rbrace>  
  COBEGIN 
    SCHEME [0\<le>i<n] 
-  .{\<acute>x=(\<Sum>i=0..<n. \<acute>c i) \<and> \<acute>c i=0}. 
+  \<lbrace>\<acute>x=(\<Sum>i=0..<n. \<acute>c i) \<and> \<acute>c i=0\<rbrace> 
    \<langle> \<acute>x:=\<acute>x+(Suc 0),, \<acute>c:=\<acute>c (i:=(Suc 0)) \<rangle>
-  .{\<acute>x=(\<Sum>i=0..<n. \<acute>c i) \<and> \<acute>c i=(Suc 0)}.
+  \<lbrace>\<acute>x=(\<Sum>i=0..<n. \<acute>c i) \<and> \<acute>c i=(Suc 0)\<rbrace>
  COEND 
- .{\<acute>x=n}."
+ \<lbrace>\<acute>x=n\<rbrace>"
 apply oghoare
 apply (simp_all cong del: strong_setsum_cong)
 apply (tactic {* ALLGOALS (clarify_tac @{context}) *})




