src/HOL/Hoare_Parallel/RG_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 \Examples\ prensani@13020 2 haftmann@27651 3 theory RG_Examples haftmann@27651 4 imports RG_Syntax haftmann@27651 5 begin prensani@13020 6 wenzelm@59189 7 lemmas definitions [simp]= stable_def Pre_def Rely_def Guar_def Post_def Com_def prensani@13020 8 wenzelm@59189 9 subsection \Set Elements of an Array to Zero\ prensani@13020 10 prensani@13020 11 lemma le_less_trans2: "\(j::nat) j\ \ i (a::nat) < c; b\d \ \ a + b < c + d" prensani@13020 15 by simp prensani@13020 16 prensani@13020 17 record Example1 = prensani@13020 18 A :: "nat list" prensani@13020 19 wenzelm@59189 20 lemma Example1: prensani@13020 21 "\ COBEGIN prensani@13020 22 SCHEME [0 \ i < n] wenzelm@59189 23 (\A := \A [i := 0], wenzelm@59189 24 \ n < length \A \, wenzelm@59189 25 \ length \A = length \A \ \A ! i = \A ! i \, wenzelm@59189 26 \ length \A = length \A \ (\j j \ \A ! j = \A ! j) \, wenzelm@59189 27 \ \A ! i = 0 \) prensani@13020 28 COEND prensani@13020 29 SAT [\ n < length \A \, \ \A = \A \, \ True \, \ \i < n. \A ! i = 0 \]" prensani@13020 30 apply(rule Parallel) wenzelm@59189 31 apply (auto intro!: Basic) prensani@13020 32 done prensani@13020 33 wenzelm@59189 34 lemma Example1_parameterized: prensani@13020 35 "k < t \ wenzelm@59189 36 \ COBEGIN wenzelm@59189 37 SCHEME [k*n\i<(Suc k)*n] (\A:=\A[i:=0], wenzelm@59189 38 \t*n < length \A\, wenzelm@59189 39 \t*n < length \A \ length \A=length \A \ \A!i = \A!i\, wenzelm@59189 40 \t*n < length \A \ length \A=length \A \ (\jA . i\j \ \A!j = \A!j)\, wenzelm@59189 41 \\A!i=0\) wenzelm@59189 42 COEND wenzelm@59189 43 SAT [\t*n < length \A\, wenzelm@59189 44 \t*n < length \A \ length \A=length \A \ (\iA!(k*n+i)=\A!(k*n+i))\, wenzelm@59189 45 \t*n < length \A \ length \A=length \A \ wenzelm@59189 46 (\iA . (i \A!i = \A!i) \ ((Suc k)*n \ i\ \A!i = \A!i))\, prensani@13020 47 \\iA!(k*n+i) = 0\]" prensani@13020 48 apply(rule Parallel) paulson@15102 49 apply auto paulson@15102 50 apply(erule_tac x="k*n +i" in allE) paulson@15102 51 apply(subgoal_tac "k*n+i Increment a Variable in Parallel\ prensani@13020 70 wenzelm@59189 71 subsubsection \Two components\ prensani@13020 72 prensani@13020 73 record Example2 = prensani@13020 74 x :: nat prensani@13020 75 c_0 :: nat prensani@13020 76 c_1 :: nat prensani@13020 77 wenzelm@59189 78 lemma Example2: prensani@13020 79 "\ COBEGIN wenzelm@59189 80 (\ \x:=\x+1;; \c_0:=\c_0 + 1 \, wenzelm@59189 81 \\x=\c_0 + \c_1 \ \c_0=0\, wenzelm@59189 82 \\c_0 = \c_0 \ wenzelm@59189 83 (\x=\c_0 + \c_1 wenzelm@59189 84 \ \x = \c_0 + \c_1)\, wenzelm@59189 85 \\c_1 = \c_1 \ wenzelm@59189 86 (\x=\c_0 + \c_1 prensani@13020 87 \ \x =\c_0 + \c_1)\, prensani@13020 88 \\x=\c_0 + \c_1 \ \c_0=1 \) prensani@13020 89 \ wenzelm@59189 90 (\ \x:=\x+1;; \c_1:=\c_1+1 \, wenzelm@59189 91 \\x=\c_0 + \c_1 \ \c_1=0 \, wenzelm@59189 92 \\c_1 = \c_1 \ wenzelm@59189 93 (\x=\c_0 + \c_1 wenzelm@59189 94 \ \x = \c_0 + \c_1)\, wenzelm@59189 95 \\c_0 = \c_0 \ wenzelm@59189 96 (\x=\c_0 + \c_1 prensani@13020 97 \ \x =\c_0 + \c_1)\, prensani@13020 98 \\x=\c_0 + \c_1 \ \c_1=1\) prensani@13020 99 COEND wenzelm@59189 100 SAT [\\x=0 \ \c_0=0 \ \c_1=0\, prensani@13020 101 \\x=\x \ \c_0= \c_0 \ \c_1=\c_1\, prensani@13020 102 \True\, prensani@13020 103 \\x=2\]" prensani@13020 104 apply(rule Parallel) prensani@13020 105 apply simp_all prensani@13020 106 apply clarify prensani@13020 107 apply(case_tac i) prensani@13020 108 apply simp paulson@15102 109 apply(rule conjI) prensani@13020 110 apply clarify prensani@13020 111 apply simp prensani@13020 112 apply clarify prensani@13020 113 apply simp prensani@13020 114 apply simp paulson@15102 115 apply(rule conjI) prensani@13020 116 apply clarify prensani@13020 117 apply simp prensani@13020 118 apply clarify prensani@13020 119 apply simp haftmann@56248 120 apply(subgoal_tac "xa=0") haftmann@56248 121 apply simp nipkow@13187 122 apply arith prensani@13020 123 apply clarify haftmann@56248 124 apply(case_tac xaa, simp, simp) nipkow@34233 125 apply clarify prensani@13020 126 apply simp prensani@13020 127 apply(erule_tac x=0 in all_dupE) prensani@13020 128 apply(erule_tac x=1 in allE,simp) prensani@13020 129 apply clarify prensani@13020 130 apply(case_tac i,simp) prensani@13020 131 apply(rule Await) prensani@13020 132 apply simp_all prensani@13020 133 apply(clarify) prensani@13020 134 apply(rule Seq) prensani@13020 135 prefer 2 prensani@13020 136 apply(rule Basic) prensani@13020 137 apply simp_all prensani@13020 138 apply(rule subset_refl) prensani@13020 139 apply(rule Basic) prensani@13020 140 apply simp_all prensani@13020 141 apply clarify prensani@13020 142 apply simp prensani@13020 143 apply(rule Await) prensani@13020 144 apply simp_all prensani@13020 145 apply(clarify) prensani@13020 146 apply(rule Seq) prensani@13020 147 prefer 2 prensani@13020 148 apply(rule Basic) prensani@13020 149 apply simp_all prensani@13020 150 apply(rule subset_refl) paulson@15102 151 apply(auto intro!: Basic) prensani@13020 152 done prensani@13020 153 wenzelm@59189 154 subsubsection \Parameterized\ prensani@13020 155 wenzelm@59189 156 lemma Example2_lemma2_aux: "j nipkow@15561 157 (\i=0..i=0..i=0.. s \ (\i::nat=0..i=0..j \ Suc (\i::nat=0..i=0..i=0..i=0..j") nipkow@15041 182 apply(drule_tac b="b" and t="(Suc 0)" in Example2_lemma2_aux2) nipkow@15041 183 apply(rotate_tac -1) nipkow@15041 184 apply(erule ssubst) prensani@13020 185 apply simp_all prensani@13020 186 done prensani@13020 187 nipkow@15561 188 lemma Example2_lemma2_Suc0: "\j \ nipkow@15561 189 Suc (\i::nat=0..< n. b i)=(\i=0..< n. (b (j:=Suc 0)) i)" prensani@13020 190 by(simp add:Example2_lemma2) prensani@13020 191 wenzelm@59189 192 record Example2_parameterized = prensani@13020 193 C :: "nat \ nat" prensani@13020 194 y :: nat prensani@13020 195 wenzelm@59189 196 lemma Example2_parameterized: "0 prensani@13020 197 \ COBEGIN SCHEME [0\i \y:=\y+1;; \C:=\C (i:=1) \, wenzelm@59189 199 \\y=(\i=0..C i) \ \C i=0\, wenzelm@59189 200 \\C i = \C i \ wenzelm@59189 201 (\y=(\i=0..C i) \ \y =(\i=0..C i))\, wenzelm@59189 202 \(\jj \ \C j = \C j) \ nipkow@15561 203 (\y=(\i=0..C i) \ \y =(\i=0..C i))\, wenzelm@59189 204 \\y=(\i=0..C i) \ \C i=1\) prensani@13020 205 COEND nipkow@15561 206 SAT [\\y=0 \ (\i=0..C i)=0 \, \\C=\C \ \y=\y\, \True\, \\y=n\]" prensani@13020 207 apply(rule Parallel) prensani@13020 208 apply force prensani@13020 209 apply force nipkow@15561 210 apply(force) prensani@13020 211 apply clarify prensani@13020 212 apply simp wenzelm@52567 213 apply simp prensani@13020 214 apply clarify prensani@13020 215 apply simp prensani@13020 216 apply(rule Await) prensani@13020 217 apply simp_all prensani@13020 218 apply clarify prensani@13020 219 apply(rule Seq) prensani@13020 220 prefer 2 prensani@13020 221 apply(rule Basic) prensani@13020 222 apply(rule subset_refl) prensani@13020 223 apply simp+ prensani@13020 224 apply(rule Basic) prensani@13020 225 apply simp prensani@13020 226 apply clarify prensani@13020 227 apply simp nipkow@16733 228 apply(simp add:Example2_lemma2_Suc0 cong:if_cong) wenzelm@52567 229 apply simp_all prensani@13020 230 done prensani@13020 231 wenzelm@59189 232 subsection \Find Least Element\ prensani@13020 233 wenzelm@59189 234 text \A previous lemma:\ prensani@13020 235 prensani@13020 236 lemma mod_aux :"\i < (n::nat); a mod n = i; j < a + n; j mod n = i; a < j\ \ False" prensani@13020 237 apply(subgoal_tac "a=a div n*n + a mod n" ) nipkow@13517 238 prefer 2 apply (simp (no_asm_use)) prensani@13020 239 apply(subgoal_tac "j=j div n*n + j mod n") nipkow@13517 240 prefer 2 apply (simp (no_asm_use)) prensani@13020 241 apply simp prensani@13020 242 apply(subgoal_tac "a div n*n < j div n*n") prensani@13020 243 prefer 2 apply arith prensani@13020 244 apply(subgoal_tac "j div n*n < (a div n + 1)*n") nipkow@13517 245 prefer 2 apply simp prensani@13020 246 apply (simp only:mult_less_cancel2) prensani@13020 247 apply arith prensani@13020 248 done prensani@13020 249 prensani@13020 250 record Example3 = prensani@13020 251 X :: "nat \ nat" prensani@13020 252 Y :: "nat \ nat" prensani@13020 253 wenzelm@59189 254 lemma Example3: "m mod n=0 \ wenzelm@59189 255 \ COBEGIN prensani@13020 256 SCHEME [0\ijX i < \Y j) DO wenzelm@59189 258 IF P(B!(\X i)) THEN \Y:=\Y (i:=\X i) wenzelm@59189 259 ELSE \X:= \X (i:=(\X i)+ n) FI prensani@13020 260 OD, prensani@13020 261 \(\X i) mod n=i \ (\j<\X i. j mod n=i \ \P(B!j)) \ (\Y i P(B!(\Y i)) \ \Y i\ m+i)\, wenzelm@59189 262 \(\jj \ \Y j \ \Y j) \ \X i = \X i \ prensani@13020 263 \Y i = \Y i\, wenzelm@59189 264 \(\jj \ \X j = \X j \ \Y j = \Y j) \ prensani@13020 265 \Y i \ \Y i\, wenzelm@59189 266 \(\X i) mod n=i \ (\j<\X i. j mod n=i \ \P(B!j)) \ (\Y i P(B!(\Y i)) \ \Y i\ m+i) \ (\jY j \ \X i) \) prensani@13020 267 COEND prensani@13020 268 SAT [\ \iX i=i \ \Y i=m+i \,\\X=\X \ \Y=\Y\,\True\, wenzelm@59189 269 \\iX i) mod n=i \ (\j<\X i. j mod n=i \ \P(B!j)) \ prensani@13020 270 (\Y i P(B!(\Y i)) \ \Y i\ m+i) \ (\jY j \ \X i)\]" prensani@13020 271 apply(rule Parallel) wenzelm@62042 272 \\5 subgoals left\ prensani@13020 273 apply force+ prensani@13020 274 apply clarify prensani@13020 275 apply simp prensani@13020 276 apply(rule While) prensani@13020 277 apply force prensani@13020 278 apply force prensani@13020 279 apply force ballarin@14174 280 apply(rule_tac pre'="\ \X i mod n = i \ (\j. j<\X i \ j mod n = i \ \P(B!j)) \ (\Y i < n * q \ P (B!(\Y i))) \ \X i<\Y i\" in Conseq) prensani@13020 281 apply force prensani@13020 282 apply(rule subset_refl)+ prensani@13020 283 apply(rule Cond) prensani@13020 284 apply force prensani@13020 285 apply(rule Basic) prensani@13020 286 apply force nipkow@44890 287 apply fastforce prensani@13020 288 apply force prensani@13020 289 apply force prensani@13020 290 apply(rule Basic) haftmann@27676 291 apply simp prensani@13020 292 apply clarify prensani@13020 293 apply simp haftmann@27651 294 apply (case_tac "X x (j mod n) \ j") haftmann@27651 295 apply (drule le_imp_less_or_eq) haftmann@27651 296 apply (erule disjE) haftmann@27651 297 apply (drule_tac j=j and n=n and i="j mod n" and a="X x (j mod n)" in mod_aux) haftmann@27651 298 apply auto prensani@13020 299 done prensani@13020 300 wenzelm@59189 301 text \Same but with a list as auxiliary variable:\ prensani@13020 302 prensani@13020 303 record Example3_list = prensani@13020 304 X :: "nat list" prensani@13020 305 Y :: "nat list" prensani@13020 306 prensani@13020 307 lemma Example3_list: "m mod n=0 \ \ (COBEGIN SCHEME [0\ijX!i < \Y!j) DO wenzelm@59189 309 IF P(B!(\X!i)) THEN \Y:=\Y[i:=\X!i] ELSE \X:= \X[i:=(\X!i)+ n] FI prensani@13020 310 OD, prensani@13020 311 \nX \ nY \ (\X!i) mod n=i \ (\j<\X!i. j mod n=i \ \P(B!j)) \ (\Y!i P(B!(\Y!i)) \ \Y!i\ m+i)\, wenzelm@59189 312 \(\jj \ \Y!j \ \Y!j) \ \X!i = \X!i \ prensani@13020 313 \Y!i = \Y!i \ length \X = length \X \ length \Y = length \Y\, wenzelm@59189 314 \(\jj \ \X!j = \X!j \ \Y!j = \Y!j) \ prensani@13020 315 \Y!i \ \Y!i \ length \X = length \X \ length \Y = length \Y\, prensani@13020 316 \(\X!i) mod n=i \ (\j<\X!i. j mod n=i \ \P(B!j)) \ (\Y!i P(B!(\Y!i)) \ \Y!i\ m+i) \ (\jY!j \ \X!i) \) COEND) prensani@13020 317 SAT [\nX \ nY \ (\iX!i=i \ \Y!i=m+i) \, prensani@13020 318 \\X=\X \ \Y=\Y\, prensani@13020 319 \True\, wenzelm@59189 320 \\iX!i) mod n=i \ (\j<\X!i. j mod n=i \ \P(B!j)) \ prensani@13020 321 (\Y!i P(B!(\Y!i)) \ \Y!i\ m+i) \ (\jY!j \ \X!i)\]" haftmann@56248 322 apply (rule Parallel) wenzelm@59189 323 apply (auto cong del: strong_INF_cong strong_SUP_cong) haftmann@56248 324 apply force haftmann@56248 325 apply (rule While) prensani@13020 326 apply force prensani@13020 327 apply force prensani@13020 328 apply force ballarin@14174 329 apply(rule_tac pre'="\nX \ nY \ \X ! i mod n = i \ (\j. j < \X ! i \ j mod n = i \ \ P (B ! j)) \ (\Y ! i < n * q \ P (B ! (\Y ! i))) \ \X!i<\Y!i\" in Conseq) prensani@13020 330 apply force prensani@13020 331 apply(rule subset_refl)+ prensani@13020 332 apply(rule Cond) prensani@13020 333 apply force prensani@13020 334 apply(rule Basic) prensani@13020 335 apply force prensani@13020 336 apply force prensani@13020 337 apply force prensani@13020 338 apply force prensani@13020 339 apply(rule Basic) prensani@13020 340 apply simp prensani@13020 341 apply clarify haftmann@27676 342 apply simp prensani@13020 343 apply(rule allI) prensani@13020 344 apply(rule impI)+ prensani@13020 345 apply(case_tac "X x ! i\ j") prensani@13020 346 apply(drule le_imp_less_or_eq) prensani@13020 347 apply(erule disjE) prensani@13020 348 apply(drule_tac j=j and n=n and i=i and a="X x ! i" in mod_aux) haftmann@27651 349 apply auto prensani@13020 350 done prensani@13020 351 nipkow@13187 352 end