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