src/HOL/HoareParallel/OG_Examples.thy
author haftmann
Mon May 11 15:57:29 2009 +0200 (2009-05-11)
changeset 31101 26c7bb764a38
parent 30686 47a32dd1b86e
permissions -rw-r--r--
qualified names for Lin_Arith tactics and simprocs
     1 
     2 header {* \section{Examples} *}
     3 
     4 theory OG_Examples imports OG_Syntax begin
     5 
     6 subsection {* Mutual Exclusion *}
     7 
     8 subsubsection {* Peterson's Algorithm I*}
     9 
    10 text {* Eike Best. "Semantics of Sequential and Parallel Programs", page 217. *}
    11 
    12 record Petersons_mutex_1 =
    13  pr1 :: nat
    14  pr2 :: nat
    15  in1 :: bool
    16  in2 :: bool 
    17  hold :: nat
    18 
    19 lemma Petersons_mutex_1: 
    20   "\<parallel>- .{\<acute>pr1=0 \<and> \<not>\<acute>in1 \<and> \<acute>pr2=0 \<and> \<not>\<acute>in2 }.  
    21   COBEGIN .{\<acute>pr1=0 \<and> \<not>\<acute>in1}.  
    22   WHILE True INV .{\<acute>pr1=0 \<and> \<not>\<acute>in1}.  
    23   DO  
    24   .{\<acute>pr1=0 \<and> \<not>\<acute>in1}. \<langle> \<acute>in1:=True,,\<acute>pr1:=1 \<rangle>;;  
    25   .{\<acute>pr1=1 \<and> \<acute>in1}.  \<langle> \<acute>hold:=1,,\<acute>pr1:=2 \<rangle>;;  
    26   .{\<acute>pr1=2 \<and> \<acute>in1 \<and> (\<acute>hold=1 \<or> \<acute>hold=2 \<and> \<acute>pr2=2)}.  
    27   AWAIT (\<not>\<acute>in2 \<or> \<not>(\<acute>hold=1)) THEN \<acute>pr1:=3 END;;    
    28   .{\<acute>pr1=3 \<and> \<acute>in1 \<and> (\<acute>hold=1 \<or> \<acute>hold=2 \<and> \<acute>pr2=2)}. 
    29    \<langle>\<acute>in1:=False,,\<acute>pr1:=0\<rangle> 
    30   OD .{\<acute>pr1=0 \<and> \<not>\<acute>in1}.  
    31   \<parallel>  
    32   .{\<acute>pr2=0 \<and> \<not>\<acute>in2}.  
    33   WHILE True INV .{\<acute>pr2=0 \<and> \<not>\<acute>in2}.  
    34   DO  
    35   .{\<acute>pr2=0 \<and> \<not>\<acute>in2}. \<langle> \<acute>in2:=True,,\<acute>pr2:=1 \<rangle>;;  
    36   .{\<acute>pr2=1 \<and> \<acute>in2}. \<langle>  \<acute>hold:=2,,\<acute>pr2:=2 \<rangle>;;  
    37   .{\<acute>pr2=2 \<and> \<acute>in2 \<and> (\<acute>hold=2 \<or> (\<acute>hold=1 \<and> \<acute>pr1=2))}.  
    38   AWAIT (\<not>\<acute>in1 \<or> \<not>(\<acute>hold=2)) THEN \<acute>pr2:=3  END;;    
    39   .{\<acute>pr2=3 \<and> \<acute>in2 \<and> (\<acute>hold=2 \<or> (\<acute>hold=1 \<and> \<acute>pr1=2))}. 
    40     \<langle>\<acute>in2:=False,,\<acute>pr2:=0\<rangle> 
    41   OD .{\<acute>pr2=0 \<and> \<not>\<acute>in2}.  
    42   COEND  
    43   .{\<acute>pr1=0 \<and> \<not>\<acute>in1 \<and> \<acute>pr2=0 \<and> \<not>\<acute>in2}."
    44 apply oghoare
    45 --{* 104 verification conditions. *}
    46 apply auto
    47 done
    48 
    49 subsubsection {*Peterson's Algorithm II: A Busy Wait Solution *}
    50  
    51 text {* Apt and Olderog. "Verification of sequential and concurrent Programs", page 282. *}
    52 
    53 record Busy_wait_mutex =
    54  flag1 :: bool
    55  flag2 :: bool
    56  turn  :: nat
    57  after1 :: bool 
    58  after2 :: bool
    59 
    60 lemma Busy_wait_mutex: 
    61  "\<parallel>-  .{True}.  
    62   \<acute>flag1:=False,, \<acute>flag2:=False,,  
    63   COBEGIN .{\<not>\<acute>flag1}.  
    64         WHILE True  
    65         INV .{\<not>\<acute>flag1}.  
    66         DO .{\<not>\<acute>flag1}. \<langle> \<acute>flag1:=True,,\<acute>after1:=False \<rangle>;;  
    67            .{\<acute>flag1 \<and> \<not>\<acute>after1}. \<langle> \<acute>turn:=1,,\<acute>after1:=True \<rangle>;;  
    68            .{\<acute>flag1 \<and> \<acute>after1 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)}.  
    69             WHILE \<not>(\<acute>flag2 \<longrightarrow> \<acute>turn=2)  
    70             INV .{\<acute>flag1 \<and> \<acute>after1 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)}.  
    71             DO .{\<acute>flag1 \<and> \<acute>after1 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)}. SKIP OD;; 
    72            .{\<acute>flag1 \<and> \<acute>after1 \<and> (\<acute>flag2 \<and> \<acute>after2 \<longrightarrow> \<acute>turn=2)}.
    73             \<acute>flag1:=False  
    74         OD  
    75        .{False}.  
    76   \<parallel>  
    77      .{\<not>\<acute>flag2}.  
    78         WHILE True  
    79         INV .{\<not>\<acute>flag2}.  
    80         DO .{\<not>\<acute>flag2}. \<langle> \<acute>flag2:=True,,\<acute>after2:=False \<rangle>;;  
    81            .{\<acute>flag2 \<and> \<not>\<acute>after2}. \<langle> \<acute>turn:=2,,\<acute>after2:=True \<rangle>;;  
    82            .{\<acute>flag2 \<and> \<acute>after2 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)}.  
    83             WHILE \<not>(\<acute>flag1 \<longrightarrow> \<acute>turn=1)  
    84             INV .{\<acute>flag2 \<and> \<acute>after2 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)}.  
    85             DO .{\<acute>flag2 \<and> \<acute>after2 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)}. SKIP OD;;  
    86            .{\<acute>flag2 \<and> \<acute>after2 \<and> (\<acute>flag1 \<and> \<acute>after1 \<longrightarrow> \<acute>turn=1)}. 
    87             \<acute>flag2:=False  
    88         OD  
    89        .{False}.  
    90   COEND  
    91   .{False}."
    92 apply oghoare
    93 --{* 122 vc *}
    94 apply auto
    95 done
    96 
    97 subsubsection {* Peterson's Algorithm III: A Solution using Semaphores  *}
    98 
    99 record  Semaphores_mutex =
   100  out :: bool
   101  who :: nat
   102 
   103 lemma Semaphores_mutex: 
   104  "\<parallel>- .{i\<noteq>j}.  
   105   \<acute>out:=True ,,  
   106   COBEGIN .{i\<noteq>j}.  
   107        WHILE True INV .{i\<noteq>j}.  
   108        DO .{i\<noteq>j}. AWAIT \<acute>out THEN  \<acute>out:=False,, \<acute>who:=i END;;  
   109           .{\<not>\<acute>out \<and> \<acute>who=i \<and> i\<noteq>j}. \<acute>out:=True OD  
   110        .{False}.  
   111   \<parallel>  
   112        .{i\<noteq>j}.  
   113        WHILE True INV .{i\<noteq>j}.  
   114        DO .{i\<noteq>j}. AWAIT \<acute>out THEN  \<acute>out:=False,,\<acute>who:=j END;;  
   115           .{\<not>\<acute>out \<and> \<acute>who=j \<and> i\<noteq>j}. \<acute>out:=True OD  
   116        .{False}.  
   117   COEND  
   118   .{False}."
   119 apply oghoare
   120 --{* 38 vc *}
   121 apply auto
   122 done
   123 
   124 subsubsection {* Peterson's Algorithm III: Parameterized version: *}
   125 
   126 lemma Semaphores_parameterized_mutex: 
   127  "0<n \<Longrightarrow> \<parallel>- .{True}.  
   128   \<acute>out:=True ,,  
   129  COBEGIN
   130   SCHEME [0\<le> i< n]
   131     .{True}.  
   132      WHILE True INV .{True}.  
   133       DO .{True}. AWAIT \<acute>out THEN  \<acute>out:=False,, \<acute>who:=i END;;  
   134          .{\<not>\<acute>out \<and> \<acute>who=i}. \<acute>out:=True OD
   135     .{False}. 
   136  COEND
   137   .{False}." 
   138 apply oghoare
   139 --{* 20 vc *}
   140 apply auto
   141 done
   142 
   143 subsubsection{* The Ticket Algorithm *}
   144 
   145 record Ticket_mutex =
   146  num :: nat
   147  nextv :: nat
   148  turn :: "nat list"
   149  index :: nat 
   150 
   151 lemma Ticket_mutex: 
   152  "\<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 
   153     \<longrightarrow> \<acute>turn!k < \<acute>num \<and> (\<acute>turn!k =0 \<or> \<acute>turn!k\<noteq>\<acute>turn!l))\<guillemotright> \<rbrakk>
   154    \<Longrightarrow> \<parallel>- .{n=length \<acute>turn}.  
   155    \<acute>index:= 0,,
   156    WHILE \<acute>index < n INV .{n=length \<acute>turn \<and> (\<forall>i<\<acute>index. \<acute>turn!i=0)}. 
   157     DO \<acute>turn:= \<acute>turn[\<acute>index:=0],, \<acute>index:=\<acute>index +1 OD,,
   158   \<acute>num:=1 ,, \<acute>nextv:=1 ,, 
   159  COBEGIN
   160   SCHEME [0\<le> i< n]
   161     .{\<acute>I}.  
   162      WHILE True INV .{\<acute>I}.  
   163       DO .{\<acute>I}. \<langle> \<acute>turn :=\<acute>turn[i:=\<acute>num],, \<acute>num:=\<acute>num+1 \<rangle>;;  
   164          .{\<acute>I}. WAIT \<acute>turn!i=\<acute>nextv END;;
   165          .{\<acute>I \<and> \<acute>turn!i=\<acute>nextv}. \<acute>nextv:=\<acute>nextv+1
   166       OD
   167     .{False}. 
   168  COEND
   169   .{False}." 
   170 apply oghoare
   171 --{* 35 vc *}
   172 apply simp_all
   173 --{* 21 vc *}
   174 apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
   175 --{* 11 vc *}
   176 apply simp_all
   177 apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
   178 --{* 10 subgoals left *}
   179 apply(erule less_SucE)
   180  apply simp
   181 apply simp
   182 --{* 9 subgoals left *}
   183 apply(case_tac "i=k")
   184  apply force
   185 apply simp
   186 apply(case_tac "i=l")
   187  apply force
   188 apply force
   189 --{* 8 subgoals left *}
   190 prefer 8
   191 apply force
   192 apply force
   193 --{* 6 subgoals left *}
   194 prefer 6
   195 apply(erule_tac x=i in allE)
   196 apply fastsimp
   197 --{* 5 subgoals left *}
   198 prefer 5
   199 apply(case_tac [!] "j=k")
   200 --{* 10 subgoals left *}
   201 apply simp_all
   202 apply(erule_tac x=k in allE)
   203 apply force
   204 --{* 9 subgoals left *}
   205 apply(case_tac "j=l")
   206  apply simp
   207  apply(erule_tac x=k in allE)
   208  apply(erule_tac x=k in allE)
   209  apply(erule_tac x=l in allE)
   210  apply force
   211 apply(erule_tac x=k in allE)
   212 apply(erule_tac x=k in allE)
   213 apply(erule_tac x=l in allE)
   214 apply force
   215 --{* 8 subgoals left *}
   216 apply force
   217 apply(case_tac "j=l")
   218  apply simp
   219 apply(erule_tac x=k in allE)
   220 apply(erule_tac x=l in allE)
   221 apply force
   222 apply force
   223 apply force
   224 --{* 5 subgoals left *}
   225 apply(erule_tac x=k in allE)
   226 apply(erule_tac x=l in allE)
   227 apply(case_tac "j=l")
   228  apply force
   229 apply force
   230 apply force
   231 --{* 3 subgoals left *}
   232 apply(erule_tac x=k in allE)
   233 apply(erule_tac x=l in allE)
   234 apply(case_tac "j=l")
   235  apply force
   236 apply force
   237 apply force
   238 --{* 1 subgoals left *}
   239 apply(erule_tac x=k in allE)
   240 apply(erule_tac x=l in allE)
   241 apply(case_tac "j=l")
   242  apply force
   243 apply force
   244 done
   245 
   246 subsection{* Parallel Zero Search *}
   247 
   248 text {* Synchronized Zero Search. Zero-6 *}
   249 
   250 text {*Apt and Olderog. "Verification of sequential and concurrent Programs" page 294: *}
   251 
   252 record Zero_search =
   253    turn :: nat
   254    found :: bool
   255    x :: nat
   256    y :: nat
   257 
   258 lemma Zero_search: 
   259   "\<lbrakk>I1= \<guillemotleft> a\<le>\<acute>x \<and> (\<acute>found \<longrightarrow> (a<\<acute>x \<and> f(\<acute>x)=0) \<or> (\<acute>y\<le>a \<and> f(\<acute>y)=0)) 
   260       \<and> (\<not>\<acute>found \<and> a<\<acute> x \<longrightarrow> f(\<acute>x)\<noteq>0) \<guillemotright> ;  
   261     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)) 
   262       \<and> (\<not>\<acute>found \<and> \<acute>y\<le>a \<longrightarrow> f(\<acute>y)\<noteq>0) \<guillemotright> \<rbrakk> \<Longrightarrow>  
   263   \<parallel>- .{\<exists> u. f(u)=0}.  
   264   \<acute>turn:=1,, \<acute>found:= False,,  
   265   \<acute>x:=a,, \<acute>y:=a+1 ,,  
   266   COBEGIN .{\<acute>I1}.  
   267        WHILE \<not>\<acute>found  
   268        INV .{\<acute>I1}.  
   269        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)}.  
   270           WAIT \<acute>turn=1 END;;  
   271           .{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)}.  
   272           \<acute>turn:=2;;  
   273           .{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)}.    
   274           \<langle> \<acute>x:=\<acute>x+1,,  
   275             IF f(\<acute>x)=0 THEN \<acute>found:=True ELSE SKIP FI\<rangle>  
   276        OD;;  
   277        .{\<acute>I1  \<and> \<acute>found}.  
   278        \<acute>turn:=2  
   279        .{\<acute>I1 \<and> \<acute>found}.  
   280   \<parallel>  
   281       .{\<acute>I2}.  
   282        WHILE \<not>\<acute>found  
   283        INV .{\<acute>I2}.  
   284        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)}.  
   285           WAIT \<acute>turn=2 END;;  
   286           .{\<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)}.  
   287           \<acute>turn:=1;;  
   288           .{\<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)}.  
   289           \<langle> \<acute>y:=(\<acute>y - 1),,  
   290             IF f(\<acute>y)=0 THEN \<acute>found:=True ELSE SKIP FI\<rangle>  
   291        OD;;  
   292        .{\<acute>I2 \<and> \<acute>found}.  
   293        \<acute>turn:=1  
   294        .{\<acute>I2 \<and> \<acute>found}.  
   295   COEND  
   296   .{f(\<acute>x)=0 \<or> f(\<acute>y)=0}."
   297 apply oghoare
   298 --{* 98 verification conditions *}
   299 apply auto 
   300 --{* auto takes about 3 minutes !! *}
   301 done
   302 
   303 text {* Easier Version: without AWAIT.  Apt and Olderog. page 256: *}
   304 
   305 lemma Zero_Search_2: 
   306 "\<lbrakk>I1=\<guillemotleft> a\<le>\<acute>x \<and> (\<acute>found \<longrightarrow> (a<\<acute>x \<and> f(\<acute>x)=0) \<or> (\<acute>y\<le>a \<and> f(\<acute>y)=0)) 
   307     \<and> (\<not>\<acute>found \<and> a<\<acute>x \<longrightarrow> f(\<acute>x)\<noteq>0)\<guillemotright>;  
   308  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)) 
   309     \<and> (\<not>\<acute>found \<and> \<acute>y\<le>a \<longrightarrow> f(\<acute>y)\<noteq>0)\<guillemotright>\<rbrakk> \<Longrightarrow>  
   310   \<parallel>- .{\<exists>u. f(u)=0}.  
   311   \<acute>found:= False,,  
   312   \<acute>x:=a,, \<acute>y:=a+1,,  
   313   COBEGIN .{\<acute>I1}.  
   314        WHILE \<not>\<acute>found  
   315        INV .{\<acute>I1}.  
   316        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)}.  
   317           \<langle> \<acute>x:=\<acute>x+1,,IF f(\<acute>x)=0 THEN  \<acute>found:=True ELSE  SKIP FI\<rangle>  
   318        OD  
   319        .{\<acute>I1 \<and> \<acute>found}.  
   320   \<parallel>  
   321       .{\<acute>I2}.  
   322        WHILE \<not>\<acute>found  
   323        INV .{\<acute>I2}.  
   324        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)}.  
   325           \<langle> \<acute>y:=(\<acute>y - 1),,IF f(\<acute>y)=0 THEN  \<acute>found:=True ELSE  SKIP FI\<rangle>  
   326        OD  
   327        .{\<acute>I2 \<and> \<acute>found}.  
   328   COEND  
   329   .{f(\<acute>x)=0 \<or> f(\<acute>y)=0}."
   330 apply oghoare
   331 --{* 20 vc *}
   332 apply auto
   333 --{* auto takes aprox. 2 minutes. *}
   334 done
   335 
   336 subsection {* Producer/Consumer *}
   337 
   338 subsubsection {* Previous lemmas *}
   339 
   340 lemma nat_lemma2: "\<lbrakk> b = m*(n::nat) + t; a = s*n + u; t=u; b-a < n \<rbrakk> \<Longrightarrow> m \<le> s"
   341 proof -
   342   assume "b = m*(n::nat) + t" "a = s*n + u" "t=u"
   343   hence "(m - s) * n = b - a" by (simp add: diff_mult_distrib)
   344   also assume "\<dots> < n"
   345   finally have "m - s < 1" by simp
   346   thus ?thesis by arith
   347 qed
   348 
   349 lemma mod_lemma: "\<lbrakk> (c::nat) \<le> a; a < b; b - c < n \<rbrakk> \<Longrightarrow> b mod n \<noteq> a mod n"
   350 apply(subgoal_tac "b=b div n*n + b mod n" )
   351  prefer 2  apply (simp add: mod_div_equality [symmetric])
   352 apply(subgoal_tac "a=a div n*n + a mod n")
   353  prefer 2
   354  apply(simp add: mod_div_equality [symmetric])
   355 apply(subgoal_tac "b - a \<le> b - c")
   356  prefer 2 apply arith
   357 apply(drule le_less_trans)
   358 back
   359  apply assumption
   360 apply(frule less_not_refl2)
   361 apply(drule less_imp_le)
   362 apply (drule_tac m = "a" and k = n in div_le_mono)
   363 apply(safe)
   364 apply(frule_tac b = "b" and a = "a" and n = "n" in nat_lemma2, assumption, assumption)
   365 apply assumption
   366 apply(drule order_antisym, assumption)
   367 apply(rotate_tac -3)
   368 apply(simp)
   369 done
   370 
   371 
   372 subsubsection {* Producer/Consumer Algorithm *}
   373 
   374 record Producer_consumer =
   375   ins :: nat
   376   outs :: nat
   377   li :: nat
   378   lj :: nat
   379   vx :: nat
   380   vy :: nat
   381   buffer :: "nat list"
   382   b :: "nat list"
   383 
   384 text {* The whole proof takes aprox. 4 minutes. *}
   385 
   386 lemma Producer_consumer: 
   387   "\<lbrakk>INIT= \<guillemotleft>0<length a \<and> 0<length \<acute>buffer \<and> length \<acute>b=length a\<guillemotright> ;  
   388     I= \<guillemotleft>(\<forall>k<\<acute>ins. \<acute>outs\<le>k \<longrightarrow> (a ! k) = \<acute>buffer ! (k mod (length \<acute>buffer))) \<and>  
   389             \<acute>outs\<le>\<acute>ins \<and> \<acute>ins-\<acute>outs\<le>length \<acute>buffer\<guillemotright> ;  
   390     I1= \<guillemotleft>\<acute>I \<and> \<acute>li\<le>length a\<guillemotright> ;  
   391     p1= \<guillemotleft>\<acute>I1 \<and> \<acute>li=\<acute>ins\<guillemotright> ;  
   392     I2 = \<guillemotleft>\<acute>I \<and> (\<forall>k<\<acute>lj. (a ! k)=(\<acute>b ! k)) \<and> \<acute>lj\<le>length a\<guillemotright> ;
   393     p2 = \<guillemotleft>\<acute>I2 \<and> \<acute>lj=\<acute>outs\<guillemotright> \<rbrakk> \<Longrightarrow>   
   394   \<parallel>- .{\<acute>INIT}.  
   395  \<acute>ins:=0,, \<acute>outs:=0,, \<acute>li:=0,, \<acute>lj:=0,,
   396  COBEGIN .{\<acute>p1 \<and> \<acute>INIT}. 
   397    WHILE \<acute>li <length a 
   398      INV .{\<acute>p1 \<and> \<acute>INIT}.   
   399    DO .{\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li<length a}.  
   400        \<acute>vx:= (a ! \<acute>li);;  
   401       .{\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li<length a \<and> \<acute>vx=(a ! \<acute>li)}. 
   402         WAIT \<acute>ins-\<acute>outs < length \<acute>buffer END;; 
   403       .{\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li<length a \<and> \<acute>vx=(a ! \<acute>li) 
   404          \<and> \<acute>ins-\<acute>outs < length \<acute>buffer}. 
   405        \<acute>buffer:=(list_update \<acute>buffer (\<acute>ins mod (length \<acute>buffer)) \<acute>vx);; 
   406       .{\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li<length a 
   407          \<and> (a ! \<acute>li)=(\<acute>buffer ! (\<acute>ins mod (length \<acute>buffer))) 
   408          \<and> \<acute>ins-\<acute>outs <length \<acute>buffer}.  
   409        \<acute>ins:=\<acute>ins+1;; 
   410       .{\<acute>I1 \<and> \<acute>INIT \<and> (\<acute>li+1)=\<acute>ins \<and> \<acute>li<length a}.  
   411        \<acute>li:=\<acute>li+1  
   412    OD  
   413   .{\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li=length a}.  
   414   \<parallel>  
   415   .{\<acute>p2 \<and> \<acute>INIT}.  
   416    WHILE \<acute>lj < length a  
   417      INV .{\<acute>p2 \<and> \<acute>INIT}.  
   418    DO .{\<acute>p2 \<and> \<acute>lj<length a \<and> \<acute>INIT}.  
   419         WAIT \<acute>outs<\<acute>ins END;; 
   420       .{\<acute>p2 \<and> \<acute>lj<length a \<and> \<acute>outs<\<acute>ins \<and> \<acute>INIT}.  
   421        \<acute>vy:=(\<acute>buffer ! (\<acute>outs mod (length \<acute>buffer)));; 
   422       .{\<acute>p2 \<and> \<acute>lj<length a \<and> \<acute>outs<\<acute>ins \<and> \<acute>vy=(a ! \<acute>lj) \<and> \<acute>INIT}.  
   423        \<acute>outs:=\<acute>outs+1;;  
   424       .{\<acute>I2 \<and> (\<acute>lj+1)=\<acute>outs \<and> \<acute>lj<length a \<and> \<acute>vy=(a ! \<acute>lj) \<and> \<acute>INIT}.  
   425        \<acute>b:=(list_update \<acute>b \<acute>lj \<acute>vy);; 
   426       .{\<acute>I2 \<and> (\<acute>lj+1)=\<acute>outs \<and> \<acute>lj<length a \<and> (a ! \<acute>lj)=(\<acute>b ! \<acute>lj) \<and> \<acute>INIT}.  
   427        \<acute>lj:=\<acute>lj+1  
   428    OD  
   429   .{\<acute>p2 \<and> \<acute>lj=length a \<and> \<acute>INIT}.  
   430  COEND  
   431  .{ \<forall>k<length a. (a ! k)=(\<acute>b ! k)}."
   432 apply oghoare
   433 --{* 138 vc  *}
   434 apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
   435 --{* 112 subgoals left *}
   436 apply(simp_all (no_asm))
   437 apply(tactic {*ALLGOALS (conjI_Tac (K all_tac)) *})
   438 --{* 930 subgoals left *}
   439 apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
   440 apply(simp_all (asm_lr) only:length_0_conv [THEN sym])
   441 --{* 44 subgoals left *}
   442 apply (simp_all (asm_lr) del:length_0_conv add: neq0_conv nth_list_update mod_less_divisor mod_lemma)
   443 --{* 32 subgoals left *}
   444 apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
   445 
   446 apply(tactic {* TRYALL (Lin_Arith.tac @{context}) *})
   447 --{* 9 subgoals left *}
   448 apply (force simp add:less_Suc_eq)
   449 apply(drule sym)
   450 apply (force simp add:less_Suc_eq)+
   451 done
   452 
   453 subsection {* Parameterized Examples *}
   454 
   455 subsubsection {* Set Elements of an Array to Zero *}
   456 
   457 record Example1 =
   458   a :: "nat \<Rightarrow> nat"
   459 
   460 lemma Example1: 
   461  "\<parallel>- .{True}.
   462    COBEGIN SCHEME [0\<le>i<n] .{True}. \<acute>a:=\<acute>a (i:=0) .{\<acute>a i=0}. COEND 
   463   .{\<forall>i < n. \<acute>a i = 0}."
   464 apply oghoare
   465 apply simp_all
   466 done
   467 
   468 text {* Same example with lists as auxiliary variables. *}
   469 record Example1_list =
   470   A :: "nat list"
   471 lemma Example1_list: 
   472  "\<parallel>- .{n < length \<acute>A}. 
   473    COBEGIN 
   474      SCHEME [0\<le>i<n] .{n < length \<acute>A}. \<acute>A:=\<acute>A[i:=0] .{\<acute>A!i=0}. 
   475    COEND 
   476     .{\<forall>i < n. \<acute>A!i = 0}."
   477 apply oghoare
   478 apply force+
   479 done
   480 
   481 subsubsection {* Increment a Variable in Parallel *}
   482 
   483 text {* First some lemmas about summation properties. *}
   484 (*
   485 lemma Example2_lemma1: "!!b. j<n \<Longrightarrow> (\<Sum>i::nat<n. b i) = (0::nat) \<Longrightarrow> b j = 0 "
   486 apply(induct n)
   487  apply simp_all
   488 apply(force simp add: less_Suc_eq)
   489 done
   490 *)
   491 lemma Example2_lemma2_aux: "!!b. j<n \<Longrightarrow> 
   492  (\<Sum>i=0..<n. (b i::nat)) =
   493  (\<Sum>i=0..<j. b i) + b j + (\<Sum>i=0..<n-(Suc j) . b (Suc j + i))"
   494 apply(induct n)
   495  apply simp_all
   496 apply(simp add:less_Suc_eq)
   497  apply(auto)
   498 apply(subgoal_tac "n - j = Suc(n- Suc j)")
   499   apply simp
   500 apply arith
   501 done
   502 
   503 lemma Example2_lemma2_aux2: 
   504   "!!b. j\<le> s \<Longrightarrow> (\<Sum>i::nat=0..<j. (b (s:=t)) i) = (\<Sum>i=0..<j. b i)"
   505 apply(induct j) 
   506  apply simp_all
   507 done
   508 
   509 lemma Example2_lemma2: 
   510  "!!b. \<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i::nat=0..<n. b i)=(\<Sum>i=0..<n. (b (j := Suc 0)) i)"
   511 apply(frule_tac b="(b (j:=(Suc 0)))" in Example2_lemma2_aux)
   512 apply(erule_tac  t="setsum (b(j := (Suc 0))) {0..<n}" in ssubst)
   513 apply(frule_tac b=b in Example2_lemma2_aux)
   514 apply(erule_tac  t="setsum b {0..<n}" in ssubst)
   515 apply(subgoal_tac "Suc (setsum b {0..<j} + b j + (\<Sum>i=0..<n - Suc j. b (Suc j + i)))=(setsum b {0..<j} + Suc (b j) + (\<Sum>i=0..<n - Suc j. b (Suc j + i)))")
   516 apply(rotate_tac -1)
   517 apply(erule ssubst)
   518 apply(subgoal_tac "j\<le>j")
   519  apply(drule_tac b="b" and t="(Suc 0)" in Example2_lemma2_aux2)
   520 apply(rotate_tac -1)
   521 apply(erule ssubst)
   522 apply simp_all
   523 done
   524 
   525 
   526 record Example2 = 
   527  c :: "nat \<Rightarrow> nat" 
   528  x :: nat
   529 
   530 lemma Example_2: "0<n \<Longrightarrow> 
   531  \<parallel>- .{\<acute>x=0 \<and> (\<Sum>i=0..<n. \<acute>c i)=0}.  
   532  COBEGIN 
   533    SCHEME [0\<le>i<n] 
   534   .{\<acute>x=(\<Sum>i=0..<n. \<acute>c i) \<and> \<acute>c i=0}. 
   535    \<langle> \<acute>x:=\<acute>x+(Suc 0),, \<acute>c:=\<acute>c (i:=(Suc 0)) \<rangle>
   536   .{\<acute>x=(\<Sum>i=0..<n. \<acute>c i) \<and> \<acute>c i=(Suc 0)}.
   537  COEND 
   538  .{\<acute>x=n}."
   539 apply oghoare
   540 apply (simp_all cong del: strong_setsum_cong)
   541 apply (tactic {* ALLGOALS (clarify_tac @{claset}) *})
   542 apply (simp_all cong del: strong_setsum_cong)
   543    apply(erule (1) Example2_lemma2)
   544   apply(erule (1) Example2_lemma2)
   545  apply(erule (1) Example2_lemma2)
   546 apply(simp)
   547 done
   548 
   549 end