1(* ------------------------------------------------------------------------- *) 2(* Loop Recurrence Theory *) 3(* ------------------------------------------------------------------------- *) 4 5(*===========================================================================*) 6 7(* add all dependent libraries for script *) 8open HolKernel boolLib bossLib Parse; 9 10(* declare new theory at start *) 11val _ = new_theory "loop"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16 17(* val _ = load "jcLib"; *) 18open jcLib; 19 20(* Get dependent theories in lib *) 21(* val _ = load "logPowerTheory"; (* has helperNum, helperSet, helperFunction *) *) 22open helperNumTheory helperSetTheory helperListTheory helperFunctionTheory; 23 24(* open dependent theories *) 25open listTheory rich_listTheory; 26open listRangeTheory; 27 28open arithmeticTheory; 29 30 31(* ------------------------------------------------------------------------- *) 32(* Loop Recurrence Documentation *) 33(* ------------------------------------------------------------------------- *) 34(* Type and Overload: 35*) 36(* Definitions and Theorems (# are exported): 37 38 Helper Theorems: 39 40 Loop Count for recurrence: 41 loop_count_def |- !modify guard R. WF R ==> (!x. ~guard x ==> R (modify x) x) ==> 42 !x. loop_count guard modify x = 43 if guard x then 0 else SUC (loop_count guard modify (modify x)) 44 loop_count_thm |- !modify guard R. WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 45 !x. loop_count guard modify x = 46 if guard x then 0 else SUC (loop_count guard modify (modify x)) 47 loop_count_0 |- !modify guard R. WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 48 !x. guard x ==> loop_count guard modify x = 0 49 loop_count_suc |- !modify guard R. WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 50 !x. ~guard x ==> loop_count guard modify x = SUC (loop_count guard modify (modify x)) 51 loop_count_iterating|- !modify guard R. WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 52 !x. guard (FUNPOW modify (loop_count guard modify x) x) 53 loop_count_exists |- !modify guard R. WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 54 !x. ?n. guard (FUNPOW modify n x) 55 loop_count_minimal |- !modify guard R. WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 56 !x n. guard (FUNPOW modify n x) /\ 57 (!m. m < n ==> ~guard (FUNPOW modify m x)) ==> 58 loop_count guard modify x = n 59 loop_count_eqn |- !modify guard R. WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 60 !x. loop_count guard modify x = LEAST n. guard (FUNPOW modify n x) 61 62 General Theory of Recurrence with 1 argument: 63 loop_modify_count_eqn 64 |- !loop guard body quit modify R. WF R /\ 65 (!x. ~guard x ==> R (modify x) x) /\ 66 (!x. loop x = if guard x then quit x else body x + loop (modify x)) ==> 67 !x. loop x = quit (FUNPOW modify (loop_count guard modify x) x) + 68 SUM (GENLIST (\j. body (FUNPOW modify j x)) (loop_count guard modify x)) 69 loop_modify_count_eqn_1 70 |- !loop guard body quit modify R. WF R /\ 71 (!x. ~guard x ==> R (modify x) x) /\ 72 (!x. loop x = if guard x then quit x else body x + loop (modify x)) ==> 73 !x. (let n = loop_count guard modify x 74 in loop x = quit (FUNPOW modify n x) + 75 SUM (GENLIST (\j. body (FUNPOW modify j x)) n)) 76 loop_modify_count_eqn_2 77 |- !loop guard body quit modify R. WF R /\ 78 (!x. ~guard x ==> R (modify x) x) /\ 79 (!x. loop x = if guard x then quit x else body x + loop (modify x)) ==> 80 !x. (let n = loop_count guard modify x 81 in loop x = quit (FUNPOW modify n x) + 82 SIGMA (\j. body (FUNPOW modify j x)) (count n)) 83 loop_modify_count_exit_le 84 |- !loop guard body quit exit modify R. WF R /\ 85 (!x. ~guard x ==> R (modify x) x) /\ 86 (!x. loop x = 87 if guard x then quit x 88 else body x + if exit x then 0 else loop (modify x)) ==> 89 !x. loop x <= quit (FUNPOW modify (loop_count guard modify x) x) + 90 SUM (GENLIST (\j. body (FUNPOW modify j x)) (loop_count guard modify x)) 91 loop_rise_count_cover_exit_le 92 |- !loop guard body quit exit modify R. WF R /\ 93 (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 94 (!x. loop x = 95 if guard x then quit x 96 else body x + if exit x then 0 else loop (modify x)) ==> 97 !x cover. (let n = loop_count guard modify x 98 in (!x. body x <= cover x) /\ MONO cover ==> 99 loop x <= quit (FUNPOW modify n x) + n * cover (FUNPOW modify n x)) 100 loop_rise_count_rcover_exit_le 101 |- !loop guard body quit exit modify R. WF R /\ 102 (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 103 (!x. loop x = 104 if guard x then quit x 105 else body x + if exit x then 0 else loop (modify x)) ==> 106 !x cover. (let n = loop_count guard modify x 107 in (!x. body x <= cover x) /\ RMONO cover ==> 108 loop x <= quit (FUNPOW modify n x) + n * cover x) 109 loop_fall_count_cover_exit_le 110 |- !loop guard body quit exit modify R. WF R /\ 111 (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 112 (!x. loop x = 113 if guard x then quit x 114 else body x + if exit x then 0 else loop (modify x)) ==> 115 !x cover. (let n = loop_count guard modify x 116 in (!x. body x <= cover x) /\ MONO cover ==> 117 loop x <= quit (FUNPOW modify n x) + n * cover x) 118 loop_fall_count_rcover_exit_le 119 |- !loop guard body quit exit modify R. WF R /\ 120 (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 121 (!x. loop x = 122 if guard x then quit x 123 else body x + if exit x then 0 else loop (modify x)) ==> 124 !x cover. (let n = loop_count guard modify x 125 in (!x. body x <= cover x) /\ RMONO cover ==> 126 loop x <= quit (FUNPOW modify n x) + n * cover (FUNPOW modify n x)) 127 128 General Theory of Recurrence with 2 arguments: 129 loop2_count_def |- !guard modify transform x y. loop2_count guard modify transform x y = 130 loop_count (\(x,y). guard x y) (\(x,y). (transform x,modify y)) (x,y) 131 loop2_count_thm |- !transform modify guard R. WF R /\ 132 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> 133 !x y. loop2_count guard modify transform x y = 134 if guard x y then 0 135 else SUC (loop2_count guard modify transform (transform x) (modify y)) 136 loop2_count_0 |- !transform modify guard R. WF R /\ 137 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> 138 !x y. guard x y ==> loop2_count guard modify transform x y = 0 139 loop2_count_suc |- !transform modify guard R. WF R /\ 140 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> 141 !x y. ~guard x y ==> loop2_count guard modify transform x y = 142 SUC (loop2_count guard modify transform (transform x) (modify y)) 143 loop2_count_iterating 144 |- !transform modify guard R. WF R /\ 145 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> 146 !x y. guard (FUNPOW transform (loop2_count guard modify transform x y) x) 147 (FUNPOW modify (loop2_count guard modify transform x y) y) 148 loop2_modify_count_eqn 149 |- !loop guard body quit modify transform R. WF R /\ 150 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 151 (!x y. loop x y = 152 if guard x y then quit x y 153 else body x y + loop (transform x) (modify y)) ==> 154 !x y. loop x y = 155 quit (FUNPOW transform (loop2_count guard modify transform x y) x) 156 (FUNPOW modify (loop2_count guard modify transform x y) y) + 157 SUM (GENLIST (\j. body (FUNPOW transform j x) (FUNPOW modify j y)) 158 (loop2_count guard modify transform x y)) 159 loop2_modify_count_exit_le 160 |- !loop guard body quit exit modify transform R. WF R /\ 161 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 162 (!x y. loop x y = 163 if guard x y then quit x y 164 else body x y + 165 if exit x y then 0 else loop (transform x) (modify y)) ==> 166 !x y. loop x y <= 167 quit (FUNPOW transform (loop2_count guard modify transform x y) x) 168 (FUNPOW modify (loop2_count guard modify transform x y) y) + 169 SUM (GENLIST (\j. body (FUNPOW transform j x) (FUNPOW modify j y)) 170 (loop2_count guard modify transform x y)) 171 172 List for Transform argument: 173 iterating_def |- !y x f. iterating f x y = 174 if y = 0 then [] else x::iterating f (f x) (y - 1) 175 iterating_nil |- !f x. iterating f x 0 = [] 176 iterating_cons |- !f x y. iterating f x (SUC y) = x::iterating f (f x) y 177 iterating_alt |- (!f x. iterating f x 0 = []) /\ 178 !f x y. iterating f x (SUC y) = x::iterating f (f x) y 179 iterating_eqn |- !f x y. iterating f x y = MAP (combin$C (FUNPOW f) x) [0 ..< y] 180 iterating_length |- !f x y. LENGTH (iterating f x y) = y 181 iterating_member |- !f x y j. j < y ==> MEM (FUNPOW f j x) (iterating f x y) 182 iterating_element |- !f x y j. j < y ==> EL j (iterating f x y) = FUNPOW f j x 183 184 Numeric Loops with transform and modify: 185 loop2_rise_fall_count_cover_exit_le 186 |- !loop guard body quit exit modify transform R. WF R /\ 187 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 188 RISING transform /\ FALLING modify /\ 189 (!x y. loop x y = 190 if guard x y then quit x y 191 else body x y + 192 if exit x y then 0 else loop (transform x) (modify y)) ==> 193 !x y cover. (let n = loop2_count guard modify transform x y 194 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 195 loop x y <= quit (FUNPOW transform n x) (FUNPOW modify n y) + 196 n * cover (FUNPOW transform n x) y) 197 loop2_fall_fall_count_cover_exit_le 198 |- !loop guard body quit exit modify transform R. WF R /\ 199 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 200 FALLING transform /\ FALLING modify /\ 201 (!x y. loop x y = 202 if guard x y then quit x y 203 else body x y + 204 if exit x y then 0 else loop (transform x) (modify y)) ==> 205 !x y cover. (let n = loop2_count guard modify transform x y 206 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 207 loop x y <= quit (FUNPOW transform n x) (FUNPOW modify n y) + 208 n * cover x y) 209 loop2_fall_rise_count_cover_exit_le 210 |- !loop guard body quit exit modify transform R. WF R /\ 211 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 212 FALLING transform /\ RISING modify /\ 213 (!x y. loop x y = 214 if guard x y then quit x y 215 else body x y + 216 if exit x y then 0 else loop (transform x) (modify y)) ==> 217 !x y cover. (let n = loop2_count guard modify transform x y 218 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 219 loop x y <= quit (FUNPOW transform n x) (FUNPOW modify n y) + 220 n * cover x (FUNPOW modify n y)) 221 loop2_rise_rise_count_cover_exit_le 222 |- !loop guard body quit exit modify transform R. WF R /\ 223 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 224 RISING transform /\ RISING modify /\ 225 (!x y. loop x y = 226 if guard x y then quit x y 227 else body x y + 228 if exit x y then 0 else loop (transform x) (modify y)) ==> 229 !x y cover. (let n = loop2_count guard modify transform x y 230 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 231 loop x y <= quit (FUNPOW transform n x) (FUNPOW modify n y) + 232 n * cover (FUNPOW transform n x) (FUNPOW modify n y)) 233 234 General Theory of Recurrence with 3 arguments: 235 loop3_count_def |- !guard modify transform convert x y z. 236 loop3_count guard modify transform convert x y z = 237 loop_count (\(x,y,z). guard x y z) 238 (\(x,y,z). (convert x,transform y,modify z)) (x,y,z) 239 loop3_count_thm |- !convert transform modify guard R. WF R /\ 240 (!x y z. ~guard x y z ==> R (convert x,transform y,modify z) (x,y,z)) ==> 241 !x y z. loop3_count guard modify transform convert x y z = 242 if guard x y z then 0 243 else SUC (loop3_count guard modify transform convert 244 (convert x) (transform y) (modify z)) 245 loop3_count_0 |- !convert transform modify guard R. WF R /\ 246 (!x y z. ~guard x y z ==> R (convert x,transform y,modify z) (x,y,z)) ==> 247 !x y z. guard x y z ==> 248 loop3_count guard modify transform convert x y z = 0 249 loop3_count_suc |- !convert transform modify guard R. WF R /\ 250 (!x y z. ~guard x y z ==> R (convert x,transform y,modify z) (x,y,z)) ==> 251 !x y z. ~guard x y z ==> 252 loop3_count guard modify transform convert x y z = 253 SUC (loop3_count guard modify transform convert 254 (convert x) (transform y) (modify z)) 255 loop3_count_iterating 256 |- !convert transform modify guard R. WF R /\ 257 (!x y z. ~guard x y z ==> R (convert x,transform y,modify z) (x,y,z)) ==> 258 !x y z. guard 259 (FUNPOW convert (loop3_count guard modify transform convert x y z) x) 260 (FUNPOW transform (loop3_count guard modify transform convert x y z) y) 261 (FUNPOW modify (loop3_count guard modify transform convert x y z) z) 262 loop3_modify_count_eqn 263 |- !loop guard body quit modify transform convert R. WF R /\ 264 (!x y z. ~guard x y z ==> R (convert x,transform y,modify z) (x,y,z)) /\ 265 (!x y z. loop x y z = 266 if guard x y z then quit x y z 267 else body x y z + loop (convert x) (transform y) (modify z)) ==> 268 !x y z. loop x y z = 269 quit (FUNPOW convert (loop3_count guard modify transform convert x y z) x) 270 (FUNPOW transform (loop3_count guard modify transform convert x y z) y) 271 (FUNPOW modify (loop3_count guard modify transform convert x y z) z) + 272 SUM (GENLIST (\j. body (FUNPOW convert j x) 273 (FUNPOW transform j y) 274 (FUNPOW modify j z)) 275 (loop3_count guard modify transform convert x y z)) 276 loop3_modify_count_exit_le 277 |- !loop guard body quit exit modify transform convert R. WF R /\ 278 (!x y z. ~guard x y z ==> R (convert x,transform y,modify z) (x,y,z)) /\ 279 (!x y z. loop x y z = 280 if guard x y z then quit x y z 281 else body x y z + if exit x y z then 0 282 else loop (convert x) (transform y) (modify z)) ==> 283 !x y z. loop x y z <= 284 quit (FUNPOW convert (loop3_count guard modify transform convert x y z) x) 285 (FUNPOW transform (loop3_count guard modify transform convert x y z) y) 286 (FUNPOW modify (loop3_count guard modify transform convert x y z) z) + 287 SUM (GENLIST (\j. body (FUNPOW convert j x) 288 (FUNPOW transform j y) 289 (FUNPOW modify j z)) 290 (loop3_count guard modify transform convert x y z)) 291 292 Original: 293 loop_arg_def |- !modify guard R. WF R ==> (!x. ~guard x ==> R (modify x) x) ==> 294 !x. loop_arg guard modify x = 295 if guard x then [] else x::loop_arg guard modify (modify x) 296 loop_arg_thm |- !modify guard R. WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 297 !x. loop_arg guard modify x = 298 if guard x then [] else x::loop_arg guard modify (modify x) 299 loop_arg_nil |- !modify guard R. WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 300 !x. guard x ==> loop_arg guard modify x = [] 301 loop_arg_cons |- !modify guard R. WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 302 !x. ~guard x ==> loop_arg guard modify x = x::loop_arg guard modify (modify x) 303 loop_arg_length |- !modify guard R. WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 304 !x. LENGTH (loop_arg guard modify x) = loop_count guard modify x 305 loop_arg_eqn |- !modify guard R. WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 306 !x. loop_arg guard modify x = 307 GENLIST (\j. FUNPOW modify j x) (loop_count guard modify x) 308 loop_arg_element |- !modify guard R. WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 309 !x k. k < loop_count guard modify x ==> 310 EL k (loop_arg guard modify x) = FUNPOW modify k x 311 loop_arg_cover_sum |- !modify guard R cover. WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 312 (!x y. R x y ==> cover x <= cover y) ==> 313 !x. SUM (MAP cover (loop_arg guard modify x)) <= 314 SUM (MAP (K (cover x)) (loop_arg guard modify x)) 315 loop_modify_count_by_sum 316 |- !loop guard body c modify R. 317 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 318 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 319 !x. loop x = c + SUM (MAP body (loop_arg guard modify x)) 320 loop_modify_count_exit_by_sum 321 |- !loop guard body c exit modify R. 322 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 323 (!x. loop x = 324 if guard x then c 325 else body x + if exit x then 0 else loop (modify x)) ==> 326 !x. loop x <= c + SUM (MAP body (loop_arg guard modify x)) 327 loop_modify_count_quitc_eqn 328 |- !loop guard body c modify R. 329 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 330 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 331 !x. loop x = c + SUM 332 (GENLIST (\j. body (FUNPOW modify j x)) (loop_count guard modify x)) 333 loop_modify_count_quitc_exit_le 334 |- !loop guard body c exit modify R. 335 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 336 (!x. loop x = 337 if guard x then c 338 else body x + if exit x then 0 else loop (modify x)) ==> 339 !x. loop x <= c + SUM 340 (GENLIST (\j. body (FUNPOW modify j x)) (loop_count guard modify x)) 341 342 loop_modify_count_cover_exit_upper 343 |- !loop guard body c cover exit modify R. 344 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 345 (!x. body x <= cover x) /\ (!x y. R x y ==> cover x <= cover y) /\ 346 (!x. loop x = 347 if guard x then c 348 else body x + if exit x then 0 else loop (modify x)) ==> 349 !x. loop x <= c + cover x * loop_count guard modify x 350 loop_modify_count_exit_upper 351 |- !loop guard body c exit modify R. 352 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 353 (!x y. R x y ==> body x <= body y) /\ 354 (!x. loop x = 355 if guard x then c 356 else body x + if exit x then 0 else loop (modify x)) ==> 357 !x. loop x <= c + body x * loop_count guard modify x 358 loop_modify_count_cover_upper 359 |- !loop guard body c cover modify R. 360 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 361 (!x. body x <= cover x) /\ (!x y. R x y ==> cover x <= cover y) /\ 362 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 363 !x. loop x <= c + cover x * loop_count guard modify x 364 loop_modify_count_upper 365 |- !loop guard body c modify R. 366 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 367 (!x y. R x y ==> body x <= body y) /\ 368 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 369 !x. loop x <= c + body x * loop_count guard modify x 370 371 General Theory of Recurrence with 2 arguments: 372 loop2_arg_def |- !guard modify transform x y. loop2_arg guard modify transform x y = 373 loop_arg (\(x,y). guard x y) (\(x,y). (transform x,modify y)) (x,y) 374 loop2_arg_thm |- !transform modify guard R. WF R /\ 375 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> 376 !x y. loop2_arg guard modify transform x y = 377 if guard x y then [] 378 else (x,y):: loop2_arg guard modify transform (transform x) (modify y) 379 loop2_arg_nil |- !transform modify guard R. WF R /\ 380 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> 381 !x y. guard x y ==> loop2_arg guard modify transform x y = [] 382 loop2_arg_cons |- !transform modify guard R. WF R /\ 383 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> 384 !x y. ~guard x y ==> loop2_arg guard modify transform x y = 385 (x,y):: loop2_arg guard modify transform (transform x) (modify y) 386 loop2_arg_length |- !transform modify guard R. WF R /\ 387 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> 388 !x y. LENGTH (loop2_arg guard modify transform x y) = 389 loop2_count guard modify transform x y 390 loop2_arg_eqn |- !transform modify guard R. WF R /\ 391 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> 392 !x y. loop2_arg guard modify transform x y = 393 GENLIST (\j. (FUNPOW transform j x,FUNPOW modify j y)) 394 (loop2_count guard modify transform x y) 395 loop2_arg_element |- !transform modify guard R. WF R /\ 396 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> 397 !x y k. k < loop2_count guard modify transform x y ==> 398 EL k (loop2_arg guard modify transform x y) = 399 (FUNPOW transform k x,FUNPOW modify k y) 400 loop2_arg_cover_sum |- !transform modify guard cover R. WF R /\ 401 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 402 (!x1 x2 y1 y2. R (x1,y1) (x2,y2) ==> cover x1 y1 <= cover x2 y2) ==> 403 !x y. SUM (MAP (UNCURRY cover) (loop2_arg guard modify transform x y)) <= 404 SUM (MAP (K (cover x y)) (loop2_arg guard modify transform x y)) 405 loop2_modify_count_by_sum 406 |- !loop guard body c modify transform R. WF R /\ 407 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 408 (!x y. loop x y = 409 if guard x y then c 410 else body x y + loop (transform x) (modify y)) ==> 411 !x y. loop x y = c + 412 SUM (MAP (UNCURRY body) (loop2_arg guard modify transform x y)) 413 loop2_modify_count_exit_by_sum 414 |- !loop guard body c exit modify transform R. WF R /\ 415 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 416 (!x y. loop x y = 417 if guard x y then c 418 else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 419 !x y. loop x y <= c + 420 SUM (MAP (UNCURRY body) (loop2_arg guard modify transform x y)) 421 loop2_modify_count_quitc_eqn 422 |- !loop guard body c modify transform R. WF R /\ 423 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 424 (!x y. loop x y = 425 if guard x y then c 426 else body x y + loop (transform x) (modify y)) ==> 427 !x y. loop x y = c + SUM (GENLIST 428 (\j. body (FUNPOW transform j x) (FUNPOW modify j y)) 429 (loop2_count guard modify transform x y)) 430 loop2_modify_count_quitc_exit_le 431 |- !loop guard body c exit modify transform R. WF R /\ 432 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 433 (!x y. loop x y = 434 if guard x y then c 435 else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 436 !x y. loop x y <= c + SUM (GENLIST 437 (\j. body (FUNPOW transform j x) (FUNPOW modify j y)) 438 (loop2_count guard modify transform x y)) 439 loop2_modify_count_bcover_exit_upper 440 |- !loop guard body c exit bcover modify transform R. WF R /\ 441 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 442 (!x y. body x y <= bcover x y) /\ 443 (!x1 x2 y1 y2. R (x1,y1) (x2,y2) ==> bcover x1 y1 <= bcover x2 y2) /\ 444 (!x y. loop x y = 445 if guard x y then c 446 else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 447 !x y. loop x y <= c + bcover x y * loop2_count guard modify transform x y 448 loop2_modify_count_exit_upper 449 |- !loop guard body c exit modify transform R. WF R /\ 450 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 451 (!x1 x2 y1 y2. R (x1,y1) (x2,y2) ==> body x1 y1 <= body x2 y2) /\ 452 (!x y. loop x y = 453 if guard x y then c 454 else body x y + 455 if exit x y then 0 else loop (transform x) (modify y)) ==> 456 !x y. loop x y <= c + body x y * loop2_count guard modify transform x y 457 loop2_modify_count_bcover_upper 458 |- !loop guard body c bcover modify transform R. WF R /\ 459 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 460 (!x y. body x y <= bcover x y) /\ 461 (!x1 x2 y1 y2. R (x1,y1) (x2,y2) ==> bcover x1 y1 <= bcover x2 y2) /\ 462 (!x y. loop x y = 463 if guard x y then c 464 else body x y + loop (transform x) (modify y)) ==> 465 !x y. loop x y <= c + bcover x y * loop2_count guard modify transform x y 466 loop2_modify_count_upper 467 |- !loop guard body c modify transform R. WF R /\ 468 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 469 (!x1 x2 y1 y2. R (x1,y1) (x2,y2) ==> body x1 y1 <= body x2 y2) /\ 470 (!x y. loop x y = 471 if guard x y then c 472 else body x y + loop (transform x) (modify y)) ==> 473 !x y. loop x y <= c + body x y * loop2_count guard modify transform x y 474 475 Numeric Loops with RISING modify: 476 loop_rise_count_cover_quitc_exit_le 477 |- !loop guard body c exit modify transform R. WF R /\ 478 (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 479 (!x. loop x = 480 if guard x then c 481 else body x + if exit x then 0 else loop (modify x)) ==> 482 !x cover. (let n = loop_count guard modify x 483 in (!x. body x <= cover x) /\ MONO cover ==> 484 loop x <= c + n * cover (FUNPOW modify n x)) 485 loop_rise_count_exit_le 486 |- !loop guard body c exit modify transform R. WF R /\ 487 (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 488 (!x. loop x = 489 if guard x then c 490 else body x + if exit x then 0 else loop (modify x)) ==> 491 !x. (let n = loop_count guard modify x 492 in MONO body ==> loop x <= c + n * body (FUNPOW modify n x)) 493 loop_rise_count_cover_le 494 |- !loop guard body c modify transform R. WF R /\ 495 (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 496 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 497 !x cover. (let n = loop_count guard modify x 498 in (!x. body x <= cover x) /\ MONO cover ==> 499 loop x <= c + n * cover (FUNPOW modify n x)) 500 loop_rise_count_le |- !loop guard body c modify transform R. WF R /\ 501 (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 502 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 503 !x. (let n = loop_count guard modify x 504 in MONO body ==> loop x <= c + n * body (FUNPOW modify n x)) 505 loop_rise_count_rcover_quitc_exit_le 506 |- !loop guard body c exit modify transform R. WF R /\ 507 (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 508 (!x. loop x = 509 if guard x then c 510 else body x + if exit x then 0 else loop (modify x)) ==> 511 !x cover. (let n = loop_count guard modify x 512 in (!x. body x <= cover x) /\ RMONO cover ==> 513 loop x <= c + n * cover x) 514 loop_rise_count_rbody_exit_le 515 |- !loop guard body c exit modify transform R. WF R /\ 516 (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 517 (!x. loop x = 518 if guard x then c 519 else body x + if exit x then 0 else loop (modify x)) ==> 520 !x. (let n = loop_count guard modify x 521 in RMONO body ==> loop x <= c + n * body x) 522 loop_rise_count_rcover_le 523 |- !loop guard body c modify transform R. WF R /\ 524 (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 525 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 526 !x cover. (let n = loop_count guard modify x 527 in (!x. body x <= cover x) /\ RMONO cover ==> 528 loop x <= c + n * cover x) 529 loop_rise_count_rbody_le 530 |- !loop guard body c modify transform R. WF R /\ 531 (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 532 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 533 !x. (let n = loop_count guard modify x 534 in RMONO body ==> loop x <= c + n * body x) 535 536 Numeric Loops with FALLING modify: 537 loop_fall_count_cover_quitc_exit_le 538 |- !loop guard body c exit modify transform R. WF R /\ 539 (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 540 (!x. loop x = 541 if guard x then c 542 else body x + if exit x then 0 else loop (modify x)) ==> 543 !x cover. (let n = loop_count guard modify x 544 in (!x. body x <= cover x) /\ MONO cover ==> 545 loop x <= c + n * cover x) 546 loop_fall_count_exit_le 547 |- !loop guard body c exit modify transform R. WF R /\ 548 (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 549 (!x. loop x = 550 if guard x then c 551 else body x + if exit x then 0 else loop (modify x)) ==> 552 !x. (let n = loop_count guard modify x 553 in MONO body ==> loop x <= c + n * body x) 554 loop_fall_count_cover_le 555 |- !loop guard body c modify transform R. WF R /\ 556 (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 557 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 558 !x cover. (let n = loop_count guard modify x 559 in (!x. body x <= cover x) /\ MONO cover ==> 560 loop x <= c + n * cover x) 561 loop_fall_count_le |- !loop guard body c modify transform R. WF R /\ 562 (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 563 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 564 !x. (let n = loop_count guard modify x 565 in MONO body ==> loop x <= c + n * body x) 566 loop_fall_count_rcover_quitc_exit_le 567 |- !loop guard body c exit modify transform R. WF R /\ 568 (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 569 (!x. loop x = 570 if guard x then c 571 else body x + if exit x then 0 else loop (modify x)) ==> 572 !x cover. (let n = loop_count guard modify x 573 in (!x. body x <= cover x) /\ RMONO cover ==> 574 loop x <= c + n * cover (FUNPOW modify n x)) 575 loop_fall_count_rbody_exit_le 576 |- !loop guard body c exit modify transform R. WF R /\ 577 (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 578 (!x. loop x = 579 if guard x then c 580 else body x + if exit x then 0 else loop (modify x)) ==> 581 !x. (let n = loop_count guard modify x 582 in RMONO body ==> loop x <= c + n * body (FUNPOW modify n x)) 583 loop_fall_count_rcover_le 584 |- !loop guard body c modify transform R. WF R /\ 585 (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 586 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 587 !x cover. (let n = loop_count guard modify x 588 in (!x. body x <= cover x) /\ RMONO cover ==> 589 loop x <= c + n * cover (FUNPOW modify n x)) 590 loop_fall_count_rbody_le 591 |- !loop guard body c modify transform R. WF R /\ 592 (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 593 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 594 !x. (let n = loop_count guard modify x 595 in RMONO body ==> loop x <= c + n * body (FUNPOW modify n x)) 596 597 Numeric Loops with RISING transform and FALLING modify: 598 loop2_rise_fall_count_cover_quitc_exit_le 599 |- !loop guard body c exit modify transform R. WF R /\ 600 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 601 RISING transform /\ FALLING modify /\ 602 (!x y. loop x y = 603 if guard x y then c 604 else body x y + 605 if exit x y then 0 else loop (transform x) (modify y)) ==> 606 !x y cover. (let n = loop2_count guard modify transform x y 607 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 608 loop x y <= c + n * cover (FUNPOW transform n x) y) 609 loop2_rise_fall_count_exit_le 610 |- !loop guard body c exit modify transform R. WF R /\ 611 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 612 RISING transform /\ FALLING modify /\ 613 (!x y. loop x y = 614 if guard x y then c 615 else body x y + 616 if exit x y then 0 else loop (transform x) (modify y)) ==> 617 !x y. (let n = loop2_count guard modify transform x y 618 in MONO2 body ==> loop x y <= c + n * body (FUNPOW transform n x) y) 619 loop2_rise_fall_count_cover_le 620 |- !loop guard body c modify transform R. WF R /\ 621 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 622 RISING transform /\ FALLING modify /\ 623 (!x y. loop x y = 624 if guard x y then c 625 else body x y + loop (transform x) (modify y)) ==> 626 !x y cover. (let n = loop2_count guard modify transform x y 627 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 628 loop x y <= c + n * cover (FUNPOW transform n x) y) 629 loop2_rise_fall_count_le 630 |- !loop guard body c modify transform R. WF R /\ 631 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 632 RISING transform /\ FALLING modify /\ 633 (!x y. loop x y = 634 if guard x y then c 635 else body x y + loop (transform x) (modify y)) ==> 636 !x y. (let n = loop2_count guard modify transform x y 637 in MONO2 body ==> loop x y <= c + n * body (FUNPOW transform n x) y) 638 639 Numeric Loops with FALLING transform and FALLING modify: 640 loop2_fall_fall_count_cover_quitc_exit_le 641 |- !loop guard body c exit modify transform R. WF R /\ 642 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 643 FALLING transform /\ FALLING modify /\ 644 (!x y. loop x y = 645 if guard x y then c 646 else body x y + 647 if exit x y then 0 else loop (transform x) (modify y)) ==> 648 !x y cover. (let n = loop2_count guard modify transform x y 649 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 650 loop x y <= c + n * cover x y) 651 loop2_fall_fall_count_exit_le 652 |- !loop guard body c exit modify transform R. WF R /\ 653 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 654 FALLING transform /\ FALLING modify /\ 655 (!x y. loop x y = 656 if guard x y then c 657 else body x y + 658 if exit x y then 0 else loop (transform x) (modify y)) ==> 659 !x y. (let n = loop2_count guard modify transform x y in 660 MONO2 body ==> loop x y <= c + n * body x y) 661 loop2_fall_fall_count_cover_le 662 |- !loop guard body c modify transform R. WF R /\ 663 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 664 FALLING transform /\ FALLING modify /\ 665 (!x y. loop x y = 666 if guard x y then c 667 else body x y + loop (transform x) (modify y)) ==> 668 !x y cover. (let n = loop2_count guard modify transform x y 669 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 670 loop x y <= c + n * cover x y) 671 loop2_fall_fall_count_le 672 |- !loop guard body c modify transform R. WF R /\ 673 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 674 FALLING transform /\ FALLING modify /\ 675 (!x y. loop x y = 676 if guard x y then c 677 else body x y + loop (transform x) (modify y)) ==> 678 !x y. (let n = loop2_count guard modify transform x y 679 in MONO2 body ==> loop x y <= c + n * body x y) 680 681 Numeric Loops with FALLING transform and RISING modify: 682 loop2_fall_rise_count_cover_quitc_exit_le 683 |- !loop guard body c exit modify transform R. WF R /\ 684 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 685 FALLING transform /\ RISING modify /\ 686 (!x y. loop x y = 687 if guard x y then c 688 else body x y + 689 if exit x y then 0 else loop (transform x) (modify y)) ==> 690 !x y cover. (let n = loop2_count guard modify transform x y 691 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 692 loop x y <= c + n * cover x (FUNPOW modify n y)) 693 loop2_fall_rise_count_exit_le 694 |- !loop guard body c exit modify transform R. WF R /\ 695 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 696 FALLING transform /\ RISING modify /\ 697 (!x y. loop x y = 698 if guard x y then c 699 else body x y + 700 if exit x y then 0 else loop (transform x) (modify y)) ==> 701 !x y. (let n = loop2_count guard modify transform x y 702 in MONO2 body ==> loop x y <= c + n * body x (FUNPOW modify n y)) 703 loop2_fall_rise_count_cover_le 704 |- !loop guard body c modify transform R. WF R /\ 705 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 706 FALLING transform /\ RISING modify /\ 707 (!x y. loop x y = 708 if guard x y then c 709 else body x y + loop (transform x) (modify y)) ==> 710 !x y cover. (let n = loop2_count guard modify transform x y 711 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 712 loop x y <= c + n * cover x (FUNPOW modify n y)) 713 loop2_fall_rise_count_le 714 |- !loop guard body c modify transform R. WF R /\ 715 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 716 FALLING transform /\ RISING modify /\ 717 (!x y. loop x y = 718 if guard x y then c 719 else body x y + loop (transform x) (modify y)) ==> 720 !x y. (let n = loop2_count guard modify transform x y 721 in MONO2 body ==> loop x y <= c + n * body x (FUNPOW modify n y)) 722 723 Numeric Loops with RISING transform and RISING modify: 724 loop2_rise_rise_count_cover_quitc_exit_le 725 |- !loop guard body c exit modify transform R. WF R /\ 726 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 727 RISING transform /\ RISING modify /\ 728 (!x y. loop x y = 729 if guard x y then c 730 else body x y + 731 if exit x y then 0 else loop (transform x) (modify y)) ==> 732 !x y cover. (let n = loop2_count guard modify transform x y 733 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 734 loop x y <= c + n * cover (FUNPOW transform n x) (FUNPOW modify n y)) 735 loop2_rise_rise_count_exit_le 736 |- !loop guard body c exit modify transform R. WF R /\ 737 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 738 RISING transform /\ RISING modify /\ 739 (!x y. loop x y = 740 if guard x y then c 741 else body x y + 742 if exit x y then 0 else loop (transform x) (modify y)) ==> 743 !x y. (let n = loop2_count guard modify transform x y 744 in MONO2 body ==> 745 loop x y <= c + n * body (FUNPOW transform n x) (FUNPOW modify n y)) 746 loop2_rise_rise_count_cover_le 747 |- !loop guard body c modify transform R. WF R /\ 748 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 749 RISING transform /\ RISING modify /\ 750 (!x y. loop x y = 751 if guard x y then c 752 else body x y + loop (transform x) (modify y)) ==> 753 !x y cover. (let n = loop2_count guard modify transform x y 754 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 755 loop x y <= c + n * cover (FUNPOW transform n x) (FUNPOW modify n y)) 756 loop2_rise_rise_count_le 757 |- !loop guard body c modify transform R. WF R /\ 758 (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 759 RISING transform /\ RISING modify /\ 760 (!x y. loop x y = 761 if guard x y then c 762 else body x y + loop (transform x) (modify y)) ==> 763 !x y. (let n = loop2_count guard modify transform x y 764 in MONO2 body ==> 765 loop x y <= c + n * body (FUNPOW transform n x) (FUNPOW modify n y)) 766*) 767 768(* ------------------------------------------------------------------------- *) 769(* Description *) 770(* ------------------------------------------------------------------------- *) 771 772(* 773 774The basic recurrence pattern for a (loop:'a -> num) is this: 775 776!x. loop x = if guard x then quit x else body x + loop (modify x) 777 778where a well-founded R relates x and (modify x) when (guard x) is false: 779WF R /\ (!x. ~guard x ==> R (modify x) x) 780 781The recurrence means: 782 loop x = body x + body (modify x) + body (modify (modify x)) + .... 783 ... (until guard x is true for last x) ... + quit (last x) 784 = quit (last x) + SUM (GENLIST (\j. body (FUNPOW modify j x)) (count-to-last)) 785 786To get hold of the count-to-last, define (loop_count x) by a schema: 787 loop_count x = if guard x then 0 else SUC (loop_count (modify x)) 788 789which is in sync with the loop behaviour. 790 791With these two, we have the fundamental result: 792 793 loop_modify_count_eqn 794 |- !loop guard body quit modify R. WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 795 (!x. loop x = if guard x then quit x else body x + loop (modify x)) ==> 796 !x. loop x = quit (FUNPOW modify (loop_count guard modify x) x) + 797 SUM (GENLIST (\j. body (FUNPOW modify j x)) (loop_count guard modify x)) 798 799Let n = loop_count guard modify x, this can be expressed as: 800 801 loop x = quit ((modify ** n) x) + SIGMA (0 .. n) (\j. body (modify ** j x)) 802 803All other variations, e.g. 804with exit: if exit x then 0 else loop (modify x) 805with cover: !x. body x <= cover x 806with two arguments: 807 !x y. loop x y = if guard x y then quit x y else body x y + loop (transform x) (modify y) 808with three arguments: 809 !x y z. loop x y z = if guard x y z then quit x y z 810 else body x y z + loop (convert x) (transform y) (modify z) 811 812are drived from this basic pattern. 813 814*) 815 816(* ------------------------------------------------------------------------- *) 817(* Helper *) 818(* ------------------------------------------------------------------------- *) 819 820(* Eliminate parenthesis around equality *) 821val _ = ParseExtras.tight_equality(); 822 823(* ------------------------------------------------------------------------- *) 824(* Loop Count for recurrence *) 825(* ------------------------------------------------------------------------- *) 826 827(* Define a loop count corresponding to the length of a loop argument list *) 828(* Use a schema to figure out the hypothesis. *) 829val loop_count_def = TotalDefn.DefineSchema` 830 loop_count (x:'a) = 831 if guard x then 0 else SUC (loop_count (modify x)) 832`; 833(* 834val loop_count_def = 835 [..] |- !x. loop_count guard modify x = 836 if guard x then 0 else SUC (loop_count guard modify (modify x)): thm 837to see the [..], which is hypothesis, 838> hyp loop_count_def; 839val it = [``!x. ~guard x ==> R (modify x) x``, ``WF R``]: term list 840*) 841 842(* Obtain theorem from loop_count definition *) 843val loop_count_thm = save_thm("loop_count_thm", 844 loop_count_def |> DISCH_ALL |> SIMP_RULE bool_ss [AND_IMP_INTRO] |> GEN_ALL); 845(* val loop_count_thm = 846 |- !modify guard R. WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 847 !x. loop_count guard modify x = 848 if guard x then 0 else SUC (loop_count guard modify (modify x)): thm 849*) 850 851(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 852 !x. guard x ==> (loop_count guard modify x = 0) *) 853(* Proof: by loop_count_def *) 854val loop_count_0 = store_thm( 855 "loop_count_0", 856 ``!modify guard R. WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 857 !x. guard x ==> (loop_count guard modify x = 0)``, 858 rpt strip_tac >> 859 rw[Once loop_count_def]); 860 861(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 862 !x. ~guard x ==> (loop_count guard modify x = SUC (loop_count guard modify (modify x))) *) 863(* Proof: by loop_count_def *) 864val loop_count_suc = store_thm( 865 "loop_count_suc", 866 ``!modify guard R. WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 867 !x. ~guard x ==> (loop_count guard modify x = SUC (loop_count guard modify (modify x)))``, 868 rpt strip_tac >> 869 rw[Once loop_count_def]); 870 871(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 872 !x. guard (FUNPOW modify (loop_count guard modify x) x) *) 873(* Proof: 874 If guard x, 875 guard (FUNPOW modify (loop_count guard modify x) x) 876 <=> guard (FUNPOW modify 0 x) by loop_count_0 877 <=> guard x by FUNPOW_0 878 <=> T by this case, guard x. 879 If ~guard x, 880 guard (FUNPOW modify (loop_count guard modify x) x) 881 <=> guard (FUNPOW modify (SUC (loop_count guard modify (modify x))) x) by loop_count_suc 882 <=> guard (FUNPOW modify (loop_count guard modify (modify x)) (modify x)) by FUNPOW 883 <=> T by induction hypothesis 884*) 885val loop_count_iterating = store_thm( 886 "loop_count_iterating", 887 ``!modify guard R. WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 888 !x. guard (FUNPOW modify (loop_count guard modify x) x)``, 889 ntac 4 strip_tac >> 890 ho_match_mp_tac (theorem "loop_count_ind") >> 891 rw[] >> 892 Cases_on `guard x` >- 893 metis_tac[loop_count_0, FUNPOW_0] >> 894 qabbrev_tac `n = loop_count guard modify (modify x)` >> 895 `guard (FUNPOW modify (loop_count guard modify x) x) <=> guard (FUNPOW modify (SUC n) x)` by metis_tac[loop_count_suc] >> 896 metis_tac[FUNPOW]); 897 898(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) ==> ?n. guard (FUNPOW modify n x) *) 899(* Proof: 900 By contradiction, suppose that: !n. ~guard (FUNPOW modify n x). 901 Let s = IMAGE (\n. FUNPOW modify n x) univ(:num). 902 that is, all the iterations of x by modify. 903 Note WF R means 904 !B. (?w. B w) ==> ?min. B min /\ !b. R b min ==> ~B b by WF_DEF 905 Let the B be s, we need to show: 906 (1) ?w. s w find a witness 907 Since the set s is non-empty -- it is the image of a universal set, 908 any element of s is a witness. 909 (2) ?min. s min /\ !b. R b min ==> ~s b 910 This means: (!n. min <> FUNPOW modify n x) \/ ?b. R b min /\ ?n. b = FUNPOW modify n x 911 which is: min = FUNPOW modify n x ==> ?b. R b min /\ ?n. b = FUNPOW modify n x 912 or ?k. R (FUNPOW modify k x) R b min, where min = FUNPOW modify n x. 913 that is, ?k. R (FUNPOW modify k x) (FUNPOW modify n x) 914 Take k = SUC n, then R (FUNPOW modify (SUC n) x) (FUNPOW modify n x) 915 since putting y = FUNPOW modify n x, 916 we have ~guard y by our assumption of contradiction 917 ==> R (modify y) y by given !x. ~guard x ==> R (modify x) x 918 and modify y = modify (FUNPOW modify n x) 919 = FUNPOW modify (SUC n) x by FUNPOW_SUC 920*) 921val loop_count_exists = store_thm( 922 "loop_count_exists", 923 ``!modify guard R. WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 924 !x. ?n. guard (FUNPOW modify n x)``, 925 spose_not_then strip_assume_tac >> 926 qabbrev_tac `s = IMAGE (\n. FUNPOW modify n x) univ(:num)` >> 927 fs[relationTheory.WF_DEF] >> 928 first_x_assum (qspec_then `s` mp_tac) >> 929 impl_tac >- 930 rw[Abbr`s`] >> 931 rw[Abbr`s`] >> 932 rw[DISJ_EQ_IMP] >> 933 simp[PULL_EXISTS] >> 934 qexists_tac `SUC n` >> 935 simp[FUNPOW_SUC]); 936 937(* Theorem:WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 938 !x n. guard (FUNPOW modify n x) /\ (!m. m < n ==> ~guard (FUNPOW modify m x)) ==> 939 (loop_count guard modify x = n) *) 940(* Proof: 941 By induction from loop_count_def. 942 If guard x, 943 loop_count guard modify x = 0 by loop_count_0 944 If n = 0, this is trivially true. 945 If n <> 0, then !m. m < n ==> ~guard (FUNPOW modify m x) cannot hold, 946 since m = 0 gives 947 ~guard (FUNPOW modify 0 x) 948 = ~guard x by FUNPOW_0 949 which contradicts guard x. 950 If ~guard x, 951 loop_count guard modify x 952 = SUC (loop_count guard modify (modify x)) by loop_count_suc 953 Now n <> 0, 954 since guard (FUNPOW modify 0 x) gives guard x by FUNPOW_0 955 which contradicts ~guard x. 956 Let n = SUC k. 957 Then guard (FUNPOW modify (SUC k)) /\ 958 !m. m < SUC k ==> ~guard (FUNPOW modify m x) 959 The first one gives 960 guard (FUNPOW modify k (modify x)) by !x. ~guard x ==> R (modify x) x 961 The implication gives 962 !m. m < k ==> ~guard (FUNPOW modify m (modify x)) by putting (SUC m), FUNPOW 963 Thus loop_count guard modify (modify x) = k by induction hypothesis 964 or loop_count guard modify x = SUC k = n. 965*) 966val loop_count_minimal = store_thm( 967 "loop_count_minimal", 968 ``!modify guard R. WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 969 !x n. guard (FUNPOW modify n x) /\ (!m. m < n ==> ~guard (FUNPOW modify m x)) ==> 970 (loop_count guard modify x = n)``, 971 ntac 4 strip_tac >> 972 ho_match_mp_tac (theorem "loop_count_ind") >> 973 rw[] >> 974 rw[Once loop_count_def] >| [ 975 (Cases_on `n` >> fs[]) >> 976 first_x_assum (qspec_then `0` mp_tac) >> 977 simp[], 978 fs[] >> 979 (Cases_on `n` >> fs[]) >> 980 first_x_assum irule >> 981 fs[FUNPOW] >> 982 rpt strip_tac >> 983 first_x_assum (qspec_then `SUC m` mp_tac) >> 984 simp[FUNPOW] 985 ]); 986 987(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 988 !x. loop_count guard modify x = LEAST n. guard (FUNPOW modify n x) *) 989(* Proof: 990 By LEAST elimination, this is to show: 991 (1) ?n. guard (FUNPOW modify n x)), true by loop_count_exists 992 (2) !n. (!m. m < n ==> ~guard (FUNPOW modify m x)) /\ guard (FUNPOW modify n x) ==> 993 loop_count guard modify x = n, true by loop_count_minimal 994*) 995val loop_count_eqn = store_thm( 996 "loop_count_eqn", 997 ``!modify guard R. WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 998 !x. loop_count guard modify x = LEAST n. guard (FUNPOW modify n x)``, 999 rpt strip_tac >> 1000 numLib.LEAST_ELIM_TAC >> 1001 rpt strip_tac >- 1002 metis_tac[loop_count_exists] >> 1003 metis_tac[loop_count_minimal]); 1004 1005(* ------------------------------------------------------------------------- *) 1006(* Direct derivation of general results from loop_count. *) 1007(* ------------------------------------------------------------------------- *) 1008 1009(* ------------------------------------------------------------------------- *) 1010(* General Theory of Recurrence with 1 argument *) 1011(* ------------------------------------------------------------------------- *) 1012 1013(* Note: basic solution of the recurrence: 1014 1015 Given: !x. loop x = if guard x then quit x else body x + loop (modify x) 1016 Then: loop x = SUM [body x, body (modify x), body (modify (modify x)), .....] + 1017 quit (last modify x) 1018 for n terms, where n = loop_count guard modify x 1019 and last modify x = x after n modify 1020 Thus: loop x = quit (FUNPOW modify n x) + SUM (GENLIST (\j. body (FUNPOW modify j x)) n) 1021*) 1022 1023 1024(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 1025 (!x. loop x = if guard x then quit x else body x + loop (modify x)) ==> 1026 !x. loop x = quit (FUNPOW modify (loop_count guard modify x) x) + 1027 SUM (GENLIST (\j. body (FUNPOW modify j x)) (loop_count guard modify x)) *) 1028(* Proof: 1029 By induction from loop_count_def. 1030 Let f = (\j. body (FUNPOW modify j x)), 1031 n = loop_count guard modify x. 1032 If guard x, 1033 Then n = 0 by loop_count_0 1034 LHS = loop x = quit x by given loop x, guard x 1035 RHS = quit (FUNPOW modify 0 x) + SUM (GENLIST f 0) 1036 = quit x + SUM [] by FUNPOW_0, GENLIST_0 1037 = quit x + 0 = LHS by SUM 1038 If ~guard x, 1039 Let g = (\j. body (FUNPOW modify j (modify x))), 1040 m = loop_count guard modify (modify x). 1041 Note n = SUC m by loop_count_suc 1042 and g = f o SUC by FUN_EQ_THM, FUNPOW 1043 and f 0 = body x by notation 1044 loop x 1045 = body x + loop (modify x) by given loop x, ~guard x 1046 = body x + (quit (FUNPOW modify m (modify x)) + SUM (GENLIST g m)) by induction hypothesis 1047 = quit (FUNPOW modify m (modify x)) + (body x + SUM (GENLIST g m)) by arithmetic 1048 = quit (FUNPOW modify n x) + (f 0 + SUM (GENLIST (f o SUC) m)) by FUNPOW 1049 = quit (FUNPOW modify n x) + (SUM (f 0 :: GENLIST (f o SUC) m)) by SUM 1050 = quit (FUNPOW modify n x) + SUM (GENLIST f n) by GENLIST_CONS 1051*) 1052val loop_modify_count_eqn = store_thm( 1053 "loop_modify_count_eqn", 1054 ``!loop guard body quit modify R. 1055 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 1056 (!x. loop x = if guard x then quit x else body x + loop (modify x)) ==> 1057 !x. loop x = quit (FUNPOW modify (loop_count guard modify x) x) + 1058 SUM (GENLIST (\j. body (FUNPOW modify j x)) (loop_count guard modify x))``, 1059 ntac 7 strip_tac >> 1060 ho_match_mp_tac (theorem "loop_count_ind") >> 1061 rpt strip_tac >> 1062 Cases_on `guard x` >| [ 1063 `loop x = quit x` by metis_tac[] >> 1064 `loop_count guard modify x = 0` by metis_tac[loop_count_0] >> 1065 simp[], 1066 qabbrev_tac `f = \j. body (FUNPOW modify j x)` >> 1067 qabbrev_tac `n = loop_count guard modify x` >> 1068 qabbrev_tac `g = \j. body (FUNPOW modify j (modify x))` >> 1069 qabbrev_tac `m = loop_count guard modify (modify x)` >> 1070 `n = SUC m` by metis_tac[loop_count_suc] >> 1071 `g = f o SUC` by rw[FUN_EQ_THM, FUNPOW, Abbr`f`, Abbr`g`] >> 1072 `f 0 = body x` by rw[Abbr`f`] >> 1073 `loop x = body x + loop (modify x)` by metis_tac[] >> 1074 `_ = quit (FUNPOW modify m (modify x)) + (body x + SUM (GENLIST g m))` by rw[] >> 1075 `_ = quit (FUNPOW modify n x) + (f 0 + SUM (GENLIST (f o SUC) m))` by rw[FUNPOW] >> 1076 `_ = quit (FUNPOW modify n x) + SUM (GENLIST f n)` by rw[GENLIST_CONS] >> 1077 decide_tac 1078 ]); 1079 1080(* Theorem: Equivalent form of loop_modify_count_eqn *) 1081(* Proof: by loop_modify_count_eqn *) 1082val loop_modify_count_eqn_1 = store_thm( 1083 "loop_modify_count_eqn_1", 1084 ``!loop guard body quit modify R. 1085 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 1086 (!x. loop x = if guard x then quit x else body x + loop (modify x)) ==> 1087 !x. let n = loop_count guard modify x in 1088 loop x = quit (FUNPOW modify n x) + SUM (GENLIST (\j. body (FUNPOW modify j x)) n)``, 1089 metis_tac[loop_modify_count_eqn]); 1090 1091(* Theorem: Equivalent form of loop_modify_count_eqn *) 1092(* Proof: by loop_modify_count_eqn *) 1093val loop_modify_count_eqn_2 = store_thm( 1094 "loop_modify_count_eqn_2", 1095 ``!loop guard body quit modify R. 1096 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 1097 (!x. loop x = if guard x then quit x else body x + loop (modify x)) ==> 1098 !x. let n = loop_count guard modify x in 1099 loop x = quit (FUNPOW modify n x) + SIGMA (\j. body (FUNPOW modify j x)) (count n)``, 1100 metis_tac[loop_modify_count_eqn_1, SUM_GENLIST]); 1101 1102(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 1103 (!x. loop x = if guard x then quit x else body x + if exit x then 0 else loop (modify x)) ==> 1104 !x. loop x <= quit (FUNPOW modify (loop_count guard modify x) x) + 1105 SUM (GENLIST (\j. body (FUNPOW modify j x)) (loop_count guard modify x)) *) 1106(* Proof: 1107 By induction from loop_count_def. 1108 Let f = (\j. body (FUNPOW modify j x)), 1109 n = loop_count guard modify x. 1110 If guard x, 1111 Then n = 0 by loop_count_0 1112 LHS = loop x = quit x by given loop x, guard x 1113 RHS = quit (FUNPOW modify 0 x) + SUM (GENLIST f 0) 1114 = quit x + SUM [] by FUNPOW_0, GENLIST_0 1115 = quit x + 0 by SUM 1116 Thus LHS <= RHS. 1117 If ~guard x, 1118 Let g = (\j. body (FUNPOW modify j (modify x))), 1119 m = loop_count guard modify (modify x). 1120 Note n = SUC m by loop_count_suc 1121 and g = f o SUC by FUN_EQ_THM, FUNPOW 1122 and f 0 = body x by notation 1123 loop x 1124 = body x + if exit x then 0 else loop (modify x) by given loop x, ~guard x 1125 <= body x + loop (modify x) by ignoring exit x 1126 <= body x + (quit (FUNPOW modify m (modify x)) + SUM (GENLIST g m)) by induction hypothesis 1127 = quit (FUNPOW modify m (modify x)) + (body x + SUM (GENLIST g m)) by arithmetic 1128 = quit (FUNPOW modify n x) + (f 0 + SUM (GENLIST (f o SUC) m)) by FUNPOW 1129 = quit (FUNPOW modify n x) + (SUM (f 0 :: GENLIST (f o SUC) m)) by SUM 1130 = quit (FUNPOW modify n x) + SUM (GENLIST f n) by GENLIST_CONS 1131*) 1132val loop_modify_count_exit_le = store_thm( 1133 "loop_modify_count_exit_le", 1134 ``!loop guard body quit exit modify R. 1135 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 1136 (!x. loop x = if guard x then quit x else body x + if exit x then 0 else loop (modify x)) ==> 1137 !x. loop x <= quit (FUNPOW modify (loop_count guard modify x) x) + 1138 SUM (GENLIST (\j. body (FUNPOW modify j x)) (loop_count guard modify x))``, 1139 ntac 8 strip_tac >> 1140 ho_match_mp_tac (theorem "loop_count_ind") >> 1141 rpt strip_tac >> 1142 Cases_on `guard x` >| [ 1143 `loop x = quit x` by metis_tac[] >> 1144 `loop_count guard modify x = 0` by metis_tac[loop_count_0] >> 1145 simp[], 1146 qabbrev_tac `f = \j. body (FUNPOW modify j x)` >> 1147 qabbrev_tac `n = loop_count guard modify x` >> 1148 qabbrev_tac `g = \j. body (FUNPOW modify j (modify x))` >> 1149 qabbrev_tac `m = loop_count guard modify (modify x)` >> 1150 `n = SUC m` by metis_tac[loop_count_suc] >> 1151 `g = f o SUC` by rw[FUN_EQ_THM, FUNPOW, Abbr`f`, Abbr`g`] >> 1152 `f 0 = body x` by rw[Abbr`f`] >> 1153 `loop x = body x + if exit x then 0 else loop (modify x)` by metis_tac[] >> 1154 `(body x + if exit x then 0 else loop (modify x)) <= body x + loop (modify x)` by decide_tac >> 1155 `loop x <= body x + loop (modify x)` by metis_tac[] >> 1156 `loop (modify x) <= quit (FUNPOW modify m (modify x)) + SUM (GENLIST g m)` by rw[] >> 1157 `loop x <= quit (FUNPOW modify m (modify x)) + (body x + SUM (GENLIST g m))` by decide_tac >> 1158 `quit (FUNPOW modify m (modify x)) + (body x + SUM (GENLIST g m)) = 1159 quit (FUNPOW modify n x) + (f 0 + SUM (GENLIST (f o SUC) m))` by rw[FUNPOW] >> 1160 `_ = quit (FUNPOW modify n x) + SUM (GENLIST f n)` by rw[GENLIST_CONS] >> 1161 decide_tac 1162 ]); 1163 1164(* ------------------------------------------------------------------------- *) 1165(* Estimation for Numeric Loops *) 1166(* ------------------------------------------------------------------------- *) 1167 1168(* Idea: 1169 1170 From loop_modify_count_eqn, let n = loop_count guard modify x. 1171 loop x 1172 = quit (last x) + SUM (GENLIST (\j. body (FUNPOW modify j x)) n) 1173 = quit (last x) + [body x, body (m x), body (m (m x)), ....] for n terms 1174 If FALLING m, 1175 <= quit (last x) + [body x, body x, body x, .....] if MONO body, 1176 = quit (last x) + n * body x 1177 If RISING m, 1178 <= quit (last x) + [body (last x), body (last x), ...] if MONO body, 1179 = quit (last x) + n * body (last x) 1180*) 1181 1182(* ------------------------------------------------------------------------- *) 1183(* Numeric Loops with RISING modify *) 1184(* ------------------------------------------------------------------------- *) 1185 1186(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 1187 (!x. loop x = if guard x then quit x else body x + if exit x then 0 else loop (modify x)) ==> 1188 !x cover. let n = loop_count guard modify x 1189 in (!x. body x <= cover x) /\ MONO cover ==> 1190 loop x <= quit (FUNPOW modify n x) + n * cover (FUNPOW modify n x) *) 1191(* Proof: 1192 Let f = (\j. body (FUNPOW modify j x)), 1193 n = loop_count guard modify x, 1194 z = FUNPOW modify n x. 1195 1196 For k < n, 1197 FUNPOW modify k x <= FUNPOW modify n x by FUNPOW_LE_RISING, RISING modify 1198 = z by notation 1199 Thus, 1200 loop x 1201 <= quit z + SUM (GENLIST f n) by loop_modify_count_quitc_exit_le 1202 <= quit z + SUM (GENLIST (K (cover z)) n) by SUM_LE, EL_GENLIST, RISING modify 1203 = quit z + (cover z) * n by SUM_GENLIST_K 1204 = quit z + n * cover z by MULT_COMM 1205*) 1206val loop_rise_count_cover_exit_le = store_thm( 1207 "loop_rise_count_cover_exit_le", 1208 ``!loop body quit exit guard modify R. 1209 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 1210 (!x. loop x = if guard x then quit x else body x + if exit x then 0 else loop (modify x)) ==> 1211 !x cover. let n = loop_count guard modify x 1212 in (!x. body x <= cover x) /\ MONO cover ==> 1213 loop x <= quit (FUNPOW modify n x) + n * cover (FUNPOW modify n x)``, 1214 rpt strip_tac >> 1215 qabbrev_tac `foo = !x. loop x = if guard x then quit x else body x + if exit x then 0 else loop (modify x)` >> 1216 simp[] >> 1217 unabbrev_all_tac >> 1218 rpt strip_tac >> 1219 imp_res_tac loop_modify_count_exit_le >> 1220 first_x_assum (qspec_then `x` strip_assume_tac) >> 1221 qabbrev_tac `f = \j. body (FUNPOW modify j x)` >> 1222 qabbrev_tac `n = loop_count guard modify x` >> 1223 qabbrev_tac `z = FUNPOW modify n x` >> 1224 `SUM (GENLIST f n) <= SUM (GENLIST (K (cover z)) n)` by 1225 (irule SUM_LE >> 1226 rw[] >> 1227 rw[Abbr`f`, Abbr`z`] >> 1228 `FUNPOW modify k x <= FUNPOW modify n x` by rw[FUNPOW_LE_RISING] >> 1229 qabbrev_tac `u = FUNPOW modify k x` >> 1230 qabbrev_tac `v = FUNPOW modify n x` >> 1231 `body u <= cover u` by rw[] >> 1232 `cover u <= cover v` by rw[] >> 1233 decide_tac) >> 1234 `SUM (GENLIST (K (cover z)) n) = cover z * n` by rw[SUM_GENLIST_K] >> 1235 decide_tac); 1236 1237(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 1238 (!x. loop x = if guard x then quit x else body x + if exit x then 0 else loop (modify x)) ==> 1239 !x cover. let n = loop_count guard modify x 1240 in (!x. body x <= cover x) /\ RMONO cover ==> 1241 loop x <= quit (FUNPOW modify n x) + n * cover x *) 1242(* Proof: 1243 Let f = (\j. body (FUNPOW modify j x)), 1244 n = loop_count guard modify x, 1245 z = FUNPOW modify n x. 1246 1247 For k < n, 1248 Let u = FUNPOW modify k x. 1249 FUNPOW modify 0 x <= FUNPOW modify k x by FUNPOW_LE_RISING, RISING modify 1250 x <= u by FUNPOW_0 1251 so cover u <= cover x by RMONO cover 1252 body u <= cover u by body and cover 1253 Thus, 1254 loop x 1255 <= quit z + SUM (GENLIST f n) by loop_modify_count_exit_le 1256 <= quit z + SUM (GENLIST (K (cover x)) n) by SUM_LE, EL_GENLIST, RISING modify 1257 = quit z + (cover x) * n by SUM_GENLIST_K 1258 = quit z + n * cover x by MULT_COMM 1259*) 1260val loop_rise_count_rcover_exit_le = store_thm( 1261 "loop_rise_count_rcover_exit_le", 1262 ``!loop body quit exit guard modify R. 1263 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 1264 (!x. loop x = if guard x then quit x else body x + if exit x then 0 else loop (modify x)) ==> 1265 !x cover. let n = loop_count guard modify x 1266 in (!x. body x <= cover x) /\ RMONO cover ==> 1267 loop x <= quit (FUNPOW modify n x) + n * cover x``, 1268 rpt strip_tac >> 1269 qabbrev_tac `foo = !x. loop x = if guard x then quit x else body x + if exit x then 0 else loop (modify x)` >> 1270 simp[] >> 1271 unabbrev_all_tac >> 1272 rpt strip_tac >> 1273 imp_res_tac loop_modify_count_exit_le >> 1274 first_x_assum (qspec_then `x` strip_assume_tac) >> 1275 qabbrev_tac `f = \j. body (FUNPOW modify j x)` >> 1276 qabbrev_tac `n = loop_count guard modify x` >> 1277 qabbrev_tac `z = FUNPOW modify n x` >> 1278 `SUM (GENLIST f n) <= SUM (GENLIST (K (cover x)) n)` by 1279 (irule SUM_LE >> 1280 rw[] >> 1281 rw[Abbr`f`] >> 1282 `FUNPOW modify 0 x <= FUNPOW modify k x` by rw[FUNPOW_LE_RISING] >> 1283 `FUNPOW modify 0 x = x` by rw[] >> 1284 qabbrev_tac `u = FUNPOW modify k x` >> 1285 `body u <= cover u` by rw[] >> 1286 `cover u <= cover x` by rw[] >> 1287 decide_tac) >> 1288 `SUM (GENLIST (K (cover x)) n) = cover x * n` by rw[SUM_GENLIST_K] >> 1289 decide_tac); 1290 1291(* ------------------------------------------------------------------------- *) 1292(* Numeric Loops with FALLING modify *) 1293(* ------------------------------------------------------------------------- *) 1294 1295(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 1296 (!x. loop x = if guard x then quit x else body x + if exit x then 0 else loop (modify x)) ==> 1297 !x cover. let n = loop_count guard modify x 1298 in (!x. body x <= cover x) /\ MONO cover ==> 1299 loop x <= quit (FUNPOW modify n x) + n * cover x *) 1300(* Proof: 1301 Let f = (\j. body (FUNPOW modify j x)), 1302 n = loop_count guard modify x, 1303 z = FUNPOW modify n x. 1304 1305 For k < n, 1306 FUNPOW modify k x <= FUNPOW modify 0 x by FUNPOW_LE_FALLING, FALLING modify 1307 = x by FUNPOW_0 1308 Thus, 1309 loop x 1310 <= quit z + SUM (GENLIST f n) by loop_modify_count_exit_le 1311 <= quit z + SUM (GENLIST (K (cover x)) n) by SUM_LE, EL_GENLIST, RISING modify 1312 = quit z + (cover x) * n by SUM_GENLIST_K 1313 = quit z + n * cover x by MULT_COMM 1314*) 1315val loop_fall_count_cover_exit_le = store_thm( 1316 "loop_fall_count_cover_exit_le", 1317 ``!loop guard body quit exit modify R. 1318 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 1319 (!x. loop x = if guard x then quit x else body x + if exit x then 0 else loop (modify x)) ==> 1320 !x cover. let n = loop_count guard modify x 1321 in (!x. body x <= cover x) /\ MONO cover ==> 1322 loop x <= quit (FUNPOW modify n x) + n * cover x``, 1323 rpt strip_tac >> 1324 qabbrev_tac `foo = !x. loop x = if guard x then quit x else body x + if exit x then 0 else loop (modify x)` >> 1325 simp[] >> 1326 unabbrev_all_tac >> 1327 rpt strip_tac >> 1328 imp_res_tac loop_modify_count_exit_le >> 1329 first_x_assum (qspec_then `x` strip_assume_tac) >> 1330 qabbrev_tac `f = \j. body (FUNPOW modify j x)` >> 1331 qabbrev_tac `n = loop_count guard modify x` >> 1332 qabbrev_tac `z = FUNPOW modify n x` >> 1333 `SUM (GENLIST f n) <= SUM (GENLIST (K (cover x)) n)` by 1334 (irule SUM_LE >> 1335 rw[] >> 1336 rw[Abbr`f`] >> 1337 `FUNPOW modify k x <= FUNPOW modify 0 x` by rw[FUNPOW_LE_FALLING] >> 1338 `FUNPOW modify 0 x = x` by rw[] >> 1339 qabbrev_tac `u = FUNPOW modify k x` >> 1340 `body u <= cover u` by rw[] >> 1341 `cover u <= cover x` by rw[] >> 1342 decide_tac) >> 1343 `SUM (GENLIST (K (cover x)) n) = cover x * n` by rw[SUM_GENLIST_K] >> 1344 decide_tac); 1345 1346(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 1347 (!x. loop x = if guard x then quit x else body x + if exit x then 0 else loop (modify x)) ==> 1348 !x cover. let n = loop_count guard modify x 1349 in (!x. body x <= cover x) /\ RMONO cover ==> 1350 loop x <= quit (FUNPOW modify n x) + n * cover (FUNPOW modify n x) *) 1351(* Proof: 1352 Let f = (\j. body (FUNPOW modify j x)), 1353 n = loop_count guard modify x, 1354 z = FUNPOW modify n x. 1355 1356 For k < n, 1357 Let u = FUNPOW modify k x. 1358 FUNPOW modify n x <= FUNPOW modify k x by FUNPOW_LE_FALLING, FALLING modify 1359 z <= u by notation 1360 so cover u <= cover z by RMONO cover 1361 body u <= cover u by cover property 1362 Thus, 1363 loop x 1364 <= quit z + SUM (GENLIST f n) by loop_modify_count_exit_le 1365 <= quit z + SUM (GENLIST (K (cover z)) n) by SUM_LE, EL_GENLIST, RISING modify 1366 = quit z + (cover z) * n by SUM_GENLIST_K 1367 = quit z + n * cover z by MULT_COMM 1368*) 1369val loop_fall_count_rcover_exit_le = store_thm( 1370 "loop_fall_count_rcover_exit_le", 1371 ``!loop guard body quit exit modify R. 1372 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 1373 (!x. loop x = if guard x then quit x else body x + if exit x then 0 else loop (modify x)) ==> 1374 !x cover. let n = loop_count guard modify x 1375 in (!x. body x <= cover x) /\ RMONO cover ==> 1376 loop x <= quit (FUNPOW modify n x) + n * cover (FUNPOW modify n x)``, 1377 rpt strip_tac >> 1378 qabbrev_tac `foo = !x. loop x = if guard x then quit x else body x + if exit x then 0 else loop (modify x)` >> 1379 simp[] >> 1380 unabbrev_all_tac >> 1381 rpt strip_tac >> 1382 imp_res_tac loop_modify_count_exit_le >> 1383 first_x_assum (qspec_then `x` strip_assume_tac) >> 1384 qabbrev_tac `f = \j. body (FUNPOW modify j x)` >> 1385 qabbrev_tac `n = loop_count guard modify x` >> 1386 qabbrev_tac `z = FUNPOW modify n x` >> 1387 `SUM (GENLIST f n) <= SUM (GENLIST (K (cover z)) n)` by 1388 (irule SUM_LE >> 1389 rw[] >> 1390 rw[Abbr`f`, Abbr`z`] >> 1391 `FUNPOW modify n x <= FUNPOW modify k x` by rw[FUNPOW_LE_FALLING] >> 1392 qabbrev_tac `u = FUNPOW modify k x` >> 1393 qabbrev_tac `v = FUNPOW modify n x` >> 1394 `body u <= cover u` by rw[] >> 1395 `cover u <= cover v` by rw[] >> 1396 decide_tac) >> 1397 `SUM (GENLIST (K (cover z)) n) = cover z * n` by rw[SUM_GENLIST_K] >> 1398 decide_tac); 1399 1400(* ------------------------------------------------------------------------- *) 1401(* General Theory of Recurrence with 2 arguments *) 1402(* ------------------------------------------------------------------------- *) 1403 1404(* 1405> loop_count_def |> DISCH_ALL |> INST_TYPE [alpha |-> ``:'a # 'b``] 1406 |> SIMP_RULE (srw_ss()) [pairTheory.FORALL_PROD] 1407 |> Q.INST [`guard` |-> `(\(x,y). gd x y)`, `modify` |-> `(\(x,y). (t x, m y))`] 1408 |> SIMP_RULE (srw_ss()) []; 1409val it = |- WF R ==> (!p_1 p_2. ~gd p_1 p_2 ==> R (t p_1,m p_2) (p_1,p_2)) ==> 1410 !p_1 p_2. loop_count (\(x,y). gd x y) (\(x,y). (t x,m y)) (p_1,p_2) = 1411 if gd p_1 p_2 then 0 else 1412 SUC (loop_count (\(x,y). gd x y) (\(x,y). (t x,m y)) (t p_1,m p_2)): thm 1413*) 1414 1415(* Define loop_count for 2 arguments *) 1416val loop2_count_def = Define` 1417 loop2_count guard modify transform x y = 1418 loop_count (\(x,y). guard x y) (\(x,y). (transform x, modify y)) (x, y) 1419`; 1420 1421(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> 1422 !x y. loop2_count guard modify transform x y = 1423 if guard x y then 0 1424 else SUC (loop2_count guard modify transform (transform x) (modify y)) *) 1425(* Proof: by loop_count_thm, loop2_count_def *) 1426val loop2_count_thm = store_thm( 1427 "loop2_count_thm", 1428 ``!transform modify guard R. 1429 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> 1430 !x y. loop2_count guard modify transform x y = 1431 if guard x y then 0 1432 else SUC (loop2_count guard modify transform (transform x) (modify y))``, 1433 rw[loop2_count_def] >> 1434 imp_res_tac loop_count_thm >> 1435 rw[Once pairTheory.FORALL_PROD]); 1436 1437(* Obtain similar theorems. *) 1438val loop2_count_0 = store_thm( 1439 "loop2_count_0", 1440 ``!transform modify guard R. 1441 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> 1442 !x y. guard x y ==> (loop2_count guard modify transform x y = 0)``, 1443 rw[loop2_count_def] >> 1444 imp_res_tac loop_count_0 >> 1445 rw[Once pairTheory.FORALL_PROD]); 1446 1447val loop2_count_suc = store_thm( 1448 "loop2_count_suc", 1449 ``!transform modify guard R. 1450 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> 1451 !x y. ~guard x y ==> (loop2_count guard modify transform x y = 1452 SUC (loop2_count guard modify transform (transform x) (modify y)))``, 1453 rw[loop2_count_def] >> 1454 imp_res_tac loop_count_suc >> 1455 rw[Once pairTheory.FORALL_PROD]); 1456 1457(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> 1458 !x y. guard (FUNPOW transform (loop2_count guard modify transform x y) x) 1459 (FUNPOW modify (loop2_count guard modify transform x y) y) *) 1460(* Proof: by loop_count_iterating, loop2_count_def. *) 1461val loop2_count_iterating = store_thm( 1462 "loop2_count_iterating", 1463 ``!transform modify guard R. 1464 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> 1465 !x y. guard (FUNPOW transform (loop2_count guard modify transform x y) x) 1466 (FUNPOW modify (loop2_count guard modify transform x y) y)``, 1467 rpt strip_tac >> 1468 assume_tac (loop_count_iterating 1469 |> SPEC_ALL |> INST_TYPE [``:'a`` |-> ``:'a # 'b``] 1470 |> SIMP_RULE bool_ss [pairTheory.FORALL_PROD] 1471 |> Q.INST [`loop` |-> `(\(x,y). lp x y)`, `guard` |-> `(\(x,y). gd x y)`, `quit` |-> `(\(x,y). qt x y)`, 1472 `body` |-> `(\(x,y). b x y)`, `modify` |-> `(\(x,y). (t x, m y))`] 1473 |> SIMP_RULE bool_ss [FUNPOW_PAIR, GSYM loop2_count_def] 1474 |> Q.INST [`lp` |-> `loop`, `gd` |-> `guard`, `qt` |-> `quit`, `b` |-> `body`, `t` |-> `transform`, `m` |-> `modify`] 1475 |> PairRules.PBETA_RULE) >> 1476 metis_tac[]); 1477 1478(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 1479 (!x y. loop x y = if guard x y then quit x y else body x y + loop (transform x) (modify y)) ==> 1480 !x y. loop x y = quit (FUNPOW transform (loop2_count guard modify transform x y) x) 1481 (FUNPOW modify (loop2_count guard modify transform x y) y) + 1482 SUM (GENLIST (\j. body (FUNPOW transform j x) (FUNPOW modify j y)) 1483 (loop2_count guard modify transform x y)) *) 1484(* Proof: by loop_modify_count_eqn, loop2_count_def *) 1485val loop2_modify_count_eqn = store_thm( 1486 "loop2_modify_count_eqn", 1487 ``!loop guard body quit modify transform R. 1488 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 1489 (!x y. loop x y = if guard x y then quit x y else body x y + loop (transform x) (modify y)) ==> 1490 !x y. loop x y = quit (FUNPOW transform (loop2_count guard modify transform x y) x) 1491 (FUNPOW modify (loop2_count guard modify transform x y) y) + 1492 SUM (GENLIST (\j. body (FUNPOW transform j x) (FUNPOW modify j y)) 1493 (loop2_count guard modify transform x y))``, 1494 rpt strip_tac >> 1495 assume_tac (loop_modify_count_eqn 1496 |> SPEC_ALL |> INST_TYPE [``:'a`` |-> ``:'a # 'b``] 1497 |> SIMP_RULE bool_ss [pairTheory.FORALL_PROD] 1498 |> Q.INST [`loop` |-> `(\(x,y). lp x y)`, `guard` |-> `(\(x,y). gd x y)`, `quit` |-> `(\(x,y). qt x y)`, 1499 `body` |-> `(\(x,y). b x y)`, `modify` |-> `(\(x,y). (t x, m y))`] 1500 |> SIMP_RULE bool_ss [FUNPOW_PAIR, GSYM loop2_count_def] 1501 |> Q.INST [`lp` |-> `loop`, `gd` |-> `guard`, `qt` |-> `quit`, `b` |-> `body`, `t` |-> `transform`, `m` |-> `modify`] 1502 |> PairRules.PBETA_RULE) >> 1503 metis_tac[]); 1504 1505(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 1506 (!x y. loop x y = if guard x y then quit x y else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 1507 !x y. loop x y <= quit (FUNPOW transform (loop2_count guard modify transform x y) x) 1508 (FUNPOW modify (loop2_count guard modify transform x y) y) + 1509 SUM (GENLIST (\j. body (FUNPOW transform j x) (FUNPOW modify j y)) 1510 (loop2_count guard modify transform x y)) *) 1511(* Proof: by loop_modify_count_exit_le, loop2_count_def. *) 1512val loop2_modify_count_exit_le = store_thm( 1513 "loop2_modify_count_exit_le", 1514 ``!loop guard body quit exit modify transform R. 1515 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 1516 (!x y. loop x y = if guard x y then quit x y else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 1517 !x y. loop x y <= quit (FUNPOW transform (loop2_count guard modify transform x y) x) 1518 (FUNPOW modify (loop2_count guard modify transform x y) y) + 1519 SUM (GENLIST (\j. body (FUNPOW transform j x) (FUNPOW modify j y)) 1520 (loop2_count guard modify transform x y))``, 1521 rpt strip_tac >> 1522 assume_tac (loop_modify_count_exit_le 1523 |> SPEC_ALL |> INST_TYPE [``:'a`` |-> ``:'a # 'b``] 1524 |> SIMP_RULE bool_ss [pairTheory.FORALL_PROD] 1525 |> Q.INST [`loop` |-> `(\(x,y). lp x y)`, `guard` |-> `(\(x,y). gd x y)`,`quit` |-> `(\(x,y). qt x y)`, 1526 `body` |-> `(\(x,y). b x y)`, `modify` |-> `(\(x,y). (t x, m y))`, `exit` |-> `(\(x,y). et x y)`] 1527 |> SIMP_RULE bool_ss [FUNPOW_PAIR, GSYM loop2_count_def] 1528 |> Q.INST [`lp` |-> `loop`, `gd` |-> `guard`, `qt` |-> `quit`, `et` |-> `exit`, `b` |-> `body`, `t` |-> `transform`, `m` |-> `modify`] 1529 |> PairRules.PBETA_RULE) >> 1530 metis_tac[]); 1531 1532(* ------------------------------------------------------------------------- *) 1533(* List for Transform argument *) 1534(* ------------------------------------------------------------------------- *) 1535 1536(* Define the iterating list *) 1537val iterating_def = Define` 1538 iterating f x y = if y = 0 then [] else x::iterating f (f x) (y - 1) 1539`; 1540 1541(* 1542EVAL ``iterating SQ 2 (pop 2 10)``; = [2; 4; 16; 256]: thm 1543EVAL ``iterating SQ 3 (pop 2 7)``; = [3; 9; 81]: thm 1544EVAL ``MAP (\j. FUNPOW SQ j 2) [0 ..< (pop 2 10)]``; = [2; 4; 16; 256]: thm 1545EVAL ``MAP ((combin$C (FUNPOW SQ)) 2) [0 ..< (pop 2 10)]``; = [2; 4; 16; 256]:thm 1546*) 1547 1548(* Theorem: iterating f x 0 = [] *) 1549(* Proof: by iterating_def *) 1550val iterating_nil = store_thm( 1551 "iterating_nil", 1552 ``!f x. iterating f x 0 = []``, 1553 rw[Once iterating_def]); 1554 1555(* Theorem: iterating f x (SUC y) = x::iterating f (f x) y *) 1556(* Proof: by iterating_def *) 1557val iterating_cons = store_thm( 1558 "iterating_cons", 1559 ``!f x y. iterating f x (SUC y) = x::iterating f (f x) y``, 1560 rw[Once iterating_def]); 1561 1562(* Combine these theorems *) 1563val iterating_alt = save_thm("iterating_alt", CONJ iterating_nil iterating_cons); 1564(* 1565val iterating_alt = |- (!f x. iterating f x 0 = []) /\ 1566 !f x y. iterating f x (SUC y) = x::iterating f (f x) y: thm 1567*) 1568 1569(* Theorem: iterating f x y = MAP (combin$C (FUNPOW f) x) [0 ..< y] *) 1570(* Proof: 1571 By induction on y. 1572 Let g = combin$C (FUNPOW f) x, which is (\j. FUNPOW f j x). 1573 Base: !x. iterating f x 0 = MAP g [0 ..< 0] 1574 LHS = iterating f x 0 = [] by iterating_nil 1575 RHS = MAP g [0 ..< 0] 1576 = MAP g [] by listRangeLHI_def 1577 = [] = LHS by MAP 1578 Step: !x. iterating f x y = MAP (combin$C (FUNPOW f) x) [0 ..< y] ==> 1579 !x. iterating f x (SUC y) = MAP (combin$C (FUNPOW f) x) [0 ..< SUC y] 1580 1581 Let h = combin$C (FUNPOW f) (f x), which is (\j. FUNPOW f j (f x)). 1582 Then h = g o SUC by FUNPOW 1583 and g 0 = x by FUNPOW_0 1584 1585 iterating f x (SUC y) 1586 = x :: iterating f (f x) y by iterating_cons 1587 = x :: MAP h [0 ..< y] by induction hypothesis 1588 = x :: MAP (g o SUC) [0 ..< y] by h = g o SUC 1589 = x :: MAP g [1 ..< SUC y] by listRangeLHI_MAP_SUC 1590 = g 0 :: MAP g [1 ..< SUC y] by x = g 0 1591 = MAP g (0::[1 ..< SUC y]) by MAP 1592 = MAP g [0 ..< SUC y] by listRangeLHI_CONS 1593*) 1594val iterating_eqn = store_thm( 1595 "iterating_eqn", 1596 ``!f x y. iterating f x y = MAP (combin$C (FUNPOW f) x) [0 ..< y]``, 1597 strip_tac >> 1598 Induct_on `y` >- 1599 rw[Once iterating_def] >> 1600 rpt strip_tac >> 1601 qabbrev_tac `g = combin$C (FUNPOW f) x` >> 1602 qabbrev_tac `h = combin$C (FUNPOW f) (f x)` >> 1603 `x = g 0` by rw[Abbr`g`] >> 1604 `h = g o SUC` by rw[FUN_EQ_THM, FUNPOW, Abbr`g`, Abbr`h`] >> 1605 `iterating f x (SUC y) = x :: iterating f (f x) y` by rw[Once iterating_def] >> 1606 `_ = x :: MAP h [0 ..< y]` by rw[Abbr`h`] >> 1607 `_ = x :: MAP (g o SUC) [0 ..< y]` by rw[] >> 1608 `_ = g 0 :: MAP g [1 ..< SUC y]` by rw[GSYM listRangeLHI_MAP_SUC, ADD1] >> 1609 `_ = MAP g [0 ..< SUC y]` by rw[listRangeLHI_CONS] >> 1610 rw[]); 1611 1612(* Theorem: LENGTH (iterating f x y) = y *) 1613(* Proof: 1614 LENGTH (iterating f x y) 1615 = LENGTH (MAP (combin$C (FUNPOW f) x) [0 ..< y]) by iterating_eqn 1616 = LENGTH [0 ..< y] by LENGTH_MAP 1617 = y by listRangeLHI_LEN 1618*) 1619val iterating_length = store_thm( 1620 "iterating_length", 1621 ``!f x y. LENGTH (iterating f x y) = y``, 1622 rw[iterating_eqn, listRangeLHI_LEN]); 1623 1624(* Theorem: j < y ==> MEM (FUNPOW f j x) (iterating f x y) *) 1625(* Proof: 1626 MEM k (iterating f x y) 1627 <=> MEM k (MAP (combin$C (FUNPOW f) x) [0 ..< y]) by iterating_eqn 1628 <=> ?t. k = combin$C (FUNPOW f) x t /\ MEM t [0 ..< y] by MEM_MAP 1629 <=> ?t. k = FUNPOW f t x /\ 0 <= t /\ t < y by listRangeLHI_MEM 1630*) 1631val iterating_member = store_thm( 1632 "iterating_member", 1633 ``!f x y j. j < y ==> MEM (FUNPOW f j x) (iterating f x y)``, 1634 rw[iterating_eqn, MEM_MAP] >> 1635 metis_tac[]); 1636 1637(* Theorem: j < y ==> EL j (iterating f x y) = FUNPOW f j x *) 1638(* Proof: 1639 Since j < y = LENGTH (iterating f x y) by iterating_length 1640 EL j (iterating f x y) 1641 = EL j (MAP (combin$C (FUNPOW f) x) [0 ..< y]) by iterating_eqn 1642 = combin$C (FUNPOW f) x (EL j [0 ..< y]) by EL_MAP 1643 = combin$C (FUNPOW f) j k by listRangeLHI_EL 1644 = FUNPOW f j x 1645*) 1646val iterating_element = store_thm( 1647 "iterating_element", 1648 ``!f x y j. j < y ==> EL j (iterating f x y) = FUNPOW f j x``, 1649 rw[iterating_eqn, iterating_length, EL_MAP, listRangeLHI_EL]); 1650 1651(* ------------------------------------------------------------------------- *) 1652(* Numeric Loops with transform and modify *) 1653(* ------------------------------------------------------------------------- *) 1654 1655(* Idea: 1656 1657 From loop2_modify_count_eqn, let n = loop2_count guard modify transform x y. 1658 loop x y 1659 = quit (last x) (last y) + SUM (GENLIST (\j. body (FUNPOW transform j x) (FUNPOW modify j y)) n) 1660 = quit (last x) (last y) + [body x y, body (t x) (m y), body (t (t x)) (m (m y)), ....] for n terms 1661 <= quit (last x) (last y) + [body x y, body (t x) y, body (t (t x)) y, .....] if MONO2 body, FALLING m 1662 If FALLING t, 1663 <= quit (last x) (last y) + [body x y, body x y, ....] = c + n * body x y 1664 If RISING t, 1665 <= quit (last x) (last y) + [body (last x) y, body (last x) y, ...] = c + n * body (last x) y 1666 Similar estimates for RISING m 1667*) 1668 1669(* ------------------------------------------------------------------------- *) 1670(* Numeric Loops with RISING transform and FALLING modify *) 1671(* ------------------------------------------------------------------------- *) 1672 1673(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 1674 RISING transform /\ FALLING modify /\ 1675 (!x y. loop x y = 1676 if guard x y then quit x y 1677 else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 1678 !x y cover. let n = loop2_count guard modify transform x y 1679 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 1680 loop x y <= quit (FUNPOW transform n x) (FUNPOW modify n y) + 1681 n * cover (FUNPOW transform n x) y *) 1682(* Proof: 1683 Let f = (\j. body (FUNPOW transform j x) (FUNPOW modify j y)), 1684 n = loop2_count guard modify transform x y, 1685 p = FUNPOW transform n x, 1686 q = FUNPOW modify n y. 1687 1688 For k < n, 1689 FUNPOW transform k x <= FUNPOW transform n x by FUNPOW_LE_RISING, RISING transform 1690 = p by notation 1691 FUNPOW modify k y <= FUNPOW modify 0 y by FUNPOW_LE_FALLING, FALLING modify 1692 = y by FUNPOW_0 1693 Thus, 1694 loop x y 1695 <= quit p q + SUM (GENLIST f n) by loop2_modify_count_exit_le 1696 <= quit p q + SUM (GENLIST (K (cover p y)) n) by SUM_LE, EL_GENLIST, FALLING modify, RISING transform 1697 = quit p q + (cover p y) * n by SUM_GENLIST_K 1698 = quit p q + n * cover p y by MULT_COMM 1699*) 1700val loop2_rise_fall_count_cover_exit_le = store_thm( 1701 "loop2_rise_fall_count_cover_exit_le", 1702 ``!loop guard body quit exit modify transform R. 1703 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 1704 RISING transform /\ FALLING modify /\ 1705 (!x y. loop x y = 1706 if guard x y then quit x y 1707 else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 1708 !x y cover. let n = loop2_count guard modify transform x y 1709 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 1710 loop x y <= quit (FUNPOW transform n x) (FUNPOW modify n y) + 1711 n * cover (FUNPOW transform n x) y``, 1712 rpt strip_tac >> 1713 qabbrev_tac `foo = !x y. loop x y = 1714 if guard x y then quit x y 1715 else body x y + if exit x y then 0 else loop (transform x) (modify y)` >> 1716 simp[] >> 1717 unabbrev_all_tac >> 1718 rpt strip_tac >> 1719 imp_res_tac loop2_modify_count_exit_le >> 1720 first_x_assum (qspecl_then [`y`, `x`] strip_assume_tac) >> 1721 qabbrev_tac `f = \j. body (FUNPOW transform j x) (FUNPOW modify j y)` >> 1722 qabbrev_tac `n = loop2_count guard modify transform x y` >> 1723 qabbrev_tac `p = FUNPOW transform n x` >> 1724 qabbrev_tac `q = FUNPOW modify n y` >> 1725 `SUM (GENLIST f n) <= SUM (GENLIST (K (cover p y)) n)` by 1726 (irule SUM_LE >> 1727 rw[] >> 1728 rw[Abbr`f`, Abbr`p`] >> 1729 `FUNPOW transform k x <= FUNPOW transform n x` by rw[FUNPOW_LE_RISING] >> 1730 `FUNPOW modify k y <= FUNPOW modify 0 y` by rw[FUNPOW_LE_FALLING] >> 1731 `FUNPOW modify 0 y = y` by rw[] >> 1732 qabbrev_tac `u = FUNPOW transform k x` >> 1733 qabbrev_tac `v = FUNPOW modify k y` >> 1734 `body u v <= cover u v` by rw[] >> 1735 `cover u v <= cover (FUNPOW transform n x) y` by rw[] >> 1736 decide_tac) >> 1737 `SUM (GENLIST (K (cover p y)) n) = cover p y * n` by rw[SUM_GENLIST_K] >> 1738 decide_tac); 1739 1740(* ------------------------------------------------------------------------- *) 1741(* Numeric Loops with FALLING transform and FALLING modify *) 1742(* ------------------------------------------------------------------------- *) 1743 1744(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 1745 FALLING transform /\ FALLING modify /\ 1746 (!x y. loop x y = 1747 if guard x y then quit x y 1748 else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 1749 !x y cover. let n = loop2_count guard modify transform x y 1750 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 1751 loop x y <= quit (FUNPOW transform n x) (FUNPOW modify n y) + n * cover x y *) 1752(* Proof: 1753 Let f = (\j. body (FUNPOW transform j x) (FUNPOW modify j y)), 1754 n = loop2_count guard modify transform x y, 1755 p = FUNPOW transform n x, 1756 q = FUNPOW modify n y. 1757 1758 For k < n, 1759 FUNPOW transform k x <= FUNPOW transform 0 x by FUNPOW_LE_FALLING, FALLING transform 1760 = x by FUNPOW_0 1761 FUNPOW modify k y <= FUNPOW modify 0 y by FUNPOW_LE_FALLING, FALLING modify 1762 = y by FUNPOW_0 1763 Thus, 1764 loop x y 1765 <= quit p q + SUM (GENLIST f n) by loop2_modify_count_exit_le 1766 <= quit p q + SUM (GENLIST (K (cover x y)) n) by SUM_LE, EL_GENLIST, FALLING modify, FALLING transform 1767 = quit p q + (cover x y) * n by SUM_GENLIST_K 1768 = quit p q + n * cover x y by MULT_COMM 1769*) 1770val loop2_fall_fall_count_cover_exit_le = store_thm( 1771 "loop2_fall_fall_count_cover_exit_le", 1772 ``!loop guard body quit exit modify transform R. 1773 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 1774 FALLING transform /\ FALLING modify /\ 1775 (!x y. loop x y = 1776 if guard x y then quit x y 1777 else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 1778 !x y cover. let n = loop2_count guard modify transform x y 1779 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 1780 loop x y <= quit (FUNPOW transform n x) (FUNPOW modify n y) + n * cover x y``, 1781 rpt strip_tac >> 1782 qabbrev_tac `foo = !x y. loop x y = 1783 if guard x y then quit x y 1784 else body x y + if exit x y then 0 else loop (transform x) (modify y)` >> 1785 simp[] >> 1786 unabbrev_all_tac >> 1787 rpt strip_tac >> 1788 imp_res_tac loop2_modify_count_exit_le >> 1789 first_x_assum (qspecl_then [`y`, `x`] strip_assume_tac) >> 1790 qabbrev_tac `f = \j. body (FUNPOW transform j x) (FUNPOW modify j y)` >> 1791 qabbrev_tac `n = loop2_count guard modify transform x y` >> 1792 qabbrev_tac `p = FUNPOW transform n x` >> 1793 qabbrev_tac `q = FUNPOW modify n y` >> 1794 `SUM (GENLIST f n) <= SUM (GENLIST (K (cover x y)) n)` by 1795 (irule SUM_LE >> 1796 rw[] >> 1797 rw[Abbr`f`] >> 1798 `FUNPOW transform k x <= FUNPOW transform 0 x` by rw[FUNPOW_LE_FALLING] >> 1799 `FUNPOW modify k y <= FUNPOW modify 0 y` by rw[FUNPOW_LE_FALLING] >> 1800 `FUNPOW transform 0 x = x` by rw[] >> 1801 `FUNPOW modify 0 y = y` by rw[] >> 1802 qabbrev_tac `u = FUNPOW transform k x` >> 1803 qabbrev_tac `v = FUNPOW modify k y` >> 1804 `body u v <= cover u v` by rw[] >> 1805 `cover u v <= cover x y` by rw[] >> 1806 decide_tac) >> 1807 `SUM (GENLIST (K (cover x y)) n) = cover x y * n` by rw[SUM_GENLIST_K] >> 1808 decide_tac); 1809 1810(* ------------------------------------------------------------------------- *) 1811(* Numeric Loops with FALLING transform and RISING modify *) 1812(* ------------------------------------------------------------------------- *) 1813 1814(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 1815 FALLING transform /\ RISING modify /\ 1816 (!x y. loop x y = 1817 if guard x y then quit x y 1818 else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 1819 !x y cover. let n = loop2_count guard modify transform x y 1820 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 1821 loop x y <= quit (FUNPOW transform n x) (FUNPOW modify n y) + 1822 n * cover x (FUNPOW modify n y) *) 1823(* Proof: 1824 Let f = (\j. body (FUNPOW transform j x) (FUNPOW modify j y)), 1825 n = loop2_count guard modify transform x y, 1826 p = FUNPOW transform n x, 1827 q = FUNPOW modify n y. 1828 1829 For k < n, 1830 FUNPOW transform k x <= FUNPOW transform 0 x by FUNPOW_LE_FALLING, FALLING transform 1831 = x by FUNPOW_0 1832 FUNPOW modify k y <= FUNPOW modify n y by FUNPOW_LE_RISING, RISING modify 1833 = q by notation 1834 Thus, 1835 loop x y 1836 <= quit p q + SUM (GENLIST f n) by loop2_modify_count_exit_le 1837 <= quit p q + SUM (GENLIST (K (cover x q)) n) by SUM_LE, EL_GENLIST, RISING modify, FALLING transform 1838 = quit p q + (cover x q) * n by SUM_GENLIST_K 1839 = quit p q + n * cover x q by MULT_COMM 1840*) 1841val loop2_fall_rise_count_cover_exit_le = store_thm( 1842 "loop2_fall_rise_count_cover_exit_le", 1843 ``!loop guard body quit exit modify transform R. 1844 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 1845 FALLING transform /\ RISING modify /\ 1846 (!x y. loop x y = 1847 if guard x y then quit x y 1848 else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 1849 !x y cover. let n = loop2_count guard modify transform x y 1850 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 1851 loop x y <= quit (FUNPOW transform n x) (FUNPOW modify n y) + 1852 n * cover x (FUNPOW modify n y)``, 1853 rpt strip_tac >> 1854 qabbrev_tac `foo = !x y. loop x y = 1855 if guard x y then quit x y 1856 else body x y + if exit x y then 0 else loop (transform x) (modify y)` >> 1857 simp[] >> 1858 unabbrev_all_tac >> 1859 rpt strip_tac >> 1860 imp_res_tac loop2_modify_count_exit_le >> 1861 first_x_assum (qspecl_then [`y`, `x`] strip_assume_tac) >> 1862 qabbrev_tac `f = \j. body (FUNPOW transform j x) (FUNPOW modify j y)` >> 1863 qabbrev_tac `n = loop2_count guard modify transform x y` >> 1864 qabbrev_tac `p = FUNPOW transform n x` >> 1865 qabbrev_tac `q = FUNPOW modify n y` >> 1866 `SUM (GENLIST f n) <= SUM (GENLIST (K (cover x q)) n)` by 1867 (irule SUM_LE >> 1868 rw[] >> 1869 rw[Abbr`f`, Abbr`q`] >> 1870 `FUNPOW transform k x <= FUNPOW transform 0 x` by rw[FUNPOW_LE_FALLING] >> 1871 `FUNPOW modify k y <= FUNPOW modify n y` by rw[FUNPOW_LE_RISING] >> 1872 `FUNPOW transform 0 x = x` by rw[] >> 1873 qabbrev_tac `u = FUNPOW transform k x` >> 1874 qabbrev_tac `v = FUNPOW modify k y` >> 1875 `body u v <= cover u v` by rw[] >> 1876 `cover u v <= cover x (FUNPOW modify n y)` by rw[] >> 1877 decide_tac) >> 1878 `SUM (GENLIST (K (cover x q)) n) = cover x q * n` by rw[SUM_GENLIST_K] >> 1879 decide_tac); 1880 1881(* ------------------------------------------------------------------------- *) 1882(* Numeric Loops with RISING transform and RISING modify *) 1883(* ------------------------------------------------------------------------- *) 1884 1885(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 1886 RISING transform /\ RISING modify /\ 1887 (!x y. loop x y = 1888 if guard x y then quit x y 1889 else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 1890 !x y cover. let n = loop2_count guard modify transform x y 1891 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 1892 loop x y <= quit (FUNPOW transform n x) (FUNPOW modify n y) + 1893 n * cover (FUNPOW transform n x) (FUNPOW modify n y) *) 1894(* Proof: 1895 Let f = (\j. body (FUNPOW transform j x) (FUNPOW modify j y)), 1896 n = loop2_count guard modify transform x y, 1897 p = FUNPOW transform n x, 1898 q = FUNPOW modify n y. 1899 1900 For k < n, 1901 FUNPOW transform k x <= FUNPOW transform n x by FUNPOW_LE_RISING, RISING transform 1902 = p by notation 1903 FUNPOW modify k y <= FUNPOW modify n y by FUNPOW_LE_RISING, RISING modify 1904 = q by notation 1905 Thus, 1906 loop x y 1907 <= quit p q + SUM (GENLIST f n) by loop2_modify_count_exit_le 1908 <= quit p q + SUM (GENLIST (K (cover p q)) n) by SUM_LE, EL_GENLIST, RISING modify, RISING transform 1909 = quit p q + (cover p q) * n by SUM_GENLIST_K 1910 = quit p q + n * cover p q by MULT_COMM 1911*) 1912val loop2_rise_rise_count_cover_exit_le = store_thm( 1913 "loop2_rise_rise_count_cover_exit_le", 1914 ``!loop guard body quit exit modify transform R. 1915 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 1916 RISING transform /\ RISING modify /\ 1917 (!x y. loop x y = 1918 if guard x y then quit x y 1919 else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 1920 !x y cover. let n = loop2_count guard modify transform x y 1921 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 1922 loop x y <= quit (FUNPOW transform n x) (FUNPOW modify n y) + 1923 n * cover (FUNPOW transform n x) (FUNPOW modify n y)``, 1924 rpt strip_tac >> 1925 qabbrev_tac `foo = !x y. loop x y = 1926 if guard x y then quit x y 1927 else body x y + if exit x y then 0 else loop (transform x) (modify y)` >> 1928 simp[] >> 1929 unabbrev_all_tac >> 1930 rpt strip_tac >> 1931 imp_res_tac loop2_modify_count_exit_le >> 1932 first_x_assum (qspecl_then [`y`, `x`] strip_assume_tac) >> 1933 qabbrev_tac `f = \j. body (FUNPOW transform j x) (FUNPOW modify j y)` >> 1934 qabbrev_tac `n = loop2_count guard modify transform x y` >> 1935 qabbrev_tac `p = FUNPOW transform n x` >> 1936 qabbrev_tac `q = FUNPOW modify n y` >> 1937 `SUM (GENLIST f n) <= SUM (GENLIST (K (cover p q)) n)` by 1938 (irule SUM_LE >> 1939 rw[] >> 1940 rw[Abbr`f`, Abbr`p`, Abbr`q`] >> 1941 `FUNPOW transform k x <= FUNPOW transform n x` by rw[FUNPOW_LE_RISING] >> 1942 `FUNPOW modify k y <= FUNPOW modify n y` by rw[FUNPOW_LE_RISING] >> 1943 qabbrev_tac `u = FUNPOW transform k x` >> 1944 qabbrev_tac `v = FUNPOW modify k y` >> 1945 `body u v <= cover u v` by rw[] >> 1946 `cover u v <= cover (FUNPOW transform n x) (FUNPOW modify n y)` by rw[] >> 1947 decide_tac) >> 1948 `SUM (GENLIST (K (cover p q)) n) = cover p q * n` by rw[SUM_GENLIST_K] >> 1949 decide_tac); 1950 1951(* ------------------------------------------------------------------------- *) 1952(* General Theory of Recurrence with 3 arguments *) 1953(* ------------------------------------------------------------------------- *) 1954 1955(* 1956> loop_count_def |> DISCH_ALL |> INST_TYPE [alpha |-> ``:'a # 'b # 'c``] 1957 |> SIMP_RULE (srw_ss()) [pairTheory.FORALL_PROD] 1958 |> Q.INST [`guard` |-> `(\(x,y,z). gd x y z)`, `modify` |-> `(\(x,y,z). (c x, t y, m z))`] 1959 |> SIMP_RULE (srw_ss()) []; 1960val it = |- WF R ==> (!p_1 p_1' p_2. ~gd p_1 p_1' p_2 ==> R (c p_1,t p_1',m p_2) (p_1,p_1',p_2)) ==> 1961 !p_1 p_1' p_2. loop_count (\(x,y,z). gd x y z) (\(x,y,z). (c x,t y,m z)) (p_1,p_1',p_2) = 1962 if gd p_1 p_1' p_2 then 0 1963 else SUC (loop_count (\(x,y,z). gd x y z) (\(x,y,z). (c x,t y,m z)) (c p_1,t p_1',m p_2)): thm 1964*) 1965 1966(* Define loop_count for 3 arguments *) 1967val loop3_count_def = Define` 1968 loop3_count guard modify transform convert x y z = 1969 loop_count (\(x,y,z). guard x y z) (\(x,y,z). (convert x, transform y, modify z)) (x, y, z) 1970`; 1971 1972(* Theorem: WF R /\ (!x y z. ~guard x y z ==> R (convert x, transform y,modify z) (x,y,z)) ==> 1973 !x y z. loop3_count guard modify transform convert x y z = 1974 if guard x y z then 0 1975 else SUC (loop3_count guard modify transform convert (convert x) (transform y) (modify z)) *) 1976(* Proof: by loop_count_thm, loop3_count_def *) 1977val loop3_count_thm = store_thm( 1978 "loop3_count_thm", 1979 ``!convert transform modify guard R. 1980 WF R /\ (!x y z. ~guard x y z ==> R (convert x, transform y,modify z) (x,y,z)) ==> 1981 !x y z. loop3_count guard modify transform convert x y z = 1982 if guard x y z then 0 1983 else SUC (loop3_count guard modify transform convert (convert x) (transform y) (modify z))``, 1984 rw[loop3_count_def] >> 1985 imp_res_tac loop_count_thm >> 1986 fs[Once pairTheory.FORALL_PROD]); 1987 1988(* Obtain similar theorems. *) 1989val loop3_count_0 = store_thm( 1990 "loop3_count_0", 1991 ``!convert transform modify guard R. 1992 WF R /\ (!x y z. ~guard x y z ==> R (convert x, transform y,modify z) (x,y,z)) ==> 1993 !x y z. guard x y z ==> (loop3_count guard modify transform convert x y z = 0)``, 1994 rw[loop3_count_def] >> 1995 imp_res_tac loop_count_0 >> 1996 fs[Once pairTheory.FORALL_PROD]); 1997 1998val loop3_count_suc = store_thm( 1999 "loop3_count_suc", 2000 ``!convert transform modify guard R. 2001 WF R /\ (!x y z. ~guard x y z ==> R (convert x, transform y,modify z) (x,y,z)) ==> 2002 !x y z. ~guard x y z ==> (loop3_count guard modify transform convert x y z = 2003 SUC (loop3_count guard modify transform convert (convert x) (transform y) (modify z)))``, 2004 rw[loop3_count_def] >> 2005 imp_res_tac loop_count_suc >> 2006 fs[Once pairTheory.FORALL_PROD]); 2007 2008(* Theorem: WF R /\ (!x y z. ~guard x y z ==> R (convert x, transform y,modify z) (x,y,z)) ==> 2009 !x y. guard (FUNPOW convert (loop3_count guard modify transform convert x y z) x) 2010 (FUNPOW transform (loop3_count guard modify transform convert x y z) y) 2011 (FUNPOW modify (loop3_count guard modify transform convert x y z) z) *) 2012(* Proof: by loop_count_iterating, loop3_count_def. *) 2013val loop3_count_iterating = store_thm( 2014 "loop3_count_iterating", 2015 ``!convert transform modify guard R. 2016 WF R /\ (!x y z. ~guard x y z ==> R (convert x, transform y,modify z) (x,y,z)) ==> 2017 !x y z. guard (FUNPOW convert (loop3_count guard modify transform convert x y z) x) 2018 (FUNPOW transform (loop3_count guard modify transform convert x y z) y) 2019 (FUNPOW modify (loop3_count guard modify transform convert x y z) z)``, 2020 rpt strip_tac >> 2021 assume_tac (loop_count_iterating 2022 |> SPEC_ALL |> INST_TYPE [``:'a`` |-> ``:'a # 'b # 'c``] 2023 |> SIMP_RULE bool_ss [pairTheory.FORALL_PROD] 2024 |> Q.INST [`loop` |-> `(\(x,y,z). lp x y z)`, `guard` |-> `(\(x,y,z). gd x y z)`, 2025 `quit` |-> `(\(x,y,z). qt x y z)`, `body` |-> `(\(x,y,z). b x y z)`, 2026 `modify` |-> `(\(x,y,z). (c x, t y, m z))`] 2027 |> SIMP_RULE bool_ss [FUNPOW_TRIPLE, GSYM loop3_count_def] 2028 |> Q.INST [`lp` |-> `loop`, `gd` |-> `guard`, `qt` |-> `quit`, `b` |-> `body`, 2029 `c` |-> `convert`, `t` |-> `transform`, `m` |-> `modify`] 2030 |> PairRules.PBETA_RULE) >> 2031 metis_tac[]); 2032 2033(* Theorem: WF R /\ (!x y z. ~guard x y z ==> R (convert x, transform y,modify z) (x,y,z)) /\ 2034 (!x y z. loop x y z = 2035 if guard x y z then quit x y z 2036 else body x y z + loop (convert x) (transform y) (modify z)) ==> 2037 !x y z. loop x y z = quit (FUNPOW convert (loop3_count guard modify transform convert x y z) x) 2038 (FUNPOW transform (loop3_count guard modify transform convert x y z) y) 2039 (FUNPOW modify (loop3_count guard modify transform convert x y z) z) + 2040 SUM (GENLIST (\j. body (FUNPOW convert j x) (FUNPOW transform j y) (FUNPOW modify j z)) 2041 (loop3_count guard modify transform convert x y z)) *) 2042(* Proof: by loop_modify_count_eqn, loop3_count_def *) 2043val loop3_modify_count_eqn = store_thm( 2044 "loop3_modify_count_eqn", 2045 ``!loop guard body quit modify transform convert R. 2046 WF R /\ (!x y z. ~guard x y z ==> R (convert x, transform y,modify z) (x,y,z)) /\ 2047 (!x y z. loop x y z = 2048 if guard x y z then quit x y z 2049 else body x y z + loop (convert x) (transform y) (modify z)) ==> 2050 !x y z. loop x y z = quit (FUNPOW convert (loop3_count guard modify transform convert x y z) x) 2051 (FUNPOW transform (loop3_count guard modify transform convert x y z) y) 2052 (FUNPOW modify (loop3_count guard modify transform convert x y z) z) + 2053 SUM (GENLIST (\j. body (FUNPOW convert j x) (FUNPOW transform j y) (FUNPOW modify j z)) 2054 (loop3_count guard modify transform convert x y z))``, 2055 rpt strip_tac >> 2056 assume_tac (loop_modify_count_eqn 2057 |> SPEC_ALL |> INST_TYPE [``:'a`` |-> ``:'a # 'b # 'c``] 2058 |> SIMP_RULE bool_ss [pairTheory.FORALL_PROD] 2059 |> Q.INST [`loop` |-> `(\(x,y,z). lp x y z)`, `guard` |-> `(\(x,y,z). gd x y z)`, 2060 `quit` |-> `(\(x,y,z). qt x y z)`, `body` |-> `(\(x,y,z). b x y z)`, 2061 `modify` |-> `(\(x,y,z). (c x, t y, m z))`] 2062 |> SIMP_RULE bool_ss [FUNPOW_TRIPLE, GSYM loop3_count_def] 2063 |> Q.INST [`lp` |-> `loop`, `gd` |-> `guard`, `qt` |-> `quit`, `b` |-> `body`, 2064 `c` |-> `convert`, `t` |-> `transform`, `m` |-> `modify`] 2065 |> PairRules.PBETA_RULE) >> 2066 metis_tac[]); 2067 2068(* Theorem: WF R /\ (!x y z. ~guard x y z ==> R (convert x, transform y,modify z) (x,y,z)) /\ 2069 (!x y z. loop x y z = 2070 if guard x y z then quit x y z 2071 else body x y z + if exit x y z then 0 else loop (convert x) (transform y) (modify z)) ==> 2072 !x y z. loop x y z <= quit (FUNPOW convert (loop3_count guard modify transform convert x y z) x) 2073 (FUNPOW transform (loop3_count guard modify transform convert x y z) y) 2074 (FUNPOW modify (loop3_count guard modify transform convert x y z) z) + 2075 SUM (GENLIST (\j. body (FUNPOW convert j x) (FUNPOW transform j y) (FUNPOW modify j z)) 2076 (loop3_count guard modify transform convert x y z)) *) 2077(* Proof: by loop_modify_count_exit_le, loop3_count_def. *) 2078val loop3_modify_count_exit_le = store_thm( 2079 "loop3_modify_count_exit_le", 2080 ``!loop guard body quit exit modify transform convert R. 2081 WF R /\ (!x y z. ~guard x y z ==> R (convert x, transform y,modify z) (x,y,z)) /\ 2082 (!x y z. loop x y z = 2083 if guard x y z then quit x y z 2084 else body x y z + if exit x y z then 0 else loop (convert x) (transform y) (modify z)) ==> 2085 !x y z. loop x y z <= quit (FUNPOW convert (loop3_count guard modify transform convert x y z) x) 2086 (FUNPOW transform (loop3_count guard modify transform convert x y z) y) 2087 (FUNPOW modify (loop3_count guard modify transform convert x y z) z) + 2088 SUM (GENLIST (\j. body (FUNPOW convert j x) (FUNPOW transform j y) (FUNPOW modify j z)) 2089 (loop3_count guard modify transform convert x y z))``, 2090 rpt strip_tac >> 2091 assume_tac (loop_modify_count_exit_le 2092 |> SPEC_ALL |> INST_TYPE [``:'a`` |-> ``:'a # 'b # 'c``] 2093 |> SIMP_RULE bool_ss [pairTheory.FORALL_PROD] 2094 |> Q.INST [`loop` |-> `(\(x,y,z). lp x y z)`, `guard` |-> `(\(x,y,z). gd x y z)`, 2095 `quit` |-> `(\(x,y,z). qt x y z)`, `body` |-> `(\(x,y,z). b x y z)`, 2096 `modify` |-> `(\(x,y,z). (c x, t y, m z))`, `exit` |-> `(\(x,y,z). et x y z)`] 2097 |> SIMP_RULE bool_ss [FUNPOW_TRIPLE, GSYM loop3_count_def] 2098 |> Q.INST [`lp` |-> `loop`, `gd` |-> `guard`, `qt` |-> `quit`, `b` |-> `body`, 2099 `et` |-> `exit`, `c` |-> `convert`, `t` |-> `transform`, `m` |-> `modify`] 2100 |> PairRules.PBETA_RULE) >> 2101 qabbrev_tac `foo1 = !x y z. ~guard x y z ==> R (convert x,transform y,modify z) (x,y,z)` >> 2102 qabbrev_tac `foo2 = !x y z. loop x y z = if guard x y z then quit x y z else body x y z + if exit x y z then 0 else loop (convert x) (transform y) (modify z)` >> 2103 metis_tac[]); 2104 2105(* ------------------------------------------------------------------------- *) 2106(* Original investigation, some with quit = constant, name has _quitc_ *) 2107(* ------------------------------------------------------------------------- *) 2108 2109(* Define a loop argument list to capture the process of recurrence. *) 2110(* Use a schema to figure out the hypothesis. *) 2111val loop_arg_def = TotalDefn.DefineSchema` 2112 loop_arg (x:'a) = 2113 if guard x then [] else x :: loop_arg (modify x) 2114`; 2115(* 2116val loop_arg_def = 2117 [..] |- !x. loop_arg guard modify x = 2118 if guard x then [] else x::loop_arg guard modify (modify x): thm 2119to see the [..], which is hypothesis, 2120> hyp loop_arg_def; 2121val it = [``!x. ~guard x ==> R (modify x) x``, ``WF R``]: term list 2122 2123> loop_arg_def |> hyp; 2124val it = [``!x. ~guard x ==> R (modify x) x``, ``WF R``]: term list 2125 2126``!(x :'a). ~(guard :'a -> bool) x ==> (R :'a -> 'a -> bool) ((modify :'a -> 'a) x) x``, 2127``WF (R :'a -> 'a -> bool)`` 2128 2129> loop_arg_def |> DISCH_ALL |> GEN_ALL; 2130val it = |- !modify guard R. WF R ==> (!x. ~guard x ==> R (modify x) x) ==> 2131 !x. loop_arg guard modify x = if guard x then [] else x::loop_arg guard modify (modify x): thm 2132*) 2133 2134(* Obtain theorem from loop_count definition *) 2135val loop_arg_thm = save_thm("loop_arg_thm", 2136 loop_arg_def |> DISCH_ALL |> SIMP_RULE bool_ss [AND_IMP_INTRO] |> GEN_ALL); 2137(* val loop_arg_thm = 2138 |- !modify guard R. WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 2139 !x. loop_arg guard modify x = 2140 if guard x then [] else x::loop_arg guard modify (modify x): thm 2141*) 2142 2143(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 2144 !x. guard x ==> (loop_arg guard modify x = []) *) 2145(* Proof: by loop_arg_def *) 2146val loop_arg_nil = store_thm( 2147 "loop_arg_nil", 2148 ``!modify guard R. WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 2149 !x. guard x ==> (loop_arg guard modify x = [])``, 2150 rpt strip_tac >> 2151 rw[Once loop_arg_def]); 2152 2153(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 2154 !x. ~guard x ==> (loop_arg guard modify x = x :: loop_arg guard modify (modify x)) *) 2155(* Proof: by loop_arg_def *) 2156val loop_arg_cons = store_thm( 2157 "loop_arg_cons", 2158 ``!modify guard R. WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 2159 !x. ~guard x ==> (loop_arg guard modify x = x :: loop_arg guard modify (modify x))``, 2160 rpt strip_tac >> 2161 rw[Once loop_arg_def]); 2162 2163(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 2164 !x. LENGTH (loop_arg guard modify x) = loop_count guard modify x *) 2165(* Proof: 2166 By induction from loop_arg_def. 2167 If guard x, 2168 LENGTH (loop_arg guard modify x) 2169 = LENGTH [] by loop_arg_nil, guard x. 2170 = 0 by LENGTH 2171 = loop_count guard modify x by loop_count_0 2172 If ~guard x, 2173 LENGTH (loop_arg guard modify x) 2174 = LENGTH (x:: loop_arg guard modify (modify x)) by loop_arg_cons, ~guard x. 2175 = SUC (LENGTH loop_arg guard modify (modify x)) by LENGTH 2176 = SUC (loop_count guard modify (modify x)) by induction hypothesis 2177 = loop_count guard modify x by loop_count_suc 2178*) 2179val loop_arg_length = store_thm( 2180 "loop_arg_length", 2181 ``!modify guard R. WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 2182 !x. LENGTH (loop_arg guard modify x) = loop_count guard modify x``, 2183 ntac 4 strip_tac >> 2184 ho_match_mp_tac (theorem "loop_arg_ind") >> 2185 rpt strip_tac >> 2186 Cases_on `guard x` >- 2187 metis_tac[loop_arg_nil, loop_count_0, LENGTH] >> 2188 metis_tac[loop_arg_cons, loop_count_suc, LENGTH]); 2189 2190(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 2191 !x. loop_arg guard modify x = GENLIST (\j. FUNPOW modify j x) (loop_count guard modify x) *) 2192(* Proof: 2193 By induction from loop_arg_def. 2194 If guard x, 2195 LHS = loop_arg guard modify x = [] by loop_arg_nil, guard x 2196 RHS = GENLIST (\j. FUNPOW modify j x) (loop_count guard modify x) 2197 = GENLIST (\j. FUNPOW modify j x) 0 by loop_count_0, guard x 2198 = [] = LHS by GENLIST_0 2199 If ~guard x, 2200 Let f = \j. FUNPOW modify j x, n = loop_count guard modify (modify x). 2201 Then f o SUC = \j. FUNPOW modify j (modify x) by FUN_EQ_THM 2202 and f 0 = x by notation 2203 loop_arg guard modify x 2204 = x::loop_arg guard modify (modify x) by loop_arg_cons 2205 = x:: GENLIST (\j. FUNPOW modify j (modify x)) n by induction hypothesis 2206 = f 0:: GENLIST (f o SUC) n by above 2207 = GENLIST f (SUC n) by GENLIST_CONS 2208 = GENLIST f (loop_count guard modify x) by loop_count_suc 2209*) 2210val loop_arg_eqn = store_thm( 2211 "loop_arg_eqn", 2212 ``!modify guard R. WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 2213 !x. loop_arg guard modify x = GENLIST (\j. FUNPOW modify j x) (loop_count guard modify x)``, 2214 ntac 4 strip_tac >> 2215 ho_match_mp_tac (theorem "loop_arg_ind") >> 2216 rpt strip_tac >> 2217 Cases_on `guard x` >- 2218 metis_tac[loop_arg_nil, loop_count_0, GENLIST_0] >> 2219 qabbrev_tac `f = \j. FUNPOW modify j x` >> 2220 qabbrev_tac `n = loop_count guard modify (modify x)` >> 2221 `f o SUC = \j. FUNPOW modify j (modify x)` by rw[FUNPOW, FUN_EQ_THM, Abbr`f`] >> 2222 `f 0 = x` by rw[Abbr`f`] >> 2223 `loop_arg guard modify x = x::loop_arg guard modify (modify x)` by metis_tac[loop_arg_cons] >> 2224 `_ = f 0:: GENLIST (f o SUC) n` by rw[Abbr`n`] >> 2225 `SUC n = loop_count guard modify x` by metis_tac[loop_count_suc] >> 2226 rw[GSYM GENLIST_CONS, Abbr`n`]); 2227 2228(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 2229 !x k. k < loop_count guard modify x ==> 2230 (EL k (loop_arg guard modify x) = FUNPOW modify k x) *) 2231(* Proof: 2232 Let f = (\j. FUNPOW modify j x), ls = loop_arg guard modify x. 2233 Note LENGTH ls 2234 = loop_count guard modify x by loop_arg_length 2235 EL k ls 2236 = EL k (GENLIST f (LENGTH ls)) by loop_arg_eqn 2237 = f k by EL_GENLIST, k < LENGTH ls 2238 = FUNPOW modify k x by notation 2239*) 2240val loop_arg_element = store_thm( 2241 "loop_arg_element", 2242 ``!modify guard R. WF R /\ (!x. ~guard x ==> R (modify x) x) ==> 2243 !x k. k < loop_count guard modify x ==> (EL k (loop_arg guard modify x) = FUNPOW modify k x)``, 2244 rpt strip_tac >> 2245 imp_res_tac loop_arg_eqn >> 2246 first_x_assum (qspec_then `x` strip_assume_tac) >> 2247 qabbrev_tac `f = \j. FUNPOW modify j x` >> 2248 qabbrev_tac `ls = loop_arg guard modify x` >> 2249 `LENGTH ls = loop_count guard modify x` by metis_tac[loop_arg_length] >> 2250 fs[EL_GENLIST, Abbr`ls`, Abbr`f`]); 2251 2252(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 2253 (!x y. R x y ==> cover x <= cover y) ==> 2254 !x. SUM (MAP cover (loop_arg guard modify x)) <= 2255 SUM (MAP (K (cover x)) (loop_arg guard modify x)) *) 2256(* Proof: 2257 By induction from loop_arg_def. 2258 Let ls = loop_arg guard modify x, 2259 the goal is: SUM (MAP cover ls) <= SUM (MAP (K (cover x)) ls) 2260 2261 If guard x, 2262 Then ls = [] by loop_arg_nil 2263 LHS = SUM (MAP cover []) 2264 = SUM [] by MAP 2265 = SUM (MAP (K (cover x)) []) by MAP 2266 = RHS 2267 If ~guard x, 2268 Then ls = x::loop_arg guard modify (modify x) by loop_arg_cons 2269 and R (modify x) x by given 2270 so cover (modify x) <= cover x by cover property 2271 SUM (MAP cover ls) 2272 = SUM (MAP cover (x::loop_arg guard modify (modify x))) by ls above 2273 = cover x + SUM (MAP cover (loop_arg guard modify (modify x))) by SUM, MAP 2274 <= cover x + SUM (MAP (K (cover (modify x))) (loop_arg guard modify (modify x))) by induction hypothesis 2275 <= cover x + SUM (MAP (K (cover x)) (loop_arg guard modify (modify x)) by SUM_MAP_K_LE 2276 = SUM (MAP (K (cover x) x::(loop_arg guard modify (modify x)))) by SUM, MAP 2277 = SUM (MAP (K (cover x) ls)) by ls above 2278*) 2279val loop_arg_cover_sum = store_thm( 2280 "loop_arg_cover_sum", 2281 ``!modify guard R cover. 2282 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 2283 (!x y. R x y ==> cover x <= cover y) ==> 2284 !x. SUM (MAP cover (loop_arg guard modify x)) <= 2285 SUM (MAP (K (cover x)) (loop_arg guard modify x))``, 2286 ntac 5 strip_tac >> 2287 ho_match_mp_tac (theorem "loop_arg_ind") >> 2288 rw[] >> 2289 qabbrev_tac `ls = loop_arg guard modify x` >> 2290 Cases_on `guard x` >| [ 2291 `ls = []` by metis_tac[loop_arg_nil] >> 2292 rw[], 2293 qabbrev_tac `t = loop_arg guard modify (modify x)` >> 2294 `ls = x::t` by metis_tac[loop_arg_cons] >> 2295 `cover (modify x) <= cover x` by rw[] >> 2296 `SUM (MAP cover ls) = cover x + SUM (MAP cover t)` by rw[] >> 2297 `SUM (MAP cover t) <= SUM (MAP (K (cover (modify x))) t)` by rw[Abbr`t`] >> 2298 `SUM (MAP (K (cover (modify x))) t) <= SUM (MAP (K (cover x)) t)` by rw[SUM_MAP_K_LE] >> 2299 `cover x + SUM (MAP (K (cover x)) t) = SUM (MAP (K (cover x)) ls)` by rw[] >> 2300 decide_tac 2301 ]); 2302 2303(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 2304 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 2305 !x. loop x = c + SUM (MAP body (loop_arg guard modify x)) *) 2306(* Proof: 2307 By induction from loop_arg_def. 2308 If guard x, 2309 LHS = loop x = c by loop property, guard x. 2310 RHS = c + SUM (MAP body (loop_arg guard modify x)) 2311 = c + SUM (MAP body []) by loop_arg_nil, guard x. 2312 = c + 0 by MAP, SUM 2313 = c = LHS by arithmetic 2314 If ~guard x, 2315 loop x 2316 = body x + loop (modify x) by loop property, ~guard x. 2317 = body x + (c + SUM (MAP body (loop_arg guard modify (modify x)))) 2318 by induction hypothesis 2319 = c + (body x + SUM (MAP body (loop_arg guard modify (modify x)))) 2320 by arithmetic 2321 = c + SUM (MAP body (x :: (loop_arg guard modify (modify x)))) by MAP, SUM 2322 = c + SUM (MAP body (loop_arg guard modify x)) by loop_arg_cons, ~guard x 2323*) 2324val loop_modify_count_by_sum = store_thm( 2325 "loop_modify_count_by_sum", 2326 ``!loop guard body c modify R. 2327 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 2328 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 2329 !x. loop x = c + SUM (MAP body (loop_arg guard modify x))``, 2330 ntac 7 strip_tac >> 2331 ho_match_mp_tac (theorem "loop_arg_ind") >> 2332 rpt strip_tac >> 2333 Cases_on `guard x` >| [ 2334 `loop x = c` by metis_tac[] >> 2335 `loop_arg guard modify x = []` by metis_tac[loop_arg_nil] >> 2336 metis_tac[SUM, MAP, ADD_0], 2337 `loop x = body x + loop (modify x)` by metis_tac[] >> 2338 `_ = c + SUM (MAP body (x :: (loop_arg guard modify (modify x))))` by rw[] >> 2339 `_ = c + SUM (MAP body (loop_arg guard modify x))` by metis_tac[loop_arg_cons] >> 2340 decide_tac 2341 ]); 2342 2343(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 2344 (!x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)) ==> 2345 !x. loop x <= c + SUM (MAP body (loop_arg guard modify x)) *) 2346(* Proof: 2347 By induction from loop_arg_def. 2348 If guard x, 2349 LHS = loop x = c by loop property, guard x. 2350 RHS = c + SUM (MAP body (loop_arg guard modify x)) 2351 = c + SUM (MAP body []) by loop_arg_nil, guard x. 2352 = c + 0 by MAP, SUM 2353 = c >= LHS by LESS_EQ_REFL 2354 If ~guard x, 2355 loop x 2356 <= body x + loop (modify x) by loop property, ~guard x, cases on exit x. 2357 <= body x + (c + SUM (MAP body (loop_arg guard modify (modify x)))) 2358 by induction hypothesis 2359 = c + (body x + SUM (MAP body (loop_arg guard modify (modify x)))) 2360 by arithmetic 2361 = c + SUM (MAP body (x :: (loop_arg guard modify (modify x)))) by MAP, SUM 2362 = c + SUM (MAP body (loop_arg guard modify x)) by loop_arg_cons, ~guard x 2363*) 2364val loop_modify_count_exit_by_sum = store_thm( 2365 "loop_modify_count_exit_by_sum", 2366 ``!loop guard body c exit modify R. 2367 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 2368 (!x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)) ==> 2369 !x. loop x <= c + SUM (MAP body (loop_arg guard modify x))``, 2370 ntac 8 strip_tac >> 2371 ho_match_mp_tac (theorem "loop_arg_ind") >> 2372 rpt strip_tac >> 2373 Cases_on `guard x` >| [ 2374 `loop x = c` by metis_tac[] >> 2375 `loop_arg guard modify x = []` by metis_tac[loop_arg_nil] >> 2376 metis_tac[SUM, MAP, ADD_0, LESS_EQ_REFL], 2377 `loop x <= body x + loop (modify x)` by 2378 (Cases_on `exit x` >| [ 2379 `loop x = body x` by metis_tac[ADD_0] >> 2380 decide_tac, 2381 `loop x = body x + loop (modify x)` by metis_tac[] >> 2382 decide_tac 2383 ]) >> 2384 `body x + loop (modify x) <= 2385 body x + (c + SUM (MAP body (loop_arg guard modify (modify x))))` by metis_tac[ADD_MONO_LESS_EQ] >> 2386 `body x + (c + SUM (MAP body (loop_arg guard modify (modify x)))) = 2387 c + SUM (MAP body (x :: (loop_arg guard modify (modify x))))` by rw[] >> 2388 `_ = c + SUM (MAP body (loop_arg guard modify x))` by metis_tac[loop_arg_cons] >> 2389 decide_tac 2390 ]); 2391 2392(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 2393 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 2394 !x. loop x = c + SUM (GENLIST (\j. body (FUNPOW modify j x)) (loop_count guard modify x)) *) 2395(* Proof: 2396 Let f = (\j. FUNPOW modify j x), 2397 n = loop_count guard modify x. 2398 loop x 2399 = c + SUM (MAP body (loop_arg guard modify x)) by loop_modify_count_by_sum 2400 = c + SUM (MAP body (GENLIST f n)) by loop_arg_eqn 2401 = c + SUM (GENLIST (body o f) n) by MAP_GENLIST 2402 = c + SUM (GENLIST (\j. body (FUNPOW modify j x)) (loop_count guard modify x)) 2403*) 2404val loop_modify_count_quitc_eqn = store_thm( 2405 "loop_modify_count_quitc_eqn", 2406 ``!loop guard body c modify R. 2407 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 2408 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 2409 !x. loop x = c + SUM (GENLIST (\j. body (FUNPOW modify j x)) (loop_count guard modify x))``, 2410 rpt strip_tac >> 2411 imp_res_tac loop_modify_count_by_sum >> 2412 first_x_assum (qspec_then `x` strip_assume_tac) >> 2413 imp_res_tac loop_arg_eqn >> 2414 first_x_assum (qspec_then `x` strip_assume_tac) >> 2415 qabbrev_tac `ls = loop_arg guard modify x` >> 2416 qabbrev_tac `n = loop_count guard modify x` >> 2417 qabbrev_tac `f = \j. FUNPOW modify j x` >> 2418 qabbrev_tac `g = \j. body (FUNPOW modify j x)` >> 2419 `g = body o f` by rw[FUN_EQ_THM, Abbr`g`, Abbr`f`] >> 2420 metis_tac[MAP_GENLIST]); 2421 2422(* Note: this is the solution of the recurrence: 2423 2424 Given: !x. loop x = if guard x then c else body x + loop (modify x) 2425 Then: loop x = c + SUM [body x, body (modify x), body (modify (modify x)), .....] 2426 for n terms, where n = loop_count guard modify x 2427*) 2428 2429(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 2430 (!x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)) ==> 2431 !x. loop x <= c + SUM (GENLIST (\j. body (FUNPOW modify j x)) (loop_count guard modify x)) *) 2432(* Proof: 2433 Let f = (\j. FUNPOW modify j x), 2434 n = loop_count guard modify x. 2435 loop x 2436 <= c + SUM (MAP body (loop_arg guard modify x)) by loop_modify_count_exit_by_sum 2437 = c + SUM (MAP body (GENLIST f n)) by loop_arg_eqn 2438 = c + SUM (GENLIST (body o f) n) by MAP_GENLIST 2439 = c + SUM (GENLIST (\j. body (FUNPOW modify j x)) (loop_count guard modify x)) 2440*) 2441val loop_modify_count_quitc_exit_le = store_thm( 2442 "loop_modify_count_quitc_exit_le", 2443 ``!loop guard body c exit modify R. 2444 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 2445 (!x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)) ==> 2446 !x. loop x <= c + SUM (GENLIST (\j. body (FUNPOW modify j x)) (loop_count guard modify x))``, 2447 rpt strip_tac >> 2448 imp_res_tac loop_modify_count_exit_by_sum >> 2449 first_x_assum (qspec_then `x` strip_assume_tac) >> 2450 imp_res_tac loop_arg_eqn >> 2451 first_x_assum (qspec_then `x` strip_assume_tac) >> 2452 qabbrev_tac `ls = loop_arg guard modify x` >> 2453 qabbrev_tac `n = loop_count guard modify x` >> 2454 qabbrev_tac `f = \j. FUNPOW modify j x` >> 2455 qabbrev_tac `g = \j. body (FUNPOW modify j x)` >> 2456 `g = body o f` by rw[FUN_EQ_THM, Abbr`g`, Abbr`f`] >> 2457 metis_tac[MAP_GENLIST]); 2458 2459 2460(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 2461 (!x. body x <= cover x) /\ (!x y. R x y ==> cover x <= cover y) /\ 2462 (!x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)) ==> 2463 !x. loop x <= c + cover x * loop_count guard modify x *) 2464(* Proof: 2465 Let ls = loop_arg guard modify x. 2466 loop x 2467 <= c + SUM (MAP body ls) by loop_modify_count_exit_by_sum 2468 <= c + SUM (MAP cover ls) by SUM_LE, loop_arg_length, EL_MAP, body and cover 2469 <= c + SUM (MAP (K (cover x)) ls) by loop_arg_cover_sum, cover property 2470 = (cover x) * LENGTH ls by SUM_MAP_K 2471 = (cover x) * (loop_count guard modify x) by loop_arg_length 2472*) 2473val loop_modify_count_cover_exit_upper = store_thm( 2474 "loop_modify_count_cover_exit_upper", 2475 ``!loop guard body c cover exit modify R. 2476 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 2477 (!x. body x <= cover x) /\ (!x y. R x y ==> cover x <= cover y) /\ 2478 (!x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)) ==> 2479 !x. loop x <= c + cover x * loop_count guard modify x``, 2480 rpt strip_tac >> 2481 qabbrev_tac `ls = loop_arg guard modify x` >> 2482 `loop x <= c + SUM (MAP body ls)` by metis_tac[loop_modify_count_exit_by_sum] >> 2483 `SUM (MAP body ls) <= SUM (MAP cover ls)` by 2484 (irule SUM_LE >> 2485 rw[loop_arg_length, EL_MAP]) >> 2486 `SUM (MAP cover ls) <= SUM (MAP (K (cover x)) ls)` by metis_tac[loop_arg_cover_sum] >> 2487 `SUM (MAP (K (cover x)) ls) = (cover x) * LENGTH ls` by rw[SUM_MAP_K] >> 2488 `_ = (cover x) * (loop_count guard modify x)` by metis_tac[loop_arg_length] >> 2489 decide_tac); 2490 2491(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 2492 (!x y. R x y ==> body x <= body y) /\ 2493 (!x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)) ==> 2494 !x. loop x <= c + body x * loop_count guard modify x *) 2495(* Proof: by loop_modify_count_cover_exit_upper with cover = body. *) 2496val loop_modify_count_exit_upper = store_thm( 2497 "loop_modify_count_exit_upper", 2498 ``!loop guard body c exit modify R. 2499 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 2500 (!x y. R x y ==> body x <= body y) /\ 2501 (!x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)) ==> 2502 !x. loop x <= c + body x * loop_count guard modify x``, 2503 rpt strip_tac >> 2504 assume_tac loop_modify_count_cover_exit_upper >> 2505 last_x_assum (qspecl_then [`loop`, `guard`, `body`, `c`, `body`, `exit`, `modify`, `R`] strip_assume_tac) >> 2506 metis_tac[LESS_EQ_REFL]); 2507 2508(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 2509 (!x. body x <= cover x) /\ (!x y. R x y ==> cover x <= cover y) /\ 2510 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 2511 !x. loop x <= c + cover x * loop_count guard modify x *) 2512(* Proof: by loop_modify_count_cover_exit_upper with exit = K F. *) 2513val loop_modify_count_cover_upper = store_thm( 2514 "loop_modify_count_cover_upper", 2515 ``!loop guard body c cover modify R. 2516 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 2517 (!x. body x <= cover x) /\ (!x y. R x y ==> cover x <= cover y) /\ 2518 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 2519 !x. loop x <= c + cover x * loop_count guard modify x``, 2520 rpt strip_tac >> 2521 qabbrev_tac `exit = (\x:'a. F)` >> 2522 assume_tac loop_modify_count_cover_exit_upper >> 2523 last_x_assum (qspecl_then [`loop`, `guard`, `body`, `c`, `cover`, `exit`, `modify`, `R`] strip_assume_tac) >> 2524 metis_tac[]); 2525 2526(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 2527 (!x y. R x y ==> body x <= body y) /\ 2528 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 2529 !x. loop x <= c + body x * loop_count guard modify x *) 2530(* Proof: by loop_modify_count_cover_upper with body = cover. *) 2531val loop_modify_count_upper = store_thm( 2532 "loop_modify_count_upper", 2533 ``!loop guard body c modify R. 2534 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ 2535 (!x y. R x y ==> body x <= body y) /\ 2536 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 2537 !x. loop x <= c + body x * loop_count guard modify x``, 2538 rpt strip_tac >> 2539 assume_tac loop_modify_count_cover_upper >> 2540 last_x_assum (qspecl_then [`loop`, `guard`, `body`, `c`, `body`, `modify`, `R`] strip_assume_tac) >> 2541 metis_tac[LESS_EQ_REFL]); 2542 2543(* ------------------------------------------------------------------------- *) 2544(* General Theory of Recurrence with 2 arguments *) 2545(* ------------------------------------------------------------------------- *) 2546 2547(* 2548> loop_count_def |> DISCH_ALL |> INST_TYPE [alpha |-> ``:'a # 'b``] 2549 |> SIMP_RULE (srw_ss()) [pairTheory.FORALL_PROD] 2550 |> Q.INST [`guard` |-> `(\(x,y). gd x y)`, `modify` |-> `(\(x,y). (t x, m y))`] 2551 |> SIMP_RULE (srw_ss()) []; 2552val it = |- WF R ==> (!p_1 p_2. ~gd p_1 p_2 ==> R (t p_1,m p_2) (p_1,p_2)) ==> 2553 !p_1 p_2. loop_count (\(x,y). gd x y) (\(x,y). (t x,m y)) (p_1,p_2) = 2554 if gd p_1 p_2 then 0 else 2555 SUC (loop_count (\(x,y). gd x y) (\(x,y). (t x,m y)) (t p_1,m p_2)): thm 2556> loop_arg_def |> DISCH_ALL |> INST_TYPE [alpha |-> ``:'a # 'b``] 2557 |> SIMP_RULE (srw_ss()) [pairTheory.FORALL_PROD] 2558 |> Q.INST [`guard` |-> `(\(x,y). gd x y)`, `modify` |-> `(\(x,y). (t x, m y))`] 2559 |> SIMP_RULE (srw_ss()) []; 2560val it = |- WF R ==> (!p_1 p_2. ~gd p_1 p_2 ==> R (t p_1,m p_2) (p_1,p_2)) ==> 2561 !p_1 p_2. loop_arg (\(x,y). gd x y) (\(x,y). (t x,m y)) (p_1,p_2) = 2562 if gd p_1 p_2 then [] else 2563 (p_1,p_2):: loop_arg (\(x,y). gd x y) (\(x,y). (t x,m y)) (t p_1,m p_2): thm 2564*) 2565 2566(* Define loop_count for 2 arguments *) 2567 2568(* Define loop_arg for 2 arguments *) 2569val loop2_arg_def = Define` 2570 loop2_arg guard modify transform x y = 2571 loop_arg (\(x,y). guard x y) (\(x,y). (transform x, modify y)) (x, y) 2572`; 2573 2574(* Obtain theorem by transform: 2575 2576val loop2_count_thm = save_thm("loop2_count_thm", 2577 loop_count_thm |> SPEC_ALL |> INST_TYPE [alpha |-> ``:'a # 'b``] 2578 |> SIMP_RULE (srw_ss()) [pairTheory.FORALL_PROD] 2579 |> Q.INST [`guard` |-> `(\(x,y). gd x y)`, `modify` |-> `(\(x,y). (t x, m y))`] 2580 |> SIMP_RULE (srw_ss()) [GSYM loop2_count_def] |> GEN_ALL); 2581 2582val loop2_count_thm = 2583 |- !t m gd R. WF R /\ (!p_1 p_2. ~gd p_1 p_2 ==> R (t p_1,m p_2) (p_1,p_2)) ==> 2584 !p_1 p_2. loop2_count gd m t p_1 p_2 = 2585 if gd p_1 p_2 then 0 else SUC (loop2_count gd m t (t p_1) (m p_2)): thm 2586 2587loop_count_0 |> SPEC_ALL |> INST_TYPE [alpha |-> ``:'a # 'b``] 2588 |> SIMP_RULE (srw_ss()) [pairTheory.FORALL_PROD] 2589 |> Q.INST [`guard` |-> `(\(x,y). gd x y)`, `modify` |-> `(\(x,y). (t x, m y))`] 2590 |> SIMP_RULE (srw_ss()) [GSYM loop2_count_def] |> GEN_ALL 2591 |> CONV_RULE (RENAME_VARS_CONV ["transform", "modify", "guard"]); 2592 2593loop_count_0 |> SPEC_ALL |> INST_TYPE [alpha |-> ``:'a # 'b``] 2594 |> SIMP_RULE (srw_ss()) [pairTheory.FORALL_PROD] 2595 |> Q.INST [`guard` |-> `(\(x,y). gd x y)`, `modify` |-> `(\(x,y). (t x, m y))`] 2596 |> SIMP_RULE (srw_ss()) [GSYM loop2_count_def] 2597 |> Q.INST [`gd` |-> `guard`, `t` |-> `transform`, `m` |-> `modify`] 2598 |> GEN_ALL; 2599*) 2600 2601 2602(* Obtain theorems by transform *) 2603fun loop2_thm_type_a suffix = let 2604 val th1 = DB.fetch "loop" ("loop_" ^ suffix) 2605 val th2 = th1 |> SPEC_ALL |> INST_TYPE [alpha |-> ``:'a # 'b``] 2606 |> SIMP_RULE (srw_ss()) [pairTheory.FORALL_PROD] 2607 |> Q.INST [`guard` |-> `(\(x,y). gd x y)`, `modify` |-> `(\(x,y). (t x, m y))`] 2608 |> SIMP_RULE (srw_ss()) [GSYM loop2_count_def, GSYM loop2_arg_def] |> GEN_ALL 2609 |> CONV_RULE (RENAME_VARS_CONV ["transform", "modify", "guard"]) 2610in 2611 save_thm("loop2_" ^ suffix, th2 |> DISCH_ALL |> GEN_ALL) 2612end; 2613 2614 2615val loop2_arg_thm = loop2_thm_type_a "arg_thm"; 2616(* val loop2_arg_thm = |- !transform modify guard R. 2617 WF R /\ (!p_1 p_2. ~guard p_1 p_2 ==> R (transform p_1,modify p_2) (p_1,p_2)) ==> 2618 !p_1 p_2. loop2_arg guard modify transform p_1 p_2 = 2619 if guard p_1 p_2 then [] 2620 else (p_1,p_2):: loop2_arg guard modify transform (transform p_1) (modify p_2): thm 2621*) 2622 2623val loop2_arg_nil = loop2_thm_type_a "arg_nil"; 2624(* val loop2_arg_nil = |- !transform modify guard R. 2625 WF R /\ (!p_1 p_2. ~guard p_1 p_2 ==> R (transform p_1,modify p_2) (p_1,p_2)) ==> 2626 !p_1 p_2. guard p_1 p_2 ==> (loop2_arg guard modify transform p_1 p_2 = []): thm 2627*) 2628 2629val loop2_arg_cons = loop2_thm_type_a "arg_cons"; 2630(* val loop2_arg_cons = |- !transform modify guard R. 2631 WF R /\ (!p_1 p_2. ~guard p_1 p_2 ==> R (transform p_1,modify p_2) (p_1,p_2)) ==> 2632 !p_1 p_2. ~guard p_1 p_2 ==> 2633 (loop2_arg guard modify transform p_1 p_2 = 2634 (p_1,p_2)::loop2_arg guard modify transform (transform p_1) (modify p_2)): thm 2635*) 2636 2637val loop2_arg_length = loop2_thm_type_a "arg_length"; 2638(* val loop2_arg_length = |- !transform modify guard R. 2639 WF R /\ (!p_1 p_2. ~guard p_1 p_2 ==> R (transform p_1,modify p_2) (p_1,p_2)) ==> 2640 !p_1 p_2. LENGTH (loop2_arg guard modify transform p_1 p_2) = 2641 loop2_count guard modify transform p_1 p_2: thm 2642*) 2643 2644val loop2_arg_eqn = loop2_thm_type_a "arg_eqn"; 2645(* val loop2_arg_eqn = |- !transform modify guard R. 2646 WF R /\ (!p_1 p_2. ~guard p_1 p_2 ==> R (transform p_1,modify p_2) (p_1,p_2)) ==> 2647 !p_1 p_2. loop2_arg guard modify transform p_1 p_2 = 2648 GENLIST (\j. FUNPOW (\(x,y). (transform x,modify y)) j (p_1,p_2)) 2649 (loop2_count guard modify transform p_1 p_2): thm 2650 2651*) 2652 2653val loop2_arg_element = loop2_thm_type_a "arg_element"; 2654(* val loop2_arg_element = |- !transform modify guard R. 2655 WF R /\ (!p_1 p_2. ~guard p_1 p_2 ==> R (transform p_1,modify p_2) (p_1,p_2)) ==> 2656 !p_1 p_2 k. k < loop2_count guard modify transform p_1 p_2 ==> 2657 (EL k (loop2_arg guard modify transform p_1 p_2) = 2658 FUNPOW (\(x,y). (transform x,modify y)) k (p_1,p_2)): thm 2659*) 2660 2661val loop2_arg_cover_sum = loop2_thm_type_a "arg_cover_sum"; 2662(* val loop2_arg_cover_sum = |- !transform modify guard cover R. 2663 WF R /\ (!p_1 p_2. ~guard p_1 p_2 ==> R (transform p_1,modify p_2) (p_1,p_2)) /\ 2664 (!p_1 p_2 p_1' p_2'. R (p_1,p_2) (p_1',p_2') ==> 2665 cover (p_1,p_2) <= cover (p_1',p_2')) ==> 2666 !p_1 p_2. 2667 SUM (MAP cover (loop2_arg guard modify transform p_1 p_2)) <= 2668 SUM (MAP (K (cover (p_1,p_2))) (loop2_arg guard modify transform p_1 p_2)): thm 2669*) 2670 2671(* Not using theorem transform *) 2672 2673 2674val loop2_arg_thm = store_thm( 2675 "loop2_arg_thm", 2676 ``!transform modify guard R. 2677 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> 2678 !x y. loop2_arg guard modify transform x y = 2679 if guard x y then [] 2680 else (x,y)::(loop2_arg guard modify transform (transform x) (modify y))``, 2681 rw[loop2_arg_def] >> 2682 imp_res_tac loop_arg_thm >> 2683 rw[Once pairTheory.FORALL_PROD]); 2684 2685val loop2_arg_nil = store_thm( 2686 "loop2_arg_nil", 2687 ``!transform modify guard R. 2688 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> 2689 !x y. guard x y ==> (loop2_arg guard modify transform x y = [])``, 2690 rw[loop2_arg_def] >> 2691 imp_res_tac loop_arg_nil >> 2692 rw[Once pairTheory.FORALL_PROD]); 2693 2694val loop2_arg_cons = store_thm( 2695 "loop2_arg_cons", 2696 ``!transform modify guard R. 2697 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> 2698 !x y. ~guard x y ==> (loop2_arg guard modify transform x y = 2699 (x,y)::(loop2_arg guard modify transform (transform x) (modify y)))``, 2700 rw[loop2_arg_def] >> 2701 imp_res_tac loop_arg_cons >> 2702 rw[Once pairTheory.FORALL_PROD]); 2703 2704val loop2_arg_length = store_thm( 2705 "loop2_arg_length", 2706 ``!transform modify guard R. 2707 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> 2708 !x y. LENGTH (loop2_arg guard modify transform x y) = 2709 loop2_count guard modify transform x y``, 2710 rw[loop2_arg_def, loop2_count_def] >> 2711 imp_res_tac loop_arg_length >> 2712 rw[Once pairTheory.FORALL_PROD]); 2713 2714(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> 2715 !x y. loop2_arg guard modify transform x y = 2716 GENLIST (\j. (FUNPOW transform j x,FUNPOW modify j y)) 2717 (loop2_count guard modify transform x y) *) 2718(* Proof: by loop_arg_eqn, loop2_arg_def, loop2_count_def *) 2719val loop2_arg_eqn = store_thm( 2720 "loop2_arg_eqn", 2721 ``!transform modify guard R. 2722 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> 2723 !x y. loop2_arg guard modify transform x y = 2724 GENLIST (\j. (FUNPOW transform j x,FUNPOW modify j y)) 2725 (loop2_count guard modify transform x y)``, 2726 rw[loop2_arg_def, loop2_count_def] >> 2727 imp_res_tac loop_arg_eqn >> 2728 rw[Once pairTheory.FORALL_PROD] >> 2729 qabbrev_tac `f1 = \j. FUNPOW (\(x,y). (transform x,modify y)) j (x,y)` >> 2730 qabbrev_tac `f2 = \j. (FUNPOW transform j x,FUNPOW modify j y)` >> 2731 `f1 = f2` by rw[FUN_EQ_THM, FUNPOW_PAIR, Abbr`f1`, Abbr`f2`] >> 2732 rw[]); 2733 2734val loop2_arg_element = store_thm( 2735 "loop2_arg_element", 2736 ``!transform modify guard R. 2737 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> 2738 !x y k. k < loop2_count guard modify transform x y ==> 2739 (EL k (loop2_arg guard modify transform x y) = 2740 (FUNPOW transform k x,FUNPOW modify k y))``, 2741 rw[loop2_arg_def, loop2_count_def] >> 2742 imp_res_tac loop_arg_element >> 2743 rw[Once pairTheory.FORALL_PROD, FUNPOW_PAIR]); 2744 2745(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> 2746 (!x1 x2 y1 y2. R (x1,y1) (x2,y2) ==> cover x1 y1 <= cover x2 y2) ==> 2747 !x y. SUM (MAP (UNCURRY cover) (loop2_arg guard modify transform x y)) <= 2748 SUM (MAP (K (cover x y)) (loop2_arg guard modify transform x y)) *) 2749(* Proof: by loop_arg_cover_sum, loop2_count_def, loop2_arg_def. *) 2750val loop2_arg_cover_sum = store_thm( 2751 "loop2_arg_cover_sum", 2752 ``!transform modify guard cover R. 2753 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> 2754 (!x1 x2 y1 y2. R (x1,y1) (x2,y2) ==> cover x1 y1 <= cover x2 y2) ==> 2755 !x y. SUM (MAP (UNCURRY cover) (loop2_arg guard modify transform x y)) <= 2756 SUM (MAP (K (cover x y)) (loop2_arg guard modify transform x y))``, 2757 rpt strip_tac >> 2758 assume_tac (loop_arg_cover_sum |> SPEC_ALL |> INST_TYPE [alpha |-> ``:'a # 'b``] 2759 |> SIMP_RULE (srw_ss()) [pairTheory.FORALL_PROD] 2760 |> Q.INST [`guard` |-> `(\(x,y). gd x y)`, `modify` |-> `(\(x,y). (t x, m y))`] 2761 |> SIMP_RULE (srw_ss()) [GSYM loop2_arg_def] |> GEN_ALL 2762 |> CONV_RULE (RENAME_VARS_CONV ["transform", "modify", "guard"])) >> 2763 first_x_assum (qspecl_then [`transform`, `modify`, `guard`, `UNCURRY cover`, `R`] strip_assume_tac) >> 2764 fs[]); 2765 2766(* Obtain theorems by transform *) 2767fun loop2_thm_type_b suffix = let 2768 val th1 = DB.fetch "loop" ("loop_" ^ suffix) 2769 val th2 = th1 |> SPEC_ALL |> INST_TYPE [alpha |-> ``:'a # 'b``] 2770 |> SIMP_RULE (srw_ss()) [pairTheory.FORALL_PROD] 2771 |> Q.INST [`guard` |-> `(\(x,y). gd x y)`, `modify` |-> `(\(x,y). (t x, m y))`] 2772 |> SIMP_RULE (srw_ss()) [GSYM loop2_count_def, GSYM loop2_arg_def] |> GEN_ALL 2773 |> CONV_RULE (RENAME_VARS_CONV ["transform", "modify", "guard"]) 2774in 2775 save_thm("loop2_" ^ suffix, th2 |> DISCH_ALL |> GEN_ALL) 2776end; 2777(* Type B is intended for loop and body -- simplification cannot cope with loop. *) 2778 2779(* 2780This works: 2781loop_modify_count_by_sum 2782 |> SPEC_ALL |> INST_TYPE [``:'a`` |-> ``:'a # 'b``] 2783 |> SIMP_RULE (srw_ss()) [pairTheory.FORALL_PROD] 2784 |> Q.INST [`loop` |-> `(\(x,y). lp x y)`, `guard` |-> `(\(x,y). gd x y)`, 2785 `body` |-> `(\(x,y). b x y)`, `modify` |-> `(\(x,y). (t x, m y))`] 2786 |> PairRules.PBETA_RULE; 2787 2788But this fails, as SIMP_RULE cannot handle loop: 2789loop_modify_count_by_sum 2790 |> SPEC_ALL |> INST_TYPE [``:'a`` |-> ``:'a # 'b``] 2791 |> SIMP_RULE (srw_ss()) [pairTheory.FORALL_PROD] 2792 |> Q.INST [`loop` |-> `(\(x,y). lp x y)`, `guard` |-> `(\(x,y). gd x y)`, 2793 `body` |-> `(\(x,y). b x y)`, `modify` |-> `(\(x,y). (t x, m y))`] 2794 |> SIMP_RULE (srw_ss()) [GSYM loop2_count_def, GSYM loop2_arg_def]; 2795*) 2796 2797(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 2798 (!x y. loop x y = if guard x y then c else body x y + loop (transform x) (modify y)) ==> 2799 !x y. loop x y = c + SUM (MAP (UNCURRY body) (loop2_arg guard modify transform x y)) *) 2800(* Proof: by loop_modify_count_by_sum, loop2_arg_def *) 2801val loop2_modify_count_by_sum = store_thm( 2802 "loop2_modify_count_by_sum", 2803 ``!loop guard body c modify transform R. 2804 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 2805 (!x y. loop x y = if guard x y then c else body x y + loop (transform x) (modify y)) ==> 2806 !x y. loop x y = c + SUM (MAP (UNCURRY body) (loop2_arg guard modify transform x y))``, 2807 rpt strip_tac >> 2808 assume_tac (loop_modify_count_by_sum 2809 |> SPEC_ALL |> INST_TYPE [``:'a`` |-> ``:'a # 'b``] 2810 |> SIMP_RULE bool_ss [pairTheory.FORALL_PROD] 2811 |> Q.INST [`loop` |-> `(\(x,y). lp x y)`, `guard` |-> `(\(x,y). gd x y)`, 2812 `body` |-> `(\(x,y). b x y)`, `modify` |-> `(\(x,y). (t x, m y))`] 2813 |> Q.INST [`lp` |-> `loop`, `gd` |-> `guard`, `b` |-> `body`, `t` |-> `transform`, `m` |-> `modify`] 2814 |> PairRules.PBETA_RULE) >> 2815 qabbrev_tac `foo1 = !x y. ~guard x y ==> R (transform x,modify y) (x,y)` >> 2816 qabbrev_tac `foo2 = !x y. loop x y = if guard x y then c else body x y + loop (transform x) (modify y)` >> 2817 `UNCURRY body = \(x,y). body x y` by rw[FUN_EQ_THM] >> 2818 metis_tac[loop2_arg_def]); 2819 2820(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 2821 (!x y. loop x y = if guard x y then c else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 2822 !x y. loop x y <= c + SUM (MAP (UNCURRY body) (loop2_arg guard modify transform x y)) *) 2823(* Proof: by loop_modify_count_exit_by_sum, loop2_arg_def. *) 2824val loop2_modify_count_exit_by_sum = store_thm( 2825 "loop2_modify_count_exit_by_sum", 2826 ``!loop guard body c exit modify transform R. 2827 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 2828 (!x y. loop x y = if guard x y then c else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 2829 !x y. loop x y <= c + SUM (MAP (UNCURRY body) (loop2_arg guard modify transform x y))``, 2830 rpt strip_tac >> 2831 assume_tac (loop_modify_count_exit_by_sum 2832 |> SPEC_ALL |> INST_TYPE [``:'a`` |-> ``:'a # 'b``] 2833 |> SIMP_RULE bool_ss [pairTheory.FORALL_PROD] 2834 |> Q.INST [`loop` |-> `(\(x,y). lp x y)`, `guard` |-> `(\(x,y). gd x y)`, 2835 `body` |-> `(\(x,y). b x y)`, `modify` |-> `(\(x,y). (t x, m y))`, `exit` |-> `(\(x,y). et x y)`] 2836 |> Q.INST [`lp` |-> `loop`, `gd` |-> `guard`, `et` |-> `exit`, `b` |-> `body`, `t` |-> `transform`, `m` |-> `modify`] 2837 |> PairRules.PBETA_RULE) >> 2838 qabbrev_tac `foo1 = !x y. ~guard x y ==> R (transform x,modify y) (x,y)` >> 2839 qabbrev_tac `foo2 = !x y. loop x y = if guard x y then c else body x y + if exit x y then 0 else loop (transform x) (modify y)` >> 2840 `UNCURRY body = \(x,y). body x y` by rw[FUN_EQ_THM] >> 2841 metis_tac[loop2_arg_def]); 2842 2843(* 2844loop_modify_count_quitc_eqn 2845 |> SPEC_ALL |> INST_TYPE [``:'a`` |-> ``:'a # 'b``] 2846 |> SIMP_RULE (srw_ss()) [pairTheory.FORALL_PROD] 2847 |> Q.INST [`loop` |-> `(\(x,y). lp x y)`, `guard` |-> `(\(x,y). gd x y)`, 2848 `body` |-> `(\(x,y). b x y)`, `modify` |-> `(\(x,y). (t x, m y))`] 2849 |> PairRules.PBETA_RULE; 2850val it = 2851 |- WF R /\ (!p_1 p_2. ~gd p_1 p_2 ==> R (t p_1,m p_2) (p_1,p_2)) /\ 2852 (!p_1 p_2. lp p_1 p_2 = 2853 if gd p_1 p_2 then c else b p_1 p_2 + lp (t p_1) (m p_2)) ==> 2854 !p_1 p_2. (if gd p_1 p_2 then c else b p_1 p_2 + lp (t p_1) (m p_2)) = 2855 c + SUM (GENLIST 2856 (\j. 2857 b (FST (FUNPOW (\(x,y). (t x,m y)) j (p_1,p_2))) 2858 (SND (FUNPOW (\(x,y). (t x,m y)) j (p_1,p_2)))) 2859 (loop_count (\(x,y). gd x y) (\(x,y). (t x,m y)) (p_1,p_2))): thm 2860*) 2861 2862(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 2863 (!x y. loop x y = if guard x y then c else body x y + loop (transform x) (modify y)) ==> 2864 !x y. loop x y = c + SUM (GENLIST (\j. body (FUNPOW transform j x) (FUNPOW modify j y)) 2865 (loop2_count guard modify transform x y)) *) 2866(* Proof: by loop_modify_count_quitc_eqn, loop2_count_def *) 2867val loop2_modify_count_quitc_eqn = store_thm( 2868 "loop2_modify_count_quitc_eqn", 2869 ``!loop guard body c modify transform R. 2870 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 2871 (!x y. loop x y = if guard x y then c else body x y + loop (transform x) (modify y)) ==> 2872 !x y. loop x y = c + SUM (GENLIST (\j. body (FUNPOW transform j x) (FUNPOW modify j y)) 2873 (loop2_count guard modify transform x y))``, 2874 rpt strip_tac >> 2875 assume_tac (loop_modify_count_quitc_eqn 2876 |> SPEC_ALL |> INST_TYPE [``:'a`` |-> ``:'a # 'b``] 2877 |> SIMP_RULE bool_ss [pairTheory.FORALL_PROD] 2878 |> Q.INST [`loop` |-> `(\(x,y). lp x y)`, `guard` |-> `(\(x,y). gd x y)`, 2879 `body` |-> `(\(x,y). b x y)`, `modify` |-> `(\(x,y). (t x, m y))`] 2880 |> SIMP_RULE bool_ss [FUNPOW_PAIR, GSYM loop2_count_def] 2881 |> Q.INST [`lp` |-> `loop`, `gd` |-> `guard`, `b` |-> `body`, `t` |-> `transform`, `m` |-> `modify`] 2882 |> PairRules.PBETA_RULE) >> 2883 qabbrev_tac `foo1 = !x y. ~guard x y ==> R (transform x,modify y) (x,y)` >> 2884 qabbrev_tac `foo2 = !x y. loop x y = if guard x y then c else body x y + loop (transform x) (modify y)` >> 2885 metis_tac[]); 2886 2887 2888(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 2889 (!x y. loop x y = if guard x y then c else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 2890 !x y. loop x y <= c + SUM (GENLIST 2891 (\j. body (FUNPOW transform j x) (FUNPOW modify j y)) 2892 (loop2_count guard modify transform x y)) *) 2893(* Proof: by loop_modify_count_quitc_exit_le, loop2_count_def. *) 2894val loop2_modify_count_quitc_exit_le = store_thm( 2895 "loop2_modify_count_quitc_exit_le", 2896 ``!loop guard body c exit modify transform R. 2897 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 2898 (!x y. loop x y = if guard x y then c else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 2899 !x y. loop x y <= c + SUM (GENLIST 2900 (\j. body (FUNPOW transform j x) (FUNPOW modify j y)) 2901 (loop2_count guard modify transform x y))``, 2902 rpt strip_tac >> 2903 assume_tac (loop_modify_count_quitc_exit_le 2904 |> SPEC_ALL |> INST_TYPE [``:'a`` |-> ``:'a # 'b``] 2905 |> SIMP_RULE bool_ss [pairTheory.FORALL_PROD] 2906 |> Q.INST [`loop` |-> `(\(x,y). lp x y)`, `guard` |-> `(\(x,y). gd x y)`, 2907 `body` |-> `(\(x,y). b x y)`, `modify` |-> `(\(x,y). (t x, m y))`, `exit` |-> `(\(x,y). et x y)`] 2908 |> SIMP_RULE bool_ss [FUNPOW_PAIR, GSYM loop2_count_def] 2909 |> Q.INST [`lp` |-> `loop`, `gd` |-> `guard`, `et` |-> `exit`, `b` |-> `body`, `t` |-> `transform`, `m` |-> `modify`] 2910 |> PairRules.PBETA_RULE) >> 2911 qabbrev_tac `foo1 = !x y. ~guard x y ==> R (transform x,modify y) (x,y)` >> 2912 qabbrev_tac `foo2 = !x y. loop x y = if guard x y then c else body x y + if exit x y then 0 else loop (transform x) (modify y)` >> 2913 metis_tac[]); 2914 2915(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 2916 (!x y. body x y <= cover x y) /\ 2917 (!x1 x2 y1 y2. R (x1,y1) (x2,y2) ==> bcover x1 y1 <= bcover x2 y2) /\ 2918 (!x y. loop x y = if guard x y then c else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 2919 !x y. loop x y <= c + (bcover x y) * loop2_count guard modify transform x y *) 2920(* Proof: by loop_modify_count_cover_exit_upper, loop2_count_def *) 2921val loop2_modify_count_bcover_exit_upper = store_thm( 2922 "loop2_modify_count_bcover_exit_upper", 2923 ``!loop guard body c exit bcover modify transform R. 2924 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 2925 (!x y. body x y <= bcover x y) /\ 2926 (!x1 x2 y1 y2. R (x1,y1) (x2,y2) ==> bcover x1 y1 <= bcover x2 y2) /\ 2927 (!x y. loop x y = if guard x y then c else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 2928 !x y. loop x y <= c + (bcover x y) * loop2_count guard modify transform x y``, 2929 rpt strip_tac >> 2930 assume_tac (loop_modify_count_cover_exit_upper 2931 |> SPEC_ALL |> INST_TYPE [``:'a`` |-> ``:'a # 'b``] 2932 |> SIMP_RULE bool_ss [pairTheory.FORALL_PROD] 2933 |> Q.INST [`loop` |-> `(\(x,y). lp x y)`, `guard` |-> `(\(x,y). gd x y)`, `cover` |-> `(\(x,y). cv x y)`, 2934 `body` |-> `(\(x,y). b x y)`, `modify` |-> `(\(x,y). (t x, m y))`, `exit` |-> `(\(x,y). et x y)`] 2935 |> Q.INST [`lp` |-> `loop`, `gd` |-> `guard`, `et` |-> `exit`, `b` |-> `body`, `cv` |-> `bcover`, `t` |-> `transform`, `m` |-> `modify`] 2936 |> PairRules.PBETA_RULE) >> 2937 qabbrev_tac `foo1 = !x y. ~guard x y ==> R (transform x,modify y) (x,y)` >> 2938 qabbrev_tac `foo2 = !x y. body x y <= bcover x y` >> 2939 metis_tac[loop2_count_def]); 2940 2941(* Note: the most general form should involve tcover, for the transform. *) 2942 2943(* Since lifting is so complicated, just derive specific cases from this one. *) 2944 2945(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 2946 (!x1 x2 y1 y2. R (x1,y1) (x2,y2) ==> body x1 y1 <= body x2 y2) /\ 2947 (!x y. loop x y = if guard x y then c else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 2948 !x y. loop x y <= c + (body x y) * loop2_count guard modify transform x y *) 2949(* Proof: by loop2_modify_count_bcover_exit_upper, with bcover = body. *) 2950val loop2_modify_count_exit_upper = store_thm( 2951 "loop2_modify_count_exit_upper", 2952 ``!loop guard body c exit modify transform R. 2953 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 2954 (!x1 x2 y1 y2. R (x1,y1) (x2,y2) ==> body x1 y1 <= body x2 y2) /\ 2955 (!x y. loop x y = if guard x y then c else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 2956 !x y. loop x y <= c + (body x y) * loop2_count guard modify transform x y``, 2957 rpt strip_tac >> 2958 assume_tac loop2_modify_count_bcover_exit_upper >> 2959 last_x_assum (qspecl_then [`loop`, `guard`, `body`, `c`, `exit`, `body`, `modify`, `transform`, `R`] strip_assume_tac) >> 2960 metis_tac[LESS_EQ_REFL]); 2961 2962(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 2963 (!x y. body x y <= bcover x y) /\ 2964 (!x1 x2 y1 y2. R (x1,y1) (x2,y2) ==> bcover x1 y1 <= bcover x2 y2) /\ 2965 (!x y. loop x y = if guard x y then c else body x y + loop (transform x) (modify y)) ==> 2966 !x y. loop x y <= c + (bcover x y) * loop2_count guard modify transform x y *) 2967(* Proof: by loop2_modify_count_bcover_exit_upper, with exit = F. *) 2968val loop2_modify_count_bcover_upper = store_thm( 2969 "loop2_modify_count_bcover_upper", 2970 ``!loop guard body c bcover modify transform R. 2971 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 2972 (!x y. body x y <= bcover x y) /\ 2973 (!x1 x2 y1 y2. R (x1,y1) (x2,y2) ==> bcover x1 y1 <= bcover x2 y2) /\ 2974 (!x y. loop x y = if guard x y then c else body x y + loop (transform x) (modify y)) ==> 2975 !x y. loop x y <= c + (bcover x y) * loop2_count guard modify transform x y``, 2976 rpt strip_tac >> 2977 qabbrev_tac `exit = \x y. F` >> 2978 assume_tac loop2_modify_count_bcover_exit_upper >> 2979 last_x_assum (qspecl_then [`loop`, `guard`, `body`, `c`, `exit`, `bcover`, `modify`, `transform`, `R`] strip_assume_tac) >> 2980 metis_tac[]); 2981 2982(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 2983 (!x1 x2 y1 y2. R (x1,y1) (x2,y2) ==> body x1 y1 <= body x2 y2) /\ 2984 (!x y. loop x y = if guard x y then c else body x y + loop (transform x) (modify y)) ==> 2985 !x y. loop x y <= c + (bcover x y) * loop2_count guard modify transform x y *) 2986(* Proof: by loop2_modify_count_bcover_upper, with bcover = body. *) 2987val loop2_modify_count_upper = store_thm( 2988 "loop2_modify_count_upper", 2989 ``!loop guard body c modify transform R. 2990 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 2991 (!x1 x2 y1 y2. R (x1,y1) (x2,y2) ==> body x1 y1 <= body x2 y2) /\ 2992 (!x y. loop x y = if guard x y then c else body x y + loop (transform x) (modify y)) ==> 2993 !x y. loop x y <= c + (body x y) * loop2_count guard modify transform x y``, 2994 rpt strip_tac >> 2995 assume_tac loop2_modify_count_bcover_upper >> 2996 last_x_assum (qspecl_then [`loop`, `guard`, `body`, `c`, `body`, `modify`, `transform`, `R`] strip_assume_tac) >> 2997 metis_tac[LESS_EQ_REFL]); 2998 2999(* ------------------------------------------------------------------------- *) 3000(* Estimation for Numeric Loops *) 3001(* ------------------------------------------------------------------------- *) 3002 3003(* Idea: 3004 3005 From loop_modify_count_quitc_eqn, let n = loop_count guard modify x. 3006 loop x 3007 = c + SUM (GENLIST (\j. body (FUNPOW modify j x)) n) 3008 = c + [body x, body (m x), body (m (m x)), ....] for n terms 3009 If FALLING m, 3010 <= c + [body x, body x, body x, .....] if MONO body, 3011 = c + n * body x 3012 If RISING m, 3013 <= c + [body (last x), body (last x), ...] if MONO body, 3014 = c + n * body (last x) 3015*) 3016 3017(* ------------------------------------------------------------------------- *) 3018(* Numeric Loops with RISING modify *) 3019(* ------------------------------------------------------------------------- *) 3020 3021(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 3022 (!x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)) ==> 3023 !x cover. let n = loop_count guard modify x 3024 in (!x. body x <= cover x) /\ MONO cover ==> 3025 loop x <= c + n * cover (FUNPOW modify n x) *) 3026(* Proof: 3027 Let n = loop_count guard modify x, 3028 z = FUNPOW modify n x, 3029 f = (\j. body (FUNPOW modify j x)). 3030 3031 For k < n, 3032 FUNPOW modify k x <= FUNPOW modify n x by FUNPOW_LE_RISING, RISING modify 3033 = z by notation 3034 Thus, 3035 loop x 3036 <= c + SUM (GENLIST f n) by loop_modify_count_quitc_exit_le 3037 <= c + SUM (GENLIST (K (cover z)) n) by SUM_LE, EL_GENLIST, RISING modify 3038 = c + (cover z) * n by SUM_GENLIST_K 3039 = c + n * cover z by MULT_COMM 3040*) 3041val loop_rise_count_cover_quitc_exit_le = store_thm( 3042 "loop_rise_count_cover_quitc_exit_le", 3043 ``!loop guard body c exit modify transform R. 3044 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 3045 (!x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)) ==> 3046 !x cover. let n = loop_count guard modify x 3047 in (!x. body x <= cover x) /\ MONO cover ==> 3048 loop x <= c + n * cover (FUNPOW modify n x)``, 3049 rpt strip_tac >> 3050 qabbrev_tac `foo = !x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)` >> 3051 simp[] >> 3052 unabbrev_all_tac >> 3053 rpt strip_tac >> 3054 imp_res_tac loop_modify_count_quitc_exit_le >> 3055 first_x_assum (qspec_then `x` strip_assume_tac) >> 3056 qabbrev_tac `n = loop_count guard modify x` >> 3057 qabbrev_tac `z = FUNPOW modify n x` >> 3058 qabbrev_tac `f = \j. body (FUNPOW modify j x)` >> 3059 `SUM (GENLIST f n) <= SUM (GENLIST (K (cover z)) n)` by 3060 (irule SUM_LE >> 3061 rw[] >> 3062 rw[Abbr`f`, Abbr`z`] >> 3063 `FUNPOW modify k x <= FUNPOW modify n x` by rw[FUNPOW_LE_RISING] >> 3064 qabbrev_tac `u = FUNPOW modify k x` >> 3065 qabbrev_tac `v = FUNPOW modify n x` >> 3066 `body u <= cover u` by rw[] >> 3067 `cover u <= cover v` by rw[] >> 3068 decide_tac) >> 3069 `SUM (GENLIST (K (cover z)) n) = cover z * n` by rw[SUM_GENLIST_K] >> 3070 decide_tac); 3071 3072(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 3073 (!x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)) ==> 3074 !x. let n = loop_count guard modify x 3075 in MONO body ==> loop x <= c + n * body (FUNPOW modify n x) *) 3076(* Proof: by loop_rise_count_cover_quitc_exit_le with cover = body. *) 3077val loop_rise_count_exit_le = store_thm( 3078 "loop_rise_count_exit_le", 3079 ``!loop guard body c exit modify transform R. 3080 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 3081 (!x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)) ==> 3082 !x. let n = loop_count guard modify x 3083 in MONO body ==> loop x <= c + n * body (FUNPOW modify n x)``, 3084 rpt strip_tac >> 3085 imp_res_tac loop_rise_count_cover_quitc_exit_le >> 3086 first_x_assum (qspecl_then [`x`, `body`] strip_assume_tac) >> 3087 metis_tac[LESS_EQ_REFL]); 3088 3089(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 3090 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 3091 !x cover. let n = loop_count guard modify x 3092 in (!x. body x <= cover x) /\ MONO cover ==> 3093 loop x <= c + n * cover (FUNPOW modify n x) *) 3094(* Proof: by loop_rise_count_cover_quitc_exit_le with exit = F. *) 3095val loop_rise_count_cover_le = store_thm( 3096 "loop_rise_count_cover_le", 3097 ``!loop guard body c modify transform R. 3098 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 3099 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 3100 !x cover. let n = loop_count guard modify x 3101 in (!x. body x <= cover x) /\ MONO cover ==> 3102 loop x <= c + n * cover (FUNPOW modify n x)``, 3103 rpt strip_tac >> 3104 qabbrev_tac `exit = \x:num. F` >> 3105 assume_tac loop_rise_count_cover_quitc_exit_le >> 3106 first_x_assum (qspecl_then [`loop`, `guard`, `body`, `c`, `exit`, `modify`, `transform`, `R`] strip_assume_tac) >> 3107 metis_tac[]); 3108 3109(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 3110 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 3111 !x. let n = loop_count guard modify x 3112 in MONO body ==> loop x <= c + n * body (FUNPOW modify n x) *) 3113(* Proof: by loop_rise_count_cover_le with cover = body *) 3114val loop_rise_count_le = store_thm( 3115 "loop_rise_count_le", 3116 ``!loop guard body c modify transform R. 3117 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 3118 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 3119 !x. let n = loop_count guard modify x 3120 in MONO body ==> loop x <= c + n * body (FUNPOW modify n x)``, 3121 rpt strip_tac >> 3122 imp_res_tac loop_rise_count_cover_le >> 3123 first_x_assum (qspecl_then [`x`, `body`] strip_assume_tac) >> 3124 metis_tac[LESS_EQ_REFL]); 3125 3126(* ------------------------------------------------------------------------- *) 3127 3128(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 3129 (!x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)) ==> 3130 !x cover. let n = loop_count guard modify x 3131 in (!x. body x <= cover x) /\ RMONO cover ==> 3132 loop x <= c + n * cover x *) 3133(* Proof: 3134 Let n = loop_count guard modify x, 3135 u = FUNPOW modify k x, 3136 f = (\j. body (FUNPOW modify j x)). 3137 3138 For k < n, 3139 FUNPOW modify 0 x <= FUNPOW modify k x by FUNPOW_LE_RISING, RISING modify 3140 x <= u by FUNPOW_0 3141 so cover u <= cover x by RMONO cover 3142 body u <= cover u by body and cover 3143 Thus, 3144 loop x 3145 <= c + SUM (GENLIST f n) by loop_modify_count_quitc_exit_le 3146 <= c + SUM (GENLIST (K (cover x)) n) by SUM_LE, EL_GENLIST, RISING modify 3147 = c + (cover x) * n by SUM_GENLIST_K 3148 = c + n * cover x by MULT_COMM 3149*) 3150val loop_rise_count_rcover_quitc_exit_le = store_thm( 3151 "loop_rise_count_rcover_quitc_exit_le", 3152 ``!loop guard body c exit modify transform R. 3153 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 3154 (!x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)) ==> 3155 !x cover. let n = loop_count guard modify x 3156 in (!x. body x <= cover x) /\ RMONO cover ==> 3157 loop x <= c + n * cover x``, 3158 rpt strip_tac >> 3159 qabbrev_tac `foo = !x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)` >> 3160 simp[] >> 3161 unabbrev_all_tac >> 3162 rpt strip_tac >> 3163 imp_res_tac loop_modify_count_quitc_exit_le >> 3164 first_x_assum (qspec_then `x` strip_assume_tac) >> 3165 qabbrev_tac `f = \j. body (FUNPOW modify j x)` >> 3166 qabbrev_tac `n = loop_count guard modify x` >> 3167 `SUM (GENLIST f n) <= SUM (GENLIST (K (cover x)) n)` by 3168 (irule SUM_LE >> 3169 rw[] >> 3170 rw[Abbr`f`] >> 3171 `FUNPOW modify 0 x <= FUNPOW modify k x` by rw[FUNPOW_LE_RISING] >> 3172 `FUNPOW modify 0 x = x` by rw[] >> 3173 qabbrev_tac `u = FUNPOW modify k x` >> 3174 `body u <= cover u` by rw[] >> 3175 `cover u <= cover x` by rw[] >> 3176 decide_tac) >> 3177 `SUM (GENLIST (K (cover x)) n) = cover x * n` by rw[SUM_GENLIST_K] >> 3178 decide_tac); 3179 3180(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 3181 (!x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)) ==> 3182 !x. let n = loop_count guard modify x 3183 in RMONO body ==> loop x <= c + n * body x *) 3184(* Proof: by loop_rise_count_rcover_quitc_exit_le with cover = body. *) 3185val loop_rise_count_rbody_exit_le = store_thm( 3186 "loop_rise_count_rbody_exit_le", 3187 ``!loop guard body c exit modify transform R. 3188 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 3189 (!x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)) ==> 3190 !x. let n = loop_count guard modify x 3191 in RMONO body ==> loop x <= c + n * body x``, 3192 rpt strip_tac >> 3193 imp_res_tac loop_rise_count_rcover_quitc_exit_le >> 3194 first_x_assum (qspecl_then [`x`, `body`] strip_assume_tac) >> 3195 metis_tac[LESS_EQ_REFL]); 3196 3197(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 3198 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 3199 !x cover. let n = loop_count guard modify x 3200 in (!x. body x <= cover x) /\ RMONO cover ==> 3201 loop x <= c + n * cover x *) 3202(* Proof: by loop_rise_count_rcover_quitc_exit_le with exit = F. *) 3203val loop_rise_count_rcover_le = store_thm( 3204 "loop_rise_count_rcover_le", 3205 ``!loop guard body c modify transform R. 3206 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 3207 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 3208 !x cover. let n = loop_count guard modify x 3209 in (!x. body x <= cover x) /\ RMONO cover ==> 3210 loop x <= c + n * cover x``, 3211 rpt strip_tac >> 3212 qabbrev_tac `exit = \x:num. F` >> 3213 assume_tac loop_rise_count_rcover_quitc_exit_le >> 3214 first_x_assum (qspecl_then [`loop`, `guard`, `body`, `c`, `exit`, `modify`, `transform`, `R`] strip_assume_tac) >> 3215 metis_tac[]); 3216 3217(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 3218 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 3219 !x. let n = loop_count guard modify x 3220 in RMONO body ==> loop x <= c + n * body x *) 3221(* Proof: by loop_rise_count_rcover_le with cover = body. *) 3222val loop_rise_count_rbody_le = store_thm( 3223 "loop_rise_count_rbody_le", 3224 ``!loop guard body c modify transform R. 3225 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ RISING modify /\ 3226 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 3227 !x. let n = loop_count guard modify x 3228 in RMONO body ==> loop x <= c + n * body x``, 3229 rpt strip_tac >> 3230 imp_res_tac loop_rise_count_rcover_le >> 3231 first_x_assum (qspecl_then [`x`, `body`] strip_assume_tac) >> 3232 metis_tac[LESS_EQ_REFL]); 3233 3234(* ------------------------------------------------------------------------- *) 3235(* Numeric Loops with FALLING modify *) 3236(* ------------------------------------------------------------------------- *) 3237 3238(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 3239 (!x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)) ==> 3240 !x cover. let n = loop_count guard modify x 3241 in (!x. body x <= cover x) /\ MONO cover ==> 3242 loop x <= c + n * cover x *) 3243(* Proof: 3244 Let n = loop_count guard modify x, 3245 f = (\j. body (FUNPOW modify j x)). 3246 3247 For k < n, 3248 FUNPOW modify k x <= FUNPOW modify 0 x by FUNPOW_LE_FALLING, FALLING modify 3249 = x by FUNPOW_0 3250 Thus, 3251 loop x 3252 <= c + SUM (GENLIST f n) by loop_modify_count_quitc_exit_le 3253 <= c + SUM (GENLIST (K (cover x)) n) by SUM_LE, EL_GENLIST, RISING modify 3254 = c + (cover x) * n by SUM_GENLIST_K 3255 = c + n * cover x by MULT_COMM 3256*) 3257val loop_fall_count_cover_quitc_exit_le = store_thm( 3258 "loop_fall_count_cover_quitc_exit_le", 3259 ``!loop guard body c exit modify transform R. 3260 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 3261 (!x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)) ==> 3262 !x cover. let n = loop_count guard modify x 3263 in (!x. body x <= cover x) /\ MONO cover ==> 3264 loop x <= c + n * cover x``, 3265 rpt strip_tac >> 3266 qabbrev_tac `foo = !x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)` >> 3267 simp[] >> 3268 unabbrev_all_tac >> 3269 rpt strip_tac >> 3270 imp_res_tac loop_modify_count_quitc_exit_le >> 3271 first_x_assum (qspec_then `x` strip_assume_tac) >> 3272 qabbrev_tac `n = loop_count guard modify x` >> 3273 qabbrev_tac `f = \j. body (FUNPOW modify j x)` >> 3274 `SUM (GENLIST f n) <= SUM (GENLIST (K (cover x)) n)` by 3275 (irule SUM_LE >> 3276 rw[] >> 3277 rw[Abbr`f`] >> 3278 `FUNPOW modify k x <= FUNPOW modify 0 x` by rw[FUNPOW_LE_FALLING] >> 3279 `FUNPOW modify 0 x = x` by rw[] >> 3280 qabbrev_tac `u = FUNPOW modify k x` >> 3281 `body u <= cover u` by rw[] >> 3282 `cover u <= cover x` by rw[] >> 3283 decide_tac) >> 3284 `SUM (GENLIST (K (cover x)) n) = cover x * n` by rw[SUM_GENLIST_K] >> 3285 decide_tac); 3286 3287(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 3288 (!x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)) ==> 3289 !x. let n = loop_count guard modify x 3290 in MONO body ==> loop x <= c + n * body x *) 3291(* Proof: by loop_fall_count_cover_quitc_exit_le with cover = body *) 3292val loop_fall_count_exit_le = store_thm( 3293 "loop_fall_count_exit_le", 3294 ``!loop guard body c exit modify transform R. 3295 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 3296 (!x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)) ==> 3297 !x. let n = loop_count guard modify x 3298 in MONO body ==> loop x <= c + n * body x``, 3299 rpt strip_tac >> 3300 imp_res_tac loop_fall_count_cover_quitc_exit_le >> 3301 first_x_assum (qspecl_then [`x`, `body`] strip_assume_tac) >> 3302 metis_tac[LESS_EQ_REFL]); 3303 3304(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 3305 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 3306 !x cover. let n = loop_count guard modify x 3307 in (!x. body x <= cover x) /\ MONO cover ==> 3308 loop x <= c + n * cover x *) 3309(* Proof: by loop_fall_count_cover_quitc_exit_le with exit = F. *) 3310val loop_fall_count_cover_le = store_thm( 3311 "loop_fall_count_cover_le", 3312 ``!loop guard body c modify transform R. 3313 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 3314 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 3315 !x cover. let n = loop_count guard modify x 3316 in (!x. body x <= cover x) /\ MONO cover ==> 3317 loop x <= c + n * cover x``, 3318 rpt strip_tac >> 3319 qabbrev_tac `exit = \x:num. F` >> 3320 assume_tac loop_fall_count_cover_quitc_exit_le >> 3321 first_x_assum (qspecl_then [`loop`, `guard`, `body`, `c`, `exit`, `modify`, `transform`, `R`] strip_assume_tac) >> 3322 metis_tac[]); 3323 3324(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 3325 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 3326 !x. let n = loop_count guard modify x 3327 in MONO body ==> loop x <= c + n * body x *) 3328(* Proof: by loop_fall_count_cover_le with cover = body *) 3329val loop_fall_count_le = store_thm( 3330 "loop_fall_count_le", 3331 ``!loop guard body c modify transform R. 3332 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 3333 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 3334 !x. let n = loop_count guard modify x 3335 in MONO body ==> loop x <= c + n * body x``, 3336 rpt strip_tac >> 3337 imp_res_tac loop_fall_count_cover_le >> 3338 first_x_assum (qspecl_then [`x`, `body`] strip_assume_tac) >> 3339 metis_tac[LESS_EQ_REFL]); 3340 3341(* ------------------------------------------------------------------------- *) 3342 3343(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 3344 (!x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)) ==> 3345 !x cover. let n = loop_count guard modify x 3346 in (!x. body x <= cover x) /\ RMONO cover ==> 3347 loop x <= c + n * cover (FUNPOW modify n x) *) 3348(* Proof: 3349 Let n = loop_count guard modify x, 3350 u = FUNPOW modify k x, 3351 z = FUNPOW modify n x, 3352 f = (\j. body (FUNPOW modify j x)). 3353 3354 For k < n, 3355 FUNPOW modify n x <= FUNPOW modify k x by FUNPOW_LE_FALLING, FALLING modify 3356 z <= u by notation 3357 so cover u <= cover z by RMONO cover 3358 body u <= cover u by cover property 3359 Thus, 3360 loop x 3361 <= c + SUM (GENLIST f n) by loop_modify_count_quitc_exit_le 3362 <= c + SUM (GENLIST (K (cover z)) n) by SUM_LE, EL_GENLIST, RISING modify 3363 = c + (cover z) * n by SUM_GENLIST_K 3364 = c + n * cover z by MULT_COMM 3365*) 3366val loop_fall_count_rcover_quitc_exit_le = store_thm( 3367 "loop_fall_count_rcover_quitc_exit_le", 3368 ``!loop guard body c exit modify transform R. 3369 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 3370 (!x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)) ==> 3371 !x cover. let n = loop_count guard modify x 3372 in (!x. body x <= cover x) /\ RMONO cover ==> 3373 loop x <= c + n * cover (FUNPOW modify n x)``, 3374 rpt strip_tac >> 3375 qabbrev_tac `foo = !x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)` >> 3376 simp[] >> 3377 unabbrev_all_tac >> 3378 rpt strip_tac >> 3379 imp_res_tac loop_modify_count_quitc_exit_le >> 3380 first_x_assum (qspec_then `x` strip_assume_tac) >> 3381 qabbrev_tac `f = \j. body (FUNPOW modify j x)` >> 3382 qabbrev_tac `n = loop_count guard modify x` >> 3383 qabbrev_tac `z = FUNPOW modify n x` >> 3384 `SUM (GENLIST f n) <= SUM (GENLIST (K (cover z)) n)` by 3385 (irule SUM_LE >> 3386 rw[] >> 3387 rw[Abbr`f`, Abbr`z`] >> 3388 `FUNPOW modify n x <= FUNPOW modify k x` by rw[FUNPOW_LE_FALLING] >> 3389 qabbrev_tac `u = FUNPOW modify k x` >> 3390 qabbrev_tac `v = FUNPOW modify n x` >> 3391 `body u <= cover u` by rw[] >> 3392 `cover u <= cover v` by rw[] >> 3393 decide_tac) >> 3394 `SUM (GENLIST (K (cover z)) n) = cover z * n` by rw[SUM_GENLIST_K] >> 3395 decide_tac); 3396 3397(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 3398 (!x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)) ==> 3399 !x. let n = loop_count guard modify x 3400 in RMONO body ==> loop x <= c + n * body (FUNPOW modify n x) *) 3401(* Proof: by loop_fall_count_rcover_quitc_exit_le with cover = body. *) 3402val loop_fall_count_rbody_exit_le = store_thm( 3403 "loop_fall_count_rbody_exit_le", 3404 ``!loop guard body c exit modify transform R. 3405 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 3406 (!x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)) ==> 3407 !x. let n = loop_count guard modify x 3408 in RMONO body ==> loop x <= c + n * body (FUNPOW modify n x)``, 3409 rpt strip_tac >> 3410 imp_res_tac loop_fall_count_rcover_quitc_exit_le >> 3411 first_x_assum (qspecl_then [`x`, `body`] strip_assume_tac) >> 3412 metis_tac[LESS_EQ_REFL]); 3413 3414(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 3415 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 3416 !x cover. let n = loop_count guard modify x 3417 in (!x. body x <= cover x) /\ RMONO cover ==> 3418 loop x <= c + n * cover (FUNPOW modify n x) *) 3419(* Proof: by loop_fall_count_rcover_quitc_exit_le with exit = F. *) 3420val loop_fall_count_rcover_le = store_thm( 3421 "loop_fall_count_rcover_le", 3422 ``!loop guard body c modify transform R. 3423 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 3424 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 3425 !x cover. let n = loop_count guard modify x 3426 in (!x. body x <= cover x) /\ RMONO cover ==> 3427 loop x <= c + n * cover (FUNPOW modify n x)``, 3428 rpt strip_tac >> 3429 qabbrev_tac `exit = \x: num. F` >> 3430 assume_tac loop_fall_count_rcover_quitc_exit_le >> 3431 first_x_assum (qspecl_then [`loop`, `guard`, `body`, `c`, `exit`, `modify`, `transform`, `R`] strip_assume_tac) >> 3432 metis_tac[]); 3433 3434(* Theorem: WF R /\ (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 3435 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 3436 !x. let n = loop_count guard modify x 3437 in RMONO body ==> loop x <= c + n * body (FUNPOW modify n x) *) 3438(* Proof: by loop_fall_count_rcover_le with cover = body. *) 3439val loop_fall_count_rbody_le = store_thm( 3440 "loop_fall_count_rbody_le", 3441 ``!loop guard body c modify transform R. 3442 WF R /\ (!x. ~guard x ==> R (modify x) x) /\ FALLING modify /\ 3443 (!x. loop x = if guard x then c else body x + loop (modify x)) ==> 3444 !x. let n = loop_count guard modify x 3445 in RMONO body ==> loop x <= c + n * body (FUNPOW modify n x)``, 3446 rpt strip_tac >> 3447 imp_res_tac loop_fall_count_rcover_le >> 3448 first_x_assum (qspecl_then [`x`, `body`] strip_assume_tac) >> 3449 metis_tac[LESS_EQ_REFL]); 3450 3451(* ------------------------------------------------------------------------- *) 3452 3453(* Idea: 3454 3455 From loop2_modify_count_quitc_eqn, let n = loop2_count guard modify transform x y. 3456 loop x y 3457 = c + SUM (GENLIST (\j. body (FUNPOW transform j x) (FUNPOW modify j y)) n) 3458 = c + [body x y, body (t x) (m y), body (t (t x)) (m (m y)), ....] for n terms 3459 <= c + [body x y, body (t x) y, body (t (t x)) y, .....] if MONO2 body, FALLING m 3460 If FALLING t, 3461 <= c + [body x y, body x y, ....] = c + n * body x y 3462 If RISING t, 3463 <= c + [body (last x) y, body (last x) y, ...] = c + n * body (last x) y 3464 Similar estimates for RISING m 3465*) 3466 3467(* ------------------------------------------------------------------------- *) 3468(* Numeric Loops with RISING transform and FALLING modify *) 3469(* ------------------------------------------------------------------------- *) 3470 3471(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3472 RISING transform /\ FALLING modify /\ 3473 (!x y. loop x y = 3474 if guard x y then c 3475 else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 3476 !x y cover. let n = loop2_count guard modify transform x y 3477 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 3478 loop x y <= c + n * cover (FUNPOW transform n x) y *) 3479(* Proof: 3480 Let n = loop2_count guard modify transform x y, 3481 p = FUNPOW transform n x, 3482 f = (\j. body (FUNPOW transform j x) (FUNPOW modify j y)). 3483 3484 For k < n, 3485 FUNPOW transform k x <= FUNPOW transform n x by FUNPOW_LE_RISING, RISING transform 3486 = p by notation 3487 FUNPOW modify k y <= FUNPOW modify 0 y by FUNPOW_LE_FALLING, FALLING modify 3488 = y by FUNPOW_0 3489 Thus, 3490 loop x y 3491 <= c + SUM (GENLIST f n) by loop2_modify_count_quitc_exit_le 3492 <= c + SUM (GENLIST (K (cover p y)) n) by SUM_LE, EL_GENLIST, FALLING modify, RISING transform 3493 = c + (cover p y) * n by SUM_GENLIST_K 3494 = c + n * cover p y by MULT_COMM 3495*) 3496val loop2_rise_fall_count_cover_quitc_exit_le = store_thm( 3497 "loop2_rise_fall_count_cover_quitc_exit_le", 3498 ``!loop guard body c exit modify transform R. 3499 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3500 RISING transform /\ FALLING modify /\ 3501 (!x y. loop x y = 3502 if guard x y then c 3503 else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 3504 !x y cover. let n = loop2_count guard modify transform x y 3505 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 3506 loop x y <= c + n * cover (FUNPOW transform n x) y``, 3507 rpt strip_tac >> 3508 qabbrev_tac `foo = !x y. loop x y = 3509 if guard x y then c 3510 else body x y + if exit x y then 0 else loop (transform x) (modify y)` >> 3511 simp[] >> 3512 unabbrev_all_tac >> 3513 rpt strip_tac >> 3514 imp_res_tac loop2_modify_count_quitc_exit_le >> 3515 first_x_assum (qspecl_then [`y`, `x`] strip_assume_tac) >> 3516 qabbrev_tac `n = loop2_count guard modify transform x y` >> 3517 qabbrev_tac `p = FUNPOW transform n x` >> 3518 qabbrev_tac `f = \j. body (FUNPOW transform j x) (FUNPOW modify j y)` >> 3519 `SUM (GENLIST f n) <= SUM (GENLIST (K (cover p y)) n)` by 3520 (irule SUM_LE >> 3521 rw[] >> 3522 rw[Abbr`f`, Abbr`p`] >> 3523 `FUNPOW transform k x <= FUNPOW transform n x` by rw[FUNPOW_LE_RISING] >> 3524 `FUNPOW modify k y <= FUNPOW modify 0 y` by rw[FUNPOW_LE_FALLING] >> 3525 `FUNPOW modify 0 y = y` by rw[] >> 3526 qabbrev_tac `u = FUNPOW transform k x` >> 3527 qabbrev_tac `v = FUNPOW modify k y` >> 3528 `body u v <= cover u v` by rw[] >> 3529 `cover u v <= cover (FUNPOW transform n x) y` by rw[] >> 3530 decide_tac) >> 3531 `SUM (GENLIST (K (cover p y)) n) = cover p y * n` by rw[SUM_GENLIST_K] >> 3532 decide_tac); 3533 3534(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3535 RISING transform /\ FALLING modify /\ 3536 (!x y. loop x y = 3537 if guard x y then c 3538 else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 3539 !x y. let n = loop2_count guard modify transform x y 3540 in MONO2 body ==> loop x y <= c + n * body (FUNPOW transform n x) y *) 3541(* Proof: by loop2_rise_fall_count_cover_quitc_exit_le with cover = body. *) 3542val loop2_rise_fall_count_exit_le = store_thm( 3543 "loop2_rise_fall_count_exit_le", 3544 ``!loop guard body c exit modify transform R. 3545 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3546 RISING transform /\ FALLING modify /\ 3547 (!x y. loop x y = 3548 if guard x y then c 3549 else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 3550 !x y. let n = loop2_count guard modify transform x y 3551 in MONO2 body ==> loop x y <= c + n * body (FUNPOW transform n x) y``, 3552 rpt strip_tac >> 3553 imp_res_tac loop2_rise_fall_count_cover_quitc_exit_le >> 3554 first_x_assum (qspecl_then [`y`, `x`, `body`] strip_assume_tac) >> 3555 metis_tac[LESS_EQ_REFL]); 3556 3557(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3558 RISING transform /\ FALLING modify /\ 3559 (!x y. loop x y = if guard x y then c else body x y + loop (transform x) (modify y)) ==> 3560 !x y cover. let n = loop2_count guard modify transform x y 3561 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 3562 loop x y <= c + n * cover (FUNPOW transform n x) y *) 3563(* Proof: by loop2_rise_fall_count_cover_quitc_exit_le with exit = F. *) 3564val loop2_rise_fall_count_cover_le = store_thm( 3565 "loop2_rise_fall_count_cover_le", 3566 ``!loop guard body c modify transform R. 3567 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3568 RISING transform /\ FALLING modify /\ 3569 (!x y. loop x y = if guard x y then c else body x y + loop (transform x) (modify y)) ==> 3570 !x y cover. let n = loop2_count guard modify transform x y 3571 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 3572 loop x y <= c + n * cover (FUNPOW transform n x) y``, 3573 rpt strip_tac >> 3574 qabbrev_tac `exit = \x:num y:num. F` >> 3575 assume_tac loop2_rise_fall_count_cover_quitc_exit_le >> 3576 first_x_assum (qspecl_then [`loop`, `guard`, `body`, `c`, `exit`, `modify`, `transform`, `R`] strip_assume_tac) >> 3577 metis_tac[]); 3578 3579(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3580 RISING transform /\ FALLING modify /\ 3581 (!x y. loop x y = if guard x y then c else body x y + loop (transform x) (modify y)) ==> 3582 !x y. let n = loop2_count guard modify transform x y 3583 in MONO2 body ==> loop x y <= c + n * body (FUNPOW transform n x) y *) 3584(* Proof: by loop2_rise_fall_count_cover_le with cover = body. *) 3585val loop2_rise_fall_count_le = store_thm( 3586 "loop2_rise_fall_count_le", 3587 ``!loop guard body c modify transform R. 3588 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3589 RISING transform /\ FALLING modify /\ 3590 (!x y. loop x y = if guard x y then c else body x y + loop (transform x) (modify y)) ==> 3591 !x y. let n = loop2_count guard modify transform x y 3592 in MONO2 body ==> loop x y <= c + n * body (FUNPOW transform n x) y``, 3593 rpt strip_tac >> 3594 imp_res_tac loop2_rise_fall_count_cover_le >> 3595 first_x_assum (qspecl_then [`y`, `x`, `body`] strip_assume_tac) >> 3596 metis_tac[LESS_EQ_REFL]); 3597 3598(* ------------------------------------------------------------------------- *) 3599(* Numeric Loops with FALLING transform and FALLING modify *) 3600(* ------------------------------------------------------------------------- *) 3601 3602(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3603 FALLING transform /\ FALLING modify /\ 3604 (!x y. loop x y = 3605 if guard x y then c 3606 else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 3607 !x y cover. let n = loop2_count guard modify transform x y 3608 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 3609 loop x y <= c + n * cover x y *) 3610(* Proof: 3611 Let n = loop2_count guard modify transform x y, 3612 f = (\j. body (FUNPOW transform j x) (FUNPOW modify j y)). 3613 3614 For k < n, 3615 FUNPOW transform k x <= FUNPOW transform 0 x by FUNPOW_LE_FALLING, FALLING transform 3616 = x by FUNPOW_0 3617 FUNPOW modify k y <= FUNPOW modify 0 y by FUNPOW_LE_FALLING, FALLING modify 3618 = y by FUNPOW_0 3619 Thus, 3620 loop x y 3621 <= c + SUM (GENLIST f n) by loop2_modify_count_quitc_exit_le 3622 <= c + SUM (GENLIST (K (cover x y)) n) by SUM_LE, EL_GENLIST, FALLING modify, FALLING transform 3623 = c + (cover x y) * n by SUM_GENLIST_K 3624 = c + n * cover x y by MULT_COMM 3625*) 3626val loop2_fall_fall_count_cover_quitc_exit_le = store_thm( 3627 "loop2_fall_fall_count_cover_quitc_exit_le", 3628 ``!loop guard body c exit modify transform R. 3629 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3630 FALLING transform /\ FALLING modify /\ 3631 (!x y. loop x y = 3632 if guard x y then c 3633 else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 3634 !x y cover. let n = loop2_count guard modify transform x y 3635 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 3636 loop x y <= c + n * cover x y``, 3637 rpt strip_tac >> 3638 qabbrev_tac `foo = !x y. loop x y = 3639 if guard x y then c 3640 else body x y + if exit x y then 0 else loop (transform x) (modify y)` >> 3641 simp[] >> 3642 unabbrev_all_tac >> 3643 rpt strip_tac >> 3644 imp_res_tac loop2_modify_count_quitc_exit_le >> 3645 first_x_assum (qspecl_then [`y`, `x`] strip_assume_tac) >> 3646 qabbrev_tac `n = loop2_count guard modify transform x y` >> 3647 qabbrev_tac `f = \j. body (FUNPOW transform j x) (FUNPOW modify j y)` >> 3648 `SUM (GENLIST f n) <= SUM (GENLIST (K (cover x y)) n)` by 3649 (irule SUM_LE >> 3650 rw[] >> 3651 rw[Abbr`f`] >> 3652 `FUNPOW transform k x <= FUNPOW transform 0 x` by rw[FUNPOW_LE_FALLING] >> 3653 `FUNPOW modify k y <= FUNPOW modify 0 y` by rw[FUNPOW_LE_FALLING] >> 3654 `FUNPOW transform 0 x = x` by rw[] >> 3655 `FUNPOW modify 0 y = y` by rw[] >> 3656 qabbrev_tac `u = FUNPOW transform k x` >> 3657 qabbrev_tac `v = FUNPOW modify k y` >> 3658 `body u v <= cover u v` by rw[] >> 3659 `cover u v <= cover x y` by rw[] >> 3660 decide_tac) >> 3661 `SUM (GENLIST (K (cover x y)) n) = cover x y * n` by rw[SUM_GENLIST_K] >> 3662 decide_tac); 3663 3664(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3665 FALLING transform /\ FALLING modify /\ 3666 (!x y. loop x y = 3667 if guard x y then c 3668 else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 3669 !x y. let n = loop2_count guard modify transform x y 3670 in MONO2 body ==> loop x y <= c + n * body x y *) 3671(* Proof: by loop2_fall_fall_count_cover_quitc_exit_le with cover = body. *) 3672val loop2_fall_fall_count_exit_le = store_thm( 3673 "loop2_fall_fall_count_exit_le", 3674 ``!loop guard body c exit modify transform R. 3675 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3676 FALLING transform /\ FALLING modify /\ 3677 (!x y. loop x y = 3678 if guard x y then c 3679 else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 3680 !x y. let n = loop2_count guard modify transform x y 3681 in MONO2 body ==> loop x y <= c + n * body x y``, 3682 rpt strip_tac >> 3683 assume_tac loop2_fall_fall_count_cover_quitc_exit_le >> 3684 first_x_assum (qspecl_then [`loop`, `guard`, `body`, `c`, `exit`, `modify`, `transform`, `R`] strip_assume_tac) >> 3685 metis_tac[LESS_EQ_REFL]); 3686 3687(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3688 FALLING transform /\ FALLING modify /\ 3689 (!x y. loop x y = if guard x y then c else body x y + loop (transform x) (modify y)) ==> 3690 !x y cover. let n = loop2_count guard modify transform x y 3691 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 3692 loop x y <= c + n * cover x y *) 3693(* Proof: by loop2_fall_fall_count_cover_quitc_exit_le with exit = F. *) 3694val loop2_fall_fall_count_cover_le = store_thm( 3695 "loop2_fall_fall_count_cover_le", 3696 ``!loop guard body c modify transform R. 3697 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3698 FALLING transform /\ FALLING modify /\ 3699 (!x y. loop x y = if guard x y then c else body x y + loop (transform x) (modify y)) ==> 3700 !x y cover. let n = loop2_count guard modify transform x y 3701 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 3702 loop x y <= c + n * cover x y``, 3703 rpt strip_tac >> 3704 qabbrev_tac `exit = \x:num y:num. F` >> 3705 assume_tac loop2_fall_fall_count_cover_quitc_exit_le >> 3706 first_x_assum (qspecl_then [`loop`, `guard`, `body`, `c`, `exit`, `modify`, `transform`, `R`] strip_assume_tac) >> 3707 metis_tac[]); 3708 3709(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3710 FALLING transform /\ FALLING modify /\ 3711 (!x y. loop x y = if guard x y then c else body x y + loop (transform x) (modify y)) ==> 3712 !x y. let n = loop2_count guard modify transform x y 3713 in MONO2 body ==> loop x y <= c + n * body x y *) 3714(* Proof: by loop2_fall_fall_count_cover_le with cover = body *) 3715val loop2_fall_fall_count_le = store_thm( 3716 "loop2_fall_fall_count_le", 3717 ``!loop guard body c modify transform R. 3718 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3719 FALLING transform /\ FALLING modify /\ 3720 (!x y. loop x y = if guard x y then c else body x y + loop (transform x) (modify y)) ==> 3721 !x y. let n = loop2_count guard modify transform x y 3722 in MONO2 body ==> loop x y <= c + n * body x y``, 3723 rpt strip_tac >> 3724 assume_tac loop2_fall_fall_count_cover_le >> 3725 first_x_assum (qspecl_then [`loop`, `guard`, `body`, `c`, `modify`, `transform`, `R`] strip_assume_tac) >> 3726 metis_tac[LESS_EQ_REFL]); 3727 3728(* ------------------------------------------------------------------------- *) 3729(* Numeric Loops with FALLING transform and RISING modify *) 3730(* ------------------------------------------------------------------------- *) 3731 3732(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3733 FALLING transform /\ RISING modify /\ 3734 (!x y. loop x y = 3735 if guard x y then c 3736 else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 3737 !x y cover. let n = loop2_count guard modify transform x y 3738 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 3739 loop x y <= c + n * cover x (FUNPOW modify n y) *) 3740(* Proof: 3741 Let n = loop2_count guard modify transform x y, 3742 q = FUNPOW modify n y, 3743 f = (\j. body (FUNPOW transform j x) (FUNPOW modify j y)). 3744 3745 For k < n, 3746 FUNPOW transform k x <= FUNPOW transform 0 x by FUNPOW_LE_FALLING, FALLING transform 3747 = x by FUNPOW_0 3748 FUNPOW modify k y <= FUNPOW modify n y by FUNPOW_LE_RISING, RISING modify 3749 = q by notation 3750 Thus, 3751 loop x y 3752 <= c + SUM (GENLIST f n) by loop2_modify_count_quitc_exit_le 3753 <= c + SUM (GENLIST (K (cover x q)) n) by SUM_LE, EL_GENLIST, RISING modify, FALLING transform 3754 = c + (cover x q) * n by SUM_GENLIST_K 3755 = c + n * cover x q by MULT_COMM 3756*) 3757val loop2_fall_rise_count_cover_quitc_exit_le = store_thm( 3758 "loop2_fall_rise_count_cover_quitc_exit_le", 3759 ``!loop guard body c exit modify transform R. 3760 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3761 FALLING transform /\ RISING modify /\ 3762 (!x y. loop x y = 3763 if guard x y then c 3764 else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 3765 !x y cover. let n = loop2_count guard modify transform x y 3766 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 3767 loop x y <= c + n * cover x (FUNPOW modify n y)``, 3768 rpt strip_tac >> 3769 qabbrev_tac `foo = !x y. loop x y = 3770 if guard x y then c 3771 else body x y + if exit x y then 0 else loop (transform x) (modify y)` >> 3772 simp[] >> 3773 unabbrev_all_tac >> 3774 rpt strip_tac >> 3775 imp_res_tac loop2_modify_count_quitc_exit_le >> 3776 first_x_assum (qspecl_then [`y`, `x`] strip_assume_tac) >> 3777 qabbrev_tac `n = loop2_count guard modify transform x y` >> 3778 qabbrev_tac `q = FUNPOW modify n y` >> 3779 qabbrev_tac `f = \j. body (FUNPOW transform j x) (FUNPOW modify j y)` >> 3780 `SUM (GENLIST f n) <= SUM (GENLIST (K (cover x q)) n)` by 3781 (irule SUM_LE >> 3782 rw[] >> 3783 rw[Abbr`f`, Abbr`q`] >> 3784 `FUNPOW transform k x <= FUNPOW transform 0 x` by rw[FUNPOW_LE_FALLING] >> 3785 `FUNPOW modify k y <= FUNPOW modify n y` by rw[FUNPOW_LE_RISING] >> 3786 `FUNPOW transform 0 x = x` by rw[] >> 3787 qabbrev_tac `u = FUNPOW transform k x` >> 3788 qabbrev_tac `v = FUNPOW modify k y` >> 3789 `body u v <= cover u v` by rw[] >> 3790 `cover u v <= cover x (FUNPOW modify n y)` by rw[] >> 3791 decide_tac) >> 3792 `SUM (GENLIST (K (cover x q)) n) = cover x q * n` by rw[SUM_GENLIST_K] >> 3793 decide_tac); 3794 3795(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3796 FALLING transform /\ RISING modify /\ 3797 (!x y. loop x y = 3798 if guard x y then c 3799 else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 3800 !x y. let n = loop2_count guard modify transform x y 3801 in MONO2 body ==> loop x y <= c + n * body x (FUNPOW modify n y) *) 3802(* Proof: by loop2_fall_rise_count_cover_quitc_exit_le with cover = body. *) 3803val loop2_fall_rise_count_exit_le = store_thm( 3804 "loop2_fall_rise_count_exit_le", 3805 ``!loop guard body c exit modify transform R. 3806 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3807 FALLING transform /\ RISING modify /\ 3808 (!x y. loop x y = 3809 if guard x y then c 3810 else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 3811 !x y. let n = loop2_count guard modify transform x y 3812 in MONO2 body ==> loop x y <= c + n * body x (FUNPOW modify n y)``, 3813 rpt strip_tac >> 3814 imp_res_tac loop2_fall_rise_count_cover_quitc_exit_le >> 3815 first_x_assum (qspecl_then [`y`, `x`, `body`] strip_assume_tac) >> 3816 metis_tac[LESS_EQ_REFL]); 3817 3818(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3819 FALLING transform /\ RISING modify /\ 3820 (!x y. loop x y = if guard x y then c else body x y + loop (transform x) (modify y)) ==> 3821 !x y cover. let n = loop2_count guard modify transform x y 3822 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 3823 loop x y <= c + n * cover x (FUNPOW modify n y) *) 3824(* Proof: by loop2_fall_rise_count_cover_quitc_exit_le with exit = F. *) 3825val loop2_fall_rise_count_cover_le = store_thm( 3826 "loop2_fall_rise_count_cover_le", 3827 ``!loop guard body c modify transform R. 3828 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3829 FALLING transform /\ RISING modify /\ 3830 (!x y. loop x y = if guard x y then c else body x y + loop (transform x) (modify y)) ==> 3831 !x y cover. let n = loop2_count guard modify transform x y 3832 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 3833 loop x y <= c + n * cover x (FUNPOW modify n y)``, 3834 rpt strip_tac >> 3835 qabbrev_tac `exit = \x:num y:num. F` >> 3836 assume_tac loop2_fall_rise_count_cover_quitc_exit_le >> 3837 first_x_assum (qspecl_then [`loop`, `guard`, `body`, `c`, `exit`, `modify`, `transform`, `R`] strip_assume_tac) >> 3838 metis_tac[]); 3839 3840(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3841 FALLING transform /\ RISING modify /\ 3842 (!x y. loop x y = if guard x y then c else body x y + loop (transform x) (modify y)) ==> 3843 !x y. let n = loop2_count guard modify transform x y 3844 in MONO2 body ==> loop x y <= c + n * body x (FUNPOW modify n y) *) 3845(* Proof: by loop2_fall_rise_count_cover_le with cover = body. *) 3846val loop2_fall_rise_count_le = store_thm( 3847 "loop2_fall_rise_count_le", 3848 ``!loop guard body c modify transform R. 3849 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3850 FALLING transform /\ RISING modify /\ 3851 (!x y. loop x y = if guard x y then c else body x y + loop (transform x) (modify y)) ==> 3852 !x y. let n = loop2_count guard modify transform x y 3853 in MONO2 body ==> loop x y <= c + n * body x (FUNPOW modify n y)``, 3854 rpt strip_tac >> 3855 imp_res_tac loop2_fall_rise_count_cover_le >> 3856 first_x_assum (qspecl_then [`y`, `x`, `body`] strip_assume_tac) >> 3857 metis_tac[LESS_EQ_REFL]); 3858 3859(* ------------------------------------------------------------------------- *) 3860(* Numeric Loops with RISING transform and RISING modify *) 3861(* ------------------------------------------------------------------------- *) 3862 3863(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3864 RISING transform /\ RISING modify /\ 3865 (!x y. loop x y = 3866 if guard x y then c 3867 else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 3868 !x y cover. let n = loop2_count guard modify transform x y 3869 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 3870 loop x y <= c + n * cover (FUNPOW transform n x) (FUNPOW modify n y) *) 3871(* Proof: 3872 Let n = loop2_count guard modify transform x y, 3873 p = FUNPOW transform n x, 3874 q = FUNPOW modify n y, 3875 f = (\j. body (FUNPOW transform j x) (FUNPOW modify j y)). 3876 3877 For k < n, 3878 FUNPOW transform k x <= FUNPOW transform n x by FUNPOW_LE_RISING, RISING transform 3879 = p by notation 3880 FUNPOW modify k y <= FUNPOW modify n y by FUNPOW_LE_RISING, RISING modify 3881 = q by notation 3882 Thus, 3883 loop x y 3884 <= c + SUM (GENLIST f n) by loop2_modify_count_quitc_exit_le 3885 <= c + SUM (GENLIST (K (cover p q)) n) by SUM_LE, EL_GENLIST, RISING modify, RISING transform 3886 = c + (cover p q) * n by SUM_GENLIST_K 3887 = c + n * cover p q by MULT_COMM 3888*) 3889val loop2_rise_rise_count_cover_quitc_exit_le = store_thm( 3890 "loop2_rise_rise_count_cover_quitc_exit_le", 3891 ``!loop guard body c exit modify transform R. 3892 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3893 RISING transform /\ RISING modify /\ 3894 (!x y. loop x y = 3895 if guard x y then c 3896 else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 3897 !x y cover. let n = loop2_count guard modify transform x y 3898 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 3899 loop x y <= c + n * cover (FUNPOW transform n x) (FUNPOW modify n y)``, 3900 rpt strip_tac >> 3901 qabbrev_tac `foo = !x y. loop x y = 3902 if guard x y then c 3903 else body x y + if exit x y then 0 else loop (transform x) (modify y)` >> 3904 simp[] >> 3905 unabbrev_all_tac >> 3906 rpt strip_tac >> 3907 imp_res_tac loop2_modify_count_quitc_exit_le >> 3908 first_x_assum (qspecl_then [`y`, `x`] strip_assume_tac) >> 3909 qabbrev_tac `n = loop2_count guard modify transform x y` >> 3910 qabbrev_tac `p = FUNPOW transform n x` >> 3911 qabbrev_tac `q = FUNPOW modify n y` >> 3912 qabbrev_tac `f = \j. body (FUNPOW transform j x) (FUNPOW modify j y)` >> 3913 `SUM (GENLIST f n) <= SUM (GENLIST (K (cover p q)) n)` by 3914 (irule SUM_LE >> 3915 rw[] >> 3916 rw[Abbr`f`, Abbr`p`, Abbr`q`] >> 3917 `FUNPOW transform k x <= FUNPOW transform n x` by rw[FUNPOW_LE_RISING] >> 3918 `FUNPOW modify k y <= FUNPOW modify n y` by rw[FUNPOW_LE_RISING] >> 3919 qabbrev_tac `u = FUNPOW transform k x` >> 3920 qabbrev_tac `v = FUNPOW modify k y` >> 3921 `body u v <= cover u v` by rw[] >> 3922 `cover u v <= cover (FUNPOW transform n x) (FUNPOW modify n y)` by rw[] >> 3923 decide_tac) >> 3924 `SUM (GENLIST (K (cover p q)) n) = cover p q * n` by rw[SUM_GENLIST_K] >> 3925 decide_tac); 3926 3927(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3928 RISING transform /\ RISING modify /\ 3929 (!x y. loop x y = 3930 if guard x y then c 3931 else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 3932 !x y. let n = loop2_count guard modify transform x y 3933 in MONO2 body ==> 3934 loop x y <= c + n * body (FUNPOW transform n x) (FUNPOW modify n y) *) 3935(* Proof: by loop2_rise_rise_count_cover_quitc_exit_le with cover = body. *) 3936val loop2_rise_rise_count_exit_le = store_thm( 3937 "loop2_rise_rise_count_exit_le", 3938 ``!loop guard body c exit modify transform R. 3939 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3940 RISING transform /\ RISING modify /\ 3941 (!x y. loop x y = 3942 if guard x y then c 3943 else body x y + if exit x y then 0 else loop (transform x) (modify y)) ==> 3944 !x y. let n = loop2_count guard modify transform x y 3945 in MONO2 body ==> 3946 loop x y <= c + n * body (FUNPOW transform n x) (FUNPOW modify n y)``, 3947 rpt strip_tac >> 3948 assume_tac loop2_rise_rise_count_cover_quitc_exit_le >> 3949 first_x_assum (qspecl_then [`loop`, `guard`, `body`, `c`, `exit`, `modify`, `transform`, `R`] strip_assume_tac) >> 3950 metis_tac[LESS_EQ_REFL]); 3951 3952(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3953 RISING transform /\ RISING modify /\ 3954 (!x y. loop x y = if guard x y then c else body x y + loop (transform x) (modify y)) ==> 3955 !x y cover. let n = loop2_count guard modify transform x y 3956 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 3957 loop x y <= c + n * cover (FUNPOW transform n x) (FUNPOW modify n y) *) 3958(* Proof: by loop2_rise_rise_count_cover_quitc_exit_le with exit = F. *) 3959val loop2_rise_rise_count_cover_le = store_thm( 3960 "loop2_rise_rise_count_cover_le", 3961 ``!loop guard body c modify transform R. 3962 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3963 RISING transform /\ RISING modify /\ 3964 (!x y. loop x y = if guard x y then c else body x y + loop (transform x) (modify y)) ==> 3965 !x y cover. let n = loop2_count guard modify transform x y 3966 in (!x y. body x y <= cover x y) /\ MONO2 cover ==> 3967 loop x y <= c + n * cover (FUNPOW transform n x) (FUNPOW modify n y)``, 3968 rpt strip_tac >> 3969 qabbrev_tac `exit = \x:num y:num. F` >> 3970 assume_tac loop2_rise_rise_count_cover_quitc_exit_le >> 3971 first_x_assum (qspecl_then [`loop`, `guard`, `body`, `c`, `exit`, `modify`, `transform`, `R`] strip_assume_tac) >> 3972 metis_tac[]); 3973 3974(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3975 RISING transform /\ RISING modify /\ 3976 (!x y. loop x y = if guard x y then c else body x y + loop (transform x) (modify y)) ==> 3977 !x y. let n = loop2_count guard modify transform x y 3978 in MONO2 body ==> 3979 loop x y <= c + n * body (FUNPOW transform n x) (FUNPOW modify n y) *) 3980(* Proof: by loop2_rise_rise_count_cover_le with cover = body. *) 3981val loop2_rise_rise_count_le = store_thm( 3982 "loop2_rise_rise_count_le", 3983 ``!loop guard body c modify transform R. 3984 WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) /\ 3985 RISING transform /\ RISING modify /\ 3986 (!x y. loop x y = if guard x y then c else body x y + loop (transform x) (modify y)) ==> 3987 !x y. let n = loop2_count guard modify transform x y 3988 in MONO2 body ==> 3989 loop x y <= c + n * body (FUNPOW transform n x) (FUNPOW modify n y)``, 3990 rpt strip_tac >> 3991 assume_tac loop2_rise_rise_count_cover_le >> 3992 first_x_assum (qspecl_then [`loop`, `guard`, `body`, `c`, `modify`, `transform`, `R`] strip_assume_tac) >> 3993 metis_tac[LESS_EQ_REFL]); 3994 3995 3996 3997(* ------------------------------------------------------------------------- *) 3998 3999(* export theory at end *) 4000val _ = export_theory(); 4001 4002(*===========================================================================*) 4003