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
```