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