src/HOL/Hoare_Parallel/OG_Examples.thy
 author wenzelm Sat Nov 04 15:24:40 2017 +0100 (21 months ago) changeset 67003 49850a679c2c parent 64267 b9a1486e79be child 67443 3abf6a722518 permissions -rw-r--r--
more robust sorted_entries;
```     1 section \<open>Examples\<close>
```
```     2
```
```     3 theory OG_Examples imports OG_Syntax begin
```
```     4
```
```     5 subsection \<open>Mutual Exclusion\<close>
```
```     6
```
```     7 subsubsection \<open>Peterson's Algorithm I\<close>
```
```     8
```
```     9 text \<open>Eike Best. "Semantics of Sequential and Parallel Programs", page 217.\<close>
```
```    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>- \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1 \<and> \<acute>pr2=0 \<and> \<not>\<acute>in2 \<rbrace>
```
```    20   COBEGIN \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1\<rbrace>
```
```    21   WHILE True INV \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1\<rbrace>
```
```    22   DO
```
```    23   \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1\<rbrace> \<langle> \<acute>in1:=True,,\<acute>pr1:=1 \<rangle>;;
```
```    24   \<lbrace>\<acute>pr1=1 \<and> \<acute>in1\<rbrace>  \<langle> \<acute>hold:=1,,\<acute>pr1:=2 \<rangle>;;
```
```    25   \<lbrace>\<acute>pr1=2 \<and> \<acute>in1 \<and> (\<acute>hold=1 \<or> \<acute>hold=2 \<and> \<acute>pr2=2)\<rbrace>
```
```    26   AWAIT (\<not>\<acute>in2 \<or> \<not>(\<acute>hold=1)) THEN \<acute>pr1:=3 END;;
```
```    27   \<lbrace>\<acute>pr1=3 \<and> \<acute>in1 \<and> (\<acute>hold=1 \<or> \<acute>hold=2 \<and> \<acute>pr2=2)\<rbrace>
```
```    28    \<langle>\<acute>in1:=False,,\<acute>pr1:=0\<rangle>
```
```    29   OD \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1\<rbrace>
```
```    30   \<parallel>
```
```    31   \<lbrace>\<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace>
```
```    32   WHILE True INV \<lbrace>\<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace>
```
```    33   DO
```
```    34   \<lbrace>\<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace> \<langle> \<acute>in2:=True,,\<acute>pr2:=1 \<rangle>;;
```
```    35   \<lbrace>\<acute>pr2=1 \<and> \<acute>in2\<rbrace> \<langle>  \<acute>hold:=2,,\<acute>pr2:=2 \<rangle>;;
```
```    36   \<lbrace>\<acute>pr2=2 \<and> \<acute>in2 \<and> (\<acute>hold=2 \<or> (\<acute>hold=1 \<and> \<acute>pr1=2))\<rbrace>
```
```    37   AWAIT (\<not>\<acute>in1 \<or> \<not>(\<acute>hold=2)) THEN \<acute>pr2:=3  END;;
```
```    38   \<lbrace>\<acute>pr2=3 \<and> \<acute>in2 \<and> (\<acute>hold=2 \<or> (\<acute>hold=1 \<and> \<acute>pr1=2))\<rbrace>
```
```    39     \<langle>\<acute>in2:=False,,\<acute>pr2:=0\<rangle>
```
```    40   OD \<lbrace>\<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace>
```
```    41   COEND
```
```    42   \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1 \<and> \<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace>"
```
```    43 apply oghoare
```
```    44 \<comment>\<open>104 verification conditions.\<close>
```
```    45 apply auto
```
```    46 done
```
```    47
```
```    48 subsubsection \<open>Peterson's Algorithm II: A Busy Wait Solution\<close>
```
```    49
```
```    50 text \<open>Apt and Olderog. "Verification of sequential and concurrent Programs", page 282.\<close>
```
```    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>-  \<lbrace>True\<rbrace>
```
```    61   \<acute>flag1:=False,, \<acute>flag2:=False,,
```
```    62   COBEGIN \<lbrace>\<not>\<acute>flag1\<rbrace>
```
```    63         WHILE True
```
```    64         INV \<lbrace>\<not>\<acute>flag1\<rbrace>
```
```    65         DO \<lbrace>\<not>\<acute>flag1\<rbrace> \<langle> \<acute>flag1:=True,,\<acute>after1:=False \<rangle>;;
```
```    66            \<lbrace>\<acute>flag1 \<and> \<not>\<acute>after1\<rbrace> \<langle> \<acute>turn:=1,,\<acute>after1:=True \<rangle>;;
```
```    67            \<lbrace>\<acute>flag1 \<and> \<acute>after1 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)\<rbrace>
```
```    68             WHILE \<not>(\<acute>flag2 \<longrightarrow> \<acute>turn=2)
```
```    69             INV \<lbrace>\<acute>flag1 \<and> \<acute>after1 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)\<rbrace>
```
```    70             DO \<lbrace>\<acute>flag1 \<and> \<acute>after1 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)\<rbrace> SKIP OD;;
```
```    71            \<lbrace>\<acute>flag1 \<and> \<acute>after1 \<and> (\<acute>flag2 \<and> \<acute>after2 \<longrightarrow> \<acute>turn=2)\<rbrace>
```
```    72             \<acute>flag1:=False
```
```    73         OD
```
```    74        \<lbrace>False\<rbrace>
```
```    75   \<parallel>
```
```    76      \<lbrace>\<not>\<acute>flag2\<rbrace>
```
```    77         WHILE True
```
```    78         INV \<lbrace>\<not>\<acute>flag2\<rbrace>
```
```    79         DO \<lbrace>\<not>\<acute>flag2\<rbrace> \<langle> \<acute>flag2:=True,,\<acute>after2:=False \<rangle>;;
```
```    80            \<lbrace>\<acute>flag2 \<and> \<not>\<acute>after2\<rbrace> \<langle> \<acute>turn:=2,,\<acute>after2:=True \<rangle>;;
```
```    81            \<lbrace>\<acute>flag2 \<and> \<acute>after2 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)\<rbrace>
```
```    82             WHILE \<not>(\<acute>flag1 \<longrightarrow> \<acute>turn=1)
```
```    83             INV \<lbrace>\<acute>flag2 \<and> \<acute>after2 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)\<rbrace>
```
```    84             DO \<lbrace>\<acute>flag2 \<and> \<acute>after2 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)\<rbrace> SKIP OD;;
```
```    85            \<lbrace>\<acute>flag2 \<and> \<acute>after2 \<and> (\<acute>flag1 \<and> \<acute>after1 \<longrightarrow> \<acute>turn=1)\<rbrace>
```
```    86             \<acute>flag2:=False
```
```    87         OD
```
```    88        \<lbrace>False\<rbrace>
```
```    89   COEND
```
```    90   \<lbrace>False\<rbrace>"
```
```    91 apply oghoare
```
```    92 \<comment>\<open>122 vc\<close>
```
```    93 apply auto
```
```    94 done
```
```    95
```
```    96 subsubsection \<open>Peterson's Algorithm III: A Solution using Semaphores\<close>
```
```    97
```
```    98 record  Semaphores_mutex =
```
```    99  out :: bool
```
```   100  who :: nat
```
```   101
```
```   102 lemma Semaphores_mutex:
```
```   103  "\<parallel>- \<lbrace>i\<noteq>j\<rbrace>
```
```   104   \<acute>out:=True ,,
```
```   105   COBEGIN \<lbrace>i\<noteq>j\<rbrace>
```
```   106        WHILE True INV \<lbrace>i\<noteq>j\<rbrace>
```
```   107        DO \<lbrace>i\<noteq>j\<rbrace> AWAIT \<acute>out THEN  \<acute>out:=False,, \<acute>who:=i END;;
```
```   108           \<lbrace>\<not>\<acute>out \<and> \<acute>who=i \<and> i\<noteq>j\<rbrace> \<acute>out:=True OD
```
```   109        \<lbrace>False\<rbrace>
```
```   110   \<parallel>
```
```   111        \<lbrace>i\<noteq>j\<rbrace>
```
```   112        WHILE True INV \<lbrace>i\<noteq>j\<rbrace>
```
```   113        DO \<lbrace>i\<noteq>j\<rbrace> AWAIT \<acute>out THEN  \<acute>out:=False,,\<acute>who:=j END;;
```
```   114           \<lbrace>\<not>\<acute>out \<and> \<acute>who=j \<and> i\<noteq>j\<rbrace> \<acute>out:=True OD
```
```   115        \<lbrace>False\<rbrace>
```
```   116   COEND
```
```   117   \<lbrace>False\<rbrace>"
```
```   118 apply oghoare
```
```   119 \<comment>\<open>38 vc\<close>
```
```   120 apply auto
```
```   121 done
```
```   122
```
```   123 subsubsection \<open>Peterson's Algorithm III: Parameterized version:\<close>
```
```   124
```
```   125 lemma Semaphores_parameterized_mutex:
```
```   126  "0<n \<Longrightarrow> \<parallel>- \<lbrace>True\<rbrace>
```
```   127   \<acute>out:=True ,,
```
```   128  COBEGIN
```
```   129   SCHEME [0\<le> i< n]
```
```   130     \<lbrace>True\<rbrace>
```
```   131      WHILE True INV \<lbrace>True\<rbrace>
```
```   132       DO \<lbrace>True\<rbrace> AWAIT \<acute>out THEN  \<acute>out:=False,, \<acute>who:=i END;;
```
```   133          \<lbrace>\<not>\<acute>out \<and> \<acute>who=i\<rbrace> \<acute>out:=True OD
```
```   134     \<lbrace>False\<rbrace>
```
```   135  COEND
```
```   136   \<lbrace>False\<rbrace>"
```
```   137 apply oghoare
```
```   138 \<comment>\<open>20 vc\<close>
```
```   139 apply auto
```
```   140 done
```
```   141
```
```   142 subsubsection\<open>The Ticket Algorithm\<close>
```
```   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>- \<lbrace>n=length \<acute>turn\<rbrace>
```
```   154    \<acute>index:= 0,,
```
```   155    WHILE \<acute>index < n INV \<lbrace>n=length \<acute>turn \<and> (\<forall>i<\<acute>index. \<acute>turn!i=0)\<rbrace>
```
```   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     \<lbrace>\<acute>I\<rbrace>
```
```   161      WHILE True INV \<lbrace>\<acute>I\<rbrace>
```
```   162       DO \<lbrace>\<acute>I\<rbrace> \<langle> \<acute>turn :=\<acute>turn[i:=\<acute>num],, \<acute>num:=\<acute>num+1 \<rangle>;;
```
```   163          \<lbrace>\<acute>I\<rbrace> WAIT \<acute>turn!i=\<acute>nextv END;;
```
```   164          \<lbrace>\<acute>I \<and> \<acute>turn!i=\<acute>nextv\<rbrace> \<acute>nextv:=\<acute>nextv+1
```
```   165       OD
```
```   166     \<lbrace>False\<rbrace>
```
```   167  COEND
```
```   168   \<lbrace>False\<rbrace>"
```
```   169 apply oghoare
```
```   170 \<comment>\<open>35 vc\<close>
```
```   171 apply simp_all
```
```   172 \<comment>\<open>16 vc\<close>
```
```   173 apply(tactic \<open>ALLGOALS (clarify_tac @{context})\<close>)
```
```   174 \<comment>\<open>11 vc\<close>
```
```   175 apply simp_all
```
```   176 apply(tactic \<open>ALLGOALS (clarify_tac @{context})\<close>)
```
```   177 \<comment>\<open>10 subgoals left\<close>
```
```   178 apply(erule less_SucE)
```
```   179  apply simp
```
```   180 apply simp
```
```   181 \<comment>\<open>9 subgoals left\<close>
```
```   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 \<comment>\<open>8 subgoals left\<close>
```
```   189 prefer 8
```
```   190 apply force
```
```   191 apply force
```
```   192 \<comment>\<open>6 subgoals left\<close>
```
```   193 prefer 6
```
```   194 apply(erule_tac x=j in allE)
```
```   195 apply fastforce
```
```   196 \<comment>\<open>5 subgoals left\<close>
```
```   197 prefer 5
```
```   198 apply(case_tac [!] "j=k")
```
```   199 \<comment>\<open>10 subgoals left\<close>
```
```   200 apply simp_all
```
```   201 apply(erule_tac x=k in allE)
```
```   202 apply force
```
```   203 \<comment>\<open>9 subgoals left\<close>
```
```   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 \<comment>\<open>8 subgoals left\<close>
```
```   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 \<comment>\<open>5 subgoals left\<close>
```
```   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 \<comment>\<open>3 subgoals left\<close>
```
```   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 \<comment>\<open>1 subgoals left\<close>
```
```   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\<open>Parallel Zero Search\<close>
```
```   246
```
```   247 text \<open>Synchronized Zero Search. Zero-6\<close>
```
```   248
```
```   249 text \<open>Apt and Olderog. "Verification of sequential and concurrent Programs" page 294:\<close>
```
```   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>- \<lbrace>\<exists> u. f(u)=0\<rbrace>
```
```   263   \<acute>turn:=1,, \<acute>found:= False,,
```
```   264   \<acute>x:=a,, \<acute>y:=a+1 ,,
```
```   265   COBEGIN \<lbrace>\<acute>I1\<rbrace>
```
```   266        WHILE \<not>\<acute>found
```
```   267        INV \<lbrace>\<acute>I1\<rbrace>
```
```   268        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>
```
```   269           WAIT \<acute>turn=1 END;;
```
```   270           \<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>
```
```   271           \<acute>turn:=2;;
```
```   272           \<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>
```
```   273           \<langle> \<acute>x:=\<acute>x+1,,
```
```   274             IF f(\<acute>x)=0 THEN \<acute>found:=True ELSE SKIP FI\<rangle>
```
```   275        OD;;
```
```   276        \<lbrace>\<acute>I1  \<and> \<acute>found\<rbrace>
```
```   277        \<acute>turn:=2
```
```   278        \<lbrace>\<acute>I1 \<and> \<acute>found\<rbrace>
```
```   279   \<parallel>
```
```   280       \<lbrace>\<acute>I2\<rbrace>
```
```   281        WHILE \<not>\<acute>found
```
```   282        INV \<lbrace>\<acute>I2\<rbrace>
```
```   283        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>
```
```   284           WAIT \<acute>turn=2 END;;
```
```   285           \<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>
```
```   286           \<acute>turn:=1;;
```
```   287           \<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>
```
```   288           \<langle> \<acute>y:=(\<acute>y - 1),,
```
```   289             IF f(\<acute>y)=0 THEN \<acute>found:=True ELSE SKIP FI\<rangle>
```
```   290        OD;;
```
```   291        \<lbrace>\<acute>I2 \<and> \<acute>found\<rbrace>
```
```   292        \<acute>turn:=1
```
```   293        \<lbrace>\<acute>I2 \<and> \<acute>found\<rbrace>
```
```   294   COEND
```
```   295   \<lbrace>f(\<acute>x)=0 \<or> f(\<acute>y)=0\<rbrace>"
```
```   296 apply oghoare
```
```   297 \<comment>\<open>98 verification conditions\<close>
```
```   298 apply auto
```
```   299 \<comment>\<open>auto takes about 3 minutes !!\<close>
```
```   300 done
```
```   301
```
```   302 text \<open>Easier Version: without AWAIT.  Apt and Olderog. page 256:\<close>
```
```   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>- \<lbrace>\<exists>u. f(u)=0\<rbrace>
```
```   310   \<acute>found:= False,,
```
```   311   \<acute>x:=a,, \<acute>y:=a+1,,
```
```   312   COBEGIN \<lbrace>\<acute>I1\<rbrace>
```
```   313        WHILE \<not>\<acute>found
```
```   314        INV \<lbrace>\<acute>I1\<rbrace>
```
```   315        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>
```
```   316           \<langle> \<acute>x:=\<acute>x+1,,IF f(\<acute>x)=0 THEN  \<acute>found:=True ELSE  SKIP FI\<rangle>
```
```   317        OD
```
```   318        \<lbrace>\<acute>I1 \<and> \<acute>found\<rbrace>
```
```   319   \<parallel>
```
```   320       \<lbrace>\<acute>I2\<rbrace>
```
```   321        WHILE \<not>\<acute>found
```
```   322        INV \<lbrace>\<acute>I2\<rbrace>
```
```   323        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>
```
```   324           \<langle> \<acute>y:=(\<acute>y - 1),,IF f(\<acute>y)=0 THEN  \<acute>found:=True ELSE  SKIP FI\<rangle>
```
```   325        OD
```
```   326        \<lbrace>\<acute>I2 \<and> \<acute>found\<rbrace>
```
```   327   COEND
```
```   328   \<lbrace>f(\<acute>x)=0 \<or> f(\<acute>y)=0\<rbrace>"
```
```   329 apply oghoare
```
```   330 \<comment>\<open>20 vc\<close>
```
```   331 apply auto
```
```   332 \<comment>\<open>auto takes aprox. 2 minutes.\<close>
```
```   333 done
```
```   334
```
```   335 subsection \<open>Producer/Consumer\<close>
```
```   336
```
```   337 subsubsection \<open>Previous lemmas\<close>
```
```   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: div_mult_mod_eq [symmetric])
```
```   351 apply(subgoal_tac "a=a div n*n + a mod n")
```
```   352  prefer 2
```
```   353  apply(simp add: div_mult_mod_eq [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 \<open>Producer/Consumer Algorithm\<close>
```
```   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 \<open>The whole proof takes aprox. 4 minutes.\<close>
```
```   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>- \<lbrace>\<acute>INIT\<rbrace>
```
```   394  \<acute>ins:=0,, \<acute>outs:=0,, \<acute>li:=0,, \<acute>lj:=0,,
```
```   395  COBEGIN \<lbrace>\<acute>p1 \<and> \<acute>INIT\<rbrace>
```
```   396    WHILE \<acute>li <length a
```
```   397      INV \<lbrace>\<acute>p1 \<and> \<acute>INIT\<rbrace>
```
```   398    DO \<lbrace>\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li<length a\<rbrace>
```
```   399        \<acute>vx:= (a ! \<acute>li);;
```
```   400       \<lbrace>\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li<length a \<and> \<acute>vx=(a ! \<acute>li)\<rbrace>
```
```   401         WAIT \<acute>ins-\<acute>outs < length \<acute>buffer END;;
```
```   402       \<lbrace>\<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\<rbrace>
```
```   404        \<acute>buffer:=(list_update \<acute>buffer (\<acute>ins mod (length \<acute>buffer)) \<acute>vx);;
```
```   405       \<lbrace>\<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\<rbrace>
```
```   408        \<acute>ins:=\<acute>ins+1;;
```
```   409       \<lbrace>\<acute>I1 \<and> \<acute>INIT \<and> (\<acute>li+1)=\<acute>ins \<and> \<acute>li<length a\<rbrace>
```
```   410        \<acute>li:=\<acute>li+1
```
```   411    OD
```
```   412   \<lbrace>\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li=length a\<rbrace>
```
```   413   \<parallel>
```
```   414   \<lbrace>\<acute>p2 \<and> \<acute>INIT\<rbrace>
```
```   415    WHILE \<acute>lj < length a
```
```   416      INV \<lbrace>\<acute>p2 \<and> \<acute>INIT\<rbrace>
```
```   417    DO \<lbrace>\<acute>p2 \<and> \<acute>lj<length a \<and> \<acute>INIT\<rbrace>
```
```   418         WAIT \<acute>outs<\<acute>ins END;;
```
```   419       \<lbrace>\<acute>p2 \<and> \<acute>lj<length a \<and> \<acute>outs<\<acute>ins \<and> \<acute>INIT\<rbrace>
```
```   420        \<acute>vy:=(\<acute>buffer ! (\<acute>outs mod (length \<acute>buffer)));;
```
```   421       \<lbrace>\<acute>p2 \<and> \<acute>lj<length a \<and> \<acute>outs<\<acute>ins \<and> \<acute>vy=(a ! \<acute>lj) \<and> \<acute>INIT\<rbrace>
```
```   422        \<acute>outs:=\<acute>outs+1;;
```
```   423       \<lbrace>\<acute>I2 \<and> (\<acute>lj+1)=\<acute>outs \<and> \<acute>lj<length a \<and> \<acute>vy=(a ! \<acute>lj) \<and> \<acute>INIT\<rbrace>
```
```   424        \<acute>b:=(list_update \<acute>b \<acute>lj \<acute>vy);;
```
```   425       \<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>
```
```   426        \<acute>lj:=\<acute>lj+1
```
```   427    OD
```
```   428   \<lbrace>\<acute>p2 \<and> \<acute>lj=length a \<and> \<acute>INIT\<rbrace>
```
```   429  COEND
```
```   430  \<lbrace> \<forall>k<length a. (a ! k)=(\<acute>b ! k)\<rbrace>"
```
```   431 apply oghoare
```
```   432 \<comment>\<open>138 vc\<close>
```
```   433 apply(tactic \<open>ALLGOALS (clarify_tac @{context})\<close>)
```
```   434 \<comment>\<open>112 subgoals left\<close>
```
```   435 apply(simp_all (no_asm))
```
```   436 \<comment>\<open>43 subgoals left\<close>
```
```   437 apply(tactic \<open>ALLGOALS (conjI_Tac @{context} (K all_tac))\<close>)
```
```   438 \<comment>\<open>419 subgoals left\<close>
```
```   439 apply(tactic \<open>ALLGOALS (clarify_tac @{context})\<close>)
```
```   440 \<comment>\<open>99 subgoals left\<close>
```
```   441 apply(simp_all only:length_0_conv [THEN sym])
```
```   442 \<comment>\<open>20 subgoals left\<close>
```
```   443 apply (simp_all del:length_0_conv length_greater_0_conv add: nth_list_update mod_lemma)
```
```   444 \<comment>\<open>9 subgoals left\<close>
```
```   445 apply (force simp add:less_Suc_eq)
```
```   446 apply(hypsubst_thin, drule sym)
```
```   447 apply (force simp add:less_Suc_eq)+
```
```   448 done
```
```   449
```
```   450 subsection \<open>Parameterized Examples\<close>
```
```   451
```
```   452 subsubsection \<open>Set Elements of an Array to Zero\<close>
```
```   453
```
```   454 record Example1 =
```
```   455   a :: "nat \<Rightarrow> nat"
```
```   456
```
```   457 lemma Example1:
```
```   458  "\<parallel>- \<lbrace>True\<rbrace>
```
```   459    COBEGIN SCHEME [0\<le>i<n] \<lbrace>True\<rbrace> \<acute>a:=\<acute>a (i:=0) \<lbrace>\<acute>a i=0\<rbrace> COEND
```
```   460   \<lbrace>\<forall>i < n. \<acute>a i = 0\<rbrace>"
```
```   461 apply oghoare
```
```   462 apply simp_all
```
```   463 done
```
```   464
```
```   465 text \<open>Same example with lists as auxiliary variables.\<close>
```
```   466 record Example1_list =
```
```   467   A :: "nat list"
```
```   468 lemma Example1_list:
```
```   469  "\<parallel>- \<lbrace>n < length \<acute>A\<rbrace>
```
```   470    COBEGIN
```
```   471      SCHEME [0\<le>i<n] \<lbrace>n < length \<acute>A\<rbrace> \<acute>A:=\<acute>A[i:=0] \<lbrace>\<acute>A!i=0\<rbrace>
```
```   472    COEND
```
```   473     \<lbrace>\<forall>i < n. \<acute>A!i = 0\<rbrace>"
```
```   474 apply oghoare
```
```   475 apply force+
```
```   476 done
```
```   477
```
```   478 subsubsection \<open>Increment a Variable in Parallel\<close>
```
```   479
```
```   480 text \<open>First some lemmas about summation properties.\<close>
```
```   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="sum (b(j := (Suc 0))) {0..<n}" in ssubst)
```
```   510 apply(frule_tac b=b in Example2_lemma2_aux)
```
```   511 apply(erule_tac  t="sum b {0..<n}" in ssubst)
```
```   512 apply(subgoal_tac "Suc (sum b {0..<j} + b j + (\<Sum>i=0..<n - Suc j. b (Suc j + i)))=(sum 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>- \<lbrace>\<acute>x=0 \<and> (\<Sum>i=0..<n. \<acute>c i)=0\<rbrace>
```
```   529  COBEGIN
```
```   530    SCHEME [0\<le>i<n]
```
```   531   \<lbrace>\<acute>x=(\<Sum>i=0..<n. \<acute>c i) \<and> \<acute>c i=0\<rbrace>
```
```   532    \<langle> \<acute>x:=\<acute>x+(Suc 0),, \<acute>c:=\<acute>c (i:=(Suc 0)) \<rangle>
```
```   533   \<lbrace>\<acute>x=(\<Sum>i=0..<n. \<acute>c i) \<and> \<acute>c i=(Suc 0)\<rbrace>
```
```   534  COEND
```
```   535  \<lbrace>\<acute>x=n\<rbrace>"
```
```   536 apply oghoare
```
```   537 apply (simp_all cong del: sum.strong_cong)
```
```   538 apply (tactic \<open>ALLGOALS (clarify_tac @{context})\<close>)
```
```   539 apply (simp_all cong del: sum.strong_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
```