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